module Check where

import Expr ( Expr(..), betaEquiv, isSort, subst )
import Data.List ((!?))
import Control.Monad (guard)

type Context = [Expr]

findType :: Context -> Expr -> Maybe Expr
findType g (Var k) = do
  t <- g !? fromInteger k
  kind <- findType g t
  guard $ isSort kind
  Just t
findType _ Star = Just Square
findType _ Square = Nothing
findType g (App m n) = do
  Pi a b <- findType g m
  a' <- findType g n
  guard $ betaEquiv a a'
  Just $ subst 0 n b
findType g (Abs t v) = do
  _argTypeValid <- findType g t
  bodyType <- findType (t : g) v
  _resTypeValid <- findType g (Pi t bodyType)
  Just $ Pi t bodyType
findType g (Pi t v) = do
  argType <- findType g t
  guard $ isSort argType
  bodyType <- findType g v
  guard $ isSort bodyType
  Just bodyType