def Lean.IR.leanMainFn : String

Equations

• Lean.IR.leanMainFn = "_lean_main"

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

Equations

• Lean.IR.LLVM.size_tType llvmctx = LLVM.i64Type llvmctx

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

Equations

• Lean.IR.LLVM.unsignedType llvmctx = LLVM.i32Type llvmctx

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.IR.LLVM.getOrAddGlobal m name type = do let __do_lift ← LLVM.getNamedGlobal m name match __do_lift with | some fn => pure fn | none => LLVM.addGlobal m name type

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

Equations

• Lean.IR.EmitLLVM.Error = String

@[reducible, inline]

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

Equations

• Lean.IR.EmitLLVM.M llvmctx = StateRefT' IO.RealWorld (Lean.IR.EmitLLVM.State llvmctx) (ReaderT (Lean.IR.EmitLLVM.Context llvmctx) (ExceptT Lean.IR.EmitLLVM.Error IO))

Instances For

• Lean.IR.EmitLLVM.instInhabitedM

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

Equations

• Lean.IR.EmitLLVM.instInhabitedM = { default := throw "Error: inhabitant" }

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

Equations

• Lean.IR.EmitLLVM.addVartoState x v ty = modify fun (s : Lean.IR.EmitLLVM.State llvmctx) => { var2val := s.var2val.insert x (ty, v), jp2bb := s.jp2bb }

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

Equations

• Lean.IR.EmitLLVM.addJpTostate jp bb = modify fun (s : Lean.IR.EmitLLVM.State llvmctx) => { var2val := s.var2val, jp2bb := s.jp2bb.insert jp bb }

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

Equations

• Lean.IR.EmitLLVM.emitJp jp = do let state ← get match state.jp2bb[jp]? with | some bb => pure bb | none => throw (toString "unable to find join point " ++ toString jp ++ toString "")

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

Equations

• Lean.IR.EmitLLVM.getLLVMModule = Lean.IR.EmitLLVM.Context.llvmmodule <$> read

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

Equations

• Lean.IR.EmitLLVM.getEnv = Lean.IR.EmitLLVM.Context.env <$> read

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

Equations

• Lean.IR.EmitLLVM.getModName = Lean.IR.EmitLLVM.Context.modName <$> read

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.IR.EmitLLVM.constInt8 n = liftM (LLVM.constInt8 llvmctx (UInt64.ofNat n))

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

Equations

• Lean.IR.EmitLLVM.constInt64 n = liftM (LLVM.constInt64 llvmctx (UInt64.ofNat n))

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

Equations

• Lean.IR.EmitLLVM.constIntSizeT n = liftM (LLVM.constIntSizeT llvmctx (UInt64.ofNat n))

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

Equations

• Lean.IR.EmitLLVM.constIntUnsigned n = liftM (LLVM.constIntUnsigned llvmctx (UInt64.ofNat n))

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)

Equations

• Lean.IR.EmitLLVM.getOrCreateFunctionPrototype mod retty name args = do let __do_lift ← liftM (LLVM.functionType retty args) liftM (Lean.IR.LLVM.getOrAddFunction mod name __do_lift)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

inductive Lean.IR.EmitLLVM.RefcountKind : Type

• inc : RefcountKind
• dec : RefcountKind

Instances For

• Lean.IR.EmitLLVM.instToStringRefcountKind

instance Lean.IR.EmitLLVM.instToStringRefcountKind : ToString RefcountKind

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.IR.EmitLLVM.toLLVMType Lean.IR.IRType.float = liftM (LLVM.doubleTypeInContext llvmctx)
• Lean.IR.EmitLLVM.toLLVMType Lean.IR.IRType.float32 = liftM (LLVM.floatTypeInContext llvmctx)
• Lean.IR.EmitLLVM.toLLVMType Lean.IR.IRType.uint8 = liftM (LLVM.intTypeInContext llvmctx 8)
• Lean.IR.EmitLLVM.toLLVMType Lean.IR.IRType.uint16 = liftM (LLVM.intTypeInContext llvmctx 16)
• Lean.IR.EmitLLVM.toLLVMType Lean.IR.IRType.uint32 = liftM (LLVM.intTypeInContext llvmctx 32)
• Lean.IR.EmitLLVM.toLLVMType Lean.IR.IRType.uint64 = liftM (LLVM.intTypeInContext llvmctx 64)
• Lean.IR.EmitLLVM.toLLVMType Lean.IR.IRType.usize = liftM (Lean.IR.LLVM.size_tType llvmctx)
• Lean.IR.EmitLLVM.toLLVMType Lean.IR.IRType.object = do let __do_lift ← liftM (LLVM.i8Type llvmctx) liftM (LLVM.pointerType __do_lift)
• Lean.IR.EmitLLVM.toLLVMType Lean.IR.IRType.tobject = do let __do_lift ← liftM (LLVM.i8Type llvmctx) liftM (LLVM.pointerType __do_lift)
• Lean.IR.EmitLLVM.toLLVMType Lean.IR.IRType.irrelevant = do let __do_lift ← liftM (LLVM.i8Type llvmctx) liftM (LLVM.pointerType __do_lift)
• Lean.IR.EmitLLVM.toLLVMType (Lean.IR.IRType.struct leanTypeName types) = panicWithPosWithDecl "Lean.Compiler.IR.EmitLLVM" "Lean.IR.EmitLLVM.toLLVMType" 327 25 "not implemented yet"
• Lean.IR.EmitLLVM.toLLVMType (Lean.IR.IRType.union leanTypeName types) = panicWithPosWithDecl "Lean.Compiler.IR.EmitLLVM" "Lean.IR.EmitLLVM.toLLVMType" 328 25 "not implemented yet"

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

Equations

• Lean.IR.EmitLLVM.throwInvalidExportName n = throw (toString "invalid export name " ++ toString n.toString ++ toString "")

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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)

Equations

• Lean.IR.EmitLLVM.builderGetInsertionFn builder = do let builderBB ← liftM (LLVM.getInsertBlock builder) liftM (LLVM.getBasicBlockParent builderBB)

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

Equations

• Lean.IR.EmitLLVM.builderAppendBasicBlock builder name = do let fn ← Lean.IR.EmitLLVM.builderGetInsertionFn builder liftM (LLVM.appendBasicBlockInContext llvmctx fn name)

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.IR.EmitLLVM.buildLeanBoolTrue? builder b name = do let __do_lift ← Lean.IR.EmitLLVM.constInt8 0 liftM (LLVM.buildICmp builder LLVM.IntPredicate.NE b __do_lift name)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.IR.EmitLLVM.emitLhsSlot_ x = do let state ← get match state.var2val[x]? with | some v => pure v | none => throw (toString "unable to find variable " ++ toString x ++ toString "")

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

Equations

• Lean.IR.EmitLLVM.emitLhsVal builder x name = do let __discr ← Lean.IR.EmitLLVM.emitLhsSlot_ x match __discr with | (xty, xslot) => liftM (LLVM.buildLoad2 builder xty xslot name)

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

Equations

• Lean.IR.EmitLLVM.emitLhsSlotStore builder x v = do let __discr ← Lean.IR.EmitLLVM.emitLhsSlot_ x match __discr with | (fst, slot) => liftM (LLVM.buildStore builder v slot)

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.IR.EmitLLVM.emitArgSlot_ builder (Lean.IR.Arg.var x_2) = Lean.IR.EmitLLVM.emitLhsSlot_ x_2

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.IR.EmitLLVM.emitAllocCtor builder c = Lean.IR.EmitLLVM.callLeanAllocCtor builder c.cidx c.size (8 * c.usize + c.ssize) "lean_alloc_ctor_out"

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.IR.EmitLLVM.toHexDigit c = String.singleton c.digitChar

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

Equations

• One or more equations did not get rendered due to their size.

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)

Equations

• One or more equations did not get rendered due to their size.

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)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.IR.EmitLLVM.IRType.isIntegerType Lean.IR.IRType.uint8 = true
• Lean.IR.EmitLLVM.IRType.isIntegerType Lean.IR.IRType.uint16 = true
• Lean.IR.EmitLLVM.IRType.isIntegerType Lean.IR.IRType.uint32 = true
• Lean.IR.EmitLLVM.IRType.isIntegerType Lean.IR.IRType.uint64 = true
• Lean.IR.EmitLLVM.IRType.isIntegerType Lean.IR.IRType.usize = true
• Lean.IR.EmitLLVM.IRType.isIntegerType t = false

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)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.IR.EmitLLVM.emitVDecl builder z t (Lean.IR.Expr.ctor c ys) = Lean.IR.EmitLLVM.emitCtor builder z c ys
• Lean.IR.EmitLLVM.emitVDecl builder z t (Lean.IR.Expr.reset n x) = Lean.IR.EmitLLVM.emitReset builder z n x
• Lean.IR.EmitLLVM.emitVDecl builder z t (Lean.IR.Expr.reuse x c u ys) = Lean.IR.EmitLLVM.emitReuse builder z x c u ys
• Lean.IR.EmitLLVM.emitVDecl builder z t (Lean.IR.Expr.proj i x) = Lean.IR.EmitLLVM.emitProj builder z i x
• Lean.IR.EmitLLVM.emitVDecl builder z t (Lean.IR.Expr.uproj i x) = Lean.IR.EmitLLVM.emitUProj builder z i x
• Lean.IR.EmitLLVM.emitVDecl builder z t (Lean.IR.Expr.sproj n o x) = Lean.IR.EmitLLVM.emitSProj builder z t n o x
• Lean.IR.EmitLLVM.emitVDecl builder z t (Lean.IR.Expr.fap c ys) = Lean.IR.EmitLLVM.emitFullApp builder z c ys
• Lean.IR.EmitLLVM.emitVDecl builder z t (Lean.IR.Expr.pap c ys) = Lean.IR.EmitLLVM.emitPartialApp builder z c ys
• Lean.IR.EmitLLVM.emitVDecl builder z t (Lean.IR.Expr.ap x ys) = Lean.IR.EmitLLVM.emitApp builder z x ys
• Lean.IR.EmitLLVM.emitVDecl builder z t (Lean.IR.Expr.box t_1 x) = Lean.IR.EmitLLVM.emitBox builder z x t_1
• Lean.IR.EmitLLVM.emitVDecl builder z t (Lean.IR.Expr.unbox x) = Lean.IR.EmitLLVM.emitUnbox builder z t x
• Lean.IR.EmitLLVM.emitVDecl builder z t (Lean.IR.Expr.isShared x) = Lean.IR.EmitLLVM.emitIsShared builder z x
• Lean.IR.EmitLLVM.emitVDecl builder z t (Lean.IR.Expr.lit v_2) = do let __discr ← Lean.IR.EmitLLVM.emitLit builder z t v_2 let x : LLVM.Value llvmctx := __discr pure PUnit.unit

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

Equations

• One or more equations did not get rendered due to their size.

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)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.IR.EmitLLVM.emitTailCall builder f v = throw (toString "EmitTailCall expects function application, found '" ++ toString v ++ toString "'")

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.IR.EmitLLVM.emitFns mod builder = do let env ← Lean.IR.EmitLLVM.getEnv let decls : List Lean.IR.Decl := Lean.IR.getDecls env decls.reverse.forM (Lean.IR.EmitLLVM.emitDecl mod builder)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.IR.EmitLLVM.hasMainFn = do let env ← Lean.IR.EmitLLVM.getEnv let decls : List Lean.IR.Decl := Lean.IR.getDecls env pure (decls.any fun (d : Lean.IR.Decl) => d.name == `main)

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

Equations

• Lean.IR.EmitLLVM.emitMainFnIfNeeded mod builder = do let __do_lift ← Lean.IR.EmitLLVM.hasMainFn if __do_lift = true then Lean.IR.EmitLLVM.emitMainFn mod builder else pure PUnit.unit

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.IR.getLeanHBcPath : IO System.FilePath

Equations

• Lean.IR.getLeanHBcPath = do let __do_lift ← Lean.getBuildDir let __do_lift ← Lean.getLibDir __do_lift pure (__do_lift / { toString := "lean.h.bc" })

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

Equations

• Lean.IR.getModuleGlobals mod = do let __do_lift ← liftM (LLVM.getFirstGlobal mod) Lean.IR.getModuleGlobals.go __do_lift #[]

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

Equations

• Lean.IR.getModuleFunctions mod = do let __do_lift ← liftM (LLVM.getFirstFunction mod) Lean.IR.getModuleFunctions.go __do_lift #[]

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.

Equations

• One or more equations did not get rendered due to their size.