diff options
41 files changed, 403 insertions, 298 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 5fa01e5db..589a26134 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -165,18 +165,37 @@ let constr_of_def = function | Def cs -> Mod_subst.force_constr cs | OpaqueDef lc -> Opaqueproof.force_proof lc +let expmod_constr_subst cache modlist subst c = + let c = expmod_constr cache modlist c in + Vars.subst_univs_level_constr subst c let cook_constr { Opaqueproof.modlist ; abstract } c = let cache = RefTable.create 13 in - let hyps = Context.map_named_context (expmod_constr cache modlist) (fst abstract) in - abstract_constant_body (expmod_constr cache modlist c) hyps + let expmod = expmod_constr_subst cache modlist (pi2 abstract) in + let hyps = Context.map_named_context expmod (pi1 abstract) in + abstract_constant_body (expmod c) hyps + +let lift_univs cb subst = + if cb.const_polymorphic then + let inst = Univ.UContext.instance cb.const_universes in + let cstrs = Univ.UContext.constraints cb.const_universes in + let len = Univ.LMap.cardinal subst in + let subst = + Array.fold_left_i (fun i acc v -> Univ.LMap.add (Level.var i) (Level.var (i + len)) acc) + subst (Univ.Instance.to_array inst) + in + let cstrs' = Univ.subst_univs_level_constraints subst cstrs in + subst, Univ.UContext.make (inst,cstrs') + else subst, cb.const_universes let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } = let cache = RefTable.create 13 in - let abstract, abs_ctx = abstract in - let hyps = Context.map_named_context (expmod_constr cache modlist) abstract in - let body = on_body modlist (hyps, abs_ctx) - (fun c -> abstract_constant_body (expmod_constr cache modlist c) hyps) + let abstract, usubst, abs_ctx = abstract in + let usubst, univs = lift_univs cb usubst in + let expmod = expmod_constr_subst cache modlist usubst in + let hyps = Context.map_named_context expmod abstract in + let body = on_body modlist (hyps, usubst, abs_ctx) + (fun c -> abstract_constant_body (expmod c) hyps) cb.const_body in let const_hyps = @@ -186,17 +205,16 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } = let typ = match cb.const_type with | RegularArity t -> let typ = - abstract_constant_type (expmod_constr cache modlist t) hyps in + abstract_constant_type (expmod t) hyps in RegularArity typ | TemplateArity (ctx,s) -> let t = mkArity (ctx,Type s.template_level) in - let typ = - abstract_constant_type (expmod_constr cache modlist t) hyps in + let typ = abstract_constant_type (expmod t) hyps in let j = make_judge (constr_of_def body) typ in Typeops.make_polymorphic_if_constant_for_ind env j in let projection pb = - let c' = abstract_constant_body (expmod_constr cache modlist pb.proj_body) hyps in + let c' = abstract_constant_body (expmod pb.proj_body) hyps in let ((mind, _), _), n' = try let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in @@ -213,7 +231,7 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } = { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg; proj_type = ty'; proj_body = c' } in - let univs = UContext.union abs_ctx cb.const_universes in + let univs = UContext.union abs_ctx univs in (body, typ, Option.map projection cb.const_proj, cb.const_polymorphic, univs, cb.const_inline_code, Some const_hyps) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 4524b55bb..f583bff64 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -37,10 +37,22 @@ let hcons_template_arity ar = (** {6 Constants } *) +let instantiate cb c = + if cb.const_polymorphic then + Vars.subst_instance_constr (Univ.UContext.instance cb.const_universes) c + else c + let body_of_constant cb = match cb.const_body with | Undef _ -> None - | Def c -> Some (force_constr c) - | OpaqueDef o -> Some (Opaqueproof.force_proof o) + | Def c -> Some (instantiate cb (force_constr c)) + | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof o)) + +let type_of_constant cb = + match cb.const_type with + | RegularArity t as x -> + let t' = instantiate cb t in + if t' == t then x else RegularArity t' + | TemplateArity _ as x -> x let constraints_of_constant cb = Univ.Constraint.union (Univ.UContext.constraints cb.const_universes) @@ -57,7 +69,9 @@ let universes_of_constant cb = (Univ.ContextSet.to_context (Opaqueproof.force_constraints o)) let universes_of_polymorphic_constant cb = - if cb.const_polymorphic then universes_of_constant cb + if cb.const_polymorphic then + let univs = universes_of_constant cb in + Univ.instantiate_univ_context univs else Univ.UContext.empty let constant_has_body cb = match cb.const_body with diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 6c43bffa9..04a067aff 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -29,6 +29,7 @@ val constant_has_body : constant_body -> bool Only use this function if you know what you're doing. *) val body_of_constant : constant_body -> Term.constr option +val type_of_constant : constant_body -> constant_type val constraints_of_constant : constant_body -> Univ.constraints val universes_of_constant : constant_body -> Univ.universe_context diff --git a/kernel/environ.ml b/kernel/environ.ml index 48a7964c3..2a4f3a948 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -212,13 +212,9 @@ let add_constant_key kn cb linkinfo env = let add_constant kn cb env = add_constant_key kn cb (no_link_info ()) env -let universes_of cb = - cb.const_universes - -let universes_and_subst_of cb u = - let univs = universes_of cb in - let subst = Univ.make_universe_subst u univs in - subst, Univ.instantiate_univ_context subst univs +let constraints_of cb u = + let univs = cb.const_universes in + Univ.subst_instance_constraints u (Univ.UContext.constraints univs) let map_regular_arity f = function | RegularArity a as ar -> @@ -230,8 +226,8 @@ let map_regular_arity f = function let constant_type env (kn,u) = let cb = lookup_constant kn env in if cb.const_polymorphic then - let subst, csts = universes_and_subst_of cb u in - (map_regular_arity (subst_univs_level_constr subst) cb.const_type, csts) + let csts = constraints_of cb u in + (map_regular_arity (subst_instance_constr u) cb.const_type, csts) else cb.const_type, Univ.Constraint.empty let constant_context env kn = @@ -249,8 +245,8 @@ let constant_value env (kn,u) = match cb.const_body with | Def l_body -> if cb.const_polymorphic then - let subst, csts = universes_and_subst_of cb u in - (subst_univs_level_constr subst (Mod_subst.force_constr l_body), csts) + let csts = constraints_of cb u in + (subst_instance_constr u (Mod_subst.force_constr l_body), csts) else Mod_subst.force_constr l_body, Univ.Constraint.empty | OpaqueDef _ -> raise (NotEvaluableConst Opaque) | Undef _ -> raise (NotEvaluableConst NoBody) @@ -263,13 +259,13 @@ let constant_opt_value env cst = let constant_value_and_type env (kn, u) = let cb = lookup_constant kn env in if cb.const_polymorphic then - let subst, cst = universes_and_subst_of cb u in + let cst = constraints_of cb u in let b' = match cb.const_body with - | Def l_body -> Some (subst_univs_level_constr subst (Mod_subst.force_constr l_body)) + | Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body)) | OpaqueDef _ -> None | Undef _ -> None in - b', map_regular_arity (subst_univs_level_constr subst) cb.const_type, cst + b', map_regular_arity (subst_instance_constr u) cb.const_type, cst else let b' = match cb.const_body with | Def l_body -> Some (Mod_subst.force_constr l_body) @@ -285,8 +281,7 @@ let constant_value_and_type env (kn, u) = let constant_type_in env (kn,u) = let cb = lookup_constant kn env in if cb.const_polymorphic then - let subst = Univ.make_universe_subst u cb.const_universes in - map_regular_arity (subst_univs_level_constr subst) cb.const_type + map_regular_arity (subst_instance_constr u) cb.const_type else cb.const_type let constant_value_in env (kn,u) = @@ -294,10 +289,7 @@ let constant_value_in env (kn,u) = match cb.const_body with | Def l_body -> let b = Mod_subst.force_constr l_body in - if cb.const_polymorphic then - let subst = Univ.make_universe_subst u cb.const_universes in - subst_univs_level_constr subst b - else b + subst_instance_constr u b | OpaqueDef _ -> raise (NotEvaluableConst Opaque) | Undef _ -> raise (NotEvaluableConst NoBody) diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index 83f1e74ba..a88302e04 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -302,8 +302,7 @@ let judge_of_projection env p c ct = with Not_found -> error_case_not_inductive env (make_judge c ct) in assert(eq_mind pb.proj_ind (fst ind)); - let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in - let ty = Vars.subst_univs_level_constr usubst pb.Declarations.proj_type in + let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in substl (c :: List.rev args) ty diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 89d2d7b67..ff5ce284e 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -683,12 +683,20 @@ let compute_expansion ((kn, _ as ind), u) params ctx = let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in (* Compute the set of used section variables *) - let hyps = used_section_variables env inds in + let hyps = used_section_variables env inds in let nparamargs = rel_context_nhyps params in let nparamdecls = rel_context_length params in + let subst, ctx = Univ.abstract_universes p ctx in + let params = Vars.subst_univs_level_context subst params in + let env_ar = + let ctx = Environ.rel_context env_ar in + let ctx' = Vars.subst_univs_level_context subst ctx in + Environ.push_rel_context ctx' env + in (* Check one inductive *) let build_one_packet (id,cnames,lc,(ar_sign,ar_kind)) recarg = (* Type of constructors in normal form *) + let lc = Array.map (Vars.subst_univs_level_constr subst) lc in let splayed_lc = Array.map (dest_prod_assum env_ar) lc in let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in let consnrealdecls = @@ -707,7 +715,8 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re let s = sort_of_univ defs in let kelim = allowed_sorts info s in let ar = RegularArity - { mind_user_arity = ar; mind_sort = s; } in + { mind_user_arity = Vars.subst_univs_level_constr subst ar; + mind_sort = sort_of_univ (Univ.subst_univs_level_universe subst defs); } in ar, kelim in (* Assigning VM tags to constructors *) let nconst, nblock = ref 0, ref 0 in @@ -726,7 +735,7 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re (* Build the inductive packet *) { mind_typename = id; mind_arity = arkind; - mind_arity_ctxt = ar_sign; + mind_arity_ctxt = Vars.subst_univs_level_context subst ar_sign; mind_nrealargs = rel_context_nhyps ar_sign - nparamargs; mind_nrealdecls = rel_context_length ar_sign - nparamdecls; mind_kelim = kelim; diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 163bc3a42..dfed98071 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -50,28 +50,22 @@ let find_coinductive env c = let inductive_params (mib,_) = mib.mind_nparams -let make_inductive_subst mib u = - if mib.mind_polymorphic then - make_universe_subst u mib.mind_universes - else Univ.empty_level_subst - let inductive_paramdecls (mib,u) = - let subst = make_inductive_subst mib u in - Vars.subst_univs_level_context subst mib.mind_params_ctxt + Vars.subst_instance_context u mib.mind_params_ctxt let inductive_instance mib = - if mib.mind_polymorphic then + if mib.mind_polymorphic then UContext.instance mib.mind_universes else Instance.empty let inductive_context mib = if mib.mind_polymorphic then - mib.mind_universes + instantiate_univ_context mib.mind_universes else UContext.empty -let instantiate_inductive_constraints mib subst = +let instantiate_inductive_constraints mib u = if mib.mind_polymorphic then - instantiate_univ_context subst mib.mind_universes + subst_instance_constraints u (UContext.constraints mib.mind_universes) else Constraint.empty (************************************************************************) @@ -84,9 +78,9 @@ let ind_subst mind mib u = List.init ntypes make_Ik (* Instantiate inductives in constructor type *) -let constructor_instantiate mind u subst mib c = +let constructor_instantiate mind u mib c = let s = ind_subst mind mib u in - substl s (subst_univs_level_constr subst c) + substl s (subst_instance_constr u c) let instantiate_params full t args sign = let fail () = @@ -108,13 +102,11 @@ 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 subst = make_inductive_subst mib u in let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in - Vars.subst_univs_level_context subst ar + Vars.subst_instance_context u ar let full_constructor_instantiate ((mind,_),u,(mib,_),params) = - let subst = make_inductive_subst mib u in - let inst_ind = constructor_instantiate mind u subst mib in + let inst_ind = constructor_instantiate mind u mib in (fun t -> instantiate_params true (inst_ind t) params mib.mind_params_ctxt) @@ -204,30 +196,9 @@ let instantiate_universes env ctx ar argsorts = (* Type of an inductive type *) -let type_of_inductive_subst ?(polyprop=true) env ((mib,mip),u) paramtyps = - match mip.mind_arity with - | RegularArity a -> - if not mib.mind_polymorphic then (a.mind_user_arity, Univ.LMap.empty) - else - let subst = make_inductive_subst mib u in - (subst_univs_level_constr subst a.mind_user_arity, subst) - | TemplateArity ar -> - let ctx = List.rev mip.mind_arity_ctxt in - let ctx,s = instantiate_universes env 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 *) - if not polyprop && not (is_type0m_univ ar.template_level) && is_prop_sort s - then raise (SingletonInductiveBecomesProp mip.mind_typename); - mkArity (List.rev ctx,s), Univ.LMap.empty - let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = match mip.mind_arity with - | RegularArity a -> - if not mib.mind_polymorphic then a.mind_user_arity - else - let subst = make_inductive_subst mib u in - (subst_univs_level_constr subst a.mind_user_arity) + | 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 @@ -242,13 +213,13 @@ let type_of_inductive env pind = type_of_inductive_gen env pind [||] let constrained_type_of_inductive env ((mib,mip),u as pind) = - let ty, subst = type_of_inductive_subst env pind [||] in - let cst = instantiate_inductive_constraints mib subst in + let ty = type_of_inductive env 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, subst = type_of_inductive_subst env pind args in - let cst = instantiate_inductive_constraints mib subst in + let ty = type_of_inductive_gen env pind args in + let cst = instantiate_inductive_constraints mib u in (ty, cst) let type_of_inductive_knowing_parameters env ?(polyprop=false) mip args = @@ -267,44 +238,29 @@ let max_inductive_sort = (************************************************************************) (* Type of a constructor *) -let type_of_constructor_subst cstr u subst (mib,mip) = +let type_of_constructor (cstr, u) (mib,mip) = let ind = inductive_of_constructor cstr in let specif = mip.mind_user_lc in let i = index_of_constructor cstr in let nconstr = Array.length mip.mind_consnames in if i > nconstr then error "Not enough constructors in the type."; - let c = constructor_instantiate (fst ind) u subst mib specif.(i-1) in - c - -let type_of_constructor_gen (cstr,u) (mib,mip as mspec) = - let subst = make_inductive_subst mib u in - type_of_constructor_subst cstr u subst mspec, subst - -let type_of_constructor cstru mspec = - fst (type_of_constructor_gen cstru mspec) - -let type_of_constructor_in_ctx cstr (mib,mip as mspec) = - let u = UContext.instance mib.mind_universes in - let c = type_of_constructor_gen (cstr, u) mspec in - (fst c, mib.mind_universes) + constructor_instantiate (fst ind) u mib specif.(i-1) let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) = - let ty, subst = type_of_constructor_gen cstru ind in - let cst = instantiate_inductive_constraints mib subst in + let ty = type_of_constructor cstru ind in + let cst = instantiate_inductive_constraints mib u in (ty, cst) let arities_of_specif (kn,u) (mib,mip) = let specif = mip.mind_nf_lc in - let subst = make_inductive_subst mib u in - Array.map (constructor_instantiate kn u subst mib) specif + Array.map (constructor_instantiate kn u mib) specif let arities_of_constructors ind specif = arities_of_specif (fst (fst ind), snd ind) specif let type_of_constructors (ind,u) (mib,mip) = let specif = mip.mind_user_lc in - let subst = make_inductive_subst mib u in - Array.map (constructor_instantiate (fst ind) u subst mib) specif + Array.map (constructor_instantiate (fst ind) u mib) specif (************************************************************************) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 8bd1a5605..9140d171d 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -35,14 +35,12 @@ val lookup_mind_specif : env -> inductive -> mind_specif (** {6 Functions to build standard types related to inductive } *) val ind_subst : mutual_inductive -> mutual_inductive_body -> universe_instance -> constr list -val make_inductive_subst : mutual_inductive_body -> universe_instance -> universe_level_subst - val inductive_instance : mutual_inductive_body -> universe_instance val inductive_context : mutual_inductive_body -> universe_context val inductive_paramdecls : mutual_inductive_body puniverses -> rel_context val instantiate_inductive_constraints : - mutual_inductive_body -> universe_level_subst -> constraints + mutual_inductive_body -> universe_instance -> constraints val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained val constrained_type_of_inductive_knowing_parameters : @@ -59,7 +57,6 @@ val elim_sorts : mind_specif -> sorts_family list val constrained_type_of_constructor : pconstructor -> mind_specif -> types constrained val type_of_constructor : pconstructor -> mind_specif -> types -val type_of_constructor_in_ctx : constructor -> mind_specif -> types in_universe_context (** Return constructor types in normal form *) val arities_of_constructors : pinductive -> mind_specif -> types array diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 7aed4bf50..a5def3dc8 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -16,7 +16,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t * type cooking_info = { modlist : work_list; - abstract : Context.named_context in_universe_context } + abstract : Context.named_context * Univ.universe_level_subst * Univ.UContext.t } type proofterm = (constr * Univ.universe_context_set) Future.computation type opaque = | Indirect of substitution list * DirPath.t * int (* subst, lib, index *) diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 3e45f65b4..092f0aeb1 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -43,7 +43,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t * type cooking_info = { modlist : work_list; - abstract : Context.named_context Univ.in_universe_context } + abstract : Context.named_context * Univ.universe_level_subst * Univ.UContext.t } (* The type has two caveats: 1) cook_constr is defined after diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 0578d35fc..71a6b7a39 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -363,15 +363,6 @@ let constraints_of_sfb sfb = | SFBmodtype mtb -> [Now mtb.typ_constraints] | SFBmodule mb -> [Now mb.mod_constraints] -(* let add_constraints cst senv = *) -(* { senv with *) -(* env = Environ.add_constraints cst senv.env; *) -(* univ = Univ.Constraint.union cst senv.univ } *) - -(* let next_universe senv = *) -(* let univ = senv.max_univ in *) -(* univ + 1, { senv with max_univ = univ + 1 } *) - (** A generic function for adding a new field in a same environment. It also performs the corresponding [add_constraints]. *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 9f30b7da3..c44adad5c 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -24,21 +24,21 @@ open Entries open Typeops open Fast_typeops -let constrain_type env j poly = function +let constrain_type env j poly subst = function | `None -> if not poly then (* Old-style polymorphism *) make_polymorphic_if_constant_for_ind env j - else RegularArity j.uj_type + else RegularArity (Vars.subst_univs_level_constr subst j.uj_type) | `Some t -> let tj = infer_type env t in let _ = judge_of_cast env j DEFAULTcast tj in assert (eq_constr t tj.utj_val); - RegularArity t + RegularArity (Vars.subst_univs_level_constr subst t) | `SomeWJ (t, tj) -> let tj = infer_type env t in let _ = judge_of_cast env j DEFAULTcast tj in assert (eq_constr t tj.utj_val); - RegularArity t + RegularArity (Vars.subst_univs_level_constr subst t) let map_option_typ = function None -> `None | Some x -> `Some x @@ -65,11 +65,12 @@ let handle_side_effects env body side_eff = | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub c i x) i x in let rec sub_body c u b i x = match kind_of_term x with | Const (c',u') when eq_constant c c' -> - let subst = - Array.fold_left2 (fun subst l l' -> Univ.LMap.add l l' subst) - Univ.LMap.empty (Instance.to_array u) (Instance.to_array u') - in - Vars.subst_univs_level_constr subst b + (* let subst = *) + (* Array.fold_left2 (fun subst l l' -> Univ.LMap.add l l' subst) *) + (* Univ.LMap.empty (Instance.to_array u) (Instance.to_array u') *) + (* in *) + (* Vars.subst_univs_level_constr subst b *) + Vars.subst_instance_constr u' b | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub_body c u b i x) i x in let fix_body (c,cb) t = match cb.const_body with @@ -107,7 +108,7 @@ let hcons_j j = let feedback_completion_typecheck = Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete) -let check_projection env kn inst body = +let check_projection env kn usubst body = let cannot_recognize () = error ("Cannot recognize a projection") in let ctx, m = decompose_lam_assum body in let () = if not (isCase m) then cannot_recognize () in @@ -136,19 +137,27 @@ let check_projection env kn inst body = let pb = { proj_ind = fst ci.ci_ind; proj_npars = n; proj_arg = arg; - proj_type = ty; - proj_body = body } + proj_type = Vars.subst_univs_level_constr usubst ty; + proj_body = Vars.subst_univs_level_constr usubst body } in pb +let subst_instance_j s j = + { uj_val = Vars.subst_univs_level_constr s j.uj_val; + uj_type = Vars.subst_univs_level_constr s j.uj_type } + let infer_declaration env kn dcl = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> let env = push_context uctx env in let j = infer env t in - let t = hcons_constr (Typeops.assumption_of_judgment env j) in - Undef nl, RegularArity t, None, poly, uctx, false, ctx + let abstract = poly && not (Option.is_empty kn) in + let usubst, univs = Univ.abstract_universes abstract uctx in + let c = Typeops.assumption_of_judgment env j in + let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in + Undef nl, RegularArity t, None, poly, univs, false, ctx | DefinitionEntry ({ const_entry_type = Some typ; - const_entry_opaque = true } as c) -> + const_entry_opaque = true; + const_entry_polymorphic = false} as c) -> let env = push_context c.const_entry_universes env in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in @@ -158,7 +167,9 @@ let infer_declaration env kn dcl = let env' = push_context_set ctx env in let j = infer env' body in let j = hcons_j j in - let _typ = constrain_type env' j c.const_entry_polymorphic (`SomeWJ (typ,tyj)) in + let subst = Univ.LMap.empty in + let _typ = constrain_type env' j c.const_entry_polymorphic subst + (`SomeWJ (typ,tyj)) in feedback_completion_typecheck feedback_id; j.uj_val, ctx) in let def = OpaqueDef (Opaqueproof.create proofterm) in @@ -172,28 +183,28 @@ let infer_declaration env kn dcl = let (body, ctx), side_eff = Future.join body in assert(Univ.ContextSet.is_empty ctx); let body = handle_side_effects env body side_eff in + let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in + let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in let def, typ, proj = if c.const_entry_proj then (** This should be the projection defined as a match. *) let j = infer env body in - let typ = constrain_type env j c.const_entry_polymorphic (map_option_typ typ) in + let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in (** We check it does indeed have the shape of a projection. *) - let inst = Univ.UContext.instance c.const_entry_universes in - let pb = check_projection env (Option.get kn) inst body in + let pb = check_projection env (Option.get kn) usubst body in (** We build the eta-expanded form. *) let context, m = decompose_lam_n_assum (pb.proj_npars + 1) body in let body' = mkProj (Option.get kn, mkRel 1) in let body = it_mkLambda_or_LetIn body' context in - Def (Mod_subst.from_val (hcons_constr body)), + Def (Mod_subst.from_val (hcons_constr (Vars.subst_univs_level_constr usubst body))), typ, Some pb else let j = infer env body in - let j = hcons_j j in - let typ = constrain_type env j c.const_entry_polymorphic (map_option_typ typ) in - let def = Def (Mod_subst.from_val j.uj_val) in + let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in + let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in + let def = Def (Mod_subst.from_val def) in def, typ, None in - let univs = c.const_entry_universes in feedback_completion_typecheck feedback_id; def, typ, proj, c.const_entry_polymorphic, univs, c.const_entry_inline_code, c.const_entry_secctx diff --git a/kernel/typeops.ml b/kernel/typeops.ml index cd1f2c856..cb0c429a9 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -189,9 +189,7 @@ let type_of_projection env (cst,u) = match cb.const_proj with | Some pb -> if cb.const_polymorphic then - let mib,_ = lookup_mind_specif env (pb.proj_ind,0) in - let subst = make_inductive_subst mib u in - Vars.subst_univs_level_constr subst pb.proj_type + Vars.subst_instance_constr u pb.proj_type else pb.proj_type | None -> raise (Invalid_argument "type_of_projection: not a projection") @@ -388,8 +386,7 @@ let judge_of_projection env p cj = with Not_found -> error_case_not_inductive env cj in assert(eq_mind pb.proj_ind (fst ind)); - let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in - let ty = Vars.subst_univs_level_constr usubst pb.Declarations.proj_type in + let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in let ty = substl (cj.uj_val :: List.rev args) ty in (* TODO: Universe polymorphism for projections *) {uj_val = mkProj (p,cj.uj_val); diff --git a/kernel/univ.ml b/kernel/univ.ml index 4adc1e683..2fd94e1a9 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -254,6 +254,7 @@ struct | Prop | Set | Level of int * DirPath.t + | Var of int (* Hash-consing *) @@ -264,6 +265,7 @@ struct | Set, Set -> true | Level (n,d), Level (n',d') -> Int.equal n n' && DirPath.equal d d' + | Var n, Var n' -> true | _ -> false let compare u v = @@ -278,20 +280,26 @@ struct if i1 < i2 then -1 else if i1 > i2 then 1 else DirPath.compare dp1 dp2 - + | Level _, _ -> -1 + | _, Level _ -> 1 + | Var n, Var m -> Int.compare n m + let hcons = function | Prop as x -> x | Set as x -> x | Level (n,d) as x -> let d' = Names.DirPath.hcons d in if d' == d then x else Level (n,d') + | Var n as x -> x open Hashset.Combine let hash = function | Prop -> combinesmall 1 0 | Set -> combinesmall 1 1 - | Level (n, d) -> combinesmall 2 (combine n (Names.DirPath.hash d)) + | Var n -> combinesmall 2 n + | Level (n, d) -> combinesmall 3 (combine n (Names.DirPath.hash d)) + end module Level = struct @@ -302,6 +310,7 @@ module Level = struct | Prop | Set | Level of int * DirPath.t + | Var of int (** Embed levels with their hash value *) type t = { @@ -365,6 +374,7 @@ module Level = struct | Prop -> "Prop" | Set -> "Set" | Level (n,d) -> Names.DirPath.to_string d^"."^string_of_int n + | Var n -> "Var(" ^ string_of_int n ^ ")" let pr u = str (to_string u) @@ -373,6 +383,10 @@ module Level = struct | Prop, Set | Set, Prop -> true | _ -> false + let vars = Array.init 20 (fun i -> make (Var i)) + + let var n = + if n < 20 then vars.(n) else make (Var n) let make m n = make (Level (n, Names.DirPath.hcons m)) @@ -1690,7 +1704,7 @@ let level_subst_of f = with Not_found -> l module Instance : sig - type t + type t = Level.t array val empty : t val is_empty : t -> bool @@ -1894,12 +1908,6 @@ type 'a in_universe_context_set = 'a * universe_context_set (** Substitutions. *) -let make_universe_subst inst (ctx, csts) = - try Array.fold_left2 (fun acc c i -> LMap.add c i acc) - LMap.empty (Instance.to_array ctx) (Instance.to_array inst) - with Invalid_argument _ -> - anomaly (Pp.str "Mismatched instance and context when building universe substitution") - let empty_subst = LMap.empty let is_empty_subst = LMap.is_empty @@ -1930,10 +1938,6 @@ let subst_univs_level_constraints subst csts = (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c)) csts Constraint.empty -(** Substitute instance inst for ctx in csts *) -let instantiate_univ_context subst (_, csts) = - subst_univs_level_constraints subst csts - (** With level to universe substitutions. *) type universe_subst_fn = universe_level -> universe @@ -1976,6 +1980,62 @@ let subst_univs_constraints subst csts = (fun c cstrs -> subst_univs_constraint subst c cstrs) csts Constraint.empty + +let subst_instance_level s l = + match l.Level.data with + | Level.Var n -> s.(n) + | _ -> l + +let subst_instance_instance s i = + Array.smartmap (fun l -> subst_instance_level s l) i + +let subst_instance_universe s u = + let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in + let u' = Universe.smartmap f u in + if u == u' then u + else Universe.sort u' + +let subst_instance_constraint s (u,d,v as c) = + let u' = subst_instance_level s u in + let v' = subst_instance_level s v in + if u' == u && v' == v then c + else (u',d,v') + +let subst_instance_constraints s csts = + Constraint.fold + (fun c csts -> Constraint.add (subst_instance_constraint s c) csts) + csts Constraint.empty + +(** Substitute instance inst for ctx in csts *) +let instantiate_univ_context (ctx, csts) = + (ctx, subst_instance_constraints ctx csts) + +let instantiate_univ_constraints u (_, csts) = + subst_instance_constraints u csts + +let make_instance_subst i = + let arr = Instance.to_array i in + Array.fold_left_i (fun i acc l -> + LMap.add l (Level.var i) acc) + LMap.empty arr + +let make_inverse_instance_subst i = + let arr = Instance.to_array i in + Array.fold_left_i (fun i acc l -> + LMap.add (Level.var i) l acc) + LMap.empty arr + +let abstract_universes poly ctx = + let instance = UContext.instance ctx in + if poly then + let subst = make_instance_subst instance in + let cstrs = subst_univs_level_constraints subst + (UContext.constraints ctx) + in + let ctx = UContext.make (instance, cstrs) in + subst, ctx + else empty_level_subst, ctx + (** Pretty-printing *) let pr_arc = function @@ -2065,7 +2125,11 @@ let eq_levels = Level.equal let equal_universes = Universe.equal -(* +let subst_instance_constraints = + if Flags.profile then + let key = Profile.declare_profile "subst_instance_constraints" in + Profile.profile2 key subst_instance_constraints + else subst_instance_constraints let merge_constraints = if Flags.profile then @@ -2089,4 +2153,3 @@ let check_leq = let check_leq_key = Profile.declare_profile "check_leq" in Profile.profile3 check_leq_key check_leq else check_leq -*) diff --git a/kernel/univ.mli b/kernel/univ.mli index 8f40bc5f8..655f87bb5 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -27,15 +27,14 @@ sig val equal : t -> t -> bool (** Equality function *) - (* val hash : t -> int *) - (** Hash function *) - val make : Names.DirPath.t -> int -> t (** Create a new universe level from a unique identifier and an associated module path. *) val pr : t -> Pp.std_ppcmds (** Pretty-printing *) + + val var : int -> t end type universe_level = Level.t @@ -370,11 +369,6 @@ val subst_univs_level_level : universe_level_subst -> universe_level -> universe val subst_univs_level_universe : universe_level_subst -> universe -> universe val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints -(** Make a universe level substitution: the instances must match. *) -val make_universe_subst : Instance.t -> universe_context -> universe_level_subst -(** Get the instantiated graph. *) -val instantiate_univ_context : universe_level_subst -> universe_context -> constraints - (** Level to universe substitutions. *) val empty_subst : universe_subst @@ -384,6 +378,21 @@ val make_subst : universe_subst -> universe_subst_fn val subst_univs_universe : universe_subst_fn -> universe -> universe val subst_univs_constraints : universe_subst_fn -> constraints -> constraints +(** Substitution of instances *) +val subst_instance_instance : universe_instance -> universe_instance -> universe_instance +val subst_instance_universe : universe_instance -> universe -> universe +val subst_instance_constraints : universe_instance -> constraints -> constraints + +val make_instance_subst : universe_instance -> universe_level_subst +val make_inverse_instance_subst : universe_instance -> universe_level_subst + +val abstract_universes : bool -> universe_context -> universe_level_subst * universe_context + +(** Get the instantiated graph. *) +val instantiate_univ_context : universe_context -> universe_context + +val instantiate_univ_constraints : universe_instance -> universe_context -> constraints + (** {6 Pretty-printing of universes. } *) val pr_universes : universes -> Pp.std_ppcmds diff --git a/kernel/vars.ml b/kernel/vars.ml index 386a3e8ff..ee156d8c9 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -295,3 +295,44 @@ let subst_univs_level_constr subst c = let subst_univs_level_context s = map_rel_context (subst_univs_level_constr s) + +let subst_instance_constr subst c = + if Univ.Instance.is_empty subst then c + else + let f u = Univ.subst_instance_instance subst u in + let changed = ref false in + let rec aux t = + match kind t with + | Const (c, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (changed := true; mkConstU (c, u')) + | Ind (i, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (changed := true; mkIndU (i, u')) + | Construct (c, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (changed := true; mkConstructU (c, u')) + | Sort (Sorts.Type u) -> + let u' = Univ.subst_instance_universe subst u in + if u' == u then t else + (changed := true; mkSort (Sorts.sort_of_univ u')) + | _ -> Constr.map aux t + in + let c' = aux c in + if !changed then c' else c + +(* let substkey = Profile.declare_profile "subst_instance_constr";; *) +(* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *) + +let subst_instance_context s ctx = + if Univ.Instance.is_empty s then ctx + else map_rel_context (fun x -> subst_instance_constr s x) ctx diff --git a/kernel/vars.mli b/kernel/vars.mli index 0d5ab07db..cfa9fcb26 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -83,3 +83,7 @@ val subst_univs_constr : universe_subst -> constr -> constr val subst_univs_level_constr : universe_level_subst -> constr -> constr val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_context + +(** Instance substitution for polymorphism. *) +val subst_instance_constr : universe_instance -> constr -> constr +val subst_instance_context : universe_instance -> rel_context -> rel_context diff --git a/library/declare.ml b/library/declare.ml index bacd9e2c1..b80ceb6e6 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -158,9 +158,9 @@ let discharge_constant ((sp, kn), obj) = let from = Global.lookup_constant con in let modlist = replacement_context () in - let hyps,uctx = section_segment_of_constant con in + let hyps,subst,uctx = section_segment_of_constant con in let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in - let abstract = (named_of_variable_context hyps, uctx) in + let abstract = (named_of_variable_context hyps, subst, uctx) in let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; } @@ -227,7 +227,14 @@ let declare_sideff env fix_exn se = | Declarations.TemplateArity _ -> None in let cst_of cb = let pt, opaque = pt_opaque_of cb in - let ty = ty_of cb in + let univs, subst = + if cb.const_polymorphic then + let univs = Univ.instantiate_univ_context cb.const_universes in + univs, Vars.subst_instance_constr (Univ.UContext.instance univs) + else cb.const_universes, fun x -> x + in + let pt = (subst (fst pt), snd pt) in + let ty = Option.map subst (ty_of cb) in { cst_decl = ConstantEntry (DefinitionEntry { const_entry_body = Future.from_here ~fix_exn (pt, Declareops.no_seff); const_entry_secctx = Some cb.Declarations.const_hyps; @@ -236,7 +243,7 @@ let declare_sideff env fix_exn se = const_entry_inline_code = false; const_entry_feedback = None; const_entry_polymorphic = cb.const_polymorphic; - const_entry_universes = cb.const_universes; + const_entry_universes = univs; const_entry_proj = false; }); cst_hyps = [] ; @@ -352,7 +359,7 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) = let mind = Global.mind_of_delta_kn kn in let mie = Global.lookup_mind mind in let repl = replacement_context () in - let sechyps,uctx = section_segment_of_mutual_inductive mind in + let sechyps,usubst,uctx = section_segment_of_mutual_inductive mind in Some (discharged_hyps kn sechyps, Discharge.process_inductive (named_of_variable_context sechyps,uctx) repl mie) diff --git a/library/global.ml b/library/global.ml index c3c309c39..65e895dfd 100644 --- a/library/global.ml +++ b/library/global.ml @@ -198,10 +198,10 @@ let universes_of_global env r = Declareops.universes_of_constant cb | IndRef ind -> let (mib, oib) = Inductive.lookup_mind_specif env ind in - mib.mind_universes + Univ.instantiate_univ_context mib.mind_universes | ConstructRef cstr -> let (mib,oib) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - mib.mind_universes + Univ.instantiate_univ_context mib.mind_universes let universes_of_global gr = universes_of_global (env ()) gr diff --git a/library/impargs.ml b/library/impargs.ml index 0126c4ad7..55e21b2c8 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -525,10 +525,10 @@ let impls_of_context ctx = List.rev_map map (List.filter is_set ctx) let section_segment_of_reference = function - | ConstRef con -> section_segment_of_constant con + | ConstRef con -> pi1 (section_segment_of_constant con) | IndRef (kn,_) | ConstructRef ((kn,_),_) -> - section_segment_of_mutual_inductive kn - | _ -> [], Univ.UContext.empty + pi1 (section_segment_of_mutual_inductive kn) + | _ -> [] let adjust_side_condition p = function | LessArgsThan n -> LessArgsThan (n+p) @@ -543,7 +543,7 @@ let discharge_implicits (_,(req,l)) = | ImplLocal -> None | ImplInteractive (ref,flags,exp) -> (try - let vars,_ = section_segment_of_reference ref in + let vars = section_segment_of_reference ref in (* let isproj = *) (* match ref with *) (* | ConstRef cst -> is_projection cst (Global.env ()) *) @@ -560,7 +560,7 @@ let discharge_implicits (_,(req,l)) = | ImplConstant (con,flags) -> (try let con' = pop_con con in - let vars,_ = section_segment_of_constant con in + let vars,_,_ = section_segment_of_constant con in let extra_impls = impls_of_context vars in let newimpls = (* if is_projection con (Global.env()) then (snd (List.hd l)) *) @@ -572,7 +572,7 @@ let discharge_implicits (_,(req,l)) = | ImplMutualInductive (kn,flags) -> (try let l' = List.map (fun (gr, l) -> - let vars,_ = section_segment_of_reference gr in + let vars = section_segment_of_reference gr in let extra_impls = impls_of_context vars in ((if isVarRef gr then gr else pop_global_reference gr), List.map (add_section_impls vars extra_impls) l)) l diff --git a/library/lib.ml b/library/lib.ml index 92bace745..1ee3ca57b 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -382,8 +382,9 @@ let find_opening_node id = type variable_info = Names.Id.t * Decl_kinds.binding_kind * Term.constr option * Term.types type variable_context = variable_info list -type abstr_list = variable_context Univ.in_universe_context Names.Cmap.t * - variable_context Univ.in_universe_context Names.Mindmap.t +type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t + +type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t let sectab = Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind * @@ -427,8 +428,9 @@ let add_section_replacement f g hyps = | (vars,exps,abs)::sl -> let sechyps,ctx = extract_hyps (vars,hyps) in let ctx = Univ.ContextSet.to_context ctx in + let subst, ctx = Univ.abstract_universes true ctx in let args = instance_from_variable_context (List.rev sechyps) in - sectab := (vars,f (Univ.UContext.instance ctx,args) exps,g (sechyps,ctx) abs)::sl + sectab := (vars,f (Univ.UContext.instance ctx,args) exps,g (sechyps,subst,ctx) abs)::sl let add_section_kn kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in @@ -464,7 +466,7 @@ let full_replacement_context () = List.map pi2 !sectab let full_section_segment_of_constant con = List.map (fun (vars,_,(x,_)) -> fun hyps -> named_of_variable_context - (try fst (Names.Cmap.find con x) + (try pi1 (Names.Cmap.find con x) with Not_found -> fst (extract_hyps (vars, hyps)))) !sectab (*************) diff --git a/library/lib.mli b/library/lib.mli index 759a1a135..615a39f9e 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -162,12 +162,13 @@ val xml_close_section : (Names.Id.t -> unit) Hook.t type variable_info = Names.Id.t * Decl_kinds.binding_kind * Term.constr option * Term.types type variable_context = variable_info list +type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t val instance_from_variable_context : variable_context -> Names.Id.t array val named_of_variable_context : variable_context -> Context.named_context -val section_segment_of_constant : Names.constant -> variable_context Univ.in_universe_context -val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_context Univ.in_universe_context +val section_segment_of_constant : Names.constant -> abstr_info +val section_segment_of_mutual_inductive: Names.mutual_inductive -> abstr_info val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array val is_in_section : Globnames.global_reference -> bool diff --git a/library/universes.ml b/library/universes.ml index c38d25d75..c5363fd9a 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -236,23 +236,19 @@ let fresh_universe_instance ctx = let fresh_instance_from_context ctx = let inst = fresh_universe_instance ctx in - let subst = make_universe_subst inst ctx in - let constraints = instantiate_univ_context subst ctx in - (inst, subst), constraints + let constraints = instantiate_univ_constraints inst ctx in + inst, constraints let fresh_instance ctx = let ctx' = ref LSet.empty in - let s = ref LMap.empty in let inst = Instance.subst_fn (fun v -> let u = new_univ_level (Global.current_dirpath ()) in - ctx' := LSet.add u !ctx'; - s := LMap.add v u !s; u) + ctx' := LSet.add u !ctx'; u) (UContext.instance ctx) - in !ctx', !s, inst + in !ctx', inst let existing_instance ctx inst = - let s = ref LMap.empty in let () = let a1 = Instance.to_array inst and a2 = Instance.to_array (UContext.instance ctx) in @@ -261,18 +257,18 @@ let existing_instance ctx inst = Errors.errorlabstrm "Universes" (str "Polymorphic constant expected " ++ int len2 ++ str" levels but was given " ++ int len1) - else Array.iter2 (fun u v -> s := LMap.add v u !s) a1 a2 - in LSet.empty, !s, inst + else () + in LSet.empty, inst let fresh_instance_from ctx inst = - let ctx', subst, inst = + let ctx', inst = match inst with | Some inst -> existing_instance ctx inst | None -> fresh_instance ctx in - let constraints = instantiate_univ_context subst ctx in - (inst, subst), (ctx', constraints) - + let constraints = instantiate_univ_constraints inst ctx in + inst, (ctx', constraints) + let unsafe_instance_from ctx = (Univ.UContext.instance ctx, ctx) @@ -281,21 +277,21 @@ let unsafe_instance_from ctx = let fresh_constant_instance env c inst = let cb = lookup_constant c env in if cb.Declarations.const_polymorphic then - let (inst,_), ctx = fresh_instance_from (Declareops.universes_of_constant cb) inst in + let inst, ctx = fresh_instance_from (Declareops.universes_of_constant cb) inst in ((c, inst), ctx) else ((c,Instance.empty), ContextSet.empty) let fresh_inductive_instance env ind inst = let mib, mip = Inductive.lookup_mind_specif env ind in if mib.Declarations.mind_polymorphic then - let (inst,_), ctx = fresh_instance_from mib.Declarations.mind_universes inst in + let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in ((ind,inst), ctx) else ((ind,Instance.empty), ContextSet.empty) let fresh_constructor_instance env (ind,i) inst = let mib, mip = Inductive.lookup_mind_specif env ind in if mib.Declarations.mind_polymorphic then - let (inst,_), ctx = fresh_instance_from mib.Declarations.mind_universes inst in + let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in (((ind,i),inst), ctx) else (((ind,i),Instance.empty), ContextSet.empty) @@ -412,15 +408,14 @@ let type_of_reference env r = let cb = Environ.lookup_constant c env in let ty = Typeops.type_of_constant_type env cb.const_type in if cb.const_polymorphic then - let (inst, subst), ctx = - fresh_instance_from (Declareops.universes_of_constant cb) None in - Vars.subst_univs_level_constr subst ty, ctx + let inst, ctx = fresh_instance_from (Declareops.universes_of_constant cb) None in + Vars.subst_instance_constr inst ty, ctx else ty, ContextSet.empty | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in if mib.mind_polymorphic then - let (inst, subst), ctx = fresh_instance_from mib.mind_universes None in + let inst, ctx = fresh_instance_from mib.mind_universes None in let ty = Inductive.type_of_inductive env (specif, inst) in ty, ctx else @@ -429,7 +424,7 @@ let type_of_reference env r = | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in if mib.mind_polymorphic then - let (inst, subst), ctx = fresh_instance_from mib.mind_universes None in + let inst, ctx = fresh_instance_from mib.mind_universes None in Inductive.type_of_constructor (cstr,inst) specif, ctx else Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty diff --git a/library/universes.mli b/library/universes.mli index 565f9fb0a..6cfee48d2 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -84,10 +84,10 @@ val leq_constr_universes : constr -> constr -> bool universe_constrained the instantiated constraints. *) val fresh_instance_from_context : universe_context -> - (universe_instance * universe_level_subst) constrained + universe_instance constrained val fresh_instance_from : universe_context -> universe_instance option -> - (universe_instance * universe_level_subst) in_universe_context_set + universe_instance in_universe_context_set val fresh_sort_in_family : env -> sorts_family -> sorts in_universe_context_set diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index be22030ce..3c7d4f75b 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -41,12 +41,12 @@ let section_segment_of_reference = function | ConstRef con -> Lib.section_segment_of_constant con | IndRef (kn,_) | ConstructRef ((kn,_),_) -> Lib.section_segment_of_mutual_inductive kn - | _ -> [], Univ.UContext.empty + | _ -> [], Univ.LMap.empty, Univ.UContext.empty let discharge_rename_args = function | _, (ReqGlobal (c, names), _ as req) -> (try - let vars,_ = section_segment_of_reference c in + let vars,_,_ = section_segment_of_reference c in let c' = pop_global_reference c in let var_names = List.map (fun (id, _,_,_) -> Name id) vars in let names' = List.map (fun l -> var_names @ l) names in diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index a12fe6b67..81b5c9ad8 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -59,10 +59,7 @@ let check_privacy_block mib = (* Christine Paulin, 1996 *) let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = - let usubst = Inductive.make_inductive_subst mib u in - let lnamespar = Vars.subst_univs_level_context usubst - mib.mind_params_ctxt - in + let lnamespar = Vars.subst_instance_context u mib.mind_params_ctxt in let () = check_privacy_block mib in let () = if not (Sorts.List.mem kind (elim_sorts specif)) then @@ -282,9 +279,8 @@ let mis_make_indrec env sigma listdepkind mib u = let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in let evdref = ref sigma in - let usubst = Inductive.make_inductive_subst mib u in let lnonparrec,lnamesparrec = - context_chop (nparams-nparrec) (Vars.subst_univs_level_context usubst mib.mind_params_ctxt) in + context_chop (nparams-nparrec) (Vars.subst_instance_context u mib.mind_params_ctxt) in let nrec = List.length listdepkind in let depPvec = Array.make mib.mind_ntypes (None : (bool * constr) option) in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index dee22cb17..f6ca611a3 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -35,11 +35,6 @@ let type_of_constructor env (cstr,u) = Typeops.check_hyps_inclusion env (mkConstruct cstr) mib.mind_hyps; Inductive.type_of_constructor (cstr,u) specif -let type_of_constructor_in_ctx env cstr = - let specif = - Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - Inductive.type_of_constructor_in_ctx cstr specif - (* Return constructor types in user form *) let type_of_constructors env (ind,u as indu) = let specif = Inductive.lookup_mind_specif env ind in @@ -101,8 +96,7 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j = and nconstr = Array.length mip.mind_consnames in let make_Ik k = mkIndU (((fst ind),ntypes-k-1),u) in if j > nconstr then error "Not enough constructors in the type."; - let univsubst = make_inductive_subst mib u in - substl (List.init ntypes make_Ik) (subst_univs_level_constr univsubst specif.(j-1)) + substl (List.init ntypes make_Ik) (subst_instance_constr u specif.(j-1)) (* Number of constructors *) @@ -248,13 +242,11 @@ let inductive_paramdecls_env env (ind,u) = let inductive_alldecls (ind,u) = let (mib,mip) = Global.lookup_inductive ind in - let subst = Inductive.make_inductive_subst mib u in - Vars.subst_univs_level_context subst mip.mind_arity_ctxt + Vars.subst_instance_context u mip.mind_arity_ctxt let inductive_alldecls_env env (ind,u) = let (mib,mip) = Inductive.lookup_mind_specif env ind in - let subst = Inductive.make_inductive_subst mib u in - Vars.subst_univs_level_context subst mip.mind_arity_ctxt + Vars.subst_instance_context u mip.mind_arity_ctxt let constructor_has_local_defs (indsp,j) = let (mib,mip) = Global.lookup_inductive indsp in @@ -353,7 +345,6 @@ let instantiate_context sign args = let get_arity env ((ind,u),params) = let (mib,mip) = Inductive.lookup_mind_specif env ind in - let univsubst = make_inductive_subst mib u in let parsign = (* Dynamically detect if called with an instance of recursively uniform parameter only or also of non recursively uniform @@ -364,11 +355,11 @@ let get_arity env ((ind,u),params) = snd (List.chop nnonrecparams mib.mind_params_ctxt) else parsign in - let parsign = Vars.subst_univs_level_context univsubst parsign in + let parsign = Vars.subst_instance_context u parsign in let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in let arsign,_ = List.chop arproperlength mip.mind_arity_ctxt in let subst = instantiate_context parsign params in - let arsign = Vars.subst_univs_level_context univsubst arsign in + let arsign = Vars.subst_instance_context u arsign in (substl_rel_context subst arsign, Inductive.inductive_sort_family mip) (* Functions to build standard types related to inductive *) @@ -583,9 +574,7 @@ let rec instantiate_universes env evdref scl is = function let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = match mip.mind_arity with - | RegularArity s -> - let subst = Inductive.make_inductive_subst mib u in - sigma, subst_univs_level_constr subst s.mind_user_arity + | RegularArity s -> sigma, subst_instance_constr u s.mind_user_arity | TemplateArity ar -> let _,scl = Reduction.dest_arity env conclty in let ctx = List.rev mip.mind_arity_ctxt in diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index cefd5bd9d..5583eff4d 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -20,7 +20,6 @@ val type_of_inductive : env -> pinductive -> types (** Return type as quoted by the user *) val type_of_constructor : env -> pconstructor -> types -val type_of_constructor_in_ctx : env -> constructor -> types Univ.in_universe_context val type_of_constructors : env -> pinductive -> types array (** Return constructor types in normal form *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e5023e858..fe9646b9d 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -532,8 +532,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t = (mk_tycon (applist (mkIndU ind, args))) in j', (ind, args)) in - let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in - let ty = Vars.subst_univs_level_constr usubst ty in + let ty = Vars.subst_instance_constr u ty in let ty = substl (recty.uj_val :: List.rev pars) ty in let j = {uj_val = mkProj (cst,recty.uj_val); uj_type = ty} in inh_conv_coerce_to_tycon loc env evdref j tycon diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e6844673c..1f3e7b571 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -61,7 +61,7 @@ module ReductionBehaviour = struct let discharge = function | _,(ReqGlobal (ConstRef c, req), (_, b)) -> let c' = pop_con c in - let vars, _ctx = Lib.section_segment_of_constant c in + let vars, _subst, _ctx = Lib.section_segment_of_constant c in let extra = List.length vars in let nargs' = if b.b_nargs < 0 then b.b_nargs else b.b_nargs + extra in let recargs' = List.map ((+) extra) b.b_recargs in @@ -654,23 +654,23 @@ let reducible_mind_case c = match kind_of_term c with *) let magicaly_constant_of_fixbody env bd = function | Name.Anonymous -> bd - | Name.Name id -> - try - let cst = Nametab.locate_constant - (Libnames.make_qualid DirPath.empty id) in - let (cst, u), ctx = Universes.fresh_constant_instance env cst in - match constant_opt_value env (cst,u) with - | None -> bd - | Some (t,cstrs) -> - let b, csts = Universes.eq_constr_universes t bd in - let subst = Universes.Constraints.fold (fun (l,d,r) acc -> - Univ.LMap.add (Option.get (Universe.level l)) (Option.get (Universe.level r)) acc) - csts Univ.LMap.empty - in - let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in - if b then mkConstU (cst,inst) else bd - with - | Not_found -> bd + | Name.Name id -> bd + (* try *) + (* let cst = Nametab.locate_constant *) + (* (Libnames.make_qualid DirPath.empty id) in *) + (* let (cst, u), ctx = Universes.fresh_constant_instance env cst in *) + (* match constant_opt_value_in env (cst,u) with *) + (* | None -> bd *) + (* | Some t -> *) + (* let b, csts = Universes.eq_constr_universes t bd in *) + (* let subst = Universes.Constraints.fold (fun (l,d,r) acc -> *) + (* Univ.LMap.add (Option.get (Universe.level l)) (Option.get (Universe.level r)) acc) *) + (* csts Univ.LMap.empty *) + (* in *) + (* let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in *) + (* if b then mkConstU (cst,inst) else bd *) + (* with *) + (* | Not_found -> bd *) let contract_cofix ?env (bodynum,(names,types,bodies as typedbodies)) = let nbodies = Array.length bodies in diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index fad8623b0..f2a0b6fd1 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -896,6 +896,12 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c = in app_stack (redrec (c, empty_stack)) *) +let whd_simpl_stack = + if Flags.profile then + let key = Profile.declare_profile "whd_simpl_stack" in + Profile.profile3 key whd_simpl_stack + else whd_simpl_stack + (* Same as [whd_simpl] but also reduces constants that do not hide a reducible fix, but does this reduction of constants only until it immediately hides a non reducible fix or a cofix *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index dd09d5b29..67189e22d 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -210,7 +210,7 @@ let discharge_class (_,cl) = in grs', discharge_rel_context subst 1 ctx @ ctx' in let cl_impl' = Lib.discharge_global cl.cl_impl in if cl_impl' == cl.cl_impl then cl else - let ctx, uctx = abs_context cl in + let ctx, usubst, uctx = abs_context cl in let ctx, subst = rel_of_variable_context ctx in let context = discharge_context ctx subst cl.cl_context in let props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props in @@ -379,7 +379,7 @@ let remove_instance i = remove_instance_hint i.is_impl let declare_instance pri local glob = - let ty = Global.type_of_global_unsafe (*FIXME*) glob in + let ty = Global.type_of_global_unsafe glob in match class_of_constr ty with | Some (rels, ((tc,_), args) as _cl) -> add_instance (new_instance tc pri (not local) (Flags.use_polymorphic_flag ()) glob) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b21f4e383..758686aa9 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -58,8 +58,7 @@ let find_rectype_a env c = let type_constructor mind mib u typ params = let s = ind_subst mind mib u in let ctyp = substl s typ in - let usubst = make_inductive_subst mib u in - let ctyp = subst_univs_level_constr usubst ctyp in + let ctyp = subst_instance_constr u ctyp in let nparams = Array.length params in if Int.equal nparams 0 then ctyp else diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 42d779f04..6e45cb6b0 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -458,8 +458,9 @@ let ungeneralized_type_of_constant_type t = let print_constant with_values sep sp = let cb = Global.lookup_constant sp in let val_0 = Declareops.body_of_constant cb in - let typ = ungeneralized_type_of_constant_type cb.const_type in - let univs = Declareops.universes_of_constant cb in + let typ = Declareops.type_of_constant cb in + let typ = ungeneralized_type_of_constant_type typ in + let univs = Univ.instantiate_univ_context (Declareops.universes_of_constant cb) in hov 0 (pr_polymorphic cb.const_polymorphic ++ match val_0 with | None -> diff --git a/printing/printer.ml b/printing/printer.ml index 03f416a51..55a7d36a3 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -756,12 +756,12 @@ let build_ind_type env mip = Inductive.type_of_inductive env mip let print_one_inductive env mib ((_,i) as ind) = - let mip = mib.mind_packets.(i) in - let params = mib.mind_params_ctxt in - let args = extended_rel_list 0 params in let u = if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes else Univ.Instance.empty in + let mip = mib.mind_packets.(i) in + let params = Inductive.inductive_paramdecls (mib,u) in + let args = extended_rel_list 0 params in let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in @@ -794,12 +794,14 @@ let get_fields = prodec_rec [] [] let print_record env mind mib = + let u = + if mib.mind_polymorphic then + Univ.UContext.instance mib.mind_universes + else Univ.Instance.empty + in let mip = mib.mind_packets.(0) in - let params = mib.mind_params_ctxt in + let params = Inductive.inductive_paramdecls (mib,u) in let args = extended_rel_list 0 params in - let u = if mib.mind_polymorphic then - Univ.UContext.instance mib.mind_universes - else Univ.Instance.empty in let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in let cstrtype = hnf_prod_applist env cstrtypes.(0) args in diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 9cf2baf6f..349d6e29e 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -102,8 +102,7 @@ let get_sym_eq_data env (ind,u) = if not (Int.equal (Array.length mib.mind_packets) 1) || not (Int.equal (Array.length mip.mind_nf_lc) 1) then error "Not an inductive type with a single constructor."; - let subst = Inductive.make_inductive_subst mib u in - let arityctxt = Vars.subst_univs_level_context subst mip.mind_arity_ctxt in + let arityctxt = Vars.subst_instance_context u mip.mind_arity_ctxt in let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then error "Inductive equalities with local definitions in arity not supported."; @@ -115,7 +114,7 @@ let get_sym_eq_data env (ind,u) = if mip.mind_nrealargs > mib.mind_nparams then error "Constructors arguments must repeat the parameters."; let _,params2 = List.chop (mib.mind_nparams-mip.mind_nrealargs) params in - let paramsctxt = Vars.subst_univs_level_context subst mib.mind_params_ctxt in + let paramsctxt = Vars.subst_instance_context u mib.mind_params_ctxt in let paramsctxt1,_ = List.chop (mib.mind_nparams-mip.mind_nrealargs) paramsctxt in if not (List.equal eq_constr params2 constrargs) then @@ -138,8 +137,7 @@ let get_non_sym_eq_data env (ind,u) = if not (Int.equal (Array.length mib.mind_packets) 1) || not (Int.equal (Array.length mip.mind_nf_lc) 1) then error "Not an inductive type with a single constructor."; - let subst = Inductive.make_inductive_subst mib u in - let arityctxt = Vars.subst_univs_level_context subst mip.mind_arity_ctxt in + let arityctxt = Vars.subst_instance_context u mip.mind_arity_ctxt in let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then error "Inductive equalities with local definitions in arity not supported"; @@ -148,8 +146,8 @@ let get_non_sym_eq_data env (ind,u) = if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; let _,constrargs = List.chop mib.mind_nparams constrargs in - let constrargs = List.map (Vars.subst_univs_level_constr subst) constrargs in - let paramsctxt = Vars.subst_univs_level_context subst mib.mind_params_ctxt in + let constrargs = List.map (Vars.subst_instance_constr u) constrargs in + let paramsctxt = Vars.subst_instance_context u mib.mind_params_ctxt in (specif,constrargs,realsign,paramsctxt,mip.mind_nrealargs) (**********************************************************************) @@ -729,14 +727,13 @@ let build_congr env (eq,refl,ctx) ind = let (ind,u as indu), ctx = with_context_set ctx (Universes.fresh_inductive_instance env ind) in let (mib,mip) = lookup_mind_specif env ind in - let subst = Inductive.make_inductive_subst mib u in if not (Int.equal (Array.length mib.mind_packets) 1) || not (Int.equal (Array.length mip.mind_nf_lc) 1) then error "Not an inductive type with a single constructor."; if not (Int.equal mip.mind_nrealargs 1) then error "Expect an inductive type with one predicate parameter."; let i = 1 in - let arityctxt = Vars.subst_univs_level_context subst mip.mind_arity_ctxt in - let paramsctxt = Vars.subst_univs_level_context subst mib.mind_params_ctxt in + let arityctxt = Vars.subst_instance_context u mip.mind_arity_ctxt in + let paramsctxt = Vars.subst_instance_context u mib.mind_params_ctxt in let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then error "Inductive equalities with local definitions in arity not supported."; diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index d36833c71..a644654bc 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -73,7 +73,6 @@ Section Proper. Definition respectful (R : crelation A) (R' : crelation B) : crelation (A -> B) := Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R'). - End Proper. (** We favor the use of Leibniz equality or a declared reflexive crelation @@ -396,14 +395,14 @@ Section GenericInstances. Reflexive (@Logic.eq A ==> R'). Proof. simpl_crelation. Qed. - (** [respectful] is a morphism for crelation equivalence. *) - + (** [respectful] is a morphism for crelation equivalence . *) + Set Printing All. Set Printing Universes. Global Instance respectful_morphism : Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). Proof. - intros R R' HRR' S S' HSS' f g. - unfold respectful, relation_equivalence in * ; simpl in *. + intros R R' HRR' S S' HSS' f g. + unfold respectful , relation_equivalence in *; simpl in *. split ; intros H x y Hxy. apply (fst (HSS' _ _)). apply H. now apply (snd (HRR' _ _)). apply (snd (HSS' _ _)). apply H. now apply (fst (HRR' _ _)). diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v index ed43a5e52..6899d2e52 100644 --- a/theories/Classes/CRelationClasses.v +++ b/theories/Classes/CRelationClasses.v @@ -66,7 +66,7 @@ Section Defs. (** Various combinations of reflexivity, symmetry and transitivity. *) (** A [PreOrder] is both Reflexive and Transitive. *) - + Class PreOrder (R : crelation A) := { PreOrder_Reflexive :> Reflexive R | 2 ; PreOrder_Transitive :> Transitive R | 2 }. @@ -270,8 +270,7 @@ Instance iff_Transitive : Transitive iff := iff_trans. (** Logical equivalence [iff] is an equivalence crelation. *) -Program Instance iff_equivalence : Equivalence iff. - +Program Instance iff_equivalence : Equivalence iff. Program Instance arrow_Reflexive : Reflexive arrow. Program Instance arrow_Transitive : Transitive arrow. diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index bd5218eff..971ae70d8 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -77,12 +77,23 @@ let refresh_polymorphic_type_of_inductive (_,mip) = let process_inductive (sechyps,abs_ctx) modlist mib = let nparams = mib.mind_nparams in + let subst, univs = + if mib.mind_polymorphic then + let inst = Univ.UContext.instance mib.mind_universes in + let cstrs = Univ.UContext.constraints mib.mind_universes in + inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs) + else Univ.Instance.empty, mib.mind_universes + in let inds = Array.map_to_list (fun mip -> let ty = refresh_polymorphic_type_of_inductive (mib,mip) in let arity = expmod_constr modlist ty in - let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in + let arity = Vars.subst_instance_constr subst arity in + let lc = Array.map + (fun c -> Vars.subst_instance_constr subst (expmod_constr modlist c)) + mip.mind_user_lc + in (mip.mind_typename, arity, Array.to_list mip.mind_consnames, @@ -90,7 +101,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib = mib.mind_packets in let sechyps' = map_named_context (expmod_constr modlist) sechyps in let (params',inds') = abstract_inductive sechyps' nparams inds in - let univs = Univ.UContext.union abs_ctx mib.mind_universes in + let univs = Univ.UContext.union abs_ctx univs in let record = match mib.mind_record with | None -> None | Some (_, a) -> Some (Array.length a > 0) diff --git a/toplevel/record.ml b/toplevel/record.ml index 896cc41c7..302fe6280 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -209,9 +209,9 @@ let instantiate_possibly_recursive_type indu paramdecls fields = let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in - let paramdecls = mib.mind_params_ctxt in - let poly = mib.mind_polymorphic and ctx = mib.mind_universes in let u = Inductive.inductive_instance mib in + let paramdecls = Inductive.inductive_paramdecls (mib, u) in + let poly = mib.mind_polymorphic and ctx = Univ.instantiate_univ_context mib.mind_universes in let indu = indsp, u in let r = mkIndU (indsp,u) in let rp = applist (r, Termops.extended_rel_list 0 paramdecls) in diff --git a/toplevel/search.ml b/toplevel/search.ml index 016b9f22b..e2a4ad25c 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -43,9 +43,9 @@ module SearchBlacklist = of the object, the assumptions that will make it possible to print its type, and the constr term that represent its type. *) -let iter_constructors indsp fn env nconstr = +let iter_constructors indsp u fn env nconstr = for i = 1 to nconstr do - let typ, _ = Inductiveops.type_of_constructor_in_ctx env (indsp, i) in + let typ = Inductiveops.type_of_constructor env ((indsp, i), u) in fn (ConstructRef (indsp, i)) env typ done @@ -68,11 +68,12 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) = let mib = Global.lookup_mind mind in let iter_packet i mip = let ind = (mind, i) in - let i = (ind, Inductive.inductive_instance mib) in + let u = Inductive.inductive_instance mib in + let i = (ind, u) in let typ = Inductiveops.type_of_inductive env i in let () = fn (IndRef ind) env typ in let len = Array.length mip.mind_user_lc in - iter_constructors ind fn env len + iter_constructors ind u fn env len in Array.iteri iter_packet mib.mind_packets | _ -> () |