aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--kernel/kernel.mllib6
-rw-r--r--kernel/nativeconv.ml2
-rw-r--r--kernel/reduction.ml18
-rw-r--r--kernel/reduction.mli6
-rw-r--r--kernel/typeops.ml2
-rw-r--r--kernel/vconv.ml14
6 files changed, 16 insertions, 32 deletions
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