Commits

Anonymous committed 2250715

more definitions

  • Participants
  • Parent commits 41a9252

Comments (0)

Files changed (1)

 {-# COMPILED_DATA _×_ (,) (,) #-}  
 
 postulate
-  DataLayout   Linkage Visibility Constant MetadataNodeID   
-     Parameter  
-     Terminator 
-    Word Word32 Word64 AddrSpace FloatingFormat : Set
+  DataLayout     Constant MetadataNodeID   
+        Word Word32 Word64   : Set
+
+
+{-# COMPILED_TYPE Word  Data.Word.Word #-}
+{-# COMPILED_TYPE Word32  Data.Word.Word32 #-}
+{-# COMPILED_TYPE Word64  Data.Word.Word64 #-}
+
+data FloatingFormat : Set where
+  ieee  doubleExtended pairOfFloats : FloatingFormat
+
+{-# COMPILED_DATA FloatingFormat
+    LLVM.General.AST.FloatingPointFormat
+    LLVM.General.AST.IEEE
+    LLVM.General.AST.DoubleExtended
+    LLVM.General.AST.PairOfFloats
+#-}
+
+data AddrSpace : Set where
+  addrSpace : Word32 → AddrSpace
+
+{-# COMPILED_DATA AddrSpace
+  LLVM.General.AST.AddrSpace.AddrSpace  LLVM.General.AST.AddrSpace.AddrSpace #-}
+
+data Linkage : Set where
+  privat linkerPrivate linkerPrivateWeak internal availableExternally linkOnce
+    weak common appending externWeak linkOnceODR weakODR external dllImport dllExport : Linkage
+{-# COMPILED_DATA Linkage
+  LLVM.General.AST.Linkage.Linkage
+  LLVM.General.AST.Linkage.Private
+  LLVM.General.AST.Linkage.LinkerPrivate
+  LLVM.General.AST.Linkage.LinkerPrivateWeak
+  LLVM.General.AST.Linkage.Internal
+  LLVM.General.AST.Linkage.AvailableExternally
+  LLVM.General.AST.Linkage.LinkOnce
+  LLVM.General.AST.Linkage.Weak
+  LLVM.General.AST.Linkage.Common
+  LLVM.General.AST.Linkage.Appending
+  LLVM.General.AST.Linkage.ExternWeak
+  LLVM.General.AST.Linkage.LinkOnceODR
+  LLVM.General.AST.Linkage.WeakODR
+  LLVM.General.AST.Linkage.External
+  LLVM.General.AST.Linkage.DLLImport
+  LLVM.General.AST.Linkage.DLLExport
+#-}
 
 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
   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.MetadataType
 #-}
 
+
 data Named (a : Set)  : Set where
   _≔_ : Name → a → Named _
   do : a → Named _ 
     (LLVM.General.AST.Instruction.:=) LLVM.General.AST.Do
  #-}
 
-{-# COMPILED_TYPE Terminator LLVM.General.AST.Terminator #-}
 {-# COMPILED_TYPE Constant LLVM.General.AST.Constant.Constant #-}
 
 {-------------------BUG-BUG-BUG-BUG --------------------------------
       LLVM.General.AST.Attribute.Nest 
 #-}
 
+
+
+data Parameter : Set where
+  parameter : (type : Type) (name : Name)(attributes : Colist ParameterAttribute) → Parameter
+
+{-# COMPILED_DATA Parameter 
+  LLVM.General.AST.Parameter
+  LLVM.General.AST.Parameter
+#-}
+
 data Operand : Set where
   localReference : (name : Name) → Operand
   constant : (val : Constant) → Operand
   
   
 
-data Instruction : Set 
-private
-  Meta = (metadata : InstructionMetadata) → Instruction
-  Op₂ = (op₁ op₂ : Operand) → Meta
-  IOp₂ = (nsw nuw : Bool) → Op₂
-  Exact = (exact : Bool) → Op₂
-  Aligned = (alignment : Word32) → Meta
-  Atomic = (atomicity : Atomicity) → Meta
-  Convert = (operand : Operand) (type : Type) → Meta
+module _ where
+  data Instruction : Set 
+  private
+    Meta = (metadata : InstructionMetadata) → Instruction
+    Op₂ = (op₁ op₂ : Operand) → Meta
+    IOp₂ = (nsw nuw : Bool) → Op₂
+    Exact = (exact : Bool) → Op₂
+    Aligned = (alignment : Word32) → Meta
+    Atomic = (atomicity : Atomicity) → Meta
+    Convert = (operand : Operand) (type : Type) → Meta
+   
+  data Instruction  where
+    add  :  IOp₂
+    fadd : Op₂
+    sub : IOp₂
+    fsub : Op₂
+    mul : IOp₂  
+    fmul : Op₂
+    udiv sdiv :  Exact
+    fdiv urem srem frem : Op₂
+    shl : IOp₂
+    lshr ashr : Exact
+    and or xor : Op₂
+    alloca : (type : Type) (numElements : Maybe Operand) (alignment : Word32) → Meta
+    load  : (volatile : Bool) (address : Operand) (atomicity : Maybe Atomicity) → Aligned
+    store : (volatile : Bool) (address value  : Operand) (atomicity : Maybe Atomicity) → Aligned
+    getElementPtr : (inBounds : Bool)(address : Operand)(indices : Colist Operand) → Meta
+    fence :  Atomic 
+    cmpxchg : (volatile : Bool) (address expected replacement : Operand ) → Atomic
+    atomicRMW : (volatile : Bool) (operation : RMWOperation)(address value : Operand) → Atomic
+    trunc zext sext fp2ui fp2si ui2fp si2fp fpTrunc fpExt ptr2int int2ptr bitcast addrSpaceCast  : Convert
+   
+    icmp : IntegerPredicate → Op₂
+    fcmp : FloatingPredicate → Op₂
+    phi : (type : Type)(incomingValues : Colist (Operand × Name)) → Meta
+    call :
+      (isTailCall : Bool) (callingConvention : CallingConvention) (returnAttributes : Colist ParameterAttribute)
+        (function : CallableOperand) (arguments : Colist (Operand × Colist ParameterAttribute))
+        (functionAttributes : Colist FunctionAttribute)
+        → Meta
+    select : (condition : Operand) → Op₂
+    vaarg : (arglist : Operand) (type : Type) → Meta
+    extractElement : (vector index : Operand) → Meta
+    insertElement  : (vector element index : Operand) → Meta
+    shuffleVector : (op₁ op₂ : Operand) (mask : Constant) → Meta
+    extractValue : (val : Operand) (indices : Colist Word32) → Meta
+    insertValue : (agregate element : Operand) (indices : Colist Word32) → Meta
+    landingPad : (type : Type) (personalityFunction : Operand)(cleanup : Bool) (clauses : Colist LandingPadClause) → Meta
 
-data Instruction  where
-  add  :  IOp₂
-  fadd : Op₂
-  sub : IOp₂
-  fsub : Op₂
-  mul : IOp₂  
-  fmul : Op₂
-  udiv sdiv :  Exact
-  fdiv urem srem frem : Op₂
-  shl : IOp₂
-  lshr ashr : Exact
-  and or xor : Op₂
-  alloca : (type : Type) (numElements : Maybe Operand) (alignment : Word32) → Meta
-  load  : (volatile : Bool) (address : Operand) (atomicity : Maybe Atomicity) → Aligned
-  store : (volatile : Bool) (address value  : Operand) (atomicity : Maybe Atomicity) → Aligned
-  getElementPtr : (inBounds : Bool)(address : Operand)(indices : Colist Operand) → Meta
-  fence :  Atomic 
-  cmpxchg : (volatile : Bool) (address expected replacement : Operand ) → Atomic
-  atomicRMW : (volatile : Bool) (operation : RMWOperation)(address value : Operand) → Atomic
-  trunc zext sext fp2ui fp2si ui2fp si2fp fpTrunc fpExt ptr2int int2ptr bitcast addrSpaceCast  : Convert
+  {-# COMPILED_DATA Instruction
+    LLVM.General.AST.Instruction
+    LLVM.General.AST.Add 
+    LLVM.General.AST.FAdd 
+    LLVM.General.AST.Sub 
+    LLVM.General.AST.FSub 
+    LLVM.General.AST.Mul 
+    LLVM.General.AST.FMul 
+    LLVM.General.AST.UDiv 
+    LLVM.General.AST.SDiv 
+    LLVM.General.AST.FDiv 
+    LLVM.General.AST.URem 
+    LLVM.General.AST.SRem 
+    LLVM.General.AST.FRem 
+    LLVM.General.AST.Shl 
+    LLVM.General.AST.LShr 
+    LLVM.General.AST.AShr 
+    LLVM.General.AST.And 
+    LLVM.General.AST.Or 
+    LLVM.General.AST.Xor 
+    LLVM.General.AST.Alloca 
+    LLVM.General.AST.Load 
+    LLVM.General.AST.Store 
+    LLVM.General.AST.GetElementPtr 
+    LLVM.General.AST.Fence 
+    LLVM.General.AST.CmpXchg 
+    LLVM.General.AST.AtomicRMW 
+    LLVM.General.AST.Trunc 
+    LLVM.General.AST.ZExt 
+    LLVM.General.AST.SExt 
+    LLVM.General.AST.FPToUI 
+    
+    LLVM.General.AST.FPToSI 
+    LLVM.General.AST.UIToFP 
+    LLVM.General.AST.SIToFP 
+    LLVM.General.AST.FPTrunc 
+    LLVM.General.AST.FPExt 
+    LLVM.General.AST.PtrToInt 
+    LLVM.General.AST.IntToPtr 
+    LLVM.General.AST.BitCast 
+    LLVM.General.AST.AddrSpaceCast
+    
+    LLVM.General.AST.ICmp 
+    LLVM.General.AST.FCmp 
+    LLVM.General.AST.Phi 
+    LLVM.General.AST.Call 
+    LLVM.General.AST.Select 
+    LLVM.General.AST.VAArg 
+    LLVM.General.AST.ExtractElement 
+    LLVM.General.AST.InsertElement 
+    LLVM.General.AST.ShuffleVector 
+    LLVM.General.AST.ExtractValue 
+    LLVM.General.AST.InsertValue 
+    LLVM.General.AST.LandingPad 
+   
+  #-}
+   
 
-  icmp : IntegerPredicate → Op₂
-  fcmp : FloatingPredicate → Op₂
-  phi : (type : Type)(incomingValues : Colist (Operand × Name)) → Meta
-  call :
-    (isTailCall : Bool) (callingConvention : CallingConvention) (returnAttributes : Colist ParameterAttribute)
-      (function : CallableOperand) (arguments : Colist (Operand × Colist ParameterAttribute))
-      (functionAttributes : Colist FunctionAttribute)
+module _ where
+  data Terminator : Set
+  private
+    Meta = InstructionMetadata → Terminator
+  data Terminator  where
+    ret : (returnOperand : Maybe Operand) → Meta
+    condBr : (condition : Operand) (trueDest falseDest : Name) → Meta
+    br : (dest : Name) → Meta
+    switch : (op : Operand) (defaultDest : Name) (dests : Colist (Constant × Name)) → Meta
+    indirectBr : (op : Operand) (possibleDests : Colist Name) → Meta
+    invoke : 
+      (callingConvention : CallingConvention) 
+      (returnAttributes : Colist ParameterAttribute)
+      (function : CallableOperand)
+      (arguments : Colist (Operand × Colist ParameterAttribute ))
+      (functionAttributes : Colist FunctionAttribute) 
+      (returnDest : Name)
+      (exceptionDest : Name)
       → Meta
-  select : (condition : Operand) → Op₂
-  vaarg : (arglist : Operand) (type : Type) → Meta
-  extractElement : (vector index : Operand) → Meta
-  insertElement  : (vector element index : Operand) → Meta
-  shuffleVector : (op₁ op₂ : Operand) (mask : Constant) → Meta
-  extractValue : (val : Operand) (indices : Colist Word32) → Meta
-  insertValue : (agregate element : Operand) (indices : Colist Word32) → Meta
-  landingPad : (type : Type) (personalityFunction : Operand)(cleanup : Bool) (clauses : Colist LandingPadClause) → Meta
+    resume : (op : Operand) → Meta
+    unreachable : Meta
 
-{-# COMPILED_DATA Instruction
-  LLVM.General.AST.Instruction
-  LLVM.General.AST.Add 
-  LLVM.General.AST.FAdd 
-  LLVM.General.AST.Sub 
-  LLVM.General.AST.FSub 
-  LLVM.General.AST.Mul 
-  LLVM.General.AST.FMul 
-  LLVM.General.AST.UDiv 
-  LLVM.General.AST.SDiv 
-  LLVM.General.AST.FDiv 
-  LLVM.General.AST.URem 
-  LLVM.General.AST.SRem 
-  LLVM.General.AST.FRem 
-  LLVM.General.AST.Shl 
-  LLVM.General.AST.LShr 
-  LLVM.General.AST.AShr 
-  LLVM.General.AST.And 
-  LLVM.General.AST.Or 
-  LLVM.General.AST.Xor 
-  LLVM.General.AST.Alloca 
-  LLVM.General.AST.Load 
-  LLVM.General.AST.Store 
-  LLVM.General.AST.GetElementPtr 
-  LLVM.General.AST.Fence 
-  LLVM.General.AST.CmpXchg 
-  LLVM.General.AST.AtomicRMW 
-  LLVM.General.AST.Trunc 
-  LLVM.General.AST.ZExt 
-  LLVM.General.AST.SExt 
-  LLVM.General.AST.FPToUI 
-  
-  LLVM.General.AST.FPToSI 
-  LLVM.General.AST.UIToFP 
-  LLVM.General.AST.SIToFP 
-  LLVM.General.AST.FPTrunc 
-  LLVM.General.AST.FPExt 
-  LLVM.General.AST.PtrToInt 
-  LLVM.General.AST.IntToPtr 
-  LLVM.General.AST.BitCast 
-  LLVM.General.AST.AddrSpaceCast
-  
-  LLVM.General.AST.ICmp 
-  LLVM.General.AST.FCmp 
-  LLVM.General.AST.Phi 
-  LLVM.General.AST.Call 
-  LLVM.General.AST.Select 
-  LLVM.General.AST.VAArg 
-  LLVM.General.AST.ExtractElement 
-  LLVM.General.AST.InsertElement 
-  LLVM.General.AST.ShuffleVector 
-  LLVM.General.AST.ExtractValue 
-  LLVM.General.AST.InsertValue 
-  LLVM.General.AST.LandingPad 
+  {-# COMPILED_DATA Terminator 
+      LLVM.General.AST.Instruction.Terminator
+      LLVM.General.AST.Instruction.Ret
 
-#-}
-
+      LLVM.General.AST.Instruction.CondBr
+      LLVM.General.AST.Instruction.Br
+      LLVM.General.AST.Instruction.Switch
+      LLVM.General.AST.Instruction.IndirectBr
+      LLVM.General.AST.Instruction.Invoke
+      LLVM.General.AST.Instruction.Resume
+      LLVM.General.AST.Instruction.Unreachable
+    #-}
 
 data BasicBlock : Set where
   block : (name : Name) (instructions : Colist (Named Instruction)) (terminator : Named Terminator) → BasicBlock
 {-# COMPILED_DATA BasicBlock LLVM.General.AST.BasicBlock LLVM.General.AST.BasicBlock #-}
 
 
+data Visibility : Set where
+  default hidden protected : Visibility
+
+{-# COMPILED_DATA Visibility
+    LLVM.General.AST.Visibility.Visibility
+    LLVM.General.AST.Visibility.Default
+    LLVM.General.AST.Visibility.Hidden
+    LLVM.General.AST.Visibility.Protected
+#-}
 
 data Global : Set where
   variable : 
     
     → 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 Parameter LLVM.General.AST.Parameter #-}
 
 {-# COMPILED_DATA Global
   LLVM.General.AST.Global