Generalise slice and join into cut and splice.

2 files changed, 148 insertions, 176 deletions

diff --git a/src/Helium/Semantics/Axiomatic/Core.agda b/src/Helium/Semantics/Axiomatic/Core.agda
index 92c67bb..176dbdd 100644
--- a/src/Helium/Semantics/Axiomatic/Core.agda
+++ b/src/Helium/Semantics/Axiomatic/Core.agda
@@ -16,153 +16,108 @@ module Helium.Semantics.Axiomatic.Core
 private
   open module C = RawPseudocode rawPseudocode
 
-open import Data.Bool using (Bool; T)
-open import Data.Fin as Fin using (zero; suc)
-import Data.Fin.Properties as Finₚ
--- open import Data.Nat as ℕ using (zero; suc)
-import Data.Nat as ℕ
+open import Data.Bool as Bool using (Bool)
+open import Data.Fin as Fin using (Fin; zero; suc)
+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 using (∃; _×_; _,_; <_,_>)
+open import Data.Product as × using (_,_; uncurry)
 open import Data.Sum using (_⊎_)
 open import Data.Unit using (⊤)
-open import Data.Vec using (Vec; _∷_; lookup)
+open import Data.Vec as Vec using (Vec; []; _∷_; _++_; lookup)
 open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
-open import Function using (_$_)
+open import Function using (_on_)
 open import Helium.Data.Pseudocode.Core
-open import Helium.Semantics.Core rawPseudocode
-open import Level using (_⊔_; Lift)
-open import Relation.Binary.PropositionalEquality using (refl)
-open import Relation.Nullary using (yes; no)
-open import Relation.Unary using (Decidable; _⊆_)
-
-module _ {o} (Σ : Vec Type o) {n} (Γ : Vec Type n) where
-  data Term {m} (Δ : Vec Type m) : Type → Set (b₁ ⊔ i₁ ⊔ r₁) where
-    state : ∀ i → Term Δ (lookup Σ i)
-    var   : ∀ i → Term Δ (lookup Γ i)
-    meta  : ∀ i → Term Δ (lookup Δ i)
-    funct : ∀ {m ts t} → (⟦ tuple m ts ⟧ₜˡ → ⟦ t ⟧ₜˡ) → All (Term Δ) ts → Term Δ t
-
-  infixl 7 _⇒_
-  infixl 6 _∧_
-  infixl 5 _∨_
-
-  data Assertion {m} (Δ : Vec Type m) : Set (b₁ ⊔ i₁ ⊔ r₁) where
-    _∧_  : Assertion Δ → Assertion Δ → Assertion Δ
-    _∨_  : Assertion Δ → Assertion Δ → Assertion Δ
-    _⇒_  : Assertion Δ → Assertion Δ → Assertion Δ
-    all  : ∀ {t} → Assertion (t ∷ Δ) → Assertion Δ
-    some : ∀ {t} → Assertion (t ∷ Δ) → Assertion Δ
-    pred : ∀ {m ts} → (⟦ tuple m ts ⟧ₜˡ → Bool) → All (Term Δ) ts → Assertion Δ
-
-module _ {o} {Σ : Vec Type o} {n} {Γ : Vec Type n} {m} {Δ : Vec Type m} where
-  ⟦_⟧ : ∀ {t} → Term Σ Γ Δ t → ⟦ Σ ⟧ₜˡ′ → ⟦ Γ ⟧ₜˡ′ → ⟦ Δ ⟧ₜˡ′ → ⟦ t ⟧ₜˡ
-  ⟦_⟧′ : ∀ {n ts} → All (Term Σ Γ Δ) ts → ⟦ Σ ⟧ₜˡ′ → ⟦ Γ ⟧ₜˡ′ → ⟦ Δ ⟧ₜˡ′ → ⟦ tuple n ts ⟧ₜˡ
-  ⟦ state i ⟧    σ γ δ = fetchˡ Σ σ i
-  ⟦ var i ⟧      σ γ δ = fetchˡ Γ γ i
-  ⟦ meta i ⟧     σ γ δ = fetchˡ Δ δ i
-  ⟦ funct f ts ⟧ σ γ δ = f (⟦ ts ⟧′ σ γ δ)
-
-  ⟦ [] ⟧′            σ γ δ = _
-  ⟦ (t ∷ []) ⟧′      σ γ δ = ⟦ t ⟧ σ γ δ
-  ⟦ (t ∷ t′ ∷ ts) ⟧′ σ γ δ = ⟦ t ⟧ σ γ δ , ⟦ t′ ∷ ts ⟧′ σ γ δ
-
-  termSubstState : ∀ {t} → Term Σ Γ Δ t → ∀ j → Term Σ Γ Δ (lookup Σ j) → Term Σ Γ Δ t
-  termSubstState (state i)    j t′ with j Fin.≟ i
-  ...                                 | yes refl = t′
-  ...                                 | no _     = state i
-  termSubstState (var i)      j t′ = var i
-  termSubstState (meta i)     j t′ = meta i
-  termSubstState (funct f ts) j t′ = funct f (helper ts)
-    where
-    helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ Γ Δ) ts
-    helper []       = []
-    helper (t ∷ ts) = termSubstState t j t′ ∷ helper ts
-
-  termSubstVar : ∀ {t} → Term Σ Γ Δ t → ∀ j → Term Σ Γ Δ (lookup Γ j) → Term Σ Γ Δ t
-  termSubstVar (state i)     j t′ = state i
-  termSubstVar (var i)       j t′ with j Fin.≟ i
-  ...                                | yes refl = t′
-  ...                                | no _     = var i
-  termSubstVar (meta i)      j t′ = meta i
-  termSubstVar (funct f ts)  j t′ = funct f (helper ts)
-    where
-    helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ Γ Δ) ts
-    helper []       = []
-    helper (t ∷ ts) = termSubstVar t j t′ ∷ helper ts
-
-  termElimVar : ∀ {t t′} → Term Σ (t′ ∷ Γ) Δ t → Term Σ Γ Δ t′ → Term Σ Γ Δ t
-  termElimVar (state i)     t′ = state i
-  termElimVar (var zero)    t′ = t′
-  termElimVar (var (suc i)) t′ = var i
-  termElimVar (meta i)      t′ = meta i
-  termElimVar (funct f ts)  t′ = funct f (helper ts)
-    where
-    helper : ∀ {n ts} → All (Term _ _ _) {n} ts → All (Term _ _ _) ts
-    helper []       = []
-    helper (t ∷ ts) = termElimVar t t′ ∷ helper ts
-
-  termWknVar : ∀ {t t′} → Term Σ Γ Δ t → Term Σ (t′ ∷ Γ) Δ t
-  termWknVar (state i)    = state i
-  termWknVar (var i)      = var (suc i)
-  termWknVar (meta i)     = meta i
-  termWknVar (funct f ts) = funct f (helper ts)
-    where
-    helper : ∀ {n ts} → All (Term _ _ _) {n} ts → All (Term _ _ _) ts
-    helper []       = []
-    helper (t ∷ ts) = termWknVar t ∷ helper ts
-
-  termWknMeta : ∀ {t t′} → Term Σ Γ Δ t → Term Σ Γ (t′ ∷ Δ) t
-  termWknMeta (state i)    = state i
-  termWknMeta (var i)      = var i
-  termWknMeta (meta i)     = meta (suc i)
-  termWknMeta (funct f ts) = funct f (helper ts)
-    where
-    helper : ∀ {n ts} → All (Term _ _ _) {n} ts → All (Term _ _ _) ts
-    helper []       = []
-    helper (t ∷ ts) = termWknMeta t ∷ helper ts
-
-module _ {o} {Σ : Vec Type o} {n} {Γ : Vec Type n} where
-  infix 4 _∋[_] _⊨_
-
-  _∋[_] : ∀ {m Δ} → Assertion Σ Γ {m} Δ → ⟦ Σ ⟧ₜˡ′ × ⟦ Γ ⟧ₜˡ′ × ⟦ Δ ⟧ₜˡ′ → Set (b₁ ⊔ i₁ ⊔ r₁)
-  P ∧ Q ∋[ s ] = P ∋[ s ] × Q ∋[ s ]
-  P ∨ Q ∋[ s ] = P ∋[ s ] ⊎ Q ∋[ s ]
-  P ⇒ Q ∋[ s ] = P ∋[ s ] → Q ∋[ s ]
-  pred P ts ∋[ σ , γ , δ ] = Lift (b₁ ⊔ i₁ ⊔ r₁) $ T $ P (⟦ ts ⟧′ σ γ δ)
-  _∋[_] {Δ = Δ} (all P)  (σ , γ , δ) = ∀ v → P ∋[ σ , γ , consˡ Δ v δ ]
-  _∋[_] {Δ = Δ} (some P) (σ , γ , δ) = ∃ λ v → P ∋[ σ , γ , consˡ Δ v δ ]
-
-  _⊨_ : ∀ {m Δ} → ⟦ Σ ⟧ₜˡ′ × ⟦ Γ ⟧ₜˡ′ × ⟦ Δ ⟧ₜˡ′ → Assertion Σ Γ {m} Δ → Set (b₁ ⊔ i₁ ⊔ r₁)
-  s ⊨ P = P ∋[ s ]
-
-  asstSubstState : ∀ {m Δ} → Assertion Σ Γ {m} Δ → ∀ j → Term Σ Γ Δ (lookup Σ j) → Assertion Σ Γ Δ
-  asstSubstState (P ∧ Q)     j t = asstSubstState P j t ∧ asstSubstState Q j t
-  asstSubstState (P ∨ Q)     j t = asstSubstState P j t ∨ asstSubstState Q j t
-  asstSubstState (P ⇒ Q)     j t = asstSubstState P j t ⇒ asstSubstState Q j t
-  asstSubstState (all P)     j t = all (asstSubstState P j (termWknMeta t))
-  asstSubstState (some P)    j t = some (asstSubstState P j (termWknMeta t))
-  asstSubstState (pred p ts) j t = pred p (All.map (λ t′ → termSubstState t′ j t) ts)
-
-  asstSubstVar : ∀ {m Δ} → Assertion Σ Γ {m} Δ → ∀ j → Term Σ Γ Δ (lookup Γ j) → Assertion Σ Γ Δ
-  asstSubstVar (P ∧ Q)     j t = asstSubstVar P j t ∧ asstSubstVar Q j t
-  asstSubstVar (P ∨ Q)     j t = asstSubstVar P j t ∨ asstSubstVar Q j t
-  asstSubstVar (P ⇒ Q)     j t = asstSubstVar P j t ⇒ asstSubstVar Q j t
-  asstSubstVar (all P)     j t = all (asstSubstVar P j (termWknMeta t))
-  asstSubstVar (some P)    j t = some (asstSubstVar P j (termWknMeta t))
-  asstSubstVar (pred p ts) j t = pred p (All.map (λ t′ → termSubstVar t′ j t) ts)
-
-  asstElimVar : ∀ {m Δ t′} → Assertion Σ (t′ ∷ Γ) {m} Δ → Term Σ Γ Δ t′ → Assertion Σ Γ Δ
-  asstElimVar (P ∧ Q)     t = asstElimVar P t ∧ asstElimVar Q t
-  asstElimVar (P ∨ Q)     t = asstElimVar P t ∨ asstElimVar Q t
-  asstElimVar (P ⇒ Q)     t = asstElimVar P t ⇒ asstElimVar Q t
-  asstElimVar (all P)     t = all (asstElimVar P (termWknMeta t))
-  asstElimVar (some P)    t = some (asstElimVar P (termWknMeta t))
-  asstElimVar (pred p ts) t = pred p (All.map (λ t′ → termElimVar t′ t) ts)
-
-module _ {o} {Σ : Vec Type o} where
-  open Code Σ
-
-  data HoareTriple {n Γ m Δ} : Assertion Σ {n} Γ {m} Δ → Statement Γ → Assertion Σ Γ Δ → Set (b₁ ⊔ i₁ ⊔ r₁) where
-    csqs : ∀ {P₁ P₂ Q₁ Q₂ : Assertion Σ Γ Δ} {s} → (_⊨ P₁) ⊆ (_⊨ P₂) → HoareTriple P₂ s Q₂ → (_⊨ Q₂) ⊆ (_⊨ Q₁) → HoareTriple P₁ s Q₁
-    _∙_  : ∀ {P Q R s₁ s₂} → HoareTriple P s₁ Q → HoareTriple Q s₂ R → HoareTriple P (s₁ ∙ s₂) R
-    skip : ∀ {P} → HoareTriple P skip P
+open import Helium.Data.Pseudocode.Properties
+import Induction.WellFounded as Wf
+open import Level using (_⊔_; Lift; lift)
+import Relation.Binary.Construct.On as On
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂)
+open import Relation.Nullary using (Dec; does; yes; no)
+open import Relation.Nullary.Decidable.Core using (True; toWitness; map′)
+open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Unary using (_⊆_)
+
+private
+  variable
+    t t′     : Type
+    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
+
+allocateSpace : Vec Type n → Sliced → ℕ
+allocateSpace []       s = 0
+allocateSpace (t ∷ ts) s = sizeOf t s ℕ.+ allocateSpace ts s
+
+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
+
+Transform : Vec Type m → Type → Set (b₁ ⊔ i₁ ⊔ r₁)
+Transform ts t = ∀ counts → Heap counts → ⟦ counts ； tuple _ ts ⟧ₜ → ⟦ counts ； 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
+-- --   ℰ = {!!}
+
+-- --   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)) [])))
+
+-- --     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/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
index 474a60f..ff5a56d 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -111,8 +111,8 @@ 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
+join bits      x y = y VecF.++ x
+join (array _) x y = y Vec.++ x
 
 -- take from 0
 take : ∀ t i {j} → ⟦ asType t (i ℕ.+ j) ⟧ₜ → ⟦ asType t i ⟧ₜ
@@ -134,26 +134,39 @@ module _ where
   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) ∎)
+  slicedSize : ∀ n m (i : Fin (suc n)) → P.∃ λ k → n ℕ.+ m ≡ Fin.toℕ i ℕ.+ (m ℕ.+ k) × Fin.toℕ i ℕ.+ k ≡ n
+  slicedSize n m i = k , (begin
+    n ℕ.+ m                   ≡˘⟨ ≡.cong (ℕ._+ m) (P.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) ∎) ,
+    P.proj₂ i+k≡n
     where
     open ≡-Reasoning
-    off+k≤i = m≤n⇒m+k≡n (ℕₚ.≤-pred (Finₚ.toℕ<n off))
-    k = P.proj₁ off+k≤i
+    i+k≡n = m≤n⇒m+k≡n (ℕₚ.≤-pred (Finₚ.toℕ<n i))
+    k = P.proj₁ i+k≡n
 
-  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))
+  -- 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 i = casted t eq (join t (join t high x) low)
+    where
+    reasoning = slicedSize _ m i
+    k = P.proj₁ reasoning
+    n≡i+k = ≡.sym (P.proj₂ (P.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 (P.proj₁ (P.proj₂ reasoning))
+
+  sliced : ∀ t {m n} → ⟦ asType t (n ℕ.+ m) ⟧ₜ → ⟦ fin (suc n) ⟧ₜ → ⟦ asType t m ∷ asType t n ∷ [] ⟧ₜ′
+  sliced t {m} x i = middle , casted t i+k≡n (join t high low)
+    where
+    reasoning = slicedSize _ m i
+    k = P.proj₁ reasoning
+    i+k≡n = P.proj₂ (P.proj₂ reasoning)
+    eq = P.proj₁ (P.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))
 
 box : ∀ t → ⟦ elemType t ⟧ₜ → ⟦ asType t 1 ⟧ₜ
 box bits      v = v VecF.∷ VecF.[]
@@ -214,8 +227,8 @@ module Expression
   ⟦ e or e₁ ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ Bits.∨ ⟦ e₁ ⟧ᵉ σ γ
   ⟦ [_] {t = t} e ⟧ᵉ σ γ = box t (⟦ e ⟧ᵉ σ γ)
   ⟦ unbox {t = t} e ⟧ᵉ σ γ = unboxed t (⟦ e ⟧ᵉ σ γ)
-  ⟦ _∶_ {t = t} e e₁ ⟧ᵉ σ γ = join t (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ)
-  ⟦ slice {t = t} e e₁ ⟧ᵉ σ γ = sliced t (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ)
+  ⟦ splice {t = t} e e₁ e₂ ⟧ᵉ σ γ = spliced t (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ) (⟦ e₂ ⟧ᵉ σ γ)
+  ⟦ cut {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₁ ⟧ᵉ σ γ)
@@ -267,16 +280,20 @@ module Expression
 
   update (state i) v σ γ = updateAt Σ i v σ , γ
   update {Γ = Γ} (var i) v σ γ = σ , updateAt Γ i 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 (abort _) v σ γ = σ , γ
   update ([_] {t = t} e) v σ γ = update e (unboxed t v) σ γ
   update (unbox {t = t} e) v σ γ = update e (box t v) σ γ
-  update (slice {t = t} {e₁ = e₁} a e₂) v σ γ = updateSliced t (⟦ e₁ ⟧ᵉ σ γ) (⟦ e₂ ⟧ᵉ σ γ) v (λ v → update a v σ γ)
+  update (splice {m = m} {t = t} e e₁ e₂) v σ γ = do
+    let i = ⟦ e₂ ⟧ᵉ σ γ
+    let σ′ , γ′ = update e (P.proj₁ (sliced t v i)) σ γ
+    update e₁ (P.proj₂ (sliced t v i)) σ′ γ′
+  update (cut {t = t} a e₂) v σ γ = do
+    let i = ⟦ e₂ ⟧ᵉ σ γ
+    update a (spliced t (P.proj₁ v) (P.proj₂ v) i) σ γ
   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 σ′ γ′
+  update (tup {es = []} x) vs σ γ = σ , γ
+  update (tup {ts = _ ∷ ts} {es = _ ∷ _} (x ∷ xs)) vs σ γ = do
+    let σ′ , γ′ = update x (tupHead ts vs) σ γ
+    update (tup xs) (tupTail ts vs) σ′ γ′
+  update (head {ts = ts} {e = e} a) v σ γ = update a (tupCons ts v (tupTail ts (⟦ e ⟧ᵉ σ γ))) σ γ
+  update (tail {ts = ts} {e = e} a) v σ γ = update a (tupCons ts (tupHead ts (⟦ e ⟧ᵉ σ γ)) v) σ γ