This file defines bindings for LLVM. The main mechanisms are to:

• Mirror the values of C enumerations.
• Create opaque values for LLVM's pointer based API
• Write bindings that are IO based, which mutate the underlying in-memory data structures to build IR.

structure LLVM.CodegenFileType : Type

• val : UInt64

def LLVM.CodegenFileType.AssemblyFile : CodegenFileType

def LLVM.CodegenFileType.ObjectFile : CodegenFileType

structure LLVM.IntPredicate : Type

• val : UInt64

def LLVM.IntPredicate.EQ : IntPredicate

def LLVM.IntPredicate.NE : IntPredicate

def LLVM.IntPredicate.UGT : IntPredicate

structure LLVM.AttributeIndex : Type

• val : UInt64

def LLVM.AttributeIndex.AttributeReturnIndex : AttributeIndex

def LLVM.AttributeIndex.AttributeFunctionIndex : AttributeIndex

structure LLVM.BasicBlock {Context : Sort u_1} (ctx : Context) : Type

• ptr : USize

instance LLVM.instNonemptyBasicBlock {Context✝ : Sort u_1} {ctx : Context✝} : Nonempty (BasicBlock ctx)

structure LLVM.Builder {Context : Sort u_1} (ctx : Context) : Type

• ptr : USize

instance LLVM.instNonemptyBuilder {Context✝ : Sort u_1} {ctx : Context✝} : Nonempty (Builder ctx)

structure LLVM.Context : Type

• ptr : USize

instance LLVM.instNonemptyContext : Nonempty Context

structure LLVM.LLVMType (ctx : Context) : Type

• ptr : USize

instance LLVM.instNonemptyLLVMType {ctx : Context} : Nonempty (LLVMType ctx)

structure LLVM.MemoryBuffer (ctx : Context) : Type

• ptr : USize

instance LLVM.instNonemptyMemoryBuffer {ctx : Context} : Nonempty (MemoryBuffer ctx)

structure LLVM.Module (ctx : Context) : Type

• ptr : USize

instance LLVM.instNonemptyModule {ctx : Context} : Nonempty (Module ctx)

structure LLVM.Target (ctx : Context) : Type

• ptr : USize

instance LLVM.instNonemptyTarget {ctx : Context} : Nonempty (Target ctx)

structure LLVM.TargetMachine (ctx : Context) : Type

• ptr : USize

instance LLVM.instNonemptyTargetMachine {ctx : Context} : Nonempty (TargetMachine ctx)

structure LLVM.Value (ctx : Context) : Type

• ptr : USize

instance LLVM.instNonemptyValue {ctx : Context} : Nonempty (Value ctx)

def LLVM.Value.isNull {ctx : Context} (v : Value ctx) : Bool

Check if the value is a null pointer. -

@[extern lean_llvm_get_value_name2]

opaque LLVM.Value.getName {ctx : Context} (value : Value ctx) : BaseIO String

structure LLVM.Attribute (ctx : Context) : Type

• ptr : USize

instance LLVM.instNonemptyAttribute {ctx : Context} : Nonempty (Attribute ctx)

@[extern lean_llvm_initialize_target_info]

opaque LLVM.llvmInitializeTargetInfo : BaseIO Unit

@[extern lean_llvm_create_context]

opaque LLVM.createContext : BaseIO Context

@[extern lean_llvm_create_module]

opaque LLVM.createModule (ctx : Context) (name : String) : BaseIO (Module ctx)

@[extern lean_llvm_module_to_string]

opaque LLVM.moduleToString {ctx : Context} (m : Module ctx) : BaseIO String

@[extern lean_llvm_write_bitcode_to_file]

opaque LLVM.writeBitcodeToFile {ctx : Context} (m : Module ctx) (path : String) : BaseIO Unit

@[extern lean_llvm_add_function]

opaque LLVM.addFunction {ctx : Context} (m : Module ctx) (name : String) (type : LLVMType ctx) : BaseIO (Value ctx)

@[extern lean_llvm_get_first_function]

opaque LLVM.getFirstFunction {ctx : Context} (m : Module ctx) : BaseIO (Value ctx)

@[extern lean_llvm_get_next_function]

opaque LLVM.getNextFunction {ctx : Context} (glbl : Value ctx) : BaseIO (Value ctx)

@[extern lean_llvm_get_named_function]

opaque LLVM.getNamedFunction {ctx : Context} (m : Module ctx) (name : String) : BaseIO (Option (Value ctx))

@[extern lean_llvm_add_global]

opaque LLVM.addGlobal {ctx : Context} (m : Module ctx) (name : String) (type : LLVMType ctx) : BaseIO (Value ctx)

@[extern lean_llvm_get_named_global]

opaque LLVM.getNamedGlobal {ctx : Context} (m : Module ctx) (name : String) : BaseIO (Option (Value ctx))

@[extern lean_llvm_get_first_global]

opaque LLVM.getFirstGlobal {ctx : Context} (m : Module ctx) : BaseIO (Value ctx)

@[extern lean_llvm_get_next_global]

opaque LLVM.getNextGlobal {ctx : Context} (glbl : Value ctx) : BaseIO (Value ctx)

@[extern lean_llvm_build_global_string]

opaque LLVM.buildGlobalString {ctx : Context} (builder : Builder ctx) (value : String) (name : String := "") : BaseIO (Value ctx)

@[extern llvm_is_declaration]

opaque LLVM.isDeclaration {ctx : Context} (global : Value ctx) : BaseIO Bool

@[extern lean_llvm_set_initializer]

opaque LLVM.setInitializer {ctx : Context} (glbl val : Value ctx) : BaseIO Unit

@[extern lean_llvm_function_type]

opaque LLVM.functionType {ctx : Context} (retty : LLVMType ctx) (args : Array (LLVMType ctx)) (isVarArg : Bool := false) : BaseIO (LLVMType ctx)

@[extern lean_llvm_void_type_in_context]

opaque LLVM.voidType (ctx : Context) : BaseIO (LLVMType ctx)

@[extern lean_llvm_int_type_in_context]

opaque LLVM.intTypeInContext (ctx : Context) (width : UInt64) : BaseIO (LLVMType ctx)

@[extern lean_llvm_opaque_pointer_type_in_context]

opaque LLVM.opaquePointerTypeInContext (ctx : Context) (addrspace : UInt64 := 0) : BaseIO (LLVMType ctx)

@[extern lean_llvm_float_type_in_context]

opaque LLVM.floatTypeInContext (ctx : Context) : BaseIO (LLVMType ctx)

@[extern lean_llvm_double_type_in_context]

opaque LLVM.doubleTypeInContext (ctx : Context) : BaseIO (LLVMType ctx)

@[extern lean_llvm_pointer_type]

opaque LLVM.pointerType {ctx : Context} (elemty : LLVMType ctx) : BaseIO (LLVMType ctx)

@[extern lean_llvm_array_type]

opaque LLVM.arrayType {ctx : Context} (elemty : LLVMType ctx) (nelem : UInt64) : BaseIO (LLVMType ctx)

@[extern lean_llvm_const_array]

opaque LLVM.constArray {ctx : Context} (elemty : LLVMType ctx) (vals : Array (Value ctx)) : BaseIO (LLVMType ctx)

@[extern lean_llvm_const_string]

opaque LLVM.constString (ctx : Context) (str : String) : BaseIO (Value ctx)

@[extern lean_llvm_const_pointer_null]

opaque LLVM.constPointerNull {ctx : Context} (elemty : LLVMType ctx) : BaseIO (Value ctx)

@[extern lean_llvm_get_undef]

opaque LLVM.getUndef {ctx : Context} (elemty : LLVMType ctx) : BaseIO (Value ctx)

@[extern lean_llvm_create_builder_in_context]

opaque LLVM.createBuilderInContext (ctx : Context) : BaseIO (Builder ctx)

@[extern lean_llvm_append_basic_block_in_context]

opaque LLVM.appendBasicBlockInContext (ctx : Context) (fn : Value ctx) (name : String) : BaseIO (BasicBlock ctx)

@[extern lean_llvm_count_basic_blocks]

opaque LLVM.countBasicBlocks {ctx : Context} (fn : Value ctx) : BaseIO UInt64

@[extern lean_llvm_get_entry_basic_block]

opaque LLVM.getEntryBasicBlock {ctx : Context} (fn : Value ctx) : BaseIO (BasicBlock ctx)

@[extern lean_llvm_get_first_instruction]

opaque LLVM.getFirstInstruction {ctx : Context} (bb : BasicBlock ctx) : BaseIO (Option (Value ctx))

@[extern lean_llvm_position_builder_before]

opaque LLVM.positionBuilderBefore {ctx : Context} (builder : Builder ctx) (instr : Value ctx) : BaseIO Unit

@[extern lean_llvm_position_builder_at_end]

opaque LLVM.positionBuilderAtEnd {Context✝ : Sort u_1} {ctx : Context✝} (builder : Builder ctx) (bb : BasicBlock ctx) : BaseIO Unit

@[extern lean_llvm_build_call2]

opaque LLVM.buildCall2 {ctx : Context} (builder : Builder ctx) (ty : LLVMType ctx) (fn : Value ctx) (args : Array (Value ctx)) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_set_tail_call]

opaque LLVM.setTailCall {ctx : Context} (fn : Value ctx) (istail : Bool) : BaseIO Unit

@[extern lean_llvm_build_cond_br]

opaque LLVM.buildCondBr {ctx : Context} (builder : Builder ctx) (if_ : Value ctx) (thenbb elsebb : BasicBlock ctx) : BaseIO (Value ctx)

@[extern lean_llvm_build_br]

opaque LLVM.buildBr {ctx : Context} (builder : Builder ctx) (bb : BasicBlock ctx) : BaseIO (Value ctx)

@[extern lean_llvm_build_alloca]

opaque LLVM.buildAlloca {ctx : Context} (builder : Builder ctx) (ty : LLVMType ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_load2]

opaque LLVM.buildLoad2 {ctx : Context} (builder : Builder ctx) (ty : LLVMType ctx) (val : Value ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_store]

opaque LLVM.buildStore {ctx : Context} (builder : Builder ctx) (val store_loc_ptr : Value ctx) : BaseIO Unit

@[extern lean_llvm_build_ret]

opaque LLVM.buildRet {ctx : Context} (builder : Builder ctx) (val : Value ctx) : BaseIO (Value ctx)

@[extern lean_llvm_build_unreachable]

opaque LLVM.buildUnreachable {ctx : Context} (builder : Builder ctx) : BaseIO (Value ctx)

@[extern lean_llvm_build_gep2]

opaque LLVM.buildGEP2 {ctx : Context} (builder : Builder ctx) (ty : LLVMType ctx) (base : Value ctx) (ixs : Array (Value ctx)) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_inbounds_gep2]

opaque LLVM.buildInBoundsGEP2 {ctx : Context} (builder : Builder ctx) (ty : LLVMType ctx) (base : Value ctx) (ixs : Array (Value ctx)) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_sext]

opaque LLVM.buildSext {ctx : Context} (builder : Builder ctx) (val : Value ctx) (destTy : LLVMType ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_zext]

opaque LLVM.buildZext {ctx : Context} (builder : Builder ctx) (val : Value ctx) (destTy : LLVMType ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_sext_or_trunc]

opaque LLVM.buildSextOrTrunc {ctx : Context} (builder : Builder ctx) (val : Value ctx) (destTy : LLVMType ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_switch]

opaque LLVM.buildSwitch {ctx : Context} (builder : Builder ctx) (val : Value ctx) (elseBB : BasicBlock ctx) (numCasesHint : UInt64) : BaseIO (Value ctx)

@[extern lean_llvm_build_ptr_to_int]

opaque LLVM.buildPtrToInt {ctx : Context} (builder : Builder ctx) (ptr : Value ctx) (destTy : LLVMType ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_mul]

opaque LLVM.buildMul {ctx : Context} (builder : Builder ctx) (x y : Value ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_add]

opaque LLVM.buildAdd {ctx : Context} (builder : Builder ctx) (x y : Value ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_sub]

opaque LLVM.buildSub {ctx : Context} (builder : Builder ctx) (x y : Value ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_not]

opaque LLVM.buildNot {ctx : Context} (builder : Builder ctx) (x : Value ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_build_icmp]

opaque LLVM.buildICmp {ctx : Context} (builder : Builder ctx) (predicate : IntPredicate) (x y : Value ctx) (name : String := "") : BaseIO (Value ctx)

@[extern lean_llvm_add_case]

opaque LLVM.addCase {ctx : Context} (switch onVal : Value ctx) (destBB : BasicBlock ctx) : BaseIO Unit

@[extern lean_llvm_get_insert_block]

opaque LLVM.getInsertBlock {Context✝ : Sort u_1} {ctx : Context✝} (builder : Builder ctx) : BaseIO (BasicBlock ctx)

@[extern lean_llvm_clear_insertion_position]

opaque LLVM.clearInsertionPosition {Context✝ : Sort u_1} {ctx : Context✝} (builder : Builder ctx) : BaseIO Unit

@[extern lean_llvm_get_basic_block_parent]

opaque LLVM.getBasicBlockParent {ctx : Context} (bb : BasicBlock ctx) : BaseIO (Value ctx)

@[extern lean_llvm_type_of]

opaque LLVM.typeOf {ctx : Context} (val : Value ctx) : BaseIO (LLVMType ctx)

@[extern lean_llvm_const_int]

opaque LLVM.constInt {ctx : Context} (intty : LLVMType ctx) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx)

@[extern lean_llvm_print_module_to_string]

opaque LLVM.printModuletoString {ctx : Context} (mod : Module ctx) : BaseIO String

@[extern lean_llvm_print_module_to_file]

opaque LLVM.printModuletoFile {ctx : Context} (mod : Module ctx) (file : String) : BaseIO Unit

@[extern llvm_count_params]

opaque LLVM.countParams {ctx : Context} (fn : Value ctx) : BaseIO UInt64

@[extern llvm_get_param]

opaque LLVM.getParam {ctx : Context} (fn : Value ctx) (ix : UInt64) : BaseIO (Value ctx)

@[extern lean_llvm_create_memory_buffer_with_contents_of_file]

opaque LLVM.createMemoryBufferWithContentsOfFile {ctx : Context} (path : String) : BaseIO (MemoryBuffer ctx)

@[extern lean_llvm_parse_bitcode]

opaque LLVM.parseBitcode (ctx : Context) (membuf : MemoryBuffer ctx) : BaseIO (Module ctx)

@[extern lean_llvm_link_modules]

opaque LLVM.linkModules {ctx : Context} (dest src : Module ctx) : BaseIO Unit

@[extern lean_llvm_get_default_target_triple]

opaque LLVM.getDefaultTargetTriple : BaseIO String

@[extern lean_llvm_get_target_from_triple]

opaque LLVM.getTargetFromTriple {ctx : Context} (triple : String) : BaseIO (Target ctx)

@[extern lean_llvm_create_target_machine]

opaque LLVM.createTargetMachine {ctx : Context} (target : Target ctx) (tripleStr cpu features : String) : BaseIO (TargetMachine ctx)

@[extern lean_llvm_target_machine_emit_to_file]

opaque LLVM.targetMachineEmitToFile {ctx : Context} (targetMachine : TargetMachine ctx) (module : Module ctx) (filepath : String) (codegenType : CodegenFileType) : BaseIO Unit

@[extern lean_llvm_dispose_target_machine]

opaque LLVM.disposeTargetMachine {ctx : Context} (tm : TargetMachine ctx) : BaseIO Unit

@[extern lean_llvm_dispose_module]

opaque LLVM.disposeModule {ctx : Context} (m : Module ctx) : BaseIO Unit

@[extern lean_llvm_verify_module]

opaque LLVM.verifyModule {ctx : Context} (m : Module ctx) : BaseIO (Option String)

@[extern lean_llvm_create_string_attribute]

opaque LLVM.createStringAttribute {ctx : Context} (key value : String) : BaseIO (Attribute ctx)

@[extern lean_llvm_add_attribute_at_index]

opaque LLVM.addAttributeAtIndex {ctx : Context} (fn : Value ctx) (idx : AttributeIndex) (attr : Attribute ctx) : BaseIO Unit

structure LLVM.Visibility : Type

• val : UInt64

def LLVM.Visibility.default : Visibility

def LLVM.Visibility.hidden : Visibility

def LLVM.Visibility.protected : Visibility

@[extern lean_llvm_set_visibility]

opaque LLVM.setVisibility {ctx : Context} (value : Value ctx) (visibility : Visibility) : BaseIO Unit

structure LLVM.DLLStorageClass : Type

• val : UInt64

def LLVM.DLLStorageClass.default : DLLStorageClass

def LLVM.DLLStorageClass.import : DLLStorageClass

def LLVM.DLLStorageClass.export : DLLStorageClass

@[extern lean_llvm_set_dll_storage_class]

opaque LLVM.setDLLStorageClass {ctx : Context} (value : Value ctx) (dllStorageClass : DLLStorageClass) : BaseIO Unit

structure LLVM.Linkage : Type

• val : UInt64

def LLVM.Linkage.external : Linkage

Externally visible function

def LLVM.Linkage.availableExternally : Linkage

def LLVM.Linkage.linkOnceAny : Linkage

Keep one copy of function when linking (inline)

def LLVM.Linkage.linkOnceODR : Linkage

Same, but only replaced by something equivalent

def LLVM.Linkage.linkOnceODRAutoHide : Linkage

Obsolete

def LLVM.Linkage.weakAny : Linkage

Keep one copy of function when linking (weak)

def LLVM.Linkage.weakODR : Linkage

Same, but only replaced by something equivalent

def LLVM.Linkage.appending : Linkage

Special purpose, only applies to global arrays

def LLVM.Linkage.internal : Linkage

Rename collisions when linking (static functions)

def LLVM.Linkage.private : Linkage

Like Internal, but omit from symbol table

def LLVM.Linkage.dllImport : Linkage

Obsolete

def LLVM.Linkage.dllExport : Linkage

Obsolete

def LLVM.Linkage.externalWeak : Linkage

ExternalWeak linkage description

def LLVM.Linkage.ghost : Linkage

Obsolete

def LLVM.Linkage.common : Linkage

Tentative definitions

def LLVM.Linkage.linkerPrivate : Linkage

Like Private, but linker removes.

def LLVM.Linkage.linkerPrivateWeak : Linkage

Like LinkerPrivate, but is weak.

@[extern lean_llvm_set_linkage]

opaque LLVM.setLinkage {ctx : Context} (value : Value ctx) (linkage : Linkage) : BaseIO Unit

def LLVM.i1Type (ctx : Context) : BaseIO (LLVMType ctx)

def LLVM.i8Type (ctx : Context) : BaseIO (LLVMType ctx)

def LLVM.i16Type (ctx : Context) : BaseIO (LLVMType ctx)

def LLVM.i32Type (ctx : Context) : BaseIO (LLVMType ctx)

def LLVM.i64Type (ctx : Context) : BaseIO (LLVMType ctx)

def LLVM.voidPtrType (ctx : Context) : BaseIO (LLVMType ctx)

def LLVM.i8PtrType (ctx : Context) : BaseIO (LLVMType ctx)

def LLVM.constTrue (ctx : Context) : BaseIO (Value ctx)

def LLVM.constFalse (ctx : Context) : BaseIO (Value ctx)

def LLVM.constInt' (ctx : Context) (width value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx)

def LLVM.constInt1 (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx)

def LLVM.constInt8 (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx)

def LLVM.constInt32 (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx)

def LLVM.constInt64 (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx)

def LLVM.constIntSizeT (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx)

def LLVM.constIntUnsigned (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx)