From 12c389057d20ad58b77c6d2a6bf955f9500446c6 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Mon, 20 Dec 2021 19:01:00 +0000 Subject: Define vsub. --- src/Helium/Instructions.agda | 2 ++ src/Helium/Semantics/Denotational.agda | 3 +++ 2 files changed, 5 insertions(+) (limited to 'src') diff --git a/src/Helium/Instructions.agda b/src/Helium/Instructions.agda index 256f9c4..1fa2829 100644 --- a/src/Helium/Instructions.agda +++ b/src/Helium/Instructions.agda @@ -41,6 +41,8 @@ record VecOp₂ : Set where VAdd = VecOp₂ +VSub = VecOp₂ + record VHSub : Set where field op₂ : VecOp₂ 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 -- cgit v1.2.3