From 2e8c02d5644e8e8e446ab6dfd832322276e44f89 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 7 Apr 2014 15:45:33 -0400 Subject: Machine arithmetic operations for native compiler. This completes the port of the native compiler to retroknowledge. However, some testing and optimizations are still to be done. --- kernel/retroknowledge.mli | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) (limited to 'kernel/retroknowledge.mli') diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 644fb7074..30d824a9b 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -118,9 +118,8 @@ val get_vm_before_match_info : retroknowledge -> entry -> Cbytecodes.bytecodes val get_vm_decompile_constant_info : retroknowledge -> entry -> int -> Term.constr -val get_native_compiling_info : retroknowledge -> entry -> Cbytecodes.comp_env -> - constr array -> - int -> Cbytecodes.bytecodes-> Cbytecodes.bytecodes +val get_native_compiling_info : retroknowledge -> entry -> Nativeinstr.prefix -> + Nativeinstr.lambda array -> Nativeinstr.lambda val get_native_constant_static_info : retroknowledge -> entry -> constr array -> Nativeinstr.lambda @@ -134,8 +133,6 @@ val get_native_before_match_info : retroknowledge -> entry -> Nativeinstr.prefix -> constructor -> Nativeinstr.lambda -> Nativeinstr.lambda -val get_native_decompile_constant_info : retroknowledge -> entry -> int -> Term.constr - (** the following functions are solely used in Pre_env and Environ to implement the functions register and unregister (and mem) of Environ *) val add_field : retroknowledge -> field -> entry -> retroknowledge @@ -167,9 +164,9 @@ val add_vm_decompile_constant_info : retroknowledge -> entry -> (int -> constr) -> retroknowledge val add_native_compiling_info : retroknowledge-> entry -> - (bool -> Cbytecodes.comp_env -> constr array -> int -> - Cbytecodes.bytecodes -> Cbytecodes.bytecodes) -> - retroknowledge + (bool -> Nativeinstr.prefix -> + Nativeinstr.lambda array -> Nativeinstr.lambda) -> + retroknowledge val add_native_constant_static_info : retroknowledge -> entry -> (bool -> constr array -> @@ -187,9 +184,6 @@ val add_native_before_match_info : retroknowledge -> entry -> Nativeinstr.lambda -> Nativeinstr.lambda) -> retroknowledge -val add_native_decompile_constant_info : retroknowledge -> entry -> - (int -> constr) -> retroknowledge - val clear_info : retroknowledge-> entry -> retroknowledge -- cgit v1.2.3