diff options
Diffstat (limited to 'kernel/cbytegen.mli')
| -rw-r--r-- | kernel/cbytegen.mli | 45 |
1 files changed, 15 insertions, 30 deletions
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index c0f48641..abab58b6 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -1,42 +1,27 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + open Cbytecodes open Cemitcodes -open Term +open Constr 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 -> - env -> constant_universes option -> constant_def -> body_code option +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 -> 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 +val compile_alias : Names.Constant.t -> body_code |