Merge PR #688: Binding universe constraints in Definition/Inductive/etc...

5 files changed, 110 insertions, 53 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index cfc9aa635..f1b5419de 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -748,7 +748,10 @@ let evar_universe_context d = d.universes
 
 let universe_context_set d = UState.context_set d.universes
 
-let universe_context ?names evd = UState.universe_context ?names evd.universes
+let universe_context ~names ~extensible evd =
+  UState.universe_context ~names ~extensible evd.universes
+
+let check_univ_decl evd decl = UState.check_univ_decl evd.universes decl
 
 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 3f00a3b0b..abcabe815 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -493,7 +493,7 @@ val empty_evar_universe_context : evar_universe_context
 val union_evar_universe_context : evar_universe_context -> evar_universe_context ->
   evar_universe_context
 val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst
-val constrain_variables : Univ.LSet.t -> evar_universe_context -> Univ.constraints
+val constrain_variables : Univ.LSet.t -> evar_universe_context -> evar_universe_context
 
 
 val evar_universe_context_of_binders :
@@ -547,11 +547,13 @@ val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool
 
 val evar_universe_context : evar_map -> evar_universe_context
 val universe_context_set : evar_map -> Univ.universe_context_set
-val universe_context : ?names:(Id.t located) list -> evar_map ->
+val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map ->
 		       (Id.t * Univ.Level.t) list * Univ.universe_context
 val universe_subst : evar_map -> Universes.universe_opt_subst
 val universes : evar_map -> UGraph.t
 
+val check_univ_decl : evar_map -> UState.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 63bd247d5..13a9bb373 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -97,17 +97,9 @@ let subst ctx = ctx.uctx_univ_variables
 
 let ugraph ctx = ctx.uctx_universes
 
-let algebraics ctx = ctx.uctx_univ_algebraic
+let initial_graph ctx = ctx.uctx_initial_universes
 
-let constrain_variables diff ctx =
-  Univ.LSet.fold
-    (fun l cstrs ->
-      try
-        match Univ.LMap.find l ctx.uctx_univ_variables with
-        | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs
-        | None -> cstrs
-      with Not_found | Option.IsNone -> cstrs)
-    diff Univ.Constraint.empty
+let algebraics ctx = ctx.uctx_univ_algebraic
 
 let add_uctx_names ?loc s l (names, names_rev) =
   (UNameMap.add s l names, Univ.LMap.add l { uname = Some s; uloc = loc } names_rev)
@@ -240,6 +232,24 @@ let add_universe_constraints ctx cstrs =
       uctx_univ_variables = vars;
       uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
 
+let constrain_variables diff ctx =
+  let univs, local = ctx.uctx_local in
+  let univs, vars, local =
+    Univ.LSet.fold
+      (fun l (univs, vars, cstrs) ->
+        try
+          match Univ.LMap.find l vars with
+          | Some u ->
+             (Univ.LSet.add l univs,
+              Univ.LMap.remove l vars,
+              Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs)
+          | None -> (univs, vars, cstrs)
+        with Not_found | Option.IsNone -> (univs, vars, cstrs))
+      diff (univs, ctx.uctx_univ_variables, local)
+  in
+  { ctx with uctx_local = (univs, local); uctx_univ_variables = vars }
+  
+
 let pr_uctx_level uctx = 
   let map, map_rev = uctx.uctx_names in 
     fun l ->
@@ -247,41 +257,63 @@ let pr_uctx_level uctx =
       with Not_found | Option.IsNone ->
         Universes.pr_with_global_universes l
 
-let universe_context ?names ctx =
-  match names with
-  | None -> [], Univ.ContextSet.to_context ctx.uctx_local
-  | Some pl ->
-     let levels = Univ.ContextSet.levels ctx.uctx_local in
-     let newinst, map, left =
-       List.fold_right
-         (fun (loc,id) (newinst, map, acc) ->
-          let l =
-            try UNameMap.find (Id.to_string id) (fst ctx.uctx_names)
-            with Not_found ->
-              user_err ?loc ~hdr:"universe_context"
-                            (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.")
-          in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc))
-         pl ([], [], levels)
-     in
-       if not (Univ.LSet.is_empty left) then
-         let n = Univ.LSet.cardinal left in
-         let loc =
-           try
-             let info =
-               Univ.LMap.find (Univ.LSet.choose left) (snd ctx.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 ++
-			   spc () ++ str (CString.conjugate_verb_to_be n) ++
-                           str" unbound."))
-      else
-        let inst = Univ.Instance.of_array (Array.of_list newinst) in
-        let ctx = Univ.UContext.make (inst,
-          Univ.ContextSet.constraints ctx.uctx_local)
-        in map, ctx
+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 newinst, left =
+    List.fold_right
+      (fun (loc,id) (newinst, acc) ->
+         let l =
+           try UNameMap.find (Id.to_string id) (fst ctx.uctx_names)
+           with Not_found ->
+             user_err ?loc ~hdr:"universe_context"
+               (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.")
+         in (l :: newinst, Univ.LSet.remove l acc))
+      names ([], levels)
+  in
+  if not extensible && not (Univ.LSet.is_empty left) then
+    let n = Univ.LSet.cardinal left in
+    let loc =
+      try
+        let info =
+          Univ.LMap.find (Univ.LSet.choose left) (snd ctx.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 ++
+	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
+
+let check_implication uctx cstrs ctx =
+  let gr = 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 uctx decl =
+  let open Misctypes in
+  let pl, ctx = universe_context
+      ~names:decl.univdecl_instance
+      ~extensible:decl.univdecl_extensible_instance
+      uctx
+  in
+  if not decl.univdecl_extensible_constraints then
+    check_implication uctx decl.univdecl_constraints ctx;
+  pl, ctx
 
 let restrict ctx vars =
   let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in
diff --git a/engine/uState.mli b/engine/uState.mli
index d198fbfbe..c44f2c1d7 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. *)
@@ -105,7 +108,7 @@ val is_sort_variable : t -> Sorts.t -> Univ.Level.t option
 
 val normalize_variables : t -> Univ.universe_subst * t
 
-val constrain_variables : Univ.LSet.t -> t -> Univ.constraints
+val constrain_variables : Univ.LSet.t -> t -> t
 
 val abstract_undefined_variables : t -> t
 
@@ -115,9 +118,26 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
 
 val normalize : t -> t
 
-(** {5 TODO: Document me} *)
+(** [universe_context names extensible ctx]
+
+    Return a universe context containing the local universes of [ctx]
+    and their constraints. The universes corresponding to [names] come
+    first in the order defined by that list.
+
+    If [extensible] is false, check that the universes of [names] are
+    the only local universes.
 
-val universe_context : ?names:(Id.t Loc.located) list -> t -> (Id.t * Univ.Level.t) list * Univ.universe_context
+    Also return the association list of universe names and universes
+    (including those not in [names]). *)
+val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t ->
+  (Id.t * Univ.Level.t) list * Univ.universe_context
+
+type universe_decl =
+  (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+
+val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.universe_context
+
+(** {5 TODO: Document me} *)
 
 val update_sigma_env : t -> Environ.env -> t
 
diff --git a/engine/universes.ml b/engine/universes.ml
index 686411e7d..7f5bf24b7 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