Skip to content

Commit 216e135

Browse files
committed
fix: apply the lean_apply_m over-application fix in script/apply.lean
`src/runtime/apply.cpp` is generated and carries a "DO NOT EDIT" header, so the fix has to live in `mkApplyM` in the generator. Regenerating now reproduces the committed `apply.cpp`. Also correct the generator path in the generated header, which still pointed at the long-gone `../../gen/apply.lean`.
1 parent df1b1f0 commit 216e135

2 files changed

Lines changed: 17 additions & 8 deletions

File tree

‎script/apply.lean‎

Lines changed: 16 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -132,12 +132,21 @@ if (arity == fixed + n) \{
132132
lean_dec_ref(f);
133133
return r;
134134
} else if (arity < fixed + n) \{
135-
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
136-
for (unsigned i = 0; i < fixed; i++) \{ lean_inc(fx(i)); args[i] = fx(i); }
137-
for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
138-
obj * new_f = FNN(f)(args);
139-
lean_dec_ref(f);
140-
return lean_apply_n(new_f, n+fixed-arity, &as[arity-fixed]);
135+
unsigned m = arity - fixed;
136+
obj * new_f;
137+
if (arity > LEAN_CLOSURE_MAX_ARGS) \{
138+
// `f`'s code takes its arguments as an array
139+
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
140+
for (unsigned i = 0; i < fixed; i++) \{ lean_inc(fx(i)); args[i] = fx(i); }
141+
for (unsigned i = 0; i < m; i++) args[fixed+i] = as[i];
142+
new_f = FNN(f)(args);
143+
lean_dec_ref(f);
144+
} else \{
145+
// `f`'s code takes `arity` separate arguments, so it must not be invoked through `FNN`;
146+
// `lean_apply_n` dispatches on `m` and consumes `f`.
147+
new_f = lean_apply_n(f, m, as);
148+
}
149+
return lean_apply_n(new_f, n - m, &as[m]);
141150
} else \{
142151
return fix_args(f, n, as);
143152
}
@@ -186,7 +195,7 @@ Author: Leonardo de Moura
186195
def mkApplyCpp (max : Nat) : M Unit := do
187196
mkCopyright
188197
emit "// DO NOT EDIT, this is an automatically generated file
189-
// Generated using script: ../../gen/apply.lean
198+
// Generated using script: script/apply.lean
190199
#include \"runtime/apply.h\"
191200
namespace lean {
192201
#define obj lean_object

‎src/runtime/apply.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
55
Author: Leonardo de Moura
66
*/
77
// DO NOT EDIT, this is an automatically generated file
8-
// Generated using script: ../../gen/apply.lean
8+
// Generated using script: script/apply.lean
99
#include "runtime/apply.h"
1010
namespace lean {
1111
#define obj lean_object

0 commit comments

Comments
 (0)