StackLanguage.agda

{-
  A simple stack language example. Illustrating that one
  wants dependent elimination of inductive families.
-}

module StackLanguage where

open import Lib.Nat
open import Lib.Vec
open import Lib.Id

data Prog (A : Set) : Nat -> Set where
  init : Prog A 0
  push : forall {n} -> A -> Prog A n -> Prog A (suc n)
  pop  : forall {n} -> Prog A (suc n) -> Prog A n

⟦_⟧ : forall {A n} -> Prog A n -> Vec A n
⟦ init     ⟧ = ε
⟦ push x p ⟧ = x ► ⟦ p ⟧
⟦ pop p    ⟧ with ⟦ p ⟧
...             | x ► xs = xs

reify : forall {A n} -> Vec A n -> Prog A n
reify ε        = init
reify (x ► xs) = push x (reify xs)

normalise : forall {A n} -> Prog A n -> Prog A n
normalise p = reify ⟦ p ⟧

_≅_ : forall {A n} -> Prog A n -> Prog A n -> Set
p₁ ≅ p₂ = ⟦ p₁ ⟧ == ⟦ p₂ ⟧

sound : forall {A n} -> (p : Prog A n) -> normalise p ≅ p
sound init       = refl
sound (push x p) = cong (_►_ x) (sound p)
sound (pop p)    with ⟦ p ⟧ | sound p
...           | x ► xs | ih with ⟦ reify xs ⟧
sound (pop p) | x ► xs | refl  | .xs = refl