From bfcbca52a117ec207addf629f1cada93e0f12e02 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Sun, 13 Feb 2022 14:01:44 +0000
Subject: Refactor to group instruction definitions together

---
 src/Helium/Instructions/Core.agda | 96 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 96 insertions(+)
 create mode 100644 src/Helium/Instructions/Core.agda

(limited to 'src/Helium/Instructions/Core.agda')

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
-- 
cgit v1.2.3