aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli2
-rw-r--r--engine/evd.ml2
-rw-r--r--engine/evd.mli14
-rw-r--r--engine/uState.ml33
-rw-r--r--engine/uState.mli6
-rw-r--r--engine/universes.ml8
-rw-r--r--engine/universes.mli4
-rw-r--r--interp/declare.ml8
-rw-r--r--pretyping/pretyping.ml25
-rw-r--r--pretyping/univdecls.ml2
-rw-r--r--vernac/classes.ml4
-rw-r--r--vernac/command.ml2
-rw-r--r--vernac/obligations.ml4
-rw-r--r--vernac/record.ml2
14 files changed, 60 insertions, 56 deletions
diff --git a/API/API.mli b/API/API.mli
index d912dc771..63c675221 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2869,7 +2869,7 @@ sig
val clear_metas : evar_map -> evar_map
(** Allocates a new evar that represents a {i sort}. *)
- val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Sorts.t
+ val new_sort_variable : ?loc:Loc.t -> ?name:Names.Id.t -> rigid -> evar_map -> evar_map * Sorts.t
val remove : evar_map -> Evar.t -> evar_map
val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> Environ.env ->
diff --git a/engine/evd.ml b/engine/evd.ml
index 60bd6de2a..ca1196b94 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -802,7 +802,7 @@ let make_evar_universe_context e l =
| Some us ->
List.fold_left
(fun uctx (loc,id) ->
- fst (UState.new_univ_variable ?loc univ_rigid (Some (Id.to_string id)) uctx))
+ fst (UState.new_univ_variable ?loc univ_rigid (Some id) uctx))
uctx us
(****************************************)
diff --git a/engine/evd.mli b/engine/evd.mli
index 853a34bc4..36c399e98 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -502,12 +502,12 @@ val constrain_variables : Univ.LSet.t -> UState.t -> UState.t
val evar_universe_context_of_binders :
Universes.universe_binders -> UState.t
-
+
val make_evar_universe_context : env -> (Id.t located) list option -> UState.t
-val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
+val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
(** Raises Not_found if not a name for a universe in this map. *)
-val universe_of_name : evar_map -> string -> Univ.Level.t
-val add_universe_name : evar_map -> string -> Univ.Level.t -> evar_map
+val universe_of_name : evar_map -> Id.t -> Univ.Level.t
+val add_universe_name : evar_map -> Id.t -> Univ.Level.t -> evar_map
val add_constraints_context : UState.t ->
Univ.constraints -> UState.t
@@ -519,9 +519,9 @@ val normalize_evar_universe_context_variables : UState.t ->
val normalize_evar_universe_context : UState.t ->
UState.t
-val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.Level.t
-val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.Universe.t
-val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Sorts.t
+val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t
+val new_univ_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t
+val new_sort_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Sorts.t
val add_global_univ : evar_map -> Univ.Level.t -> evar_map
diff --git a/engine/uState.ml b/engine/uState.ml
index 123b64314..498d73fd3 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -11,16 +11,16 @@ open CErrors
open Util
open Names
-module UNameMap = String.Map
+module UNameMap = Names.Id.Map
type uinfo = {
- uname : string option;
+ uname : Id.t option;
uloc : Loc.t option;
}
(* 2nd part used to check consistency on the fly. *)
type t =
- { uctx_names : Univ.Level.t UNameMap.t * uinfo Univ.LMap.t;
+ { uctx_names : Universes.universe_binders * uinfo Univ.LMap.t;
uctx_local : Univ.ContextSet.t; (** The local context of variables *)
uctx_univ_variables : Universes.universe_opt_subst;
(** The local universes that are unification variables *)
@@ -107,10 +107,12 @@ let add_uctx_loc l loc (names, names_rev) =
let of_binders b =
let ctx = empty in
- let names =
- List.fold_left (fun acc (id, l) -> add_uctx_names (Id.to_string id) l acc)
- ctx.uctx_names b
- in { ctx with uctx_names = names }
+ let rmap =
+ UNameMap.fold (fun id l rmap ->
+ Univ.LMap.add l { uname = Some id; uloc = None } rmap)
+ b Univ.LMap.empty
+ in
+ { ctx with uctx_names = b, rmap }
let instantiate_variable l b v =
try v := Univ.LMap.update l (Some b) !v
@@ -249,20 +251,20 @@ let constrain_variables diff ctx =
let pr_uctx_level uctx =
let map, map_rev = uctx.uctx_names in
fun l ->
- try str (Option.get (Univ.LMap.find l map_rev).uname)
+ try Id.print (Option.get (Univ.LMap.find l map_rev).uname)
with Not_found | Option.IsNone ->
Universes.pr_with_global_universes l
type universe_decl =
(Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
-let universe_context ~names ~extensible ctx =
- let levels = Univ.ContextSet.levels ctx.uctx_local in
+let universe_context ~names ~extensible uctx =
+ let levels = Univ.ContextSet.levels uctx.uctx_local in
let newinst, left =
List.fold_right
(fun (loc,id) (newinst, acc) ->
let l =
- try UNameMap.find (Id.to_string id) (fst ctx.uctx_names)
+ try UNameMap.find id (fst uctx.uctx_names)
with Not_found ->
user_err ?loc ~hdr:"universe_context"
(str"Universe " ++ Id.print id ++ str" is not bound anymore.")
@@ -274,23 +276,22 @@ let universe_context ~names ~extensible ctx =
let loc =
try
let info =
- Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in
+ Univ.LMap.find (Univ.LSet.choose left) (snd uctx.uctx_names) in
info.uloc
with Not_found -> None
in
user_err ?loc ~hdr:"universe_context"
((str(CString.plural n "Universe") ++ spc () ++
- Univ.LSet.pr (pr_uctx_level ctx) left ++
+ Univ.LSet.pr (pr_uctx_level uctx) left ++
spc () ++ str (CString.conjugate_verb_to_be n) ++
str" unbound."))
else
let left = Univ.ContextSet.sort_levels (Array.of_list (Univ.LSet.elements left)) in
let inst = Array.append (Array.of_list newinst) left in
let inst = Univ.Instance.of_array inst in
- let map = List.map (fun (s,l) -> Id.of_string s, l) (UNameMap.bindings (fst ctx.uctx_names)) in
let ctx = Univ.UContext.make (inst,
- Univ.ContextSet.constraints ctx.uctx_local) in
- map, ctx
+ Univ.ContextSet.constraints uctx.uctx_local) in
+ fst uctx.uctx_names, ctx
let check_implication uctx cstrs ctx =
let gr = initial_graph uctx in
diff --git a/engine/uState.mli b/engine/uState.mli
index f54bcc832..7f2357a68 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -71,10 +71,10 @@ val add_universe_constraints : t -> Universes.universe_constraints -> t
(** {5 Names} *)
-val add_universe_name : t -> string -> Univ.Level.t -> t
+val add_universe_name : t -> Id.t -> Univ.Level.t -> t
(** Associate a human-readable name to a local variable. *)
-val universe_of_name : t -> string -> Univ.Level.t
+val universe_of_name : t -> Id.t -> Univ.Level.t
(** Retrieve the universe associated to the name. *)
(** {5 Unification} *)
@@ -93,7 +93,7 @@ val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.ContextSet.t -> t
val merge_subst : t -> Universes.universe_opt_subst -> t
val emit_side_effects : Safe_typing.private_constants -> t -> t
-val new_univ_variable : ?loc:Loc.t -> rigid -> string option -> t -> t * Univ.Level.t
+val new_univ_variable : ?loc:Loc.t -> rigid -> Id.t option -> t -> t * Univ.Level.t
val add_global_univ : t -> Univ.Level.t -> t
(** [make_flexible_variable g algebraic l]
diff --git a/engine/universes.ml b/engine/universes.ml
index 6c1b64d74..459c53002 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -21,14 +21,16 @@ let pr_with_global_universes l =
(** Local universe names of polymorphic references *)
-type universe_binders = (Id.t * Univ.Level.t) list
+type universe_binders = Univ.Level.t Names.Id.Map.t
+
+let empty_binders = Id.Map.empty
let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders"
-let universe_binders_of_global ref =
+let universe_binders_of_global ref : universe_binders =
try
let l = Refmap.find ref !universe_binders_table in l
- with Not_found -> []
+ with Not_found -> Names.Id.Map.empty
let register_universe_binders ref l =
universe_binders_table := Refmap.add ref l !universe_binders_table
diff --git a/engine/universes.mli b/engine/universes.mli
index a960099ed..621ca5e84 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -21,7 +21,9 @@ val pr_with_global_universes : Level.t -> Pp.t
(** Local universe name <-> level mapping *)
-type universe_binders = (Id.t * Univ.Level.t) list
+type universe_binders = Univ.Level.t Names.Id.Map.t
+
+val empty_binders : universe_binders
val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
val universe_binders_of_global : Globnames.global_reference -> universe_binders
diff --git a/interp/declare.ml b/interp/declare.ml
index 7ab13b859..dc77981f2 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -462,11 +462,11 @@ type universe_decl = polymorphic * Universes.universe_binders
let cache_universes (p, l) =
let glob = Global.global_universe_names () in
let glob', ctx =
- List.fold_left (fun ((idl,lid),ctx) (id, lev) ->
+ Id.Map.fold (fun id lev ((idl,lid),ctx) ->
((Id.Map.add id (p, lev) idl,
Univ.LMap.add lev id lid),
Univ.ContextSet.add_universe lev ctx))
- (glob, Univ.ContextSet.empty) l
+ l (glob, Univ.ContextSet.empty)
in
cache_universe_context (p, ctx);
Global.set_global_universe_names glob'
@@ -487,9 +487,9 @@ let do_universe poly l =
(str"Cannot declare polymorphic universes outside sections")
in
let l =
- List.map (fun (l, id) ->
+ List.fold_left (fun acc (l, id) ->
let lev = Universes.new_univ_level (Global.current_dirpath ()) in
- (id, lev)) l
+ Id.Map.add id lev acc) Id.Map.empty l
in
Lib.add_anonymous_leaf (input_universes (poly, l))
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e3470b0f1..ffbc21a5e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -181,9 +181,8 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) =
match s with
| Anonymous ->
new_univ_level_variable ?loc anon_rigidity evd
- | Name s ->
- let s = Id.to_string s in
- let names, _ = Global.global_universe_names () in
+ | Name id ->
+ let s = Id.to_string id in
if CString.string_contains ~where:s ~what:"." then
match List.rev (CString.split '.' s) with
| [] -> anomaly (str"Invalid universe name " ++ str s ++ str".")
@@ -197,17 +196,17 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) =
in evd, level
else
try
- let level = Evd.universe_of_name evd s in
- evd, level
+ let level = Evd.universe_of_name evd id in
+ evd, level
with Not_found ->
- try
- let id = try Id.of_string s with _ -> raise Not_found in
- evd, snd (Id.Map.find id names)
- with Not_found ->
- if not (is_strict_universe_declarations ()) then
- new_univ_level_variable ?loc ~name:s univ_rigid evd
- else user_err ?loc ~hdr:"interp_universe_level_name"
- (Pp.(str "Undeclared universe: " ++ str s))
+ try
+ let names, _ = Global.global_universe_names () in
+ evd, snd (Id.Map.find id names)
+ with Not_found ->
+ if not (is_strict_universe_declarations ()) then
+ new_univ_level_variable ?loc ~name:id univ_rigid evd
+ else user_err ?loc ~hdr:"interp_universe_level_name"
+ (Pp.(str "Undeclared universe: " ++ str s))
let interp_universe ?loc evd = function
| [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in
diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml
index 5576e33f4..a5266125a 100644
--- a/pretyping/univdecls.ml
+++ b/pretyping/univdecls.ml
@@ -31,7 +31,7 @@ let interp_univ_constraints env evd cstrs =
user_err ~hdr:"interp_constraint"
(str "Cannot declare constraints on anonymous universes")
| GType (Some (loc, Name id)) ->
- try loc, Evd.universe_of_name evd (Id.to_string id)
+ try loc, Evd.universe_of_name evd id
with Not_found ->
user_err ?loc ~hdr:"interp_constraint" (str "Undeclared universe " ++ Id.print id)
in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 20cb43b24..ed37bab6d 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -411,14 +411,14 @@ let context poly l =
let decl = (Discharge, poly, Definitional) in
let nstatus = match b with
| None ->
- pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl
+ pi3 (Command.declare_assumption false decl (t, !uctx) Universes.empty_binders [] impl
Vernacexpr.NoInline (Loc.tag id))
| Some b ->
let ctx = Univ.ContextSet.to_context !uctx in
let decl = (Discharge, poly, Definition) in
let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in
let hook = Lemmas.mk_hook (fun _ gr -> gr) in
- let _ = DeclareDef.declare_definition id decl entry [] [] hook in
+ let _ = DeclareDef.declare_definition id decl entry Universes.empty_binders [] hook in
Lib.sections_are_opened () || Lib.is_modtype_strict ()
in
status && nstatus
diff --git a/vernac/command.ml b/vernac/command.ml
index 257c003b5..5d83de070 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -258,7 +258,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
let l = List.map (on_pi2 nf_evar) l in
pi2 (List.fold_left (fun (subst,status,ctx) ((is_coe,idl),t,imps) ->
let t = replace_vars subst t in
- let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in
+ let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) Universes.empty_binders imps false nl in
let subst' = List.map2
(fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u)))
idl refs
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index a44de66e9..590332d08 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -484,7 +484,7 @@ let declare_definition prg =
let () = progmap_remove prg in
let cst =
DeclareDef.declare_definition prg.prg_name
- prg.prg_kind ce [] prg.prg_implicits
+ prg.prg_kind ce Universes.empty_binders prg.prg_implicits
(Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r))
in
Universes.register_universe_binders cst pl;
@@ -554,7 +554,7 @@ let declare_mutual_definition l =
(* Declare the recursive definitions *)
let ctx = Evd.evar_context_universe_context first.prg_ctx in
let fix_exn = Hook.get get_fix_exn () in
- let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) [] ctx)
+ let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders ctx)
fixnames fixdecls fixtypes fiximps in
(* Declare notations *)
List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
diff --git a/vernac/record.ml b/vernac/record.ml
index f09b57048..6ffbd1584 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -426,7 +426,7 @@ let declare_structure finite univs id idbuild paramimpls params arity template
else
mie
in
- let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in
+ let kn = Command.declare_mutual_inductive_with_eliminations mie Universes.empty_binders [(paramimpls,[])] in
let rsp = (kn,0) in (* This is ind path of idstruc *)
let cstr = (rsp,1) in
let fields =
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 16:40:03 +0000