Use Entries.constant_universes_entry more.

This reduces conversions between ContextSet/UContext and encodes
whether we are polymorphic by which constructor we use rather than
using some boolean.

1 files changed, 76 insertions, 31 deletions

diff --git a/engine/uState.ml b/engine/uState.ml
index ff91493ee..dadc004c5 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -87,6 +87,17 @@ let constraints ctx = snd ctx.uctx_local
 
 let context ctx = Univ.ContextSet.to_context ctx.uctx_local
 
+let const_univ_entry ~poly uctx =
+  let open Entries in
+  if poly then Polymorphic_const_entry (context uctx)
+  else Monomorphic_const_entry (context_set uctx)
+
+(* does not support cumulativity since you need more info *)
+let ind_univ_entry ~poly uctx =
+  let open Entries in
+  if poly then Polymorphic_ind_entry (context uctx)
+  else Monomorphic_ind_entry (context_set uctx)
+
 let of_context_set ctx = { empty with uctx_local = ctx }
 
 let subst ctx = ctx.uctx_univ_variables
@@ -260,58 +271,92 @@ let pr_uctx_level uctx =
 type universe_decl =
   (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
 
+let error_unbound_universes left uctx =
+  let open Univ in
+  let n = LSet.cardinal left in
+  let loc =
+    try
+      let info =
+        LMap.find (LSet.choose left) (snd uctx.uctx_names) in
+      info.uloc
+    with Not_found -> None
+  in
+  user_err ?loc ~hdr:"universe_context"
+    ((str(CString.plural n "Universe") ++ spc () ++
+      LSet.pr (pr_uctx_level uctx) left ++
+      spc () ++ str (CString.conjugate_verb_to_be n) ++
+      str" unbound."))
+
 let universe_context ~names ~extensible uctx =
-  let levels = Univ.ContextSet.levels uctx.uctx_local in
+  let open Univ in
+  let levels = ContextSet.levels uctx.uctx_local in
   let newinst, left =
     List.fold_right
       (fun (loc,id) (newinst, acc) ->
          let l =
            try UNameMap.find id (fst uctx.uctx_names)
-           with Not_found ->
-             user_err ?loc ~hdr:"universe_context"
-               (str"Universe " ++ Id.print id ++ str" is not bound anymore.")
-         in (l :: newinst, Univ.LSet.remove l acc))
+           with Not_found -> assert false
+         in (l :: newinst, 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 uctx.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 uctx) left ++
-	spc () ++ str (CString.conjugate_verb_to_be n) ++
-        str" unbound."))
+  if not extensible && not (LSet.is_empty left)
+  then error_unbound_universes left uctx
   else
-    let left = Univ.ContextSet.sort_levels (Array.of_list (Univ.LSet.elements left)) in
+    let left = ContextSet.sort_levels (Array.of_list (LSet.elements left)) in
     let inst = Array.append (Array.of_list newinst) left in
-    let inst = Univ.Instance.of_array inst in
-    let ctx = Univ.UContext.make (inst,
-                                  Univ.ContextSet.constraints uctx.uctx_local) in
+    let inst = Instance.of_array inst in
+    let ctx = UContext.make (inst, ContextSet.constraints uctx.uctx_local) in
     ctx
 
-let check_implication uctx cstrs ctx =
+let check_universe_context_set ~names ~extensible uctx =
+  if extensible then ()
+  else
+    let open Univ in
+    let left = List.fold_left (fun left (loc,id) ->
+        let l =
+          try UNameMap.find id (fst uctx.uctx_names)
+          with Not_found -> assert false
+        in LSet.remove l left)
+        (ContextSet.levels uctx.uctx_local) names
+    in
+    if not (LSet.is_empty left)
+    then error_unbound_universes left uctx
+
+let check_implication uctx cstrs cstrs' =
   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 check_mono_univ_decl uctx decl =
+  let open Misctypes in
+  let () =
+    let names = decl.univdecl_instance in
+    let extensible = decl.univdecl_extensible_instance in
+    check_universe_context_set ~names ~extensible uctx
+  in
+  if not decl.univdecl_extensible_constraints then
+    check_implication uctx
+      decl.univdecl_constraints
+      (Univ.ContextSet.constraints uctx.uctx_local);
+  uctx.uctx_local
+
+let check_univ_decl ~poly uctx decl =
   let open Misctypes in
-  let ctx = universe_context
-      ~names:decl.univdecl_instance
-      ~extensible:decl.univdecl_extensible_instance
-      uctx
+  let ctx =
+    let names = decl.univdecl_instance in
+    let extensible = decl.univdecl_extensible_instance in
+    if poly
+    then Entries.Polymorphic_const_entry (universe_context ~names ~extensible uctx)
+    else
+      let () = check_universe_context_set ~names ~extensible uctx in
+      Entries.Monomorphic_const_entry uctx.uctx_local
   in
   if not decl.univdecl_extensible_constraints then
-    check_implication uctx decl.univdecl_constraints ctx;
+    check_implication uctx
+      decl.univdecl_constraints
+      (Univ.ContextSet.constraints uctx.uctx_local);
   ctx
 
 let restrict ctx vars =