diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indtypes.ml | 2 | ||||
| -rw-r--r-- | kernel/inductive.ml | 40 | ||||
| -rw-r--r-- | kernel/inductive.mli | 18 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 4 | ||||
| -rw-r--r-- | kernel/typeops.ml | 10 |
5 files changed, 42 insertions, 32 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 3771454db5..b6b8e5265c 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -158,7 +158,7 @@ let ienv_push_var (env, n, ntypes, lra) (x,a,ra) = let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) = let auxntyp = 1 in let specif = (lookup_mind_specif env mi, u) in - let ty = type_of_inductive env specif in + let ty = type_of_inductive specif in let env' = let r = (snd (fst specif)).mind_relevance in let anon = Context.make_annot Anonymous r in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 5d8e1f0fdb..c6035f78ff 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -143,9 +143,16 @@ let remember_subst u subst = Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst with Not_found -> subst +type param_univs = (unit -> Universe.t) list + +let make_param_univs env argtys = + Array.map_to_list (fun arg () -> + Sorts.univ_of_sort (snd (Reduction.dest_arity env arg))) + argtys + (* Bind expected levels of parameters to actual levels *) (* Propagate the new levels in the signature *) -let make_subst env = +let make_subst = let rec make subst = function | LocalDef _ :: sign, exp, args -> make subst (sign, exp, args) @@ -158,8 +165,8 @@ let make_subst env = (* 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 = Sorts.univ_of_sort (snd (dest_arity env (Lazy.force a))) in - make (cons_subst u s subst) (sign, exp, args) + let s = a () in + make (cons_subst u s subst) (sign, exp, args) | LocalAssum (_na,_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 *) @@ -178,9 +185,8 @@ let make_subst env = exception SingletonInductiveBecomesProp of Id.t -let instantiate_universes env ctx ar argsorts = - let args = Array.to_list argsorts in - let subst = make_subst env (ctx,ar.template_param_levels,args) in +let instantiate_universes ctx ar args = + let subst = make_subst (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 *) @@ -204,13 +210,13 @@ let check_instance mib u = | Polymorphic uctx -> Instance.length u = AUContext.size uctx) then CErrors.anomaly Pp.(str "bad instance length on mutind.") -let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = +let type_of_inductive_gen ?(polyprop=true) ((mib,mip),u) paramtyps = check_instance mib u; match mip.mind_arity with | RegularArity a -> subst_instance_constr u a.mind_user_arity | TemplateArity ar -> let ctx = List.rev mip.mind_arity_ctxt in - let ctx,s = instantiate_universes env ctx ar paramtyps in + let ctx,s = instantiate_universes ctx ar paramtyps in (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. the situation where a non-Prop singleton inductive becomes Prop when applied to Prop params *) @@ -218,21 +224,21 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = then raise (SingletonInductiveBecomesProp mip.mind_typename); Term.mkArity (List.rev ctx,s) -let type_of_inductive env pind = - type_of_inductive_gen env pind [||] +let type_of_inductive pind = + type_of_inductive_gen pind [] -let constrained_type_of_inductive env ((mib,_mip),u as pind) = - let ty = type_of_inductive env pind in +let constrained_type_of_inductive ((mib,_mip),u as pind) = + let ty = type_of_inductive pind in let cst = instantiate_inductive_constraints mib u in (ty, cst) -let constrained_type_of_inductive_knowing_parameters env ((mib,_mip),u as pind) args = - let ty = type_of_inductive_gen env pind args in +let constrained_type_of_inductive_knowing_parameters ((mib,_mip),u as pind) args = + let ty = type_of_inductive_gen pind args in let cst = instantiate_inductive_constraints mib u in (ty, cst) -let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args = - type_of_inductive_gen ~polyprop env mip args +let type_of_inductive_knowing_parameters ?(polyprop=true) mip args = + type_of_inductive_gen ~polyprop mip args (* The max of an array of universes *) @@ -589,7 +595,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = let push_ind specif env = let r = specif.mind_relevance in let anon = Context.make_annot Anonymous r in - let decl = LocalAssum (anon, hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in + let decl = LocalAssum (anon, hnf_prod_applist env (type_of_inductive ((mib,specif),u)) lpar) in push_rel decl env in let env = Array.fold_right push_ind mib.mind_packets env in diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 8c40c318c5..b690fe1157 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -41,16 +41,22 @@ val inductive_paramdecls : mutual_inductive_body puniverses -> Constr.rel_contex val instantiate_inductive_constraints : mutual_inductive_body -> Instance.t -> Constraint.t -val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained +type param_univs = (unit -> Universe.t) list + +val make_param_univs : Environ.env -> constr array -> param_univs +(** The constr array is the types of the arguments to a template + polymorphic inductive. *) + +val constrained_type_of_inductive : mind_specif puniverses -> types constrained val constrained_type_of_inductive_knowing_parameters : - env -> mind_specif puniverses -> types Lazy.t array -> types constrained + mind_specif puniverses -> param_univs -> types constrained val relevance_of_inductive : env -> inductive -> Sorts.relevance -val type_of_inductive : env -> mind_specif puniverses -> types +val type_of_inductive : mind_specif puniverses -> types val type_of_inductive_knowing_parameters : - env -> ?polyprop:bool -> mind_specif puniverses -> types Lazy.t array -> types + ?polyprop:bool -> mind_specif puniverses -> param_univs -> types val elim_sort : mind_specif -> Sorts.family @@ -117,8 +123,8 @@ exception SingletonInductiveBecomesProp of Id.t val max_inductive_sort : Sorts.t array -> Universe.t -val instantiate_universes : env -> Constr.rel_context -> - template_arity -> constr Lazy.t array -> Constr.rel_context * Sorts.t +val instantiate_universes : Constr.rel_context -> + template_arity -> param_univs -> Constr.rel_context * Sorts.t (** {6 Debug} *) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 0a654adf7f..11c455de73 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -150,8 +150,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 (* nparams done *) (* params_ctxt done because part of the inductive types *) (* Don't check the sort of the type if polymorphic *) - let ty1 = type_of_inductive env ((mib1, p1), inst) in - let ty2 = type_of_inductive env ((mib2, p2), inst) in + let ty1 = type_of_inductive ((mib1, p1), inst) in + let ty2 = type_of_inductive ((mib2, p2), inst) in let cst = check_inductive_type cst p2.mind_typename ty1 ty2 in cst in diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 2a35f87db8..80accc1ced 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -372,7 +372,7 @@ let type_of_inductive_knowing_parameters env (ind,u) args = let (mib,_mip) as spec = lookup_mind_specif env ind in check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters - env (spec,u) args + (spec,u) (Inductive.make_param_univs env args) in check_constraints cst env; t @@ -380,7 +380,7 @@ let type_of_inductive_knowing_parameters env (ind,u) args = let type_of_inductive env (ind,u) = let (mib,mip) = lookup_mind_specif env ind in check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; - let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in + let t,cst = Inductive.constrained_type_of_inductive ((mib,mip),u) in check_constraints cst env; t @@ -461,8 +461,7 @@ let type_of_global_in_context env r = let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in let univs = Declareops.inductive_polymorphic_context mib in let inst = Univ.make_abstract_instance univs in - let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in - Inductive.type_of_inductive env (specif, inst), univs + Inductive.type_of_inductive (specif, inst), univs | ConstructRef cstr -> let (mib,_ as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) @@ -515,8 +514,7 @@ let rec execute env cstr = let f', ft = match kind f with | Ind ind when Environ.template_polymorphic_pind ind env -> - let args = Array.map (fun t -> lazy t) argst in - f, type_of_inductive_knowing_parameters env ind args + f, type_of_inductive_knowing_parameters env ind argst | _ -> (* No template polymorphism *) execute env f |