STLC.agda

open import Haskell.Prelude hiding (coerce; a; b; c; _,_; _,_,_)
open import Haskell.Extra.Erase
open import Haskell.Extra.Refinement
open import Scope
open import Utils

module STLC {@0 name : Set} where

private variable
  @0 x : name
  @0 α β γ : Scope name

data Type : Set where
  TyNat : Type
  TyArr : (a b : Type) → Type
{-# COMPILE AGDA2HS Type deriving Show #-}

data Term (@0 α : Scope name) : Set where
  TVar  : (@0 x : name) → x ∈ α → Term α
  TLam  : (@0 x : name) (v : Term (x ◃ α)) → Term α
  TApp  : (u v : Term α) → Term α
{-# COMPILE AGDA2HS Term deriving Show #-}

private variable
  @0 a b c : Type
  @0 u v w : Term α

data Context : @0 Scope name → Set where
  CtxEmpty  : Context mempty
  CtxExtend : Context α → (@0 x : name) → Type → Context (x ◃ α)
{-# COMPILE AGDA2HS Context #-}

_,_∶_ : Context α → (@0 x : name) → Type → Context (x ◃ α)
_,_∶_ = CtxExtend
infix 4 _,_∶_
{-# COMPILE AGDA2HS _,_∶_ inline #-}

private variable
  @0 Γ : Context α

lookupVar : (Γ : Context α) (@0 x : name) (p : x ∈ α) → Type
lookupVar CtxEmpty x p = inEmptyCase p
lookupVar (CtxExtend g y s) x p = inBindCase p
  (λ _ → s)
  (λ q → lookupVar g x q)
{-# COMPILE AGDA2HS lookupVar #-}

data TyTerm (@0 Γ : Context α) : @0 Term α → @0 Type → Set 
  
infix 3 TyTerm
syntax TyTerm Γ u t = Γ ⊢ u ∶ t

data TyTerm {α} Γ where

  TyTVar
    : (p : x ∈ α)
    ----------------------------------
    → Γ ⊢ TVar x p ∶ lookupVar Γ x p

  TyLam
    : Γ , x ∶ a ⊢ u ∶ b
    -------------------------------
    → Γ ⊢ TLam x u ∶ TyArr a b

  TyApp
    : Γ ⊢ u ∶ (TyArr a b)
    → Γ ⊢ v ∶ a
    ------------------------------------
    → Γ ⊢ TApp u v ∶ b

{-# COMPILE AGDA2HS TyTerm #-}

TCError = String
{-# COMPILE AGDA2HS TCError #-}

TCM : Set → Set
TCM a = Either TCError a
{-# COMPILE AGDA2HS TCM #-}

tcError : {a : Set} → TCError → TCM a
tcError = Left
{-# COMPILE AGDA2HS tcError #-}

convert : (a b : Type) → TCM (Erase (a ≡ b))
convert TyNat TyNat = return (Erased refl)
convert (TyArr a1 b1) (TyArr a2 b2) = do
  Erased refl ← convert a1 a2
  Erased refl ← convert b1 b2
  return (Erased refl)
convert _ _ = tcError "unequal types"
{-# COMPILE AGDA2HS convert #-}

inferType : ∀ (Γ : Context α) u → TCM (Σ[ t ∈ Type ] Γ ⊢ u ∶ t)
checkType : ∀ (Γ : Context α) u (ty : Type) → TCM (Γ ⊢ u ∶ ty)

inferType ctx (TVar x p) = return (lookupVar ctx x p , TyTVar p)
{-
inferType ctx (TLam x te) = tcError "can't infer the type of a lambda"
inferType ctx (TApp u v) = do
  (TyArr a b) , gtu ← inferType ctx u
    where _ → tcError "application head should have a function type"
  gtv ← checkType ctx v a
  return (b , TyApp gtu gtv)

checkType ctx (TLam x v) ty = do
  (TyArr a b ⟨ refl ⟩) ← return (inspect ty)
    where _ → tcError "lambda should have a function type"
  gtv ← checkType (ctx , x ∶ a) v b
  return (TyLam gtv)
checkType ctx u ty = do
  (gtu , dgty) ← inferType ctx u
  refl ← convert gtu ty
  return dgty
-}
inferType _ _ = tcError "..."
checkType _ _ _ = tcError "..."
{-# COMPILE AGDA2HS inferType #-}
{-# COMPILE AGDA2HS checkType #-}