feat(library/init/fix, runtime): add fixpoint2, ..., fixpoint6
The idea is to avoid allocating tuples when creating the fixpoint of nary functions. For example, consider the new tests: - tests/playground/fix.lean - tests/playground/fix_with_tuples.lean The second one (`fix_with_tuples`) uses the `fix` operator and tuples. For input = 20, it creates more than 1 million extra objects. The first implementation (`fix.lean`) using `fix₂` avoids this overhead. TODO: Add support for pattern #N with N > 9 at ``` def expand_extern_pattern_aux (args : list string) : nat → string.iterator → string → string ```
This commit is contained in:
Leonardo de Moura
parent
4ca9c6f22e
commit
ff3bf508aa
6 changed files with 1130 additions and 23 deletions
|
|
@ -12,8 +12,66 @@ def bfix {α β : Type u} (base : α → β) (rec : (α → β) → α → β) :
|
|||
| (n+1) a := rec (bfix n) a
|
||||
|
||||
@[extern cpp inline "lean::fixpoint(#4, #5)"]
|
||||
def fix_core {α β : Type u} (base : @& (α → β)) (rec : (α → β) → α → β) (a : α) : β :=
|
||||
bfix base rec usize_sz a
|
||||
def fix_core {α β : Type u} (base : @& (α → β)) (rec : (α → β) → α → β) : α → β :=
|
||||
bfix base rec usize_sz
|
||||
|
||||
@[inline] def fix {α β : Type u} [inhabited β] (rec : (α → β) → α → β) (a : α) : β :=
|
||||
fix_core (λ _, default β) rec a
|
||||
@[inline] def fix {α β : Type u} [inhabited β] (rec : (α → β) → α → β) : α → β :=
|
||||
fix_core (λ _, default β) rec
|
||||
|
||||
@[inline] def fix₁ {α β : Type u} [inhabited β] (rec : (α → β) → α → β) : α → β :=
|
||||
fix_core (λ _, default β) rec
|
||||
|
||||
def bfix₂ {α₁ α₂ β : Type u} (base : α₁ → α₂ → β) (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) : nat → α₁ → α₂ → β
|
||||
| 0 a₁ a₂ := base a₁ a₂
|
||||
| (n+1) a₁ a₂ := rec (bfix₂ n) a₁ a₂
|
||||
|
||||
@[extern cpp inline "lean::fixpoint2(#5, #6, #7)"]
|
||||
def fix_core₂ {α₁ α₂ β : Type u} (base : α₁ → α₂ → β) (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) : α₁ → α₂ → β :=
|
||||
bfix₂ base rec usize_sz
|
||||
|
||||
@[inline] def fix₂ {α₁ α₂ β : Type u} [inhabited β] (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) : α₁ → α₂ → β :=
|
||||
fix_core₂ (λ _ _, default β) rec
|
||||
|
||||
def bfix₃ {α₁ α₂ α₃ β : Type u} (base : α₁ → α₂ → α₃ → β) (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) : nat → α₁ → α₂ → α₃ → β
|
||||
| 0 a₁ a₂ a₃ := base a₁ a₂ a₃
|
||||
| (n+1) a₁ a₂ a₃ := rec (bfix₃ n) a₁ a₂ a₃
|
||||
|
||||
@[extern cpp inline "lean::fixpoint3(#6, #7, #8, #9)"]
|
||||
def fix_core₃ {α₁ α₂ α₃ β : Type u} (base : α₁ → α₂ → α₃ → β) (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) : α₁ → α₂ → α₃ → β :=
|
||||
bfix₃ base rec usize_sz
|
||||
|
||||
@[inline] def fix₃ {α₁ α₂ α₃ β : Type u} [inhabited β] (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) : α₁ → α₂ → α₃ → β :=
|
||||
fix_core₃ (λ _ _ _, default β) rec
|
||||
|
||||
def bfix₄ {α₁ α₂ α₃ α₄ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → β) (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) : nat → α₁ → α₂ → α₃ → α₄ → β
|
||||
| 0 a₁ a₂ a₃ a₄ := base a₁ a₂ a₃ a₄
|
||||
| (n+1) a₁ a₂ a₃ a₄ := rec (bfix₄ n) a₁ a₂ a₃ a₄
|
||||
|
||||
-- @[extern cpp inline "lean::fixpoint4(#7, #8, #9, #10, #11)"]
|
||||
def fix_core₄ {α₁ α₂ α₃ α₄ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → β) (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) : α₁ → α₂ → α₃ → α₄ → β :=
|
||||
bfix₄ base rec usize_sz
|
||||
|
||||
@[inline] def fix₄ {α₁ α₂ α₃ α₄ β : Type u} [inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) : α₁ → α₂ → α₃ → α₄ → β :=
|
||||
fix_core₄ (λ _ _ _ _, default β) rec
|
||||
|
||||
def bfix₅ {α₁ α₂ α₃ α₄ α₅ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) : nat → α₁ → α₂ → α₃ → α₄ → α₅ → β
|
||||
| 0 a₁ a₂ a₃ a₄ a₅ := base a₁ a₂ a₃ a₄ a₅
|
||||
| (n+1) a₁ a₂ a₃ a₄ a₅ := rec (bfix₅ n) a₁ a₂ a₃ a₄ a₅
|
||||
|
||||
-- @[extern cpp inline "lean::fixpoint5(#8, #9, #10, #11, #12, #13)"]
|
||||
def fix_core₅ {α₁ α₂ α₃ α₄ α₅ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → β :=
|
||||
bfix₅ base rec usize_sz
|
||||
|
||||
@[inline] def fix₅ {α₁ α₂ α₃ α₄ α₅ β : Type u} [inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → β :=
|
||||
fix_core₅ (λ _ _ _ _ _, default β) rec
|
||||
|
||||
def bfix₆ {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) : nat → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β
|
||||
| 0 a₁ a₂ a₃ a₄ a₅ a₆ := base a₁ a₂ a₃ a₄ a₅ a₆
|
||||
| (n+1) a₁ a₂ a₃ a₄ a₅ a₆ := rec (bfix₆ n) a₁ a₂ a₃ a₄ a₅ a₆
|
||||
|
||||
-- @[extern cpp inline "lean::fixpoint6(#9, #10, #11, #12, #13, #14, #15)"]
|
||||
def fix_core₆ {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β :=
|
||||
bfix₆ base rec usize_sz
|
||||
|
||||
@[inline] def fix₆ {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} [inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β :=
|
||||
fix_core₆ (λ _ _ _ _ _ _, default β) rec
|
||||
|
|
|
|||
|
|
@ -14,26 +14,106 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
|
|||
#pragma GCC diagnostic ignored "-Wunused-label"
|
||||
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
|
||||
#endif
|
||||
obj* l_fix_u_2082___rarg___lambda__1___boxed(obj*, obj*, obj*);
|
||||
obj* l_fix_u_2084(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix_u_2086___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2083___boxed(obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2083___main___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2083(obj*, obj*, obj*, obj*);
|
||||
obj* l_fix_u_2081___boxed(obj*, obj*);
|
||||
obj* l_bfix_u_2086___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2085___main___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix__core_u_2084___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2084___main___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix_u_2085___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2085___main(obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix_u_2085___rarg___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2085___main___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix__core_u_2086___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2085___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix___rarg___lambda__1___boxed(obj*, obj*);
|
||||
obj* l_fix_u_2083___boxed(obj*, obj*, obj*, obj*);
|
||||
obj* l_fix_u_2082___rarg(obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2084___main___boxed(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2084___main(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2084(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2082___rarg(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2083___main___boxed(obj*, obj*, obj*, obj*);
|
||||
obj* l_fix__core_u_2082___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix_u_2082(obj*, obj*, obj*);
|
||||
obj* l_fix__core_u_2084___boxed(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix___rarg(obj*, obj*, obj*);
|
||||
obj* l_fix_u_2086___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix___main(obj*, obj*);
|
||||
obj* l_bfix_u_2086___main___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2082___main___boxed(obj*, obj*, obj*);
|
||||
namespace lean {
|
||||
uint8 nat_dec_eq(obj*, obj*);
|
||||
}
|
||||
obj* l_bfix_u_2084___main___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2086___main(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix_u_2086___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix___rarg(obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2082___rarg___boxed(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix__core_u_2086___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix___main___rarg(obj*, obj*, obj*, obj*);
|
||||
obj* l_fix_u_2084___rarg___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix_u_2084___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2086___main___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix_u_2084___boxed(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix(obj*, obj*);
|
||||
obj* l_fix_u_2082___boxed(obj*, obj*, obj*);
|
||||
obj* l_fix_u_2086___rarg___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2086___main___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2082(obj*, obj*, obj*);
|
||||
obj* l_fix(obj*, obj*);
|
||||
obj* l_bfix_u_2084___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix___rarg___lambda__1(obj*, obj*);
|
||||
obj* l_fix__core_u_2086(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix__core_u_2085___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2085___main___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2083___main___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix__core___boxed(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix__core_u_2085___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2084___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix_u_2083___rarg___lambda__1(obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2082___main___rarg___boxed(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix_u_2086(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2083___main(obj*, obj*, obj*, obj*);
|
||||
obj* l_fix_u_2083___rarg___lambda__1___boxed(obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix___main___boxed(obj*, obj*);
|
||||
obj* l_fix_u_2083___rarg(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix_u_2081(obj*, obj*);
|
||||
extern obj* l_usize__sz;
|
||||
obj* l_fix_u_2083(obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2084___boxed(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix_u_2082___rarg___lambda__1(obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2082___main(obj*, obj*, obj*);
|
||||
obj* l_fix__core_u_2083___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix_u_2085___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2083___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix__core_u_2084(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix_u_2085(obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2085___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix_u_2081___rarg(obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2085(obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix__core_u_2085(obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2086___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
namespace lean {
|
||||
obj* nat_sub(obj*, obj*);
|
||||
}
|
||||
obj* l_fix_u_2084___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2082___main___rarg(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2082___boxed(obj*, obj*, obj*);
|
||||
obj* l_bfix___main___rarg___boxed(obj*, obj*, obj*, obj*);
|
||||
obj* l_fix___boxed(obj*, obj*);
|
||||
obj* l_bfix_u_2086(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2083___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_fix_u_2085___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix___rarg___boxed(obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix___boxed(obj*, obj*);
|
||||
obj* l_bfix_u_2085___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix_u_2086___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_bfix___main___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -179,6 +259,882 @@ lean::dec(x_1);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2081___rarg(obj* x_0, obj* x_1, obj* x_2) {
|
||||
_start:
|
||||
{
|
||||
obj* x_3; obj* x_4;
|
||||
x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_fix___rarg___lambda__1___boxed), 2, 1);
|
||||
lean::closure_set(x_3, 0, x_0);
|
||||
x_4 = lean::fixpoint(x_1, x_2);
|
||||
lean::dec(x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2081(obj* x_0, obj* x_1) {
|
||||
_start:
|
||||
{
|
||||
obj* x_2;
|
||||
x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_fix_u_2081___rarg), 3, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2081___boxed(obj* x_0, obj* x_1) {
|
||||
_start:
|
||||
{
|
||||
obj* x_2;
|
||||
x_2 = l_fix_u_2081(x_0, x_1);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2082___main___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
|
||||
_start:
|
||||
{
|
||||
obj* x_5; uint8 x_6;
|
||||
x_5 = lean::mk_nat_obj(0u);
|
||||
x_6 = lean::nat_dec_eq(x_2, x_5);
|
||||
if (x_6 == 0)
|
||||
{
|
||||
obj* x_7; obj* x_8; obj* x_10; obj* x_11;
|
||||
x_7 = lean::mk_nat_obj(1u);
|
||||
x_8 = lean::nat_sub(x_2, x_7);
|
||||
lean::inc(x_1);
|
||||
x_10 = lean::alloc_closure(reinterpret_cast<void*>(l_bfix_u_2082___main___rarg___boxed), 5, 3);
|
||||
lean::closure_set(x_10, 0, x_0);
|
||||
lean::closure_set(x_10, 1, x_1);
|
||||
lean::closure_set(x_10, 2, x_8);
|
||||
x_11 = lean::apply_3(x_1, x_10, x_3, x_4);
|
||||
return x_11;
|
||||
}
|
||||
else
|
||||
{
|
||||
obj* x_13;
|
||||
lean::dec(x_1);
|
||||
x_13 = lean::apply_2(x_0, x_3, x_4);
|
||||
return x_13;
|
||||
}
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2082___main(obj* x_0, obj* x_1, obj* x_2) {
|
||||
_start:
|
||||
{
|
||||
obj* x_3;
|
||||
x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_bfix_u_2082___main___rarg___boxed), 5, 0);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2082___main___rarg___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
|
||||
_start:
|
||||
{
|
||||
obj* x_5;
|
||||
x_5 = l_bfix_u_2082___main___rarg(x_0, x_1, x_2, x_3, x_4);
|
||||
lean::dec(x_2);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2082___main___boxed(obj* x_0, obj* x_1, obj* x_2) {
|
||||
_start:
|
||||
{
|
||||
obj* x_3;
|
||||
x_3 = l_bfix_u_2082___main(x_0, x_1, x_2);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2082___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
|
||||
_start:
|
||||
{
|
||||
obj* x_5;
|
||||
x_5 = l_bfix_u_2082___main___rarg(x_0, x_1, x_2, x_3, x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2082(obj* x_0, obj* x_1, obj* x_2) {
|
||||
_start:
|
||||
{
|
||||
obj* x_3;
|
||||
x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_bfix_u_2082___rarg___boxed), 5, 0);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2082___rarg___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
|
||||
_start:
|
||||
{
|
||||
obj* x_5;
|
||||
x_5 = l_bfix_u_2082___rarg(x_0, x_1, x_2, x_3, x_4);
|
||||
lean::dec(x_2);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2082___boxed(obj* x_0, obj* x_1, obj* x_2) {
|
||||
_start:
|
||||
{
|
||||
obj* x_3;
|
||||
x_3 = l_bfix_u_2082(x_0, x_1, x_2);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
obj* l_fix__core_u_2082___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
|
||||
_start:
|
||||
{
|
||||
obj* x_7;
|
||||
x_7 = lean::fixpoint2(x_4, x_5, x_6);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2082___rarg___lambda__1(obj* x_0, obj* x_1, obj* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean::inc(x_0);
|
||||
return x_0;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2082___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
|
||||
_start:
|
||||
{
|
||||
obj* x_4; obj* x_5;
|
||||
x_4 = lean::alloc_closure(reinterpret_cast<void*>(l_fix_u_2082___rarg___lambda__1___boxed), 3, 1);
|
||||
lean::closure_set(x_4, 0, x_0);
|
||||
x_5 = lean::fixpoint2(x_1, x_2, x_3);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2082(obj* x_0, obj* x_1, obj* x_2) {
|
||||
_start:
|
||||
{
|
||||
obj* x_3;
|
||||
x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_fix_u_2082___rarg), 4, 0);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2082___rarg___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2) {
|
||||
_start:
|
||||
{
|
||||
obj* x_3;
|
||||
x_3 = l_fix_u_2082___rarg___lambda__1(x_0, x_1, x_2);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2082___boxed(obj* x_0, obj* x_1, obj* x_2) {
|
||||
_start:
|
||||
{
|
||||
obj* x_3;
|
||||
x_3 = l_fix_u_2082(x_0, x_1, x_2);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2083___main___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
|
||||
_start:
|
||||
{
|
||||
obj* x_6; uint8 x_7;
|
||||
x_6 = lean::mk_nat_obj(0u);
|
||||
x_7 = lean::nat_dec_eq(x_2, x_6);
|
||||
if (x_7 == 0)
|
||||
{
|
||||
obj* x_8; obj* x_9; obj* x_11; obj* x_12;
|
||||
x_8 = lean::mk_nat_obj(1u);
|
||||
x_9 = lean::nat_sub(x_2, x_8);
|
||||
lean::inc(x_1);
|
||||
x_11 = lean::alloc_closure(reinterpret_cast<void*>(l_bfix_u_2083___main___rarg___boxed), 6, 3);
|
||||
lean::closure_set(x_11, 0, x_0);
|
||||
lean::closure_set(x_11, 1, x_1);
|
||||
lean::closure_set(x_11, 2, x_9);
|
||||
x_12 = lean::apply_4(x_1, x_11, x_3, x_4, x_5);
|
||||
return x_12;
|
||||
}
|
||||
else
|
||||
{
|
||||
obj* x_14;
|
||||
lean::dec(x_1);
|
||||
x_14 = lean::apply_3(x_0, x_3, x_4, x_5);
|
||||
return x_14;
|
||||
}
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2083___main(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
|
||||
_start:
|
||||
{
|
||||
obj* x_4;
|
||||
x_4 = lean::alloc_closure(reinterpret_cast<void*>(l_bfix_u_2083___main___rarg___boxed), 6, 0);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2083___main___rarg___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
|
||||
_start:
|
||||
{
|
||||
obj* x_6;
|
||||
x_6 = l_bfix_u_2083___main___rarg(x_0, x_1, x_2, x_3, x_4, x_5);
|
||||
lean::dec(x_2);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2083___main___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
|
||||
_start:
|
||||
{
|
||||
obj* x_4;
|
||||
x_4 = l_bfix_u_2083___main(x_0, x_1, x_2, x_3);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
lean::dec(x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2083___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
|
||||
_start:
|
||||
{
|
||||
obj* x_6;
|
||||
x_6 = l_bfix_u_2083___main___rarg(x_0, x_1, x_2, x_3, x_4, x_5);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2083(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
|
||||
_start:
|
||||
{
|
||||
obj* x_4;
|
||||
x_4 = lean::alloc_closure(reinterpret_cast<void*>(l_bfix_u_2083___rarg___boxed), 6, 0);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2083___rarg___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
|
||||
_start:
|
||||
{
|
||||
obj* x_6;
|
||||
x_6 = l_bfix_u_2083___rarg(x_0, x_1, x_2, x_3, x_4, x_5);
|
||||
lean::dec(x_2);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2083___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
|
||||
_start:
|
||||
{
|
||||
obj* x_4;
|
||||
x_4 = l_bfix_u_2083(x_0, x_1, x_2, x_3);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
lean::dec(x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
obj* l_fix__core_u_2083___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8) {
|
||||
_start:
|
||||
{
|
||||
obj* x_9;
|
||||
x_9 = lean::fixpoint3(x_5, x_6, x_7, x_8);
|
||||
return x_9;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2083___rarg___lambda__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean::inc(x_0);
|
||||
return x_0;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2083___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
|
||||
_start:
|
||||
{
|
||||
obj* x_5; obj* x_6;
|
||||
x_5 = lean::alloc_closure(reinterpret_cast<void*>(l_fix_u_2083___rarg___lambda__1___boxed), 4, 1);
|
||||
lean::closure_set(x_5, 0, x_0);
|
||||
x_6 = lean::fixpoint3(x_1, x_2, x_3, x_4);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2083(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
|
||||
_start:
|
||||
{
|
||||
obj* x_4;
|
||||
x_4 = lean::alloc_closure(reinterpret_cast<void*>(l_fix_u_2083___rarg), 5, 0);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2083___rarg___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
|
||||
_start:
|
||||
{
|
||||
obj* x_4;
|
||||
x_4 = l_fix_u_2083___rarg___lambda__1(x_0, x_1, x_2, x_3);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
lean::dec(x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2083___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
|
||||
_start:
|
||||
{
|
||||
obj* x_4;
|
||||
x_4 = l_fix_u_2083(x_0, x_1, x_2, x_3);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
lean::dec(x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2084___main___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
|
||||
_start:
|
||||
{
|
||||
obj* x_7; uint8 x_8;
|
||||
x_7 = lean::mk_nat_obj(0u);
|
||||
x_8 = lean::nat_dec_eq(x_2, x_7);
|
||||
if (x_8 == 0)
|
||||
{
|
||||
obj* x_9; obj* x_10; obj* x_12; obj* x_13;
|
||||
x_9 = lean::mk_nat_obj(1u);
|
||||
x_10 = lean::nat_sub(x_2, x_9);
|
||||
lean::inc(x_1);
|
||||
x_12 = lean::alloc_closure(reinterpret_cast<void*>(l_bfix_u_2084___main___rarg___boxed), 7, 3);
|
||||
lean::closure_set(x_12, 0, x_0);
|
||||
lean::closure_set(x_12, 1, x_1);
|
||||
lean::closure_set(x_12, 2, x_10);
|
||||
x_13 = lean::apply_5(x_1, x_12, x_3, x_4, x_5, x_6);
|
||||
return x_13;
|
||||
}
|
||||
else
|
||||
{
|
||||
obj* x_15;
|
||||
lean::dec(x_1);
|
||||
x_15 = lean::apply_4(x_0, x_3, x_4, x_5, x_6);
|
||||
return x_15;
|
||||
}
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2084___main(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
|
||||
_start:
|
||||
{
|
||||
obj* x_5;
|
||||
x_5 = lean::alloc_closure(reinterpret_cast<void*>(l_bfix_u_2084___main___rarg___boxed), 7, 0);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2084___main___rarg___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
|
||||
_start:
|
||||
{
|
||||
obj* x_7;
|
||||
x_7 = l_bfix_u_2084___main___rarg(x_0, x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
lean::dec(x_2);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2084___main___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
|
||||
_start:
|
||||
{
|
||||
obj* x_5;
|
||||
x_5 = l_bfix_u_2084___main(x_0, x_1, x_2, x_3, x_4);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
lean::dec(x_3);
|
||||
lean::dec(x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2084___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
|
||||
_start:
|
||||
{
|
||||
obj* x_7;
|
||||
x_7 = l_bfix_u_2084___main___rarg(x_0, x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2084(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
|
||||
_start:
|
||||
{
|
||||
obj* x_5;
|
||||
x_5 = lean::alloc_closure(reinterpret_cast<void*>(l_bfix_u_2084___rarg___boxed), 7, 0);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2084___rarg___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
|
||||
_start:
|
||||
{
|
||||
obj* x_7;
|
||||
x_7 = l_bfix_u_2084___rarg(x_0, x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
lean::dec(x_2);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2084___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
|
||||
_start:
|
||||
{
|
||||
obj* x_5;
|
||||
x_5 = l_bfix_u_2084(x_0, x_1, x_2, x_3, x_4);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
lean::dec(x_3);
|
||||
lean::dec(x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
obj* l_fix__core_u_2084___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
|
||||
_start:
|
||||
{
|
||||
obj* x_6; obj* x_7;
|
||||
x_6 = l_usize__sz;
|
||||
x_7 = l_bfix_u_2084___main___rarg(x_0, x_1, x_6, x_2, x_3, x_4, x_5);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
obj* l_fix__core_u_2084(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
|
||||
_start:
|
||||
{
|
||||
obj* x_5;
|
||||
x_5 = lean::alloc_closure(reinterpret_cast<void*>(l_fix__core_u_2084___rarg), 6, 0);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
obj* l_fix__core_u_2084___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
|
||||
_start:
|
||||
{
|
||||
obj* x_5;
|
||||
x_5 = l_fix__core_u_2084(x_0, x_1, x_2, x_3, x_4);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
lean::dec(x_3);
|
||||
lean::dec(x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2084___rarg___lambda__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean::inc(x_0);
|
||||
return x_0;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2084___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
|
||||
_start:
|
||||
{
|
||||
obj* x_6; obj* x_7; obj* x_8;
|
||||
x_6 = lean::alloc_closure(reinterpret_cast<void*>(l_fix_u_2084___rarg___lambda__1___boxed), 5, 1);
|
||||
lean::closure_set(x_6, 0, x_0);
|
||||
x_7 = l_usize__sz;
|
||||
x_8 = l_bfix_u_2084___main___rarg(x_6, x_1, x_7, x_2, x_3, x_4, x_5);
|
||||
return x_8;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2084(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
|
||||
_start:
|
||||
{
|
||||
obj* x_5;
|
||||
x_5 = lean::alloc_closure(reinterpret_cast<void*>(l_fix_u_2084___rarg), 6, 0);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2084___rarg___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
|
||||
_start:
|
||||
{
|
||||
obj* x_5;
|
||||
x_5 = l_fix_u_2084___rarg___lambda__1(x_0, x_1, x_2, x_3, x_4);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
lean::dec(x_3);
|
||||
lean::dec(x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2084___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
|
||||
_start:
|
||||
{
|
||||
obj* x_5;
|
||||
x_5 = l_fix_u_2084(x_0, x_1, x_2, x_3, x_4);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
lean::dec(x_3);
|
||||
lean::dec(x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2085___main___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7) {
|
||||
_start:
|
||||
{
|
||||
obj* x_8; uint8 x_9;
|
||||
x_8 = lean::mk_nat_obj(0u);
|
||||
x_9 = lean::nat_dec_eq(x_2, x_8);
|
||||
if (x_9 == 0)
|
||||
{
|
||||
obj* x_10; obj* x_11; obj* x_13; obj* x_14;
|
||||
x_10 = lean::mk_nat_obj(1u);
|
||||
x_11 = lean::nat_sub(x_2, x_10);
|
||||
lean::inc(x_1);
|
||||
x_13 = lean::alloc_closure(reinterpret_cast<void*>(l_bfix_u_2085___main___rarg___boxed), 8, 3);
|
||||
lean::closure_set(x_13, 0, x_0);
|
||||
lean::closure_set(x_13, 1, x_1);
|
||||
lean::closure_set(x_13, 2, x_11);
|
||||
x_14 = lean::apply_6(x_1, x_13, x_3, x_4, x_5, x_6, x_7);
|
||||
return x_14;
|
||||
}
|
||||
else
|
||||
{
|
||||
obj* x_16;
|
||||
lean::dec(x_1);
|
||||
x_16 = lean::apply_5(x_0, x_3, x_4, x_5, x_6, x_7);
|
||||
return x_16;
|
||||
}
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2085___main(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
|
||||
_start:
|
||||
{
|
||||
obj* x_6;
|
||||
x_6 = lean::alloc_closure(reinterpret_cast<void*>(l_bfix_u_2085___main___rarg___boxed), 8, 0);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2085___main___rarg___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7) {
|
||||
_start:
|
||||
{
|
||||
obj* x_8;
|
||||
x_8 = l_bfix_u_2085___main___rarg(x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7);
|
||||
lean::dec(x_2);
|
||||
return x_8;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2085___main___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
|
||||
_start:
|
||||
{
|
||||
obj* x_6;
|
||||
x_6 = l_bfix_u_2085___main(x_0, x_1, x_2, x_3, x_4, x_5);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
lean::dec(x_3);
|
||||
lean::dec(x_4);
|
||||
lean::dec(x_5);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2085___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7) {
|
||||
_start:
|
||||
{
|
||||
obj* x_8;
|
||||
x_8 = l_bfix_u_2085___main___rarg(x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7);
|
||||
return x_8;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2085(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
|
||||
_start:
|
||||
{
|
||||
obj* x_6;
|
||||
x_6 = lean::alloc_closure(reinterpret_cast<void*>(l_bfix_u_2085___rarg___boxed), 8, 0);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2085___rarg___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7) {
|
||||
_start:
|
||||
{
|
||||
obj* x_8;
|
||||
x_8 = l_bfix_u_2085___rarg(x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7);
|
||||
lean::dec(x_2);
|
||||
return x_8;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2085___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
|
||||
_start:
|
||||
{
|
||||
obj* x_6;
|
||||
x_6 = l_bfix_u_2085(x_0, x_1, x_2, x_3, x_4, x_5);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
lean::dec(x_3);
|
||||
lean::dec(x_4);
|
||||
lean::dec(x_5);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
obj* l_fix__core_u_2085___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
|
||||
_start:
|
||||
{
|
||||
obj* x_7; obj* x_8;
|
||||
x_7 = l_usize__sz;
|
||||
x_8 = l_bfix_u_2085___main___rarg(x_0, x_1, x_7, x_2, x_3, x_4, x_5, x_6);
|
||||
return x_8;
|
||||
}
|
||||
}
|
||||
obj* l_fix__core_u_2085(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
|
||||
_start:
|
||||
{
|
||||
obj* x_6;
|
||||
x_6 = lean::alloc_closure(reinterpret_cast<void*>(l_fix__core_u_2085___rarg), 7, 0);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
obj* l_fix__core_u_2085___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
|
||||
_start:
|
||||
{
|
||||
obj* x_6;
|
||||
x_6 = l_fix__core_u_2085(x_0, x_1, x_2, x_3, x_4, x_5);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
lean::dec(x_3);
|
||||
lean::dec(x_4);
|
||||
lean::dec(x_5);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2085___rarg___lambda__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
|
||||
_start:
|
||||
{
|
||||
lean::inc(x_0);
|
||||
return x_0;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2085___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
|
||||
_start:
|
||||
{
|
||||
obj* x_7; obj* x_8; obj* x_9;
|
||||
x_7 = lean::alloc_closure(reinterpret_cast<void*>(l_fix_u_2085___rarg___lambda__1___boxed), 6, 1);
|
||||
lean::closure_set(x_7, 0, x_0);
|
||||
x_8 = l_usize__sz;
|
||||
x_9 = l_bfix_u_2085___main___rarg(x_7, x_1, x_8, x_2, x_3, x_4, x_5, x_6);
|
||||
return x_9;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2085(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
|
||||
_start:
|
||||
{
|
||||
obj* x_6;
|
||||
x_6 = lean::alloc_closure(reinterpret_cast<void*>(l_fix_u_2085___rarg), 7, 0);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2085___rarg___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
|
||||
_start:
|
||||
{
|
||||
obj* x_6;
|
||||
x_6 = l_fix_u_2085___rarg___lambda__1(x_0, x_1, x_2, x_3, x_4, x_5);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
lean::dec(x_3);
|
||||
lean::dec(x_4);
|
||||
lean::dec(x_5);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2085___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
|
||||
_start:
|
||||
{
|
||||
obj* x_6;
|
||||
x_6 = l_fix_u_2085(x_0, x_1, x_2, x_3, x_4, x_5);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
lean::dec(x_3);
|
||||
lean::dec(x_4);
|
||||
lean::dec(x_5);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2086___main___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8) {
|
||||
_start:
|
||||
{
|
||||
obj* x_9; uint8 x_10;
|
||||
x_9 = lean::mk_nat_obj(0u);
|
||||
x_10 = lean::nat_dec_eq(x_2, x_9);
|
||||
if (x_10 == 0)
|
||||
{
|
||||
obj* x_11; obj* x_12; obj* x_14; obj* x_15;
|
||||
x_11 = lean::mk_nat_obj(1u);
|
||||
x_12 = lean::nat_sub(x_2, x_11);
|
||||
lean::inc(x_1);
|
||||
x_14 = lean::alloc_closure(reinterpret_cast<void*>(l_bfix_u_2086___main___rarg___boxed), 9, 3);
|
||||
lean::closure_set(x_14, 0, x_0);
|
||||
lean::closure_set(x_14, 1, x_1);
|
||||
lean::closure_set(x_14, 2, x_12);
|
||||
x_15 = lean::apply_7(x_1, x_14, x_3, x_4, x_5, x_6, x_7, x_8);
|
||||
return x_15;
|
||||
}
|
||||
else
|
||||
{
|
||||
obj* x_17;
|
||||
lean::dec(x_1);
|
||||
x_17 = lean::apply_6(x_0, x_3, x_4, x_5, x_6, x_7, x_8);
|
||||
return x_17;
|
||||
}
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2086___main(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
|
||||
_start:
|
||||
{
|
||||
obj* x_7;
|
||||
x_7 = lean::alloc_closure(reinterpret_cast<void*>(l_bfix_u_2086___main___rarg___boxed), 9, 0);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2086___main___rarg___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8) {
|
||||
_start:
|
||||
{
|
||||
obj* x_9;
|
||||
x_9 = l_bfix_u_2086___main___rarg(x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
|
||||
lean::dec(x_2);
|
||||
return x_9;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2086___main___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
|
||||
_start:
|
||||
{
|
||||
obj* x_7;
|
||||
x_7 = l_bfix_u_2086___main(x_0, x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
lean::dec(x_3);
|
||||
lean::dec(x_4);
|
||||
lean::dec(x_5);
|
||||
lean::dec(x_6);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2086___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8) {
|
||||
_start:
|
||||
{
|
||||
obj* x_9;
|
||||
x_9 = l_bfix_u_2086___main___rarg(x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
|
||||
return x_9;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2086(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
|
||||
_start:
|
||||
{
|
||||
obj* x_7;
|
||||
x_7 = lean::alloc_closure(reinterpret_cast<void*>(l_bfix_u_2086___rarg___boxed), 9, 0);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2086___rarg___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8) {
|
||||
_start:
|
||||
{
|
||||
obj* x_9;
|
||||
x_9 = l_bfix_u_2086___rarg(x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
|
||||
lean::dec(x_2);
|
||||
return x_9;
|
||||
}
|
||||
}
|
||||
obj* l_bfix_u_2086___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
|
||||
_start:
|
||||
{
|
||||
obj* x_7;
|
||||
x_7 = l_bfix_u_2086(x_0, x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
lean::dec(x_3);
|
||||
lean::dec(x_4);
|
||||
lean::dec(x_5);
|
||||
lean::dec(x_6);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
obj* l_fix__core_u_2086___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7) {
|
||||
_start:
|
||||
{
|
||||
obj* x_8; obj* x_9;
|
||||
x_8 = l_usize__sz;
|
||||
x_9 = l_bfix_u_2086___main___rarg(x_0, x_1, x_8, x_2, x_3, x_4, x_5, x_6, x_7);
|
||||
return x_9;
|
||||
}
|
||||
}
|
||||
obj* l_fix__core_u_2086(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
|
||||
_start:
|
||||
{
|
||||
obj* x_7;
|
||||
x_7 = lean::alloc_closure(reinterpret_cast<void*>(l_fix__core_u_2086___rarg), 8, 0);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
obj* l_fix__core_u_2086___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
|
||||
_start:
|
||||
{
|
||||
obj* x_7;
|
||||
x_7 = l_fix__core_u_2086(x_0, x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
lean::dec(x_3);
|
||||
lean::dec(x_4);
|
||||
lean::dec(x_5);
|
||||
lean::dec(x_6);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2086___rarg___lambda__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
|
||||
_start:
|
||||
{
|
||||
lean::inc(x_0);
|
||||
return x_0;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2086___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7) {
|
||||
_start:
|
||||
{
|
||||
obj* x_8; obj* x_9; obj* x_10;
|
||||
x_8 = lean::alloc_closure(reinterpret_cast<void*>(l_fix_u_2086___rarg___lambda__1___boxed), 7, 1);
|
||||
lean::closure_set(x_8, 0, x_0);
|
||||
x_9 = l_usize__sz;
|
||||
x_10 = l_bfix_u_2086___main___rarg(x_8, x_1, x_9, x_2, x_3, x_4, x_5, x_6, x_7);
|
||||
return x_10;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2086(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
|
||||
_start:
|
||||
{
|
||||
obj* x_7;
|
||||
x_7 = lean::alloc_closure(reinterpret_cast<void*>(l_fix_u_2086___rarg), 8, 0);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2086___rarg___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
|
||||
_start:
|
||||
{
|
||||
obj* x_7;
|
||||
x_7 = l_fix_u_2086___rarg___lambda__1(x_0, x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
lean::dec(x_3);
|
||||
lean::dec(x_4);
|
||||
lean::dec(x_5);
|
||||
lean::dec(x_6);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
obj* l_fix_u_2086___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
|
||||
_start:
|
||||
{
|
||||
obj* x_7;
|
||||
x_7 = l_fix_u_2086(x_0, x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
lean::dec(x_3);
|
||||
lean::dec(x_4);
|
||||
lean::dec(x_5);
|
||||
lean::dec(x_6);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
void initialize_init_data_uint();
|
||||
static bool _G_initialized = false;
|
||||
void initialize_init_fix() {
|
||||
|
|
|
|||
|
|
@ -102,16 +102,9 @@ class emit_bytecode_fn {
|
|||
} else {
|
||||
#if defined(LEAN_IGNORE_UNKNOWN_DECLS)
|
||||
if (optional<unsigned> arity = get_extern_constant_arity(m_env, fn)) {
|
||||
switch (*arity) {
|
||||
case 1: return *::lean::get_vm_decl(m_env, "not_implemented_1");
|
||||
case 2: return *::lean::get_vm_decl(m_env, "not_implemented_2");
|
||||
case 3: return *::lean::get_vm_decl(m_env, "not_implemented_3");
|
||||
case 4: return *::lean::get_vm_decl(m_env, "not_implemented_4");
|
||||
case 5: return *::lean::get_vm_decl(m_env, "not_implemented_5");
|
||||
case 6: return *::lean::get_vm_decl(m_env, "not_implemented_6");
|
||||
case 7: return *::lean::get_vm_decl(m_env, "not_implemented_7");
|
||||
case 8: return *::lean::get_vm_decl(m_env, "not_implemented_8");
|
||||
}
|
||||
name n("not_implemented");
|
||||
n = n.append_after(*arity);
|
||||
return *::lean::get_vm_decl(m_env, n);
|
||||
}
|
||||
#endif
|
||||
throw_unknown_constant(fn);
|
||||
|
|
|
|||
|
|
@ -3647,7 +3647,7 @@ vm_obj not_implemented_5(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj
|
|||
vm_obj not_implemented_6(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &) { throw exception("not implemented yet"); }
|
||||
vm_obj not_implemented_7(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &) { throw exception("not implemented yet"); }
|
||||
vm_obj not_implemented_8(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &) { throw exception("not implemented yet"); }
|
||||
|
||||
vm_obj not_implemented_N(unsigned, vm_obj const *) { throw exception("not implemented yet"); }
|
||||
|
||||
void initialize_vm_core() {
|
||||
g_vm_index_manager = new vm_index_manager;
|
||||
|
|
@ -3659,14 +3659,19 @@ void initialize_vm_core() {
|
|||
register_trace_class("vm");
|
||||
register_trace_class({"vm", "run"});
|
||||
});
|
||||
DECLARE_VM_BUILTIN(name({"not_implemented_1"}), not_implemented_1);
|
||||
DECLARE_VM_BUILTIN(name({"not_implemented_2"}), not_implemented_2);
|
||||
DECLARE_VM_BUILTIN(name({"not_implemented_3"}), not_implemented_3);
|
||||
DECLARE_VM_BUILTIN(name({"not_implemented_4"}), not_implemented_4);
|
||||
DECLARE_VM_BUILTIN(name({"not_implemented_5"}), not_implemented_5);
|
||||
DECLARE_VM_BUILTIN(name({"not_implemented_6"}), not_implemented_6);
|
||||
DECLARE_VM_BUILTIN(name({"not_implemented_7"}), not_implemented_7);
|
||||
DECLARE_VM_BUILTIN(name({"not_implemented_8"}), not_implemented_8);
|
||||
DECLARE_VM_BUILTIN(name({"not_implemented_1"}), not_implemented_1);
|
||||
DECLARE_VM_BUILTIN(name({"not_implemented_2"}), not_implemented_2);
|
||||
DECLARE_VM_BUILTIN(name({"not_implemented_3"}), not_implemented_3);
|
||||
DECLARE_VM_BUILTIN(name({"not_implemented_4"}), not_implemented_4);
|
||||
DECLARE_VM_BUILTIN(name({"not_implemented_5"}), not_implemented_5);
|
||||
DECLARE_VM_BUILTIN(name({"not_implemented_6"}), not_implemented_6);
|
||||
DECLARE_VM_BUILTIN(name({"not_implemented_7"}), not_implemented_7);
|
||||
DECLARE_VM_BUILTIN(name({"not_implemented_8"}), not_implemented_8);
|
||||
for (unsigned i = 9; i < 32; i++) {
|
||||
name n ("not_implemented");
|
||||
n = n.append_after(i);
|
||||
declare_vm_builtin(n, n.to_string().c_str(), i, not_implemented_N);
|
||||
}
|
||||
}
|
||||
|
||||
void finalize_vm_core() {
|
||||
|
|
|
|||
|
|
@ -1980,6 +1980,81 @@ obj_res fixpoint(obj_arg rec, obj_arg a) {
|
|||
return r;
|
||||
}
|
||||
|
||||
obj_res fixpoint_aux2(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2) {
|
||||
object * k = weak_ptr_to_ptr(weak_k);
|
||||
inc(k);
|
||||
return apply_3(rec, k, a1, a2);
|
||||
}
|
||||
|
||||
obj_res fixpoint2(obj_arg rec, obj_arg a1, obj_arg a2) {
|
||||
object * k = alloc_closure(fixpoint_aux2, 2);
|
||||
inc(rec);
|
||||
closure_set(k, 0, rec);
|
||||
closure_set(k, 1, ptr_to_weak_ptr(k));
|
||||
object * r = apply_3(rec, k, a1, a2);
|
||||
return r;
|
||||
}
|
||||
|
||||
obj_res fixpoint_aux3(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2, obj_arg a3) {
|
||||
object * k = weak_ptr_to_ptr(weak_k);
|
||||
inc(k);
|
||||
return apply_4(rec, k, a1, a2, a3);
|
||||
}
|
||||
|
||||
obj_res fixpoint3(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3) {
|
||||
object * k = alloc_closure(fixpoint_aux3, 2);
|
||||
inc(rec);
|
||||
closure_set(k, 0, rec);
|
||||
closure_set(k, 1, ptr_to_weak_ptr(k));
|
||||
object * r = apply_4(rec, k, a1, a2, a3);
|
||||
return r;
|
||||
}
|
||||
|
||||
obj_res fixpoint_aux4(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4) {
|
||||
object * k = weak_ptr_to_ptr(weak_k);
|
||||
inc(k);
|
||||
return apply_5(rec, k, a1, a2, a3, a4);
|
||||
}
|
||||
|
||||
obj_res fixpoint4(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4) {
|
||||
object * k = alloc_closure(fixpoint_aux4, 2);
|
||||
inc(rec);
|
||||
closure_set(k, 0, rec);
|
||||
closure_set(k, 1, ptr_to_weak_ptr(k));
|
||||
object * r = apply_5(rec, k, a1, a2, a3, a4);
|
||||
return r;
|
||||
}
|
||||
|
||||
obj_res fixpoint_aux5(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5) {
|
||||
object * k = weak_ptr_to_ptr(weak_k);
|
||||
inc(k);
|
||||
return apply_6(rec, k, a1, a2, a3, a4, a5);
|
||||
}
|
||||
|
||||
obj_res fixpoint5(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5) {
|
||||
object * k = alloc_closure(fixpoint_aux5, 2);
|
||||
inc(rec);
|
||||
closure_set(k, 0, rec);
|
||||
closure_set(k, 1, ptr_to_weak_ptr(k));
|
||||
object * r = apply_6(rec, k, a1, a2, a3, a4, a5);
|
||||
return r;
|
||||
}
|
||||
|
||||
obj_res fixpoint_aux6(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5, obj_arg a6) {
|
||||
object * k = weak_ptr_to_ptr(weak_k);
|
||||
inc(k);
|
||||
return apply_7(rec, k, a1, a2, a3, a4, a5, a6);
|
||||
}
|
||||
|
||||
obj_res fixpoint6(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5, obj_arg a6) {
|
||||
object * k = alloc_closure(fixpoint_aux6, 2);
|
||||
inc(rec);
|
||||
closure_set(k, 0, rec);
|
||||
closure_set(k, 1, ptr_to_weak_ptr(k));
|
||||
object * r = apply_7(rec, k, a1, a2, a3, a4, a5, a6);
|
||||
return r;
|
||||
}
|
||||
|
||||
// =======================================
|
||||
// Debugging helper functions
|
||||
|
||||
|
|
|
|||
|
|
@ -621,11 +621,31 @@ inline obj_res alloc_closure(object*(*fun)(object *, object *), unsigned num_fix
|
|||
inline obj_res alloc_closure(object*(*fun)(object *, object *, object *), unsigned num_fixed) {
|
||||
return alloc_closure(reinterpret_cast<void*>(fun), 3, num_fixed);
|
||||
}
|
||||
inline obj_res alloc_closure(object*(*fun)(object *, object *, object *, object *), unsigned num_fixed) {
|
||||
return alloc_closure(reinterpret_cast<void*>(fun), 4, num_fixed);
|
||||
}
|
||||
inline obj_res alloc_closure(object*(*fun)(object *, object *, object *, object *, object *), unsigned num_fixed) {
|
||||
return alloc_closure(reinterpret_cast<void*>(fun), 5, num_fixed);
|
||||
}
|
||||
inline obj_res alloc_closure(object*(*fun)(object *, object *, object *, object *, object *, object *), unsigned num_fixed) {
|
||||
return alloc_closure(reinterpret_cast<void*>(fun), 6, num_fixed);
|
||||
}
|
||||
inline obj_res alloc_closure(object*(*fun)(object *, object *, object *, object *, object *, object *, object *), unsigned num_fixed) {
|
||||
return alloc_closure(reinterpret_cast<void*>(fun), 7, num_fixed);
|
||||
}
|
||||
inline obj_res alloc_closure(object*(*fun)(object *, object *, object *, object *, object *, object *, object *, object *), unsigned num_fixed) {
|
||||
return alloc_closure(reinterpret_cast<void*>(fun), 8, num_fixed);
|
||||
}
|
||||
|
||||
// =======================================
|
||||
// Fixpoint
|
||||
|
||||
obj_res fixpoint(obj_arg rec, obj_arg a);
|
||||
obj_res fixpoint2(obj_arg rec, obj_arg a1, obj_arg a2);
|
||||
obj_res fixpoint3(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3);
|
||||
obj_res fixpoint4(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4);
|
||||
obj_res fixpoint5(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5);
|
||||
obj_res fixpoint6(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5, obj_arg a6);
|
||||
|
||||
// =======================================
|
||||
// Array of objects
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue