diff options
| author | Maxime Dénès | 2014-04-06 12:41:26 -0400 |
|---|---|---|
| committer | Maxime Dénès | 2014-04-09 01:05:48 -0400 |
| commit | aa3b8b7b24e809b379fcc86f2b21ae4380b211d5 (patch) | |
| tree | 254b9d84ee42798a513bcd5aea032a6e552b2067 /kernel/retroknowledge.ml | |
| parent | de61c7d77e49286622c4aebd56f2e87b0df93903 (diff) | |
Partial support for open terms in int31.
Diffstat (limited to 'kernel/retroknowledge.ml')
| -rw-r--r-- | kernel/retroknowledge.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 1049ab94dd..b39ae94a57 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -13,6 +13,7 @@ (* This file defines the knowledge that the kernel is able to optimize for evaluation in the bytecode virtual machine *) +open Names open Term (* Type declarations, these types shouldn't be exported they are accessed @@ -127,17 +128,21 @@ type reactive_end = {(*information required by the compiler of the VM *) 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->Cbytecodes.comp_env->constr array -> int->Cbytecodes.bytecodes->Cbytecodes.bytecodes) option; + native_constant_static : (bool -> constr array -> Nativeinstr.lambda) option; + native_constant_dynamic : - (bool->Cbytecodes.comp_env->Cbytecodes.block array->int-> - Cbytecodes.bytecodes->Cbytecodes.bytecodes) - option; + (bool -> Nativeinstr.prefix -> constructor -> + Nativeinstr.lambda array -> Nativeinstr.lambda) option; + native_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option; + native_decompile_const : (int -> Term.constr) option } |