def Lean.IR.leanMainFn : String

def Lean.IR.LLVM.size_tType (llvmctx : LLVM.Context) : BaseIO (LLVM.LLVMType llvmctx)

def Lean.IR.LLVM.unsignedType (llvmctx : LLVM.Context) : BaseIO (LLVM.LLVMType llvmctx)

def Lean.IR.LLVM.getOrAddFunction {ctx : LLVM.Context} (m : LLVM.Module ctx) (name : String) (type : LLVM.LLVMType ctx) : BaseIO (LLVM.Value ctx)

def Lean.IR.LLVM.getOrAddGlobal {ctx : LLVM.Context} (m : LLVM.Module ctx) (name : String) (type : LLVM.LLVMType ctx) : BaseIO (LLVM.Value ctx)

structure Lean.IR.EmitLLVM.Context (llvmctx : LLVM.Context) : Type

• env : Environment
• modName : Name
• jpMap : JPParamsMap
• mainFn : FunId
• mainParams : Array Param
• llvmmodule : LLVM.Module llvmctx

structure Lean.IR.EmitLLVM.State (llvmctx : LLVM.Context) : Type

• var2val : Std.HashMap VarId (LLVM.LLVMType llvmctx × LLVM.Value llvmctx)
• jp2bb : Std.HashMap JoinPointId (LLVM.BasicBlock llvmctx)

@[reducible, inline]

abbrev Lean.IR.EmitLLVM.Error : Type

@[reducible, inline]

abbrev Lean.IR.EmitLLVM.M (llvmctx : LLVM.Context) (α : Type) : Type

instance Lean.IR.EmitLLVM.instInhabitedM {llvmctx : LLVM.Context} {α : Type} : Inhabited (M llvmctx α)

def Lean.IR.EmitLLVM.addVartoState {llvmctx : LLVM.Context} (x : VarId) (v : LLVM.Value llvmctx) (ty : LLVM.LLVMType llvmctx) : M llvmctx Unit

def Lean.IR.EmitLLVM.addJpTostate {llvmctx : LLVM.Context} (jp : JoinPointId) (bb : LLVM.BasicBlock llvmctx) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitJp {llvmctx : LLVM.Context} (jp : JoinPointId) : M llvmctx (LLVM.BasicBlock llvmctx)

def Lean.IR.EmitLLVM.getLLVMModule {llvmctx : LLVM.Context} : M llvmctx (LLVM.Module llvmctx)

def Lean.IR.EmitLLVM.getEnv {llvmctx : LLVM.Context} : M llvmctx Environment

def Lean.IR.EmitLLVM.getModName {llvmctx : LLVM.Context} : M llvmctx Name

def Lean.IR.EmitLLVM.getDecl {llvmctx : LLVM.Context} (n : Name) : M llvmctx Decl

def Lean.IR.EmitLLVM.constInt8 {llvmctx : LLVM.Context} (n : Nat) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.constInt64 {llvmctx : LLVM.Context} (n : Nat) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.constIntSizeT {llvmctx : LLVM.Context} (n : Nat) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.constIntUnsigned {llvmctx : LLVM.Context} (n : Nat) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.getOrCreateFunctionPrototype {llvmctx : LLVM.Context} (mod : LLVM.Module llvmctx) (retty : LLVM.LLVMType llvmctx) (name : String) (args : Array (LLVM.LLVMType llvmctx)) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.callLeanBox {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (arg : LLVM.Value llvmctx) (name : String := "") : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.callLeanMarkPersistentFn {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (arg : LLVM.Value llvmctx) : M llvmctx Unit

inductive Lean.IR.EmitLLVM.RefcountKind : Type

• inc : RefcountKind
• dec : RefcountKind

instance Lean.IR.EmitLLVM.instToStringRefcountKind : ToString RefcountKind

def Lean.IR.EmitLLVM.callLeanRefcountFn {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (kind : RefcountKind) (checkRef? : Bool) (arg : LLVM.Value llvmctx) (delta : Option (LLVM.Value llvmctx) := none) : M llvmctx Unit

def Lean.IR.EmitLLVM.callLeanDecRef {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (res : LLVM.Value llvmctx) : M llvmctx Unit

def Lean.IR.EmitLLVM.callLeanUnsignedToNatFn {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (n : Nat) (name : String := "") : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.callLeanMkStringUncheckedFn {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (strPtr nBytes nChars : LLVM.Value llvmctx) (name : String) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.callLeanMkString {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (strPtr : LLVM.Value llvmctx) (name : String) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.callLeanCStrToNatFn {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (n : Nat) (name : String := "") : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.callLeanIOMkWorld {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.callLeanIOResultIsError {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (arg : LLVM.Value llvmctx) (name : String := "") : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.callLeanAllocCtor {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (tag num_objs scalar_sz : Nat) (name : String := "") : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.callLeanCtorSet {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (o i v : LLVM.Value llvmctx) : M llvmctx Unit

def Lean.IR.EmitLLVM.callLeanIOResultMKOk {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (v : LLVM.Value llvmctx) (name : String := "") : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.callLeanAllocClosureFn {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (f arity nys : LLVM.Value llvmctx) (retName : String := "") : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.callLeanClosureSetFn {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (closure ix arg : LLVM.Value llvmctx) (retName : String := "") : M llvmctx Unit

def Lean.IR.EmitLLVM.callLeanObjTag {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (closure : LLVM.Value llvmctx) (retName : String := "") : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.callLeanIOResultGetValue {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (v : LLVM.Value llvmctx) (name : String := "") : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.callLeanCtorRelease {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (closure i : LLVM.Value llvmctx) (retName : String := "") : M llvmctx Unit

def Lean.IR.EmitLLVM.callLeanCtorSetTag {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (closure i : LLVM.Value llvmctx) (retName : String := "") : M llvmctx Unit

def Lean.IR.EmitLLVM.toLLVMType {llvmctx : LLVM.Context} (t : IRType) : M llvmctx (LLVM.LLVMType llvmctx)

def Lean.IR.EmitLLVM.throwInvalidExportName {llvmctx : LLVM.Context} {α : Type} (n : Name) : M llvmctx α

def Lean.IR.EmitLLVM.toCName {llvmctx : LLVM.Context} (n : Name) : M llvmctx String

def Lean.IR.EmitLLVM.toCInitName {llvmctx : LLVM.Context} (n : Name) : M llvmctx String

inductive Lean.IR.EmitLLVM.ShouldForwardControlFlow : Type

LLVM Control flow Utilities

• yes : ShouldForwardControlFlow
• no : ShouldForwardControlFlow

def Lean.IR.EmitLLVM.builderGetInsertionFn {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.builderAppendBasicBlock {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (name : String) : M llvmctx (LLVM.BasicBlock llvmctx)

def Lean.IR.EmitLLVM.buildPrologueAlloca {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (ty : LLVM.LLVMType llvmctx) (name : String := "") : M llvmctx (LLVM.Value llvmctx)

Add an alloca to the first BB of the current function. The builders final position will be the end of the BB that we came from.

If it is possible to put an alloca in the first BB this approach is to be preferred over putting it in other BBs. This is because mem2reg only inspects allocas in the first BB, leading to missed optimizations for allocas in other BBs.

def Lean.IR.EmitLLVM.buildWhile_ {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (name : String) (condcodegen : LLVM.Builder llvmctx → M llvmctx (LLVM.Value llvmctx)) (bodycodegen : LLVM.Builder llvmctx → M llvmctx Unit) : M llvmctx Unit

def Lean.IR.EmitLLVM.buildIfThen_ {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (name : String) (brval : LLVM.Value llvmctx) (thencodegen : LLVM.Builder llvmctx → M llvmctx ShouldForwardControlFlow) : M llvmctx Unit

def Lean.IR.EmitLLVM.buildIfThenElse_ {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (name : String) (brval : LLVM.Value llvmctx) (thencodegen elsecodegen : LLVM.Builder llvmctx → M llvmctx ShouldForwardControlFlow) : M llvmctx Unit

def Lean.IR.EmitLLVM.buildLeanBoolTrue? {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (b : LLVM.Value llvmctx) (name : String := "") : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.emitFnDeclAux {llvmctx : LLVM.Context} (mod : LLVM.Module llvmctx) (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.emitFnDecl {llvmctx : LLVM.Context} (decl : Decl) (isExternal : Bool) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitExternDeclAux {llvmctx : LLVM.Context} (decl : Decl) (cNameStr : String) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitFnDecls {llvmctx : LLVM.Context} : M llvmctx Unit

def Lean.IR.EmitLLVM.emitLhsSlot_ {llvmctx : LLVM.Context} (x : VarId) : M llvmctx (LLVM.LLVMType llvmctx × LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.emitLhsVal {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (x : VarId) (name : String := "") : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.emitLhsSlotStore {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (x : VarId) (v : LLVM.Value llvmctx) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitArgSlot_ {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (x : Arg) : M llvmctx (LLVM.LLVMType llvmctx × LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.emitArgVal {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (x : Arg) (name : String := "") : M llvmctx (LLVM.LLVMType llvmctx × LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.emitAllocCtor {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (c : CtorInfo) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.emitCtorSetArgs {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (z : VarId) (ys : Array Arg) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitCtor {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (z : VarId) (c : CtorInfo) (ys : Array Arg) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitInc {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (x : VarId) (n : Nat) (checkRef? : Bool) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitDec {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (x : VarId) (n : Nat) (checkRef? : Bool) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitNumLit {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (t : IRType) (v : Nat) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.toHexDigit (c : Nat) : String

def Lean.IR.EmitLLVM.quoteString (s : String) : String

def Lean.IR.EmitLLVM.emitSimpleExternalCall {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (f : String) (ps : Array Param) (ys : Array Arg) (retty : IRType) (name : String) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.emitExternCall {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (f : FunId) (ps : Array Param) (extData : ExternAttrData) (ys : Array Arg) (retty : IRType) (name : String := "") : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.getFunIdTy {llvmctx : LLVM.Context} (f : FunId) : M llvmctx (LLVM.LLVMType llvmctx)

def Lean.IR.EmitLLVM.getOrAddFunIdValue {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (f : FunId) : M llvmctx (LLVM.Value llvmctx)

Create a function declaration and return a pointer to the function. If the function actually takes arguments, then we must have a function pointer in scope. If the function takes no arguments, then it is a top-level closed term, and its value will be stored in a global pointer. So, we load from the global pointer. The type of the global is function pointer pointer. This returns a function pointer.

def Lean.IR.EmitLLVM.emitPartialApp {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (z : VarId) (f : FunId) (ys : Array Arg) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitApp {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (z f : VarId) (ys : Array Arg) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitFullApp {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (z : VarId) (f : FunId) (ys : Array Arg) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitLit {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (z : VarId) (t : IRType) (v : LitVal) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.callLeanCtorGet {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (x i : LLVM.Value llvmctx) (retName : String) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.emitProj {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (z : VarId) (i : Nat) (x : VarId) : M llvmctx Unit

def Lean.IR.EmitLLVM.callLeanCtorGetUsize {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (x i : LLVM.Value llvmctx) (retName : String) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.emitUProj {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (z : VarId) (i : Nat) (x : VarId) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitOffset {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (n offset : Nat) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.emitSProj {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (z : VarId) (t : IRType) (n offset : Nat) (x : VarId) : M llvmctx Unit

def Lean.IR.EmitLLVM.callLeanIsExclusive {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (closure : LLVM.Value llvmctx) (retName : String := "") : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.callLeanIsScalar {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (closure : LLVM.Value llvmctx) (retName : String := "") : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.emitIsShared {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (z x : VarId) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitBox {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (z x : VarId) (xType : IRType) : M llvmctx Unit

def Lean.IR.EmitLLVM.IRType.isIntegerType (t : IRType) : Bool

def Lean.IR.EmitLLVM.callUnboxForType {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (t : IRType) (v : LLVM.Value llvmctx) (retName : String := "") : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.emitUnbox {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (z : VarId) (t : IRType) (x : VarId) (retName : String := "") : M llvmctx Unit

def Lean.IR.EmitLLVM.emitReset {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (z : VarId) (n : Nat) (x : VarId) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitReuse {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (z x : VarId) (c : CtorInfo) (updtHeader : Bool) (ys : Array Arg) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitVDecl {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (z : VarId) (t : IRType) (v : Expr) : M llvmctx Unit

def Lean.IR.EmitLLVM.declareVar {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (x : VarId) (t : IRType) : M llvmctx Unit

partial def Lean.IR.EmitLLVM.declareVars {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (f : FnBody) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitTag {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (x : VarId) (xType : IRType) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.emitSet {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) (y : Arg) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitUSet {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) (y : VarId) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitTailCall {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (f : FunId) (v : Expr) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitJmp {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (jp : JoinPointId) (xs : Array Arg) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitSSet {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (x : VarId) (n offset : Nat) (y : VarId) (t : IRType) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitDel {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (x : VarId) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitSetTag {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) : M llvmctx Unit

def Lean.IR.EmitLLVM.ensureHasDefault' (alts : Array Alt) : Array Alt

partial def Lean.IR.EmitLLVM.emitCase {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (x : VarId) (xType : IRType) (alts : Array Alt) : M llvmctx Unit

partial def Lean.IR.EmitLLVM.emitJDecl {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (jp : JoinPointId) (_ps : Array Param) (b : FnBody) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitUnreachable {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) : M llvmctx Unit

partial def Lean.IR.EmitLLVM.emitBlock {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (b : FnBody) : M llvmctx Unit

partial def Lean.IR.EmitLLVM.emitFnBody {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (b : FnBody) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitFnArgs {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (needsPackedArgs? : Bool) (llvmfn : LLVM.Value llvmctx) (params : Array Param) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitDeclAux {llvmctx : LLVM.Context} (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) (d : Decl) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitDecl {llvmctx : LLVM.Context} (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) (d : Decl) : M llvmctx Unit

def Lean.IR.EmitLLVM.emitFns {llvmctx : LLVM.Context} (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M llvmctx Unit

def Lean.IR.EmitLLVM.callIODeclInitFn {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (initFnName : String) (world : LLVM.Value llvmctx) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.callPureDeclInitFn {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (initFnName : String) (retty : LLVM.LLVMType llvmctx) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.emitDeclInit {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (parentFn : LLVM.Value llvmctx) (d : Decl) : M llvmctx Unit

def Lean.IR.EmitLLVM.callModInitFn {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (modName : Name) (input world : LLVM.Value llvmctx) (retName : String) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.emitInitFn {llvmctx : LLVM.Context} (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M llvmctx Unit

def Lean.IR.EmitLLVM.callLeanInitialize {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) : M llvmctx Unit

def Lean.IR.EmitLLVM.callLeanInitializeRuntimeModule {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) : M llvmctx Unit

def Lean.IR.EmitLLVM.callLeanSetPanicMessages {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (enable? : LLVM.Value llvmctx) : M llvmctx Unit

def Lean.IR.EmitLLVM.callLeanIOMarkEndInitialization {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) : M llvmctx Unit

def Lean.IR.EmitLLVM.callLeanIOResultIsOk {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (arg : LLVM.Value llvmctx) (name : String := "") : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.callLeanInitTaskManager {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) : M llvmctx Unit

def Lean.IR.EmitLLVM.callLeanFinalizeTaskManager {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) : M llvmctx Unit

def Lean.IR.EmitLLVM.callLeanUnboxUint32 {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (v : LLVM.Value llvmctx) (name : String := "") : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.callLeanIOResultShowError {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (v : LLVM.Value llvmctx) (name : String := "") : M llvmctx Unit

def Lean.IR.EmitLLVM.callLeanMainFn {llvmctx : LLVM.Context} (builder : LLVM.Builder llvmctx) (argv? : Option (LLVM.Value llvmctx)) (world : LLVM.Value llvmctx) (name : String) : M llvmctx (LLVM.Value llvmctx)

def Lean.IR.EmitLLVM.emitMainFn {llvmctx : LLVM.Context} (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M llvmctx Unit

def Lean.IR.EmitLLVM.hasMainFn {llvmctx : LLVM.Context} : M llvmctx Bool

def Lean.IR.EmitLLVM.emitMainFnIfNeeded {llvmctx : LLVM.Context} (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M llvmctx Unit

def Lean.IR.EmitLLVM.main {llvmctx : LLVM.Context} : M llvmctx Unit

def Lean.IR.getLeanHBcPath : IO System.FilePath

def Lean.IR.getModuleGlobals {llvmctx : LLVM.Context} (mod : LLVM.Module llvmctx) : IO (Array (LLVM.Value llvmctx))

Get the names of all global symbols in the module

partial def Lean.IR.getModuleGlobals.go {llvmctx : LLVM.Context} (v : LLVM.Value llvmctx) (acc : Array (LLVM.Value llvmctx)) : IO (Array (LLVM.Value llvmctx))

def Lean.IR.getModuleFunctions {llvmctx : LLVM.Context} (mod : LLVM.Module llvmctx) : IO (Array (LLVM.Value llvmctx))

Get the names of all global functions in the module

partial def Lean.IR.getModuleFunctions.go {llvmctx : LLVM.Context} (v : LLVM.Value llvmctx) (acc : Array (LLVM.Value llvmctx)) : IO (Array (LLVM.Value llvmctx))

@[export lean_ir_emit_llvm]

def Lean.IR.emitLLVM (env : Environment) (modName : Name) (filepath : String) : IO Unit

emitLLVM is the entrypoint for the lean shell to code generate LLVM.