From 0d9a91113c4112eece0680e433f435fdfb39ea4b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 7 Jul 2017 16:33:47 +0200 Subject: Getting rid of simple calls to AUContext.instance. This function breaks the abstraction barrier of abstract universe contexts, as it provides a way to observe the bound names of such a context. We remove all the uses that can be easily get rid of with the current API. --- library/lib.ml | 3 ++- library/univops.ml | 39 --------------------------------------- library/univops.mli | 2 -- 3 files changed, 2 insertions(+), 42 deletions(-) (limited to 'library') diff --git a/library/lib.ml b/library/lib.ml index 009eb88fc1..439f83578d 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -465,9 +465,10 @@ let add_section_replacement f g poly hyps = let () = check_same_poly poly vars in let sechyps,ctx = extract_hyps (vars,hyps) in let ctx = Univ.ContextSet.to_context ctx in + let inst = Univ.UContext.instance ctx in let subst, ctx = Univ.abstract_universes ctx in let args = instance_from_variable_context (List.rev sechyps) in - sectab := (vars,f (Univ.AUContext.instance ctx,args) exps, + sectab := (vars,f (inst,args) exps, g (sechyps,subst,ctx) abs)::sl let add_section_kn poly kn = diff --git a/library/univops.ml b/library/univops.ml index 669be2d452..3bafb824d1 100644 --- a/library/univops.ml +++ b/library/univops.ml @@ -8,7 +8,6 @@ open Term open Univ -open Declarations let universes_of_constr c = let rec aux s c = @@ -21,44 +20,6 @@ let universes_of_constr c = | _ -> fold_constr aux s c in aux LSet.empty c -let universes_of_inductive mind = - let process auctx = - let u = Univ.AUContext.instance auctx in - let univ_of_one_ind oind = - let arity_univs = - Context.Rel.fold_outside - (fun decl unvs -> - Univ.LSet.union - (Context.Rel.Declaration.fold_constr - (fun cnstr unvs -> - let cnstr = Vars.subst_instance_constr u cnstr in - Univ.LSet.union - (universes_of_constr cnstr) unvs) - decl Univ.LSet.empty) unvs) - oind.mind_arity_ctxt ~init:Univ.LSet.empty - in - Array.fold_left (fun unvs cns -> - let cns = Vars.subst_instance_constr u cns in - Univ.LSet.union (universes_of_constr cns) unvs) arity_univs - oind.mind_nf_lc - in - let univs = - Array.fold_left - (fun unvs pk -> - Univ.LSet.union - (univ_of_one_ind pk) unvs - ) - Univ.LSet.empty mind.mind_packets - in - let mindcnt = Univ.UContext.constraints (Univ.instantiate_univ_context auctx) in - let univs = Univ.LSet.union univs (Univ.universes_of_constraints mindcnt) in - univs - in - match mind.mind_universes with - | Monomorphic_ind _ -> LSet.empty - | Polymorphic_ind auctx -> process auctx - | Cumulative_ind cumi -> process (Univ.ACumulativityInfo.univ_context cumi) - let restrict_universe_context (univs,csts) s = (* Universes that are not necessary to typecheck the term. E.g. univs introduced by tactics and not used in the proof term. *) diff --git a/library/univops.mli b/library/univops.mli index b5f7715b11..09147cb41c 100644 --- a/library/univops.mli +++ b/library/univops.mli @@ -8,10 +8,8 @@ open Term open Univ -open Declarations (** Shrink a universe context to a restricted set of variables *) val universes_of_constr : constr -> universe_set -val universes_of_inductive : mutual_inductive_body -> universe_set val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set -- cgit v1.2.3 From 012f5fb722a9d5dcef82c800aa54ed50c0a58957 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 10 Jul 2017 19:11:20 +0200 Subject: Safe API for accessing universe constraints of global references. Instead of returning either an instance or the set of constraints, we rather return the corresponding abstracted context. We also push back all uses of abstraction-breaking calls from these functions out of the kernel. --- library/global.ml | 48 ++++++++++++++++++++++++------------------------ library/global.mli | 2 +- 2 files changed, 25 insertions(+), 25 deletions(-) (limited to 'library') diff --git a/library/global.ml b/library/global.ml index 8b59c84dda..09c202c500 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 754fa1516b..5ddf54b4af 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 } *) -- cgit v1.2.3 From 91df402729f70144a4e4d198c4384dc515920e59 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 11 Jul 2017 15:42:43 +0200 Subject: Moving the last bits of abtraction-breaking code out of the kernel. --- library/global.ml | 17 ++++++++++++++++- library/heads.ml | 2 +- 2 files changed, 17 insertions(+), 2 deletions(-) (limited to 'library') diff --git a/library/global.ml b/library/global.ml index 09c202c500..e90151bffe 100644 --- a/library/global.ml +++ b/library/global.ml @@ -122,7 +122,22 @@ let lookup_modtype kn = lookup_modtype kn (env()) let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ()) let opaque_tables () = Environ.opaque_tables (env ()) -let body_of_constant_body cb = Declareops.body_of_constant (opaque_tables ()) cb + +let instantiate cb c = + let open Declarations in + match cb.const_universes with + | Monomorphic_const _ -> c + | Polymorphic_const ctx -> + Vars.subst_instance_constr (Univ.AUContext.instance ctx) c + +let body_of_constant_body cb = + let open Declarations in + let otab = opaque_tables () in + match cb.const_body with + | Undef _ -> None + | Def c -> Some (instantiate cb (Mod_subst.force_constr c)) + | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof otab o)) + let body_of_constant cst = body_of_constant_body (lookup_constant cst) (** Operations on kernel names *) diff --git a/library/heads.ml b/library/heads.ml index 0f420c0e65..a1cb812429 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -128,7 +128,7 @@ let compute_head = function let is_Def = function Declarations.Def _ -> true | _ -> false in let body = if cb.Declarations.const_proj = None && is_Def cb.Declarations.const_body - then Declareops.body_of_constant (Environ.opaque_tables env) cb else None + then Global.body_of_constant cst else None in (match body with | None -> RigidHead (RigidParameter cst) -- cgit v1.2.3