module TypeChecker where

open import Data.List
open import Data.Nat

-- Exercise: Add negative feedback to the type checker.

-- TeX mode for ∈ is \in
data _∈_ {A : Set}(x : A) : List A -> Set where
  hd : forall {xs}   -> x ∈ x :: xs
  tl : forall {y xs} -> x ∈ xs -> x ∈ y :: xs

index : forall {A}{x : A}{xs} -> x ∈ xs -> Nat
index hd     = zero
index (tl p) = suc (index p)

data Lookup {A : Set}(xs : List A) : Nat -> Set where
  inside  : (x : A)(p : x ∈ xs) -> Lookup xs (index p)
  outside : (m : Nat) -> Lookup xs (length xs + m)

_!_ : {A : Set}(xs : List A)(n : Nat) -> Lookup xs n
[] ! n = outside n
(x :: xs) ! zero  = inside x hd
(x :: xs) ! suc n with xs ! n
(x :: xs) ! suc .(index p)       | inside y p = inside y (tl p)
(x :: xs) ! suc .(length xs + n) | outside n  = outside n

infixr 30 _→_
data Type : Set where
  ι   : Type                  -- TeX mode: \iota
  _→_ : Type -> Type -> Type  -- TeX mode: \to

data _≠_ : Type -> Type -> Set where
  -- TODO: look at _=?=_ for hints

data Equal? : Type -> Type -> Set where
  yes : forall {τ} -> Equal? τ τ
  no  : forall {σ τ} -> σ ≠ τ -> Equal? σ τ

_=?=_ : (σ τ : Type) -> Equal? σ τ
ι         =?= ι       = yes
ι         =?= (σ → τ) = no {! !}
(σ → τ)   =?= ι       = no {! !}
(σ₁ → τ₁) =?= (σ₂ → τ₂) with σ₁ =?= σ₂ | τ₁ =?= τ₂
(σ → τ)   =?= (.σ → .τ) | yes  | yes  = yes
(σ → τ₁)  =?= (.σ → τ₂) | yes  | no p = no {! !}
(σ₁ → τ₁) =?= (σ₂ → τ₂) | no p | _    = no {! !}

infixl 80 _$_
data Raw : Set where
  var : Nat -> Raw
  _$_ : Raw -> Raw -> Raw
  lam : Type -> Raw -> Raw

Cxt = List Type

data Term (Γ : Cxt) : Type -> Set where
  var : forall {τ} -> τ ∈ Γ -> Term Γ τ
  _$_ : forall {σ τ} -> Term Γ (σ → τ) -> Term Γ σ -> Term Γ τ
  lam : forall σ {τ} -> Term (σ :: Γ) τ -> Term Γ (σ → τ)

erase : forall {Γ τ} -> Term Γ τ -> Raw
erase (var x)   = var (index x)
erase (t $ u)   = erase t $ erase u
erase (lam σ t) = lam σ (erase t)

data BadTerm (Γ : Cxt) : Set where
  -- TODO: look at the definition of infer for
  -- clues as to which constructors you need.

eraseBad : {Γ : Cxt} -> BadTerm Γ -> Raw
eraseBad b = {! !}

data Infer (Γ : Cxt) : Raw -> Set where
  ok  : (τ : Type)(t : Term Γ τ) -> Infer Γ (erase t)
  bad : (b : BadTerm Γ) -> Infer Γ (eraseBad b)

infer : (Γ : Cxt)(e : Raw) -> Infer Γ e

infer Γ (var n)   with Γ ! n
infer Γ (var .(length Γ + n)) | outside n  = {! bad ? !}
infer Γ (var .(index x))      | inside σ x = ok σ (var x)

infer Γ (e₁ $ e₂)
  with infer Γ e₁
infer Γ (.(eraseBad b) $ e₂) | bad b   = {! bad ? !}
infer Γ (.(erase t₁) $ e₂)   | ok ι t₁ = {! bad ? !}
infer Γ (.(erase t₁) $ e₂)   | ok (σ → τ) t₁
  with infer Γ e₂
infer Γ (.(erase t₁) $ .(eraseBad b)) | ok (σ → τ) t₁ | bad b = {! bad ? !}
infer Γ (.(erase t₁) $ .(erase t₂))   | ok (σ → τ) t₁ | ok σ' t₂
  with σ =?= σ'
infer Γ (.(erase t₁) $ .(erase t₂))
  | ok (σ → τ) t₁ | ok .σ t₂ | yes = ok τ (t₁ $ t₂)
infer Γ (.(erase t₁) $ .(erase t₂))
  | ok (σ → τ) t₁ | ok σ' t₂ | no p = {! bad ? !}

infer Γ (lam σ e) with infer (σ :: Γ) e
infer Γ (lam σ .(erase t))    | ok τ t  = ok (σ → τ) (lam σ t)
infer Γ (lam σ .(eraseBad b)) | bad b   = {! bad ? !}