Allow declaring universe constraints at definition level.

Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof.  By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.

Declarations of universe binders and constraints also works for
monomorphic definitions.

5 files changed, 31 insertions, 2 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index cfc9aa6351..06b257a9e5 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -750,6 +750,26 @@ let universe_context_set d = UState.context_set d.universes
 
 let universe_context ?names evd = UState.universe_context ?names evd.universes
 
+open Misctypes
+type universe_decl =
+  (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+
+let check_implication evd cstrs ctx =
+  let uctx = evar_universe_context evd in
+  let gr = UState.initial_graph uctx in
+  let grext = UGraph.merge_constraints cstrs gr in
+  let cstrs' = Univ.UContext.constraints ctx in
+  if UGraph.check_constraints cstrs' grext then ()
+  else CErrors.user_err ~hdr:"check_univ_decl"
+                  (str "Universe constraints are not implied by the ones declared.")
+
+let check_univ_decl evd decl =
+  let pl = if decl.univdecl_extensible_instance then None else Some decl.univdecl_instance in
+  let pl, ctx = universe_context ?names:pl evd in
+  if not decl.univdecl_extensible_constraints then
+    check_implication evd decl.univdecl_constraints ctx;
+  pl, ctx
+
 let restrict_universe_context evd vars =
   { evd with universes = UState.restrict evd.universes vars }
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 3f00a3b0b2..76fa69e313 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -552,6 +552,10 @@ val universe_context : ?names:(Id.t located) list -> evar_map ->
 val universe_subst : evar_map -> Universes.universe_opt_subst
 val universes : evar_map -> UGraph.t
 
+type universe_decl =
+  (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+
+val check_univ_decl : evar_map -> universe_decl -> Universes.universe_binders * Univ.universe_context
 
 val merge_universe_context : evar_map -> evar_universe_context -> evar_map
 val set_universe_context : evar_map -> evar_universe_context -> evar_map
diff --git a/engine/uState.ml b/engine/uState.ml
index 63bd247d56..312502491c 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -97,6 +97,8 @@ let subst ctx = ctx.uctx_univ_variables
 
 let ugraph ctx = ctx.uctx_universes
 
+let initial_graph ctx = ctx.uctx_initial_universes
+
 let algebraics ctx = ctx.uctx_univ_algebraic
 
 let constrain_variables diff ctx =
diff --git a/engine/uState.mli b/engine/uState.mli
index d198fbfbe9..ba03058693 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -44,6 +44,9 @@ val subst : t -> Universes.universe_opt_subst
 val ugraph : t -> UGraph.t
 (** The current graph extended with the local constraints *)
 
+val initial_graph : t -> UGraph.t
+(** The initial graph with just the declarations of new universes. *)
+
 val algebraics : t -> Univ.LSet.t
 (** The subset of unification variables that can be instantiated with algebraic
     universes as they appear in inferred types only. *)
diff --git a/engine/universes.ml b/engine/universes.ml
index 719af43edf..91398d162c 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -14,7 +14,7 @@ open Environ
 open Univ
 open Globnames
 
-let pr_with_global_universes l = 
+let pr_with_global_universes l =
   try Nameops.pr_id (LMap.find l (snd (Global.global_universe_names ())))
   with Not_found -> Level.pr l
 
@@ -31,7 +31,7 @@ let universe_binders_of_global ref =
 
 let register_universe_binders ref l =
   universe_binders_table := Refmap.add ref l !universe_binders_table
-		     
+
 (* To disallow minimization to Set *)
 
 let set_minimization = ref true