From b053d98fb17d2f46878f49d7adf4839ae632c10b Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Tue, 15 May 2018 21:51:21 +0200
Subject: Remove vm_conv hook and reorganize kernel files

---
 kernel/kernel.mllib  |  6 +++---
 kernel/nativeconv.ml |  2 +-
 kernel/reduction.ml  | 18 ------------------
 kernel/reduction.mli |  6 ------
 kernel/typeops.ml    |  2 +-
 kernel/vconv.ml      | 14 +++++++++++---
 6 files changed, 16 insertions(+), 32 deletions(-)

(limited to 'kernel')

diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 5d270125a..3fed3ed29 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -29,8 +29,11 @@ Cbytegen
 Nativecode
 Nativelib
 Environ
+Csymtable
+Vm
 CClosure
 Reduction
+Vconv
 Nativeconv
 Type_errors
 Modops
@@ -43,6 +46,3 @@ Subtyping
 Mod_typing
 Nativelibrary
 Safe_typing
-Csymtable
-Vm
-Vconv
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index c71f746be..f51b58322 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -163,7 +163,7 @@ let warn_no_native_compiler =
 let native_conv cv_pb sigma env t1 t2 =
   if not Coq_config.native_compiler then begin
     warn_no_native_compiler ();
-    vm_conv cv_pb env t1 t2
+    Vconv.vm_conv cv_pb env t1 t2
   end
   else
   let univs = Environ.universes env in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 38106fbf6..6cd3917c7 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -789,24 +789,6 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta
     env univs t1 t2 = 
   infer_conv_universes CUMUL l2r evars ts env univs t1 t2
 
-(* This reference avoids always having to link C code with the kernel *)
-let vm_conv = ref (fun cv_pb env ->
-		   gen_conv cv_pb env ~evars:((fun _->None), universes env))
-
-let warn_bytecode_compiler_failed =
-  let open Pp in
-  CWarnings.create ~name:"bytecode-compiler-failed" ~category:"bytecode-compiler"
-         (fun () -> strbrk "Bytecode compiler failed, " ++
-                      strbrk "falling back to standard conversion")
-
-let set_vm_conv (f:conv_pb -> types kernel_conversion_function) = vm_conv := f
-let vm_conv cv_pb env t1 t2 =
-  try
-    !vm_conv cv_pb env t1 t2
-  with Not_found | Invalid_argument _ ->
-    warn_bytecode_compiler_failed ();
-    gen_conv cv_pb env t1 t2
-
 let default_conv cv_pb ?(l2r=false) env t1 t2 =
     gen_conv cv_pb env t1 t2
 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 14e4270b7..2e10f98c5 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -87,10 +87,6 @@ val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) ->
 val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) ->
   Names.transparent_state -> (constr,'a) generic_conversion_function
 
-(** option for conversion *)
-val set_vm_conv : (conv_pb -> types kernel_conversion_function) -> unit
-val vm_conv : conv_pb -> types kernel_conversion_function
-
 val default_conv     : conv_pb -> ?l2r:bool -> types kernel_conversion_function
 val default_conv_leq : ?l2r:bool -> types kernel_conversion_function
 
@@ -128,5 +124,3 @@ exception NotArity
 
 val dest_arity : env -> types -> Term.arity (* raises NotArity if not an arity *)
 val is_arity   : env -> types -> bool
-
-val warn_bytecode_compiler_failed : ?loc:Loc.t -> unit -> unit
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index be4c0e1ec..fd9cefb2c 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -221,7 +221,7 @@ let check_cast env c ct k expected_type =
   try
     match k with
     | VMcast ->
-      vm_conv CUMUL env ct expected_type
+      Vconv.vm_conv CUMUL env ct expected_type
     | DEFAULTcast ->
       default_conv ~l2r:false CUMUL env ct expected_type
     | REVERTcast ->
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index f11803b67..6f350951c 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -185,8 +185,18 @@ and conv_arguments env ?from:(from=0) k args1 args2 cu =
       !rcu
     else raise NotConvertible
 
+let warn_bytecode_compiler_failed =
+  let open Pp in
+  CWarnings.create ~name:"bytecode-compiler-failed" ~category:"bytecode-compiler"
+         (fun () -> strbrk "Bytecode compiler failed, " ++
+                      strbrk "falling back to standard conversion")
+
 let vm_conv_gen cv_pb env univs t1 t2 =
-  try 
+  if not Coq_config.bytecode_compiler then
+    Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
+      full_transparent_state env univs t1 t2
+  else
+  try
     let v1 = val_of_constr env t1 in
     let v2 = val_of_constr env t2 in
     fst (conv_val env cv_pb (nb_rel env) v1 v2 univs)
@@ -204,5 +214,3 @@ let vm_conv cv_pb env t1 t2 =
   if not b then
     let univs = (univs, checked_universes) in
     let _ = vm_conv_gen cv_pb env univs t1 t2 in ()
-
-let _ = if Coq_config.bytecode_compiler then Reduction.set_vm_conv vm_conv
-- 
cgit v1.2.3