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.Int
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.TypeChecking.CompiledClause
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.Permutation
#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 :: PragmaOptions
, stStatistics :: Statistics
, 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 = optPragmaOptions $ defaultOptions
, stStatistics = Map.empty
, 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
, iPragmaOptions :: [OptionsPragma]
}
deriving (Typeable, Data, Show)
data Closure a = Closure { clSignature :: Signature
, clEnv :: TCEnv
, clScope :: ScopeInfo
, 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
return $ Closure sig env scope x
type ConstraintClosure = Closure Constraint
data Constraint = ValueCmp Comparison Type Term Term
| ArgsCmp [Polarity] Type Args Args
| TypeCmp Comparison Type Type
| TelCmp Comparison Telescope Telescope
| SortCmp Comparison Sort Sort
| LevelCmp Comparison Term Term
| 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
, mvPermutation :: Permutation
, 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 perm j inst ls) =
MetaVar (mi {clValue = r}) p perm 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
{ defRelevance :: Relevance
, defName :: QName
, defType :: Type
, defDisplay :: [Open DisplayForm]
, defMutual :: MutualId
, theDef :: Defn
}
deriving (Typeable, Data, Show)
type HaskellCode = String
type HaskellType = String
type EpicCode = 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
, axEpDef :: Maybe EpicCode
}
| Function
{ funClauses :: [Clauses]
, funCompiled :: CompiledClauses
, funInv :: FunctionInverse
, funPolarity :: [Polarity]
, funArgOccurrences :: [Occurrence]
, funAbstr :: IsAbstract
, funDelayed :: Delayed
, funProjection :: Maybe Int
}
| 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 :: QName
, recNamedCon :: Bool
, recConType :: Type
, recFields :: [Arg A.QName]
, recTel :: Telescope
, recPolarity :: [Polarity]
, recArgOccurrences :: [Occurrence]
, recEtaEquality :: Bool
, recAbstr :: IsAbstract
}
| Constructor
{ conPars :: Nat
, conSrcCon :: QName
, conData :: QName
, conHsCode :: Maybe (HaskellType, HaskellCode)
, conAbstr :: IsAbstract
, conInd :: Induction
}
| Primitive
{ primAbstr :: IsAbstract
, primName :: String
, primClauses :: Maybe [Clauses]
, primCompiled :: Maybe CompiledClauses
}
deriving (Typeable, Data, Show)
defIsRecord :: Defn -> Bool
defIsRecord Record{} = True
defIsRecord _ = False
newtype Fields = Fields [(C.Name, Type)]
deriving (Typeable, Data)
data Reduced no yes = NoReduction no | YesReduction yes
deriving (Typeable)
data IsReduced = NotReduced | Reduced (Blocked ())
data MaybeReduced a = MaybeRed
{ isReduced :: IsReduced
, ignoreReduced :: a
}
instance Functor MaybeReduced where
fmap f (MaybeRed r x) = MaybeRed r (f x)
type MaybeReducedArgs = [MaybeReduced (Arg Term)]
notReduced :: a -> MaybeReduced a
notReduced x = MaybeRed NotReduced x
reduced :: Blocked a -> MaybeReduced a
reduced b = MaybeRed (Reduced $ fmap (const ()) b) (ignoreBlocking b)
data PrimFun = PrimFun
{ primFunName :: QName
, primFunArity :: Arity
, primFunImplementation :: MonadTCM tcm => [Arg Term] -> tcm (Reduced MaybeReducedArgs Term)
}
deriving (Typeable)
defClauses :: Definition -> [Clauses]
defClauses Defn{theDef = Function{funClauses = cs}} = cs
defClauses Defn{theDef = Primitive{primClauses = Just cs}} = cs
defClauses Defn{theDef = Datatype{dataClause = Just c}} = [Clauses Nothing c]
defClauses Defn{theDef = Record{recClause = Just c}} = [Clauses Nothing c]
defClauses _ = []
defCompiled :: Definition -> Maybe CompiledClauses
defCompiled Defn{theDef = Function{funCompiled = cc}} = Just cc
defCompiled Defn{theDef = Primitive{primCompiled = mcc}} = mcc
defCompiled _ = Nothing
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 Int32
deriving (Typeable, Data, Eq, Ord, Show, Num)
type Statistics = Map String Int
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 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
, envIrrelevant :: Bool
, envReplace :: Bool
, envDisplayFormsEnabled :: Bool
, envReifyInteractionPoints :: Bool
, envEtaContractImplicit :: Bool
, envRange :: Range
, envCall :: Maybe (Closure Call)
}
deriving (Typeable, Data)
initEnv :: TCEnv
initEnv = TCEnv { envContext = []
, envLetBindings = Map.empty
, envCurrentModule = noModuleName
, envAnonymousModules = []
, envImportPath = []
, envMutualBlock = Nothing
, envAbstractMode = AbstractMode
, envIrrelevant = False
, envReplace = True
, envDisplayFormsEnabled = True
, envReifyInteractionPoints = True
, envEtaContractImplicit = True
, envRange = noRange
, envCall = Nothing
}
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, Arg 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
| IndicesNotConstructorApplications [Arg Term]
| IndexVariablesNotDistinct [Arg Term]
| IndexFreeInParameter Nat [Arg Term]
| DoesNotConstructAnElementOf QName Term
| DifferentArities
| WrongHidingInLHS Type
| WrongHidingInLambda Type
| WrongHidingInApplication Type
| 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
| SplitOnIrrelevant A.Pattern (Arg Type)
| DefinitionIsIrrelevant QName
| VariableIsIrrelevant Name
| UnequalLevel Comparison Term Term
| UnequalTerms Comparison Term Term Type
| UnequalTypes Comparison Type Type
| UnequalTelescopes Comparison Telescope Telescope
| UnequalRelevance Type Type
| 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]
| DuplicateImports 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 (envRange $ clEnv 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) = envRange $ clEnv cl
getRange (Exception r _) = r
getRange (IOException r _) = r
getRange (PatternErr s) = noRange
getRange (AbortAssign s) = noRange
instance HasRange TCErr where
getRange = getRange . errError
instance Exception TCErr
newtype TCMT m a = TCM { unTCM :: TCState -> TCEnv -> m (a, TCState) }
instance MonadIO m => MonadReader TCEnv (TCMT m) where
ask = TCM $ \s e -> return (e, s)
local f (TCM m) = TCM $ \s e -> m s (f e)
instance MonadIO m => MonadState TCState (TCMT m) where
get = TCM $ \s _ -> return (s, s)
put s = TCM $ \_ _ -> return ((), s)
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 $ \s e ->
unTCM m s e `E.catch` \err -> unTCM (h err) s e
catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a
catchError_ m h = TCM $ \s e ->
unTCM m s e
`E.catch` \err -> unTCM (h err) (error "catchError_") e
mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a
mapTCMT f (TCM m) = TCM $ \s e -> f (m s e)
pureTCM :: Monad m => (TCState -> TCEnv -> a) -> TCMT m a
pureTCM f = TCM $ \s 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 m = TCM $ \s _ -> m >>= \x -> return (x, s)
instance MonadIO m => Monad (TCMT m) where
return x = TCM $ \s _ -> return (x, s)
m >>= k = TCM $ \s e -> do
(x, s') <- unTCM m s e
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 $ \s e ->
do let r = envRange e
liftIO $ wrap r $ do
x <- m
x `seq` return (x, s)
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 = liftM fst (unTCM m initState initEnv)