diff options
| author | Maxime Dénès | 2019-04-15 15:23:39 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-15 15:28:09 +0200 |
| commit | 8b886a0a201444b7eb782f3fa0dc52a7b6fe8837 (patch) | |
| tree | 19735dcfda794009b01c617438a34e3340463f23 /kernel/nativelambda.mli | |
| parent | 7205996bf25a542224c815b38f92da0ffef76b5d (diff) | |
[native compiler] Encoding of constructors based on tags
This serves two purposes:
1. It makes the native compiler use the same encoding and
lambda-representation as the bytecode compiler
2. It avoid relying on fragile invariants relating tags and constructor
indices. For example, previously, the mapping from indices to tags
had to be increasing.
Diffstat (limited to 'kernel/nativelambda.mli')
| -rw-r--r-- | kernel/nativelambda.mli | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 093665df9b..446df1a1ea 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -34,8 +34,8 @@ type lambda = | Lfix of (int array * (string * inductive) array * int) * fix_decl | Lcofix of int * fix_decl | Lint of int (* a constant constructor *) - | Lmakeblock of prefix * constructor * int * lambda array - (* prefix, constructor Name.t, constructor tag, arguments *) + | Lmakeblock of prefix * inductive * int * lambda array + (* prefix, inductive name, constructor tag, arguments *) (* A fully applied non-constant constructor *) | Luint of Uint63.t | Lval of Nativevalues.t @@ -44,7 +44,10 @@ type lambda = | Llazy | Lforce -and lam_branches = (constructor * Name.t Context.binder_annot array * lambda) array +and lam_branches = + { constant_branches : lambda array; + nonconstant_branches : (Name.t Context.binder_annot array * lambda) array; + } and fix_decl = Name.t Context.binder_annot array * lambda array * lambda array |