diff options
| -rw-r--r-- | checker/inductive.ml | 7 | ||||
| -rw-r--r-- | checker/inductive.mli | 2 | ||||
| -rw-r--r-- | kernel/declareops.ml | 28 | ||||
| -rw-r--r-- | kernel/declareops.mli | 9 | ||||
| -rw-r--r-- | kernel/environ.ml | 10 | ||||
| -rw-r--r-- | kernel/environ.mli | 5 | ||||
| -rw-r--r-- | kernel/nativecode.ml | 4 | ||||
| -rw-r--r-- | library/global.ml | 48 | ||||
| -rw-r--r-- | library/global.mli | 2 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 5 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 4 | ||||
| -rw-r--r-- | pretyping/vnorm.ml | 4 | ||||
| -rw-r--r-- | printing/prettyp.ml | 7 | ||||
| -rw-r--r-- | printing/printmod.ml | 15 | ||||
| -rw-r--r-- | tactics/elimschemes.ml | 6 | ||||
| -rw-r--r-- | vernac/obligations.ml | 2 | ||||
| -rw-r--r-- | vernac/record.ml | 4 | ||||
| -rw-r--r-- | vernac/search.ml | 2 |
18 files changed, 67 insertions, 97 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml index a145165aa..1271a02b0 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -66,13 +66,6 @@ let inductive_is_cumulative mib = | Polymorphic_ind ctx -> false | Cumulative_ind cumi -> true -let inductive_polymorphic_context mib = - match mib.mind_universes with - | Monomorphic_ind _ -> Univ.UContext.empty - | Polymorphic_ind ctx -> Univ.instantiate_univ_context ctx - | Cumulative_ind cumi -> - Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi) - (************************************************************************) (* Build the substitution that replaces Rels by the appropriate *) diff --git a/checker/inductive.mli b/checker/inductive.mli index b8cbda7cf..8f605935d 100644 --- a/checker/inductive.mli +++ b/checker/inductive.mli @@ -26,8 +26,6 @@ val inductive_is_polymorphic : mutual_inductive_body -> bool val inductive_is_cumulative : mutual_inductive_body -> bool -val inductive_polymorphic_context : mutual_inductive_body -> Univ.universe_context - val type_of_inductive : env -> mind_specif puniverses -> constr (* Return type as quoted by the user *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 1337036b8..cf6d3c55e 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -67,24 +67,14 @@ let type_of_constant cb = if t' == t then x else RegularArity t' | TemplateArity _ as x -> x -let universes_of_polymorphic_constant otab cb = - match cb.const_universes with - | Monomorphic_const _ -> Univ.UContext.empty - | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx - let constant_has_body cb = match cb.const_body with | Undef _ -> false | Def _ | OpaqueDef _ -> true -let constant_polymorphic_instance cb = - match cb.const_universes with - | Monomorphic_const _ -> Univ.Instance.empty - | Polymorphic_const ctx -> Univ.AUContext.instance ctx - let constant_polymorphic_context cb = match cb.const_universes with - | Monomorphic_const _ -> Univ.UContext.empty - | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx + | Monomorphic_const _ -> Univ.AUContext.empty + | Polymorphic_const ctx -> ctx let is_opaque cb = match cb.const_body with | OpaqueDef _ -> true @@ -268,19 +258,11 @@ let subst_mind_body sub mib = mind_typing_flags = mib.mind_typing_flags; } -let inductive_polymorphic_instance mib = - match mib.mind_universes with - | Monomorphic_ind _ -> Univ.Instance.empty - | Polymorphic_ind ctx -> Univ.AUContext.instance ctx - | Cumulative_ind cumi -> - Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) - let inductive_polymorphic_context mib = match mib.mind_universes with - | Monomorphic_ind _ -> Univ.UContext.empty - | Polymorphic_ind ctx -> Univ.instantiate_univ_context ctx - | Cumulative_ind cumi -> - Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi) + | Monomorphic_ind _ -> Univ.AUContext.empty + | Polymorphic_ind ctx -> ctx + | Cumulative_ind cumi -> Univ.ACumulativityInfo.univ_context cumi let inductive_is_polymorphic mib = match mib.mind_universes with diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 7350724b8..987c1adaf 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -27,8 +27,7 @@ val subst_const_body : substitution -> constant_body -> constant_body val constant_has_body : constant_body -> bool -val constant_polymorphic_instance : constant_body -> universe_instance -val constant_polymorphic_context : constant_body -> universe_context +val constant_polymorphic_context : constant_body -> abstract_universe_context (** Is the constant polymorphic? *) val constant_is_polymorphic : constant_body -> bool @@ -43,9 +42,6 @@ val type_of_constant : constant_body -> constant_type (** Return the universe context, in case the definition is polymorphic, otherwise the context is empty. *) -val universes_of_polymorphic_constant : - Opaqueproof.opaquetab -> constant_body -> Univ.universe_context - val is_opaque : constant_body -> bool (** Side effects *) @@ -68,8 +64,7 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body -val inductive_polymorphic_instance : mutual_inductive_body -> universe_instance -val inductive_polymorphic_context : mutual_inductive_body -> universe_context +val inductive_polymorphic_context : mutual_inductive_body -> abstract_universe_context (** Is the inductive polymorphic? *) val inductive_is_polymorphic : mutual_inductive_body -> bool diff --git a/kernel/environ.ml b/kernel/environ.ml index ca2c8e135..b01b65200 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -247,17 +247,11 @@ let constant_type env (kn,u) = let csts = constraints_of cb u in (map_regular_arity (subst_instance_constr u) cb.const_type, csts) -let constant_instance env kn = - let cb = lookup_constant kn env in - match cb.const_universes with - | Monomorphic_const _ -> Univ.Instance.empty - | Polymorphic_const ctx -> Univ.AUContext.instance ctx - let constant_context env kn = let cb = lookup_constant kn env in match cb.const_universes with - | Monomorphic_const _ -> Univ.UContext.empty - | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx + | Monomorphic_const _ -> Univ.AUContext.empty + | Polymorphic_const ctx -> ctx type const_evaluation_result = NoBody | Opaque | IsProj diff --git a/kernel/environ.mli b/kernel/environ.mli index f8887d8e8..cd7a9d279 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -160,10 +160,7 @@ val constant_value_and_type : env -> constant puniverses -> constr option * constant_type * Univ.constraints (** The universe context associated to the constant, empty if not polymorphic *) -val constant_context : env -> constant -> Univ.universe_context -(** The universe isntance associated to the constant, empty if not - polymorphic *) -val constant_instance : env -> constant -> Univ.universe_instance +val constant_context : env -> constant -> Univ.abstract_universe_context (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 9d7262206..da7fcd6f2 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1959,14 +1959,14 @@ let param_name = Name (id_of_string "params") let arg_name = Name (id_of_string "arg") let compile_mind prefix ~interactive mb mind stack = - let u = Declareops.inductive_polymorphic_instance mb in + let u = Declareops.inductive_polymorphic_context mb in let f i stack ob = let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in let j = push_symbol (SymbInd (mind,i)) in let name = Gind ("", (mind, i)) in let accu = let args = - if Univ.Instance.is_empty u then + if Int.equal (Univ.AUContext.size u) 0 then [|get_ind_code j; MLarray [||]|] else [|get_ind_code j|] in diff --git a/library/global.ml b/library/global.ml index 8b59c84dd..09c202c50 100644 --- a/library/global.ml +++ b/library/global.ml @@ -164,49 +164,49 @@ let type_of_global_unsafe r = match r with | VarRef id -> Environ.named_type id env | ConstRef c -> - let cb = Environ.lookup_constant c env in - let univs = - Declareops.universes_of_polymorphic_constant - (Environ.opaque_tables env) cb in - let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in - Vars.subst_instance_constr (Univ.UContext.instance univs) ty + let cb = Environ.lookup_constant c env in + let inst = Univ.AUContext.instance (Declareops.constant_polymorphic_context cb) in + let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in + Vars.subst_instance_constr inst ty | IndRef ind -> - let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - let inst = Declareops.inductive_polymorphic_instance mib in - Inductive.type_of_inductive env (specif, inst) + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in + let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in + Inductive.type_of_inductive env (specif, inst) | ConstructRef cstr -> - let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - let inst = Declareops.inductive_polymorphic_instance mib in - Inductive.type_of_constructor (cstr,inst) specif + let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in + Inductive.type_of_constructor (cstr,inst) specif let type_of_global_in_context env r = match r with | VarRef id -> Environ.named_type id env, Univ.UContext.empty | ConstRef c -> - let cb = Environ.lookup_constant c env in - let univs = - Declareops.universes_of_polymorphic_constant - (Environ.opaque_tables env) cb in - Typeops.type_of_constant_type env cb.Declarations.const_type, univs + let cb = Environ.lookup_constant c env in + let univs = Declareops.constant_polymorphic_context cb in + let inst = Univ.AUContext.instance univs in + let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in + Typeops.type_of_constant_type env cb.Declarations.const_type, univs | IndRef ind -> - let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - let univs = Declareops.inductive_polymorphic_context mib in - Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in + let univs = Declareops.inductive_polymorphic_context mib in + let inst = Univ.AUContext.instance univs in + let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in + Inductive.type_of_inductive env (specif, inst), univs | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in let univs = Declareops.inductive_polymorphic_context mib in - let inst = Univ.UContext.instance univs in + let inst = Univ.AUContext.instance univs in + let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in Inductive.type_of_constructor (cstr,inst) specif, univs let universes_of_global env r = match r with - | VarRef id -> Univ.UContext.empty + | VarRef id -> Univ.AUContext.empty | ConstRef c -> let cb = Environ.lookup_constant c env in - Declareops.universes_of_polymorphic_constant - (Environ.opaque_tables env) cb + Declareops.constant_polymorphic_context cb | IndRef ind -> let (mib, oib) = Inductive.lookup_mind_specif env ind in Declareops.inductive_polymorphic_context mib diff --git a/library/global.mli b/library/global.mli index 754fa1516..5ddf54b4a 100644 --- a/library/global.mli +++ b/library/global.mli @@ -141,7 +141,7 @@ val type_of_global_unsafe : Globnames.global_reference -> Constr.types [Evarutil.new_global] and [Retyping.get_type_of]. *) (** Returns the universe context of the global reference (whatever its polymorphic status is). *) -val universes_of_global : Globnames.global_reference -> Univ.universe_context +val universes_of_global : Globnames.global_reference -> Univ.abstract_universe_context (** {6 Retroknowledge } *) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 1cb694da6..9fc2573ac 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -198,7 +198,8 @@ let warn_projection_no_head_constant = let compute_canonical_projections warn (con,ind) = let env = Global.env () in let ctx = Environ.constant_context env con in - let u = Univ.UContext.instance ctx in + let u = Univ.AUContext.instance ctx in + let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in let v = (mkConstU (con,u)) in let ctx = Univ.ContextSet.of_context ctx in let c = Environ.constant_value_in env (con,u) in @@ -298,7 +299,7 @@ let error_not_structure ref = let check_and_decompose_canonical_structure ref = let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in let env = Global.env () in - let u = Environ.constant_instance env sp in + let u = Univ.AUContext.instance (Environ.constant_context env sp) in let vc = match Environ.constant_opt_value_in env (sp, u) with | Some vc -> vc | None -> error_not_structure ref in diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 201f79c39..bae831b63 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -117,10 +117,10 @@ let typeclass_univ_instance (cl,u') = match cl.cl_impl with | ConstRef c -> let cb = Global.lookup_constant c in - Declareops.constant_polymorphic_instance cb + Univ.AUContext.instance (Declareops.constant_polymorphic_context cb) | IndRef c -> let mib,oib = Global.lookup_inductive c in - Declareops.inductive_polymorphic_instance mib + Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) | _ -> Univ.Instance.empty in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u') diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b3eaa3cb9..66cc42cb6 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -174,7 +174,7 @@ and nf_whd env sigma whd typ = | Vatom_stk(Aind ((mi,i) as ind), stk) -> let mib = Environ.lookup_mind mi env in let nb_univs = - Univ.Instance.length (Declareops.inductive_polymorphic_instance mib) + Univ.AUContext.size (Declareops.inductive_polymorphic_context mib) in let mk u = let pind = (ind, u) in (mkIndU pind, type_of_ind env pind) @@ -203,7 +203,7 @@ and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk = | ConstKey cst -> let cbody = Environ.lookup_constant cst env in let nb_univs = - Univ.Instance.length (Declareops.constant_polymorphic_instance cbody) + Univ.AUContext.size (Declareops.constant_polymorphic_context cbody) in let mk u = let pcst = (cst, u) in (mkConstU pcst, Typeops.type_of_constant_in env pcst) diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 15c0f80b9..d9bb97be1 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -78,6 +78,8 @@ let print_ref reduce ref = in EConstr.it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in + let inst = Univ.AUContext.instance univs in + let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in let env = Global.env () in let bl = Universes.universe_binders_of_global ref in let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in @@ -503,7 +505,10 @@ let ungeneralized_type_of_constant_type t = let print_instance sigma cb = if Declareops.constant_is_polymorphic cb then - pr_universe_instance sigma (Declareops.constant_polymorphic_context cb) + let univs = Declareops.constant_polymorphic_context cb in + let inst = Univ.AUContext.instance univs in + let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in + pr_universe_instance sigma univs else mt() let print_constant with_values sep sp = diff --git a/printing/printmod.ml b/printing/printmod.ml index 10b791e37..2e0e6d284 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -89,7 +89,7 @@ let build_ind_type env mip = let print_one_inductive env sigma mib ((_,i) as ind) = let u = if Declareops.inductive_is_polymorphic mib then - Declareops.inductive_polymorphic_instance mib + Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) else Univ.Instance.empty in let mip = mib.mind_packets.(i) in let params = Inductive.inductive_paramdecls (mib,u) in @@ -100,7 +100,9 @@ let print_one_inductive env sigma mib ((_,i) as ind) = let envpar = push_rel_context params env in let inst = if Declareops.inductive_is_polymorphic mib then - Printer.pr_universe_instance sigma (Declareops.inductive_polymorphic_context mib) + let ctx = Declareops.inductive_polymorphic_context mib in + let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in + Printer.pr_universe_instance sigma ctx else mt () in hov 0 ( @@ -149,7 +151,7 @@ let get_fields = let print_record env mind mib = let u = if Declareops.inductive_is_polymorphic mib then - Declareops.inductive_polymorphic_instance mib + Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) else Univ.Instance.empty in let mip = mib.mind_packets.(0) in @@ -292,11 +294,13 @@ let print_body is_impl env mp (l,body) = | SFBmodule _ -> keyword "Module" ++ spc () ++ name | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name | SFBconst cb -> + let ctx = Declareops.constant_polymorphic_context cb in let u = if Declareops.constant_is_polymorphic cb then - Declareops.constant_polymorphic_instance cb + Univ.AUContext.instance ctx else Univ.Instance.empty in + let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in let sigma = Evd.empty in (match cb.const_body with | Def _ -> def "Definition" ++ spc () @@ -316,8 +320,7 @@ let print_body is_impl env mp (l,body) = Printer.pr_lconstr_env env sigma (Vars.subst_instance_constr u (Mod_subst.force_constr l))) | _ -> mt ()) ++ str "." ++ - Printer.pr_universe_ctx sigma - (Declareops.constant_polymorphic_context cb)) + Printer.pr_universe_ctx sigma ctx) | SFBmind mib -> try let env = Option.get env in diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 5d9d36958..e058806a3 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -48,7 +48,8 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = else let mib,mip = Inductive.lookup_mind_specif env ind in let ctx = Declareops.inductive_polymorphic_context mib in - let u = Univ.UContext.instance ctx in + let u = Univ.AUContext.instance ctx in + let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in let ctxset = Univ.ContextSet.of_context ctx in let ectx = Evd.evar_universe_context_of ctxset in let sigma = Evd.merge_universe_context sigma ectx in @@ -62,7 +63,8 @@ let build_induction_scheme_in_type dep sort ind = let mib,mip = Inductive.lookup_mind_specif env ind in Declareops.inductive_polymorphic_context mib in - let u = Univ.UContext.instance ctx in + let u = Univ.AUContext.instance ctx in + let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in let ctxset = Univ.ContextSet.of_context ctx in let sigma = Evd.merge_universe_context sigma (Evd.evar_universe_context_of ctxset) in let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index c0acdaf57..5a1c260b1 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -362,7 +362,7 @@ let get_body obl = match obl.obl_body with | None -> None | Some (DefinedObl c) -> - let u = Environ.constant_instance (Global.env ()) c in + let u = Univ.AUContext.instance (Environ.constant_context (Global.env ()) c) in let pc = (c, u) in Some (DefinedObl pc) | Some (TermObl c) -> diff --git a/vernac/record.ml b/vernac/record.ml index d61f44cac..366f50454 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -265,7 +265,7 @@ let warn_non_primitive_record = let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in - let u = Declareops.inductive_polymorphic_instance mib in + let u = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in let paramdecls = Inductive.inductive_paramdecls (mib, u) in let poly = Declareops.inductive_is_polymorphic mib in let ctx = @@ -547,7 +547,7 @@ let add_inductive_class ind = let mind, oneind = Global.lookup_inductive ind in let k = let ctx = oneind.mind_arity_ctxt in - let inst = Declareops.inductive_polymorphic_instance mind in + let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mind) in let ty = Inductive.type_of_inductive (push_rel_context ctx (Global.env ())) ((mind,oneind),inst) diff --git a/vernac/search.ml b/vernac/search.ml index 00536e52e..788a2aa4a 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -85,7 +85,7 @@ 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 u = Declareops.inductive_polymorphic_instance mib in + let u = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in let i = (ind, u) in let typ = Inductiveops.type_of_inductive env i in let () = fn (IndRef ind) env typ in |