chore: update script/apply.lean semantics
This commit is contained in:
Sebastian Ullrich
Leonardo de Moura
parent
5be816244e
commit
9f2182fdd9
2 changed files with 66 additions and 85 deletions
|
|
@ -14,7 +14,7 @@ def emit (s : String) : M Unit := do
|
|||
def mkTypedefFn (i : Nat) : M Unit := do
|
||||
let args := (List.replicate i "obj*").intersperse ", " |> String.join
|
||||
emit s!"typedef obj* (*fn{i})({args}); // NOLINT\n"
|
||||
emit s!"#define FN{i}(f) reinterpret_cast<fn{i}>(closure_fun(f))\n"
|
||||
emit s!"#define FN{i}(f) reinterpret_cast<fn{i}>(lean_closure_fun(f))\n"
|
||||
|
||||
def genSeq (n : Nat) (f : Nat → String) (sep := ", ") : String :=
|
||||
List.range n |>.map f |>.intersperse sep |> .join
|
||||
|
|
@ -32,105 +32,107 @@ def mkArgs (n : Nat) : String := mkArgsFrom 0 n
|
|||
|
||||
-- make string: "as[0], as[1], ..., as[n-1]"
|
||||
def mkAsArgs (n : Nat) : String :=
|
||||
genSeq n (s!"a[{·}]")
|
||||
genSeq n (s!"as[{·}]")
|
||||
|
||||
-- make string: "fx(0), ..., fx(n-1)"
|
||||
def mkFsArgs (n : Nat) : String :=
|
||||
genSeq n (s!"fx({·})")
|
||||
|
||||
-- make string: "inc(fx(0)); ...; inc(fx(n-1))"
|
||||
-- make string: "lean_inc(fx(0)); ...; lean_inc(fx(n-1))"
|
||||
def mkIncFs (n : Nat) : String :=
|
||||
genSeq n (s!"inc(fx({·}))") (sep := "; ")
|
||||
genSeq n (s!"lean_inc(fx({·})); ") (sep := "")
|
||||
|
||||
def mkApplyI (n : Nat) (max : Nat) : M Unit := do
|
||||
let argDecls := mkArgDecls n
|
||||
let args := mkArgs n
|
||||
emit s!"obj* apply_{n}(obj* f, {argDecls}) \{
|
||||
unsigned arity = closure_arity(f);
|
||||
unsigned fixed = closure_num_fixed(f);
|
||||
emit s!"extern \"C\" LEAN_EXPORT obj* lean_apply_{n}(obj* f, {argDecls}) \{
|
||||
if (lean_is_scalar(f)) \{ {genSeq n (s!"lean_dec(a{·+1}); ") (sep := "")}return f; } // f is an erased proof
|
||||
unsigned arity = lean_closure_arity(f);
|
||||
unsigned fixed = lean_closure_num_fixed(f);
|
||||
if (arity == fixed + {n}) \{
|
||||
if (is_exclusive(f)) \{
|
||||
if (lean_is_exclusive(f)) \{
|
||||
switch (arity) \{\n"
|
||||
for j in [n:max + 1] do
|
||||
let fs := mkFsArgs (j - n)
|
||||
let sep := if j = n then "" else ", "
|
||||
emit s!" case {j}: \{ obj* r = FN{j}(f)({fs}{sep}{args}); free_closure_obj(f); return r; }\n"
|
||||
emit s!" case {j}: \{ obj* r = FN{j}(f)({fs}{sep}{args}); lean_free_small_object(f); return r; }\n"
|
||||
emit " }
|
||||
}
|
||||
switch (arity) {\n"
|
||||
for j in [n:max + 1] do
|
||||
let incfs := mkIncFs (j - n)
|
||||
let lean_incfs := mkIncFs (j - n)
|
||||
let fs := mkFsArgs (j - n)
|
||||
let sep := if j = n then "" else ", "
|
||||
emit s!" case {j}: \{ {incfs}obj* r = FN{j}(f)({fs}{sep}{args}); dec_ref(f); return r; }\n"
|
||||
emit s!" case {j}: \{ {lean_incfs}obj* r = FN{j}(f)({fs}{sep}{args}); lean_dec_ref(f); return r; }\n"
|
||||
emit s!" default:
|
||||
lean_assert(arity > {max});
|
||||
obj * as[{n}] = \{ {args} };
|
||||
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
|
||||
for (unsigned i = 0; i < fixed; i++) \{ inc(fx(i)); args[i] = fx(i); }
|
||||
for (unsigned i = 0; i < fixed; i++) \{ lean_inc(fx(i)); args[i] = fx(i); }
|
||||
for (unsigned i = 0; i < {n}; i++) args[fixed+i] = as[i];
|
||||
obj * r = FNN(f)(args);
|
||||
dec_ref(f);
|
||||
lean_dec_ref(f);
|
||||
return r;
|
||||
}
|
||||
} else if (arity < fixed + {n}) \{\n"
|
||||
if n ≥ 2 then do
|
||||
emit s!" obj * as[{n}] = \{ {args} };
|
||||
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
|
||||
for (unsigned i = 0; i < fixed; i++) \{ inc(fx(i)); args[i] = fx(i); }
|
||||
for (unsigned i = 0; i < fixed; i++) \{ lean_inc(fx(i)); args[i] = fx(i); }
|
||||
for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
|
||||
obj * new_f = curry(f, arity, args);
|
||||
dec_ref(f);
|
||||
return apply_n(new_f, {n}+fixed-arity, as+arity-fixed);\n"
|
||||
lean_dec_ref(f);
|
||||
return lean_apply_n(new_f, {n}+fixed-arity, &as[arity-fixed]);\n"
|
||||
else emit s!" lean_assert(fixed < arity);
|
||||
lean_unreachable();
|
||||
} else \{
|
||||
lean_unreachable();\n"
|
||||
emit s!"} else \{
|
||||
return fix_args(f, \{{args}});
|
||||
}
|
||||
}\n"
|
||||
|
||||
def mkCurry (max : Nat) : M Unit := do
|
||||
emit "static obj* curry(void* f, unsigned n, obj** as) {
|
||||
emit "obj* curry(void* f, unsigned n, obj** as) {
|
||||
switch (n) {
|
||||
case 0: lean_unreachable();\n"
|
||||
for i in [0:max] do
|
||||
let as := mkAsArgs (i+1)
|
||||
emit s!"case {i+1}: return reinterpret_cast<fn{i+1}>(f)({as});
|
||||
default: return reinterpret_cast<fnn>(f)(as);
|
||||
emit s!"case {i+1}: return reinterpret_cast<fn{i+1}>(f)({as});\n"
|
||||
emit "default: return reinterpret_cast<fnn>(f)(as);
|
||||
}
|
||||
}
|
||||
static obj* curry(obj* f, unsigned n, obj** as) \{ return curry(closure_fun(f), n, as); }\n"
|
||||
static obj* curry(obj* f, unsigned n, obj** as) { return curry(lean_closure_fun(f), n, as); }\n"
|
||||
|
||||
def mkApplyN (max : Nat) : M Unit := do
|
||||
emit "obj* apply_n(obj* f, unsigned n, obj** as) {
|
||||
emit "extern \"C\" LEAN_EXPORT obj* lean_apply_n(obj* f, unsigned n, obj** as) {
|
||||
switch (n) {
|
||||
case 0: lean_unreachable();\n"
|
||||
for i in [0:max] do
|
||||
let as := mkAsArgs (i+1)
|
||||
emit s!"case {i+1}: return apply_{i+1}(f, {as});
|
||||
default: return apply_m(f, n, as);
|
||||
emit s!"case {i+1}: return lean_apply_{i+1}(f, {as});\n"
|
||||
emit "default: return lean_apply_m(f, n, as);
|
||||
}
|
||||
}\n"
|
||||
|
||||
def mkApplyM (max : Nat) : M Unit :=
|
||||
emit s!"obj* apply_m(obj* f, unsigned n, obj** as) \{
|
||||
emit s!"extern \"C\" LEAN_EXPORT obj* lean_apply_m(obj* f, unsigned n, obj** as) \{
|
||||
lean_assert(n > {max});
|
||||
unsigned arity = closure_arity(f);
|
||||
unsigned fixed = closure_num_fixed(f);
|
||||
if (lean_is_scalar(f)) \{ for (unsigned i = 0; i < n; i++) \{ lean_dec(as[i]); } return f; } // f is an erased proof
|
||||
unsigned arity = lean_closure_arity(f);
|
||||
unsigned fixed = lean_closure_num_fixed(f);
|
||||
if (arity == fixed + n) \{
|
||||
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
|
||||
for (unsigned i = 0; i < fixed; i++) \{ inc(fx(i)); args[i] = fx(i); }
|
||||
for (unsigned i = 0; i < fixed; i++) \{ lean_inc(fx(i)); args[i] = fx(i); }
|
||||
for (unsigned i = 0; i < n; i++) args[fixed+i] = as[i];
|
||||
obj * r = FNN(f)(args);
|
||||
dec_ref(f);
|
||||
lean_dec_ref(f);
|
||||
return r;
|
||||
} else if (arity < fixed + n) \{
|
||||
obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
|
||||
for (unsigned i = 0; i < fixed; i++) \{ inc(fx(i)); args[i] = fx(i); }
|
||||
for (unsigned i = 0; i < fixed; i++) \{ lean_inc(fx(i)); args[i] = fx(i); }
|
||||
for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
|
||||
obj * new_f = FNN(f)(args);
|
||||
dec_ref(f);
|
||||
return apply_n(new_f, n+fixed-arity, as+arity-fixed);
|
||||
lean_dec_ref(f);
|
||||
return lean_apply_n(new_f, n+fixed-arity, &as[arity-fixed]);
|
||||
} else \{
|
||||
return fix_args(f, n, as);
|
||||
}
|
||||
|
|
@ -138,24 +140,24 @@ if (arity == fixed + n) \{
|
|||
|
||||
def mkFixArgs : M Unit := emit "
|
||||
static obj* fix_args(obj* f, unsigned n, obj*const* as) {
|
||||
unsigned arity = closure_arity(f);
|
||||
unsigned fixed = closure_num_fixed(f);
|
||||
unsigned arity = lean_closure_arity(f);
|
||||
unsigned fixed = lean_closure_num_fixed(f);
|
||||
unsigned new_fixed = fixed + n;
|
||||
lean_assert(new_fixed < arity);
|
||||
obj * r = alloc_closure(closure_fun(f), arity, new_fixed);
|
||||
obj ** source = closure_arg_cptr(f);
|
||||
obj ** target = closure_arg_cptr(r);
|
||||
if (!is_exclusive(f)) {
|
||||
obj * r = lean_alloc_closure(lean_closure_fun(f), arity, new_fixed);
|
||||
obj ** source = lean_closure_arg_cptr(f);
|
||||
obj ** target = lean_closure_arg_cptr(r);
|
||||
if (!lean_is_exclusive(f)) {
|
||||
for (unsigned i = 0; i < fixed; i++, source++, target++) {
|
||||
*target = *source;
|
||||
inc(*target);
|
||||
lean_inc(*target);
|
||||
}
|
||||
dec_ref(f);
|
||||
lean_dec_ref(f);
|
||||
} else {
|
||||
for (unsigned i = 0; i < fixed; i++, source++, target++) {
|
||||
*target = *source;
|
||||
}
|
||||
free_closure_obj(f);
|
||||
lean_free_small_object(f);
|
||||
}
|
||||
for (unsigned i = 0; i < n; i++, as++, target++) {
|
||||
*target = *as;
|
||||
|
|
@ -182,40 +184,19 @@ def mkApplyCpp (max : Nat) : M Unit := do
|
|||
// Generated using script: ../../gen/apply.lean
|
||||
#include \"runtime/apply.h\"
|
||||
namespace lean {
|
||||
#define obj object
|
||||
#define fx(i) closure_arg_cptr(f)[i]\n"
|
||||
#define obj lean_object
|
||||
#define fx(i) lean_closure_arg_cptr(f)[i]\n"
|
||||
mkFixArgs
|
||||
for i in [0:max] do mkTypedefFn (i+1)
|
||||
emit "typedef obj* (*fnn)(obj**); // NOLINT
|
||||
#define FNN(f) reinterpret_cast<fnn>(closure_fun(f))\n"
|
||||
#define FNN(f) reinterpret_cast<fnn>(lean_closure_fun(f))\n"
|
||||
mkCurry max
|
||||
emit "obj* apply_n(obj*, unsigned, obj**);\n"
|
||||
emit "extern \"C\" obj* lean_apply_n(obj*, unsigned, obj**);\n"
|
||||
for i in [0:max] do mkApplyI (i+1) max
|
||||
mkApplyM max
|
||||
mkApplyN max
|
||||
emit "}\n"
|
||||
|
||||
-- make string: "object* a1, object* a2, ..., object** an"
|
||||
def mkArgDecls' (n : Nat) : String :=
|
||||
genSeq n (s!"object* a{·+1}")
|
||||
|
||||
def mkApplyH (max : Nat) : M Unit := do
|
||||
mkCopyright
|
||||
emit "// DO NOT EDIT, this is an automatically generated file
|
||||
// Generated using script: ../../gen/apply.lean
|
||||
#pragma once
|
||||
#include \"runtime/object.h\"
|
||||
#define LEAN_CLOSURE_MAX_ARGS {max}"
|
||||
emit "namespace lean {\n"
|
||||
for i in [0:max] do
|
||||
let args := mkArgDecls' (i+1)
|
||||
emit s!"object* apply_{i+1}(object* f, {args});
|
||||
object* apply_n(object* f, unsigned n, object** args);
|
||||
// pre: n > {max}
|
||||
object* apply_m(object* f, unsigned n, object** args);
|
||||
}\n"
|
||||
|
||||
-- #eval (mkApplyCpp 4).run none
|
||||
|
||||
#eval (mkApplyCpp Lean.closureMaxArgs).run "../src/runtime/apply.cpp"
|
||||
#eval (mkApplyH Lean.closureMaxArgs).run "../src/runtime/apply.h"
|
||||
#eval (mkApplyCpp Lean.closureMaxArgs).run "src/runtime/apply.cpp"
|
||||
|
|
|
|||
|
|
@ -24,7 +24,7 @@ static obj* fix_args(obj* f, unsigned n, obj*const* as) {
|
|||
*target = *source;
|
||||
lean_inc(*target);
|
||||
}
|
||||
dec_ref(f);
|
||||
lean_dec_ref(f);
|
||||
} else {
|
||||
for (unsigned i = 0; i < fixed; i++, source++, target++) {
|
||||
*target = *source;
|
||||
|
|
@ -103,7 +103,7 @@ if (lean_is_scalar(f)) { lean_dec(a1); return f; } // f is an erased proof
|
|||
unsigned arity = lean_closure_arity(f);
|
||||
unsigned fixed = lean_closure_num_fixed(f);
|
||||
if (arity == fixed + 1) {
|
||||
if (is_exclusive(f)) {
|
||||
if (lean_is_exclusive(f)) {
|
||||
switch (arity) {
|
||||
case 1: { obj* r = FN1(f)(a1); lean_free_small_object(f); return r; }
|
||||
case 2: { obj* r = FN2(f)(fx(0), a1); lean_free_small_object(f); return r; }
|
||||
|
|
@ -162,7 +162,7 @@ if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); return f; } // f is an eras
|
|||
unsigned arity = lean_closure_arity(f);
|
||||
unsigned fixed = lean_closure_num_fixed(f);
|
||||
if (arity == fixed + 2) {
|
||||
if (is_exclusive(f)) {
|
||||
if (lean_is_exclusive(f)) {
|
||||
switch (arity) {
|
||||
case 2: { obj* r = FN2(f)(a1, a2); lean_free_small_object(f); return r; }
|
||||
case 3: { obj* r = FN3(f)(fx(0), a1, a2); lean_free_small_object(f); return r; }
|
||||
|
|
@ -224,7 +224,7 @@ if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); return f; } /
|
|||
unsigned arity = lean_closure_arity(f);
|
||||
unsigned fixed = lean_closure_num_fixed(f);
|
||||
if (arity == fixed + 3) {
|
||||
if (is_exclusive(f)) {
|
||||
if (lean_is_exclusive(f)) {
|
||||
switch (arity) {
|
||||
case 3: { obj* r = FN3(f)(a1, a2, a3); lean_free_small_object(f); return r; }
|
||||
case 4: { obj* r = FN4(f)(fx(0), a1, a2, a3); lean_free_small_object(f); return r; }
|
||||
|
|
@ -284,7 +284,7 @@ if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4);
|
|||
unsigned arity = lean_closure_arity(f);
|
||||
unsigned fixed = lean_closure_num_fixed(f);
|
||||
if (arity == fixed + 4) {
|
||||
if (is_exclusive(f)) {
|
||||
if (lean_is_exclusive(f)) {
|
||||
switch (arity) {
|
||||
case 4: { obj* r = FN4(f)(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_small_object(f); return r; }
|
||||
|
|
@ -342,7 +342,7 @@ if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4);
|
|||
unsigned arity = lean_closure_arity(f);
|
||||
unsigned fixed = lean_closure_num_fixed(f);
|
||||
if (arity == fixed + 5) {
|
||||
if (is_exclusive(f)) {
|
||||
if (lean_is_exclusive(f)) {
|
||||
switch (arity) {
|
||||
case 5: { obj* r = FN5(f)(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_small_object(f); return r; }
|
||||
|
|
@ -398,7 +398,7 @@ if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4);
|
|||
unsigned arity = lean_closure_arity(f);
|
||||
unsigned fixed = lean_closure_num_fixed(f);
|
||||
if (arity == fixed + 6) {
|
||||
if (is_exclusive(f)) {
|
||||
if (lean_is_exclusive(f)) {
|
||||
switch (arity) {
|
||||
case 6: { obj* r = FN6(f)(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_small_object(f); return r; }
|
||||
|
|
@ -452,7 +452,7 @@ if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4);
|
|||
unsigned arity = lean_closure_arity(f);
|
||||
unsigned fixed = lean_closure_num_fixed(f);
|
||||
if (arity == fixed + 7) {
|
||||
if (is_exclusive(f)) {
|
||||
if (lean_is_exclusive(f)) {
|
||||
switch (arity) {
|
||||
case 7: { obj* r = FN7(f)(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_small_object(f); return r; }
|
||||
|
|
@ -504,7 +504,7 @@ if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4);
|
|||
unsigned arity = lean_closure_arity(f);
|
||||
unsigned fixed = lean_closure_num_fixed(f);
|
||||
if (arity == fixed + 8) {
|
||||
if (is_exclusive(f)) {
|
||||
if (lean_is_exclusive(f)) {
|
||||
switch (arity) {
|
||||
case 8: { obj* r = FN8(f)(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_small_object(f); return r; }
|
||||
|
|
@ -554,7 +554,7 @@ if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4);
|
|||
unsigned arity = lean_closure_arity(f);
|
||||
unsigned fixed = lean_closure_num_fixed(f);
|
||||
if (arity == fixed + 9) {
|
||||
if (is_exclusive(f)) {
|
||||
if (lean_is_exclusive(f)) {
|
||||
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 10: { obj* r = FN10(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9); lean_free_small_object(f); return r; }
|
||||
|
|
@ -602,7 +602,7 @@ if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4);
|
|||
unsigned arity = lean_closure_arity(f);
|
||||
unsigned fixed = lean_closure_num_fixed(f);
|
||||
if (arity == fixed + 10) {
|
||||
if (is_exclusive(f)) {
|
||||
if (lean_is_exclusive(f)) {
|
||||
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 11: { obj* r = FN11(f)(fx(0), a1, a2, a3, a4, a5, a6, a7, a8, a9, a10); lean_free_small_object(f); return r; }
|
||||
|
|
@ -648,7 +648,7 @@ if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4);
|
|||
unsigned arity = lean_closure_arity(f);
|
||||
unsigned fixed = lean_closure_num_fixed(f);
|
||||
if (arity == fixed + 11) {
|
||||
if (is_exclusive(f)) {
|
||||
if (lean_is_exclusive(f)) {
|
||||
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 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; }
|
||||
|
|
@ -692,7 +692,7 @@ if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4);
|
|||
unsigned arity = lean_closure_arity(f);
|
||||
unsigned fixed = lean_closure_num_fixed(f);
|
||||
if (arity == fixed + 12) {
|
||||
if (is_exclusive(f)) {
|
||||
if (lean_is_exclusive(f)) {
|
||||
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 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; }
|
||||
|
|
@ -734,7 +734,7 @@ if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4);
|
|||
unsigned arity = lean_closure_arity(f);
|
||||
unsigned fixed = lean_closure_num_fixed(f);
|
||||
if (arity == fixed + 13) {
|
||||
if (is_exclusive(f)) {
|
||||
if (lean_is_exclusive(f)) {
|
||||
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 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; }
|
||||
|
|
@ -774,7 +774,7 @@ if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4);
|
|||
unsigned arity = lean_closure_arity(f);
|
||||
unsigned fixed = lean_closure_num_fixed(f);
|
||||
if (arity == fixed + 14) {
|
||||
if (is_exclusive(f)) {
|
||||
if (lean_is_exclusive(f)) {
|
||||
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 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; }
|
||||
|
|
@ -812,7 +812,7 @@ if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4);
|
|||
unsigned arity = lean_closure_arity(f);
|
||||
unsigned fixed = lean_closure_num_fixed(f);
|
||||
if (arity == fixed + 15) {
|
||||
if (is_exclusive(f)) {
|
||||
if (lean_is_exclusive(f)) {
|
||||
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 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; }
|
||||
|
|
@ -848,7 +848,7 @@ if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4);
|
|||
unsigned arity = lean_closure_arity(f);
|
||||
unsigned fixed = lean_closure_num_fixed(f);
|
||||
if (arity == fixed + 16) {
|
||||
if (is_exclusive(f)) {
|
||||
if (lean_is_exclusive(f)) {
|
||||
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; }
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue