From 535e4297a08c626d0e2e1923914727f914b8c9bd Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sat, 19 Mar 2022 13:28:42 +0000 Subject: Modify pseudocode definition. This change makes the following changes to the definition of pseudocode: - Add a separate type `bit` for single-bit values. - Change `var` and `state` to take `Fin`s instead of bounded naturals. - Make `[_]` and `unbox` work for any sliced type. - Generalise `_:_` and `slice` into `splice` and `cut` respectively, making the two new operations inverses. - Replace `tup` with `nil` and `cons` for building tuples. - Add destructors `head` and `tail` for tuple types. - Make function and procedure calls take a vector of arguments instead of a tuple. - Introduce an `if_then_` expression for if statements with a trivial else branch. --- src/Helium/Instructions/Instances/Barrett.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Helium/Instructions/Instances/Barrett.agda') diff --git a/src/Helium/Instructions/Instances/Barrett.agda b/src/Helium/Instructions/Instances/Barrett.agda index 5ec9ba4..606a9e9 100644 --- a/src/Helium/Instructions/Instances/Barrett.agda +++ b/src/Helium/Instructions/Instances/Barrett.agda @@ -25,9 +25,9 @@ open import Helium.Instructions.Core barret : (m -n : Expression [] (bits 32)) (t z : VecReg) (im : GenReg) → Procedure [] barret m -n t z im = index R (lit (im ′f)) ≔ m ∙ - invoke vqrdmulh-s32,t,z,m (tup []) ∙ + invoke vqrdmulh-s32,t,z,m [] ∙ index R (lit (im ′f)) ≔ -n ∙ - invoke vmla-s32,z,t,-n (tup []) ∙end + invoke vmla-s32,z,t,-n [] ∙end where vqrdmulh-s32,t,z,m = ExecBeats (vqrdmulh (record -- cgit v1.2.3