Source

Agda-LLVM / LLVM / AST.agda

Full commit
open import Data.Maybe
{-# IMPORT LLVM.General.AST #-}
{-# IMPORT LLVM.General.AST.DataLayout #-}
{-# IMPORT LLVM.General.AST.Operand #-}
{-# IMPORT LLVM.General.AST.Name #-}
{-# IMPORT LLVM.General.AST.AddrSpace #-}
{-# IMPORT LLVM.General.AST.Linkage #-}
{-# IMPORT LLVM.General.AST.Visibility #-}
{-# IMPORT LLVM.General.AST.Constant #-}
{-# IMPORT LLVM.General.AST.CallingConvention #-}
{-# IMPORT LLVM.General.AST.Attribute #-}
{-# IMPORT Data.Word #-}
open import Data.String
open import Data.Colist
open import Data.Bool

data _×_ (A B : Set) : Set where
  _,_ : (proj₁ : A) (proj₂ : B)  A × B

{-# COMPILED_DATA _×_ (,) (,) #-}  

postulate
  DataLayout   Linkage Visibility Constant MetadataNodeID  Operand 
    CallingConvention ParameterAttribute Parameter FunctionAttribute BasicBlock
    Word Word32 Word64 AddrSpace FloatingFormat : Set

data Name : Set where
  name : Costring  Name
  unName : Word  Name

{-# COMPILED_TYPE Word  Data.Word.Word #-}
{-# COMPILED_TYPE Word32  Data.Word.Word32 #-}
{-# COMPILED_TYPE Word64  Data.Word.Word64 #-}


{-# COMPILED_DATA Name
    LLVM.General.AST.Name.Name
      LLVM.General.AST.Name.Name
      LLVM.General.AST.Name.UnName
#-}



data Type : Set where
  void : Type 
  integer : (bits : Word32)  Type
  pointer : (referent : Type)(space : AddrSpace)  Type
  floating : (bits : Word32) (format : FloatingFormat)  Type
  function : (result : Type) (arguments : Colist Type) (isVarArg : Bool)  Type
  vector   : (numElems : Word32) (elemType : Type)  Type
  struct    : (isPacket : Bool) (elemType : Colist Type)  Type
  array    : (numElems : Word64) (elemType : Type)  Type
  namedRef : (typeName : Name)  Type
  metadata : Type

{-# COMPILED_TYPE AddrSpace LLVM.General.AST.AddrSpace.AddrSpace #-}
{-# COMPILED_TYPE FloatingFormat LLVM.General.AST.FloatingPointFormat #-}
{-# COMPILED_DATA Type
    LLVM.General.AST.Type 
      LLVM.General.AST.VoidType
      LLVM.General.AST.IntegerType
      LLVM.General.AST.PointerType
      LLVM.General.AST.FloatingPointType
      LLVM.General.AST.FunctionType
      LLVM.General.AST.VectorType
      LLVM.General.AST.StructureType
      LLVM.General.AST.ArrayType
      LLVM.General.AST.NamedTypeReference
      LLVM.General.AST.MetadataType
#-}

data Global : Set where
  variable : 
    (name : Name)
    (linkage : Linkage)
    (visibility : Visibility)
    (isThreadLocal : Bool)
    (addrSpace : AddrSpace)
    (hasUnnamedAddr : Bool)
    (isConstant : Bool)
    (type : Type)
    (initializer : Maybe Constant)
    (section : Maybe Costring)
    (alignment : Word32) 
     Global
  alias :
    (name : Name)
    (linkage : Linkage)
    (visibility : Visibility)
    (type : Type) 
    (aliasee : Constant)
     Global
  function : 
    (linkage : Linkage)
    (visibility : Visibility) 
    (callingConvention : CallingConvention)
    (returnAttributes : Colist ParameterAttribute)
    (returnType : Type)
    (name : Name)
    (parameters : (Colist Parameter × Name))
    (functionAttributes : (Colist FunctionAttribute))
    (section : (Maybe Costring))
    (alignment : Word32)
    (garbageCollectorName : Maybe Costring)
    (basicBlocks : Colist BasicBlock)
    
     Global
  
{-# COMPILED_TYPE Linkage LLVM.General.AST.Linkage.Linkage #-}
{-# COMPILED_TYPE Visibility LLVM.General.AST.Visibility.Visibility #-}
{-# COMPILED_TYPE Constant LLVM.General.AST.Constant.Constant #-}
{-# COMPILED_TYPE CallingConvention LLVM.General.AST.CallingConvention.CallingConvention #-}
{-# COMPILED_TYPE ParameterAttribute LLVM.General.AST.Attribute.ParameterAttribute #-} 
{-# COMPILED_TYPE Parameter LLVM.General.AST.Parameter #-}
{-# COMPILED_TYPE FunctionAttribute LLVM.General.AST.Attribute.FunctionAttribute #-}
{-# COMPILED_TYPE BasicBlock LLVM.General.AST.BasicBlock #-}

{-# COMPILED_DATA Global
  LLVM.General.AST.Global
    LLVM.General.AST.GlobalVariable 
    LLVM.General.AST.GlobalAlias 
    LLVM.General.AST.Function
#-}

data Definition : Set where
  global     : (g : Global)                                                              Definition
  type        : (name : Name) (type : Maybe Type)                         Definition
  metadata : (id : MetadataNodeID) (operand : Maybe Operand)  Definition
  namedMetadata : (name : Costring) (nodeId : MetadataNodeID)  Definition
  inlineAssembly : (assembly : Costring)                                       Definition

{-# COMPILED_TYPE MetadataNodeID LLVM.General.AST.Operand.MetadataNodeID #-}
{-# COMPILED_TYPE DataLayout LLVM.General.AST.DataLayout.DataLayout #-}
{-# COMPILED_TYPE Operand    LLVM.General.AST.Operand #-}
{-# COMPILED_DATA 
  Definition LLVM.General.AST.Definition
                LLVM.General.AST.GlobalDefinition
                LLVM.General.AST.TypeDefinition
                LLVM.General.AST.MetadataNodeDefinition
                LLVM.General.AST.NamedMetadataDefinition
                LLVM.General.AST.ModuleInlineAssembly 
#-}

data Module  : Set where
  mkModule : 
    (name                   : Costring)
    (dataLayout           : Maybe DataLayout)
    (targetTriple         : Maybe Costring)
    (definitions           : Colist Definition)
     Module
    
{-# COMPILED_DATA Module 
  LLVM.General.AST.Module
  LLVM.General.AST.Module #-}

postulate 
  defaultModule : Module
{-# COMPILED defaultModule LLVM.General.AST.defaultModule #-}