summaryrefslogtreecommitdiff
path: root/src/Helium
diff options
context:
space:
mode:
Diffstat (limited to 'src/Helium')
-rw-r--r--src/Helium/Data/Pseudocode/Core.agda4
-rw-r--r--src/Helium/Instructions/Base.agda26
-rw-r--r--src/Helium/Instructions/Instances/Barrett.agda4
-rw-r--r--src/Helium/Semantics/Denotational/Core.agda9
4 files changed, 24 insertions, 19 deletions
diff --git a/src/Helium/Data/Pseudocode/Core.agda b/src/Helium/Data/Pseudocode/Core.agda
index 8a0c4e3..4728e44 100644
--- a/src/Helium/Data/Pseudocode/Core.agda
+++ b/src/Helium/Data/Pseudocode/Core.agda
@@ -145,7 +145,7 @@ module Code {o} (Σ : Vec Type o) where
fin : ∀ {k ms n} → (All (Fin) ms → Fin n) → Expression Γ (tuple k (map fin ms)) → Expression Γ (fin n)
asInt : ∀ {m} → Expression Γ (fin m) → Expression Γ int
tup : ∀ {m ts} → All (Expression Γ) ts → Expression Γ (tuple m ts)
- call : ∀ {t m Δ} → Function Δ t → Expression Γ (tuple m Δ) → Expression Γ t
+ call : ∀ {t m Δ} → Function Δ t → All (Expression Γ) {m} Δ → Expression Γ t
if_then_else_ : ∀ {t} → Expression Γ bool → Expression Γ t → Expression Γ t → Expression Γ t
data CanAssign {n} {Γ} where
@@ -225,7 +225,7 @@ module Code {o} (Σ : Vec Type o) where
skip : Statement Γ
_≔_ : ∀ {t} → (ref : Expression Γ t) → {canAssign : True (canAssign? ref)} → Expression Γ t → Statement Γ
declare : ∀ {t} → Expression Γ t → Statement (t ∷ Γ) → Statement Γ
- invoke : ∀ {m Δ} → Procedure Δ → Expression Γ (tuple m Δ) → Statement Γ
+ invoke : ∀ {m Δ} → Procedure Δ → All (Expression Γ) {m} Δ → Statement Γ
if_then_else_ : Expression Γ bool → Statement Γ → Statement Γ → Statement Γ
for : ∀ m → Statement (fin m ∷ Γ) → Statement Γ
diff --git a/src/Helium/Instructions/Base.agda b/src/Helium/Instructions/Base.agda
index 62a6968..c19e8ad 100644
--- a/src/Helium/Instructions/Base.agda
+++ b/src/Helium/Instructions/Base.agda
@@ -163,7 +163,7 @@ VPTAdvance = declare (fin div2 (tup (var 0 ∷ []))) (
then (
declare (lit ((false ∷ []) ′x)) (
-- 0:inv 1:vptState 2:maskId 3:beat
- tup (var 1 ∷ var 0 ∷ []) ≔ call (LSL-C 0) (tup (var 1 ∷ [])) ∙
+ tup (var 1 ∷ var 0 ∷ []) ≔ call (LSL-C 0) (var 1 ∷ []) ∙
if var 0 ≟ lit ((true ∷ []) ′x)
then
elem 4 VPR-P0 (var 3) ≔ not (elem 4 VPR-P0 (var 3))
@@ -181,7 +181,7 @@ VPTActive = skip ∙return inv (elem 4 VPR-mask (fin div2 (tup (var 0 ∷ [])))
GetCurInstrBeat : Function [] (tuple 2 (beat ∷ elmtMask ∷ []))
GetCurInstrBeat = declare (lit (Vec.replicate true ′x)) (
-- 0:elmtMask 1:beat
- if call VPTActive (tup (BeatId ∷ []))
+ if call VPTActive (BeatId ∷ [])
then
var 0 ≔ var 0 and elem 4 VPR-P0 BeatId
else skip
@@ -199,10 +199,10 @@ ExecBeats DecodeExec =
-- 0:beatId
BeatId ≔ var 0 ∙
AdvanceVPTState ≔ lit (true ′b) ∙
- invoke DecodeExec (tup []) ∙
+ invoke DecodeExec [] ∙
if AdvanceVPTState
then
- invoke VPTAdvance (tup (var 0 ∷ []))
+ invoke VPTAdvance (var 0 ∷ [])
else skip)
∙end
@@ -224,7 +224,7 @@ module _ (d : Instr.VecOp₂) where
vec-op₂′ op = declare (lit (zero ′f)) (
declare (lit (Vec.replicate false ′x)) (
-- 0:elmtMask 1:curBeat
- tup (var 1 ∷ var 0 ∷ []) ≔ call GetCurInstrBeat (tup []) ∙
+ tup (var 1 ∷ var 0 ∷ []) ≔ call GetCurInstrBeat [] ∙
declare (lit ((Vec.replicate false ′x) ′a)) (
declare (from32 size (index (index Q (lit (src₁ ′f))) (var 2))) (
-- 0:op₁ 1:result 2:elmtMask 3:curBeat
@@ -232,7 +232,7 @@ module _ (d : Instr.VecOp₂) where
-- 0:e 1:op₁ 2:result 3:elmtMask 4:curBeat
declare op₂ op ) ∙
-- 0:op₁ 1:result 2:elmtMask 3:curBeat
- invoke copyMasked (tup (lit (dest ′f) ∷ to32 size (var 1) ∷ var 3 ∷ var 2 ∷ []))))
+ invoke copyMasked (lit (dest ′f) ∷ to32 size (var 1) ∷ var 3 ∷ var 2 ∷ [])))
∙end))
where
-- 0:e 1:op₁ 2:result 3:elmtMask 4:curBeat
@@ -242,7 +242,7 @@ module _ (d : Instr.VecOp₂) where
]′ src₂
vec-op₂ : Function (bits (toℕ esize) ∷ bits (toℕ esize) ∷ []) (bits (toℕ esize)) → Procedure []
- vec-op₂ op = vec-op₂′ (index (var 3) (var 1) ≔ call op (tup (index (var 2) (var 1) ∷ var 0 ∷ [])))
+ vec-op₂ op = vec-op₂′ (index (var 3) (var 1) ≔ call op (index (var 2) (var 1) ∷ var 0 ∷ []))
vadd : Instr.VAdd → Procedure []
vadd d = vec-op₂ d (skip ∙return sliceⁱ 0 (uint (var 0) + uint (var 1)))
@@ -252,7 +252,7 @@ vsub d = vec-op₂ d (skip ∙return sliceⁱ 0 (uint (var 0) - uint (var 1)))
vhsub : Instr.VHSub → Procedure []
vhsub d = vec-op₂ op₂ (skip ∙return sliceⁱ 1 (toInt (var 0) - toInt (var 1)))
- where open Instr.VHSub d; toInt = λ i → call Int (tup (i ∷ lit (unsigned ′b) ∷ []))
+ where open Instr.VHSub d; toInt = λ i → call Int (i ∷ lit (unsigned ′b) ∷ [])
vmul : Instr.VMul → Procedure []
vmul d = vec-op₂ d (skip ∙return sliceⁱ 0 (sint (var 0) * sint (var 1)))
@@ -260,29 +260,29 @@ vmul d = vec-op₂ d (skip ∙return sliceⁱ 0 (sint (var 0) * sint (var 1)))
vmulh : Instr.VMulH → Procedure []
vmulh d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0) * toInt (var 1)))
where
- open Instr.VMulH d; toInt = λ i → call Int (tup (i ∷ lit (unsigned ′b) ∷ []))
+ open Instr.VMulH d; toInt = λ i → call Int (i ∷ lit (unsigned ′b) ∷ [])
vrmulh : Instr.VRMulH → Procedure []
vrmulh d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0) * toInt (var 1) + lit (1 ′i) << toℕ esize-1))
where
- open Instr.VRMulH d; toInt = λ i → call Int (tup (i ∷ lit (unsigned ′b) ∷ []))
+ open Instr.VRMulH d; toInt = λ i → call Int (i ∷ lit (unsigned ′b) ∷ [])
vmla : Instr.VMlA → Procedure []
vmla d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0) * element₂ + toInt (var 1)))
where
open Instr.VMlA d
op₂ = record { size = size ; dest = acc ; src₁ = src₁ ; src₂ = inj₂ acc }
- toInt = λ i → call Int (tup (i ∷ lit (unsigned ′b) ∷ []))
+ toInt = λ i → call Int (i ∷ lit (unsigned ′b) ∷ [])
element₂ = toInt (index (from32 size (index R (lit (src₂ ′f)))) (lit (zero ′f)))
private
vqr?dmulh : Instr.VQDMulH → Function (int ∷ int ∷ []) int → Procedure []
vqr?dmulh d f = vec-op₂′ d (
-- 0:op₂ 1:e 2:op₁ 3:result 4:elmtMask 5:curBeat
- declare (call f (tup (sint (index (var 2) (var 1)) ∷ sint (var 0) ∷ []))) (
+ declare (call f (sint (index (var 2) (var 1)) ∷ sint (var 0) ∷ [])) (
declare (lit (false ′b)) (
-- 0:sat 1:value 2:op₂ 3:e 4:op₁ 5:result 6:elmtMask 7:curBeat
- tup (index (var 5) (var 3) ∷ var 0 ∷ []) ≔ call (SignedSatQ (toℕ esize-1)) (tup (var 1 ∷ [])) ∙
+ tup (index (var 5) (var 3) ∷ var 0 ∷ []) ≔ call (SignedSatQ (toℕ esize-1)) (var 1 ∷ []) ∙
if var 0 && hasBit (var 6) (fin e*esize>>3 (tup ((var 3) ∷ [])))
then
FPSCR-QC ≔ lit ((true ∷ []) ′x)
diff --git a/src/Helium/Instructions/Instances/Barrett.agda b/src/Helium/Instructions/Instances/Barrett.agda
index 5ec9ba4..606a9e9 100644
--- a/src/Helium/Instructions/Instances/Barrett.agda
+++ b/src/Helium/Instructions/Instances/Barrett.agda
@@ -25,9 +25,9 @@ open import Helium.Instructions.Core
barret : (m -n : Expression [] (bits 32)) (t z : VecReg) (im : GenReg) → Procedure []
barret m -n t z im =
index R (lit (im ′f)) ≔ m ∙
- invoke vqrdmulh-s32,t,z,m (tup []) ∙
+ invoke vqrdmulh-s32,t,z,m [] ∙
index R (lit (im ′f)) ≔ -n ∙
- invoke vmla-s32,z,t,-n (tup []) ∙end
+ invoke vmla-s32,z,t,-n [] ∙end
where
vqrdmulh-s32,t,z,m =
ExecBeats (vqrdmulh (record
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
index 25f0448..d4060f5 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -152,6 +152,7 @@ module Expression
⟦_⟧ˢ : ∀ {n} {Γ : Vec Type n} → Statement Γ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′
⟦_⟧ᶠ : ∀ {n} {Γ : Vec Type n} {ret} → Function Γ ret → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ ret ⟧ₜ
⟦_⟧ᵖ : ∀ {n} {Γ : Vec Type n} → Procedure Γ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′
+ ⟦_⟧ᵉ′ : ∀ {n} {Γ : Vec Type n} {m ts} → All (Expression Γ) ts → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ tuple m ts ⟧ₜ
update : ∀ {n Γ t e} → CanAssign {n} {Γ} {t} e → ⟦ t ⟧ₜ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′
⟦ lit x ⟧ᵉ σ γ = 𝒦 x
@@ -188,14 +189,18 @@ module Expression
⟦ tup [] ⟧ᵉ σ γ = _
⟦ tup (e ∷ []) ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ
⟦ tup (e ∷ e′ ∷ es) ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ , ⟦ tup (e′ ∷ es) ⟧ᵉ σ γ
- ⟦ call f e ⟧ᵉ σ γ = ⟦ f ⟧ᶠ σ (⟦ e ⟧ᵉ σ γ)
+ ⟦ call f e ⟧ᵉ σ γ = ⟦ f ⟧ᶠ σ (⟦ e ⟧ᵉ′ σ γ)
⟦ if e then e₁ else e₂ ⟧ᵉ σ γ = Bool.if ⟦ e ⟧ᵉ σ γ then ⟦ e₁ ⟧ᵉ σ γ else ⟦ e₂ ⟧ᵉ σ γ
+ ⟦ [] ⟧ᵉ′ σ γ = _
+ ⟦ e ∷ [] ⟧ᵉ′ σ γ = ⟦ e ⟧ᵉ σ γ
+ ⟦ e ∷ e′ ∷ es ⟧ᵉ′ σ γ = ⟦ e ⟧ᵉ σ γ , ⟦ e′ ∷ es ⟧ᵉ′ σ γ
+
⟦ s ∙ s₁ ⟧ˢ σ γ = P.uncurry ⟦ s ⟧ˢ (⟦ s ⟧ˢ σ γ)
⟦ skip ⟧ˢ σ γ = σ , γ
⟦ _≔_ ref {canAssign = canAssign} e ⟧ˢ σ γ = update (toWitness canAssign) (⟦ e ⟧ᵉ σ γ) σ γ
⟦_⟧ˢ {Γ = Γ} (declare e s) σ γ = P.map₂ (tupTail Γ) (⟦ s ⟧ˢ σ (tupCons Γ (⟦ e ⟧ᵉ σ γ) γ))
- ⟦ invoke p e ⟧ˢ σ γ = ⟦ p ⟧ᵖ σ (⟦ e ⟧ᵉ σ γ) , γ
+ ⟦ invoke p e ⟧ˢ σ γ = ⟦ p ⟧ᵖ σ (⟦ e ⟧ᵉ′ σ γ) , γ
⟦ if e then s₁ else s₂ ⟧ˢ σ γ = Bool.if ⟦ e ⟧ᵉ σ γ then ⟦ s₁ ⟧ˢ σ γ else ⟦ s₂ ⟧ˢ σ γ
⟦_⟧ˢ {Γ = Γ} (for m s) σ γ = helper m ⟦ s ⟧ˢ σ γ
where
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 12:50:03 +0000