Safe Haskell | None |
---|
Agda.TypeChecking.Monad.Base
Contents
- 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 :: PatternSynDefns
- stPatternSynImports :: 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 {}
- data FreshThings = Fresh {}
- initState :: TCState
- stBuiltinThings :: TCState -> BuiltinThings PrimFun
- newtype ProblemId = ProblemId Nat
- data ModuleInfo = ModuleInfo {}
- type VisitedModules = Map TopLevelModuleName ModuleInfo
- type DecodedModules = Map 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 :: PatternSynDefns
- data Closure a = Closure {}
- buildClosure :: a -> TCM (Closure a)
- type Constraints = [ProblemConstraint]
- data ProblemConstraint = PConstr {}
- 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)]
- data Comparison
- data Open a = OpenThing [CtxId] a
- data Judgement t a
- data MetaVariable = MetaVar {}
- data Listener
- data Frozen
- = Frozen
- | Instantiable
- data MetaInstantiation
- newtype MetaPriority = MetaPriority Int
- data RunMetaOccursCheck
- data MetaInfo = MetaInfo {}
- type MetaNameSuggestion = String
- data NamedMeta = NamedMeta {}
- type MetaStore = Map MetaId MetaVariable
- normalMetaPriority :: MetaPriority
- lowMetaPriority :: MetaPriority
- highMetaPriority :: MetaPriority
- getMetaInfo :: MetaVariable -> Closure Range
- getMetaScope :: MetaVariable -> ScopeInfo
- getMetaEnv :: MetaVariable -> TCEnv
- getMetaSig :: MetaVariable -> Signature
- getMetaRelevance :: MetaVariable -> Relevance
- type InteractionPoints = Map InteractionId MetaId
- newtype InteractionId = InteractionId Nat
- data Signature = Sig {}
- type Sections = Map ModuleName Section
- type Definitions = HashMap QName Definition
- data Section = Section {}
- emptySignature :: Signature
- data DisplayForm = Display Nat [Term] DisplayTerm
- data DisplayTerm
- = DWithApp [DisplayTerm] Args
- | DCon QName [Arg DisplayTerm]
- | DDef QName [Arg DisplayTerm]
- | DDot Term
- | DTerm Term
- defaultDisplayForm :: QName -> [Open DisplayForm]
- data Definition = Defn {}
- type HaskellCode = String
- type HaskellType = String
- type EpicCode = String
- type JSCode = Exp
- data HaskellRepresentation
- data Polarity
- = Covariant
- | Contravariant
- | Invariant
- | Nonvariant
- data CompiledRepresentation = CompiledRep {}
- noCompiledRep :: CompiledRepresentation
- data 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 QName]
- recTel :: Telescope
- recMutual :: [QName]
- recEtaEquality :: Bool
- recInduction :: Induction
- recRecursive :: Bool
- recAbstr :: IsAbstract
- | Constructor { }
- | Primitive { }
- defIsRecord :: Defn -> Bool
- defIsDataOrRecord :: Defn -> Bool
- newtype Fields = Fields [(Name, Type)]
- data Reduced no yes
- = NoReduction no
- | YesReduction yes
- data IsReduced
- = NotReduced
- | Reduced (Blocked ())
- data MaybeReduced a = MaybeRed {
- isReduced :: IsReduced
- ignoreReduced :: a
- type MaybeReducedArgs = [MaybeReduced (Arg Term)]
- notReduced :: a -> MaybeReduced a
- reduced :: Blocked (Arg Term) -> MaybeReduced (Arg Term)
- data PrimFun = PrimFun {
- primFunName :: QName
- primFunArity :: Arity
- primFunImplementation :: [Arg Term] -> TCM (Reduced MaybeReducedArgs Term)
- defClauses :: Definition -> [Clause]
- defCompiled :: Definition -> Maybe CompiledClauses
- defJSDef :: Definition -> Maybe JSCode
- defEpicDef :: Definition -> Maybe EpicCode
- defDelayed :: Definition -> Delayed
- defCopy :: Definition -> Bool
- defAbstract :: Definition -> IsAbstract
- type FunctionInverse = FunctionInverse' Clause
- data FunctionInverse' c
- = NotInjective
- | Inverse (Map TermHead c)
- data TermHead
- newtype MutualId = MutId Int32
- type Statistics = Map String Integer
- data Call
- = CheckClause Type Clause (Maybe Clause)
- | forall a . CheckPattern Pattern Telescope Type (Maybe a)
- | CheckLetBinding LetBinding (Maybe ())
- | InferExpr Expr (Maybe (Term, Type))
- | CheckExpr Expr Type (Maybe Term)
- | CheckDotPattern Expr Term (Maybe Constraints)
- | CheckPatternShadowing Clause (Maybe ())
- | IsTypeCall Expr Sort (Maybe Type)
- | IsType_ Expr (Maybe Type)
- | InferVar Name (Maybe (Term, Type))
- | InferDef Range QName (Maybe (Term, Type))
- | CheckArguments Range [NamedArg Expr] Type Type (Maybe (Args, Type))
- | CheckDataDef Range Name [LamBinding] [Constructor] (Maybe ())
- | CheckRecDef Range Name [LamBinding] [Constructor] (Maybe ())
- | CheckConstructor QName Telescope Sort Constructor (Maybe ())
- | CheckFunDef Range Name [Clause] (Maybe ())
- | CheckPragma Range Pragma (Maybe ())
- | CheckPrimitive Range Name Expr (Maybe ())
- | CheckIsEmpty Range Type (Maybe ())
- | CheckWithFunctionType Expr (Maybe ())
- | CheckSectionApplication Range ModuleName ModuleApplication (Maybe ())
- | ScopeCheckExpr Expr (Maybe Expr)
- | ScopeCheckDeclaration NiceDeclaration (Maybe [Declaration])
- | ScopeCheckLHS Name Pattern (Maybe LHS)
- | forall a . NoHighlighting (Maybe a)
- | forall a . SetRange Range (Maybe a)
- 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 {}
- type BuiltinThings pf = Map String (Builtin pf)
- data Builtin pf
- data HighlightingLevel
- = None
- | NonInteractive
- | Interactive
- data HighlightingMethod
- ifTopLevelAndHighlightingLevelIs :: MonadTCM tcm => HighlightingLevel -> tcm () -> tcm ()
- data TCEnv = TCEnv {
- envContext :: Context
- envLetBindings :: LetBindings
- envCurrentModule :: ModuleName
- envCurrentPath :: AbsolutePath
- envAnonymousModules :: [(ModuleName, Nat)]
- envImportPath :: [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
- initEnv :: TCEnv
- type Context = [ContextEntry]
- data ContextEntry = Ctx {}
- newtype CtxId = CtxId Nat
- type LetBindings = Map Name (Open (Term, Dom Type))
- data AbstractMode
- data ExpandHidden
- data ExpandInstances
- data Occ
- = OccCon { }
- | OccClause {
- occFunction :: QName
- occClause :: Int
- occPosition :: OccPos
- data OccPos
- data CallInfo = CallInfo {}
- data TerminationError = TerminationError {
- termErrFunctions :: [QName]
- termErrCalls :: [CallInfo]
- 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 Expr
- | IlltypedPattern Pattern Type
- | TooManyArgumentsInLHS Type
- | WrongNumberOfConstructorArguments QName Nat Nat
- | ShouldBeEmpty Type [Pattern]
- | ShouldBeASort Type
- | ShouldBePi Type
- | ShouldBeRecordType Type
- | ShouldBeRecordPattern Pattern
- | NotAProperTerm
- | SetOmegaNotValidType
- | SplitOnIrrelevant 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 Expr
- | NoSuchBuiltinName String
- | DuplicateBuiltinBinding String Term Term
- | NoBindingForBuiltin String
- | NoSuchPrimitiveFunction String
- | ShadowedModule Name [ModuleName]
- | BuiltinInParameterisedModule String
- | NoRHSRequiresAbsurdPattern [NamedArg Pattern]
- | AbsurdPatternRequiresNoRHS [NamedArg Pattern]
- | TooFewFields QName [Name]
- | TooManyFields QName [Name]
- | DuplicateFields [Name]
- | DuplicateConstructors [Name]
- | UnexpectedWithPatterns [Pattern]
- | WithClausePatternMismatch Pattern Pattern
- | FieldOutsideRecord
- | ModuleArityMismatch ModuleName Telescope [NamedArg 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 [TopLevelModuleName]
- | FileNotFound TopLevelModuleName [AbsolutePath]
- | OverlappingProjects AbsolutePath TopLevelModuleName TopLevelModuleName
- | AmbiguousTopLevelModuleName TopLevelModuleName [AbsolutePath]
- | ModuleNameDoesntMatchFileName TopLevelModuleName [AbsolutePath]
- | ClashingFileNamesFor ModuleName [AbsolutePath]
- | ModuleDefinedInOtherFile TopLevelModuleName AbsolutePath AbsolutePath
- | BothWithAndRHS
- | NotInScope [QName]
- | NoSuchModule QName
- | AmbiguousName QName [QName]
- | AmbiguousModule QName [ModuleName]
- | UninstantiatedModule QName
- | ClashingDefinition QName QName
- | ClashingModule ModuleName ModuleName
- | ClashingImport Name QName
- | ClashingModuleImport Name ModuleName
- | PatternShadowsConstructor Name QName
- | ModuleDoesntExport QName [ImportedName]
- | DuplicateImports QName [ImportedName]
- | InvalidPattern Pattern
- | RepeatedVariablesInPattern [Name]
- | NotAModuleExpr Expr
- | NotAnExpression Expr
- | NotAValidLetBinding NiceDeclaration
- | NothingAppliedToHiddenArg Expr
- | NothingAppliedToInstanceArg Expr
- | UnusedVariableInPatternSynonym
- | PatternSynonymArityMismatch QName
- | NoParseForApplication [Expr]
- | AmbiguousParseForApplication [Expr] [Expr]
- | NoParseForLHS LHSOrPatSyn Pattern
- | AmbiguousParseForLHS LHSOrPatSyn Pattern [Pattern]
- | IFSNoCandidateInScope Type
- | SafeFlagPostulate Name
- | SafeFlagPragma [String]
- | SafeFlagNoTerminationCheck
- | SafeFlagPrimTrustMe
- | NeedOptionCopatterns
- data LHSOrPatSyn
- data TCErr
- newtype TCMT m a = TCM {}
- type TCM = TCMT IO
- class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm) => MonadTCM tcm where
- catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a
- mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a
- pureTCM :: MonadIO m => (TCState -> TCEnv -> a) -> TCMT m a
- returnTCMT :: MonadIO m => a -> TCMT m a
- bindTCMT :: MonadIO m => TCMT m a -> (a -> TCMT m b) -> TCMT m b
- thenTCMT :: MonadIO m => TCMT m a -> TCMT m b -> TCMT m b
- fmapTCMT :: MonadIO m => (a -> b) -> TCMT m a -> TCMT m b
- apTCMT :: MonadIO m => TCMT m (a -> b) -> TCMT m a -> TCMT m b
- patternViolation :: TCM a
- internalError :: MonadTCM tcm => String -> tcm a
- typeError :: MonadTCM tcm => TypeError -> tcm a
- runTCM :: TCMT IO a -> IO (Either TCErr a)
- runTCM' :: MonadIO m => TCMT m a -> m a
- forkTCM :: TCM a -> TCM ()
- extendlambdaname :: [Char]
Type checking state
data TCState
Constructors
Instances
MonadState TCState Unify | |
HasFresh i FreshThings => HasFresh i TCState | |
MonadIO m => MonadState TCState (TCMT m) |
data PersistentTCState
A part of the state which is not reverted when an error is thrown or the state is reset.
Constructors
PersistentTCSt | |
Fields
|
data FreshThings
Constructors
Fresh | |
newtype ProblemId
Interface
data ModuleInfo
Constructors
ModuleInfo | |
Fields
|
type DecodedModules = Map TopLevelModuleName (Interface, ClockTime)
data Interface
Constructors
Interface | |
Fields
|
Closure
data Closure a
Instances
Typeable1 Closure | |
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) | |
Show a => Show (Closure a) | |
HasRange a => HasRange (Closure a) | |
PrettyTCM a => PrettyTCM (Closure a) | |
InstantiateFull a => InstantiateFull (Closure a) | |
Normalise a => Normalise (Closure a) | |
Reduce a => Reduce (Closure a) | |
Instantiate a => Instantiate (Closure a) | |
MentionsMeta a => MentionsMeta (Closure a) |
buildClosure :: a -> TCM (Closure a)
Constraints
type Constraints = [ProblemConstraint]
data ProblemConstraint
Constructors
PConstr | |
Fields |
data Constraint
Constructors
ValueCmp Comparison Type Term Term | |
ElimCmp [Polarity] Type Term [Elim] [Elim] | |
TypeCmp Comparison Type Type | |
TelCmp Type Type Comparison Telescope Telescope | the two types are for the error message only |
SortCmp Comparison Sort Sort | |
LevelCmp Comparison Level Level | |
UnBlock MetaId | |
Guarded Constraint ProblemId | |
IsEmpty Range Type | the range is the one of the absurd pattern |
FindInScope MetaId [(Term, Type)] |
data Comparison
Instances
Open things
data Open a
A thing tagged with the context it came from.
Judgements
data Judgement t a
Meta variables
data MetaVariable
Constructors
MetaVar | |
Fields
|
data Listener
Constructors
EtaExpand MetaId | |
CheckConstraint Nat ProblemConstraint |
data Frozen
Frozen meta variable cannot be instantiated by unification. This serves to prevent the completion of a definition by its use outside of the current block. (See issues 118, 288, 399).
Constructors
Frozen | Do not instantiate. |
Instantiable |
data MetaInstantiation
Constructors
InstV Term | solved by term |
InstS Term | solved by |
Open | unsolved |
OpenIFS | open, to be instantiated as implicit from scope |
BlockedConst Term | solution blocked by unsolved constraints |
PostponedTypeCheckingProblem (Closure (Expr, Type, TCM Bool)) |
Instances
data RunMetaOccursCheck
Constructors
RunMetaOccursCheck | |
DontRunMetaOccursCheck |
data MetaInfo
MetaInfo
is cloned from one meta to the next during pruning.
Constructors
MetaInfo | |
Fields
|
type MetaNameSuggestion = String
Name suggestion for meta variable. Empty string means no suggestion.
data NamedMeta
For printing, we couple a meta with its name suggestion.
Constructors
NamedMeta | |
Fields |
Instances
type MetaStore = Map MetaId MetaVariable
getMetaInfo :: MetaVariable -> Closure Range
getMetaEnv :: MetaVariable -> TCEnv
getMetaSig :: MetaVariable -> Signature
Interaction meta variables
type InteractionPoints = Map InteractionId MetaId
newtype InteractionId
Constructors
InteractionId Nat |
Signature
type Sections = Map ModuleName Section
type Definitions = HashMap QName Definition
data Section
Constructors
Section | |
Fields
|
data DisplayForm
Constructors
Display Nat [Term] DisplayTerm | The three arguments are:
|
data DisplayTerm
Constructors
DWithApp [DisplayTerm] Args | |
DCon QName [Arg DisplayTerm] | |
DDef QName [Arg DisplayTerm] | |
DDot Term | |
DTerm Term |
defaultDisplayForm :: QName -> [Open DisplayForm]
data Definition
Constructors
Defn | |
Fields
|
type HaskellCode = String
type HaskellType = String
Constructors
HsDefn HaskellType HaskellCode | |
HsType HaskellType |
data Polarity
Polarity for equality and subtype checking.
Constructors
Covariant | monotone |
Contravariant | antitone |
Invariant | no information (mixed variance) |
Nonvariant | constant |
Constructors
CompiledRep | |
Fields |
data Occurrence
Subterm occurrences for positivity checking.
The constructors are listed in increasing information they provide:
Mixed <= JustPos <= StrictPos <= GuardPos <= Unused
Mixed <= JustNeg <= Unused
.
Constructors
Mixed | Arbitrary occurrence (positive and negative). |
JustNeg | Negative occurrence. |
JustPos | Positive occurrence, but not strictly positive. |
StrictPos | Strictly positive occurrence. |
GuardPos | Guarded strictly positive occurrence (i.e., under ∞). For checking recursive records. |
Unused |
Instances
Eq Occurrence | |
Ord Occurrence | |
Show Occurrence | |
Typeable Occurrence | |
NFData Occurrence | |
SemiRing Occurrence |
It forms a commutative semiring where For |
PrettyTCM Occurrence | |
EmbPrj Occurrence | |
Abstract [Occurrence] | |
Apply [Occurrence] | |
PrettyTCM n => PrettyTCM (n, Occurrence) |
data Defn
Constructors
Axiom | |
Function | |
Fields
| |
Datatype | |
Fields
| |
Record | |
Fields
| |
Constructor | |
Primitive | Primitive or builtin functions. |
Fields
|
defIsRecord :: Defn -> Bool
defIsDataOrRecord :: Defn -> Bool
data Reduced no yes
Constructors
NoReduction no | |
YesReduction yes |
data IsReduced
Constructors
NotReduced | |
Reduced (Blocked ()) |
type MaybeReducedArgs = [MaybeReduced (Arg Term)]
notReduced :: a -> MaybeReduced a
data PrimFun
Constructors
PrimFun | |
Fields
|
defClauses :: Definition -> [Clause]
defJSDef :: Definition -> Maybe JSCode
defEpicDef :: Definition -> Maybe EpicCode
defDelayed :: Definition -> Delayed
Are the clauses of this definition delayed?
defCopy :: Definition -> Bool
Is the definition just a copy created by a module instantiation?
defAbstract :: Definition -> IsAbstract
Injectivity
data FunctionInverse' c
Constructors
NotInjective | |
Inverse (Map TermHead c) |
data TermHead
Mutual blocks
newtype MutualId
Statistics
type Statistics = Map String Integer
Trace
data Call
Constructors
Builtin things
data BuiltinDescriptor
Constructors
BuiltinData (TCM Type) [String] | |
BuiltinDataCons (TCM Type) | |
BuiltinPrim String (Term -> TCM ()) | |
BuiltinPostulate Relevance (TCM Type) | |
BuiltinUnknown (Maybe (TCM Type)) (Term -> TCM ()) |
data BuiltinInfo
Constructors
BuiltinInfo | |
Fields |
type BuiltinThings pf = Map String (Builtin pf)
data Builtin pf
Highlighting levels
data HighlightingLevel
How much highlighting should be sent to the user interface?
Constructors
None | |
NonInteractive | |
Interactive | This includes both non-interactive highlighting and interactive highlighting of the expression that is currently being type-checked. |
data HighlightingMethod
How should highlighting be sent to the user interface?
ifTopLevelAndHighlightingLevelIs :: MonadTCM tcm => HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs l m
runs m
when we're
type-checking the top-level module and the highlighting level is
at least l
.
Type checking environment
data TCEnv
Constructors
TCEnv | |
Fields
|
Instances
Typeable TCEnv | |
MonadReader TCEnv Unify | |
MonadIO m => MonadReader TCEnv (TCMT m) |
Context
type Context = [ContextEntry]
The Context
is a stack of ContextEntry
s.
data ContextEntry
Instances
newtype CtxId
Let bindings
Abstract mode
data AbstractMode
Constructors
AbstractMode | abstract things in the current module can be accessed |
ConcreteMode | no abstract things can be accessed |
IgnoreAbstractMode | all abstract things can be accessed |
Instances
Insertion of implicit arguments
data ExpandHidden
Constructors
ExpandLast | Add implicit arguments in the end until type is no longer hidden |
DontExpandLast | Do not append implicit arguments. |
Type checking errors
data Occ
Constructors
OccCon | |
Fields
| |
OccClause | |
Fields
|
data CallInfo
Information about a call.
Constructors
CallInfo | |
Fields
|
data TerminationError
Information about a mutual block which did not pass the termination checker.
Constructors
TerminationError | |
Fields
|
data TypeError
Constructors
data TCErr
Type-checking errors.
Constructors
TypeError TCState (Closure TypeError) | |
Exception Range String | |
IOException Range IOException | |
PatternErr TCState | for pattern violations |
Type checking monad transformer
newtype TCMT m a
Instances
class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm) => MonadTCM tcm where
catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a
Preserve the state of the failing computation.
returnTCMT :: MonadIO m => a -> TCMT m a
patternViolation :: TCM a
internalError :: MonadTCM tcm => String -> tcm a
Runs the given computation in a separate thread, with a copy of the current state and environment.
Note that Agda sometimes uses actual, mutable state. If the
computation given to forkTCM
tries to modify this state, then
bad things can happen, because accesses are not mutually exclusive.
The forkTCM
function has been added mainly to allow the thread to
read (a snapshot of) the current state in a convenient way.
Note also that exceptions which are raised in the thread are not propagated to the parent, so the thread should not do anything important.
extendlambdaname :: [Char]
Base name for extended lambda patterns