diff options
author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2021-12-20 19:01:00 +0000 |
---|---|---|
committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2021-12-20 19:01:00 +0000 |
commit | 12c389057d20ad58b77c6d2a6bf955f9500446c6 (patch) | |
tree | 33933a7f564389d961f47b0a7d2d5397fcb4c9e9 /src/Helium/Semantics | |
parent | 22b2a854fa02fd8c79a1351066922c0ba2e0cf42 (diff) |
Define vsub.
Diffstat (limited to 'src/Helium/Semantics')
-rw-r--r-- | src/Helium/Semantics/Denotational.agda | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda index c2a4d6e..93c784c 100644 --- a/src/Helium/Semantics/Denotational.agda +++ b/src/Helium/Semantics/Denotational.agda @@ -152,6 +152,9 @@ module _ vadd : VAdd → Procedure 2 (Beat , ElmtMask , _) vadd d = vec-op₂ d (λ x y → sliceᶻ _ zero (uint x +ᶻ uint y)) + vsub : VSub → Procedure 2 (Beat , ElmtMask , _) + vsub 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 zero) (int x +ᶻ -ᶻ int y)) where open VHSub d ; int = Bool.if unsigned then uint else sint |