Commits

Anonymous committed 386c88e

BasicBlock definition

Comments (0)

Files changed (1)

 {-# IMPORT LLVM.General.AST.Constant #-}
 {-# IMPORT LLVM.General.AST.CallingConvention #-}
 {-# IMPORT LLVM.General.AST.Attribute #-}
+{-# IMPORT LLVM.General.AST.Instruction #-}
+
 {-# IMPORT Data.Word #-}
 open import Data.String
 open import Data.Colist
 
 postulate
   DataLayout   Linkage Visibility Constant MetadataNodeID  Operand 
-    CallingConvention ParameterAttribute Parameter FunctionAttribute BasicBlock
+    CallingConvention ParameterAttribute Parameter FunctionAttribute 
+    Instruction Terminator
     Word Word32 Word64 AddrSpace FloatingFormat : Set
 
 data Name : Set where
       LLVM.General.AST.MetadataType
 #-}
 
+data Named (a : Set)  : Set where
+  _≔_ : Name → a → Named _
+  do : a → Named _ 
+
+{-# COMPILED_DATA Named
+  LLVM.General.AST.Instruction.Named
+    (LLVM.General.AST.Instruction.:=) LLVM.General.AST.Do
+ #-}
+{-# COMPILED_TYPE Instruction LLVM.General.AST.Instruction #-}
+{-# COMPILED_TYPE Terminator LLVM.General.AST.Terminator #-}
+
+
+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 Global : Set where
   variable : 
     (name : Name)
 {-# 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