Add toplevel commands to declare global universes and constraints.

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) ->