Adds support for the virtual machine to perform reduction of universe polymorphic definitions.

- This implementation passes universes in separate arguments and does not
  eagerly instanitate polymorphic definitions.
- This means that it pays no cost on monomorphic definitions.

1 files changed, 42 insertions, 8 deletions

diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 2f6be0601..e0d968848 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -45,8 +45,15 @@ let rec conv_val env pb k v1 v2 cu =
   else conv_whd env pb k (whd_val v1) (whd_val v2) cu
 
 and conv_whd env pb k whd1 whd2 cu =
+(*  Pp.(msg_debug (str "conv_whd(" ++ pr_whd whd1 ++ str ", " ++ pr_whd whd2 ++ str ")")) ; *)
   match whd1, whd2 with
   | Vsort s1, Vsort s2 -> sort_cmp_universes env pb s1 s2 cu
+  | Vuniv_level _ , _
+  | _ , Vuniv_level _ ->
+    (** Both of these are invalid since universes are handled via
+     ** special cases in the code.
+     **)
+    assert false
   | Vprod p1, Vprod p2 ->
       let cu = conv_val env CONV k (dom p1) (dom p2) cu in
       conv_fun env pb k (codom p1) (codom p2) cu
@@ -81,26 +88,53 @@ and conv_whd env pb k whd1 whd2 cu =
 
 
 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 ind1, Aind ind2 ->
-      if eq_puniverses eq_ind ind1 ind2 && compare_stack stk1 stk2
+  | Aind ((mi,i) as ind1) , Aind ind2 ->
+      if eq_ind ind1 ind2 && compare_stack stk1 stk2
       then
-	conv_stack env k stk1 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
+          match stk1 , stk2 with
+	  | Zapp args1 :: stk1' , Zapp args2 :: stk2' ->
+	    assert (ulen <= nargs args1) ;
+            assert (ulen <= nargs args2) ;
+            for i = 0 to ulen - 1 do
+              let a1 = uni_lvl_val (arg args1 i) in
+              let a2 = uni_lvl_val (arg args2 i) in
+              let result = Univ.Level.equal a1 a2 in
+              if not result
+              then raise NotConvertible
+            done ;
+            conv_arguments env ~from:ulen k args1 args2
+              (conv_stack env k stk1' stk2' cu)
+	  | _ -> raise NotConvertible
+        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
 	conv_stack env k stk1 stk2 cu
       else raise NotConvertible
+  | Atype u1 , Atype u2 ->
+    let u1 = Vm.instantiate_universe u1 stk1 in
+    let u2 = Vm.instantiate_universe u2 stk2 in
+    sort_cmp_universes env pb (Type u1) (Type u2) cu
+  | Atype _ , Aid _
+  | Atype _ , Aind _
+  | Aid _ , Atype _
   | Aind _, _ | Aid _, _ -> raise NotConvertible
 
-and conv_stack env k stk1 stk2 cu =
+and conv_stack env ?from:(from=0) k stk1 stk2 cu =
   match stk1, stk2 with
   | [], [] -> cu
   | Zapp args1 :: stk1, Zapp args2 :: stk2 ->
-      conv_stack env k stk1 stk2 (conv_arguments env k args1 args2 cu)
+      conv_stack env k stk1 stk2 (conv_arguments env ~from:from k args1 args2 cu)
   | Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 ->
       conv_stack env k stk1 stk2
-	(conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu))
+	(conv_arguments env ~from:from k args1 args2 (conv_fix env k f1 f2 cu))
   | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 ->
       if check_switch sw1 sw2 then
 	let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in
@@ -144,13 +178,13 @@ and conv_cofix env k cf1 cf2 cu =
       conv_vect (conv_val env CONV (k + Array.length tcf1)) bcf1 bcf2 cu
     else raise NotConvertible
 
-and conv_arguments env k args1 args2 cu =
+and conv_arguments env ?from:(from=0) k args1 args2 cu =
   if args1 == args2 then cu
   else
     let n = nargs args1 in
     if Int.equal n (nargs args2) then
       let rcu = ref cu in
-      for i = 0 to n - 1 do
+      for i = from to n - 1 do
 	rcu := conv_val env CONV k (arg args1 i) (arg args2 i) !rcu
       done;
       !rcu