Do a big refactor.

- Replace the decidable predicates on expressions and statements with
  separate data types.

- Reorganise the Hoare logic semantics to remove unnecessary
  definitions.

- Make liberal use of modules to group related definitions together.

- Unify the types for denotational and Hoare logic semantics.

- Make bits an abstraction of array types.

1 files changed, 222 insertions, 300 deletions

diff --git a/src/Helium/Data/Pseudocode/Core.agda b/src/Helium/Data/Pseudocode/Core.agda
index 079e2ce..579d68d 100644
--- a/src/Helium/Data/Pseudocode/Core.agda
+++ b/src/Helium/Data/Pseudocode/Core.agda
@@ -11,20 +11,18 @@ module Helium.Data.Pseudocode.Core where
 open import Data.Bool using (Bool; true; false)
 open import Data.Fin as Fin using (Fin)
 open import Data.Fin.Patterns
+open import Data.Integer as ℤ using (ℤ)
 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.Sum using ([_,_]′; inj₁; inj₂)
+open import Data.Product using (_×_; _,_)
+open import Data.Unit using (⊤)
 open import Data.Vec using (Vec; []; _∷_; lookup; map)
-open import Data.Vec.Relation.Unary.All using (All; []; _∷_; reduce)
-open import Data.Vec.Relation.Unary.Any using (Any; here; there)
-open import Function as F using (_∘_; _∘′_; _∋_)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
-open import Relation.Nullary using (Dec; yes; no)
-open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromWitness; map′)
-open import Relation.Nullary.Product using (_×-dec_)
-open import Relation.Nullary.Sum using (_⊎-dec_)
-open import Relation.Unary using (Decidable)
+open import Data.Vec.Relation.Unary.All using (All; []; _∷_)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+
+private
+  variable
+    k m n o : ℕ
 
 --- The set of types and boolean properties of them
 data Type : Set where
@@ -33,297 +31,221 @@ data Type : Set where
   fin   : (n : ℕ) → Type
   real  : Type
   bit   : Type
-  bits  : (n : ℕ) → Type
-  tuple : ∀ n → Vec Type n → Type
+  tuple : Vec Type n → Type
   array : Type → (n : ℕ) → Type
 
+bits : ℕ → Type
+bits = array bit
+
+private
+  variable
+    t t′ t₁ t₂ : Type
+    Σ Γ Δ ts : Vec Type n
+
 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
-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 (λ ())
+  instance bool  : HasEquality bool
+  instance int   : HasEquality int
+  instance fin   : HasEquality (fin n)
+  instance real  : HasEquality real
+  instance bit   : HasEquality bit
+  instance array : ∀ {t n} → ⦃ HasEquality t ⦄ → HasEquality (array t n)
+
+data Ordered : Type → Set where
+  instance int  : Ordered int
+  instance fin  : Ordered (fin n)
+  instance real : Ordered real
 
 data IsNumeric : Type → Set where
-  int  : IsNumeric int
-  real : IsNumeric real
-
-isNumeric? : Decidable IsNumeric
-isNumeric? bool        = no (λ ())
-isNumeric? int         = yes int
-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 (λ ())
-
-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
-  array : Type → Sliced
-
-asType : Sliced → ℕ → Type
-asType bits      n = bits n
-asType (array t) n = array t n
-
-elemType : Sliced → Type
-elemType bits      = bit
-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  : 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
-
-module Code {o} (Σ : Vec Type o) where
-  data Expression {n} (Γ : Vec Type n) : Type → Set
-  data CanAssign {n Γ} : ∀ {t} → Expression {n} Γ t → Set
-  canAssign? : ∀ {n Γ t} → Decidable (CanAssign {n} {Γ} {t})
-  data ReferencesState {n Γ} : ∀ {t} → Expression {n} Γ t → Set
-  referencesState? : ∀ {n Γ t} → Decidable (ReferencesState {n} {Γ} {t})
-  data Statement {n} (Γ : Vec Type n) : Set
-  data ChangesState {n Γ} : Statement {n} Γ → Set
-  changesState? : ∀ {n Γ} → Decidable (ChangesState {n} {Γ})
-  data Function {n} (Γ : Vec Type n) (ret : Type) : Set
-  data Procedure {n} (Γ : Vec Type n) : Set
-
-  infix  8 -_
-  infixr 7 _^_
-  infixl 6 _*_ _and_ _>>_
-  -- infixl 6 _/_
-  infixl 5 _+_ _or_ _&&_ _||_
-  infix  4 _≟_ _<?_
-
-  data Expression {n} Γ where
-    lit    : ∀ {t} → Literal t → Expression Γ t
-    state  : ∀ i → Expression Γ (lookup Σ i)
-    var    : ∀ i → Expression Γ (lookup Γ i)
-    abort  : ∀ {t} → Expression Γ (fin 0) → Expression Γ t
-    _≟_    : ∀ {t} {hasEquality : True (hasEquality? t)} → Expression Γ t → Expression Γ t → Expression Γ bool
-    _<?_   : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → Expression Γ t → Expression Γ bool
-    inv    : Expression Γ bool → Expression Γ bool
-    _&&_   : Expression Γ bool → Expression Γ bool → Expression Γ bool
-    _||_   : Expression Γ bool → Expression Γ bool → Expression Γ bool
-    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 Γ (elemType t) → Expression Γ (asType t 1)
-    unbox  : ∀ {t} → Expression Γ (asType t 1) → Expression Γ (elemType t)
-    splice : ∀ {m n t} → Expression Γ (asType t m) → Expression Γ (asType t n) → Expression Γ (fin (suc n)) → Expression Γ (asType t (n ℕ.+ m))
-    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₂)
-    -- _/_   : Expression Γ real → Expression Γ real → Expression Γ real
-    _^_    : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → ℕ → Expression Γ t
-    _>>_   : Expression Γ int → ℕ → Expression Γ int
-    rnd    : Expression Γ real → Expression Γ int
-    fin    : ∀ {k ms n} → (All (Fin) ms → Fin n) → Expression Γ (tuple k (map fin ms)) → Expression Γ (fin n)
-    asInt  : ∀ {m} → Expression Γ (fin m) → Expression Γ int
-    nil    : Expression Γ (tuple 0 [])
-    cons   : ∀ {m t ts} → Expression Γ t → Expression Γ (tuple m ts) → Expression Γ (tuple (suc m) (t ∷ 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 → All (Expression Γ) {m} Δ → Expression Γ t
-    if_then_else_ : ∀ {t} → Expression Γ bool → Expression Γ t → Expression Γ t → Expression Γ t
-
-  data CanAssign {n} {Γ} where
-    state : ∀ i → CanAssign (state i)
-    var   : ∀ i → CanAssign (var i)
-    abort : ∀ {t} e → CanAssign (abort {t = t} e)
-    [_]   : ∀ {t e} → CanAssign e → CanAssign ([_] {t = t} e)
-    unbox : ∀ {t e} → CanAssign e → CanAssign (unbox {t = t} e)
-    splice : ∀ {m n t e₁ e₂} → CanAssign e₁ → CanAssign e₂ → ∀ e₃ → CanAssign (splice {m = m} {n} {t} e₁ e₂ e₃)
-    cut    : ∀ {m n t e₁} → CanAssign e₁ → ∀ e₂ → CanAssign (cut {m = m} {n} {t} e₁ e₂)
-    cast  : ∀ {i j t e} .(eq : i ≡ j) → CanAssign e → CanAssign (cast {t = t} eq e)
-    nil   : CanAssign nil
-    cons  : ∀ {m t ts e₁ e₂} → CanAssign e₁ → CanAssign e₂ → CanAssign (cons {m = m} {t} {ts} e₁ e₂)
-    head  : ∀ {m t ts e} → CanAssign e → CanAssign (head {m = m} {t} {ts} e)
-    tail  : ∀ {m t ts e} → CanAssign e → CanAssign (tail {m = m} {t} {ts} e)
-
-  canAssign? (lit x)      = no λ ()
-  canAssign? (state i)    = yes (state i)
-  canAssign? (var i)      = yes (var i)
-  canAssign? (abort e)    = yes (abort e)
-  canAssign? (e ≟ e₁)     = no λ ()
-  canAssign? (e <? e₁)    = no λ ()
-  canAssign? (inv e)      = no λ ()
-  canAssign? (e && e₁)    = no λ ()
-  canAssign? (e || e₁)    = no λ ()
-  canAssign? (not e)      = no λ ()
-  canAssign? (e and e₁)   = no λ ()
-  canAssign? (e or e₁)    = no λ ()
-  canAssign? [ e ]        = map′ [_] (λ { [ e ] → e }) (canAssign? e)
-  canAssign? (unbox e)    = map′ unbox (λ { (unbox e) → e }) (canAssign? e)
-  canAssign? (splice e e₁ e₂) = map′ (λ (e , e₁) → splice e e₁ e₂) (λ { (splice e e₁ _) → e , e₁ }) (canAssign? e ×-dec canAssign? e₁)
-  canAssign? (cut e e₁)       = map′ (λ e → cut e e₁) (λ { (cut 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? (rnd e)      = no λ ()
-  canAssign? (fin x e)    = no λ ()
-  canAssign? (asInt e)    = no λ ()
-  canAssign? nil          = yes nil
-  canAssign? (cons e e₁)  = map′ (uncurry cons) (λ { (cons e e₁) → e , e₁ }) (canAssign? e ×-dec canAssign? e₁)
-  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 λ ()
-
-  data ReferencesState where
-    state : ∀ i → ReferencesState (state i)
-    [_] : ∀ {t e} → ReferencesState e → ReferencesState ([_] {t = t} e)
-    unbox : ∀ {t e} → ReferencesState e → ReferencesState (unbox {t = t} e)
-    spliceˡ : ∀ {m n t e} → ReferencesState e → ∀ e₁ e₂ → ReferencesState (splice {m = m} {n} {t} e e₁ e₂)
-    spliceʳ : ∀ {m n t} e {e₁} → ReferencesState e₁ → ∀ e₂ → ReferencesState (splice {m = m} {n} {t} e e₁ e₂)
-    cut : ∀ {m n t e} → ReferencesState e → ∀ e₁ → ReferencesState (cut {m = m} {n} {t} e e₁)
-    cast : ∀ {i j t} .(eq : i ≡ j) {e} → ReferencesState e → ReferencesState (cast {t = t} eq e)
-    consˡ : ∀ {m t ts e} → ReferencesState e → ∀ e₁ → ReferencesState (cons {m = m} {t} {ts} e e₁)
-    consʳ : ∀ {m t ts} e {e₁} → ReferencesState e₁ → ReferencesState (cons {m = m} {t} {ts} e e₁)
-    head : ∀ {m t ts e} → ReferencesState e → ReferencesState (head {m = m} {t} {ts} e)
-    tail : ∀ {m t ts e} → ReferencesState e → ReferencesState (tail {m = m} {t} {ts} e)
-
-  referencesState? (lit x) = no λ ()
-  referencesState? (state i) = yes (state i)
-  referencesState? (var i) = no λ ()
-  referencesState? (abort e) = no λ ()
-  referencesState? (e ≟ e₁) = no λ ()
-  referencesState? (e <? e₁) = no λ ()
-  referencesState? (inv e) = no λ ()
-  referencesState? (e && e₁) = no λ ()
-  referencesState? (e || e₁) = no λ ()
-  referencesState? (not e) = no λ ()
-  referencesState? (e and e₁) = no λ ()
-  referencesState? (e or e₁) = no λ ()
-  referencesState? [ e ] = map′ [_] (λ { [ e ] → e }) (referencesState? e)
-  referencesState? (unbox e) = map′ unbox (λ { (unbox e) → e }) (referencesState? e)
-  referencesState? (splice e e₁ e₂) = map′ [ (λ e → spliceˡ e e₁ e₂) , (λ e₁ → spliceʳ e e₁ e₂) ]′ (λ { (spliceˡ e e₁ e₂) → inj₁ e ; (spliceʳ e e₁ e₂) → inj₂ e₁ }) (referencesState? e ⊎-dec referencesState? e₁)
-  referencesState? (cut e e₁) = map′ (λ e → cut e e₁) (λ { (cut e e₁) → e }) (referencesState? e)
-  referencesState? (cast eq e) = map′ (cast eq) (λ { (cast eq e) → e }) (referencesState? e)
-  referencesState? (- e) = no λ ()
-  referencesState? (e + e₁) = no λ ()
-  referencesState? (e * e₁) = no λ ()
-  referencesState? (e ^ x) = no λ ()
-  referencesState? (e >> x) = no λ ()
-  referencesState? (rnd e) = no λ ()
-  referencesState? (fin x e) = no λ ()
-  referencesState? (asInt e) = no λ ()
-  referencesState? nil = no λ ()
-  referencesState? (cons e e₁) = map′ [ (λ e → consˡ e e₁) , (λ e₁ → consʳ e e₁) ]′ (λ { (consˡ e e₁) → inj₁ e ; (consʳ e e₁) → inj₂ e₁ }) (referencesState? e ⊎-dec referencesState? e₁)
-  referencesState? (head e) = map′ head (λ { (head e) → e }) (referencesState? e)
-  referencesState? (tail e) = map′ tail (λ { (tail e) → e }) (referencesState? e)
-  referencesState? (call f es) = no λ ()
-  referencesState? (if e then e₁ else e₂) = no λ ()
-
-  infix  4 _≔_
-  infixl 2 if_then_else_ if_then_
-  infixl 1 _∙_ _∙return_
-  infix  1 _∙end
-
-  data Statement Γ where
-    _∙_           : Statement Γ → Statement Γ → Statement Γ
-    skip          : Statement Γ
-    _≔_           : ∀ {t} → (ref : Expression Γ t) → {canAssign : True (canAssign? ref)} → Expression Γ t → Statement Γ
-    declare       : ∀ {t} → Expression Γ t → Statement (t ∷ Γ) → Statement Γ
-    invoke        : ∀ {m Δ} → Procedure Δ → All (Expression Γ) {m} Δ → Statement Γ
-    if_then_      : Expression Γ bool → Statement Γ → Statement Γ
-    if_then_else_ : Expression Γ bool → Statement Γ → Statement Γ → Statement Γ
-    for           : ∀ m → Statement (fin m ∷ Γ) → Statement Γ
-
-  data ChangesState where
-    _∙ˡ_           : ∀ {s} → ChangesState s → ∀ s₁ → ChangesState (s ∙ s₁)
-    _∙ʳ_           : ∀ s {s₁} → ChangesState s₁ → ChangesState (s ∙ s₁)
-    _≔_            : ∀ {t} ref {canAssign : True (canAssign? ref)} {refsState : True (referencesState? ref)} e₂ → ChangesState (_≔_ {t = t} ref {canAssign} e₂)
-    declare        : ∀ {t} e {s} → ChangesState s → ChangesState (declare {t = t} e s)
-    invoke         : ∀ {m Δ} p es → ChangesState (invoke {m = m} {Δ} p es)
-    if_then_       : ∀ e {s} → ChangesState s → ChangesState (if e then s)
-    if_then′_else_ : ∀ e {s} → ChangesState s → ∀ s₁ → ChangesState (if e then s else s₁)
-    if_then_else′_ : ∀ e s {s₁} → ChangesState s₁ → ChangesState (if e then s else s₁)
-    for            : ∀ m {s} → ChangesState s → ChangesState (for m s)
-
-  changesState? (s ∙ s₁)              = map′ [ _∙ˡ s₁ , s ∙ʳ_ ]′ (λ { (s ∙ˡ s₁) → inj₁ s ; (s ∙ʳ s₁) → inj₂ s₁ }) (changesState? s ⊎-dec changesState? s₁)
-  changesState? skip                  = no λ ()
-  changesState? (_≔_ ref e)           = map′ (λ refsState → _≔_ ref {refsState = fromWitness refsState} e) (λ { (_≔_ ref {refsState = refsState} e) → toWitness refsState }) (referencesState? ref)
-  changesState? (declare e s)         = map′ (declare e) (λ { (declare e s) → s }) (changesState? s)
-  changesState? (invoke p e)          = yes (invoke p e)
-  changesState? (if e then s)         = map′ (if e then_) (λ { (if e then s) → s }) (changesState? s)
-  changesState? (if e then s else s₁) = map′ [ if e then′_else s₁ , if e then s else′_ ]′ (λ { (if e then′ s else s₁) → inj₁ s ; (if e then s else′ s₁) → inj₂ s₁ }) (changesState? s ⊎-dec changesState? s₁)
-  changesState? (for m s)             = map′ (for m) (λ { (for m s) → s }) (changesState? s)
-
-  data Function Γ ret where
-    _∙return_ : (s : Statement Γ) → {False (changesState? s)} → Expression Γ ret → Function Γ ret
-    declare   : ∀ {t} → Expression Γ t → Function (t ∷ Γ) ret → Function Γ ret
-
-  data Procedure Γ where
-    _∙end   : Statement Γ → Procedure Γ
-
-  infixl  6 _<<_
-  infixl 5 _-_ _∶_
-
-  tup : ∀ {n Γ m ts} → All (Expression {n} Γ) ts → Expression Γ (tuple m ts)
-  tup []       = nil
-  tup (e ∷ es) = cons e (tup es)
-
-  _∶_ : ∀ {n Γ i j t} → Expression {n} Γ (asType t j) → Expression Γ (asType t i) → Expression Γ (asType t (i ℕ.+ j))
-  e₁ ∶ e₂ = splice e₁ e₂ (lit (Fin.fromℕ _ ′f))
-
-  slice : ∀ {n Γ i j t} → Expression {n} Γ (asType t (i ℕ.+ j)) → Expression Γ (fin (suc i)) → Expression Γ (asType t j)
-  slice e₁ e₂ = head (cut e₁ e₂)
-
-  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
-  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 (1F ′f))) +
-    ( if slice′ x (lit (0F ′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 ∷ []) ′xs) then - lit (1 ′i) else lit (0 ′i)
-  sint {m = suc (suc m)} x =
-    lit (2 ′i) * sint (slice {i = 1} x (lit (1F ′f))) +
-    ( if slice′ x (lit (0F ′f)) ≟ lit ((true ∷ []) ′xs)
-      then lit (1 ′i)
-      else lit (0 ′i))
+  instance int  : IsNumeric int
+  instance real : IsNumeric real
+
+_+ᵗ_ : IsNumeric t₁ → IsNumeric t₂ → Type
+int  +ᵗ int  = int
+int  +ᵗ real = real
+real +ᵗ t₂   = real
+
+literalType : Type → Set
+literalTypes : Vec Type n → Set
+
+literalType bool        = Bool
+literalType int         = ℤ
+literalType (fin n)     = Fin n
+literalType real        = ℤ
+literalType bit         = Bool
+literalType (tuple ts)  = literalTypes ts
+literalType (array t n) = Vec (literalType t) n
+
+literalTypes []            = ⊤
+literalTypes (t ∷ [])      = literalType t
+literalTypes (t ∷ t′ ∷ ts) = literalType t × literalTypes (t′ ∷ ts)
+
+infix  8 -_
+infixr 7 _^_
+infixl 6 _*_ _and_ _>>_
+infixl 5 _+_ _or_ _&&_ _||_
+infix  4 _≟_ _<?_
+infix  3 _≔_
+
+infixl 2 if_then_ if_then_else_
+infixl 1 _∙_ _∙return_
+infix  1 _∙end
+
+data Expression (Σ : Vec Type o) (Γ : Vec Type n) : Type → Set
+data Reference (Σ : Vec Type o) (Γ : Vec Type n) : Type → Set
+data LocalReference (Σ : Vec Type o) (Γ : Vec Type n) : Type → Set
+data Statement (Σ : Vec Type o) (Γ : Vec Type n) : Set
+data LocalStatement (Σ : Vec Type o) (Γ : Vec Type n) : Set
+data Function (Σ : Vec Type o) (Γ : Vec Type n) (ret : Type) : Set
+data Procedure (Σ : Vec Type o) (Γ : Vec Type n) : Set
+
+data Expression Σ Γ where
+  lit           : literalType t → Expression Σ Γ t
+  state         : ∀ i → Expression Σ Γ (lookup Σ i)
+  var           : ∀ i → Expression Σ Γ (lookup Γ i)
+  _≟_           : ⦃ HasEquality t ⦄ → Expression Σ Γ t → Expression Σ Γ t → Expression Σ Γ bool
+  _<?_          : ⦃ Ordered t ⦄ → Expression Σ Γ t → Expression Σ Γ t → Expression Σ Γ bool
+  inv           : Expression Σ Γ bool → Expression Σ Γ bool
+  _&&_          : Expression Σ Γ bool → Expression Σ Γ bool → Expression Σ Γ bool
+  _||_          : Expression Σ Γ bool → Expression Σ Γ bool → Expression Σ Γ bool
+  not           : Expression Σ Γ (bits n) → Expression Σ Γ (bits n)
+  _and_         : Expression Σ Γ (bits n) → Expression Σ Γ (bits n) → Expression Σ Γ (bits n)
+  _or_          : Expression Σ Γ (bits n) → Expression Σ Γ (bits n) → Expression Σ Γ (bits n)
+  [_]           : Expression Σ Γ t → Expression Σ Γ (array t 1)
+  unbox         : Expression Σ Γ (array t 1) → Expression Σ Γ t
+  merge         : Expression Σ Γ (array t m) → Expression Σ Γ (array t n) → Expression Σ Γ (fin (suc n)) → Expression Σ Γ (array t (n ℕ.+ m))
+  slice         : Expression Σ Γ (array t (n ℕ.+ m)) → Expression Σ Γ (fin (suc n)) → Expression Σ Γ (array t m)
+  cut           : Expression Σ Γ (array t (n ℕ.+ m)) → Expression Σ Γ (fin (suc n)) → Expression Σ Γ (array t n)
+  cast          : .(eq : m ≡ n) → Expression Σ Γ (array t m) → Expression Σ Γ (array t n)
+  -_            : ⦃ IsNumeric t ⦄ → Expression Σ Γ t → Expression Σ Γ t
+  _+_           : ⦃ isNum₁ : IsNumeric t₁ ⦄ → ⦃ isNum₂ : IsNumeric t₂ ⦄ → Expression Σ Γ t₁ → Expression Σ Γ t₂ → Expression Σ Γ (isNum₁ +ᵗ isNum₂)
+  _*_           : ⦃ isNum₁ : IsNumeric t₁ ⦄ → ⦃ isNum₂ : IsNumeric t₂ ⦄ → Expression Σ Γ t₁ → Expression Σ Γ t₂ → Expression Σ Γ (isNum₁ +ᵗ isNum₂)
+  _^_           : ⦃ IsNumeric t ⦄ → Expression Σ Γ t → ℕ → Expression Σ Γ t
+  _>>_          : Expression Σ Γ int → (n : ℕ) → Expression Σ Γ int
+  rnd           : Expression Σ Γ real → Expression Σ Γ int
+  fin           : ∀ {ms} (f : literalTypes (map fin ms) → Fin n) → Expression Σ Γ (tuple {n = k} (map fin ms)) → Expression Σ Γ (fin n)
+  asInt         : Expression Σ Γ (fin n) → Expression Σ Γ int
+  nil           : Expression Σ Γ (tuple [])
+  cons          : Expression Σ Γ t → Expression Σ Γ (tuple ts) → Expression Σ Γ (tuple (t ∷ ts))
+  head          : Expression Σ Γ (tuple (t ∷ ts)) → Expression Σ Γ t
+  tail          : Expression Σ Γ (tuple (t ∷ ts)) → Expression Σ Γ (tuple ts)
+  call          : (f : Function Σ Δ t) → All (Expression Σ Γ) Δ → Expression Σ Γ t
+  if_then_else_ : Expression Σ Γ bool → Expression Σ Γ t → Expression Σ Γ t → Expression Σ Γ t
+
+data Reference Σ Γ where
+  state : ∀ i → Reference Σ Γ (lookup Σ i)
+  var   : ∀ i → Reference Σ Γ (lookup Γ i)
+  [_]   : Reference Σ Γ t → Reference Σ Γ (array t 1)
+  unbox : Reference Σ Γ (array t 1) → Reference Σ Γ t
+  merge : Reference Σ Γ (array t m) → Reference Σ Γ (array t n) → Expression Σ Γ (fin (suc n)) → Reference Σ Γ (array t (n ℕ.+ m))
+  slice : Reference Σ Γ (array t (n ℕ.+ m)) → Expression Σ Γ (fin (suc n)) → Reference Σ Γ (array t m)
+  cut   : Reference Σ Γ (array t (n ℕ.+ m)) → Expression Σ Γ (fin (suc n)) → Reference Σ Γ (array t n)
+  cast  : .(eq : m ≡ n) → Reference Σ Γ (array t m) → Reference Σ Γ (array t n)
+  nil   : Reference Σ Γ (tuple [])
+  cons  : Reference Σ Γ t → Reference Σ Γ (tuple ts) → Reference Σ Γ (tuple (t ∷ ts))
+  head  : Reference Σ Γ (tuple (t ∷ ts)) → Reference Σ Γ t
+  tail  : Reference Σ Γ (tuple (t ∷ ts)) → Reference Σ Γ (tuple ts)
+
+data LocalReference Σ Γ where
+  var   : ∀ i → LocalReference Σ Γ (lookup Γ i)
+  [_]   : LocalReference Σ Γ t → LocalReference Σ Γ (array t 1)
+  unbox : LocalReference Σ Γ (array t 1) → LocalReference Σ Γ t
+  merge : LocalReference Σ Γ (array t m) → LocalReference Σ Γ (array t n) → Expression Σ Γ (fin (suc n)) → LocalReference Σ Γ (array t (n ℕ.+ m))
+  slice : LocalReference Σ Γ (array t (n ℕ.+ m)) → Expression Σ Γ (fin (suc n)) → LocalReference Σ Γ (array t m)
+  cut   : LocalReference Σ Γ (array t (n ℕ.+ m)) → Expression Σ Γ (fin (suc n)) → LocalReference Σ Γ (array t n)
+  cast  : .(eq : m ≡ n) → LocalReference Σ Γ (array t m) → LocalReference Σ Γ (array t n)
+  nil   : LocalReference Σ Γ (tuple [])
+  cons  : LocalReference Σ Γ t → LocalReference Σ Γ (tuple ts) → LocalReference Σ Γ (tuple (t ∷ ts))
+  head  : LocalReference Σ Γ (tuple (t ∷ ts)) → LocalReference Σ Γ t
+  tail  : LocalReference Σ Γ (tuple (t ∷ ts)) → LocalReference Σ Γ (tuple ts)
+
+data Statement Σ Γ where
+  _∙_           : Statement Σ Γ → Statement Σ Γ → Statement Σ Γ
+  skip          : Statement Σ Γ
+  _≔_           : Reference Σ Γ t → Expression Σ Γ t → Statement Σ Γ
+  declare       : Expression Σ Γ t → Statement Σ (t ∷ Γ) → Statement Σ Γ
+  invoke        : (f : Procedure Σ Δ) → All (Expression Σ Γ) Δ → Statement Σ Γ
+  if_then_      : Expression Σ Γ bool → Statement Σ Γ → Statement Σ Γ
+  if_then_else_ : Expression Σ Γ bool → Statement Σ Γ → Statement Σ Γ → Statement Σ Γ
+  for           : ∀ n → Statement Σ (fin n ∷ Γ) → Statement Σ Γ
+
+data LocalStatement Σ Γ where
+  _∙_           : LocalStatement Σ Γ → LocalStatement Σ Γ → LocalStatement Σ Γ
+  skip          : LocalStatement Σ Γ
+  _≔_           : LocalReference Σ Γ t → Expression Σ Γ t → LocalStatement Σ Γ
+  declare       : Expression Σ Γ t → LocalStatement Σ (t ∷ Γ) → LocalStatement Σ Γ
+  if_then_      : Expression Σ Γ bool → LocalStatement Σ Γ → LocalStatement Σ Γ
+  if_then_else_ : Expression Σ Γ bool → LocalStatement Σ Γ → LocalStatement Σ Γ → LocalStatement Σ Γ
+  for           : ∀ n → LocalStatement Σ (fin n ∷ Γ) → LocalStatement Σ Γ
+
+data Function Σ Γ ret where
+  declare   : Expression Σ Γ t → Function Σ (t ∷ Γ) ret → Function Σ Γ ret
+  _∙return_ : LocalStatement Σ Γ → Expression Σ Γ ret → Function Σ Γ ret
+
+data Procedure Σ Γ where
+  _∙end : Statement Σ Γ → Procedure Σ Γ
+
+infixl 6 _<<_
+infixl 5 _-_ _∶_
+
+tup : All (Expression Σ Γ) ts → Expression Σ Γ (tuple ts)
+tup []       = nil
+tup (e ∷ es) = cons e (tup es)
+
+_∶_ : Expression Σ Γ (array t m) → Expression Σ Γ (array t n) → Expression Σ Γ (array t (n ℕ.+ m))
+e ∶ e₁ = merge e e₁ (lit (Fin.fromℕ _))
+
+slice′ : Expression Σ Γ (array t (n ℕ.+ m)) → Expression Σ Γ (fin (suc m)) → Expression Σ Γ (array t n)
+slice′ {m = m} e = slice (cast (+-comm _ m) e)
+
+_-_ : Expression Σ Γ t₁ → ⦃ isNum₁ : IsNumeric t₁ ⦄ → Expression Σ Γ t₂ → ⦃ isNum₂ : IsNumeric t₂ ⦄ → Expression Σ Γ (isNum₁ +ᵗ isNum₂)
+e - e₁ = e + (- e₁)
+
+_<<_ : Expression Σ Γ int → (n : ℕ) → Expression Σ Γ int
+e << n = e * lit (ℤ.+ (2 ℕ.^ n))
+
+getBit : ℕ → Expression Σ Γ int → Expression Σ Γ bit
+getBit i x = if x - x >> suc i << suc i <? lit (ℤ.+ (2 ℕ.^ i)) then lit false else lit true
+
+uint : Expression Σ Γ (bits m) → Expression Σ Γ int
+uint {m = 0}     x = lit ℤ.0ℤ
+uint {m = suc m} x =
+  lit (ℤ.+ 2) * uint {m = m} (slice x (lit 1F)) +
+  ( if slice′ x (lit 0F) ≟ lit (true ∷ [])
+    then lit ℤ.1ℤ
+    else lit ℤ.0ℤ)
+
+sint : Expression Σ Γ (bits m) → Expression Σ Γ int
+sint {m = 0}           x = lit ℤ.0ℤ
+sint {m = 1}           x = if x ≟ lit (true ∷ []) then lit ℤ.-1ℤ else lit ℤ.0ℤ
+sint {m = suc (suc m)} x =
+  lit (ℤ.+ 2) * sint {m = m} (slice x (lit 1F)) +
+  ( if slice′ x (lit 0F) ≟ lit (true ∷ [])
+    then lit ℤ.1ℤ
+    else lit ℤ.0ℤ)
+
+!_ : Reference Σ Γ t → Expression Σ Γ t
+! state i          = state i
+! var i            = var i
+! [ ref ]          = [ ! ref ]
+! unbox ref        = unbox (! ref)
+! merge ref ref₁ e = merge (! ref) (! ref₁) e
+! slice ref x      = slice (! ref) x
+! cut ref x        = cut (! ref) x
+! cast eq ref      = cast eq (! ref)
+! nil              = nil
+! cons ref ref₁    = cons (! ref) (! ref₁)
+! head ref         = head (! ref)
+! tail ref         = tail (! ref)
+
+!!_ : LocalReference Σ Γ t → Expression Σ Γ t
+!! var i            = var i
+!! [ ref ]          = [ !! ref ]
+!! unbox ref        = unbox (!! ref)
+!! merge ref ref₁ x = merge (!! ref) (!! ref₁) x
+!! slice ref x      = slice (!! ref) x
+!! cut ref x        = cut (!! ref) x
+!! cast eq ref      = cast eq (!! ref)
+!! nil              = nil
+!! cons ref ref₁    = cons (!! ref) (!! ref₁)
+!! head ref         = head (!! ref)
+!! tail ref         = tail (!! ref)