From 5250643e58e3eb4d277178f06c8984027ca3e01a Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Sat, 19 Feb 2022 16:06:57 +0000
Subject: Unalias bit type.

---
 src/Helium/Data/Pseudocode/Core.agda        | 38 ++++++-------
 src/Helium/Instructions/Base.agda           | 35 ++++++------
 src/Helium/Semantics/Core.agda              | 82 -----------------------------
 src/Helium/Semantics/Denotational/Core.agda | 67 +++++++++++++++++++----
 4 files changed, 93 insertions(+), 129 deletions(-)
 delete mode 100644 src/Helium/Semantics/Core.agda

(limited to 'src')

diff --git a/src/Helium/Data/Pseudocode/Core.agda b/src/Helium/Data/Pseudocode/Core.agda
index 4dbf552..6ae1d34 100644
--- a/src/Helium/Data/Pseudocode/Core.agda
+++ b/src/Helium/Data/Pseudocode/Core.agda
@@ -31,18 +31,17 @@ data Type : Set where
   int   : Type
   fin   : (n : ℕ) → Type
   real  : Type
+  bit   : Type
   bits  : (n : ℕ) → Type
   tuple : ∀ n → Vec Type n → Type
   array : Type → (n : ℕ) → Type
 
-bit : Type
-bit = bits 1
-
 data HasEquality : Type → Set where
   bool : HasEquality bool
   int  : HasEquality int
   fin  : ∀ {n} → HasEquality (fin n)
   real : HasEquality real
+  bit  : HasEquality bit
   bits : ∀ {n} → HasEquality (bits n)
 
 hasEquality? : Decidable HasEquality
@@ -50,6 +49,7 @@ hasEquality? bool        = yes bool
 hasEquality? int         = yes int
 hasEquality? (fin n)     = yes fin
 hasEquality? real        = yes real
+hasEquality? bit         = yes bit
 hasEquality? (bits n)    = yes bits
 hasEquality? (tuple n x) = no (λ ())
 hasEquality? (array t n) = no (λ ())
@@ -61,8 +61,9 @@ data IsNumeric : Type → Set where
 isNumeric? : Decidable IsNumeric
 isNumeric? bool        = no (λ ())
 isNumeric? int         = yes int
-isNumeric? real        = yes real
 isNumeric? (fin n)     = no (λ ())
+isNumeric? real        = yes real
+isNumeric? bit         = no (λ ())
 isNumeric? (bits n)    = no (λ ())
 isNumeric? (tuple n x) = no (λ ())
 isNumeric? (array t n) = no (λ ())
@@ -87,12 +88,13 @@ elemType (array t) = t
 --- Literals
 
 data Literal : Type → Set where
-  _′b : Bool → Literal bool
-  _′i : ℕ → Literal int
-  _′f : ∀ {n} → Fin n → Literal (fin n)
-  _′r : ℕ → Literal real
-  _′x : ∀ {n} → Vec Bool n → Literal (bits n)
-  _′a : ∀ {n t} → Literal t → Literal (array t n)
+  _′b  : Bool → Literal bool
+  _′i  : ℕ → Literal int
+  _′f  : ∀ {n} → Fin n → Literal (fin n)
+  _′r  : ℕ → Literal real
+  _′x  : Bool → Literal bit
+  _′xs : ∀ {n} → Vec Bool n → Literal (bits n)
+  _′a  : ∀ {n t} → Literal t → Literal (array t n)
 
 --- Expressions, references, statements, functions and procedures
 
@@ -130,8 +132,8 @@ module Code {o} (Σ : Vec Type o) where
     not   : ∀ {m} → Expression Γ (bits m) → Expression Γ (bits m)
     _and_ : ∀ {m} → Expression Γ (bits m) → Expression Γ (bits m) → Expression Γ (bits m)
     _or_  : ∀ {m} → Expression Γ (bits m) → Expression Γ (bits m) → Expression Γ (bits m)
-    [_]   : ∀ {t} → Expression Γ t → Expression Γ (array t 1)
-    unbox : ∀ {t} → Expression Γ (array t 1) → Expression Γ t
+    [_]   : ∀ {t} → Expression Γ (elemType t) → Expression Γ (asType t 1)
+    unbox : ∀ {t} → Expression Γ (asType t 1) → Expression Γ (elemType t)
     _∶_   : ∀ {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)
@@ -153,8 +155,8 @@ module Code {o} (Σ : Vec Type o) where
     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)
+    [_]   : ∀ {t} {e : Expression Γ (elemType t)} → CanAssign e → CanAssign ([_] {t = t} e)
+    unbox : ∀ {t} {e : Expression Γ (asType t 1)} → CanAssign e → CanAssign (unbox 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)
@@ -267,21 +269,21 @@ module Code {o} (Σ : Vec Type o) where
   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)
+  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)
+    ( if slice′ x (lit ((# 0) ′f)) ≟ lit ((true ∷ []) ′xs)
       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 zero}    x = if x ≟ lit ((true ∷ []) ′xs) 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)
+    ( if slice′ x (lit ((# 0) ′f)) ≟ lit ((true ∷ []) ′xs)
       then lit (1 ′i)
       else lit (0 ′i))
diff --git a/src/Helium/Instructions/Base.agda b/src/Helium/Instructions/Base.agda
index a76b2b1..3261107 100644
--- a/src/Helium/Instructions/Base.agda
+++ b/src/Helium/Instructions/Base.agda
@@ -84,8 +84,7 @@ join {k = k} {suc m} x = cast eq (join (slice x (lit (Fin.fromℕ 1 ′f))) ∶
   eq = P.trans (P.cong (k ℕ.+_) (ℕₚ.*-comm k (suc m))) (ℕₚ.*-comm (suc (suc m)) k)
 
 index : ∀ {n Γ t m} → Expression {n} Γ (asType t (suc m)) → Expression Γ (fin (suc m)) → Expression Γ (elemType t)
-index {t = bits}    {m} x i = slice (cast (ℕₚ.+-comm 1 m) x) i
-index {t = array _} {m} x i = unbox (slice (cast (ℕₚ.+-comm 1 m) x) i)
+index {m = m} x i = unbox (slice (cast (ℕₚ.+-comm 1 m) x) i)
 
 Q : ∀ {n Γ} → Expression {n} Γ (array (array (bits 32) 4) 8)
 Q = group 7 S
@@ -98,11 +97,11 @@ elem {k = suc k} (suc m) x i = index (group k (cast (ℕₚ.*-comm (suc k) (suc
 --- Other utiliies
 
 hasBit : ∀ {n Γ m} → Expression {n} Γ (bits (suc m)) → Expression Γ (fin (suc m)) → Expression Γ bool
-hasBit {n} x i = index x i ≟ lit ((true ∷ []) ′x)
+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 = sliceⁱ (suc n) i ∶ get n i
+sliceⁱ {m = zero}  n i = lit ([] ′xs)
+sliceⁱ {m = suc m} n i = sliceⁱ (suc n) i ∶ [ get n i ]
 
 --- Functions
 
@@ -127,10 +126,10 @@ SignedSatQ n = declare (lit (true ′b)) (
 
 -- 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))
+LSL-C {n} shift = declare (var 0 ∶ lit ((Vec.replicate {n = (suc shift)} false) ′xs))
   (skip ∙return tup
     ( slice (var 0) (lit (zero ′f))
-    ∷ slice (cast eq (var 0)) (lit (Fin.inject+ shift (Fin.fromℕ n) ′f))
+    ∷ unbox (slice (cast eq (var 0)) (lit (Fin.inject+ shift (Fin.fromℕ n) ′f)))
     ∷ []))
   where
   eq = P.trans (ℕₚ.+-comm 1 (shift ℕ.+ n)) (P.cong (ℕ._+ 1) (ℕₚ.+-comm shift n))
@@ -156,30 +155,30 @@ VPTAdvance : Procedure (beat ∷ [])
 VPTAdvance = declare (fin div2 (tup (var 0 ∷ []))) (
   declare (elem 4 VPR-mask (var 0)) (
     -- 0:vptState 1:maskId 2:beat
-    if var 0 ≟ lit ((true ∷ false ∷ false ∷ false ∷ []) ′x)
+    if var 0 ≟ lit ((true ∷ false ∷ false ∷ false ∷ []) ′xs)
     then
-      var 0 ≔ lit (Vec.replicate false ′x)
-    else if inv (var 0 ≟ lit (Vec.replicate false ′x))
+      var 0 ≔ lit (Vec.replicate false ′xs)
+    else if inv (var 0 ≟ lit (Vec.replicate false ′xs))
     then (
-      declare (lit ((false ∷ []) ′x)) (
+      declare (lit (false ′x)) (
         -- 0:inv 1:vptState 2:maskId 3:beat
         tup (var 1 ∷ var 0 ∷ []) ≔ call (LSL-C 0) (var 1 ∷ []) ∙
-        if var 0 ≟ lit ((true ∷ []) ′x)
+        if var 0 ≟ lit (true ′x)
         then
           elem 4 VPR-P0 (var 3) ≔ not (elem 4 VPR-P0 (var 3))
         else skip))
     else skip ∙
-    if get 0 (asInt (var 2)) ≟ lit ((true ∷ []) ′x)
+    if get 0 (asInt (var 2)) ≟ lit (true ′x)
     then
       elem 4 VPR-mask (var 1) ≔ var 0
     else skip))
     ∙end
 
 VPTActive : Function (beat ∷ []) bool
-VPTActive = skip ∙return inv (elem 4 VPR-mask (fin div2 (tup (var 0 ∷ []))) ≟ lit (Vec.replicate false ′x))
+VPTActive = skip ∙return inv (elem 4 VPR-mask (fin div2 (tup (var 0 ∷ []))) ≟ lit (Vec.replicate false ′xs))
 
 GetCurInstrBeat : Function [] (tuple 2 (beat ∷ elmtMask ∷ []))
-GetCurInstrBeat = declare (lit (Vec.replicate true ′x)) (
+GetCurInstrBeat = declare (lit (Vec.replicate true ′xs)) (
   -- 0:elmtMask 1:beat
   if call VPTActive (BeatId ∷ [])
   then
@@ -222,10 +221,10 @@ module _ (d : Instr.VecOp₂) where
  -- 0:op₂ 1:e 2:op₁ 3:result 4:elmtMask 5:curBeat
   vec-op₂′ : Statement (bits (toℕ esize) ∷ fin (toℕ elements) ∷ array (bits (toℕ esize)) (toℕ elements) ∷ array (bits (toℕ esize)) (toℕ elements) ∷ elmtMask ∷ beat ∷ []) → Procedure []
   vec-op₂′ op = declare (lit (zero ′f)) (
-    declare (lit (Vec.replicate false ′x)) (
+    declare (lit (Vec.replicate false ′xs)) (
     -- 0:elmtMask 1:curBeat
     tup (var 1 ∷ var 0 ∷ []) ≔ call GetCurInstrBeat [] ∙
-    declare (lit ((Vec.replicate false ′x) ′a)) (
+    declare (lit ((Vec.replicate false ′xs) ′a)) (
     declare (from32 size (index (index Q (lit (src₁ ′f))) (var 2))) (
     -- 0:op₁ 1:result 2:elmtMask 3:curBeat
     for (toℕ elements) (
@@ -285,7 +284,7 @@ private
       tup (index (var 5) (var 3) ∷ var 0 ∷ []) ≔ call (SignedSatQ (toℕ esize-1)) (var 1 ∷ []) ∙
       if var 0 && hasBit (var 6) (fin e*esize>>3 (tup ((var 3) ∷ [])))
       then
-        FPSCR-QC ≔ lit ((true ∷ []) ′x)
+        FPSCR-QC ≔ lit (true ′x)
       else skip)))
     where
     open Instr.VecOp₂ d
diff --git a/src/Helium/Semantics/Core.agda b/src/Helium/Semantics/Core.agda
deleted file mode 100644
index 749e1ca..0000000
--- a/src/Helium/Semantics/Core.agda
+++ /dev/null
@@ -1,82 +0,0 @@
-------------------------------------------------------------------------
--- Agda Helium
---
--- Shared definitions between semantic systems
-------------------------------------------------------------------------
-
-{-# OPTIONS --safe --without-K #-}
-
-open import Helium.Data.Pseudocode.Types using (RawPseudocode)
-
-module Helium.Semantics.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 using (Bool)
-open import Data.Fin using (Fin; zero; suc)
-open import Data.Product using (_×_; _,_)
-open import Data.Unit using (⊤)
-open import Data.Vec using (Vec; []; _∷_; lookup)
-open import Helium.Data.Pseudocode.Core
-open import Level hiding (zero; suc)
-
-⟦_⟧ₗ : Type → Level
-⟦ 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 ⟧ₗ
-
-⟦ bool ⟧ₜ       = Bool
-⟦ int ⟧ₜ        = ℤ
-⟦ fin n ⟧ₜ      = Fin n
-⟦ real ⟧ₜ       = ℝ
-⟦ bits n ⟧ₜ     = Bits n
-⟦ tuple n ts ⟧ₜ = ⟦ ts ⟧ₜ′
-⟦ array t n ⟧ₜ  = Vec ⟦ t ⟧ₜ n
-
-⟦ [] ⟧ₜ′          = ⊤
-⟦ t ∷ [] ⟧ₜ′      = ⟦ t ⟧ₜ
-⟦ t ∷ t′ ∷ ts ⟧ₜ′ = ⟦ t ⟧ₜ × ⟦ t′ ∷ ts ⟧ₜ′
-
-⟦_⟧ₜˡ : Type → Set (b₁ ⊔ i₁ ⊔ r₁)
-⟦_⟧ₜˡ′ : ∀ {n} → Vec Type n → Set (b₁ ⊔ i₁ ⊔ r₁)
-
-⟦ bool ⟧ₜˡ       = Lift (b₁ ⊔ i₁ ⊔ r₁) Bool
-⟦ int ⟧ₜˡ        = Lift (b₁ ⊔ r₁) ℤ
-⟦ fin n ⟧ₜˡ      = Lift (b₁ ⊔ i₁ ⊔ r₁) (Fin n)
-⟦ real ⟧ₜˡ       = Lift (b₁ ⊔ i₁) ℝ
-⟦ bits n ⟧ₜˡ     = Lift (i₁ ⊔ r₁) (Bits n)
-⟦ tuple n ts ⟧ₜˡ = ⟦ ts ⟧ₜˡ′ 
-⟦ array t n ⟧ₜˡ  = Vec ⟦ t ⟧ₜˡ n
-
-⟦ [] ⟧ₜˡ′          = Lift (b₁ ⊔ i₁ ⊔ r₁) ⊤
-⟦ t ∷ [] ⟧ₜˡ′      = ⟦ t ⟧ₜˡ
-⟦ t ∷ t′ ∷ ts ⟧ₜˡ′ = ⟦ t ⟧ₜˡ × ⟦ t′ ∷ ts ⟧ₜˡ′
-
-fetch : ∀ {n} ts → ⟦ tuple n ts ⟧ₜ → ∀ i → ⟦ lookup ts i ⟧ₜ
-fetch (_ ∷ [])     x        zero    = x
-fetch (_ ∷ _ ∷ _)  (x , xs) zero    = x
-fetch (_ ∷ t ∷ ts) (x , xs) (suc i) = fetch (t ∷ ts) xs i
-
-fetchˡ : ∀ {n} ts → ⟦ tuple n ts ⟧ₜˡ → ∀ i → ⟦ lookup ts i ⟧ₜˡ
-fetchˡ (_ ∷ [])     x        zero    = x
-fetchˡ (_ ∷ _ ∷ _)  (x , xs) zero    = x
-fetchˡ (_ ∷ t ∷ ts) (x , xs) (suc i) = fetchˡ (t ∷ ts) xs i
-
-consˡ : ∀ {n t} ts → ⟦ t ⟧ₜˡ → ⟦ tuple n ts ⟧ₜˡ → ⟦ t ∷ ts ⟧ₜˡ′
-consˡ []      x xs = x
-consˡ (_ ∷ _) x xs = x , xs
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
index 6ec0b24..46d68bc 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -29,21 +29,57 @@ 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
-open import Helium.Semantics.Core rawPseudocode
 import Induction as I
 import Induction.WellFounded as Wf
+open import Level using (Level; _⊔_; 0ℓ)
 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
+⟦ bool ⟧ₗ       = 0ℓ
+⟦ int ⟧ₗ        = i₁
+⟦ fin n ⟧ₗ      = 0ℓ
+⟦ real ⟧ₗ       = r₁
+⟦ bit ⟧ₗ        = b₁
+⟦ 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 ⟧ₗ
+
+⟦ bool ⟧ₜ       = Bool
+⟦ int ⟧ₜ        = ℤ
+⟦ fin n ⟧ₜ      = Fin n
+⟦ real ⟧ₜ       = ℝ
+⟦ bit ⟧ₜ        = Bit
+⟦ bits n ⟧ₜ     = Bits n
+⟦ tuple n ts ⟧ₜ = ⟦ ts ⟧ₜ′
+⟦ array t n ⟧ₜ  = Vec ⟦ t ⟧ₜ n
+
+⟦ [] ⟧ₜ′          = ⊤
+⟦ 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)
+𝒦 (x ′b)   = x
+𝒦 (x ′i)   = x ℤ′.×′ 1ℤ
+𝒦 (x ′f)   = x
+𝒦 (x ′r)   = x ℝ′.×′ 1ℝ
+𝒦 (x ′x)   = Bool.if x then 1𝔹 else 0𝔹
+𝒦 (xs ′xs) = 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
@@ -66,6 +102,7 @@ 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
@@ -118,6 +155,14 @@ updateSliced t {i} {j} orig off v f = f (casted t (≡.sym eq) (join t (join t u
   dropped = take t (Fin.toℕ off) (casted t eq orig)
   untaken = drop t j (drop t (Fin.toℕ off) (casted t eq orig))
 
+box : ∀ t → ⟦ elemType t ⟧ₜ → ⟦ asType t 1 ⟧ₜ
+box bits      v = v VecF.∷ VecF.[]
+box (array t) v = v ∷ []
+
+unboxed : ∀ t → ⟦ asType t 1 ⟧ₜ → ⟦ elemType t ⟧ₜ
+unboxed bits      v        = v (Fin.zero)
+unboxed (array t) (v ∷ []) = v
+
 neg : ∀ {t} → IsNumeric t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ
 neg int  x = ℤ.- x
 neg real x = ℝ.- x
@@ -167,8 +212,8 @@ module Expression
   ⟦ not e ⟧ᵉ σ γ = Bits.¬_ (⟦ e ⟧ᵉ σ γ)
   ⟦ e and e₁ ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ Bits.∧ ⟦ e₁ ⟧ᵉ σ γ
   ⟦ e or e₁ ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ Bits.∨ ⟦ e₁ ⟧ᵉ σ γ
-  ⟦ [ e ] ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ Vec.∷ []
-  ⟦ unbox e ⟧ᵉ σ γ = Vec.head (⟦ e ⟧ᵉ σ γ)
+  ⟦ [_] {t = t} e ⟧ᵉ σ γ = 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₁ ⟧ᵉ σ γ)
   ⟦ cast {t = t} eq e ⟧ᵉ σ γ = casted t eq (⟦ e ⟧ᵉ σ γ)
@@ -224,8 +269,8 @@ module Expression
   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 ([_] {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 (cast {t = t} eq e) v σ γ = update e (casted t (≡.sym eq) v) σ γ
   update (tup {es = []} x) v σ γ = σ , γ
-- 
cgit v1.2.3