diff options
| -rw-r--r-- | kernel/kernel.mllib | 6 | ||||
| -rw-r--r-- | kernel/nativeconv.ml | 2 | ||||
| -rw-r--r-- | kernel/reduction.ml | 18 | ||||
| -rw-r--r-- | kernel/reduction.mli | 6 | ||||
| -rw-r--r-- | kernel/typeops.ml | 2 | ||||
| -rw-r--r-- | kernel/vconv.ml | 14 |
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 |