Define semantics of vhsub.

4 files changed, 111 insertions, 44 deletions

diff --git a/src/Helium/Data/Pseudocode.agda b/src/Helium/Data/Pseudocode.agda
index 61a6b23..6cf25ec 100644
--- a/src/Helium/Data/Pseudocode.agda
+++ b/src/Helium/Data/Pseudocode.agda
@@ -3,10 +3,11 @@
 module Helium.Data.Pseudocode where
 
 open import Algebra.Core
-open import Data.Bool using (if_then_else_)
+open import Data.Bool using (Bool; if_then_else_)
 open import Data.Fin hiding (_+_; cast)
 import Data.Fin.Properties as Finₚ
 open import Data.Nat using (ℕ; zero; suc; _+_; _^_)
+import Data.Vec as Vec
 open import Level using (_⊔_) renaming (suc to ℓsuc)
 open import Relation.Binary using (REL; Rel; Symmetric; Transitive; Decidable)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
@@ -63,8 +64,6 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁
     _∶_ : ∀ {m n} → Bits m → Bits n → Bits (m + n)
     sliceᵇ  : ∀ {n} (i : Fin (suc n)) j → Bits n → Bits (toℕ (i - j))
     updateᵇ : ∀ {n} (i : Fin (suc n)) j → Bits (toℕ (i - j)) → Op₁ (Bits n)
-    signed : ∀ {n} → Bits n → ℤ
-    unsigned : ∀ {n} → Bits n → ℤ
 
   field
     -- Arithmetic operations
@@ -79,6 +78,53 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁
     _⁻¹  : ∀ (y : ℝ) → .{False (y ≟ʳ 0ℝ)} → ℝ
 
   -- Convenience operations
+
+  zeros : ∀ {n} → Bits n
+  zeros {zero}  = []
+  zeros {suc n} = 0b ∶ zeros
+
+  _eor_ : ∀ {n} → Op₂ (Bits n)
+  x eor y = (x or y) and not (x and y)
+
+  getᵇ : ∀ {n} → Fin n → Bits n → Bits 1
+  getᵇ i x = cast (eq i) (sliceᵇ (suc i) (inject₁ (strengthen i)) x)
+    where
+    eq : ∀ {n} (i : Fin n) → toℕ (suc i - inject₁ (strengthen i)) ≡ 1
+    eq zero    = refl
+    eq (suc i) = eq i
+
+  setᵇ : ∀ {n} → Fin n → Bits 1 → Op₁ (Bits n)
+  setᵇ i y = updateᵇ (suc i) (inject₁ (strengthen i)) (cast (sym (eq i)) y)
+    where
+    eq : ∀ {n} (i : Fin n) → toℕ (suc i - inject₁ (strengthen i)) ≡ 1
+    eq zero    = refl
+    eq (suc i) = eq i
+
+  hasBit : ∀ {n} → Fin n → Bits n → Bool
+  hasBit i x = does (getᵇ i x ≟ᵇ 1b)
+
+  -- Stray constant cannot live with the others, because + is not defined at that point.
+  2ℤ : ℤ
+  2ℤ = 1ℤ +ᶻ 1ℤ
+
+  _^ᶻ_ : ℤ → ℕ → ℤ
+  x ^ᶻ zero  = 1ℤ
+  x ^ᶻ suc y = x *ᶻ x ^ᶻ y
+
+  _^ʳ_ : ℝ → ℕ → ℝ
+  x ^ʳ zero  = 1ℝ
+  x ^ʳ suc y = x *ʳ x ^ʳ y
+
+  _<<_ : ℤ → ℕ → ℤ
+  x << n = x *ᶻ 2ℤ ^ᶻ n
+
+  uint : ∀ {n} → Bits n → ℤ
+  uint x = Vec.foldr (λ _ → ℤ) _+ᶻ_ 0ℤ (Vec.tabulate (λ i → if hasBit i x then 1ℤ << toℕ i else 0ℤ))
+
+  sint : ∀ {n} → Bits n → ℤ
+  sint {zero}  x = 0ℤ
+  sint {suc n} x = uint x +ᶻ (if hasBit (fromℕ n) x then -ᶻ 1ℤ << suc n else 0ℤ)
+
   module divmod
     (≈ᶻ-trans : Transitive _≈ᶻ_)
     (round∘⟦⟧ : ∀ x → x ≈ᶻ round ⟦ x ⟧)
@@ -96,21 +142,6 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁
     _mod_ : ∀ (x y : ℤ) → .{≢0 : False (y ≟ᶻ 0ℤ)} → ℤ
     (x mod y) {≢0} = x +ᶻ -ᶻ y *ᶻ (x div y) {≢0}
 
-  _^ᶻ_ : ℤ → ℕ → ℤ
-  x ^ᶻ zero  = 1ℤ
-  x ^ᶻ suc y = x *ᶻ x ^ᶻ y
-
-  _^ʳ_ : ℝ → ℕ → ℝ
-  x ^ʳ zero  = 1ℝ
-  x ^ʳ suc y = x *ʳ x ^ʳ y
-
-  -- Stray constant cannot live with the others, because + is not yet defined.
-  2ℤ : ℤ
-  2ℤ = 1ℤ +ᶻ 1ℤ
-
-  _<<_ : ℤ → ℕ → ℤ
-  x << n = x *ᶻ 2ℤ ^ᶻ n
-
   module 2^n≢0
     (≈ᶻ-trans : Transitive _≈ᶻ_)
     (round∘⟦⟧ : ∀ x → x ≈ᶻ round ⟦ x ⟧)
@@ -149,27 +180,4 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁
       2≢0 = map-False (≈ᶻ-trans (*ᶻ-identityʳ 2ℤ)) (2^n≢0 1)
 
     _+ᵇ_ : ∀ {n} → Op₂ (Bits n)
-    x +ᵇ y = sliceᶻ _ zero (unsigned x +ᶻ unsigned y)
-
-  _eor_ : ∀ {n} → Op₂ (Bits n)
-  x eor y = (x or y) and not (x and y)
-
-  getᵇ : ∀ {n} → Fin n → Bits n → Bits 1
-  getᵇ i x = cast (eq i) (sliceᵇ (suc i) (inject₁ (strengthen i)) x)
-    where
-    eq : ∀ {n} (i : Fin n) → toℕ (suc i - inject₁ (strengthen i)) ≡ 1
-    eq zero    = refl
-    eq (suc i) = eq i
-
-  setᵇ : ∀ {n} → Fin n → Bits 1 → Op₁ (Bits n)
-  setᵇ i y = updateᵇ (suc i) (inject₁ (strengthen i)) (cast (sym (eq i)) y)
-    where
-    eq : ∀ {n} (i : Fin n) → toℕ (suc i - inject₁ (strengthen i)) ≡ 1
-    eq zero    = refl
-    eq (suc i) = eq i
-
-  -- Conveniences
-
-  zeros : ∀ {n} → Bits n
-  zeros {zero}  = []
-  zeros {suc n} = 0b ∶ zeros
+    x +ᵇ y = sliceᶻ _ zero (uint x +ᶻ uint y)
diff --git a/src/Helium/Instructions.agda b/src/Helium/Instructions.agda
index 0d21322..2baf39d 100644
--- a/src/Helium/Instructions.agda
+++ b/src/Helium/Instructions.agda
@@ -2,6 +2,7 @@
 
 module Helium.Instructions where
 
+open import Data.Bool
 open import Data.Fin
 open import Data.Nat
 open import Data.Sum
@@ -37,3 +38,29 @@ module VAdd
   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 VHSub
+  where
+
+  record VHSub : Set where
+    field
+      unsigned : Bool
+      size : Fin 3
+      dest : VecReg
+      src₁ : VecReg
+      src₂ : GenReg ⊎ VecReg
+
+  esize : VHSub → Fin 33
+  esize record { size = zero }             = # 8
+  esize record { size = (suc zero) }       = # 16
+  esize record { size = (suc (suc zero)) } = # 32
+
+  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
diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda
index 8a6e0b5..c6d019e 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 Data.Bool as Bool using (Bool)
 open import Data.Fin as Fin hiding (cast; lift; _+_)
 import Data.Fin.Properties as Finₚ
 open import Data.Maybe using (just; nothing; _>>=_)
@@ -103,6 +104,11 @@ elem m &v idx = slice &v λ σ ρ → idx σ ρ >>= λ (σ , i) → just (σ , h
     cast‿- {suc m} {suc n} x       zero    eq = Finₚ.toℕ-cast eq x
     cast‿- {suc m} {suc n} (suc x) (suc y) eq = cast‿- x y (ℕₚ.suc-injective eq)
 
+-- General functions
+
+int : ∀ {n} → Bool → Function 1 (Bits n , _) ℤ
+int b = return ⦇ (Bool.if b then uint else sint) (!# 0) ⦈
+
 -- Instruction semantics
 
 module _
@@ -139,3 +145,29 @@ module _
     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) ≔
+      ⦇ (sliceᶻ (suc (toℕ esize)) (suc zero))
+        ⦇ call (int unsigned) (! elem (toℕ esize) (&cast (sym e*e≡32) (var (# 1))) (!# 0)) +ᶻ
+          ⦇ -ᶻ (call (int unsigned)
+            ([ (λ src₂ → ! slice (&R ⦇ src₂ ⦈) ⦇ (esize , zero , refl) ⦈)
+             , (λ src₂ → ! elem (toℕ esize) (&cast (sym e*e≡32) (&Q ⦇ src₂ ⦈ (!# 3))) (!# 0))
+             ]′ src₂)) ⦈ ⦈ ⦈
+    )) ∙
+    for 4 (lift (
+      -- e op₁ result beat elmtMask
+      if ⦇ (λ x y → does (getᵇ y x ≟ᵇ 1b)) (!# 4) (!# 0) ⦈
+      then
+        elem 8 (&Q ⦇ dest ⦈ (!# 3)) (!# 0) ≔ (! elem 8 (var (# 2)) (!# 0))
+      else
+        skip))))
+    where
+    open VHSub.VHSub d
+    esize = VHSub.esize d
+    elements = VHSub.elements d
+    e*e≡32 = VHSub.elem*esize≡32 d
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
index a0a37e8..bf5f20f 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -75,8 +75,8 @@ _<*>_ f e σ ρ = f σ ρ >>= λ (σ , f) → apply f e σ ρ
 !_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Expr n Γ τ
 ! r = Reference.get r
 
-call : ∀ {m n ls₁ ls₂} {Γ : Sets m ls₁} {Δ : Sets n ls₂} → Function m Γ τ → Expr n Δ (Product⊤ m Γ) → Expr n Δ τ
-call f e σ ρ = e σ ρ >>= λ (σ , v) → f unknown σ v
+call : ∀ {m n ls₁ ls₂} {Γ : Sets m ls₁} {Δ : Sets n ls₂} → Function m Γ τ → Expr n Δ (Product m Γ) → Expr n Δ τ
+call f e σ ρ = e σ ρ >>= λ (σ , v) → f unknown σ (toProduct⊤ _ v)
 
 -- References