Commits

Anonymous committed d5ef7e3

Import typing fixed

  • Participants
  • Parent commits 698b0d8

Comments (0)

Files changed (1)

+module LLVM.AST where
 open import Data.Maybe
 {-# IMPORT LLVM.General.AST #-}
 {-# IMPORT LLVM.General.AST.DataLayout #-}
 data Name : Set where
   name : Costring → Name
   unName : Word → Name
-
-
 {-# COMPILED_DATA Name
     LLVM.General.AST.Name.Name
       LLVM.General.AST.Name.Name
   lshr ashr :    (exact : Bool)(op₁ op₂ : Constant) → Constant 
   and or xor : (op₁ op₂ : Constant) → Constant
   getElementPtr : (inBounds : Bool) (address : Constant) (indices : Colist Constant) → Constant
-  trunc zext sext fp2ui fp2si ui2fp si2pf fptrunc fpext ptr2int int2ptr bitCast : Operand → Type → Constant
+  trunc zext sext fp2ui fp2si ui2fp si2pf fptrunc fpext ptr2int int2ptr bitCast : Constant → Type → Constant
   icmp : (pred : IntegerPredicate)(op₁ op₂ : Constant) → Constant
   fcmp : (pred : FloatingPredicate)(op₁ op₂ : Constant) → Constant
   select : (cond true false : Constant) → Constant
     (returnAttributes : Colist ParameterAttribute)
     (returnType : Type)
     (name : Name)
-    (parameters : (Colist Parameter × Name))
+    (parameters : Colist Parameter × Bool)
     (functionAttributes : (Colist FunctionAttribute))
     (section : (Maybe Costring))
     (alignment : Word32)
 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
+  metadata : (id : MetadataNodeID) (operand : Colist (Maybe Operand)) → Definition
+  namedMetadata : (name : Costring) (nodeId : Colist MetadataNodeID) → Definition
   inlineAssembly : (assembly : Costring)                                      → Definition
 
 {-# COMPILED_TYPE DataLayout LLVM.General.AST.DataLayout.DataLayout #-}