diff options
| author | Maxime Dénès | 2018-02-24 09:33:03 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-24 09:33:03 +0100 |
| commit | bd41af496fd09d6ecd965190cad2873f1cd6b029 (patch) | |
| tree | 029c44d509cdaba200db07dfed61adb55b237f9e /kernel/cbytegen.mli | |
| parent | c4aeaa7aedb04bf156a4946b05bad8f66d5eec69 (diff) | |
| parent | 557c5a2938f16c0601f5a0323c66b78d2da01ee9 (diff) | |
Merge PR #6784: New IR in VM: Clambda
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 c117d3fb57..99f2a3c01a 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 |