aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/values.ml4
-rw-r--r--engine/termops.mli2
-rw-r--r--engine/uState.ml6
-rw-r--r--engine/uState.mli2
-rw-r--r--engine/univGen.ml9
-rw-r--r--engine/univGen.mli6
-rw-r--r--engine/univNames.ml17
-rw-r--r--engine/univNames.mli2
-rw-r--r--interp/declare.ml8
-rw-r--r--kernel/indtypes.ml4
-rw-r--r--kernel/inductive.ml6
-rw-r--r--kernel/uGraph.ml2
-rw-r--r--kernel/univ.ml27
-rw-r--r--kernel/univ.mli22
-rw-r--r--library/nametab.ml10
-rw-r--r--library/nametab.mli10
-rw-r--r--pretyping/detyping.ml19
-rw-r--r--pretyping/pretyping.ml2
-rw-r--r--stm/asyncTaskQueue.ml2
19 files changed, 75 insertions, 85 deletions
diff --git a/checker/values.ml b/checker/values.ml
index f73e19a972..863f965896 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_level_global = v_tuple "Level.Global.t" [|v_dp;Int|]
let v_raw_level = v_sum "raw_level" 2 (* Prop, Set *)
- [|(*Level*)[|v_level_qualid|]; (*Var*)[|Int|]|]
+ [|(*Level*)[|v_level_global|]; (*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/termops.mli b/engine/termops.mli
index eef8452e64..7920af8e0e 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -290,7 +290,7 @@ 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.qualid
+val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option
(** Combinators on judgments *)
diff --git a/engine/uState.ml b/engine/uState.ml
index 56b7a16ace..185283225c 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -324,12 +324,14 @@ let constrain_variables diff ctx =
let qualid_of_level uctx =
let map, map_rev = uctx.uctx_names in
fun l ->
- try Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname)
+ try Some (Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname))
with Not_found | Option.IsNone ->
UnivNames.qualid_of_level l
let pr_uctx_level uctx l =
- Libnames.pr_qualid (qualid_of_level uctx l)
+ match qualid_of_level uctx l with
+ | Some qid -> Libnames.pr_qualid qid
+ | None -> Univ.Level.pr l
type ('a, 'b) gen_universe_decl = {
univdecl_instance : 'a; (* Declared universes *)
diff --git a/engine/uState.mli b/engine/uState.mli
index ad0cd5c1bb..5170184ef4 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -188,6 +188,6 @@ val update_sigma_env : t -> Environ.env -> t
(** {5 Pretty-printing} *)
val pr_uctx_level : t -> Univ.Level.t -> Pp.t
-val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid
+val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid option
val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t
diff --git a/engine/univGen.ml b/engine/univGen.ml
index 5aa4734b23..40c4c909fe 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -13,14 +13,17 @@ open Names
open Constr
open Univ
+type univ_unique_id = int
(* Generator of levels *)
let new_univ_id, set_remote_new_univ_id =
RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
- ~build:(fun n -> Level.Id.make n)
+ ~build:(fun n -> n)
+
+let new_univ_global () =
+ Univ.Level.UGlobal.make (Global.current_dirpath ()) (new_univ_id ())
let fresh_level () =
- let id = new_univ_id () in
- Univ.Level.make2 (Global.current_dirpath ()) id
+ Univ.Level.make (new_univ_global ())
(* TODO: remove *)
let new_univ () = Univ.Universe.make (fresh_level ())
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 66e80368a4..b4598e10d0 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -15,11 +15,13 @@ open Univ
(** The global universe counter *)
-val set_remote_new_univ_id : Level.Id.t RemoteCounter.installer
+type univ_unique_id
+val set_remote_new_univ_id : univ_unique_id RemoteCounter.installer
+val new_univ_id : unit -> univ_unique_id (** for the stm *)
(** Side-effecting functions creating new universe levels. *)
-val new_univ_id : unit -> Level.Id.t
+val new_univ_global : unit -> Level.UGlobal.t
val fresh_level : unit -> Level.t
val new_univ : unit -> Universe.t
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 6bf1187b65..19705f9d36 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -16,17 +16,14 @@ open Univ
let qualid_of_level l =
match Level.name l with
| Some qid ->
- begin
- try Nametab.shortest_qualid_of_universe qid
- with Not_found ->
- 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)
+ (try Some (Nametab.shortest_qualid_of_universe qid)
+ with Not_found -> None)
+ | None -> None
-let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l)
+let pr_with_global_universes l =
+ match qualid_of_level l with
+ | Some qid -> Libnames.pr_qualid qid
+ | None -> Level.pr l
(** Global universe information outside the kernel, to handle
polymorphic universe names in sections that have to be discharged. *)
diff --git a/engine/univNames.mli b/engine/univNames.mli
index 6e68153ac2..e9c517babf 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -11,7 +11,7 @@
open Univ
val pr_with_global_universes : Level.t -> Pp.t
-val qualid_of_level : Level.t -> Libnames.qualid
+val qualid_of_level : Level.t -> Libnames.qualid option
(** Local universe name <-> level mapping *)
diff --git a/interp/declare.ml b/interp/declare.ml
index 0c9d26dd01..a809a856b9 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 * Univ.Level.Qualid.t) list
+type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list
let check_exists sp =
if Nametab.exists_universe sp then
@@ -540,11 +540,7 @@ let do_universe poly l =
user_err ~hdr:"Constraint"
(str"Cannot declare polymorphic universes outside sections")
in
- let l =
- List.map (fun {CAst.v=id} ->
- let lev = UnivGen.new_univ_id () in
- (id, Univ.Level.Qualid.make (Global.current_dirpath ()) lev)) l
- in
+ let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in
let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx)
Univ.LSet.empty l, Univ.Constraint.empty
in
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 8efda16d64..68d44f8782 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -218,7 +218,9 @@ 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) (fun i -> Level.make2 DirPath.empty (Level.Id.make i)) in
+ let new_levels = Array.init (UContext.size uctx)
+ (fun i -> Level.make (Level.UGlobal.make DirPath.empty 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 30d96a22e0..05c5c0e821 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -593,10 +593,10 @@ let rec ienv_decompose_prod (env,_ as ienv) n c =
ienv_decompose_prod ienv' (n-1) b
| _ -> assert false
+let dummy_univ = Level.(make (UGlobal.make (DirPath.make [Id.of_string "implicit"]) 0))
+let dummy_implicit_sort = mkType (Universe.make dummy_univ)
let lambda_implicit_lift n a =
- 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
+ let lambda_implicit a = mkLambda (Anonymous, dummy_implicit_sort, a) in
iterate lambda_implicit n (lift n a)
(* This removes global parameters of the inductive types in lc (for
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 064fffe98e..5fc8d0297f 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.make2 mp (Level.Id.make (n-2)))
+ | n -> Level.make (Level.UGlobal.make mp (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 57a5dce8a4..7b5ed05bda 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -37,19 +37,10 @@ module RawLevel =
struct
open Names
- module Id = struct
- type t = int
+ module UGlobal = struct
+ type t = DirPath.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 make dp i = (DirPath.hcons dp,i)
let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i'
@@ -64,7 +55,7 @@ struct
type t =
| Prop
| Set
- | Level of Qualid.t
+ | Level of UGlobal.t
| Var of int
(* Hash-consing *)
@@ -74,8 +65,7 @@ struct
match x, y with
| Prop, Prop -> true
| Set, Set -> true
- | Level (d,n), Level (d',n') ->
- Int.equal n n' && DirPath.equal d d'
+ | Level l, Level l' -> UGlobal.equal l l'
| Var n, Var n' -> Int.equal n n'
| _ -> false
@@ -125,14 +115,12 @@ end
module Level = struct
- module Id = RawLevel.Id
-
- module Qualid = RawLevel.Qualid
+ module UGlobal = RawLevel.UGlobal
type raw_level = RawLevel.t =
| Prop
| Set
- | Level of Qualid.t
+ | Level of UGlobal.t
| Var of int
(** Embed levels with their hash value *)
@@ -212,7 +200,6 @@ module Level = struct
match data u with
| Var n -> Some n | _ -> None
- let make2 m n = make (Level (Names.DirPath.hcons m, n))
let make qid = make (Level qid)
let name u =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 69aecac4f3..512f38cedd 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -12,20 +12,10 @@
module Level :
sig
- module Id : sig
+ module UGlobal : 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 make : Names.DirPath.t -> int -> t
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int
@@ -57,11 +47,7 @@ sig
val hash : t -> int
- 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. *)
+ val make : UGlobal.t -> t
val pr : t -> Pp.t
(** Pretty-printing *)
@@ -73,7 +59,7 @@ sig
val var_index : t -> int option
- val name : t -> Qualid.t option
+ val name : t -> UGlobal.t option
end
(** Sets of universe levels *)
diff --git a/library/nametab.ml b/library/nametab.ml
index ab69da3467..f0f643d9b5 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -349,8 +349,8 @@ let the_dirtab = Summary.ref ~name:"dirtab" (DirTab.empty : dirtab)
module UnivIdEqual =
struct
- type t = Univ.Level.Qualid.t
- let equal = Univ.Level.Qualid.equal
+ type t = Univ.Level.UGlobal.t
+ let equal = Univ.Level.UGlobal.equal
end
module UnivTab = Make(FullPath)(UnivIdEqual)
type univtab = UnivTab.t
@@ -373,9 +373,9 @@ let the_modtyperevtab = Summary.ref ~name:"modtyperevtab" (MPmap.empty : mptrevt
module UnivIdOrdered =
struct
- type t = Univ.Level.Qualid.t
- let hash = Univ.Level.Qualid.hash
- let compare = Univ.Level.Qualid.compare
+ type t = Univ.Level.UGlobal.t
+ let hash = Univ.Level.UGlobal.hash
+ let compare = Univ.Level.UGlobal.compare
end
module UnivIdMap = HMap.Make(UnivIdOrdered)
diff --git a/library/nametab.mli b/library/nametab.mli
index 496c76d9b0..b7926cf515 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -120,9 +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
-module UnivIdMap : CMap.ExtS with type key = Univ.Level.Qualid.t
+module UnivIdMap : CMap.ExtS with type key = Univ.Level.UGlobal.t
-val push_universe : visibility -> full_path -> Univ.Level.Qualid.t -> unit
+val push_universe : visibility -> full_path -> Univ.Level.UGlobal.t -> unit
(** {6 The following functions perform globalization of qualified names } *)
@@ -137,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 -> Univ.Level.Qualid.t
+val locate_universe : qualid -> Univ.Level.UGlobal.t
(** These functions globalize user-level references into global
references, like [locate] and co, but raise a nice error message
@@ -194,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 : Univ.Level.Qualid.t -> full_path
+val path_of_universe : Univ.Level.UGlobal.t -> full_path
(** Returns in particular the dirpath or the basename of the full path
associated to global reference *)
@@ -216,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 -> Univ.Level.Qualid.t -> qualid
+val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.UGlobal.t -> qualid
(** Deprecated synonyms *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 33ced6d6e0..ce7c7c8702 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -589,8 +589,23 @@ let detype_cofix detype avoid env sigma n (names,tys,bodies) =
Array.map (fun (_,_,ty) -> ty) v,
Array.map (fun (_,bd,_) -> bd) v)
+(* TODO use some algebraic type with a case for unnamed univs so we
+ can cleanly detype them. NB: this corresponds to a hack in
+ Pretyping.interp_universe_level_name to convert Foo.xx strings into
+ universes. *)
+let hack_qualid_of_univ_level sigma l =
+ match Termops.reference_of_level sigma l with
+ | Some qid -> qid
+ | None ->
+ let path = String.split_on_char '.' (Univ.Level.to_string l) in
+ let path = List.rev_map Id.of_string_soft path in
+ Libnames.qualid_of_dirpath (DirPath.make path)
+
let detype_universe sigma u =
- let fn (l, n) = Some (Termops.reference_of_level sigma l, n) in
+ let fn (l, n) =
+ let qid = hack_qualid_of_univ_level sigma l in
+ Some (qid, n)
+ in
Univ.Universe.map fn u
let detype_sort sigma = function
@@ -611,7 +626,7 @@ let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index
let set_detype_anonymous f = detype_anonymous := f
let detype_level sigma l =
- let l = Termops.reference_of_level sigma l in
+ let l = hack_qualid_of_univ_level sigma l in
GType (UNamed l)
let detype_instance sigma l =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d01c44811f..2be0f73ea4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -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.make2 dp (Univ.Level.Id.make num) in
+ let level = Univ.Level.(make (UGlobal.make dp 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 b834fb71e4..51166cf238 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 Univ.Level.Id.t list
+ | MoreDataUnivLevel of UnivGen.univ_unique_id list
let slave_respond (Request r) =
let res = T.perform r in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:29:43 +0000