diff options
-rw-r--r-- | kernel/environ.ml | 206 | ||||
-rw-r--r-- | kernel/environ.mli | 2 | ||||
-rw-r--r-- | kernel/retroknowledge.ml | 177 | ||||
-rw-r--r-- | kernel/retroknowledge.mli | 93 |
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 |