Finish definition of denotational semantics.

4 files changed, 384 insertions, 319 deletions

diff --git a/src/Helium/Data/Pseudocode.agda b/src/Helium/Data/Pseudocode.agda
index 9e4707d..9f936f2 100644
--- a/src/Helium/Data/Pseudocode.agda
+++ b/src/Helium/Data/Pseudocode.agda
@@ -71,19 +71,15 @@ 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)))
+group {k = k} (suc m) x = group m (slice x′ (lit (Fin.fromℕ k ′f))) ∶ [ slice (cast (ℕₚ.+-comm k _) x′) (lit (zero ′f))  ]
   where
-  x′ = cast (ℕₚ.*-comm k (suc (suc m))) x
+  x′ = cast (P.trans (ℕₚ.*-comm k _) (P.cong (k ℕ.+_) (ℕₚ.*-comm _ k))) 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))))
+join {k = k} {suc m} x = cast eq (join (slice x (lit (Fin.fromℕ 1 ′f))) ∶ unbox (slice {i = suc m} (cast (ℕₚ.+-comm 1 _) x) (lit (zero ′f))))
   where
   eq = P.trans (P.cong (k ℕ.+_) (ℕₚ.*-comm k (suc m))) (ℕₚ.*-comm (suc (suc m)) k)
 
@@ -106,7 +102,7 @@ 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
+sliceⁱ {m = suc m} n i = sliceⁱ (suc n) i ∶ get n i
 
 --- Functions
 
@@ -126,18 +122,18 @@ SignedSatQ n = declare (lit (true ′b)) (
     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))
+  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))
   (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))
+    ( slice (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))
+  eq = P.trans (ℕₚ.+-comm 1 (shift ℕ.+ n)) (P.cong (ℕ._+ 1) (ℕₚ.+-comm shift n))
 
 --- Procedures
 
@@ -229,7 +225,7 @@ module _ (d : Instr.VecOp₂) where
     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 (lit ((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) (
@@ -266,7 +262,7 @@ vmulh d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0)
   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)))
+vrmulh d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0) * toInt (var 1) + lit (1 ′i) << toℕ esize-1))
   where
   open Instr.VRMulH d; toInt = λ i → call Int (tup (i ∷ lit (unsigned ′b) ∷ []))
 
@@ -277,7 +273,7 @@ private
     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 (lit ((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) (
@@ -313,9 +309,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 >> lit (toℕ esize ′i))
+vqdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0 * var 1 >> 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) << lit (toℕ esize-1 ′i)) >> lit (toℕ esize ′i))
+vqrdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0 * var 1 + lit (1 ′i) << toℕ esize-1 >> toℕ esize)
   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 7b21824..a63cc39 100644
--- a/src/Helium/Data/Pseudocode/Core.agda
+++ b/src/Helium/Data/Pseudocode/Core.agda
@@ -8,9 +8,10 @@
 
 module Helium.Data.Pseudocode.Core where
 
-open import Data.Bool using (Bool)
+open import Data.Bool using (Bool; true; false)
 open import Data.Fin using (Fin; #_)
-open import Data.Nat as ℕ using (ℕ; suc)
+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.Vec using (Vec; []; _∷_; lookup; map)
 open import Data.Vec.Relation.Unary.All using (All; []; _∷_; reduce; all?)
@@ -29,7 +30,6 @@ data Type : Set where
   fin   : (n : ℕ) → Type
   real  : Type
   bits  : (n : ℕ) → Type
-  enum  : (n : ℕ) → Type
   tuple : ∀ n → Vec Type n → Type
   array : Type → (n : ℕ) → Type
 
@@ -42,7 +42,6 @@ data HasEquality : Type → Set where
   fin  : ∀ {n} → HasEquality (fin n)
   real : HasEquality real
   bits : ∀ {n} → HasEquality (bits n)
-  enum : ∀ {n} → HasEquality (enum n)
 
 hasEquality? : Decidable HasEquality
 hasEquality? unit        = no (λ ())
@@ -51,7 +50,6 @@ hasEquality? int         = yes int
 hasEquality? (fin n)     = yes fin
 hasEquality? real        = yes real
 hasEquality? (bits n)    = yes bits
-hasEquality? (enum n)    = yes enum
 hasEquality? (tuple n x) = no (λ ())
 hasEquality? (array t n) = no (λ ())
 
@@ -66,7 +64,6 @@ isNumeric? int         = yes int
 isNumeric? real        = yes real
 isNumeric? (fin n)     = no (λ ())
 isNumeric? (bits n)    = no (λ ())
-isNumeric? (enum n)    = no (λ ())
 isNumeric? (tuple n x) = no (λ ())
 isNumeric? (array t n) = no (λ ())
 
@@ -95,8 +92,7 @@ data Literal : Type → Set where
   _′f : ∀ {n} → Fin n → Literal (fin n)
   _′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)
+  _′a : ∀ {n t} → Literal t → Literal (array t n)
 
 --- Expressions, references, statements, functions and procedures
 
@@ -111,7 +107,8 @@ module Code {o} (Σ : Vec Type o) where
 
   infix  8 -_
   infixr 7 _^_
-  infixl 6 _*_ _/_ _and_
+  infixl 6 _*_ _and_ _>>_
+  -- infixl 6 _/_
   infixl 5 _+_ _or_ _&&_ _||_ _∶_
   infix  4 _≟_ _<?_
 
@@ -130,42 +127,37 @@ module Code {o} (Σ : Vec Type o) where
     _or_  : ∀ {n} → Expression Γ (bits n) → Expression Γ (bits n) → Expression Γ (bits n)
     [_]   : ∀ {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 (m ℕ.+ n))
+    _∶_   : ∀ {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₂})
-    _/_   : Expression Γ real → Expression Γ real → Expression Γ real
-    _^_   : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → Expression Γ int → Expression Γ t
-    sint  : ∀ {n} → Expression Γ (bits n) → Expression Γ int
-    uint  : ∀ {n} → Expression Γ (bits n) → Expression Γ int
+    -- _/_   : Expression Γ real → Expression Γ real → Expression Γ real
+    _^_   : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → ℕ → Expression Γ t
+    _>>_  : Expression Γ int → ℕ → Expression Γ int
     rnd   : Expression Γ real → Expression Γ int
-    get   : ℕ → Expression Γ int → Expression Γ bit
+    -- get   : ℕ → Expression Γ int → Expression Γ bit
     fin   : ∀ {k ms n} → (All (Fin) ms → Fin n) → Expression Γ (tuple k (map fin ms)) → Expression Γ (fin n)
     asInt : ∀ {n} → Expression Γ (fin n) → Expression Γ int
     tup   : ∀ {m ts} → All (Expression Γ) ts → Expression Γ (tuple m 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 → 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})
-    var   : ∀ {i} {i<n : True (i ℕ.<? n)} → CanAssign (var i {i<n})
+    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))} {e₂ : Expression Γ (fin (suc i))} → CanAssign e₁ → CanAssign (slice e₁ e₂)
-    cast  : ∀ {i j t} {e : Expression Γ (asType t i)} .{eq : i ≡ j} → CanAssign e → CanAssign (cast eq 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)
-    head  : ∀ {m t ts} {e : Expression Γ (tuple (suc m) (t ∷ ts))} → CanAssign e → CanAssign (head e)
-    tail  : ∀ {m t ts} {e : Expression Γ (tuple (suc m) (t ∷ ts))} → CanAssign e → CanAssign (tail e)
 
   canAssign? (lit x)      = no λ ()
-  canAssign? (state i)    = yes state
-  canAssign? (var i)      = yes var
+  canAssign? (state i)    = yes (state i)
+  canAssign? (var i)      = yes (var i)
   canAssign? (abort e)    = yes abort
   canAssign? (e ≟ e₁)     = no λ ()
   canAssign? (e <? e₁)    = no λ ()
@@ -178,22 +170,19 @@ module Code {o} (Σ : Vec Type o) where
   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′ slice (λ { (slice e) → e }) (canAssign? e)
-  canAssign? (cast eq e)  = map′ cast (λ { (cast e) → e }) (canAssign? e)
+  canAssign? (slice e e₁) = map′ (λ e → slice e e₁) (λ { (slice 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 λ ()
   canAssign? (e * e₁)     = no λ ()
-  canAssign? (e / e₁)     = no λ ()
+  -- canAssign? (e / e₁)     = no λ ()
   canAssign? (e ^ e₁)     = no λ ()
-  canAssign? (sint e)     = no λ ()
-  canAssign? (uint e)     = no λ ()
+  canAssign? (e >> e₁)    = no λ ()
   canAssign? (rnd e)      = no λ ()
-  canAssign? (get x 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)
-  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 λ ()
 
@@ -222,13 +211,34 @@ module Code {o} (Σ : Vec Type o) where
     _∙end   : Statement Γ unit → Procedure Γ
     declare : ∀ {t} → Expression Γ t → Procedure (t ∷ Γ) → Procedure Γ
 
-  infixl  6 _<<_ _>>_
+  infixl  6 _<<_
   infixl 5 _-_
+
+  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₂})
   _-_ {isNumeric₂ = isNumeric₂} x y = x + (-_ {isNumeric = isNumeric₂} y)
 
-  _<<_ : ∀ {n Γ} → Expression {n} Γ int → Expression Γ int → Expression Γ int
+  _<<_ : ∀ {n Γ} → Expression {n} Γ 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)
+  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)
+
+  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)
+      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 (suc m)} x =
+    lit (2 ′i) * sint (slice {i = 1} x (lit ((# 1) ′f))) +
+    ( if slice′ x (lit ((# 0) ′f)) ≟ lit ((true ∷ []) ′x)
+      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 a545ddc..971ca12 100644
--- a/src/Helium/Data/Pseudocode/Types.agda
+++ b/src/Helium/Data/Pseudocode/Types.agda
@@ -77,82 +77,6 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁
     _/1 : ℤ → ℝ
     ⌊_⌋ : ℝ → ℤ
 
-  cast : ∀ {m n} → .(eq : m ≡ n) → Bits m → Bits n
-  cast eq x i = x $ Fin.cast (P.sym eq) i
-
-  2ℤ : ℤ
-  2ℤ = 2 ℤ′.×′ 1ℤ
-
-  getᵇ : ∀ {n} → Fin n → Bits n → Bit
-  getᵇ i x = x (opposite i)
-
-  setᵇ : ∀ {n} → Fin n → Bit → Op₁ (Bits n)
-  setᵇ i b = updateAt (opposite i) λ _ → b
-
-  sliceᵇ : ∀ {n} (i : Fin (suc n)) j → Bits n → Bits (toℕ (i - j))
-  sliceᵇ         zero    zero    x = []
-  sliceᵇ {suc n} (suc i) zero    x = getᵇ i x ∷ sliceᵇ i zero (tail x)
-  sliceᵇ {suc n} (suc i) (suc j) x = sliceᵇ i j (tail x)
-
-  updateᵇ : ∀ {n} (i : Fin (suc n)) j → Bits (toℕ (i - j)) → Op₁ (Bits n)
-  updateᵇ {n} = Induction.<-weakInduction P (λ _ _ → id) helper
-    where
-    P : Fin (suc n) → Set b₁
-    P i = ∀ j → Bits (toℕ (i - j)) → Op₁ (Bits n)
-
-    eq : ∀ {n} {i : Fin n} → toℕ i ≡ toℕ (inject₁ i)
-    eq = P.sym $ Fₚ.toℕ-inject₁ _
-
-    eq′ : ∀ {n} {i : Fin n} j → toℕ (i - j) ≡ toℕ (inject₁ i - Fin.cast eq j)
-    eq′             zero    = eq
-    eq′ {i = suc _} (suc j) = eq′ j
-
-    helper : ∀ i → P (inject₁ i) → P (suc i)
-    helper i rec zero    y = rec zero (cast eq (tail y)) ∘′ setᵇ i (y zero)
-    helper i rec (suc j) y = rec (Fin.cast eq j) (cast (eq′ j) y)
-
-  hasBit : ∀ {n} → Fin n → Bits n → Bool
-  hasBit i x = does (getᵇ i x ≟ᵇ₁ 1𝔹)
-
-  infixl 7 _div_ _mod_
-
-  _div_ : ∀ (x y : ℤ) → {y≉0 : False (y /1 ≟ʳ 0ℝ)} → ℤ
-  (x div y) {y≉0} = ⌊ x /1 ℝ.* toWitnessFalse y≉0 ℝ.⁻¹ ⌋
-
-  _mod_ : ∀ (x y : ℤ) → {y≉0 : False (y /1 ≟ʳ 0ℝ)} → ℤ
-  (x mod y) {y≉0} = x ℤ.+ ℤ.- y ℤ.* (x div y) {y≉0}
-
-  infixl 5 _<<_
-  _<<_ : ℤ → ℕ → ℤ
-  x << n = 2ℤ ℤ′.^′ n ℤ.* x
-
-  module ShiftNotZero
-    (1<<n≉0 : ∀ n → False ((1ℤ << n) /1 ≟ʳ 0ℝ))
-    where
-
-    infixl 5 _>>_
-    _>>_ : ℤ → ℕ → ℤ
-    x >> zero  = x
-    x >> suc n = (x div (1ℤ << suc n)) {1<<n≉0 (suc n)}
-
-    getᶻ : ℕ → ℤ → Bit
-    getᶻ n x =
-      if does ((x mod (1ℤ << suc n)) {1<<n≉0 (suc n)} <ᶻ? 1ℤ << n)
-      then 1𝔹
-      else 0𝔹
-
-    sliceᶻ : ∀ n i → ℤ → Bits (n ℕ-ℕ i)
-    sliceᶻ zero    zero    x = []
-    sliceᶻ (suc n) zero    x = getᶻ n x ∷ sliceᶻ n zero x
-    sliceᶻ (suc n) (suc i) x = sliceᶻ n i (x >> 1)
-
-  uint : ∀ {n} → Bits n → ℤ
-  uint x = ℤ′.sum λ i → if hasBit i x then 1ℤ << toℕ i else 0ℤ
-
-  sint : ∀ {n} → Bits n → ℤ
-  sint {zero}  x = 0ℤ
-  sint {suc n} x = uint x ℤ.+ ℤ.- (if hasBit (fromℕ n) x then 1ℤ << suc n else 0ℤ)
-
 record Pseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ :
                   Set (ℓsuc (b₁ ⊔ b₂ ⊔ i₁ ⊔ i₂ ⊔ i₃ ⊔ r₁ ⊔ r₂ ⊔ r₃)) where
   field
@@ -222,191 +146,3 @@ record Pseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ :
     ; _/1 = _/1
     ; ⌊_⌋ = ⌊_⌋
     }
-
-  open RawPseudocode rawPseudocode public
-    using
-    ( 2ℤ; cast; getᵇ; setᵇ; sliceᵇ; updateᵇ; hasBit
-    ; _div_; _mod_; _<<_; uint; sint
-    )
-
-  private
-    -- FIXME: move almost all of these proofs into a separate module
-    a<b⇒ca<cb : ∀ {a b c} → 0ℤ ℤ.< c → a ℤ.< b → c ℤ.* a ℤ.< c ℤ.* b
-    a<b⇒ca<cb {a} {b} {c} 0<c a<b = begin-strict
-      c ℤ.* a                     ≈˘⟨ ℤ.+-identityʳ _ ⟩
-      c ℤ.* a ℤ.+ 0ℤ              <⟨  ℤ.+-invariantˡ _ $ ℤ.0<a+0<b⇒0<ab 0<c 0<b-a ⟩
-      c ℤ.* a ℤ.+ c ℤ.* (b ℤ.- a) ≈˘⟨ ℤ.distribˡ c a (b ℤ.- a) ⟩
-      c ℤ.* (a ℤ.+ (b ℤ.- a))     ≈⟨  ℤ.*-congˡ $ ℤ.+-congˡ $ ℤ.+-comm b (ℤ.- a) ⟩
-      c ℤ.* (a ℤ.+ (ℤ.- a ℤ.+ b)) ≈˘⟨ ℤ.*-congˡ $ ℤ.+-assoc a (ℤ.- a) b ⟩
-      c ℤ.* ((a ℤ.+ ℤ.- a) ℤ.+ b) ≈⟨  ℤ.*-congˡ $ ℤ.+-congʳ $ ℤ.-‿inverseʳ a ⟩
-      c ℤ.* (0ℤ ℤ.+ b)            ≈⟨  (ℤ.*-congˡ $ ℤ.+-identityˡ b) ⟩
-      c ℤ.* b                     ∎
-      where
-      open ℤ-Reasoning
-
-      0<b-a : 0ℤ ℤ.< b ℤ.- a
-      0<b-a = begin-strict
-        0ℤ      ≈˘⟨ ℤ.-‿inverseʳ a ⟩
-        a ℤ.- a <⟨  ℤ.+-invariantʳ (ℤ.- a) a<b ⟩
-        b ℤ.- a ∎
-
-    -‿idem : ∀ x → ℤ.- (ℤ.- x) ℤ.≈ x
-    -‿idem x = begin-equality
-      ℤ.- (ℤ.- x)             ≈˘⟨ ℤ.+-identityˡ _ ⟩
-      0ℤ ℤ.- ℤ.- x            ≈˘⟨ ℤ.+-congʳ $ ℤ.-‿inverseʳ x ⟩
-      x ℤ.- x ℤ.- ℤ.- x       ≈⟨  ℤ.+-assoc x (ℤ.- x) _ ⟩
-      x ℤ.+ (ℤ.- x ℤ.- ℤ.- x) ≈⟨  ℤ.+-congˡ $ ℤ.-‿inverseʳ (ℤ.- x) ⟩
-      x ℤ.+ 0ℤ                ≈⟨  ℤ.+-identityʳ x ⟩
-      x                       ∎
-      where open ℤ-Reasoning
-
-    -a*b≈-ab : ∀ a b → ℤ.- a ℤ.* b ℤ.≈ ℤ.- (a ℤ.* b)
-    -a*b≈-ab a b = begin-equality
-      ℤ.- a ℤ.* b                           ≈˘⟨ ℤ.+-identityʳ _ ⟩
-      ℤ.- a ℤ.* b ℤ.+ 0ℤ                    ≈˘⟨ ℤ.+-congˡ $ ℤ.-‿inverseʳ _ ⟩
-      ℤ.- a ℤ.* b ℤ.+ (a ℤ.* b ℤ.- a ℤ.* b) ≈˘⟨ ℤ.+-assoc _ _ _ ⟩
-      ℤ.- a ℤ.* b ℤ.+ a ℤ.* b ℤ.- a ℤ.* b   ≈˘⟨ ℤ.+-congʳ $ ℤ.distribʳ b _ a ⟩
-      (ℤ.- a ℤ.+ a) ℤ.* b ℤ.- a ℤ.* b       ≈⟨  ℤ.+-congʳ $ ℤ.*-congʳ $ ℤ.-‿inverseˡ a ⟩
-      0ℤ ℤ.* b ℤ.- a ℤ.* b                  ≈⟨  ℤ.+-congʳ $ ℤ.zeroˡ b ⟩
-      0ℤ ℤ.- a ℤ.* b                        ≈⟨  ℤ.+-identityˡ _ ⟩
-      ℤ.- (a ℤ.* b)                         ∎
-      where open ℤ-Reasoning
-
-    a*-b≈-ab : ∀ a b → a ℤ.* ℤ.- b ℤ.≈ ℤ.- (a ℤ.* b)
-    a*-b≈-ab a b = begin-equality
-      a ℤ.* ℤ.- b   ≈⟨ ℤ.*-comm a (ℤ.- b) ⟩
-      ℤ.- b ℤ.* a   ≈⟨ -a*b≈-ab b a ⟩
-      ℤ.- (b ℤ.* a) ≈⟨ ℤ.-‿cong $ ℤ.*-comm b a ⟩
-      ℤ.- (a ℤ.* b) ∎
-      where open ℤ-Reasoning
-
-    0<a⇒0>-a : ∀ {a} → 0ℤ ℤ.< a → 0ℤ ℤ.> ℤ.- a
-    0<a⇒0>-a {a} 0<a = begin-strict
-      ℤ.- a    ≈˘⟨ ℤ.+-identityˡ _ ⟩
-      0ℤ ℤ.- a <⟨  ℤ.+-invariantʳ _ 0<a ⟩
-      a ℤ.- a  ≈⟨  ℤ.-‿inverseʳ a ⟩
-      0ℤ       ∎
-      where open ℤ-Reasoning
-
-    0>a⇒0<-a : ∀ {a} → 0ℤ ℤ.> a → 0ℤ ℤ.< ℤ.- a
-    0>a⇒0<-a {a} 0>a = begin-strict
-      0ℤ       ≈˘⟨ ℤ.-‿inverseʳ a ⟩
-      a ℤ.- a  <⟨  ℤ.+-invariantʳ _ 0>a ⟩
-      0ℤ ℤ.- a ≈⟨  ℤ.+-identityˡ _ ⟩
-      ℤ.- a    ∎
-      where open ℤ-Reasoning
-
-    0<-a⇒0>a : ∀ {a} → 0ℤ ℤ.< ℤ.- a → 0ℤ ℤ.> a
-    0<-a⇒0>a {a} 0<-a = begin-strict
-      a        ≈˘⟨ ℤ.+-identityʳ a ⟩
-      a ℤ.+ 0ℤ <⟨  ℤ.+-invariantˡ a 0<-a ⟩
-      a ℤ.- a  ≈⟨  ℤ.-‿inverseʳ a ⟩
-      0ℤ       ∎
-      where open ℤ-Reasoning
-
-    0>-a⇒0<a : ∀ {a} → 0ℤ ℤ.> ℤ.- a → 0ℤ ℤ.< a
-    0>-a⇒0<a {a} 0>-a = begin-strict
-      0ℤ       ≈˘⟨ ℤ.-‿inverseʳ a ⟩
-      a ℤ.- a  <⟨  ℤ.+-invariantˡ a 0>-a ⟩
-      a ℤ.+ 0ℤ ≈⟨  ℤ.+-identityʳ a ⟩
-      a        ∎
-      where open ℤ-Reasoning
-
-    0>a+0<b⇒0>ab : ∀ {a b} → 0ℤ ℤ.> a → 0ℤ ℤ.< b → 0ℤ ℤ.> a ℤ.* b
-    0>a+0<b⇒0>ab {a} {b} 0>a 0<b = 0<-a⇒0>a $ begin-strict
-      0ℤ              <⟨ ℤ.0<a+0<b⇒0<ab (0>a⇒0<-a 0>a) 0<b ⟩
-      ℤ.- a ℤ.* b     ≈⟨ -a*b≈-ab a b ⟩
-      ℤ.- (a ℤ.* b)   ∎
-      where open ℤ-Reasoning
-
-    0<a+0>b⇒0>ab : ∀ {a b} → 0ℤ ℤ.< a → 0ℤ ℤ.> b → 0ℤ ℤ.> a ℤ.* b
-    0<a+0>b⇒0>ab {a} {b} 0<a 0>b = 0<-a⇒0>a $ begin-strict
-      0ℤ              <⟨ ℤ.0<a+0<b⇒0<ab 0<a (0>a⇒0<-a 0>b) ⟩
-      a ℤ.* ℤ.- b     ≈⟨ a*-b≈-ab a b ⟩
-      ℤ.- (a ℤ.* b)   ∎
-      where open ℤ-Reasoning
-
-    0>a+0>b⇒0<ab : ∀ {a b} → 0ℤ ℤ.> a → 0ℤ ℤ.> b → 0ℤ ℤ.< a ℤ.* b
-    0>a+0>b⇒0<ab {a} {b} 0>a 0>b = begin-strict
-      0ℤ                  <⟨ ℤ.0<a+0<b⇒0<ab (0>a⇒0<-a 0>a) (0>a⇒0<-a 0>b) ⟩
-      ℤ.- a ℤ.* ℤ.- b     ≈⟨ -a*b≈-ab a (ℤ.- b) ⟩
-      ℤ.- (a ℤ.* ℤ.- b)   ≈⟨ ℤ.-‿cong $ a*-b≈-ab a b ⟩
-      ℤ.- (ℤ.- (a ℤ.* b)) ≈⟨ -‿idem (a ℤ.* b) ⟩
-      a ℤ.* b             ∎
-      where open ℤ-Reasoning
-
-    a≉0+b≉0⇒ab≉0 : ∀ {a b} → a ℤ.≉ 0ℤ → b ℤ.≉ 0ℤ → a ℤ.* b ℤ.≉ 0ℤ
-    a≉0+b≉0⇒ab≉0 {a} {b} a≉0 b≉0 ab≈0 with ℤ.compare a 0ℤ | ℤ.compare b 0ℤ
-    ... | tri< a<0 _ _ | tri< b<0 _ _ = ℤ.irrefl (ℤ.Eq.sym ab≈0) $ 0>a+0>b⇒0<ab a<0 b<0
-    ... | tri< a<0 _ _ | tri≈ _ b≈0 _ = b≉0 b≈0
-    ... | tri< a<0 _ _ | tri> _ _ b>0 = ℤ.irrefl ab≈0 $ 0>a+0<b⇒0>ab a<0 b>0
-    ... | tri≈ _ a≈0 _ | _            = a≉0 a≈0
-    ... | tri> _ _ a>0 | tri< b<0 _ _ = ℤ.irrefl ab≈0 $ 0<a+0>b⇒0>ab a>0 b<0
-    ... | tri> _ _ a>0 | tri≈ _ b≈0 _ = b≉0 b≈0
-    ... | tri> _ _ a>0 | tri> _ _ b>0 = ℤ.irrefl (ℤ.Eq.sym ab≈0) $ ℤ.0<a+0<b⇒0<ab a>0 b>0
-
-    ab≈0⇒a≈0⊎b≈0 : ∀ {a b} → a ℤ.* b ℤ.≈ 0ℤ → a ℤ.≈ 0ℤ ⊎ b ℤ.≈ 0ℤ
-    ab≈0⇒a≈0⊎b≈0 {a} {b} ab≈0 with a ℤ.≟ 0ℤ | b ℤ.≟ 0ℤ
-    ... | yes a≈0 | _       = inj₁ a≈0
-    ... | no a≉0  | yes b≈0 = inj₂ b≈0
-    ... | no a≉0  | no b≉0  = ⊥-elim (a≉0+b≉0⇒ab≉0 a≉0 b≉0 ab≈0)
-
-    2a<<n≈a<<1+n : ∀ a n → 2ℤ ℤ.* (a << n) ℤ.≈ a << suc n
-    2a<<n≈a<<1+n a zero    = ℤ.*-congˡ $ ℤ.*-identityˡ a
-    2a<<n≈a<<1+n a (suc n) = begin-equality
-      2ℤ ℤ.* (a << suc n) ≈˘⟨ ℤ.*-assoc 2ℤ _ a ⟩
-      (2ℤ ℤ.* _) ℤ.* a    ≈⟨  ℤ.*-congʳ $ ℤ.*-comm 2ℤ _ ⟩
-      a << suc (suc n)    ∎
-      where open ℤ-Reasoning
-
-    0<1 : 0ℤ ℤ.< 1ℤ
-    0<1 with ℤ.compare 0ℤ 1ℤ
-    ... | tri< 0<1 _ _ = 0<1
-    ... | tri≈ _ 0≈1 _ = ⊥-elim (1≉0 (ℤ.Eq.sym 0≈1))
-    ... | tri> _ _ 0>1 = begin-strict
-        0ℤ                  ≈˘⟨ ℤ.zeroʳ (ℤ.- 1ℤ) ⟩
-        ℤ.- 1ℤ ℤ.* 0ℤ       <⟨  a<b⇒ca<cb (0>a⇒0<-a 0>1) (0>a⇒0<-a 0>1) ⟩
-        ℤ.- 1ℤ ℤ.* ℤ.- 1ℤ   ≈⟨  -a*b≈-ab 1ℤ (ℤ.- 1ℤ) ⟩
-        ℤ.- (1ℤ ℤ.* ℤ.- 1ℤ) ≈⟨  ℤ.-‿cong $ ℤ.*-identityˡ (ℤ.- 1ℤ) ⟩
-        ℤ.- (ℤ.- 1ℤ)        ≈⟨  -‿idem 1ℤ ⟩
-        1ℤ                  ∎
-      where open ℤ-Reasoning
-
-    0<2 : 0ℤ ℤ.< 2ℤ
-    0<2 = begin-strict
-      0ℤ        ≈˘⟨ ℤ.+-identity² ⟩
-      0ℤ ℤ.+ 0ℤ <⟨  ℤ.+-invariantˡ 0ℤ 0<1 ⟩
-      0ℤ ℤ.+ 1ℤ <⟨  ℤ.+-invariantʳ 1ℤ 0<1 ⟩
-      2ℤ        ∎
-      where open ℤ-Reasoning
-
-    1<<n≉0 : ∀ n → 1ℤ << n ℤ.≉ 0ℤ
-    1<<n≉0 zero          eq = 1≉0 1≈0
-      where
-      open ℤ-Reasoning
-      1≈0 = begin-equality
-        1ℤ        ≈˘⟨ ℤ.*-identity² ⟩
-        1ℤ ℤ.* 1ℤ ≈⟨  eq ⟩
-        0ℤ        ∎
-    1<<n≉0 (suc zero)    eq = ℤ.irrefl 0≈2 0<2
-      where
-      open ℤ-Reasoning
-      0≈2 = begin-equality
-        0ℤ        ≈˘⟨ eq ⟩
-        2ℤ ℤ.* 1ℤ ≈⟨  ℤ.*-identityʳ 2ℤ ⟩
-        2ℤ        ∎
-    1<<n≉0 (suc (suc n)) eq =
-      [ (λ 2≈0 → ℤ.irrefl (ℤ.Eq.sym 2≈0) 0<2) , 1<<n≉0 (suc n) ]′
-      $ ab≈0⇒a≈0⊎b≈0 $ ℤ.Eq.trans (2a<<n≈a<<1+n 1ℤ (suc n)) eq
-
-    1<<n≉0ℝ : ∀ n → (1ℤ << n) /1 ℝ.≉ 0ℝ
-    1<<n≉0ℝ n eq = 1<<n≉0 n $ (begin-equality
-      1ℤ << n          ≈˘⟨ ⌊⌋∘/1≗id (1ℤ << n) ⟩
-      ⌊ (1ℤ << n) /1 ⌋ ≈⟨  ⌊⌋.cong $ eq ⟩
-      ⌊ 0ℝ ⌋           ≈⟨  ⌊⌋.0#-homo ⟩
-      0ℤ               ∎)
-      where open ℤ-Reasoning
-
-    open RawPseudocode rawPseudocode using (module ShiftNotZero)
-
-  open ShiftNotZero (λ n → fromWitnessFalse (1<<n≉0ℝ n)) public
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
new file mode 100644
index 0000000..6dd76b0
--- /dev/null
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -0,0 +1,323 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Base definitions for the denotational semantics.
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Data.Pseudocode.Types using (RawPseudocode)
+
+module Helium.Semantics.Denotational.Core
+  {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
+  (rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃)
+  where
+
+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; #_)
+import Data.Fin.Properties as Finₚ
+open import Data.Nat as ℕ using (ℕ; zero; suc)
+import Data.Nat.Properties as ℕₚ
+open import Data.Product as P using (_×_; _,_)
+open import Data.Sum as S using (_⊎_) renaming (inj₁ to next; inj₂ to ret)
+open import Data.Unit using (⊤)
+open import Data.Vec as Vec using (Vec; []; _∷_)
+open import Data.Vec.Relation.Unary.All using (All; []; _∷_)
+import Data.Vec.Functional as VecF
+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 Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
+open import Relation.Nullary using (does)
+open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromWitness)
+
+⟦_⟧ₗ : Type → Level
+⟦ unit ⟧ₗ       = 0ℓ
+⟦ bool ⟧ₗ       = 0ℓ
+⟦ int ⟧ₗ        = i₁
+⟦ fin n ⟧ₗ      = 0ℓ
+⟦ real ⟧ₗ       = r₁
+⟦ bits n ⟧ₗ     = b₁
+⟦ tuple n ts ⟧ₗ = helper ts
+  where
+  helper : ∀ {n} → Vec Type n → Level
+  helper []       = 0ℓ
+  helper (t ∷ ts) = ⟦ t ⟧ₗ ⊔ helper ts
+⟦ array t n ⟧ₗ  = ⟦ t ⟧ₗ
+
+⟦_⟧ₜ : ∀ t → Set ⟦ t ⟧ₗ
+⟦_⟧ₜ′ : ∀ {n} ts → Set ⟦ tuple n ts ⟧ₗ
+
+⟦ unit ⟧ₜ       = ⊤
+⟦ bool ⟧ₜ       = Bool
+⟦ int ⟧ₜ        = ℤ
+⟦ fin n ⟧ₜ      = Fin n
+⟦ real ⟧ₜ       = ℝ
+⟦ bits n ⟧ₜ     = Bits n
+⟦ tuple n ts ⟧ₜ = ⟦ ts ⟧ₜ′
+⟦ array t n ⟧ₜ  = Vec ⟦ t ⟧ₜ n
+
+⟦ [] ⟧ₜ′          = ⟦ unit ⟧ₜ
+⟦ t ∷ [] ⟧ₜ′      = ⟦ t ⟧ₜ
+⟦ t ∷ t′ ∷ ts ⟧ₜ′ = ⟦ t ⟧ₜ × ⟦ t′ ∷ ts ⟧ₜ′
+
+-- 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)
+
+
+fetch : ∀ {n} ts → ⟦ tuple n ts ⟧ₜ → ∀ i → ⟦ Vec.lookup ts i ⟧ₜ
+fetch (_ ∷ [])     x        zero    = x
+fetch (_ ∷ _ ∷ _)  (x , xs) zero    = x
+fetch (_ ∷ t ∷ ts) (x , xs) (suc i) = fetch (t ∷ ts) xs i
+
+updateAt : ∀ {n} ts i → ⟦ Vec.lookup ts i ⟧ₜ → ⟦ tuple n ts ⟧ₜ → ⟦ tuple n ts ⟧ₜ
+updateAt (_ ∷ [])     zero    v _        = v
+updateAt (_ ∷ _ ∷ _)  zero    v (_ , xs) = v , xs
+updateAt (_ ∷ t ∷ ts) (suc i) v (x , xs) = x , updateAt (t ∷ ts) i v xs
+
+tupCons : ∀ {n t} ts → ⟦ t ⟧ₜ → ⟦ tuple n ts ⟧ₜ → ⟦ tuple _ (t ∷ ts) ⟧ₜ
+tupCons []       x xs = x
+tupCons (t ∷ ts) x xs = x , xs
+
+tupHead : ∀ {n t} ts → ⟦ tuple (suc n) (t ∷ ts) ⟧ₜ → ⟦ t ⟧ₜ
+tupHead {t = t} ts xs = fetch (t ∷ ts) xs zero
+
+tupTail : ∀ {n t} ts → ⟦ tuple _ (t ∷ ts) ⟧ₜ → ⟦ tuple n ts ⟧ₜ
+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 bits x y = does (x ≟ᵇ y)
+
+comp : ∀ {t} → IsNumeric t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ → Bool
+comp int  x y = does (x <ᶻ? y)
+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
+
+-- take from 0
+take : ∀ t i {j} → ⟦ asType t (i ℕ.+ j) ⟧ₜ → ⟦ asType t i ⟧ₜ
+take bits      i x = VecF.take i x
+take (array _) i x = Vec.take i x
+
+-- drop from 0
+drop : ∀ t i {j} → ⟦ asType t (i ℕ.+ j) ⟧ₜ → ⟦ asType t j ⟧ₜ
+drop bits      i x = VecF.drop i x
+drop (array _) i x = Vec.drop i x
+
+casted : ∀ t {i j} → .(eq : i ≡ j) → ⟦ asType t i ⟧ₜ → ⟦ asType t j ⟧ₜ
+casted bits                  eq x       = x ∘′ Fin.cast (≡.sym eq)
+casted (array _) {j = zero}  eq []      = []
+casted (array t) {j = suc _} eq (x ∷ y) = x ∷ casted (array t) (ℕₚ.suc-injective eq) y
+
+module _ where
+  m≤n⇒m+k≡n : ∀ {m n} → m ℕ.≤ n → P.∃ λ k → m ℕ.+ k ≡ n
+  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) ∎)
+    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))
+
+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))
+
+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₁ = 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₁ = 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
+mul {t₁ = real} {t₂ = real} _ _ x y = x ℝ.* y
+
+pow : ∀ {t} → IsNumeric t → ⟦ t ⟧ₜ → ℕ → ⟦ t ⟧ₜ
+pow int  x n = x ℤ′.^′ n
+pow real x n = x ℝ′.^′ n
+
+shiftr : 2 ℝ′.×′ 1ℝ ℝ.≉ 0ℝ → ⟦ int ⟧ₜ → ℕ → ⟦ int ⟧ₜ
+shiftr 2≉0 x n = ⌊ x /1 ℝ.* 2≉0 ℝ.⁻¹ ℝ′.^′ n ⌋
+
+module _
+  {o} {Σ : Vec Type o}
+  (2≉0 : 2 ℝ′.×′ 1ℝ ℝ.≉ 0ℝ)
+  where
+
+  open Code Σ
+
+  ⟦_⟧ᵉ : ∀ {n} {Γ : Vec Type n} {t} → Expression Γ t → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × ⟦ t ⟧ₜ
+  ⟦_⟧ˢ : ∀ {n} {Γ : Vec Type n} {ret} → Statement Γ 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
+  -- ⟦ 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 ⟧ᵉ σ γ)
+    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 [] ⟧ᵉ σ γ = σ , _
+  ⟦ 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 σ′ , v = ⟦ s ⟧ˢ σ γ
+    S.[ ⟦ s ⟧ˢ σ′ , (λ v → σ′ , ret v) ] v
+  ⟦ skip ⟧ˢ σ γ = σ , next γ
+  ⟦ _≔_ ref {canAssign = canAssign} e ⟧ˢ σ γ = do
+    let σ′ , v = ⟦ e ⟧ᵉ σ γ
+    let σ′′ , γ′ = update (toWitness canAssign) v σ′ γ
+    σ′′ , next γ′
+  ⟦_⟧ˢ {Γ = Γ} (declare e s) σ γ = do
+    let σ′ , x = ⟦ e ⟧ᵉ σ γ
+    let σ′′ , v = ⟦ s ⟧ˢ σ′ (tupCons Γ x γ)
+    σ′′ , S.map₁ (tupTail Γ) v
+  ⟦ invoke p e ⟧ˢ σ γ = do
+    let σ′ , v = ⟦ e ⟧ᵉ σ γ
+    ⟦ p ⟧ᵖ σ′ v , next γ
+  ⟦ if e then s₁ else s₂ ⟧ˢ σ γ = do
+    let σ′ , x = ⟦ e ⟧ᵉ σ γ
+    Bool.if x then ⟦ s₁ ⟧ˢ σ′ γ else ⟦ s₂ ⟧ˢ σ′ γ
+  ⟦_⟧ˢ {Γ = Γ} {ret = t} (for m s) σ γ = helper m ⟦ s ⟧ˢ σ γ
+    where
+    helper : ∀ m → (⟦ Σ ⟧ₜ′ → ⟦ fin m ∷ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × (⟦ fin m ∷ Γ ⟧ₜ′ ⊎ ⟦ t ⟧ₜ)) → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × (⟦ Γ ⟧ₜ′ ⊎ ⟦ t ⟧ₜ)
+    helper zero    s σ γ = σ , next γ
+    helper (suc m) s σ γ with s σ (tupCons Γ zero γ)
+    ... | σ′ , ret v   = σ′ , ret v
+    ... | σ′ , next γ′ = helper m s′ σ′ (tupTail Γ γ′)
+      where
+      s′ : ⟦ Σ ⟧ₜ′ → ⟦ fin m ∷ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × (⟦ fin m ∷ Γ ⟧ₜ′ ⊎ ⟦ t ⟧ₜ)
+      s′ σ γ =
+        P.map₂ (S.map₁ (tupCons Γ (tupHead Γ γ) ∘′ (tupTail Γ)))
+               (s σ (tupCons Γ (suc (tupHead Γ γ)) (tupTail Γ γ)))
+
+  ⟦ s ∙return e ⟧ᶠ σ γ with ⟦ s ⟧ˢ σ γ
+  ... | σ′ , ret v   = σ′ , v
+  ... | σ′ , next γ′ = ⟦ e ⟧ᵉ σ′ γ′
+  ⟦_⟧ᶠ {Γ = Γ} (declare e f) σ γ = do
+    let σ′ , x = ⟦ e ⟧ᵉ σ γ
+    ⟦ f ⟧ᶠ σ′ (tupCons Γ x γ)
+
+  ⟦ s ∙end ⟧ᵖ σ γ = P.proj₁ (⟦ s ⟧ˢ σ γ)
+  ⟦_⟧ᵖ {Γ = Γ} (declare e p) σ γ = do
+    let σ′ , x = ⟦ e ⟧ᵉ σ γ
+    ⟦ p ⟧ᵖ σ′ (tupCons Γ x γ)
+
+  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 σ γ = do
+    let σ′ , off = ⟦ e₂ ⟧ᵉ σ γ
+    let σ′′ , orig = ⟦ e₁ ⟧ᵉ σ′ γ
+    updateSliced t orig off 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 σ γ
+  update (tup {es = _ ∷ _ ∷ _} (x ∷ xs)) (v , vs) σ γ = do
+    let σ′ , γ′ = update x v σ γ
+    update (tup xs) vs σ′ γ′