diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2021-12-21 11:37:20 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2021-12-21 11:37:20 +0000 |
| commit | ef9f0202c1acae915f02ee2b39ab92981f800297 (patch) | |
| tree | 63084bde178d4cb0f35954fe1bd61e9aee0d1f63 /src/Helium/Semantics/Denotational.agda | |
| parent | 12c389057d20ad58b77c6d2a6bf955f9500446c6 (diff) | |
Define semantics for vmulh.
Diffstat (limited to 'src/Helium/Semantics/Denotational.agda')
| -rw-r--r-- | src/Helium/Semantics/Denotational.agda | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda index 93c784c..2cf1607 100644 --- a/src/Helium/Semantics/Denotational.agda +++ b/src/Helium/Semantics/Denotational.agda @@ -161,3 +161,15 @@ module _ vmul : VMul → Procedure 2 (Beat , ElmtMask , _) vmul d = vec-op₂ d (λ x y → sliceᶻ _ zero (sint x *ᶻ sint y)) + + vmulh : VMulH → Procedure 2 (Beat , ElmtMask , _) + vmulh d = vec-op₂ op₂ (λ x y → cast (eq _ esize) (sliceᶻ 2esize esize′ (int x *ᶻ int y +ᶻ rval))) + where + open VMulH d + int = Bool.if unsigned then uint else sint + rval = Bool.if rounding then 1ℤ << toℕ esize-1 else 0ℤ + 2esize = toℕ esize + toℕ esize + esize′ = inject+ _ (strengthen esize) + eq : ∀ {n} m (i : Fin n) → toℕ i + m ℕ-ℕ inject+ m (strengthen i) ≡ m + eq m zero = refl + eq m (suc i) = eq m i |