feat: add low-level skeleton.

...because it is not there with Nix

.github/workflows/ci.yml

@@ -27,7 +27,7 @@ jobs:
             os: ubuntu-latest
             release: true
             CMAKE_OPTIONS: -DSTATIC=ON
-            shell: nix-shell --arg pkgs "import (fetchTarball \"channel:nixos-19.03\") {{}}" --argstr llvmPackages latest --run "bash -euxo pipefail {0}"
+            shell: nix-shell --arg static true --arg pkgs "import (fetchTarball \"channel:nixos-19.03\") {{}}" --argstr llvmPackages latest --run "bash -euxo pipefail {0}"
           - name: Linux
             os: ubuntu-latest
             check-stage3: true
@@ -43,6 +43,7 @@ jobs:
             os: macos-latest
             release: true
             CMAKE_OPTIONS: -DSTATIC=ON
+            shell: nix-shell --arg static true --run "bash -euxo pipefail {0}"
           - name: Windows
             os: windows-latest
             release: true
@@ -71,8 +72,9 @@ jobs:
         if: matrix.os != 'windows-latest'
       - name: Install MSYS2
         uses: msys2/setup-msys2@v2
+        # `polly` seems to be necessary for the LLVM cmake config to work, probably a packaging bug
         with:
-          install: make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x86_64-ccache git diffutils
+          install: make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x86_64-polly mingw-w64-x86_64-ccache git diffutils
         if: matrix.os == 'windows-latest'
       - name: Cache
         uses: actions/cache@v2
@@ -113,6 +115,7 @@ jobs:
         run: |
           for f in lean leanpkg; do
             patchelf --set-interpreter /lib64/ld-linux-x86-64.so.2 --remove-rpath build/stage1/bin/$f
+            ldd build/stage1/bin/$f
           done
         if: matrix.name == 'Linux release'
       - name: Patch
@@ -121,6 +124,7 @@ jobs:
             for lib in $(otool -L build/stage1/bin/$f | tail -n +2 | cut -d' ' -f1); do
               install_name_tool -change "$lib" "/usr/lib/$(basename $lib | sed 's/libc++\.1\.0/libc++.1/')" build/stage1/bin/$f
             done
+            otool -L build/stage1/bin/$f
           done
         if: matrix.name == 'macOS'
       - name: Pack

.gitignore

@@ -21,3 +21,4 @@ settings.json
 CMakeSettings.json
 CppProperties.json
 result
+.cache/

nix/bootstrap.nix

@@ -1,11 +1,11 @@
 { debug ? false, stage0debug ? false, extraCMakeFlags ? [],
-  stdenv, lib, cmake, gmp, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir,
+  stdenv, lib, cmake, gmp, llvm, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir,
   ... } @ args:
 rec {
   inherit stdenv;
   buildCMake = args: stdenv.mkDerivation ({
     nativeBuildInputs = [ cmake ];
-    buildInputs = [ gmp ];
+    buildInputs = [ gmp llvm ];
     # https://github.com/NixOS/nixpkgs/issues/60919
     hardeningDisable = [ "all" ];
     dontStrip = (args.debug or debug);
@@ -24,6 +24,7 @@ rec {
       touch empty.cpp
       sed -i 's/find_package.*//;s/add_subdirectory.*//;s/set(LEAN_OBJS.*/set(LEAN_OBJS empty.cpp)/' CMakeLists.txt
     '';
+    extraCMakeFlags = [ "-DLLVM=OFF" ];
     dontBuild = true;
     installPhase = ''
       mkdir $out
@@ -78,7 +79,11 @@ rec {
     in (all: all // all.lean) rec {
       Init = build { name = "Init"; deps = []; };
       Std  = build { name = "Std";  deps = [ Init ]; };
-      Lean = build { name = "Lean"; deps = [ Init Std ]; linkFlags = ["${stdlibLinkFlags} -rdynamic ${leancpp}/lib/lean.cpp.o"]; };
+      Lean = build {
+        name = "Lean";
+        deps = [ Init Std ];
+        linkFlags = ["${stdlibLinkFlags} -rdynamic -L${lib.makeLibraryPath [llvm]} -lLLVM ${leancpp}/lib/lean.cpp.o"];
+      };
       Leanpkg = build { name = "Leanpkg"; deps = [ Init Std Lean ]; linkFlags = ["${stdlibLinkFlags} -rdynamic"]; };
       inherit (Lean) emacs-dev emacs-package vscode-dev vscode-package;
       mods = Init.mods // Std.mods // Lean.mods;

nix/packages.nix

@@ -32,6 +32,7 @@ let
   lean = callPackage (import ./bootstrap.nix) (args // {
     stdenv = overrideCC llvmPackages.stdenv cc;
     inherit buildLeanPackage;
+    inherit (llvmPackages) llvm;
   });
   makeOverridableLeanPackage = f:
     let newF = origArgs: f origArgs // {

shell.nix

@@ -1,6 +1,6 @@
 let
   flakePkgs = (import ./default.nix).packages.${builtins.currentSystem};
-in { pkgs ? flakePkgs.nixpkgs, llvmPackages ? null }:
+in { pkgs ? flakePkgs.nixpkgs, llvmPackages ? null, static ? false }:
 # use `shell` as default
 (attribs: attribs.shell // attribs) rec {
   inherit (flakePkgs) temci;
@@ -9,7 +9,16 @@ in { pkgs ? flakePkgs.nixpkgs, llvmPackages ? null }:
                                           then flakePkgs.llvmPackages
                                           else pkgs.${"llvmPackages_${llvmPackages}"}).clang;
   } rec {
-    buildInputs = with pkgs; [ cmake (gmp.override { withStatic = true; }) ccache temci ];
+    buildInputs = with pkgs; [
+      cmake
+      (gmp.override { withStatic = static; })
+      llvm
+      ccache
+      temci
+      # LLVM dependencies
+      (if static then zlib.static else zlib)
+      (ncurses.override { enableStatic = static; })
+    ];
     # https://github.com/NixOS/nixpkgs/issues/60919
     hardeningDisable = [ "all" ];
     # more convenient `ctest` output

src/CMakeLists.txt

@@ -34,7 +34,7 @@ option(CCACHE             "use ccache"         ON)
 option(STATIC             "STATIC"             OFF)
 option(SPLIT_STACK        "SPLIT_STACK"        OFF)
 # When OFF we disable LLVM support
-option(LLVM               "LLVM"               OFF)
+option(LLVM               "LLVM"               ON)
 option(COMPRESSED_OBJECT_HEADER "Use compressed object headers in 64-bit machines, this option is ignored in 32-bit machines, and assumes the 64-bit OS can only address 2^48 bytes" ON)
 option(SMALL_RC "Use only 32-bits for RC, this option is only relevant when COMPRESSED_OBJECT_HEARDER is ON" ON)
 option(CHECK_RC_OVERFLOW "Check for RC overflows when SMALL_RC is ON" OFF)
@@ -69,6 +69,7 @@ option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current ver
 
 set(LEAN_EXTRA_MAKE_OPTS  ""                           CACHE STRING "extra options to lean --make")
 set(MINGW_LOCAL_DIR       "C:/msys64/mingw64/bin"      CACHE STRING "where to find MSYS2 required DLLs and binaries")
+set(CMAKE_EXPORT_COMPILE_COMMANDS                 ON) # genereate compile_commands.json for clangd
 
 if ("${FAKE_FREE}" MATCHES "ON")
   set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_FAKE_FREE")
@@ -193,7 +194,7 @@ if(LLVM)
   set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_LLVM")
   set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -D LEAN_LLVM")
 else()
-  #message(WARNING "Disabling LLVM support.  JIT compilation will not be available")
+  message(WARNING "Disabling LLVM support. JIT compilation will not be available.")
 endif()
 
 if(STATIC)

src/Lean/Compiler/IR.lean

@@ -84,4 +84,7 @@ def addBoxedVersion (env : Environment) (decl : Decl) : Except String Environmen
   | EStateM.Result.ok     _  s => Except.ok s.env
   | EStateM.Result.error msg s => Except.error msg
 
+@[extern "lean_ir_emit_llvm"]
+constant emitLLVM : @& Environment → @& Name → IO String
+
 end Lean.IR

src/Lean/Compiler/IR/CompilerM.lean

@@ -111,7 +111,8 @@ def getDecl (n : Name) : CompilerM Decl := do
 def addDeclAux (env : Environment) (decl : Decl) : Environment :=
   declMapExt.addEntry env decl
 
-def getDecls (env : Environment) : List Decl :=
+@[export lean_ir_get_decls]
+def getDecls (env : @& Environment) : List Decl :=
   declMapExt.getEntries env
 
 def getEnv : CompilerM Environment := do

src/Lean/Environment.lean

@@ -75,6 +75,10 @@ def contains (env : Environment) (n : Name) : Bool :=
 def imports (env : Environment) : Array Import :=
   env.header.imports
 
+@[export lean_environment_import_names]
+def importNames (env : Environment) : Array Name :=
+  env.imports.map (·.module)
+
 def allImportedModuleNames (env : Environment) : Array Name :=
   env.header.moduleNames
 

src/library/compiler/CMakeLists.txt

@@ -5,5 +5,5 @@ add_library(compiler OBJECT init_module.cpp ## New
   reduce_arity.cpp closed_term_cache.cpp
   export_attribute.cpp extern_attribute.cpp
   borrowed_annotation.cpp init_attribute.cpp eager_lambda_lifting.cpp
-  struct_cases_on.cpp find_jp.cpp ir.cpp implemented_by_attribute.cpp
-  ir_interpreter.cpp)
+  struct_cases_on.cpp find_jp.cpp ir.cpp ir_decode_helpers.cpp 
+  implemented_by_attribute.cpp llvm.cpp ir_interpreter.cpp)

src/library/compiler/ir_decode_helpers.cpp

@@ -0,0 +1,131 @@
+/*
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Dany Fabian, Sebastian Ullrich
+*/
+
+#include "ir_decode_helpers.h"
+
+namespace lean {
+namespace ir {
+
+type to_type(object * obj) {
+    if (!is_scalar(obj)) throw exception("unsupported IRType");
+    else return static_cast<type>(unbox(obj));
+}
+type cnstr_get_type(object_ref const & o, unsigned i) { return to_type(cnstr_get(o.raw(), i)); }
+
+bool arg_is_irrelevant(arg const & a) { return is_scalar(a.raw()); }
+var_id const & arg_var_id(arg const & a) { lean_assert(!arg_is_irrelevant(a)); return cnstr_get_ref_t<var_id>(a, 0); }
+
+lit_val_kind lit_val_tag(lit_val const & l) { return static_cast<lit_val_kind>(cnstr_tag(l.raw())); }
+nat const & lit_val_num(lit_val const & l) { lean_assert(lit_val_tag(l) == lit_val_kind::Num); return cnstr_get_ref_t<nat>(l, 0); }
+string_ref const & lit_val_str(lit_val const & l) { lean_assert(lit_val_tag(l) == lit_val_kind::Str); return cnstr_get_ref_t<string_ref>(l, 0); }
+
+name const & ctor_info_name(ctor_info const & c) { return cnstr_get_ref_t<name>(c, 0); }
+nat const & ctor_info_tag(ctor_info const & c) { return cnstr_get_ref_t<nat>(c, 1); }
+nat const & ctor_info_size(ctor_info const & c) { return cnstr_get_ref_t<nat>(c, 2); }
+nat const & ctor_info_usize(ctor_info const & c) { return cnstr_get_ref_t<nat>(c, 3); }
+nat const & ctor_info_ssize(ctor_info const & c) { return cnstr_get_ref_t<nat>(c, 4); }
+
+/* Return the only Bool scalar field in an object that has `num_obj_fields` object/usize fields */
+static inline bool get_bool_field(object * o, unsigned num_obj_fields) {
+    return cnstr_get_uint8(o, sizeof(void*)*num_obj_fields);
+}
+
+expr_kind expr_tag(expr const & e) { return static_cast<expr_kind>(cnstr_tag(e.raw())); }
+ctor_info const & expr_ctor_info(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Ctor); return cnstr_get_ref_t<ctor_info>(e, 0); }
+array_ref<arg> const & expr_ctor_args(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Ctor); return cnstr_get_ref_t<array_ref<arg>>(e, 1); }
+nat const & expr_reset_num_objs(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Reset); return cnstr_get_ref_t<nat>(e, 0); }
+var_id const & expr_reset_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Reset); return cnstr_get_ref_t<var_id>(e, 1); }
+var_id const & expr_reuse_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Reuse); return cnstr_get_ref_t<var_id>(e, 0); }
+ctor_info const & expr_reuse_ctor(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Reuse); return cnstr_get_ref_t<ctor_info>(e, 1); }
+bool expr_reuse_update_header(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Reuse); return get_bool_field(e.raw(), 3); }
+array_ref<arg> const & expr_reuse_args(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Reuse); return cnstr_get_ref_t<array_ref<arg>>(e, 2); }
+nat const & expr_proj_idx(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Proj); return cnstr_get_ref_t<nat>(e, 0); }
+var_id const & expr_proj_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Proj); return cnstr_get_ref_t<var_id>(e, 1); }
+nat const & expr_uproj_idx(expr const & e) { lean_assert(expr_tag(e) == expr_kind::UProj); return cnstr_get_ref_t<nat>(e, 0); }
+var_id const & expr_uproj_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::UProj); return cnstr_get_ref_t<var_id>(e, 1); }
+nat const & expr_sproj_idx(expr const & e) { lean_assert(expr_tag(e) == expr_kind::SProj); return cnstr_get_ref_t<nat>(e, 0); }
+nat const & expr_sproj_offset(expr const & e) { lean_assert(expr_tag(e) == expr_kind::SProj); return cnstr_get_ref_t<nat>(e, 1); }
+var_id const & expr_sproj_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::SProj); return cnstr_get_ref_t<var_id>(e, 2); }
+fun_id const & expr_fap_fun(expr const & e) { lean_assert(expr_tag(e) == expr_kind::FAp); return cnstr_get_ref_t<fun_id>(e, 0); }
+array_ref<arg> const & expr_fap_args(expr const & e) { lean_assert(expr_tag(e) == expr_kind::FAp); return cnstr_get_ref_t<array_ref<arg>>(e, 1); }
+fun_id const & expr_pap_fun(expr const & e) { lean_assert(expr_tag(e) == expr_kind::PAp); return cnstr_get_ref_t<name>(e, 0); }
+array_ref<arg> const & expr_pap_args(expr const & e) { lean_assert(expr_tag(e) == expr_kind::PAp); return cnstr_get_ref_t<array_ref<arg>>(e, 1); }
+var_id const & expr_ap_fun(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Ap); return cnstr_get_ref_t<var_id>(e, 0); }
+array_ref<arg> const & expr_ap_args(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Ap); return cnstr_get_ref_t<array_ref<arg>>(e, 1); }
+type expr_box_type(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Box); return cnstr_get_type(e, 0); }
+var_id const & expr_box_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Box); return cnstr_get_ref_t<var_id>(e, 1); }
+var_id const & expr_unbox_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Unbox); return cnstr_get_ref_t<var_id>(e, 0); }
+lit_val const & expr_lit_val(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Lit); return cnstr_get_ref_t<lit_val>(e, 0); }
+var_id const & expr_is_shared_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::IsShared); return cnstr_get_ref_t<var_id>(e, 0); }
+var_id const & expr_is_tagged_ptr_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::IsTaggedPtr); return cnstr_get_ref_t<var_id>(e, 0); }
+
+typedef object_ref param;
+var_id const & param_var(param const & p) { return cnstr_get_ref_t<var_id>(p, 0); }
+bool param_borrow(param const & p) { return get_bool_field(p.raw(), 2); }
+type param_type(param const & p) { return cnstr_get_type(p, 1); }
+
+typedef object_ref alt_core;
+alt_core_kind alt_core_tag(alt_core const & a) { return static_cast<alt_core_kind>(cnstr_tag(a.raw())); }
+ctor_info const & alt_core_ctor_info(alt_core const & a) { lean_assert(alt_core_tag(a) == alt_core_kind::Ctor); return cnstr_get_ref_t<ctor_info>(a, 0); }
+fn_body const & alt_core_ctor_cont(alt_core const & a) { lean_assert(alt_core_tag(a) == alt_core_kind::Ctor); return cnstr_get_ref_t<fn_body>(a, 1); }
+fn_body const & alt_core_default_cont(alt_core const & a) { lean_assert(alt_core_tag(a) == alt_core_kind::Default); return cnstr_get_ref_t<fn_body>(a, 0); }
+
+fn_body_kind fn_body_tag(fn_body const & a) { return is_scalar(a.raw()) ? static_cast<fn_body_kind>(unbox(a.raw())) : static_cast<fn_body_kind>(cnstr_tag(a.raw())); }
+var_id const & fn_body_vdecl_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::VDecl); return cnstr_get_ref_t<var_id>(b, 0); }
+type fn_body_vdecl_type(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::VDecl); return cnstr_get_type(b, 1); }
+expr const & fn_body_vdecl_expr(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::VDecl); return cnstr_get_ref_t<expr>(b, 2); }
+fn_body const & fn_body_vdecl_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::VDecl); return cnstr_get_ref_t<fn_body>(b, 3); }
+jp_id const & fn_body_jdecl_id(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::JDecl); return cnstr_get_ref_t<jp_id>(b, 0); }
+array_ref<param> const & fn_body_jdecl_params(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::JDecl); return cnstr_get_ref_t<array_ref<param>>(b, 1); }
+fn_body const & fn_body_jdecl_body(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::JDecl); return cnstr_get_ref_t<fn_body>(b, 2); }
+fn_body const & fn_body_jdecl_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::JDecl); return cnstr_get_ref_t<fn_body>(b, 3); }
+var_id const & fn_body_set_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Set); return cnstr_get_ref_t<var_id>(b, 0); }
+nat const & fn_body_set_idx(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Set); return cnstr_get_ref_t<nat>(b, 1); }
+arg const & fn_body_set_arg(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Set); return cnstr_get_ref_t<arg>(b, 2); }
+fn_body const & fn_body_set_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Set); return cnstr_get_ref_t<fn_body>(b, 3); }
+var_id const & fn_body_set_tag_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SetTag); return cnstr_get_ref_t<var_id>(b, 0); }
+nat const & fn_body_set_tag_cidx(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SetTag); return cnstr_get_ref_t<nat>(b, 1); }
+fn_body const & fn_body_set_tag_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SetTag); return cnstr_get_ref_t<fn_body>(b, 2); }
+var_id const & fn_body_uset_target(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::USet); return cnstr_get_ref_t<var_id>(b, 0); }
+nat const & fn_body_uset_idx(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::USet); return cnstr_get_ref_t<nat>(b, 1); }
+var_id const & fn_body_uset_source(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::USet); return cnstr_get_ref_t<var_id>(b, 2); }
+fn_body const & fn_body_uset_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::USet); return cnstr_get_ref_t<fn_body>(b, 3); }
+var_id const & fn_body_sset_target(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SSet); return cnstr_get_ref_t<var_id>(b, 0); }
+nat const & fn_body_sset_idx(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SSet); return cnstr_get_ref_t<nat>(b, 1); }
+nat const & fn_body_sset_offset(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SSet); return cnstr_get_ref_t<nat>(b, 2); }
+var_id const & fn_body_sset_source(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SSet); return cnstr_get_ref_t<var_id>(b, 3); }
+type fn_body_sset_type(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SSet); return cnstr_get_type(b, 4); }
+fn_body const & fn_body_sset_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SSet); return cnstr_get_ref_t<fn_body>(b, 5); }
+var_id const & fn_body_inc_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Inc); return cnstr_get_ref_t<var_id>(b, 0); }
+nat const & fn_body_inc_val(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Inc); return cnstr_get_ref_t<nat>(b, 1); }
+bool fn_body_inc_maybe_scalar(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Inc); return get_bool_field(b.raw(), 3); }
+fn_body const & fn_body_inc_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Inc); return cnstr_get_ref_t<fn_body>(b, 2); }
+var_id const & fn_body_dec_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Dec); return cnstr_get_ref_t<var_id>(b, 0); }
+nat const & fn_body_dec_val(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Dec); return cnstr_get_ref_t<nat>(b, 1); }
+bool fn_body_dec_maybe_scalar(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Dec); return get_bool_field(b.raw(), 3); }
+fn_body const & fn_body_dec_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Dec); return cnstr_get_ref_t<fn_body>(b, 2); }
+var_id const & fn_body_del_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Del); return cnstr_get_ref_t<var_id>(b, 0); }
+fn_body const & fn_body_del_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Del); return cnstr_get_ref_t<fn_body>(b, 1); }
+object_ref const & fn_body_mdata_data(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::MData); return cnstr_get_ref_t<object_ref>(b, 0); }
+fn_body const & fn_body_mdata_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::MData); return cnstr_get_ref_t<fn_body>(b, 1); }
+name const & fn_body_case_tid(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Case); return cnstr_get_ref_t<name>(b, 0); }
+var_id const & fn_body_case_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Case); return cnstr_get_ref_t<var_id>(b, 1); }
+type fn_body_case_var_type(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Case); return cnstr_get_type(b, 2); }
+array_ref<alt_core> const & fn_body_case_alts(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Case); return cnstr_get_ref_t<array_ref<alt_core>>(b, 3); }
+arg const & fn_body_ret_arg(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Ret); return cnstr_get_ref_t<arg>(b, 0); }
+jp_id const & fn_body_jmp_jp(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Jmp); return cnstr_get_ref_t<jp_id>(b, 0); }
+array_ref<arg> const & fn_body_jmp_args(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Jmp); return cnstr_get_ref_t<array_ref<arg>>(b, 1); }
+
+typedef object_ref decl;
+decl_kind decl_tag(decl const & a) { return is_scalar(a.raw()) ? static_cast<decl_kind>(unbox(a.raw())) : static_cast<decl_kind>(cnstr_tag(a.raw())); }
+fun_id const & decl_fun_id(decl const & b) { return cnstr_get_ref_t<fun_id>(b, 0); }
+array_ref<param> const & decl_params(decl const & b) { return cnstr_get_ref_t<array_ref<param>>(b, 1); }
+type decl_type(decl const & b) { return cnstr_get_type(b, 2); }
+fn_body const & decl_fun_body(decl const & b) { lean_assert(decl_tag(b) == decl_kind::Fun); return cnstr_get_ref_t<fn_body>(b, 3); }
+
+} // namespace ir
+}

src/library/compiler/ir_decode_helpers.h

@@ -0,0 +1,136 @@
+/*
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Dany Fabian, Sebastian Ullrich
+*/
+
+#pragma once
+#include "library/compiler/ir.h"
+#include "util/array_ref.h"
+
+namespace lean {
+namespace ir {
+// C++ wrappers of Lean data types
+
+typedef object_ref lit_val;
+typedef object_ref ctor_info;
+
+type to_type(object *obj);
+type cnstr_get_type(object_ref const &o, unsigned i);
+
+bool arg_is_irrelevant(arg const &a);
+var_id const &arg_var_id(arg const &a);
+
+enum class lit_val_kind { Num, Str };
+lit_val_kind lit_val_tag(lit_val const &l);
+nat const &lit_val_num(lit_val const &l);
+string_ref const &lit_val_str(lit_val const &l);
+
+name const &ctor_info_name(ctor_info const &c);
+nat const &ctor_info_tag(ctor_info const &c);
+nat const &ctor_info_size(ctor_info const &c);
+nat const &ctor_info_usize(ctor_info const &c);
+nat const &ctor_info_ssize(ctor_info const &c);
+
+/* Return the only Bool scalar field in an object that has `num_obj_fields` object/usize fields */
+static inline bool get_bool_field(object *o, unsigned num_obj_fields);
+
+enum class expr_kind { Ctor, Reset, Reuse, Proj, UProj, SProj, FAp, PAp, Ap, Box, Unbox, Lit, IsShared, IsTaggedPtr };
+expr_kind expr_tag(expr const &e);
+ctor_info const &expr_ctor_info(expr const &e);
+array_ref<arg> const &expr_ctor_args(expr const &e);
+nat const &expr_reset_num_objs(expr const &e);
+var_id const &expr_reset_obj(expr const &e);
+var_id const &expr_reuse_obj(expr const &e);
+ctor_info const &expr_reuse_ctor(expr const &e);
+bool expr_reuse_update_header(expr const &e);
+array_ref<arg> const &expr_reuse_args(expr const &e);
+nat const &expr_proj_idx(expr const &e);
+var_id const &expr_proj_obj(expr const &e);
+nat const &expr_uproj_idx(expr const &e);
+var_id const &expr_uproj_obj(expr const &e);
+nat const &expr_sproj_idx(expr const &e);
+nat const &expr_sproj_offset(expr const &e);
+var_id const &expr_sproj_obj(expr const &e);
+fun_id const &expr_fap_fun(expr const &e);
+array_ref<arg> const &expr_fap_args(expr const &e);
+fun_id const &expr_pap_fun(expr const &e);
+array_ref<arg> const &expr_pap_args(expr const &e);
+var_id const &expr_ap_fun(expr const &e);
+array_ref<arg> const &expr_ap_args(expr const &e);
+type expr_box_type(expr const &e);
+var_id const &expr_box_obj(expr const &e);
+var_id const &expr_unbox_obj(expr const &e);
+lit_val const &expr_lit_val(expr const &e);
+var_id const &expr_is_shared_obj(expr const &e);
+var_id const &expr_is_tagged_ptr_obj(expr const &e);
+
+typedef object_ref param;
+var_id const &param_var(param const &p);
+bool param_borrow(param const &p);
+type param_type(param const &p);
+
+typedef object_ref alt_core;
+enum class alt_core_kind { Ctor, Default };
+alt_core_kind alt_core_tag(alt_core const &a);
+ctor_info const &alt_core_ctor_info(alt_core const &a);
+fn_body const &alt_core_ctor_cont(alt_core const &a);
+fn_body const &alt_core_default_cont(alt_core const &a);
+
+enum class fn_body_kind { VDecl, JDecl, Set, SetTag, USet, SSet, Inc, Dec, Del, MData, Case, Ret, Jmp, Unreachable };
+fn_body_kind fn_body_tag(fn_body const &a);
+var_id const &fn_body_vdecl_var(fn_body const &b);
+type fn_body_vdecl_type(fn_body const &b);
+expr const &fn_body_vdecl_expr(fn_body const &b);
+fn_body const &fn_body_vdecl_cont(fn_body const &b);
+jp_id const &fn_body_jdecl_id(fn_body const &b);
+array_ref<param> const &fn_body_jdecl_params(fn_body const &b);
+fn_body const &fn_body_jdecl_body(fn_body const &b);
+fn_body const &fn_body_jdecl_cont(fn_body const &b);
+var_id const &fn_body_set_var(fn_body const &b);
+nat const &fn_body_set_idx(fn_body const &b);
+arg const &fn_body_set_arg(fn_body const &b);
+fn_body const &fn_body_set_cont(fn_body const &b);
+var_id const &fn_body_set_tag_var(fn_body const &b);
+nat const &fn_body_set_tag_cidx(fn_body const &b);
+fn_body const &fn_body_set_tag_cont(fn_body const &b);
+var_id const &fn_body_uset_target(fn_body const &b);
+nat const &fn_body_uset_idx(fn_body const &b);
+var_id const &fn_body_uset_source(fn_body const &b);
+fn_body const &fn_body_uset_cont(fn_body const &b);
+var_id const &fn_body_sset_target(fn_body const &b);
+nat const &fn_body_sset_idx(fn_body const &b);
+nat const &fn_body_sset_offset(fn_body const &b);
+var_id const &fn_body_sset_source(fn_body const &b);
+type fn_body_sset_type(fn_body const &b);
+fn_body const &fn_body_sset_cont(fn_body const &b);
+var_id const &fn_body_inc_var(fn_body const &b);
+nat const &fn_body_inc_val(fn_body const &b);
+bool fn_body_inc_maybe_scalar(fn_body const &b);
+fn_body const &fn_body_inc_cont(fn_body const &b);
+var_id const &fn_body_dec_var(fn_body const &b);
+nat const &fn_body_dec_val(fn_body const &b);
+bool fn_body_dec_maybe_scalar(fn_body const &b);
+fn_body const &fn_body_dec_cont(fn_body const &b);
+var_id const &fn_body_del_var(fn_body const &b);
+fn_body const &fn_body_del_cont(fn_body const &b);
+object_ref const &fn_body_mdata_data(fn_body const &b);
+fn_body const &fn_body_mdata_cont(fn_body const &b);
+name const &fn_body_case_tid(fn_body const &b);
+var_id const &fn_body_case_var(fn_body const &b);
+type fn_body_case_var_type(fn_body const &b);
+array_ref<alt_core> const &fn_body_case_alts(fn_body const &b);
+arg const &fn_body_ret_arg(fn_body const &b);
+jp_id const &fn_body_jmp_jp(fn_body const &b);
+array_ref<arg> const &fn_body_jmp_args(fn_body const &b);
+
+typedef object_ref decl;
+enum class decl_kind { Fun, Extern };
+decl_kind decl_tag(decl const &a);
+fun_id const &decl_fun_id(decl const &b);
+array_ref<param> const &decl_params(decl const &b);
+type decl_type(decl const &b);
+fn_body const &decl_fun_body(decl const &b);
+}
+}

src/library/compiler/ir_interpreter.cpp

@@ -40,7 +40,7 @@ functions, which have a (relatively) homogeneous ABI that we can use without run
 #include <lean/io.h>
 #include "library/time_task.h"
 #include "library/trace.h"
-#include "library/compiler/ir.h"
+#include "library/compiler/ir_decode_helpers.h"
 #include "library/compiler/init_attribute.h"
 #include "util/option_ref.h"
 #include "util/array_ref.h"
@@ -58,133 +58,6 @@ functions, which have a (relatively) homogeneous ABI that we can use without run
 
 namespace lean {
 namespace ir {
-// C++ wrappers of Lean data types
-
-typedef object_ref lit_val;
-typedef object_ref ctor_info;
-
-type to_type(object * obj) {
-    if (!is_scalar(obj)) throw exception("unsupported IRType");
-    else return static_cast<type>(unbox(obj));
-}
-type cnstr_get_type(object_ref const & o, unsigned i) { return to_type(cnstr_get(o.raw(), i)); }
-
-bool arg_is_irrelevant(arg const & a) { return is_scalar(a.raw()); }
-var_id const & arg_var_id(arg const & a) { lean_assert(!arg_is_irrelevant(a)); return cnstr_get_ref_t<var_id>(a, 0); }
-
-enum class lit_val_kind { Num, Str };
-lit_val_kind lit_val_tag(lit_val const & l) { return static_cast<lit_val_kind>(cnstr_tag(l.raw())); }
-nat const & lit_val_num(lit_val const & l) { lean_assert(lit_val_tag(l) == lit_val_kind::Num); return cnstr_get_ref_t<nat>(l, 0); }
-string_ref const & lit_val_str(lit_val const & l) { lean_assert(lit_val_tag(l) == lit_val_kind::Str); return cnstr_get_ref_t<string_ref>(l, 0); }
-
-name const & ctor_info_name(ctor_info const & c) { return cnstr_get_ref_t<name>(c, 0); }
-nat const & ctor_info_tag(ctor_info const & c) { return cnstr_get_ref_t<nat>(c, 1); }
-nat const & ctor_info_size(ctor_info const & c) { return cnstr_get_ref_t<nat>(c, 2); }
-nat const & ctor_info_usize(ctor_info const & c) { return cnstr_get_ref_t<nat>(c, 3); }
-nat const & ctor_info_ssize(ctor_info const & c) { return cnstr_get_ref_t<nat>(c, 4); }
-
-/* Return the only Bool scalar field in an object that has `num_obj_fields` object/usize fields */
-static inline bool get_bool_field(object * o, unsigned num_obj_fields) {
-    return cnstr_get_uint8(o, sizeof(void*)*num_obj_fields);
-}
-
-enum class expr_kind { Ctor, Reset, Reuse, Proj, UProj, SProj, FAp, PAp, Ap, Box, Unbox, Lit, IsShared, IsTaggedPtr };
-expr_kind expr_tag(expr const & e) { return static_cast<expr_kind>(cnstr_tag(e.raw())); }
-ctor_info const & expr_ctor_info(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Ctor); return cnstr_get_ref_t<ctor_info>(e, 0); }
-array_ref<arg> const & expr_ctor_args(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Ctor); return cnstr_get_ref_t<array_ref<arg>>(e, 1); }
-nat const & expr_reset_num_objs(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Reset); return cnstr_get_ref_t<nat>(e, 0); }
-var_id const & expr_reset_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Reset); return cnstr_get_ref_t<var_id>(e, 1); }
-var_id const & expr_reuse_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Reuse); return cnstr_get_ref_t<var_id>(e, 0); }
-ctor_info const & expr_reuse_ctor(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Reuse); return cnstr_get_ref_t<ctor_info>(e, 1); }
-bool expr_reuse_update_header(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Reuse); return get_bool_field(e.raw(), 3); }
-array_ref<arg> const & expr_reuse_args(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Reuse); return cnstr_get_ref_t<array_ref<arg>>(e, 2); }
-nat const & expr_proj_idx(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Proj); return cnstr_get_ref_t<nat>(e, 0); }
-var_id const & expr_proj_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Proj); return cnstr_get_ref_t<var_id>(e, 1); }
-nat const & expr_uproj_idx(expr const & e) { lean_assert(expr_tag(e) == expr_kind::UProj); return cnstr_get_ref_t<nat>(e, 0); }
-var_id const & expr_uproj_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::UProj); return cnstr_get_ref_t<var_id>(e, 1); }
-nat const & expr_sproj_idx(expr const & e) { lean_assert(expr_tag(e) == expr_kind::SProj); return cnstr_get_ref_t<nat>(e, 0); }
-nat const & expr_sproj_offset(expr const & e) { lean_assert(expr_tag(e) == expr_kind::SProj); return cnstr_get_ref_t<nat>(e, 1); }
-var_id const & expr_sproj_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::SProj); return cnstr_get_ref_t<var_id>(e, 2); }
-fun_id const & expr_fap_fun(expr const & e) { lean_assert(expr_tag(e) == expr_kind::FAp); return cnstr_get_ref_t<fun_id>(e, 0); }
-array_ref<arg> const & expr_fap_args(expr const & e) { lean_assert(expr_tag(e) == expr_kind::FAp); return cnstr_get_ref_t<array_ref<arg>>(e, 1); }
-fun_id const & expr_pap_fun(expr const & e) { lean_assert(expr_tag(e) == expr_kind::PAp); return cnstr_get_ref_t<name>(e, 0); }
-array_ref<arg> const & expr_pap_args(expr const & e) { lean_assert(expr_tag(e) == expr_kind::PAp); return cnstr_get_ref_t<array_ref<arg>>(e, 1); }
-var_id const & expr_ap_fun(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Ap); return cnstr_get_ref_t<var_id>(e, 0); }
-array_ref<arg> const & expr_ap_args(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Ap); return cnstr_get_ref_t<array_ref<arg>>(e, 1); }
-type expr_box_type(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Box); return cnstr_get_type(e, 0); }
-var_id const & expr_box_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Box); return cnstr_get_ref_t<var_id>(e, 1); }
-var_id const & expr_unbox_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Unbox); return cnstr_get_ref_t<var_id>(e, 0); }
-lit_val const & expr_lit_val(expr const & e) { lean_assert(expr_tag(e) == expr_kind::Lit); return cnstr_get_ref_t<lit_val>(e, 0); }
-var_id const & expr_is_shared_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::IsShared); return cnstr_get_ref_t<var_id>(e, 0); }
-var_id const & expr_is_tagged_ptr_obj(expr const & e) { lean_assert(expr_tag(e) == expr_kind::IsTaggedPtr); return cnstr_get_ref_t<var_id>(e, 0); }
-
-typedef object_ref param;
-var_id const & param_var(param const & p) { return cnstr_get_ref_t<var_id>(p, 0); }
-bool param_borrow(param const & p) { return get_bool_field(p.raw(), 2); }
-type param_type(param const & p) { return cnstr_get_type(p, 1); }
-
-typedef object_ref alt_core;
-enum class alt_core_kind { Ctor, Default };
-alt_core_kind alt_core_tag(alt_core const & a) { return static_cast<alt_core_kind>(cnstr_tag(a.raw())); }
-ctor_info const & alt_core_ctor_info(alt_core const & a) { lean_assert(alt_core_tag(a) == alt_core_kind::Ctor); return cnstr_get_ref_t<ctor_info>(a, 0); }
-fn_body const & alt_core_ctor_cont(alt_core const & a) { lean_assert(alt_core_tag(a) == alt_core_kind::Ctor); return cnstr_get_ref_t<fn_body>(a, 1); }
-fn_body const & alt_core_default_cont(alt_core const & a) { lean_assert(alt_core_tag(a) == alt_core_kind::Default); return cnstr_get_ref_t<fn_body>(a, 0); }
-
-enum class fn_body_kind { VDecl, JDecl, Set, SetTag, USet, SSet, Inc, Dec, Del, MData, Case, Ret, Jmp, Unreachable };
-fn_body_kind fn_body_tag(fn_body const & a) { return is_scalar(a.raw()) ? static_cast<fn_body_kind>(unbox(a.raw())) : static_cast<fn_body_kind>(cnstr_tag(a.raw())); }
-var_id const & fn_body_vdecl_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::VDecl); return cnstr_get_ref_t<var_id>(b, 0); }
-type fn_body_vdecl_type(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::VDecl); return cnstr_get_type(b, 1); }
-expr const & fn_body_vdecl_expr(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::VDecl); return cnstr_get_ref_t<expr>(b, 2); }
-fn_body const & fn_body_vdecl_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::VDecl); return cnstr_get_ref_t<fn_body>(b, 3); }
-jp_id const & fn_body_jdecl_id(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::JDecl); return cnstr_get_ref_t<jp_id>(b, 0); }
-array_ref<param> const & fn_body_jdecl_params(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::JDecl); return cnstr_get_ref_t<array_ref<param>>(b, 1); }
-fn_body const & fn_body_jdecl_body(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::JDecl); return cnstr_get_ref_t<fn_body>(b, 2); }
-fn_body const & fn_body_jdecl_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::JDecl); return cnstr_get_ref_t<fn_body>(b, 3); }
-var_id const & fn_body_set_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Set); return cnstr_get_ref_t<var_id>(b, 0); }
-nat const & fn_body_set_idx(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Set); return cnstr_get_ref_t<nat>(b, 1); }
-arg const & fn_body_set_arg(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Set); return cnstr_get_ref_t<arg>(b, 2); }
-fn_body const & fn_body_set_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Set); return cnstr_get_ref_t<fn_body>(b, 3); }
-var_id const & fn_body_set_tag_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SetTag); return cnstr_get_ref_t<var_id>(b, 0); }
-nat const & fn_body_set_tag_cidx(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SetTag); return cnstr_get_ref_t<nat>(b, 1); }
-fn_body const & fn_body_set_tag_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SetTag); return cnstr_get_ref_t<fn_body>(b, 2); }
-var_id const & fn_body_uset_target(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::USet); return cnstr_get_ref_t<var_id>(b, 0); }
-nat const & fn_body_uset_idx(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::USet); return cnstr_get_ref_t<nat>(b, 1); }
-var_id const & fn_body_uset_source(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::USet); return cnstr_get_ref_t<var_id>(b, 2); }
-fn_body const & fn_body_uset_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::USet); return cnstr_get_ref_t<fn_body>(b, 3); }
-var_id const & fn_body_sset_target(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SSet); return cnstr_get_ref_t<var_id>(b, 0); }
-nat const & fn_body_sset_idx(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SSet); return cnstr_get_ref_t<nat>(b, 1); }
-nat const & fn_body_sset_offset(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SSet); return cnstr_get_ref_t<nat>(b, 2); }
-var_id const & fn_body_sset_source(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SSet); return cnstr_get_ref_t<var_id>(b, 3); }
-type fn_body_sset_type(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SSet); return cnstr_get_type(b, 4); }
-fn_body const & fn_body_sset_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::SSet); return cnstr_get_ref_t<fn_body>(b, 5); }
-var_id const & fn_body_inc_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Inc); return cnstr_get_ref_t<var_id>(b, 0); }
-nat const & fn_body_inc_val(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Inc); return cnstr_get_ref_t<nat>(b, 1); }
-bool fn_body_inc_maybe_scalar(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Inc); return get_bool_field(b.raw(), 3); }
-fn_body const & fn_body_inc_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Inc); return cnstr_get_ref_t<fn_body>(b, 2); }
-var_id const & fn_body_dec_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Dec); return cnstr_get_ref_t<var_id>(b, 0); }
-nat const & fn_body_dec_val(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Dec); return cnstr_get_ref_t<nat>(b, 1); }
-bool fn_body_dec_maybe_scalar(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Dec); return get_bool_field(b.raw(), 3); }
-fn_body const & fn_body_dec_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Dec); return cnstr_get_ref_t<fn_body>(b, 2); }
-var_id const & fn_body_del_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Del); return cnstr_get_ref_t<var_id>(b, 0); }
-fn_body const & fn_body_del_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Del); return cnstr_get_ref_t<fn_body>(b, 1); }
-object_ref const & fn_body_mdata_data(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::MData); return cnstr_get_ref_t<object_ref>(b, 0); }
-fn_body const & fn_body_mdata_cont(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::MData); return cnstr_get_ref_t<fn_body>(b, 1); }
-name const & fn_body_case_tid(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Case); return cnstr_get_ref_t<name>(b, 0); }
-var_id const & fn_body_case_var(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Case); return cnstr_get_ref_t<var_id>(b, 1); }
-type fn_body_case_var_type(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Case); return cnstr_get_type(b, 2); }
-array_ref<alt_core> const & fn_body_case_alts(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Case); return cnstr_get_ref_t<array_ref<alt_core>>(b, 3); }
-arg const & fn_body_ret_arg(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Ret); return cnstr_get_ref_t<arg>(b, 0); }
-jp_id const & fn_body_jmp_jp(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Jmp); return cnstr_get_ref_t<jp_id>(b, 0); }
-array_ref<arg> const & fn_body_jmp_args(fn_body const & b) { lean_assert(fn_body_tag(b) == fn_body_kind::Jmp); return cnstr_get_ref_t<array_ref<arg>>(b, 1); }
-
-typedef object_ref decl;
-enum class decl_kind { Fun, Extern };
-decl_kind decl_tag(decl const & a) { return is_scalar(a.raw()) ? static_cast<decl_kind>(unbox(a.raw())) : static_cast<decl_kind>(cnstr_tag(a.raw())); }
-fun_id const & decl_fun_id(decl const & b) { return cnstr_get_ref_t<fun_id>(b, 0); }
-array_ref<param> const & decl_params(decl const & b) { return cnstr_get_ref_t<array_ref<param>>(b, 1); }
-type decl_type(decl const & b) { return cnstr_get_type(b, 2); }
-fn_body const & decl_fun_body(decl const & b) { lean_assert(decl_tag(b) == decl_kind::Fun); return cnstr_get_ref_t<fn_body>(b, 3); }
-
 extern "C" object * lean_ir_find_env_decl(object * env, object * n);
 option_ref<decl> find_ir_decl(environment const & env, name const & n) {
     return option_ref<decl>(lean_ir_find_env_decl(env.to_obj_arg(), n.to_obj_arg()));

src/library/compiler/llvm.cpp

@@ -0,0 +1,182 @@
+/*
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Dany Fabian
+*/
+
+#include "library/compiler/llvm.h"
+#include "library/compiler/ir_decode_helpers.h"
+#include "lean/io.h"
+#include "util/object_ref.h"
+#include "util/string_ref.h"
+#include "llvm/Bitcode/BitcodeReader.h"
+#include "llvm/IR/Verifier.h"
+
+namespace lean {
+
+object_ref list_to_array(object_ref list) {
+  return object_ref(lean_list_to_array(box(0), list.to_obj_arg()));
+}
+
+namespace ir {
+
+extern "C" obj_res lean_ir_emit_llvm(b_obj_arg env, b_obj_arg mod_name, obj_arg) {
+    try {
+        LeanIREmitter emitter(environment(env, true), name(mod_name, true));
+        return io_result_mk_ok(emitter.emit().steal());
+    }
+    catch (char const* msg) {
+        return io_result_mk_error(msg);
+    }
+    catch (std::string msg) {
+        return io_result_mk_error(msg);
+    }
+}
+
+LeanIREmitter::LeanIREmitter(environment&& env, name&& mod_name) : env{env}, mod_name{mod_name} {
+    const MemoryBufferRef bufferRef(StringRef(reinterpret_cast<char const*>(&gLeanRuntimeBitCodeData), gLeanRuntimeBitCodeSize), "");
+    Expected<std::unique_ptr<Module>> maybeRuntime = getLazyBitcodeModule(bufferRef, *this);
+    if (Error err = maybeRuntime.takeError()) {
+        throw "could not parse the lean runtime";
+    }
+
+    runtime = std::move(maybeRuntime.get());
+    builder = std::make_unique<IRBuilder<>>(*this);
+}
+
+string_ref LeanIREmitter::emit() {
+    module = std::make_unique<Module>(mod_name.to_string(), *this);
+    module->setDataLayout(runtime->getDataLayout());
+    module->setTargetTriple(runtime->getTargetTriple());
+
+    emitModuleInitializer();
+
+    list_ref<decl> decls = list_ref<decl>(lean_ir_get_decls(env.raw()));
+    for (decl decl : decls) {
+        emitFunction(decl);
+    }
+
+    std::string resStr{};
+    {
+        raw_string_ostream outstr(resStr);
+        outstr << "\n";
+
+        module->print(outstr, nullptr);
+        verifyModule(*module, &outstr);
+    }
+
+    return string_ref(resStr);
+}
+
+string_ref name_mangle(name name) {
+    return string_ref(lean_name_mangle(name.to_obj_arg(), string_ref("l_").to_obj_arg()));
+}
+
+void LeanIREmitter::emitFunction(decl function) {
+    fun_id declName = decl_fun_id(function);
+
+    FunctionCallee func = module->getOrInsertFunction(name_mangle(declName).to_std_string(), Type::getInt32Ty(*this));
+    Function *callee = static_cast<Function *>(func.getCallee()); 
+    BasicBlock *entry = BasicBlock::Create(*this, "entry", callee);
+    builder->SetInsertPoint(entry);
+    builder->CreateRet(ConstantInt::get(Type::getInt32Ty(*this), 42));
+}
+
+string_ref mk_module_initialization_function_name(name name) {
+    return string_ref(lean_mk_module_initialization_function_name(name.to_obj_arg()));
+}
+
+array_ref<name> environment_import_names(environment env) {
+    return array_ref<name>(lean_environment_import_names(env.to_obj_arg()));
+}
+
+void LeanIREmitter::emitModuleInitializer() {
+    IntegerType *boolTy = IntegerType::getInt1Ty(*this);
+    GlobalVariable *initialized = new GlobalVariable(*module, boolTy, false, GlobalVariable::PrivateLinkage, ConstantInt::get(boolTy, 0), "_G_initialized");
+
+    PointerType *lean_obj_ptr = PointerType::get(runtime->getTypeByName("struct.lean_object"), 0);
+    std::string initializerFuncName = mk_module_initialization_function_name(mod_name).to_std_string();
+    FunctionType *initializerFuncType = FunctionType::get(lean_obj_ptr, {lean_obj_ptr}, false);
+    Function *initializerFunc = Function::Create(initializerFuncType, llvm::GlobalValue::ExternalLinkage, initializerFuncName, *module);
+    initializerFunc->getArg(0)->setName("world");
+    BasicBlock *entry = BasicBlock::Create(*this, "entry", initializerFunc);
+    BasicBlock *ifNotInitialized = BasicBlock::Create(*this, "ifNotInitialized", initializerFunc);
+    BasicBlock *returnSuccess = createReturnIOSuccess();
+    initializerFunc->getBasicBlockList().push_back(returnSuccess);
+    builder->SetInsertPoint(entry);
+    LoadInst *initializedDeref = builder->CreateLoad(initialized->getType()->getElementType(), initialized, "isInitialized");
+    builder->CreateCondBr(initializedDeref, returnSuccess, ifNotInitialized);
+    array_ref<name> importNames = environment_import_names(env);
+    BasicBlock *next = returnSuccess;
+    BasicBlock *error = BasicBlock::Create(*this, "error", initializerFunc);
+    std::vector<std::tuple<CallInst *, BasicBlock *>> errorCalls{};
+    for (size_t i = importNames.size(); i > 0; --i)
+    {   
+        std::tuple<CallInst *, BasicBlock*>importRes = emitImportInitializer(importNames[i - 1], error, next);
+        errorCalls.push_back(importRes);
+        next = std::get<1>(importRes);
+    }
+    builder->SetInsertPoint(error);
+    if (errorCalls.size() > 0)
+    {
+        PHINode *phi = builder->CreatePHI(lean_obj_ptr, 0);
+        do {
+            std::tuple<CallInst *, BasicBlock *>errorCall = errorCalls.back();
+            errorCalls.pop_back();
+            phi->addIncoming(std::get<0>(errorCall), std::get<1>(errorCall));
+        } while (errorCalls.size() > 0);
+        builder->CreateRet(phi);
+    }
+    else {
+        builder->CreateUnreachable();
+    }
+
+    builder->SetInsertPoint(ifNotInitialized);
+    builder->CreateStore(ConstantInt::get(boolTy, 1), initialized);
+    builder->CreateBr(next);
+}
+
+std::tuple<CallInst*, BasicBlock *>LeanIREmitter::emitImportInitializer(name importName, BasicBlock *error, BasicBlock *next) {
+    BasicBlock * res = BasicBlock::Create(*this, importName.to_string(), next->getParent(), next);
+    builder->SetInsertPoint(res);
+
+    PointerType *lean_obj_ptr = PointerType::get(runtime->getTypeByName("struct.lean_object"), 0);
+    std::string initializerFuncName = mk_module_initialization_function_name(importName).to_std_string();
+    FunctionType *initializerFuncType = FunctionType::get(lean_obj_ptr, {lean_obj_ptr}, false);
+    Function *initializerFunc = Function::Create(initializerFuncType, llvm::GlobalValue::ExternalLinkage, initializerFuncName, *module);
+    CallInst *initCall = builder->CreateCall(initializerFunc, builder->CreateCall(getRuntimeFunction("lean_io_mk_world")));
+    Value *isNull = builder->CreateICmp(CmpInst::Predicate::ICMP_EQ, initCall, ConstantPointerNull::get(lean_obj_ptr), "isNull");
+
+    BasicBlock *dec = BasicBlock::Create(*this, "dec", next->getParent(), next);
+    builder->CreateCondBr(isNull, error, dec);
+    
+    builder->SetInsertPoint(dec);
+    FunctionCallee lean_dec_ref = getRuntimeFunction("lean_dec_ref");
+    builder->CreateCall(lean_dec_ref, initCall);
+    builder->CreateBr(next);
+    
+    return std::make_tuple(initCall, res);
+}
+
+BasicBlock *LeanIREmitter::createReturnIOSuccess() {
+    BasicBlock *returnSuccess = BasicBlock::Create(*this, "returnSuccess");
+    builder->SetInsertPoint(returnSuccess);
+    FunctionCallee lean_box = getRuntimeFunction("lean_box");
+    FunctionCallee lean_io_result_mk_ok = getRuntimeFunction("lean_io_result_mk_ok");
+    CallInst *box_0 = builder->CreateCall(lean_box.getFunctionType(), lean_box.getCallee(), ConstantInt::get(lean_box.getFunctionType()->getParamType(0), 0));
+    CallInst *world = builder->CreateCall(lean_io_result_mk_ok, box_0);
+    builder->CreateRet(world);
+    return returnSuccess;
+}
+
+FunctionCallee LeanIREmitter::getRuntimeFunction(std::string name) {
+    Function *runtimeFunction = runtime->getFunction(name);
+    if (runtimeFunction == nullptr) throw std::string("could not find runtime function: ").append(name);
+    FunctionCallee res = module->getOrInsertFunction(name, runtimeFunction->getFunctionType());
+    return res;
+}
+
+} // namespace ir
+
+} // namespace lean

src/library/compiler/llvm.h

@@ -0,0 +1,56 @@
+/*
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Dany Fabian
+*/
+
+#pragma once
+#include "lean/object.h"
+#include "util/incbin.h"
+#include "util/object_ref.h"
+#include "util/string_ref.h"
+#include "util/array_ref.h"
+#include "kernel/environment.h"
+#include "library/compiler/ir.h"
+#include <llvm/IR/LLVMContext.h>
+#include <llvm/IR/IRBuilder.h>
+
+using namespace llvm;
+
+namespace lean {
+extern "C" obj_res lean_list_to_array(obj_arg type, obj_arg elems);
+object_ref list_to_array(object_ref list);
+
+namespace ir {
+INCBIN(LeanRuntimeBitCode, "library/compiler/libleanruntime.bc");
+
+extern "C" obj_res lean_ir_get_decls(b_obj_arg env);
+extern "C" obj_res lean_ir_emit_llvm(b_obj_arg env, b_obj_arg mod_name, obj_arg world);
+extern "C" obj_res lean_name_mangle(obj_arg name, obj_arg prefix);
+extern "C" obj_res lean_mk_module_initialization_function_name(obj_arg name);
+extern "C" obj_res lean_environment_import_names(obj_arg name);
+string_ref name_mangle(name name);
+string_ref mk_module_initialization_function_name(name name);
+array_ref<name> environment_import_names(environment env);
+
+class LeanIREmitter : public LLVMContext {
+    const environment env;
+    const name mod_name;
+    std::unique_ptr<const Module> runtime;
+    std::unique_ptr<Module> module;
+    std::unique_ptr<IRBuilder<>> builder;
+    public:
+        LeanIREmitter(environment&& env, name&& mod_name);
+        string_ref emit();
+    private:
+        void emitFunction(decl function);
+        void emitModuleInitializer();
+        std::tuple<CallInst *, BasicBlock *>emitImportInitializer(name importName, BasicBlock *error, BasicBlock *next);
+        BasicBlock *createReturnIOSuccess();
+        FunctionCallee getRuntimeFunction(std::string name);
+};
+
+}
+
+}

src/runtime/CMakeLists.txt

@@ -5,3 +5,13 @@ platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
 process.cpp)
 add_library(runtime OBJECT ${RUNTIME_OBJS})
 add_library(leanruntime ${RUNTIME_OBJS})
+if(LLVM)
+  string(REPLACE ";" " " RUNTIME_OBJS_STR "${RUNTIME_OBJS};lean_inlines.c")
+  add_custom_command(
+    OUTPUT libleanruntime.bc
+    DEPENDS ${RUNTIME_OBJS} lean_inlines.c
+    # compile each runtime file with the original compile flags plus `-emit-llvm`, then `llvm-link` them together
+    COMMAND bash -ec "rm -rf runtmp || true; mkdir runtmp; for f in ${RUNTIME_OBJS_STR}; do ${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} -I$<JOIN:$<TARGET_PROPERTY:leanruntime,INCLUDE_DIRECTORIES>, -I> $([[ $f = \*.cpp ]] || echo \"-x c\") \"${CMAKE_CURRENT_SOURCE_DIR}/$f\" -S -emit-llvm -o runtmp/$f.ll; done; llvm-link runtmp/*.ll -o libleanruntime.bc"
+    VERBATIM)
+  add_custom_target(runtime_bc DEPENDS libleanruntime.bc)
+endif()

src/runtime/lean_inlines.c

@@ -0,0 +1,3 @@
+// generate LLVM IR for `static inline` definitions in lean.h for the LLVM backend
+#define static extern // work around clang not emitting code for unused `static` definitions
+#include <lean/lean.h>

src/shell/CMakeLists.txt

@@ -11,10 +11,13 @@ if(LLVM)
   else()
     set(LLVM_SYSTEM_LIBS "-lz")
   endif()
-  if(${STATIC} AND NOT ("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin"))
-    set(LEAN_EXE_LINKER_FLAGS "`${LLVM_TOOLS_BINARY_DIR}/llvm-config --link-static --ldflags --libs nativecodegen` -Wl,-Bstatic ${LLVM_SYSTEM_LIBS} -Wl,-Bdynamic")
+  if(STATIC)
+    if(NOT "${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")
+      set(LLVM_SYSTEM_LIBS "-Wl,-Bstatic ${LLVM_SYSTEM_LIBS} -Wl,-Bdynamic")
+    endif()
+    set(LEAN_EXE_LINKER_FLAGS "`${LLVM_TOOLS_BINARY_DIR}/llvm-config --link-static --ldflags --libs nativecodegen` ${LLVM_SYSTEM_LIBS}")
   else()
-    set(LEAN_EXE_LINKER_FLAGS "`${LLVM_TOOLS_BINARY_DIR}/llvm-config --ldflags --libs nativecodegen` ${LLVM_SYSTEM_LIBS}")
+    set(LEAN_EXE_LINKER_FLAGS "`llvm-config --ldflags --libs nativecodegen` ${LLVM_SYSTEM_LIBS}")
   endif()
   if (${CMAKE_SYSTEM_NAME} MATCHES "Windows")
     set(LEAN_EXE_LINKER_FLAGS "${LEAN_EXE_LINKER_FLAGS} -lole32 -luuid")
@@ -27,7 +30,7 @@ string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
 add_custom_command(OUTPUT ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}
   COMMAND sh -c "LEANC_GMP=${GMP_LIBRARIES} LEAN_CXX='${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}' ${CMAKE_BINARY_DIR}/bin/leanc $<TARGET_OBJECTS:shell> ${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXE_LINKER_FLAGS} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} -o ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"
   VERBATIM
-  DEPENDS Init Std Lean leancpp shell)
+  DEPENDS Init Std Lean leancpp shell $<IF:$<BOOL:${LLVM}>,runtime_bc,>)
 
 add_custom_target(lean ALL
   DEPENDS ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX})

src/util/incbin.h

@@ -0,0 +1,368 @@
+/**
+ * @file incbin.h
+ * @author Dale Weiler
+ * @brief Utility for including binary files
+ *
+ * Facilities for including binary files into the current translation unit and
+ * making use from them externally in other translation units.
+ */
+#ifndef INCBIN_HDR
+#define INCBIN_HDR
+#include <limits.h>
+#if   defined(__AVX512BW__) || \
+      defined(__AVX512CD__) || \
+      defined(__AVX512DQ__) || \
+      defined(__AVX512ER__) || \
+      defined(__AVX512PF__) || \
+      defined(__AVX512VL__) || \
+      defined(__AVX512F__)
+# define INCBIN_ALIGNMENT_INDEX 6
+#elif defined(__AVX__)      || \
+      defined(__AVX2__)
+# define INCBIN_ALIGNMENT_INDEX 5
+#elif defined(__SSE__)      || \
+      defined(__SSE2__)     || \
+      defined(__SSE3__)     || \
+      defined(__SSSE3__)    || \
+      defined(__SSE4_1__)   || \
+      defined(__SSE4_2__)   || \
+      defined(__neon__)
+# define INCBIN_ALIGNMENT_INDEX 4
+#elif ULONG_MAX != 0xffffffffu
+# define INCBIN_ALIGNMENT_INDEX 3
+# else
+# define INCBIN_ALIGNMENT_INDEX 2
+#endif
+
+/* Lookup table of (1 << n) where `n' is `INCBIN_ALIGNMENT_INDEX' */
+#define INCBIN_ALIGN_SHIFT_0 1
+#define INCBIN_ALIGN_SHIFT_1 2
+#define INCBIN_ALIGN_SHIFT_2 4
+#define INCBIN_ALIGN_SHIFT_3 8
+#define INCBIN_ALIGN_SHIFT_4 16
+#define INCBIN_ALIGN_SHIFT_5 32
+#define INCBIN_ALIGN_SHIFT_6 64
+
+/* Actual alignment value */
+#define INCBIN_ALIGNMENT \
+    INCBIN_CONCATENATE( \
+        INCBIN_CONCATENATE(INCBIN_ALIGN_SHIFT, _), \
+        INCBIN_ALIGNMENT_INDEX)
+
+/* Stringize */
+#define INCBIN_STR(X) \
+    #X
+#define INCBIN_STRINGIZE(X) \
+    INCBIN_STR(X)
+/* Concatenate */
+#define INCBIN_CAT(X, Y) \
+    X ## Y
+#define INCBIN_CONCATENATE(X, Y) \
+    INCBIN_CAT(X, Y)
+/* Deferred macro expansion */
+#define INCBIN_EVAL(X) \
+    X
+#define INCBIN_INVOKE(N, ...) \
+    INCBIN_EVAL(N(__VA_ARGS__))
+
+/* Green Hills uses a different directive for including binary data */
+#if defined(__ghs__)
+#  if (__ghs_asm == 2)
+#    define INCBIN_MACRO ".file"
+/* Or consider the ".myrawdata" entry in the ld file */
+#  else
+#    define INCBIN_MACRO "\tINCBIN"
+#  endif
+#else
+#  define INCBIN_MACRO ".incbin"
+#endif
+
+#ifndef _MSC_VER
+#  define INCBIN_ALIGN \
+    __attribute__((aligned(INCBIN_ALIGNMENT)))
+#else
+#  define INCBIN_ALIGN __declspec(align(INCBIN_ALIGNMENT))
+#endif
+
+#if defined(__arm__) || /* GNU C and RealView */ \
+    defined(__arm) || /* Diab */ \
+    defined(_ARM) /* ImageCraft */
+#  define INCBIN_ARM
+#endif
+
+#ifdef __GNUC__
+/* Utilize .balign where supported */
+#  define INCBIN_ALIGN_HOST ".balign " INCBIN_STRINGIZE(INCBIN_ALIGNMENT) "\n"
+#  define INCBIN_ALIGN_BYTE ".balign 1\n"
+#elif defined(INCBIN_ARM)
+/*
+ * On arm assemblers, the alignment value is calculated as (1 << n) where `n' is
+ * the shift count. This is the value passed to `.align'
+ */
+#  define INCBIN_ALIGN_HOST ".align " INCBIN_STRINGIZE(INCBIN_ALIGNMENT_INDEX) "\n"
+#  define INCBIN_ALIGN_BYTE ".align 0\n"
+#else
+/* We assume other inline assembler's treat `.align' as `.balign' */
+#  define INCBIN_ALIGN_HOST ".align " INCBIN_STRINGIZE(INCBIN_ALIGNMENT) "\n"
+#  define INCBIN_ALIGN_BYTE ".align 1\n"
+#endif
+
+/* INCBIN_CONST is used by incbin.c generated files */
+#if defined(__cplusplus)
+#  define INCBIN_EXTERNAL extern "C"
+#  define INCBIN_CONST    extern const
+#else
+#  define INCBIN_EXTERNAL extern
+#  define INCBIN_CONST    const
+#endif
+
+/**
+ * @brief Optionally override the linker section into which data is emitted.
+ *
+ * @warning If you use this facility, you'll have to deal with platform-specific linker output
+ * section naming on your own
+ *
+ * Overriding the default linker output section, e.g for esp8266/Arduino:
+ * @code
+ * #define INCBIN_OUTPUT_SECTION ".irom.text"
+ * #include "incbin.h"
+ * INCBIN(Foo, "foo.txt");
+ * // Data is emitted into program memory that never gets copied to RAM
+ * @endcode
+ */
+#if !defined(INCBIN_OUTPUT_SECTION)
+#  if defined(__APPLE__)
+#    define INCBIN_OUTPUT_SECTION         ".const_data"
+#  else
+#    define INCBIN_OUTPUT_SECTION         ".rodata"
+#  endif
+#endif
+
+#if defined(__APPLE__)
+/* The directives are different for Apple branded compilers */
+#  define INCBIN_SECTION         INCBIN_OUTPUT_SECTION "\n"
+#  define INCBIN_GLOBAL(NAME)    ".globl " INCBIN_MANGLE INCBIN_STRINGIZE(INCBIN_PREFIX) #NAME "\n"
+#  define INCBIN_INT             ".long "
+#  define INCBIN_MANGLE          "_"
+#  define INCBIN_BYTE            ".byte "
+#  define INCBIN_TYPE(...)
+#else
+#  define INCBIN_SECTION         ".section " INCBIN_OUTPUT_SECTION "\n"
+#  define INCBIN_GLOBAL(NAME)    ".global " INCBIN_STRINGIZE(INCBIN_PREFIX) #NAME "\n"
+#  if defined(__ghs__)
+#    define INCBIN_INT           ".word "
+#  else
+#    define INCBIN_INT           ".int "
+#  endif
+#  if defined(__USER_LABEL_PREFIX__)
+#    define INCBIN_MANGLE        INCBIN_STRINGIZE(__USER_LABEL_PREFIX__)
+#  else
+#    define INCBIN_MANGLE        ""
+#  endif
+#  if defined(INCBIN_ARM)
+/* On arm assemblers, `@' is used as a line comment token */
+#    define INCBIN_TYPE(NAME)    ".type " INCBIN_STRINGIZE(INCBIN_PREFIX) #NAME ", %object\n"
+#  elif defined(__MINGW32__) || defined(__MINGW64__)
+/* Mingw doesn't support this directive either */
+#    define INCBIN_TYPE(NAME)
+#  else
+/* It's safe to use `@' on other architectures */
+#    define INCBIN_TYPE(NAME)    ".type " INCBIN_STRINGIZE(INCBIN_PREFIX) #NAME ", @object\n"
+#  endif
+#  define INCBIN_BYTE            ".byte "
+#endif
+
+/* List of style types used for symbol names */
+#define INCBIN_STYLE_CAMEL 0
+#define INCBIN_STYLE_SNAKE 1
+
+/**
+ * @brief Specify the prefix to use for symbol names.
+ *
+ * By default this is `g', producing symbols of the form:
+ * @code
+ * #include "incbin.h"
+ * INCBIN(Foo, "foo.txt");
+ *
+ * // Now you have the following symbols:
+ * // const unsigned char gFooData[];
+ * // const unsigned char *const gFooEnd;
+ * // const unsigned int gFooSize;
+ * @endcode
+ *
+ * If however you specify a prefix before including: e.g:
+ * @code
+ * #define INCBIN_PREFIX incbin
+ * #include "incbin.h"
+ * INCBIN(Foo, "foo.txt");
+ *
+ * // Now you have the following symbols instead:
+ * // const unsigned char incbinFooData[];
+ * // const unsigned char *const incbinFooEnd;
+ * // const unsigned int incbinFooSize;
+ * @endcode
+ */
+#if !defined(INCBIN_PREFIX)
+#  define INCBIN_PREFIX g
+#endif
+
+/**
+ * @brief Specify the style used for symbol names.
+ *
+ * Possible options are
+ * - INCBIN_STYLE_CAMEL "CamelCase"
+ * - INCBIN_STYLE_SNAKE "snake_case"
+ *
+ * Default option is *INCBIN_STYLE_CAMEL* producing symbols of the form:
+ * @code
+ * #include "incbin.h"
+ * INCBIN(Foo, "foo.txt");
+ *
+ * // Now you have the following symbols:
+ * // const unsigned char <prefix>FooData[];
+ * // const unsigned char *const <prefix>FooEnd;
+ * // const unsigned int <prefix>FooSize;
+ * @endcode
+ *
+ * If however you specify a style before including: e.g:
+ * @code
+ * #define INCBIN_STYLE INCBIN_STYLE_SNAKE
+ * #include "incbin.h"
+ * INCBIN(foo, "foo.txt");
+ *
+ * // Now you have the following symbols:
+ * // const unsigned char <prefix>foo_data[];
+ * // const unsigned char *const <prefix>foo_end;
+ * // const unsigned int <prefix>foo_size;
+ * @endcode
+ */
+#if !defined(INCBIN_STYLE)
+#  define INCBIN_STYLE INCBIN_STYLE_CAMEL
+#endif
+
+/* Style lookup tables */
+#define INCBIN_STYLE_0_DATA Data
+#define INCBIN_STYLE_0_END End
+#define INCBIN_STYLE_0_SIZE Size
+#define INCBIN_STYLE_1_DATA _data
+#define INCBIN_STYLE_1_END _end
+#define INCBIN_STYLE_1_SIZE _size
+
+/* Style lookup: returning identifier */
+#define INCBIN_STYLE_IDENT(TYPE) \
+    INCBIN_CONCATENATE( \
+        INCBIN_STYLE_, \
+        INCBIN_CONCATENATE( \
+            INCBIN_EVAL(INCBIN_STYLE), \
+            INCBIN_CONCATENATE(_, TYPE)))
+
+/* Style lookup: returning string literal */
+#define INCBIN_STYLE_STRING(TYPE) \
+    INCBIN_STRINGIZE( \
+        INCBIN_STYLE_IDENT(TYPE)) \
+
+/* Generate the global labels by indirectly invoking the macro with our style
+ * type and concatenating the name against them. */
+#define INCBIN_GLOBAL_LABELS(NAME, TYPE) \
+    INCBIN_INVOKE( \
+        INCBIN_GLOBAL, \
+        INCBIN_CONCATENATE( \
+            NAME, \
+            INCBIN_INVOKE( \
+                INCBIN_STYLE_IDENT, \
+                TYPE))) \
+    INCBIN_INVOKE( \
+        INCBIN_TYPE, \
+        INCBIN_CONCATENATE( \
+            NAME, \
+            INCBIN_INVOKE( \
+                INCBIN_STYLE_IDENT, \
+                TYPE)))
+
+/**
+ * @brief Externally reference binary data included in another translation unit.
+ *
+ * Produces three external symbols that reference the binary data included in
+ * another translation unit.
+ *
+ * The symbol names are a concatenation of `INCBIN_PREFIX' before *NAME*; with
+ * "Data", as well as "End" and "Size" after. An example is provided below.
+ *
+ * @param NAME The name given for the binary data
+ *
+ * @code
+ * INCBIN_EXTERN(Foo);
+ *
+ * // Now you have the following symbols:
+ * // extern const unsigned char <prefix>FooData[];
+ * // extern const unsigned char *const <prefix>FooEnd;
+ * // extern const unsigned int <prefix>FooSize;
+ * @endcode
+ */
+#define INCBIN_EXTERN(NAME) \
+    INCBIN_EXTERNAL const INCBIN_ALIGN unsigned char \
+        INCBIN_CONCATENATE( \
+            INCBIN_CONCATENATE(INCBIN_PREFIX, NAME), \
+            INCBIN_STYLE_IDENT(DATA))[]; \
+    INCBIN_EXTERNAL const INCBIN_ALIGN unsigned char *const \
+    INCBIN_CONCATENATE( \
+        INCBIN_CONCATENATE(INCBIN_PREFIX, NAME), \
+        INCBIN_STYLE_IDENT(END)); \
+    INCBIN_EXTERNAL const unsigned int \
+        INCBIN_CONCATENATE( \
+            INCBIN_CONCATENATE(INCBIN_PREFIX, NAME), \
+            INCBIN_STYLE_IDENT(SIZE))
+
+/**
+ * @brief Include a binary file into the current translation unit.
+ *
+ * Includes a binary file into the current translation unit, producing three symbols
+ * for objects that encode the data and size respectively.
+ *
+ * The symbol names are a concatenation of `INCBIN_PREFIX' before *NAME*; with
+ * "Data", as well as "End" and "Size" after. An example is provided below.
+ *
+ * @param NAME The name to associate with this binary data (as an identifier.)
+ * @param FILENAME The file to include (as a string literal.)
+ *
+ * @code
+ * INCBIN(Icon, "icon.png");
+ *
+ * // Now you have the following symbols:
+ * // const unsigned char <prefix>IconData[];
+ * // const unsigned char *const <prefix>IconEnd;
+ * // const unsigned int <prefix>IconSize;
+ * @endcode
+ *
+ * @warning This must be used in global scope
+ * @warning The identifiers may be different if INCBIN_STYLE is not default
+ *
+ * To externally reference the data included by this in another translation unit
+ * please @see INCBIN_EXTERN.
+ */
+#ifdef _MSC_VER
+#define INCBIN(NAME, FILENAME) \
+    INCBIN_EXTERN(NAME)
+#else
+#define INCBIN(NAME, FILENAME) \
+    __asm__(INCBIN_SECTION \
+            INCBIN_GLOBAL_LABELS(NAME, DATA) \
+            INCBIN_ALIGN_HOST \
+            INCBIN_MANGLE INCBIN_STRINGIZE(INCBIN_PREFIX) #NAME INCBIN_STYLE_STRING(DATA) ":\n" \
+            INCBIN_MACRO " \"" FILENAME "\"\n" \
+            INCBIN_GLOBAL_LABELS(NAME, END) \
+            INCBIN_ALIGN_BYTE \
+            INCBIN_MANGLE INCBIN_STRINGIZE(INCBIN_PREFIX) #NAME INCBIN_STYLE_STRING(END) ":\n" \
+                INCBIN_BYTE "1\n" \
+            INCBIN_GLOBAL_LABELS(NAME, SIZE) \
+            INCBIN_ALIGN_HOST \
+            INCBIN_MANGLE INCBIN_STRINGIZE(INCBIN_PREFIX) #NAME INCBIN_STYLE_STRING(SIZE) ":\n" \
+                INCBIN_INT INCBIN_MANGLE INCBIN_STRINGIZE(INCBIN_PREFIX) #NAME INCBIN_STYLE_STRING(END) " - " \
+                           INCBIN_MANGLE INCBIN_STRINGIZE(INCBIN_PREFIX) #NAME INCBIN_STYLE_STRING(DATA) "\n" \
+            INCBIN_ALIGN_HOST \
+            ".text\n" \
+    ); \
+    INCBIN_EXTERN(NAME)
+
+#endif
+#endif

tests/playground/emitLLVM.lean

@@ -0,0 +1,39 @@
+import Lean
+open Lean
+
+
+def foo (x : Nat) : Nat :=
+  x + x + x
+
+#eval (do
+  let env ← getEnv
+  IR.emitC env `myModule |> IO.println 
+  let res ← IR.emitLLVM env `myModule 
+  IO.println res
+  : MetaM Unit)
+
+def test : MetaM Unit := do
+  let env ← getEnv
+  -- let module := env.mainModule
+  let res ← IR.emitLLVM env `myModule
+  IO.println res
+
+-- #eval test
+
+def test2 : MetaM Unit := do
+  let env ← getEnv
+  let module := env.mainModule
+  IO.println $ (IR.getDecls env).map (·.name)
+
+-- #eval test2
+
+def showIR (n : Name) : MetaM Unit := do
+  let env ← getEnv
+  let myDecls := IR.getDecls env
+  if let some decl := IR.findEnvDecl env n then
+    IO.println decl
+  else
+    throwError "not found"
+
+#eval showIR ``foo
+-- #eval showIR `test._rarg._closed_1

tests/playground/lowlevel.lean

@@ -0,0 +1,70 @@
+import Lean.Meta
+import Lean.Compiler.IR
+open Lean
+
+inductive LowLevelType where
+| Integer (bits : Nat)
+| Function (args : Array LowLevelType) (ret : LowLevelType)
+| Pointer (target : LowLevelType)
+| Struct (name : String) (fields : Array (String × LowLevelType))
+| Alias (name : String) (type : LowLevelType)
+
+open LowLevelType
+
+inductive LowLevelExpr : LowLevelType → Type where
+| Const (bits : Nat) (value : Fin (2 ^ bits)) : LowLevelExpr (Integer bits)
+
+open LowLevelExpr
+
+def ByteValue := LowLevelExpr (Integer 8)
+def BoolValue := LowLevelExpr (Integer 1)
+
+def ppBool : BoolValue → String 
+| Const _ ⟨1, _⟩ => "true"
+| Const _ ⟨0, _⟩ => "false"
+
+instance : ToString BoolValue := ⟨ppBool⟩
+
+def mkByte (n : Nat) : ByteValue := LowLevelExpr.Const 8 (Fin.ofNat n)
+def mkBool : Bool → BoolValue
+| true => LowLevelExpr.Const 1 ⟨1, rfl⟩
+| false => LowLevelExpr.Const 1 ⟨0, rfl⟩
+
+
+def LeanArray := mkByte 246
+def LeanStructArray := mkByte 247
+def LeanScalarArray := mkByte 248
+def LeanString := mkByte 249
+
+class HasBEq (α : LowLevelType) where
+  beq : LowLevelExpr α → LowLevelExpr α → BoolValue 
+
+infix:50 " == " => HasBEq.beq
+
+def compareInt {bits : Nat} : LowLevelExpr (Integer bits) → LowLevelExpr (Integer bits) → BoolValue
+| Const _ x, Const _ y => mkBool $ x == y
+
+instance {bits : Nat} : HasBEq (Integer bits) := ⟨compareInt⟩
+
+class HasOr where
+  or : BoolValue → BoolValue → BoolValue
+
+infixl:30 " || " => HasOr.or
+
+def orBool : BoolValue → BoolValue → BoolValue
+| Const _ ⟨0, _⟩, Const _ ⟨0, _⟩ => mkBool false
+| _, _ => mkBool true
+
+instance : HasOr := ⟨orBool⟩
+
+
+def lean_is_big_object_tag (tag : ByteValue) :=
+  tag == LeanArray || tag == LeanStructArray || tag == LeanScalarArray || tag == LeanString
+
+def test : MetaM Unit := 
+  let expr := lean_is_big_object_tag (mkByte 247)
+  IO.println s!"{expr}"
+
+
+#eval Lean.IR.emitLLVM
+#eval test