diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-04-06 12:41:26 -0400 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-04-09 01:05:48 -0400 |
| commit | aa3b8b7b24e809b379fcc86f2b21ae4380b211d5 (patch) | |
| tree | 254b9d84ee42798a513bcd5aea032a6e552b2067 /kernel/nativeinstr.mli | |
| parent | de61c7d77e49286622c4aebd56f2e87b0df93903 (diff) | |
Partial support for open terms in int31.
Diffstat (limited to 'kernel/nativeinstr.mli')
| -rw-r--r-- | kernel/nativeinstr.mli | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index 4e0291ed9..9c5add4df 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -12,7 +12,13 @@ open Nativevalues (** This file defines the lambda code for the native compiler. It has been extracted from Nativelambda.ml because of the retroknowledge architecture. *) -type lambda = +type prefix = string + +type uint = + | UintVal of Uint31.t + | UintDigits of prefix * constructor * lambda array + +and lambda = | Lrel of name * int | Lvar of identifier | Lmeta of metavariable * lambda (* type *) @@ -21,21 +27,21 @@ type lambda = | Llam of name array * lambda | Llet of name * lambda * lambda | Lapp of lambda * lambda array - | Lconst of string * constant (* prefix, constant name *) + | Lconst of prefix * constant | 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 + | Lmakeblock of prefix * constructor * int * lambda array (* prefix, constructor name, constructor tag, arguments *) (* A fully applied constructor *) - | Lconstruct of string * constructor (* prefix, constructor name *) + | Lconstruct of prefix * constructor (* A partially applied constructor *) - | Luint of Uint31.t + | Luint of uint | Lval of Nativevalues.t | Lsort of sorts - | Lind of string * inductive (* prefix, inductive name *) + | Lind of prefix * inductive | Llazy | Lforce |