diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-05-16 00:36:08 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-05-28 16:08:53 +0200 |
| commit | 442bd1fe4007d2f3b46cb565abbcd64011db1af4 (patch) | |
| tree | 083f5890a7a5763e884e24b1de45431573e87cae /kernel/nativeinstr.mli | |
| parent | 4552729b88058946055dddde1533057e25bfc5a9 (diff) | |
Fix #7333: vm_compute segfaults / Anomaly with cofix
We eta-expand cofixpoints when needed, so that their call-by-need
evaluation is correctly implemented by VM and native_compute.
Diffstat (limited to 'kernel/nativeinstr.mli')
| -rw-r--r-- | kernel/nativeinstr.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index 9c17cc2b5..c319be32d 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -37,7 +37,7 @@ and lambda = (* annotations, term being matched, accu, branches *) | Lif of lambda * lambda * lambda | Lfix of (int array * int) * fix_decl - | Lcofix of int * fix_decl + | Lcofix of int * fix_decl (* must be in eta-expanded form *) | Lmakeblock of prefix * pconstructor * int * lambda array (* prefix, constructor name, constructor tag, arguments *) (* A fully applied constructor *) @@ -50,6 +50,10 @@ and lambda = | Llazy | Lforce +(* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation +to be correct. Otherwise, memoization of previous evaluations will be applied +again to extra arguments (see #7333). *) + and lam_branches = (constructor * Name.t array * lambda) array and fix_decl = Name.t array * lambda array * lambda array |