open import Relation.Binary
open import Relation.Binary.PropositionalEquality

module STLC.Typecheck {U : Set} (UEq : IsDecEquivalence {A = U} _≡_) where

open import STLC.Typing U
open import STLC.Bound Type
open import STLC.Embedded as E hiding (Expr; Ctxt)

open IsDecEquivalence UEq using (_≟_)

open import Data.Nat hiding (_≟_)
open import Data.Fin
open import Data.Vec
open import Function using (_∘_; _$_)
open import Data.Product
open import STLC.Utils
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

el-inj :  {A B}  el A  el B  A  B
el-inj refl = refl

arr-injˡ :  {τ τ′ τ₂ τ₂′}  τ  τ₂  τ′  τ₂′  τ  τ′
arr-injˡ refl = refl

arr-injʳ :  {τ τ′ τ″}  τ  τ′  τ  τ″  τ′  τ″
arr-injʳ refl = refl

_T≟_ : (τ τ′ : Type)  Dec (τ  τ′)
el A T≟ el B with A  B
el A T≟ el .A | yes refl = yes refl
el A T≟ el B | no A≢B = no (A≢B  el-inj)
el A T≟ (_  _) = no  ())
(τ₁  τ₂) T≟ el B = no  ())
(τ₁  τ₂) T≟ (τ₁′  τ₂′) with τ₁ T≟ τ₁′
(τ₁  τ₂) T≟ (τ₁′  τ₂′) | no ¬p = no (¬p  arr-injˡ)
(τ₁  τ₂) T≟ (.τ₁  τ₂′) | yes refl with τ₂ T≟ τ₂′
(τ₁  τ₂) T≟ (.τ₁  .τ₂) | yes refl | yes refl = yes refl
(τ₁  τ₂) T≟ (.τ₁  τ₂′) | yes refl | no ¬p = no (¬p  arr-injʳ)

⊢-inj :  {n Γ} {E : Expr n}   {τ τ′}  Γ  E  τ  Γ  E  τ′  τ  τ′
⊢-inj tVar tVar = refl
⊢-inj {E = lam τ E} (tLam t) (tLam t′) = cong (_↣_ τ) (⊢-inj t t′)
⊢-inj (t₁ · t₂) (t₁′ · t₂′) with ⊢-inj t₁ t₁′
⊢-inj (t₁ · t₂) (t₁′ · t₂′) | refl with ⊢-inj t₂ t₂′
⊢-inj (t₁ · t₂) (t₁′ · t₂′) | refl | refl = refl

lam-injˡ :  {n τ₁ τ₂ τ} {Γ : Ctxt n} {E : Expr (suc n)} 
           Γ  lam τ E  (τ₁  τ₂)  τ₁  τ
lam-injˡ (tLam t) = refl

mutual
  infer :  {n} Γ (E : Expr n)  Dec (∃[ τ ] Γ  E  τ)
  infer Γ (var x) = yes (lookup x Γ , tVar)
  infer Γ (lam τ E) with infer (τ  Γ) E
  infer Γ (lam τ E) | yes (τ′ , E∷τ′) = yes (τ  τ′ , tLam E∷τ′)
  infer Γ (lam τ E) | no ¬p = no lem
    where
    lem : ∄[ τ′ ] Γ  lam τ E  τ′
    lem (el A , ())
    lem (.τ  _ , tLam t) = ¬p (_ , t)
  infer Γ (E · F) with infer Γ E
  infer Γ (E · F) | yes (el A , t) = no lem
    where
    lem : ∄[ τ ] Γ  E · F  τ
    lem (_ , t₁ · _) with ⊢-inj t t₁
    lem (_ , t₁ · _) | ()
  infer Γ (E · F) | yes (τ₁  τ₂ , tE) with check Γ F τ₁
  infer Γ (E · F) | yes (τ₁  τ₂ , tE) | yes tF = yes (τ₂ , tE · tF)
  infer Γ (E · F) | yes (τ₁  τ₂ , tE) | no ¬p = no lem
    where
    lem : ∄[ τ ] Γ  E · F  τ
    lem (_ , t₁ · _) with ⊢-inj t₁ tE
    lem (.τ₂ , _ · t₂) | refl = ¬p t₂
  infer Γ (E · F) | no ¬p = no lem
    where
    lem : ∄[ τ ] Γ  E · F  τ
    lem (_ , t · _) = ¬p (_ , t)

  check :  {n} Γ (E : Expr n)   τ  Dec (Γ  E  τ)
  check Γ (var x) τ with lookup x Γ T≟ τ
  check Γ (var x) .(lookup x Γ) | yes refl = yes tVar
  check Γ (var x) τ | no ¬p = no (¬p  ⊢-inj tVar)
  check Γ (lam τ′ E) (el A) = no  ())
  check Γ (lam τ′ E) (τ₁  τ₂) with τ₁ T≟ τ′
  check Γ (lam τ′ E) (.τ′  τ₂) | yes refl with check (τ′  Γ) E τ₂
  check Γ (lam τ′ E) (.τ′  τ₂) | yes refl | yes t = yes (tLam t)
  check Γ (lam τ′ E) (.τ′  τ₂) | yes refl | no ¬p = no lem
    where
    lem : ¬ Γ  lam τ′ E  τ′  τ₂
    lem (tLam t) = ¬p t
  check Γ (lam τ′ E) (τ₁  τ₂) | no ¬p = no (¬p  lam-injˡ)
  check Γ (E · F) τ with infer Γ F
  check Γ (E · F) τ | yes (τ′ , F∷τ′) with check Γ E (τ′  τ)
  check Γ (E · F) τ | yes (τ′ , F∷τ′) | yes E∷τ′↣τ = yes (E∷τ′↣τ · F∷τ′)
  check Γ (E · F) τ | yes (τ′ , F∷τ′) | no ¬p = no lem
    where
    lem : ¬ Γ  E · F  τ
    lem (_·_ {τ = τ₀} t t′) with ⊢-inj F∷τ′ t′
    lem (t · t′) | refl = ¬p t
  check Γ (E · F) τ | no ¬tF = no lem
    where
    lem : ¬ Γ  E · F  τ
    lem (_·_ {τ = τ} t t′) = ¬tF (τ , t′)