diff options
| -rw-r--r-- | src/Helium/Data/Pseudocode.agda | 92 | ||||
| -rw-r--r-- | src/Helium/Instructions.agda | 27 | ||||
| -rw-r--r-- | src/Helium/Semantics/Denotational.agda | 32 | ||||
| -rw-r--r-- | src/Helium/Semantics/Denotational/Core.agda | 4 |
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 |