Define pseudocode for a number of instructions.

5 files changed, 367 insertions, 471 deletions

diff --git a/src/Helium/Data/Pseudocode.agda b/src/Helium/Data/Pseudocode.agda
new file mode 100644
index 0000000..9e4707d
--- /dev/null
+++ b/src/Helium/Data/Pseudocode.agda
@@ -0,0 +1,321 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Definition of instructions using the Armv8-M pseudocode.
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+module Helium.Data.Pseudocode 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.Nat as ℕ using (ℕ; zero; suc)
+import Data.Nat.Properties as ℕₚ
+open import Data.Sum using ([_,_]′)
+open import Data.Vec as Vec using (Vec; []; _∷_)
+open import Data.Vec.Relation.Unary.All using (All; []; _∷_)
+open import Function using (_$_)
+open import Helium.Data.Pseudocode.Core as Core public
+  hiding (module Code)
+import Helium.Instructions as Instr
+import Relation.Binary.PropositionalEquality as P
+open import Relation.Nullary.Decidable.Core using (True)
+
+--- Types
+
+beat : Type
+beat = fin 4
+
+elmtMask : Type
+elmtMask = bits 4
+
+--- State
+
+State : Vec Type _
+State = array (bits 32) 32      -- S
+      ∷ array (bits 32) 16      -- R
+      ∷ bits 16                 -- VPR-P0
+      ∷ bits 8                  -- VPR-mask
+      ∷ bit                     -- FPSCR-QC
+      ∷ bool                    -- _AdvanceVPTState
+      ∷ beat                    -- _BeatId
+      ∷ []
+
+open Core.Code State public
+
+--- References
+
+-- Direct from State
+
+S : ∀ {n Γ} → Expression {n} Γ (array (bits 32) 32)
+S = state 0
+
+R : ∀ {n Γ} → Expression {n} Γ (array (bits 32) 16)
+R = state 1
+
+VPR-P0 : ∀ {n Γ} → Expression {n} Γ (bits 16)
+VPR-P0 = state 2
+
+VPR-mask : ∀ {n Γ} → Expression {n} Γ (bits 8)
+VPR-mask = state 3
+
+FPSCR-QC : ∀ {n Γ} → Expression {n} Γ bit
+FPSCR-QC = state 4
+
+AdvanceVPTState : ∀ {n Γ} → Expression {n} Γ bool
+AdvanceVPTState = state 5
+
+BeatId : ∀ {n Γ} → Expression {n} Γ beat
+BeatId = state 6
+
+-- Indirect
+
+tup⇒array : ∀ {n Γ t m} → Expression {n} Γ (tuple (suc m) (Vec.replicate t)) → Expression Γ (array t (suc m))
+tup⇒array {m = zero}  xs = [ head xs ]
+tup⇒array {m = suc m} xs = [ head xs ] ∶ tup⇒array (tail xs)
+
+group : ∀ {n Γ t k} m → Expression {n} Γ (asType t (k ℕ.* suc m)) → Expression Γ (array (asType t k) (suc m))
+group {k = k} zero    x = [ cast (P.trans (ℕₚ.*-comm k 1) (ℕₚ.+-comm k 0)) x ]
+group {k = k} (suc m) x = [ slice (cast (ℕₚ.+-comm k _) x′) (lit (zero ′f)) ] ∶ group m (slice (cast (P.cong (k ℕ.+_) (ℕₚ.*-comm (suc m) k)) x′) (lit (Fin.fromℕ k ′f)))
+  where
+  x′ = cast (ℕₚ.*-comm k (suc (suc m))) x
+
+join : ∀ {n Γ t k m} → Expression {n} Γ (array (asType t k) (suc m)) → Expression Γ (asType t (k ℕ.* suc m))
+join {k = k} {zero}  x = cast (P.trans (ℕₚ.+-comm 0 k) (ℕₚ.*-comm 1 k)) (unbox x)
+join {k = k} {suc m} x = cast eq (unbox (slice {i = suc m} (cast (ℕₚ.+-comm 1 (suc m)) x) (lit (zero ′f))) ∶ join (slice x (lit (Fin.fromℕ 1 ′f))))
+  where
+  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)
+
+Q : ∀ {n Γ} → Expression {n} Γ (array (array (bits 32) 4) 8)
+Q = group 7 S
+
+elem : ∀ {n Γ t k} m → Expression {n} Γ (asType t (k ℕ.* m)) → Expression Γ (fin k) → Expression Γ (asType t m)
+elem {k = zero}  m       x i = abort i
+elem {k = suc k} zero    x i = cast (ℕₚ.*-comm k 0) x
+elem {k = suc k} (suc m) x i = index (group k (cast (ℕₚ.*-comm (suc k) (suc m)) x)) i
+
+--- 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)
+
+sliceⁱ : ∀ {n Γ m} → ℕ → Expression {n} Γ int → Expression Γ (bits m)
+sliceⁱ {m = zero}  n i = lit ([] ′x)
+sliceⁱ {m = suc m} n i = get (m ℕ.+ n) i ∶ sliceⁱ n i
+
+--- Functions
+
+Int : ∀ {n} → Function (bits n ∷ bool ∷ []) int
+Int = skip ∙return (if var 1 then uint (var 0) else sint (var 0))
+
+-- arguments swapped, pred n
+SignedSatQ : ∀ n → Function (int ∷ []) (tuple 2 (bits (suc n) ∷ bool ∷ []))
+SignedSatQ n = declare (lit (true ′b)) (
+  if max <? var 1
+  then
+    var 1 ≔ max
+  else if var 1 <? min
+  then
+    var 1 ≔ min
+  else
+    var 0 ≔ lit (false ′b)
+  ∙return tup (sliceⁱ 0 (var 1) ∷ var 0 ∷ []))
+  where
+  max = lit (2 ′i) ^ lit (n ′i) + - lit (1 ′i)
+  min = - (lit (2 ′i) ^ lit (n ′i))
+
+-- 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))
+  (skip ∙return tup
+    ( slice (cast (ℕₚ.+-comm n _) (var 0)) (lit (zero ′f))
+    ∷ slice (cast eq₂ (var 0)) (lit (Fin.inject+ shift (Fin.fromℕ n) ′f))
+    ∷ []))
+  where
+  eq₂ = P.trans (P.cong (n ℕ.+_) (ℕₚ.+-comm 1 shift)) (P.sym (ℕₚ.+-assoc n shift 1))
+
+--- Procedures
+
+private
+  div2 : All Fin (4 ∷ []) → Fin 2
+  div2 (zero        ∷ []) = zero
+  div2 (suc zero    ∷ []) = zero
+  div2 (suc (suc i) ∷ []) = suc zero
+
+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)
+    then
+      elem 8 (index (index Q (var 1)) (var 3)) (var 0) ≔ elem 8 (var 2) (var 0)
+    else skip
+  ) ∙end
+
+VPTAdvance : Procedure (beat ∷ [])
+VPTAdvance = declare (fin div2 (tup (var 0 ∷ []))) (
+  declare (elem 4 VPR-mask (var 0)) (
+    -- 0:vptState 1:maskId 2:beat
+    if var 0 ≟ lit ((true ∷ false ∷ false ∷ false ∷ []) ′x)
+    then
+      var 0 ≔ lit (Vec.replicate false ′x)
+    else if inv (var 0 ≟ lit (Vec.replicate false ′x))
+    then (
+      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)
+        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)
+    then
+      elem 4 VPR-mask (var 1) ≔ var 0
+    else skip
+    ∙end))
+
+VPTActive : Function (beat ∷ []) bool
+VPTActive = skip ∙return inv (elem 4 VPR-mask (fin div2 (tup (var 0 ∷ []))) ≟ lit (Vec.replicate false ′x))
+
+GetCurInstrBeat : Function [] (tuple 2 (beat ∷ elmtMask ∷ []))
+GetCurInstrBeat = declare (lit (Vec.replicate true ′x)) (
+  -- 0:elmtMask 1:beat
+  if call VPTActive (tup (BeatId ∷ []))
+  then
+    var 0 ≔ var 0 and elem 4 VPR-P0 BeatId
+  else skip
+  ∙return tup (BeatId ∷ var 0 ∷ []))
+
+-- Assumes:
+--   MAX_OVERLAPPING_INSTRS = 1
+--   _InstInfo[0].Valid = 1
+--   BEATS_PER_TICK = 4
+--   procedure argument is action of DecodeExecute
+-- and more!
+ExecBeats : Procedure [] → Procedure []
+ExecBeats DecodeExec =
+  for 4 (
+    -- 0:beatId
+    BeatId ≔ var 0 ∙
+    AdvanceVPTState ≔ lit (true ′b) ∙
+    invoke DecodeExec (tup []) ∙
+    if AdvanceVPTState
+    then
+      invoke VPTAdvance (tup (var 0 ∷ []))
+    else skip)
+  ∙end
+
+from32 : ∀ size {n Γ} → Expression {n} Γ (bits 32) → Expression Γ (array (bits (toℕ (Instr.Size.esize size))) (toℕ (Instr.Size.elements size)))
+from32 Instr.8bit  = group 3
+from32 Instr.16bit = group 1
+from32 Instr.32bit = group 0
+
+to32 : ∀ size {n Γ} → Expression {n} Γ (array (bits (toℕ (Instr.Size.esize size))) (toℕ (Instr.Size.elements size))) → Expression Γ (bits 32)
+to32 Instr.8bit  = join
+to32 Instr.16bit = join
+to32 Instr.32bit = join
+
+module _ (d : Instr.VecOp₂) where
+  open Instr.VecOp₂ d
+
+  vec-op₂ : Function (bits (toℕ esize) ∷ bits (toℕ esize) ∷ []) (bits (toℕ esize)) → Procedure []
+  vec-op₂ op =
+    declare (lit (zero ′f)) (
+    declare (lit (Vec.replicate false ′x)) (
+    -- 0:elmtMask 1:curBeat
+    tup (var 1 ∷ var 0 ∷ []) ≔ call GetCurInstrBeat (tup []) ∙
+    declare (lit (Vec.replicate (Vec.replicate false ′x) ′a)) (
+    declare (from32 size (index (index Q (lit (src₁ ′f))) (var 2))) (
+    -- 0:op₁ 1:result 2:elmtMask 3:curBeat
+    for (toℕ elements) (
+       -- 0:e 1:op₁ 2:result 3:elmtMask 4:curBeat
+      declare op₂ (
+      -- 0:op₂ 1:e 2:op₁ 3:result 4:elmtMask 5:curBeat
+      index (var 3) (var 1) ≔ call op (tup (index (var 2) (var 1) ∷ var 0 ∷ [])))) ∙
+    -- 0:op₁ 1:result 2:elmtMask 3:curBeat
+    invoke copyMasked (tup (lit (dest ′f) ∷ to32 size (var 1) ∷ var 3 ∷ var 2 ∷ []))))
+    ∙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₂
+
+vadd : Instr.VAdd → Procedure []
+vadd d = vec-op₂ d (skip ∙return sliceⁱ 0 (uint (var 0) + uint (var 1)))
+
+vsub : Instr.VSub → Procedure []
+vsub d = vec-op₂ d (skip ∙return sliceⁱ 0 (uint (var 0) - uint (var 1)))
+
+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) ∷ []))
+
+vmul : Instr.VMul → Procedure []
+vmul d = vec-op₂ d (skip ∙return sliceⁱ 0 (sint (var 0) * sint (var 1)))
+
+vmulh : Instr.VMulH → Procedure []
+vmulh d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0) * toInt (var 1)))
+  where
+  open Instr.VMulH d; toInt = λ i → call Int (tup (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) << lit (toℕ esize-1 ′i)))
+  where
+  open Instr.VRMulH d; toInt = λ i → call Int (tup (i ∷ lit (unsigned ′b) ∷ []))
+
+private
+  vqr?dmulh : Instr.VQDMulH → Function (int ∷ int ∷ []) int → Procedure []
+  vqr?dmulh d f =
+    declare (lit (zero ′f)) (
+    declare (lit (Vec.replicate false ′x)) (
+    -- 0:elmtMask 1:curBeat
+    tup (var 1 ∷ var 0 ∷ []) ≔ call GetCurInstrBeat (tup []) ∙
+    declare (lit (Vec.replicate (Vec.replicate false ′x) ′a)) (
+    declare (from32 size (index (index Q (lit (src₁ ′f))) (var 2))) (
+    -- 0:op₁ 1:result 2:elmtMask 3:curBeat
+    for (toℕ elements) (
+       -- 0:e 1:op₁ 2:result 3:elmtMask 4:curBeat
+      declare op₂ (
+      -- 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) ∷ []))) (
+      -- 0:value 1:op₂ 2:e 3:op₁ 4:result 5:elmtMask 6:curBeat
+      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 ∷ [])))
+      then
+        FPSCR-QC ≔ lit ((true ∷ []) ′x)
+      else skip)))) ∙
+    -- 0:op₁ 1:result 2:elmtMask 3:curBeat
+    invoke copyMasked (tup (lit (dest ′f) ∷ to32 size (var 1) ∷ var 3 ∷ var 2 ∷ []))))
+    ∙end))
+      where
+      open Instr.VecOp₂ d
+      -- 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₂
+
+      e*esize>>3 : All Fin (toℕ elements ∷ []) → Fin 4
+      e*esize>>3 (x ∷ []) = helper size x
+        where
+        helper : ∀ size → Fin′ (Instr.Size.elements size) → Fin 4
+        helper Instr.8bit  i = Fin.combine i (zero {0})
+        helper Instr.16bit i = Fin.combine i (zero {1})
+        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 >> lit (toℕ esize ′i))
+  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) << lit (toℕ esize-1 ′i)) >> lit (toℕ esize ′i))
+  where open Instr.VecOp₂ d using (esize; esize-1)
diff --git a/src/Helium/Data/Pseudocode/Core.agda b/src/Helium/Data/Pseudocode/Core.agda
index 68b5449..7b21824 100644
--- a/src/Helium/Data/Pseudocode/Core.agda
+++ b/src/Helium/Data/Pseudocode/Core.agda
@@ -96,6 +96,7 @@ data Literal : Type → Set where
   _′r : ℕ → Literal real
   _′x : ∀ {n} → Vec Bool n → Literal (bits n)
   _′e : ∀ {n} → Fin n → Literal (enum n)
+  _′a : ∀ {n t} → Vec (Literal t) n → Literal (array t n)
 
 --- Expressions, references, statements, functions and procedures
 
@@ -147,6 +148,7 @@ module Code {o} (Σ : Vec Type o) where
     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 → Expression Γ (tuple 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})
@@ -193,6 +195,7 @@ module Code {o} (Σ : Vec Type o) where
   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)
@@ -218,3 +221,14 @@ module Code {o} (Σ : Vec Type o) where
   data Procedure Γ where
     _∙end   : Statement Γ unit → Procedure Γ
     declare : ∀ {t} → Expression Γ t → Procedure (t ∷ Γ) → Procedure Γ
+
+  infixl  6 _<<_ _>>_
+  infixl 5 _-_
+  _-_   : ∀ {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 → Expression Γ int
+  x << n = rnd (x * lit (2 ′r) ^ n)
+
+  _>>_ : ∀ {n Γ} → Expression {n} Γ int → Expression Γ int → Expression Γ int
+  x >> n = rnd (x * lit (2 ′r) ^ - n)
diff --git a/src/Helium/Instructions.agda b/src/Helium/Instructions.agda
index 41bc74d..ebe3f32 100644
--- a/src/Helium/Instructions.agda
+++ b/src/Helium/Instructions.agda
@@ -21,45 +21,42 @@ GenReg = Fin 16
 VecReg : Set
 VecReg = Fin 8
 
-record VecOp₂ : Set where
-  field
-    size : Fin 3
-    dest : VecReg
-    src₁ : VecReg
-    src₂ : GenReg ⊎ VecReg
-
-  private
-    split32 : ∃ λ (elements : Fin 5) → ∃ λ (esize>>3-1 : Fin 4) → ∃ λ (esize-1 : Fin 32) → (8 * toℕ (suc esize>>3-1) ≡ toℕ (suc esize-1)) × (toℕ elements * toℕ (suc esize-1) ≡ 32) × (toℕ elements * toℕ (suc esize>>3-1) ≡ 4)
-    split32 = helper size
-      where
-      helper : _ → _
-      helper zero             = # 4 , # 0 , # 7 , refl , refl , refl
-      helper (suc zero)       = # 2 , # 1 , # 15 , refl , refl , refl
-      helper (suc (suc zero)) = # 1 , # 3 , # 31 , refl , refl , refl
+data VecOpSize : Set where
+  8bit  : VecOpSize
+  16bit : VecOpSize
+  32bit : VecOpSize
+
+module Size (size : VecOpSize) where
+  elements-1 : Fin 4
+  elements-1 = helper size
+    where
+    helper : VecOpSize → Fin 4
+    helper 8bit  = # 3
+    helper 16bit = # 1
+    helper 32bit = # 0
 
   elements : Fin 5
-  elements with (elmt , _ ) ← split32 = elmt
-
-  esize>>3-1 : Fin 4
-  esize>>3-1 with (_ , esize>>3-1 , _) ← split32 = esize>>3-1
-
-  esize>>3 : Fin 5
-  esize>>3 = suc esize>>3-1
+  elements = suc elements-1
 
   esize-1 : Fin 32
-  esize-1 with (_ , _ , esize-1 , _) ← split32 = esize-1
+  esize-1 = helper size
+    where
+    helper : VecOpSize → Fin 32
+    helper 8bit  = # 7
+    helper 16bit = # 15
+    helper 32bit = # 31
 
   esize : Fin 33
   esize = suc esize-1
 
-  8*e>>3≡e : 8 * toℕ esize>>3 ≡ toℕ esize
-  8*e>>3≡e with (_ , _ , _ , eq , _) ← split32 = eq
-
-  e*e≡32 : toℕ elements * toℕ esize ≡ 32
-  e*e≡32 with (_ , _ , _ , _ , eq , _) ← split32 = eq
+record VecOp₂ : Set where
+  field
+    size : VecOpSize
+    dest : VecReg
+    src₁ : VecReg
+    src₂ : GenReg ⊎ VecReg
 
-  e*e>>3≡4 : toℕ elements * toℕ esize>>3 ≡ 4
-  e*e>>3≡4 with (_ , _ , _ , _ , _ , eq) ← split32 = eq
+  open Size size public
 
 VAdd = VecOp₂
 
@@ -78,17 +75,19 @@ record VMulH : Set where
   field
     op₂ : VecOp₂
     unsigned : Bool
-    rounding : Bool
 
   open VecOp₂ op₂ public
 
-record VQDMulH : Set where
+record VRMulH : Set where
   field
     op₂ : VecOp₂
-    rounding : Bool
+    unsigned : Bool
 
   open VecOp₂ op₂ public
 
+VQDMulH = VecOp₂
+VQRDMulH = VecOp₂
+
 data Instruction : Set where
   vadd : VAdd → Instruction
   vsub : VSub → Instruction
diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda
deleted file mode 100644
index 8e521ea..0000000
--- a/src/Helium/Semantics/Denotational.agda
+++ /dev/null
@@ -1,310 +0,0 @@
-------------------------------------------------------------------------
--- Agda Helium
---
--- Denotational semantics of Armv8-M instructions.
-------------------------------------------------------------------------
-
-{-# OPTIONS --safe --without-K #-}
-
-open import Helium.Data.Pseudocode.Types
-
-module Helium.Semantics.Denotational
-  {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
-  (pseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃)
-  where
-
-open import Algebra.Core using (Op₂)
-open import Data.Bool as Bool using (Bool; true; false)
-open import Data.Fin as Fin hiding (cast; lift; _+_)
-import Data.Fin.Properties as Finₚ
-import Data.List as List
-open import Data.Nat hiding (_⊔_)
-import Data.Nat.Properties as ℕₚ
-open import Data.Product using (∃; _×_; _,_; dmap)
-open import Data.Sum using ([_,_]′)
-open import Data.Vec.Functional as V using (Vector; []; _∷_)
-open import Function using (_|>_; _$_; _∘₂_)
-open import Function.Nary.NonDependent.Base
-import Helium.Instructions as Instr
-import Helium.Semantics.Denotational.Core as Core
-open import Level using (Level; _⊔_)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong)
-open import Relation.Nullary using (does)
-open import Relation.Nullary.Decidable
-
-open RawPseudocode pseudocode
-
-private
-  ℓ : Level
-  ℓ = b₁
-
-record State : Set ℓ where
-  field
-    S : Vector (Bits 32) 32
-    R : Vector (Bits 32) 16
-    P0 : Bits 16
-    mask : Bits 8
-    QC : Bit
-    advanceVPT : Bool
-
-open Core State
-
-Beat : Set
-Beat = Fin 4
-
-hilow : Beat → Fin 2
-hilow zero          = zero
-hilow (suc zero)    = zero
-hilow (suc (suc _)) = suc zero
-
-oddeven : Beat → Fin 2
-oddeven zero                   = zero
-oddeven (suc zero)             = suc zero
-oddeven (suc (suc zero))       = zero
-oddeven (suc (suc (suc zero))) = suc zero
-
-ElmtMask : Set b₁
-ElmtMask = Bits 4
-
--- State properties
-
-&R : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ (Fin 16) → Reference n Γ (Bits 32)
-&R e = record
-  { get = λ σ ρ → State.R σ (e σ ρ)
-  ; set = λ x σ ρ → record σ { R = V.updateAt (e σ ρ) (λ _ → x) (State.R σ) } , ρ
-  }
-
-&S : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ (Fin 32) → Reference n Γ (Bits 32)
-&S e = record
-  { get = λ σ ρ → State.S σ (e σ ρ)
-  ; set = λ x σ ρ → record σ { S = V.updateAt (e σ ρ) (λ _ → x) (State.S σ) } , ρ
-  }
-
-&Q : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ Instr.VecReg → Expr n Γ Beat → Reference n Γ (Bits 32)
-&Q reg beat = &S λ σ ρ → combine (reg σ ρ) (beat σ ρ)
-
-&FPSCR-QC : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ Bit
-&FPSCR-QC = record
-  { get = λ σ ρ → State.QC σ
-  ; set = λ x σ ρ → record σ { QC = x } , ρ
-  }
-
-&VPR-P0 : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ (Bits 16)
-&VPR-P0 = record
-  { get = λ σ ρ → State.P0 σ
-  ; set = λ x σ ρ → record σ { P0 = x } , ρ
-  }
-
-&VPR-mask : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ (Bits 8)
-&VPR-mask = record
-  { get = λ σ ρ → State.mask σ
-  ; set = λ x σ ρ → record σ { mask = x } , ρ
-  }
-
-&AdvanceVPT : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ Bool
-&AdvanceVPT = record
-  { get = λ σ ρ → State.advanceVPT σ
-  ; set = λ x σ ρ → record σ { advanceVPT = x } , ρ
-  }
-
--- Reference properties
-
-&cast : ∀ {k m n ls} {Γ : Sets n ls} → .(eq : k ≡ m) → Reference n Γ (Bits k) → Reference n Γ (Bits m)
-&cast eq &v = record
-  { get = λ σ ρ → cast eq (Reference.get &v σ ρ)
-  ; set = λ x σ ρ → Reference.set &v (cast (sym eq) x) σ ρ
-  }
-
-slice : ∀ {k m n ls} {Γ : Sets n ls} → Reference n Γ (Bits m) → Expr n Γ (∃ λ (i : Fin (suc m)) → ∃ λ j → toℕ (i - j) ≡ k) → Reference n Γ (Bits k)
-slice &v idx = record
-  { get = λ σ ρ → let (i , j , i-j≡k) = idx σ ρ in cast i-j≡k (sliceᵇ i j (Reference.get &v σ ρ))
-  ; set = λ v σ ρ →
-    let (i , j , i-j≡k) = idx σ ρ in
-    Reference.set &v (updateᵇ i j (cast (sym (i-j≡k)) v) (Reference.get &v σ ρ)) σ ρ
-  }
-
-elem : ∀ {k n ls} {Γ : Sets n ls} m → Reference n Γ (Bits (k * m)) → Expr n Γ (Fin k) → Reference n Γ (Bits m)
-elem m &v idx = slice &v (λ σ ρ → helper _ _ (idx σ ρ))
-  where
-  helper : ∀ m n → Fin m → ∃ λ (i : Fin (suc (m * n))) → ∃ λ j → toℕ (i - j) ≡ n
-  helper (suc m) n zero    = inject+ (m * n) (fromℕ n) , # 0 , eq
-    where
-    eq = trans (sym (Finₚ.toℕ-inject+ (m * n) (fromℕ n))) (Finₚ.toℕ-fromℕ n)
-  helper (suc m) n (suc i) with x , y , x-y≡n ← helper m n i =
-      u ,
-      v ,
-      trans
-        (cast‿- (raise n x) (Fin.cast eq₂ (raise n y)) eq₁)
-        (trans (raise‿- (suc (m * n)) n x y eq₂) x-y≡n)
-    where
-    eq₁ = ℕₚ.+-suc n (m * n)
-    eq₂ = trans (ℕₚ.+-suc n (toℕ x)) (cong suc (sym (Finₚ.toℕ-raise n x)))
-    eq₂′ = cong suc (sym (Finₚ.toℕ-cast eq₁ (raise n x)))
-    u = Fin.cast eq₁ (raise n x)
-    v = Fin.cast eq₂′ (Fin.cast eq₂ (raise n y))
-
-    raise‿- : ∀ m n (x : Fin m) y .(eq : n + suc (toℕ x) ≡ suc (toℕ (raise n x))) → toℕ (raise n x - Fin.cast eq (raise n y)) ≡ toℕ (x - y)
-    raise‿- m       ℕ.zero  x       zero    _ = refl
-    raise‿- (suc m) ℕ.zero  (suc x) (suc y) p = raise‿- m ℕ.zero x y (ℕₚ.suc-injective p)
-    raise‿- m       (suc n) x       y       p = raise‿- m n x y (ℕₚ.suc-injective p)
-
-    cast‿- : ∀ {m n} (x : Fin m) y .(eq : m ≡ n) → toℕ (Fin.cast eq x - Fin.cast (cong suc (sym (Finₚ.toℕ-cast eq x))) y) ≡ toℕ (x - y)
-    cast‿- {suc m} {suc n} x       zero    eq = Finₚ.toℕ-cast eq x
-    cast‿- {suc m} {suc n} (suc x) (suc y) eq = cast‿- x y (ℕₚ.suc-injective eq)
-
--- General functions
-
-copyMasked : Instr.VecReg → Procedure 3 (Bits 32 , Beat , ElmtMask , _)
-copyMasked dest =
-  for 4 (
-    -- 0:e 1:result 2:beat 3:elmtMask
-    if ⦇ hasBit (!# 0) (!# 3) ⦈
-    then
-      elem 8 (&Q ⦇ dest ⦈ (!# 2)) (!# 0) ≔ ! elem 8 (var (# 1)) (!# 0)
-    else skip)
-  ∙end
-
-module fun-sliceᶻ
-  (1<<n≉0 : ∀ n → False ((1ℤ << n) /1 ≟ʳ 0ℝ))
-  where
-
-  open ShiftNotZero 1<<n≉0
-
-  signedSatQ : ∀ n → Function 1 (ℤ , _) (Bits (suc n) × Bool)
-  signedSatQ n = declare ⦇ true ⦈ $
-    -- 0:sat 1:x
-    if ⦇ (λ i → does ((1ℤ << n) ℤ.+ ℤ.- 1ℤ <ᶻ? i)) (!# 1) ⦈
-    then
-      var (# 1) ≔ ⦇ ((1ℤ << n) ℤ.+ ℤ.- 1ℤ) ⦈
-    else if ⦇ (λ i → does (ℤ.- 1ℤ << n <ᶻ? i)) (!# 1) ⦈
-    then
-      var (# 1) ≔ ⦇ (ℤ.- 1ℤ << n) ⦈
-    else
-      var (# 0) ≔ ⦇ false ⦈
-    ∙return ⦇ ⦇ (sliceᶻ (suc n) zero) (!# 1) ⦈ , (!# 0) ⦈
-
-advanceVPT : Procedure 1 (Beat , _)
-advanceVPT = declare (! elem 4 &VPR-mask (hilow ∘₂ !# 0)) $
-  -- 0:vptState 1:beat
-  if ⦇ (λ x → does (x ≟ᵇ 1𝔹 ∷ zeros)) (!# 0) ⦈
-  then
-    var (# 0) ≔ ⦇ zeros ⦈
-  else if ⦇ (λ x → does (x ≟ᵇ zeros)) (!# 0) ⦈
-  then skip
-  else (
-    if ⦇ (hasBit (# 3)) (!# 0) ⦈
-    then
-      elem 4 &VPR-P0 (!# 1) ⟵ (Bits.¬_)
-    else skip ∙
-    (var (# 0) ⟵ λ x → sliceᵇ (# 3) zero x V.++ 0𝔹 ∷ [])) ∙
-  if ⦇ (λ x → does (oddeven x Finₚ.≟ # 1)) (!# 1) ⦈
-  then
-    elem 4 &VPR-mask (hilow ∘₂ !# 1) ≔ !# 0
-  else skip
-  ∙end
-
-execBeats : Procedure 2 (Beat , ElmtMask , _) → Procedure 0 _
-execBeats inst = declare ⦇ ones ⦈ $
-  for 4 (
-    -- 0:beat 1:elmtMask
-    if ⦇ (λ x → does (x ≟ᵇ zeros)) (! elem 4 &VPR-mask (hilow ∘₂ !# 0)) ⦈
-    then
-      var (# 1) ≔ ⦇ ones ⦈
-    else
-      var (# 1) ≔ ! elem 4 &VPR-P0 (!# 0) ∙
-    &AdvanceVPT ≔ ⦇ true ⦈ ∙
-    invoke inst ⦇ !# 0 , !# 1 ⦈ ∙
-    if ! &AdvanceVPT
-    then
-      invoke advanceVPT (!# 0)
-    else skip)
-  ∙end
-
-module _
-  (d : Instr.VecOp₂)
-  where
-
-  open Instr.VecOp₂ d
-
-  vec-op₂ : Op₂ (Bits (toℕ esize)) → Procedure 2 (Beat , ElmtMask , _)
-  vec-op₂ op = declare ⦇ zeros ⦈ $ declare (! &Q ⦇ src₁ ⦈ (!# 1)) $
-    for (toℕ elements) (
-      -- 0:e 1:op₁ 2:result 3:beat 4:elmntMask
-      elem (toℕ esize) (&cast (sym e*e≡32) (var (# 2))) (!# 0) ≔
-        (⦇ op
-           (! elem (toℕ esize) (&cast (sym e*e≡32) (var (# 1))) (!# 0))
-           ([ (λ src₂ → ! slice (&R ⦇ src₂ ⦈) ⦇ (esize , zero , refl) ⦈)
-            , (λ src₂ → ! elem (toℕ esize) (&cast (sym e*e≡32) (&Q ⦇ src₂ ⦈ (!# 3))) (!# 0))
-            ]′ src₂) ⦈)) ∙
-    invoke (copyMasked dest) ⦇ !# 1 , ⦇ !# 2 , !# 3 ⦈ ⦈
-    ∙end
-
--- Instruction semantics
-
-module _
-  (1<<n≉0 : ∀ n → False ((1ℤ << n) /1 ≟ʳ 0ℝ))
-  where
-
-  open ShiftNotZero 1<<n≉0
-  open fun-sliceᶻ 1<<n≉0
-
-  vadd : Instr.VAdd → Procedure 2 (Beat , ElmtMask , _)
-  vadd d = vec-op₂ d (λ x y → sliceᶻ _ zero (uint x ℤ.+ uint y))
-
-  vsub : Instr.VSub → Procedure 2 (Beat , ElmtMask , _)
-  vsub d = vec-op₂ d (λ x y → sliceᶻ _ zero (uint x ℤ.+ ℤ.- uint y))
-
-  vhsub : Instr.VHSub → Procedure 2 (Beat , ElmtMask , _)
-  vhsub d = vec-op₂ op₂ (λ x y → sliceᶻ _ (suc zero) (int x ℤ.+ ℤ.- int y))
-    where open Instr.VHSub d ; int = Bool.if unsigned then uint else sint
-
-  vmul : Instr.VMul → Procedure 2 (Beat , ElmtMask , _)
-  vmul d = vec-op₂ d (λ x y → sliceᶻ _ zero (sint x ℤ.* sint y))
-
-  vmulh : Instr.VMulH → Procedure 2 (Beat , ElmtMask , _)
-  vmulh d = vec-op₂ op₂ (λ x y → cast (eq _ esize) (sliceᶻ 2esize esize′ (int x ℤ.* int y ℤ.+ rval)))
-    where
-    open Instr.VMulH d
-    int = Bool.if unsigned then uint else sint
-    rval = Bool.if rounding then 1ℤ << toℕ esize-1 else 0ℤ
-    2esize = toℕ esize + toℕ esize
-    esize′ = inject+ _ (strengthen esize)
-    eq : ∀ {n} m (i : Fin n) → toℕ i + m ℕ-ℕ inject+ m (strengthen i) ≡ m
-    eq m zero    = refl
-    eq m (suc i) = eq m i
-
-  vqdmulh : Instr.VQDMulH → Procedure 2 (Beat , ElmtMask , _)
-  vqdmulh d = declare ⦇ zeros ⦈ $ declare (! &Q ⦇ src₁ ⦈ (!# 1)) $ declare ⦇ false ⦈ $
-    for (toℕ elements) (
-      -- 0:e 1:sat 2:op₁ 3:result 4:beat 5:elmntMask
-      elem (toℕ esize) (&cast (sym e*e≡32) (var (# 3))) (!# 0) ,′ var (# 1) ≔
-      call (signedSatQ (toℕ esize-1))
-           ⦇ (λ x y → (2ℤ ℤ.* sint x ℤ.* sint y ℤ.+ rval) >> toℕ esize)
-             (! elem (toℕ esize) (&cast (sym e*e≡32) (var (# 2))) (!# 0))
-             ([ (λ src₂ → ! slice (&R ⦇ src₂ ⦈) ⦇ (esize , zero , refl) ⦈)
-              , (λ src₂ → ! elem (toℕ esize) (&cast (sym e*e≡32) (&Q ⦇ src₂ ⦈ (!# 4))) (!# 0))
-              ]′ src₂) ⦈ ∙
-      if !# 1
-      then if ⦇ (λ m e → hasBit (combine e zero) (cast (sym e*e>>3≡4) m)) (!# 5) (!# 0) ⦈
-      then
-        &FPSCR-QC ≔ ⦇ 1𝔹 ⦈
-      else skip
-      else skip) ∙
-    invoke (copyMasked dest) ⦇ !# 2 , ⦇ !# 3 , !# 4 ⦈ ⦈
-    ∙end
-    where
-    open Instr.VQDMulH d
-    rval = Bool.if rounding then 1ℤ << toℕ esize-1 else 0ℤ
-
-  ⟦_⟧₁ : Instr.Instruction → Procedure 0 _
-  ⟦ Instr.vadd x ⟧₁ = execBeats (vadd x)
-  ⟦ Instr.vsub x ⟧₁ = execBeats (vsub x)
-  ⟦ Instr.vmul x ⟧₁ = execBeats (vmul x)
-  ⟦ Instr.vmulh x ⟧₁ = execBeats (vmulh x)
-  ⟦ Instr.vqdmulh x ⟧₁ = execBeats (vqdmulh x)
-
-  open List using (List; []; _∷_)
-
-  ⟦_⟧ : List (Instr.Instruction) → Procedure 0 _
-  ⟦ [] ⟧     = skip ∙end
-  ⟦ i ∷ is ⟧ = invoke ⟦ i ⟧₁ ⦇ _ ⦈ ∙ invoke ⟦ is ⟧ ⦇ _ ⦈ ∙end
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
deleted file mode 100644
index 9b6a3c8..0000000
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ /dev/null
@@ -1,128 +0,0 @@
-------------------------------------------------------------------------
--- Agda Helium
---
--- Base definitions for the denotational semantics.
-------------------------------------------------------------------------
-
-{-# OPTIONS --safe --without-K #-}
-
-module Helium.Semantics.Denotational.Core
-  {ℓ′}
-  (State : Set ℓ′)
-  where
-
-open import Algebra.Core
-open import Data.Bool as Bool using (Bool)
-open import Data.Fin hiding (lift)
-open import Data.Nat using (ℕ; zero; suc)
-import Data.Nat.Properties as ℕₚ
-open import Data.Product hiding (_<*>_; _,′_)
-open import Data.Product.Nary.NonDependent
-open import Data.Sum using (_⊎_; inj₁; inj₂; fromInj₂; [_,_]′)
-open import Data.Unit using (⊤)
-open import Level renaming (suc to ℓsuc) hiding (zero)
-open import Function using (_∘_; _∘₂_; _|>_)
-open import Function.Nary.NonDependent.Base
-open import Relation.Nullary.Decidable using (True)
-
-private
-  variable
-    ℓ ℓ₁ ℓ₂ : Level
-    τ τ′ : Set ℓ
-
-  update : ∀ {n ls} {Γ : Sets n ls} i → Projₙ Γ i → Product⊤ n Γ → Product⊤ n Γ
-  update zero    y (_ , xs) = y , xs
-  update (suc i) y (x , xs) = x , update i y xs
-
-Expr : ∀ n {ls} → Sets n ls → Set ℓ → Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′)
-Expr n Γ τ = (σ : State) → (ρ : Product⊤ n Γ) → τ
-
-record Reference n {ls} (Γ : Sets n ls) (τ : Set ℓ) : Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′) where
-  field
-    get : Expr n Γ τ
-    set : τ → Expr n Γ (State × Product⊤ n Γ)
-
-Function : ∀ n {ls} → Sets n ls → Set ℓ → Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′)
-Function n Γ τ = Expr n Γ τ
-
-Procedure : ∀ n {ls} → Sets n ls → Set (⨆ n ls ⊔ ℓ′)
-Procedure n Γ = Expr n Γ State
-
-Statement : ∀ n {ls} → Sets n ls → Set ℓ → Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′)
-Statement n Γ τ = Expr n Γ (State × (Product⊤ n Γ ⊎ τ))
-
--- Expressions
-
-pure : ∀ {n ls} {Γ : Sets n ls} → τ → Expr n Γ τ
-pure v σ ρ = v
-
-_<*>_ : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ (τ → τ′) → Expr n Γ τ → Expr n Γ τ′
-_<*>_ f e σ ρ = f σ ρ |> λ f → f (e σ ρ)
-
-!_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Expr n Γ τ
-! r = Reference.get r
-
-call : ∀ {m n ls₁ ls₂} {Γ : Sets m ls₁} {Δ : Sets n ls₂} → Function m Γ τ → Expr n Δ (Product m Γ) → Expr n Δ τ
-call f e σ ρ = e σ ρ |> toProduct⊤ _ |> f σ
-
-declare : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ τ → Expr (suc n) (τ , Γ) τ′ → Expr n Γ τ′
-declare e s σ ρ = e σ ρ |> _, ρ |> s σ
-
--- References
-
-var : ∀ {n ls} {Γ : Sets n ls} i → Reference n Γ (Projₙ Γ i)
-var i = record
-  { get = λ σ ρ → projₙ _ i (toProduct _ ρ)
-  ; set = λ v → curry (map₂ (update i v))
-  }
-
-!#_ : ∀ {n ls} {Γ : Sets n ls} m {m<n : True (suc m ℕₚ.≤? n)} → Expr n Γ (Projₙ Γ (#_ m {n} {m<n}))
-(!# m) {m<n} = ! var (#_ m {m<n = m<n})
-
-_,′_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Reference n Γ τ′ → Reference n Γ (τ × τ′)
-&x ,′ &y = record
-  { get = λ σ ρ → Reference.get &x σ ρ , Reference.get &y σ ρ
-  ; set = λ (x , y) σ ρ → uncurry (Reference.set &y y) (Reference.set &x x σ ρ)
-  }
-
--- Statements
-
-infixl 1 _∙_ _∙return_
-infix 1 _∙end
-infixl 2 if_then_else_
-infix 4 _≔_ _⟵_
-
-skip : ∀ {n ls} {Γ : Sets n ls} → Statement n Γ τ
-skip σ ρ = σ , inj₁ ρ
-
-invoke : ∀ {m n ls₁ ls₂} {Γ : Sets m ls₁} {Δ : Sets n ls₂} → Procedure m Γ → Expr n Δ (Product m Γ) → Statement n Δ τ
-invoke f e σ ρ = call f e σ ρ |> _, inj₁ ρ
-
-_≔_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Expr n Γ τ → Statement n Γ τ′
-(&x ≔ e) σ ρ = e σ ρ |> λ x → Reference.set &x x σ ρ |> map₂ inj₁
-
-_⟵_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Op₁ τ → Statement n Γ τ′
-&x ⟵ e = &x ≔ ⦇ e (! &x) ⦈
-
-if_then_else_ : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ Bool → Statement n Γ τ → Statement n Γ τ → Statement n Γ τ
-(if e then b₁ else b₂) σ ρ = e σ ρ |> (Bool.if_then b₁ σ ρ else b₂ σ ρ)
-
-for : ∀ {n ls} {Γ : Sets n ls} m → Statement (suc n) (Fin m , Γ) τ → Statement n Γ τ
-for zero    b σ ρ = σ , inj₁ ρ
-for (suc m) b σ ρ with b σ (zero , ρ)
-... | σ′ , inj₂ x        = σ′ , inj₂ x
-... | σ′ , inj₁ (_ , ρ′) = for m b′ σ′ ρ′
-  where
-  b′ : Statement (suc _) (Fin m , _) _
-  b′ σ (i , ρ) with b σ (suc i , ρ)
-  ... | σ′ , inj₂ x        = σ′ , inj₂ x
-  ... | σ′ , inj₁ (_ , ρ′) = σ′ , inj₁ (i , ρ′)
-
-_∙_ : ∀ {n ls} {Γ : Sets n ls} → Statement n Γ τ → Statement n Γ τ → Statement n Γ τ
-(b₁ ∙ b₂) σ ρ = b₁ σ ρ |> λ (σ , ρ⊎x) → [ b₂ σ , (σ ,_) ∘ inj₂ ]′ ρ⊎x
-
-_∙end : ∀ {n ls} {Γ : Sets n ls} → Statement n Γ ⊤ → Procedure n Γ
-_∙end s σ ρ = s σ ρ |> proj₁
-
-_∙return_ : ∀ {n ls} {Γ : Sets n ls} → Statement n Γ τ → Expr n Γ τ → Function n Γ τ
-(s ∙return e) σ ρ = s σ ρ |> λ (σ , ρ⊎x) → fromInj₂ (e σ) ρ⊎x