feat(library/init/lean/compiler/ir): add Lean.IR.CompilerM

and environment extension for storing Lean IR declarations.

library/init/lean/compiler/ir/basic.lean

@@ -340,18 +340,25 @@ inductive Decl
 | fdecl  (f : FunId) (xs : Array Param) (ty : IRType) (b : FnBody)
 | extern (f : FunId) (xs : Array Param) (ty : IRType)
 
-def Decl.id : Decl → FunId
+namespace Decl
+
+instance : Inhabited Decl :=
+⟨extern (default _) (default _) IRType.irrelevant⟩
+
+def name : Decl → FunId
 | (Decl.fdecl f _ _ _) := f
 | (Decl.extern f _ _)  := f
 
-def Decl.params : Decl → Array Param
+def params : Decl → Array Param
 | (Decl.fdecl _ xs _ _) := xs
 | (Decl.extern _ xs _)  := xs
 
-def Decl.resultType : Decl → IRType
+def resultType : Decl → IRType
 | (Decl.fdecl _ _ t _) := t
 | (Decl.extern _ _ t)  := t
 
+end Decl
+
 @[export lean.ir.mk_decl_core] def mkDecl (f : FunId) (xs : Array Param) (ty : IRType) (b : FnBody) : Decl := Decl.fdecl f xs ty b
 
 /-- `Expr.isPure e` return `true` Iff `e` is in the `λPure` fragment. -/

library/init/lean/compiler/ir/checker.lean

@@ -106,7 +106,7 @@ end Checker
 
 def Decl.check (d : Decl) : IO Unit :=
 match Checker.checkDecl d {} with
-| Except.error msg := throw (IO.userError ("IR check failed at '" ++ toString d.id ++ "', error: " ++ msg))
+| Except.error msg := throw (IO.userError ("IR check failed at '" ++ toString d.name ++ "', error: " ++ msg))
 | other := pure ()
 
 end IR

library/init/lean/compiler/ir/compilerm.lean

@@ -0,0 +1,85 @@
+/-
+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.reader
+import init.lean.environment
+import init.lean.compiler.ir.basic
+import init.lean.compiler.ir.format
+
+namespace Lean
+namespace IR
+
+inductive LogEntry
+| step (cls : Name) (decls : Array Decl)
+| message (msg : Format)
+
+abbrev Log := Array LogEntry
+
+structure CompilerState :=
+(env : Environment) (log : Log)
+
+abbrev CompilerM := ReaderT Options (EState String CompilerState)
+
+def log (entry : LogEntry) : CompilerM Unit :=
+modify $ λ s, { log := s.log.push entry, .. s }
+
+def logDecls (cls : Name) (decls : Array Decl) : CompilerM Unit :=
+do opts ← read,
+   when (opts.getBool cls) $ log (LogEntry.step cls decls)
+
+def logMessage {α : Type} [HasFormat α] (a : α) : CompilerM Unit :=
+log (LogEntry.message (format a))
+
+def logMessageIf {α : Type} [HasFormat α] (cls : Name) (a : α) : CompilerM Unit :=
+do opts ← read,
+   when (opts.getBool cls) $ logMessage a
+
+@[inline] def modifyEnv (f : Environment → Environment) : CompilerM Unit :=
+modify $ λ s, { env := f s.env, .. s }
+
+abbrev DeclMap := SMap Name Decl Name.quickLt
+
+/- Create an array of decls to be saved on .olean file.
+   `decls` may contain duplicate entries, but we assume the one that occurs last is the most recent one. -/
+private def mkEntryArray (decls : List Decl) : Array Decl :=
+/- Remove duplicates by adding decls into a map -/
+let map : HashMap Name Decl := {} in
+let map := decls.foldl (λ (map : HashMap Name Decl) decl, map.insert decl.name decl) map in
+map.fold (λ a k v, a.push v) Array.empty
+
+def mkDeclMapExtension : IO (PersistentEnvExtension Decl DeclMap) :=
+registerPersistentEnvExtension {
+  name       := `IRDecls,
+  initState  := {},
+  addEntryFn := λ init s d,
+    let s := if init then s else s.switch in
+    s.insert d.name d,
+  toArrayFn  := mkEntryArray,
+  lazy       := false }
+
+@[init mkDeclMapExtension]
+constant declMapExt : PersistentEnvExtension Decl DeclMap := default _
+
+def findDecl (n : Name) : CompilerM (Option Decl) :=
+do s ← get,
+   pure $ (declMapExt.getState s.env).find n
+
+def containsDecl (n : Name) : CompilerM Bool :=
+do s ← get,
+   pure $ (declMapExt.getState s.env).contains n
+
+def getDecl (n : Name) : CompilerM Decl :=
+do (some decl) ← findDecl n | throw ("unknown declaration '" ++ toString n ++ "'"),
+   pure decl
+
+def addDecl (decl : Decl) : CompilerM Unit :=
+modifyEnv (λ env, declMapExt.addEntry env decl)
+
+def addDecls (decls : Array Decl) : CompilerM Unit :=
+decls.mfor addDecl
+
+end IR
+end Lean

library/init/lean/compiler/ir/default.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import init.lean.compiler.ir.basic
 import init.lean.compiler.ir.format
+import init.lean.compiler.ir.compilerm
 import init.lean.compiler.ir.pushproj
 import init.lean.compiler.ir.elimdead
 import init.lean.compiler.ir.simpcase
@@ -17,7 +18,6 @@ import init.lean.compiler.ir.boxing
 namespace Lean
 namespace IR
 
-@[export lean.ir.test_core]
 def test (d : Decl) : IO Unit :=
 do
    d.check,
@@ -41,5 +41,10 @@ do
    d.check,
    pure ()
 
+def compileAux (decls : Array Decl) : CompilerM Unit :=
+-- TODO: new IR
+pure ()
+
+
 end IR
 end Lean

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/ir/basic.cpp ./init/lean/compiler/ir/boxing.cpp ./init/lean/compiler/ir/checker.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.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/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/util.cpp ./init/lean/config.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/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/ir/basic.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/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/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/util.cpp ./init/lean/config.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/smap.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp)

src/stage0/init/lean/compiler/ir/basic.cpp

@@ -154,6 +154,7 @@ obj* string_append(obj*, obj*);
 obj* l_RBNode_balLeft___main___rarg(obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_addParamsRename(obj*, obj*, obj*);
 obj* l_Lean_IR_Expr_alphaEqv___boxed(obj*, obj*, obj*);
+obj* l_Lean_IR_Decl_Inhabited;
 obj* l_Lean_IR_Decl_params___boxed(obj*);
 obj* l_Lean_IR_Context_isParam___boxed(obj*, obj*);
 obj* l_Lean_IR_args_hasAeqv;
@@ -162,12 +163,11 @@ uint8 nat_dec_lt(obj*, obj*);
 }
 obj* l_Lean_IR_args_alphaEqv___boxed(obj*, obj*, obj*);
 obj* l_Lean_IR_FnBody_HasBeq;
-obj* l_Lean_IR_Decl_id___main(obj*);
 uint8 l_Lean_IR_Expr_alphaEqv(obj*, obj*, obj*);
 uint8 l_Lean_IR_FnBody_isTerminal___main(obj*);
-obj* l_Lean_IR_Decl_id___main___boxed(obj*);
-obj* l_Lean_IR_Decl_id(obj*);
+obj* l_Lean_IR_Decl_name___boxed(obj*);
 obj* l_Lean_IR_LitVal_beq___boxed(obj*, obj*);
+obj* l_Lean_IR_Decl_name___main(obj*);
 obj* l_RBNode_appendTrees___main___rarg(obj*, obj*);
 obj* l_RBNode_ins___main___at_Lean_IR_Context_addLocal___spec__2(obj*, obj*, obj*);
 namespace lean {
@@ -242,6 +242,7 @@ obj* l_Array_hmmapAux___main___at_Lean_IR_mmodifyJPs___spec__1___rarg(obj*, obj*
 obj* l_Lean_IR_Context_eraseJoinPointDecl(obj*, obj*);
 obj* l_Lean_IR_AltCore_mmodifyBody___main___rarg(obj*, obj*, obj*);
 uint8 l_Lean_IR_FnBody_isPure___main(obj*);
+obj* l_Lean_IR_Decl_name(obj*);
 uint8 l_Lean_IR_Arg_alphaEqv___main(obj*, obj*, obj*);
 obj* l_Lean_IR_VarId_alphaEqv___boxed(obj*, obj*, obj*);
 obj* l_Lean_IR_AltCore_body___main(obj*);
@@ -300,6 +301,7 @@ obj* l_Lean_IR_JoinPointId_HasToString(obj*);
 obj* l_RBNode_erase___at_Lean_IR_Context_eraseJoinPointDecl___spec__1(obj*, obj*);
 obj* l_Lean_IR_IRType_isObj___main___boxed(obj*);
 obj* l_Lean_IR_IRType_beq___boxed(obj*, obj*);
+obj* l_Lean_IR_Decl_name___main___boxed(obj*);
 obj* l_RBNode_insert___at_Lean_IR_addVarRename___spec__1(obj*, obj*, obj*);
 obj* l_Lean_IR_Index_lt___boxed(obj*, obj*);
 obj* l_Lean_IR_AltCore_setBody___main(obj*, obj*);
@@ -312,7 +314,6 @@ obj* l_Array_hmmapAux___main___at_Lean_IR_mmodifyJPs___spec__1(obj*);
 obj* l_Lean_IR_CtorInfo_beq___boxed(obj*, obj*);
 obj* l_RBNode_del___main___at_Lean_IR_Context_eraseJoinPointDecl___spec__2(obj*, obj*);
 uint8 l_Lean_IR_IRType_isObj(uint8);
-obj* l_Lean_IR_Decl_id___boxed(obj*);
 obj* l_Lean_IR_reshapeAux(obj*, obj*, obj*);
 obj* l_Lean_IR_FnBody_resetBody(obj*);
 obj* l_Array_isEqv___at_Lean_IR_FnBody_alphaEqv___main___spec__1___boxed(obj*, obj*, obj*);
@@ -2563,7 +2564,23 @@ return x_7;
 }
 }
 }}
-obj* l_Lean_IR_Decl_id___main(obj* x_0) {
+obj* _init_l_Lean_IR_Decl_Inhabited() {
+_start:
+{
+obj* x_0; obj* x_1; obj* x_2; uint8 x_3; obj* x_4; obj* x_5; 
+x_0 = lean::mk_nat_obj(0ul);
+x_1 = lean::mk_empty_array(x_0);
+x_2 = lean::box(0);
+x_3 = 6;
+x_4 = lean::alloc_cnstr(1, 2, 1);
+lean::cnstr_set(x_4, 0, x_2);
+lean::cnstr_set(x_4, 1, x_1);
+lean::cnstr_set_scalar(x_4, sizeof(void*)*2, x_3);
+x_5 = x_4;
+return x_5;
+}
+}
+obj* l_Lean_IR_Decl_name___main(obj* x_0) {
 _start:
 {
 obj* x_1; 
@@ -2572,28 +2589,28 @@ lean::inc(x_1);
 return x_1;
 }
 }
-obj* l_Lean_IR_Decl_id___main___boxed(obj* x_0) {
+obj* l_Lean_IR_Decl_name___main___boxed(obj* x_0) {
 _start:
 {
 obj* x_1; 
-x_1 = l_Lean_IR_Decl_id___main(x_0);
+x_1 = l_Lean_IR_Decl_name___main(x_0);
 lean::dec(x_0);
 return x_1;
 }
 }
-obj* l_Lean_IR_Decl_id(obj* x_0) {
+obj* l_Lean_IR_Decl_name(obj* x_0) {
 _start:
 {
 obj* x_1; 
-x_1 = l_Lean_IR_Decl_id___main(x_0);
+x_1 = l_Lean_IR_Decl_name___main(x_0);
 return x_1;
 }
 }
-obj* l_Lean_IR_Decl_id___boxed(obj* x_0) {
+obj* l_Lean_IR_Decl_name___boxed(obj* x_0) {
 _start:
 {
 obj* x_1; 
-x_1 = l_Lean_IR_Decl_id(x_0);
+x_1 = l_Lean_IR_Decl_name(x_0);
 lean::dec(x_0);
 return x_1;
 }
@@ -8094,6 +8111,8 @@ lean::mark_persistent(lean::ir::mk_unreachable_core);
 lean::mark_persistent(l_Lean_IR_altInh);
  l_Lean_IR_AltCore_mmodifyBody___main___rarg___closed__1 = _init_l_Lean_IR_AltCore_mmodifyBody___main___rarg___closed__1();
 lean::mark_persistent(l_Lean_IR_AltCore_mmodifyBody___main___rarg___closed__1);
+ l_Lean_IR_Decl_Inhabited = _init_l_Lean_IR_Decl_Inhabited();
+lean::mark_persistent(l_Lean_IR_Decl_Inhabited);
  l_Lean_IR_vsetInh = _init_l_Lean_IR_vsetInh();
 lean::mark_persistent(l_Lean_IR_vsetInh);
  l_Lean_IR_VarId_hasAeqv = _init_l_Lean_IR_VarId_hasAeqv();

src/stage0/init/lean/compiler/ir/checker.cpp

@@ -50,8 +50,8 @@ obj* l_Array_mforAux___main___at_Lean_IR_Checker_checkArgs___spec__1(obj*, obj*,
 namespace lean {
 uint8 nat_dec_lt(obj*, obj*);
 }
-obj* l_Lean_IR_Decl_id___main(obj*);
 extern obj* l_Char_HasRepr___closed__1;
+obj* l_Lean_IR_Decl_name___main(obj*);
 namespace lean {
 obj* nat_add(obj*, obj*);
 }
@@ -2194,7 +2194,7 @@ if (lean::is_exclusive(x_1)) {
  lean::dec(x_1);
  x_10 = lean::box(0);
 }
-x_11 = l_Lean_IR_Decl_id___main(x_0);
+x_11 = l_Lean_IR_Decl_name___main(x_0);
 lean::dec(x_0);
 x_13 = l_Lean_Name_toString___closed__1;
 x_14 = l_Lean_Name_toStringWithSep___main(x_13, x_11);

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.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.boxing
+// 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.boxing
 #include "runtime/object.h"
 #include "runtime/apply.h"
 typedef lean::object obj;    typedef lean::usize  usize;
@@ -17,10 +17,7 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
 obj* l_Lean_IR_test___closed__2;
 obj* l_Lean_IR_test___closed__5;
 obj* l_Lean_IR_Decl_normalizeIds(obj*);
-namespace lean {
-namespace ir {
-obj* test_core(obj*, obj*);
-}}
+obj* l_Lean_IR_test(obj*, obj*);
 namespace lean {
 namespace ir {
 obj* decl_to_string_core(obj*);
@@ -30,15 +27,18 @@ obj* l_IO_println___at_Lean_IR_test___spec__1(obj*, obj*);
 obj* l_Lean_IR_MaxIndex_collectDecl___main(obj*, obj*);
 obj* l_Lean_IR_Decl_pushProj___main(obj*);
 obj* l_Nat_repr(obj*);
+obj* l_Lean_IR_compileAux(obj*, obj*);
 namespace lean {
 obj* string_append(obj*, obj*);
 }
 obj* l_Lean_IR_test___closed__1;
 obj* l_Lean_IR_Decl_elimDead___main(obj*);
 obj* l_Lean_IR_test___closed__4;
+obj* l_Lean_IR_compileAux___boxed(obj*, obj*);
 obj* l_IO_println___at_HasRepr_HasEval___spec__1(obj*, obj*);
 obj* l_Lean_IR_Decl_insertResetReuse___main(obj*);
 obj* l_Lean_IR_test___closed__6;
+obj* l_Lean_IR_compileAux___rarg(obj*);
 obj* l_IO_print___at_Lean_IR_test___spec__2(obj*, obj*);
 obj* l_Lean_IR_Decl_simpCase___main(obj*);
 extern obj* l_IO_println___rarg___closed__1;
@@ -155,9 +155,7 @@ x_0 = lean::mk_string("=== After normalize Ids ===");
 return x_0;
 }
 }
-namespace lean {
-namespace ir {
-obj* test_core(obj* x_0, obj* x_1) {
+obj* l_Lean_IR_test(obj* x_0, obj* x_1) {
 _start:
 {
 obj* x_3; 
@@ -805,9 +803,51 @@ return x_194;
 }
 }
 }
-}}
+obj* l_Lean_IR_compileAux___rarg(obj* x_0) {
+_start:
+{
+obj* x_1; obj* x_3; obj* x_4; obj* x_5; 
+x_1 = lean::cnstr_get(x_0, 1);
+if (lean::is_exclusive(x_0)) {
+ lean::cnstr_release(x_0, 0);
+ x_3 = x_0;
+} else {
+ lean::inc(x_1);
+ lean::dec(x_0);
+ x_3 = lean::box(0);
+}
+x_4 = lean::box(0);
+if (lean::is_scalar(x_3)) {
+ x_5 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_5 = x_3;
+}
+lean::cnstr_set(x_5, 0, x_4);
+lean::cnstr_set(x_5, 1, x_1);
+return x_5;
+}
+}
+obj* l_Lean_IR_compileAux(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_IR_compileAux___rarg), 1, 0);
+return x_2;
+}
+}
+obj* l_Lean_IR_compileAux___boxed(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_Lean_IR_compileAux(x_0, x_1);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_2;
+}
+}
 obj* initialize_init_lean_compiler_ir_basic(obj*);
 obj* initialize_init_lean_compiler_ir_format(obj*);
+obj* initialize_init_lean_compiler_ir_compilerm(obj*);
 obj* initialize_init_lean_compiler_ir_pushproj(obj*);
 obj* initialize_init_lean_compiler_ir_elimdead(obj*);
 obj* initialize_init_lean_compiler_ir_simpcase(obj*);
@@ -824,6 +864,8 @@ w = initialize_init_lean_compiler_ir_basic(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_lean_compiler_ir_format(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;
 w = initialize_init_lean_compiler_ir_pushproj(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_lean_compiler_ir_elimdead(w);