module WellTypedComb where

data Base : Set where

data TyCode : Set where
  ι : TyCode
  _⇒_ : TyCode → TyCode → TyCode

infixr 10 _⇒_

data Con : Set where
  ε : Con
  _<_ : Con → TyCode → Con

data Var : Con → TyCode → Set where
  z : ∀{Γ σ} → Var (Γ < σ) σ
  s : ∀{Γ σ τ} → Var Γ τ → Var (Γ < σ) τ

data Comb : Con → TyCode → Set where
  var : ∀{Γ σ} → Var Γ σ → Comb Γ σ
  _$_ : ∀{Γ σ τ} → Comb Γ (σ ⇒ τ) → Comb Γ σ → Comb Γ τ
  K   : ∀{Γ σ τ} → Comb Γ (σ ⇒ τ ⇒ σ)
  S   : ∀{Γ σ τ ρ} → Comb Γ ((σ ⇒ τ ⇒ ρ) ⇒ (σ ⇒ τ) ⇒ σ ⇒ ρ)

infixl 10 _$_

I : ∀{Γ σ} → Comb Γ (σ ⇒ σ)
I {Γ}{σ} = S $ K $ K {τ = σ}

weak : ∀{Γ σ τ} → Comb Γ τ → Comb (Γ < σ) τ
weak (var i) = var (s i)
weak (t $ u) = weak t $ weak u
weak K       = K
weak S       = S

lamvar : ∀{Γ σ τ} → Var (Γ < σ) τ → Comb Γ (σ ⇒ τ)
lamvar z         = I
lamvar (s z)     = K $ var z
lamvar (s (s i)) = weak (lamvar (s i)) 

lam : ∀{Γ σ τ} → Comb (Γ < σ) τ → Comb Γ (σ ⇒ τ)
lam (var i) = lamvar i
lam (t $ u) = S $ lam t $ lam u
lam K       = K $ K
lam S       = K $ S