summaryrefslogtreecommitdiff
path: root/src/Helium/Instructions/Base.agda
diff options
context:
space:
mode:
Diffstat (limited to 'src/Helium/Instructions/Base.agda')
-rw-r--r--src/Helium/Instructions/Base.agda145
1 files changed, 69 insertions, 76 deletions
diff --git a/src/Helium/Instructions/Base.agda b/src/Helium/Instructions/Base.agda
index 62a6968..d157d5a 100644
--- a/src/Helium/Instructions/Base.agda
+++ b/src/Helium/Instructions/Base.agda
@@ -10,6 +10,7 @@ module Helium.Instructions.Base where
open import Data.Bool as Bool using (true; false)
open import Data.Fin as Fin using (Fin; Fin′; zero; suc; toℕ)
+open import Data.Fin.Patterns
open import Data.Nat as ℕ using (ℕ; zero; suc)
import Data.Nat.Properties as ℕₚ
open import Data.Sum using ([_,_]′; inj₂)
@@ -49,25 +50,25 @@ open Core.Code State public
-- Direct from State
S : ∀ {n Γ} → Expression {n} Γ (array (bits 32) 32)
-S = state 0
+S = state 0F
R : ∀ {n Γ} → Expression {n} Γ (array (bits 32) 16)
-R = state 1
+R = state 1F
VPR-P0 : ∀ {n Γ} → Expression {n} Γ (bits 16)
-VPR-P0 = state 2
+VPR-P0 = state 2F
VPR-mask : ∀ {n Γ} → Expression {n} Γ (bits 8)
-VPR-mask = state 3
+VPR-mask = state 3F
FPSCR-QC : ∀ {n Γ} → Expression {n} Γ bit
-FPSCR-QC = state 4
+FPSCR-QC = state 4F
AdvanceVPTState : ∀ {n Γ} → Expression {n} Γ bool
-AdvanceVPTState = state 5
+AdvanceVPTState = state 5F
BeatId : ∀ {n Γ} → Expression {n} Γ beat
-BeatId = state 6
+BeatId = state 6F
-- Indirect
@@ -84,8 +85,7 @@ join {k = k} {suc m} x = cast eq (join (slice x (lit (Fin.fromℕ 1 ′f))) ∶
eq = P.trans (P.cong (k ℕ.+_) (ℕₚ.*-comm k (suc m))) (ℕₚ.*-comm (suc (suc m)) k)
index : ∀ {n Γ t m} → Expression {n} Γ (asType t (suc m)) → Expression Γ (fin (suc m)) → Expression Γ (elemType t)
-index {t = bits} {m} x i = slice (cast (ℕₚ.+-comm 1 m) x) i
-index {t = array _} {m} x i = unbox (slice (cast (ℕₚ.+-comm 1 m) x) i)
+index {m = m} x i = unbox (slice (cast (ℕₚ.+-comm 1 m) x) i)
Q : ∀ {n Γ} → Expression {n} Γ (array (array (bits 32) 4) 8)
Q = group 7 S
@@ -98,39 +98,39 @@ elem {k = suc k} (suc m) x i = index (group k (cast (ℕₚ.*-comm (suc k) (suc
--- Other utiliies
hasBit : ∀ {n Γ m} → Expression {n} Γ (bits (suc m)) → Expression Γ (fin (suc m)) → Expression Γ bool
-hasBit {n} x i = index x i ≟ lit ((true ∷ []) ′x)
+hasBit {n} x i = index x i ≟ lit (true ′x)
sliceⁱ : ∀ {n Γ m} → ℕ → Expression {n} Γ int → Expression Γ (bits m)
-sliceⁱ {m = zero} n i = lit ([] ′x)
-sliceⁱ {m = suc m} n i = sliceⁱ (suc n) i ∶ get n i
+sliceⁱ {m = zero} n i = lit ([] ′xs)
+sliceⁱ {m = suc m} n i = sliceⁱ (suc n) i ∶ [ get n i ]
--- Functions
Int : ∀ {n} → Function (bits n ∷ bool ∷ []) int
-Int = skip ∙return (if var 1 then uint (var 0) else sint (var 0))
+Int = skip ∙return (if var 1F then uint (var 0F) else sint (var 0F))
-- arguments swapped, pred n
SignedSatQ : ∀ n → Function (int ∷ []) (tuple 2 (bits (suc n) ∷ bool ∷ []))
SignedSatQ n = declare (lit (true ′b)) (
- if max <? var 1
+ if max <? var 1F
then
- var 1 ≔ max
- else if var 1 <? min
+ var 1F ≔ max
+ else if var 1F <? min
then
- var 1 ≔ min
+ var 1F ≔ min
else
- var 0 ≔ lit (false ′b)
- ∙return tup (sliceⁱ 0 (var 1) ∷ var 0 ∷ []))
+ var 0F ≔ lit (false ′b)
+ ∙return tup (sliceⁱ 0 (var 1F) ∷ var 0F ∷ []))
where
max = lit (2 ′i) ^ n + - lit (1 ′i)
min = - (lit (2 ′i) ^ n)
-- actual shift if 'shift + 1'
LSL-C : ∀ {n} (shift : ℕ) → Function (bits n ∷ []) (tuple 2 (bits n ∷ bit ∷ []))
-LSL-C {n} shift = declare (var 0 ∶ lit ((Vec.replicate {n = (suc shift)} false) ′x))
+LSL-C {n} shift = declare (var 0F ∶ lit ((Vec.replicate {n = (suc shift)} false) ′xs))
(skip ∙return tup
- ( slice (var 0) (lit (zero ′f))
- ∷ slice (cast eq (var 0)) (lit (Fin.inject+ shift (Fin.fromℕ n) ′f))
+ ( slice (var 0F) (lit (zero ′f))
+ ∷ unbox (slice (cast eq (var 0F)) (lit (Fin.inject+ shift (Fin.fromℕ n) ′f)))
∷ []))
where
eq = P.trans (ℕₚ.+-comm 1 (shift ℕ.+ n)) (P.cong (ℕ._+ 1) (ℕₚ.+-comm shift n))
@@ -146,46 +146,41 @@ private
copyMasked : Procedure (fin 8 ∷ bits 32 ∷ beat ∷ elmtMask ∷ [])
copyMasked = for 4
-- 0:e 1:dest 2:result 3:beat 4:elmtMask
- ( if hasBit (var 4) (var 0)
+ ( if hasBit (var 4F) (var 0F)
then
- elem 8 (index (index Q (var 1)) (var 3)) (var 0) ≔ elem 8 (var 2) (var 0)
- else skip
+ elem 8 (index (index Q (var 1F)) (var 3F)) (var 0F) ≔ elem 8 (var 2F) (var 0F)
) ∙end
VPTAdvance : Procedure (beat ∷ [])
-VPTAdvance = declare (fin div2 (tup (var 0 ∷ []))) (
- declare (elem 4 VPR-mask (var 0)) (
+VPTAdvance = declare (fin div2 (tup (var 0F ∷ []))) (
+ declare (elem 4 VPR-mask (var 0F)) (
-- 0:vptState 1:maskId 2:beat
- if var 0 ≟ lit ((true ∷ false ∷ false ∷ false ∷ []) ′x)
+ if var 0F ≟ lit ((true ∷ false ∷ false ∷ false ∷ []) ′xs)
then
- var 0 ≔ lit (Vec.replicate false ′x)
- else if inv (var 0 ≟ lit (Vec.replicate false ′x))
+ var 0F ≔ lit (Vec.replicate false ′xs)
+ else if inv (var 0F ≟ lit (Vec.replicate false ′xs))
then (
- declare (lit ((false ∷ []) ′x)) (
+ declare (lit (false ′x)) (
-- 0:inv 1:vptState 2:maskId 3:beat
- tup (var 1 ∷ var 0 ∷ []) ≔ call (LSL-C 0) (tup (var 1 ∷ [])) ∙
- if var 0 ≟ lit ((true ∷ []) ′x)
+ tup (var 1F ∷ var 0F ∷ []) ≔ call (LSL-C 0) (var 1F ∷ []) ∙
+ if var 0F ≟ lit (true ′x)
then
- elem 4 VPR-P0 (var 3) ≔ not (elem 4 VPR-P0 (var 3))
- else skip))
- else skip ∙
- if get 0 (asInt (var 2)) ≟ lit ((true ∷ []) ′x)
+ elem 4 VPR-P0 (var 3F) ≔ not (elem 4 VPR-P0 (var 3F)))) ∙
+ if get 0 (asInt (var 2F)) ≟ lit (true ′x)
then
- elem 4 VPR-mask (var 1) ≔ var 0
- else skip
- ∙end))
+ elem 4 VPR-mask (var 1F) ≔ var 0F))
+ ∙end
VPTActive : Function (beat ∷ []) bool
-VPTActive = skip ∙return inv (elem 4 VPR-mask (fin div2 (tup (var 0 ∷ []))) ≟ lit (Vec.replicate false ′x))
+VPTActive = skip ∙return inv (elem 4 VPR-mask (fin div2 (tup (var 0F ∷ []))) ≟ lit (Vec.replicate false ′xs))
GetCurInstrBeat : Function [] (tuple 2 (beat ∷ elmtMask ∷ []))
-GetCurInstrBeat = declare (lit (Vec.replicate true ′x)) (
+GetCurInstrBeat = declare (lit (Vec.replicate true ′xs)) (
-- 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
- ∙return tup (BeatId ∷ var 0 ∷ []))
+ var 0F ≔ var 0F and elem 4 VPR-P0 BeatId
+ ∙return tup (BeatId ∷ var 0F ∷ []))
-- Assumes:
-- MAX_OVERLAPPING_INSTRS = 1
@@ -197,13 +192,12 @@ ExecBeats : Procedure [] → Procedure []
ExecBeats DecodeExec =
for 4 (
-- 0:beatId
- BeatId ≔ var 0 ∙
+ BeatId ≔ var 0F ∙
AdvanceVPTState ≔ lit (true ′b) ∙
- invoke DecodeExec (tup []) ∙
+ invoke DecodeExec [] ∙
if AdvanceVPTState
then
- invoke VPTAdvance (tup (var 0 ∷ []))
- else skip)
+ invoke VPTAdvance (var 0F ∷ []))
∙end
from32 : ∀ size {n Γ} → Expression {n} Γ (bits 32) → Expression Γ (array (bits (toℕ (Instr.Size.esize size))) (toℕ (Instr.Size.elements size)))
@@ -222,71 +216,70 @@ module _ (d : Instr.VecOp₂) where
-- 0:op₂ 1:e 2:op₁ 3:result 4:elmtMask 5:curBeat
vec-op₂′ : Statement (bits (toℕ esize) ∷ fin (toℕ elements) ∷ array (bits (toℕ esize)) (toℕ elements) ∷ array (bits (toℕ esize)) (toℕ elements) ∷ elmtMask ∷ beat ∷ []) → Procedure []
vec-op₂′ op = declare (lit (zero ′f)) (
- declare (lit (Vec.replicate false ′x)) (
+ declare (lit (Vec.replicate false ′xs)) (
-- 0:elmtMask 1:curBeat
- tup (var 1 ∷ var 0 ∷ []) ≔ call GetCurInstrBeat (tup []) ∙
- declare (lit ((Vec.replicate false ′x) ′a)) (
- declare (from32 size (index (index Q (lit (src₁ ′f))) (var 2))) (
+ tup (var 1F ∷ var 0F ∷ []) ≔ call GetCurInstrBeat [] ∙
+ declare (lit ((Vec.replicate false ′xs) ′a)) (
+ declare (from32 size (index (index Q (lit (src₁ ′f))) (var 2F))) (
-- 0:op₁ 1:result 2:elmtMask 3:curBeat
for (toℕ elements) (
-- 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 ∷ []))))
- ∙end))
+ invoke copyMasked (lit (dest ′f) ∷ to32 size (var 1F) ∷ var 3F ∷ var 2F ∷ [])))))
+ ∙end
where
-- 0:e 1:op₁ 2:result 3:elmtMask 4:curBeat
op₂ =
[ (λ src₂ → index (from32 size (index R (lit (src₂ ′f)))) (lit (zero ′f)))
- , (λ src₂ → index (from32 size (index (index Q (lit (src₂ ′f))) (var 4))) (var 0))
+ , (λ src₂ → index (from32 size (index (index Q (lit (src₂ ′f))) (var 4F))) (var 0F))
]′ 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 3F) (var 1F) ≔ call op (index (var 2F) (var 1F) ∷ var 0F ∷ []))
vadd : Instr.VAdd → Procedure []
-vadd d = vec-op₂ d (skip ∙return sliceⁱ 0 (uint (var 0) + uint (var 1)))
+vadd d = vec-op₂ d (skip ∙return sliceⁱ 0 (uint (var 0F) + uint (var 1F)))
vsub : Instr.VSub → Procedure []
-vsub d = vec-op₂ d (skip ∙return sliceⁱ 0 (uint (var 0) - uint (var 1)))
+vsub d = vec-op₂ d (skip ∙return sliceⁱ 0 (uint (var 0F) - uint (var 1F)))
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) ∷ []))
+vhsub d = vec-op₂ op₂ (skip ∙return sliceⁱ 1 (toInt (var 0F) - toInt (var 1F)))
+ 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)))
+vmul d = vec-op₂ d (skip ∙return sliceⁱ 0 (sint (var 0F) * sint (var 1F)))
vmulh : Instr.VMulH → Procedure []
-vmulh d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0) * toInt (var 1)))
+vmulh d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0F) * toInt (var 1F)))
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))
+vrmulh d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0F) * toInt (var 1F) + 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)))
+vmla d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0F) * element₂ + toInt (var 1F)))
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 2F) (var 1F)) ∷ sint (var 0F) ∷ [])) (
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 ∷ [])) ∙
- if var 0 && hasBit (var 6) (fin e*esize>>3 (tup ((var 3) ∷ [])))
+ tup (index (var 5F) (var 3F) ∷ var 0F ∷ []) ≔ call (SignedSatQ (toℕ esize-1)) (var 1F ∷ []) ∙
+ if var 0F && hasBit (var 6F) (fin e*esize>>3 (tup ((var 3F) ∷ [])))
then
- FPSCR-QC ≔ lit ((true ∷ []) ′x)
- else skip)))
+ FPSCR-QC ≔ lit (true ′x))))
where
open Instr.VecOp₂ d
@@ -299,9 +292,9 @@ private
helper Instr.32bit i = Fin.combine i zero
vqdmulh : Instr.VQDMulH → Procedure []
-vqdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0 * var 1 >> toℕ esize)
+vqdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0F * var 1F >> toℕ esize)
where open Instr.VecOp₂ d using (esize)
vqrdmulh : Instr.VQRDMulH → Procedure []
-vqrdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0 * var 1 + lit (1 ′i) << toℕ esize-1 >> toℕ esize)
+vqrdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0F * var 1F + lit (1 ′i) << toℕ esize-1 >> toℕ esize)
where open Instr.VecOp₂ d using (esize; esize-1)
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 07:35:20 +0000