From de61c7d77e49286622c4aebd56f2e87b0df93903 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sat, 5 Apr 2014 19:51:04 -0400 Subject: Had to split Nativelambda in two files because of Retroknowledge dependencies. --- kernel/nativelambda.mli | 32 +------------------------------- 1 file changed, 1 insertion(+), 31 deletions(-) (limited to 'kernel/nativelambda.mli') diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 751f11978..d4be2279d 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -9,40 +9,10 @@ open Names open Term open Pre_env open Nativevalues +open Nativeinstr (** This file defines the lambda code generation phase of the native compiler *) -type lambda = - | Lrel of name * int - | Lvar of identifier - | Lmeta of metavariable * lambda (* type *) - | Levar of existential * lambda (* type *) - | Lprod of lambda * lambda - | Llam of name array * lambda - | Llet of name * lambda * lambda - | Lapp of lambda * lambda array - | Lconst of string * constant (* prefix, constant name *) - | Lcase of annot_sw * lambda * lambda * lam_branches - (* annotations, term being matched, accu, branches *) - | Lif of lambda * lambda * lambda - | Lfix of (int array * int) * fix_decl - | Lcofix of int * fix_decl - | Lmakeblock of string * constructor * int * lambda array - (* prefix, constructor name, constructor tag, arguments *) - (* A fully applied constructor *) - | Lconstruct of string * constructor (* prefix, constructor name *) - (* A partially applied constructor *) - | Luint of Uint31.t - | Lval of Nativevalues.t - | Lsort of sorts - | Lind of string * inductive (* prefix, inductive name *) - | Llazy - | Lforce - -and lam_branches = (constructor * name array * lambda) array - -and fix_decl = name array * lambda array * lambda array - type evars = { evars_val : existential -> constr option; evars_typ : existential -> types; -- cgit v1.2.3