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/cbytegen.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/cbytegen.mli')
| -rw-r--r-- | kernel/cbytegen.mli | 29 |
1 files changed, 2 insertions, 27 deletions
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index c117d3fb5..99f2a3c01 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -13,38 +13,13 @@ open Declarations open Pre_env (** Should only be used for monomorphic terms *) -val compile : bool -> (* Fail on error with a nice user message, otherwise simply a warning *) +val compile : fail_on_error:bool -> ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option (** init, fun, fv *) -val compile_constant_body : bool -> +val compile_constant_body : fail_on_error:bool -> env -> constant_universes -> constant_def -> body_code option (** Shortcut of the previous function used during module strengthening *) val compile_alias : Names.Constant.t -> body_code - -(** spiwack: this function contains the information needed to perform - the static compilation of int31 (trying and obtaining - a 31-bit integer in processor representation at compile time) *) -val compile_structured_int31 : bool -> constr array -> - structured_constant - -(** this function contains the information needed to perform - the dynamic compilation of int31 (trying and obtaining a - 31-bit integer in processor representation at runtime when - it failed at compile time *) -val dynamic_int31_compilation : bool -> comp_env -> - block array -> - int -> bytecodes -> bytecodes - -(*spiwack: template for the compilation n-ary operation, invariant: n>=1. - works as follow: checks if all the arguments are non-pointers - if they are applies the operation (second argument) if not - all of them are, returns to a coq definition (third argument) *) -val op_compilation : int -> instruction -> pconstant -> bool -> comp_env -> - constr array -> int -> bytecodes-> bytecodes - -(*spiwack: compiling function to insert dynamic decompilation before - matching integers (in case they are in processor representation) *) -val int31_escape_before_match : bool -> bytecodes -> bytecodes |