Programming Language Foundations in Agda: More

More.agda

module More where

-- This Gist is really underwhelming. I only added let statements to STLC. The
-- most interesting part are the functions `_⊆_` and `_⊑_` used for renamings
-- and substitutions respectively.

infixr 7 _⇒_
infixl 5 _,_

data Type : Set where
    _⇒_ : Type → Type → Type
    `⊤  : Type

data Context : Set where
    ∅   : Context
    _,_ : Context → Type → Context

infix 4 _∈_
infix 4 _⊢_

data _∈_ : Type → Context → Set where
    zero : ∀ {Γ A}
        -----------
        → A ∈ Γ , A

    suc : ∀ {Γ A B}
        → A ∈ Γ
        -----------
        → A ∈ Γ , B

data _⊢_ : Context → Type → Set where
    ` : ∀ {Γ A}
        → A ∈ Γ
        -------
        → Γ ⊢ A

    -- Arrow introduction.
    ƛ : ∀ {Γ A B}
        → Γ , A ⊢ B
        -----------
        → Γ ⊢ A ⇒ B

    -- Arrow elimination.
    _·_ : ∀ {Γ A B}
        → Γ ⊢ A ⇒ B
        → Γ ⊢ A
        -----------
        → Γ ⊢ B

    `let : ∀ {Γ A B}
        → Γ ⊢ A
        → Γ , A ⊢ B
        -----------
        → Γ ⊢ B

    `tt : ∀ {Γ}
        --------
        → Γ ⊢ `⊤

infix 4 _⊆_

_⊆_ : Context → Context → Set
Γ ⊆ Δ = ∀ {A} → A ∈ Γ → A ∈ Δ

ext : ∀ {Γ Δ A}
    → Γ ⊆ Δ
    ---------------
    → Γ , A ⊆ Δ , A
ext ρ zero    = zero
ext ρ (suc x) = suc (ρ x)

rename : ∀ {Γ Δ A}
    → Γ ⊆ Δ
    → Γ ⊢ A
    -------
    → Δ ⊢ A
rename ρ (` x)       = ` (ρ x)
rename ρ (ƛ M)       = ƛ (rename (ext ρ) M)
rename ρ (M · N)     = rename ρ M · rename ρ N
rename ρ (`let M N)  = `let (rename ρ M) (rename (ext ρ) N)
rename ρ `tt         = `tt

infix 4 _⊑_

_⊑_ : Context → Context → Set
Γ ⊑ Δ = ∀ {A} → A ∈ Γ → Δ ⊢ A

exts : ∀ {Γ Δ A}
    → Γ ⊑ Δ
    ---------------
    → Γ , A ⊑ Δ , A
exts σ zero    = ` zero
exts σ (suc x) = rename suc (σ x)

subst : ∀ {Γ Δ A}
    → Γ ⊑ Δ
    → Γ ⊢ A
    -------
    → Δ ⊢ A
subst σ (` x)      = σ x
subst σ (ƛ M)      = ƛ (subst (exts σ) M)
subst σ (M · N)    = subst σ M · subst σ N
subst σ (`let M N) = `let (subst σ M) (subst (exts σ) N)
subst σ `tt        = `tt

_[_] : ∀ {Γ A B}
    → Γ , A ⊢ B
    → Γ ⊢ A
    -----------
    → Γ ⊢ B
_[_] {Γ} {A} M N = subst σ M
    where
    σ : Γ , A ⊑ Γ
    σ zero    = N
    σ (suc x) = ` x

data Value : ∀ {Γ A} → Γ ⊢ A → Set where
    ƛ : ∀ {Γ A B} {M : Γ , A ⊢ B}
        -------------
        → Value (ƛ M)

    `tt : ∀ {Γ}
        ---------------
        → Value (`tt {Γ})

infix 3 _—→_

data _—→_ : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A → Set where
    ξ-·₁ : ∀ {Γ A B} {M M' : Γ ⊢ A ⇒ B} {N : Γ ⊢ A}
        → M —→ M'
        -----------------
        → M · N —→ M' · N

    ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M' : Γ ⊢ A}
        → Value V
        → M —→ M'
        -----------------
        → V · M —→ V · M'

    β-ƛ : ∀ {Γ A B} {M : Γ , A ⊢ B} {V : Γ ⊢ A}
        → Value V
        ----------------------
        → (ƛ M) · V —→ M [ V ]

    ξ-`let : ∀ {Γ A B} {M M' : Γ ⊢ A} {N : Γ , A ⊢ B}
        → M —→ M'
        -----------------------
        → `let M N —→ `let M' N

    β-`let : ∀ {Γ A B} {V : Γ ⊢ A} {M : Γ , A ⊢ B}
        → Value V
        ---------------------
        → `let V M —→ M [ V ]

infix 3 _—→*_

data _—→*_ : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A → Set where
    _∎ : ∀ {Γ A} (M : Γ ⊢ A)
        ---------
        → M —→* M

    _—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
        → L —→ M
        → M —→* N
        ---------
        → L —→* N

data Progress {A} (M : ∅ ⊢ A) : Set where
    step : ∀ {N : ∅ ⊢ A}
        → M —→ N
        ------------
        → Progress M

    done :
        Value M
        ------------
        → Progress M

progress : ∀ {A}
    → ∀ (M : ∅ ⊢ A)
    ---------------
    → Progress M
progress (ƛ M) = done ƛ
progress (M · N) with progress M
... | step M—→M' = step (ξ-·₁ M—→M')
... | done ƛ with progress N
...     | step N—→N' = step (ξ-·₂ ƛ N—→N')
...     | done VN    = step (β-ƛ VN)
progress (`let M N) with progress M
... | step M—→M' = step (ξ-`let M—→M')
... | done VM    = step (β-`let VM)
progress `tt = done `tt