module Agda.TypeChecking.Monad.Base where
import Control.Arrow
import Control.Exception as E
import Control.Monad.Error
import Control.Monad.State
import Control.Monad.Reader
import Control.Applicative
import Data.Function
import Data.Int
import Data.Map as Map
import Data.Set as Set
import Data.Generics
import Data.Foldable
import Data.Traversable
import Data.IORef
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 qualified Agda.Compiler.JS.Syntax as JS
import Agda.Utils.FileName
import Agda.Utils.Fresh
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Pretty
#include "../../undefined.h"
import Agda.Utils.Impossible
data TCState =
TCSt { stFreshThings :: FreshThings
, stMetaStore :: MetaStore
, stInteractionPoints :: InteractionPoints
, stAwakeConstraints :: Constraints
, stSleepingConstraints :: Constraints
, stSignature :: Signature
, stImports :: Signature
, stImportedModules :: Set ModuleName
, stModuleToSource :: ModuleToSource
, stVisitedModules :: VisitedModules
, stCurrentModule :: Maybe ModuleName
, stScope :: ScopeInfo
, stPragmaOptions :: PragmaOptions
, stStatistics :: Statistics
, stExtLambdaTele :: Map QName (Int , Int)
, stMutualBlocks :: Map MutualId (Set QName)
, stLocalBuiltins :: BuiltinThings PrimFun
, stImportedBuiltins :: BuiltinThings PrimFun
, stHaskellImports :: Set String
, stPersistent :: PersistentTCState
}
data PersistentTCState = PersistentTCSt
{ stDecodedModules :: DecodedModules
, stPersistentOptions :: CommandLineOptions
}
data FreshThings =
Fresh { fMeta :: MetaId
, fInteraction :: InteractionId
, fMutual :: MutualId
, fName :: NameId
, fCtx :: CtxId
, fProblem :: ProblemId
, fInteger :: Integer
}
deriving (Show)
initState :: TCState
initState =
TCSt { stFreshThings = (Fresh 0 0 0 (NameId 0 0) 0 0 0) { fProblem = 1 }
, stMetaStore = Map.empty
, stInteractionPoints = Map.empty
, stAwakeConstraints = []
, stSleepingConstraints = []
, stSignature = emptySignature
, stImports = emptySignature
, stImportedModules = Set.empty
, stModuleToSource = Map.empty
, stVisitedModules = Map.empty
, stCurrentModule = Nothing
, stScope = emptyScopeInfo
, stPragmaOptions = optPragmaOptions $ defaultOptions
, stStatistics = Map.empty
, stExtLambdaTele = Map.empty
, stMutualBlocks = Map.empty
, stLocalBuiltins = Map.empty
, stImportedBuiltins = Map.empty
, stHaskellImports = Set.empty
, stPersistent = PersistentTCSt
{ stPersistentOptions = defaultOptions
, stDecodedModules = Map.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
newtype ProblemId = ProblemId Nat
deriving (Typeable, Data, Eq, Ord, Enum, Real, Integral, Num)
instance Show ProblemId where
show (ProblemId n) = show n
instance HasFresh ProblemId FreshThings where
nextFresh s = (i, s { fProblem = succ i })
where i = fProblem 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 :: a -> TCM (Closure a)
buildClosure x = do
env <- ask
sig <- gets stSignature
scope <- gets stScope
return $ Closure sig env scope x
type Constraints = [ProblemConstraint]
data ProblemConstraint = PConstr
{ constraintProblem :: ProblemId
, theConstraint :: Closure Constraint
}
deriving (Typeable, Show)
data Constraint
= ValueCmp Comparison Type Term Term
| ElimCmp [Polarity] Type Term [Elim] [Elim]
| TypeCmp Comparison Type Type
| TelCmp Type Type Comparison Telescope Telescope
| SortCmp Comparison Sort Sort
| LevelCmp Comparison Level Level
| UnBlock MetaId
| Guarded Constraint ProblemId
| IsEmpty Type
| FindInScope MetaId
deriving (Typeable, Show)
data Comparison = CmpEq | CmpLeq
deriving (Eq, Typeable, Show)
data Open a = OpenThing [CtxId] a
deriving (Typeable, Data, Show, Functor)
data Judgement t a
= HasType { jMetaId :: a, jMetaType :: t }
| IsSort { jMetaId :: a, jMetaType :: t }
deriving (Typeable, Data, Functor, Foldable, Traversable)
instance (Show t, Show a) => Show (Judgement t a) where
show (HasType a t) = show a ++ " : " ++ show t
show (IsSort a t) = show a ++ " :sort " ++ show t
data MetaVariable =
MetaVar { mvInfo :: MetaInfo
, mvPriority :: MetaPriority
, mvPermutation :: Permutation
, mvJudgement :: Judgement Type MetaId
, mvInstantiation :: MetaInstantiation
, mvListeners :: Set Listener
, mvFrozen :: Frozen
}
deriving (Typeable)
data Listener = EtaExpand MetaId
| CheckConstraint Nat ProblemConstraint
deriving (Typeable)
instance Eq Listener where
EtaExpand x == EtaExpand y = x == y
CheckConstraint x _ == CheckConstraint y _ = x == y
_ == _ = False
instance Ord Listener where
EtaExpand x `compare` EtaExpand y = x `compare` y
CheckConstraint x _ `compare` CheckConstraint y _ = x `compare` y
EtaExpand{} `compare` CheckConstraint{} = LT
CheckConstraint{} `compare` EtaExpand{} = Prelude.GT
data Frozen
= Frozen
| Instantiable
deriving (Eq, Show)
data MetaInstantiation
= InstV Term
| InstS Term
| Open
| OpenIFS
| 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 OpenIFS = "OpenIFS"
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 frozen) =
MetaVar (mi {clValue = r}) p perm j inst ls frozen
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
| DCon QName [Arg DisplayTerm]
| DDef QName [Arg DisplayTerm]
| DDot Term
| 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
, defCompiledRep :: CompiledRepresentation
, theDef :: Defn
}
deriving (Typeable, Data, Show)
type HaskellCode = String
type HaskellType = String
type EpicCode = String
type JSCode = JS.Exp
data HaskellRepresentation
= HsDefn HaskellType HaskellCode
| HsType HaskellType
deriving (Typeable, Data, Show)
data Polarity = Covariant | Contravariant | Invariant
deriving (Typeable, Data, Show, Eq)
data CompiledRepresentation = CompiledRep
{ compiledHaskell :: Maybe HaskellRepresentation
, compiledEpic :: Maybe EpicCode
, compiledJS :: Maybe JSCode
}
deriving (Typeable, Data, Show)
noCompiledRep :: CompiledRepresentation
noCompiledRep = CompiledRep Nothing Nothing Nothing
data Occurrence = Positive | Negative | Unused
deriving (Typeable, Data, Show, Eq, Ord)
data Defn = Axiom
| Function
{ funClauses :: [Clause]
, funCompiled :: CompiledClauses
, funInv :: FunctionInverse
, funPolarity :: [Polarity]
, funArgOccurrences :: [Occurrence]
, funAbstr :: IsAbstract
, funDelayed :: Delayed
, funProjection :: Maybe (QName, Int)
, funStatic :: Bool
}
| Datatype
{ dataPars :: Nat
, dataIxs :: Nat
, dataInduction :: Induction
, dataClause :: (Maybe Clause)
, dataCons :: [QName]
, dataSort :: Sort
, dataPolarity :: [Polarity]
, dataArgOccurrences :: [Occurrence]
, 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
, conAbstr :: IsAbstract
, conInd :: Induction
}
| Primitive
{ primAbstr :: IsAbstract
, primName :: String
, primClauses :: Maybe [Clause]
, 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, Functor)
data IsReduced = NotReduced | Reduced (Blocked ())
data MaybeReduced a = MaybeRed
{ isReduced :: IsReduced
, ignoreReduced :: a
}
deriving (Functor)
type MaybeReducedArgs = [MaybeReduced (Arg Term)]
notReduced :: a -> MaybeReduced a
notReduced x = MaybeRed NotReduced x
reduced :: Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced b = case b of
NotBlocked (Arg _ _ (MetaV x _)) -> MaybeRed (Reduced $ Blocked x ()) v
_ -> MaybeRed (Reduced $ () <$ b) v
where
v = ignoreBlocking b
data PrimFun = PrimFun
{ primFunName :: QName
, primFunArity :: Arity
, primFunImplementation :: [Arg Term] -> TCM (Reduced MaybeReducedArgs 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 _ = []
defCompiled :: Definition -> Maybe CompiledClauses
defCompiled Defn{theDef = Function{funCompiled = cc}} = Just cc
defCompiled Defn{theDef = Primitive{primCompiled = mcc}} = mcc
defCompiled _ = Nothing
defJSDef :: Definition -> Maybe JSCode
defJSDef = compiledJS . defCompiledRep
defEpicDef :: Definition -> Maybe EpicCode
defEpicDef = compiledEpic . defCompiledRep
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{} -> ConcreteDef
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 Integer
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))
| 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 ())
| CheckIsEmpty Type (Maybe ())
| CheckWithFunctionType A.Expr (Maybe ())
| CheckSectionApplication Range ModuleName A.ModuleApplication (Maybe ())
| ScopeCheckExpr C.Expr (Maybe A.Expr)
| ScopeCheckDeclaration D.NiceDeclaration (Maybe [A.Declaration])
| ScopeCheckLHS C.Name C.Pattern (Maybe A.LHS)
| 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 CheckWithFunctionType{} = noRange
getRange (ScopeCheckExpr e _) = getRange e
getRange (ScopeCheckDeclaration d _) = getRange d
getRange (ScopeCheckLHS _ p _) = getRange p
getRange (CheckDotPattern e _ _) = getRange e
getRange (CheckPatternShadowing c _) = getRange c
getRange (TermFunDef i _ _ _) = getRange i
getRange (SetRange r _) = r
getRange (CheckSectionApplication r _ _ _) = r
getRange (CheckIsEmpty _ _) = noRange
data BuiltinDescriptor = BuiltinData (TCM Type) [String]
| BuiltinDataCons (TCM Type)
| BuiltinPrim String (Term -> TCM ())
| BuiltinPostulate (TCM Type)
| BuiltinUnknown (Maybe (TCM Type)) (Term -> TCM ())
data BuiltinInfo =
BuiltinInfo { builtinName :: String
, builtinDesc :: BuiltinDescriptor }
type BuiltinThings pf = Map String (Builtin pf)
data Builtin pf
= Builtin Term
| Prim pf
deriving (Typeable, Data, Show, Functor, Foldable, Traversable)
data TCEnv =
TCEnv { envContext :: Context
, envLetBindings :: LetBindings
, envCurrentModule :: ModuleName
, envAnonymousModules :: [(ModuleName, Nat)]
, envImportPath :: [C.TopLevelModuleName]
, envMutualBlock :: Maybe MutualId
, envSolvingConstraints :: Bool
, envActiveProblems :: [ProblemId]
, envAbstractMode :: AbstractMode
, envTopLevel :: Bool
, envRelevance :: Relevance
, 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
, envSolvingConstraints = False
, envActiveProblems = [0]
, envAbstractMode = AbstractMode
, envTopLevel = True
, envRelevance = Relevant
, 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
}
deriving (Show)
data OccPos = NonPositively | ArgumentTo Nat QName
deriving (Show)
data CallInfo = CallInfo
{ callInfoRange :: Range
, callInfoCall :: String
} deriving (Eq, Ord, Typeable, Show)
data TerminationError = TerminationError
{ termErrFunctions :: [QName]
, termErrCalls :: [CallInfo]
} deriving (Typeable, Show)
data TypeError
= InternalError String
| NotImplemented String
| NotSupported String
| CompilationError String
| TerminationCheckFailed [TerminationError]
| 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
| WrongIrrelevanceInLambda 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
| HeterogeneousEquality Term Type Term Type
| 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 Telescope Args Args
| CoverageCantSplitIrrelevantType Type
| 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
| NothingAppliedToInstanceArg C.Expr
| NoParseForApplication [C.Expr]
| AmbiguousParseForApplication [C.Expr] [C.Expr]
| NoParseForLHS C.Pattern
| AmbiguousParseForLHS C.Pattern [C.Pattern]
| IFSNoCandidateInScope Type
| SafeFlagPostulate C.Name
| SafeFlagPragma [String]
| SafeFlagPrimTrustMe
deriving (Typeable, Show)
instance Error TypeError where
noMsg = strMsg ""
strMsg = GenericError
data TCErr' = TypeError TCState (Closure TypeError)
| Exception Range String
| IOException Range E.IOException
| PatternErr 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)"
instance HasRange TCErr' where
getRange (TypeError _ cl) = envRange $ clEnv cl
getRange (Exception r _) = r
getRange (IOException r _) = r
getRange (PatternErr s) = noRange
instance HasRange TCErr where
getRange = getRange . errError
instance Exception TCErr
newtype TCMT m a = TCM { unTCM :: IORef TCState -> TCEnv -> m a }
instance MonadIO m => MonadReader TCEnv (TCMT m) where
ask = TCM $ \s e -> return e
local f (TCM m) = TCM $ \s e -> m s (f e)
instance MonadIO m => MonadState TCState (TCMT m) where
get = TCM $ \s _ -> liftIO (readIORef s)
put s = TCM $ \r _ -> liftIO (writeIORef r 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 $ \r e -> do
oldState <- liftIO (readIORef r)
unTCM m r e `E.catch` \err -> do
liftIO $ do
newState <- readIORef r
writeIORef r $ oldState { stPersistent = stPersistent newState }
unTCM (h err) r e
catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a
catchError_ m h = TCM $ \r e ->
unTCM m r e
`E.catch` \err -> unTCM (h err) r 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 :: MonadIO m => (TCState -> TCEnv -> a) -> TCMT m a
pureTCM f = TCM $ \r e -> do
s <- liftIO $ readIORef r
return (f s e)
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 $ \_ _ -> m
instance MonadIO m => Monad (TCMT m) where
return x = TCM $ \_ _ -> return x
TCM m >>= k = TCM $ \r e -> do
x <- m r e
let TCM m' = k x in m' r e
TCM m1 >> TCM m2 = TCM $ \r e -> m1 r e >> m2 r 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
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 :: TCM a
patternViolation = 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' :: MonadIO m => TCMT m a -> m a
runTCM' m = do
r <- liftIO $ newIORef initState
unTCM m r initEnv
extendlambdaname = ".extendedlambda"