diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-04-07 15:45:33 -0400 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-04-09 01:05:48 -0400 |
| commit | 2e8c02d5644e8e8e446ab6dfd832322276e44f89 (patch) | |
| tree | 9f7564ac88d210611cbd5fa5cf2de8efad038e36 /kernel/retroknowledge.mli | |
| parent | a91518d0b07b9a2cd7d9381044c20365771ec382 (diff) | |
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.
Diffstat (limited to 'kernel/retroknowledge.mli')
| -rw-r--r-- | kernel/retroknowledge.mli | 16 |
1 files changed, 5 insertions, 11 deletions
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 |