diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-02-16 17:53:12 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-23 15:51:40 +0100 |
commit | 557c5a2938f16c0601f5a0323c66b78d2da01ee9 (patch) | |
tree | 8dc727525696f27856ae241bec442769e99c8e58 /kernel/retroknowledge.mli | |
parent | aa2653b5e6877547ece7a8d3051fc67414390240 (diff) |
New IR in VM: Clambda.
This intermediate representation serves two purposes:
1- It is a preliminary step for primitive machine integers, as iterators
will be compiled to Clambda.
2- It makes the VM compilation passes closer to the ones of
native_compute. Once we unifiy the representation of values, we should
be able to factorize the lambda-code generation between the two
compilers, as well as the reification code.
This code was written by Benjamin Grégoire and myself.
Diffstat (limited to 'kernel/retroknowledge.mli')
-rw-r--r-- | kernel/retroknowledge.mli | 26 |
1 files changed, 10 insertions, 16 deletions
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index e4d78ba14..134b4b4f7 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -82,9 +82,8 @@ val initial_retroknowledge : retroknowledge and the continuation cont of the bytecode compilation returns the compilation of id in cont if it has a specific treatment or raises Not_found if id should be compiled as usual *) -val get_vm_compiling_info : retroknowledge -> entry -> Cbytecodes.comp_env -> - constr array -> - int -> Cbytecodes.bytecodes-> Cbytecodes.bytecodes +val get_vm_compiling_info : retroknowledge -> entry -> + Cinstr.lambda array -> Cinstr.lambda (*Given an identifier id (usually Construct _) and its argument array, returns a function that tries an ad-hoc optimisated compilation (in the case of the 31-bit integers it means compiling them @@ -93,8 +92,7 @@ val get_vm_compiling_info : retroknowledge -> entry -> Cbytecodes.comp_env -> CBytecodes.NotClosed if the term is not a closed constructor pattern (a constant for the compiler) *) val get_vm_constant_static_info : retroknowledge -> entry -> - constr array -> - Cbytecodes.structured_constant + constr array -> Cinstr.lambda (*Given an identifier id (usually Construct _ ) its argument array and a continuation, returns the compiled version @@ -102,16 +100,14 @@ val get_vm_constant_static_info : retroknowledge -> entry -> 31-bit integers, that would be the dynamic compilation into integers) or raises Not_found if id should be compiled as usual *) val get_vm_constant_dynamic_info : retroknowledge -> entry -> - Cbytecodes.comp_env -> - Cbytecodes.block array -> - int -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes + Cinstr.lambda array -> Cinstr.lambda (** Given a type identifier, this function is used before compiling a match over this type. In the case of 31-bit integers for instance, it is used to add the instruction sequence which would perform a dynamic decompilation in case the argument of the match is not in coq representation *) -val get_vm_before_match_info : retroknowledge -> entry -> Cbytecodes.bytecodes - -> Cbytecodes.bytecodes +val get_vm_before_match_info : retroknowledge -> entry -> Cinstr.lambda + -> Cinstr.lambda (** Given a type identifier, this function is used by pretyping/vnorm.ml to recover the elements of that type from their compiled form if it's non @@ -148,20 +144,18 @@ val find : retroknowledge -> field -> entry 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) + (bool -> Cinstr.lambda array -> Cinstr.lambda) option; vm_constant_static : (*fastcomputation flag -> constructor -> args -> result*) - (bool->constr array->Cbytecodes.structured_constant) + (bool -> constr array -> Cinstr.lambda) option; vm_constant_dynamic : (*fastcomputation flag -> constructor -> reloc -> args -> sz -> cont -> result *) - (bool->Cbytecodes.comp_env->Cbytecodes.block array->int-> - Cbytecodes.bytecodes->Cbytecodes.bytecodes) + (bool -> Cinstr.lambda array -> Cinstr.lambda) option; (* fastcomputation flag -> cont -> result *) - vm_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option; + vm_before_match : (bool -> Cinstr.lambda -> Cinstr.lambda) option; (* tag (= compiled int for instance) -> result *) vm_decompile_const : (int -> constr) option; |