module Agda.TypeChecking.Monad.Base where
import Control.Exception as E
import Control.Monad.Error
import Control.Monad.State
import Control.Monad.Reader
import Control.Applicative
import Data.Map as Map
import Data.Set as Set
import Data.Generics
import Data.Foldable
import Data.Traversable
import System.Time
import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Concrete.Definitions as D
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Internal
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.Interaction.Exceptions
import Agda.Interaction.FindFile
import Agda.Interaction.Options
import qualified Agda.Interaction.Highlighting.Range as R
import Agda.Interaction.Highlighting.Precise (HighlightingInfo)
import Agda.Utils.FileName
import Agda.Utils.Fresh
import Agda.Utils.Monad
import Agda.Utils.Trace
#include "../../undefined.h"
import Agda.Utils.Impossible
data TCState =
TCSt { stFreshThings :: FreshThings
, stMetaStore :: MetaStore
, stInteractionPoints :: InteractionPoints
, stConstraints :: Constraints
, stSignature :: Signature
, stImports :: Signature
, stImportedModules :: Set ModuleName
, stModuleToSource :: ModuleToSource
, stVisitedModules :: VisitedModules
, stDecodedModules :: DecodedModules
, stCurrentModule :: Maybe ModuleName
, stScope :: ScopeInfo
, stPersistentOptions :: CommandLineOptions
, stPragmaOptions :: CommandLineOptions
, stStatistics :: Statistics
, stTrace :: CallTrace
, stMutualBlocks :: Map MutualId (Set QName)
, stLocalBuiltins :: BuiltinThings PrimFun
, stImportedBuiltins :: BuiltinThings PrimFun
, stHaskellImports :: Set String
}
data FreshThings =
Fresh { fMeta :: MetaId
, fInteraction :: InteractionId
, fMutual :: MutualId
, fName :: NameId
, fCtx :: CtxId
, fInteger :: Integer
}
deriving (Show)
initState :: TCState
initState =
TCSt { stFreshThings = Fresh 0 0 0 (NameId 0 0) 0 0
, stMetaStore = Map.empty
, stInteractionPoints = Map.empty
, stConstraints = []
, stSignature = emptySignature
, stImports = emptySignature
, stImportedModules = Set.empty
, stModuleToSource = Map.empty
, stVisitedModules = Map.empty
, stDecodedModules = Map.empty
, stCurrentModule = Nothing
, stScope = emptyScopeInfo
, stPersistentOptions = defaultOptions
, stPragmaOptions = defaultOptions
, stStatistics = Map.empty
, stTrace = noTrace
, stMutualBlocks = Map.empty
, stLocalBuiltins = Map.empty
, stImportedBuiltins = Map.empty
, stHaskellImports = Set.empty
}
stBuiltinThings :: TCState -> BuiltinThings PrimFun
stBuiltinThings s = stLocalBuiltins s `Map.union` stImportedBuiltins s
instance HasFresh MetaId FreshThings where
nextFresh s = (i, s { fMeta = i + 1 })
where
i = fMeta s
instance HasFresh MutualId FreshThings where
nextFresh s = (i, s { fMutual = i + 1 })
where
i = fMutual s
instance HasFresh InteractionId FreshThings where
nextFresh s = (i, s { fInteraction = i + 1 })
where
i = fInteraction s
instance HasFresh NameId FreshThings where
nextFresh s = (i, s { fName = succ i })
where
i = fName s
instance HasFresh CtxId FreshThings where
nextFresh s = (i, s { fCtx = succ i })
where
i = fCtx s
instance HasFresh Integer FreshThings where
nextFresh s = (i, s { fInteger = succ i })
where
i = fInteger s
instance HasFresh i FreshThings => HasFresh i TCState where
nextFresh s = (i, s { stFreshThings = f })
where
(i,f) = nextFresh $ stFreshThings s
data ModuleInfo = ModuleInfo
{ miInterface :: Interface
, miWarnings :: Bool
, miTimeStamp :: ClockTime
}
type VisitedModules = Map C.TopLevelModuleName ModuleInfo
type DecodedModules = Map C.TopLevelModuleName (Interface, ClockTime)
data Interface = Interface
{ iImportedModules :: [ModuleName]
, iModuleName :: ModuleName
, iScope :: Map ModuleName Scope
, iInsideScope :: ScopeInfo
, iSignature :: Signature
, iBuiltin :: BuiltinThings String
, iHaskellImports :: Set String
, iHighlighting :: HighlightingInfo
}
deriving (Typeable, Data, Show)
data Closure a = Closure { clSignature :: Signature
, clEnv :: TCEnv
, clScope :: ScopeInfo
, clTrace :: CallTrace
, clValue :: a
}
deriving (Typeable, Data)
instance Show a => Show (Closure a) where
show cl = "Closure " ++ show (clValue cl)
instance HasRange a => HasRange (Closure a) where
getRange = getRange . clValue
buildClosure :: MonadTCM tcm => a -> tcm (Closure a)
buildClosure x = liftTCM $ do
env <- ask
sig <- gets stSignature
scope <- gets stScope
trace <- gets stTrace
return $ Closure sig env scope trace x
type ConstraintClosure = Closure Constraint
data Constraint = ValueCmp Comparison Type Term Term
| TypeCmp Comparison Type Type
| TelCmp Comparison Telescope Telescope
| SortCmp Comparison Sort Sort
| UnBlock MetaId
| Guarded Constraint Constraints
| IsEmpty Type
deriving (Typeable, Show)
data Comparison = CmpEq | CmpLeq
deriving (Eq, Typeable, Show)
type Constraints = [ConstraintClosure]
data Open a = OpenThing [CtxId] a
deriving (Typeable, Data, Show)
data Judgement t a
= HasType a t
| IsSort a
deriving (Typeable, Data)
instance (Show t, Show a) => Show (Judgement t a) where
show (HasType a t) = show a ++ " : " ++ show t
show (IsSort a) = show a ++ " sort"
instance Functor (Judgement t) where
fmap f (HasType x t) = HasType (f x) t
fmap f (IsSort x) = IsSort (f x)
instance Foldable (Judgement t) where
foldr f z (HasType x _) = f x z
foldr f z (IsSort x) = f x z
instance Traversable (Judgement t) where
traverse f (HasType x t) = flip HasType t <$> f x
traverse f (IsSort x) = IsSort <$> f x
data MetaVariable =
MetaVar { mvInfo :: MetaInfo
, mvPriority :: MetaPriority
, mvJudgement :: Judgement Type MetaId
, mvInstantiation :: MetaInstantiation
, mvListeners :: Set MetaId
}
deriving (Typeable)
data MetaInstantiation
= InstV Term
| InstS Term
| Open
| BlockedConst Term
| PostponedTypeCheckingProblem (Closure (A.Expr, Type, TCM Bool))
deriving (Typeable)
instance Show MetaInstantiation where
show (InstV t) = "InstV (" ++ show t ++ ")"
show (InstS s) = "InstS (" ++ show s ++ ")"
show Open = "Open"
show (BlockedConst t) = "BlockedConst (" ++ show t ++ ")"
show (PostponedTypeCheckingProblem{}) = "PostponedTypeCheckingProblem (...)"
newtype MetaPriority = MetaPriority Int
deriving (Eq, Ord, Show)
type MetaInfo = Closure Range
type MetaStore = Map MetaId MetaVariable
instance HasRange MetaVariable where
getRange m = getRange $ getMetaInfo m
instance SetRange MetaVariable where
setRange r (MetaVar mi p j inst ls) = MetaVar (mi {clValue = r}) p j inst ls
normalMetaPriority :: MetaPriority
normalMetaPriority = MetaPriority 0
lowMetaPriority :: MetaPriority
lowMetaPriority = MetaPriority (10)
highMetaPriority :: MetaPriority
highMetaPriority = MetaPriority 10
getMetaInfo :: MetaVariable -> MetaInfo
getMetaInfo = mvInfo
getMetaScope :: MetaVariable -> ScopeInfo
getMetaScope m = clScope $ getMetaInfo m
getMetaEnv :: MetaVariable -> TCEnv
getMetaEnv m = clEnv $ getMetaInfo m
getMetaSig :: MetaVariable -> Signature
getMetaSig m = clSignature $ getMetaInfo m
type InteractionPoints = Map InteractionId MetaId
newtype InteractionId = InteractionId Nat
deriving (Eq,Ord,Num,Integral,Real,Enum)
instance Show InteractionId where
show (InteractionId x) = "?" ++ show x
data Signature = Sig
{ sigSections :: Sections
, sigDefinitions :: Definitions
}
deriving (Typeable, Data, Show)
type Sections = Map ModuleName Section
type Definitions = Map QName Definition
data Section = Section
{ secTelescope :: Telescope
, secFreeVars :: Nat
}
deriving (Typeable, Data, Show)
emptySignature :: Signature
emptySignature = Sig Map.empty Map.empty
data DisplayForm = Display Nat [Term] DisplayTerm
deriving (Typeable, Data, Show)
data DisplayTerm = DWithApp [DisplayTerm] Args
| DTerm Term
deriving (Typeable, Data, Show)
defaultDisplayForm :: QName -> [Open DisplayForm]
defaultDisplayForm c = []
data Definition = Defn { defName :: QName
, defType :: Type
, defDisplay :: [Open DisplayForm]
, defMutual :: MutualId
, theDef :: Defn
}
deriving (Typeable, Data, Show)
type HaskellCode = String
type HaskellType = String
data HaskellRepresentation
= HsDefn HaskellType HaskellCode
| HsType HaskellType
deriving (Typeable, Data, Show)
data Polarity = Covariant | Contravariant | Invariant
deriving (Typeable, Data, Show, Eq)
data Occurrence = Positive | Negative | Unused
deriving (Typeable, Data, Show, Eq, Ord)
data Defn = Axiom
{ axHsDef :: Maybe HaskellRepresentation
}
| Function
{ funClauses :: [Clause]
, funInv :: FunctionInverse
, funPolarity :: [Polarity]
, funArgOccurrences :: [Occurrence]
, funAbstr :: IsAbstract
, funDelayed :: Delayed
}
| Datatype
{ dataPars :: Nat
, dataIxs :: Nat
, dataInduction :: Induction
, dataClause :: (Maybe Clause)
, dataCons :: [QName]
, dataSort :: Sort
, dataPolarity :: [Polarity]
, dataArgOccurrences :: [Occurrence]
, dataHsType :: Maybe HaskellType
, dataAbstr :: IsAbstract
}
| Record
{ recPars :: Nat
, recClause :: Maybe Clause
, recCon :: Maybe QName
, recConType :: Type
, recFields :: [(Hiding, A.QName)]
, recTel :: Telescope
, recPolarity :: [Polarity]
, recArgOccurrences :: [Occurrence]
, recAbstr :: IsAbstract
}
| Constructor
{ conPars :: Nat
, conSrcCon :: QName
, conData :: QName
, conHsCode :: Maybe (HaskellType, HaskellCode)
, conAbstr :: IsAbstract
, conInd :: Induction
}
| Primitive
{ primAbstr :: IsAbstract
, primName :: String
, primClauses :: Maybe [Clause]
}
deriving (Typeable, Data, Show)
newtype Fields = Fields [(C.Name, Type)]
deriving (Typeable, Data)
data Reduced no yes = NoReduction no | YesReduction yes
deriving (Typeable)
data PrimFun = PrimFun
{ primFunName :: QName
, primFunArity :: Arity
, primFunImplementation :: MonadTCM tcm => [Arg Term] -> tcm (Reduced [Arg Term] Term)
}
deriving (Typeable)
defClauses :: Definition -> [Clause]
defClauses Defn{theDef = Function{funClauses = cs}} = cs
defClauses Defn{theDef = Primitive{primClauses = Just cs}} = cs
defClauses Defn{theDef = Datatype{dataClause = Just c}} = [c]
defClauses Defn{theDef = Record{recClause = Just c}} = [c]
defClauses _ = []
data Delayed = Delayed | NotDelayed
deriving (Typeable, Data, Show, Eq)
defDelayed :: Definition -> Delayed
defDelayed Defn{theDef = Function{funDelayed = d}} = d
defDelayed _ = NotDelayed
defAbstract :: Definition -> IsAbstract
defAbstract d = case theDef d of
Axiom{} -> AbstractDef
Function{funAbstr = a} -> a
Datatype{dataAbstr = a} -> a
Record{recAbstr = a} -> a
Constructor{conAbstr = a} -> a
Primitive{primAbstr = a} -> a
data FunctionInverse = NotInjective
| Inverse (Map TermHead Clause)
deriving (Typeable, Data, Show)
data TermHead = SortHead
| PiHead
| ConHead QName
deriving (Typeable, Data, Eq, Ord, Show)
newtype MutualId = MutId Int
deriving (Typeable, Data, Eq, Ord, Show, Num)
type Statistics = Map String Int
type CallTrace = Trace (Closure Call)
noTrace :: CallTrace
noTrace = TopLevel []
data Call = CheckClause Type A.Clause (Maybe Clause)
| forall a. CheckPattern A.Pattern Telescope Type (Maybe a)
| CheckLetBinding A.LetBinding (Maybe ())
| InferExpr A.Expr (Maybe (Term, Type))
| CheckExpr A.Expr Type (Maybe Term)
| CheckDotPattern A.Expr Term (Maybe Constraints)
| CheckPatternShadowing A.Clause (Maybe ())
| IsTypeCall A.Expr Sort (Maybe Type)
| IsType_ A.Expr (Maybe Type)
| InferVar Name (Maybe (Term, Type))
| InferDef Range QName (Maybe (Term, Type))
| CheckArguments Range [NamedArg A.Expr] Type Type (Maybe (Args, Type, Constraints))
| CheckDataDef Range Name [A.LamBinding] [A.Constructor] (Maybe ())
| CheckRecDef Range Name [A.LamBinding] [A.Constructor] (Maybe ())
| CheckConstructor QName Telescope Sort A.Constructor (Maybe ())
| CheckFunDef Range Name [A.Clause] (Maybe ())
| CheckPragma Range A.Pragma (Maybe ())
| CheckPrimitive Range Name A.Expr (Maybe ())
| CheckSectionApplication Range ModuleName A.Telescope ModuleName [NamedArg A.Expr] (Maybe ())
| ScopeCheckExpr C.Expr (Maybe A.Expr)
| ScopeCheckDeclaration D.NiceDeclaration (Maybe [A.Declaration])
| ScopeCheckLHS C.Name C.Pattern (Maybe A.LHS)
| ScopeCheckDefinition D.NiceDefinition (Maybe A.Definition)
| forall a. TermFunDef Range Name [A.Clause] (Maybe a)
| forall a. SetRange Range (Maybe a)
deriving (Typeable)
instance Data Call where
dataTypeOf _ = mkDataType "Call" []
toConstr x = mkConstr (dataTypeOf x) "Dummy" [] Prefix
gunfold k z _ = __IMPOSSIBLE__
instance HasRange a => HasRange (Trace a) where
getRange (TopLevel _) = noRange
getRange (Current c par _ _)
| r == noRange = getRange par
| otherwise = r
where r = getRange c
instance HasRange a => HasRange (ParentCall a) where
getRange NoParent = noRange
getRange (Parent c par _)
| r == noRange = getRange par
| otherwise = r
where r = getRange c
instance HasRange Call where
getRange (CheckClause _ c _) = getRange c
getRange (CheckPattern p _ _ _) = getRange p
getRange (InferExpr e _) = getRange e
getRange (CheckExpr e _ _) = getRange e
getRange (CheckLetBinding b _) = getRange b
getRange (IsTypeCall e s _) = getRange e
getRange (IsType_ e _) = getRange e
getRange (InferVar x _) = getRange x
getRange (InferDef _ f _) = getRange f
getRange (CheckArguments r _ _ _ _) = r
getRange (CheckDataDef i _ _ _ _) = getRange i
getRange (CheckRecDef i _ _ _ _) = getRange i
getRange (CheckConstructor _ _ _ c _) = getRange c
getRange (CheckFunDef i _ _ _) = getRange i
getRange (CheckPragma r _ _) = r
getRange (CheckPrimitive i _ _ _) = getRange i
getRange (ScopeCheckExpr e _) = getRange e
getRange (ScopeCheckDeclaration d _) = getRange d
getRange (ScopeCheckLHS _ p _) = getRange p
getRange (ScopeCheckDefinition d _) = getRange d
getRange (CheckDotPattern e _ _) = getRange e
getRange (CheckPatternShadowing c _) = getRange c
getRange (TermFunDef i _ _ _) = getRange i
getRange (SetRange r _) = r
getRange (CheckSectionApplication r _ _ _ _ _) = r
type BuiltinThings pf = Map String (Builtin pf)
data Builtin pf
= Builtin Term
| Prim pf
deriving (Typeable, Data, Show)
instance Functor Builtin where
fmap f (Builtin t) = Builtin t
fmap f (Prim x) = Prim $ f x
instance Foldable Builtin where
foldr f z (Builtin t) = z
foldr f z (Prim x) = f x z
instance Traversable Builtin where
traverse f (Builtin t) = pure $ Builtin t
traverse f (Prim x) = Prim <$> f x
data TCEnv =
TCEnv { envContext :: Context
, envLetBindings :: LetBindings
, envCurrentModule :: ModuleName
, envAnonymousModules :: [(ModuleName, Nat)]
, envImportPath :: [C.TopLevelModuleName]
, envMutualBlock :: Maybe MutualId
, envAbstractMode :: AbstractMode
, envReplace :: Bool
, envDisplayFormsEnabled :: Bool
, envReifyInteractionPoints :: Bool
}
deriving (Typeable, Data)
initEnv :: TCEnv
initEnv = TCEnv { envContext = []
, envLetBindings = Map.empty
, envCurrentModule = noModuleName
, envAnonymousModules = []
, envImportPath = []
, envMutualBlock = Nothing
, envAbstractMode = AbstractMode
, envReplace = True
, envDisplayFormsEnabled = True
, envReifyInteractionPoints = True
}
type Context = [ContextEntry]
data ContextEntry = Ctx { ctxId :: CtxId
, ctxEntry :: Arg (Name, Type)
}
deriving (Typeable, Data)
newtype CtxId = CtxId Nat
deriving (Typeable, Data, Eq, Ord, Show, Enum, Real, Integral, Num)
type LetBindings = Map Name (Open (Term, Type))
data AbstractMode = AbstractMode
| ConcreteMode
| IgnoreAbstractMode
deriving (Typeable, Data)
data Occ = OccCon { occDatatype :: QName
, occConstructor :: QName
, occPosition :: OccPos
}
| OccClause { occFunction :: QName
, occClause :: Int
, occPosition :: OccPos
}
data OccPos = NonPositively | ArgumentTo Nat QName
data TypeError
= InternalError String
| NotImplemented String
| NotSupported String
| CompilationError String
| TerminationCheckFailed [([QName], [R.Range])]
| PropMustBeSingleton
| DataMustEndInSort Term
| ShouldEndInApplicationOfTheDatatype Type
| ShouldBeAppliedToTheDatatypeParameters Term Term
| ShouldBeApplicationOf Type QName
| ConstructorPatternInWrongDatatype QName QName
| DoesNotConstructAnElementOf QName Term
| DifferentArities
| WrongHidingInLHS Type
| WrongHidingInLambda Type
| WrongHidingInApplication Type
| DependentPatternMatchingOnCodata
| NotInductive Term
| UninstantiatedDotPattern A.Expr
| IlltypedPattern A.Pattern Type
| TooManyArgumentsInLHS Nat Type
| WrongNumberOfConstructorArguments QName Nat Nat
| ShouldBeEmpty Type [Pattern]
| ShouldBeASort Type
| ShouldBePi Type
| ShouldBeRecordType Type
| NotAProperTerm
| UnequalTerms Comparison Term Term Type
| UnequalTypes Comparison Type Type
| UnequalTelescopes Comparison Telescope Telescope
| UnequalHiding Type Type
| UnequalSorts Sort Sort
| NotLeqSort Sort Sort
| MetaCannotDependOn MetaId [Nat] Nat
| MetaOccursInItself MetaId
| GenericError String
| BuiltinMustBeConstructor String A.Expr
| NoSuchBuiltinName String
| DuplicateBuiltinBinding String Term Term
| NoBindingForBuiltin String
| NoSuchPrimitiveFunction String
| ShadowedModule [A.ModuleName]
| BuiltinInParameterisedModule String
| NoRHSRequiresAbsurdPattern [NamedArg A.Pattern]
| AbsurdPatternRequiresNoRHS [NamedArg A.Pattern]
| TooFewFields QName [C.Name]
| TooManyFields QName [C.Name]
| DuplicateFields [C.Name]
| DuplicateConstructors [C.Name]
| UnexpectedWithPatterns [A.Pattern]
| WithClausePatternMismatch A.Pattern Pattern
| FieldOutsideRecord
| ModuleArityMismatch A.ModuleName Telescope [NamedArg A.Expr]
| IncompletePatternMatching Term Args
| CoverageFailure QName [[Arg Pattern]]
| UnreachableClauses QName [[Arg Pattern]]
| CoverageCantSplitOn QName
| CoverageCantSplitType Type
| NotStrictlyPositive QName [Occ]
| LocalVsImportedModuleClash ModuleName
| UnsolvedMetas [Range]
| UnsolvedConstraints Constraints
| CyclicModuleDependency [C.TopLevelModuleName]
| FileNotFound C.TopLevelModuleName [AbsolutePath]
| OverlappingProjects AbsolutePath C.TopLevelModuleName C.TopLevelModuleName
| AmbiguousTopLevelModuleName C.TopLevelModuleName [AbsolutePath]
| ModuleNameDoesntMatchFileName C.TopLevelModuleName [AbsolutePath]
| ClashingFileNamesFor ModuleName [AbsolutePath]
| ModuleDefinedInOtherFile C.TopLevelModuleName AbsolutePath AbsolutePath
| BothWithAndRHS
| NotInScope [C.QName]
| NoSuchModule C.QName
| AmbiguousName C.QName [A.QName]
| AmbiguousModule C.QName [A.ModuleName]
| UninstantiatedModule C.QName
| ClashingDefinition C.QName A.QName
| ClashingModule A.ModuleName A.ModuleName
| ClashingImport C.Name A.QName
| ClashingModuleImport C.Name A.ModuleName
| PatternShadowsConstructor A.Name A.QName
| ModuleDoesntExport C.QName [C.ImportedName]
| InvalidPattern C.Pattern
| RepeatedVariablesInPattern [C.Name]
| NotAModuleExpr C.Expr
| NotAnExpression C.Expr
| NotAValidLetBinding D.NiceDeclaration
| NothingAppliedToHiddenArg C.Expr
| NoParseForApplication [C.Expr]
| AmbiguousParseForApplication [C.Expr] [C.Expr]
| NoParseForLHS C.Pattern
| AmbiguousParseForLHS C.Pattern [C.Pattern]
deriving (Typeable)
instance Show TypeError where
show _ = "<TypeError>"
instance Error TypeError where
noMsg = strMsg ""
strMsg = GenericError
data TCErr' = TypeError TCState (Closure TypeError)
| Exception Range String
| IOException Range E.IOException
| PatternErr TCState
| AbortAssign TCState
deriving (Typeable)
data TCErr =
TCErr { errHighlighting :: Maybe (HighlightingInfo, ModuleToSource)
, errError :: TCErr'
}
deriving (Typeable)
instance Error TCErr where
noMsg = strMsg ""
strMsg = TCErr Nothing . Exception noRange . strMsg
instance Show TCErr where
show = show . errError
instance Show TCErr' where
show (TypeError _ e) = show (getRange $ clTrace e) ++ ": " ++ show (clValue e)
show (Exception r s) = show r ++ ": " ++ s
show (IOException r e) = show r ++ ": " ++ show e
show (PatternErr _) = "Pattern violation (you shouldn't see this)"
show (AbortAssign _) = "Abort assignment (you shouldn't see this)"
instance HasRange TCErr' where
getRange (TypeError _ cl) = getRange $ clTrace cl
getRange (Exception r _) = r
getRange (IOException r _) = r
getRange (PatternErr s) = getRange $ stTrace s
getRange (AbortAssign s) = getRange $ stTrace s
instance HasRange TCErr where
getRange = getRange . errError
instance Exception TCErr
newtype TCMT m a = TCM { unTCM :: StateT TCState
(ReaderT TCEnv m) a
}
deriving ( MonadState TCState
, MonadReader TCEnv
)
type TCM = TCMT IO
class ( Applicative tcm, MonadIO tcm
, MonadReader TCEnv tcm
, MonadState TCState tcm
) => MonadTCM tcm where
liftTCM :: TCM a -> tcm a
instance MonadError TCErr (TCMT IO) where
throwError = liftIO . throwIO
catchError m h = TCM $ StateT $ \s -> ReaderT $ \e ->
runReaderT (runStateT (unTCM m) s) e
`E.catch` \err -> runReaderT (runStateT (unTCM (h err)) s) e
mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a
mapTCMT f = TCM . mapStateT (mapReaderT f) . unTCM
pureTCM :: Monad m => (TCState -> TCEnv -> a) -> TCMT m a
pureTCM f = TCM $ StateT $ \s -> ReaderT $ \e -> return (f s e, s)
instance MonadIO m => MonadTCM (TCMT m) where
liftTCM = mapTCMT liftIO
instance (Error err, MonadTCM tcm) => MonadTCM (ErrorT err tcm) where
liftTCM = lift . liftTCM
instance MonadTrans TCMT where
lift = TCM . lift . lift
instance MonadIO m => Monad (TCMT m) where
return = TCM . return
m >>= k = TCM $ StateT $ \s -> ReaderT $ \e -> do
(x, s') <- runReaderT (runStateT (unTCM m) s) e
runReaderT (runStateT (unTCM (k x)) s') e
fail = internalError
instance MonadIO m => Functor (TCMT m) where
fmap = liftM
instance MonadIO m => Applicative (TCMT m) where
pure = return
(<*>) = ap
instance MonadIO m => MonadIO (TCMT m) where
liftIO m = TCM $ do r <- gets $ getRange . stTrace
liftIO $ wrap r $ do
x <- m
x `seq` return x
where
wrap r m = failOnException handleException
$ E.catch m (handleIOException r)
handleIOException r e = throwIO $ TCErr Nothing $ IOException r e
handleException r s = throwIO $ TCErr Nothing $ Exception r s
patternViolation :: MonadTCM tcm => tcm a
patternViolation = liftTCM $ do
s <- get
throwError $ TCErr Nothing $ PatternErr s
internalError :: MonadTCM tcm => String -> tcm a
internalError s = typeError $ InternalError s
typeError :: MonadTCM tcm => TypeError -> tcm a
typeError err = liftTCM $ do
cl <- buildClosure err
s <- get
throwError $ TCErr Nothing $ TypeError s cl
runTCM :: TCMT IO a -> IO (Either TCErr a)
runTCM m = (Right <$> runTCM' m) `E.catch` (return . Left)
runTCM' :: Monad m => TCMT m a -> m a
runTCM' m = flip runReaderT initEnv
$ flip evalStateT initState
$ unTCM m