Separate out Hoare logic terms.

2 files changed, 348 insertions, 68 deletions

diff --git a/src/Helium/Semantics/Axiomatic/Core.agda b/src/Helium/Semantics/Axiomatic/Core.agda
index 176dbdd..de4f411 100644
--- a/src/Helium/Semantics/Axiomatic/Core.agda
+++ b/src/Helium/Semantics/Axiomatic/Core.agda
@@ -22,7 +22,7 @@ open import Data.Fin.Patterns
 open import Data.Nat as ℕ using (ℕ; suc)
 import Data.Nat.Induction as Natᵢ
 import Data.Nat.Properties as ℕₚ
-open import Data.Product as × using (_,_; uncurry)
+open import Data.Product as × using (_×_; _,_; uncurry)
 open import Data.Sum using (_⊎_)
 open import Data.Unit using (⊤)
 open import Data.Vec as Vec using (Vec; []; _∷_; _++_; lookup)
@@ -45,79 +45,37 @@ private
     m n      : ℕ
     Γ Δ Σ ts : Vec Type m
 
-sizeOf : Type → Sliced → ℕ
-sizeOf bool s = 0
-sizeOf int s = 0
-sizeOf (fin n) s = 0
-sizeOf real s = 0
-sizeOf bit s = 0
-sizeOf (bits n) s = Bool.if does (s ≟ˢ bits) then n else 0
-sizeOf (tuple _ []) s = 0
-sizeOf (tuple _ (t ∷ ts)) s = sizeOf t s ℕ.+ sizeOf (tuple _ ts) s
-sizeOf (array t n) s = Bool.if does (s ≟ˢ array t) then n else sizeOf t s
+⟦_⟧ₜ  : Type → Set (b₁ ⊔ i₁ ⊔ r₁)
+⟦_⟧ₜ′ : Vec Type n → Set (b₁ ⊔ i₁ ⊔ r₁)
 
-allocateSpace : Vec Type n → Sliced → ℕ
-allocateSpace []       s = 0
-allocateSpace (t ∷ ts) s = sizeOf t s ℕ.+ allocateSpace ts s
+⟦ bool ⟧ₜ       = Lift (b₁ ⊔ i₁ ⊔ r₁) Bool
+⟦ int ⟧ₜ        = Lift (b₁ ⊔ r₁) ℤ
+⟦ fin n ⟧ₜ      = Lift (b₁ ⊔ i₁ ⊔ r₁) (Fin n)
+⟦ real ⟧ₜ       = Lift (b₁ ⊔ i₁) ℝ
+⟦ bit ⟧ₜ        = Lift (i₁ ⊔ r₁) Bit
+⟦ bits n ⟧ₜ     = Vec ⟦ bit ⟧ₜ n
+⟦ tuple n ts ⟧ₜ = ⟦ ts ⟧ₜ′ 
+⟦ array t n ⟧ₜ  = Vec ⟦ t ⟧ₜ n
 
-private
-  getSliced : ∀ {t} → True (sliced? t) → Sliced
-  getSliced t = ×.proj₁ (toWitness t)
-
-  getCount : ∀ {t} → True (sliced? t) → ℕ
-  getCount t = ×.proj₁ (×.proj₂ (toWitness t))
-
-data ⟦_；_⟧ₜ (counts : Sliced → ℕ) : (τ : Type) → Set (b₁ ⊔ i₁ ⊔ r₁) where
-  bool   : Bool → ⟦ counts ； bool ⟧ₜ
-  int    : ℤ → ⟦ counts ； int ⟧ₜ
-  fin    : ∀ {n} → Fin n → ⟦ counts ； fin n ⟧ₜ
-  real   : ℝ → ⟦ counts ； real ⟧ₜ
-  bit    : Bit → ⟦ counts ； bit ⟧ₜ
-  bits   : ∀ {n} → Vec (⟦ counts ； bit ⟧ₜ ⊎ Fin (counts bits)) n → ⟦ counts ； bits n ⟧ₜ
-  array  : ∀ {t n} → Vec (⟦ counts ； t ⟧ₜ ⊎ Fin (counts (array t))) n → ⟦ counts ； array t n ⟧ₜ
-  tuple  : ∀ {n ts} → All ⟦ counts ；_⟧ₜ  ts → ⟦ counts ； tuple n ts ⟧ₜ
-
-Stack : (counts : Sliced → ℕ) → Vec Type n → Set (b₁ ⊔ i₁ ⊔ r₁)
-Stack counts Γ = ⟦ counts ； tuple _ Γ ⟧ₜ
-
-Heap : (counts : Sliced → ℕ) → Set (b₁ ⊔ i₁ ⊔ r₁)
-Heap counts = ∀ t → Vec ⟦ counts ； elemType t ⟧ₜ (counts t)
-
-record State (Γ : Vec Type n) : Set (b₁ ⊔ i₁ ⊔ r₁) where
-  private
-    counts = allocateSpace Γ
-  field
-    stack   : Stack counts Γ
-    heap    : Heap counts
+⟦ [] ⟧ₜ′     = Lift (b₁ ⊔ i₁ ⊔ r₁) ⊤
+⟦ t ∷ ts ⟧ₜ′ = ⟦ t ⟧ₜ × ⟦ ts ⟧ₜ′
 
 Transform : Vec Type m → Type → Set (b₁ ⊔ i₁ ⊔ r₁)
-Transform ts t = ∀ counts → Heap counts → ⟦ counts ； tuple _ ts ⟧ₜ → ⟦ counts ； t ⟧ₜ
+Transform ts t = ⟦ ts ⟧ₜ′ → ⟦ t ⟧ₜ
 
 Predicate : Vec Type m → Set (b₁ ⊔ i₁ ⊔ r₁)
-Predicate ts = ∀ counts → ⟦ counts ； tuple _ ts ⟧ₜ → Bool
-
--- --   ⟦_⟧ₐ : ∀ {m Δ} → Assertion Σ Γ {m} Δ → State (Σ ++ Γ ++ Δ) → Set (b₁ ⊔ i₁ ⊔ r₁)
--- --   ⟦_⟧ₐ = {!!}
-
--- -- module _ {o} {Σ : Vec Type o} where
--- --   open Code Σ
-
--- --   𝒦 : ∀ {n Γ m Δ t} → Literal t → Term Σ {n} Γ {m} Δ t
--- --   𝒦 = {!!}
-
--- --   ℰ : ∀ {n Γ m Δ t} → Expression {n} Γ t → Term Σ Γ {m} Δ t
--- --   ℰ = {!!}
+Predicate ts =  ⟦ ts ⟧ₜ′ → Bool
 
--- --   data HoareTriple {n Γ m Δ} : Assertion Σ {n} Γ {m} Δ → Statement Γ → Assertion Σ Γ Δ → Set (b₁ ⊔ i₁ ⊔ r₁) where
--- --     _∙_ : ∀ {P Q R s₁ s₂} → HoareTriple P s₁ Q → HoareTriple Q s₂ R → HoareTriple P (s₁ ∙ s₂) R
--- --     skip : ∀ {P} → HoareTriple P skip P
+--   data HoareTriple {n Γ m Δ} : Assertion Σ {n} Γ {m} Δ → Statement Γ → Assertion Σ Γ Δ → Set (b₁ ⊔ i₁ ⊔ r₁) where
+--     _∙_ : ∀ {P Q R s₁ s₂} → HoareTriple P s₁ Q → HoareTriple Q s₂ R → HoareTriple P (s₁ ∙ s₂) R
+--     skip : ∀ {P} → HoareTriple P skip P
 
--- --     assign : ∀ {P t ref canAssign e} → HoareTriple (asrtSubst P (toWitness canAssign) (ℰ e)) (_≔_ {t = t} ref {canAssign} e) P
--- --     declare : ∀ {t P Q e s} → HoareTriple (P ∧ equal (var 0F) (termWknVar (ℰ e))) s (asrtWknVar Q) → HoareTriple (asrtElimVar P (ℰ e)) (declare {t = t} e s) Q
--- --     invoke : ∀ {m ts P Q s e} → HoareTriple (assignMetas Δ ts (All.tabulate var) (asrtAddVars P)) s (asrtAddVars Q) → HoareTriple (assignMetas Δ ts (All.tabulate (λ i → ℰ (All.lookup i e))) (asrtAddVars P)) (invoke {m = m} {ts} (s ∙end) e) (asrtAddVars Q)
--- --     if : ∀ {P Q e s₁ s₂} → HoareTriple (P ∧ equal (ℰ e) (𝒦 (Bool.true ′b))) s₁ Q → HoareTriple (P ∧ equal (ℰ e) (𝒦 (Bool.false ′b))) s₂ Q → HoareTriple P (if e then s₁ else s₂) Q
--- --     for : ∀ {m} {I : Assertion Σ Γ (fin (suc m) ∷ Δ)} {s} → HoareTriple (some (asrtWknVar (asrtWknMetaAt 1F I) ∧ equal (meta 1F) (var 0F) ∧ equal (meta 0F) (func (λ { _ (lift x ∷ []) → lift (Fin.inject₁ x) }) (meta 1F ∷ [])))) s (some (asrtWknVar (asrtWknMetaAt 1F I) ∧ equal (meta 0F) (func (λ { _ (lift x ∷ []) → lift (Fin.suc x) }) (meta 1F ∷ [])))) → HoareTriple (some (I ∧ equal (meta 0F) (func (λ _ _ → lift 0F) []))) (for m s) (some (I ∧ equal (meta 0F) (func (λ _ _ → lift (Fin.fromℕ m)) [])))
+--     assign : ∀ {P t ref canAssign e} → HoareTriple (asrtSubst P (toWitness canAssign) (ℰ e)) (_≔_ {t = t} ref {canAssign} e) P
+--     declare : ∀ {t P Q e s} → HoareTriple (P ∧ equal (var 0F) (termWknVar (ℰ e))) s (asrtWknVar Q) → HoareTriple (asrtElimVar P (ℰ e)) (declare {t = t} e s) Q
+--     invoke : ∀ {m ts P Q s e} → HoareTriple (assignMetas Δ ts (All.tabulate var) (asrtAddVars P)) s (asrtAddVars Q) → HoareTriple (assignMetas Δ ts (All.tabulate (λ i → ℰ (All.lookup i e))) (asrtAddVars P)) (invoke {m = m} {ts} (s ∙end) e) (asrtAddVars Q)
+--     if : ∀ {P Q e s₁ s₂} → HoareTriple (P ∧ equal (ℰ e) (𝒦 (Bool.true ′b))) s₁ Q → HoareTriple (P ∧ equal (ℰ e) (𝒦 (Bool.false ′b))) s₂ Q → HoareTriple P (if e then s₁ else s₂) Q
+--     for : ∀ {m} {I : Assertion Σ Γ (fin (suc m) ∷ Δ)} {s} → HoareTriple (some (asrtWknVar (asrtWknMetaAt 1F I) ∧ equal (meta 1F) (var 0F) ∧ equal (meta 0F) (func (λ { _ (lift x ∷ []) → lift (Fin.inject₁ x) }) (meta 1F ∷ [])))) s (some (asrtWknVar (asrtWknMetaAt 1F I) ∧ equal (meta 0F) (func (λ { _ (lift x ∷ []) → lift (Fin.suc x) }) (meta 1F ∷ [])))) → HoareTriple (some (I ∧ equal (meta 0F) (func (λ _ _ → lift 0F) []))) (for m s) (some (I ∧ equal (meta 0F) (func (λ _ _ → lift (Fin.fromℕ m)) [])))
 
--- --     consequence : ∀ {P₁ P₂ Q₁ Q₂ s} → ⟦ P₁ ⟧ₐ ⊆ ⟦ P₂ ⟧ₐ → HoareTriple P₂ s Q₂ → ⟦ Q₂ ⟧ₐ ⊆ ⟦ Q₁ ⟧ₐ → HoareTriple P₁ s Q₁
--- --     some : ∀ {t P Q s} → HoareTriple P s Q → HoareTriple (some {t = t} P) s (some Q)
--- --     frame : ∀ {P Q R s} → HoareTriple P s Q → HoareTriple (P * R) s (Q * R)
+--     consequence : ∀ {P₁ P₂ Q₁ Q₂ s} → ⟦ P₁ ⟧ₐ ⊆ ⟦ P₂ ⟧ₐ → HoareTriple P₂ s Q₂ → ⟦ Q₂ ⟧ₐ ⊆ ⟦ Q₁ ⟧ₐ → HoareTriple P₁ s Q₁
+--     some : ∀ {t P Q s} → HoareTriple P s Q → HoareTriple (some {t = t} P) s (some Q)
+--     frame : ∀ {P Q R s} → HoareTriple P s Q → HoareTriple (P * R) s (Q * R)
diff --git a/src/Helium/Semantics/Axiomatic/Term.agda b/src/Helium/Semantics/Axiomatic/Term.agda
new file mode 100644
index 0000000..980b85a
--- /dev/null
+++ b/src/Helium/Semantics/Axiomatic/Term.agda
@@ -0,0 +1,322 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Definition of terms for use in assertions
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Data.Pseudocode.Types using (RawPseudocode)
+
+module Helium.Semantics.Axiomatic.Term
+  {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
+  (rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃)
+  where
+
+open RawPseudocode rawPseudocode
+
+import Data.Bool as Bool
+open import Data.Fin as Fin using (Fin; suc)
+import Data.Fin.Properties as Finₚ
+open import Data.Fin.Patterns
+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.Properties as Vecₚ
+open import Data.Vec.Relation.Unary.All using (All; []; _∷_)
+open import Function using (_∘_; _∘₂_; id)
+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.Nullary using (does; yes; no; ¬_)
+open import Relation.Nullary.Decidable.Core using (True; toWitness)
+open import Relation.Nullary.Negation using (contradiction)
+
+private
+  variable
+    t t′ t₁ t₂ : Type
+    m n o      : ℕ
+    Γ Δ Σ ts   : Vec Type m
+
+data Term (Σ : Vec Type o) (Γ : Vec Type n) (Δ : Vec Type m) : Type → Set (b₁ ⊔ i₁ ⊔ r₁) where
+  state : ∀ i → Term Σ Γ Δ (lookup Σ i)
+  var   : ∀ i → Term Σ Γ Δ (lookup Γ i)
+  meta  : ∀ i → Term Σ Γ Δ (lookup Δ i)
+  func  : Transform ts t → All (Term Σ Γ Δ) ts → Term Σ Γ Δ t
+
+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
+
+substState : Term Σ Γ Δ t → ∀ i → Term Σ Γ Δ (lookup Σ i) → Term Σ Γ Δ t
+substState (state i) j t′ with i Fin.≟ j
+... | yes refl = t′
+... | no _     = state i
+substState (var i) j t′ = var i
+substState (meta i) j t′ = meta i
+substState (func f ts) j t′ = func f (helper ts j t′)
+  where
+  helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → ∀ i → Term Σ Γ Δ (lookup Σ i) → All (Term Σ Γ Δ) ts
+  helper []       i t′ = []
+  helper (t ∷ ts) i t′ = substState t i t′ ∷ helper ts i t′
+
+substVar : Term Σ Γ Δ t → ∀ i → Term Σ Γ Δ (lookup Γ i) → Term Σ Γ Δ t
+substVar (state i) j t′ = state i
+substVar (var i) j t′ with i Fin.≟ j
+... | yes refl = t′
+... | no _     = var i
+substVar (meta i) j t′ = meta i
+substVar (func f ts) j t′ = func f (helper ts j t′)
+  where
+  helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → ∀ i → Term Σ Γ Δ (lookup Γ i) → All (Term Σ Γ Δ) ts
+  helper []       i t′ = []
+  helper (t ∷ ts) i t′ = substVar t i t′ ∷ helper ts i t′
+
+
+elimVar : Term Σ (t′ ∷ Γ) Δ t → Term Σ Γ Δ t′ → Term Σ Γ Δ t
+elimVar (state i)     t′ = state i
+elimVar (var 0F)      t′ = t′
+elimVar (var (suc i)) t′ = var i
+elimVar (meta i)      t′ = meta i
+elimVar (func f ts)   t′ = func f (helper ts t′)
+  where
+  helper : ∀ {n ts} → All (Term Σ (_ ∷ Γ) Δ) {n} ts → Term Σ Γ Δ _ → All (Term Σ Γ Δ) ts
+  helper []       t′ = []
+  helper (t ∷ ts) t′ = elimVar t t′ ∷ helper ts t′
+
+wknVar : Term Σ Γ Δ t → Term Σ (t′ ∷ Γ) Δ t
+wknVar (state i)   = state i
+wknVar (var i)     = var (suc i)
+wknVar (meta i)    = meta i
+wknVar (func f ts) = func f (helper ts)
+  where
+  helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ (_ ∷ Γ) Δ) ts
+  helper []       = []
+  helper (t ∷ ts) = wknVar t ∷ helper ts
+
+wknVars : (ts : Vec Type n) → Term Σ Γ Δ t → Term Σ (ts ++ Γ) Δ t
+wknVars τs (state i)   = state i
+wknVars τs (var i)     = castType (var (Fin.raise (Vec.length τs) i)) (Vecₚ.lookup-++ʳ τs _ i)
+wknVars τs (meta i)    = meta i
+wknVars τs (func f ts) = func f (helper ts)
+  where
+  helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ (τs ++ Γ) Δ) ts
+  helper []       = []
+  helper (t ∷ ts) = wknVars τs t ∷ helper ts
+
+addVars : Term Σ [] Δ t → Term Σ Γ Δ t
+addVars (state i)   = state i
+addVars (meta i)    = meta i
+addVars (func f ts) = func f (helper ts)
+  where
+  helper : ∀ {n ts} → All (Term Σ [] Δ) {n} ts → All (Term Σ Γ Δ) ts
+  helper []       = []
+  helper (t ∷ ts) = addVars t ∷ helper ts
+
+wknMetaAt : ∀ i → Term Σ Γ Δ t → Term Σ Γ (Vec.insert Δ i t′) t
+wknMetaAt i (state j)   = state j
+wknMetaAt i (var j)     = var j
+wknMetaAt i (meta j)    = castType (meta (Fin.punchIn i j)) (Vecₚ.insert-punchIn _ i _ j)
+wknMetaAt i (func f ts) = func f (helper ts)
+  where
+  helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ Γ (Vec.insert Δ i _)) ts
+  helper []       = []
+  helper (t ∷ ts) = wknMetaAt i t ∷ helper ts
+
+wknMeta : Term Σ Γ Δ t → Term Σ Γ (t′ ∷ Δ) t
+wknMeta = wknMetaAt 0F
+
+wknMetas : (ts : Vec Type n) → Term Σ Γ Δ t → Term Σ Γ (ts ++ Δ) t
+wknMetas τs (state i)   = state i
+wknMetas τs (var i)     = var i
+wknMetas τs (meta i)    = castType (meta (Fin.raise (Vec.length τs) i)) (Vecₚ.lookup-++ʳ τs _ i)
+wknMetas τs (func f ts) = func f (helper ts)
+  where
+  helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ Γ (τs ++ Δ)) ts
+  helper []       = []
+  helper (t ∷ ts) = wknMetas τs t ∷ helper ts
+
+module _ {Σ : Vec Type o} (2≉0 : ¬ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ) where
+  open Code Σ
+
+  𝒦 : 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 ∷ [])
+
+  ℰ : Expression Γ t → Term Σ Γ Δ t
+  ℰ e = (uncurry helper) (M.elimFunctions e)
+    where
+    1+m⊔n≡1+k : ∀ m n → ∃ λ k → suc m ℕ.⊔ n ≡ suc k
+    1+m⊔n≡1+k m 0       = m , refl
+    1+m⊔n≡1+k m (suc n) = m ℕ.⊔ n , refl
+
+    pull-0₂ : ∀ {x y} → x ℕ.⊔ y ≡ 0 → x ≡ 0
+    pull-0₂ {0} {0}     refl = refl
+    pull-0₂ {0} {suc y} ()
+
+    pull-0₃ : ∀ {x y z} → x ℕ.⊔ y ℕ.⊔ z ≡ 0 → x ≡ 0
+    pull-0₃ {0}     {0}     {0} refl = refl
+    pull-0₃ {0}     {suc y} {0}     ()
+    pull-0₃ {suc x} {0}     {0}     ()
+    pull-0₃ {suc x} {0}     {suc z} ()
+
+    pull-1₃ : ∀ x {y z} → x ℕ.⊔ y ℕ.⊔ z ≡ 0 → y ≡ 0
+    pull-1₃ 0       {0}     {0}     refl = refl
+    pull-1₃ 0       {suc y} {0}     ()
+    pull-1₃ (suc x) {0}     {0}     ()
+    pull-1₃ (suc x) {0}     {suc z} ()
+
+    pull-last : ∀ {x y} → x ℕ.⊔ y ≡ 0 → y ≡ 0
+    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 (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.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) ∷ [])