From c86ae0d13408aa3dc2fccde9abacd116d33af7dd Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Tue, 8 Mar 2022 15:44:13 +0000
Subject: Add reference substitution to terms.

---
 src/Helium/Data/Pseudocode/Core.agda        |  18 +-
 src/Helium/Semantics/Axiomatic/Term.agda    | 333 +++++++++++++++-------------
 src/Helium/Semantics/Denotational/Core.agda |  16 +-
 3 files changed, 201 insertions(+), 166 deletions(-)

(limited to 'src')

diff --git a/src/Helium/Data/Pseudocode/Core.agda b/src/Helium/Data/Pseudocode/Core.agda
index a229e8a..86bbffd 100644
--- a/src/Helium/Data/Pseudocode/Core.agda
+++ b/src/Helium/Data/Pseudocode/Core.agda
@@ -43,7 +43,7 @@ data HasEquality : Type → Set where
   fin  : ∀ {n} → HasEquality (fin n)
   real : HasEquality real
   bit  : HasEquality bit
-  bits : ∀ {n} → HasEquality (bits n)
+  bits : ∀ n → HasEquality (bits n)
 
 hasEquality? : Decidable HasEquality
 hasEquality? bool        = yes bool
@@ -51,7 +51,7 @@ hasEquality? int         = yes int
 hasEquality? (fin n)     = yes fin
 hasEquality? real        = yes real
 hasEquality? bit         = yes bit
-hasEquality? (bits n)    = yes bits
+hasEquality? (bits n)    = yes (bits n)
 hasEquality? (tuple n x) = no (λ ())
 hasEquality? (array t n) = no (λ ())
 
@@ -69,10 +69,10 @@ isNumeric? (bits n)    = no (λ ())
 isNumeric? (tuple n x) = no (λ ())
 isNumeric? (array t n) = no (λ ())
 
-combineNumeric : ∀ t₁ t₂ → {isNumeric₁ : True (isNumeric? t₁)} → {isNumeric₂ : True (isNumeric? t₂)} → Type
-combineNumeric int  int  = int
-combineNumeric int  real = real
-combineNumeric real _    = real
+combineNumeric : ∀ t₁ t₂ → (isNumeric₁ : True (isNumeric? t₁)) → (isNumeric₂ : True (isNumeric? t₂)) → Type
+combineNumeric int  int  _ _ = int
+combineNumeric int  real _ _ = real
+combineNumeric real _    _ _ = real
 
 data Sliced : Set where
   bits  : Sliced
@@ -147,8 +147,8 @@ module Code {o} (Σ : Vec Type o) where
     cut    : ∀ {m n t} → Expression Γ (asType t (n ℕ.+ m)) → Expression Γ (fin (suc n)) → Expression Γ (tuple 2 (asType t m ∷ asType t n ∷ []))
     cast   : ∀ {i j t} → .(eq : i ≡ j) → Expression Γ (asType t i) → Expression Γ (asType t j)
     -_     : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → Expression Γ t
-    _+_    : ∀ {t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ {isNumeric₁} {isNumeric₂})
-    _*_    : ∀ {t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ {isNumeric₁} {isNumeric₂})
+    _+_    : ∀ {t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ isNumeric₁ isNumeric₂)
+    _*_    : ∀ {t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ isNumeric₁ isNumeric₂)
     -- _/_   : Expression Γ real → Expression Γ real → Expression Γ real
     _^_    : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → ℕ → Expression Γ t
     _>>_   : Expression Γ int → ℕ → Expression Γ int
@@ -312,7 +312,7 @@ module Code {o} (Σ : Vec Type o) where
   slice′ : ∀ {n Γ i j t} → Expression {n} Γ (asType t (i ℕ.+ j)) → Expression Γ (fin (suc j)) → Expression Γ (asType t i)
   slice′ {i = i} e₁ e₂ = slice (cast (+-comm i _) e₁) e₂
 
-  _-_   : ∀ {n Γ t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression {n} Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ {isNumeric₁} {isNumeric₂})
+  _-_   : ∀ {n Γ t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression {n} Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ isNumeric₁ isNumeric₂)
   _-_ {isNumeric₂ = isNumeric₂} x y = x + (-_ {isNumeric = isNumeric₂} y)
 
   _<<_ : ∀ {n Γ} → Expression {n} Γ int → ℕ → Expression Γ int
diff --git a/src/Helium/Semantics/Axiomatic/Term.agda b/src/Helium/Semantics/Axiomatic/Term.agda
index 980b85a..1ccef89 100644
--- a/src/Helium/Semantics/Axiomatic/Term.agda
+++ b/src/Helium/Semantics/Axiomatic/Term.agda
@@ -23,14 +23,15 @@ open import Data.Nat as ℕ using (ℕ; suc)
 import Data.Nat.Properties as ℕₚ
 open import Data.Product using (∃; _×_; _,_; proj₁; proj₂; uncurry; dmap)
 open import Data.Vec as Vec using (Vec; []; _∷_; _++_; lookup)
+import Data.Vec.Functional as VecF
 import Data.Vec.Properties as Vecₚ
 open import Data.Vec.Relation.Unary.All using (All; []; _∷_)
-open import Function using (_∘_; _∘₂_; id)
+open import Function using (_∘_; _∘₂_; id; flip)
 open import Helium.Data.Pseudocode.Core
 import Helium.Data.Pseudocode.Manipulate as M
 open import Helium.Semantics.Axiomatic.Core rawPseudocode
 open import Level using (_⊔_; lift; lower)
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality hiding ([_]) renaming (subst to ≡-subst)
 open import Relation.Nullary using (does; yes; no; ¬_)
 open import Relation.Nullary.Decidable.Core using (True; toWitness)
 open import Relation.Nullary.Negation using (contradiction)
@@ -51,7 +52,7 @@ castType : Term Σ Γ Δ t → t ≡ t′ → Term Σ Γ Δ t′
 castType (state i)   refl = state i
 castType (var i)     refl = var i
 castType (meta i)    refl = meta i
-castType (func f ts) eq   = func (subst (Transform _) eq f) ts
+castType (func f ts) eq   = func (≡-subst (Transform _) eq f) ts
 
 substState : Term Σ Γ Δ t → ∀ i → Term Σ Γ Δ (lookup Σ i) → Term Σ Γ Δ t
 substState (state i) j t′ with i Fin.≟ j
@@ -141,20 +142,147 @@ wknMetas τs (func f ts) = func f (helper ts)
   helper []       = []
   helper (t ∷ ts) = wknMetas τs t ∷ helper ts
 
-module _ {Σ : Vec Type o} (2≉0 : ¬ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ) where
-  open Code Σ
+func₀ : ⟦ t ⟧ₜ → Term Σ Γ Δ t
+func₀ f = func (λ _ → f) []
 
-  𝒦 : Literal t → Term Σ Γ Δ t
-  𝒦 (x ′b) = func (λ _ → lift x) []
-  𝒦 (x ′i) = func (λ _ → lift (x ℤ′.×′ 1ℤ)) []
-  𝒦 (x ′f) = func (λ _ → lift x) []
-  𝒦 (x ′r) = func (λ _ → lift (x ℝ′.×′ 1ℝ)) []
-  𝒦 (x ′x) = func (λ _ → lift (Bool.if x then 1𝔹 else 0𝔹)) []
-  𝒦 ([] ′xs) = func (λ _ → []) []
-  𝒦 ((x ∷ xs) ′xs) = func (λ (x , xs , _) → xs Vec.∷ʳ x) (𝒦 (x ′x) ∷ 𝒦 (xs ′xs) ∷ [])
-  𝒦 (x ′a) = func (λ (x , _) → Vec.replicate x) (𝒦 x ∷ [])
+func₁ : (⟦ t ⟧ₜ → ⟦ t′ ⟧ₜ) → Term Σ Γ Δ t → Term Σ Γ Δ t′
+func₁ f t = func (λ (x , _) → f x) (t ∷ [])
 
-  ℰ : Expression Γ t → Term Σ Γ Δ t
+func₂ : (⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ t′ ⟧ₜ) → Term Σ Γ Δ t₁ → Term Σ Γ Δ t₂ → Term Σ Γ Δ t′
+func₂ f t₁ t₂ = func (λ (x , y , _) → f x y) (t₁ ∷ t₂ ∷ [])
+
+[_][_≟_] : HasEquality t → Term Σ Γ Δ t → Term Σ Γ Δ t → Term Σ Γ Δ bool
+[ bool ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x Bool.≟ y))) t t′
+[ int ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x ≟ᶻ y))) t t′
+[ fin ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x Fin.≟ y))) t t′
+[ real ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x ≟ʳ y))) t t′
+[ bit ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x ≟ᵇ₁ y))) t t′
+[ bits n ][ t ≟ t′ ] = func₂ (λ xs ys → lift (does (VecF.fromVec (Vec.map lower xs) ≟ᵇ VecF.fromVec (Vec.map lower ys)))) t t′
+
+[_][_<?_] : IsNumeric t → Term Σ Γ Δ t → Term Σ Γ Δ t → Term Σ Γ Δ bool
+[ int ][ t <? t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x <ᶻ? y))) t t′
+[ real ][ t <? t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x <ʳ? y))) t t′
+
+[_][_] : ∀ t → Term Σ Γ Δ (elemType t) → Term Σ Γ Δ (asType t 1)
+[ bits ][ t ] = func₁ (_∷ []) t
+[ array τ ][ t ] = func₁ (_∷ []) t
+
+unbox : ∀ t → Term Σ Γ Δ (asType t 1) → Term Σ Γ Δ (elemType t)
+unbox bits = func₁ Vec.head
+unbox (array t) = func₁ Vec.head
+
+castV : ∀ {a} {A : Set a} {m n} → .(eq : m ≡ n) → Vec A m → Vec A n
+castV {n = 0}     eq []       = []
+castV {n = suc n} eq (x ∷ xs) = x ∷ castV (ℕₚ.suc-injective eq) xs
+
+cast′ : ∀ t → .(eq : m ≡ n) → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ
+cast′ bits      eq = castV eq
+cast′ (array τ) eq = castV eq
+
+cast : ∀ t → .(eq : m ≡ n) → Term Σ Γ Δ (asType t m) → Term Σ Γ Δ (asType t n)
+cast τ eq = func₁ (cast′ τ eq)
+
+[_][-_] : IsNumeric t → Term Σ Γ Δ t → Term Σ Γ Δ t
+[ int ][- t ] = func₁ (lift ∘ ℤ.-_ ∘ lower) t
+[ real ][- t ] = func₁ (lift ∘ ℝ.-_ ∘ lower) t
+
+[_,_,_,_][_+_] : ∀ t₁ t₂ → (isNum₁ : True (isNumeric? t₁)) → (isNum₂ : True (isNumeric? t₂)) → Term Σ Γ Δ t₁ → Term Σ Γ Δ t₂ → Term Σ Γ Δ (combineNumeric t₁ t₂ isNum₁ isNum₂)
+[ int , int , _ , _ ][ t + t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℤ.+ y)) t t′
+[ int , real , _ , _ ][ t + t′ ] = func₂ (λ (lift x) (lift y) → lift (x /1 ℝ.+ y)) t t′
+[ real , int , _ , _ ][ t + t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℝ.+ y /1)) t t′
+[ real , real , _ , _ ][ t + t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℝ.+ y)) t t′
+
+[_,_,_,_][_*_] : ∀ t₁ t₂ → (isNum₁ : True (isNumeric? t₁)) → (isNum₂ : True (isNumeric? t₂)) → Term Σ Γ Δ t₁ → Term Σ Γ Δ t₂ → Term Σ Γ Δ (combineNumeric t₁ t₂ isNum₁ isNum₂)
+[ int , int , _ , _ ][ t * t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℤ.* y)) t t′
+[ int , real , _ , _ ][ t * t′ ] = func₂ (λ (lift x) (lift y) → lift (x /1 ℝ.* y)) t t′
+[ real , int , _ , _ ][ t * t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℝ.* y /1)) t t′
+[ real , real , _ , _ ][ t * t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℝ.* y)) t t′
+
+[_][_^_] : IsNumeric t → Term Σ Γ Δ t → ℕ → Term Σ Γ Δ t
+[ int ][ t ^ n ] = func₁ (lift ∘ (ℤ′._^′ n) ∘ lower) t
+[ real ][ t ^ n ] = func₁ (lift ∘ (ℝ′._^′ n) ∘ lower) t
+
+2≉0 : Set _
+2≉0 = ¬ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ
+
+[_][_>>_] : 2≉0 → Term Σ Γ Δ int → ℕ → Term Σ Γ Δ int
+[ 2≉0 ][ t >> n ] = func₁ (lift ∘ ⌊_⌋ ∘ (ℝ._* 2≉0 ℝ.⁻¹ ℝ′.^′ n) ∘ _/1 ∘ lower) t
+
+-- 0 of y is 0 of result
+join′ : ∀ t → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ → ⟦ asType t (n ℕ.+ m) ⟧ₜ
+join′ bits      = flip _++_
+join′ (array t) = flip _++_
+
+take′ : ∀ t m {n} → ⟦ asType t (m ℕ.+ n) ⟧ₜ → ⟦ asType t m ⟧ₜ
+take′ bits      m = Vec.take m
+take′ (array t) m = Vec.take m
+
+drop′ : ∀ t m {n} → ⟦ asType t (m ℕ.+ n) ⟧ₜ → ⟦ asType t n ⟧ₜ
+drop′ bits      m = Vec.drop m
+drop′ (array t) m = Vec.drop m
+
+private
+  m≤n⇒m+k≡n : ∀ {m n} → m ℕ.≤ n → ∃ λ k → m ℕ.+ k ≡ n
+  m≤n⇒m+k≡n ℕ.z≤n       = _ , refl
+  m≤n⇒m+k≡n (ℕ.s≤s m≤n) = dmap id (cong suc) (m≤n⇒m+k≡n m≤n)
+
+  slicedSize : ∀ n m (i : Fin (suc n)) → ∃ λ k → n ℕ.+ m ≡ Fin.toℕ i ℕ.+ (m ℕ.+ k) × Fin.toℕ i ℕ.+ k ≡ n
+  slicedSize n m i = k , (begin
+    n ℕ.+ m                 ≡˘⟨ cong (ℕ._+ m) (proj₂ i+k≡n) ⟩
+    (Fin.toℕ i ℕ.+ k) ℕ.+ m ≡⟨  ℕₚ.+-assoc (Fin.toℕ i) k m ⟩
+    Fin.toℕ i ℕ.+ (k ℕ.+ m) ≡⟨  cong (Fin.toℕ i ℕ.+_) (ℕₚ.+-comm k m) ⟩
+    Fin.toℕ i ℕ.+ (m ℕ.+ k) ∎) ,
+    proj₂ i+k≡n
+    where
+    open ≡-Reasoning
+    i+k≡n = m≤n⇒m+k≡n (ℕₚ.≤-pred (Finₚ.toℕ<n i))
+    k = proj₁ i+k≡n
+
+-- 0 of x is i of result
+splice′ : ∀ t → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ → ⟦ fin (suc n) ⟧ₜ → ⟦ asType t (n ℕ.+ m) ⟧ₜ
+splice′ {m = m} t x y (lift i) = cast′ t eq (join′ t (join′ t high x) low)
+  where
+  reasoning = slicedSize _ m i
+  k = proj₁ reasoning
+  n≡i+k = sym (proj₂ (proj₂ reasoning))
+  low = take′ t (Fin.toℕ i) (cast′ t n≡i+k y)
+  high = drop′ t (Fin.toℕ i) (cast′ t n≡i+k y)
+  eq = sym (proj₁ (proj₂ reasoning))
+
+splice : ∀ t → Term Σ Γ Δ (asType t m) → Term Σ Γ Δ (asType t n) → Term Σ Γ Δ (fin (suc n)) → Term Σ Γ Δ (asType t (n ℕ.+ m))
+splice τ t₁ t₂ t′ = func (λ (x , y , i , _) → splice′ τ x y i) (t₁ ∷ t₂ ∷ t′ ∷ [])
+
+-- i of x is 0 of first
+cut′ : ∀ t → ⟦ asType t (n ℕ.+ m) ⟧ₜ → ⟦ fin (suc n) ⟧ₜ → ⟦ asType t m ∷ asType t n ∷ [] ⟧ₜ′
+cut′ {m = m} t x (lift i) = middle , cast′ t i+k≡n (join′ t high low) , _
+  where
+  reasoning = slicedSize _ m i
+  k = proj₁ reasoning
+  i+k≡n = proj₂ (proj₂ reasoning)
+  eq = proj₁ (proj₂ reasoning)
+  low = take′ t (Fin.toℕ i) (cast′ t eq x)
+  middle = take′ t m (drop′ t (Fin.toℕ i) (cast′ t eq x))
+  high = drop′ t m (drop′ t (Fin.toℕ i) (cast′ t eq x))
+
+cut : ∀ t → Term Σ Γ Δ (asType t (n ℕ.+ m)) → Term Σ Γ Δ (fin (suc n)) → Term Σ Γ Δ (tuple _ (asType t m ∷ asType t n ∷ []))
+cut τ t t′ = func₂ (cut′ τ) t t′
+
+flatten : ∀ {ms : Vec ℕ n} → ⟦ Vec.map fin ms ⟧ₜ′ → All Fin ms
+flatten {ms = []}     _             = []
+flatten {ms = _ ∷ ms} (lift x , xs) = x ∷ flatten xs
+
+𝒦 : Literal t → Term Σ Γ Δ t
+𝒦 (x ′b) = func₀ (lift x)
+𝒦 (x ′i) = func₀ (lift (x ℤ′.×′ 1ℤ))
+𝒦 (x ′f) = func₀ (lift x)
+𝒦 (x ′r) = func₀ (lift (x ℝ′.×′ 1ℝ))
+𝒦 (x ′x) = func₀ (lift (Bool.if x then 1𝔹 else 0𝔹))
+𝒦 ([] ′xs) = func₀ []
+𝒦 ((x ∷ xs) ′xs) = func₂ (flip Vec._∷ʳ_) (𝒦 (x ′x)) (𝒦 (xs ′xs))
+𝒦 (x ′a) = func₁ Vec.replicate (𝒦 x)
+
+module _ (2≉0 : 2≉0) where
+  ℰ : Code.Expression Σ Γ t → Term Σ Γ Δ t
   ℰ e = (uncurry helper) (M.elimFunctions e)
     where
     1+m⊔n≡1+k : ∀ m n → ∃ λ k → suc m ℕ.⊔ n ≡ suc k
@@ -181,142 +309,49 @@ module _ {Σ : Vec Type o} (2≉0 : ¬ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ) where
     pull-last {0}     {0} refl = refl
     pull-last {suc x} {0} ()
 
-    equal : HasEquality t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ → ⟦ bool ⟧ₜ
-    equal bool (lift x) (lift y) = lift (does (x Bool.≟ y))
-    equal int (lift x) (lift y) = lift (does (x ≟ᶻ y))
-    equal fin (lift x) (lift y) = lift (does (x Fin.≟ y))
-    equal real (lift x) (lift y) = lift (does (x ≟ʳ y))
-    equal bit (lift x) (lift y) = lift (does (x ≟ᵇ₁ y))
-    equal bits []       []       = lift (Bool.true)
-    equal bits (x ∷ xs) (y ∷ ys) = lift (lower (equal bit x y) Bool.∧ lower (equal bits xs ys))
-
-    less : IsNumeric t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ → ⟦ bool ⟧ₜ
-    less int (lift x) (lift y) = lift (does (x <ᶻ? y))
-    less real (lift x) (lift y) = lift (does (x <ʳ? y))
-
-    box : ∀ t → ⟦ elemType t ⟧ₜ → ⟦ asType t 1 ⟧ₜ
-    box bits x = x ∷ []
-    box (array t) x = x ∷ []
-
-    unboxed : ∀ t → ⟦ asType t 1 ⟧ₜ → ⟦ elemType t ⟧ₜ
-    unboxed bits (x ∷ []) = x
-    unboxed (array t) (x ∷ []) = x
-
-    casted : ∀ t {i j} → .(eq : i ≡ j) → ⟦ asType t i ⟧ₜ → ⟦ asType t j ⟧ₜ
-    casted bits      {j = 0}     eq []       = []
-    casted bits      {j = suc j} eq (x ∷ xs) = x ∷ casted bits (ℕₚ.suc-injective eq) xs
-    casted (array t) {j = 0}     eq []       = []
-    casted (array t) {j = suc j} eq (x ∷ xs) = x ∷ casted (array t) (ℕₚ.suc-injective eq) xs
-
-    neg : IsNumeric t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ
-    neg int (lift x) = lift (ℤ.- x)
-    neg real (lift x) = lift (ℝ.- x)
-
-    add : (isNum₁ : True (isNumeric? t₁)) → (isNum₂ : True (isNumeric? t₂)) → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ combineNumeric t₁ t₂ {isNum₁} {isNum₂} ⟧ₜ
-    add {int} {int} _ _ (lift x) (lift y) = lift (x ℤ.+ y)
-    add {int} {real} _ _ (lift x) (lift y) = lift (x /1 ℝ.+ y)
-    add {real} {int} _ _ (lift x) (lift y) = lift (x ℝ.+ y /1)
-    add {real} {real} _ _ (lift x) (lift y) = lift (x ℝ.+ y)
-
-    mul : (isNum₁ : True (isNumeric? t₁)) → (isNum₂ : True (isNumeric? t₂)) → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ combineNumeric t₁ t₂ {isNum₁} {isNum₂} ⟧ₜ
-    mul {int} {int} _ _ (lift x) (lift y) = lift (x ℤ.* y)
-    mul {int} {real} _ _ (lift x) (lift y) = lift (x /1 ℝ.* y)
-    mul {real} {int} _ _ (lift x) (lift y) = lift (x ℝ.* y /1)
-    mul {real} {real} _ _ (lift x) (lift y) = lift (x ℝ.* y)
-
-    pow : IsNumeric t → ⟦ t ⟧ₜ → ℕ → ⟦ t ⟧ₜ
-    pow int (lift x) y = lift (x ℤ′.^′ y)
-    pow real (lift x) y = lift (x ℝ′.^′ y)
-
-    shift : ⟦ int ⟧ₜ → ℕ → ⟦ int ⟧ₜ
-    shift (lift x) n = lift (⌊ x /1 ℝ.* 2≉0 ℝ.⁻¹ ℝ′.^′ n ⌋)
-
-    flatten : ∀ {ms : Vec ℕ n} → ⟦ Vec.map fin ms ⟧ₜ′ → All Fin ms
-    flatten {ms = []}     _             = []
-    flatten {ms = _ ∷ ms} (lift x , xs) = x ∷ flatten xs
-
-    private
-      m≤n⇒m+k≡n : ∀ {m n} → m ℕ.≤ n → ∃ λ k → m ℕ.+ k ≡ n
-      m≤n⇒m+k≡n ℕ.z≤n       = _ , refl
-      m≤n⇒m+k≡n (ℕ.s≤s m≤n) = dmap id (cong suc) (m≤n⇒m+k≡n m≤n)
-
-      slicedSize : ∀ n m (i : Fin (suc n)) → ∃ λ k → n ℕ.+ m ≡ Fin.toℕ i ℕ.+ (m ℕ.+ k) × Fin.toℕ i ℕ.+ k ≡ n
-      slicedSize n m i = k , (begin
-        n ℕ.+ m                 ≡˘⟨ cong (ℕ._+ m) (proj₂ i+k≡n) ⟩
-        (Fin.toℕ i ℕ.+ k) ℕ.+ m ≡⟨  ℕₚ.+-assoc (Fin.toℕ i) k m ⟩
-        Fin.toℕ i ℕ.+ (k ℕ.+ m) ≡⟨  cong (Fin.toℕ i ℕ.+_) (ℕₚ.+-comm k m) ⟩
-        Fin.toℕ i ℕ.+ (m ℕ.+ k) ∎) ,
-        proj₂ i+k≡n
-        where
-        open ≡-Reasoning
-        i+k≡n = m≤n⇒m+k≡n (ℕₚ.≤-pred (Finₚ.toℕ<n i))
-        k = proj₁ i+k≡n
-
-    -- 0 of y is 0 of result
-    join : ∀ t → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ → ⟦ asType t (n ℕ.+ m) ⟧ₜ
-    join bits      xs ys = ys ++ xs
-    join (array t) xs ys = ys ++ xs
-
-    take : ∀ t i {j} → ⟦ asType t (i ℕ.+ j) ⟧ₜ → ⟦ asType t i ⟧ₜ
-    take bits      i xs = Vec.take i xs
-    take (array t) i xs = Vec.take i xs
-
-    drop : ∀ t i {j} → ⟦ asType t (i ℕ.+ j) ⟧ₜ → ⟦ asType t j ⟧ₜ
-    drop bits      i xs = Vec.drop i xs
-    drop (array t) i xs = Vec.drop i xs
-
-    -- 0 of x is i of result
-    spliced : ∀ t {m n} → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ → ⟦ fin (suc n) ⟧ₜ → ⟦ asType t (n ℕ.+ m) ⟧ₜ
-    spliced t {m} x y (lift i) = casted t eq (join t (join t high x) low)
-      where
-      reasoning = slicedSize _ m i
-      k = proj₁ reasoning
-      n≡i+k = sym (proj₂ (proj₂ reasoning))
-      low = take t (Fin.toℕ i) (casted t n≡i+k y)
-      high = drop t (Fin.toℕ i) (casted t n≡i+k y)
-      eq = sym (proj₁ (proj₂ reasoning))
-
-    -- i of x is 0 of first
-    sliced : ∀ t {m n} → ⟦ asType t (n ℕ.+ m) ⟧ₜ → ⟦ fin (suc n) ⟧ₜ → ⟦ asType t m ∷ asType t n ∷ [] ⟧ₜ′
-    sliced t {m} x (lift i) = middle , casted t i+k≡n (join t high low) , _
-      where
-      reasoning = slicedSize _ m i
-      k = proj₁ reasoning
-      i+k≡n = proj₂ (proj₂ reasoning)
-      eq = proj₁ (proj₂ reasoning)
-      low = take t (Fin.toℕ i) (casted t eq x)
-      middle = take t m (drop t (Fin.toℕ i) (casted t eq x))
-      high = drop t m (drop t (Fin.toℕ i) (casted t eq x))
-
-    helper : ∀ (e : Expression Γ t) → M.callDepth e ≡ 0 → Term Σ Γ Δ t
+    helper : ∀ (e : Code.Expression Σ Γ t) → M.callDepth e ≡ 0 → Term Σ Γ Δ t
     helper (Code.lit x) eq = 𝒦 x
     helper (Code.state i) eq = state i
     helper (Code.var i) eq = var i
-    helper (Code.abort e) eq = func (λ ()) (helper e eq ∷ [])
-    helper (_≟_ {hasEquality = hasEq} e e₁) eq = func (λ (x , y , _) → equal (toWitness hasEq) x y) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ [])
-    helper (_<?_ {isNumeric = isNum} e e₁) eq = func (λ (x , y , _) → less (toWitness isNum) x y) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ [])
-    helper (Code.inv e) eq = func (λ (lift b , _) → lift (Bool.not b)) (helper e eq ∷ [])
-    helper (e Code.&& e₁) eq = func (λ (lift b , lift b₁ , _) → lift (b Bool.∧ b₁)) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ [])
-    helper (e Code.|| e₁) eq = func (λ (lift b , lift b₁ , _) → lift (b Bool.∨ b₁)) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ [])
-    helper (Code.not e) eq = func (λ (xs , _) → Vec.map (lift ∘ 𝔹.¬_ ∘ lower) xs) (helper e eq ∷ [])
-    helper (e Code.and e₁) eq = func (λ (xs , ys , _) → Vec.zipWith (lift ∘₂ 𝔹._∧_ ) (Vec.map lower xs) (Vec.map lower ys)) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ [])
-    helper (e Code.or e₁) eq = func (λ (xs , ys , _) → Vec.zipWith (lift ∘₂ 𝔹._∨_ ) (Vec.map lower xs) (Vec.map lower ys)) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ [])
-    helper ([_] {t = t} e) eq = func (λ (x , _) → box t x) (helper e eq ∷ [])
-    helper (Code.unbox {t = t} e) eq = func (λ (x , _) → unboxed t x) (helper e eq ∷ [])
-    helper (Code.splice {t = t} e e₁ e₂) eq = func (λ (x , y , i , _) → spliced t x y i) (helper e (pull-0₃ eq) ∷ helper e₁ (pull-1₃ (M.callDepth e) eq) ∷ helper e₂ (pull-last eq) ∷ [])
-    helper (Code.cut {t = t} e e₁) eq = func (λ (x , i , _) → sliced t x i) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ [])
-    helper (Code.cast {t = t} i≡j e) eq = func (λ (x , _) → casted t i≡j x) (helper e eq ∷ [])
-    helper (-_ {isNumeric = isNum} e) eq = func (λ (x , _) → neg (toWitness isNum) x) (helper e eq ∷ [])
-    helper (_+_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁) eq = func (λ (x , y , _) → add isNum₁ isNum₂ x y) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ [])
-    helper (_*_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁) eq = func (λ (x , y , _) → mul isNum₁ isNum₂ x y) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ [])
-    helper (_^_ {isNumeric = isNum} e y) eq = func (λ (x , _) → pow (toWitness isNum) x y) (helper e eq ∷ [])
-    helper (e >> n) eq = func (λ (x , _) → shift x n) (helper e eq ∷ [])
-    helper (Code.rnd e) eq = func (λ (lift x , _) → lift ⌊ x ⌋) (helper e eq ∷ [])
-    helper (Code.fin f e) eq = func (λ (xs , _) → lift (f (flatten xs))) (helper e eq ∷ [])
-    helper (Code.asInt e) eq = func (λ (lift x , _) → lift (Fin.toℕ x ℤ′.×′ 1ℤ)) (helper e eq ∷ [])
-    helper Code.nil eq = func (λ args → _) []
-    helper (Code.cons e e₁) eq = func (λ (x , xs , _) → x , xs) (helper e (pull-0₂ eq) ∷ helper e₁ (pull-last eq) ∷ [])
-    helper (Code.head e) eq = func (λ ((x , _) , _) → x) (helper e eq ∷ [])
-    helper (Code.tail e) eq = func (λ ((_ , xs) , _) → xs) (helper e eq ∷ [])
+    helper (Code.abort e) eq = func₁ (λ ()) (helper e eq)
+    helper (Code._≟_ {hasEquality = hasEq} e e₁) eq = [ toWitness hasEq ][ helper e (pull-0₂ eq) ≟ helper e₁ (pull-last eq) ]
+    helper (Code._<?_ {isNumeric = isNum} e e₁) eq = [ toWitness isNum ][ helper e (pull-0₂ eq) <? helper e₁ (pull-last eq) ]
+    helper (Code.inv e) eq = func₁ (lift ∘ Bool.not ∘ lower) (helper e eq)
+    helper (e Code.&& e₁) eq = func₂ (λ (lift x) (lift y) → lift (x Bool.∧ y)) (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
+    helper (e Code.|| e₁) eq = func₂ (λ (lift x) (lift y) → lift (x Bool.∨ y)) (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
+    helper (Code.not e) eq = func₁ (Vec.map (lift ∘ 𝔹.¬_ ∘ lower)) (helper e eq)
+    helper (e Code.and e₁) eq = func₂ (λ xs ys → Vec.zipWith (λ (lift x) (lift y) → lift (x 𝔹.∧ y)) xs ys) (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
+    helper (e Code.or e₁) eq = func₂ (λ xs ys → Vec.zipWith (λ (lift x) (lift y) → lift (x 𝔹.∨ y)) xs ys) (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
+    helper (Code.[_] {t = t} e) eq = [ t ][ helper e eq ]
+    helper (Code.unbox {t = t} e) eq = unbox t (helper e eq)
+    helper (Code.splice {t = t} e e₁ e₂) eq = splice t (helper e (pull-0₃ eq)) (helper e₁ (pull-1₃ (M.callDepth e) eq)) (helper e₂ (pull-last eq))
+    helper (Code.cut {t = t} e e₁) eq = cut t (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
+    helper (Code.cast {t = t} i≡j e) eq = cast t i≡j (helper e eq)
+    helper (Code.-_ {isNumeric = isNum} e) eq = [ toWitness isNum ][- helper e eq ]
+    helper (Code._+_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁) eq = [ _ , _ , isNum₁ , isNum₂ ][ helper e (pull-0₂ eq) + helper e₁ (pull-last eq) ]
+    helper (Code._*_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁) eq = [ _ , _ , isNum₁ , isNum₂ ][ helper e (pull-0₂ eq) * helper e₁ (pull-last eq) ]
+    helper (Code._^_ {isNumeric = isNum} e y) eq = [ toWitness isNum ][ helper e eq ^ y ]
+    helper (e Code.>> n) eq = [ 2≉0 ][ helper e eq >> n ]
+    helper (Code.rnd e) eq = func₁ (lift ∘ ⌊_⌋ ∘ lower) (helper e eq)
+    helper (Code.fin f e) eq = func₁ (lift ∘ f ∘ flatten) (helper e eq)
+    helper (Code.asInt e) eq = func₁ (lift ∘ (ℤ′._×′ 1ℤ) ∘ Fin.toℕ ∘ lower) (helper e eq)
+    helper Code.nil eq = func₀ _
+    helper (Code.cons e e₁) eq = func₂ _,_ (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
+    helper (Code.head e) eq = func₁ proj₁ (helper e eq)
+    helper (Code.tail e) eq = func₁ proj₂ (helper e eq)
     helper (Code.call f es) eq = contradiction (trans (sym eq) (proj₂ (1+m⊔n≡1+k (M.funCallDepth f) (M.callDepth′ es)))) ℕₚ.0≢1+n
     helper (Code.if e then e₁ else e₂) eq = func (λ (lift b , x , x₁ , _) → Bool.if b then x else x₁) (helper e (pull-0₃ eq) ∷ helper e₁ (pull-1₃ (M.callDepth e) eq) ∷ helper e₂ (pull-last eq) ∷ [])
+
+  subst : Term Σ Γ Δ t → {e : Code.Expression Σ Γ t′} → Code.CanAssign Σ e → Term Σ Γ Δ t′ → Term Σ Γ Δ t
+  subst t (Code.state i) t′ = substState t i t′
+  subst t (Code.var i) t′ = substVar t i t′
+  subst t (Code.abort e) t′ = func₁ (λ ()) (ℰ e)
+  subst t (Code.[_] {t = τ} ref) t′ = subst t ref (unbox τ t′)
+  subst t (Code.unbox {t = τ} ref) t′ = subst t ref [ τ ][ t′ ]
+  subst t (Code.splice {t = τ} ref ref₁ e₃) t′ = subst (subst t ref (func₁ proj₁ (cut τ t′ (ℰ e₃)))) ref₁ (func₁ (proj₁ ∘ proj₂) (cut τ t′ (ℰ e₃)))
+  subst t (Code.cut {t = τ} ref e₂) t′ = subst t ref (splice τ (func₁ proj₁ t′) (func₁ (proj₁ ∘ proj₂) t′) (ℰ e₂))
+  subst t (Code.cast {t = τ} eq ref) t′ = subst t ref (cast τ (sym eq) t′)
+  subst t Code.nil t′ = t
+  subst t (Code.cons ref ref₁) t′ = subst (subst t ref (func₁ proj₁ t′)) ref₁ (func₁ proj₂ t′)
+  subst t (Code.head {e = e} ref) t′ = subst t ref (func₂ _,_ t′ (func₁ proj₂ (ℰ e)))
+  subst t (Code.tail {t = τ} {e = e} ref) t′ = subst t ref (func₂ {t₁ = τ} _,_ (func₁ proj₁ (ℰ e)) t′)
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
index e605439..ec2a374 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -98,12 +98,12 @@ 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 bit  x y = does (x ≟ᵇ₁ y)
-equal bits x y = does (x ≟ᵇ y)
+equal bool     x y = does (x Bool.≟ y)
+equal int      x y = does (x ≟ᶻ y)
+equal fin      x y = does (x Fin.≟ y)
+equal real     x y = does (x ≟ʳ y)
+equal bit      x y = does (x ≟ᵇ₁ y)
+equal (bits _) x y = does (x ≟ᵇ y)
 
 comp : ∀ {t} → IsNumeric t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ → Bool
 comp int  x y = does (x <ᶻ? y)
@@ -180,13 +180,13 @@ neg : ∀ {t} → IsNumeric t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ
 neg int  x = ℤ.- x
 neg real x = ℝ.- x
 
-add : ∀ {t₁ t₂} (isNum₁ : True (isNumeric? t₁)) (isNum₂ : True (isNumeric? t₂)) → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ combineNumeric t₁ t₂ {isNum₁} {isNum₂} ⟧ₜ
+add : ∀ {t₁ t₂} (isNum₁ : True (isNumeric? t₁)) (isNum₂ : True (isNumeric? t₂)) → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ combineNumeric t₁ t₂ isNum₁ isNum₂ ⟧ₜ
 add {t₁ = int}  {t₂ = int}  _ _ x y = x ℤ.+ y
 add {t₁ = int}  {t₂ = real} _ _ x y = x /1 ℝ.+ y
 add {t₁ = real} {t₂ = int}  _ _ x y = x ℝ.+ y /1
 add {t₁ = real} {t₂ = real} _ _ x y = x ℝ.+ y
 
-mul : ∀ {t₁ t₂} (isNum₁ : True (isNumeric? t₁)) (isNum₂ : True (isNumeric? t₂)) → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ combineNumeric t₁ t₂ {isNum₁} {isNum₂} ⟧ₜ
+mul : ∀ {t₁ t₂} (isNum₁ : True (isNumeric? t₁)) (isNum₂ : True (isNumeric? t₂)) → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ combineNumeric t₁ t₂ isNum₁ isNum₂ ⟧ₜ
 mul {t₁ = int}  {t₂ = int}  _ _ x y = x ℤ.* y
 mul {t₁ = int}  {t₂ = real} _ _ x y = x /1 ℝ.* y
 mul {t₁ = real} {t₂ = int}  _ _ x y = x ℝ.* y /1
-- 
cgit v1.2.3