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 7 _⇒_

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 4 _≠_ _≟_

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)