Imported Upstream version 8.5~beta1+dfsg

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