Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.TypeChecking.Monad.Base
Contents
- data TCState = TCSt {}
- class Monad m => ReadTCState m where
- data PreScopeState = PreScopeState {
- stPreTokens :: !CompressedFile
- stPreImports :: !Signature
- stPreImportedModules :: !(Set ModuleName)
- stPreModuleToSource :: !ModuleToSource
- stPreVisitedModules :: !VisitedModules
- stPreScope :: !ScopeInfo
- stPrePatternSyns :: !PatternSynDefns
- stPrePatternSynImports :: !PatternSynDefns
- stPrePragmaOptions :: !PragmaOptions
- stPreImportedBuiltins :: !(BuiltinThings PrimFun)
- stPreImportedDisplayForms :: !DisplayForms
- stPreImportedInstanceDefs :: !InstanceTable
- stPreHaskellImports :: !(Set String)
- stPreHaskellImportsUHC :: !(Set String)
- stPreHaskellCode :: ![String]
- stPreFreshInteractionId :: !InteractionId
- type DisambiguatedNames = IntMap QName
- data PostScopeState = PostScopeState {
- stPostSyntaxInfo :: !CompressedFile
- stPostDisambiguatedNames :: !DisambiguatedNames
- stPostMetaStore :: !MetaStore
- stPostInteractionPoints :: !InteractionPoints
- stPostSolvedInteractionPoints :: !InteractionPoints
- stPostAwakeConstraints :: !Constraints
- stPostSleepingConstraints :: !Constraints
- stPostDirty :: !Bool
- stPostOccursCheckDefs :: !(Set QName)
- stPostSignature :: !Signature
- stPostModuleParameters :: !ModuleParamDict
- stPostImportsDisplayForms :: !DisplayForms
- stPostCurrentModule :: !(Maybe ModuleName)
- stPostInstanceDefs :: !TempInstanceTable
- stPostStatistics :: !Statistics
- stPostTCWarnings :: ![TCWarning]
- stPostMutualBlocks :: !(Map MutualId MutualBlock)
- stPostLocalBuiltins :: !(BuiltinThings PrimFun)
- stPostFreshMetaId :: !MetaId
- stPostFreshMutualId :: !MutualId
- stPostFreshCtxId :: !CtxId
- stPostFreshProblemId :: !ProblemId
- stPostFreshInt :: !Int
- stPostFreshNameId :: !NameId
- data MutualBlock = MutualBlock {}
- data PersistentTCState = PersistentTCSt {}
- data LoadedFileCache = LoadedFileCache {}
- type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)]
- type CurrentTypeCheckLog = [(TypeCheckAction, PostScopeState)]
- data TypeCheckAction
- initPersistentState :: PersistentTCState
- initPreScopeState :: PreScopeState
- initPostScopeState :: PostScopeState
- initState :: TCState
- stTokens :: Lens' CompressedFile TCState
- stImports :: Lens' Signature TCState
- stImportedModules :: Lens' (Set ModuleName) TCState
- stModuleToSource :: Lens' ModuleToSource TCState
- stVisitedModules :: Lens' VisitedModules TCState
- stScope :: Lens' ScopeInfo TCState
- stPatternSyns :: Lens' PatternSynDefns TCState
- stPatternSynImports :: Lens' PatternSynDefns TCState
- stPragmaOptions :: Lens' PragmaOptions TCState
- stImportedBuiltins :: Lens' (BuiltinThings PrimFun) TCState
- stHaskellImports :: Lens' (Set String) TCState
- stHaskellImportsUHC :: Lens' (Set String) TCState
- stHaskellCode :: Lens' [String] TCState
- stFreshInteractionId :: Lens' InteractionId TCState
- stFreshNameId :: Lens' NameId TCState
- stSyntaxInfo :: Lens' CompressedFile TCState
- stDisambiguatedNames :: Lens' DisambiguatedNames TCState
- stMetaStore :: Lens' MetaStore TCState
- stInteractionPoints :: Lens' InteractionPoints TCState
- stSolvedInteractionPoints :: Lens' InteractionPoints TCState
- stAwakeConstraints :: Lens' Constraints TCState
- stSleepingConstraints :: Lens' Constraints TCState
- stDirty :: Lens' Bool TCState
- stOccursCheckDefs :: Lens' (Set QName) TCState
- stSignature :: Lens' Signature TCState
- stModuleParameters :: Lens' ModuleParamDict TCState
- stImportsDisplayForms :: Lens' DisplayForms TCState
- stImportedDisplayForms :: Lens' DisplayForms TCState
- stCurrentModule :: Lens' (Maybe ModuleName) TCState
- stImportedInstanceDefs :: Lens' InstanceTable TCState
- stInstanceDefs :: Lens' TempInstanceTable TCState
- stStatistics :: Lens' Statistics TCState
- stTCWarnings :: Lens' [TCWarning] TCState
- stMutualBlocks :: Lens' (Map MutualId MutualBlock) TCState
- stLocalBuiltins :: Lens' (BuiltinThings PrimFun) TCState
- stFreshMetaId :: Lens' MetaId TCState
- stFreshMutualId :: Lens' MutualId TCState
- stFreshCtxId :: Lens' CtxId TCState
- stFreshProblemId :: Lens' ProblemId TCState
- stFreshInt :: Lens' Int TCState
- stBuiltinThings :: TCState -> BuiltinThings PrimFun
- class Enum i => HasFresh i where
- nextFresh :: HasFresh i => TCState -> (i, TCState)
- fresh :: (HasFresh i, MonadState TCState m) => m i
- newtype ProblemId = ProblemId Nat
- freshName :: (MonadState TCState m, HasFresh NameId) => Range -> String -> m Name
- freshNoName :: (MonadState TCState m, HasFresh NameId) => Range -> m Name
- freshNoName_ :: (MonadState TCState m, HasFresh NameId) => m Name
- class FreshName a where
- type ModuleToSource = Map TopLevelModuleName AbsolutePath
- type SourceToModule = Map AbsolutePath TopLevelModuleName
- sourceToModule :: TCM SourceToModule
- lookupModuleFromSource :: AbsolutePath -> TCM (Maybe TopLevelModuleName)
- data ModuleInfo = ModuleInfo {}
- type VisitedModules = Map TopLevelModuleName ModuleInfo
- type DecodedModules = Map TopLevelModuleName Interface
- data Interface = Interface {
- iSourceHash :: Hash
- iImportedModules :: [(ModuleName, Hash)]
- iModuleName :: ModuleName
- iScope :: Map ModuleName Scope
- iInsideScope :: ScopeInfo
- iSignature :: Signature
- iDisplayForms :: DisplayForms
- iBuiltin :: BuiltinThings (String, QName)
- iHaskellImports :: Set String
- iHaskellImportsUHC :: Set String
- iHaskellCode :: [String]
- iHighlighting :: HighlightingInfo
- iPragmaOptions :: [OptionsPragma]
- iPatternSyns :: PatternSynDefns
- iFullHash :: Interface -> Hash
- 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
- | CheckSizeLtSat Term
- | FindInScope MetaId (Maybe MetaId) (Maybe [Candidate])
- data Comparison
- data CompareDirection
- fromCmp :: Comparison -> CompareDirection
- flipCmp :: CompareDirection -> CompareDirection
- dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
- data Open a = OpenThing {
- openThingCtxIds :: [CtxId]
- openThing :: a
- data Local a
- = Local ModuleName a
- | Global a
- isGlobal :: Local a -> Bool
- data Judgement a
- data MetaVariable = MetaVar {}
- data Listener
- data Frozen
- data MetaInstantiation
- data TypeCheckingProblem
- 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
- data InteractionPoint = InteractionPoint {}
- type InteractionPoints = Map InteractionId InteractionPoint
- data IPClause
- = IPClause { }
- | IPNoClause
- data Signature = Sig {}
- sigSections :: Lens' Sections Signature
- sigDefinitions :: Lens' Definitions Signature
- sigRewriteRules :: Lens' RewriteRuleMap Signature
- type Sections = Map ModuleName Section
- type Definitions = HashMap QName Definition
- type RewriteRuleMap = HashMap QName RewriteRules
- type DisplayForms = HashMap QName [LocalDisplayForm]
- data Section = Section {}
- secTelescope :: Lens' Telescope Section
- emptySignature :: Signature
- data DisplayForm = Display {
- dfFreeVars :: Nat
- dfPats :: Elims
- dfRHS :: DisplayTerm
- type LocalDisplayForm = Local DisplayForm
- data DisplayTerm
- = DWithApp DisplayTerm [DisplayTerm] Elims
- | DCon ConHead ConInfo [Arg DisplayTerm]
- | DDef QName [Elim' DisplayTerm]
- | DDot Term
- | DTerm Term
- defaultDisplayForm :: QName -> [LocalDisplayForm]
- defRelevance :: Definition -> Relevance
- data NLPat
- type PElims = [Elim' NLPat]
- data NLPType = NLPType {}
- type RewriteRules = [RewriteRule]
- data RewriteRule = RewriteRule {}
- data Definition = Defn {}
- theDefLens :: Lens' Defn Definition
- defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition
- type HaskellCode = String
- type HaskellType = String
- type EpicCode = String
- type JSCode = String
- data HaskellRepresentation
- data HaskellExport = HsExport HaskellType String
- data CoreRepresentation
- data Polarity
- data CompiledRepresentation = CompiledRep {}
- noCompiledRep :: CompiledRepresentation
- data ExtLamInfo = ExtLamInfo {}
- data Projection = Projection {}
- newtype ProjLams = ProjLams {
- getProjLams :: [Arg ArgName]
- projDropPars :: Projection -> ProjOrigin -> Term
- projArgInfo :: Projection -> ArgInfo
- data EtaEquality
- etaEqualityToBool :: EtaEquality -> Bool
- setEtaEquality :: EtaEquality -> Bool -> EtaEquality
- data FunctionFlag
- data Defn
- = Axiom
- | AbstractDefn
- | Function {
- funClauses :: [Clause]
- funCompiled :: Maybe CompiledClauses
- funTreeless :: Maybe Compiled
- funInv :: FunctionInverse
- funMutual :: [QName]
- funAbstr :: IsAbstract
- funDelayed :: Delayed
- funProjection :: Maybe Projection
- funFlags :: Set FunctionFlag
- funTerminates :: Maybe Bool
- funExtLam :: Maybe ExtLamInfo
- funWith :: Maybe QName
- funCopatternLHS :: Bool
- | Datatype {
- dataPars :: Nat
- dataSmallPars :: Permutation
- dataNonLinPars :: Drop Permutation
- dataIxs :: Nat
- dataInduction :: Induction
- dataClause :: Maybe Clause
- dataCons :: [QName]
- dataSort :: Sort
- dataMutual :: [QName]
- dataAbstr :: IsAbstract
- | Record {
- recPars :: Nat
- recClause :: Maybe Clause
- recConHead :: ConHead
- recNamedCon :: Bool
- recFields :: [Arg QName]
- recTel :: Telescope
- recMutual :: [QName]
- recEtaEquality' :: EtaEquality
- recInduction :: Maybe Induction
- recRecursive :: Bool
- recAbstr :: IsAbstract
- | Constructor { }
- | Primitive { }
- recEtaEquality :: Defn -> Bool
- emptyFunction :: Defn
- funFlag :: FunctionFlag -> Lens' Bool Defn
- funStatic :: Lens' Bool Defn
- funInline :: Lens' Bool Defn
- funMacro :: Lens' Bool Defn
- isMacro :: Defn -> Bool
- isEmptyFunction :: Defn -> Bool
- isCopatternLHS :: [Clause] -> Bool
- recCon :: Defn -> QName
- defIsRecord :: Defn -> Bool
- defIsDataOrRecord :: Defn -> Bool
- newtype Fields = Fields [(Name, Type)]
- data Simplification
- data Reduced no yes
- = NoReduction no
- | YesReduction Simplification yes
- data IsReduced
- = NotReduced
- | Reduced (Blocked ())
- data MaybeReduced a = MaybeRed {
- isReduced :: IsReduced
- ignoreReduced :: a
- type MaybeReducedArgs = [MaybeReduced (Arg Term)]
- type MaybeReducedElims = [MaybeReduced Elim]
- notReduced :: a -> MaybeReduced a
- reduced :: Blocked (Arg Term) -> MaybeReduced (Arg Term)
- data AllowedReduction
- type AllowedReductions = [AllowedReduction]
- allReductions :: AllowedReductions
- data PrimFun = PrimFun {
- primFunName :: QName
- primFunArity :: Arity
- primFunImplementation :: [Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term)
- defClauses :: Definition -> [Clause]
- defCompiled :: Definition -> Maybe CompiledClauses
- defParameters :: Definition -> Maybe Nat
- defJSDef :: Definition -> Maybe JSCode
- defEpicDef :: Definition -> Maybe EpicCode
- defCoreDef :: Definition -> Maybe CoreRepresentation
- defDelayed :: Definition -> Delayed
- defNonterminating :: 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 SpineClause
- | CheckPattern Pattern Telescope Type
- | CheckLetBinding LetBinding
- | InferExpr Expr
- | CheckExprCall Expr Type
- | CheckDotPattern Expr Term
- | CheckPatternShadowing SpineClause
- | CheckProjection Range QName Type
- | IsTypeCall Expr Sort
- | IsType_ Expr
- | InferVar Name
- | InferDef QName
- | CheckArguments Range [NamedArg Expr] Type Type
- | CheckDataDef Range Name [LamBinding] [Constructor]
- | CheckRecDef Range Name [LamBinding] [Constructor]
- | CheckConstructor QName Telescope Sort Constructor
- | CheckFunDef Range Name [Clause]
- | CheckPragma Range Pragma
- | CheckPrimitive Range Name Expr
- | CheckIsEmpty Range Type
- | CheckWithFunctionType Expr
- | CheckSectionApplication Range ModuleName ModuleApplication
- | ScopeCheckExpr Expr
- | ScopeCheckDeclaration NiceDeclaration
- | ScopeCheckLHS QName Pattern
- | NoHighlighting
- | ModuleContents
- | SetRange Range
- type InstanceTable = Map QName (Set QName)
- type TempInstanceTable = (InstanceTable, Set QName)
- data BuiltinDescriptor
- = BuiltinData (TCM Type) [String]
- | BuiltinDataCons (TCM Type)
- | BuiltinPrim String (Term -> TCM ())
- | BuiltinPostulate Relevance (TCM Type)
- | BuiltinUnknown (Maybe (TCM Type)) (Term -> Type -> TCM ())
- data BuiltinInfo = BuiltinInfo {}
- type BuiltinThings pf = Map String (Builtin pf)
- data Builtin pf
- data HighlightingLevel
- data HighlightingMethod
- ifTopLevelAndHighlightingLevelIs :: MonadTCM tcm => HighlightingLevel -> tcm () -> tcm ()
- data ModuleParameters = ModuleParams {}
- defaultModuleParameters :: ModuleParameters
- type ModuleParamDict = Map ModuleName ModuleParameters
- data TCEnv = TCEnv {
- envContext :: Context
- envLetBindings :: LetBindings
- envCurrentModule :: ModuleName
- envCurrentPath :: Maybe AbsolutePath
- envAnonymousModules :: [(ModuleName, Nat)]
- envImportPath :: [TopLevelModuleName]
- envMutualBlock :: Maybe MutualId
- envTerminationCheck :: TerminationCheck ()
- envSolvingConstraints :: Bool
- envCheckingWhere :: Bool
- envAssignMetas :: Bool
- envActiveProblems :: [ProblemId]
- envAbstractMode :: AbstractMode
- envRelevance :: Relevance
- envDisplayFormsEnabled :: Bool
- envRange :: Range
- envHighlightingRange :: Range
- envClause :: IPClause
- envCall :: Maybe (Closure Call)
- envHighlightingLevel :: HighlightingLevel
- envHighlightingMethod :: HighlightingMethod
- envModuleNestingLevel :: !Int
- envAllowDestructiveUpdate :: Bool
- envExpandLast :: ExpandHidden
- envAppDef :: Maybe QName
- envSimplification :: Simplification
- envAllowedReductions :: AllowedReductions
- envCompareBlocked :: Bool
- envPrintDomainFreePi :: Bool
- envPrintMetasBare :: Bool
- envInsideDotPattern :: Bool
- envUnquoteFlags :: UnquoteFlags
- envInstanceDepth :: !Int
- initEnv :: TCEnv
- disableDestructiveUpdate :: TCM a -> TCM a
- data UnquoteFlags = UnquoteFlags {}
- defaultUnquoteFlags :: UnquoteFlags
- unquoteNormalise :: Lens' Bool UnquoteFlags
- eUnquoteNormalise :: Lens' Bool TCEnv
- eContext :: Lens' Context TCEnv
- eLetBindings :: Lens' LetBindings TCEnv
- eCurrentModule :: Lens' ModuleName TCEnv
- eCurrentPath :: Lens' (Maybe AbsolutePath) TCEnv
- eAnonymousModules :: Lens' [(ModuleName, Nat)] TCEnv
- eImportPath :: Lens' [TopLevelModuleName] TCEnv
- eMutualBlock :: Lens' (Maybe MutualId) TCEnv
- eTerminationCheck :: Lens' (TerminationCheck ()) TCEnv
- eSolvingConstraints :: Lens' Bool TCEnv
- eCheckingWhere :: Lens' Bool TCEnv
- eAssignMetas :: Lens' Bool TCEnv
- eActiveProblems :: Lens' [ProblemId] TCEnv
- eAbstractMode :: Lens' AbstractMode TCEnv
- eRelevance :: Lens' Relevance TCEnv
- eDisplayFormsEnabled :: Lens' Bool TCEnv
- eRange :: Lens' Range TCEnv
- eHighlightingRange :: Lens' Range TCEnv
- eCall :: Lens' (Maybe (Closure Call)) TCEnv
- eHighlightingLevel :: Lens' HighlightingLevel TCEnv
- eHighlightingMethod :: Lens' HighlightingMethod TCEnv
- eModuleNestingLevel :: Lens' Int TCEnv
- eAllowDestructiveUpdate :: Lens' Bool TCEnv
- eExpandLast :: Lens' ExpandHidden TCEnv
- eAppDef :: Lens' (Maybe QName) TCEnv
- eSimplification :: Lens' Simplification TCEnv
- eAllowedReductions :: Lens' AllowedReductions TCEnv
- eCompareBlocked :: Lens' Bool TCEnv
- ePrintDomainFreePi :: Lens' Bool TCEnv
- eInsideDotPattern :: Lens' Bool TCEnv
- eUnquoteFlags :: Lens' UnquoteFlags TCEnv
- eInstanceDepth :: Lens' Int TCEnv
- type Context = [ContextEntry]
- data ContextEntry = Ctx {}
- newtype CtxId = CtxId Nat
- type LetBindings = Map Name (Open (Term, Dom Type))
- data AbstractMode
- aDefToMode :: IsAbstract -> AbstractMode
- aModeToDef :: AbstractMode -> IsAbstract
- data ExpandHidden
- data ExplicitToInstance
- data Candidate = Candidate {}
- data Warning
- data TCWarning = TCWarning {}
- tcWarning :: TCWarning -> Warning
- data CallInfo = CallInfo {}
- data TerminationError = TerminationError {
- termErrFunctions :: [QName]
- termErrCalls :: [CallInfo]
- data SplitError
- data UnquoteError
- 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]
- | CantResolveOverloadedConstructorsTargetingSameDatatype QName [QName]
- | DoesNotConstructAnElementOf QName Type
- | DifferentArities
- | WrongHidingInLHS
- | WrongHidingInLambda Type
- | WrongHidingInApplication Type
- | WrongNamedArgument (NamedArg Expr)
- | WrongIrrelevanceInLambda Type
- | WrongInstanceDeclaration
- | HidingMismatch Hiding Hiding
- | RelevanceMismatch Relevance Relevance
- | NotInductive Term
- | UninstantiatedDotPattern Expr
- | IlltypedPattern Pattern Type
- | IllformedProjectionPattern Pattern
- | CannotEliminateWithPattern (NamedArg Pattern) Type
- | TooManyArgumentsInLHS Type
- | WrongNumberOfConstructorArguments QName Nat Nat
- | ShouldBeEmpty Type [DeBruijnPattern]
- | ShouldBeASort Type
- | ShouldBePi Type
- | ShouldBeRecordType Type
- | ShouldBeRecordPattern DeBruijnPattern
- | NotAProjectionPattern (NamedArg Pattern)
- | NotAProperTerm
- | SetOmegaNotValidType
- | InvalidTypeSort Sort
- | InvalidType Term
- | FunctionTypeInSizeUniv Term
- | SplitOnIrrelevant Pattern (Dom Type)
- | DefinitionIsIrrelevant QName
- | VariableIsIrrelevant Name
- | UnequalTerms Comparison Term Term Type
- | UnequalTypes Comparison Type Type
- | 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
- | IllegalLetInTelescope TypedBinding
- | NoRHSRequiresAbsurdPattern [NamedArg Pattern]
- | AbsurdPatternRequiresNoRHS [NamedArg Pattern]
- | TooFewFields QName [Name]
- | TooManyFields QName [Name]
- | DuplicateFields [Name]
- | DuplicateConstructors [Name]
- | WithOnFreeVariable Expr Term
- | UnexpectedWithPatterns [Pattern]
- | WithClausePatternMismatch Pattern Pattern
- | FieldOutsideRecord
- | ModuleArityMismatch ModuleName Telescope [NamedArg Expr]
- | IncompletePatternMatching Term [Elim]
- | CoverageFailure QName [[NamedArg DeBruijnPattern]]
- | UnreachableClauses QName [[NamedArg DeBruijnPattern]]
- | CoverageCantSplitOn QName Telescope Args Args
- | CoverageCantSplitIrrelevantType Type
- | CoverageCantSplitType Type
- | CoverageNoExactSplit QName Clause
- | WithoutKError Type Term Term
- | UnifyConflict ConHead ConHead
- | UnifyCycle Int Term
- | UnifyIndicesNotVars Type Term Term Args
- | UnificationRecursiveEq Type Int Term
- | UnificationStuck Telescope [Term] [Term]
- | SplitError SplitError
- | TooManyPolarities QName Integer
- | LocalVsImportedModuleClash ModuleName
- | SolvedButOpenHoles
- | CyclicModuleDependency [TopLevelModuleName]
- | FileNotFound TopLevelModuleName [AbsolutePath]
- | OverlappingProjects AbsolutePath TopLevelModuleName TopLevelModuleName
- | AmbiguousTopLevelModuleName TopLevelModuleName [AbsolutePath]
- | ModuleNameUnexpected TopLevelModuleName TopLevelModuleName
- | 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
- | NotValidBeforeField NiceDeclaration
- | NothingAppliedToHiddenArg Expr
- | NothingAppliedToInstanceArg Expr
- | BadArgumentsToPatternSynonym QName
- | TooFewArgumentsToPatternSynonym QName
- | UnusedVariableInPatternSynonym
- | NoParseForApplication [Expr]
- | AmbiguousParseForApplication [Expr] [Expr]
- | NoParseForLHS LHSOrPatSyn Pattern
- | AmbiguousParseForLHS LHSOrPatSyn Pattern [Pattern]
- | OperatorInformation [NotationSection] TypeError
- | OperatorChangeMessage TypeError
- | IFSNoCandidateInScope Type
- | UnquoteFailed UnquoteError
- | DeBruijnIndexOutOfScope Nat Telescope [Name]
- | SafeFlagPostulate Name
- | SafeFlagPragma [String]
- | SafeFlagNonTerminating
- | SafeFlagTerminating
- | SafeFlagPrimTrustMe
- | SafeFlagNoPositivityCheck
- | SafeFlagPolarity
- | NeedOptionCopatterns
- | NeedOptionRewriting
- | NonFatalErrors [TCWarning]
- | InstanceSearchDepthExhausted Term Type Int
- data LHSOrPatSyn
- data TCErr
- data ReduceEnv = ReduceEnv {}
- mapRedEnv :: (TCEnv -> TCEnv) -> ReduceEnv -> ReduceEnv
- mapRedSt :: (TCState -> TCState) -> ReduceEnv -> ReduceEnv
- mapRedEnvSt :: (TCEnv -> TCEnv) -> (TCState -> TCState) -> ReduceEnv -> ReduceEnv
- newtype ReduceM a = ReduceM {}
- fmapReduce :: (a -> b) -> ReduceM a -> ReduceM b
- apReduce :: ReduceM (a -> b) -> ReduceM a -> ReduceM b
- bindReduce :: ReduceM a -> (a -> ReduceM b) -> ReduceM b
- runReduceM :: ReduceM a -> TCM a
- runReduceF :: (a -> ReduceM b) -> TCM (a -> b)
- newtype TCMT m a = TCM {}
- type TCM = TCMT IO
- class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm) => MonadTCM tcm where
- runPM :: PM a -> TCM a
- type IM = TCMT (InputT IO)
- runIM :: IM a -> TCM a
- catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a
- finally_ :: TCM a -> TCM b -> 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
- genericError :: MonadTCM tcm => String -> tcm a
- genericDocError :: MonadTCM tcm => Doc -> tcm a
- typeError :: MonadTCM tcm => TypeError -> tcm a
- typeError_ :: MonadTCM tcm => TypeError -> tcm TCErr
- warning_ :: MonadTCM tcm => Warning -> tcm TCWarning
- warning :: MonadTCM tcm => Warning -> tcm ()
- runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState)
- runTCMTop :: TCM a -> IO (Either TCErr a)
- runTCMTop' :: MonadIO m => TCMT m a -> m a
- runSafeTCM :: TCM a -> TCState -> IO (a, TCState)
- forkTCM :: TCM a -> TCM ()
- extendedLambdaName :: String
- absurdLambdaName :: String
- isAbsurdLambdaName :: QName -> Bool
Type checking state
Constructors
TCSt | |
Fields
|
class Monad m => ReadTCState m where #
Minimal complete definition
Methods
getTCState :: m TCState #
Instances
ReadTCState ReduceM # | |
MonadIO m => ReadTCState (TCMT m) # | |
data PreScopeState #
Constructors
PreScopeState | |
Fields
|
type DisambiguatedNames = IntMap QName #
data PostScopeState #
Constructors
PostScopeState | |
Fields
|
data MutualBlock #
A mutual block of names in the signature.
Constructors
MutualBlock | |
Fields
|
Instances
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 LoadedFileCache #
Constructors
LoadedFileCache | |
Fields |
type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)] #
A log of what the type checker does and states after the action is completed. The cached version is stored first executed action first.
type CurrentTypeCheckLog = [(TypeCheckAction, PostScopeState)] #
Like CachedTypeCheckLog
, but storing the log for an ongoing type
checking of a module. Stored in reverse order (last performed action
first).
data TypeCheckAction #
A complete log for a module will look like this:
Pragmas
EnterSection
, entering the main module.- 'Decl'/'EnterSection'/'LeaveSection', for declarations and nested modules
LeaveSection
, leaving the main module.
Constructors
EnterSection !ModuleInfo !ModuleName ![TypedBindings] | |
LeaveSection !ModuleName | |
Decl !Declaration | Never a Section or ScopeDecl |
Pragmas !PragmaOptions |
initPersistentState :: PersistentTCState #
Empty persistent state.
initPreScopeState :: PreScopeState #
Empty state of type checker.
st-prefixed lenses
stHaskellCode :: Lens' [String] TCState #
stTCWarnings :: Lens' [TCWarning] TCState #
stFreshInt :: Lens' Int TCState #
Fresh things
fresh :: (HasFresh i, MonadState TCState m) => m i #
freshNoName :: (MonadState TCState m, HasFresh NameId) => Range -> m Name #
freshNoName_ :: (MonadState TCState m, HasFresh NameId) => m Name #
Create a fresh name from a
.
Minimal complete definition
Methods
freshName_ :: (MonadState TCState m, HasFresh NameId) => a -> m Name #
Managing file names
type ModuleToSource = Map TopLevelModuleName AbsolutePath #
Maps top-level module names to the corresponding source file names.
type SourceToModule = Map AbsolutePath TopLevelModuleName #
Maps source file names to the corresponding top-level module names.
sourceToModule :: TCM SourceToModule #
Creates a SourceToModule
map based on stModuleToSource
.
O(n log n).
For a single reverse lookup in stModuleToSource
,
rather use lookupModuleFromSourse
.
lookupModuleFromSource :: AbsolutePath -> TCM (Maybe TopLevelModuleName) #
Lookup an AbsolutePath
in sourceToModule
.
O(n).
Interface
data ModuleInfo #
Constructors
ModuleInfo | |
Fields
|
Constructors
Interface | |
Fields
|
iFullHash :: Interface -> Hash #
Combines the source hash and the (full) hashes of the imported modules.
Closure
Constructors
Closure | |
Fields
|
Instances
Functor Closure # | |
Foldable Closure # | |
Show a => Show (Closure a) # | |
HasRange a => HasRange (Closure a) # | |
MentionsMeta a => MentionsMeta (Closure a) # | |
PrettyTCM a => PrettyTCM (Closure a) # | |
InstantiateFull a => InstantiateFull (Closure a) # | |
Normalise a => Normalise (Closure a) # | |
Simplify a => Simplify (Closure a) # | |
Reduce a => Reduce (Closure a) # | |
Instantiate a => Instantiate (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. |
CheckSizeLtSat Term | Check that the |
FindInScope MetaId (Maybe MetaId) (Maybe [Candidate]) | the first argument is the instance argument, the second one is the meta on which the constraint may be blocked on and the third one is the list of candidates (or Nothing if we haven’t determined the list of candidates yet) |
data Comparison #
Instances
fromCmp :: Comparison -> CompareDirection #
Embed Comparison
into CompareDirection
.
flipCmp :: CompareDirection -> CompareDirection #
Flip the direction of comparison.
dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c #
Turn a Comparison
function into a CompareDirection
function.
Property: dirToCmp f (fromCmp cmp) = f cmp
Open things
A thing tagged with the context it came from.
Constructors
OpenThing | |
Fields
|
Constructors
Local ModuleName a | Local to a given module, the value should have module parameters as free variables. |
Global a | Global value, should be closed. |
Judgements
Meta variables
data MetaVariable #
Constructors
MetaVar | |
Fields
|
Instances
Constructors
EtaExpand MetaId | |
CheckConstraint Nat ProblemConstraint |
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 [Arg String] Term | solved by term (abstracted over some free variables) |
Open | unsolved |
OpenIFS | open, to be instantiated as "implicit from scope" |
BlockedConst Term | solution blocked by unsolved constraints |
PostponedTypeCheckingProblem (Closure TypeCheckingProblem) (TCM Bool) |
Instances
data TypeCheckingProblem #
Constructors
CheckExpr Expr Type | |
CheckArgs ExpandHidden Range [NamedArg Expr] Type Type (Args -> Type -> TCM Term) | |
CheckLambda (Arg ([WithHiding Name], Maybe Type)) Expr Type |
|
UnquoteTactic Term Term Type | First argument is computation and the others are hole and goal type |
Instances
newtype MetaPriority #
Meta variable priority: When we have an equation between meta-variables, which one should be instantiated?
Higher value means higher priority to be instantiated.
Constructors
MetaPriority Int |
Instances
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.
For printing, we couple a meta with its name suggestion.
Constructors
NamedMeta | |
Fields |
type MetaStore = Map MetaId MetaVariable #
getMetaInfo :: MetaVariable -> Closure Range #
getMetaScope :: MetaVariable -> ScopeInfo #
getMetaEnv :: MetaVariable -> TCEnv #
getMetaSig :: MetaVariable -> Signature #
Interaction meta variables
data InteractionPoint #
Interaction points are created by the scope checker who sets the range. The meta variable is created by the type checker and then hooked up to the interaction point.
Constructors
InteractionPoint | |
Instances
type InteractionPoints = Map InteractionId InteractionPoint #
Data structure managing the interaction points.
Which clause is an interaction point located in?
Constructors
IPClause | |
IPNoClause | The interaction point is not in the rhs of a clause. |
Signature
Constructors
Sig | |
Fields
|
type Sections = Map ModuleName Section #
type Definitions = HashMap QName Definition #
type RewriteRuleMap = HashMap QName RewriteRules #
type DisplayForms = HashMap QName [LocalDisplayForm] #
Constructors
Section | |
Fields |
data DisplayForm #
A DisplayForm
is in essence a rewrite rule
q ts --> dt
for a defined symbol (could be a constructor as well) q
.
The right hand side is a DisplayTerm
which is used to
reify
to a more readable Syntax
.
The patterns ts
are just terms, but var 0
is interpreted
as a hole. Each occurrence of var 0
is a new hole (pattern var).
For each *occurrence* of var0
the rhs dt
has a free variable.
These are instantiated when matching a display form against a
term q vs
succeeds.
Constructors
Display | |
Fields
|
type LocalDisplayForm = Local DisplayForm #
data DisplayTerm #
Constructors
DWithApp DisplayTerm [DisplayTerm] Elims |
|
DCon ConHead ConInfo [Arg DisplayTerm] |
|
DDef QName [Elim' DisplayTerm] |
|
DDot Term |
|
DTerm Term |
|
defaultDisplayForm :: QName -> [LocalDisplayForm] #
By default, we have no display form.
defRelevance :: Definition -> Relevance #
Non-linear (non-constructor) first-order pattern.
Constructors
PVar (Maybe CtxId) !Int [Arg Int] | Matches anything (modulo non-linearity) that only contains bound variables that occur in the given arguments. |
PWild | Matches anything (e.g. irrelevant terms). |
PDef QName PElims | Matches |
PLam ArgInfo (Abs NLPat) | Matches |
PPi (Dom NLPType) (Abs NLPType) | Matches |
PBoundVar !Int PElims | Matches |
PTerm Term | Matches the term modulo β (ideally βη). |
Instances
Constructors
NLPType | |
Fields
|
type RewriteRules = [RewriteRule] #
data RewriteRule #
Rewrite rules can be added independently from function clauses.
Constructors
RewriteRule | |
data Definition #
Constructors
Defn | |
Fields
|
defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition #
Create a definition with sensible defaults.
type HaskellCode = String #
type HaskellType = String #
data CoreRepresentation #
Constructors
CrDefn CoreExpr | Core code for functions. |
CrType CoreType | Core type for agda type. |
CrConstr CoreConstr | Core constructor for agda constructor. |
Instances
Polarity for equality and subtype checking.
Constructors
Covariant | monotone |
Contravariant | antitone |
Invariant | no information (mixed variance) |
Nonvariant | constant |
data ExtLamInfo #
Additional information for extended lambdas.
Constructors
ExtLamInfo | |
Fields
|
Instances
data Projection #
Additional information for projection Function
s.
Constructors
Projection | |
Fields
|
Instances
Abstractions to build projection function (dropping parameters).
Constructors
ProjLams | |
Fields
|
projDropPars :: Projection -> ProjOrigin -> Term #
Building the projection function (which drops the parameters).
projArgInfo :: Projection -> ArgInfo #
The info of the principal (record) argument.
data EtaEquality #
Should a record type admit eta-equality?
Constructors
Specified !Bool | User specifed 'eta-equality' or 'no-eta-equality' |
Inferred !Bool | Positivity checker inferred whether eta is safe/ |
Instances
etaEqualityToBool :: EtaEquality -> Bool #
setEtaEquality :: EtaEquality -> Bool -> EtaEquality #
Make sure we do not overwrite a user specification.
data FunctionFlag #
Constructors
FunStatic | Should calls to this function be normalised at compile-time? |
FunInline | Should calls to this function be inlined by the compiler? |
FunMacro | Is this function a macro? |
Instances
Constructors
Axiom | Postulate. |
AbstractDefn | Returned by |
Function | |
Fields
| |
Datatype | |
Fields
| |
Record | |
Fields
| |
Constructor | |
Fields
| |
Primitive | Primitive or builtin functions. |
Fields
|
recEtaEquality :: Defn -> Bool #
emptyFunction :: Defn #
A template for creating Function
definitions, with sensible defaults.
isEmptyFunction :: Defn -> Bool #
Checking whether we are dealing with a function yet to be defined.
isCopatternLHS :: [Clause] -> Bool #
defIsRecord :: Defn -> Bool #
defIsDataOrRecord :: Defn -> Bool #
data Simplification #
Did we encounter a simplifying reduction? In terms of CIC, that would be a iota-reduction. In terms of Agda, this is a constructor or literal pattern that matched. Just beta-reduction (substitution) or delta-reduction (unfolding of definitions) does not count as simplifying?
Constructors
YesSimplification | |
NoSimplification |
Constructors
NoReduction no | |
YesReduction Simplification yes |
Three cases: 1. not reduced, 2. reduced, but blocked, 3. reduced, not blocked.
Constructors
NotReduced | |
Reduced (Blocked ()) |
data MaybeReduced a #
Constructors
MaybeRed | |
Fields
|
Instances
Functor MaybeReduced # | |
IsProjElim e => IsProjElim (MaybeReduced e) # | |
PrettyTCM a => PrettyTCM (MaybeReduced a) # | |
type MaybeReducedArgs = [MaybeReduced (Arg Term)] #
type MaybeReducedElims = [MaybeReduced Elim] #
notReduced :: a -> MaybeReduced a #
data AllowedReduction #
Controlling reduce
.
Constructors
ProjectionReductions | (Projection and) projection-like functions may be reduced. |
InlineReductions | Functions marked INLINE may be reduced. |
CopatternReductions | Copattern definitions may be reduced. |
FunctionReductions | Functions which are not projections may be reduced. |
LevelReductions | Reduce |
NonTerminatingReductions | Functions that have not passed termination checking. |
type AllowedReductions = [AllowedReduction] #
allReductions :: AllowedReductions #
Not quite all reductions (skip non-terminating reductions)
Constructors
PrimFun | |
Fields
|
defClauses :: Definition -> [Clause] #
defParameters :: Definition -> Maybe Nat #
defJSDef :: Definition -> Maybe JSCode #
defEpicDef :: Definition -> Maybe EpicCode #
defDelayed :: Definition -> Delayed #
Are the clauses of this definition delayed?
defNonterminating :: Definition -> Bool #
Has the definition failed the termination checker?
defAbstract :: Definition -> IsAbstract #
Injectivity
type FunctionInverse = FunctionInverse' Clause #
Mutual blocks
Statistics
type Statistics = Map String Integer #
Trace
Constructors
Instance table
type InstanceTable = Map QName (Set QName) #
The instance table is a Map
associating to every name of
recorddata typepostulate its list of instances
type TempInstanceTable = (InstanceTable, Set QName) #
When typechecking something of the following form:
instance x : _ x = y
it's not yet known where to add x
, so we add it to a list of
unresolved instances and we'll deal with it later.
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 -> Type -> TCM ()) | Builtin of any kind.
Type can be checked ( |
data BuiltinInfo #
Constructors
BuiltinInfo | |
Fields |
type BuiltinThings pf = Map String (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. |
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 ModuleParameters #
Constructors
ModuleParams | |
Fields
|
Instances
type ModuleParamDict #
Arguments
= Map ModuleName ModuleParameters | The map contains for each |
Constructors
TCEnv | |
Fields
|
Instances
MonadReader TCEnv ReduceM # | |
MonadReader TCEnv TerM # | |
MonadIO m => MonadReader TCEnv (TCMT m) # | |
disableDestructiveUpdate :: TCM a -> TCM a #
data UnquoteFlags #
Constructors
UnquoteFlags | |
Fields |
e-prefixed lenses
eCurrentPath :: Lens' (Maybe AbsolutePath) TCEnv #
eAnonymousModules :: Lens' [(ModuleName, Nat)] TCEnv #
eTerminationCheck :: Lens' (TerminationCheck ()) TCEnv #
eAssignMetas :: Lens' Bool TCEnv #
eActiveProblems :: Lens' [ProblemId] TCEnv #
eInstanceDepth :: Lens' Int TCEnv #
Context
type Context = [ContextEntry] #
The Context
is a stack of ContextEntry
s.
data ContextEntry #
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
aDefToMode :: IsAbstract -> AbstractMode #
aModeToDef :: AbstractMode -> IsAbstract #
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. |
Instances
data ExplicitToInstance #
Constructors
ExplicitToInstance | Explicit arguments are considered as instance arguments |
ExplicitStayExplicit |
Instances
A candidate solution for an instance meta is a term with its type. It may be the case that the candidate is not fully applied yet or of the wrong type, hence the need for the type.
Constructors
Candidate | |
Fields |
Type checking warnings (aka non-fatal errors)
A non-fatal error is an error which does not prevent us from checking the document further and interacting with the user.
Constructors
TerminationIssue [TerminationError] | |
NotStrictlyPositive QName OccursWhere | |
UnsolvedMetaVariables [Range] | Do not use directly with |
UnsolvedInteractionMetas [Range] | Do not use directly with |
UnsolvedConstraints Constraints | Do not use directly with |
OldBuiltin String String | In `OldBuiltin old new`, the BUILTIN old has been replaced by new |
EmptyRewritePragma | |
ParseWarning ParseWarning |
Constructors
TCWarning | |
Fields
|
Type checking errors
Information about a call.
Constructors
CallInfo | |
Fields
|
data TerminationError #
Information about a mutual block which did not pass the termination checker.
Constructors
TerminationError | |
Fields
|
Instances
data SplitError #
Error when splitting a pattern variable into possible constructor patterns.
Constructors
NotADatatype (Closure Type) | Neither data type nor record. |
IrrelevantDatatype (Closure Type) | Data type, but in irrelevant position. |
CoinductiveDatatype (Closure Type) | Split on codata not allowed. UNUSED, but keep! -- | NoRecordConstructor Type -- ^ record type, but no constructor |
CantSplit | |
Fields
| |
GenericSplitError String |
Instances
data UnquoteError #
Constructors
BadVisibility String (Arg Term) | |
ConInsteadOfDef QName String String | |
DefInsteadOfCon QName String String | |
NonCanonical String Term | |
BlockedOnMeta TCState MetaId | |
UnquotePanic String |
Instances
Constructors
Type-checking errors.
Constructors
TypeError | |
Fields
| |
Exception Range Doc | |
IOException Range IOException | |
PatternErr | The exception which is usually caught.
Raised for pattern violations during unification ( |
The reduce monad
Environment of the reduce monad.
Instances
fmapReduce :: (a -> b) -> ReduceM a -> ReduceM b #
bindReduce :: ReduceM a -> (a -> ReduceM b) -> ReduceM b #
runReduceM :: ReduceM a -> TCM a #
runReduceF :: (a -> ReduceM b) -> TCM (a -> b) #
Type checking monad transformer
Instances
MonadTrans TCMT # | |
MonadError TCErr IM # | |
MonadBench Phase TCM # | We store benchmark statistics in an IORef. This enables benchmarking pure computation, see Agda.Benchmarking. |
MonadError TCErr (TCMT IO) # | |
MonadIO m => MonadReader TCEnv (TCMT m) # | |
MonadIO m => MonadState TCState (TCMT m) # | |
MonadIO m => Monad (TCMT m) # | |
MonadIO m => Functor (TCMT m) # | |
MonadIO m => Applicative (TCMT m) # | |
Semigroup (TCM Any) # | Short-cutting disjunction forms a monoid. |
Monoid (TCM Any) # | |
MonadIO m => MonadIO (TCMT m) # | |
Null (TCM Doc) # | |
MonadIO m => MonadTCM (TCMT m) # | |
MonadIO m => ReadTCState (TCMT m) # | |
MonadIO m => HasOptions (TCMT m) # | |
MonadIO m => HasBuiltins (TCMT m) # | |
HasConstInfo (TCMT IO) # | |
class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm) => MonadTCM tcm where #
Minimal complete definition
Instances
MonadTCM TerM # | |
MonadTCM tcm => MonadTCM (MaybeT tcm) # | |
MonadTCM tcm => MonadTCM (ListT tcm) # | |
MonadIO m => MonadTCM (TCMT m) # | |
MonadTCM m => MonadTCM (CompileT m) # | |
MonadTCM tcm => MonadTCM (ExceptT err tcm) # | |
(Monoid w, MonadTCM tcm) => MonadTCM (WriterT w tcm) # | |
(Error err, MonadTCM tcm) => MonadTCM (ExceptionT err tcm) # | |
finally_ :: TCM a -> TCM b -> TCM a #
Execute a finalizer even when an exception is thrown. Does not catch any errors. In case both the regular computation and the finalizer throw an exception, the one of the finalizer is propagated.
returnTCMT :: MonadIO m => a -> TCMT m a #
patternViolation :: TCM a #
internalError :: MonadTCM tcm => String -> tcm a #
genericError :: MonadTCM tcm => String -> tcm a #
genericDocError :: MonadTCM tcm => Doc -> tcm a #
typeError_ :: MonadTCM tcm => TypeError -> tcm TCErr #
runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState) #
Running the type checking monad (most general form).
runTCMTop :: TCM a -> IO (Either TCErr a) #
Running the type checking monad on toplevel (with initial state).
runTCMTop' :: MonadIO m => TCMT m a -> m a #
runSafeTCM :: TCM a -> TCState -> IO (a, TCState) #
runSafeTCM
runs a safe TCM
action (a TCM
action which cannot fail)
in the initial environment.
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.
extendedLambdaName :: String #
Base name for extended lambda patterns
Name of absurdLambda definitions.
isAbsurdLambdaName :: QName -> Bool #
Check whether we have an definition from an absurd lambda.