Using UInfoInd for universes in inductive types

It stores both universe constraints and subtyping information for
blocks of inductive declarations.

At this stage the there is no inference or checking implemented. The
subtyping information simply encodes equality of levels for the condition of
subtyping.

9 files changed, 18 insertions, 25 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 9536407d3..1bb1e885f 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -188,9 +188,7 @@ type mutual_inductive_body = {
 
     mind_polymorphic : bool; (** Is it polymorphic or not *)
 
-    mind_universes : Univ.universe_context; (** Local universe variables and constraints *)
-
-    mind_subtyping : Univ.universe_context; (** Constraints for subtyping *)
+    mind_universes : Univ.universe_info_ind; (** Local universe variables and constraints together with subtyping constraints *)
 
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 47a23c855..cdea468ad 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -261,19 +261,18 @@ let subst_mind_body sub mib =
     mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
     mind_polymorphic = mib.mind_polymorphic;
     mind_universes = mib.mind_universes;
-    mind_subtyping = mib.mind_subtyping;
     mind_private = mib.mind_private;
     mind_typing_flags = mib.mind_typing_flags;
   }
 
 let inductive_instance mib =
   if mib.mind_polymorphic then
-    Univ.UContext.instance mib.mind_universes
+    Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes)
   else Univ.Instance.empty
 
 let inductive_context mib =
   if mib.mind_polymorphic then 
-    Univ.instantiate_univ_context mib.mind_universes 
+    Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes)
   else Univ.UContext.empty
 
 (** {6 Hash-consing of inductive declarations } *)
@@ -306,7 +305,7 @@ let hcons_mind mib =
   { mib with
     mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets;
     mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
-    mind_universes = Univ.hcons_universe_context mib.mind_universes }
+    mind_universes = Univ.hcons_universe_info_ind mib.mind_universes }
 
 (** {6 Stm machinery } *)
 
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 88584e3b3..97c28025a 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -50,7 +50,7 @@ type mutual_inductive_entry = {
   mind_entry_params : (Id.t * local_entry) list;
   mind_entry_inds : one_inductive_entry list;
   mind_entry_polymorphic : bool; 
-  mind_entry_universes : Univ.universe_context * Univ.universe_context;
+  mind_entry_universes : Univ.universe_info_ind;
   (* universe constraints and the constraints for subtyping of
      inductive types in the block. *)
   mind_entry_private : bool option;
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 5d928facc..94bf1a770 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -220,7 +220,7 @@ let typecheck_inductive env mie =
   (* Check unicity of names *)
   mind_check_names mie;
   (* Params are typed-checked here *)
-  let env' = push_context (fst mie.mind_entry_universes) env in
+  let env' = push_context (Univ.UInfoInd.univ_context mie.mind_entry_universes) env in
   let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in
   (* We first type arity of each inductive definition *)
   (* This allows building the environment of arities and to share *)
@@ -822,10 +822,10 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm
   let hyps = used_section_variables env inds in
   let nparamargs = Context.Rel.nhyps paramsctxt in
   let nparamsctxt = Context.Rel.length paramsctxt in
-  let substunivs, ctxunivs = Univ.abstract_universes p (fst ctx) in
-  let substsbt, ctxsbt = Univ.abstract_universes p (snd ctx) in
+  let substunivs, ctxunivs = Univ.abstract_universes p (Univ.UInfoInd.univ_context ctx) in
+  let substsubtyp, ctxsubtyp = Univ.abstract_universes p (Univ.UInfoInd.subtyp_context ctx) in
   let paramsctxt = Vars.subst_univs_level_context substunivs paramsctxt in
-  let env_ar = 
+  let env_ar =
     let ctxunivs = Environ.rel_context env_ar in 
     let ctxunivs' = Vars.subst_univs_level_context substunivs ctxunivs in
       Environ.push_rel_context ctxunivs' env
@@ -842,9 +842,6 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm
     let consnrealargs =
       Array.map (fun (d,_) -> Context.Rel.nhyps d - nparamargs)
 	splayed_lc in
-    (* Check that the subtyping constraints (inferred outside kernel)
-       are valid. If so return (), otherwise raise an anomaly! *)
-    let () = () in
     (* Elimination sorts *)
     let arkind,kelim = 
       match ar_kind with
@@ -924,8 +921,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm
       mind_params_ctxt = paramsctxt;
       mind_packets = packets;
       mind_polymorphic = p;
-      mind_universes = ctxunivs;
-      mind_subtyping = ctxsbt;
+      mind_universes = Univ.UInfoInd.make (ctxunivs, ctxsubtyp);
       mind_private = prv;
       mind_typing_flags = Environ.typing_flags env;
     }
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index f3b03252d..0f0dc0d60 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -55,7 +55,7 @@ let inductive_paramdecls (mib,u) =
 
 let instantiate_inductive_constraints mib u =
   if mib.mind_polymorphic then
-    Univ.subst_instance_constraints u (Univ.UContext.constraints mib.mind_universes)
+    Univ.subst_instance_constraints u (Univ.UContext.constraints (Univ.UInfoInd.univ_context mib.mind_universes))
   else Univ.Constraint.empty
 
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f5e8e8653..1568fe0bf 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -429,7 +429,7 @@ let globalize_mind_universes mb =
   if mb.mind_polymorphic then
     [Now (true, Univ.ContextSet.empty)]
   else
-    [Now (false, Univ.ContextSet.of_context mb.mind_universes)]
+    [Now (false, Univ.ContextSet.of_context (Univ.UInfoInd.univ_context mb.mind_universes))]
 
 let constraints_of_sfb env sfb = 
   match sfb with
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index bdfd00a8d..3cf2299d8 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -313,7 +313,7 @@ let infer_declaration ~trust env kn dcl =
     in
     let term, typ = pb.proj_eta in
       Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb,
-      mib.mind_polymorphic, mib.mind_universes, false, None
+      mib.mind_polymorphic, Univ.UInfoInd.univ_context mib.mind_universes, false, None
 
 let global_vars_set_constant_type env = function
   | RegularArity t -> global_vars_set env t
diff --git a/kernel/univ.ml b/kernel/univ.ml
index e8b9ae33a..f124bb39e 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1053,14 +1053,14 @@ struct
     let len = Array.length (Instance.to_array ctx) in
     let halflen = len / 2 in
     (Instance.of_array (Array.sub (Instance.to_array ctx) 0 halflen),
-     Instance.of_array (Array.sub (Instance.to_array ctx) halflen len))
+     Instance.of_array (Array.sub (Instance.to_array ctx) halflen halflen))
 
   let pr prl (univcst, subtypcst) =
     if UContext.is_empty univcst then mt() else
       let (ctx, ctx') = halve_context (UContext.instance subtypcst) in
-      (UContext.pr prl univcst) ++
-      h 0 (str "~@{" ++ Instance.pr prl ctx ++ str "} <= ~@{" ++ Instance.pr prl ctx' ++ str "}")
-           ++ h 0 (v 0 (Constraint.pr prl (UContext.constraints subtypcst)))
+      (UContext.pr prl univcst) ++ fnl () ++ fnl () ++
+        h 0 (str "~@{" ++ Instance.pr prl ctx ++ str "} <= ~@{" ++ Instance.pr prl ctx' ++ str "} iff ")
+         ++ fnl () ++ h 0 (v 0 (Constraint.pr prl (UContext.constraints subtypcst)))
 
   let hcons (univcst, subtypcst) =
     (UContext.hcons univcst, UContext.hcons subtypcst)
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 74d956bef..fa1662270 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -93,7 +93,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
         if Environ.polymorphic_ind ind1 env
         then
           let mib = Environ.lookup_mind mi env in
-	  let ulen = Univ.UContext.size mib.Declarations.mind_universes in
+	  let ulen = Univ.UContext.size (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in
           match stk1 , stk2 with
 	  | [], [] -> assert (Int.equal ulen 0); cu
 	  | Zapp args1 :: stk1' , Zapp args2 :: stk2' ->