diff options
Diffstat (limited to 'kernel/nativelambda.mli')
| -rw-r--r-- | kernel/nativelambda.mli | 51 |
1 files changed, 38 insertions, 13 deletions
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 7b20258929..eb06522a33 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -10,9 +10,45 @@ open Names open Constr open Environ -open Nativeinstr +open Nativevalues (** This file defines the lambda code generation phase of the native compiler *) +type prefix = string + +type lambda = + | Lrel of Name.t * int + | Lvar of Id.t + | Lmeta of metavariable * lambda (* type *) + | Levar of Evar.t * lambda array (* arguments *) + | Lprod of lambda * lambda + | Llam of Name.t array * lambda + | Lrec of Name.t * lambda + | Llet of Name.t * lambda * lambda + | Lapp of lambda * lambda array + | Lconst of prefix * pconstant + | Lproj of prefix * inductive * int (* prefix, inductive, index starting from 0 *) + | Lprim of prefix * pconstant * CPrimitives.t * lambda array + | Lcase of annot_sw * lambda * lambda * lam_branches + (* annotations, term being matched, accu, branches *) + | Lif of lambda * lambda * lambda + | Lfix of (int array * (string * inductive) array * int) * fix_decl + | Lcofix of int * fix_decl + | Lmakeblock of prefix * pconstructor * int * lambda array + (* prefix, constructor Name.t, constructor tag, arguments *) + (* A fully applied constructor *) + | Lconstruct of prefix * pconstructor (* prefix, constructor Name.t *) + (* A partially applied constructor *) + | Luint of Uint63.t + | Lval of Nativevalues.t + | Lsort of Sorts.t + | Lind of prefix * pinductive + | Llazy + | Lforce + +and lam_branches = (constructor * Name.t array * lambda) array + +and fix_decl = Name.t array * lambda array * lambda array + type evars = { evars_val : existential -> constr option; evars_metas : metavariable -> types } @@ -22,7 +58,7 @@ val empty_evars : evars val decompose_Llam : lambda -> Name.t array * lambda val decompose_Llam_Llet : lambda -> (Name.t * lambda option) array * lambda -val is_lazy : env -> prefix -> constr -> bool +val is_lazy : constr -> bool val mk_lazy : lambda -> lambda val get_mind_prefix : env -> MutInd.t -> string @@ -30,14 +66,3 @@ val get_mind_prefix : env -> MutInd.t -> string val get_alias : env -> pconstant -> pconstant val lambda_of_constr : env -> evars -> Constr.constr -> lambda - -val compile_static_int31 : bool -> Constr.constr array -> lambda - -val compile_dynamic_int31 : bool -> prefix -> constructor -> lambda array -> - lambda - -val before_match_int31 : inductive -> bool -> prefix -> constructor -> lambda -> - lambda - -val compile_prim : CPrimitives.t -> Constant.t -> bool -> prefix -> lambda array -> - lambda |