summaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/inductive.ml')
-rw-r--r--kernel/inductive.ml105
1 files changed, 59 insertions, 46 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index ca814f49..1f870665 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -73,7 +73,7 @@ let constructor_instantiate mind u mib c =
let s = ind_subst mind mib u in
substl s (subst_instance_constr u c)
-let instantiate_params full t args sign =
+let instantiate_params full t u args sign =
let fail () =
anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
let (rem_args, subs, ty) =
@@ -81,7 +81,8 @@ let instantiate_params full t args sign =
(fun (_,copt,_) (largs,subs,ty) ->
match (copt, largs, kind_of_term ty) with
| (None, a::args, Prod(_,_,t)) -> (args, a::subs, t)
- | (Some b,_,LetIn(_,_,_,t)) -> (largs, (substl subs b)::subs, t)
+ | (Some b,_,LetIn(_,_,_,t)) ->
+ (largs, (substl subs (subst_instance_constr u b))::subs, t)
| (_,[],_) -> if full then fail() else ([], subs, ty)
| _ -> fail ())
sign
@@ -92,15 +93,13 @@ let instantiate_params full t args sign =
let full_inductive_instantiate mib u params sign =
let dummy = prop_sort in
- let t = mkArity (sign,dummy) in
- let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in
- Vars.subst_instance_context u ar
-
-let full_constructor_instantiate ((mind,_),u,(mib,_),params) =
- let inst_ind = constructor_instantiate mind u mib in
- (fun t ->
- instantiate_params true (inst_ind t) params mib.mind_params_ctxt)
+ let t = mkArity (Vars.subst_instance_context u sign,dummy) in
+ fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
+let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
+ let inst_ind = constructor_instantiate mind u mib t in
+ instantiate_params true inst_ind u params mib.mind_params_ctxt
+
(************************************************************************)
(************************************************************************)
@@ -134,46 +133,60 @@ let sort_as_univ = function
(* Template polymorphism *)
+(* cons_subst add the mapping [u |-> su] in subst if [u] is not *)
+(* in the domain or add [u |-> sup x su] if [u] is already mapped *)
+(* to [x]. *)
let cons_subst u su subst =
- Univ.LMap.add u su subst
+ try
+ Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
+ with Not_found -> Univ.LMap.add u su subst
+
+(* remember_subst updates the mapping [u |-> x] by [u |-> sup x u] *)
+(* if it is presents and returns the substitution unchanged if not.*)
+let remember_subst u subst =
+ try
+ let su = Universe.make u in
+ Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
+ with Not_found -> subst
(* Bind expected levels of parameters to actual levels *)
(* Propagate the new levels in the signature *)
-let rec make_subst env = function
- | (_,Some _,_ as t)::sign, exp, args ->
- let ctx,subst = make_subst env (sign, exp, args) in
- t::ctx, subst
- | d::sign, None::exp, args ->
- let args = match args with _::args -> args | [] -> [] in
- let ctx,subst = make_subst env (sign, exp, args) in
- d::ctx, subst
- | d::sign, Some u::exp, a::args ->
- (* We recover the level of the argument, but we don't change the *)
- (* level in the corresponding type in the arity; this level in the *)
- (* arity is a global level which, at typing time, will be enforce *)
- (* to be greater than the level of the argument; this is probably *)
- (* a useless extra constraint *)
- let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
- let ctx,subst = make_subst env (sign, exp, args) in
- d::ctx, cons_subst u s subst
- | (na,None,t as d)::sign, Some u::exp, [] ->
- (* No more argument here: we instantiate the type with a fresh level *)
- (* which is first propagated to the corresponding premise in the arity *)
- (* (actualize_decl_level), then to the conclusion of the arity (via *)
- (* the substitution) *)
- let ctx,subst = make_subst env (sign, exp, []) in
- d::ctx, subst
- | sign, [], _ ->
- (* Uniform parameters are exhausted *)
- sign, Univ.LMap.empty
- | [], _, _ ->
- assert false
+let rec make_subst env =
+ let rec make subst = function
+ | (_,Some _,_)::sign, exp, args ->
+ make subst (sign, exp, args)
+ | d::sign, None::exp, args ->
+ let args = match args with _::args -> args | [] -> [] in
+ make subst (sign, exp, args)
+ | d::sign, Some u::exp, a::args ->
+ (* We recover the level of the argument, but we don't change the *)
+ (* level in the corresponding type in the arity; this level in the *)
+ (* arity is a global level which, at typing time, will be enforce *)
+ (* to be greater than the level of the argument; this is probably *)
+ (* a useless extra constraint *)
+ let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
+ make (cons_subst u s subst) (sign, exp, args)
+ | (na,None,t)::sign, Some u::exp, [] ->
+ (* No more argument here: we add the remaining universes to the *)
+ (* substitution (when [u] is distinct from all other universes in the *)
+ (* template, it is identity substitution otherwise (ie. when u is *)
+ (* already in the domain of the substitution) [remember_subst] will *)
+ (* update its image [x] by [sup x u] in order not to forget the *)
+ (* dependency in [u] that remains to be fullfilled. *)
+ make (remember_subst u subst) (sign, exp, [])
+ | sign, [], _ ->
+ (* Uniform parameters are exhausted *)
+ subst
+ | [], _, _ ->
+ assert false
+ in
+ make Univ.LMap.empty
exception SingletonInductiveBecomesProp of Id.t
let instantiate_universes env ctx ar argsorts =
let args = Array.to_list argsorts in
- let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in
+ let subst = make_subst env (ctx,ar.template_param_levels,args) in
let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
let ty =
(* Singleton type not containing types are interpretable in Prop *)
@@ -213,8 +226,8 @@ let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) a
let cst = instantiate_inductive_constraints mib u in
(ty, cst)
-let type_of_inductive_knowing_parameters env ?(polyprop=false) mip args =
- type_of_inductive_gen env mip args
+let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args =
+ type_of_inductive_gen ~polyprop env mip args
(* The max of an array of universes *)
@@ -331,13 +344,13 @@ let is_correct_arity env c pj ind specif params =
| Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
let env' = push_rel (na1,None,a1) env in
let ksort = match kind_of_term (whd_betadeltaiota env' a2) with
- | Sort s -> family_of_sort s
- | _ -> raise (LocalArity None) in
+ | Sort s -> family_of_sort s
+ | _ -> raise (LocalArity None) in
let dep_ind = build_dependent_inductive ind specif params in
let _ =
try conv env a1 dep_ind
with NotConvertible -> raise (LocalArity None) in
- check_allowed_sort ksort specif
+ check_allowed_sort ksort specif
| _, (_,Some _,_ as d)::ar' ->
srec (push_rel d env) (lift 1 pt') ar'
| _ ->