From fd1f420aef96822bed2ce14214c34e41ceda9b4e Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Sat, 1 Apr 2017 17:35:39 +0200
Subject: 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.
---
 kernel/vconv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/vconv.ml')

diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 74d956bef0..fa16622702 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' ->
-- 
cgit v1.2.3


From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 1 Jun 2017 16:18:19 +0200
Subject: Clean up universes of constants and inductives

---
 kernel/vconv.ml | 50 +++++++++++++++++++++++++++-----------------------
 1 file changed, 27 insertions(+), 23 deletions(-)

(limited to 'kernel/vconv.ml')

diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index fa16622702..0e452621c8 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -88,30 +88,34 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
 (*  Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *)
   match a1, a2 with
   | Aind ((mi,i) as ind1) , Aind ind2 ->
-      if eq_ind ind1 ind2 && compare_stack stk1 stk2
-      then
-        if Environ.polymorphic_ind ind1 env
-        then
-          let mib = Environ.lookup_mind mi env 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' ->
-	     assert (ulen <= nargs args1);
-             assert (ulen <= nargs args2);
-	     let u1 = Array.init ulen (fun i -> uni_lvl_val (arg args1 i)) in
-	     let u2 = Array.init ulen (fun i -> uni_lvl_val (arg args2 i)) in
-	     let u1 = Univ.Instance.of_array u1 in
-	     let u2 = Univ.Instance.of_array u2 in
-	     let cu = convert_instances ~flex:false u1 u2 cu in
-             conv_arguments env ~from:ulen k args1 args2
-			    (conv_stack env k stk1' stk2' cu)
-	  | _, _ -> assert false (* Should not happen if problem is well typed *)
-        else
-	  conv_stack env k stk1 stk2 cu
-      else raise NotConvertible
+    if eq_ind ind1 ind2 && compare_stack stk1 stk2 then
+      if Environ.polymorphic_ind ind1 env then
+        let mib = Environ.lookup_mind mi env in
+	let ulen = 
+          match mib.Declarations.mind_universes with
+          | Declarations.Monomorphic_ind ctx -> Univ.UContext.size ctx
+          | Declarations.Polymorphic_ind auctx -> Univ.AUContext.size auctx
+          | Declarations.Cumulative_ind cumi -> 
+            Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
+        in
+        match stk1 , stk2 with
+	| [], [] -> assert (Int.equal ulen 0); cu
+        | Zapp args1 :: stk1' , Zapp args2 :: stk2' ->
+          assert (ulen <= nargs args1);
+          assert (ulen <= nargs args2);
+          let u1 = Array.init ulen (fun i -> uni_lvl_val (arg args1 i)) in
+          let u2 = Array.init ulen (fun i -> uni_lvl_val (arg args2 i)) in
+          let u1 = Univ.Instance.of_array u1 in
+          let u2 = Univ.Instance.of_array u2 in
+          let cu = convert_instances ~flex:false u1 u2 cu in
+          conv_arguments env ~from:ulen k args1 args2
+	    (conv_stack env k stk1' stk2' cu)
+        | _, _ -> assert false (* Should not happen if problem is well typed *)
+      else
+	conv_stack env k stk1 stk2 cu
+    else raise NotConvertible
   | Aid ik1, Aid ik2 ->
-      if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
+    if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
 	conv_stack env k stk1 stk2 cu
       else raise NotConvertible
   | Atype _ , _ | _, Atype _ -> assert false
-- 
cgit v1.2.3