From ff3bf508aafaf434a3379e72d174c8965ebab495 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 10 Mar 2019 11:19:02 -0700 Subject: [PATCH] feat(library/init/fix, runtime): add fixpoint2, ..., fixpoint6 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 ``` --- library/init/fix.lean | 66 +- src/boot/init/fix.cpp | 956 +++++++++++++++++++++++++ src/library/compiler/emit_bytecode.cpp | 13 +- src/library/vm/vm.cpp | 23 +- src/runtime/object.cpp | 75 ++ src/runtime/object.h | 20 + 6 files changed, 1130 insertions(+), 23 deletions(-) diff --git a/library/init/fix.lean b/library/init/fix.lean index b8553f03d1..387c2236fd 100644 --- a/library/init/fix.lean +++ b/library/init/fix.lean @@ -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 diff --git a/src/boot/init/fix.cpp b/src/boot/init/fix.cpp index 4218312087..f2faa096d0 100644 --- a/src/boot/init/fix.cpp +++ b/src/boot/init/fix.cpp @@ -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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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() { diff --git a/src/library/compiler/emit_bytecode.cpp b/src/library/compiler/emit_bytecode.cpp index 912dd8ec18..1f4b3ce3c5 100644 --- a/src/library/compiler/emit_bytecode.cpp +++ b/src/library/compiler/emit_bytecode.cpp @@ -102,16 +102,9 @@ class emit_bytecode_fn { } else { #if defined(LEAN_IGNORE_UNKNOWN_DECLS) if (optional 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); diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index ce03d40754..ed94f6ad25 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -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() { diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index f793262421..d8d3c59c22 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -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 diff --git a/src/runtime/object.h b/src/runtime/object.h index e5777d88c5..867e018755 100644 --- a/src/runtime/object.h +++ b/src/runtime/object.h @@ -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(fun), 3, num_fixed); } +inline obj_res alloc_closure(object*(*fun)(object *, object *, object *, object *), unsigned num_fixed) { + return alloc_closure(reinterpret_cast(fun), 4, num_fixed); +} +inline obj_res alloc_closure(object*(*fun)(object *, object *, object *, object *, object *), unsigned num_fixed) { + return alloc_closure(reinterpret_cast(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(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(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(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