From f9f4e6c14bc5736823a493e508328559e6263f0f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 23 May 2019 08:58:16 -0700 Subject: [PATCH] feat(library/init/lean/compiler/ir): add `expandresetreuse` --- library/init/lean/compiler/ir/default.lean | 3 + .../lean/compiler/ir/expandresetreuse.lean | 51 ++ src/library/compiler/compiler.cpp | 1 + src/stage0/CMakeLists.txt | 2 +- src/stage0/init/lean/compiler/ir/default.cpp | 620 +++++++++++------- .../lean/compiler/ir/expandresetreuse.cpp | 523 +++++++++++++++ 6 files changed, 945 insertions(+), 255 deletions(-) create mode 100644 library/init/lean/compiler/ir/expandresetreuse.lean create mode 100644 src/stage0/init/lean/compiler/ir/expandresetreuse.cpp diff --git a/library/init/lean/compiler/ir/default.lean b/library/init/lean/compiler/ir/default.lean index 4cd79a0313..d9daa7f49b 100644 --- a/library/init/lean/compiler/ir/default.lean +++ b/library/init/lean/compiler/ir/default.lean @@ -16,6 +16,7 @@ import init.lean.compiler.ir.checker import init.lean.compiler.ir.borrow import init.lean.compiler.ir.boxing import init.lean.compiler.ir.rc +import init.lean.compiler.ir.expandresetreuse import init.lean.compiler.ir.emitcpp namespace Lean @@ -40,6 +41,8 @@ decls ← explicitBoxing decls, logDecls `boxing decls, decls ← explicitRC decls, logDecls `rc decls, +let decls := decls.hmap Decl.expandResetReuse, +logDecls `expand_reset_reuse decls, checkDecls decls, addDecls decls, pure () diff --git a/library/init/lean/compiler/ir/expandresetreuse.lean b/library/init/lean/compiler/ir/expandresetreuse.lean new file mode 100644 index 0000000000..3d1e7acb0e --- /dev/null +++ b/library/init/lean/compiler/ir/expandresetreuse.lean @@ -0,0 +1,51 @@ +/- +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import init.control.state +import init.control.reader +import init.lean.compiler.ir.compilerm + +namespace Lean +namespace IR +namespace ExpandResetReuse + +/- Return true iff `x` is consumed in all branches of the current block. + Here consumption means the block contains a `dec x` or `reuse x ...`. -/ +partial def consumed (x : VarId) : FnBody → Bool +| (FnBody.vdecl _ _ v b) := + match v with + | Expr.reuse y _ _ _ := x == y || consumed b + | _ := consumed b +| (FnBody.dec y _ _ b) := x == y || consumed b +| (FnBody.case _ _ alts) := alts.any $ λ alt, consumed alt.body +| e := !e.isTerminal && consumed e.body + +partial def expand (bs : Array FnBody) (x : VarId) (n : Nat) (y : VarId) (b : FnBody) : FnBody := +-- dbgTrace ("FOUND " ++ toString x) $ λ _, +reshape bs (FnBody.vdecl x IRType.object (Expr.reset n y) b) + +partial def searchAndExpand : FnBody → Array FnBody → FnBody +| d@(FnBody.vdecl x t (Expr.reset n y) b) bs := + if consumed x b then + expand bs x n y b + else + searchAndExpand b (push bs d) +| (FnBody.case tid x alts) bs := + let alts := alts.hmap $ λ alt, alt.modifyBody $ λ b, searchAndExpand b Array.empty in + reshape bs (FnBody.case tid x alts) +| b bs := + if b.isTerminal then reshape bs b + else searchAndExpand b.body (push bs b) + +end ExpandResetReuse + +/-- (Try to) expand `reset` and `reuse` instructions. -/ +def Decl.expandResetReuse : Decl → Decl +| (Decl.fdecl f xs t b) := Decl.fdecl f xs t (ExpandResetReuse.searchAndExpand b Array.empty) +| other := other + +end IR +end Lean diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp index af47bc0e74..8e039c1ac0 100644 --- a/src/library/compiler/compiler.cpp +++ b/src/library/compiler/compiler.cpp @@ -288,6 +288,7 @@ void initialize_compiler() { register_trace_class({"compiler", "ir", "borrow"}); register_trace_class({"compiler", "ir", "boxing"}); register_trace_class({"compiler", "ir", "rc"}); + register_trace_class({"compiler", "ir", "expand_reset_reuse"}); } void finalize_compiler() { diff --git a/src/stage0/CMakeLists.txt b/src/stage0/CMakeLists.txt index 2eaa264193..bc97c46e7e 100644 --- a/src/stage0/CMakeLists.txt +++ b/src/stage0/CMakeLists.txt @@ -1 +1 @@ -add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/conditional.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/binsearch.cpp ./init/data/array/default.cpp ./init/data/array/qsort.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/bytearray/basic.cpp ./init/data/bytearray/default.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/env_ext.cpp ./init/fix.cpp ./init/io.cpp ./init/lean/compiler/closedtermcache.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/export.cpp ./init/lean/compiler/initattr.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/borrow.cpp ./init/lean/compiler/ir/boxing.cpp ./init/lean/compiler/ir/checker.cpp ./init/lean/compiler/ir/compilerm.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/emitcpp.cpp ./init/lean/compiler/ir/emitutil.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/rc.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/util.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/disjoint_set.cpp ./init/lean/elaborator.cpp ./init/lean/environment.cpp ./init/lean/expander.cpp ./init/lean/expr.cpp ./init/lean/extern.cpp ./init/lean/format.cpp ./init/lean/frontend.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/modifiers.cpp ./init/lean/name.cpp ./init/lean/name_mangling.cpp ./init/lean/options.cpp ./init/lean/parser/basic.cpp ./init/lean/parser/combinators.cpp ./init/lean/parser/command.cpp ./init/lean/parser/declaration.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/module.cpp ./init/lean/parser/notation.cpp ./init/lean/parser/parsec.cpp ./init/lean/parser/pratt.cpp ./init/lean/parser/rec.cpp ./init/lean/parser/stringliteral.cpp ./init/lean/parser/syntax.cpp ./init/lean/parser/term.cpp ./init/lean/parser/token.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/runtime.cpp ./init/lean/smap.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp) +add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/conditional.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/binsearch.cpp ./init/data/array/default.cpp ./init/data/array/qsort.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/bytearray/basic.cpp ./init/data/bytearray/default.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/env_ext.cpp ./init/fix.cpp ./init/io.cpp ./init/lean/compiler/closedtermcache.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/export.cpp ./init/lean/compiler/initattr.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/borrow.cpp ./init/lean/compiler/ir/boxing.cpp ./init/lean/compiler/ir/checker.cpp ./init/lean/compiler/ir/compilerm.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/emitcpp.cpp ./init/lean/compiler/ir/emitutil.cpp ./init/lean/compiler/ir/expandresetreuse.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/rc.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/util.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/disjoint_set.cpp ./init/lean/elaborator.cpp ./init/lean/environment.cpp ./init/lean/expander.cpp ./init/lean/expr.cpp ./init/lean/extern.cpp ./init/lean/format.cpp ./init/lean/frontend.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/modifiers.cpp ./init/lean/name.cpp ./init/lean/name_mangling.cpp ./init/lean/options.cpp ./init/lean/parser/basic.cpp ./init/lean/parser/combinators.cpp ./init/lean/parser/command.cpp ./init/lean/parser/declaration.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/module.cpp ./init/lean/parser/notation.cpp ./init/lean/parser/parsec.cpp ./init/lean/parser/pratt.cpp ./init/lean/parser/rec.cpp ./init/lean/parser/stringliteral.cpp ./init/lean/parser/syntax.cpp ./init/lean/parser/term.cpp ./init/lean/parser/token.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/runtime.cpp ./init/lean/smap.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp) diff --git a/src/stage0/init/lean/compiler/ir/default.cpp b/src/stage0/init/lean/compiler/ir/default.cpp index e469b036c7..624199c248 100644 --- a/src/stage0/init/lean/compiler/ir/default.cpp +++ b/src/stage0/init/lean/compiler/ir/default.cpp @@ -1,6 +1,6 @@ // Lean compiler output // Module: init.lean.compiler.ir.default -// Imports: init.lean.compiler.ir.basic init.lean.compiler.ir.format init.lean.compiler.ir.compilerm init.lean.compiler.ir.pushproj init.lean.compiler.ir.elimdead init.lean.compiler.ir.simpcase init.lean.compiler.ir.resetreuse init.lean.compiler.ir.normids init.lean.compiler.ir.checker init.lean.compiler.ir.borrow init.lean.compiler.ir.boxing init.lean.compiler.ir.rc init.lean.compiler.ir.emitcpp +// Imports: init.lean.compiler.ir.basic init.lean.compiler.ir.format init.lean.compiler.ir.compilerm init.lean.compiler.ir.pushproj init.lean.compiler.ir.elimdead init.lean.compiler.ir.simpcase init.lean.compiler.ir.resetreuse init.lean.compiler.ir.normids init.lean.compiler.ir.checker init.lean.compiler.ir.borrow init.lean.compiler.ir.boxing init.lean.compiler.ir.rc init.lean.compiler.ir.expandresetreuse init.lean.compiler.ir.emitcpp #include "runtime/object.h" #include "runtime/apply.h" typedef lean::object obj; typedef lean::usize usize; @@ -23,6 +23,7 @@ obj* l___private_init_lean_compiler_ir_default_1__compileAux___closed__15; obj* l___private_init_lean_compiler_ir_compilerm_2__logDeclsAux(obj*, obj*, obj*, obj*, obj*); obj* l___private_init_lean_compiler_ir_default_1__compileAux___closed__16; obj* l___private_init_lean_compiler_ir_default_1__compileAux___closed__6; +obj* l_Lean_IR_Decl_expandResetReuse___main(obj*); obj* l_Lean_IR_Decl_pushProj___main(obj*); obj* l___private_init_lean_compiler_ir_default_1__compileAux___closed__11; obj* l___private_init_lean_compiler_ir_default_1__compileAux___closed__14; @@ -45,6 +46,7 @@ obj* l___private_init_lean_compiler_ir_default_1__compileAux___closed__8; obj* l___private_init_lean_compiler_ir_default_1__compileAux___closed__7; obj* l___private_init_lean_compiler_ir_default_1__compileAux___closed__4; obj* l_Lean_IR_Decl_insertResetReuse___main(obj*); +obj* l___private_init_lean_compiler_ir_default_1__compileAux___closed__18; obj* l___private_init_lean_compiler_ir_default_1__compileAux___closed__9; obj* l_Array_hmmapAux___main___at_Lean_IR_inferBorrow___spec__1(obj*, obj*); obj* l___private_init_lean_compiler_ir_default_1__compileAux___closed__13; @@ -53,11 +55,13 @@ namespace ir { obj* compile_core(obj*, obj*, obj*); }} obj* l___private_init_lean_compiler_ir_default_1__compileAux___closed__10; +obj* l___private_init_lean_compiler_ir_default_1__compileAux___closed__17; obj* l_Lean_IR_Decl_simpCase___main(obj*); obj* l_Lean_Name_append___main(obj*, obj*); obj* l_Lean_IR_explicitRC(obj*, obj*, obj*); obj* l_Array_hmmapAux___main___at___private_init_lean_compiler_ir_default_1__compileAux___spec__2(obj*, obj*); obj* l___private_init_lean_compiler_ir_default_1__compileAux___closed__3; +obj* l_Array_hmmapAux___main___at___private_init_lean_compiler_ir_default_1__compileAux___spec__5(obj*, obj*); obj* l_Array_hmmapAux___main___at___private_init_lean_compiler_ir_default_1__compileAux___spec__1(obj*, obj*); obj* l_Lean_IR_explicitBoxing(obj*, obj*, obj*); obj* l___private_init_lean_compiler_ir_default_1__compileAux___closed__12; @@ -177,6 +181,35 @@ goto _start; } } } +obj* l_Array_hmmapAux___main___at___private_init_lean_compiler_ir_default_1__compileAux___spec__5(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; uint8 x_3; +x_2 = lean::array_get_size(x_1); +x_3 = lean::nat_dec_lt(x_0, x_2); +lean::dec(x_2); +if (x_3 == 0) +{ +lean::dec(x_0); +return x_1; +} +else +{ +obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; +x_6 = lean::array_fget(x_1, x_0); +x_7 = l_Lean_IR_ExplicitRC_getDecl___closed__1; +x_8 = lean::array_fset(x_1, x_0, x_7); +x_9 = l_Lean_IR_Decl_expandResetReuse___main(x_6); +x_10 = lean::mk_nat_obj(1ul); +x_11 = lean::nat_add(x_0, x_10); +x_12 = lean::array_fset(x_8, x_0, x_9); +lean::dec(x_0); +x_0 = x_11; +x_1 = x_12; +goto _start; +} +} +} obj* _init_l___private_init_lean_compiler_ir_default_1__compileAux___closed__1() { _start: { @@ -353,6 +386,28 @@ x_2 = lean_name_mk_string(x_0, x_1); return x_2; } } +obj* _init_l___private_init_lean_compiler_ir_default_1__compileAux___closed__17() { +_start: +{ +obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; +x_0 = lean::box(0); +x_1 = lean::mk_string("expand_reset_reuse"); +x_2 = lean_name_mk_string(x_0, x_1); +x_3 = l_Lean_IR_tracePrefixOptionName; +x_4 = l_Lean_Name_append___main(x_3, x_2); +return x_4; +} +} +obj* _init_l___private_init_lean_compiler_ir_default_1__compileAux___closed__18() { +_start: +{ +obj* x_0; obj* x_1; obj* x_2; +x_0 = lean::box(0); +x_1 = lean::mk_string("expand_reset_reuse"); +x_2 = lean_name_mk_string(x_0, x_1); +return x_2; +} +} obj* l___private_init_lean_compiler_ir_default_1__compileAux(obj* x_0, obj* x_1, obj* x_2) { _start: { @@ -623,7 +678,7 @@ lean::inc(x_94); x_104 = l___private_init_lean_compiler_ir_compilerm_2__logDeclsAux(x_100, x_101, x_94, x_1, x_99); if (lean::obj_tag(x_104) == 0) { -obj* x_105; obj* x_107; obj* x_108; obj* x_110; +obj* x_105; obj* x_107; obj* x_108; obj* x_109; obj* x_110; obj* x_111; obj* x_114; x_105 = lean::cnstr_get(x_104, 1); if (lean::is_exclusive(x_104)) { lean::cnstr_release(x_104, 0); @@ -640,394 +695,444 @@ if (lean::is_scalar(x_107)) { } lean::cnstr_set(x_108, 0, x_11); lean::cnstr_set(x_108, 1, x_105); -lean::inc(x_94); -x_110 = l_Array_mforAux___main___at_Lean_IR_checkDecls___spec__1(x_94, x_94, x_13, x_1, x_108); -if (lean::obj_tag(x_110) == 0) +x_109 = l_Array_hmmapAux___main___at___private_init_lean_compiler_ir_default_1__compileAux___spec__5(x_13, x_94); +x_110 = l___private_init_lean_compiler_ir_default_1__compileAux___closed__17; +x_111 = l___private_init_lean_compiler_ir_default_1__compileAux___closed__18; +lean::inc(x_1); +lean::inc(x_109); +x_114 = l___private_init_lean_compiler_ir_compilerm_2__logDeclsAux(x_110, x_111, x_109, x_1, x_108); +if (lean::obj_tag(x_114) == 0) { -obj* x_111; obj* x_113; obj* x_114; obj* x_115; -x_111 = lean::cnstr_get(x_110, 1); -if (lean::is_exclusive(x_110)) { - lean::cnstr_release(x_110, 0); - x_113 = x_110; +obj* x_115; obj* x_117; obj* x_118; obj* x_120; +x_115 = lean::cnstr_get(x_114, 1); +if (lean::is_exclusive(x_114)) { + lean::cnstr_release(x_114, 0); + x_117 = x_114; } else { - lean::inc(x_111); - lean::dec(x_110); - x_113 = lean::box(0); + lean::inc(x_115); + lean::dec(x_114); + x_117 = lean::box(0); } -if (lean::is_scalar(x_113)) { - x_114 = lean::alloc_cnstr(0, 2, 0); +if (lean::is_scalar(x_117)) { + x_118 = lean::alloc_cnstr(0, 2, 0); } else { - x_114 = x_113; + x_118 = x_117; } -lean::cnstr_set(x_114, 0, x_11); -lean::cnstr_set(x_114, 1, x_111); -x_115 = l_Array_mforAux___main___at_Lean_IR_addDecls___spec__1(x_94, x_13, x_1, x_114); +lean::cnstr_set(x_118, 0, x_11); +lean::cnstr_set(x_118, 1, x_115); +lean::inc(x_109); +x_120 = l_Array_mforAux___main___at_Lean_IR_checkDecls___spec__1(x_109, x_109, x_13, x_1, x_118); +if (lean::obj_tag(x_120) == 0) +{ +obj* x_121; obj* x_123; obj* x_124; obj* x_125; +x_121 = lean::cnstr_get(x_120, 1); +if (lean::is_exclusive(x_120)) { + lean::cnstr_release(x_120, 0); + x_123 = x_120; +} else { + lean::inc(x_121); + lean::dec(x_120); + x_123 = lean::box(0); +} +if (lean::is_scalar(x_123)) { + x_124 = lean::alloc_cnstr(0, 2, 0); +} else { + x_124 = x_123; +} +lean::cnstr_set(x_124, 0, x_11); +lean::cnstr_set(x_124, 1, x_121); +x_125 = l_Array_mforAux___main___at_Lean_IR_addDecls___spec__1(x_109, x_13, x_1, x_124); lean::dec(x_1); -lean::dec(x_94); -if (lean::obj_tag(x_115) == 0) +lean::dec(x_109); +if (lean::obj_tag(x_125) == 0) { -obj* x_118; obj* x_120; obj* x_121; -x_118 = lean::cnstr_get(x_115, 1); -if (lean::is_exclusive(x_115)) { - lean::cnstr_release(x_115, 0); - x_120 = x_115; +obj* x_128; obj* x_130; obj* x_131; +x_128 = lean::cnstr_get(x_125, 1); +if (lean::is_exclusive(x_125)) { + lean::cnstr_release(x_125, 0); + x_130 = x_125; } else { - lean::inc(x_118); - lean::dec(x_115); - x_120 = lean::box(0); + lean::inc(x_128); + lean::dec(x_125); + x_130 = lean::box(0); } -if (lean::is_scalar(x_120)) { - x_121 = lean::alloc_cnstr(0, 2, 0); +if (lean::is_scalar(x_130)) { + x_131 = lean::alloc_cnstr(0, 2, 0); } else { - x_121 = x_120; + x_131 = x_130; } -lean::cnstr_set(x_121, 0, x_11); -lean::cnstr_set(x_121, 1, x_118); -return x_121; +lean::cnstr_set(x_131, 0, x_11); +lean::cnstr_set(x_131, 1, x_128); +return x_131; } else { -obj* x_122; obj* x_124; obj* x_126; obj* x_127; -x_122 = lean::cnstr_get(x_115, 0); -x_124 = lean::cnstr_get(x_115, 1); -if (lean::is_exclusive(x_115)) { - x_126 = x_115; +obj* x_132; obj* x_134; obj* x_136; obj* x_137; +x_132 = lean::cnstr_get(x_125, 0); +x_134 = lean::cnstr_get(x_125, 1); +if (lean::is_exclusive(x_125)) { + x_136 = x_125; } else { - lean::inc(x_122); - lean::inc(x_124); - lean::dec(x_115); - x_126 = lean::box(0); -} -if (lean::is_scalar(x_126)) { - x_127 = lean::alloc_cnstr(1, 2, 0); -} else { - x_127 = x_126; -} -lean::cnstr_set(x_127, 0, x_122); -lean::cnstr_set(x_127, 1, x_124); -return x_127; -} -} -else -{ -obj* x_130; obj* x_132; obj* x_134; obj* x_135; -lean::dec(x_1); -lean::dec(x_94); -x_130 = lean::cnstr_get(x_110, 0); -x_132 = lean::cnstr_get(x_110, 1); -if (lean::is_exclusive(x_110)) { - x_134 = x_110; -} else { - lean::inc(x_130); lean::inc(x_132); - lean::dec(x_110); - x_134 = lean::box(0); + lean::inc(x_134); + lean::dec(x_125); + x_136 = lean::box(0); } -if (lean::is_scalar(x_134)) { - x_135 = lean::alloc_cnstr(1, 2, 0); +if (lean::is_scalar(x_136)) { + x_137 = lean::alloc_cnstr(1, 2, 0); } else { - x_135 = x_134; + x_137 = x_136; } -lean::cnstr_set(x_135, 0, x_130); -lean::cnstr_set(x_135, 1, x_132); -return x_135; +lean::cnstr_set(x_137, 0, x_132); +lean::cnstr_set(x_137, 1, x_134); +return x_137; } } else { -obj* x_138; obj* x_140; obj* x_142; obj* x_143; +obj* x_140; obj* x_142; obj* x_144; obj* x_145; +lean::dec(x_1); +lean::dec(x_109); +x_140 = lean::cnstr_get(x_120, 0); +x_142 = lean::cnstr_get(x_120, 1); +if (lean::is_exclusive(x_120)) { + x_144 = x_120; +} else { + lean::inc(x_140); + lean::inc(x_142); + lean::dec(x_120); + x_144 = lean::box(0); +} +if (lean::is_scalar(x_144)) { + x_145 = lean::alloc_cnstr(1, 2, 0); +} else { + x_145 = x_144; +} +lean::cnstr_set(x_145, 0, x_140); +lean::cnstr_set(x_145, 1, x_142); +return x_145; +} +} +else +{ +obj* x_148; obj* x_150; obj* x_152; obj* x_153; +lean::dec(x_1); +lean::dec(x_109); +x_148 = lean::cnstr_get(x_114, 0); +x_150 = lean::cnstr_get(x_114, 1); +if (lean::is_exclusive(x_114)) { + x_152 = x_114; +} else { + lean::inc(x_148); + lean::inc(x_150); + lean::dec(x_114); + x_152 = lean::box(0); +} +if (lean::is_scalar(x_152)) { + x_153 = lean::alloc_cnstr(1, 2, 0); +} else { + x_153 = x_152; +} +lean::cnstr_set(x_153, 0, x_148); +lean::cnstr_set(x_153, 1, x_150); +return x_153; +} +} +else +{ +obj* x_156; obj* x_158; obj* x_160; obj* x_161; lean::dec(x_1); lean::dec(x_94); -x_138 = lean::cnstr_get(x_104, 0); -x_140 = lean::cnstr_get(x_104, 1); +x_156 = lean::cnstr_get(x_104, 0); +x_158 = lean::cnstr_get(x_104, 1); if (lean::is_exclusive(x_104)) { - x_142 = x_104; + x_160 = x_104; } else { - lean::inc(x_138); - lean::inc(x_140); + lean::inc(x_156); + lean::inc(x_158); lean::dec(x_104); - x_142 = lean::box(0); + x_160 = lean::box(0); } -if (lean::is_scalar(x_142)) { - x_143 = lean::alloc_cnstr(1, 2, 0); +if (lean::is_scalar(x_160)) { + x_161 = lean::alloc_cnstr(1, 2, 0); } else { - x_143 = x_142; + x_161 = x_160; } -lean::cnstr_set(x_143, 0, x_138); -lean::cnstr_set(x_143, 1, x_140); -return x_143; +lean::cnstr_set(x_161, 0, x_156); +lean::cnstr_set(x_161, 1, x_158); +return x_161; } } else { -obj* x_145; obj* x_147; obj* x_149; obj* x_150; +obj* x_163; obj* x_165; obj* x_167; obj* x_168; lean::dec(x_1); -x_145 = lean::cnstr_get(x_93, 0); -x_147 = lean::cnstr_get(x_93, 1); +x_163 = lean::cnstr_get(x_93, 0); +x_165 = lean::cnstr_get(x_93, 1); if (lean::is_exclusive(x_93)) { - x_149 = x_93; + x_167 = x_93; } else { - lean::inc(x_145); - lean::inc(x_147); + lean::inc(x_163); + lean::inc(x_165); lean::dec(x_93); - x_149 = lean::box(0); + x_167 = lean::box(0); } -if (lean::is_scalar(x_149)) { - x_150 = lean::alloc_cnstr(1, 2, 0); +if (lean::is_scalar(x_167)) { + x_168 = lean::alloc_cnstr(1, 2, 0); } else { - x_150 = x_149; + x_168 = x_167; } -lean::cnstr_set(x_150, 0, x_145); -lean::cnstr_set(x_150, 1, x_147); -return x_150; +lean::cnstr_set(x_168, 0, x_163); +lean::cnstr_set(x_168, 1, x_165); +return x_168; } } else { -obj* x_153; obj* x_155; obj* x_157; obj* x_158; +obj* x_171; obj* x_173; obj* x_175; obj* x_176; lean::dec(x_1); lean::dec(x_78); -x_153 = lean::cnstr_get(x_88, 0); -x_155 = lean::cnstr_get(x_88, 1); +x_171 = lean::cnstr_get(x_88, 0); +x_173 = lean::cnstr_get(x_88, 1); if (lean::is_exclusive(x_88)) { - x_157 = x_88; + x_175 = x_88; } else { - lean::inc(x_153); - lean::inc(x_155); + lean::inc(x_171); + lean::inc(x_173); lean::dec(x_88); - x_157 = lean::box(0); + x_175 = lean::box(0); } -if (lean::is_scalar(x_157)) { - x_158 = lean::alloc_cnstr(1, 2, 0); +if (lean::is_scalar(x_175)) { + x_176 = lean::alloc_cnstr(1, 2, 0); } else { - x_158 = x_157; + x_176 = x_175; } -lean::cnstr_set(x_158, 0, x_153); -lean::cnstr_set(x_158, 1, x_155); -return x_158; +lean::cnstr_set(x_176, 0, x_171); +lean::cnstr_set(x_176, 1, x_173); +return x_176; } } else { -obj* x_160; obj* x_162; obj* x_164; obj* x_165; +obj* x_178; obj* x_180; obj* x_182; obj* x_183; lean::dec(x_1); -x_160 = lean::cnstr_get(x_77, 0); -x_162 = lean::cnstr_get(x_77, 1); +x_178 = lean::cnstr_get(x_77, 0); +x_180 = lean::cnstr_get(x_77, 1); if (lean::is_exclusive(x_77)) { - x_164 = x_77; + x_182 = x_77; } else { - lean::inc(x_160); - lean::inc(x_162); + lean::inc(x_178); + lean::inc(x_180); lean::dec(x_77); - x_164 = lean::box(0); + x_182 = lean::box(0); } -if (lean::is_scalar(x_164)) { - x_165 = lean::alloc_cnstr(1, 2, 0); +if (lean::is_scalar(x_182)) { + x_183 = lean::alloc_cnstr(1, 2, 0); } else { - x_165 = x_164; + x_183 = x_182; } -lean::cnstr_set(x_165, 0, x_160); -lean::cnstr_set(x_165, 1, x_162); -return x_165; +lean::cnstr_set(x_183, 0, x_178); +lean::cnstr_set(x_183, 1, x_180); +return x_183; } } else { -obj* x_168; obj* x_170; obj* x_172; obj* x_173; +obj* x_186; obj* x_188; obj* x_190; obj* x_191; lean::dec(x_1); lean::dec(x_62); -x_168 = lean::cnstr_get(x_72, 0); -x_170 = lean::cnstr_get(x_72, 1); +x_186 = lean::cnstr_get(x_72, 0); +x_188 = lean::cnstr_get(x_72, 1); if (lean::is_exclusive(x_72)) { - x_172 = x_72; + x_190 = x_72; } else { - lean::inc(x_168); - lean::inc(x_170); + lean::inc(x_186); + lean::inc(x_188); lean::dec(x_72); - x_172 = lean::box(0); + x_190 = lean::box(0); } -if (lean::is_scalar(x_172)) { - x_173 = lean::alloc_cnstr(1, 2, 0); +if (lean::is_scalar(x_190)) { + x_191 = lean::alloc_cnstr(1, 2, 0); } else { - x_173 = x_172; + x_191 = x_190; } -lean::cnstr_set(x_173, 0, x_168); -lean::cnstr_set(x_173, 1, x_170); -return x_173; +lean::cnstr_set(x_191, 0, x_186); +lean::cnstr_set(x_191, 1, x_188); +return x_191; } } else { -obj* x_175; obj* x_177; obj* x_179; obj* x_180; +obj* x_193; obj* x_195; obj* x_197; obj* x_198; lean::dec(x_1); -x_175 = lean::cnstr_get(x_61, 0); -x_177 = lean::cnstr_get(x_61, 1); +x_193 = lean::cnstr_get(x_61, 0); +x_195 = lean::cnstr_get(x_61, 1); if (lean::is_exclusive(x_61)) { - x_179 = x_61; + x_197 = x_61; } else { - lean::inc(x_175); - lean::inc(x_177); + lean::inc(x_193); + lean::inc(x_195); lean::dec(x_61); - x_179 = lean::box(0); + x_197 = lean::box(0); } -if (lean::is_scalar(x_179)) { - x_180 = lean::alloc_cnstr(1, 2, 0); +if (lean::is_scalar(x_197)) { + x_198 = lean::alloc_cnstr(1, 2, 0); } else { - x_180 = x_179; + x_198 = x_197; } -lean::cnstr_set(x_180, 0, x_175); -lean::cnstr_set(x_180, 1, x_177); -return x_180; +lean::cnstr_set(x_198, 0, x_193); +lean::cnstr_set(x_198, 1, x_195); +return x_198; } } else { -obj* x_183; obj* x_185; obj* x_187; obj* x_188; +obj* x_201; obj* x_203; obj* x_205; obj* x_206; lean::dec(x_1); lean::dec(x_50); -x_183 = lean::cnstr_get(x_55, 0); -x_185 = lean::cnstr_get(x_55, 1); +x_201 = lean::cnstr_get(x_55, 0); +x_203 = lean::cnstr_get(x_55, 1); if (lean::is_exclusive(x_55)) { - x_187 = x_55; + x_205 = x_55; } else { - lean::inc(x_183); - lean::inc(x_185); + lean::inc(x_201); + lean::inc(x_203); lean::dec(x_55); - x_187 = lean::box(0); + x_205 = lean::box(0); } -if (lean::is_scalar(x_187)) { - x_188 = lean::alloc_cnstr(1, 2, 0); +if (lean::is_scalar(x_205)) { + x_206 = lean::alloc_cnstr(1, 2, 0); } else { - x_188 = x_187; + x_206 = x_205; } -lean::cnstr_set(x_188, 0, x_183); -lean::cnstr_set(x_188, 1, x_185); -return x_188; +lean::cnstr_set(x_206, 0, x_201); +lean::cnstr_set(x_206, 1, x_203); +return x_206; } } else { -obj* x_191; obj* x_193; obj* x_195; obj* x_196; +obj* x_209; obj* x_211; obj* x_213; obj* x_214; lean::dec(x_1); lean::dec(x_40); -x_191 = lean::cnstr_get(x_45, 0); -x_193 = lean::cnstr_get(x_45, 1); +x_209 = lean::cnstr_get(x_45, 0); +x_211 = lean::cnstr_get(x_45, 1); if (lean::is_exclusive(x_45)) { - x_195 = x_45; + x_213 = x_45; } else { - lean::inc(x_191); - lean::inc(x_193); + lean::inc(x_209); + lean::inc(x_211); lean::dec(x_45); - x_195 = lean::box(0); + x_213 = lean::box(0); } -if (lean::is_scalar(x_195)) { - x_196 = lean::alloc_cnstr(1, 2, 0); +if (lean::is_scalar(x_213)) { + x_214 = lean::alloc_cnstr(1, 2, 0); } else { - x_196 = x_195; + x_214 = x_213; } -lean::cnstr_set(x_196, 0, x_191); -lean::cnstr_set(x_196, 1, x_193); -return x_196; +lean::cnstr_set(x_214, 0, x_209); +lean::cnstr_set(x_214, 1, x_211); +return x_214; } } else { -obj* x_199; obj* x_201; obj* x_203; obj* x_204; +obj* x_217; obj* x_219; obj* x_221; obj* x_222; lean::dec(x_1); lean::dec(x_30); -x_199 = lean::cnstr_get(x_35, 0); -x_201 = lean::cnstr_get(x_35, 1); +x_217 = lean::cnstr_get(x_35, 0); +x_219 = lean::cnstr_get(x_35, 1); if (lean::is_exclusive(x_35)) { - x_203 = x_35; + x_221 = x_35; } else { - lean::inc(x_199); - lean::inc(x_201); + lean::inc(x_217); + lean::inc(x_219); lean::dec(x_35); - x_203 = lean::box(0); + x_221 = lean::box(0); } -if (lean::is_scalar(x_203)) { - x_204 = lean::alloc_cnstr(1, 2, 0); +if (lean::is_scalar(x_221)) { + x_222 = lean::alloc_cnstr(1, 2, 0); } else { - x_204 = x_203; + x_222 = x_221; } -lean::cnstr_set(x_204, 0, x_199); -lean::cnstr_set(x_204, 1, x_201); -return x_204; +lean::cnstr_set(x_222, 0, x_217); +lean::cnstr_set(x_222, 1, x_219); +return x_222; } } else { -obj* x_207; obj* x_209; obj* x_211; obj* x_212; +obj* x_225; obj* x_227; obj* x_229; obj* x_230; lean::dec(x_1); lean::dec(x_20); -x_207 = lean::cnstr_get(x_25, 0); -x_209 = lean::cnstr_get(x_25, 1); +x_225 = lean::cnstr_get(x_25, 0); +x_227 = lean::cnstr_get(x_25, 1); if (lean::is_exclusive(x_25)) { - x_211 = x_25; + x_229 = x_25; } else { - lean::inc(x_207); - lean::inc(x_209); - lean::dec(x_25); - x_211 = lean::box(0); -} -if (lean::is_scalar(x_211)) { - x_212 = lean::alloc_cnstr(1, 2, 0); -} else { - x_212 = x_211; -} -lean::cnstr_set(x_212, 0, x_207); -lean::cnstr_set(x_212, 1, x_209); -return x_212; -} -} -else -{ -obj* x_215; obj* x_217; obj* x_219; obj* x_220; -lean::dec(x_1); -lean::dec(x_0); -x_215 = lean::cnstr_get(x_15, 0); -x_217 = lean::cnstr_get(x_15, 1); -if (lean::is_exclusive(x_15)) { - x_219 = x_15; -} else { - lean::inc(x_215); - lean::inc(x_217); - lean::dec(x_15); - x_219 = lean::box(0); -} -if (lean::is_scalar(x_219)) { - x_220 = lean::alloc_cnstr(1, 2, 0); -} else { - x_220 = x_219; -} -lean::cnstr_set(x_220, 0, x_215); -lean::cnstr_set(x_220, 1, x_217); -return x_220; -} -} -else -{ -obj* x_223; obj* x_225; obj* x_227; obj* x_228; -lean::dec(x_1); -lean::dec(x_0); -x_223 = lean::cnstr_get(x_7, 0); -x_225 = lean::cnstr_get(x_7, 1); -if (lean::is_exclusive(x_7)) { - x_227 = x_7; -} else { - lean::inc(x_223); lean::inc(x_225); - lean::dec(x_7); - x_227 = lean::box(0); + lean::inc(x_227); + lean::dec(x_25); + x_229 = lean::box(0); } -if (lean::is_scalar(x_227)) { - x_228 = lean::alloc_cnstr(1, 2, 0); +if (lean::is_scalar(x_229)) { + x_230 = lean::alloc_cnstr(1, 2, 0); } else { - x_228 = x_227; + x_230 = x_229; } -lean::cnstr_set(x_228, 0, x_223); -lean::cnstr_set(x_228, 1, x_225); -return x_228; +lean::cnstr_set(x_230, 0, x_225); +lean::cnstr_set(x_230, 1, x_227); +return x_230; +} +} +else +{ +obj* x_233; obj* x_235; obj* x_237; obj* x_238; +lean::dec(x_1); +lean::dec(x_0); +x_233 = lean::cnstr_get(x_15, 0); +x_235 = lean::cnstr_get(x_15, 1); +if (lean::is_exclusive(x_15)) { + x_237 = x_15; +} else { + lean::inc(x_233); + lean::inc(x_235); + lean::dec(x_15); + x_237 = lean::box(0); +} +if (lean::is_scalar(x_237)) { + x_238 = lean::alloc_cnstr(1, 2, 0); +} else { + x_238 = x_237; +} +lean::cnstr_set(x_238, 0, x_233); +lean::cnstr_set(x_238, 1, x_235); +return x_238; +} +} +else +{ +obj* x_241; obj* x_243; obj* x_245; obj* x_246; +lean::dec(x_1); +lean::dec(x_0); +x_241 = lean::cnstr_get(x_7, 0); +x_243 = lean::cnstr_get(x_7, 1); +if (lean::is_exclusive(x_7)) { + x_245 = x_7; +} else { + lean::inc(x_241); + lean::inc(x_243); + lean::dec(x_7); + x_245 = lean::box(0); +} +if (lean::is_scalar(x_245)) { + x_246 = lean::alloc_cnstr(1, 2, 0); +} else { + x_246 = x_245; +} +lean::cnstr_set(x_246, 0, x_241); +lean::cnstr_set(x_246, 1, x_243); +return x_246; } } } @@ -1097,6 +1202,7 @@ obj* initialize_init_lean_compiler_ir_checker(obj*); obj* initialize_init_lean_compiler_ir_borrow(obj*); obj* initialize_init_lean_compiler_ir_boxing(obj*); obj* initialize_init_lean_compiler_ir_rc(obj*); +obj* initialize_init_lean_compiler_ir_expandresetreuse(obj*); obj* initialize_init_lean_compiler_ir_emitcpp(obj*); static bool _G_initialized = false; obj* initialize_init_lean_compiler_ir_default(obj* w) { @@ -1127,6 +1233,8 @@ w = initialize_init_lean_compiler_ir_boxing(w); if (io_result_is_error(w)) return w; w = initialize_init_lean_compiler_ir_rc(w); if (io_result_is_error(w)) return w; +w = initialize_init_lean_compiler_ir_expandresetreuse(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_compiler_ir_emitcpp(w); if (io_result_is_error(w)) return w; l___private_init_lean_compiler_ir_default_1__compileAux___closed__1 = _init_l___private_init_lean_compiler_ir_default_1__compileAux___closed__1(); @@ -1161,5 +1269,9 @@ lean::mark_persistent(l___private_init_lean_compiler_ir_default_1__compileAux___ lean::mark_persistent(l___private_init_lean_compiler_ir_default_1__compileAux___closed__15); l___private_init_lean_compiler_ir_default_1__compileAux___closed__16 = _init_l___private_init_lean_compiler_ir_default_1__compileAux___closed__16(); lean::mark_persistent(l___private_init_lean_compiler_ir_default_1__compileAux___closed__16); + l___private_init_lean_compiler_ir_default_1__compileAux___closed__17 = _init_l___private_init_lean_compiler_ir_default_1__compileAux___closed__17(); +lean::mark_persistent(l___private_init_lean_compiler_ir_default_1__compileAux___closed__17); + l___private_init_lean_compiler_ir_default_1__compileAux___closed__18 = _init_l___private_init_lean_compiler_ir_default_1__compileAux___closed__18(); +lean::mark_persistent(l___private_init_lean_compiler_ir_default_1__compileAux___closed__18); return w; } diff --git a/src/stage0/init/lean/compiler/ir/expandresetreuse.cpp b/src/stage0/init/lean/compiler/ir/expandresetreuse.cpp new file mode 100644 index 0000000000..ac32f6065b --- /dev/null +++ b/src/stage0/init/lean/compiler/ir/expandresetreuse.cpp @@ -0,0 +1,523 @@ +// Lean compiler output +// Module: init.lean.compiler.ir.expandresetreuse +// Imports: init.control.state init.control.reader init.lean.compiler.ir.compilerm +#include "runtime/object.h" +#include "runtime/apply.h" +typedef lean::object obj; typedef lean::usize usize; +typedef lean::uint8 uint8; typedef lean::uint16 uint16; +typedef lean::uint32 uint32; typedef lean::uint64 uint64; +#if defined(__clang__) +#pragma clang diagnostic ignored "-Wunused-parameter" +#pragma clang diagnostic ignored "-Wunused-label" +#elif defined(__GNUC__) && !defined(__CLANG__) +#pragma GCC diagnostic ignored "-Wunused-parameter" +#pragma GCC diagnostic ignored "-Wunused-label" +#pragma GCC diagnostic ignored "-Wunused-but-set-variable" +#endif +obj* l_Lean_IR_Decl_expandResetReuse(obj*); +extern obj* l_Array_empty___closed__1; +obj* l_Lean_IR_ExpandResetReuse_searchAndExpand___main(obj*, obj*); +obj* l_Lean_IR_Decl_expandResetReuse___main(obj*); +obj* l_Lean_IR_ExpandResetReuse_expand(obj*, obj*, obj*, obj*, obj*); +obj* l_Lean_IR_reshape(obj*, obj*); +uint8 l_Lean_IR_ExpandResetReuse_consumed(obj*, obj*); +obj* l_Lean_IR_ExpandResetReuse_consumed___boxed(obj*, obj*); +namespace lean { +uint8 nat_dec_lt(obj*, obj*); +} +uint8 l_Lean_IR_FnBody_isTerminal___main(obj*); +obj* l_Lean_IR_ExpandResetReuse_searchAndExpand(obj*, obj*); +obj* l_Array_hmmapAux___main___at_Lean_IR_ExpandResetReuse_searchAndExpand___main___spec__1___closed__1; +namespace lean { +obj* nat_add(obj*, obj*); +} +namespace lean { +uint8 nat_dec_eq(obj*, obj*); +} +uint8 l_Lean_IR_ExpandResetReuse_consumed___main(obj*, obj*); +obj* l_Lean_IR_AltCore_body___main(obj*); +obj* l_Array_anyMAux___main___at_Lean_IR_ExpandResetReuse_consumed___main___spec__1___boxed(obj*, obj*, obj*); +obj* l_Lean_IR_ExpandResetReuse_consumed___main___boxed(obj*, obj*); +obj* l_Lean_IR_FnBody_body___main(obj*); +obj* l_Lean_IR_push(obj*, obj*); +uint8 l_Array_anyMAux___main___at_Lean_IR_ExpandResetReuse_consumed___main___spec__1(obj*, obj*, obj*); +obj* l_Array_hmmapAux___main___at_Lean_IR_ExpandResetReuse_searchAndExpand___main___spec__1(obj*, obj*); +uint8 l_Array_anyMAux___main___at_Lean_IR_ExpandResetReuse_consumed___main___spec__1(obj* x_0, obj* x_1, obj* x_2) { +_start: +{ +obj* x_3; uint8 x_4; +x_3 = lean::array_get_size(x_1); +x_4 = lean::nat_dec_lt(x_2, x_3); +lean::dec(x_3); +if (x_4 == 0) +{ +uint8 x_7; +lean::dec(x_2); +x_7 = 0; +return x_7; +} +else +{ +obj* x_8; obj* x_9; uint8 x_11; +x_8 = lean::array_fget(x_1, x_2); +x_9 = l_Lean_IR_AltCore_body___main(x_8); +lean::dec(x_8); +x_11 = l_Lean_IR_ExpandResetReuse_consumed___main(x_0, x_9); +if (x_11 == 0) +{ +obj* x_12; obj* x_13; +x_12 = lean::mk_nat_obj(1ul); +x_13 = lean::nat_add(x_2, x_12); +lean::dec(x_2); +x_2 = x_13; +goto _start; +} +else +{ +lean::dec(x_2); +return x_11; +} +} +} +} +uint8 l_Lean_IR_ExpandResetReuse_consumed___main(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +switch (lean::obj_tag(x_1)) { +case 0: +{ +obj* x_4; +x_4 = lean::cnstr_get(x_1, 1); +lean::inc(x_4); +switch (lean::obj_tag(x_4)) { +case 2: +{ +obj* x_6; obj* x_9; uint8 x_12; +x_6 = lean::cnstr_get(x_1, 2); +lean::inc(x_6); +lean::dec(x_1); +x_9 = lean::cnstr_get(x_4, 0); +lean::inc(x_9); +lean::dec(x_4); +x_12 = lean::nat_dec_eq(x_0, x_9); +lean::dec(x_9); +if (x_12 == 0) +{ +x_1 = x_6; +goto _start; +} +else +{ +uint8 x_16; +lean::dec(x_6); +x_16 = 1; +return x_16; +} +} +default: +{ +obj* x_18; +lean::dec(x_4); +x_18 = lean::cnstr_get(x_1, 2); +lean::inc(x_18); +lean::dec(x_1); +x_1 = x_18; +goto _start; +} +} +} +case 7: +{ +obj* x_22; obj* x_24; uint8 x_27; +x_22 = lean::cnstr_get(x_1, 0); +lean::inc(x_22); +x_24 = lean::cnstr_get(x_1, 2); +lean::inc(x_24); +lean::dec(x_1); +x_27 = lean::nat_dec_eq(x_0, x_22); +lean::dec(x_22); +if (x_27 == 0) +{ +x_1 = x_24; +goto _start; +} +else +{ +uint8 x_31; +lean::dec(x_24); +x_31 = 1; +return x_31; +} +} +case 10: +{ +obj* x_32; obj* x_35; uint8 x_36; +x_32 = lean::cnstr_get(x_1, 2); +lean::inc(x_32); +lean::dec(x_1); +x_35 = lean::mk_nat_obj(0ul); +x_36 = l_Array_anyMAux___main___at_Lean_IR_ExpandResetReuse_consumed___main___spec__1(x_0, x_32, x_35); +lean::dec(x_32); +return x_36; +} +default: +{ +obj* x_38; +x_38 = lean::box(0); +x_2 = x_38; +goto lbl_3; +} +} +lbl_3: +{ +uint8 x_40; +lean::dec(x_2); +x_40 = l_Lean_IR_FnBody_isTerminal___main(x_1); +if (x_40 == 0) +{ +obj* x_41; +x_41 = l_Lean_IR_FnBody_body___main(x_1); +lean::dec(x_1); +x_1 = x_41; +goto _start; +} +else +{ +uint8 x_45; +lean::dec(x_1); +x_45 = 0; +return x_45; +} +} +} +} +obj* l_Array_anyMAux___main___at_Lean_IR_ExpandResetReuse_consumed___main___spec__1___boxed(obj* x_0, obj* x_1, obj* x_2) { +_start: +{ +uint8 x_3; obj* x_4; +x_3 = l_Array_anyMAux___main___at_Lean_IR_ExpandResetReuse_consumed___main___spec__1(x_0, x_1, x_2); +x_4 = lean::box(x_3); +lean::dec(x_0); +lean::dec(x_1); +return x_4; +} +} +obj* l_Lean_IR_ExpandResetReuse_consumed___main___boxed(obj* x_0, obj* x_1) { +_start: +{ +uint8 x_2; obj* x_3; +x_2 = l_Lean_IR_ExpandResetReuse_consumed___main(x_0, x_1); +x_3 = lean::box(x_2); +lean::dec(x_0); +return x_3; +} +} +uint8 l_Lean_IR_ExpandResetReuse_consumed(obj* x_0, obj* x_1) { +_start: +{ +uint8 x_2; +x_2 = l_Lean_IR_ExpandResetReuse_consumed___main(x_0, x_1); +return x_2; +} +} +obj* l_Lean_IR_ExpandResetReuse_consumed___boxed(obj* x_0, obj* x_1) { +_start: +{ +uint8 x_2; obj* x_3; +x_2 = l_Lean_IR_ExpandResetReuse_consumed(x_0, x_1); +x_3 = lean::box(x_2); +lean::dec(x_0); +return x_3; +} +} +obj* l_Lean_IR_ExpandResetReuse_expand(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) { +_start: +{ +obj* x_5; uint8 x_6; obj* x_7; obj* x_8; obj* x_9; +x_5 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_5, 0, x_2); +lean::cnstr_set(x_5, 1, x_3); +x_6 = 7; +x_7 = lean::alloc_cnstr(0, 3, 1); +lean::cnstr_set(x_7, 0, x_1); +lean::cnstr_set(x_7, 1, x_5); +lean::cnstr_set(x_7, 2, x_4); +lean::cnstr_set_scalar(x_7, sizeof(void*)*3, x_6); +x_8 = x_7; +x_9 = l_Lean_IR_reshape(x_0, x_8); +return x_9; +} +} +obj* _init_l_Array_hmmapAux___main___at_Lean_IR_ExpandResetReuse_searchAndExpand___main___spec__1___closed__1() { +_start: +{ +obj* x_0; obj* x_1; +x_0 = lean::box(13); +x_1 = lean::alloc_cnstr(1, 1, 0); +lean::cnstr_set(x_1, 0, x_0); +return x_1; +} +} +obj* l_Array_hmmapAux___main___at_Lean_IR_ExpandResetReuse_searchAndExpand___main___spec__1(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; uint8 x_3; +x_2 = lean::array_get_size(x_1); +x_3 = lean::nat_dec_lt(x_0, x_2); +lean::dec(x_2); +if (x_3 == 0) +{ +lean::dec(x_0); +return x_1; +} +else +{ +obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; +x_6 = lean::array_fget(x_1, x_0); +x_7 = l_Array_hmmapAux___main___at_Lean_IR_ExpandResetReuse_searchAndExpand___main___spec__1___closed__1; +x_8 = lean::array_fset(x_1, x_0, x_7); +x_9 = lean::mk_nat_obj(1ul); +x_10 = lean::nat_add(x_0, x_9); +if (lean::obj_tag(x_6) == 0) +{ +obj* x_11; obj* x_13; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; +x_11 = lean::cnstr_get(x_6, 0); +x_13 = lean::cnstr_get(x_6, 1); +if (lean::is_exclusive(x_6)) { + x_15 = x_6; +} else { + lean::inc(x_11); + lean::inc(x_13); + lean::dec(x_6); + x_15 = lean::box(0); +} +x_16 = l_Array_empty___closed__1; +x_17 = l_Lean_IR_ExpandResetReuse_searchAndExpand___main(x_13, x_16); +if (lean::is_scalar(x_15)) { + x_18 = lean::alloc_cnstr(0, 2, 0); +} else { + x_18 = x_15; +} +lean::cnstr_set(x_18, 0, x_11); +lean::cnstr_set(x_18, 1, x_17); +x_19 = lean::array_fset(x_8, x_0, x_18); +lean::dec(x_0); +x_0 = x_10; +x_1 = x_19; +goto _start; +} +else +{ +obj* x_22; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_28; +x_22 = lean::cnstr_get(x_6, 0); +if (lean::is_exclusive(x_6)) { + x_24 = x_6; +} else { + lean::inc(x_22); + lean::dec(x_6); + x_24 = lean::box(0); +} +x_25 = l_Array_empty___closed__1; +x_26 = l_Lean_IR_ExpandResetReuse_searchAndExpand___main(x_22, x_25); +if (lean::is_scalar(x_24)) { + x_27 = lean::alloc_cnstr(1, 1, 0); +} else { + x_27 = x_24; +} +lean::cnstr_set(x_27, 0, x_26); +x_28 = lean::array_fset(x_8, x_0, x_27); +lean::dec(x_0); +x_0 = x_10; +x_1 = x_28; +goto _start; +} +} +} +} +obj* l_Lean_IR_ExpandResetReuse_searchAndExpand___main(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +switch (lean::obj_tag(x_0)) { +case 0: +{ +obj* x_4; +x_4 = lean::cnstr_get(x_0, 1); +lean::inc(x_4); +switch (lean::obj_tag(x_4)) { +case 1: +{ +obj* x_6; obj* x_8; obj* x_10; obj* x_12; uint8 x_16; +x_6 = lean::cnstr_get(x_0, 0); +lean::inc(x_6); +x_8 = lean::cnstr_get(x_0, 2); +lean::inc(x_8); +x_10 = lean::cnstr_get(x_4, 0); +lean::inc(x_10); +x_12 = lean::cnstr_get(x_4, 1); +lean::inc(x_12); +lean::dec(x_4); +lean::inc(x_8); +x_16 = l_Lean_IR_ExpandResetReuse_consumed___main(x_6, x_8); +if (x_16 == 0) +{ +obj* x_20; +lean::dec(x_10); +lean::dec(x_6); +lean::dec(x_12); +x_20 = l_Lean_IR_push(x_1, x_0); +x_0 = x_8; +x_1 = x_20; +goto _start; +} +else +{ +obj* x_23; +lean::dec(x_0); +x_23 = l_Lean_IR_ExpandResetReuse_expand(x_1, x_6, x_10, x_12, x_8); +return x_23; +} +} +default: +{ +obj* x_25; +lean::dec(x_4); +x_25 = lean::box(0); +x_2 = x_25; +goto lbl_3; +} +} +} +case 10: +{ +obj* x_26; obj* x_28; obj* x_30; obj* x_32; obj* x_33; obj* x_34; obj* x_35; obj* x_36; +x_26 = lean::cnstr_get(x_0, 0); +x_28 = lean::cnstr_get(x_0, 1); +x_30 = lean::cnstr_get(x_0, 2); +if (lean::is_exclusive(x_0)) { + x_32 = x_0; +} else { + lean::inc(x_26); + lean::inc(x_28); + lean::inc(x_30); + lean::dec(x_0); + x_32 = lean::box(0); +} +x_33 = lean::mk_nat_obj(0ul); +x_34 = l_Array_hmmapAux___main___at_Lean_IR_ExpandResetReuse_searchAndExpand___main___spec__1(x_33, x_30); +if (lean::is_scalar(x_32)) { + x_35 = lean::alloc_cnstr(10, 3, 0); +} else { + x_35 = x_32; +} +lean::cnstr_set(x_35, 0, x_26); +lean::cnstr_set(x_35, 1, x_28); +lean::cnstr_set(x_35, 2, x_34); +x_36 = l_Lean_IR_reshape(x_1, x_35); +return x_36; +} +default: +{ +obj* x_37; +x_37 = lean::box(0); +x_2 = x_37; +goto lbl_3; +} +} +lbl_3: +{ +uint8 x_39; +lean::dec(x_2); +x_39 = l_Lean_IR_FnBody_isTerminal___main(x_0); +if (x_39 == 0) +{ +obj* x_40; obj* x_41; +x_40 = l_Lean_IR_FnBody_body___main(x_0); +x_41 = l_Lean_IR_push(x_1, x_0); +x_0 = x_40; +x_1 = x_41; +goto _start; +} +else +{ +obj* x_43; +x_43 = l_Lean_IR_reshape(x_1, x_0); +return x_43; +} +} +} +} +obj* l_Lean_IR_ExpandResetReuse_searchAndExpand(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = l_Lean_IR_ExpandResetReuse_searchAndExpand___main(x_0, x_1); +return x_2; +} +} +obj* l_Lean_IR_Decl_expandResetReuse___main(obj* x_0) { +_start: +{ +if (lean::obj_tag(x_0) == 0) +{ +obj* x_1; obj* x_3; uint8 x_5; obj* x_6; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; +x_1 = lean::cnstr_get(x_0, 0); +x_3 = lean::cnstr_get(x_0, 1); +x_5 = lean::cnstr_get_scalar(x_0, sizeof(void*)*3); +x_6 = lean::cnstr_get(x_0, 2); +if (lean::is_exclusive(x_0)) { + x_8 = x_0; +} else { + lean::inc(x_1); + lean::inc(x_3); + lean::inc(x_6); + lean::dec(x_0); + x_8 = lean::box(0); +} +x_9 = l_Array_empty___closed__1; +x_10 = l_Lean_IR_ExpandResetReuse_searchAndExpand___main(x_6, x_9); +if (lean::is_scalar(x_8)) { + x_11 = lean::alloc_cnstr(0, 3, 1); +} else { + x_11 = x_8; +} +lean::cnstr_set(x_11, 0, x_1); +lean::cnstr_set(x_11, 1, x_3); +lean::cnstr_set(x_11, 2, x_10); +lean::cnstr_set_scalar(x_11, sizeof(void*)*3, x_5); +x_12 = x_11; +return x_12; +} +else +{ +return x_0; +} +} +} +obj* l_Lean_IR_Decl_expandResetReuse(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = l_Lean_IR_Decl_expandResetReuse___main(x_0); +return x_1; +} +} +obj* initialize_init_control_state(obj*); +obj* initialize_init_control_reader(obj*); +obj* initialize_init_lean_compiler_ir_compilerm(obj*); +static bool _G_initialized = false; +obj* initialize_init_lean_compiler_ir_expandresetreuse(obj* w) { + if (_G_initialized) return w; + _G_initialized = true; +if (io_result_is_error(w)) return w; +w = initialize_init_control_state(w); +if (io_result_is_error(w)) return w; +w = initialize_init_control_reader(w); +if (io_result_is_error(w)) return w; +w = initialize_init_lean_compiler_ir_compilerm(w); +if (io_result_is_error(w)) return w; + l_Array_hmmapAux___main___at_Lean_IR_ExpandResetReuse_searchAndExpand___main___spec__1___closed__1 = _init_l_Array_hmmapAux___main___at_Lean_IR_ExpandResetReuse_searchAndExpand___main___spec__1___closed__1(); +lean::mark_persistent(l_Array_hmmapAux___main___at_Lean_IR_ExpandResetReuse_searchAndExpand___main___spec__1___closed__1); +return w; +}