hoq-0.2: src/TypeChecking/Monad.hs
module TypeChecking.Monad
( EDocM, TCM, runTCM
, addFunctionCheck, addDataTypeCheck, addConstructorCheck
, 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
import Semantics
import Semantics.Value
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 (nameToString 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 -> Int -> Int -> SEval -> Closed (Type Semantics) -> TCM m ()
addConstructorCheck (pos, var) dt i n e ty = do
mf <- lift (getFunction var)
mc <- lift $ getConstructor var (Just dt)
if null mf && null mc then lift (addConstructor var dt i n e ty) else warn [multipleDeclaration pos var]