aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/values.ml4
-rw-r--r--engine/uState.ml2
-rw-r--r--engine/univGen.ml20
-rw-r--r--engine/univGen.mli8
-rw-r--r--engine/univNames.ml9
-rw-r--r--interp/declare.ml6
-rw-r--r--kernel/indtypes.ml2
-rw-r--r--kernel/inductive.ml2
-rw-r--r--kernel/uGraph.ml2
-rw-r--r--kernel/univ.ml50
-rw-r--r--kernel/univ.mli31
-rw-r--r--library/nametab.ml15
-rw-r--r--library/nametab.mli12
-rw-r--r--pretyping/pretyping.ml6
-rw-r--r--stm/asyncTaskQueue.ml2
15 files changed, 106 insertions, 65 deletions
diff --git a/checker/values.ml b/checker/values.ml
index dcb2bca81a..f73e19a972 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -93,9 +93,9 @@ let v_cons = v_tuple "constructor" [|v_ind;Int|]
(** kernel/univ *)
-
+let v_level_qualid = v_tuple "Level.Qualid.t" [|v_dp;Int|]
let v_raw_level = v_sum "raw_level" 2 (* Prop, Set *)
- [|(*Level*)[|Int;v_dp|]; (*Var*)[|Int|]|]
+ [|(*Level*)[|v_level_qualid|]; (*Var*)[|Int|]|]
let v_level = v_tuple "level" [|Int;v_raw_level|]
let v_expr = v_tuple "levelexpr" [|v_level;Int|]
let v_univ = List v_expr
diff --git a/engine/uState.ml b/engine/uState.ml
index 6aecc368e6..56b7a16ace 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -533,7 +533,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 = UnivGen.new_univ_level () in
+ let u = UnivGen.fresh_level () in
let ctx' = Univ.ContextSet.add_universe u ctx in
let uctx', pred =
match rigid with
diff --git a/engine/univGen.ml b/engine/univGen.ml
index 130aa06f53..5aa4734b23 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -14,25 +14,21 @@ open Constr
open Univ
(* 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
+ ~build:(fun n -> Level.Id.make n)
-let fresh_level () = new_univ_level ()
+let fresh_level () =
+ let id = new_univ_id () in
+ Univ.Level.make2 (Global.current_dirpath ()) id
(* 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 new_univ () = Univ.Universe.make (fresh_level ())
+let new_Type () = mkType (new_univ ())
+let new_Type_sort () = Type (new_univ ())
let fresh_instance auctx =
- let inst = Array.init (AUContext.size auctx) (fun _ -> new_univ_level()) in
+ let inst = Array.init (AUContext.size auctx) (fun _ -> fresh_level()) in
let ctx = Array.fold_right LSet.add inst LSet.empty in
let inst = Instance.of_array inst in
inst, (ctx, AUContext.instantiate inst auctx)
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 8af5f8fdb0..66e80368a4 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -15,14 +15,12 @@ open Univ
(** The global universe counter *)
-type universe_id = DirPath.t * int
-
-val set_remote_new_univ_id : universe_id RemoteCounter.installer
+val set_remote_new_univ_id : Level.Id.t 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_id : unit -> Level.Id.t
+val fresh_level : unit -> Level.t
val new_univ : unit -> Universe.t
[@@ocaml.deprecated "Use [new_univ_level]"]
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 1019f8f0c2..6bf1187b65 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -15,12 +15,13 @@ open Univ
let qualid_of_level l =
match Level.name l with
- | Some (d, n as na) ->
+ | Some qid ->
begin
- try Nametab.shortest_qualid_of_universe na
+ try Nametab.shortest_qualid_of_universe qid
with Not_found ->
- let name = Id.of_string_soft (string_of_int n) in
- Libnames.make_qualid d name
+ let (dp,n) = Level.Qualid.repr qid in
+ let name = Id.of_string_soft (Level.Id.to_string n) in
+ Libnames.make_qualid dp name
end
| None ->
Libnames.qualid_of_ident @@ Id.of_string_soft (Level.to_string l)
diff --git a/interp/declare.ml b/interp/declare.ml
index 1e972d3e35..0c9d26dd01 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -469,7 +469,7 @@ type universe_source =
| QualifiedUniv of Id.t (* global universe introduced by some global value *)
| UnqualifiedUniv (* other global universe *)
-type universe_name_decl = universe_source * (Id.t * Nametab.universe_id) list
+type universe_name_decl = universe_source * (Id.t * Univ.Level.Qualid.t) list
let check_exists sp =
if Nametab.exists_universe sp then
@@ -543,9 +543,9 @@ let do_universe poly l =
let l =
List.map (fun {CAst.v=id} ->
let lev = UnivGen.new_univ_id () in
- (id, lev)) l
+ (id, Univ.Level.Qualid.make (Global.current_dirpath ()) lev)) l
in
- let ctx = List.fold_left (fun ctx (_,(dp,i)) -> Univ.LSet.add (Univ.Level.make dp i) ctx)
+ let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx)
Univ.LSet.empty l, Univ.Constraint.empty
in
let () = declare_universe_context poly ctx in
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index a4a02791b4..8efda16d64 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -218,7 +218,7 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : typ
let check_subtyping cumi paramsctxt env_ar inds =
let numparams = Context.Rel.nhyps paramsctxt in
let uctx = CumulativityInfo.univ_context cumi in
- let new_levels = Array.init (UContext.size uctx) (Level.make DirPath.empty) in
+ let new_levels = Array.init (UContext.size uctx) (fun i -> Level.make2 DirPath.empty (Level.Id.make i)) in
let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap)
LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels
in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 9bbcf07f7e..30d96a22e0 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -594,7 +594,7 @@ let rec ienv_decompose_prod (env,_ as ienv) n c =
| _ -> assert false
let lambda_implicit_lift n a =
- let level = Level.make (DirPath.make [Id.of_string "implicit"]) 0 in
+ let level = Level.make2 (DirPath.make [Id.of_string "implicit"]) (Level.Id.make 0) in
let implicit_sort = mkType (Universe.make level) in
let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in
iterate lambda_implicit n (lift n a)
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index afdc8f1511..064fffe98e 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -921,7 +921,7 @@ let sort_universes g =
let types = Array.init (max_lvl + 1) (function
| 0 -> Level.prop
| 1 -> Level.set
- | n -> Level.make mp (n-2))
+ | n -> Level.make2 mp (Level.Id.make (n-2)))
in
let g = Array.fold_left (fun g u ->
let g, u = safe_repr g u in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 2b3b4f9486..57a5dce8a4 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -36,10 +36,35 @@ open Util
module RawLevel =
struct
open Names
+
+ module Id = struct
+ type t = int
+
+ let make i = i
+ let to_string i = string_of_int i
+
+ end
+
+ module Qualid = struct
+ type t = DirPath.t * Id.t
+
+ let make dp i = (dp,i)
+ let repr x = x
+
+ let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i'
+
+ let hash (d,i) = Hashset.Combine.combine i (DirPath.hash d)
+
+ let compare (d, i) (d', i') =
+ let c = Int.compare i i' in
+ if Int.equal c 0 then DirPath.compare d d'
+ else c
+ end
+
type t =
| Prop
| Set
- | Level of int * DirPath.t
+ | Level of Qualid.t
| Var of int
(* Hash-consing *)
@@ -49,7 +74,7 @@ struct
match x, y with
| Prop, Prop -> true
| Set, Set -> true
- | Level (n,d), Level (n',d') ->
+ | Level (d,n), Level (d',n') ->
Int.equal n n' && DirPath.equal d d'
| Var n, Var n' -> Int.equal n n'
| _ -> false
@@ -62,7 +87,7 @@ struct
| Set, Set -> 0
| Set, _ -> -1
| _, Set -> 1
- | Level (i1, dp1), Level (i2, dp2) ->
+ | Level (dp1, i1), Level (dp2, i2) ->
if i1 < i2 then -1
else if i1 > i2 then 1
else DirPath.compare dp1 dp2
@@ -83,9 +108,9 @@ struct
let hcons = function
| Prop as x -> x
| Set as x -> x
- | Level (n,d) as x ->
+ | Level (d,n) as x ->
let d' = Names.DirPath.hcons d in
- if d' == d then x else Level (n,d')
+ if d' == d then x else Level (d',n)
| Var _n as x -> x
open Hashset.Combine
@@ -94,18 +119,20 @@ struct
| Prop -> combinesmall 1 0
| Set -> combinesmall 1 1
| Var n -> combinesmall 2 n
- | Level (n, d) -> combinesmall 3 (combine n (Names.DirPath.hash d))
+ | Level (d, n) -> combinesmall 3 (combine n (Names.DirPath.hash d))
end
module Level = struct
- open Names
+ module Id = RawLevel.Id
+
+ module Qualid = RawLevel.Qualid
type raw_level = RawLevel.t =
| Prop
| Set
- | Level of int * DirPath.t
+ | Level of Qualid.t
| Var of int
(** Embed levels with their hash value *)
@@ -166,7 +193,7 @@ module Level = struct
match data x with
| Prop -> "Prop"
| Set -> "Set"
- | Level (n,d) -> Names.DirPath.to_string d^"."^string_of_int n
+ | Level (d,n) -> Names.DirPath.to_string d^"."^string_of_int n
| Var n -> "Var(" ^ string_of_int n ^ ")"
let pr u = str (to_string u)
@@ -185,11 +212,12 @@ module Level = struct
match data u with
| Var n -> Some n | _ -> None
- let make m n = make (Level (n, Names.DirPath.hcons m))
+ let make2 m n = make (Level (Names.DirPath.hcons m, n))
+ let make qid = make (Level qid)
let name u =
match data u with
- | Level (n, d) -> Some (d, n)
+ | Level (d, n) -> Some (d, n)
| _ -> None
end
diff --git a/kernel/univ.mli b/kernel/univ.mli
index de7b334ae4..69aecac4f3 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -11,9 +11,32 @@
(** Universes. *)
module Level :
sig
+
+ module Id : sig
+ type t
+
+ val make : int -> t
+ val to_string : t -> string
+
+ end
+ (** Non-qualified global universe level *)
+
+ module Qualid : sig
+ type t
+
+ val make : Names.DirPath.t -> Id.t -> t
+ val repr : t -> Names.DirPath.t * Id.t
+ val equal : t -> t -> bool
+ val hash : t -> int
+ val compare : t -> t -> int
+
+ end
+ (** Qualified global universe level *)
+
type t
(** Type of universe levels. A universe level is essentially a unique name
- that will be associated to constraints later on. *)
+ that will be associated to constraints later on. A level can be local to a
+ definition or global. *)
val set : t
val prop : t
@@ -34,7 +57,9 @@ sig
val hash : t -> int
- val make : Names.DirPath.t -> int -> t
+ val make : Qualid.t -> t
+
+ val make2 : Names.DirPath.t -> Id.t -> t
(** Create a new universe level from a unique identifier and an associated
module path. *)
@@ -48,7 +73,7 @@ sig
val var_index : t -> int option
- val name : t -> (Names.DirPath.t * int) option
+ val name : t -> Qualid.t option
end
(** Sets of universe levels *)
diff --git a/library/nametab.ml b/library/nametab.ml
index e29c7b2960..ab69da3467 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -347,12 +347,10 @@ module DirTab = Make(DirPath')(GlobDirRef)
type dirtab = DirTab.t
let the_dirtab = Summary.ref ~name:"dirtab" (DirTab.empty : dirtab)
-type universe_id = DirPath.t * int
-
module UnivIdEqual =
struct
- type t = universe_id
- let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i'
+ type t = Univ.Level.Qualid.t
+ let equal = Univ.Level.Qualid.equal
end
module UnivTab = Make(FullPath)(UnivIdEqual)
type univtab = UnivTab.t
@@ -375,12 +373,9 @@ let the_modtyperevtab = Summary.ref ~name:"modtyperevtab" (MPmap.empty : mptrevt
module UnivIdOrdered =
struct
- type t = universe_id
- let hash (d, i) = i + DirPath.hash d
- let compare (d, i) (d', i') =
- let c = Int.compare i i' in
- if Int.equal c 0 then DirPath.compare d d'
- else c
+ type t = Univ.Level.Qualid.t
+ let hash = Univ.Level.Qualid.hash
+ let compare = Univ.Level.Qualid.compare
end
module UnivIdMap = HMap.Make(UnivIdOrdered)
diff --git a/library/nametab.mli b/library/nametab.mli
index 24af07619d..496c76d9b0 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -120,11 +120,9 @@ val push_modtype : visibility -> full_path -> ModPath.t -> unit
val push_dir : visibility -> DirPath.t -> GlobDirRef.t -> unit
val push_syndef : visibility -> full_path -> syndef_name -> unit
-type universe_id = DirPath.t * int
+module UnivIdMap : CMap.ExtS with type key = Univ.Level.Qualid.t
-module UnivIdMap : CMap.ExtS with type key = universe_id
-
-val push_universe : visibility -> full_path -> universe_id -> unit
+val push_universe : visibility -> full_path -> Univ.Level.Qualid.t -> unit
(** {6 The following functions perform globalization of qualified names } *)
@@ -139,7 +137,7 @@ val locate_modtype : qualid -> ModPath.t
val locate_dir : qualid -> GlobDirRef.t
val locate_module : qualid -> ModPath.t
val locate_section : qualid -> DirPath.t
-val locate_universe : qualid -> universe_id
+val locate_universe : qualid -> Univ.Level.Qualid.t
(** These functions globalize user-level references into global
references, like [locate] and co, but raise a nice error message
@@ -196,7 +194,7 @@ val path_of_modtype : ModPath.t -> full_path
(** A universe_id might not be registered with a corresponding user name.
@raise Not_found if the universe was not introduced by the user. *)
-val path_of_universe : universe_id -> full_path
+val path_of_universe : Univ.Level.Qualid.t -> full_path
(** Returns in particular the dirpath or the basename of the full path
associated to global reference *)
@@ -218,7 +216,7 @@ val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid
val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid
val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid
-val shortest_qualid_of_universe : ?loc:Loc.t -> universe_id -> qualid
+val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.Qualid.t -> qualid
(** Deprecated synonyms *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f5e48bcd39..d01c44811f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -120,8 +120,8 @@ let interp_known_universe_level evd qid =
if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid
else raise Not_found
with Not_found ->
- let univ, k = Nametab.locate_universe qid in
- Univ.Level.make univ k
+ let qid = Nametab.locate_universe qid in
+ Univ.Level.make qid
let interp_universe_level_name ~anon_rigidity evd qid =
try evd, interp_known_universe_level evd qid
@@ -140,7 +140,7 @@ let interp_universe_level_name ~anon_rigidity evd qid =
user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
(Pp.(str "Undeclared global universe: " ++ Libnames.pr_qualid qid))
in
- let level = Univ.Level.make dp num in
+ let level = Univ.Level.make2 dp (Univ.Level.Id.make num) in
let evd =
try Evd.add_global_univ evd level
with UGraph.AlreadyDeclared -> evd
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 94e04d1842..b834fb71e4 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -60,7 +60,7 @@ module Make(T : Task) () = struct
type request = Request of T.request
type more_data =
- | MoreDataUnivLevel of UnivGen.universe_id list
+ | MoreDataUnivLevel of Univ.Level.Id.t list
let slave_respond (Request r) =
let res = T.perform r in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 06:34:38 +0000