From 00a0ce9082b4cc1389815defcc806efd4a9b80f4 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Mon, 18 Apr 2022 15:05:24 +0100 Subject: Do a big refactor. - Replace the decidable predicates on expressions and statements with separate data types. - Reorganise the Hoare logic semantics to remove unnecessary definitions. - Make liberal use of modules to group related definitions together. - Unify the types for denotational and Hoare logic semantics. - Make bits an abstraction of array types. --- src/Helium/Instructions/Instances/Barrett.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 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 606a9e9..b913972 100644 --- a/src/Helium/Instructions/Instances/Barrett.agda +++ b/src/Helium/Instructions/Instances/Barrett.agda @@ -22,11 +22,11 @@ open import Helium.Instructions.Core -- | z | < 2 ^ 31 -- Computes: -- z mod n -barret : (m -n : Expression [] (bits 32)) (t z : VecReg) (im : GenReg) → Procedure [] +barret : (m -n : Expression State [] (bits 32)) (t z : VecReg) (im : GenReg) → Procedure State [] barret m -n t z im = - index R (lit (im ′f)) ≔ m ∙ + *index R (lit im) ≔ m ∙ invoke vqrdmulh-s32,t,z,m [] ∙ - index R (lit (im ′f)) ≔ -n ∙ + *index R (lit im) ≔ -n ∙ invoke vmla-s32,z,t,-n [] ∙end where vqrdmulh-s32,t,z,m = -- cgit v1.2.3