From e32ce3737798d4519c5497c36e912e92d60bd36b Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Mon, 20 Dec 2021 17:43:43 +0000 Subject: Define semantics of vhsub. --- src/Helium/Semantics/Denotational.agda | 32 +++++++++++++++++++++++++++++ src/Helium/Semantics/Denotational/Core.agda | 4 ++-- 2 files changed, 34 insertions(+), 2 deletions(-) (limited to 'src/Helium/Semantics') 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 -- cgit v1.2.3