Extract structures shared by most binary vector operations.

This is the extraction promised a couple of commits ago.

2 files changed, 55 insertions, 124 deletions

diff --git a/src/Helium/Instructions.agda b/src/Helium/Instructions.agda
index 9560cc2..256f9c4 100644
--- a/src/Helium/Instructions.agda
+++ b/src/Helium/Instructions.agda
@@ -5,6 +5,7 @@ module Helium.Instructions where
 open import Data.Bool
 open import Data.Fin
 open import Data.Nat
+open import Data.Product using (∃; _,_)
 open import Data.Sum
 open import Relation.Binary.PropositionalEquality
 
@@ -14,78 +15,37 @@ GenReg = Fin 16
 VecReg : Set
 VecReg = Fin 8
 
-module VAdd
-  where
+record VecOp₂ : Set where
+  field
+    size : Fin 3
+    dest : VecReg
+    src₁ : VecReg
+    src₂ : GenReg ⊎ VecReg
 
-  record VAdd : Set where
-    field
-      size : Fin 3
-      dest : VecReg
-      src₁ : VecReg
-      src₂ : GenReg ⊎ VecReg
+  split32 : ∃ λ (elements : Fin 5) → ∃ λ (esize : Fin 33) → toℕ elements * toℕ esize ≡ 32
+  split32 = helper size
+    where
+    helper : _ → _
+    helper zero             = # 4 , # 8 , refl
+    helper (suc zero)       = # 2 , # 16 , refl
+    helper (suc (suc zero)) = # 1 , # 32 , refl
 
-  esize : VAdd → Fin 33
-  esize record { size = zero }             = # 8
-  esize record { size = (suc zero) }       = # 16
-  esize record { size = (suc (suc zero)) } = # 32
+  elements : Fin 5
+  elements with (elmt , _ , _) ← split32 = elmt
 
-  elements : VAdd → Fin 5
-  elements record { size = zero }             = # 4
-  elements record { size = (suc zero) }       = # 2
-  elements record { size = (suc (suc zero)) } = # 1
+  esize : Fin 33
+  esize with (_ , esize , _) ← split32 = esize
 
-  elem*esize≡32 : ∀ d → toℕ (elements d) * toℕ (esize d) ≡ 32
-  elem*esize≡32 record { size = zero }             = refl
-  elem*esize≡32 record { size = (suc zero) }       = refl
-  elem*esize≡32 record { size = (suc (suc zero)) } = refl
+  e*e≡32 : toℕ elements * toℕ esize ≡ 32
+  e*e≡32 with (_ , _ , eq) ← split32 = eq
 
-module VHSub
-  where
+VAdd = VecOp₂
 
-  record VHSub : Set where
-    field
-      unsigned : Bool
-      size : Fin 3
-      dest : VecReg
-      src₁ : VecReg
-      src₂ : GenReg ⊎ VecReg
+record VHSub : Set where
+  field
+    op₂ : VecOp₂
+    unsigned : Bool
 
-  esize : VHSub → Fin 33
-  esize record { size = zero }             = # 8
-  esize record { size = (suc zero) }       = # 16
-  esize record { size = (suc (suc zero)) } = # 32
+  open VecOp₂ op₂ public
 
-  elements : VHSub → Fin 5
-  elements record { size = zero }             = # 4
-  elements record { size = (suc zero) }       = # 2
-  elements record { size = (suc (suc zero)) } = # 1
-
-  elem*esize≡32 : ∀ d → toℕ (elements d) * toℕ (esize d) ≡ 32
-  elem*esize≡32 record { size = zero }             = refl
-  elem*esize≡32 record { size = (suc zero) }       = refl
-  elem*esize≡32 record { size = (suc (suc zero)) } = refl
-
-module VMul
-  where
-
-  record VMul : Set where
-    field
-      size : Fin 3
-      dest : VecReg
-      src₁ : VecReg
-      src₂ : GenReg ⊎ VecReg
-
-  esize : VMul → Fin 33
-  esize record { size = zero }             = # 8
-  esize record { size = (suc zero) }       = # 16
-  esize record { size = (suc (suc zero)) } = # 32
-
-  elements : VMul → Fin 5
-  elements record { size = zero }             = # 4
-  elements record { size = (suc zero) }       = # 2
-  elements record { size = (suc (suc zero)) } = # 1
-
-  elem*esize≡32 : ∀ d → toℕ (elements d) * toℕ (esize d) ≡ 32
-  elem*esize≡32 record { size = zero }             = refl
-  elem*esize≡32 record { size = (suc zero) }       = refl
-  elem*esize≡32 record { size = (suc (suc zero)) } = refl
+VMul = VecOp₂
diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda
index eaaad62..0739d28 100644
--- a/src/Helium/Semantics/Denotational.agda
+++ b/src/Helium/Semantics/Denotational.agda
@@ -7,6 +7,7 @@ module Helium.Semantics.Denotational
   (pseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃)
   where
 
+open import Algebra.Core using (Op₂)
 open import Data.Bool as Bool using (Bool)
 open import Data.Fin as Fin hiding (cast; lift; _+_)
 import Data.Fin.Properties as Finₚ
@@ -115,75 +116,45 @@ copy-masked dest = for 4 (lift (
   else
     skip))
 
--- vec-op₂ : VecReg → GenReg → Op₂ (Bits n)
-
--- Instruction semantics
-
 module _
-  (≈ᶻ-trans : Transitive _≈ᶻ_)
-  (round∘⟦⟧ : ∀ x → x ≈ᶻ round ⟦ x ⟧)
-  (round-cong : ∀ {x y} → x ≈ʳ y → round x ≈ᶻ round y)
-  (0#-homo-round : round 0ℝ ≈ᶻ 0ℤ)
-  (2^n≢0 : ∀ n → False (2ℤ ^ᶻ n ≟ᶻ 0ℤ))
-  (*ᶻ-identityʳ : ∀ x → x *ᶻ 1ℤ ≈ᶻ x)
+  (d : VecOp₂)
   where
 
-  open sliceᶻ ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round 2^n≢0 *ᶻ-identityʳ
+  open VecOp₂ d
 
-  vadd : VAdd.VAdd → Procedure 2 (Beat , ElmtMask , _)
-  vadd d = declare ⦇ zeros ⦈ (declare (! &Q ⦇ src₁ ⦈ (!# 1)) (
+  vec-op₂ : Op₂ (Bits (toℕ esize)) → Procedure 2 (Beat , ElmtMask , _)
+  vec-op₂ op = declare ⦇ zeros ⦈ (declare (! &Q ⦇ src₁ ⦈ (!# 1)) (
     -- op₁ result beat elmtMask
     for (toℕ elements) (lift (
       -- e op₁ result beat elmtMask
       elem (toℕ esize) (&cast (sym e*e≡32) (var (# 2))) (!# 0) ≔
-      ⦇ _+ᵇ_
+      ⦇ op
         (! elem (toℕ esize) (&cast (sym e*e≡32) (var (# 1))) (!# 0))
         ([ (λ src₂ → ! slice (&R ⦇ src₂ ⦈) ⦇ (esize , zero , refl) ⦈)
          , (λ src₂ → ! elem (toℕ esize) (&cast (sym e*e≡32) (&Q ⦇ src₂ ⦈ (!# 3))) (!# 0))
          ]′ src₂) ⦈
     )) ∙
     ignore (call (copy-masked dest) ⦇ !# 1 , ⦇ !# 2 , !# 3 ⦈ ⦈)))
-    where
-    open VAdd.VAdd d
-    esize = VAdd.esize d
-    elements = VAdd.elements d
-    e*e≡32 = VAdd.elem*esize≡32 d
 
-  vhsub : VHSub.VHSub → Procedure 2 (Beat , ElmtMask , _)
-  vhsub d = declare ⦇ zeros ⦈ (declare (! &Q ⦇ src₁ ⦈ (!# 1)) (
-    -- op₁ result beat elmtMask
-    for (toℕ elements) (lift (
-      -- e op₁ result beat elmtMask
-      elem (toℕ esize) (&cast (sym e*e≡32) (var (# 2))) (!# 0) ≔
-      ⦇ (λ x y → sliceᶻ (suc (toℕ esize)) (suc zero) (int x +ᶻ -ᶻ int y))
-        (! elem (toℕ esize) (&cast (sym e*e≡32) (var (# 1))) (!# 0))
-        ([ (λ src₂ → ! slice (&R ⦇ src₂ ⦈) ⦇ (esize , zero , refl) ⦈)
-         , (λ src₂ → ! elem (toℕ esize) (&cast (sym e*e≡32) (&Q ⦇ src₂ ⦈ (!# 3))) (!# 0))
-         ]′ src₂) ⦈
-    )) ∙
-    ignore (call (copy-masked dest) ⦇ !# 1 , ⦇ !# 2 , !# 3 ⦈ ⦈)))
-    where
-    open VHSub.VHSub d
-    esize = VHSub.esize d
-    elements = VHSub.elements d
-    e*e≡32 = VHSub.elem*esize≡32 d
-    int = Bool.if unsigned then uint else sint
-
-  vmul : VMul.VMul → Procedure 2 (Beat , ElmtMask , _)
-  vmul d = declare ⦇ zeros ⦈ (declare (! &Q ⦇ src₁ ⦈ (!# 1)) (
-    -- op₁ result beat elmtMask
-    for (toℕ elements) (lift (
-      -- e op₁ result beat elmtMask
-      elem (toℕ esize) (&cast (sym e*e≡32) (var (# 2))) (!# 0) ≔
-      ⦇ (λ x y → sliceᶻ (toℕ esize) zero (sint x *ᶻ sint y))
-        (! elem (toℕ esize) (&cast (sym e*e≡32) (var (# 1))) (!# 0))
-        ([ (λ src₂ → ! slice (&R ⦇ src₂ ⦈) ⦇ (esize , zero , refl) ⦈)
-         , (λ src₂ → ! elem (toℕ esize) (&cast (sym e*e≡32) (&Q ⦇ src₂ ⦈ (!# 3))) (!# 0))
-         ]′ src₂) ⦈
-    )) ∙
-    ignore (call (copy-masked dest) ⦇ !# 1 , ⦇ !# 2 , !# 3 ⦈ ⦈)))
-    where
-    open VMul.VMul d
-    esize = VMul.esize d
-    elements = VMul.elements d
-    e*e≡32 = VMul.elem*esize≡32 d
+-- Instruction semantics
+
+module _
+  (≈ᶻ-trans : Transitive _≈ᶻ_)
+  (round∘⟦⟧ : ∀ x → x ≈ᶻ round ⟦ x ⟧)
+  (round-cong : ∀ {x y} → x ≈ʳ y → round x ≈ᶻ round y)
+  (0#-homo-round : round 0ℝ ≈ᶻ 0ℤ)
+  (2^n≢0 : ∀ n → False (2ℤ ^ᶻ n ≟ᶻ 0ℤ))
+  (*ᶻ-identityʳ : ∀ x → x *ᶻ 1ℤ ≈ᶻ x)
+  where
+
+  open sliceᶻ ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round 2^n≢0 *ᶻ-identityʳ
+
+  vadd : VAdd → Procedure 2 (Beat , ElmtMask , _)
+  vadd d = vec-op₂ d _+ᵇ_
+
+  vhsub : VHSub → Procedure 2 (Beat , ElmtMask , _)
+  vhsub d = vec-op₂ op₂ (λ x y → sliceᶻ (suc (toℕ esize)) (suc zero) (int x +ᶻ -ᶻ int y))
+    where open VHSub d ; int = Bool.if unsigned then uint else sint
+
+  vmul : VMul → Procedure 2 (Beat , ElmtMask , _)
+  vmul d = vec-op₂ d (λ x y → sliceᶻ (toℕ _) zero (sint x *ᶻ sint y))