diff options
| author | Pierre-Marie Pédrot | 2019-04-23 21:35:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-04-23 21:35:20 +0200 |
| commit | 75c5264aa687480c66a6765d64246b5ebd2c0d54 (patch) | |
| tree | 756baf747199c1f88c601c514887adabd9a05c5f /kernel/nativelambda.mli | |
| parent | 9834f23fe9bc8a659ed36c426d557e94179476b0 (diff) | |
| parent | 8b886a0a201444b7eb782f3fa0dc52a7b6fe8837 (diff) | |
Merge PR #9962: [native compiler] Encoding of constructors based on tags
Ack-by: maximedenes
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/nativelambda.mli')
| -rw-r--r-- | kernel/nativelambda.mli | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 687789e82b..446df1a1ea 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -33,9 +33,10 @@ type lambda = | 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 *) + | Lint of int (* a constant constructor *) + | 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 | Lsort of Sorts.t @@ -43,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 |