From a51dda2344679dc6d9145f3f34acad29721f6c75 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 28 Apr 2018 19:26:21 +0200 Subject: Split off Universes functions dealing with generating new universes. --- engine/engine.mllib | 1 + engine/evd.ml | 10 +- engine/uState.ml | 4 +- engine/univGen.ml | 246 +++++++++++++++++++++++++++++++++++++++++++++++ engine/univGen.mli | 80 ++++++++++++++++ engine/universes.ml | 264 ++++++--------------------------------------------- engine/universes.mli | 154 ++++++++++++++++-------------- 7 files changed, 448 insertions(+), 311 deletions(-) create mode 100644 engine/univGen.ml create mode 100644 engine/univGen.mli (limited to 'engine') diff --git a/engine/engine.mllib b/engine/engine.mllib index 207dbde1e..512908e13 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -1,4 +1,5 @@ UnivNames +UnivGen Universes Univops UState diff --git a/engine/evd.ml b/engine/evd.ml index 20a7c80ea..b2b8e7ccc 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -804,19 +804,19 @@ let make_flexible_variable evd ~algebraic u = (****************************************) let fresh_sort_in_family ?loc ?(rigid=univ_flexible) env evd s = - with_context_set ?loc rigid evd (Universes.fresh_sort_in_family env s) + with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family env s) let fresh_constant_instance ?loc env evd c = - with_context_set ?loc univ_flexible evd (Universes.fresh_constant_instance env c) + with_context_set ?loc univ_flexible evd (UnivGen.fresh_constant_instance env c) let fresh_inductive_instance ?loc env evd i = - with_context_set ?loc univ_flexible evd (Universes.fresh_inductive_instance env i) + with_context_set ?loc univ_flexible evd (UnivGen.fresh_inductive_instance env i) let fresh_constructor_instance ?loc env evd c = - with_context_set ?loc univ_flexible evd (Universes.fresh_constructor_instance env c) + with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c) let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr = - with_context_set ?loc rigid evd (Universes.fresh_global_instance ?names env gr) + with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?names env gr) let whd_sort_variable evd t = t diff --git a/engine/uState.ml b/engine/uState.ml index ffb54d441..839bb5ae9 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -471,7 +471,7 @@ let emit_side_effects eff u = let new_univ_variable ?loc rigid name ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = - let u = Universes.new_univ_level () in + let u = UnivGen.new_univ_level () in let ctx' = Univ.ContextSet.add_universe u ctx in let uctx', pred = match rigid with @@ -582,7 +582,7 @@ let fix_undefined_variables uctx = uctx_univ_algebraic = algs' } let refresh_undefined_univ_variables uctx = - let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in + let subst, ctx' = UnivGen.fresh_universe_context_set_instance uctx.uctx_local in let subst_fn u = Univ.subst_univs_level_level subst u in let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (subst_fn u) acc) uctx.uctx_univ_algebraic Univ.LSet.empty diff --git a/engine/univGen.ml b/engine/univGen.ml new file mode 100644 index 000000000..796a1bcc1 --- /dev/null +++ b/engine/univGen.ml @@ -0,0 +1,246 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Global.current_dirpath (), n) + +let new_univ_level () = + let dp, id = new_univ_id () in + Univ.Level.make dp id + +let fresh_level () = new_univ_level () + +(* TODO: remove *) +let new_univ dp = Univ.Universe.make (new_univ_level dp) +let new_Type dp = mkType (new_univ dp) +let new_Type_sort dp = Type (new_univ dp) + +let fresh_universe_instance ctx = + let init _ = new_univ_level () in + Instance.of_array (Array.init (AUContext.size ctx) init) + +let fresh_instance_from_context ctx = + let inst = fresh_universe_instance ctx in + let constraints = AUContext.instantiate inst ctx in + inst, constraints + +let fresh_instance ctx = + let ctx' = ref LSet.empty in + let init _ = + let u = new_univ_level () in + ctx' := LSet.add u !ctx'; u + in + let inst = Instance.of_array (Array.init (AUContext.size ctx) init) + in !ctx', inst + +let existing_instance ctx inst = + let () = + let len1 = Array.length (Instance.to_array inst) + and len2 = AUContext.size ctx in + if not (len1 == len2) then + CErrors.user_err ~hdr:"Universes" + Pp.(str "Polymorphic constant expected " ++ int len2 ++ + str" levels but was given " ++ int len1) + else () + in LSet.empty, inst + +let fresh_instance_from ctx inst = + let ctx', inst = + match inst with + | Some inst -> existing_instance ctx inst + | None -> fresh_instance ctx + in + let constraints = AUContext.instantiate inst ctx in + inst, (ctx', constraints) + +(** Fresh universe polymorphic construction *) + +let fresh_constant_instance env c inst = + let cb = lookup_constant c env in + match cb.Declarations.const_universes with + | Declarations.Monomorphic_const _ -> ((c,Instance.empty), ContextSet.empty) + | Declarations.Polymorphic_const auctx -> + let inst, ctx = + fresh_instance_from auctx inst + in + ((c, inst), ctx) + +let fresh_inductive_instance env ind inst = + let mib, mip = Inductive.lookup_mind_specif env ind in + match mib.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + ((ind,Instance.empty), ContextSet.empty) + | Declarations.Polymorphic_ind uactx -> + let inst, ctx = (fresh_instance_from uactx) inst in + ((ind,inst), ctx) + | Declarations.Cumulative_ind acumi -> + let inst, ctx = + fresh_instance_from (Univ.ACumulativityInfo.univ_context acumi) inst + in ((ind,inst), ctx) + +let fresh_constructor_instance env (ind,i) inst = + let mib, mip = Inductive.lookup_mind_specif env ind in + match mib.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> (((ind,i),Instance.empty), ContextSet.empty) + | Declarations.Polymorphic_ind auctx -> + let inst, ctx = fresh_instance_from auctx inst in + (((ind,i),inst), ctx) + | Declarations.Cumulative_ind acumi -> + let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in + (((ind,i),inst), ctx) + +open Globnames + +let fresh_global_instance ?names env gr = + match gr with + | VarRef id -> mkVar id, ContextSet.empty + | ConstRef sp -> + let c, ctx = fresh_constant_instance env sp names in + mkConstU c, ctx + | ConstructRef sp -> + let c, ctx = fresh_constructor_instance env sp names in + mkConstructU c, ctx + | IndRef sp -> + let c, ctx = fresh_inductive_instance env sp names in + mkIndU c, ctx + +let fresh_constant_instance env sp = + fresh_constant_instance env sp None + +let fresh_inductive_instance env sp = + fresh_inductive_instance env sp None + +let fresh_constructor_instance env sp = + fresh_constructor_instance env sp None + +let constr_of_global gr = + let c, ctx = fresh_global_instance (Global.env ()) gr in + if not (Univ.ContextSet.is_empty ctx) then + if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then + (* Should be an error as we might forget constraints, allow for now + to make firstorder work with "using" clauses *) + c + else CErrors.user_err ~hdr:"constr_of_global" + Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ + str " would forget universes.") + else c + +let constr_of_global_univ (gr,u) = + match gr with + | VarRef id -> mkVar id + | ConstRef sp -> mkConstU (sp,u) + | ConstructRef sp -> mkConstructU (sp,u) + | IndRef sp -> mkIndU (sp,u) + +let fresh_global_or_constr_instance env = function + | IsConstr c -> c, ContextSet.empty + | IsGlobal gr -> fresh_global_instance env gr + +let global_of_constr c = + match kind c with + | Const (c, u) -> ConstRef c, u + | Ind (i, u) -> IndRef i, u + | Construct (c, u) -> ConstructRef c, u + | Var id -> VarRef id, Instance.empty + | _ -> raise Not_found + +open Declarations + +let type_of_reference env r = + match r with + | VarRef id -> Environ.named_type id env, ContextSet.empty + | ConstRef c -> + let cb = Environ.lookup_constant c env in + let ty = cb.const_type in + begin + match cb.const_universes with + | Monomorphic_const _ -> ty, ContextSet.empty + | Polymorphic_const auctx -> + let inst, ctx = fresh_instance_from auctx None in + Vars.subst_instance_constr inst ty, ctx + end + | IndRef ind -> + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in + begin + match mib.mind_universes with + | Monomorphic_ind _ -> + let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in + ty, ContextSet.empty + | Polymorphic_ind auctx -> + let inst, ctx = fresh_instance_from auctx None in + let ty = Inductive.type_of_inductive env (specif, inst) in + ty, ctx + | Cumulative_ind cumi -> + let inst, ctx = + fresh_instance_from (ACumulativityInfo.univ_context cumi) None + in + let ty = Inductive.type_of_inductive env (specif, inst) in + ty, ctx + end + + | ConstructRef cstr -> + let (mib,oib as specif) = + Inductive.lookup_mind_specif env (inductive_of_constructor cstr) + in + begin + match mib.mind_universes with + | Monomorphic_ind _ -> + Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty + | Polymorphic_ind auctx -> + let inst, ctx = fresh_instance_from auctx None in + Inductive.type_of_constructor (cstr,inst) specif, ctx + | Cumulative_ind cumi -> + let inst, ctx = + fresh_instance_from (ACumulativityInfo.univ_context cumi) None + in + Inductive.type_of_constructor (cstr,inst) specif, ctx + end + +let type_of_global t = type_of_reference (Global.env ()) t + +let fresh_sort_in_family env = function + | InProp -> Sorts.prop, ContextSet.empty + | InSet -> Sorts.set, ContextSet.empty + | InType -> + let u = fresh_level () in + Type (Univ.Universe.make u), ContextSet.singleton u + +let new_sort_in_family sf = + fst (fresh_sort_in_family (Global.env ()) sf) + +let extend_context (a, ctx) (ctx') = + (a, ContextSet.union ctx ctx') + +let new_global_univ () = + let u = fresh_level () in + (Univ.Universe.make u, ContextSet.singleton u) + +let fresh_universe_context_set_instance ctx = + if ContextSet.is_empty ctx then LMap.empty, ctx + else + let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in + let univs',subst = LSet.fold + (fun u (univs',subst) -> + let u' = fresh_level () in + (LSet.add u' univs', LMap.add u u' subst)) + univs (LSet.empty, LMap.empty) + in + let cst' = subst_univs_level_constraints subst cst in + subst, (univs', cst') diff --git a/engine/univGen.mli b/engine/univGen.mli new file mode 100644 index 000000000..8169dbda4 --- /dev/null +++ b/engine/univGen.mli @@ -0,0 +1,80 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* universe_id +val new_univ_level : unit -> Level.t +val new_univ : unit -> Universe.t +val new_Type : unit -> types +val new_Type_sort : unit -> Sorts.t + +val new_global_univ : unit -> Universe.t in_universe_context_set +val new_sort_in_family : Sorts.family -> Sorts.t + +(** Build a fresh instance for a given context, its associated substitution and + the instantiated constraints. *) + +val fresh_instance_from_context : AUContext.t -> + Instance.t constrained + +val fresh_instance_from : AUContext.t -> Instance.t option -> + Instance.t in_universe_context_set + +val fresh_sort_in_family : env -> Sorts.family -> + Sorts.t in_universe_context_set +val fresh_constant_instance : env -> Constant.t -> + pconstant in_universe_context_set +val fresh_inductive_instance : env -> inductive -> + pinductive in_universe_context_set +val fresh_constructor_instance : env -> constructor -> + pconstructor in_universe_context_set + +val fresh_global_instance : ?names:Univ.Instance.t -> env -> GlobRef.t -> + constr in_universe_context_set + +val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> + constr in_universe_context_set + +(** Get fresh variables for the universe context. + Useful to make tactics that manipulate constrs in universe contexts polymorphic. *) +val fresh_universe_context_set_instance : ContextSet.t -> + universe_level_subst * ContextSet.t + +(** Raises [Not_found] if not a global reference. *) +val global_of_constr : constr -> GlobRef.t puniverses + +val constr_of_global_univ : GlobRef.t puniverses -> constr + +val extend_context : 'a in_universe_context_set -> ContextSet.t -> + 'a in_universe_context_set + +(** Create a fresh global in the global environment, without side effects. + BEWARE: this raises an ANOMALY on polymorphic constants/inductives: + the constraints should be properly added to an evd. + See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for + the proper way to get a fresh copy of a global reference. *) +val constr_of_global : GlobRef.t -> constr + +(** Returns the type of the global reference, by creating a fresh instance of polymorphic + references and computing their instantiated universe context. (side-effect on the + universe counter, use with care). *) +val type_of_global : GlobRef.t -> types in_universe_context_set diff --git a/engine/universes.ml b/engine/universes.ml index 1dccde025..29c9bd017 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -11,9 +11,7 @@ open Sorts open Util open Pp -open Names open Constr -open Environ open Univ (* To disallow minimization to Set *) @@ -214,226 +212,6 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu = let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' 0 m n in if res then Some !cstrs else None -(* Generator of levels *) -type universe_id = DirPath.t * int - -let new_univ_id, set_remote_new_univ_id = - RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1) - ~build:(fun n -> Global.current_dirpath (), n) - -let new_univ_level () = - let dp, id = new_univ_id () in - Univ.Level.make dp id - -let fresh_level () = new_univ_level () - -(* TODO: remove *) -let new_univ dp = Univ.Universe.make (new_univ_level dp) -let new_Type dp = mkType (new_univ dp) -let new_Type_sort dp = Type (new_univ dp) - -let fresh_universe_instance ctx = - let init _ = new_univ_level () in - Instance.of_array (Array.init (AUContext.size ctx) init) - -let fresh_instance_from_context ctx = - let inst = fresh_universe_instance ctx in - let constraints = AUContext.instantiate inst ctx in - inst, constraints - -let fresh_instance ctx = - let ctx' = ref LSet.empty in - let init _ = - let u = new_univ_level () in - ctx' := LSet.add u !ctx'; u - in - let inst = Instance.of_array (Array.init (AUContext.size ctx) init) - in !ctx', inst - -let existing_instance ctx inst = - let () = - let len1 = Array.length (Instance.to_array inst) - and len2 = AUContext.size ctx in - if not (len1 == len2) then - CErrors.user_err ~hdr:"Universes" - (str "Polymorphic constant expected " ++ int len2 ++ - str" levels but was given " ++ int len1) - else () - in LSet.empty, inst - -let fresh_instance_from ctx inst = - let ctx', inst = - match inst with - | Some inst -> existing_instance ctx inst - | None -> fresh_instance ctx - in - let constraints = AUContext.instantiate inst ctx in - inst, (ctx', constraints) - -(** Fresh universe polymorphic construction *) - -let fresh_constant_instance env c inst = - let cb = lookup_constant c env in - match cb.Declarations.const_universes with - | Declarations.Monomorphic_const _ -> ((c,Instance.empty), ContextSet.empty) - | Declarations.Polymorphic_const auctx -> - let inst, ctx = - fresh_instance_from auctx inst - in - ((c, inst), ctx) - -let fresh_inductive_instance env ind inst = - let mib, mip = Inductive.lookup_mind_specif env ind in - match mib.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - ((ind,Instance.empty), ContextSet.empty) - | Declarations.Polymorphic_ind uactx -> - let inst, ctx = (fresh_instance_from uactx) inst in - ((ind,inst), ctx) - | Declarations.Cumulative_ind acumi -> - let inst, ctx = - fresh_instance_from (Univ.ACumulativityInfo.univ_context acumi) inst - in ((ind,inst), ctx) - -let fresh_constructor_instance env (ind,i) inst = - let mib, mip = Inductive.lookup_mind_specif env ind in - match mib.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> (((ind,i),Instance.empty), ContextSet.empty) - | Declarations.Polymorphic_ind auctx -> - let inst, ctx = fresh_instance_from auctx inst in - (((ind,i),inst), ctx) - | Declarations.Cumulative_ind acumi -> - let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in - (((ind,i),inst), ctx) - -open Globnames - -let fresh_global_instance ?names env gr = - match gr with - | VarRef id -> mkVar id, ContextSet.empty - | ConstRef sp -> - let c, ctx = fresh_constant_instance env sp names in - mkConstU c, ctx - | ConstructRef sp -> - let c, ctx = fresh_constructor_instance env sp names in - mkConstructU c, ctx - | IndRef sp -> - let c, ctx = fresh_inductive_instance env sp names in - mkIndU c, ctx - -let fresh_constant_instance env sp = - fresh_constant_instance env sp None - -let fresh_inductive_instance env sp = - fresh_inductive_instance env sp None - -let fresh_constructor_instance env sp = - fresh_constructor_instance env sp None - -let constr_of_global gr = - let c, ctx = fresh_global_instance (Global.env ()) gr in - if not (Univ.ContextSet.is_empty ctx) then - if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then - (* Should be an error as we might forget constraints, allow for now - to make firstorder work with "using" clauses *) - c - else CErrors.user_err ~hdr:"constr_of_global" - Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ - str " would forget universes.") - else c - -let constr_of_reference = constr_of_global - -let constr_of_global_univ (gr,u) = - match gr with - | VarRef id -> mkVar id - | ConstRef sp -> mkConstU (sp,u) - | ConstructRef sp -> mkConstructU (sp,u) - | IndRef sp -> mkIndU (sp,u) - -let fresh_global_or_constr_instance env = function - | IsConstr c -> c, ContextSet.empty - | IsGlobal gr -> fresh_global_instance env gr - -let global_of_constr c = - match kind c with - | Const (c, u) -> ConstRef c, u - | Ind (i, u) -> IndRef i, u - | Construct (c, u) -> ConstructRef c, u - | Var id -> VarRef id, Instance.empty - | _ -> raise Not_found - -open Declarations - -let type_of_reference env r = - match r with - | VarRef id -> Environ.named_type id env, ContextSet.empty - | ConstRef c -> - let cb = Environ.lookup_constant c env in - let ty = cb.const_type in - begin - match cb.const_universes with - | Monomorphic_const _ -> ty, ContextSet.empty - | Polymorphic_const auctx -> - let inst, ctx = fresh_instance_from auctx None in - Vars.subst_instance_constr inst ty, ctx - end - | IndRef ind -> - let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - begin - match mib.mind_universes with - | Monomorphic_ind _ -> - let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in - ty, ContextSet.empty - | Polymorphic_ind auctx -> - let inst, ctx = fresh_instance_from auctx None in - let ty = Inductive.type_of_inductive env (specif, inst) in - ty, ctx - | Cumulative_ind cumi -> - let inst, ctx = - fresh_instance_from (ACumulativityInfo.univ_context cumi) None - in - let ty = Inductive.type_of_inductive env (specif, inst) in - ty, ctx - end - - | ConstructRef cstr -> - let (mib,oib as specif) = - Inductive.lookup_mind_specif env (inductive_of_constructor cstr) - in - begin - match mib.mind_universes with - | Monomorphic_ind _ -> - Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty - | Polymorphic_ind auctx -> - let inst, ctx = fresh_instance_from auctx None in - Inductive.type_of_constructor (cstr,inst) specif, ctx - | Cumulative_ind cumi -> - let inst, ctx = - fresh_instance_from (ACumulativityInfo.univ_context cumi) None - in - Inductive.type_of_constructor (cstr,inst) specif, ctx - end - -let type_of_global t = type_of_reference (Global.env ()) t - -let fresh_sort_in_family env = function - | InProp -> Sorts.prop, ContextSet.empty - | InSet -> Sorts.set, ContextSet.empty - | InType -> - let u = fresh_level () in - Type (Univ.Universe.make u), ContextSet.singleton u - -let new_sort_in_family sf = - fst (fresh_sort_in_family (Global.env ()) sf) - -let extend_context (a, ctx) (ctx') = - (a, ContextSet.union ctx ctx') - -let new_global_univ () = - let u = fresh_level () in - (Univ.Universe.make u, ContextSet.singleton u) - (** Simplification *) let add_list_map u t map = @@ -504,19 +282,6 @@ let subst_univs_constr = CProfile.profile2 subst_univs_constr_key subst_univs_constr else subst_univs_constr -let fresh_universe_context_set_instance ctx = - if ContextSet.is_empty ctx then LMap.empty, ctx - else - let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in - let univs',subst = LSet.fold - (fun u (univs',subst) -> - let u' = fresh_level () in - (LSet.add u' univs', LMap.add u u' subst)) - univs (LSet.empty, LMap.empty) - in - let cst' = subst_univs_level_constraints subst cst in - subst, (univs', cst') - let normalize_univ_variable ~find = let rec aux cur = let b = find cur in @@ -1020,6 +785,8 @@ let solve_constraints_system levels level_bounds level_min = v (** Deprecated *) + +(** UnivNames *) type universe_binders = UnivNames.universe_binders type univ_name_list = UnivNames.univ_name_list @@ -1036,3 +803,30 @@ let register_universe_binders = UnivNames.register_universe_binders let universe_binders_of_global = UnivNames.universe_binders_of_global let universe_binders_with_opt_names = UnivNames.universe_binders_with_opt_names + +(** UnivGen *) +type universe_id = UnivGen.universe_id + +let set_remote_new_univ_id = UnivGen.set_remote_new_univ_id +let new_univ_id = UnivGen.new_univ_id +let new_univ_level = UnivGen.new_univ_level +let new_univ = UnivGen.new_univ +let new_Type = UnivGen.new_Type +let new_Type_sort = UnivGen.new_Type_sort +let new_global_univ = UnivGen.new_global_univ +let new_sort_in_family = UnivGen.new_sort_in_family +let fresh_instance_from_context = UnivGen.fresh_instance_from_context +let fresh_instance_from = UnivGen.fresh_instance_from +let fresh_sort_in_family = UnivGen.fresh_sort_in_family +let fresh_constant_instance = UnivGen.fresh_constant_instance +let fresh_inductive_instance = UnivGen.fresh_inductive_instance +let fresh_constructor_instance = UnivGen.fresh_constructor_instance +let fresh_global_instance = UnivGen.fresh_global_instance +let fresh_global_or_constr_instance = UnivGen.fresh_global_or_constr_instance +let fresh_universe_context_set_instance = UnivGen.fresh_universe_context_set_instance +let global_of_constr = UnivGen.global_of_constr +let constr_of_global_univ = UnivGen.constr_of_global_univ +let extend_context = UnivGen.extend_context +let constr_of_global = UnivGen.constr_of_global +let constr_of_reference = UnivGen.constr_of_global +let type_of_global = UnivGen.type_of_global diff --git a/engine/universes.mli b/engine/universes.mli index aaf295c1d..da4a00751 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -19,22 +19,6 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t) (** Universes *) -(** The global universe counter *) -type universe_id = DirPath.t * int - -val set_remote_new_univ_id : universe_id RemoteCounter.installer - -(** Side-effecting functions creating new universe levels. *) - -val new_univ_id : unit -> universe_id -val new_univ_level : unit -> Level.t -val new_univ : unit -> Universe.t -val new_Type : unit -> types -val new_Type_sort : unit -> Sorts.t - -val new_global_univ : unit -> Universe.t in_universe_context_set -val new_sort_in_family : Sorts.family -> Sorts.t - (** {6 Constraints for type inference} When doing conversion of universes, not only do we have =/<= constraints but @@ -82,43 +66,6 @@ val eq_constr_univs_infer_with : (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option -(** Build a fresh instance for a given context, its associated substitution and - the instantiated constraints. *) - -val fresh_instance_from_context : AUContext.t -> - Instance.t constrained - -val fresh_instance_from : AUContext.t -> Instance.t option -> - Instance.t in_universe_context_set - -val fresh_sort_in_family : env -> Sorts.family -> - Sorts.t in_universe_context_set -val fresh_constant_instance : env -> Constant.t -> - pconstant in_universe_context_set -val fresh_inductive_instance : env -> inductive -> - pinductive in_universe_context_set -val fresh_constructor_instance : env -> constructor -> - pconstructor in_universe_context_set - -val fresh_global_instance : ?names:Univ.Instance.t -> env -> GlobRef.t -> - constr in_universe_context_set - -val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> - constr in_universe_context_set - -(** Get fresh variables for the universe context. - Useful to make tactics that manipulate constrs in universe contexts polymorphic. *) -val fresh_universe_context_set_instance : ContextSet.t -> - universe_level_subst * ContextSet.t - -(** Raises [Not_found] if not a global reference. *) -val global_of_constr : constr -> GlobRef.t puniverses - -val constr_of_global_univ : GlobRef.t puniverses -> constr - -val extend_context : 'a in_universe_context_set -> ContextSet.t -> - 'a in_universe_context_set - (** Simplification and pruning of constraints: [normalize_context_set ctx us] @@ -166,22 +113,6 @@ val normalize_universe_opt_subst : universe_opt_subst -> val normalize_universe_subst : universe_subst -> (Universe.t -> Universe.t) -(** Create a fresh global in the global environment, without side effects. - BEWARE: this raises an ANOMALY on polymorphic constants/inductives: - the constraints should be properly added to an evd. - See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for - the proper way to get a fresh copy of a global reference. *) -val constr_of_global : GlobRef.t -> constr - -(** ** DEPRECATED ** synonym of [constr_of_global] *) -val constr_of_reference : GlobRef.t -> constr -[@@ocaml.deprecated "synonym of [constr_of_global]"] - -(** Returns the type of the global reference, by creating a fresh instance of polymorphic - references and computing their instantiated universe context. (side-effect on the - universe counter, use with care). *) -val type_of_global : GlobRef.t -> types in_universe_context_set - (** Full universes substitutions into terms *) val nf_evars_and_universes_opt_subst : (existential -> constr option) -> @@ -199,6 +130,7 @@ val solve_constraints_system : Universe.t option array -> Universe.t array -> Un Universe.t array (** *********************************** Deprecated *) + [@@@ocaml.warning "-3"] val set_minimization : bool ref [@@ocaml.deprecated "Becoming internal."] @@ -235,3 +167,87 @@ type univ_name_list = UnivNames.univ_name_list val universe_binders_with_opt_names : Globnames.global_reference -> Univ.Level.t list -> univ_name_list option -> universe_binders [@@ocaml.deprecated "Use [UnivNames.universe_binders_with_opt_names]"] + +(** ****** Deprecated: moved to [UnivGen] *) + +type universe_id = UnivGen.universe_id +[@@ocaml.deprecated "Use [UnivGen.universe_id]"] + +val set_remote_new_univ_id : universe_id RemoteCounter.installer +[@@ocaml.deprecated "Use [UnivGen.set_remote_new_univ_id]"] + +val new_univ_id : unit -> universe_id +[@@ocaml.deprecated "Use [UnivGen.new_univ_id]"] + +val new_univ_level : unit -> Level.t +[@@ocaml.deprecated "Use [UnivGen.new_univ_level]"] + +val new_univ : unit -> Universe.t +[@@ocaml.deprecated "Use [UnivGen.new_univ]"] + +val new_Type : unit -> types +[@@ocaml.deprecated "Use [UnivGen.new_Type]"] + +val new_Type_sort : unit -> Sorts.t +[@@ocaml.deprecated "Use [UnivGen.new_Type_sort]"] + +val new_global_univ : unit -> Universe.t in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.new_global_univ]"] + +val new_sort_in_family : Sorts.family -> Sorts.t +[@@ocaml.deprecated "Use [UnivGen.new_sort_in_family]"] + +val fresh_instance_from_context : AUContext.t -> + Instance.t constrained +[@@ocaml.deprecated "Use [UnivGen.fresh_instance_from_context]"] + +val fresh_instance_from : AUContext.t -> Instance.t option -> + Instance.t in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_instance_from]"] + +val fresh_sort_in_family : env -> Sorts.family -> + Sorts.t in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_sort_in_family]"] + +val fresh_constant_instance : env -> Constant.t -> + pconstant in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_constant_instance]"] + +val fresh_inductive_instance : env -> inductive -> + pinductive in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_inductive_instance]"] + +val fresh_constructor_instance : env -> constructor -> + pconstructor in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_constructor_instance]"] + +val fresh_global_instance : ?names:Univ.Instance.t -> env -> Globnames.global_reference -> + constr in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_global_instance]"] + +val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> + constr in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_global_or_constr_instance]"] + +val fresh_universe_context_set_instance : ContextSet.t -> + universe_level_subst * ContextSet.t +[@@ocaml.deprecated "Use [UnivGen.fresh_universe_context_set_instance]"] + +val global_of_constr : constr -> Globnames.global_reference puniverses +[@@ocaml.deprecated "Use [UnivGen.global_of_constr]"] + +val constr_of_global_univ : Globnames.global_reference puniverses -> constr +[@@ocaml.deprecated "Use [UnivGen.constr_of_global_univ]"] + +val extend_context : 'a in_universe_context_set -> ContextSet.t -> + 'a in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.extend_context]"] + +val constr_of_global : Globnames.global_reference -> constr +[@@ocaml.deprecated "Use [UnivGen.constr_of_global]"] + +val constr_of_reference : Globnames.global_reference -> constr +[@@ocaml.deprecated "Use [UnivGen.constr_of_global]"] + +val type_of_global : Globnames.global_reference -> types in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.type_of_global]"] -- cgit v1.2.3