From 442bd1fe4007d2f3b46cb565abbcd64011db1af4 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 16 May 2018 00:36:08 +0200 Subject: 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. --- kernel/nativeinstr.mli | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'kernel/nativeinstr.mli') 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 -- cgit v1.2.3