STLC.agda

module STLC (Atom : Set) (_≠_ : Atom → Atom → Set) where

open import Data.Empty
open import Data.Product as P hiding (_,_)
open import Data.List 
open import Function hiding (_∋_)

data ★ : Set where
  ι : ★
  _⊳_ : ★ → ★ → ★
infixr 15 _⊳_

data Term : Set where
  var  : Atom → Term
  ƛ_↦_ : Atom → Term → Term
  _⋅_  : Term → Term → Term
infix 7 ƛ_↦_
infix 6 _⋅_

_﹕_ : ∀ {A B : Set} → A → B → A × B
_﹕_ = P._,_
infix 5 _﹕_

Cx : Set
Cx = List (Term × ★)

_,_ : {A : Set} → List A → A → List A
_,_ = flip _∷_

data _∋_ : Cx → (Atom × ★) → Set where
  head : ∀ {Γ α x} → Γ , (var x ﹕ α) ∋ (x ﹕ α)
  tail : ∀ {Γ α β x y} → x ≠ y → Γ ∋ (x ﹕ α) → Γ , (var y ﹕ β) ∋ (x ﹕ α)


data _⊢_ : Cx → (Term × ★) → Set where
  VAR : ∀ {Γ α x}       → Γ ∋ (x ﹕ α) → Γ ⊢ (var x ﹕ α)
  LAM : ∀ {Γ α β x M}   → Γ , (var x ﹕ α) ⊢ (M ﹕ β) → Γ ⊢ (ƛ x ↦ M ﹕ α ⊳ β)
  APP : ∀ {Γ α β f x y} → Γ ⊢ (f ﹕ α ⊳ β) → Γ ⊢ (x ﹕ α) → Γ ⊢ (y ﹕ β)
infix 1 _⊢_ _∋_