diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 105 |
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' | _ -> |