diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2021-12-20 18:58:23 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2021-12-20 18:58:23 +0000 |
| commit | 22b2a854fa02fd8c79a1351066922c0ba2e0cf42 (patch) | |
| tree | 97b925ae6c6a0fc98b322f70a42e1914faa9fdcb /src/Helium/Semantics | |
| parent | f81f771877b77ca1c6a6278d21153fa1c3df8d83 (diff) | |
Remove bitstring addition.
Diffstat (limited to 'src/Helium/Semantics')
| -rw-r--r-- | src/Helium/Semantics/Denotational.agda | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda index 0739d28..c2a4d6e 100644 --- a/src/Helium/Semantics/Denotational.agda +++ b/src/Helium/Semantics/Denotational.agda @@ -150,11 +150,11 @@ module _ open sliceᶻ ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round 2^n≢0 *ᶻ-identityʳ vadd : VAdd → Procedure 2 (Beat , ElmtMask , _) - vadd d = vec-op₂ d _+ᵇ_ + vadd d = vec-op₂ d (λ x y → sliceᶻ _ zero (uint x +ᶻ uint y)) vhsub : VHSub → Procedure 2 (Beat , ElmtMask , _) - vhsub d = vec-op₂ op₂ (λ x y → sliceᶻ (suc (toℕ esize)) (suc zero) (int x +ᶻ -ᶻ int y)) + vhsub d = vec-op₂ op₂ (λ x y → sliceᶻ _ (suc zero) (int x +ᶻ -ᶻ int y)) where open VHSub d ; int = Bool.if unsigned then uint else sint vmul : VMul → Procedure 2 (Beat , ElmtMask , _) - vmul d = vec-op₂ d (λ x y → sliceᶻ (toℕ _) zero (sint x *ᶻ sint y)) + vmul d = vec-op₂ d (λ x y → sliceᶻ _ zero (sint x *ᶻ sint y)) |