aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml18
-rw-r--r--engine/eConstr.mli4
-rw-r--r--engine/termops.ml1
-rw-r--r--engine/termops.mli2
-rw-r--r--engine/uState.ml12
-rw-r--r--engine/uState.mli1
-rw-r--r--engine/universes.ml64
-rw-r--r--engine/universes.mli20
8 files changed, 96 insertions, 26 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index afdceae06..ea098902a 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -645,6 +645,24 @@ let eq_constr_universes_proj env sigma m n =
let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in
if res then Some !cstrs else None
+let universes_of_constr sigma c =
+ let open Univ in
+ let rec aux s c =
+ match kind sigma c with
+ | Const (_, u) | Ind (_, u) | Construct (_, u) ->
+ LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
+ | Sort u ->
+ let sort = ESorts.kind sigma u in
+ if Sorts.is_small sort then s
+ else
+ let u = Sorts.univ_of_sort sort in
+ LSet.fold LSet.add (Universe.levels u) s
+ | Evar (k, args) ->
+ let concl = Evd.evar_concl (Evd.find sigma k) in
+ fold sigma aux (aux s (of_constr concl)) c
+ | _ -> fold sigma aux s c
+ in aux LSet.empty c
+
open Context
open Environ
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index e9ef302cf..3e6a13f70 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -201,6 +201,10 @@ val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a ->
val iter_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
+(** Gather the universes transitively used in the term, including in the
+ type of evars appearing in it. *)
+val universes_of_constr : Evd.evar_map -> t -> Univ.LSet.t
+
(** {6 Substitutions} *)
module Vars :
diff --git a/engine/termops.ml b/engine/termops.ml
index 07fe90222..a71bdff31 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -288,6 +288,7 @@ let has_no_evar sigma =
with Exit -> false
let pr_evd_level evd = UState.pr_uctx_level (Evd.evar_universe_context evd)
+let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_context evd) l
let pr_evar_universe_context ctx =
let open UState in
diff --git a/engine/termops.mli b/engine/termops.mli
index c9a530076..c1600abe8 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -271,6 +271,8 @@ val is_Prop : Evd.evar_map -> constr -> bool
val is_Set : Evd.evar_map -> constr -> bool
val is_Type : Evd.evar_map -> constr -> bool
+val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.reference
+
(** Combinators on judgments *)
val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment
diff --git a/engine/uState.ml b/engine/uState.ml
index f9a57cce2..c28e78f7d 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -263,13 +263,15 @@ let constrain_variables diff ctx =
in
{ ctx with uctx_local = (univs, local); uctx_univ_variables = vars }
-
-let pr_uctx_level uctx =
+let reference_of_level uctx =
let map, map_rev = uctx.uctx_names in
fun l ->
- try Id.print (Option.get (Univ.LMap.find l map_rev).uname)
+ try Libnames.Ident (Loc.tag @@ Option.get (Univ.LMap.find l map_rev).uname)
with Not_found | Option.IsNone ->
- Universes.pr_with_global_universes l
+ Universes.reference_of_level l
+
+let pr_uctx_level uctx l =
+ Libnames.pr_reference (reference_of_level uctx l)
type universe_decl =
(Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
@@ -430,7 +432,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 (Global.current_dirpath ()) in
+ let u = Universes.new_univ_level () in
let ctx' = Univ.ContextSet.add_universe u ctx in
let uctx', pred =
match rigid with
diff --git a/engine/uState.mli b/engine/uState.mli
index 16fba41e0..2c39e85f7 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -154,3 +154,4 @@ val update_sigma_env : t -> Environ.env -> t
(** {5 Pretty-printing} *)
val pr_uctx_level : t -> Univ.Level.t -> Pp.t
+val reference_of_level : t -> Univ.Level.t -> Libnames.reference
diff --git a/engine/universes.ml b/engine/universes.ml
index d29e8777d..0250295fd 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -14,10 +14,37 @@ open Constr
open Environ
open Univ
open Globnames
-
-let pr_with_global_universes l =
- try Id.print (LMap.find l (snd (Global.global_universe_names ())))
- with Not_found -> Level.pr l
+open Nametab
+
+let reference_of_level l =
+ match Level.name l with
+ | Some (d, n as na) ->
+ let qid =
+ try Nametab.shortest_qualid_of_universe na
+ with Not_found ->
+ let name = Id.of_string_soft (string_of_int n) in
+ Libnames.make_qualid d name
+ in Libnames.Qualid (Loc.tag @@ qid)
+ | None -> Libnames.Ident (Loc.tag @@ Id.of_string_soft (Level.to_string l))
+
+let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l)
+
+(** Global universe information outside the kernel, to handle
+ polymorphic universe names in sections that have to be discharged. *)
+
+let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref)
+
+let add_global_universe u p =
+ match Level.name u with
+ | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map
+ | None -> ()
+
+let is_polymorphic l =
+ match Level.name l with
+ | Some n ->
+ (try Nametab.UnivIdMap.find n !universe_map
+ with Not_found -> false)
+ | None -> false
(** Local universe names of polymorphic references *)
@@ -53,12 +80,14 @@ let ubinder_obj : Globnames.global_reference * universe_binders -> Libobject.obj
rebuild_function = (fun x -> x); }
let register_universe_binders ref ubinders =
- (* Add the polymorphic (section) universes *)
let open Names in
- let ubinders = Id.Map.fold (fun id (poly,lvl) ubinders ->
- if poly then Id.Map.add id lvl ubinders
- else ubinders)
- (fst (Global.global_universe_names ())) ubinders
+ (* Add the polymorphic (section) universes *)
+ let ubinders = UnivIdMap.fold (fun lvl poly ubinders ->
+ let qid = Nametab.shortest_qualid_of_universe lvl in
+ let level = Level.make (fst lvl) (snd lvl) in
+ if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders
+ else ubinders)
+ !universe_map ubinders
in
if not (Id.Map.is_empty ubinders)
then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
@@ -236,14 +265,17 @@ let eq_constr_universes_proj env m n =
res, !cstrs
(* Generator of levels *)
-let new_univ_level, set_remote_new_univ_level =
+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 -> Univ.Level.make (Global.current_dirpath ()) n)
+ ~build:(fun n -> Global.current_dirpath (), n)
-let new_univ_level _ = new_univ_level ()
- (* Univ.Level.make db (new_univ_level ()) *)
+let new_univ_level () =
+ let dp, id = new_univ_id () in
+ Univ.Level.make dp id
-let fresh_level () = new_univ_level (Global.current_dirpath ())
+let fresh_level () = new_univ_level ()
(* TODO: remove *)
let new_univ dp = Univ.Universe.make (new_univ_level dp)
@@ -251,7 +283,7 @@ 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 (Global.current_dirpath ()) in
+ let init _ = new_univ_level () in
Instance.of_array (Array.init (AUContext.size ctx) init)
let fresh_instance_from_context ctx =
@@ -262,7 +294,7 @@ let fresh_instance_from_context ctx =
let fresh_instance ctx =
let ctx' = ref LSet.empty in
let init _ =
- let u = new_univ_level (Global.current_dirpath ()) in
+ let u = new_univ_level () in
ctx' := LSet.add u !ctx'; u
in
let inst = Instance.of_array (Array.init (AUContext.size ctx) init)
diff --git a/engine/universes.mli b/engine/universes.mli
index 1401c4ee8..fc9278eb5 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -18,6 +18,13 @@ val is_set_minimization : unit -> bool
(** Universes *)
val pr_with_global_universes : Level.t -> Pp.t
+val reference_of_level : Level.t -> Libnames.reference
+
+(** Global universe information outside the kernel, to handle
+ polymorphic universes in sections that have to be discharged. *)
+val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
+
+val is_polymorphic : Level.t -> bool
(** Local universe name <-> level mapping *)
@@ -40,14 +47,17 @@ val universe_binders_with_opt_names : Globnames.global_reference ->
Univ.Level.t list -> univ_name_list option -> universe_binders
(** The global universe counter *)
-val set_remote_new_univ_level : Level.t RemoteCounter.installer
+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_level : DirPath.t -> Level.t
-val new_univ : DirPath.t -> Universe.t
-val new_Type : DirPath.t -> types
-val new_Type_sort : DirPath.t -> Sorts.t
+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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 14:13:58 +0000