Eliminate even more state from the denotational semantics.

2 files changed, 81 insertions, 96 deletions

diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda
index 2a18957..3a616c0 100644
--- a/src/Helium/Semantics/Denotational.agda
+++ b/src/Helium/Semantics/Denotational.agda
@@ -23,7 +23,7 @@ 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 using (_|>_; _$_; _∘₂_)
 open import Function.Nary.NonDependent.Base
 import Helium.Instructions as Instr
 import Helium.Semantics.Denotational.Core as Core
@@ -68,19 +68,19 @@ ElmtMask = Bits 4
 
 -- State properties
 
-&R : ∀ {n ls} {Γ : Sets n ls} → PureExpr n Γ (Fin 16) → Reference n Γ (Bits 32)
+&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} → PureExpr n Γ (Fin 32) → Reference n Γ (Bits 32)
+&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} → PureExpr n Γ Instr.VecReg → PureExpr n Γ Beat → Reference n Γ (Bits 32)
+&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
@@ -115,7 +115,7 @@ ElmtMask = Bits 4
   ; set = λ x σ ρ → Reference.set &v (cast (sym eq) x) σ ρ
   }
 
-slice : ∀ {k m n ls} {Γ : Sets n ls} → Reference n Γ (Bits m) → PureExpr n Γ (∃ λ (i : Fin (suc m)) → ∃ λ j → toℕ (i - j) ≡ k) → Reference n Γ (Bits k)
+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 σ ρ →
@@ -123,7 +123,7 @@ slice &v idx = record
     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)) → PureExpr n Γ (Fin k) → Reference n Γ (Bits m)
+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
@@ -158,11 +158,11 @@ 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) ⦈
+    if ⦇ hasBit (!# 0) (!# 3) ⦈
     then
-      elem 8 (&Q (pure′ dest) (!# 2)) (!# 0) ≔ ↓! elem 8 (var (# 1)) (!# 0)
-    else skip) ∙
-  ⦇ _ ⦈
+      elem 8 (&Q ⦇ dest ⦈ (!# 2)) (!# 0) ≔ ! elem 8 (var (# 1)) (!# 0)
+    else skip)
+  ∙end
 
 module fun-sliceᶻ
   (1<<n≉0 : ∀ n → False (float (1ℤ << n) ≟ʳ 0ℝ))
@@ -173,52 +173,52 @@ module fun-sliceᶻ
   signedSatQ : ∀ n → Function 1 (ℤ , _) (Bits (suc n) × Bool)
   signedSatQ n = declare ⦇ true ⦈ $
     -- 0:sat 1:x
-    if ⦇ (λ i → does ((1ℤ << n) +ᶻ -ᶻ 1ℤ <ᶻ? i)) (↓ !# 1) ⦈
+    if ⦇ (λ i → does ((1ℤ << n) +ᶻ -ᶻ 1ℤ <ᶻ? i)) (!# 1) ⦈
     then
       var (# 1) ≔ ⦇ ((1ℤ << n) +ᶻ -ᶻ 1ℤ) ⦈
-    else if ⦇ (λ i → does (-ᶻ 1ℤ << n <ᶻ? i)) (↓ !# 1) ⦈
+    else if ⦇ (λ i → does (-ᶻ 1ℤ << n <ᶻ? i)) (!# 1) ⦈
     then
       var (# 1) ≔ ⦇ (-ᶻ 1ℤ << n) ⦈
     else
-      var (# 0) ≔ ⦇ false ⦈ ∙
-    ⦇ ⦇ (sliceᶻ (suc n) zero) (↓ !# 1) ⦈ , (↓ !# 0) ⦈
+      var (# 0) ≔ ⦇ false ⦈
+    ∙return ⦇ ⦇ (sliceᶻ (suc n) zero) (!# 1) ⦈ , (!# 0) ⦈
 
 advanceVPT : Procedure 1 (Beat , _)
-advanceVPT = declare (↓! elem 4 &VPR-mask (hilow ∘₂ !# 0)) $
+advanceVPT = declare (! elem 4 &VPR-mask (hilow ∘₂ !# 0)) $
   -- 0:vptState 1:beat
-  if ⦇ (λ x → does (x ≟ᵇ 1𝔹 ∷ zeros)) (↓ !# 0) ⦈
+  if ⦇ (λ x → does (x ≟ᵇ 1𝔹 ∷ zeros)) (!# 0) ⦈
   then
     var (# 0) ≔ ⦇ zeros ⦈
-  else if ⦇ (λ x → does (x ≟ᵇ zeros)) (↓ !# 0) ⦈
+  else if ⦇ (λ x → does (x ≟ᵇ zeros)) (!# 0) ⦈
   then skip
   else (
-    if ⦇ (hasBit (# 3)) (↓ !# 0) ⦈
+    if ⦇ (hasBit (# 3)) (!# 0) ⦈
     then
       elem 4 &VPR-P0 (!# 1) ⟵ (¬_)
     else skip ∙
     (var (# 0) ⟵ λ x → sliceᵇ (# 3) zero x V.++ 0𝔹 ∷ [])) ∙
-  if ⦇ (λ x → does (oddeven x Finₚ.≟ # 1)) (↓ !# 1) ⦈
+  if ⦇ (λ x → does (oddeven x Finₚ.≟ # 1)) (!# 1) ⦈
   then
-    elem 4 &VPR-mask (hilow ∘₂ !# 1) ≔ ↓ !# 0
-  else skip ∙
-  ⦇ _ ⦈
+    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)) ⦈
+    if ⦇ (λ x → does (x ≟ᵇ zeros)) (! elem 4 &VPR-mask (hilow ∘₂ !# 0)) ⦈
     then
       var (# 1) ≔ ⦇ ones ⦈
     else
-      var (# 1) ≔ ↓! elem 4 &VPR-P0 (!# 0) ∙
+      var (# 1) ≔ ! elem 4 &VPR-P0 (!# 0) ∙
     &AdvanceVPT ≔ ⦇ true ⦈ ∙
-    invoke inst ⦇ ↓ !# 0 , ↓ !# 1 ⦈ ∙
-    if ↓! &AdvanceVPT
+    invoke inst ⦇ !# 0 , !# 1 ⦈ ∙
+    if ! &AdvanceVPT
     then
-      invoke advanceVPT (↓ !# 0)
-    else skip) ∙
-  ⦇ _ ⦈
+      invoke advanceVPT (!# 0)
+    else skip)
+  ∙end
 
 module _
   (d : Instr.VecOp₂)
@@ -227,17 +227,17 @@ module _
   open Instr.VecOp₂ d
 
   vec-op₂ : Op₂ (Bits (toℕ esize)) → Procedure 2 (Beat , ElmtMask , _)
-  vec-op₂ op = declare ⦇ zeros ⦈ $ declare (↓! &Q (pure′ src₁) (!# 1)) $
+  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 (pure′ src₂)) (pure′ (esize , zero , refl)))
-            , (λ src₂ → ↓! elem (toℕ esize) (&cast (sym e*e≡32) (&Q (pure′ src₂) (!# 3))) (!# 0))
+           (! 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 ⦈ ⦈ ∙
-    ⦇ _ ⦈
+    invoke (copyMasked dest) ⦇ !# 1 , ⦇ !# 2 , !# 3 ⦈ ⦈
+    ∙end
 
 -- Instruction semantics
 
@@ -274,24 +274,24 @@ module _
     eq m (suc i) = eq m i
 
   vqdmulh : Instr.VQDMulH → Procedure 2 (Beat , ElmtMask , _)
-  vqdmulh d = declare ⦇ zeros ⦈ $ declare (↓! &Q (pure′ src₁) (!# 1)) $ declare ⦇ false ⦈ $
+  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 (pure′ src₂)) (pure′ (esize , zero , refl)))
-              , (λ src₂ → ↓! elem (toℕ esize) (&cast (sym e*e≡32) (&Q (pure′ src₂) (!# 4))) (!# 0))
+             (! 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) ⦈
+      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 ⦈ ⦈ ∙
-    ⦇ _ ⦈
+    invoke (copyMasked dest) ⦇ !# 2 , ⦇ !# 3 , !# 4 ⦈ ⦈
+    ∙end
     where
     open Instr.VQDMulH d
     rval = Bool.if rounding then 1ℤ << toℕ esize-1 else 0ℤ
@@ -306,5 +306,5 @@ module _
   open List using (List; []; _∷_)
 
   ⟦_⟧ : List (Instr.Instruction) → Procedure 0 _
-  ⟦ [] ⟧     = ⦇ _ ⦈
-  ⟦ i ∷ is ⟧ = invoke ⟦ i ⟧₁ ⦇ _ ⦈ ∙ ⟦ is ⟧
+  ⟦ [] ⟧     = 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
index d92c1b2..9b6a3c8 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -18,7 +18,7 @@ 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₂; [_,_]′)
+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 (_∘_; _∘₂_; _|>_)
@@ -30,65 +30,43 @@ private
     ℓ ℓ₁ ℓ₂ : Level
     τ τ′ : Set ℓ
 
-  mapAll : ∀ {m ls} {Γ : Sets m ls} {l l′}
-           (f : ∀ {ℓ} → Set ℓ → Set (l ℓ))
-           (g : ∀ {ℓ} → Set ℓ → Set (l′ ℓ))
-           (h : ∀ {a} {A : Set a} → f A → g A) →
-           Product⊤ m (smap l f m Γ) →
-           Product⊤ m (smap l′ g m Γ)
-  mapAll {zero}  f g h xs       = xs
-  mapAll {suc m} f g h (x , xs) = h x , mapAll f g h xs
-
   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
 
-PureExpr : ∀ n {ls} → Sets n ls → Set ℓ → Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′)
-PureExpr n Γ τ = (σ : State) → (ρ : Product⊤ n Γ) → τ
-
 Expr : ∀ n {ls} → Sets n ls → Set ℓ → Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′)
-Expr n Γ τ = (σ : State) → (ρ : Product⊤ n Γ) → State × τ
-
+Expr n Γ τ = (σ : State) → (ρ : Product⊤ n Γ) → τ
 
 record Reference n {ls} (Γ : Sets n ls) (τ : Set ℓ) : Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′) where
   field
-    get : PureExpr n Γ τ
-    set : τ → (σ : State) → (ρ : Product⊤ n Γ) → State × Product⊤ n Γ
+    get : Expr n Γ τ
+    set : τ → Expr n Γ (State × Product⊤ n Γ)
 
 Function : ∀ n {ls} → Sets n ls → Set ℓ → Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′)
-Function = Expr
+Function n Γ τ = Expr n Γ τ
 
 Procedure : ∀ n {ls} → Sets n ls → Set (⨆ n ls ⊔ ℓ′)
-Procedure n Γ = Function n Γ ⊤
+Procedure n Γ = Expr n Γ State
 
-Block : ∀ n {ls} → Sets n ls → Set ℓ → Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′)
-Block n Γ τ = (σ : State) → (ρ : Product⊤ n Γ) → State × (Product⊤ n Γ ⊎ τ)
+Statement : ∀ n {ls} → Sets n ls → Set ℓ → Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′)
+Statement n Γ τ = Expr n Γ (State × (Product⊤ n Γ ⊎ τ))
 
 -- Expressions
 
-pure′ : ∀ {n ls} {Γ : Sets n ls} → τ → PureExpr n Γ τ
-pure′ v σ ρ = v
-
 pure : ∀ {n ls} {Γ : Sets n ls} → τ → Expr n Γ τ
-pure v σ ρ = σ , v
-
-↓_ : ∀ {n ls} {Γ : Sets n ls} → PureExpr n Γ τ → Expr n Γ τ
-(↓ e) σ ρ = σ , e σ ρ
+pure v σ ρ = v
 
 _<*>_ : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ (τ → τ′) → Expr n Γ τ → Expr n Γ τ′
-_<*>_ f e σ ρ = f σ ρ |> λ (σ , f) → map₂ f (e σ ρ)
+_<*>_ f e σ ρ = f σ ρ |> λ f → f (e σ ρ)
 
-!_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → PureExpr n Γ τ
+!_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Expr n Γ τ
 ! r = Reference.get r
 
-↓!_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Expr n Γ τ
-↓! r = ↓ ! r
-
 call : ∀ {m n ls₁ ls₂} {Γ : Sets m ls₁} {Δ : Sets n ls₂} → Function m Γ τ → Expr n Δ (Product m Γ) → Expr n Δ τ
-call f e σ ρ = e σ ρ |> map₂ (toProduct⊤ _) |> uncurry f
+call f e σ ρ = e σ ρ |> toProduct⊤ _ |> f σ
 
 declare : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ τ → Expr (suc n) (τ , Γ) τ′ → Expr n Γ τ′
-declare e s σ ρ = e σ ρ |> map₂ (_, ρ) |> uncurry s
+declare e s σ ρ = e σ ρ |> _, ρ |> s σ
 
 -- References
 
@@ -98,7 +76,7 @@ var i = record
   ; set = λ v → curry (map₂ (update i v))
   }
 
-!#_ : ∀ {n ls} {Γ : Sets n ls} m {m<n : True (suc m ℕₚ.≤? n)} → PureExpr n Γ (Projₙ Γ (#_ m {n} {m<n}))
+!#_ : ∀ {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 Γ (τ × τ′)
@@ -107,37 +85,44 @@ _,′_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Reference n Γ τ
   ; set = λ (x , y) σ ρ → uncurry (Reference.set &y y) (Reference.set &x x σ ρ)
   }
 
--- Blocks
+-- Statements
 
-infixr 1 _∙_
+infixl 1 _∙_ _∙return_
+infix 1 _∙end
 infixl 2 if_then_else_
 infix 4 _≔_ _⟵_
 
-skip : ∀ {n ls} {Γ : Sets n ls} → Block n Γ τ
+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 Γ) → Block n Δ τ
-invoke f e σ ρ = call f e σ ρ |> map₂ (λ _ → 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 Γ τ → Block n Γ τ′
-(&x ≔ e) σ ρ = e σ ρ |> λ (σ , x) → Reference.set &x x σ ρ |> map₂ 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₁ τ → Block n Γ τ′
-&x ⟵ e = &x ≔ ⦇ e (↓ (! &x)) ⦈
+_⟵_ : ∀ {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 → Block n Γ τ → Block n Γ τ → Block n Γ τ
-(if e then b₁ else b₂) σ ρ = e σ ρ |> λ (σ , b) → Bool.if b then b₁ σ ρ else b₂ σ ρ
+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 → Block (suc n) (Fin m , Γ) τ → Block n Γ τ
+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′ : Block (suc _) (Fin m , _) _
+  b′ : Statement (suc _) (Fin m , _) _
   b′ σ (i , ρ) with b σ (suc i , ρ)
   ... | σ′ , inj₂ x        = σ′ , inj₂ x
   ... | σ′ , inj₁ (_ , ρ′) = σ′ , inj₁ (i , ρ′)
 
-_∙_ : ∀ {n ls} {Γ : Sets n ls} → Block n Γ τ → Expr n Γ τ → Expr n Γ τ
-(b ∙ e) σ τ = b σ τ |> λ (σ , ρ⊎x) → [ e σ , σ ,_ ]′ ρ⊎x
+_∙_ : ∀ {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