From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 kernel/vconv.ml | 63 ++++++++++++++++++++++++++++++++-------------------------
 1 file changed, 35 insertions(+), 28 deletions(-)

(limited to 'kernel/vconv.ml')

diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 74d956be..437de99e 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -3,6 +3,7 @@ open Names
 open Environ
 open Reduction
 open Vm
+open Vmvalues
 open Csymtable
 
 let val_of_constr env c =
@@ -43,7 +44,6 @@ let rec conv_val env pb k v1 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
@@ -80,7 +80,7 @@ and conv_whd env pb k whd1 whd2 cu =
      (* on the fly eta expansion *)
       conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu
 
-  | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _  | Vconstr_const _, _
+  | Vprod _, _ | Vfix _, _ | Vcofix _, _  | Vconstr_const _, _
   | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible
 
 
@@ -88,34 +88,39 @@ 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 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.ContextSet.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 Vmvalues.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
 	conv_stack env k stk1 stk2 cu
       else raise NotConvertible
-  | Atype _ , _ | _, Atype _ -> assert false
-  | Aind _, _ | Aid _, _ -> raise NotConvertible
+  | Asort s1, Asort s2 ->
+    sort_cmp_universes env pb s1 s2 cu
+  | Asort _ , _ | Aind _, _ | Aid _, _ -> raise NotConvertible
 
 and conv_stack env k stk1 stk2 cu =
   match stk1, stk2 with
@@ -200,4 +205,6 @@ let vm_conv cv_pb env t1 t2 =
     let univs = (univs, checked_universes) in
     let _ = vm_conv_gen cv_pb env univs t1 t2 in ()
 
-let _ = Reduction.set_vm_conv vm_conv
+let _ = if Coq_config.bytecode_compiler then Reduction.set_vm_conv vm_conv
+let _ = if Coq_config.bytecode_compiler then
+  Nativeconv.set_vm_conv_gen { Nativeconv.vm_conv_gen = vm_conv_gen }
-- 
cgit v1.2.3