module Agda.TypeChecking.Monad.Base where
import Control.Arrow
import qualified Control.Concurrent as C
import Control.DeepSeq
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.Sequence as Seq
import Data.Typeable (Typeable)
import Data.Foldable
import Data.Traversable
import Data.IORef
import Data.Hashable
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.Utils.HashMap as HMap
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.Response
(InteractionOutputCallback, defaultInteractionOutputCallback)
import Agda.Interaction.Highlighting.Precise
(CompressedFile, HighlightingInfo)
import Data.Monoid
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
import Agda.Utils.Time
#include "../../undefined.h"
import Agda.Utils.Impossible
data TCState =
TCSt { stFreshThings :: FreshThings
, stSyntaxInfo :: CompressedFile
, stTokens :: CompressedFile
, stTermErrs :: Seq TerminationError
, stMetaStore :: MetaStore
, stInteractionPoints :: InteractionPoints
, stAwakeConstraints :: Constraints
, stSleepingConstraints :: Constraints
, stDirty :: Bool
, stOccursCheckDefs :: Set QName
, stSignature :: Signature
, stImports :: Signature
, stImportedModules :: Set ModuleName
, stModuleToSource :: ModuleToSource
, stVisitedModules :: VisitedModules
, stCurrentModule :: Maybe ModuleName
, stScope :: ScopeInfo
, stPatternSyns :: A.PatternSynDefns
, stPatternSynImports :: A.PatternSynDefns
, 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
, stInteractionOutputCallback :: InteractionOutputCallback
}
data PersistentTCState = PersistentTCSt
{ stDecodedModules :: DecodedModules
, stPersistentOptions :: CommandLineOptions
}
data FreshThings =
Fresh { fMeta :: MetaId
, fInteraction :: InteractionId
, fMutual :: MutualId
, fName :: NameId
, fCtx :: CtxId
, fProblem :: ProblemId
, fInt :: Int
}
deriving (Show)
initState :: TCState
initState =
TCSt { stFreshThings = (Fresh 0 0 0 (NameId 0 0) 0 0 0) { fProblem = 1 }
, stMetaStore = Map.empty
, stSyntaxInfo = mempty
, stTokens = mempty
, stTermErrs = Seq.empty
, stInteractionPoints = Map.empty
, stAwakeConstraints = []
, stSleepingConstraints = []
, stDirty = False
, stOccursCheckDefs = Set.empty
, stSignature = emptySignature
, stImports = emptySignature
, stImportedModules = Set.empty
, stModuleToSource = Map.empty
, stVisitedModules = Map.empty
, stCurrentModule = Nothing
, stScope = emptyScopeInfo
, stPatternSyns = Map.empty
, stPatternSynImports = Map.empty
, stPragmaOptions = defaultInteractionOptions
, 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
}
, stInteractionOutputCallback = defaultInteractionOutputCallback
}
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 Int FreshThings where
nextFresh s = (i, s { fInt = succ i })
where
i = fInt s
newtype ProblemId = ProblemId Nat
deriving (Typeable, 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, QName)
, iHaskellImports :: Set String
, iHighlighting :: HighlightingInfo
, iPragmaOptions :: [OptionsPragma]
, iPatternSyns :: A.PatternSynDefns
}
deriving (Typeable, Show)
data Closure a = Closure { clSignature :: Signature
, clEnv :: TCEnv
, clScope :: ScopeInfo
, clValue :: a
}
deriving (Typeable)
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 Range Type
| FindInScope MetaId [(Term, Type)]
deriving (Typeable, Show)
data Comparison = CmpEq | CmpLeq
deriving (Eq, Typeable)
instance Show Comparison where
show CmpEq = "="
show CmpLeq = "=<"
data Open a = OpenThing [CtxId] a
deriving (Typeable, Show, Functor)
data Judgement t a
= HasType { jMetaId :: a, jMetaType :: t }
| IsSort { jMetaId :: a, jMetaType :: t }
deriving (Typeable, 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)
data RunMetaOccursCheck
= RunMetaOccursCheck
| DontRunMetaOccursCheck
deriving (Eq, Ord, Show)
data MetaInfo = MetaInfo
{ miClosRange :: Closure Range
, miMetaOccursCheck :: RunMetaOccursCheck
, miNameSuggestion :: MetaNameSuggestion
}
type MetaNameSuggestion = String
data NamedMeta = NamedMeta
{ nmSuggestion :: MetaNameSuggestion
, nmid :: MetaId
}
instance Show NamedMeta where
show (NamedMeta "" x) = show x
show (NamedMeta s x) = "_" ++ s ++ show x
type MetaStore = Map MetaId MetaVariable
instance HasRange MetaVariable where
getRange m = getRange $ getMetaInfo m
instance SetRange MetaVariable where
setRange r m = m { mvInfo = (mvInfo m)
{ miClosRange = (miClosRange (mvInfo m))
{ clValue = r }}}
normalMetaPriority :: MetaPriority
normalMetaPriority = MetaPriority 0
lowMetaPriority :: MetaPriority
lowMetaPriority = MetaPriority (10)
highMetaPriority :: MetaPriority
highMetaPriority = MetaPriority 10
getMetaInfo :: MetaVariable -> Closure Range
getMetaInfo = miClosRange . 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
getMetaRelevance :: MetaVariable -> Relevance
getMetaRelevance = envRelevance . getMetaEnv
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, Show)
type Sections = Map ModuleName Section
type Definitions = HashMap QName Definition
data Section = Section
{ secTelescope :: Telescope
, secFreeVars :: Nat
}
deriving (Typeable, Show)
emptySignature :: Signature
emptySignature = Sig Map.empty HMap.empty
data DisplayForm = Display Nat [Term] DisplayTerm
deriving (Typeable, Show)
data DisplayTerm = DWithApp [DisplayTerm] Args
| DCon QName [Arg DisplayTerm]
| DDef QName [Arg DisplayTerm]
| DDot Term
| DTerm Term
deriving (Typeable, Show)
defaultDisplayForm :: QName -> [Open DisplayForm]
defaultDisplayForm c = []
data Definition = Defn
{ defRelevance :: Relevance
, defName :: QName
, defType :: Type
, defPolarity :: [Polarity]
, defArgOccurrences :: [Occurrence]
, defDisplay :: [Open DisplayForm]
, defMutual :: MutualId
, defCompiledRep :: CompiledRepresentation
, theDef :: Defn
}
deriving (Typeable, Show)
type HaskellCode = String
type HaskellType = String
type EpicCode = String
type JSCode = JS.Exp
data HaskellRepresentation
= HsDefn HaskellType HaskellCode
| HsType HaskellType
deriving (Typeable, Show)
data Polarity
= Covariant
| Contravariant
| Invariant
| Nonvariant
deriving (Typeable, Show, Eq)
data CompiledRepresentation = CompiledRep
{ compiledHaskell :: Maybe HaskellRepresentation
, compiledEpic :: Maybe EpicCode
, compiledJS :: Maybe JSCode
}
deriving (Typeable, Show)
noCompiledRep :: CompiledRepresentation
noCompiledRep = CompiledRep Nothing Nothing Nothing
data Occurrence
= Mixed
| JustNeg
| JustPos
| StrictPos
| GuardPos
| Unused
deriving (Typeable, Show, Eq, Ord)
instance NFData Occurrence
data Defn = Axiom
| Function
{ funClauses :: [Clause]
, funCompiled :: CompiledClauses
, funInv :: FunctionInverse
, funMutual :: [QName]
, funAbstr :: IsAbstract
, funDelayed :: Delayed
, funProjection :: Maybe (QName, Int)
, funStatic :: Bool
, funCopy :: Bool
, funTerminates :: Maybe Bool
}
| Datatype
{ dataPars :: Nat
, dataIxs :: Nat
, dataInduction :: Induction
, dataClause :: (Maybe Clause)
, dataCons :: [QName]
, dataSort :: Sort
, dataMutual :: [QName]
, dataAbstr :: IsAbstract
}
| Record
{ recPars :: Nat
, recClause :: Maybe Clause
, recCon :: QName
, recNamedCon :: Bool
, recConType :: Type
, recFields :: [Arg A.QName]
, recTel :: Telescope
, recMutual :: [QName]
, recEtaEquality :: Bool
, recInduction :: Induction
, recRecursive :: 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, Show)
defIsRecord :: Defn -> Bool
defIsRecord Record{} = True
defIsRecord _ = False
defIsDataOrRecord :: Defn -> Bool
defIsDataOrRecord Record{} = True
defIsDataOrRecord Datatype{} = True
defIsDataOrRecord _ = False
newtype Fields = Fields [(C.Name, Type)]
deriving (Typeable)
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 fmap ignoreSharing <$> 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
defDelayed :: Definition -> Delayed
defDelayed Defn{theDef = Function{funDelayed = d}} = d
defDelayed _ = NotDelayed
defCopy :: Definition -> Bool
defCopy Defn{theDef = Function{funCopy = b}} = b
defCopy _ = False
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
type FunctionInverse = FunctionInverse' Clause
data FunctionInverse' c
= NotInjective
| Inverse (Map TermHead c)
deriving (Typeable, Show, Functor)
data TermHead = SortHead
| PiHead
| ConHead QName
deriving (Typeable, Eq, Ord, Show)
newtype MutualId = MutId Int32
deriving (Typeable, 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 Range 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. NoHighlighting (Maybe a)
| forall a. SetRange Range (Maybe a)
deriving (Typeable)
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 (SetRange r _) = r
getRange (CheckSectionApplication r _ _ _) = r
getRange (CheckIsEmpty r _ _) = r
getRange (NoHighlighting _) = noRange
data BuiltinDescriptor = BuiltinData (TCM Type) [String]
| BuiltinDataCons (TCM Type)
| BuiltinPrim String (Term -> TCM ())
| BuiltinPostulate Relevance (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, Show, Functor, Foldable, Traversable)
data HighlightingLevel
= None
| NonInteractive
| Interactive
deriving (Eq, Ord, Show, Read)
data HighlightingMethod
= Direct
| Indirect
deriving (Eq, Show, Read)
ifTopLevelAndHighlightingLevelIs ::
MonadTCM tcm => HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs l m = do
e <- ask
when (envModuleNestingLevel e == 0 &&
envHighlightingLevel e >= l)
m
data TCEnv =
TCEnv { envContext :: Context
, envLetBindings :: LetBindings
, envCurrentModule :: ModuleName
, envCurrentPath :: AbsolutePath
, envAnonymousModules :: [(ModuleName, Nat)]
, envImportPath :: [C.TopLevelModuleName]
, envMutualBlock :: Maybe MutualId
, envSolvingConstraints :: Bool
, envAssignMetas :: Bool
, envActiveProblems :: [ProblemId]
, envAbstractMode :: AbstractMode
, envRelevance :: Relevance
, envDisplayFormsEnabled :: Bool
, envReifyInteractionPoints :: Bool
, envEtaContractImplicit :: Bool
, envRange :: Range
, envHighlightingRange :: Range
, envCall :: Maybe (Closure Call)
, envEmacs :: Bool
, envHighlightingLevel :: HighlightingLevel
, envHighlightingMethod :: HighlightingMethod
, envModuleNestingLevel :: Integer
, envAllowDestructiveUpdate :: Bool
}
deriving (Typeable)
initEnv :: TCEnv
initEnv = TCEnv { envContext = []
, envLetBindings = Map.empty
, envCurrentModule = noModuleName
, envCurrentPath = __IMPOSSIBLE__
, envAnonymousModules = []
, envImportPath = []
, envMutualBlock = Nothing
, envSolvingConstraints = False
, envActiveProblems = [0]
, envAssignMetas = True
, envAbstractMode = AbstractMode
, envRelevance = Relevant
, envDisplayFormsEnabled = True
, envReifyInteractionPoints = True
, envEtaContractImplicit = True
, envRange = noRange
, envHighlightingRange = noRange
, envCall = Nothing
, envEmacs = False
, envHighlightingLevel = None
, envHighlightingMethod = Indirect
, envModuleNestingLevel = 1
, envAllowDestructiveUpdate = True
}
type Context = [ContextEntry]
data ContextEntry = Ctx { ctxId :: CtxId
, ctxEntry :: Dom (Name, Type)
}
deriving (Typeable)
newtype CtxId = CtxId Nat
deriving (Typeable, Eq, Ord, Show, Enum, Real, Integral, Num)
type LetBindings = Map Name (Open (Term, Dom Type))
data AbstractMode = AbstractMode
| ConcreteMode
| IgnoreAbstractMode
deriving (Typeable)
data ExpandHidden
= ExpandLast
| DontExpandLast
data ExpandInstances
= ExpandInstanceArguments
| DontExpandInstanceArguments
deriving (Eq)
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, Eq)
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 [Nat] [Arg Term]
| IndicesFreeInParameters [Nat] [Arg Term] [Arg Term]
| DoesNotConstructAnElementOf QName Term
| DifferentArities
| WrongHidingInLHS Type
| WrongHidingInLambda Type
| WrongHidingInApplication Type
| WrongIrrelevanceInLambda Type
| NotInductive Term
| UninstantiatedDotPattern A.Expr
| IlltypedPattern A.Pattern Type
| TooManyArgumentsInLHS Type
| WrongNumberOfConstructorArguments QName Nat Nat
| ShouldBeEmpty Type [Pattern]
| ShouldBeASort Type
| ShouldBePi Type
| ShouldBeRecordType Type
| ShouldBeRecordPattern Pattern
| NotAProperTerm
| SetOmegaNotValidType
| SplitOnIrrelevant A.Pattern (Dom Type)
| DefinitionIsIrrelevant QName
| VariableIsIrrelevant Name
| UnequalLevel Comparison Term Term
| UnequalTerms Comparison Term Term Type
| UnequalTypes Comparison Type Type
| UnequalTelescopes Comparison Telescope Telescope
| UnequalRelevance Comparison Term Term
| UnequalHiding Term Term
| UnequalSorts Sort Sort
| UnequalBecauseOfUniverseConflict Comparison Term Term
| HeterogeneousEquality Term Type Term Type
| NotLeqSort Sort Sort
| MetaCannotDependOn MetaId [Nat] Nat
| MetaOccursInItself MetaId
| GenericError String
| GenericDocError Doc
| BuiltinMustBeConstructor String A.Expr
| NoSuchBuiltinName String
| DuplicateBuiltinBinding String Term Term
| NoBindingForBuiltin String
| NoSuchPrimitiveFunction String
| ShadowedModule C.Name [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
| UnusedVariableInPatternSynonym
| PatternSynonymArityMismatch A.QName
| NoParseForApplication [C.Expr]
| AmbiguousParseForApplication [C.Expr] [C.Expr]
| NoParseForLHS LHSOrPatSyn C.Pattern
| AmbiguousParseForLHS LHSOrPatSyn C.Pattern [C.Pattern]
| IFSNoCandidateInScope Type
| SafeFlagPostulate C.Name
| SafeFlagPragma [String]
| SafeFlagNoTerminationCheck
| SafeFlagPrimTrustMe
| NeedOptionCopatterns
deriving (Typeable, Show)
data LHSOrPatSyn = IsLHS | IsPatSyn deriving (Eq, 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)
instance Error TCErr where
noMsg = strMsg ""
strMsg = Exception noRange . strMsg
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 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 = returnTCMT
(>>=) = bindTCMT
(>>) = thenTCMT
fail = internalError
returnTCMT :: MonadIO m => a -> TCMT m a
returnTCMT = \x -> TCM $ \_ _ -> return x
bindTCMT :: MonadIO m => TCMT m a -> (a -> TCMT m b) -> TCMT m b
bindTCMT = \(TCM m) k -> TCM $ \r e -> m r e >>= \x -> unTCM (k x) r e
thenTCMT :: MonadIO m => TCMT m a -> TCMT m b -> TCMT m b
thenTCMT = \(TCM m1) (TCM m2) -> TCM $ \r e -> m1 r e >> m2 r e
instance MonadIO m => Functor (TCMT m) where
fmap = fmapTCMT
fmapTCMT :: MonadIO m => (a -> b) -> TCMT m a -> TCMT m b
fmapTCMT = \f (TCM m) -> TCM $ \r e -> liftM f (m r e)
instance MonadIO m => Applicative (TCMT m) where
pure = returnTCMT
(<*>) = apTCMT
apTCMT :: MonadIO m => TCMT m (a -> b) -> TCMT m a -> TCMT m b
apTCMT = \(TCM mf) (TCM m) -> TCM $ \r e -> ap (mf r e) (m r e)
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 $ IOException r e
handleException r s = throwIO $ Exception r s
patternViolation :: TCM a
patternViolation = do
s <- get
throwError $ 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 $ 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
forkTCM :: TCM a -> TCM ()
forkTCM m = do
s <- get
e <- ask
liftIO $ C.forkIO $ do
runTCM $ local (\_ -> e) $ do
put s
m
return ()
return ()
extendlambdaname = ".extendedlambda"