max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: deallocation for closures in non default configurations (#11217)

Browse source 
This PR fixes fallout of the closure allocator changes in #10982. As far
as we know
this bug only meaningfully manifests in non default build configurations
without mimalloc such as:
`cmake --preset release -DUSE_MIMALLOC=OFF`

The issue is that I forgot to update the deallocation functions for
closures. However, this only
seems to matter if we disable mimalloc which is why this slipped through
testing.
This commit is contained in:
Henrik Böving 2025-11-17 17:27:20 +01:00 • committed by GitHub
parent 8eb0293098
commit 07e6b99e2e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
5 changed files with 155 additions and 140 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
script/apply.lean
View file

@ -60,7 +60,7 @@ if (arity == fixed + {n}) \{
for j in [n:max + 1] do for j in [n:max + 1] do
let fs := mkFsArgs (j - n) let fs := mkFsArgs (j - n)
let sep := if j = n then "" else ", " let sep := if j = n then "" else ", "
emit s!" case {j}: \{ obj* r = FN{j}(f)({fs}{sep}{args}); lean_free_small_object(f); return r; }\n" emit s!" case {j}: \{ obj* r = FN{j}(f)({fs}{sep}{args}); lean_free_object(f); return r; }\n"
emit " } emit " }
} }
switch (arity) {\n" switch (arity) {\n"
@ -162,7 +162,7 @@ static obj* fix_args(obj* f, unsigned n, obj*const* as) {
for (unsigned i = 0; i < fixed; i++, source++, target++) { for (unsigned i = 0; i < fixed; i++, source++, target++) {
*target = *source; *target = *source;
} }
lean_free_small_object(f); lean_free_object(f);
} }
for (unsigned i = 0; i < n; i++, as++, target++) { for (unsigned i = 0; i < n; i++, as++, target++) {
*target = *as; *target = *as;

8
src/include/lean/lean.h
View file

@ -730,6 +730,14 @@ static inline void lean_closure_set(u_lean_obj_arg o, unsigned i, lean_obj_arg a
assert(i < lean_closure_num_fixed(o)); assert(i < lean_closure_num_fixed(o));
lean_to_closure(o)->m_objs[i] = a; lean_to_closure(o)->m_objs[i] = a;
} }
static inline size_t lean_closure_byte_size(lean_object * o) {
return sizeof(lean_closure_object) + sizeof(void*)*lean_closure_num_fixed(o);
}
static inline size_t lean_closure_data_byte_size(lean_object * o) {
// Matches for closures.
return lean_closure_byte_size(o);
}
LEAN_EXPORT lean_object* lean_apply_1(lean_object* f, lean_object* a1); LEAN_EXPORT lean_object* lean_apply_1(lean_object* f, lean_object* a1);
LEAN_EXPORT lean_object* lean_apply_2(lean_object* f, lean_object* a1, lean_object* a2); LEAN_EXPORT lean_object* lean_apply_2(lean_object* f, lean_object* a1, lean_object* a2);

274
src/runtime/apply.cpp
View file

@ -29,7 +29,7 @@ static obj* fix_args(obj* f, unsigned n, obj*const* as) {
for (unsigned i = 0; i < fixed; i++, source++, target++) { for (unsigned i = 0; i < fixed; i++, source++, target++) {
*target = *source; *target = *source;
} }
lean_free_small_object(f); lean_free_object(f);
} }
for (unsigned i = 0; i < n; i++, as++, target++) { for (unsigned i = 0; i < n; i++, as++, target++) {
*target = *as; *target = *as;
@ -105,22 +105,22 @@ unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 1) { if (arity == fixed + 1) {
if (lean_is_exclusive(f)) { if (lean_is_exclusive(f)) {
switch (arity) { switch (arity) {
case 1: { obj* r = FN1(f)(a1); lean_free_small_object(f); return r; } case 1: { obj* r = FN1(f)(a1); lean_free_object(f); return r; }
case 2: { obj* r = FN2(f)(fx(0), a1); lean_free_small_object(f); return r; } case 2: { obj* r = FN2(f)(fx(0), a1); lean_free_object(f); return r; }
case 3: { obj* r = FN3(f)(fx(0), fx(1), a1); lean_free_small_object(f); return r; } case 3: { obj* r = FN3(f)(fx(0), fx(1), a1); lean_free_object(f); return r; }
case 4: { obj* r = FN4(f)(fx(0), fx(1), fx(2), a1); lean_free_small_object(f); return r; } case 4: { obj* r = FN4(f)(fx(0), fx(1), fx(2), a1); lean_free_object(f); return r; }
case 5: { obj* r = FN5(f)(fx(0), fx(1), fx(2), fx(3), a1); lean_free_small_object(f); return r; } case 5: { obj* r = FN5(f)(fx(0), fx(1), fx(2), fx(3), a1); lean_free_object(f); return r; }
case 6: { obj* r = FN6(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1); lean_free_small_object(f); return r; } case 6: { obj* r = FN6(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1); lean_free_object(f); return r; }
case 7: { obj* r = FN7(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), a1); lean_free_small_object(f); return r; } case 7: { obj* r = FN7(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), a1); lean_free_object(f); return r; }
case 8: { obj* r = FN8(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), a1); lean_free_small_object(f); return r; } case 8: { obj* r = FN8(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), a1); lean_free_object(f); return r; }
case 9: { obj* r = FN9(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), a1); lean_free_small_object(f); return r; } case 9: { obj* r = FN9(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), a1); lean_free_object(f); return r; }
case 10: { obj* r = FN10(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), a1); lean_free_small_object(f); return r; } case 10: { obj* r = FN10(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), a1); lean_free_object(f); return r; }
case 11: { obj* r = FN11(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), a1); lean_free_small_object(f); return r; } case 11: { obj* r = FN11(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), a1); lean_free_object(f); return r; }
case 12: { obj* r = FN12(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), a1); lean_free_small_object(f); return r; } case 12: { obj* r = FN12(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), a1); lean_free_object(f); return r; }
case 13: { obj* r = FN13(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), fx(11), a1); lean_free_small_object(f); return r; } case 13: { obj* r = FN13(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), fx(11), a1); lean_free_object(f); return r; }
case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), fx(11), fx(12), a1); lean_free_small_object(f); return r; } case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), fx(11), fx(12), a1); lean_free_object(f); return r; }
case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), fx(11), fx(12), fx(13), a1); lean_free_small_object(f); return r; } case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), fx(11), fx(12), fx(13), a1); lean_free_object(f); return r; }
case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), fx(11), fx(12), fx(13), fx(14), a1); lean_free_small_object(f); return r; } case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), fx(11), fx(12), fx(13), fx(14), a1); lean_free_object(f); return r; }
} }
} }
switch (arity) { switch (arity) {
@ -164,21 +164,21 @@ unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 2) { if (arity == fixed + 2) {
if (lean_is_exclusive(f)) { if (lean_is_exclusive(f)) {
switch (arity) { switch (arity) {
case 2: { obj* r = FN2(f)(a1, a2); lean_free_small_object(f); return r; } case 2: { obj* r = FN2(f)(a1, a2); lean_free_object(f); return r; }
case 3: { obj* r = FN3(f)(fx(0), a1, a2); lean_free_small_object(f); return r; } case 3: { obj* r = FN3(f)(fx(0), a1, a2); lean_free_object(f); return r; }
case 4: { obj* r = FN4(f)(fx(0), fx(1), a1, a2); lean_free_small_object(f); return r; } case 4: { obj* r = FN4(f)(fx(0), fx(1), a1, a2); lean_free_object(f); return r; }
case 5: { obj* r = FN5(f)(fx(0), fx(1), fx(2), a1, a2); lean_free_small_object(f); return r; } case 5: { obj* r = FN5(f)(fx(0), fx(1), fx(2), a1, a2); lean_free_object(f); return r; }
case 6: { obj* r = FN6(f)(fx(0), fx(1), fx(2), fx(3), a1, a2); lean_free_small_object(f); return r; } case 6: { obj* r = FN6(f)(fx(0), fx(1), fx(2), fx(3), a1, a2); lean_free_object(f); return r; }
case 7: { obj* r = FN7(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1, a2); lean_free_small_object(f); return r; } case 7: { obj* r = FN7(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1, a2); lean_free_object(f); return r; }
case 8: { obj* r = FN8(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), a1, a2); lean_free_small_object(f); return r; } case 8: { obj* r = FN8(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), a1, a2); lean_free_object(f); return r; }
case 9: { obj* r = FN9(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), a1, a2); lean_free_small_object(f); return r; } case 9: { obj* r = FN9(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), a1, a2); lean_free_object(f); return r; }
case 10: { obj* r = FN10(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), a1, a2); lean_free_small_object(f); return r; } case 10: { obj* r = FN10(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), a1, a2); lean_free_object(f); return r; }
case 11: { obj* r = FN11(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), a1, a2); lean_free_small_object(f); return r; } case 11: { obj* r = FN11(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), a1, a2); lean_free_object(f); return r; }
case 12: { obj* r = FN12(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), a1, a2); lean_free_small_object(f); return r; } case 12: { obj* r = FN12(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), a1, a2); lean_free_object(f); return r; }
case 13: { obj* r = FN13(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), a1, a2); lean_free_small_object(f); return r; } case 13: { obj* r = FN13(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), a1, a2); lean_free_object(f); return r; }
case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), fx(11), a1, a2); lean_free_small_object(f); return r; } case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), fx(11), a1, a2); lean_free_object(f); return r; }
case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), fx(11), fx(12), a1, a2); lean_free_small_object(f); return r; } case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), fx(11), fx(12), a1, a2); lean_free_object(f); return r; }
case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), fx(11), fx(12), fx(13), a1, a2); lean_free_small_object(f); return r; } case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), fx(11), fx(12), fx(13), a1, a2); lean_free_object(f); return r; }
} }
} }
switch (arity) { switch (arity) {
@ -226,20 +226,20 @@ unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 3) { if (arity == fixed + 3) {
if (lean_is_exclusive(f)) { if (lean_is_exclusive(f)) {
switch (arity) { switch (arity) {
case 3: { obj* r = FN3(f)(a1, a2, a3); lean_free_small_object(f); return r; } case 3: { obj* r = FN3(f)(a1, a2, a3); lean_free_object(f); return r; }
case 4: { obj* r = FN4(f)(fx(0), a1, a2, a3); lean_free_small_object(f); return r; } case 4: { obj* r = FN4(f)(fx(0), a1, a2, a3); lean_free_object(f); return r; }
case 5: { obj* r = FN5(f)(fx(0), fx(1), a1, a2, a3); lean_free_small_object(f); return r; } case 5: { obj* r = FN5(f)(fx(0), fx(1), a1, a2, a3); lean_free_object(f); return r; }
case 6: { obj* r = FN6(f)(fx(0), fx(1), fx(2), a1, a2, a3); lean_free_small_object(f); return r; } case 6: { obj* r = FN6(f)(fx(0), fx(1), fx(2), a1, a2, a3); lean_free_object(f); return r; }
case 7: { obj* r = FN7(f)(fx(0), fx(1), fx(2), fx(3), a1, a2, a3); lean_free_small_object(f); return r; } case 7: { obj* r = FN7(f)(fx(0), fx(1), fx(2), fx(3), a1, a2, a3); lean_free_object(f); return r; }
case 8: { obj* r = FN8(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1, a2, a3); lean_free_small_object(f); return r; } case 8: { obj* r = FN8(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1, a2, a3); lean_free_object(f); return r; }
case 9: { obj* r = FN9(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), a1, a2, a3); lean_free_small_object(f); return r; } case 9: { obj* r = FN9(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), a1, a2, a3); lean_free_object(f); return r; }
case 10: { obj* r = FN10(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), a1, a2, a3); lean_free_small_object(f); return r; } case 10: { obj* r = FN10(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), a1, a2, a3); lean_free_object(f); return r; }
case 11: { obj* r = FN11(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), a1, a2, a3); lean_free_small_object(f); return r; } case 11: { obj* r = FN11(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), a1, a2, a3); lean_free_object(f); return r; }
case 12: { obj* r = FN12(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), a1, a2, a3); lean_free_small_object(f); return r; } case 12: { obj* r = FN12(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), a1, a2, a3); lean_free_object(f); return r; }
case 13: { obj* r = FN13(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), a1, a2, a3); lean_free_small_object(f); return r; } case 13: { obj* r = FN13(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), a1, a2, a3); lean_free_object(f); return r; }
case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), a1, a2, a3); lean_free_small_object(f); return r; } case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), a1, a2, a3); lean_free_object(f); return r; }
case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), fx(11), a1, a2, a3); lean_free_small_object(f); return r; } case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), fx(11), a1, a2, a3); lean_free_object(f); return r; }
case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), fx(11), fx(12), a1, a2, a3); lean_free_small_object(f); return r; } case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), fx(11), fx(12), a1, a2, a3); lean_free_object(f); return r; }
} }
} }
switch (arity) { switch (arity) {
@ -286,19 +286,19 @@ unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 4) { if (arity == fixed + 4) {
if (lean_is_exclusive(f)) { if (lean_is_exclusive(f)) {
switch (arity) { switch (arity) {
case 4: { obj* r = FN4(f)(a1, a2, a3, a4); lean_free_small_object(f); return r; } case 4: { obj* r = FN4(f)(a1, a2, a3, a4); lean_free_object(f); return r; }
case 5: { obj* r = FN5(f)(fx(0), a1, a2, a3, a4); lean_free_small_object(f); return r; } case 5: { obj* r = FN5(f)(fx(0), a1, a2, a3, a4); lean_free_object(f); return r; }
case 6: { obj* r = FN6(f)(fx(0), fx(1), a1, a2, a3, a4); lean_free_small_object(f); return r; } case 6: { obj* r = FN6(f)(fx(0), fx(1), a1, a2, a3, a4); lean_free_object(f); return r; }
case 7: { obj* r = FN7(f)(fx(0), fx(1), fx(2), a1, a2, a3, a4); lean_free_small_object(f); return r; } case 7: { obj* r = FN7(f)(fx(0), fx(1), fx(2), a1, a2, a3, a4); lean_free_object(f); return r; }
case 8: { obj* r = FN8(f)(fx(0), fx(1), fx(2), fx(3), a1, a2, a3, a4); lean_free_small_object(f); return r; } case 8: { obj* r = FN8(f)(fx(0), fx(1), fx(2), fx(3), a1, a2, a3, a4); lean_free_object(f); return r; }
case 9: { obj* r = FN9(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1, a2, a3, a4); lean_free_small_object(f); return r; } case 9: { obj* r = FN9(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1, a2, a3, a4); lean_free_object(f); return r; }
case 10: { obj* r = FN10(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), a1, a2, a3, a4); lean_free_small_object(f); return r; } case 10: { obj* r = FN10(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), a1, a2, a3, a4); lean_free_object(f); return r; }
case 11: { obj* r = FN11(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), a1, a2, a3, a4); lean_free_small_object(f); return r; } case 11: { obj* r = FN11(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), a1, a2, a3, a4); lean_free_object(f); return r; }
case 12: { obj* r = FN12(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), a1, a2, a3, a4); lean_free_small_object(f); return r; } case 12: { obj* r = FN12(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), a1, a2, a3, a4); lean_free_object(f); return r; }
case 13: { obj* r = FN13(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), a1, a2, a3, a4); lean_free_small_object(f); return r; } case 13: { obj* r = FN13(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), a1, a2, a3, a4); lean_free_object(f); return r; }
case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), a1, a2, a3, a4); lean_free_small_object(f); return r; } case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), a1, a2, a3, a4); lean_free_object(f); return r; }
case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), a1, a2, a3, a4); lean_free_small_object(f); return r; } case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), a1, a2, a3, a4); lean_free_object(f); return r; }
case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), fx(11), a1, a2, a3, a4); lean_free_small_object(f); return r; } case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), fx(11), a1, a2, a3, a4); lean_free_object(f); return r; }
} }
} }
switch (arity) { switch (arity) {
@ -344,18 +344,18 @@ unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 5) { if (arity == fixed + 5) {
if (lean_is_exclusive(f)) { if (lean_is_exclusive(f)) {
switch (arity) { switch (arity) {
case 5: { obj* r = FN5(f)(a1, a2, a3, a4, a5); lean_free_small_object(f); return r; } case 5: { obj* r = FN5(f)(a1, a2, a3, a4, a5); lean_free_object(f); return r; }
case 6: { obj* r = FN6(f)(fx(0), a1, a2, a3, a4, a5); lean_free_small_object(f); return r; } case 6: { obj* r = FN6(f)(fx(0), a1, a2, a3, a4, a5); lean_free_object(f); return r; }
case 7: { obj* r = FN7(f)(fx(0), fx(1), a1, a2, a3, a4, a5); lean_free_small_object(f); return r; } case 7: { obj* r = FN7(f)(fx(0), fx(1), a1, a2, a3, a4, a5); lean_free_object(f); return r; }
case 8: { obj* r = FN8(f)(fx(0), fx(1), fx(2), a1, a2, a3, a4, a5); lean_free_small_object(f); return r; } case 8: { obj* r = FN8(f)(fx(0), fx(1), fx(2), a1, a2, a3, a4, a5); lean_free_object(f); return r; }
case 9: { obj* r = FN9(f)(fx(0), fx(1), fx(2), fx(3), a1, a2, a3, a4, a5); lean_free_small_object(f); return r; } case 9: { obj* r = FN9(f)(fx(0), fx(1), fx(2), fx(3), a1, a2, a3, a4, a5); lean_free_object(f); return r; }
case 10: { obj* r = FN10(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1, a2, a3, a4, a5); lean_free_small_object(f); return r; } case 10: { obj* r = FN10(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1, a2, a3, a4, a5); lean_free_object(f); return r; }
case 11: { obj* r = FN11(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), a1, a2, a3, a4, a5); lean_free_small_object(f); return r; } case 11: { obj* r = FN11(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), a1, a2, a3, a4, a5); lean_free_object(f); return r; }
case 12: { obj* r = FN12(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), a1, a2, a3, a4, a5); lean_free_small_object(f); return r; } case 12: { obj* r = FN12(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), a1, a2, a3, a4, a5); lean_free_object(f); return r; }
case 13: { obj* r = FN13(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), a1, a2, a3, a4, a5); lean_free_small_object(f); return r; } case 13: { obj* r = FN13(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), a1, a2, a3, a4, a5); lean_free_object(f); return r; }
case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), a1, a2, a3, a4, a5); lean_free_small_object(f); return r; } case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), a1, a2, a3, a4, a5); lean_free_object(f); return r; }
case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), a1, a2, a3, a4, a5); lean_free_small_object(f); return r; } case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), a1, a2, a3, a4, a5); lean_free_object(f); return r; }
case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), a1, a2, a3, a4, a5); lean_free_small_object(f); return r; } case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), fx(10), a1, a2, a3, a4, a5); lean_free_object(f); return r; }
} }
} }
switch (arity) { switch (arity) {
@ -400,17 +400,17 @@ unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 6) { if (arity == fixed + 6) {
if (lean_is_exclusive(f)) { if (lean_is_exclusive(f)) {
switch (arity) { switch (arity) {
case 6: { obj* r = FN6(f)(a1, a2, a3, a4, a5, a6); lean_free_small_object(f); return r; } case 6: { obj* r = FN6(f)(a1, a2, a3, a4, a5, a6); lean_free_object(f); return r; }
case 7: { obj* r = FN7(f)(fx(0), a1, a2, a3, a4, a5, a6); lean_free_small_object(f); return r; } case 7: { obj* r = FN7(f)(fx(0), a1, a2, a3, a4, a5, a6); lean_free_object(f); return r; }
case 8: { obj* r = FN8(f)(fx(0), fx(1), a1, a2, a3, a4, a5, a6); lean_free_small_object(f); return r; } case 8: { obj* r = FN8(f)(fx(0), fx(1), a1, a2, a3, a4, a5, a6); lean_free_object(f); return r; }
case 9: { obj* r = FN9(f)(fx(0), fx(1), fx(2), a1, a2, a3, a4, a5, a6); lean_free_small_object(f); return r; } case 9: { obj* r = FN9(f)(fx(0), fx(1), fx(2), a1, a2, a3, a4, a5, a6); lean_free_object(f); return r; }
case 10: { obj* r = FN10(f)(fx(0), fx(1), fx(2), fx(3), a1, a2, a3, a4, a5, a6); lean_free_small_object(f); return r; } case 10: { obj* r = FN10(f)(fx(0), fx(1), fx(2), fx(3), a1, a2, a3, a4, a5, a6); lean_free_object(f); return r; }
case 11: { obj* r = FN11(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1, a2, a3, a4, a5, a6); lean_free_small_object(f); return r; } case 11: { obj* r = FN11(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1, a2, a3, a4, a5, a6); lean_free_object(f); return r; }
case 12: { obj* r = FN12(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), a1, a2, a3, a4, a5, a6); lean_free_small_object(f); return r; } case 12: { obj* r = FN12(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), a1, a2, a3, a4, a5, a6); lean_free_object(f); return r; }
case 13: { obj* r = FN13(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), a1, a2, a3, a4, a5, a6); lean_free_small_object(f); return r; } case 13: { obj* r = FN13(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), a1, a2, a3, a4, a5, a6); lean_free_object(f); return r; }
case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), a1, a2, a3, a4, a5, a6); lean_free_small_object(f); return r; } case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), a1, a2, a3, a4, a5, a6); lean_free_object(f); return r; }
case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), a1, a2, a3, a4, a5, a6); lean_free_small_object(f); return r; } case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), a1, a2, a3, a4, a5, a6); lean_free_object(f); return r; }
case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), a1, a2, a3, a4, a5, a6); lean_free_small_object(f); return r; } case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), fx(9), a1, a2, a3, a4, a5, a6); lean_free_object(f); return r; }
} }
} }
switch (arity) { switch (arity) {
@ -454,16 +454,16 @@ unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 7) { if (arity == fixed + 7) {
if (lean_is_exclusive(f)) { if (lean_is_exclusive(f)) {
switch (arity) { switch (arity) {
case 7: { obj* r = FN7(f)(a1, a2, a3, a4, a5, a6, a7); lean_free_small_object(f); return r; } case 7: { obj* r = FN7(f)(a1, a2, a3, a4, a5, a6, a7); lean_free_object(f); return r; }
case 8: { obj* r = FN8(f)(fx(0), a1, a2, a3, a4, a5, a6, a7); lean_free_small_object(f); return r; } case 8: { obj* r = FN8(f)(fx(0), a1, a2, a3, a4, a5, a6, a7); lean_free_object(f); return r; }
case 9: { obj* r = FN9(f)(fx(0), fx(1), a1, a2, a3, a4, a5, a6, a7); lean_free_small_object(f); return r; } case 9: { obj* r = FN9(f)(fx(0), fx(1), a1, a2, a3, a4, a5, a6, a7); lean_free_object(f); return r; }
case 10: { obj* r = FN10(f)(fx(0), fx(1), fx(2), a1, a2, a3, a4, a5, a6, a7); lean_free_small_object(f); return r; } case 10: { obj* r = FN10(f)(fx(0), fx(1), fx(2), a1, a2, a3, a4, a5, a6, a7); lean_free_object(f); return r; }
case 11: { obj* r = FN11(f)(fx(0), fx(1), fx(2), fx(3), a1, a2, a3, a4, a5, a6, a7); lean_free_small_object(f); return r; } case 11: { obj* r = FN11(f)(fx(0), fx(1), fx(2), fx(3), a1, a2, a3, a4, a5, a6, a7); lean_free_object(f); return r; }
case 12: { obj* r = FN12(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1, a2, a3, a4, a5, a6, a7); lean_free_small_object(f); return r; } case 12: { obj* r = FN12(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1, a2, a3, a4, a5, a6, a7); lean_free_object(f); return r; }
case 13: { obj* r = FN13(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), a1, a2, a3, a4, a5, a6, a7); lean_free_small_object(f); return r; } case 13: { obj* r = FN13(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), a1, a2, a3, a4, a5, a6, a7); lean_free_object(f); return r; }
case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), a1, a2, a3, a4, a5, a6, a7); lean_free_small_object(f); return r; } case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), a1, a2, a3, a4, a5, a6, a7); lean_free_object(f); return r; }
case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), a1, a2, a3, a4, a5, a6, a7); lean_free_small_object(f); return r; } case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), a1, a2, a3, a4, a5, a6, a7); lean_free_object(f); return r; }
case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), a1, a2, a3, a4, a5, a6, a7); lean_free_small_object(f); return r; } case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), fx(8), a1, a2, a3, a4, a5, a6, a7); lean_free_object(f); return r; }
} }
} }
switch (arity) { switch (arity) {
@ -506,15 +506,15 @@ unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 8) { if (arity == fixed + 8) {
if (lean_is_exclusive(f)) { if (lean_is_exclusive(f)) {
switch (arity) { switch (arity) {
case 8: { obj* r = FN8(f)(a1, a2, a3, a4, a5, a6, a7, a8); lean_free_small_object(f); return r; } case 8: { obj* r = FN8(f)(a1, a2, a3, a4, a5, a6, a7, a8); lean_free_object(f); return r; }
case 9: { obj* r = FN9(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8); lean_free_small_object(f); return r; } case 9: { obj* r = FN9(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8); lean_free_object(f); return r; }
case 10: { obj* r = FN10(f)(fx(0), fx(1), a1, a2, a3, a4, a5, a6, a7, a8); lean_free_small_object(f); return r; } case 10: { obj* r = FN10(f)(fx(0), fx(1), a1, a2, a3, a4, a5, a6, a7, a8); lean_free_object(f); return r; }
case 11: { obj* r = FN11(f)(fx(0), fx(1), fx(2), a1, a2, a3, a4, a5, a6, a7, a8); lean_free_small_object(f); return r; } case 11: { obj* r = FN11(f)(fx(0), fx(1), fx(2), a1, a2, a3, a4, a5, a6, a7, a8); lean_free_object(f); return r; }
case 12: { obj* r = FN12(f)(fx(0), fx(1), fx(2), fx(3), a1, a2, a3, a4, a5, a6, a7, a8); lean_free_small_object(f); return r; } case 12: { obj* r = FN12(f)(fx(0), fx(1), fx(2), fx(3), a1, a2, a3, a4, a5, a6, a7, a8); lean_free_object(f); return r; }
case 13: { obj* r = FN13(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1, a2, a3, a4, a5, a6, a7, a8); lean_free_small_object(f); return r; } case 13: { obj* r = FN13(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1, a2, a3, a4, a5, a6, a7, a8); lean_free_object(f); return r; }
case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), a1, a2, a3, a4, a5, a6, a7, a8); lean_free_small_object(f); return r; } case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), a1, a2, a3, a4, a5, a6, a7, a8); lean_free_object(f); return r; }
case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), a1, a2, a3, a4, a5, a6, a7, a8); lean_free_small_object(f); return r; } case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), a1, a2, a3, a4, a5, a6, a7, a8); lean_free_object(f); return r; }
case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), a1, a2, a3, a4, a5, a6, a7, a8); lean_free_small_object(f); return r; } case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), fx(7), a1, a2, a3, a4, a5, a6, a7, a8); lean_free_object(f); return r; }
} }
} }
switch (arity) { switch (arity) {
@ -556,14 +556,14 @@ unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 9) { if (arity == fixed + 9) {
if (lean_is_exclusive(f)) { if (lean_is_exclusive(f)) {
switch (arity) { switch (arity) {
case 9: { obj* r = FN9(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9); lean_free_small_object(f); return r; } case 9: { obj* r = FN9(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9); lean_free_object(f); return r; }
case 10: { obj* r = FN10(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9); lean_free_small_object(f); return r; } case 10: { obj* r = FN10(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9); lean_free_object(f); return r; }
case 11: { obj* r = FN11(f)(fx(0), fx(1), a1, a2, a3, a4, a5, a6, a7, a8, a9); lean_free_small_object(f); return r; } case 11: { obj* r = FN11(f)(fx(0), fx(1), a1, a2, a3, a4, a5, a6, a7, a8, a9); lean_free_object(f); return r; }
case 12: { obj* r = FN12(f)(fx(0), fx(1), fx(2), a1, a2, a3, a4, a5, a6, a7, a8, a9); lean_free_small_object(f); return r; } case 12: { obj* r = FN12(f)(fx(0), fx(1), fx(2), a1, a2, a3, a4, a5, a6, a7, a8, a9); lean_free_object(f); return r; }
case 13: { obj* r = FN13(f)(fx(0), fx(1), fx(2), fx(3), a1, a2, a3, a4, a5, a6, a7, a8, a9); lean_free_small_object(f); return r; } case 13: { obj* r = FN13(f)(fx(0), fx(1), fx(2), fx(3), a1, a2, a3, a4, a5, a6, a7, a8, a9); lean_free_object(f); return r; }
case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1, a2, a3, a4, a5, a6, a7, a8, a9); lean_free_small_object(f); return r; } case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1, a2, a3, a4, a5, a6, a7, a8, a9); lean_free_object(f); return r; }
case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), a1, a2, a3, a4, a5, a6, a7, a8, a9); lean_free_small_object(f); return r; } case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), a1, a2, a3, a4, a5, a6, a7, a8, a9); lean_free_object(f); return r; }
case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), a1, a2, a3, a4, a5, a6, a7, a8, a9); lean_free_small_object(f); return r; } case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), fx(6), a1, a2, a3, a4, a5, a6, a7, a8, a9); lean_free_object(f); return r; }
} }
} }
switch (arity) { switch (arity) {
@ -604,13 +604,13 @@ unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 10) { if (arity == fixed + 10) {
if (lean_is_exclusive(f)) { if (lean_is_exclusive(f)) {
switch (arity) { switch (arity) {
case 10: { obj* r = FN10(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10); lean_free_small_object(f); return r; } case 10: { obj* r = FN10(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10); lean_free_object(f); return r; }
case 11: { obj* r = FN11(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10); lean_free_small_object(f); return r; } case 11: { obj* r = FN11(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10); lean_free_object(f); return r; }
case 12: { obj* r = FN12(f)(fx(0), fx(1), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10); lean_free_small_object(f); return r; } case 12: { obj* r = FN12(f)(fx(0), fx(1), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10); lean_free_object(f); return r; }
case 13: { obj* r = FN13(f)(fx(0), fx(1), fx(2), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10); lean_free_small_object(f); return r; } case 13: { obj* r = FN13(f)(fx(0), fx(1), fx(2), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10); lean_free_object(f); return r; }
case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), fx(3), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10); lean_free_small_object(f); return r; } case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), fx(3), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10); lean_free_object(f); return r; }
case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10); lean_free_small_object(f); return r; } case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10); lean_free_object(f); return r; }
case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10); lean_free_small_object(f); return r; } case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), fx(5), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10); lean_free_object(f); return r; }
} }
} }
switch (arity) { switch (arity) {
@ -650,12 +650,12 @@ unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 11) { if (arity == fixed + 11) {
if (lean_is_exclusive(f)) { if (lean_is_exclusive(f)) {
switch (arity) { switch (arity) {
case 11: { obj* r = FN11(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11); lean_free_small_object(f); return r; } case 11: { obj* r = FN11(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11); lean_free_object(f); return r; }
case 12: { obj* r = FN12(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11); lean_free_small_object(f); return r; } case 12: { obj* r = FN12(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11); lean_free_object(f); return r; }
case 13: { obj* r = FN13(f)(fx(0), fx(1), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11); lean_free_small_object(f); return r; } case 13: { obj* r = FN13(f)(fx(0), fx(1), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11); lean_free_object(f); return r; }
case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11); lean_free_small_object(f); return r; } case 14: { obj* r = FN14(f)(fx(0), fx(1), fx(2), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11); lean_free_object(f); return r; }
case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11); lean_free_small_object(f); return r; } case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), fx(3), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11); lean_free_object(f); return r; }
case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11); lean_free_small_object(f); return r; } case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), fx(4), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11); lean_free_object(f); return r; }
} }
} }
switch (arity) { switch (arity) {
@ -694,11 +694,11 @@ unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 12) { if (arity == fixed + 12) {
if (lean_is_exclusive(f)) { if (lean_is_exclusive(f)) {
switch (arity) { switch (arity) {
case 12: { obj* r = FN12(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12); lean_free_small_object(f); return r; } case 12: { obj* r = FN12(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12); lean_free_object(f); return r; }
case 13: { obj* r = FN13(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12); lean_free_small_object(f); return r; } case 13: { obj* r = FN13(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12); lean_free_object(f); return r; }
case 14: { obj* r = FN14(f)(fx(0), fx(1), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12); lean_free_small_object(f); return r; } case 14: { obj* r = FN14(f)(fx(0), fx(1), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12); lean_free_object(f); return r; }
case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12); lean_free_small_object(f); return r; } case 15: { obj* r = FN15(f)(fx(0), fx(1), fx(2), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12); lean_free_object(f); return r; }
case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12); lean_free_small_object(f); return r; } case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), fx(3), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12); lean_free_object(f); return r; }
} }
} }
switch (arity) { switch (arity) {
@ -736,10 +736,10 @@ unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 13) { if (arity == fixed + 13) {
if (lean_is_exclusive(f)) { if (lean_is_exclusive(f)) {
switch (arity) { switch (arity) {
case 13: { obj* r = FN13(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13); lean_free_small_object(f); return r; } case 13: { obj* r = FN13(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13); lean_free_object(f); return r; }
case 14: { obj* r = FN14(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13); lean_free_small_object(f); return r; } case 14: { obj* r = FN14(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13); lean_free_object(f); return r; }
case 15: { obj* r = FN15(f)(fx(0), fx(1), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13); lean_free_small_object(f); return r; } case 15: { obj* r = FN15(f)(fx(0), fx(1), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13); lean_free_object(f); return r; }
case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13); lean_free_small_object(f); return r; } case 16: { obj* r = FN16(f)(fx(0), fx(1), fx(2), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13); lean_free_object(f); return r; }
} }
} }
switch (arity) { switch (arity) {
@ -776,9 +776,9 @@ unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 14) { if (arity == fixed + 14) {
if (lean_is_exclusive(f)) { if (lean_is_exclusive(f)) {
switch (arity) { switch (arity) {
case 14: { obj* r = FN14(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14); lean_free_small_object(f); return r; } case 14: { obj* r = FN14(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14); lean_free_object(f); return r; }
case 15: { obj* r = FN15(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14); lean_free_small_object(f); return r; } case 15: { obj* r = FN15(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14); lean_free_object(f); return r; }
case 16: { obj* r = FN16(f)(fx(0), fx(1), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14); lean_free_small_object(f); return r; } case 16: { obj* r = FN16(f)(fx(0), fx(1), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14); lean_free_object(f); return r; }
} }
} }
switch (arity) { switch (arity) {
@ -814,8 +814,8 @@ unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 15) { if (arity == fixed + 15) {
if (lean_is_exclusive(f)) { if (lean_is_exclusive(f)) {
switch (arity) { switch (arity) {
case 15: { obj* r = FN15(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15); lean_free_small_object(f); return r; } case 15: { obj* r = FN15(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15); lean_free_object(f); return r; }
case 16: { obj* r = FN16(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15); lean_free_small_object(f); return r; } case 16: { obj* r = FN16(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15); lean_free_object(f); return r; }
} }
} }
switch (arity) { switch (arity) {
@ -850,7 +850,7 @@ unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 16) { if (arity == fixed + 16) {
if (lean_is_exclusive(f)) { if (lean_is_exclusive(f)) {
switch (arity) { switch (arity) {
case 16: { obj* r = FN16(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16); lean_free_small_object(f); return r; } case 16: { obj* r = FN16(f)(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16); lean_free_object(f); return r; }
} }
} }
switch (arity) { switch (arity) {

7
src/runtime/object.cpp
View file

@ -185,6 +185,7 @@ extern "C" LEAN_EXPORT size_t lean_object_byte_size(lean_object * o) {
case LeanArray: return lean_array_byte_size(o); case LeanArray: return lean_array_byte_size(o);
case LeanScalarArray: return lean_sarray_byte_size(o); case LeanScalarArray: return lean_sarray_byte_size(o);
case LeanString: return lean_string_byte_size(o); case LeanString: return lean_string_byte_size(o);
case LeanClosure: return lean_closure_byte_size(o);
default: return lean_small_object_size(o); default: return lean_small_object_size(o);
} }
} else { } else {
@ -193,6 +194,7 @@ extern "C" LEAN_EXPORT size_t lean_object_byte_size(lean_object * o) {
case LeanArray: return lean_array_byte_size(o); case LeanArray: return lean_array_byte_size(o);
case LeanScalarArray: return lean_sarray_byte_size(o); case LeanScalarArray: return lean_sarray_byte_size(o);
case LeanString: return lean_string_byte_size(o); case LeanString: return lean_string_byte_size(o);
case LeanClosure: return lean_closure_byte_size(o);
default: return o->m_cs_sz; default: return o->m_cs_sz;
} }
} }
@ -207,6 +209,7 @@ extern "C" LEAN_EXPORT size_t lean_object_data_byte_size(lean_object * o) {
case LeanArray: return lean_array_data_byte_size(o); case LeanArray: return lean_array_data_byte_size(o);
case LeanScalarArray: return lean_sarray_data_byte_size(o); case LeanScalarArray: return lean_sarray_data_byte_size(o);
case LeanString: return lean_string_data_byte_size(o); case LeanString: return lean_string_data_byte_size(o);
case LeanClosure: return lean_closure_data_byte_size(o);
default: return lean_small_object_size(o); default: return lean_small_object_size(o);
} }
} else { } else {
@ -215,6 +218,7 @@ extern "C" LEAN_EXPORT size_t lean_object_data_byte_size(lean_object * o) {
case LeanArray: return lean_array_data_byte_size(o); case LeanArray: return lean_array_data_byte_size(o);
case LeanScalarArray: return lean_sarray_data_byte_size(o); case LeanScalarArray: return lean_sarray_data_byte_size(o);
case LeanString: return lean_string_data_byte_size(o); case LeanString: return lean_string_data_byte_size(o);
case LeanClosure: return lean_closure_data_byte_size(o);
default: return o->m_cs_sz; default: return o->m_cs_sz;
} }
} }
@ -235,6 +239,7 @@ extern "C" LEAN_EXPORT void lean_free_object(lean_object * o) {
case LeanArray: return lean_dealloc(o, lean_array_byte_size(o)); case LeanArray: return lean_dealloc(o, lean_array_byte_size(o));
case LeanScalarArray: return lean_dealloc(o, lean_sarray_byte_size(o)); case LeanScalarArray: return lean_dealloc(o, lean_sarray_byte_size(o));
case LeanString: return lean_dealloc(o, lean_string_byte_size(o)); case LeanString: return lean_dealloc(o, lean_string_byte_size(o));
case LeanClosure: return lean_dealloc(o, lean_closure_byte_size(o));
case LeanMPZ: to_mpz(o)->m_value.~mpz(); return lean_free_small_object(o); case LeanMPZ: to_mpz(o)->m_value.~mpz(); return lean_free_small_object(o);
default: return lean_free_small_object(o); default: return lean_free_small_object(o);
} }
@ -335,7 +340,7 @@ static void lean_del_core(object * o, object * & todo) {
object ** it = lean_closure_arg_cptr(o); object ** it = lean_closure_arg_cptr(o);
object ** end = it + lean_closure_num_fixed(o); object ** end = it + lean_closure_num_fixed(o);
for (; it != end; ++it) dec(*it, todo); for (; it != end; ++it) dec(*it, todo);
lean_free_small_object(o); lean_dealloc(o, lean_closure_byte_size(o));
break; break;
} }
case LeanArray: { case LeanArray: {

2
stage0/src/stdlib_flags.h
View file

@ -1,5 +1,7 @@
#include "util/options.h" #include "util/options.h"
// perform the update good sir
namespace lean { namespace lean {
options get_default_options() { options get_default_options() {
options opts; options opts;