Documentation

Lean.Compiler.IR.LLVMBindings

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

Instances For
    Instances For
      Equations
      Instances For
        Instances For
          structure LLVM.BasicBlock {Context : Sort u_1} (ctx : Context) :
          Instances For
            instance LLVM.instNonemptyBasicBlock {Context✝ : Sort u_1} {ctx : Context✝} :
            structure LLVM.Builder {Context : Sort u_1} (ctx : Context) :
            Instances For
              instance LLVM.instNonemptyBuilder {Context✝ : Sort u_1} {ctx : Context✝} :
              structure LLVM.Context :
              Instances For
                structure LLVM.LLVMType (ctx : Context) :
                Instances For
                  structure LLVM.MemoryBuffer (ctx : Context) :
                  Instances For
                    structure LLVM.Module (ctx : Context) :
                    Instances For
                      structure LLVM.Target (ctx : Context) :
                      Instances For
                        structure LLVM.TargetMachine (ctx : Context) :
                        Instances For
                          structure LLVM.Value (ctx : Context) :
                          Instances For
                            def LLVM.Value.isNull {ctx : Context} (v : Value ctx) :

                            Check if the value is a null pointer. -

                            Equations
                            Instances For
                              @[extern lean_llvm_get_value_name2]
                              opaque LLVM.Value.getName {ctx : Context} (value : Value ctx) :
                              structure LLVM.Attribute (ctx : Context) :
                              Instances For
                                @[extern lean_llvm_initialize_target_info]
                                @[extern lean_llvm_create_context]
                                @[extern lean_llvm_create_module]
                                opaque LLVM.createModule (ctx : Context) (name : String) :
                                @[extern lean_llvm_module_to_string]
                                opaque LLVM.moduleToString {ctx : Context} (m : Module ctx) :
                                @[extern lean_llvm_write_bitcode_to_file]
                                opaque LLVM.writeBitcodeToFile {ctx : Context} (m : Module ctx) (path : String) :
                                @[extern lean_llvm_add_function]
                                opaque LLVM.addFunction {ctx : Context} (m : Module ctx) (name : String) (type : LLVMType ctx) :
                                @[extern lean_llvm_get_first_function]
                                opaque LLVM.getFirstFunction {ctx : Context} (m : Module ctx) :
                                @[extern lean_llvm_get_next_function]
                                opaque LLVM.getNextFunction {ctx : Context} (glbl : Value ctx) :
                                @[extern lean_llvm_get_named_function]
                                opaque LLVM.getNamedFunction {ctx : Context} (m : Module ctx) (name : String) :
                                @[extern lean_llvm_add_global]
                                opaque LLVM.addGlobal {ctx : Context} (m : Module ctx) (name : String) (type : LLVMType ctx) :
                                @[extern lean_llvm_get_named_global]
                                opaque LLVM.getNamedGlobal {ctx : Context} (m : Module ctx) (name : String) :
                                @[extern lean_llvm_get_first_global]
                                opaque LLVM.getFirstGlobal {ctx : Context} (m : Module ctx) :
                                @[extern lean_llvm_get_next_global]
                                opaque LLVM.getNextGlobal {ctx : Context} (glbl : Value ctx) :
                                @[extern lean_llvm_build_global_string]
                                opaque LLVM.buildGlobalString {ctx : Context} (builder : Builder ctx) (value : String) (name : String := "") :
                                @[extern llvm_is_declaration]
                                opaque LLVM.isDeclaration {ctx : Context} (global : Value ctx) :
                                @[extern lean_llvm_set_initializer]
                                opaque LLVM.setInitializer {ctx : Context} (glbl val : Value ctx) :
                                @[extern lean_llvm_function_type]
                                opaque LLVM.functionType {ctx : Context} (retty : LLVMType ctx) (args : Array (LLVMType ctx)) (isVarArg : Bool := false) :
                                @[extern lean_llvm_void_type_in_context]
                                opaque LLVM.voidType (ctx : Context) :
                                @[extern lean_llvm_int_type_in_context]
                                opaque LLVM.intTypeInContext (ctx : Context) (width : UInt64) :
                                @[extern lean_llvm_opaque_pointer_type_in_context]
                                opaque LLVM.opaquePointerTypeInContext (ctx : Context) (addrspace : UInt64 := 0) :
                                @[extern lean_llvm_float_type_in_context]
                                @[extern lean_llvm_double_type_in_context]
                                @[extern lean_llvm_pointer_type]
                                opaque LLVM.pointerType {ctx : Context} (elemty : LLVMType ctx) :
                                @[extern lean_llvm_array_type]
                                opaque LLVM.arrayType {ctx : Context} (elemty : LLVMType ctx) (nelem : UInt64) :
                                @[extern lean_llvm_const_array]
                                opaque LLVM.constArray {ctx : Context} (elemty : LLVMType ctx) (vals : Array (Value ctx)) :
                                @[extern lean_llvm_const_string]
                                opaque LLVM.constString (ctx : Context) (str : String) :
                                @[extern lean_llvm_const_pointer_null]
                                opaque LLVM.constPointerNull {ctx : Context} (elemty : LLVMType ctx) :
                                @[extern lean_llvm_get_undef]
                                opaque LLVM.getUndef {ctx : Context} (elemty : LLVMType ctx) :
                                @[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) :
                                @[extern lean_llvm_count_basic_blocks]
                                opaque LLVM.countBasicBlocks {ctx : Context} (fn : Value ctx) :
                                @[extern lean_llvm_get_entry_basic_block]
                                opaque LLVM.getEntryBasicBlock {ctx : Context} (fn : Value ctx) :
                                @[extern lean_llvm_get_first_instruction]
                                opaque LLVM.getFirstInstruction {ctx : Context} (bb : BasicBlock ctx) :
                                @[extern lean_llvm_position_builder_before]
                                opaque LLVM.positionBuilderBefore {ctx : Context} (builder : Builder ctx) (instr : Value ctx) :
                                @[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_call2]
                                opaque LLVM.buildCall2 {ctx : Context} (builder : Builder ctx) (ty : LLVMType ctx) (fn : Value ctx) (args : Array (Value ctx)) (name : String := "") :
                                @[extern lean_llvm_set_tail_call]
                                opaque LLVM.setTailCall {ctx : Context} (fn : Value ctx) (istail : Bool) :
                                @[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]
                                opaque LLVM.buildBr {ctx : Context} (builder : Builder ctx) (bb : BasicBlock ctx) :
                                @[extern lean_llvm_build_alloca]
                                opaque LLVM.buildAlloca {ctx : Context} (builder : Builder ctx) (ty : LLVMType ctx) (name : String := "") :
                                @[extern lean_llvm_build_load2]
                                opaque LLVM.buildLoad2 {ctx : Context} (builder : Builder ctx) (ty : LLVMType ctx) (val : Value ctx) (name : String := "") :
                                @[extern lean_llvm_build_store]
                                opaque LLVM.buildStore {ctx : Context} (builder : Builder ctx) (val store_loc_ptr : Value ctx) :
                                @[extern lean_llvm_build_ret]
                                opaque LLVM.buildRet {ctx : Context} (builder : Builder ctx) (val : Value ctx) :
                                @[extern lean_llvm_build_unreachable]
                                opaque LLVM.buildUnreachable {ctx : Context} (builder : Builder 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 := "") :
                                @[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 := "") :
                                @[extern lean_llvm_build_sext]
                                opaque LLVM.buildSext {ctx : Context} (builder : Builder ctx) (val : Value ctx) (destTy : LLVMType ctx) (name : String := "") :
                                @[extern lean_llvm_build_zext]
                                opaque LLVM.buildZext {ctx : Context} (builder : Builder ctx) (val : Value ctx) (destTy : LLVMType ctx) (name : String := "") :
                                @[extern lean_llvm_build_sext_or_trunc]
                                opaque LLVM.buildSextOrTrunc {ctx : Context} (builder : Builder ctx) (val : Value ctx) (destTy : LLVMType ctx) (name : String := "") :
                                @[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_ptr_to_int]
                                opaque LLVM.buildPtrToInt {ctx : Context} (builder : Builder ctx) (ptr : Value ctx) (destTy : LLVMType ctx) (name : String := "") :
                                @[extern lean_llvm_build_mul]
                                opaque LLVM.buildMul {ctx : Context} (builder : Builder ctx) (x y : Value ctx) (name : String := "") :
                                @[extern lean_llvm_build_add]
                                opaque LLVM.buildAdd {ctx : Context} (builder : Builder ctx) (x y : Value ctx) (name : String := "") :
                                @[extern lean_llvm_build_sub]
                                opaque LLVM.buildSub {ctx : Context} (builder : Builder ctx) (x y : Value ctx) (name : String := "") :
                                @[extern lean_llvm_build_not]
                                opaque LLVM.buildNot {ctx : Context} (builder : Builder ctx) (x : Value ctx) (name : String := "") :
                                @[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]
                                opaque LLVM.addCase {ctx : Context} (switch onVal : Value ctx) (destBB : BasicBlock ctx) :
                                @[extern lean_llvm_get_insert_block]
                                opaque LLVM.getInsertBlock {Context✝ : Sort u_1} {ctx : Context✝} (builder : Builder ctx) :
                                @[extern lean_llvm_clear_insertion_position]
                                opaque LLVM.clearInsertionPosition {Context✝ : Sort u_1} {ctx : Context✝} (builder : Builder ctx) :
                                @[extern lean_llvm_get_basic_block_parent]
                                opaque LLVM.getBasicBlockParent {ctx : Context} (bb : BasicBlock ctx) :
                                @[extern lean_llvm_type_of]
                                opaque LLVM.typeOf {ctx : Context} (val : Value ctx) :
                                @[extern lean_llvm_const_int]
                                opaque LLVM.constInt {ctx : Context} (intty : LLVMType ctx) (value : UInt64) (signExtend : Bool := false) :
                                @[extern lean_llvm_print_module_to_string]
                                @[extern lean_llvm_print_module_to_file]
                                opaque LLVM.printModuletoFile {ctx : Context} (mod : Module ctx) (file : String) :
                                @[extern llvm_count_params]
                                opaque LLVM.countParams {ctx : Context} (fn : Value ctx) :
                                @[extern llvm_get_param]
                                opaque LLVM.getParam {ctx : Context} (fn : Value ctx) (ix : UInt64) :
                                @[extern lean_llvm_create_memory_buffer_with_contents_of_file]
                                @[extern lean_llvm_parse_bitcode]
                                opaque LLVM.parseBitcode (ctx : Context) (membuf : MemoryBuffer ctx) :
                                @[extern lean_llvm_link_modules]
                                opaque LLVM.linkModules {ctx : Context} (dest src : Module ctx) :
                                @[extern lean_llvm_get_default_target_triple]
                                @[extern lean_llvm_get_target_from_triple]
                                opaque LLVM.getTargetFromTriple {ctx : Context} (triple : String) :
                                @[extern lean_llvm_create_target_machine]
                                opaque LLVM.createTargetMachine {ctx : Context} (target : Target ctx) (tripleStr cpu features : String) :
                                @[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_dispose_module]
                                opaque LLVM.disposeModule {ctx : Context} (m : Module ctx) :
                                @[extern lean_llvm_verify_module]
                                opaque LLVM.verifyModule {ctx : Context} (m : Module ctx) :
                                @[extern lean_llvm_create_string_attribute]
                                opaque LLVM.createStringAttribute {ctx : Context} (key value : String) :
                                @[extern lean_llvm_add_attribute_at_index]
                                opaque LLVM.addAttributeAtIndex {ctx : Context} (fn : Value ctx) (idx : AttributeIndex) (attr : Attribute ctx) :
                                Instances For
                                  @[extern lean_llvm_set_visibility]
                                  opaque LLVM.setVisibility {ctx : Context} (value : Value ctx) (visibility : Visibility) :
                                  Instances For
                                    @[extern lean_llvm_set_dll_storage_class]
                                    opaque LLVM.setDLLStorageClass {ctx : Context} (value : Value ctx) (dllStorageClass : DLLStorageClass) :
                                    structure LLVM.Linkage :
                                    Instances For

                                      Externally visible function

                                      Equations
                                      Instances For

                                        Keep one copy of function when linking (inline)

                                        Equations
                                        Instances For

                                          Same, but only replaced by something equivalent

                                          Equations
                                          Instances For

                                            Keep one copy of function when linking (weak)

                                            Equations
                                            Instances For

                                              Same, but only replaced by something equivalent

                                              Equations
                                              Instances For

                                                Special purpose, only applies to global arrays

                                                Equations
                                                Instances For

                                                  Rename collisions when linking (static functions)

                                                  Equations
                                                  Instances For

                                                    Like Internal, but omit from symbol table

                                                    Equations
                                                    Instances For

                                                      Obsolete

                                                      Equations
                                                      Instances For

                                                        Obsolete

                                                        Equations
                                                        Instances For

                                                          ExternalWeak linkage description

                                                          Equations
                                                          Instances For

                                                            Obsolete

                                                            Equations
                                                            Instances For

                                                              Tentative definitions

                                                              Equations
                                                              Instances For

                                                                Like Private, but linker removes.

                                                                Equations
                                                                Instances For

                                                                  Like LinkerPrivate, but is weak.

                                                                  Equations
                                                                  Instances For
                                                                    @[extern lean_llvm_set_linkage]
                                                                    opaque LLVM.setLinkage {ctx : Context} (value : Value ctx) (linkage : Linkage) :
                                                                    def LLVM.i1Type (ctx : Context) :
                                                                    Equations
                                                                    Instances For
                                                                      def LLVM.i8Type (ctx : Context) :
                                                                      Equations
                                                                      Instances For
                                                                        def LLVM.i16Type (ctx : Context) :
                                                                        Equations
                                                                        Instances For
                                                                          def LLVM.i32Type (ctx : Context) :
                                                                          Equations
                                                                          Instances For
                                                                            def LLVM.i64Type (ctx : Context) :
                                                                            Equations
                                                                            Instances For
                                                                              Equations
                                                                              Instances For
                                                                                Equations
                                                                                Instances For
                                                                                  def LLVM.constTrue (ctx : Context) :
                                                                                  Equations
                                                                                  Instances For
                                                                                    def LLVM.constFalse (ctx : Context) :
                                                                                    Equations
                                                                                    Instances For
                                                                                      def LLVM.constInt' (ctx : Context) (width value : UInt64) (signExtend : Bool := false) :
                                                                                      Equations
                                                                                      Instances For
                                                                                        def LLVM.constInt1 (ctx : Context) (value : UInt64) (signExtend : Bool := false) :
                                                                                        Equations
                                                                                        Instances For
                                                                                          def LLVM.constInt8 (ctx : Context) (value : UInt64) (signExtend : Bool := false) :
                                                                                          Equations
                                                                                          Instances For
                                                                                            def LLVM.constInt32 (ctx : Context) (value : UInt64) (signExtend : Bool := false) :
                                                                                            Equations
                                                                                            Instances For
                                                                                              def LLVM.constInt64 (ctx : Context) (value : UInt64) (signExtend : Bool := false) :
                                                                                              Equations
                                                                                              Instances For
                                                                                                def LLVM.constIntSizeT (ctx : Context) (value : UInt64) (signExtend : Bool := false) :
                                                                                                Equations
                                                                                                Instances For
                                                                                                  def LLVM.constIntUnsigned (ctx : Context) (value : UInt64) (signExtend : Bool := false) :
                                                                                                  Equations
                                                                                                  Instances For