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/nativeconv.ml | 57 +++++++++++++++++++++++++++++++++-------------------
 1 file changed, 36 insertions(+), 21 deletions(-)

(limited to 'kernel/nativeconv.ml')

diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 3c0afe38..2a7afdca 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open CErrors
@@ -54,13 +56,18 @@ and conv_accu env pb lvl k1 k2 cu =
     conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu
   else
     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
+    Array.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 cu
   else
     match a1, a2 with
-    | Ameta _, _ | _, Ameta _ | Aevar _, _ | _, Aevar _ -> assert false
+    | Ameta (m1,_), Ameta (m2,_) ->
+      if Int.equal m1 m2 then cu else raise NotConvertible
+    | Aevar (ev1,_,args1), Aevar (ev2,_,args2) ->
+      if Evar.equal ev1 ev2 then
+        Array.fold_right2 (conv_val env CONV lvl) args1 args2 cu
+      else raise NotConvertible
     | Arel i1, Arel i2 -> 
 	if Int.equal i1 i2 then cu else raise NotConvertible
     | Aind (ind1,u1), Aind (ind2,u2) ->
@@ -112,7 +119,7 @@ and conv_atom env pb lvl a1 a2 cu =
        else conv_accu env CONV lvl ac1 ac2 cu
     | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _
     | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _
-    | Aproj _, _ -> raise NotConvertible
+    | Aproj _, _ | Ameta _, _ | Aevar _, _ -> raise NotConvertible
 
 (* Precondition length t1 = length f1 = length f2 = length t2 *)
 and conv_fix env lvl t1 f1 t2 f2 cu =
@@ -128,11 +135,30 @@ and conv_fix env lvl t1 f1 t2 f2 cu =
     else aux (i+1) (conv_val env CONV flvl fi1 fi2 cu) in
   aux 0 cu
 
+let warn_no_native_compiler =
+  let open Pp in
+  CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler"
+         (fun () -> strbrk "Native compiler is disabled," ++
+                      strbrk " falling back to VM conversion test.")
+
+type vm_conv_gen = { vm_conv_gen : 'a. conv_pb -> (Constr.types, 'a) generic_conversion_function }
+
+let vm_conv_gen =
+  ref { vm_conv_gen = fun cv_pb env univs t1 t2 ->
+    generic_conv cv_pb ~l2r:false (fun _ -> None) full_transparent_state env univs t1 t2 }
+
+let set_vm_conv_gen f = vm_conv_gen := f
+
 let native_conv_gen pb sigma env univs t1 t2 =
+  if not Coq_config.native_compiler then begin
+    warn_no_native_compiler ();
+    vm_conv_gen.contents.vm_conv_gen pb env univs t1 t2
+  end
+  else
   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
-  match compile ml_filename code with
+  match compile ml_filename code ~profile:false with
   | (true, fn) ->
       begin
         if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
@@ -141,24 +167,13 @@ let native_conv_gen pb sigma env univs t1 t2 =
         let t1 = Sys.time () in
         let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
         if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
-        (* TODO change 0 when we can have deBruijn *)
+        (* TODO change 0 when we can have de Bruijn *)
         fst (conv_val env pb 0 !rt1 !rt2 univs)
       end
-  | _ -> anomaly (Pp.str "Compilation failure") 
-
-let warn_no_native_compiler =
-  let open Pp in
-  CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler"
-         (fun () -> strbrk "Native compiler is disabled," ++
-                      strbrk " falling back to VM conversion test.")
+  | _ -> anomaly (Pp.str "Compilation failure.") 
 
 (* Wrapper for [native_conv] above *)
 let native_conv cv_pb sigma env t1 t2 =
-  if Coq_config.no_native_compiler then begin
-    warn_no_native_compiler ();
-    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
-- 
cgit v1.2.3