{-

    Interactive Programming with Dependent Types
    
                      Ulf Norell

                  ICFP 2013, Boston

 -}

module ICFP where

open import ICFPPrelude

data Type : Set where
  nat : Type
  _⇒_ : (a b : Type) → Type

infixr  _⇒_

data Raw : Set where
  var : (n : Nat) → Raw
  app : (e₁ e₂ : Raw) → Raw
  lam : (a : Type) (e : Raw) → Raw

data Cxt : Set where
  [] : Cxt
  _,_ : (Γ : Cxt) (a : Type) → Cxt

data Var : Cxt → Type → Set where
  zero : ∀ {Γ a} → Var (Γ , a) a
  suc  : ∀ {Γ a b} → Var Γ a → Var (Γ , b) a

data Term : Cxt → Type → Set where
  var : ∀ {Γ a} → Var Γ a → Term Γ a
  app : ∀ {Γ a b} (u : Term Γ (a ⇒ b)) (v : Term Γ a) →
        Term Γ b
  lam : ∀ {Γ} a {b} (u : Term (Γ , a) b) → Term Γ (a ⇒ b)

eraseVar : ∀ {Γ a} → Var Γ a → Nat
eraseVar zero = zero
eraseVar (suc x) = suc (eraseVar x)

erase : ∀ {Γ a} → Term Γ a → Raw
erase (var x) = var (eraseVar x)
erase (app v v₁) = app (erase v) (erase v₁)
erase (lam a v) = lam a (erase v)

data _≠_ : Type → Type → Set where
  nat≠fun : ∀ {a b} → nat ≠ a ⇒ b
  fun≠nat : ∀ {a b} → a ⇒ b ≠ nat
  src≠    : ∀ {a a′ b c} → a ≠ a′ → a ⇒ b ≠ a′ ⇒ c
  tgt≠    : ∀ {a b c c′} → c ≠ c′ → a ⇒ c ≠ b ⇒ c′

sound : ∀ a → a ≠ a → ⊥
sound nat ()
sound (a ⇒ b) (src≠ x) = sound a x
sound (a ⇒ b) (tgt≠ x) = sound b x

infix  _≠_ _≟_

data _≟_ : Type → Type → Set where
  equal : ∀ {a} → a ≟ a
  not-equal : ∀ {a b} → a ≠ b → a ≟ b

compareFun : ∀ {a b c d} → a ≟ b → c ≟ d → a ⇒ c ≟ b ⇒ d
compareFun equal equal = equal
compareFun equal (not-equal x) = not-equal (tgt≠ x)
compareFun (not-equal x) q = not-equal (src≠ x)

compare : ∀ a b → a ≟ b
compare nat nat = equal
compare nat (a ⇒ b) = not-equal nat≠fun
compare (a ⇒ b) nat = not-equal fun≠nat
compare (a ⇒ b) (a₁ ⇒ b₁) = compareFun (compare a a₁) (compare b b₁)

data OutOfScope : Cxt → Nat → Set where
  oops : ∀ {n} → OutOfScope [] n
  suc  : ∀ {Γ a n} → OutOfScope Γ n → OutOfScope (Γ , a) (suc n)

data WellScoped? : Cxt → Nat → Set where
  yes : ∀ {Γ} a (x : Var Γ a) → WellScoped? Γ (eraseVar x)
  no  : ∀ {Γ n} → OutOfScope Γ n → WellScoped? Γ n

data TypeError : Cxt → Raw → Set where
  arg-mismatch : ∀ {a a′ Γ b} {u : Term Γ (a ⇒ b)} {u₁ : Term Γ a′} →
                 a ≠ a′ → TypeError Γ (app (erase u) (erase u₁))
  not-fun : ∀ {Γ} {u : Term Γ nat} {a₁} {u₁ : Term Γ a₁} →
            TypeError Γ (app (erase u) (erase u₁))
  bad-arg : ∀ {Γ e₂ e₁} → TypeError Γ e₂ → TypeError Γ (app e₁ e₂)
  bad-fun : ∀ {Γ e₁ e₂} → TypeError Γ e₁ → TypeError Γ (app e₁ e₂)
  out-of-scope : ∀ {Γ n} → OutOfScope Γ n → TypeError Γ (var n)
  lam : ∀ {Γ e} a → TypeError (Γ , a) e → TypeError Γ (lam a e)

data WellTyped? : Cxt → Raw → Set where
  yes : ∀ {Γ} a (u : Term Γ a) → WellTyped? Γ (erase u)
  no  : ∀ {Γ e} (err : TypeError Γ e) → WellTyped? Γ e

checkApp : ∀ {Γ e₁ e₂} → WellTyped? Γ e₁ → WellTyped? Γ e₂ →
             WellTyped? Γ (app e₁ e₂)
checkApp (yes nat u) (yes a₁ u₁) = no not-fun
checkApp (yes (a ⇒ b) u) (yes a′ u₁) with compare a a′
checkApp (yes (a ⇒ b) u) (yes .a u₁) | equal         = yes b (app u u₁)
checkApp (yes (a ⇒ b) u) (yes a′ u₁) | not-equal err = no (arg-mismatch err)
checkApp (yes a u) (no err) = no (bad-arg err)
checkApp (no err) (yes a u) = no (bad-fun err)
checkApp (no err) (no err₁) = no (bad-arg err₁)

lookupSuc : ∀ {Γ a n} →
            WellScoped? Γ n → WellScoped? (Γ , a) (suc n)
lookupSuc (yes a₁ x) = yes a₁ (suc x)
lookupSuc (no x) = no (suc x)

lookupVar : ∀ Γ n → WellScoped? Γ n
lookupVar [] n = no oops
lookupVar (Γ , a) zero = yes a zero
lookupVar (Γ , a) (suc n) = lookupSuc (lookupVar Γ n)

checkVar : ∀ {Γ n} → WellScoped? Γ n → WellTyped? Γ (var n)
checkVar (yes a x) = yes a (var x)
checkVar (no x) = no (out-of-scope x)

checkLam : ∀ {Γ e} a → WellTyped? (Γ , a) e → WellTyped? Γ (lam a e)
checkLam a (yes a₁ u) = yes (a ⇒ a₁) (lam a u)
checkLam a (no err) = no (lam a err)

check : ∀ Γ e → WellTyped? Γ e
check Γ (var n) = checkVar (lookupVar Γ n)
check Γ (app e₁ e₂) = checkApp (check Γ e₁) (check Γ e₂)
check Γ (lam a e) = checkLam a (check (Γ , a) e)