Imported Upstream version 8.5~beta3+dfsg

1 files changed, 77 insertions, 59 deletions

diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 75a3fc45..0242fd46 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -16,17 +16,21 @@ open Nativecode
 
 (** This module implements the conversion test by compiling to OCaml code *)
 
-let rec conv_val env pb lvl cu v1 v2 = 
-  if v1 == v2 then ()
+let rec conv_val env pb lvl v1 v2 cu =
+  if v1 == v2 then cu
   else
     match kind_of_value v1, kind_of_value v2 with
-    | Vaccu k1, Vaccu k2 ->
-	conv_accu env pb lvl cu k1 k2
     | Vfun f1, Vfun f2 ->
 	let v = mk_rel_accu lvl in
-	conv_val env CONV (lvl+1) cu (f1 v) (f2 v)
+	conv_val env CONV (lvl+1) (f1 v) (f2 v) cu
+    | Vfun f1, _ ->
+	conv_val env CONV lvl v1 (fun x -> v2 x) cu
+    | _, Vfun f2 ->
+	conv_val env CONV lvl (fun x -> v1 x) v2 cu
+    | Vaccu k1, Vaccu k2 ->
+	conv_accu env pb lvl k1 k2 cu
     | Vconst i1, Vconst i2 -> 
-	if not (Int.equal i1 i2) then raise NotConvertible
+	if Int.equal i1 i2 then cu else raise NotConvertible
     | Vblock b1, Vblock b2 ->
 	let n1 = block_size b1 in
         let n2 = block_size b2 in
@@ -34,77 +38,81 @@ let rec conv_val env pb lvl cu v1 v2 =
 	  raise NotConvertible;
 	let rec aux lvl max b1 b2 i cu =
 	  if Int.equal i max then 
-	    conv_val env CONV lvl cu (block_field b1 i) (block_field b2 i)
+	    conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu
 	  else
-	      (conv_val env CONV lvl cu (block_field b1 i) (block_field b2 i);
-	    aux lvl max b1 b2 (i+1) cu)
+	    let cu = conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu in
+	    aux lvl max b1 b2 (i+1) cu
 	in
 	aux lvl (n1-1) b1 b2 0 cu
-    | Vfun f1, _ -> 
-	conv_val env CONV lvl cu v1 (fun x -> v2 x)
-    | _, Vfun f2 ->
-	conv_val env CONV lvl cu (fun x -> v1 x) v2
-    | _, _ -> raise NotConvertible
+    | Vaccu _, _ | Vconst _, _ | Vblock _, _ -> raise NotConvertible
 
-and conv_accu env pb lvl cu k1 k2 = 
+and conv_accu env pb lvl k1 k2 cu =
   let n1 = accu_nargs k1 in
   let n2 = accu_nargs k2 in
   if not (Int.equal n1 n2) then raise NotConvertible;
   if Int.equal n1 0 then 
     conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu
   else
-    (conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu;
-    List.iter2 (conv_val env CONV lvl cu) (args_of_accu k1) (args_of_accu k2))
+    let cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in
+    List.fold_right2 (conv_val env CONV lvl) (args_of_accu k1) (args_of_accu k2) cu
 
 and conv_atom env pb lvl a1 a2 cu =
-  if a1 == a2 then ()
+  if a1 == a2 then cu
   else
     match a1, a2 with
+    | Ameta _, _ | _, Ameta _ | Aevar _, _ | _, Aevar _ -> assert false
     | Arel i1, Arel i2 -> 
-	if not (Int.equal i1 i2) then raise NotConvertible
-    | Aind ind1, Aind ind2 ->
-	if not (eq_puniverses eq_ind ind1 ind2) then raise NotConvertible
-    | Aconstant c1, Aconstant c2 ->
-	if not (eq_puniverses eq_constant c1 c2) then raise NotConvertible
+	if Int.equal i1 i2 then cu else raise NotConvertible
+    | Aind (ind1,u1), Aind (ind2,u2) ->
+       if eq_ind ind1 ind2 then convert_instances ~flex:false u1 u2 cu
+       else raise NotConvertible
+    | Aconstant (c1,u1), Aconstant (c2,u2) ->
+       if Constant.equal c1 c2 then convert_instances ~flex:true u1 u2 cu
+       else raise NotConvertible
     | Asort s1, Asort s2 -> 
-        check_sort_cmp_universes env pb s1 s2 cu
+        sort_cmp_universes env pb s1 s2 cu
     | Avar id1, Avar id2 ->
-	if not (Id.equal id1 id2) then raise NotConvertible
+	if Id.equal id1 id2 then cu else raise NotConvertible
     | Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) ->
 	if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible;
-	conv_accu env CONV lvl cu ac1 ac2;
+	let cu = conv_accu env CONV lvl ac1 ac2 cu in
 	let tbl = a1.asw_reloc in
 	let len = Array.length tbl in
-	if Int.equal len 0 then conv_val env CONV lvl cu p1 p2
+	if Int.equal len 0 then conv_val env CONV lvl p1 p2 cu
 	else begin
-	  conv_val env CONV lvl cu p1 p2;
-	  let max = len - 1 in
-	  let rec aux i =
-	    let tag,arity = tbl.(i) in
-	    let ci = 
-	      if Int.equal arity 0 then mk_const tag
-	      else mk_block tag (mk_rels_accu lvl arity) in
-	    let bi1 = bs1 ci and bi2 = bs2 ci in
-	    if Int.equal i max then conv_val env CONV (lvl + arity) cu bi1 bi2
-	    else (conv_val env CONV (lvl + arity) cu bi1 bi2; aux (i+1)) in
-	  aux 0
+	    let cu = conv_val env CONV lvl p1 p2 cu in
+	    let max = len - 1 in
+	    let rec aux i cu =
+	      let tag,arity = tbl.(i) in
+	      let ci =
+		if Int.equal arity 0 then mk_const tag
+		else mk_block tag (mk_rels_accu lvl arity) in
+	      let bi1 = bs1 ci and bi2 = bs2 ci in
+	      if Int.equal i max then conv_val env CONV (lvl + arity) bi1 bi2 cu
+	      else aux (i+1) (conv_val env CONV (lvl + arity) bi1 bi2 cu) in
+	    aux 0 cu
 	  end
     | Afix(t1,f1,rp1,s1), Afix(t2,f2,rp2,s2) ->
 	if not (Int.equal s1 s2) || not (Array.equal Int.equal rp1 rp2) then raise NotConvertible;
-	if f1 == f2 then ()
+	if f1 == f2 then cu
 	else conv_fix env lvl t1 f1 t2 f2 cu
     | (Acofix(t1,f1,s1,_) | Acofixe(t1,f1,s1,_)),
       (Acofix(t2,f2,s2,_) | Acofixe(t2,f2,s2,_)) ->
 	if not (Int.equal s1 s2) then raise NotConvertible;
-	if f1 == f2 then ()
+	if f1 == f2 then cu
 	else
 	  if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible
 	  else conv_fix env lvl t1 f1 t2 f2 cu 
     | Aprod(_,d1,c1), Aprod(_,d2,c2) ->
-	conv_val env CONV lvl cu d1 d2;
-	let v = mk_rel_accu lvl in
-	conv_val env pb (lvl + 1) cu (d1 v) (d2 v)
-    | _, _ -> raise NotConvertible
+       let cu = conv_val env CONV lvl d1 d2 cu in
+       let v = mk_rel_accu lvl in
+       conv_val env pb (lvl + 1) (d1 v) (d2 v) cu
+    | Aproj(p1,ac1), Aproj(p2,ac2) ->
+       if not (Constant.equal p1 p2) then raise NotConvertible
+       else conv_accu env CONV lvl ac1 ac2 cu
+    | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _
+    | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _
+    | Aproj _, _ -> raise NotConvertible
 
 (* Precondition length t1 = length f1 = length f2 = length t2 *)
 and conv_fix env lvl t1 f1 t2 f2 cu =
@@ -112,22 +120,15 @@ and conv_fix env lvl t1 f1 t2 f2 cu =
   let max = len - 1 in
   let fargs = mk_rels_accu lvl len in
   let flvl = lvl + len in
-  let rec aux i =
-    conv_val env CONV lvl cu t1.(i) t2.(i);
+  let rec aux i cu =
+    let cu = conv_val env CONV lvl t1.(i) t2.(i) cu in
     let fi1 = napply f1.(i) fargs in
     let fi2 = napply f2.(i) fargs in
-    if Int.equal i max then conv_val env CONV flvl cu fi1 fi2
-    else (conv_val env CONV flvl cu fi1 fi2; aux (i+1)) in
-  aux 0
+    if Int.equal i max then conv_val env CONV flvl fi1 fi2 cu
+    else aux (i+1) (conv_val env CONV flvl fi1 fi2 cu) in
+  aux 0 cu
 
-let native_conv pb sigma env t1 t2 =
-  if !Flags.no_native_compiler then begin
-    let msg = "Native compiler is disabled, "^
-    "falling back to VM conversion test." in
-    Pp.msg_warning (Pp.str msg);
-    vm_conv pb env t1 t2
-  end
-  else
+let native_conv_gen pb sigma env univs t1 t2 =
   let penv = Environ.pre_env env in 
   let ml_filename, prefix = get_ml_filename () in
   let code, upds = mk_conv_code penv sigma prefix t1 t2 in
@@ -141,8 +142,25 @@ let native_conv pb sigma env t1 t2 =
         let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
         if !Flags.debug then Pp.msg_debug (Pp.str time_info);
         (* TODO change 0 when we can have deBruijn *)
-        conv_val env pb 0 (Environ.universes env) !rt1 !rt2
+        fst (conv_val env pb 0 !rt1 !rt2 univs)
       end
   | _ -> anomaly (Pp.str "Compilation failure") 
 
-let _ = set_nat_conv native_conv
+(* Wrapper for [native_conv] above *)
+let native_conv cv_pb sigma env t1 t2 =
+  if Coq_config.no_native_compiler then begin
+    let msg = "Native compiler is disabled, falling back to VM conversion test." in
+    Pp.msg_warning (Pp.str msg);
+    vm_conv cv_pb env t1 t2
+  end
+  else
+  let univs = Environ.universes env in
+  let b =
+    if cv_pb = CUMUL then Constr.leq_constr_univs univs t1 t2
+    else Constr.eq_constr_univs univs t1 t2
+  in
+  if not b then
+    let univs = (univs, checked_universes) in
+    let t1 = Term.it_mkLambda_or_LetIn t1 (Environ.rel_context env) in
+    let t2 = Term.it_mkLambda_or_LetIn t2 (Environ.rel_context env) in
+    let _ = native_conv_gen cv_pb sigma env univs t1 t2 in ()