Introduce semantics for sequences of instructions.

2 files changed, 33 insertions, 15 deletions

diff --git a/src/Helium/Instructions.agda b/src/Helium/Instructions.agda
index 4bd02ac..41bc74d 100644
--- a/src/Helium/Instructions.agda
+++ b/src/Helium/Instructions.agda
@@ -88,3 +88,10 @@ record VQDMulH : Set where
     rounding : Bool
 
   open VecOp₂ op₂ public
+
+data Instruction : Set where
+  vadd : VAdd → Instruction
+  vsub : VSub → Instruction
+  vmul : VMul → Instruction
+  vmulh : VMulH → Instruction
+  vqdmulh : VQDMulH → Instruction
diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda
index 77786f1..8e2cf85 100644
--- a/src/Helium/Semantics/Denotational.agda
+++ b/src/Helium/Semantics/Denotational.agda
@@ -17,7 +17,7 @@ open import Algebra.Core using (Op₂)
 open import Data.Bool as Bool using (Bool; true; false)
 open import Data.Fin as Fin hiding (cast; lift; _+_)
 import Data.Fin.Properties as Finₚ
-open import Data.Maybe using (just; nothing; _>>=_)
+open import Data.List using (List; []; _∷_)
 open import Data.Nat hiding (_⊔_)
 import Data.Nat.Properties as ℕₚ
 open import Data.Product using (∃; _×_; _,_; dmap)
@@ -25,7 +25,7 @@ open import Data.Sum using ([_,_]′)
 open import Data.Vec.Functional as V using (Vector)
 open import Function using (_$_; _∘₂_)
 open import Function.Nary.NonDependent.Base
-open import Helium.Instructions
+import Helium.Instructions as Instr
 import Helium.Semantics.Denotational.Core as Core
 open import Level hiding (lift; zero; suc)
 open import Relation.Binary using (Transitive)
@@ -81,7 +81,7 @@ ElmtMask = Bits 4
   ; set = λ x σ ρ → record σ { S = V.updateAt (e σ ρ) (λ _ → x) (State.S σ) } , ρ
   }
 
-&Q : ∀ {n ls} {Γ : Sets n ls} → PureExpr n Γ VecReg → PureExpr n Γ Beat → Reference n Γ (Bits 32)
+&Q : ∀ {n ls} {Γ : Sets n ls} → PureExpr n Γ Instr.VecReg → PureExpr n Γ Beat → Reference n Γ (Bits 32)
 &Q reg beat = &S λ σ ρ → combine (reg σ ρ) (beat σ ρ)
 
 &FPSCR-QC : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ (Bits 1)
@@ -155,7 +155,7 @@ elem m &v idx = slice &v (λ σ ρ → helper _ _ (idx σ ρ))
 
 -- General functions
 
-copyMasked : VecReg → Procedure 3 (Bits 32 , Beat , ElmtMask , _)
+copyMasked : Instr.VecReg → Procedure 3 (Bits 32 , Beat , ElmtMask , _)
 copyMasked dest =
   for 4 (
     -- 0:e 1:result 2:beat 3:elmtMask
@@ -227,10 +227,10 @@ execBeats inst = declare ⦇ ones ⦈ $
   ⦇ _ ⦈
 
 module _
-  (d : VecOp₂)
+  (d : Instr.VecOp₂)
   where
 
-  open VecOp₂ d
+  open Instr.VecOp₂ d
 
   vec-op₂ : Op₂ (Bits (toℕ esize)) → Procedure 2 (Beat , ElmtMask , _)
   vec-op₂ op = declare ⦇ zeros ⦈ $ declare (↓! &Q (pure′ src₁) (!# 1)) $
@@ -259,23 +259,23 @@ module _
   open sliceᶻ ≈ᶻ-trans round∘float round-cong 0#-homo-round 2^n≢0 *ᶻ-identityʳ
   open fun-sliceᶻ ≈ᶻ-trans round∘float round-cong 0#-homo-round 2^n≢0 *ᶻ-identityʳ
 
-  vadd : VAdd → Procedure 2 (Beat , ElmtMask , _)
+  vadd : Instr.VAdd → Procedure 2 (Beat , ElmtMask , _)
   vadd d = vec-op₂ d (λ x y → sliceᶻ _ zero (uint x +ᶻ uint y))
 
-  vsub : VSub → Procedure 2 (Beat , ElmtMask , _)
+  vsub : Instr.VSub → Procedure 2 (Beat , ElmtMask , _)
   vsub d = vec-op₂ d (λ x y → sliceᶻ _ zero (uint x +ᶻ -ᶻ uint y))
 
-  vhsub : VHSub → Procedure 2 (Beat , ElmtMask , _)
+  vhsub : Instr.VHSub → Procedure 2 (Beat , ElmtMask , _)
   vhsub d = vec-op₂ op₂ (λ x y → sliceᶻ _ (suc zero) (int x +ᶻ -ᶻ int y))
-    where open VHSub d ; int = Bool.if unsigned then uint else sint
+    where open Instr.VHSub d ; int = Bool.if unsigned then uint else sint
 
-  vmul : VMul → Procedure 2 (Beat , ElmtMask , _)
+  vmul : Instr.VMul → Procedure 2 (Beat , ElmtMask , _)
   vmul d = vec-op₂ d (λ x y → sliceᶻ _ zero (sint x *ᶻ sint y))
 
-  vmulh : VMulH → Procedure 2 (Beat , ElmtMask , _)
+  vmulh : Instr.VMulH → Procedure 2 (Beat , ElmtMask , _)
   vmulh d = vec-op₂ op₂ (λ x y → cast (eq _ esize) (sliceᶻ 2esize esize′ (int x *ᶻ int y +ᶻ rval)))
     where
-    open VMulH d
+    open Instr.VMulH d
     int = Bool.if unsigned then uint else sint
     rval = Bool.if rounding then 1ℤ << toℕ esize-1 else 0ℤ
     2esize = toℕ esize + toℕ esize
@@ -284,7 +284,7 @@ module _
     eq m zero    = refl
     eq m (suc i) = eq m i
 
-  vqdmulh : VQDMulH → Procedure 2 (Beat , ElmtMask , _)
+  vqdmulh : Instr.VQDMulH → Procedure 2 (Beat , ElmtMask , _)
   vqdmulh d = declare ⦇ zeros ⦈ $ declare (↓! &Q (pure′ src₁) (!# 1)) $ declare ⦇ false ⦈ $
     for (toℕ elements) (
       -- 0:e 1:sat 2:op₁ 3:result 4:beat 5:elmntMask
@@ -304,5 +304,16 @@ module _
     invoke (copyMasked dest) ⦇ ↓ !# 2 , ⦇ ↓ !# 3 , ↓ !# 4 ⦈ ⦈ ∙
     ⦇ _ ⦈
     where
-    open VQDMulH d
+    open Instr.VQDMulH d
     rval = Bool.if rounding then 1ℤ << toℕ esize-1 else 0ℤ
+
+  ⟦_⟧₁ : Instr.Instruction → Procedure 0 _
+  ⟦ Instr.vadd x ⟧₁ = execBeats (vadd x)
+  ⟦ Instr.vsub x ⟧₁ = execBeats (vsub x)
+  ⟦ Instr.vmul x ⟧₁ = execBeats (vmul x)
+  ⟦ Instr.vmulh x ⟧₁ = execBeats (vmulh x)
+  ⟦ Instr.vqdmulh x ⟧₁ = execBeats (vqdmulh x)
+
+  ⟦_⟧ : List (Instr.Instruction) → Procedure 0 _
+  ⟦ [] ⟧     = ⦇ _ ⦈
+  ⟦ i ∷ is ⟧ = invoke ⟦ i ⟧₁ ⦇ _ ⦈ ∙ ⟦ is ⟧