From 78aad93db3d7029e0a9a8517a2db92533fd1f401 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Tue, 15 Feb 2022 17:04:28 +0000
Subject: Make expressions unable to change state.

---
 src/Helium/Data/Pseudocode/Core.agda        |  61 +++++++++++--
 src/Helium/Instructions/Base.agda           |  25 ++---
 src/Helium/Semantics/Denotational/Core.agda | 137 +++++++++-------------------
 3 files changed, 106 insertions(+), 117 deletions(-)

diff --git a/src/Helium/Data/Pseudocode/Core.agda b/src/Helium/Data/Pseudocode/Core.agda
index a50fb84..8a0c4e3 100644
--- a/src/Helium/Data/Pseudocode/Core.agda
+++ b/src/Helium/Data/Pseudocode/Core.agda
@@ -13,13 +13,16 @@ open import Data.Fin using (Fin; #_)
 open import Data.Nat as ℕ using (ℕ; zero; suc)
 open import Data.Nat.Properties using (+-comm)
 open import Data.Product using (∃; _,_; proj₂; uncurry)
+open import Data.Sum using ([_,_]′; inj₁; inj₂)
 open import Data.Vec using (Vec; []; _∷_; lookup; map)
-open import Data.Vec.Relation.Unary.All using (All; []; _∷_; reduce; all?)
+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.Decidable.Core using (True; map′)
+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_)
 open import Relation.Unary using (Decidable)
 
 --- The set of types and boolean properties of them
@@ -95,10 +98,15 @@ data Literal : Type → Set where
 
 module Code {o} (Σ : Vec Type o) where
   data Expression {n} (Γ : Vec Type n) : Type → Set
-  data CanAssign {n} {Γ} : ∀ {t} → Expression {n} Γ t → 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 Statement {n} (Γ : Vec Type n) : Set
+  data ChangesState {n Γ} : Statement {n} Γ → Set
+  changesState? : ∀ {n Γ} → Decidable (ChangesState {n} {Γ})
   data Function {n} (Γ : Vec Type n) (ret : Type) : Set
   data Procedure {n} (Γ : Vec Type n) : Set
 
@@ -134,7 +142,6 @@ module Code {o} (Σ : Vec Type o) where
     _^_   : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → ℕ → Expression Γ t
     _>>_  : Expression Γ int → ℕ → Expression Γ int
     rnd   : Expression Γ real → Expression Γ int
-    -- get   : ℕ → Expression Γ int → Expression Γ bit
     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)
@@ -176,7 +183,6 @@ module Code {o} (Σ : Vec Type o) where
   canAssign? (e ^ e₁)     = no λ ()
   canAssign? (e >> e₁)    = no λ ()
   canAssign? (rnd e)      = no λ ()
-  -- canAssign? (get x e)    = no λ ()
   canAssign? (fin x e)    = no λ ()
   canAssign? (asInt e)    = no λ ()
   canAssign? (tup es)     = map′ tup (λ { (tup es) → es }) (canAssignAll? es)
@@ -186,6 +192,29 @@ module Code {o} (Σ : Vec Type o) where
   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)
+
   infix  4 _≔_
   infixl 2 if_then_else_
   infixl 1 _∙_ _∙return_
@@ -194,14 +223,32 @@ module Code {o} (Σ : Vec Type o) where
   data Statement Γ where
     _∙_           : Statement Γ → Statement Γ → Statement Γ
     skip          : Statement Γ
-    _≔_           : ∀ {t} → (ref : Expression Γ t) → {canAssign : True (canAssign? ref)}→ Expression Γ t → 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 Γ
     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₂)
+    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₂)
+    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)
+
   data Function Γ ret where
-    _∙return_ : Statement Γ → Expression Γ ret → Function Γ ret
+    _∙return_ : (s : Statement Γ) → {False (changesState? s)} → Expression Γ ret → Function Γ ret
     declare   : ∀ {t} → Expression Γ t → Function (t ∷ Γ) ret → Function Γ ret
 
   data Procedure Γ where
diff --git a/src/Helium/Instructions/Base.agda b/src/Helium/Instructions/Base.agda
index 8473d65..62a6968 100644
--- a/src/Helium/Instructions/Base.agda
+++ b/src/Helium/Instructions/Base.agda
@@ -219,8 +219,8 @@ to32 Instr.32bit = join
 module _ (d : Instr.VecOp₂) where
   open Instr.VecOp₂ d
 
-  -- op₁, op₂, e, elmtMask -> result
-  vec-op₂′ : Function (bits (toℕ esize) ∷ bits (toℕ esize) ∷ fin (toℕ elements) ∷ elmtMask ∷ []) (bits (toℕ esize)) → Procedure []
+ -- 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)) (
     -- 0:elmtMask 1:curBeat
@@ -230,9 +230,7 @@ module _ (d : Instr.VecOp₂) where
     -- 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 ∷ var 1 ∷ var 4 ∷ [])))) ∙
+      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))
@@ -244,7 +242,7 @@ module _ (d : Instr.VecOp₂) where
       ]′ src₂
 
   vec-op₂ : Function (bits (toℕ esize) ∷ bits (toℕ esize) ∷ []) (bits (toℕ esize)) → Procedure []
-  vec-op₂ op = vec-op₂′ (skip ∙return call op (tup (var 0 ∷ var 1 ∷ [])))
+  vec-op₂ op = vec-op₂′ (index (var 3) (var 1) ≔ call op (tup (index (var 2) (var 1) ∷ var 0 ∷ [])))
 
 vadd : Instr.VAdd → Procedure []
 vadd d = vec-op₂ d (skip ∙return sliceⁱ 0 (uint (var 0) + uint (var 1)))
@@ -280,18 +278,15 @@ vmla d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0) *
 private
   vqr?dmulh : Instr.VQDMulH → Function (int ∷ int ∷ []) int → Procedure []
   vqr?dmulh d f = vec-op₂′ d (
-    -- 0:op₁ 1:op₂ 2:e 3:elmtMask
-    declare (call f (tup (sint (var 0) ∷ sint (var 1) ∷ []))) (
-    declare (lit (Vec.replicate false ′x)) (
+    -- 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 (lit (false ′b)) (
-      -- 0:sat 1:result 2:value 3:op₁ 4:op₂ 5:e 6:elmtMask
-      tup (var 1 ∷ var 0 ∷ []) ≔ call (SignedSatQ (toℕ esize-1)) (tup (var 2 ∷ [])) ∙
-      if var 0 && hasBit (var 6) (fin e*esize>>3 (tup (var 5 ∷ [])))
+      -- 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
-      ∙return var 1
-    ))))
+      else skip)))
     where
     open Instr.VecOp₂ d
 
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
index a644adb..b425252 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -182,121 +182,71 @@ module Expression
 
   open Code Σ
 
-  ⟦_⟧ᵉ : ∀ {n} {Γ : Vec Type n} {t} → Expression Γ t → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ t ⟧ₜ
+  ⟦_⟧ᵉ : ∀ {n} {Γ : Vec Type n} {t} → Expression Γ t → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ t ⟧ₜ
   ⟦_⟧ˢ : ∀ {n} {Γ : Vec Type n} → Statement Γ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′
-  ⟦_⟧ᶠ : ∀ {n} {Γ : Vec Type n} {ret} → Function Γ ret → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ ret ⟧ₜ
+  ⟦_⟧ᶠ : ∀ {n} {Γ : Vec Type n} {ret} → Function Γ ret → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ ret ⟧ₜ
   ⟦_⟧ᵖ : ∀ {n} {Γ : Vec Type n} → Procedure Γ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′
   update : ∀ {n Γ t e} → CanAssign {n} {Γ} {t} e → ⟦ t ⟧ₜ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′
 
-  ⟦ lit x ⟧ᵉ σ γ = σ , 𝒦 x
-  ⟦ state i ⟧ᵉ σ γ = σ , fetch Σ σ (# i)
-  ⟦_⟧ᵉ {Γ = Γ} (var i) σ γ = σ , fetch Γ γ (# i)
-  ⟦ abort e ⟧ᵉ σ γ = case P.proj₂ (⟦ e ⟧ᵉ σ γ) of λ ()
-  ⟦ _≟_ {hasEquality = hasEq} e e₁ ⟧ᵉ σ γ = do
-    let σ′ , x = ⟦ e ⟧ᵉ σ γ
-    let σ′′ , y = ⟦ e ⟧ᵉ σ′ γ
-    σ′′ , equal (toWitness hasEq) x y
-  ⟦ _<?_ {isNumeric = isNum} e e₁ ⟧ᵉ σ γ = do
-    let σ′ , x = ⟦ e ⟧ᵉ σ γ
-    let σ′′ , y = ⟦ e ⟧ᵉ σ′ γ
-    σ′′ , comp (toWitness isNum) x y
-  ⟦ inv e ⟧ᵉ σ γ = P.map₂ Bool.not (⟦ e ⟧ᵉ σ γ)
-  ⟦ e && e₁ ⟧ᵉ σ γ = do
-    let σ′ , x = ⟦ e ⟧ᵉ σ γ
-    Bool.if x then ⟦ e₁ ⟧ᵉ σ′ γ else σ′ , false
-  ⟦ e || e₁ ⟧ᵉ σ γ = do
-    let σ′ , x = ⟦ e ⟧ᵉ σ γ
-    Bool.if x then σ′ , true else ⟦ e₁ ⟧ᵉ σ′ γ
-  ⟦ not e ⟧ᵉ σ γ = P.map₂ Bits.¬_ (⟦ e ⟧ᵉ σ γ)
-  ⟦ e and e₁ ⟧ᵉ σ γ = do
-    let σ′ , x = ⟦ e ⟧ᵉ σ γ
-    let σ′′ , y = ⟦ e₁ ⟧ᵉ σ′ γ
-    σ′′ , x Bits.∧ y
-  ⟦ e or e₁ ⟧ᵉ σ γ = do
-    let σ′ , x = ⟦ e ⟧ᵉ σ γ
-    let σ′′ , y = ⟦ e₁ ⟧ᵉ σ′ γ
-    σ′′ , x Bits.∨ y
-  ⟦ [ e ] ⟧ᵉ σ γ = P.map₂ (Vec._∷ []) (⟦ e ⟧ᵉ σ γ)
-  ⟦ unbox e ⟧ᵉ σ γ = P.map₂ Vec.head (⟦ e ⟧ᵉ σ γ)
-  ⟦ _∶_ {t = t} e e₁ ⟧ᵉ σ γ = do
-    let σ′ , x = ⟦ e ⟧ᵉ σ γ
-    let σ′′ , y = ⟦ e₁ ⟧ᵉ σ′ γ
-    σ′′ , join t x y
-  ⟦ slice {t = t} e e₁ ⟧ᵉ σ γ = do
-    let σ′ , x = ⟦ e ⟧ᵉ σ γ
-    let σ′′ , y = ⟦ e₁ ⟧ᵉ σ′ γ
-    σ′′ , sliced t x y
-  ⟦ cast {t = t} eq e ⟧ᵉ σ γ = P.map₂ (casted t eq) (⟦ e ⟧ᵉ σ γ)
-  ⟦ -_ {isNumeric = isNum} e ⟧ᵉ σ γ = P.map₂ (neg (toWitness isNum)) (⟦ e ⟧ᵉ σ γ)
-  ⟦ _+_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁ ⟧ᵉ σ γ = do
-    let σ′ , x = ⟦ e ⟧ᵉ σ γ
-    let σ′′ , y = ⟦ e₁ ⟧ᵉ σ′ γ
-    σ′′ , add isNum₁ isNum₂ x y
-  ⟦ _*_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁ ⟧ᵉ σ γ = do
-    let σ′ , x = ⟦ e ⟧ᵉ σ γ
-    let σ′′ , y = ⟦ e₁ ⟧ᵉ σ′ γ
-    σ′′ , mul isNum₁ isNum₂ x y
+  ⟦ lit x ⟧ᵉ σ γ = 𝒦 x
+  ⟦ 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₁ ⟧ᵉ σ γ)
+  ⟦ inv e ⟧ᵉ σ γ = Bool.not (⟦ e ⟧ᵉ σ γ)
+  ⟦ e && e₁ ⟧ᵉ σ γ = Bool.if ⟦ e ⟧ᵉ σ γ then ⟦ e₁ ⟧ᵉ σ γ else false
+  ⟦ e || e₁ ⟧ᵉ σ γ = Bool.if ⟦ e ⟧ᵉ σ γ then true else ⟦ e₁ ⟧ᵉ σ γ
+  ⟦ 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₁ ⟧ᵉ σ γ)
+  ⟦ 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₁ ⟧ᵉ σ γ)
+  ⟦ _*_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁ ⟧ᵉ σ γ = mul isNum₁ isNum₂ (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ)
   -- ⟦ e / e₁ ⟧ᵉ σ γ = {!!}
-  ⟦ _^_ {isNumeric = isNum} e n ⟧ᵉ σ γ = P.map₂ (λ x → pow (toWitness isNum) x n) (⟦ e ⟧ᵉ σ γ)
-  ⟦ _>>_ e n ⟧ᵉ σ γ = P.map₂ (λ x → shiftr 2≉0 x n) (⟦ e ⟧ᵉ σ γ)
-  ⟦ rnd e ⟧ᵉ σ γ = P.map₂ ⌊_⌋ (⟦ e ⟧ᵉ σ γ)
-  ⟦ fin x e ⟧ᵉ σ γ = P.map₂ (apply x) (⟦ e ⟧ᵉ σ γ)
+  ⟦ _^_ {isNumeric = isNum} e n ⟧ᵉ σ γ = pow (toWitness isNum) (⟦ e ⟧ᵉ σ γ) n
+  ⟦ _>>_ e n ⟧ᵉ σ γ = shiftr 2≉0 (⟦ e ⟧ᵉ σ γ) n
+  ⟦ rnd e ⟧ᵉ σ γ = ⌊ ⟦ e ⟧ᵉ σ γ ⌋
+  ⟦ fin x e ⟧ᵉ σ γ = apply x (⟦ e ⟧ᵉ σ γ)
     where
     apply : ∀ {k ms n} → (All Fin ms → Fin n) → ⟦ Vec.map {n = k} fin ms ⟧ₜ′ → ⟦ fin n ⟧ₜ
     apply {zero}  {[]}     f xs = f []
     apply {suc k} {_ ∷ ms} f xs =
       apply (λ x → f (tupHead (Vec.map fin ms) xs ∷ x)) (tupTail (Vec.map fin ms) xs)
-  ⟦ asInt e ⟧ᵉ σ γ = P.map₂ (λ i → Fin.toℕ i ℤ′.×′ 1ℤ) (⟦ e ⟧ᵉ σ γ)
-  ⟦ tup [] ⟧ᵉ σ γ = σ , _
+  ⟦ asInt e ⟧ᵉ σ γ = Fin.toℕ (⟦ e ⟧ᵉ σ γ) ℤ′.×′ 1ℤ
+  ⟦ tup [] ⟧ᵉ σ γ = _
   ⟦ tup (e ∷ []) ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ
-  ⟦ tup (e ∷ e′ ∷ es) ⟧ᵉ σ γ = do
-    let σ′ , v = ⟦ e ⟧ᵉ σ γ
-    let σ′′ , vs = ⟦ tup (e′ ∷ es) ⟧ᵉ σ′ γ
-    σ′′ , (v , vs)
-  ⟦ call f e ⟧ᵉ σ γ = P.uncurry ⟦ f ⟧ᶠ (⟦ e ⟧ᵉ σ γ)
-  ⟦ if e then e₁ else e₂ ⟧ᵉ σ γ = do
-    let σ′ , x = ⟦ e ⟧ᵉ σ γ
-    Bool.if x then ⟦ e₁ ⟧ᵉ σ′ γ else ⟦ e₂ ⟧ᵉ σ′ γ
-
-  ⟦ s ∙ s₁ ⟧ˢ σ γ = do
-    let σ′ , γ′ = ⟦ s ⟧ˢ σ γ
-    ⟦ s ⟧ˢ σ′ γ′
+  ⟦ tup (e ∷ e′ ∷ es) ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ , ⟦ tup (e′ ∷ es) ⟧ᵉ σ γ
+  ⟦ call f e ⟧ᵉ σ γ = ⟦ f ⟧ᶠ σ (⟦ e ⟧ᵉ σ γ)
+  ⟦ if e then e₁ else e₂ ⟧ᵉ σ γ = Bool.if ⟦ e ⟧ᵉ σ γ then ⟦ e₁ ⟧ᵉ σ γ else ⟦ e₂ ⟧ᵉ σ γ
+
+  ⟦ s ∙ s₁ ⟧ˢ σ γ = P.uncurry ⟦ s ⟧ˢ (⟦ s ⟧ˢ σ γ)
   ⟦ skip ⟧ˢ σ γ = σ , γ
-  ⟦ _≔_ ref {canAssign = canAssign} e ⟧ˢ σ γ = do
-    let σ′ , v = ⟦ e ⟧ᵉ σ γ
-    update (toWitness canAssign) v σ′ γ
-  ⟦_⟧ˢ {Γ = Γ} (declare e s) σ γ = do
-    let σ′ , x = ⟦ e ⟧ᵉ σ γ
-    let σ′′ , γ′ = ⟦ s ⟧ˢ σ′ (tupCons Γ x γ)
-    σ′′ , tupTail Γ γ′
-  ⟦ invoke p e ⟧ˢ σ γ = do
-    let σ′ , v = ⟦ e ⟧ᵉ σ γ
-    ⟦ p ⟧ᵖ σ′ v , γ
-  ⟦ if e then s₁ else s₂ ⟧ˢ σ γ = do
-    let σ′ , x = ⟦ e ⟧ᵉ σ γ
-    Bool.if x then ⟦ s₁ ⟧ˢ σ′ γ else ⟦ s₂ ⟧ˢ σ′ γ
+  ⟦ _≔_ ref {canAssign = canAssign} e ⟧ˢ σ γ = update (toWitness canAssign) (⟦ e ⟧ᵉ σ γ) σ γ
+  ⟦_⟧ˢ {Γ = Γ} (declare e s) σ γ = P.map₂ (tupTail Γ) (⟦ s ⟧ˢ σ (tupCons Γ (⟦ e ⟧ᵉ σ γ) γ))
+  ⟦ invoke p e ⟧ˢ σ γ = ⟦ p ⟧ᵖ σ (⟦ e ⟧ᵉ σ γ) , γ
+  ⟦ if e then s₁ else s₂ ⟧ˢ σ γ = Bool.if ⟦ e ⟧ᵉ σ γ then ⟦ s₁ ⟧ˢ σ γ else ⟦ s₂ ⟧ˢ σ γ
   ⟦_⟧ˢ {Γ = Γ} (for m s) σ γ = helper m ⟦ s ⟧ˢ σ γ
     where
     helper : ∀ m → (⟦ Σ ⟧ₜ′ → ⟦ fin m ∷ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ fin m ∷ Γ ⟧ₜ′) → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ Γ ⟧ₜ′
     helper zero    s σ γ = σ , γ
-    helper (suc m) s σ γ with s σ (tupCons Γ zero γ)
-    ... | σ′ , γ′ = helper m s′ σ′ (tupTail Γ γ′)
+    helper (suc m) s σ γ = P.uncurry (helper m s′) (P.map₂ (tupTail Γ) (s σ (tupCons Γ zero γ)))
       where
       s′ : ⟦ Σ ⟧ₜ′ → ⟦ fin m ∷ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ fin m ∷ Γ ⟧ₜ′
       s′ σ γ =
         P.map₂ (tupCons Γ (tupHead Γ γ) ∘′ (tupTail Γ))
                (s σ (tupCons Γ (suc (tupHead Γ γ)) (tupTail Γ γ)))
 
-  ⟦ s ∙return e ⟧ᶠ σ γ with ⟦ s ⟧ˢ σ γ
-  ... | σ′ , γ′ = ⟦ e ⟧ᵉ σ′ γ′
-  ⟦_⟧ᶠ {Γ = Γ} (declare e f) σ γ = do
-    let σ′ , x = ⟦ e ⟧ᵉ σ γ
-    ⟦ f ⟧ᶠ σ′ (tupCons Γ x γ)
+  ⟦ s ∙return e ⟧ᶠ σ γ = P.uncurry ⟦ e ⟧ᵉ (⟦ s ⟧ˢ σ γ)
+  ⟦_⟧ᶠ {Γ = Γ} (declare e f) σ γ = ⟦ f ⟧ᶠ σ (tupCons Γ (⟦ e ⟧ᵉ σ γ) γ)
 
   ⟦ s ∙end ⟧ᵖ σ γ = P.proj₁ (⟦ s ⟧ˢ σ γ)
-  ⟦_⟧ᵖ {Γ = Γ} (declare e p) σ γ = do
-    let σ′ , x = ⟦ e ⟧ᵉ σ γ
-    ⟦ p ⟧ᵖ σ′ (tupCons Γ x γ)
+  ⟦_⟧ᵖ {Γ = Γ} (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 γ
@@ -306,10 +256,7 @@ module Expression
     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 σ γ = do
-    let σ′ , off = ⟦ e₂ ⟧ᵉ σ γ
-    let σ′′ , orig = ⟦ e₁ ⟧ᵉ σ′ γ
-    updateSliced t orig off v (λ v → update a v σ′′ γ)
+  update (slice {t = t} {e₁ = e₁} a e₂) v σ γ = updateSliced t (⟦ e₁ ⟧ᵉ σ γ) (⟦ e₂ ⟧ᵉ σ γ) v (λ v → update a v σ γ)
   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 σ γ
-- 
cgit v1.2.3