Programming Language Foundations in Agda: Untyped

Untyped.agda

module Untyped where

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

    ƛ : ∀ {Γ}
        → Γ , ★ ⊢ ★
        -----------
        → Γ ⊢ ★

    _·_ : ∀ {Γ}
        → Γ ⊢ ★
        → Γ ⊢ ★
        -------
        → Γ ⊢ ★

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

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

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

data Neutral : ∀ {Γ A} → Γ ⊢ A → Set
data Normal  : ∀ {Γ A} → Γ ⊢ A → Set

data Neutral where
    ` : ∀ {Γ A} (x : A ∈ Γ)
        ---------------
        → Neutral (` x)

    _·_ : ∀ {Γ} {M N : Γ ⊢ ★}
        → Neutral M
        → Normal N
        -----------------
        → Neutral (M · N)

data Normal where
    ` : ∀ {Γ A} {M : Γ ⊢ A}
        → Neutral M
        -----------
        → Normal M

    ƛ : ∀ {Γ} {M : Γ , ★ ⊢ ★}
        → Normal M
        --------------
        → Normal (ƛ M)

infix 3 _—→_

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

    ξ₂ : ∀ {Γ} {M N N' : Γ ⊢ ★}
        → N —→ N'
        -----------------
        → M · N —→ M · N'

    β : ∀ {Γ} {M : Γ , ★ ⊢ ★} {N : Γ ⊢ ★}
        ----------------------
        → (ƛ M) · N —→ M [ N ]

    ζ : ∀ {Γ} {M M' : Γ , ★ ⊢ ★}
        → M —→ M'
        -------------
        → ƛ M —→ ƛ M'

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 :
        Normal M
        ------------
        → Progress M

progress : ∀ {Γ A}
    → (M : Γ ⊢ A)
    -------------
    → Progress M
progress (` x) = done (` (` x))
progress (M · N) with progress M
... | step M—→M'  = step (ξ₁ M—→M')
... | done (ƛ NM) = step β
... | done (` x) with progress N
...     | step N—→N' = step (ξ₂ N—→N')
...     | done NN    = done (` (x · NN))
progress (ƛ M) with progress M
... | step M—→M' = step (ζ M—→M')
... | done NM    = done (ƛ NM)

data Gas : Set where
    zero : Gas
    suc  : Gas → Gas

{-# BUILTIN NATURAL Gas #-}

data Finished {Γ A} (M : Γ ⊢ A) : Set where
    done :
        Normal M
        ------------
        → Finished M

    out-of-gas :
        ----------
        Finished M

data Steps : ∀ {Γ A} → Γ ⊢ A → Set where
    steps : ∀ {Γ A} {M N : Γ ⊢ A}
        → M —→* N
        → Finished N
        ------------
        → Steps M

eval : ∀ {Γ A}
    → Gas
    → (M : Γ ⊢ A)
    -------------
    → Steps M
eval zero    M = steps (M ∎) out-of-gas
eval (suc x) M with progress M
... | done NM = steps (M ∎) (done NM)
... | step {M'} M—→M' with eval x M'
...     | steps M'—→*M'' fin = steps (M —→⟨ M—→M' ⟩ M'—→*M'') fin

-- eval 100 (ƛ (` zero))
-- eval 100 ((ƛ (` zero)) · (ƛ (` zero)))
-- eval 100 (ƛ (ƛ (` (suc zero))))
-- eval 100 (ƛ (ƛ (ƛ ((` (suc (suc zero)) · ` zero) · (` (suc zero) · ` zero)))))
-- eval 100 (((ƛ (ƛ (ƛ ((` (suc (suc zero)) · ` zero) · (` (suc zero) · ` zero))))) · (ƛ (ƛ (` (suc zero))))) · (ƛ (ƛ (` (suc zero)))))