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.
Equations
- LLVM.CodegenFileType.AssemblyFile = { val := 0 }
Instances For
Equations
- LLVM.CodegenFileType.ObjectFile = { val := 1 }
Instances For
Equations
- LLVM.IntPredicate.EQ = { val := 32 }
Instances For
Equations
- LLVM.IntPredicate.NE = { val := LLVM.IntPredicate.EQ.val + 1 }
Instances For
Equations
- LLVM.IntPredicate.UGT = { val := LLVM.IntPredicate.NE.val + 1 }
Instances For
Equations
- LLVM.AttributeIndex.AttributeReturnIndex = { val := 0 }
Instances For
Equations
- LLVM.AttributeIndex.AttributeFunctionIndex = { val := 18446744073709551615 }
Instances For
instance
LLVM.instNonemptyBasicBlock
{Context✝ : Sort u_1}
{ctx : Context✝}
:
Nonempty (BasicBlock ctx)
@[extern lean_llvm_void_type_in_context]
@[extern lean_llvm_float_type_in_context]
@[extern lean_llvm_double_type_in_context]
@[extern lean_llvm_create_builder_in_context]
@[extern lean_llvm_append_basic_block_in_context]
opaque
LLVM.appendBasicBlockInContext
(ctx : Context)
(fn : Value ctx)
(name : String)
:
BaseIO (BasicBlock ctx)
@[extern lean_llvm_get_entry_basic_block]
@[extern lean_llvm_get_first_instruction]
@[extern lean_llvm_position_builder_at_end]
opaque
LLVM.positionBuilderAtEnd
{Context✝ : Sort u_1}
{ctx : Context✝}
(builder : Builder ctx)
(bb : BasicBlock ctx)
:
@[extern lean_llvm_build_cond_br]
opaque
LLVM.buildCondBr
{ctx : Context}
(builder : Builder ctx)
(if_ : Value ctx)
(thenbb elsebb : BasicBlock ctx)
:
@[extern lean_llvm_build_br]
@[extern lean_llvm_build_switch]
opaque
LLVM.buildSwitch
{ctx : Context}
(builder : Builder ctx)
(val : Value ctx)
(elseBB : BasicBlock ctx)
(numCasesHint : UInt64)
:
@[extern lean_llvm_build_icmp]
opaque
LLVM.buildICmp
{ctx : Context}
(builder : Builder ctx)
(predicate : IntPredicate)
(x y : Value ctx)
(name : String := "")
:
@[extern lean_llvm_add_case]
@[extern lean_llvm_get_insert_block]
opaque
LLVM.getInsertBlock
{Context✝ : Sort u_1}
{ctx : Context✝}
(builder : Builder ctx)
:
BaseIO (BasicBlock ctx)
@[extern lean_llvm_get_basic_block_parent]
@[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]
@[extern lean_llvm_get_default_target_triple]
@[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)
:
@[extern lean_llvm_dispose_target_machine]
@[extern lean_llvm_add_attribute_at_index]
opaque
LLVM.addAttributeAtIndex
{ctx : Context}
(fn : Value ctx)
(idx : AttributeIndex)
(attr : Attribute ctx)
:
Equations
- LLVM.Visibility.default = { val := 0 }
Instances For
Equations
- LLVM.Visibility.protected = { val := 2 }
Instances For
@[extern lean_llvm_set_visibility]
Equations
- LLVM.DLLStorageClass.default = { val := 0 }
Instances For
Equations
- LLVM.DLLStorageClass.import = { val := 1 }
Instances For
Equations
- LLVM.DLLStorageClass.export = { val := 2 }
Instances For
@[extern lean_llvm_set_dll_storage_class]
opaque
LLVM.setDLLStorageClass
{ctx : Context}
(value : Value ctx)
(dllStorageClass : DLLStorageClass)
:
Equations
- LLVM.Linkage.availableExternally = { val := 1 }
Instances For
Keep one copy of function when linking (inline)
Equations
- LLVM.Linkage.linkOnceAny = { val := 2 }
Instances For
Same, but only replaced by something equivalent
Equations
- LLVM.Linkage.linkOnceODR = { val := 3 }
Instances For
Keep one copy of function when linking (weak)
Equations
- LLVM.Linkage.weakAny = { val := 5 }
Instances For
Same, but only replaced by something equivalent
Equations
- LLVM.Linkage.weakODR = { val := 6 }
Instances For
Special purpose, only applies to global arrays
Equations
- LLVM.Linkage.appending = { val := 7 }
Instances For
Rename collisions when linking (static functions)
Equations
- LLVM.Linkage.internal = { val := 8 }
Instances For
Like LinkerPrivate, but is weak.
Equations
- LLVM.Linkage.linkerPrivateWeak = { val := 16 }
Instances For
Equations
- LLVM.i1Type ctx = LLVM.intTypeInContext ctx 1
Instances For
Equations
- LLVM.i8Type ctx = LLVM.intTypeInContext ctx 8
Instances For
Equations
- LLVM.i16Type ctx = LLVM.intTypeInContext ctx 16
Instances For
Equations
- LLVM.i32Type ctx = LLVM.intTypeInContext ctx 32
Instances For
Equations
- LLVM.i64Type ctx = LLVM.intTypeInContext ctx 64
Instances For
Equations
- LLVM.voidPtrType ctx = do let __do_lift ← LLVM.intTypeInContext ctx 8 LLVM.pointerType __do_lift
Instances For
Equations
- LLVM.i8PtrType ctx = LLVM.voidPtrType ctx
Instances For
Equations
- LLVM.constTrue ctx = do let __do_lift ← LLVM.i1Type ctx LLVM.constInt __do_lift 1
Instances For
Equations
- LLVM.constFalse ctx = do let __do_lift ← LLVM.i1Type ctx LLVM.constInt __do_lift 0
Instances For
Equations
- LLVM.constInt' ctx width value signExtend = do let __do_lift ← LLVM.intTypeInContext ctx width LLVM.constInt __do_lift value signExtend
Instances For
Equations
- LLVM.constInt1 ctx value signExtend = LLVM.constInt' ctx 1 value signExtend
Instances For
Equations
- LLVM.constInt8 ctx value signExtend = LLVM.constInt' ctx 8 value signExtend
Instances For
Equations
- LLVM.constInt32 ctx value signExtend = LLVM.constInt' ctx 32 value signExtend
Instances For
Equations
- LLVM.constInt64 ctx value signExtend = LLVM.constInt' ctx 64 value signExtend
Instances For
Equations
- LLVM.constIntSizeT ctx value signExtend = LLVM.constInt' ctx 64 value signExtend
Instances For
Equations
- LLVM.constIntUnsigned ctx value signExtend = LLVM.constInt' ctx 32 value signExtend