aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/vernacexpr.mli2
-rw-r--r--kernel/univ.ml11
-rw-r--r--kernel/univ.mli2
-rw-r--r--library/declare.ml50
-rw-r--r--library/declare.mli7
-rw-r--r--library/global.ml1
-rw-r--r--library/global.mli4
-rw-r--r--library/universes.ml10
-rw-r--r--library/universes.mli7
-rw-r--r--parsing/g_vernac.ml46
-rw-r--r--pretyping/detyping.ml7
-rw-r--r--pretyping/pretyping.ml13
-rw-r--r--printing/ppvernac.ml10
-rw-r--r--stm/vernac_classifier.ml1
-rw-r--r--toplevel/command.ml3
-rw-r--r--toplevel/command.mli3
-rw-r--r--toplevel/vernacentries.ml5
17 files changed, 132 insertions, 10 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index af65f6541..5aa9d51fc 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -303,6 +303,8 @@ type vernac_expr =
locality option * (cofixpoint_expr * decl_notation list) list
| VernacScheme of (lident option * scheme) list
| VernacCombinedScheme of lident * lident list
+ | VernacUniverse of lident list
+ | VernacConstraint of (lident * Univ.constraint_type * lident) list
(* Gallina extensions *)
| VernacBeginSection of lident
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 1e7d2c83c..b42de5a76 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -539,6 +539,10 @@ struct
let pr x = str(to_string x)
+ let pr_with f (v, n) =
+ if Int.equal n 0 then f v
+ else f v ++ str"+" ++ int n
+
let is_level = function
| (v, 0) -> true
| _ -> false
@@ -591,6 +595,13 @@ struct
str "max(" ++ hov 0
(prlist_with_sep pr_comma Expr.pr (to_list l)) ++
str ")"
+
+ let pr_with f l = match node l with
+ | Cons (u, n) when is_nil n -> Expr.pr_with f u
+ | _ ->
+ str "max(" ++ hov 0
+ (prlist_with_sep pr_comma (Expr.pr_with f) (to_list l)) ++
+ str ")"
let atom l = match node l with
| Cons (l, n) when is_nil n -> Some l
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 832da157e..8166d75e6 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -79,6 +79,8 @@ sig
val pr : t -> Pp.std_ppcmds
(** Pretty-printing *)
+ val pr_with : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
+
val is_level : t -> bool
(** Test if the universe is a level or an algebraic universe. *)
diff --git a/library/declare.ml b/library/declare.ml
index 7a80d103d..f746282d1 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -430,3 +430,53 @@ let definition_message id =
let assumption_message id =
Flags.if_verbose msg_info (pr_id id ++ str " is assumed")
+
+(** Global universe names, in a different summary *)
+
+type universe_names =
+ (Univ.universe_level Idmap.t * Id.t Univ.LMap.t)
+
+let input_universes : universe_names -> Libobject.obj =
+ let open Libobject in
+ declare_object
+ { (default_object "Global universe name state") with
+ cache_function = (fun (na, pi) -> Universes.set_global_universe_names pi);
+ load_function = (fun _ (_, pi) -> Universes.set_global_universe_names pi);
+ discharge_function = (fun (_, a) -> Some a);
+ classify_function = (fun a -> Keep a) }
+
+let do_universe l =
+ let glob = Universes.global_universe_names () in
+ let glob' =
+ List.fold_left (fun (idl,lid) (l, id) ->
+ let lev = Universes.new_univ_level (Global.current_dirpath ()) in
+ (Idmap.add id lev idl, Univ.LMap.add lev id lid))
+ glob l
+ in
+ Lib.add_anonymous_leaf (input_universes glob')
+
+
+let input_constraints : Univ.constraints -> Libobject.obj =
+ let open Libobject in
+ declare_object
+ { (default_object "Global universe constraints") with
+ cache_function = (fun (na, c) -> Global.add_constraints c);
+ load_function = (fun _ (_, c) -> Global.add_constraints c);
+ discharge_function = (fun (_, a) -> Some a);
+ classify_function = (fun a -> Keep a) }
+
+let do_constraint l =
+ let u_of_id =
+ let names, _ = Universes.global_universe_names () in
+ fun (loc, id) ->
+ try Idmap.find id names
+ with Not_found ->
+ user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)
+ in
+ let constraints = List.fold_left (fun acc (l, d, r) ->
+ let lu = u_of_id l and ru = u_of_id r in
+ Univ.Constraint.add (lu, d, ru) acc)
+ Univ.Constraint.empty l
+ in
+ Lib.add_anonymous_leaf (input_constraints constraints)
+
diff --git a/library/declare.mli b/library/declare.mli
index ed3e4dcc3..a9fd8956e 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -85,3 +85,10 @@ val recursive_message : bool (** true = fixpoint *) ->
int array option -> Id.t list -> unit
val exists_name : Id.t -> bool
+
+
+
+(** Global universe names and constraints *)
+
+val do_universe : Id.t Loc.located list -> unit
+val do_constraint : (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit
diff --git a/library/global.ml b/library/global.ml
index 378e7aaa3..c3c309c39 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -237,3 +237,4 @@ let register_inline c = globalize0 (Safe_typing.register_inline c)
let set_strategy k l =
GlobalSafeEnv.set_safe_env (Safe_typing.set_strategy (safe_env ()) k l)
+
diff --git a/library/global.mli b/library/global.mli
index de19e888c..9e47c16ff 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -28,9 +28,6 @@ val named_context : unit -> Context.named_context
(** Changing the (im)predicativity of the system *)
val set_engagement : Declarations.engagement -> unit
-(** Extra universe constraints *)
-val add_constraints : Univ.constraints -> unit
-
(** Variables, Local definitions, constants, inductive types *)
val push_named_assum : (Id.t * Constr.types) Univ.in_universe_context_set -> unit
@@ -41,6 +38,7 @@ val add_constant :
val add_mind :
DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive
+(** Extra universe constraints *)
val add_constraints : Univ.constraints -> unit
val push_context : Univ.universe_context -> unit
diff --git a/library/universes.ml b/library/universes.ml
index 0699326c5..e84f1f975 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -13,6 +13,16 @@ open Term
open Environ
open Univ
+type universe_names =
+ Univ.universe_level Idmap.t * Id.t Univ.LMap.t
+
+let global_universes = Summary.ref ~name:"Global universe names"
+ ((Idmap.empty, Univ.LMap.empty) : universe_names)
+
+let global_universe_names () = !global_universes
+let set_global_universe_names s = global_universes := s
+
+
type universe_constraint_type = ULe | UEq | ULub
type universe_constraint = universe * universe_constraint_type * universe
diff --git a/library/universes.mli b/library/universes.mli
index 691f404aa..5b0951928 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -17,6 +17,12 @@ open Univ
(** Universes *)
+type universe_names =
+ Univ.universe_level Idmap.t * Id.t Univ.LMap.t
+
+val global_universe_names : unit -> universe_names
+val set_global_universe_names : universe_names -> unit
+
(** The global universe counter *)
val set_remote_new_univ_level : universe_level RemoteCounter.installer
@@ -237,4 +243,3 @@ val minimize_univ_variables :
Univ.LSet.t * Univ.universe option Univ.LMap.t *
Univ.LSet.t *
(bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints
-
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 39c93e316..5f49a318d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -210,6 +210,8 @@ GEXTEND Gram
l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l)
| IDENT "Register"; IDENT "Inline"; id = identref ->
VernacRegister(id, RegisterInline)
+ | IDENT "Universe"; l = LIST1 identref -> VernacUniverse l
+ | IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> VernacConstraint l
] ]
;
@@ -256,6 +258,10 @@ GEXTEND Gram
| IDENT "Inline" -> DefaultInline
| -> NoInline] ]
;
+ univ_constraint:
+ [ [ l = identref; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ];
+ r = identref -> (l, ord, r) ] ]
+ ;
finite_token:
[ [ "Inductive" -> (Inductive_kw,Finite)
| "CoInductive" -> (CoInductive,CoFinite) ] ]
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a7a8bf5be..92a29fce7 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -370,7 +370,12 @@ let detype_sort = function
| Type u ->
GType
(if !print_universes
- then Some (Pp.string_of_ppcmds (Univ.Universe.pr u))
+ then
+ let _, map = Universes.global_universe_names () in
+ let pr_level u =
+ try Nameops.pr_id (Univ.LMap.find u map) with Not_found -> Univ.Level.pr u
+ in
+ Some (Pp.string_of_ppcmds (Univ.Universe.pr_with pr_level u))
else None)
type binder_kind = BProd | BLambda | BLetIn
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c8c1d0e21..9609a959b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -96,10 +96,15 @@ let ((constr_in : constr -> Dyn.t),
let interp_universe_name evd = function
| None -> new_univ_level_variable univ_rigid evd
| Some s ->
- try let level = Evd.universe_of_name evd s in
- evd, level
- with Not_found ->
- new_univ_level_variable ~name:s univ_rigid evd
+ try
+ let id = try Id.of_string s with _ -> raise Not_found in
+ let names, _ = Universes.global_universe_names () in
+ evd, Idmap.find id names
+ with Not_found ->
+ try let level = Evd.universe_of_name evd s in
+ evd, level
+ with Not_found ->
+ new_univ_level_variable ~name:s univ_rigid evd
let interp_sort evd = function
| GProp -> evd, Prop Null
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index d89731147..f088477e7 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -691,7 +691,15 @@ let rec pr_vernac = function
hov 2 (str"Combined Scheme" ++ spc() ++
pr_lident id ++ spc() ++ str"from" ++ spc() ++
prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l)
-
+ | VernacUniverse v ->
+ hov 2 (str"Universe" ++ spc () ++
+ prlist_with_sep (fun _ -> str",") pr_lident v)
+ | VernacConstraint v ->
+ let pr_uconstraint (l, d, r) =
+ pr_lident l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ pr_lident r
+ in
+ hov 2 (str"Constraint" ++ spc () ++
+ prlist_with_sep (fun _ -> str",") pr_uconstraint v)
(* Gallina extensions *)
| VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_lident id)
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 05c8fdd0d..12d3a3787 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -139,6 +139,7 @@ let rec classify_vernac e =
let ids = List.map snd (CList.map_filter (fun (x,_) -> x) l) in
VtSideff ids, VtLater
| VernacCombinedScheme ((_,id),_) -> VtSideff [id], VtLater
+ | VernacUniverse _ | VernacConstraint _
| VernacBeginSection _
| VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _
| VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
diff --git a/toplevel/command.ml b/toplevel/command.ml
index faa4b12df..95ddf1fb0 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -38,6 +38,9 @@ open Indschemes
open Misctypes
open Vernacexpr
+let do_universe l = Declare.do_universe l
+let do_constraint l = Declare.do_constraint l
+
let rec under_binders env f n c =
if Int.equal n 0 then f env Evd.empty c else
match kind_of_term c with
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 4d1c74907..d14af7394 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -21,6 +21,9 @@ open Pfedit
(** This file is about the interpretation of raw commands into typed
ones and top-level declaration of the main Gallina objects *)
+val do_universe : Id.t Loc.located list -> unit
+val do_constraint : (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit
+
(** {6 Hooks for Pcoq} *)
val set_declare_definition_hook : (definition_entry -> unit) -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b1ed564d8..1d05f4e62 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -605,6 +605,9 @@ let vernac_combined_scheme lid l =
List.iter (fun lid -> dump_global (Misctypes.AN (Ident lid))) l);
Indschemes.do_combined_scheme lid l
+let vernac_universe l = do_universe l
+let vernac_constraint l = do_constraint l
+
(**********************)
(* Modules *)
@@ -1721,6 +1724,8 @@ let interp ?proof locality poly c =
| VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l
| VernacScheme l -> vernac_scheme l
| VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
+ | VernacUniverse l -> vernac_universe l
+ | VernacConstraint l -> vernac_constraint l
(* Modules *)
| VernacDeclareModule (export,lid,bl,mtyo) ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 18:19:13 +0000