Add toplevel commands to declare global universes and constraints.

6 files changed, 75 insertions, 4 deletions

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
-