packages feed

hoq-0.3: src/TypeChecking/Monad.hs

module TypeChecking.Monad
    ( EDocM, TCM, runTCM
    , addFunctionCheck, addDataTypeCheck
    , addConstructorCheck, addFieldCheck
    , module TypeChecking.Monad.Warn
    , module TypeChecking.Monad.Scope
    , lift
    ) where

import Control.Monad
import Control.Monad.Trans(lift)

import TypeChecking.Expressions.Utils
import TypeChecking.Monad.Warn
import TypeChecking.Monad.Scope
import Syntax hiding (Clause)
import Semantics
import Semantics.Value
import Semantics.Pattern
import Syntax.ErrorDoc

type EDocM = WarnT [Error]
type TCM m = EDocM (ScopeT m)

runTCM :: Monad m => TCM m a -> m (Maybe a)
runTCM = liftM snd . runScopeT . runWarnT

multipleDeclaration :: Posn -> Name -> Error
multipleDeclaration pos var = Error Other $ emsgLC pos ("Multiple declarations of " ++ show (nameToPrefix var)) enull

addFunctionCheck :: Monad m => PName -> SEval -> Closed (Type Semantics) -> TCM m ID
addFunctionCheck (pos, var) e ty = do
    mr <- lift (getEntry var Nothing)
    if null mr then lift (addFunction var e ty) else throwError [multipleDeclaration pos var]

addDataTypeCheck :: Monad m => PName -> Int -> Closed (Type Semantics) -> TCM m ID
addDataTypeCheck (pos, var) n ty = do
    mf <- lift (getFunction var)
    md <- lift (getDataType var)
    if null mf && null md then lift (addDataType var n ty) else throwError [multipleDeclaration pos var]

addConstructorCheck :: Monad m => PName -> (ID, Name) -> Int -> [ClauseInCtx] -> [[ClauseInCtx]] -> Closed (Type Semantics) -> TCM m ()
addConstructorCheck (pos, var) dt i e es ty = do
    mf <- lift (getFunction var)
    mc <- lift $ getConstructor var $ Just (fst dt, [])
    if null mf && null mc then lift (addConstructor var dt i e es ty) else warn [multipleDeclaration pos var]

addFieldCheck :: Monad m => PIdent -> ID -> Int -> SEval -> Closed (Type Semantics) -> TCM m ()
addFieldCheck (PIdent pos fn) dtID ind e ty = do
    mind <- lift (getField fn dtID)
    case mind of
        Nothing -> lift (addField fn dtID ind e ty)
        Just{} -> warn [multipleDeclaration pos $ Ident fn]