module TypeChecking.Definitions
    ( typeCheckDefs
    ) where

import Data.Void

import Syntax
import Syntax.ErrorDoc
import TypeChecking.Expressions
import TypeChecking.Expressions.Utils
import TypeChecking.Definitions.Records
import TypeChecking.Definitions.DataTypes
import TypeChecking.Definitions.Functions
import TypeChecking.Monad

typeCheckDefs :: Monad m => [Def] -> TCM m ()
typeCheckDefs [] = return ()
typeCheckDefs (DefImport{} : defs) = typeCheckDefs defs
typeCheckDefs (DefFixity{} : defs) = typeCheckDefs defs
typeCheckDefs (DefType p@(pos, name) ty : defs) = case span (theSameAs name) defs of
    ([],_) -> do
        warn [Error Other $ emsgLC pos ("Missing a realization of function " ++ show (nameToString name)) enull]
        typeCheckDefs defs
    (defs1,defs2) -> do
        typeCheckFunction p ty (map (\d -> case d of
            DefFun (pos, _) pats expr -> (pos, pats, expr)
            _ -> error "typeCheckDefs") defs1)
            `catchError` \errs -> warn errs >> return ()
        typeCheckDefs defs2
typeCheckDefs (DefFun p@(pos, name) [] (Just expr) : defs) = do
    (term, ty) <- typeCheck expr Nothing
    addFunctionCheck p ([([], closed term)]) $ Closed (vacuous ty)
    typeCheckDefs defs
typeCheckDefs (DefFun (pos, name) [] Nothing : defs) = do
    warn [Error Other $ emsgLC pos "Expected right hand side" enull]
    typeCheckDefs $ dropWhile (theSameAs name) defs
typeCheckDefs (DefFun (pos, name) _ _ : defs) = do
    warn [inferErrorMsg pos "the argument"]
    typeCheckDefs $ dropWhile (theSameAs name) defs
typeCheckDefs (DefData dt ty cons conds : defs) = do
    typeCheckDataType dt ty cons conds
    typeCheckDefs defs
typeCheckDefs (DefRecord name params mcon fields conds : defs) = do
    typeCheckRecord name params mcon fields conds
    typeCheckDefs defs

theSameAs :: Name -> Def -> Bool
theSameAs name (DefFun (_, name') _ _) = name == name'
theSameAs _ _ = False