Refactor to group instruction definitions together

1 files changed, 96 insertions, 0 deletions

diff --git a/src/Helium/Instructions/Core.agda b/src/Helium/Instructions/Core.agda
new file mode 100644
index 0000000..466a396
--- /dev/null
+++ b/src/Helium/Instructions/Core.agda
@@ -0,0 +1,96 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Definitions of the data for a subset of Armv8-M instructions.
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+module Helium.Instructions.Core 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