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.

5 files changed, 319 insertions, 249 deletions

diff --git a/src/Helium/Data/Pseudocode/Core.agda b/src/Helium/Data/Pseudocode/Core.agda
index 8a0c4e3..079e2ce 100644
--- a/src/Helium/Data/Pseudocode/Core.agda
+++ b/src/Helium/Data/Pseudocode/Core.agda
@@ -9,7 +9,8 @@
 module Helium.Data.Pseudocode.Core where
 
 open import Data.Bool using (Bool; true; false)
-open import Data.Fin using (Fin; #_)
+open import Data.Fin as Fin using (Fin)
+open import Data.Fin.Patterns
 open import Data.Nat as ℕ using (ℕ; zero; suc)
 open import Data.Nat.Properties using (+-comm)
 open import Data.Product using (∃; _,_; proj₂; uncurry)
@@ -19,7 +20,7 @@ open import Data.Vec.Relation.Unary.All using (All; []; _∷_; reduce)
 open import Data.Vec.Relation.Unary.Any using (Any; here; there)
 open import Function as F using (_∘_; _∘′_; _∋_)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary using (Dec; yes; no)
 open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromWitness; map′)
 open import Relation.Nullary.Product using (_×-dec_)
 open import Relation.Nullary.Sum using (_⊎-dec_)
@@ -31,18 +32,17 @@ data Type : Set where
   int   : Type
   fin   : (n : ℕ) → Type
   real  : Type
+  bit   : Type
   bits  : (n : ℕ) → Type
   tuple : ∀ n → Vec Type n → Type
   array : Type → (n : ℕ) → Type
 
-bit : Type
-bit = bits 1
-
 data HasEquality : Type → Set where
   bool : HasEquality bool
   int  : HasEquality int
   fin  : ∀ {n} → HasEquality (fin n)
   real : HasEquality real
+  bit  : HasEquality bit
   bits : ∀ {n} → HasEquality (bits n)
 
 hasEquality? : Decidable HasEquality
@@ -50,6 +50,7 @@ hasEquality? bool        = yes bool
 hasEquality? int         = yes int
 hasEquality? (fin n)     = yes fin
 hasEquality? real        = yes real
+hasEquality? bit         = yes bit
 hasEquality? (bits n)    = yes bits
 hasEquality? (tuple n x) = no (λ ())
 hasEquality? (array t n) = no (λ ())
@@ -61,16 +62,17 @@ data IsNumeric : Type → Set where
 isNumeric? : Decidable IsNumeric
 isNumeric? bool        = no (λ ())
 isNumeric? int         = yes int
-isNumeric? real        = yes real
 isNumeric? (fin n)     = no (λ ())
+isNumeric? real        = yes real
+isNumeric? bit         = no (λ ())
 isNumeric? (bits n)    = no (λ ())
 isNumeric? (tuple n x) = no (λ ())
 isNumeric? (array t n) = no (λ ())
 
-combineNumeric : ∀ t₁ t₂ → {isNumeric₁ : True (isNumeric? t₁)} → {isNumeric₂ : True (isNumeric? t₂)} → Type
-combineNumeric int  int  = int
-combineNumeric int  real = real
-combineNumeric real _    = real
+combineNumeric : ∀ t₁ t₂ → (isNumeric₁ : True (isNumeric? t₁)) → (isNumeric₂ : True (isNumeric? t₂)) → Type
+combineNumeric int  int  _ _ = int
+combineNumeric int  real _ _ = real
+combineNumeric real _    _ _ = real
 
 data Sliced : Set where
   bits  : Sliced
@@ -87,12 +89,13 @@ elemType (array t) = t
 --- Literals
 
 data Literal : Type → Set where
-  _′b : Bool → Literal bool
-  _′i : ℕ → Literal int
-  _′f : ∀ {n} → Fin n → Literal (fin n)
-  _′r : ℕ → Literal real
-  _′x : ∀ {n} → Vec Bool n → Literal (bits n)
-  _′a : ∀ {n t} → Literal t → Literal (array t n)
+  _′b  : Bool → Literal bool
+  _′i  : ℕ → Literal int
+  _′f  : ∀ {n} → Fin n → Literal (fin n)
+  _′r  : ℕ → Literal real
+  _′x  : Bool → Literal bit
+  _′xs : ∀ {n} → Vec Bool n → Literal (bits n)
+  _′a  : ∀ {n t} → Literal t → Literal (array t n)
 
 --- Expressions, references, statements, functions and procedures
 
@@ -100,10 +103,8 @@ module Code {o} (Σ : Vec Type o) where
   data Expression {n} (Γ : Vec Type n) : Type → Set
   data CanAssign {n Γ} : ∀ {t} → Expression {n} Γ t → Set
   canAssign? : ∀ {n Γ t} → Decidable (CanAssign {n} {Γ} {t})
-  canAssignAll? : ∀ {n Γ m ts} → Decidable {A = All (Expression {n} Γ) {m} ts} (All (CanAssign ∘ proj₂) ∘ (reduce (λ {x} e → x , e)))
-  data AssignsState {n Γ} : ∀ {t e} → CanAssign {n} {Γ} {t} e → Set
-  assignsState? : ∀ {n Γ t e} → Decidable (AssignsState {n} {Γ} {t} {e})
-  assignsStateAny? : ∀ {n Γ m ts es} → Decidable {A = All (CanAssign ∘ proj₂) (reduce {P = Expression {n} Γ} (λ {x} e → x , e) {m} {ts} es)} (Any (AssignsState ∘ proj₂) ∘ reduce (λ {x} a → x , a))
+  data ReferencesState {n Γ} : ∀ {t} → Expression {n} Γ t → Set
+  referencesState? : ∀ {n Γ t} → Decidable (ReferencesState {n} {Γ} {t})
   data Statement {n} (Γ : Vec Type n) : Set
   data ChangesState {n Γ} : Statement {n} Γ → Set
   changesState? : ∀ {n Γ} → Decidable (ChangesState {n} {Γ})
@@ -114,55 +115,61 @@ module Code {o} (Σ : Vec Type o) where
   infixr 7 _^_
   infixl 6 _*_ _and_ _>>_
   -- infixl 6 _/_
-  infixl 5 _+_ _or_ _&&_ _||_ _∶_
+  infixl 5 _+_ _or_ _&&_ _||_
   infix  4 _≟_ _<?_
 
   data Expression {n} Γ where
-    lit   : ∀ {t} → Literal t → Expression Γ t
-    state : ∀ i {i<o : True (i ℕ.<? o)} → Expression Γ (lookup Σ (#_ i {m<n = i<o}))
-    var   : ∀ i {i<n : True (i ℕ.<? n)} → Expression Γ (lookup Γ (#_ i {m<n = i<n}))
-    abort : ∀ {t} → Expression Γ (fin 0) → Expression Γ t
-    _≟_   : ∀ {t} {hasEquality : True (hasEquality? t)} → Expression Γ t → Expression Γ t → Expression Γ bool
-    _<?_  : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → Expression Γ t → Expression Γ bool
-    inv   : Expression Γ bool → Expression Γ bool
-    _&&_  : Expression Γ bool → Expression Γ bool → Expression Γ bool
-    _||_  : Expression Γ bool → Expression Γ bool → Expression Γ bool
-    not   : ∀ {m} → Expression Γ (bits m) → Expression Γ (bits m)
-    _and_ : ∀ {m} → Expression Γ (bits m) → Expression Γ (bits m) → Expression Γ (bits m)
-    _or_  : ∀ {m} → Expression Γ (bits m) → Expression Γ (bits m) → Expression Γ (bits m)
-    [_]   : ∀ {t} → Expression Γ t → Expression Γ (array t 1)
-    unbox : ∀ {t} → Expression Γ (array t 1) → Expression Γ t
-    _∶_   : ∀ {m n t} → Expression Γ (asType t m) → Expression Γ (asType t n) → Expression Γ (asType t (n ℕ.+ m))
-    slice : ∀ {i j t} → Expression Γ (asType t (i ℕ.+ j)) → Expression Γ (fin (suc i)) → Expression Γ (asType t j)
-    cast  : ∀ {i j t} → .(eq : i ≡ j) → Expression Γ (asType t i) → Expression Γ (asType t j)
-    -_    : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → Expression Γ t
-    _+_   : ∀ {t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ {isNumeric₁} {isNumeric₂})
-    _*_   : ∀ {t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ {isNumeric₁} {isNumeric₂})
+    lit    : ∀ {t} → Literal t → Expression Γ t
+    state  : ∀ i → Expression Γ (lookup Σ i)
+    var    : ∀ i → Expression Γ (lookup Γ i)
+    abort  : ∀ {t} → Expression Γ (fin 0) → Expression Γ t
+    _≟_    : ∀ {t} {hasEquality : True (hasEquality? t)} → Expression Γ t → Expression Γ t → Expression Γ bool
+    _<?_   : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → Expression Γ t → Expression Γ bool
+    inv    : Expression Γ bool → Expression Γ bool
+    _&&_   : Expression Γ bool → Expression Γ bool → Expression Γ bool
+    _||_   : Expression Γ bool → Expression Γ bool → Expression Γ bool
+    not    : ∀ {m} → Expression Γ (bits m) → Expression Γ (bits m)
+    _and_  : ∀ {m} → Expression Γ (bits m) → Expression Γ (bits m) → Expression Γ (bits m)
+    _or_   : ∀ {m} → Expression Γ (bits m) → Expression Γ (bits m) → Expression Γ (bits m)
+    [_]    : ∀ {t} → Expression Γ (elemType t) → Expression Γ (asType t 1)
+    unbox  : ∀ {t} → Expression Γ (asType t 1) → Expression Γ (elemType t)
+    splice : ∀ {m n t} → Expression Γ (asType t m) → Expression Γ (asType t n) → Expression Γ (fin (suc n)) → Expression Γ (asType t (n ℕ.+ m))
+    cut    : ∀ {m n t} → Expression Γ (asType t (n ℕ.+ m)) → Expression Γ (fin (suc n)) → Expression Γ (tuple 2 (asType t m ∷ asType t n ∷ []))
+    cast   : ∀ {i j t} → .(eq : i ≡ j) → Expression Γ (asType t i) → Expression Γ (asType t j)
+    -_     : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → Expression Γ t
+    _+_    : ∀ {t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ isNumeric₁ isNumeric₂)
+    _*_    : ∀ {t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ isNumeric₁ isNumeric₂)
     -- _/_   : Expression Γ real → Expression Γ real → Expression Γ real
-    _^_   : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → ℕ → Expression Γ t
-    _>>_  : Expression Γ int → ℕ → Expression Γ int
-    rnd   : Expression Γ real → Expression Γ int
-    fin   : ∀ {k ms n} → (All (Fin) ms → Fin n) → Expression Γ (tuple k (map fin ms)) → Expression Γ (fin n)
-    asInt : ∀ {m} → Expression Γ (fin m) → Expression Γ int
-    tup   : ∀ {m ts} → All (Expression Γ) ts → Expression Γ (tuple m ts)
-    call  : ∀ {t m Δ} → Function Δ t → Expression Γ (tuple m Δ) → Expression Γ t
+    _^_    : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → ℕ → Expression Γ t
+    _>>_   : Expression Γ int → ℕ → Expression Γ int
+    rnd    : Expression Γ real → Expression Γ int
+    fin    : ∀ {k ms n} → (All (Fin) ms → Fin n) → Expression Γ (tuple k (map fin ms)) → Expression Γ (fin n)
+    asInt  : ∀ {m} → Expression Γ (fin m) → Expression Γ int
+    nil    : Expression Γ (tuple 0 [])
+    cons   : ∀ {m t ts} → Expression Γ t → Expression Γ (tuple m ts) → Expression Γ (tuple (suc m) (t ∷ ts))
+    head   : ∀ {m t ts} → Expression Γ (tuple (suc m) (t ∷ ts)) → Expression Γ t
+    tail   : ∀ {m t ts} → Expression Γ (tuple (suc m) (t ∷ ts)) → Expression Γ (tuple m ts)
+    call   : ∀ {t m Δ} → Function Δ t → All (Expression Γ) {m} Δ → Expression Γ t
     if_then_else_ : ∀ {t} → Expression Γ bool → Expression Γ t → Expression Γ t → Expression Γ t
 
   data CanAssign {n} {Γ} where
-    state : ∀ i {i<o : True (i ℕ.<? o)} → CanAssign (state i {i<o})
-    var   : ∀ i {i<n : True (i ℕ.<? n)} → CanAssign (var i {i<n})
-    abort : ∀ {t} {e : Expression Γ (fin 0)} → CanAssign (abort {t = t} e)
-    _∶_   : ∀ {m n t} {e₁ : Expression Γ (asType t m)} {e₂ : Expression Γ (asType t n)} → CanAssign e₁ → CanAssign e₂ → CanAssign (e₁ ∶ e₂)
-    [_]   : ∀ {t} {e : Expression Γ t} → CanAssign e → CanAssign [ e ]
-    unbox : ∀ {t} {e : Expression Γ (array t 1)} → CanAssign e → CanAssign (unbox e)
-    slice : ∀ {i j t} {e₁ : Expression Γ (asType t (i ℕ.+ j))} → CanAssign e₁ → (e₂ : Expression Γ (fin (suc i))) → CanAssign (slice e₁ e₂)
-    cast  : ∀ {i j t} {e : Expression Γ (asType t i)} .(eq : i ≡ j) → CanAssign e → CanAssign (cast eq e)
-    tup   : ∀ {m ts} {es : All (Expression Γ) {m} ts} → All (CanAssign ∘ proj₂) (reduce (λ {x} e → x , e) es) → CanAssign (tup es)
+    state : ∀ i → CanAssign (state i)
+    var   : ∀ i → CanAssign (var i)
+    abort : ∀ {t} e → CanAssign (abort {t = t} e)
+    [_]   : ∀ {t e} → CanAssign e → CanAssign ([_] {t = t} e)
+    unbox : ∀ {t e} → CanAssign e → CanAssign (unbox {t = t} e)
+    splice : ∀ {m n t e₁ e₂} → CanAssign e₁ → CanAssign e₂ → ∀ e₃ → CanAssign (splice {m = m} {n} {t} e₁ e₂ e₃)
+    cut    : ∀ {m n t e₁} → CanAssign e₁ → ∀ e₂ → CanAssign (cut {m = m} {n} {t} e₁ e₂)
+    cast  : ∀ {i j t e} .(eq : i ≡ j) → CanAssign e → CanAssign (cast {t = t} eq e)
+    nil   : CanAssign nil
+    cons  : ∀ {m t ts e₁ e₂} → CanAssign e₁ → CanAssign e₂ → CanAssign (cons {m = m} {t} {ts} e₁ e₂)
+    head  : ∀ {m t ts e} → CanAssign e → CanAssign (head {m = m} {t} {ts} e)
+    tail  : ∀ {m t ts e} → CanAssign e → CanAssign (tail {m = m} {t} {ts} e)
 
   canAssign? (lit x)      = no λ ()
   canAssign? (state i)    = yes (state i)
   canAssign? (var i)      = yes (var i)
-  canAssign? (abort e)    = yes abort
+  canAssign? (abort e)    = yes (abort e)
   canAssign? (e ≟ e₁)     = no λ ()
   canAssign? (e <? e₁)    = no λ ()
   canAssign? (inv e)      = no λ ()
@@ -173,8 +180,8 @@ module Code {o} (Σ : Vec Type o) where
   canAssign? (e or e₁)    = no λ ()
   canAssign? [ e ]        = map′ [_] (λ { [ e ] → e }) (canAssign? e)
   canAssign? (unbox e)    = map′ unbox (λ { (unbox e) → e }) (canAssign? e)
-  canAssign? (e ∶ e₁)     = map′ (uncurry _∶_) (λ { (e ∶ e₁) → e , e₁ }) (canAssign? e ×-dec canAssign? e₁)
-  canAssign? (slice e e₁) = map′ (λ e → slice e e₁) (λ { (slice e e₁) → e }) (canAssign? e)
+  canAssign? (splice e e₁ e₂) = map′ (λ (e , e₁) → splice e e₁ e₂) (λ { (splice e e₁ _) → e , e₁ }) (canAssign? e ×-dec canAssign? e₁)
+  canAssign? (cut e e₁)       = map′ (λ e → cut e e₁) (λ { (cut e e₁) → e }) (canAssign? e)
   canAssign? (cast eq e)  = map′ (cast eq) (λ { (cast eq e) → e }) (canAssign? e)
   canAssign? (- e)        = no λ ()
   canAssign? (e + e₁)     = no λ ()
@@ -185,38 +192,60 @@ module Code {o} (Σ : Vec Type o) where
   canAssign? (rnd e)      = no λ ()
   canAssign? (fin x e)    = no λ ()
   canAssign? (asInt e)    = no λ ()
-  canAssign? (tup es)     = map′ tup (λ { (tup es) → es }) (canAssignAll? es)
+  canAssign? nil          = yes nil
+  canAssign? (cons e e₁)  = map′ (uncurry cons) (λ { (cons e e₁) → e , e₁ }) (canAssign? e ×-dec canAssign? e₁)
+  canAssign? (head e)     = map′ head (λ { (head e) → e }) (canAssign? e)
+  canAssign? (tail e)     = map′ tail (λ { (tail e) → e }) (canAssign? e)
   canAssign? (call x e)   = no λ ()
   canAssign? (if e then e₁ else e₂) = no λ ()
 
-  canAssignAll? []       = yes []
-  canAssignAll? (e ∷ es) = map′ (uncurry _∷_) (λ { (e ∷ es) → e , es }) (canAssign? e ×-dec canAssignAll? es)
-
-  data AssignsState where
-    state : ∀ i {i<o} → AssignsState (state i {i<o})
-    _∶ˡ_ : ∀ {m n t e₁ e₂ a₁} → AssignsState a₁ → ∀ a₂ → AssignsState (_∶_ {m = m} {n} {t} {e₁} {e₂} a₁ a₂)
-    _∶ʳ_ : ∀ {m n t e₁ e₂} a₁ {a₂} → AssignsState a₂ → AssignsState (_∶_ {m = m} {n} {t} {e₁} {e₂} a₁ a₂)
-    [_] : ∀ {t e a} → AssignsState a → AssignsState ([_] {t = t} {e} a)
-    unbox : ∀ {t e a} → AssignsState a → AssignsState (unbox {t = t} {e} a)
-    slice : ∀ {i j t e₁ a} → AssignsState a → ∀ e₂ → AssignsState (slice {i = i} {j} {t} {e₁} a e₂)
-    cast : ∀ {i j t e} .(eq : i ≡ j) {a} → AssignsState a → AssignsState (cast {t = t} {e} eq a)
-    tup : ∀ {m ts es as} → Any (AssignsState ∘ proj₂) (reduce (λ {x} a → x , a) as) → AssignsState (tup {m = m} {ts} {es} as)
-
-  assignsState? (state i)    = yes (state i)
-  assignsState? (var i)      = no λ ()
-  assignsState? abort        = no λ ()
-  assignsState? (a ∶ a₁)     = map′ [ (_∶ˡ a₁) , (a ∶ʳ_) ]′ (λ { (s ∶ˡ _) → inj₁ s ; (_ ∶ʳ s) → inj₂ s }) (assignsState? a ⊎-dec assignsState? a₁)
-  assignsState? [ a ]        = map′ [_] (λ { [ s ] → s }) (assignsState? a)
-  assignsState? (unbox a)    = map′ unbox (λ { (unbox s) → s }) (assignsState? a)
-  assignsState? (slice a e₂) = map′ (λ s → slice s e₂ ) (λ { (slice s _) → s }) (assignsState? a)
-  assignsState? (cast eq a)  = map′ (cast eq) (λ { (cast _ s) → s }) (assignsState? a)
-  assignsState? (tup as)     = map′ tup (λ { (tup ss) → ss }) (assignsStateAny? as)
-
-  assignsStateAny? {es = []}     []       = no λ ()
-  assignsStateAny? {es = e ∷ es} (a ∷ as) = map′ [ here , there ]′ (λ { (here s) → inj₁ s ; (there ss) → inj₂ ss }) (assignsState? a ⊎-dec assignsStateAny? as)
+  data ReferencesState where
+    state : ∀ i → ReferencesState (state i)
+    [_] : ∀ {t e} → ReferencesState e → ReferencesState ([_] {t = t} e)
+    unbox : ∀ {t e} → ReferencesState e → ReferencesState (unbox {t = t} e)
+    spliceˡ : ∀ {m n t e} → ReferencesState e → ∀ e₁ e₂ → ReferencesState (splice {m = m} {n} {t} e e₁ e₂)
+    spliceʳ : ∀ {m n t} e {e₁} → ReferencesState e₁ → ∀ e₂ → ReferencesState (splice {m = m} {n} {t} e e₁ e₂)
+    cut : ∀ {m n t e} → ReferencesState e → ∀ e₁ → ReferencesState (cut {m = m} {n} {t} e e₁)
+    cast : ∀ {i j t} .(eq : i ≡ j) {e} → ReferencesState e → ReferencesState (cast {t = t} eq e)
+    consˡ : ∀ {m t ts e} → ReferencesState e → ∀ e₁ → ReferencesState (cons {m = m} {t} {ts} e e₁)
+    consʳ : ∀ {m t ts} e {e₁} → ReferencesState e₁ → ReferencesState (cons {m = m} {t} {ts} e e₁)
+    head : ∀ {m t ts e} → ReferencesState e → ReferencesState (head {m = m} {t} {ts} e)
+    tail : ∀ {m t ts e} → ReferencesState e → ReferencesState (tail {m = m} {t} {ts} e)
+
+  referencesState? (lit x) = no λ ()
+  referencesState? (state i) = yes (state i)
+  referencesState? (var i) = no λ ()
+  referencesState? (abort e) = no λ ()
+  referencesState? (e ≟ e₁) = no λ ()
+  referencesState? (e <? e₁) = no λ ()
+  referencesState? (inv e) = no λ ()
+  referencesState? (e && e₁) = no λ ()
+  referencesState? (e || e₁) = no λ ()
+  referencesState? (not e) = no λ ()
+  referencesState? (e and e₁) = no λ ()
+  referencesState? (e or e₁) = no λ ()
+  referencesState? [ e ] = map′ [_] (λ { [ e ] → e }) (referencesState? e)
+  referencesState? (unbox e) = map′ unbox (λ { (unbox e) → e }) (referencesState? e)
+  referencesState? (splice e e₁ e₂) = map′ [ (λ e → spliceˡ e e₁ e₂) , (λ e₁ → spliceʳ e e₁ e₂) ]′ (λ { (spliceˡ e e₁ e₂) → inj₁ e ; (spliceʳ e e₁ e₂) → inj₂ e₁ }) (referencesState? e ⊎-dec referencesState? e₁)
+  referencesState? (cut e e₁) = map′ (λ e → cut e e₁) (λ { (cut e e₁) → e }) (referencesState? e)
+  referencesState? (cast eq e) = map′ (cast eq) (λ { (cast eq e) → e }) (referencesState? e)
+  referencesState? (- e) = no λ ()
+  referencesState? (e + e₁) = no λ ()
+  referencesState? (e * e₁) = no λ ()
+  referencesState? (e ^ x) = no λ ()
+  referencesState? (e >> x) = no λ ()
+  referencesState? (rnd e) = no λ ()
+  referencesState? (fin x e) = no λ ()
+  referencesState? (asInt e) = no λ ()
+  referencesState? nil = no λ ()
+  referencesState? (cons e e₁) = map′ [ (λ e → consˡ e e₁) , (λ e₁ → consʳ e e₁) ]′ (λ { (consˡ e e₁) → inj₁ e ; (consʳ e e₁) → inj₂ e₁ }) (referencesState? e ⊎-dec referencesState? e₁)
+  referencesState? (head e) = map′ head (λ { (head e) → e }) (referencesState? e)
+  referencesState? (tail e) = map′ tail (λ { (tail e) → e }) (referencesState? e)
+  referencesState? (call f es) = no λ ()
+  referencesState? (if e then e₁ else e₂) = no λ ()
 
   infix  4 _≔_
-  infixl 2 if_then_else_
+  infixl 2 if_then_else_ if_then_
   infixl 1 _∙_ _∙return_
   infix  1 _∙end
 
@@ -225,27 +254,30 @@ module Code {o} (Σ : Vec Type o) where
     skip          : Statement Γ
     _≔_           : ∀ {t} → (ref : Expression Γ t) → {canAssign : True (canAssign? ref)} → Expression Γ t → Statement Γ
     declare       : ∀ {t} → Expression Γ t → Statement (t ∷ Γ) → Statement Γ
-    invoke        : ∀ {m Δ} → Procedure Δ → Expression Γ (tuple m Δ) → Statement Γ
+    invoke        : ∀ {m Δ} → Procedure Δ → All (Expression Γ) {m} Δ → Statement Γ
+    if_then_      : Expression Γ bool → Statement Γ → Statement Γ
     if_then_else_ : Expression Γ bool → Statement Γ → Statement Γ → Statement Γ
     for           : ∀ m → Statement (fin m ∷ Γ) → Statement Γ
 
   data ChangesState where
-    _∙ˡ_           : ∀ {s₁} → ChangesState s₁ → ∀ s₂ → ChangesState (s₁ ∙ s₂)
-    _∙ʳ_           : ∀ s₁ {s₂} → ChangesState s₂ → ChangesState (s₁ ∙ s₂)
-    _≔_            : ∀ {t ref} canAssign {assignsState : True (assignsState? (toWitness canAssign))} e₂ → ChangesState (_≔_ {t = t} ref {canAssign} e₂)
+    _∙ˡ_           : ∀ {s} → ChangesState s → ∀ s₁ → ChangesState (s ∙ s₁)
+    _∙ʳ_           : ∀ s {s₁} → ChangesState s₁ → ChangesState (s ∙ s₁)
+    _≔_            : ∀ {t} ref {canAssign : True (canAssign? ref)} {refsState : True (referencesState? ref)} e₂ → ChangesState (_≔_ {t = t} ref {canAssign} e₂)
     declare        : ∀ {t} e {s} → ChangesState s → ChangesState (declare {t = t} e s)
-    invoke         : ∀ {m Δ} p e → ChangesState (invoke {m = m} {Δ} p e)
-    if_then′_else_ : ∀ e {s₁} → ChangesState s₁ → ∀ s₂ → ChangesState (if e then s₁ else s₂)
-    if_then_else′_ : ∀ e s₁ {s₂} → ChangesState s₂ → ChangesState (if e then s₁ else s₂)
+    invoke         : ∀ {m Δ} p es → ChangesState (invoke {m = m} {Δ} p es)
+    if_then_       : ∀ e {s} → ChangesState s → ChangesState (if e then s)
+    if_then′_else_ : ∀ e {s} → ChangesState s → ∀ s₁ → ChangesState (if e then s else s₁)
+    if_then_else′_ : ∀ e s {s₁} → ChangesState s₁ → ChangesState (if e then s else s₁)
     for            : ∀ m {s} → ChangesState s → ChangesState (for m s)
 
-  changesState? (s₁ ∙ s₂)              = map′ [ _∙ˡ s₂ , s₁ ∙ʳ_ ]′ (λ { (s ∙ˡ _) → inj₁ s ; (_ ∙ʳ s) → inj₂ s }) (changesState? s₁ ⊎-dec changesState? s₂)
-  changesState? skip                   = no λ ()
-  changesState? (_≔_ ref {a} e)        = map′ (λ s → _≔_ a {fromWitness s} e) (λ { (_≔_ _ {s} _) → toWitness s }) (assignsState? (toWitness a))
-  changesState? (declare e s)          = map′ (declare e) (λ { (declare e s) → s }) (changesState? s)
-  changesState? (invoke p e)           = yes (invoke p e)
-  changesState? (if e then s₁ else s₂) = map′ [ if e then′_else s₂ , if e then s₁ else′_ ]′ (λ { (if _ then′ s else _) → inj₁ s ; (if _ then _ else′ s) → inj₂ s }) (changesState? s₁ ⊎-dec changesState? s₂)
-  changesState? (for m s)              = map′ (for m) (λ { (for m s) → s }) (changesState? s)
+  changesState? (s ∙ s₁)              = map′ [ _∙ˡ s₁ , s ∙ʳ_ ]′ (λ { (s ∙ˡ s₁) → inj₁ s ; (s ∙ʳ s₁) → inj₂ s₁ }) (changesState? s ⊎-dec changesState? s₁)
+  changesState? skip                  = no λ ()
+  changesState? (_≔_ ref e)           = map′ (λ refsState → _≔_ ref {refsState = fromWitness refsState} e) (λ { (_≔_ ref {refsState = refsState} e) → toWitness refsState }) (referencesState? ref)
+  changesState? (declare e s)         = map′ (declare e) (λ { (declare e s) → s }) (changesState? s)
+  changesState? (invoke p e)          = yes (invoke p e)
+  changesState? (if e then s)         = map′ (if e then_) (λ { (if e then s) → s }) (changesState? s)
+  changesState? (if e then s else s₁) = map′ [ if e then′_else s₁ , if e then s else′_ ]′ (λ { (if e then′ s else s₁) → inj₁ s ; (if e then s else′ s₁) → inj₂ s₁ }) (changesState? s ⊎-dec changesState? s₁)
+  changesState? (for m s)             = map′ (for m) (λ { (for m s) → s }) (changesState? s)
 
   data Function Γ ret where
     _∙return_ : (s : Statement Γ) → {False (changesState? s)} → Expression Γ ret → Function Γ ret
@@ -253,36 +285,45 @@ module Code {o} (Σ : Vec Type o) where
 
   data Procedure Γ where
     _∙end   : Statement Γ → Procedure Γ
-    declare : ∀ {t} → Expression Γ t → Procedure (t ∷ Γ) → Procedure Γ
 
   infixl  6 _<<_
-  infixl 5 _-_
+  infixl 5 _-_ _∶_
+
+  tup : ∀ {n Γ m ts} → All (Expression {n} Γ) ts → Expression Γ (tuple m ts)
+  tup []       = nil
+  tup (e ∷ es) = cons e (tup es)
+
+  _∶_ : ∀ {n Γ i j t} → Expression {n} Γ (asType t j) → Expression Γ (asType t i) → Expression Γ (asType t (i ℕ.+ j))
+  e₁ ∶ e₂ = splice e₁ e₂ (lit (Fin.fromℕ _ ′f))
+
+  slice : ∀ {n Γ i j t} → Expression {n} Γ (asType t (i ℕ.+ j)) → Expression Γ (fin (suc i)) → Expression Γ (asType t j)
+  slice e₁ e₂ = head (cut e₁ e₂)
 
   slice′ : ∀ {n Γ i j t} → Expression {n} Γ (asType t (i ℕ.+ j)) → Expression Γ (fin (suc j)) → Expression Γ (asType t i)
   slice′ {i = i} e₁ e₂ = slice (cast (+-comm i _) e₁) e₂
 
-  _-_   : ∀ {n Γ t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression {n} Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ {isNumeric₁} {isNumeric₂})
+  _-_   : ∀ {n Γ t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression {n} Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ isNumeric₁ isNumeric₂)
   _-_ {isNumeric₂ = isNumeric₂} x y = x + (-_ {isNumeric = isNumeric₂} y)
 
   _<<_ : ∀ {n Γ} → Expression {n} Γ int → ℕ → Expression Γ int
   x << n = rnd (x * lit (2 ′r) ^ n)
 
   get : ∀ {n Γ} → ℕ → Expression {n} Γ int → Expression Γ bit
-  get i x = if x - x >> suc i << suc i <? lit (2 ′i) ^ i then lit ((false ∷ []) ′x) else lit ((true ∷ []) ′x)
+  get i x = if x - x >> suc i << suc i <? lit (2 ′i) ^ i then lit (false ′x) else lit (true ′x)
 
   uint : ∀ {n Γ m} → Expression {n} Γ (bits m) → Expression Γ int
   uint {m = zero}  x = lit (0 ′i)
   uint {m = suc m} x =
-    lit (2 ′i) * uint {m = m} (slice x (lit ((# 1) ′f))) +
-    ( if slice′ x (lit ((# 0) ′f)) ≟ lit ((true ∷ []) ′x)
+    lit (2 ′i) * uint {m = m} (slice x (lit (1F ′f))) +
+    ( if slice′ x (lit (0F ′f)) ≟ lit ((true ∷ []) ′xs)
       then lit (1 ′i)
       else lit (0 ′i))
 
   sint : ∀ {n Γ m} → Expression {n} Γ (bits m) → Expression Γ int
   sint {m = zero}        x = lit (0 ′i)
-  sint {m = suc zero}    x = if x ≟ lit ((true ∷ []) ′x) then - lit (1 ′i) else lit (0 ′i)
+  sint {m = suc zero}    x = if x ≟ lit ((true ∷ []) ′xs) then - lit (1 ′i) else lit (0 ′i)
   sint {m = suc (suc m)} x =
-    lit (2 ′i) * sint (slice {i = 1} x (lit ((# 1) ′f))) +
-    ( if slice′ x (lit ((# 0) ′f)) ≟ lit ((true ∷ []) ′x)
+    lit (2 ′i) * sint (slice {i = 1} x (lit (1F ′f))) +
+    ( if slice′ x (lit (0F ′f)) ≟ lit ((true ∷ []) ′xs)
       then lit (1 ′i)
       else lit (0 ′i))
diff --git a/src/Helium/Data/Pseudocode/Types.agda b/src/Helium/Data/Pseudocode/Types.agda
index 971ca12..dbd3c6b 100644
--- a/src/Helium/Data/Pseudocode/Types.agda
+++ b/src/Helium/Data/Pseudocode/Types.agda
@@ -146,3 +146,5 @@ record Pseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ :
     ; _/1 = _/1
     ; ⌊_⌋ = ⌊_⌋
     }
+
+  open RawPseudocode rawPseudocode using (module ℤ′; module ℝ′) public
diff --git a/src/Helium/Instructions/Base.agda b/src/Helium/Instructions/Base.agda
index 62a6968..d157d5a 100644
--- a/src/Helium/Instructions/Base.agda
+++ b/src/Helium/Instructions/Base.agda
@@ -10,6 +10,7 @@ module Helium.Instructions.Base where
 
 open import Data.Bool as Bool using (true; false)
 open import Data.Fin as Fin using (Fin; Fin′; zero; suc; toℕ)
+open import Data.Fin.Patterns
 open import Data.Nat as ℕ using (ℕ; zero; suc)
 import Data.Nat.Properties as ℕₚ
 open import Data.Sum using ([_,_]′; inj₂)
@@ -49,25 +50,25 @@ open Core.Code State public
 -- Direct from State
 
 S : ∀ {n Γ} → Expression {n} Γ (array (bits 32) 32)
-S = state 0
+S = state 0F
 
 R : ∀ {n Γ} → Expression {n} Γ (array (bits 32) 16)
-R = state 1
+R = state 1F
 
 VPR-P0 : ∀ {n Γ} → Expression {n} Γ (bits 16)
-VPR-P0 = state 2
+VPR-P0 = state 2F
 
 VPR-mask : ∀ {n Γ} → Expression {n} Γ (bits 8)
-VPR-mask = state 3
+VPR-mask = state 3F
 
 FPSCR-QC : ∀ {n Γ} → Expression {n} Γ bit
-FPSCR-QC = state 4
+FPSCR-QC = state 4F
 
 AdvanceVPTState : ∀ {n Γ} → Expression {n} Γ bool
-AdvanceVPTState = state 5
+AdvanceVPTState = state 5F
 
 BeatId : ∀ {n Γ} → Expression {n} Γ beat
-BeatId = state 6
+BeatId = state 6F
 
 -- Indirect
 
@@ -84,8 +85,7 @@ join {k = k} {suc m} x = cast eq (join (slice x (lit (Fin.fromℕ 1 ′f))) ∶
   eq = P.trans (P.cong (k ℕ.+_) (ℕₚ.*-comm k (suc m))) (ℕₚ.*-comm (suc (suc m)) k)
 
 index : ∀ {n Γ t m} → Expression {n} Γ (asType t (suc m)) → Expression Γ (fin (suc m)) → Expression Γ (elemType t)
-index {t = bits}    {m} x i = slice (cast (ℕₚ.+-comm 1 m) x) i
-index {t = array _} {m} x i = unbox (slice (cast (ℕₚ.+-comm 1 m) x) i)
+index {m = m} x i = unbox (slice (cast (ℕₚ.+-comm 1 m) x) i)
 
 Q : ∀ {n Γ} → Expression {n} Γ (array (array (bits 32) 4) 8)
 Q = group 7 S
@@ -98,39 +98,39 @@ elem {k = suc k} (suc m) x i = index (group k (cast (ℕₚ.*-comm (suc k) (suc
 --- Other utiliies
 
 hasBit : ∀ {n Γ m} → Expression {n} Γ (bits (suc m)) → Expression Γ (fin (suc m)) → Expression Γ bool
-hasBit {n} x i = index x i ≟ lit ((true ∷ []) ′x)
+hasBit {n} x i = index x i ≟ lit (true ′x)
 
 sliceⁱ : ∀ {n Γ m} → ℕ → Expression {n} Γ int → Expression Γ (bits m)
-sliceⁱ {m = zero}  n i = lit ([] ′x)
-sliceⁱ {m = suc m} n i = sliceⁱ (suc n) i ∶ get n i
+sliceⁱ {m = zero}  n i = lit ([] ′xs)
+sliceⁱ {m = suc m} n i = sliceⁱ (suc n) i ∶ [ get n i ]
 
 --- Functions
 
 Int : ∀ {n} → Function (bits n ∷ bool ∷ []) int
-Int = skip ∙return (if var 1 then uint (var 0) else sint (var 0))
+Int = skip ∙return (if var 1F then uint (var 0F) else sint (var 0F))
 
 -- arguments swapped, pred n
 SignedSatQ : ∀ n → Function (int ∷ []) (tuple 2 (bits (suc n) ∷ bool ∷ []))
 SignedSatQ n = declare (lit (true ′b)) (
-  if max <? var 1
+  if max <? var 1F
   then
-    var 1 ≔ max
-  else if var 1 <? min
+    var 1F ≔ max
+  else if var 1F <? min
   then
-    var 1 ≔ min
+    var 1F ≔ min
   else
-    var 0 ≔ lit (false ′b)
-  ∙return tup (sliceⁱ 0 (var 1) ∷ var 0 ∷ []))
+    var 0F ≔ lit (false ′b)
+  ∙return tup (sliceⁱ 0 (var 1F) ∷ var 0F ∷ []))
   where
   max = lit (2 ′i) ^ n + - lit (1 ′i)
   min = - (lit (2 ′i) ^ n)
 
 -- actual shift if 'shift + 1'
 LSL-C : ∀ {n} (shift : ℕ) → Function (bits n ∷ []) (tuple 2 (bits n ∷ bit ∷ []))
-LSL-C {n} shift = declare (var 0 ∶ lit ((Vec.replicate {n = (suc shift)} false) ′x))
+LSL-C {n} shift = declare (var 0F ∶ lit ((Vec.replicate {n = (suc shift)} false) ′xs))
   (skip ∙return tup
-    ( slice (var 0) (lit (zero ′f))
-    ∷ slice (cast eq (var 0)) (lit (Fin.inject+ shift (Fin.fromℕ n) ′f))
+    ( slice (var 0F) (lit (zero ′f))
+    ∷ unbox (slice (cast eq (var 0F)) (lit (Fin.inject+ shift (Fin.fromℕ n) ′f)))
     ∷ []))
   where
   eq = P.trans (ℕₚ.+-comm 1 (shift ℕ.+ n)) (P.cong (ℕ._+ 1) (ℕₚ.+-comm shift n))
@@ -146,46 +146,41 @@ private
 copyMasked : Procedure (fin 8 ∷ bits 32 ∷ beat ∷ elmtMask ∷ [])
 copyMasked = for 4
   -- 0:e 1:dest 2:result 3:beat 4:elmtMask
-  ( if hasBit (var 4) (var 0)
+  ( if hasBit (var 4F) (var 0F)
     then
-      elem 8 (index (index Q (var 1)) (var 3)) (var 0) ≔ elem 8 (var 2) (var 0)
-    else skip
+      elem 8 (index (index Q (var 1F)) (var 3F)) (var 0F) ≔ elem 8 (var 2F) (var 0F)
   ) ∙end
 
 VPTAdvance : Procedure (beat ∷ [])
-VPTAdvance = declare (fin div2 (tup (var 0 ∷ []))) (
-  declare (elem 4 VPR-mask (var 0)) (
+VPTAdvance = declare (fin div2 (tup (var 0F ∷ []))) (
+  declare (elem 4 VPR-mask (var 0F)) (
     -- 0:vptState 1:maskId 2:beat
-    if var 0 ≟ lit ((true ∷ false ∷ false ∷ false ∷ []) ′x)
+    if var 0F ≟ lit ((true ∷ false ∷ false ∷ false ∷ []) ′xs)
     then
-      var 0 ≔ lit (Vec.replicate false ′x)
-    else if inv (var 0 ≟ lit (Vec.replicate false ′x))
+      var 0F ≔ lit (Vec.replicate false ′xs)
+    else if inv (var 0F ≟ lit (Vec.replicate false ′xs))
     then (
-      declare (lit ((false ∷ []) ′x)) (
+      declare (lit (false ′x)) (
         -- 0:inv 1:vptState 2:maskId 3:beat
-        tup (var 1 ∷ var 0 ∷ []) ≔ call (LSL-C 0) (tup (var 1 ∷ [])) ∙
-        if var 0 ≟ lit ((true ∷ []) ′x)
+        tup (var 1F ∷ var 0F ∷ []) ≔ call (LSL-C 0) (var 1F ∷ []) ∙
+        if var 0F ≟ lit (true ′x)
         then
-          elem 4 VPR-P0 (var 3) ≔ not (elem 4 VPR-P0 (var 3))
-        else skip))
-    else skip ∙
-    if get 0 (asInt (var 2)) ≟ lit ((true ∷ []) ′x)
+          elem 4 VPR-P0 (var 3F) ≔ not (elem 4 VPR-P0 (var 3F)))) ∙
+    if get 0 (asInt (var 2F)) ≟ lit (true ′x)
     then
-      elem 4 VPR-mask (var 1) ≔ var 0
-    else skip
-    ∙end))
+      elem 4 VPR-mask (var 1F) ≔ var 0F))
+    ∙end
 
 VPTActive : Function (beat ∷ []) bool
-VPTActive = skip ∙return inv (elem 4 VPR-mask (fin div2 (tup (var 0 ∷ []))) ≟ lit (Vec.replicate false ′x))
+VPTActive = skip ∙return inv (elem 4 VPR-mask (fin div2 (tup (var 0F ∷ []))) ≟ lit (Vec.replicate false ′xs))
 
 GetCurInstrBeat : Function [] (tuple 2 (beat ∷ elmtMask ∷ []))
-GetCurInstrBeat = declare (lit (Vec.replicate true ′x)) (
+GetCurInstrBeat = declare (lit (Vec.replicate true ′xs)) (
   -- 0:elmtMask 1:beat
-  if call VPTActive (tup (BeatId ∷ []))
+  if call VPTActive (BeatId ∷ [])
   then
-    var 0 ≔ var 0 and elem 4 VPR-P0 BeatId
-  else skip
-  ∙return tup (BeatId ∷ var 0 ∷ []))
+    var 0F ≔ var 0F and elem 4 VPR-P0 BeatId
+  ∙return tup (BeatId ∷ var 0F ∷ []))
 
 -- Assumes:
 --   MAX_OVERLAPPING_INSTRS = 1
@@ -197,13 +192,12 @@ ExecBeats : Procedure [] → Procedure []
 ExecBeats DecodeExec =
   for 4 (
     -- 0:beatId
-    BeatId ≔ var 0 ∙
+    BeatId ≔ var 0F ∙
     AdvanceVPTState ≔ lit (true ′b) ∙
-    invoke DecodeExec (tup []) ∙
+    invoke DecodeExec [] ∙
     if AdvanceVPTState
     then
-      invoke VPTAdvance (tup (var 0 ∷ []))
-    else skip)
+      invoke VPTAdvance (var 0F ∷ []))
   ∙end
 
 from32 : ∀ size {n Γ} → Expression {n} Γ (bits 32) → Expression Γ (array (bits (toℕ (Instr.Size.esize size))) (toℕ (Instr.Size.elements size)))
@@ -222,71 +216,70 @@ module _ (d : Instr.VecOp₂) where
  -- 0:op₂ 1:e 2:op₁ 3:result 4:elmtMask 5:curBeat
   vec-op₂′ : Statement (bits (toℕ esize) ∷ fin (toℕ elements) ∷ array (bits (toℕ esize)) (toℕ elements) ∷ array (bits (toℕ esize)) (toℕ elements) ∷ elmtMask ∷ beat ∷ []) → Procedure []
   vec-op₂′ op = declare (lit (zero ′f)) (
-    declare (lit (Vec.replicate false ′x)) (
+    declare (lit (Vec.replicate false ′xs)) (
     -- 0:elmtMask 1:curBeat
-    tup (var 1 ∷ var 0 ∷ []) ≔ call GetCurInstrBeat (tup []) ∙
-    declare (lit ((Vec.replicate false ′x) ′a)) (
-    declare (from32 size (index (index Q (lit (src₁ ′f))) (var 2))) (
+    tup (var 1F ∷ var 0F ∷ []) ≔ call GetCurInstrBeat [] ∙
+    declare (lit ((Vec.replicate false ′xs) ′a)) (
+    declare (from32 size (index (index Q (lit (src₁ ′f))) (var 2F))) (
     -- 0:op₁ 1:result 2:elmtMask 3:curBeat
     for (toℕ elements) (
        -- 0:e 1:op₁ 2:result 3:elmtMask 4:curBeat
       declare op₂ op ) ∙
     -- 0:op₁ 1:result 2:elmtMask 3:curBeat
-    invoke copyMasked (tup (lit (dest ′f) ∷ to32 size (var 1) ∷ var 3 ∷ var 2 ∷ []))))
-    ∙end))
+    invoke copyMasked (lit (dest ′f) ∷ to32 size (var 1F) ∷ var 3F ∷ var 2F ∷ [])))))
+    ∙end
     where
     -- 0:e 1:op₁ 2:result 3:elmtMask 4:curBeat
     op₂ =
       [ (λ src₂ → index (from32 size (index R (lit (src₂ ′f)))) (lit (zero ′f)))
-      , (λ src₂ → index (from32 size (index (index Q (lit (src₂ ′f))) (var 4))) (var 0))
+      , (λ src₂ → index (from32 size (index (index Q (lit (src₂ ′f))) (var 4F))) (var 0F))
       ]′ src₂
 
   vec-op₂ : Function (bits (toℕ esize) ∷ bits (toℕ esize) ∷ []) (bits (toℕ esize)) → Procedure []
-  vec-op₂ op = vec-op₂′ (index (var 3) (var 1) ≔ call op (tup (index (var 2) (var 1) ∷ var 0 ∷ [])))
+  vec-op₂ op = vec-op₂′ (index (var 3F) (var 1F) ≔ call op (index (var 2F) (var 1F) ∷ var 0F ∷ []))
 
 vadd : Instr.VAdd → Procedure []
-vadd d = vec-op₂ d (skip ∙return sliceⁱ 0 (uint (var 0) + uint (var 1)))
+vadd d = vec-op₂ d (skip ∙return sliceⁱ 0 (uint (var 0F) + uint (var 1F)))
 
 vsub : Instr.VSub → Procedure []
-vsub d = vec-op₂ d (skip ∙return sliceⁱ 0 (uint (var 0) - uint (var 1)))
+vsub d = vec-op₂ d (skip ∙return sliceⁱ 0 (uint (var 0F) - uint (var 1F)))
 
 vhsub : Instr.VHSub → Procedure []
-vhsub d = vec-op₂ op₂ (skip ∙return sliceⁱ 1 (toInt (var 0) - toInt (var 1)))
-  where open Instr.VHSub d; toInt = λ i → call Int (tup (i ∷ lit (unsigned ′b) ∷ []))
+vhsub d = vec-op₂ op₂ (skip ∙return sliceⁱ 1 (toInt (var 0F) - toInt (var 1F)))
+  where open Instr.VHSub d; toInt = λ i → call Int (i ∷ lit (unsigned ′b) ∷ [])
 
 vmul : Instr.VMul → Procedure []
-vmul d = vec-op₂ d (skip ∙return sliceⁱ 0 (sint (var 0) * sint (var 1)))
+vmul d = vec-op₂ d (skip ∙return sliceⁱ 0 (sint (var 0F) * sint (var 1F)))
 
 vmulh : Instr.VMulH → Procedure []
-vmulh d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0) * toInt (var 1)))
+vmulh d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0F) * toInt (var 1F)))
   where
-  open Instr.VMulH d; toInt = λ i → call Int (tup (i ∷ lit (unsigned ′b) ∷ []))
+  open Instr.VMulH d; toInt = λ i → call Int (i ∷ lit (unsigned ′b) ∷ [])
 
 vrmulh : Instr.VRMulH → Procedure []
-vrmulh d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0) * toInt (var 1) + lit (1 ′i) << toℕ esize-1))
+vrmulh d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0F) * toInt (var 1F) + lit (1 ′i) << toℕ esize-1))
   where
-  open Instr.VRMulH d; toInt = λ i → call Int (tup (i ∷ lit (unsigned ′b) ∷ []))
+  open Instr.VRMulH d; toInt = λ i → call Int (i ∷ lit (unsigned ′b) ∷ [])
 
 vmla : Instr.VMlA → Procedure []
-vmla d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0) * element₂ + toInt (var 1)))
+vmla d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0F) * element₂ + toInt (var 1F)))
   where
   open Instr.VMlA d
   op₂ = record { size = size ; dest = acc ; src₁ = src₁ ; src₂ = inj₂ acc }
-  toInt = λ i → call Int (tup (i ∷ lit (unsigned ′b) ∷ []))
+  toInt = λ i → call Int (i ∷ lit (unsigned ′b) ∷ [])
   element₂ = toInt (index (from32 size (index R (lit (src₂ ′f)))) (lit (zero ′f)))
 
 private
   vqr?dmulh : Instr.VQDMulH → Function (int ∷ int ∷ []) int → Procedure []
   vqr?dmulh d f = vec-op₂′ d (
     -- 0:op₂ 1:e 2:op₁ 3:result 4:elmtMask 5:curBeat
-    declare (call f (tup (sint (index (var 2) (var 1)) ∷ sint (var 0) ∷ []))) (
+    declare (call f (sint (index (var 2F) (var 1F)) ∷ sint (var 0F) ∷ [])) (
     declare (lit (false ′b)) (
       -- 0:sat 1:value 2:op₂ 3:e 4:op₁ 5:result 6:elmtMask 7:curBeat
-      tup (index (var 5) (var 3) ∷ var 0 ∷ []) ≔ call (SignedSatQ (toℕ esize-1)) (tup (var 1 ∷ [])) ∙
-      if var 0 && hasBit (var 6) (fin e*esize>>3 (tup ((var 3) ∷ [])))
+      tup (index (var 5F) (var 3F) ∷ var 0F ∷ []) ≔ call (SignedSatQ (toℕ esize-1)) (var 1F ∷ []) ∙
+      if var 0F && hasBit (var 6F) (fin e*esize>>3 (tup ((var 3F) ∷ [])))
       then
-        FPSCR-QC ≔ lit ((true ∷ []) ′x)
-      else skip)))
+        FPSCR-QC ≔ lit (true ′x))))
     where
     open Instr.VecOp₂ d
 
@@ -299,9 +292,9 @@ private
       helper Instr.32bit i = Fin.combine i zero
 
 vqdmulh : Instr.VQDMulH → Procedure []
-vqdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0 * var 1 >> toℕ esize)
+vqdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0F * var 1F >> toℕ esize)
   where open Instr.VecOp₂ d using (esize)
 
 vqrdmulh : Instr.VQRDMulH → Procedure []
-vqrdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0 * var 1 + lit (1 ′i) << toℕ esize-1 >> toℕ esize)
+vqrdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0F * var 1F + lit (1 ′i) << toℕ esize-1 >> toℕ esize)
   where open Instr.VecOp₂ d using (esize; esize-1)
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
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
index b425252..0bd1794 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -17,7 +17,7 @@ private
   open module C = RawPseudocode rawPseudocode
 
 open import Data.Bool as Bool using (Bool; true; false)
-open import Data.Fin as Fin using (Fin; zero; suc; #_)
+open import Data.Fin as Fin using (Fin; zero; suc)
 import Data.Fin.Properties as Finₚ
 open import Data.Nat as ℕ using (ℕ; zero; suc)
 import Data.Nat.Properties as ℕₚ
@@ -31,7 +31,7 @@ open import Function using (case_of_; _∘′_; id)
 open import Helium.Data.Pseudocode.Core
 import Induction as I
 import Induction.WellFounded as Wf
-open import Level hiding (zero; suc)
+open import Level using (Level; _⊔_; 0ℓ)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
 open import Relation.Nullary using (does)
 open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromWitness)
@@ -41,6 +41,7 @@ open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromW
 ⟦ int ⟧ₗ        = i₁
 ⟦ fin n ⟧ₗ      = 0ℓ
 ⟦ real ⟧ₗ       = r₁
+⟦ bit ⟧ₗ        = b₁
 ⟦ bits n ⟧ₗ     = b₁
 ⟦ tuple n ts ⟧ₗ = helper ts
   where
@@ -56,6 +57,7 @@ open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromW
 ⟦ int ⟧ₜ        = ℤ
 ⟦ fin n ⟧ₜ      = Fin n
 ⟦ real ⟧ₜ       = ℝ
+⟦ bit ⟧ₜ        = Bit
 ⟦ bits n ⟧ₜ     = Bits n
 ⟦ tuple n ts ⟧ₜ = ⟦ ts ⟧ₜ′
 ⟦ array t n ⟧ₜ  = Vec ⟦ t ⟧ₜ n
@@ -66,13 +68,13 @@ open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromW
 
 -- The case for bitvectors looks odd so that the right-most bit is bit 0.
 𝒦 : ∀ {t} → Literal t → ⟦ t ⟧ₜ
-𝒦 (x ′b)  = x
-𝒦 (x ′i)  = x ℤ′.×′ 1ℤ
-𝒦 (x ′f)  = x
-𝒦 (x ′r)  = x ℝ′.×′ 1ℝ
-𝒦 (xs ′x) = Vec.foldl Bits (λ bs b → (Bool.if b then 1𝔹 else 0𝔹) VecF.∷ bs) VecF.[] xs
-𝒦 (x ′a)  = Vec.replicate (𝒦 x)
-
+𝒦 (x ′b)   = x
+𝒦 (x ′i)   = x ℤ′.×′ 1ℤ
+𝒦 (x ′f)   = x
+𝒦 (x ′r)   = x ℝ′.×′ 1ℝ
+𝒦 (x ′x)   = Bool.if x then 1𝔹 else 0𝔹
+𝒦 (xs ′xs) = Vec.foldl Bits (λ bs b → (Bool.if b then 1𝔹 else 0𝔹) VecF.∷ bs) VecF.[] xs
+𝒦 (x ′a)   = Vec.replicate (𝒦 x)
 
 fetch : ∀ {n} ts → ⟦ tuple n ts ⟧ₜ → ∀ i → ⟦ Vec.lookup ts i ⟧ₜ
 fetch (_ ∷ [])     x        zero    = x
@@ -96,10 +98,11 @@ tupTail []      x        = _
 tupTail (_ ∷ _) (x , xs) = xs
 
 equal : ∀ {t} → HasEquality t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ → Bool
-equal bool x y = does (x Bool.≟ y)
-equal int  x y = does (x ≟ᶻ y)
-equal fin  x y = does (x Fin.≟ y)
-equal real x y = does (x ≟ʳ y)
+equal bool     x y = does (x Bool.≟ y)
+equal int      x y = does (x ≟ᶻ y)
+equal fin      x y = does (x Fin.≟ y)
+equal real     x y = does (x ≟ʳ y)
+equal bit      x y = does (x ≟ᵇ₁ y)
 equal bits x y = does (x ≟ᵇ y)
 
 comp : ∀ {t} → IsNumeric t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ → Bool
@@ -108,8 +111,8 @@ comp real x y = does (x <ʳ? y)
 
 -- 0 of y is 0 of result
 join : ∀ t {m n} → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ → ⟦ asType t (n ℕ.+ m) ⟧ₜ
-join bits      {m} x y = y VecF.++ x
-join (array _) {m} x y = y Vec.++ x
+join bits      x y = y VecF.++ x
+join (array _) x y = y Vec.++ x
 
 -- take from 0
 take : ∀ t i {j} → ⟦ asType t (i ℕ.+ j) ⟧ₜ → ⟦ asType t i ⟧ₜ
@@ -131,38 +134,59 @@ module _ where
   m≤n⇒m+k≡n ℕ.z≤n       = _ , ≡.refl
   m≤n⇒m+k≡n (ℕ.s≤s m≤n) = P.dmap id (≡.cong suc) (m≤n⇒m+k≡n m≤n)
 
-  slicedSize : ∀ i j (off : Fin (suc i)) → P.∃ λ k → i ℕ.+ j ≡ Fin.toℕ off ℕ.+ (j ℕ.+ k)
-  slicedSize i j off = k , (begin
-    i ℕ.+ j                   ≡˘⟨ ≡.cong (ℕ._+ j) (P.proj₂ off+k≤i) ⟩
-    (Fin.toℕ off ℕ.+ k) ℕ.+ j ≡⟨  ℕₚ.+-assoc (Fin.toℕ off) k j ⟩
-    Fin.toℕ off ℕ.+ (k ℕ.+ j) ≡⟨  ≡.cong (Fin.toℕ off ℕ.+_) (ℕₚ.+-comm k j) ⟩
-    Fin.toℕ off ℕ.+ (j ℕ.+ k) ∎)
+  slicedSize : ∀ n m (i : Fin (suc n)) → P.∃ λ k → n ℕ.+ m ≡ Fin.toℕ i ℕ.+ (m ℕ.+ k) × Fin.toℕ i ℕ.+ k ≡ n
+  slicedSize n m i = k , (begin
+    n ℕ.+ m                   ≡˘⟨ ≡.cong (ℕ._+ m) (P.proj₂ i+k≡n) ⟩
+    (Fin.toℕ i ℕ.+ k) ℕ.+ m ≡⟨  ℕₚ.+-assoc (Fin.toℕ i) k m ⟩
+    Fin.toℕ i ℕ.+ (k ℕ.+ m) ≡⟨  ≡.cong (Fin.toℕ i ℕ.+_) (ℕₚ.+-comm k m) ⟩
+    Fin.toℕ i ℕ.+ (m ℕ.+ k) ∎) ,
+    P.proj₂ i+k≡n
     where
     open ≡-Reasoning
-    off+k≤i = m≤n⇒m+k≡n (ℕₚ.≤-pred (Finₚ.toℕ<n off))
-    k = P.proj₁ off+k≤i
-
-  sliced : ∀ t {i j} → ⟦ asType t (i ℕ.+ j) ⟧ₜ → ⟦ fin (suc i) ⟧ₜ → ⟦ asType t j ⟧ₜ
-  sliced t {i} {j} x off = take t j (drop t (Fin.toℕ off) (casted t (P.proj₂ (slicedSize i j off)) x))
+    i+k≡n = m≤n⇒m+k≡n (ℕₚ.≤-pred (Finₚ.toℕ<n i))
+    k = P.proj₁ i+k≡n
 
-updateSliced : ∀ {a} {A : Set a} t {i j} → ⟦ asType t (i ℕ.+ j) ⟧ₜ → ⟦ fin (suc i) ⟧ₜ → ⟦ asType t j ⟧ₜ → (⟦ asType t (i ℕ.+ j) ⟧ₜ → A) → A
-updateSliced t {i} {j} orig off v f = f (casted t (≡.sym eq) (join t (join t untaken v) dropped))
-  where
-  eq = P.proj₂ (slicedSize i j off)
-  dropped = take t (Fin.toℕ off) (casted t eq orig)
-  untaken = drop t j (drop t (Fin.toℕ off) (casted t eq orig))
+  -- 0 of x is i of result
+  spliced : ∀ t {m n} → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ → ⟦ fin (suc n) ⟧ₜ → ⟦ asType t (n ℕ.+ m) ⟧ₜ
+  spliced t {m} x y i = casted t eq (join t (join t high x) low)
+    where
+    reasoning = slicedSize _ m i
+    k = P.proj₁ reasoning
+    n≡i+k = ≡.sym (P.proj₂ (P.proj₂ reasoning))
+    low = take t (Fin.toℕ i) (casted t n≡i+k y)
+    high = drop t (Fin.toℕ i) (casted t n≡i+k y)
+    eq = ≡.sym (P.proj₁ (P.proj₂ reasoning))
+
+  sliced : ∀ t {m n} → ⟦ asType t (n ℕ.+ m) ⟧ₜ → ⟦ fin (suc n) ⟧ₜ → ⟦ asType t m ∷ asType t n ∷ [] ⟧ₜ′
+  sliced t {m} x i = middle , casted t i+k≡n (join t high low)
+    where
+    reasoning = slicedSize _ m i
+    k = P.proj₁ reasoning
+    i+k≡n = P.proj₂ (P.proj₂ reasoning)
+    eq = P.proj₁ (P.proj₂ reasoning)
+    low = take t (Fin.toℕ i) (casted t eq x)
+    middle = take t m (drop t (Fin.toℕ i) (casted t eq x))
+    high = drop t m (drop t (Fin.toℕ i) (casted t eq x))
+
+box : ∀ t → ⟦ elemType t ⟧ₜ → ⟦ asType t 1 ⟧ₜ
+box bits      v = v VecF.∷ VecF.[]
+box (array t) v = v ∷ []
+
+unboxed : ∀ t → ⟦ asType t 1 ⟧ₜ → ⟦ elemType t ⟧ₜ
+unboxed bits      v        = v (Fin.zero)
+unboxed (array t) (v ∷ []) = v
 
 neg : ∀ {t} → IsNumeric t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ
 neg int  x = ℤ.- x
 neg real x = ℝ.- x
 
-add : ∀ {t₁ t₂} (isNum₁ : True (isNumeric? t₁)) (isNum₂ : True (isNumeric? t₂)) → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ combineNumeric t₁ t₂ {isNum₁} {isNum₂} ⟧ₜ
+add : ∀ {t₁ t₂} (isNum₁ : True (isNumeric? t₁)) (isNum₂ : True (isNumeric? t₂)) → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ combineNumeric t₁ t₂ isNum₁ isNum₂ ⟧ₜ
 add {t₁ = int}  {t₂ = int}  _ _ x y = x ℤ.+ y
 add {t₁ = int}  {t₂ = real} _ _ x y = x /1 ℝ.+ y
 add {t₁ = real} {t₂ = int}  _ _ x y = x ℝ.+ y /1
 add {t₁ = real} {t₂ = real} _ _ x y = x ℝ.+ y
 
-mul : ∀ {t₁ t₂} (isNum₁ : True (isNumeric? t₁)) (isNum₂ : True (isNumeric? t₂)) → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ combineNumeric t₁ t₂ {isNum₁} {isNum₂} ⟧ₜ
+mul : ∀ {t₁ t₂} (isNum₁ : True (isNumeric? t₁)) (isNum₂ : True (isNumeric? t₂)) → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ combineNumeric t₁ t₂ isNum₁ isNum₂ ⟧ₜ
 mul {t₁ = int}  {t₂ = int}  _ _ x y = x ℤ.* y
 mul {t₁ = int}  {t₂ = real} _ _ x y = x /1 ℝ.* y
 mul {t₁ = real} {t₂ = int}  _ _ x y = x ℝ.* y /1
@@ -186,11 +210,12 @@ module Expression
   ⟦_⟧ˢ : ∀ {n} {Γ : Vec Type n} → Statement Γ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′
   ⟦_⟧ᶠ : ∀ {n} {Γ : Vec Type n} {ret} → Function Γ ret → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ ret ⟧ₜ
   ⟦_⟧ᵖ : ∀ {n} {Γ : Vec Type n} → Procedure Γ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′
+  ⟦_⟧ᵉ′ : ∀ {n} {Γ : Vec Type n} {m ts} → All (Expression Γ) ts → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ tuple m ts ⟧ₜ
   update : ∀ {n Γ t e} → CanAssign {n} {Γ} {t} e → ⟦ t ⟧ₜ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′
 
   ⟦ lit x ⟧ᵉ σ γ = 𝒦 x
-  ⟦ state i ⟧ᵉ σ γ = fetch Σ σ (# i)
-  ⟦_⟧ᵉ {Γ = Γ} (var i) σ γ = fetch Γ γ (# i)
+  ⟦ state i ⟧ᵉ σ γ = fetch Σ σ i
+  ⟦_⟧ᵉ {Γ = Γ} (var i) σ γ = fetch Γ γ i
   ⟦ abort e ⟧ᵉ σ γ = case ⟦ e ⟧ᵉ σ γ of λ ()
   ⟦ _≟_ {hasEquality = hasEq} e e₁ ⟧ᵉ σ γ = equal (toWitness hasEq) (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ)
   ⟦ _<?_ {isNumeric = isNum} e e₁ ⟧ᵉ σ γ = comp (toWitness isNum) (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ)
@@ -200,10 +225,10 @@ module Expression
   ⟦ not e ⟧ᵉ σ γ = Bits.¬_ (⟦ e ⟧ᵉ σ γ)
   ⟦ e and e₁ ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ Bits.∧ ⟦ e₁ ⟧ᵉ σ γ
   ⟦ e or e₁ ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ Bits.∨ ⟦ e₁ ⟧ᵉ σ γ
-  ⟦ [ e ] ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ Vec.∷ []
-  ⟦ unbox e ⟧ᵉ σ γ = Vec.head (⟦ e ⟧ᵉ σ γ)
-  ⟦ _∶_ {t = t} e e₁ ⟧ᵉ σ γ = join t (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ)
-  ⟦ slice {t = t} e e₁ ⟧ᵉ σ γ = sliced t (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ)
+  ⟦ [_] {t = t} e ⟧ᵉ σ γ = box t (⟦ e ⟧ᵉ σ γ)
+  ⟦ unbox {t = t} e ⟧ᵉ σ γ = unboxed t (⟦ e ⟧ᵉ σ γ)
+  ⟦ splice {t = t} e e₁ e₂ ⟧ᵉ σ γ = spliced t (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ) (⟦ e₂ ⟧ᵉ σ γ)
+  ⟦ cut {t = t} e e₁ ⟧ᵉ σ γ = sliced t (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ)
   ⟦ cast {t = t} eq e ⟧ᵉ σ γ = casted t eq (⟦ e ⟧ᵉ σ γ)
   ⟦ -_ {isNumeric = isNum} e ⟧ᵉ σ γ = neg (toWitness isNum) (⟦ e ⟧ᵉ σ γ)
   ⟦ _+_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁ ⟧ᵉ σ γ = add isNum₁ isNum₂ (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ)
@@ -219,17 +244,23 @@ module Expression
     apply {suc k} {_ ∷ ms} f xs =
       apply (λ x → f (tupHead (Vec.map fin ms) xs ∷ x)) (tupTail (Vec.map fin ms) xs)
   ⟦ asInt e ⟧ᵉ σ γ = Fin.toℕ (⟦ e ⟧ᵉ σ γ) ℤ′.×′ 1ℤ
-  ⟦ tup [] ⟧ᵉ σ γ = _
-  ⟦ tup (e ∷ []) ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ
-  ⟦ tup (e ∷ e′ ∷ es) ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ , ⟦ tup (e′ ∷ es) ⟧ᵉ σ γ
-  ⟦ call f e ⟧ᵉ σ γ = ⟦ f ⟧ᶠ σ (⟦ e ⟧ᵉ σ γ)
+  ⟦ nil ⟧ᵉ σ γ = _
+  ⟦ cons {ts = ts} e e₁ ⟧ᵉ σ γ = tupCons ts (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ)
+  ⟦ head {ts = ts} e ⟧ᵉ σ γ = tupHead ts (⟦ e ⟧ᵉ σ γ)
+  ⟦ tail {ts = ts} e ⟧ᵉ σ γ = tupTail ts (⟦ e ⟧ᵉ σ γ)
+  ⟦ call f e ⟧ᵉ σ γ = ⟦ f ⟧ᶠ σ (⟦ e ⟧ᵉ′ σ γ)
   ⟦ if e then e₁ else e₂ ⟧ᵉ σ γ = Bool.if ⟦ e ⟧ᵉ σ γ then ⟦ e₁ ⟧ᵉ σ γ else ⟦ e₂ ⟧ᵉ σ γ
 
+  ⟦ [] ⟧ᵉ′          σ γ = _
+  ⟦ e ∷ [] ⟧ᵉ′      σ γ = ⟦ e ⟧ᵉ σ γ
+  ⟦ e ∷ e′ ∷ es ⟧ᵉ′ σ γ = ⟦ e ⟧ᵉ σ γ , ⟦ e′ ∷ es ⟧ᵉ′ σ γ
+
   ⟦ s ∙ s₁ ⟧ˢ σ γ = P.uncurry ⟦ s ⟧ˢ (⟦ s ⟧ˢ σ γ)
   ⟦ skip ⟧ˢ σ γ = σ , γ
   ⟦ _≔_ ref {canAssign = canAssign} e ⟧ˢ σ γ = update (toWitness canAssign) (⟦ e ⟧ᵉ σ γ) σ γ
   ⟦_⟧ˢ {Γ = Γ} (declare e s) σ γ = P.map₂ (tupTail Γ) (⟦ s ⟧ˢ σ (tupCons Γ (⟦ e ⟧ᵉ σ γ) γ))
-  ⟦ invoke p e ⟧ˢ σ γ = ⟦ p ⟧ᵖ σ (⟦ e ⟧ᵉ σ γ) , γ
+  ⟦ invoke p e ⟧ˢ σ γ = ⟦ p ⟧ᵖ σ (⟦ e ⟧ᵉ′ σ γ) , γ
+  ⟦ if e then s₁ ⟧ˢ σ γ = Bool.if ⟦ e ⟧ᵉ σ γ then ⟦ s₁ ⟧ˢ σ γ else (σ , γ)
   ⟦ if e then s₁ else s₂ ⟧ˢ σ γ = Bool.if ⟦ e ⟧ᵉ σ γ then ⟦ s₁ ⟧ˢ σ γ else ⟦ s₂ ⟧ˢ σ γ
   ⟦_⟧ˢ {Γ = Γ} (for m s) σ γ = helper m ⟦ s ⟧ˢ σ γ
     where
@@ -246,20 +277,23 @@ module Expression
   ⟦_⟧ᶠ {Γ = Γ} (declare e f) σ γ = ⟦ f ⟧ᶠ σ (tupCons Γ (⟦ e ⟧ᵉ σ γ) γ)
 
   ⟦ s ∙end ⟧ᵖ σ γ = P.proj₁ (⟦ s ⟧ˢ σ γ)
-  ⟦_⟧ᵖ {Γ = Γ} (declare e p) σ γ = ⟦ p ⟧ᵖ σ (tupCons Γ (⟦ e ⟧ᵉ σ γ) γ)
-
-  update (state i {i<o}) v σ γ = updateAt Σ (#_ i {m<n = i<o}) v σ , γ
-  update {Γ = Γ} (var i {i<n}) v σ γ = σ , updateAt Γ (#_ i {m<n = i<n}) v γ
-  update abort v σ γ = σ , γ
-  update (_∶_ {m = m} {t = t} e e₁) v σ γ = do
-    let σ′ , γ′ = update e (sliced t v (Fin.fromℕ _)) σ γ
-    update e₁ (sliced t (casted t (ℕₚ.+-comm _ m) v) zero) σ′ γ′
-  update [ e ] v σ γ = update e (Vec.head v) σ γ
-  update (unbox e) v σ γ = update e (v ∷ []) σ γ
-  update (slice {t = t} {e₁ = e₁} a e₂) v σ γ = updateSliced t (⟦ e₁ ⟧ᵉ σ γ) (⟦ e₂ ⟧ᵉ σ γ) v (λ v → update a v σ γ)
+
+  update (state i) v σ γ = updateAt Σ i v σ , γ
+  update {Γ = Γ} (var i) v σ γ = σ , updateAt Γ i v γ
+  update (abort _) v σ γ = σ , γ
+  update ([_] {t = t} e) v σ γ = update e (unboxed t v) σ γ
+  update (unbox {t = t} e) v σ γ = update e (box t v) σ γ
+  update (splice {m = m} {t = t} e e₁ e₂) v σ γ = do
+    let i = ⟦ e₂ ⟧ᵉ σ γ
+    let σ′ , γ′ = update e (P.proj₁ (sliced t v i)) σ γ
+    update e₁ (P.proj₂ (sliced t v i)) σ′ γ′
+  update (cut {t = t} a e₂) v σ γ = do
+    let i = ⟦ e₂ ⟧ᵉ σ γ
+    update a (spliced t (P.proj₁ v) (P.proj₂ v) i) σ γ
   update (cast {t = t} eq e) v σ γ = update e (casted t (≡.sym eq) v) σ γ
-  update (tup {es = []} x) v σ γ = σ , γ
-  update (tup {es = _ ∷ []} (x ∷ [])) v σ γ = update x v σ γ
-  update (tup {es = _ ∷ _ ∷ _} (x ∷ xs)) (v , vs) σ γ = do
-    let σ′ , γ′ = update x v σ γ
-    update (tup xs) vs σ′ γ′
+  update nil v σ γ = σ , γ
+  update (cons {ts = ts} e e₁) vs σ γ = do
+    let σ′ , γ′ = update e (tupHead ts vs) σ γ
+    update e₁ (tupTail ts vs) σ′ γ′
+  update (head {ts = ts} {e = e} a) v σ γ = update a (tupCons ts v (tupTail ts (⟦ e ⟧ᵉ σ γ))) σ γ
+  update (tail {ts = ts} {e = e} a) v σ γ = update a (tupCons ts (tupHead ts (⟦ e ⟧ᵉ σ γ)) v) σ γ