module WellTypedLam where

data Base : Set where

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

Val : TyCode → Set
Val ι         = Base
Val (σ ⇒ τ) = Val σ → Val τ  

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

data Env : Con → Set where
  e   : Env ε
  _::_ : ∀{Γ σ} → Env Γ → Val σ → Env (Γ < σ) 

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

data Lam : Con → TyCode → Set where
  var : ∀{Γ σ} → Var Γ σ → Lam Γ σ
  _$_ : ∀{Γ σ τ} → Lam Γ (σ ⇒ τ) → Lam Γ σ → Lam Γ τ
  lam : ∀{Γ σ τ} → Lam (Γ < σ) τ → Lam Γ (σ ⇒ τ)

lookup : ∀{Γ σ} → Env Γ → Var Γ σ → Val σ
lookup e         ()
lookup (γ :: v) z     = v
lookup (γ :: v) (s i) = lookup γ i

eval : ∀{Γ σ} → Lam Γ σ → Env Γ → Val σ
eval (var i) γ = lookup γ i
eval (t $ u) γ = eval t γ (eval u γ) 
eval (lam t) γ = λ v → eval t (γ :: v)