1 files changed, 0 insertions, 96 deletions
diff --git a/src/Helium/Instructions.agda b/src/Helium/Instructions.agda
deleted file mode 100644
index ebe3f32..0000000
--- a/src/Helium/Instructions.agda
+++ /dev/null
@@ -1,96 +0,0 @@
-------------------------------------------------------------------------
--- Agda Helium
---
--- Definitions of a subset of Armv8-M instructions.
-------------------------------------------------------------------------
-
-{-# OPTIONS --safe --without-K #-}
-
-module Helium.Instructions where
-
-open import Data.Bool
-open import Data.Fin
-open import Data.Nat hiding (pred)
-open import Data.Product using (∃; _×_; _,_)
-open import Data.Sum
-open import Relation.Binary.PropositionalEquality
-
-GenReg : Set
-GenReg = Fin 16
-
-VecReg : Set
-VecReg = Fin 8
-
-data VecOpSize : Set where
-  8bit  : VecOpSize
-  16bit : VecOpSize
-  32bit : VecOpSize
-
-module Size (size : VecOpSize) where
-  elements-1 : Fin 4
-  elements-1 = helper size
-    where
-    helper : VecOpSize → Fin 4
-    helper 8bit  = # 3
-    helper 16bit = # 1
-    helper 32bit = # 0
-
-  elements : Fin 5
-  elements = suc elements-1
-
-  esize-1 : Fin 32
-  esize-1 = helper size
-    where
-    helper : VecOpSize → Fin 32
-    helper 8bit  = # 7
-    helper 16bit = # 15
-    helper 32bit = # 31
-
-  esize : Fin 33
-  esize = suc esize-1
-
-record VecOp₂ : Set where
-  field
-    size : VecOpSize
-    dest : VecReg
-    src₁ : VecReg
-    src₂ : GenReg ⊎ VecReg
-
-  open Size size public
-
-VAdd = VecOp₂
-
-VSub = VecOp₂
-
-record VHSub : Set where
-  field
-    op₂ : VecOp₂
-    unsigned : Bool
-
-  open VecOp₂ op₂ public
-
-VMul = VecOp₂
-
-record VMulH : Set where
-  field
-    op₂ : VecOp₂
-    unsigned : Bool
-
-  open VecOp₂ op₂ public
-
-record VRMulH : Set where
-  field
-    op₂ : VecOp₂
-    unsigned : Bool
-
-  open VecOp₂ op₂ public
-
-VQDMulH = VecOp₂
-VQRDMulH = VecOp₂
-
-data Instruction : Set where
-  vadd : VAdd → Instruction
-  vsub : VSub → Instruction
-  vmul : VMul → Instruction
-  vmulh : VMulH → Instruction
-  vqdmulh : VQDMulH → Instruction