diff options
Diffstat (limited to 'kernel/retroknowledge.mli')
| -rw-r--r-- | kernel/retroknowledge.mli | 96 |
1 files changed, 66 insertions, 30 deletions
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 0b1d8c69..9a63deb7 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -12,7 +12,7 @@ open Term type retroknowledge (** aliased type for clarity purpose*) -type entry = (constr, types) kind_of_term +type entry = Constr.t (** the following types correspond to the different "things" the kernel can learn about.*) @@ -34,6 +34,7 @@ type n_field = type int31_field = | Int31Bits | Int31Type + | Int31Constructor | Int31Twice | Int31TwicePlusOne | Int31Phi @@ -48,10 +49,14 @@ type int31_field = | Int31TimesC | Int31Div21 | Int31Div + | Int31Diveucl | Int31AddMulDiv | Int31Compare | Int31Head0 | Int31Tail0 + | Int31Lor + | Int31Land + | Int31Lxor type field = @@ -115,38 +120,69 @@ val get_vm_before_match_info : retroknowledge -> entry -> Cbytecodes.bytecodes val get_vm_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 -val mem : retroknowledge -> field -> bool -val remove : retroknowledge -> field -> retroknowledge -val find : retroknowledge -> field -> entry +val get_native_compiling_info : retroknowledge -> entry -> Nativeinstr.prefix -> + Nativeinstr.lambda array -> Nativeinstr.lambda -(** the following function manipulate the reactive information of values - they are only used by the functions of Pre_env, and Environ to implement - the functions register and unregister of Environ *) -val add_vm_compiling_info : retroknowledge-> entry -> - (bool -> Cbytecodes.comp_env -> constr array -> int -> - Cbytecodes.bytecodes -> Cbytecodes.bytecodes) -> - retroknowledge -val add_vm_constant_static_info : retroknowledge-> entry -> - (bool->constr array-> - Cbytecodes.structured_constant) -> - retroknowledge -val add_vm_constant_dynamic_info : retroknowledge-> entry -> - (bool -> Cbytecodes.comp_env -> - Cbytecodes.block array -> int -> - Cbytecodes.bytecodes -> Cbytecodes.bytecodes) -> - retroknowledge -val add_vm_before_match_info : retroknowledge -> entry -> - (bool->Cbytecodes.bytecodes->Cbytecodes.bytecodes) -> - retroknowledge +val get_native_constant_static_info : retroknowledge -> entry -> + constr array -> Nativeinstr.lambda -val add_vm_decompile_constant_info : retroknowledge -> entry -> - (int -> constr) -> retroknowledge +val get_native_constant_dynamic_info : retroknowledge -> entry -> + Nativeinstr.prefix -> constructor -> + Nativeinstr.lambda array -> + Nativeinstr.lambda +val get_native_before_match_info : retroknowledge -> entry -> + Nativeinstr.prefix -> constructor -> + Nativeinstr.lambda -> Nativeinstr.lambda -val clear_info : retroknowledge-> entry -> retroknowledge +(** 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 +val mem : retroknowledge -> field -> bool +(* val remove : retroknowledge -> field -> retroknowledge *) +val find : retroknowledge -> field -> entry +(** Dispatching type for the above [get_*] functions. *) +type reactive_info = {(*information required by the compiler of the VM *) + vm_compiling : + (*fastcomputation flag -> continuation -> result *) + (bool->Cbytecodes.comp_env->constr array -> + int->Cbytecodes.bytecodes->Cbytecodes.bytecodes) + option; + vm_constant_static : + (*fastcomputation flag -> constructor -> args -> result*) + (bool->constr array->Cbytecodes.structured_constant) + option; + vm_constant_dynamic : + (*fastcomputation flag -> constructor -> reloc -> args -> sz -> cont -> result *) + (bool->Cbytecodes.comp_env->Cbytecodes.block array->int-> + Cbytecodes.bytecodes->Cbytecodes.bytecodes) + option; + (* fastcomputation flag -> cont -> result *) + vm_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option; + (* tag (= compiled int for instance) -> result *) + vm_decompile_const : (int -> Term.constr) option; + + native_compiling : + (bool -> Nativeinstr.prefix -> Nativeinstr.lambda array -> + Nativeinstr.lambda) option; + + native_constant_static : + (bool -> constr array -> Nativeinstr.lambda) option; + + native_constant_dynamic : + (bool -> Nativeinstr.prefix -> constructor -> + Nativeinstr.lambda array -> Nativeinstr.lambda) option; + + native_before_match : (bool -> Nativeinstr.prefix -> constructor -> + Nativeinstr.lambda -> Nativeinstr.lambda) option + +} + +val empty_reactive_info : reactive_info + +(** Hook to be set after the compiler are installed to dispatch fields + into the above [get_*] functions. *) +val dispatch_hook : (retroknowledge -> entry -> field -> reactive_info) Hook.t |