Make the retroknowledge marshalable.

Essential for parallel processing of Coq documents.

It is a fairly straightforward change but a tad tedious, I may have introduced some bugs in the process.

4 files changed, 158 insertions, 320 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index aa83864c6..6b0b0bdba 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -549,35 +549,23 @@ let retroknowledge f env =
 let registered env field =
     retroknowledge mem env field
 
-(* spiwack: this unregistration function is not in operation yet. It should
-            not be used *)
-(* this unregistration function assumes that no "constr" can hold two different
-   places in the retroknowledge. There is no reason why it shouldn't be true,
-   but in case someone needs it, remember to add special branches to the
-   unregister function *)
-let unregister env field =
-  match field with
-    | KInt31 (_,Int31Type) ->
-	(*there is only one matching kind due to the fact that Environ.env
-          is abstract, and that the only function which add elements to the
-          retroknowledge is Environ.register which enforces this shape *)
-	(match kind_of_term (retroknowledge find env field) with
-	   | Ind i31t -> let i31c = mkConstructUi (i31t, 1) in
-	     {env with retroknowledge =
-		 remove (retroknowledge clear_info env i31c) field}
-	   | _ -> assert false)
-    |_ -> {env with retroknowledge =
-	   try
-	     remove (retroknowledge clear_info env
-                       (retroknowledge find env field)) field
-	   with Not_found ->
-	     retroknowledge remove env field}
-
+let register_one env field entry =
+  { env with retroknowledge = Retroknowledge.add_field env.retroknowledge field entry }
 
+(* [register env field entry] may register several fields when needed *)
+let register env field entry =
+  match field with
+    | KInt31 (grp, Int31Type) ->
+        let i31c = match kind_of_term entry with
+                     | Ind i31t -> mkConstructUi (i31t, 1)
+		     | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type")
+	in
+        register_one (register_one env (KInt31 (grp,Int31Constructor)) i31c) field entry
+    | field -> register_one env field entry
 
 (* the Environ.register function syncrhonizes the proactive and reactive
    retroknowledge. *)
-let register =
+let dispatch =
 
   (* subfunction used for static decompilation of int31 (after a vm_compute,
      see pretyping/vnorm.ml for more information) *)
@@ -598,126 +586,94 @@ let register =
 	  mkApp(mkConstruct(ind, 1), array_of_int tag)
   in
 
-  (* subfunction which adds the information bound to the constructor of
-     the int31 type to the reactive retroknowledge *)
-  let add_int31c retroknowledge c =
-    let rk = add_vm_constant_static_info retroknowledge c
-                                         Cbytegen.compile_structured_int31
-    in
-    let rk =
-      add_vm_constant_dynamic_info rk c Cbytegen.dynamic_int31_compilation
-    in
-    let rk =
-      add_native_constant_static_info rk c Nativelambda.compile_static_int31
-    in
-    add_native_constant_dynamic_info rk c Nativelambda.compile_dynamic_int31
-  in
-
-  (* subfunction which adds the compiling information of an
+  (* subfunction which dispatches the compiling information of an
      int31 operation which has a specific vm instruction (associates
      it to the name of the coq definition in the reactive retroknowledge) *)
-  let add_int31_op retroknowledge v n op prim kn =
-    let rk =
-      add_vm_compiling_info retroknowledge v (Cbytegen.op_compilation n op kn)
-    in
-    add_native_compiling_info rk v (Nativelambda.compile_prim prim kn)
-  in
-
-  let add_int31_before_match rk grp v =
-    let rk = add_vm_before_match_info rk v Cbytegen.int31_escape_before_match in
-    match kind_of_term (Retroknowledge.find rk (KInt31 (grp,Int31Bits))) with
-    | Ind (i31bit_type,_) ->
-    add_native_before_match_info rk v (Nativelambda.before_match_int31 i31bit_type)
-    | _ ->
-       anomaly ~label:"Environ.register" (Pp.str "Int31Bits should be an inductive type")
+  let int31_op n op prim kn =
+    { empty_reactive_info with
+      vm_compiling = Some (Cbytegen.op_compilation n op kn);
+      native_compiling = Some (Nativelambda.compile_prim prim kn);
+    }
   in
 
-fun env field value ->
-  (* subfunction which shortens the (very often use) registration of binary
-     operators to the reactive retroknowledge. *)
-  let add_int31_binop_from_const op prim =
-    match kind_of_term value with
-      | Const (kn,_) ->  retroknowledge add_int31_op env value 2
-	                               op prim kn
-      | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")
-  in
-  let add_int31_unop_from_const op prim =
+fun rk value field ->
+  (* subfunction which shortens the (very common) dispatch of operations *)
+  let int31_op_from_const n op prim =
     match kind_of_term value with
-      | Const (kn,_) ->  retroknowledge add_int31_op env value 1
-	                               op prim kn
+      | Const (kn,_) ->  int31_op n op prim kn
       | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")
   in
-  (* subfunction which completes the function constr_of_int31 above
-     by performing the actual retroknowledge operations *)
-  let add_int31_decompilation_from_type rk =
-    (* invariant : the type of bits is registered, otherwise the function
-       would raise Not_found. The invariant is enforced in safe_typing.ml *)
-    match field with
-      | KInt31 (grp, Int31Type) ->
-	  (match kind_of_term (Retroknowledge.find rk (KInt31 (grp,Int31Bits))) with
-	    | Ind (i31bit_type,_) ->
-		(match kind_of_term value with
-		  | Ind (i31t,_) ->
-		      Retroknowledge.add_vm_decompile_constant_info rk
-		               value (constr_of_int31 i31t i31bit_type)
-		  | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type"))
-	    | _ -> anomaly ~label:"Environ.register" (Pp.str "Int31Bits should be an inductive type"))
-      | _ -> anomaly ~label:"Environ.register" (Pp.str "add_int31_decompilation_from_type called with an abnormal field")
-  in
-  {env with retroknowledge =
-  let retroknowledge_with_reactive_info =
+  let int31_binop_from_const op prim = int31_op_from_const 2 op prim in
+  let int31_unop_from_const op prim = int31_op_from_const 1 op prim in
   match field with
     | KInt31 (grp, Int31Type) ->
-        let i31c = match kind_of_term value with
-                     | Ind i31t -> mkConstructUi (i31t, 1)
-		     | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type")
-	in
-	add_int31_decompilation_from_type
-	  (add_int31_before_match
-	     (retroknowledge add_int31c env i31c) grp value)
-    | KInt31 (_, Int31Plus) -> add_int31_binop_from_const Cbytecodes.Kaddint31
+        let int31bit =
+          (* invariant : the type of bits is registered, otherwise the function
+             would raise Not_found. The invariant is enforced in safe_typing.ml *)
+          match field with
+          | KInt31 (grp, Int31Type) -> Retroknowledge.find rk (KInt31 (grp,Int31Bits))
+          | _ -> anomaly ~label:"Environ.register"
+              (Pp.str "add_int31_decompilation_from_type called with an abnormal field")
+        in
+        let i31bit_type =
+          match kind_of_term int31bit with
+          | Ind (i31bit_type,_) -> i31bit_type
+          |  _ -> anomaly ~label:"Environ.register"
+              (Pp.str "Int31Bits should be an inductive type")
+        in
+        let int31_decompilation =
+          match kind_of_term value with
+          | Ind (i31t,_) ->
+              constr_of_int31 i31t i31bit_type
+          | _ -> anomaly ~label:"Environ.register"
+              (Pp.str "should be an inductive type")
+        in
+        { empty_reactive_info with
+          vm_decompile_const = Some int31_decompilation;
+          vm_before_match = Some Cbytegen.int31_escape_before_match;
+          native_before_match = Some (Nativelambda.before_match_int31 i31bit_type);
+        }
+    | KInt31 (_, Int31Constructor) ->
+        { empty_reactive_info with
+          vm_constant_static = Some Cbytegen.compile_structured_int31;
+          vm_constant_dynamic = Some Cbytegen.dynamic_int31_compilation;
+          native_constant_static = Some Nativelambda.compile_static_int31;
+          native_constant_dynamic = Some Nativelambda.compile_dynamic_int31;
+        }
+    | KInt31 (_, Int31Plus) -> int31_binop_from_const Cbytecodes.Kaddint31
 							  Primitives.Int31add
-    | KInt31 (_, Int31PlusC) -> add_int31_binop_from_const Cbytecodes.Kaddcint31
+    | KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31
 							   Primitives.Int31addc
-    | KInt31 (_, Int31PlusCarryC) -> add_int31_binop_from_const Cbytecodes.Kaddcarrycint31
+    | KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31
 								Primitives.Int31addcarryc
-    | KInt31 (_, Int31Minus) -> add_int31_binop_from_const Cbytecodes.Ksubint31
+    | KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31
 							   Primitives.Int31sub
-    | KInt31 (_, Int31MinusC) -> add_int31_binop_from_const Cbytecodes.Ksubcint31
+    | KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31
 							    Primitives.Int31subc
-    | KInt31 (_, Int31MinusCarryC) -> add_int31_binop_from_const
+    | KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const
 	                                Cbytecodes.Ksubcarrycint31 Primitives.Int31subcarryc
-    | KInt31 (_, Int31Times) -> add_int31_binop_from_const Cbytecodes.Kmulint31
+    | KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31
 							   Primitives.Int31mul
-    | KInt31 (_, Int31TimesC) -> add_int31_binop_from_const Cbytecodes.Kmulcint31
-							    Primitives.Int31mulc
-    | KInt31 (_, Int31Div21) -> (* this is a ternary operation *)
-                                (match kind_of_term value with
-				 | Const (kn,u) ->
-				     retroknowledge add_int31_op env value 3
-	                               Cbytecodes.Kdiv21int31 Primitives.Int31div21 kn
-				 | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant"))
-    | KInt31 (_, Int31Div) -> add_int31_binop_from_const Cbytecodes.Kdivint31
+    | KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31
+							   Primitives.Int31mulc
+    | KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31
+                                                           Primitives.Int31div21
+    | KInt31 (_, Int31Div) -> int31_binop_from_const Cbytecodes.Kdivint31
 							 Primitives.Int31div
-    | KInt31 (_, Int31AddMulDiv) -> (* this is a ternary operation *)
-                                (match kind_of_term value with
-				 | Const (kn,u) ->
-				     retroknowledge add_int31_op env value 3
-	                               Cbytecodes.Kaddmuldivint31 Primitives.Int31addmuldiv kn
-				 | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant"))
-    | KInt31 (_, Int31Compare) -> add_int31_binop_from_const Cbytecodes.Kcompareint31
+    | KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31
+                                                         Primitives.Int31addmuldiv
+    | KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31
 							     Primitives.Int31compare
-    | KInt31 (_, Int31Head0) -> add_int31_unop_from_const Cbytecodes.Khead0int31
+    | KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31
 							  Primitives.Int31head0
-    | KInt31 (_, Int31Tail0) -> add_int31_unop_from_const Cbytecodes.Ktail0int31
+    | KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31
 							  Primitives.Int31tail0
-    | KInt31 (_, Int31Lor) -> add_int31_binop_from_const Cbytecodes.Klorint31
+    | KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31
 							 Primitives.Int31lor
-    | KInt31 (_, Int31Land) -> add_int31_binop_from_const Cbytecodes.Klandint31
+    | KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31
 							  Primitives.Int31land
-    | KInt31 (_, Int31Lxor) -> add_int31_binop_from_const Cbytecodes.Klxorint31
+    | KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31
 							  Primitives.Int31lxor
-    | _ -> env.retroknowledge
-  in
-  Retroknowledge.add_field retroknowledge_with_reactive_info field value
-  }
+    | _ -> empty_reactive_info
+
+let _ = Hook.set Retroknowledge.dispatch_hook dispatch
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 7f3fdc536..5e9e5264d 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -284,8 +284,6 @@ val retroknowledge : (retroknowledge->'a) -> env -> 'a
 
 val registered : env -> field -> bool
 
-val unregister : env -> field -> env
-
 val register : env -> field -> Retroknowledge.entry -> env
 
 (** Native compiler *)
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 5a2f5ced7..b645e256f 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -16,19 +16,14 @@
 open Names
 open Term
 
-(* Type declarations, these types shouldn't be exported they are accessed
-   through specific functions. As being mutable and all it is wiser *)
-(* These types are put into two distinct categories: proactive and reactive.
-   Proactive information allows finding the name of a combinator, constructor
-   or inductive type handling a specific function.
-   Reactive information is, on the other hand, everything you need to know
-   about a specific name.*)
+(* The retroknowledge defines a bijective correspondance between some
+   [entry]-s (which are, in fact, merely terms) and [field]-s which
+   are roles assigned to these entries. *)
 
 (* aliased type for clarity purpose*)
 type entry = Constr.t
 
-(* the following types correspond to the different "things"
-   the kernel can learn about. These are the fields of the proactive knowledge*)
+(* [field]-s are the roles the kernel can learn of. *)
 type nat_field =
   | NatType
   | NatPlus
@@ -47,6 +42,7 @@ type n_field =
 type int31_field =
   | Int31Bits
   | Int31Type
+  | Int31Constructor
   | Int31Twice
   | Int31TwicePlusOne
   | Int31Phi
@@ -70,9 +66,9 @@ type int31_field =
   | Int31Lxor
 
 type field =
- (* | KEq
-  | KNat of nat_field
-  | KN of n_field *)
+  (* | KEq
+     | KNat of nat_field
+     | KN of n_field *)
   | KInt31 of string*int31_field
 
 
@@ -83,23 +79,16 @@ type flags = {fastcomputation : bool}
 
 
 
-(*A definition of maps from strings to pro_int31, to be able
-  to have any amount of coq representation for the 31bits integers *)
+(* The [proactive] knowledge contains the mapping [field->entry]. *)
 
 module Proactive =
   Map.Make (struct type t = field let compare = compare end)
 
 type proactive = entry Proactive.t
 
-(* the reactive knowledge is represented as a functionaly map
-   from the type of terms (actually it is the terms whose outermost
-   layer is unfolded (typically by Term.kind_of_term)) to the
-   type reactive_end which is a record containing all the kind of reactive
-   information needed *)
-(* todo: because of the bug with output state, reactive_end should eventually
-   contain no function. A forseen possibility is to make it a map from
-   a finite type describing the fields to the field of proactive retroknowledge
-   (and then to make as many functions as needed in environ.ml) *)
+(* The [reactive] knowledge contains the mapping
+   [entry->field]. Fields are later to be interpreted as a
+   [reactive_info]. *)
 
 module EntryOrd =
 struct
@@ -109,7 +98,7 @@ end
 
 module Reactive = Map.Make (EntryOrd)
 
-type reactive_end = {(*information required by the compiler of the VM *)
+type reactive_info = {(*information required by the compiler of the VM *)
   vm_compiling :
       (*fastcomputation flag -> continuation -> result *)
       (bool->Cbytecodes.comp_env->constr array ->
@@ -147,7 +136,7 @@ type reactive_end = {(*information required by the compiler of the VM *)
 
 
 
-and reactive = reactive_end Reactive.t
+and reactive = field Reactive.t
 
 and retroknowledge = {flags : flags; proactive : proactive; reactive : reactive}
 
@@ -174,7 +163,7 @@ let initial_retroknowledge =
    proactive = initial_proactive;
    reactive = initial_reactive }
 
-let empty_reactive_end =
+let empty_reactive_info =
   { vm_compiling = None ;
     vm_constant_static = None;
     vm_constant_dynamic = None;
@@ -188,184 +177,82 @@ let empty_reactive_end =
 
 
 
+(* adds a binding [entry<->field]. *)
+let add_field knowledge field entry =
+  {knowledge with
+    proactive = Proactive.add field entry knowledge.proactive;
+    reactive = Reactive.add entry field knowledge.reactive}
 
 (* acces functions for proactive retroknowledge *)
-let add_field knowledge field value =
-  {knowledge with proactive = Proactive.add field value knowledge.proactive}
-
 let mem knowledge field =
   Proactive.mem field knowledge.proactive
 
-let remove knowledge field =
-  {knowledge with proactive = Proactive.remove field knowledge.proactive}
-
 let find knowledge field =
   Proactive.find field knowledge.proactive
 
 
+let (dispatch,dispatch_hook) = Hook.make ()
 
-
+let dispatch_reactive entry retroknowledge =
+  Hook.get dispatch retroknowledge entry (Reactive.find entry retroknowledge.reactive)
 
 (*access functions for reactive retroknowledge*)
 
 (* used for compiling of functions (add, mult, etc..) *)
 let get_vm_compiling_info knowledge key =
-  match (Reactive.find key knowledge.reactive).vm_compiling
+  match (dispatch_reactive key knowledge).vm_compiling
   with
     | None -> raise Not_found
     | Some f -> f knowledge.flags.fastcomputation
 
 (* used for compilation of fully applied constructors *)
 let get_vm_constant_static_info knowledge key =
-  match (Reactive.find key knowledge.reactive).vm_constant_static
+  match (dispatch_reactive key knowledge).vm_constant_static
   with
     | None -> raise Not_found
     | Some f -> f knowledge.flags.fastcomputation
 
 (* used for compilation of partially applied constructors *)
 let get_vm_constant_dynamic_info knowledge key =
-  match (Reactive.find key knowledge.reactive).vm_constant_dynamic
+  match (dispatch_reactive key knowledge).vm_constant_dynamic
   with
     | None -> raise Not_found
     | Some f -> f knowledge.flags.fastcomputation
 
 let get_vm_before_match_info knowledge key =
-  match (Reactive.find key knowledge.reactive).vm_before_match
+  match (dispatch_reactive key knowledge).vm_before_match
   with
     | None -> raise Not_found
     | Some f -> f knowledge.flags.fastcomputation
 
 let get_vm_decompile_constant_info knowledge key =
-  match (Reactive.find key knowledge.reactive).vm_decompile_const
+  match (dispatch_reactive key knowledge).vm_decompile_const
   with
     | None -> raise Not_found
     | Some f -> f
 
 let get_native_compiling_info knowledge key =
-  match (Reactive.find key knowledge.reactive).native_compiling
+  match (dispatch_reactive key knowledge).native_compiling
   with
     | None -> raise Not_found
     | Some f -> f knowledge.flags.fastcomputation
 
 (* used for compilation of fully applied constructors *)
 let get_native_constant_static_info knowledge key =
-  match (Reactive.find key knowledge.reactive).native_constant_static
+  match (dispatch_reactive key knowledge).native_constant_static
   with
     | None -> raise Not_found
     | Some f -> f knowledge.flags.fastcomputation
 
 (* used for compilation of partially applied constructors *)
 let get_native_constant_dynamic_info knowledge key =
-  match (Reactive.find key knowledge.reactive).native_constant_dynamic
+  match (dispatch_reactive key knowledge).native_constant_dynamic
   with
     | None -> raise Not_found
     | Some f -> f knowledge.flags.fastcomputation
 
 let get_native_before_match_info knowledge key =
-  match (Reactive.find key knowledge.reactive).native_before_match
+  match (dispatch_reactive key knowledge).native_before_match
   with
     | None -> raise Not_found
     | Some f -> f knowledge.flags.fastcomputation
-
-(* functions manipulating reactive knowledge *)
-let add_vm_compiling_info knowledge value nfo =
-  {knowledge with reactive =
-   try
-     Reactive.add value
-       {(Reactive.find value (knowledge.reactive)) with vm_compiling = Some nfo}
-       knowledge.reactive
-   with Not_found ->
-     Reactive.add value {empty_reactive_end with vm_compiling = Some nfo}
-       knowledge.reactive
-  }
-
-let add_vm_constant_static_info knowledge value nfo =
-  {knowledge with reactive =
-   try
-     Reactive.add value
-       {(Reactive.find value (knowledge.reactive)) with vm_constant_static = Some nfo}
-       knowledge.reactive
-   with Not_found ->
-     Reactive.add value {empty_reactive_end with vm_constant_static = Some nfo}
-       knowledge.reactive
-  }
-
-let add_vm_constant_dynamic_info knowledge value nfo =
-  {knowledge with reactive =
-   try
-     Reactive.add value
-       {(Reactive.find value (knowledge.reactive)) with vm_constant_dynamic = Some nfo}
-       knowledge.reactive
-   with Not_found ->
-     Reactive.add value {empty_reactive_end with vm_constant_dynamic = Some nfo}
-       knowledge.reactive
-  }
-
-let add_vm_before_match_info knowledge value nfo =
-  {knowledge with reactive =
-   try
-     Reactive.add value
-       {(Reactive.find value (knowledge.reactive)) with vm_before_match = Some nfo}
-       knowledge.reactive
-   with Not_found ->
-     Reactive.add value {empty_reactive_end with vm_before_match = Some nfo}
-       knowledge.reactive
-  }
-
-let add_vm_decompile_constant_info knowledge value nfo =
-  {knowledge with reactive =
-   try
-     Reactive.add value
-       {(Reactive.find value (knowledge.reactive)) with vm_decompile_const = Some nfo}
-       knowledge.reactive
-   with Not_found ->
-     Reactive.add value {empty_reactive_end with vm_decompile_const = Some nfo}
-       knowledge.reactive
-  }
-
-let add_native_compiling_info knowledge value nfo =
-  {knowledge with reactive =
-   try
-     Reactive.add value
-       {(Reactive.find value (knowledge.reactive)) with native_compiling = Some nfo}
-       knowledge.reactive
-   with Not_found ->
-     Reactive.add value {empty_reactive_end with native_compiling = Some nfo}
-       knowledge.reactive
-  }
-
-let add_native_constant_static_info knowledge value nfo =
-  {knowledge with reactive =
-   try
-     Reactive.add value
-       {(Reactive.find value (knowledge.reactive)) with native_constant_static = Some nfo}
-       knowledge.reactive
-   with Not_found ->
-     Reactive.add value {empty_reactive_end with native_constant_static = Some nfo}
-       knowledge.reactive
-  }
-
-let add_native_constant_dynamic_info knowledge value nfo =
-  {knowledge with reactive =
-   try
-     Reactive.add value
-       {(Reactive.find value (knowledge.reactive)) with native_constant_dynamic = Some nfo}
-       knowledge.reactive
-   with Not_found ->
-     Reactive.add value {empty_reactive_end with native_constant_dynamic = Some nfo}
-       knowledge.reactive
-  }
-
-let add_native_before_match_info knowledge value nfo =
-  {knowledge with reactive =
-   try
-     Reactive.add value
-       {(Reactive.find value (knowledge.reactive)) with native_before_match = Some nfo}
-       knowledge.reactive
-   with Not_found ->
-     Reactive.add value {empty_reactive_end with native_before_match = Some nfo}
-       knowledge.reactive
-  }
-
-let clear_info knowledge value =
-  {knowledge with reactive = Reactive.remove value knowledge.reactive}
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 30d824a9b..846f135e6 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -34,6 +34,7 @@ type n_field =
 type int31_field =
   | Int31Bits
   | Int31Type
+  | Int31Constructor
   | Int31Twice
   | Int31TwicePlusOne
   | Int31Phi
@@ -133,58 +134,54 @@ val get_native_before_match_info : retroknowledge -> entry ->
 				   Nativeinstr.prefix -> constructor ->
 				   Nativeinstr.lambda -> Nativeinstr.lambda
 
+
 (** 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 remove : retroknowledge -> field -> retroknowledge *)
 val find : retroknowledge -> field -> entry
 
-(** 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 add_vm_decompile_constant_info : retroknowledge -> entry ->
-                                    (int -> constr) -> retroknowledge
-
-val add_native_compiling_info : retroknowledge-> entry ->
-				(bool -> Nativeinstr.prefix ->
-			         Nativeinstr.lambda array -> Nativeinstr.lambda) ->
-				retroknowledge
-
-val add_native_constant_static_info : retroknowledge -> entry ->
-                                  (bool -> constr array ->
-                                      Nativeinstr.lambda) ->
-                                  retroknowledge
-
-val add_native_constant_dynamic_info : retroknowledge -> entry ->
-                                   (bool -> Nativeinstr.prefix -> constructor ->
-				      Nativeinstr.lambda array ->
-				      Nativeinstr.lambda) ->
-                                   retroknowledge
-
-val add_native_before_match_info : retroknowledge -> entry ->
-				   (bool -> Nativeinstr.prefix -> constructor ->
-				      Nativeinstr.lambda -> Nativeinstr.lambda) ->
-				   retroknowledge
-
-val clear_info : retroknowledge-> entry -> retroknowledge
-
-
 
+(** 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