summaryrefslogtreecommitdiff
path: root/kernel/retroknowledge.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/retroknowledge.mli')
-rw-r--r--kernel/retroknowledge.mli96
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