module Application where
open import Data.Nat public
open import Data.Nat.Properties public
open import Data.String using (String) public
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; cong; sym; ≢-sym) public
Id : Set
Id = String
infixr 5 ƛ_⇒_
infixl 7 _·_
infix 9 `_
infixr 8 _⇒_
data Type : Set where
Int : Type
_⇒_ : Type → Type → Type
data Term : Set where
lit : ℕ → Term
`_ : Id → Term
ƛ_⇒_ : Id → Term → Term
_·_ : Term → Term → Term
infixl 5 _,_⦂_
data Context : Set where
∅ : Context
_,_⦂_ : Context → Id → Type → Context
infix 4 _∋_⦂_
data _∋_⦂_ : Context → Id → Type → Set where
Z : ∀ {Γ x A}
→ Γ , x ⦂ A ∋ x ⦂ A
S : ∀ {Γ x y A B}
→ x ≢ y
→ Γ ∋ x ⦂ A
→ Γ , y ⦂ B ∋ x ⦂ A
data AppContext : Set where
∅ : AppContext
_,,_ : AppContext → Type → AppContext
infix 3 _~_⊢_⇒_
data _~_⊢_⇒_ : Context → AppContext → Term → Type → Set where
⊢int : ∀ {Γ n}
→ Γ ~ ∅ ⊢ lit n ⇒ Int
⊢var : ∀ {Γ x A}
→ Γ ∋ x ⦂ A
→ Γ ~ ∅ ⊢ ` x ⇒ A
⊢lam : ∀ {Γ : Context} {Ψ : AppContext} {e x A B}
→ (Γ , x ⦂ A) ~ Ψ ⊢ e ⇒ B
→ Γ ~ (Ψ ,, A) ⊢ (ƛ x ⇒ e) ⇒ (A ⇒ B)
⊢app : ∀ {Γ Ψ e₁ e₂ A B}
→ Γ ~ ∅ ⊢ e₂ ⇒ A
→ Γ ~ Ψ ,, A ⊢ e₁ ⇒ (A ⇒ B)
→ Γ ~ Ψ ⊢ e₁ · e₂ ⇒ B
data Counter : Set where
Z : Counter
S : Counter → Counter
infix 4 _⊢d_#_⦂_
data _⊢d_#_⦂_ : Context → Counter → Term → Type → Set where
⊢d-int : ∀ {Γ i}
→ Γ ⊢d Z # (lit i) ⦂ Int
⊢d-var : ∀ {Γ x A}
→ Γ ∋ x ⦂ A
→ Γ ⊢d Z # ` x ⦂ A
⊢d-lam : ∀ {Γ e x A B n}
→ Γ , x ⦂ A ⊢d n # e ⦂ B
→ Γ ⊢d S n # (ƛ x ⇒ e) ⦂ A ⇒ B
⊢d-app : ∀ {Γ e₁ e₂ A B n}
→ Γ ⊢d (S n) # e₁ ⦂ A ⇒ B
→ Γ ⊢d Z # e₂ ⦂ A
→ Γ ⊢d n # e₁ · e₂ ⦂ B
data R : AppContext → Counter → Type → Set where
R-Z : ∀ {A} → R ∅ Z A
R-S : ∀ {Ψ n A B}
→ R Ψ n B
→ R (Ψ ,, A) (S n) (A ⇒ B)
complete : ∀ {Γ Ψ n e A}
→ Γ ~ Ψ ⊢ e ⇒ A
→ R Ψ n A
→ Γ ⊢d n # e ⦂ A
complete ⊢int R-Z = ⊢d-int
complete (⊢var x) R-Z = ⊢d-var x
complete (⊢lam ⊢e) (R-S r) = ⊢d-lam (complete ⊢e r)
complete (⊢app ⊢e ⊢e₁) r = ⊢d-app (complete ⊢e₁ (R-S r)) (complete ⊢e R-Z)
sound : ∀ {Γ Ψ n e A}
→ Γ ⊢d n # e ⦂ A
→ R Ψ n A
→ Γ ~ Ψ ⊢ e ⇒ A
sound ⊢d-int R-Z = ⊢int
sound (⊢d-var x) R-Z = ⊢var x
sound (⊢d-lam ⊢e) (R-S r) = ⊢lam (sound ⊢e r)
sound (⊢d-app ⊢e ⊢e₁) r = ⊢app (sound ⊢e₁ R-Z) (sound ⊢e (R-S r))