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.

1 files changed, 2 insertions, 2 deletions

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