Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.TypeChecking.Monad.Base
Contents
- Type checking state
- st-prefixed lenses
- Fresh things
- Open things
- Judgements
- Highlighting levels
- Type checking environment
- e-prefixed lenses
- Type checking warnings (aka non-fatal errors)
- Type checking errors
- Accessing options
- The reduce monad
- Monad with read-only
TCEnv
- Monad with mutable
TCState
- Type checking monad transformer
- KillRange instances
Synopsis
- data TCState = TCSt {}
- class Monad m => ReadTCState m where
- getTCState :: m TCState
- withTCState :: (TCState -> TCState) -> m a -> m a
- data PreScopeState = PreScopeState {
- stPreTokens :: !CompressedFile
- stPreImports :: !Signature
- stPreImportedModules :: !(Set ModuleName)
- stPreModuleToSource :: !ModuleToSource
- stPreVisitedModules :: !VisitedModules
- stPreScope :: !ScopeInfo
- stPrePatternSyns :: !PatternSynDefns
- stPrePatternSynImports :: !PatternSynDefns
- stPreGeneralizedVars :: !(Maybe (Set QName))
- stPrePragmaOptions :: !PragmaOptions
- stPreImportedBuiltins :: !(BuiltinThings PrimFun)
- stPreImportedDisplayForms :: !DisplayForms
- stPreImportedInstanceDefs :: !InstanceTable
- stPreForeignCode :: !(Map BackendName [ForeignCode])
- stPreFreshInteractionId :: !InteractionId
- stPreImportedUserWarnings :: !(Map QName String)
- stPreLocalUserWarnings :: !(Map QName String)
- type DisambiguatedNames = IntMap QName
- data PostScopeState = PostScopeState {
- stPostSyntaxInfo :: !CompressedFile
- stPostDisambiguatedNames :: !DisambiguatedNames
- stPostMetaStore :: !MetaStore
- stPostInteractionPoints :: !InteractionPoints
- stPostAwakeConstraints :: !Constraints
- stPostSleepingConstraints :: !Constraints
- stPostDirty :: !Bool
- stPostOccursCheckDefs :: !(Set QName)
- stPostSignature :: !Signature
- stPostModuleCheckpoints :: !(Map ModuleName CheckpointId)
- stPostImportsDisplayForms :: !DisplayForms
- stPostCurrentModule :: !(Maybe ModuleName)
- stPostInstanceDefs :: !TempInstanceTable
- stPostConcreteNames :: !(Map Name [Name])
- stPostShadowingNames :: !(Map Name [Name])
- stPostStatistics :: !Statistics
- stPostTCWarnings :: ![TCWarning]
- stPostMutualBlocks :: !(Map MutualId MutualBlock)
- stPostLocalBuiltins :: !(BuiltinThings PrimFun)
- stPostFreshMetaId :: !MetaId
- stPostFreshMutualId :: !MutualId
- stPostFreshProblemId :: !ProblemId
- stPostFreshCheckpointId :: !CheckpointId
- stPostFreshInt :: !Int
- stPostFreshNameId :: !NameId
- stPostAreWeCaching :: !Bool
- stPostConsideringInstance :: !Bool
- data MutualBlock = MutualBlock {
- mutualInfo :: MutualInfo
- mutualNames :: Set QName
- 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
- stGeneralizedVars :: Lens' (Maybe (Set QName)) TCState
- stPragmaOptions :: Lens' PragmaOptions TCState
- stImportedBuiltins :: Lens' (BuiltinThings PrimFun) TCState
- stForeignCode :: Lens' (Map BackendName [ForeignCode]) TCState
- stFreshInteractionId :: Lens' InteractionId TCState
- stImportedUserWarnings :: Lens' (Map QName String) TCState
- stLocalUserWarnings :: Lens' (Map QName String) TCState
- getUserWarnings :: MonadTCState m => m (Map QName String)
- stBackends :: Lens' [Backend] TCState
- stFreshNameId :: Lens' NameId TCState
- stSyntaxInfo :: Lens' CompressedFile TCState
- stDisambiguatedNames :: Lens' DisambiguatedNames TCState
- stMetaStore :: Lens' MetaStore TCState
- stInteractionPoints :: Lens' InteractionPoints TCState
- stAwakeConstraints :: Lens' Constraints TCState
- stSleepingConstraints :: Lens' Constraints TCState
- stDirty :: Lens' Bool TCState
- stOccursCheckDefs :: Lens' (Set QName) TCState
- stSignature :: Lens' Signature TCState
- stModuleCheckpoints :: Lens' (Map ModuleName CheckpointId) TCState
- stImportsDisplayForms :: Lens' DisplayForms TCState
- stImportedDisplayForms :: Lens' DisplayForms TCState
- stCurrentModule :: Lens' (Maybe ModuleName) TCState
- stImportedInstanceDefs :: Lens' InstanceTable TCState
- stInstanceDefs :: Lens' TempInstanceTable TCState
- stConcreteNames :: Lens' (Map Name [Name]) TCState
- stShadowingNames :: Lens' (Map Name [Name]) 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
- stFreshProblemId :: Lens' ProblemId TCState
- stFreshCheckpointId :: Lens' CheckpointId TCState
- stFreshInt :: Lens' Int TCState
- stAreWeCaching :: Lens' Bool TCState
- stConsideringInstance :: Lens' Bool TCState
- stBuiltinThings :: TCState -> BuiltinThings PrimFun
- class Enum i => HasFresh i where
- freshLens :: Lens' i TCState
- nextFresh' :: i -> i
- nextFresh :: HasFresh i => TCState -> (i, TCState)
- fresh :: (HasFresh i, MonadTCState m) => m i
- newtype ProblemId = ProblemId Nat
- newtype CheckpointId = CheckpointId Int
- freshName :: MonadTCState m => Range -> String -> m Name
- freshNoName :: MonadTCState m => Range -> m Name
- freshNoName_ :: MonadTCState m => m Name
- freshRecordName :: MonadTCState m => m Name
- class FreshName a where
- freshName_ :: MonadTCState m => a -> m Name
- type ModuleToSource = Map TopLevelModuleName AbsolutePath
- type SourceToModule = Map AbsolutePath TopLevelModuleName
- sourceToModule :: TCM SourceToModule
- lookupModuleFromSource :: AbsolutePath -> TCM (Maybe TopLevelModuleName)
- data ModuleInfo = ModuleInfo {
- miInterface :: Interface
- miWarnings :: Bool
- miPrimitive :: Bool
- type VisitedModules = Map TopLevelModuleName ModuleInfo
- type DecodedModules = Map TopLevelModuleName Interface
- data ForeignCode = ForeignCode Range String
- data Interface = Interface {
- iSourceHash :: Hash
- iSource :: Text
- iFileType :: FileType
- iImportedModules :: [(ModuleName, Hash)]
- iModuleName :: ModuleName
- iScope :: Map ModuleName Scope
- iInsideScope :: ScopeInfo
- iSignature :: Signature
- iDisplayForms :: DisplayForms
- iUserWarnings :: Map QName String
- iBuiltin :: BuiltinThings (String, QName)
- iForeignCode :: Map BackendName [ForeignCode]
- iHighlighting :: HighlightingInfo
- iPragmaOptions :: [OptionsPragma]
- iOptionsUsed :: PragmaOptions
- iPatternSyns :: PatternSynDefns
- iWarnings :: [TCWarning]
- iFullHash :: Interface -> Hash
- data Closure a = Closure {
- clSignature :: Signature
- clEnv :: TCEnv
- clScope :: ScopeInfo
- clModuleCheckpoints :: Map ModuleName CheckpointId
- clValue :: a
- buildClosure :: a -> TCM (Closure a)
- type Constraints = [ProblemConstraint]
- data ProblemConstraint = PConstr {}
- data Constraint
- = ValueCmp Comparison Type Term Term
- | ValueCmpOnFace Comparison Term Type Term Term
- | ElimCmp [Polarity] [IsForced] Type Term [Elim] [Elim]
- | TypeCmp Comparison Type Type
- | TelCmp Type Type Comparison Telescope Telescope
- | SortCmp Comparison Sort Sort
- | LevelCmp Comparison Level Level
- | HasBiggerSort Sort
- | HasPTSRule Sort (Abs Sort)
- | UnBlock MetaId
- | Guarded Constraint ProblemId
- | IsEmpty Range Type
- | CheckSizeLtSat Term
- | FindInstance MetaId (Maybe MetaId) (Maybe [Candidate])
- | CheckFunDef Delayed DefInfo QName [Clause]
- | UnquoteTactic (Maybe MetaId) Term Term Type
- data Comparison
- data CompareDirection
- fromCmp :: Comparison -> CompareDirection
- flipCmp :: CompareDirection -> CompareDirection
- dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
- data Open a = OpenThing {}
- data Judgement a
- data DoGeneralize
- data GeneralizedValue = GeneralizedValue {}
- data MetaVariable = MetaVar {}
- data Listener
- data Frozen
- data MetaInstantiation
- = InstV [Arg String] Term
- | Open
- | OpenInstance
- | BlockedConst Term
- | PostponedTypeCheckingProblem (Closure TypeCheckingProblem) (TCM Bool)
- data CheckedTarget
- = CheckedTarget (Maybe ProblemId)
- | NotCheckedTarget
- data TypeCheckingProblem
- = CheckExpr Comparison Expr Type
- | CheckArgs ExpandHidden Range [NamedArg Expr] Type Type ([Maybe Range] -> Elims -> Type -> CheckedTarget -> TCM Term)
- | CheckProjAppToKnownPrincipalArg Comparison Expr ProjOrigin (NonemptyList QName) Args Type Int Term Type
- | CheckLambda Comparison (Arg ([WithHiding Name], Maybe Type)) Expr Type
- | DoQuoteTerm Comparison Term Type
- newtype MetaPriority = MetaPriority Int
- data RunMetaOccursCheck
- data MetaInfo = MetaInfo {}
- type MetaNameSuggestion = String
- data NamedMeta = NamedMeta {}
- type MetaStore = IntMap MetaVariable
- normalMetaPriority :: MetaPriority
- lowMetaPriority :: MetaPriority
- highMetaPriority :: MetaPriority
- getMetaInfo :: MetaVariable -> Closure Range
- getMetaScope :: MetaVariable -> ScopeInfo
- getMetaEnv :: MetaVariable -> TCEnv
- getMetaSig :: MetaVariable -> Signature
- getMetaRelevance :: MetaVariable -> Relevance
- getMetaModality :: MetaVariable -> Modality
- metaFrozen :: Lens' Frozen MetaVariable
- data InteractionPoint = InteractionPoint {}
- type InteractionPoints = Map InteractionId InteractionPoint
- data IPClause
- = IPClause {
- ipcQName :: QName
- ipcClauseNo :: Int
- ipcClause :: RHS
- | IPNoClause
- = IPClause {
- 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]
- newtype Section = Section {}
- secTelescope :: Lens' Telescope Section
- emptySignature :: Signature
- data DisplayForm = Display {
- dfFreeVars :: Nat
- dfPats :: Elims
- dfRHS :: DisplayTerm
- type LocalDisplayForm = Open 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 {
- defArgInfo :: ArgInfo
- defName :: QName
- defType :: Type
- defPolarity :: [Polarity]
- defArgOccurrences :: [Occurrence]
- defArgGeneralizable :: NumGeneralizableArgs
- defGeneralizedParams :: [Maybe Name]
- defDisplay :: [LocalDisplayForm]
- defMutual :: MutualId
- defCompiledRep :: CompiledRepresentation
- defInstance :: Maybe QName
- defCopy :: Bool
- defMatchable :: Bool
- defNoCompilation :: Bool
- defInjective :: Bool
- theDef :: Defn
- data NumGeneralizableArgs
- theDefLens :: Lens' Defn Definition
- defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition
- data Polarity
- data IsForced
- data CompilerPragma = CompilerPragma Range String
- type BackendName = String
- jsBackendName :: BackendName
- ghcBackendName :: BackendName
- type CompiledRepresentation = Map BackendName [CompilerPragma]
- noCompiledRep :: CompiledRepresentation
- type Face = [(Term, Bool)]
- data System = System {
- systemTel :: Telescope
- systemClauses :: [(Face, Term)]
- data ExtLamInfo = ExtLamInfo {
- extLamModule :: ModuleName
- extLamSys :: !(Maybe System)
- modifySystem :: (System -> System) -> ExtLamInfo -> ExtLamInfo
- data Projection = Projection {
- projProper :: Maybe QName
- projOrig :: QName
- projFromType :: Arg QName
- projIndex :: Int
- projLams :: ProjLams
- newtype ProjLams = ProjLams {
- getProjLams :: [Arg ArgName]
- projDropPars :: Projection -> ProjOrigin -> Term
- projArgInfo :: Projection -> ArgInfo
- data EtaEquality
- = Specified {
- theEtaEquality :: !HasEta
- | Inferred {
- theEtaEquality :: !HasEta
- = Specified {
- setEtaEquality :: EtaEquality -> HasEta -> EtaEquality
- data FunctionFlag
- data CompKit = CompKit {
- nameOfHComp :: Maybe QName
- nameOfTransp :: Maybe QName
- emptyCompKit :: CompKit
- data Defn
- = Axiom
- | DataOrRecSig {
- datarecPars :: Int
- | GeneralizableVar
- | AbstractDefn Defn
- | Function {
- funClauses :: [Clause]
- funCompiled :: Maybe CompiledClauses
- funSplitTree :: Maybe SplitTree
- funTreeless :: Maybe Compiled
- funCovering :: [Closure Clause]
- funInv :: FunctionInverse
- funMutual :: Maybe [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
- dataIxs :: Nat
- dataInduction :: Induction
- dataClause :: Maybe Clause
- dataCons :: [QName]
- dataSort :: Sort
- dataMutual :: Maybe [QName]
- dataAbstr :: IsAbstract
- dataPathCons :: [QName]
- | Record {
- recPars :: Nat
- recClause :: Maybe Clause
- recConHead :: ConHead
- recNamedCon :: Bool
- recFields :: [Arg QName]
- recTel :: Telescope
- recMutual :: Maybe [QName]
- recEtaEquality' :: EtaEquality
- recInduction :: Maybe Induction
- recAbstr :: IsAbstract
- recComp :: CompKit
- | Constructor { }
- | Primitive {
- primAbstr :: IsAbstract
- primName :: String
- primClauses :: [Clause]
- primInv :: FunctionInverse
- primCompiled :: Maybe CompiledClauses
- recRecursive :: Defn -> Bool
- recEtaEquality :: Defn -> HasEta
- 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
- defConstructors :: Defn -> [QName]
- 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] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
- primFun :: QName -> Arity -> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
- defClauses :: Definition -> [Clause]
- defCompiled :: Definition -> Maybe CompiledClauses
- defParameters :: Definition -> Maybe Nat
- defInverse :: Definition -> FunctionInverse
- defCompilerPragmas :: BackendName -> Definition -> [CompilerPragma]
- defDelayed :: Definition -> Delayed
- defNonterminating :: Definition -> Bool
- defTerminationUnconfirmed :: Definition -> Bool
- defAbstract :: Definition -> IsAbstract
- defForced :: Definition -> [IsForced]
- type FunctionInverse = FunctionInverse' Clause
- type InversionMap c = Map TermHead [c]
- data FunctionInverse' c
- = NotInjective
- | Inverse (InversionMap 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 Comparison 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 (Maybe Type)
- | CheckTargetType Range Type Type
- | CheckDataDef Range QName [LamBinding] [Constructor]
- | CheckRecDef Range QName [LamBinding] [Constructor]
- | CheckConstructor QName Telescope Sort Constructor
- | CheckConstructorFitsIn QName Type Sort
- | CheckFunDefCall Range QName [Clause]
- | CheckPragma Range Pragma
- | CheckPrimitive Range QName Expr
- | CheckIsEmpty Range Type
- | CheckWithFunctionType Type
- | CheckSectionApplication Range ModuleName ModuleApplication
- | CheckNamedWhere ModuleName
- | 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 {
- builtinName :: String
- builtinDesc :: BuiltinDescriptor
- type BuiltinThings pf = Map String (Builtin pf)
- data Builtin pf
- data HighlightingLevel
- data HighlightingMethod
- ifTopLevelAndHighlightingLevelIsOr :: MonadTCM tcm => HighlightingLevel -> Bool -> tcm () -> tcm ()
- ifTopLevelAndHighlightingLevelIs :: MonadTCM tcm => HighlightingLevel -> tcm () -> tcm ()
- 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
- envWorkingOnTypes :: Bool
- envAssignMetas :: Bool
- envActiveProblems :: Set ProblemId
- envAbstractMode :: AbstractMode
- envModality :: Modality
- envDisplayFormsEnabled :: Bool
- envRange :: Range
- envHighlightingRange :: Range
- envClause :: IPClause
- envCall :: Maybe (Closure Call)
- envHighlightingLevel :: HighlightingLevel
- envHighlightingMethod :: HighlightingMethod
- envModuleNestingLevel :: !Int
- envExpandLast :: ExpandHidden
- envAppDef :: Maybe QName
- envSimplification :: Simplification
- envAllowedReductions :: AllowedReductions
- envInjectivityDepth :: Int
- envCompareBlocked :: Bool
- envPrintDomainFreePi :: Bool
- envPrintMetasBare :: Bool
- envInsideDotPattern :: Bool
- envUnquoteFlags :: UnquoteFlags
- envInstanceDepth :: !Int
- envIsDebugPrinting :: Bool
- envPrintingPatternLambdas :: [QName]
- envCallByNeed :: Bool
- envCurrentCheckpoint :: CheckpointId
- envCheckpoints :: Map CheckpointId Substitution
- envGeneralizeMetas :: DoGeneralize
- envGeneralizedVars :: Map QName GeneralizedValue
- envCheckOptionConsistency :: Bool
- initEnv :: TCEnv
- envRelevance :: TCEnv -> Relevance
- data UnquoteFlags = UnquoteFlags {
- _unquoteNormalise :: Bool
- 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
- eWorkingOnTypes :: Lens' Bool TCEnv
- eAssignMetas :: Lens' Bool TCEnv
- eActiveProblems :: Lens' (Set ProblemId) TCEnv
- eAbstractMode :: Lens' AbstractMode TCEnv
- eModality :: Lens' Modality TCEnv
- eRelevance :: Lens' Relevance TCEnv
- eQuantity :: Lens' Quantity 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
- eExpandLast :: Lens' ExpandHidden TCEnv
- eAppDef :: Lens' (Maybe QName) TCEnv
- eSimplification :: Lens' Simplification TCEnv
- eAllowedReductions :: Lens' AllowedReductions TCEnv
- eInjectivityDepth :: Lens' Int TCEnv
- eCompareBlocked :: Lens' Bool TCEnv
- ePrintDomainFreePi :: Lens' Bool TCEnv
- eInsideDotPattern :: Lens' Bool TCEnv
- eUnquoteFlags :: Lens' UnquoteFlags TCEnv
- eInstanceDepth :: Lens' Int TCEnv
- eIsDebugPrinting :: Lens' Bool TCEnv
- ePrintingPatternLambdas :: Lens' [QName] TCEnv
- eCallByNeed :: Lens' Bool TCEnv
- eCurrentCheckpoint :: Lens' CheckpointId TCEnv
- eCheckpoints :: Lens' (Map CheckpointId Substitution) TCEnv
- eGeneralizeMetas :: Lens' DoGeneralize TCEnv
- eGeneralizedVars :: Lens' (Map QName GeneralizedValue) TCEnv
- type Context = [ContextEntry]
- type ContextEntry = Dom (Name, Type)
- type LetBindings = Map Name (Open (Term, Dom Type))
- data AbstractMode
- aDefToMode :: IsAbstract -> AbstractMode
- aModeToDef :: AbstractMode -> IsAbstract
- data ExpandHidden
- data Candidate = Candidate {
- candidateTerm :: Term
- candidateType :: Type
- candidateOverlappable :: Bool
- data Warning
- = NicifierIssue DeclarationWarning
- | TerminationIssue [TerminationError]
- | UnreachableClauses QName [[NamedArg DeBruijnPattern]]
- | CoverageIssue QName [(Telescope, [NamedArg DeBruijnPattern])]
- | CoverageNoExactSplit QName [Clause]
- | NotStrictlyPositive QName (Seq OccursWhere)
- | UnsolvedMetaVariables [Range]
- | UnsolvedInteractionMetas [Range]
- | UnsolvedConstraints Constraints
- | CantGeneralizeOverSorts [MetaId]
- | AbsurdPatternRequiresNoRHS [NamedArg DeBruijnPattern]
- | OldBuiltin String String
- | EmptyRewritePragma
- | IllformedAsClause String
- | UselessPublic
- | UselessInline QName
- | WrongInstanceDeclaration
- | InstanceWithExplicitArg QName
- | InstanceNoOutputTypeName Doc
- | InstanceArgWithExplicitArg Doc
- | InversionDepthReached QName
- | GenericWarning Doc
- | GenericNonFatalError Doc
- | SafeFlagPostulate Name
- | SafeFlagPragma [String]
- | SafeFlagNonTerminating
- | SafeFlagTerminating
- | SafeFlagWithoutKFlagPrimEraseEquality
- | WithoutKFlagPrimEraseEquality
- | SafeFlagNoPositivityCheck
- | SafeFlagPolarity
- | SafeFlagNoUniverseCheck
- | ParseWarning ParseWarning
- | LibraryWarning LibWarning
- | DeprecationWarning String String String
- | UserWarning String
- | ModuleDoesntExport QName [ImportedName]
- | InfectiveImport String ModuleName
- | CoInfectiveImport String ModuleName
- warningName :: Warning -> WarningName
- data TCWarning = TCWarning {
- tcWarningRange :: Range
- tcWarning :: Warning
- tcWarningPrintedWarning :: Doc
- tcWarningCached :: Bool
- tcWarningOrigin :: TCWarning -> SrcFile
- equalHeadConstructors :: Warning -> Warning -> Bool
- getPartialDefs :: ReadTCState tcm => tcm [QName]
- data CallInfo = CallInfo {}
- data TerminationError = TerminationError {
- termErrFunctions :: [QName]
- termErrCalls :: [CallInfo]
- data SplitError
- = NotADatatype (Closure Type)
- | IrrelevantDatatype (Closure Type)
- | ErasedDatatype (Closure Type)
- | CoinductiveDatatype (Closure Type)
- | UnificationStuck { }
- | CosplitCatchall
- | CosplitNoTarget
- | CosplitNoRecordType (Closure Type)
- | CannotCreateMissingClause QName (Telescope, [NamedArg DeBruijnPattern]) Doc (Closure (Abs Type))
- | GenericSplitError String
- data NegativeUnification
- data UnificationFailure
- data UnquoteError
- = BadVisibility String (Arg Term)
- | ConInsteadOfDef QName String String
- | DefInsteadOfCon QName String String
- | NonCanonical String Term
- | BlockedOnMeta TCState MetaId
- | UnquotePanic String
- data TypeError
- = InternalError String
- | NotImplemented String
- | NotSupported String
- | CompilationError String
- | PropMustBeSingleton
- | DataMustEndInSort Term
- | ShouldEndInApplicationOfTheDatatype Type
- | ShouldBeAppliedToTheDatatypeParameters Term Term
- | ShouldBeApplicationOf Type QName
- | ConstructorPatternInWrongDatatype QName QName
- | CantResolveOverloadedConstructorsTargetingSameDatatype QName [QName]
- | DoesNotConstructAnElementOf QName Type
- | WrongHidingInLHS
- | WrongHidingInLambda Type
- | WrongHidingInApplication Type
- | WrongNamedArgument (NamedArg Expr)
- | WrongIrrelevanceInLambda
- | WrongQuantityInLambda
- | HidingMismatch Hiding Hiding
- | RelevanceMismatch Relevance Relevance
- | UninstantiatedDotPattern Expr
- | ForcedConstructorNotInstantiated Pattern
- | IlltypedPattern Pattern Type
- | IllformedProjectionPattern Pattern
- | CannotEliminateWithPattern (NamedArg Pattern) Type
- | WrongNumberOfConstructorArguments QName Nat Nat
- | ShouldBeEmpty Type [DeBruijnPattern]
- | ShouldBeASort Type
- | ShouldBePi Type
- | ShouldBePath Type
- | ShouldBeRecordType Type
- | ShouldBeRecordPattern DeBruijnPattern
- | NotAProjectionPattern (NamedArg Pattern)
- | NotAProperTerm
- | InvalidTypeSort Sort
- | InvalidType Term
- | FunctionTypeInSizeUniv Term
- | SplitOnIrrelevant (Dom Type)
- | SplitOnNonVariable Term Type
- | DefinitionIsIrrelevant QName
- | VariableIsIrrelevant Name
- | VariableIsErased Name
- | UnequalTerms Comparison Term Term Type
- | UnequalTypes Comparison Type Type
- | UnequalRelevance Comparison Term Term
- | UnequalHiding Term Term
- | UnequalSorts Sort Sort
- | UnequalBecauseOfUniverseConflict Comparison Term Term
- | NotLeqSort Sort Sort
- | MetaCannotDependOn MetaId [Nat] Nat
- | MetaOccursInItself MetaId
- | MetaIrrelevantSolution MetaId Term
- | GenericError String
- | GenericDocError Doc
- | BuiltinMustBeConstructor String Expr
- | NoSuchBuiltinName String
- | DuplicateBuiltinBinding String Term Term
- | NoBindingForBuiltin String
- | NoSuchPrimitiveFunction String
- | DuplicatePrimitiveBinding String QName QName
- | ShadowedModule Name [ModuleName]
- | BuiltinInParameterisedModule String
- | IllegalLetInTelescope TypedBinding
- | NoRHSRequiresAbsurdPattern [NamedArg Pattern]
- | TooManyFields QName [Name] [Name]
- | DuplicateFields [Name]
- | DuplicateConstructors [Name]
- | WithOnFreeVariable Expr Term
- | UnexpectedWithPatterns [Pattern]
- | WithClausePatternMismatch Pattern (NamedArg DeBruijnPattern)
- | FieldOutsideRecord
- | ModuleArityMismatch ModuleName Telescope [NamedArg Expr]
- | GeneralizeCyclicDependency
- | GeneralizeUnsolvedMeta
- | SplitError SplitError
- | ImpossibleConstructor QName NegativeUnification
- | TooManyPolarities QName Int
- | 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
- | AbstractConstructorNotInScope QName
- | NotInScope [QName]
- | NoSuchModule QName
- | AmbiguousName QName (NonemptyList QName)
- | AmbiguousModule QName (NonemptyList ModuleName)
- | ClashingDefinition QName QName
- | ClashingModule ModuleName ModuleName
- | ClashingImport Name QName
- | ClashingModuleImport Name ModuleName
- | PatternShadowsConstructor Name QName
- | DuplicateImports QName [ImportedName]
- | InvalidPattern Pattern
- | RepeatedVariablesInPattern [Name]
- | GeneralizeNotSupportedHere QName
- | MultipleFixityDecls [(Name, [Fixity'])]
- | MultiplePolarityPragmas [Name]
- | NotAModuleExpr Expr
- | NotAnExpression Expr
- | NotAValidLetBinding NiceDeclaration
- | NotValidBeforeField NiceDeclaration
- | NothingAppliedToHiddenArg Expr
- | NothingAppliedToInstanceArg Expr
- | BadArgumentsToPatternSynonym AmbiguousQName
- | TooFewArgumentsToPatternSynonym AmbiguousQName
- | CannotResolveAmbiguousPatternSynonym (NonemptyList (QName, PatternSynDefn))
- | UnusedVariableInPatternSynonym
- | NoParseForApplication [Expr]
- | AmbiguousParseForApplication [Expr] [Expr]
- | NoParseForLHS LHSOrPatSyn Pattern
- | AmbiguousParseForLHS LHSOrPatSyn Pattern [Pattern]
- | OperatorInformation [NotationSection] TypeError
- | InstanceNoCandidate Type [(Term, TCErr)]
- | UnquoteFailed UnquoteError
- | DeBruijnIndexOutOfScope Nat Telescope [Name]
- | NeedOptionCopatterns
- | NeedOptionRewriting
- | NeedOptionProp
- | NonFatalErrors [TCWarning]
- | InstanceSearchDepthExhausted Term Type Int
- | TriedToCopyConstrainedPrim QName
- data LHSOrPatSyn
- data TCErr
- = TypeError { }
- | Exception Range Doc
- | IOException TCState Range IOException
- | PatternErr
- class (Functor m, Applicative m, Monad m) => HasOptions m where
- sizedTypesOption :: HasOptions m => m Bool
- guardednessOption :: HasOptions m => m Bool
- withoutKOption :: HasOptions m => m Bool
- data ReduceEnv = ReduceEnv {}
- mapRedEnv :: (TCEnv -> TCEnv) -> ReduceEnv -> ReduceEnv
- mapRedSt :: (TCState -> TCState) -> ReduceEnv -> ReduceEnv
- mapRedEnvSt :: (TCEnv -> TCEnv) -> (TCState -> TCState) -> ReduceEnv -> ReduceEnv
- reduceEnv :: Lens' TCEnv ReduceEnv
- reduceSt :: Lens' TCState ReduceEnv
- newtype ReduceM a = ReduceM {}
- onReduceEnv :: (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a
- 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)
- useR :: ReadTCState m => Lens' a TCState -> m a
- askR :: ReduceM ReduceEnv
- localR :: (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a
- class (Applicative m, MonadTCEnv m, ReadTCState m, HasOptions m) => MonadReduce m where
- liftReduce :: ReduceM a -> m a
- class Monad m => MonadTCEnv m where
- asksTC :: MonadTCEnv m => (TCEnv -> a) -> m a
- viewTC :: MonadTCEnv m => Lens' a TCEnv -> m a
- locallyTC :: MonadTCEnv m => Lens' a TCEnv -> (a -> a) -> m b -> m b
- class Monad m => MonadTCState m where
- getsTC :: MonadTCState m => (TCState -> a) -> m a
- modifyTC' :: MonadTCState m => (TCState -> TCState) -> m ()
- useTC :: MonadTCState m => Lens' a TCState -> m a
- setTCLens :: MonadTCState m => Lens' a TCState -> a -> m ()
- modifyTCLens :: MonadTCState m => Lens' a TCState -> (a -> a) -> m ()
- modifyTCLensM :: MonadTCState m => Lens' a TCState -> (a -> m a) -> m ()
- locallyTCState :: MonadTCState m => Lens' a TCState -> (a -> a) -> m b -> m b
- newtype TCMT m a = TCM {}
- type TCM = TCMT IO
- class (Applicative tcm, MonadIO tcm, MonadTCEnv tcm, MonadTCState tcm, HasOptions tcm) => MonadTCM tcm where
- 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
- 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
- isExtendedLambdaName :: QName -> Bool
- absurdLambdaName :: String
- isAbsurdLambdaName :: QName -> Bool
- generalizedFieldName :: String
- getGeneralizedFieldName :: QName -> Maybe String
Type checking state
Constructors
TCSt | |
Fields
|
Instances
class Monad m => ReadTCState m where Source #
Instances
data PreScopeState Source #
Constructors
PreScopeState | |
Fields
|
type DisambiguatedNames = IntMap QName Source #
data PostScopeState Source #
Constructors
PostScopeState | |
Fields
|
data MutualBlock Source #
A mutual block of names in the signature.
Constructors
MutualBlock | |
Fields
|
Instances
Eq MutualBlock Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
Show MutualBlock Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> MutualBlock -> ShowS show :: MutualBlock -> String showList :: [MutualBlock] -> ShowS | |
Null MutualBlock Source # | |
Defined in Agda.TypeChecking.Monad.Base |
data PersistentTCState Source #
A part of the state which is not reverted when an error is thrown or the state is reset.
Constructors
PersistentTCSt | |
Fields
|
Instances
data LoadedFileCache Source #
Constructors
LoadedFileCache | |
Fields |
type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)] Source #
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)] Source #
Like CachedTypeCheckLog
, but storing the log for an ongoing type
checking of a module. Stored in reverse order (last performed action
first).
data TypeCheckAction Source #
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 !Telescope | |
LeaveSection !ModuleName | |
Decl !Declaration | Never a Section or ScopeDecl |
Pragmas !PragmaOptions |
initPersistentState :: PersistentTCState Source #
Empty persistent state.
initPreScopeState :: PreScopeState Source #
Empty state of type checker.
st-prefixed lenses
stImportedModules :: Lens' (Set ModuleName) TCState Source #
stForeignCode :: Lens' (Map BackendName [ForeignCode]) TCState Source #
getUserWarnings :: MonadTCState m => m (Map QName String) Source #
stModuleCheckpoints :: Lens' (Map ModuleName CheckpointId) TCState Source #
stCurrentModule :: Lens' (Maybe ModuleName) TCState Source #
stMutualBlocks :: Lens' (Map MutualId MutualBlock) TCState Source #
stFreshInt :: Lens' Int TCState Source #
stAreWeCaching :: Lens' Bool TCState Source #
stConsideringInstance :: Lens' Bool TCState Source #
Fresh things
class Enum i => HasFresh i where Source #
Minimal complete definition
Instances
HasFresh Int Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
HasFresh InteractionId Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
HasFresh MetaId Source # | |
HasFresh NameId Source # | |
HasFresh MutualId Source # | |
HasFresh CheckpointId Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
HasFresh ProblemId Source # | |
fresh :: (HasFresh i, MonadTCState m) => m i Source #
Instances
Enum ProblemId Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
Eq ProblemId Source # | |
Integral ProblemId Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
Data ProblemId Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemId -> c ProblemId gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemId toConstr :: ProblemId -> Constr dataTypeOf :: ProblemId -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemId) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemId) gmapT :: (forall b. Data b => b -> b) -> ProblemId -> ProblemId gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemId -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemId -> r gmapQ :: (forall d. Data d => d -> u) -> ProblemId -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemId -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId | |
Num ProblemId Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
Ord ProblemId Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
Real ProblemId Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods toRational :: ProblemId -> Rational | |
Show ProblemId Source # | |
Pretty ProblemId Source # | |
HasFresh ProblemId Source # | |
PrettyTCM ProblemId Source # | |
newtype CheckpointId Source #
Constructors
CheckpointId Int |
Instances
freshNoName :: MonadTCState m => Range -> m Name Source #
freshNoName_ :: MonadTCState m => m Name Source #
freshRecordName :: MonadTCState m => m Name Source #
class FreshName a where Source #
Create a fresh name from a
.
Methods
freshName_ :: MonadTCState m => a -> m Name Source #
Instances
FreshName () Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadTCState m => () -> m Name Source # | |
FreshName String Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadTCState m => String -> m Name Source # | |
FreshName Range Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadTCState m => Range -> m Name Source # | |
FreshName (Range, String) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadTCState m => (Range, String) -> m Name Source # |
Managing file names
type ModuleToSource = Map TopLevelModuleName AbsolutePath Source #
Maps top-level module names to the corresponding source file names.
type SourceToModule = Map AbsolutePath TopLevelModuleName Source #
Maps source file names to the corresponding top-level module names.
sourceToModule :: TCM SourceToModule Source #
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) Source #
Lookup an AbsolutePath
in sourceToModule
.
O(n).
Interface
data ModuleInfo Source #
Constructors
ModuleInfo | |
Fields
|
type VisitedModules = Map TopLevelModuleName ModuleInfo Source #
type DecodedModules = Map TopLevelModuleName Interface Source #
data ForeignCode Source #
Constructors
ForeignCode Range String |
Instances
Show ForeignCode Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> ForeignCode -> ShowS show :: ForeignCode -> String showList :: [ForeignCode] -> ShowS | |
EmbPrj ForeignCode Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Compilers Methods icode :: ForeignCode -> S Int32 Source # icod_ :: ForeignCode -> S Int32 Source # value :: Int32 -> R ForeignCode Source # |
Constructors
Interface | |
Fields
|
iFullHash :: Interface -> Hash Source #
Combines the source hash and the (full) hashes of the imported modules.
Closure
Constructors
Closure | |
Fields
|
Instances
Functor Closure Source # | |
Foldable Closure Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods fold :: Monoid m => Closure m -> m foldMap :: Monoid m => (a -> m) -> Closure a -> m foldr :: (a -> b -> b) -> b -> Closure a -> b foldr' :: (a -> b -> b) -> b -> Closure a -> b foldl :: (b -> a -> b) -> b -> Closure a -> b foldl' :: (b -> a -> b) -> b -> Closure a -> b foldr1 :: (a -> a -> a) -> Closure a -> a foldl1 :: (a -> a -> a) -> Closure a -> a elem :: Eq a => a -> Closure a -> Bool maximum :: Ord a => Closure a -> a minimum :: Ord a => Closure a -> a | |
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) Source # | |
Defined in Agda.Interaction.BasicOps Methods reify :: ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) Source # reifyWhen :: Bool -> ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) Source # | |
Data a => Data (Closure a) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Closure a -> c (Closure a) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Closure a) toConstr :: Closure a -> Constr dataTypeOf :: Closure a -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Closure a)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Closure a)) gmapT :: (forall b. Data b => b -> b) -> Closure a -> Closure a gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Closure a -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Closure a -> r gmapQ :: (forall d. Data d => d -> u) -> Closure a -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Closure a -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Closure a -> m (Closure a) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Closure a -> m (Closure a) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Closure a -> m (Closure a) | |
Show a => Show (Closure a) Source # | |
KillRange a => KillRange (Closure a) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT (Closure a) Source # | |
HasRange a => HasRange (Closure a) Source # | |
PrettyTCM a => PrettyTCM (Closure a) Source # | |
MentionsMeta a => MentionsMeta (Closure a) Source # | |
Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Closure a -> Bool Source # | |
InstantiateFull a => InstantiateFull (Closure a) Source # | |
Defined in Agda.TypeChecking.Reduce | |
Normalise a => Normalise (Closure a) Source # | |
Defined in Agda.TypeChecking.Reduce | |
Simplify a => Simplify (Closure a) Source # | |
Reduce a => Reduce (Closure a) Source # | |
Instantiate a => Instantiate (Closure a) Source # | |
Defined in Agda.TypeChecking.Reduce |
buildClosure :: a -> TCM (Closure a) Source #
Constraints
type Constraints = [ProblemConstraint] Source #
data ProblemConstraint Source #
Constructors
PConstr | |
Fields |
Instances
data Constraint Source #
Constructors
ValueCmp Comparison Type Term Term | |
ValueCmpOnFace Comparison Term Type Term Term | |
ElimCmp [Polarity] [IsForced] 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 | |
HasBiggerSort Sort | |
HasPTSRule Sort (Abs Sort) | |
UnBlock MetaId | |
Guarded Constraint ProblemId | |
IsEmpty Range Type | The range is the one of the absurd pattern. |
CheckSizeLtSat Term | Check that the |
FindInstance 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) |
CheckFunDef Delayed DefInfo QName [Clause] | |
UnquoteTactic (Maybe MetaId) Term Term Type | First argument is computation and the others are hole and goal type |
Instances
data Comparison Source #
Instances
Eq Comparison Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
Data Comparison Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Comparison -> c Comparison gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Comparison toConstr :: Comparison -> Constr dataTypeOf :: Comparison -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Comparison) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Comparison) gmapT :: (forall b. Data b => b -> b) -> Comparison -> Comparison gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Comparison -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Comparison -> r gmapQ :: (forall d. Data d => d -> u) -> Comparison -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Comparison -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison | |
Show Comparison Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Comparison -> ShowS show :: Comparison -> String showList :: [Comparison] -> ShowS | |
Pretty Comparison Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Comparison -> Doc Source # prettyPrec :: Int -> Comparison -> Doc Source # prettyList :: [Comparison] -> Doc Source # | |
PrettyTCM Comparison Source # | |
Defined in Agda.TypeChecking.Pretty |
data CompareDirection Source #
An extension of Comparison
to >=
.
Instances
Eq CompareDirection Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods (==) :: CompareDirection -> CompareDirection -> Bool (/=) :: CompareDirection -> CompareDirection -> Bool | |
Show CompareDirection Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> CompareDirection -> ShowS show :: CompareDirection -> String showList :: [CompareDirection] -> ShowS | |
Pretty CompareDirection Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods pretty :: CompareDirection -> Doc Source # prettyPrec :: Int -> CompareDirection -> Doc Source # prettyList :: [CompareDirection] -> Doc Source # |
fromCmp :: Comparison -> CompareDirection Source #
Embed Comparison
into CompareDirection
.
flipCmp :: CompareDirection -> CompareDirection Source #
Flip the direction of comparison.
dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c Source #
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
|
Instances
Functor Open Source # | |
Foldable Open Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods fold :: Monoid m => Open m -> m foldMap :: Monoid m => (a -> m) -> Open a -> m foldr :: (a -> b -> b) -> b -> Open a -> b foldr' :: (a -> b -> b) -> b -> Open a -> b foldl :: (b -> a -> b) -> b -> Open a -> b foldl' :: (b -> a -> b) -> b -> Open a -> b foldr1 :: (a -> a -> a) -> Open a -> a foldl1 :: (a -> a -> a) -> Open a -> a elem :: Eq a => a -> Open a -> Bool maximum :: Ord a => Open a -> a | |
Traversable Open Source # | |
Decoration Open Source # | |
Data a => Data (Open a) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Open a -> c (Open a) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Open a) dataTypeOf :: Open a -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Open a)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Open a)) gmapT :: (forall b. Data b => b -> b) -> Open a -> Open a gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Open a -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Open a -> r gmapQ :: (forall d. Data d => d -> u) -> Open a -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Open a -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Open a -> m (Open a) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Open a -> m (Open a) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Open a -> m (Open a) | |
Show a => Show (Open a) Source # | |
KillRange a => KillRange (Open a) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT (Open a) Source # | |
EmbPrj a => EmbPrj (Open a) Source # | |
NamesIn a => NamesIn (Open a) Source # | |
InstantiateFull a => InstantiateFull (Open a) Source # | |
Defined in Agda.TypeChecking.Reduce |
Judgements
Parametrized since it is used without MetaId when creating a new meta.
Generalizable variables
data DoGeneralize Source #
Constructors
YesGeneralize | |
NoGeneralize |
Instances
Eq DoGeneralize Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
Data DoGeneralize Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DoGeneralize -> c DoGeneralize gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DoGeneralize toConstr :: DoGeneralize -> Constr dataTypeOf :: DoGeneralize -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DoGeneralize) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DoGeneralize) gmapT :: (forall b. Data b => b -> b) -> DoGeneralize -> DoGeneralize gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DoGeneralize -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DoGeneralize -> r gmapQ :: (forall d. Data d => d -> u) -> DoGeneralize -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DoGeneralize -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DoGeneralize -> m DoGeneralize gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DoGeneralize -> m DoGeneralize gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DoGeneralize -> m DoGeneralize | |
Ord DoGeneralize Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods compare :: DoGeneralize -> DoGeneralize -> Ordering (<) :: DoGeneralize -> DoGeneralize -> Bool (<=) :: DoGeneralize -> DoGeneralize -> Bool (>) :: DoGeneralize -> DoGeneralize -> Bool (>=) :: DoGeneralize -> DoGeneralize -> Bool max :: DoGeneralize -> DoGeneralize -> DoGeneralize min :: DoGeneralize -> DoGeneralize -> DoGeneralize | |
Show DoGeneralize Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> DoGeneralize -> ShowS show :: DoGeneralize -> String showList :: [DoGeneralize] -> ShowS | |
KillRange DoGeneralize Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
EmbPrj DoGeneralize Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DoGeneralize -> S Int32 Source # icod_ :: DoGeneralize -> S Int32 Source # value :: Int32 -> R DoGeneralize Source # |
data GeneralizedValue Source #
The value of a generalizable variable. This is created to be a generalizable meta before checking the type to be generalized.
Constructors
GeneralizedValue | |
Fields
|
Instances
Data GeneralizedValue Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GeneralizedValue -> c GeneralizedValue gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GeneralizedValue toConstr :: GeneralizedValue -> Constr dataTypeOf :: GeneralizedValue -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GeneralizedValue) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GeneralizedValue) gmapT :: (forall b. Data b => b -> b) -> GeneralizedValue -> GeneralizedValue gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GeneralizedValue -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GeneralizedValue -> r gmapQ :: (forall d. Data d => d -> u) -> GeneralizedValue -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> GeneralizedValue -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> GeneralizedValue -> m GeneralizedValue gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralizedValue -> m GeneralizedValue gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralizedValue -> m GeneralizedValue | |
Show GeneralizedValue Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> GeneralizedValue -> ShowS show :: GeneralizedValue -> String showList :: [GeneralizedValue] -> ShowS |
Meta variables
data MetaVariable Source #
Constructors
MetaVar | |
Fields
|
Instances
SetRange MetaVariable Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods setRange :: Range -> MetaVariable -> MetaVariable Source # | |
HasRange MetaVariable Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods getRange :: MetaVariable -> Range Source # |
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 Source #
Constructors
InstV [Arg String] Term | solved by term (abstracted over some free variables) |
Open | unsolved |
OpenInstance | open, to be instantiated by instance search |
BlockedConst Term | solution blocked by unsolved constraints |
PostponedTypeCheckingProblem (Closure TypeCheckingProblem) (TCM Bool) |
Instances
Show MetaInstantiation Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> MetaInstantiation -> ShowS show :: MetaInstantiation -> String showList :: [MetaInstantiation] -> ShowS |
data CheckedTarget Source #
Solving a CheckArgs
constraint may or may not check the target type. If
it did, it returns a handle to any unsolved constraints.
Constructors
CheckedTarget (Maybe ProblemId) | |
NotCheckedTarget |
data TypeCheckingProblem Source #
Constructors
CheckExpr Comparison Expr Type | |
CheckArgs ExpandHidden Range [NamedArg Expr] Type Type ([Maybe Range] -> Elims -> Type -> CheckedTarget -> TCM Term) | |
CheckProjAppToKnownPrincipalArg Comparison Expr ProjOrigin (NonemptyList QName) Args Type Int Term Type | |
CheckLambda Comparison (Arg ([WithHiding Name], Maybe Type)) Expr Type |
|
DoQuoteTerm Comparison Term Type | Quote the given term and check type against |
Instances
PrettyTCM TypeCheckingProblem Source # | |
Defined in Agda.TypeChecking.Pretty |
newtype MetaPriority Source #
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
Eq MetaPriority Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
Ord MetaPriority Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods compare :: MetaPriority -> MetaPriority -> Ordering (<) :: MetaPriority -> MetaPriority -> Bool (<=) :: MetaPriority -> MetaPriority -> Bool (>) :: MetaPriority -> MetaPriority -> Bool (>=) :: MetaPriority -> MetaPriority -> Bool max :: MetaPriority -> MetaPriority -> MetaPriority min :: MetaPriority -> MetaPriority -> MetaPriority | |
Show MetaPriority Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> MetaPriority -> ShowS show :: MetaPriority -> String showList :: [MetaPriority] -> ShowS |
data RunMetaOccursCheck Source #
Constructors
RunMetaOccursCheck | |
DontRunMetaOccursCheck |
Instances
Eq RunMetaOccursCheck Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods (==) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool (/=) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool | |
Ord RunMetaOccursCheck Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods compare :: RunMetaOccursCheck -> RunMetaOccursCheck -> Ordering (<) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool (<=) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool (>) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool (>=) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool max :: RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck min :: RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck | |
Show RunMetaOccursCheck Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> RunMetaOccursCheck -> ShowS show :: RunMetaOccursCheck -> String showList :: [RunMetaOccursCheck] -> ShowS |
MetaInfo
is cloned from one meta to the next during pruning.
Constructors
MetaInfo | |
Fields
|
type MetaNameSuggestion = String Source #
Name suggestion for meta variable. Empty string means no suggestion.
For printing, we couple a meta with its name suggestion.
Constructors
NamedMeta | |
Fields |
Instances
Pretty NamedMeta Source # | |
ToConcrete NamedMeta Expr Source # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete |
type MetaStore = IntMap MetaVariable Source #
getMetaInfo :: MetaVariable -> Closure Range Source #
getMetaScope :: MetaVariable -> ScopeInfo Source #
getMetaEnv :: MetaVariable -> TCEnv Source #
getMetaSig :: MetaVariable -> Signature Source #
Interaction meta variables
data InteractionPoint Source #
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
Eq InteractionPoint Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods (==) :: InteractionPoint -> InteractionPoint -> Bool (/=) :: InteractionPoint -> InteractionPoint -> Bool |
type InteractionPoints = Map InteractionId InteractionPoint Source #
Data structure managing the interaction points.
We never remove interaction points from this map, only set their
ipSolved
to True
. (Issue #2368)
Which clause is an interaction point located in?
Constructors
IPClause | |
Fields
| |
IPNoClause | The interaction point is not in the rhs of a clause. |
Instances
Eq IPClause Source # | |
Data IPClause Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IPClause -> c IPClause gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IPClause toConstr :: IPClause -> Constr dataTypeOf :: IPClause -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IPClause) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IPClause) gmapT :: (forall b. Data b => b -> b) -> IPClause -> IPClause gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IPClause -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IPClause -> r gmapQ :: (forall d. Data d => d -> u) -> IPClause -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> IPClause -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> IPClause -> m IPClause gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IPClause -> m IPClause gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IPClause -> m IPClause |
Signature
Constructors
Sig | |
Fields
|
Instances
Data Signature Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Signature -> c Signature gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Signature toConstr :: Signature -> Constr dataTypeOf :: Signature -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Signature) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Signature) gmapT :: (forall b. Data b => b -> b) -> Signature -> Signature gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Signature -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Signature -> r gmapQ :: (forall d. Data d => d -> u) -> Signature -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Signature -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Signature -> m Signature gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Signature -> m Signature gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Signature -> m Signature | |
Show Signature Source # | |
KillRange Signature Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
EmbPrj Signature Source # | |
InstantiateFull Signature Source # | |
Defined in Agda.TypeChecking.Reduce |
type Sections = Map ModuleName Section Source #
type Definitions = HashMap QName Definition Source #
type RewriteRuleMap = HashMap QName RewriteRules Source #
type DisplayForms = HashMap QName [LocalDisplayForm] Source #
Constructors
Section | |
Fields |
Instances
Eq Section | |
Data Section Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Section -> c Section gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Section dataTypeOf :: Section -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Section) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Section) gmapT :: (forall b. Data b => b -> b) -> Section -> Section gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Section -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Section -> r gmapQ :: (forall d. Data d => d -> u) -> Section -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Section -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Section -> m Section gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Section -> m Section gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Section -> m Section | |
Show Section Source # | |
Pretty Section Source # | |
KillRange Section Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
KillRange Sections Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
EmbPrj Section Source # | |
InstantiateFull Section Source # | |
Defined in Agda.TypeChecking.Reduce |
data DisplayForm Source #
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
|
Instances
Data DisplayForm Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DisplayForm -> c DisplayForm gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DisplayForm toConstr :: DisplayForm -> Constr dataTypeOf :: DisplayForm -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DisplayForm) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DisplayForm) gmapT :: (forall b. Data b => b -> b) -> DisplayForm -> DisplayForm gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DisplayForm -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DisplayForm -> r gmapQ :: (forall d. Data d => d -> u) -> DisplayForm -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DisplayForm -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DisplayForm -> m DisplayForm gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DisplayForm -> m DisplayForm gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DisplayForm -> m DisplayForm | |
Show DisplayForm Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> DisplayForm -> ShowS show :: DisplayForm -> String showList :: [DisplayForm] -> ShowS | |
KillRange DisplayForm Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
Free DisplayForm Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
EmbPrj DisplayForm Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DisplayForm -> S Int32 Source # icod_ :: DisplayForm -> S Int32 Source # value :: Int32 -> R DisplayForm Source # | |
NamesIn DisplayForm Source # | |
Defined in Agda.Syntax.Internal.Names Methods namesIn :: DisplayForm -> Set QName Source # | |
InstantiateFull DisplayForm Source # | |
Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: DisplayForm -> ReduceM DisplayForm Source # | |
Normalise DisplayForm Source # | |
Defined in Agda.TypeChecking.Reduce Methods | |
Simplify DisplayForm Source # | |
Defined in Agda.TypeChecking.Reduce Methods | |
Subst Term DisplayForm Source # | |
Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> DisplayForm -> DisplayForm Source # |
type LocalDisplayForm = Open DisplayForm Source #
data DisplayTerm Source #
Constructors
DWithApp DisplayTerm [DisplayTerm] Elims |
|
DCon ConHead ConInfo [Arg DisplayTerm] |
|
DDef QName [Elim' DisplayTerm] |
|
DDot Term |
|
DTerm Term |
|
Instances
defaultDisplayForm :: QName -> [LocalDisplayForm] Source #
By default, we have no display form.
defRelevance :: Definition -> Relevance Source #
Non-linear (non-constructor) first-order pattern.
Constructors
PVar !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
|
Instances
Data NLPType Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NLPType -> c NLPType gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NLPType dataTypeOf :: NLPType -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NLPType) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NLPType) gmapT :: (forall b. Data b => b -> b) -> NLPType -> NLPType gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NLPType -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NLPType -> r gmapQ :: (forall d. Data d => d -> u) -> NLPType -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> NLPType -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> NLPType -> m NLPType gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NLPType -> m NLPType gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NLPType -> m NLPType | |
Show NLPType Source # | |
KillRange NLPType Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
Free NLPType Source # | |
EmbPrj NLPType Source # | |
PrettyTCM NLPType Source # | |
InstantiateFull NLPType Source # | |
Defined in Agda.TypeChecking.Reduce | |
NLPatVars NLPType Source # | |
Defined in Agda.TypeChecking.Rewriting | |
Subst NLPat NLPType Source # | |
Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' NLPat -> NLPType -> NLPType Source # | |
Match () NLPType Type Source # | |
PatternFrom () Type NLPType Source # | |
Defined in Agda.TypeChecking.Rewriting.NonLinMatch |
type RewriteRules = [RewriteRule] Source #
data RewriteRule Source #
Rewrite rules can be added independently from function clauses.
Constructors
RewriteRule | |
Instances
Data RewriteRule Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RewriteRule -> c RewriteRule gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RewriteRule toConstr :: RewriteRule -> Constr dataTypeOf :: RewriteRule -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RewriteRule) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RewriteRule) gmapT :: (forall b. Data b => b -> b) -> RewriteRule -> RewriteRule gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RewriteRule -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RewriteRule -> r gmapQ :: (forall d. Data d => d -> u) -> RewriteRule -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> RewriteRule -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> RewriteRule -> m RewriteRule gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RewriteRule -> m RewriteRule gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RewriteRule -> m RewriteRule | |
Show RewriteRule Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> RewriteRule -> ShowS show :: RewriteRule -> String showList :: [RewriteRule] -> ShowS | |
KillRange RewriteRule Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
KillRange RewriteRuleMap Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
Abstract RewriteRule Source # |
|
Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> RewriteRule -> RewriteRule Source # | |
Apply RewriteRule Source # | |
Defined in Agda.TypeChecking.Substitute Methods apply :: RewriteRule -> Args -> RewriteRule Source # applyE :: RewriteRule -> Elims -> RewriteRule Source # | |
EmbPrj RewriteRule Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: RewriteRule -> S Int32 Source # icod_ :: RewriteRule -> S Int32 Source # value :: Int32 -> R RewriteRule Source # | |
PrettyTCM RewriteRule Source # | |
Defined in Agda.TypeChecking.Pretty | |
InstantiateFull RewriteRule Source # | |
Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: RewriteRule -> ReduceM RewriteRule Source # | |
GetMatchables RewriteRule Source # | |
Defined in Agda.TypeChecking.Rewriting Methods getMatchables :: RewriteRule -> [QName] Source # | |
Subst NLPat RewriteRule Source # | |
Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' NLPat -> RewriteRule -> RewriteRule Source # |
data Definition Source #
Constructors
Defn | |
Fields
|
Instances
data NumGeneralizableArgs Source #
Constructors
NoGeneralizableArgs | |
SomeGeneralizableArgs Int | When lambda-lifting new args are generalizable if
|
Instances
defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition Source #
Create a definition with sensible defaults.
Polarity for equality and subtype checking.
Constructors
Covariant | monotone |
Contravariant | antitone |
Invariant | no information (mixed variance) |
Nonvariant | constant |
Instances
Eq Polarity Source # | |
Data Polarity Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Polarity -> c Polarity gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Polarity toConstr :: Polarity -> Constr dataTypeOf :: Polarity -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Polarity) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Polarity) gmapT :: (forall b. Data b => b -> b) -> Polarity -> Polarity gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Polarity -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Polarity -> r gmapQ :: (forall d. Data d => d -> u) -> Polarity -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Polarity -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity | |
Show Polarity Source # | |
Pretty Polarity Source # | |
KillRange Polarity Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
EmbPrj Polarity Source # | |
PrettyTCM Polarity Source # | |
Abstract [Polarity] Source # | |
Apply [Polarity] Source # | |
Information about whether an argument is forced by the type of a function.
Instances
Eq IsForced Source # | |
Data IsForced Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsForced -> c IsForced gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsForced toConstr :: IsForced -> Constr dataTypeOf :: IsForced -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsForced) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsForced) gmapT :: (forall b. Data b => b -> b) -> IsForced -> IsForced gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsForced -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsForced -> r gmapQ :: (forall d. Data d => d -> u) -> IsForced -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> IsForced -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsForced -> m IsForced gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsForced -> m IsForced gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsForced -> m IsForced | |
Show IsForced Source # | |
KillRange IsForced Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
EmbPrj IsForced Source # | |
PrettyTCM IsForced Source # | |
data CompilerPragma Source #
The backends are responsible for parsing their own pragmas.
Constructors
CompilerPragma Range String |
Instances
Eq CompilerPragma Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods (==) :: CompilerPragma -> CompilerPragma -> Bool (/=) :: CompilerPragma -> CompilerPragma -> Bool | |
Data CompilerPragma Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CompilerPragma -> c CompilerPragma gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CompilerPragma toConstr :: CompilerPragma -> Constr dataTypeOf :: CompilerPragma -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CompilerPragma) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CompilerPragma) gmapT :: (forall b. Data b => b -> b) -> CompilerPragma -> CompilerPragma gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CompilerPragma -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CompilerPragma -> r gmapQ :: (forall d. Data d => d -> u) -> CompilerPragma -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> CompilerPragma -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> CompilerPragma -> m CompilerPragma gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CompilerPragma -> m CompilerPragma gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CompilerPragma -> m CompilerPragma | |
Show CompilerPragma Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> CompilerPragma -> ShowS show :: CompilerPragma -> String showList :: [CompilerPragma] -> ShowS | |
KillRange CompiledRepresentation Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
HasRange CompilerPragma Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods getRange :: CompilerPragma -> Range Source # | |
EmbPrj CompilerPragma Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Compilers Methods icode :: CompilerPragma -> S Int32 Source # icod_ :: CompilerPragma -> S Int32 Source # value :: Int32 -> R CompilerPragma Source # |
type BackendName = String Source #
type CompiledRepresentation = Map BackendName [CompilerPragma] Source #
An alternative representation of partial elements in a telescope: Γ ⊢ λ Δ. [φ₁ u₁, ... , φₙ uₙ] : Δ → PartialP (∨_ᵢ φᵢ) T see cubicaltt paper (however we do not store the type T).
Constructors
System | |
Fields
|
Instances
Data System Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> System -> c System gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c System dataTypeOf :: System -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c System) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c System) gmapT :: (forall b. Data b => b -> b) -> System -> System gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> System -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> System -> r gmapQ :: (forall d. Data d => d -> u) -> System -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> System -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> System -> m System gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> System -> m System gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> System -> m System | |
Show System Source # | |
KillRange System Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
Abstract System Source # | |
Apply System Source # | |
EmbPrj System Source # | |
InstantiateFull System Source # | |
Defined in Agda.TypeChecking.Reduce | |
Reify (QNamed System) [Clause] Source # | |
data ExtLamInfo Source #
Additional information for extended lambdas.
Constructors
ExtLamInfo | |
Fields
|
Instances
Data ExtLamInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExtLamInfo -> c ExtLamInfo gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExtLamInfo toConstr :: ExtLamInfo -> Constr dataTypeOf :: ExtLamInfo -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExtLamInfo) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExtLamInfo) gmapT :: (forall b. Data b => b -> b) -> ExtLamInfo -> ExtLamInfo gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExtLamInfo -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExtLamInfo -> r gmapQ :: (forall d. Data d => d -> u) -> ExtLamInfo -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ExtLamInfo -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExtLamInfo -> m ExtLamInfo gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExtLamInfo -> m ExtLamInfo gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExtLamInfo -> m ExtLamInfo | |
Show ExtLamInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> ExtLamInfo -> ShowS show :: ExtLamInfo -> String showList :: [ExtLamInfo] -> ShowS | |
KillRange ExtLamInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
Apply ExtLamInfo Source # | |
Defined in Agda.TypeChecking.Substitute Methods apply :: ExtLamInfo -> Args -> ExtLamInfo Source # applyE :: ExtLamInfo -> Elims -> ExtLamInfo Source # | |
EmbPrj ExtLamInfo Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ExtLamInfo -> S Int32 Source # icod_ :: ExtLamInfo -> S Int32 Source # value :: Int32 -> R ExtLamInfo Source # | |
InstantiateFull ExtLamInfo Source # | |
Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ExtLamInfo -> ReduceM ExtLamInfo Source # |
modifySystem :: (System -> System) -> ExtLamInfo -> ExtLamInfo Source #
data Projection Source #
Additional information for projection Function
s.
Constructors
Projection | |
Fields
|
Instances
Data Projection Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Projection -> c Projection gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Projection toConstr :: Projection -> Constr dataTypeOf :: Projection -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Projection) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Projection) gmapT :: (forall b. Data b => b -> b) -> Projection -> Projection gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Projection -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Projection -> r gmapQ :: (forall d. Data d => d -> u) -> Projection -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Projection -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Projection -> m Projection gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Projection -> m Projection gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Projection -> m Projection | |
Show Projection Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Projection -> ShowS show :: Projection -> String showList :: [Projection] -> ShowS | |
KillRange Projection Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
Abstract Projection Source # | |
Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Projection -> Projection Source # | |
Apply Projection Source # | |
Defined in Agda.TypeChecking.Substitute Methods apply :: Projection -> Args -> Projection Source # applyE :: Projection -> Elims -> Projection Source # | |
EmbPrj Projection Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Projection -> S Int32 Source # icod_ :: Projection -> S Int32 Source # value :: Int32 -> R Projection Source # |
Abstractions to build projection function (dropping parameters).
Constructors
ProjLams | |
Fields
|
Instances
Data ProjLams Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProjLams -> c ProjLams gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProjLams toConstr :: ProjLams -> Constr dataTypeOf :: ProjLams -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProjLams) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProjLams) gmapT :: (forall b. Data b => b -> b) -> ProjLams -> ProjLams gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProjLams -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProjLams -> r gmapQ :: (forall d. Data d => d -> u) -> ProjLams -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ProjLams -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProjLams -> m ProjLams gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProjLams -> m ProjLams gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProjLams -> m ProjLams | |
Show ProjLams Source # | |
Null ProjLams Source # | |
KillRange ProjLams Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
Abstract ProjLams Source # | |
Apply ProjLams Source # | |
EmbPrj ProjLams Source # | |
projDropPars :: Projection -> ProjOrigin -> Term Source #
Building the projection function (which drops the parameters).
projArgInfo :: Projection -> ArgInfo Source #
The info of the principal (record) argument.
data EtaEquality Source #
Should a record type admit eta-equality?
Constructors
Specified | User specifed 'eta-equality' or 'no-eta-equality'. |
Fields
| |
Inferred | Positivity checker inferred whether eta is safe. |
Fields
|
Instances
Eq EtaEquality Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
Data EtaEquality Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EtaEquality -> c EtaEquality gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EtaEquality toConstr :: EtaEquality -> Constr dataTypeOf :: EtaEquality -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EtaEquality) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EtaEquality) gmapT :: (forall b. Data b => b -> b) -> EtaEquality -> EtaEquality gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EtaEquality -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EtaEquality -> r gmapQ :: (forall d. Data d => d -> u) -> EtaEquality -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> EtaEquality -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> EtaEquality -> m EtaEquality gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EtaEquality -> m EtaEquality gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EtaEquality -> m EtaEquality | |
Show EtaEquality Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> EtaEquality -> ShowS show :: EtaEquality -> String showList :: [EtaEquality] -> ShowS | |
KillRange EtaEquality Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
EmbPrj EtaEquality Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: EtaEquality -> S Int32 Source # icod_ :: EtaEquality -> S Int32 Source # value :: Int32 -> R EtaEquality Source # |
setEtaEquality :: EtaEquality -> HasEta -> EtaEquality Source #
Make sure we do not overwrite a user specification.
data FunctionFlag Source #
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
CompKit | |
Fields
|
Instances
Eq CompKit Source # | |
Data CompKit Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CompKit -> c CompKit gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CompKit dataTypeOf :: CompKit -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CompKit) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CompKit) gmapT :: (forall b. Data b => b -> b) -> CompKit -> CompKit gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CompKit -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CompKit -> r gmapQ :: (forall d. Data d => d -> u) -> CompKit -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> CompKit -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> CompKit -> m CompKit gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CompKit -> m CompKit gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CompKit -> m CompKit | |
Ord CompKit Source # | |
Show CompKit Source # | |
KillRange CompKit Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
EmbPrj CompKit Source # | |
NamesIn CompKit Source # | |
Constructors
Axiom | Postulate |
DataOrRecSig | Data or record type signature that doesn't yet have a definition |
Fields
| |
GeneralizableVar | Generalizable variable (introduced in |
AbstractDefn Defn | Returned by |
Function | |
Fields
| |
Datatype | |
Fields
| |
Record | |
Fields
| |
Constructor | |
Fields
| |
Primitive | Primitive or builtin functions. |
Fields
|
Instances
Data Defn Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Defn -> c Defn gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Defn dataTypeOf :: Defn -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Defn) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn) gmapT :: (forall b. Data b => b -> b) -> Defn -> Defn gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r gmapQ :: (forall d. Data d => d -> u) -> Defn -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Defn -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Defn -> m Defn gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Defn -> m Defn gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Defn -> m Defn | |
Show Defn Source # | |
Pretty Defn Source # | |
KillRange Defn Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
Abstract Defn Source # | |
Apply Defn Source # | |
EmbPrj Defn Source # | |
NamesIn Defn Source # | |
InstantiateFull Defn Source # | |
Defined in Agda.TypeChecking.Reduce | |
Occurs Defn Source # | |
recRecursive :: Defn -> Bool Source #
Is the record type recursive?
recEtaEquality :: Defn -> HasEta Source #
emptyFunction :: Defn Source #
A template for creating Function
definitions, with sensible defaults.
isEmptyFunction :: Defn -> Bool Source #
Checking whether we are dealing with a function yet to be defined.
isCopatternLHS :: [Clause] -> Bool Source #
defIsRecord :: Defn -> Bool Source #
defIsDataOrRecord :: Defn -> Bool Source #
defConstructors :: Defn -> [QName] Source #
data Simplification Source #
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 |
Instances
Eq Simplification Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods (==) :: Simplification -> Simplification -> Bool (/=) :: Simplification -> Simplification -> Bool | |
Data Simplification Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Simplification -> c Simplification gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Simplification toConstr :: Simplification -> Constr dataTypeOf :: Simplification -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Simplification) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Simplification) gmapT :: (forall b. Data b => b -> b) -> Simplification -> Simplification gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Simplification -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Simplification -> r gmapQ :: (forall d. Data d => d -> u) -> Simplification -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Simplification -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Simplification -> m Simplification gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Simplification -> m Simplification gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Simplification -> m Simplification | |
Show Simplification Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Simplification -> ShowS show :: Simplification -> String showList :: [Simplification] -> ShowS | |
Semigroup Simplification Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods (<>) :: Simplification -> Simplification -> Simplification sconcat :: NonEmpty Simplification -> Simplification stimes :: Integral b => b -> Simplification -> Simplification | |
Monoid Simplification Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods mappend :: Simplification -> Simplification -> Simplification mconcat :: [Simplification] -> Simplification | |
Null Simplification Source # | |
Defined in Agda.TypeChecking.Monad.Base |
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 Source #
Constructors
MaybeRed | |
Fields
|
Instances
Functor MaybeReduced Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods fmap :: (a -> b) -> MaybeReduced a -> MaybeReduced b (<$) :: a -> MaybeReduced b -> MaybeReduced a # | |
IsProjElim e => IsProjElim (MaybeReduced e) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods isProjElim :: MaybeReduced e -> Maybe (ProjOrigin, QName) Source # | |
PrettyTCM a => PrettyTCM (MaybeReduced a) Source # | |
Defined in Agda.TypeChecking.Pretty |
type MaybeReducedArgs = [MaybeReduced (Arg Term)] Source #
type MaybeReducedElims = [MaybeReduced Elim] Source #
notReduced :: a -> MaybeReduced a Source #
data AllowedReduction Source #
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 | Non-recursive functions and primitives may be reduced. |
RecursiveReductions | Even recursive functions may be reduced. |
LevelReductions | Reduce |
UnconfirmedReductions | Functions whose termination has not (yet) been confirmed. |
NonTerminatingReductions | Functions that have failed termination checking. |
Instances
type AllowedReductions = [AllowedReduction] Source #
allReductions :: AllowedReductions Source #
Not quite all reductions (skip non-terminating reductions)
Constructors
PrimFun | |
Fields
|
primFun :: QName -> Arity -> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun Source #
defClauses :: Definition -> [Clause] Source #
defCompiled :: Definition -> Maybe CompiledClauses Source #
defParameters :: Definition -> Maybe Nat Source #
defCompilerPragmas :: BackendName -> Definition -> [CompilerPragma] Source #
defDelayed :: Definition -> Delayed Source #
Are the clauses of this definition delayed?
defNonterminating :: Definition -> Bool Source #
Has the definition failed the termination checker?
defTerminationUnconfirmed :: Definition -> Bool Source #
Has the definition not termination checked or did the check fail?
defAbstract :: Definition -> IsAbstract Source #
defForced :: Definition -> [IsForced] Source #
Injectivity
type FunctionInverse = FunctionInverse' Clause Source #
type InversionMap c = Map TermHead [c] Source #
data FunctionInverse' c Source #
Constructors
NotInjective | |
Inverse (InversionMap c) |
Instances
Instances
Eq TermHead Source # | |
Data TermHead Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TermHead -> c TermHead gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TermHead toConstr :: TermHead -> Constr dataTypeOf :: TermHead -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TermHead) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TermHead) gmapT :: (forall b. Data b => b -> b) -> TermHead -> TermHead gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TermHead -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TermHead -> r gmapQ :: (forall d. Data d => d -> u) -> TermHead -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TermHead -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TermHead -> m TermHead gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TermHead -> m TermHead gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TermHead -> m TermHead | |
Ord TermHead Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
Show TermHead Source # | |
Pretty TermHead Source # | |
KillRange TermHead Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
EmbPrj TermHead Source # | |
Mutual blocks
Constructors
MutId Int32 |
Instances
Enum MutualId Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
Eq MutualId Source # | |
Data MutualId Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MutualId -> c MutualId gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MutualId toConstr :: MutualId -> Constr dataTypeOf :: MutualId -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MutualId) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MutualId) gmapT :: (forall b. Data b => b -> b) -> MutualId -> MutualId gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MutualId -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MutualId -> r gmapQ :: (forall d. Data d => d -> u) -> MutualId -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> MutualId -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> MutualId -> m MutualId gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MutualId -> m MutualId gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MutualId -> m MutualId | |
Num MutualId Source # | |
Ord MutualId Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
Show MutualId Source # | |
KillRange MutualId Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
HasFresh MutualId Source # | |
EmbPrj MutualId Source # | |
Statistics
type Statistics = Map String Integer Source #
Trace
Constructors
Instances
Data Call Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Call -> c Call gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Call dataTypeOf :: Call -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Call) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Call) gmapT :: (forall b. Data b => b -> b) -> Call -> Call gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Call -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Call -> r gmapQ :: (forall d. Data d => d -> u) -> Call -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Call -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Call -> m Call gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Call -> m Call gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Call -> m Call | |
Pretty Call Source # | |
HasRange Call Source # | |
PrettyTCM Call Source # | |
Instance table
type InstanceTable = Map QName (Set QName) Source #
The instance table is a Map
associating to every name of
recorddata typepostulate its list of instances
type TempInstanceTable = (InstanceTable, Set QName) Source #
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 Source #
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 Source #
Constructors
BuiltinInfo | |
Fields
|
type BuiltinThings pf = Map String (Builtin pf) Source #
Instances
Functor Builtin Source # | |
Foldable Builtin Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods fold :: Monoid m => Builtin m -> m foldMap :: Monoid m => (a -> m) -> Builtin a -> m foldr :: (a -> b -> b) -> b -> Builtin a -> b foldr' :: (a -> b -> b) -> b -> Builtin a -> b foldl :: (b -> a -> b) -> b -> Builtin a -> b foldl' :: (b -> a -> b) -> b -> Builtin a -> b foldr1 :: (a -> a -> a) -> Builtin a -> a foldl1 :: (a -> a -> a) -> Builtin a -> a elem :: Eq a => a -> Builtin a -> Bool maximum :: Ord a => Builtin a -> a minimum :: Ord a => Builtin a -> a | |
Traversable Builtin Source # | |
Show pf => Show (Builtin pf) Source # | |
EmbPrj a => EmbPrj (Builtin a) Source # | |
InstantiateFull a => InstantiateFull (Builtin a) Source # | |
Defined in Agda.TypeChecking.Reduce |
Highlighting levels
data HighlightingLevel Source #
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. |
Instances
data HighlightingMethod Source #
How should highlighting be sent to the user interface?
Instances
Eq HighlightingMethod Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods (==) :: HighlightingMethod -> HighlightingMethod -> Bool (/=) :: HighlightingMethod -> HighlightingMethod -> Bool | |
Data HighlightingMethod Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HighlightingMethod -> c HighlightingMethod gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HighlightingMethod toConstr :: HighlightingMethod -> Constr dataTypeOf :: HighlightingMethod -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HighlightingMethod) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HighlightingMethod) gmapT :: (forall b. Data b => b -> b) -> HighlightingMethod -> HighlightingMethod gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HighlightingMethod -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HighlightingMethod -> r gmapQ :: (forall d. Data d => d -> u) -> HighlightingMethod -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> HighlightingMethod -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> HighlightingMethod -> m HighlightingMethod gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HighlightingMethod -> m HighlightingMethod gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HighlightingMethod -> m HighlightingMethod | |
Read HighlightingMethod Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods readsPrec :: Int -> ReadS HighlightingMethod readList :: ReadS [HighlightingMethod] readPrec :: ReadPrec HighlightingMethod readListPrec :: ReadPrec [HighlightingMethod] | |
Show HighlightingMethod Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> HighlightingMethod -> ShowS show :: HighlightingMethod -> String showList :: [HighlightingMethod] -> ShowS |
ifTopLevelAndHighlightingLevelIsOr :: MonadTCM tcm => HighlightingLevel -> Bool -> tcm () -> tcm () Source #
ifTopLevelAndHighlightingLevelIs l b m
runs m
when we're
type-checking the top-level module and either the highlighting
level is at least l
or b
is True
.
ifTopLevelAndHighlightingLevelIs :: MonadTCM tcm => HighlightingLevel -> tcm () -> tcm () Source #
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
Constructors
TCEnv | |
Fields
|
Instances
Data TCEnv Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TCEnv -> c TCEnv gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TCEnv dataTypeOf :: TCEnv -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TCEnv) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TCEnv) gmapT :: (forall b. Data b => b -> b) -> TCEnv -> TCEnv gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TCEnv -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TCEnv -> r gmapQ :: (forall d. Data d => d -> u) -> TCEnv -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TCEnv -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TCEnv -> m TCEnv gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TCEnv -> m TCEnv gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TCEnv -> m TCEnv |
data UnquoteFlags Source #
Constructors
UnquoteFlags | |
Fields
|
Instances
Data UnquoteFlags Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UnquoteFlags -> c UnquoteFlags gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UnquoteFlags toConstr :: UnquoteFlags -> Constr dataTypeOf :: UnquoteFlags -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UnquoteFlags) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UnquoteFlags) gmapT :: (forall b. Data b => b -> b) -> UnquoteFlags -> UnquoteFlags gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UnquoteFlags -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UnquoteFlags -> r gmapQ :: (forall d. Data d => d -> u) -> UnquoteFlags -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> UnquoteFlags -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> UnquoteFlags -> m UnquoteFlags gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UnquoteFlags -> m UnquoteFlags gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UnquoteFlags -> m UnquoteFlags |
unquoteNormalise :: Lens' Bool UnquoteFlags Source #
eUnquoteNormalise :: Lens' Bool TCEnv Source #
e-prefixed lenses
eCurrentPath :: Lens' (Maybe AbsolutePath) TCEnv Source #
eAnonymousModules :: Lens' [(ModuleName, Nat)] TCEnv Source #
eTerminationCheck :: Lens' (TerminationCheck ()) TCEnv Source #
eSolvingConstraints :: Lens' Bool TCEnv Source #
eCheckingWhere :: Lens' Bool TCEnv Source #
eWorkingOnTypes :: Lens' Bool TCEnv Source #
eAssignMetas :: Lens' Bool TCEnv Source #
eDisplayFormsEnabled :: Lens' Bool TCEnv Source #
eModuleNestingLevel :: Lens' Int TCEnv Source #
eInjectivityDepth :: Lens' Int TCEnv Source #
eCompareBlocked :: Lens' Bool TCEnv Source #
ePrintDomainFreePi :: Lens' Bool TCEnv Source #
eInsideDotPattern :: Lens' Bool TCEnv Source #
eInstanceDepth :: Lens' Int TCEnv Source #
eIsDebugPrinting :: Lens' Bool TCEnv Source #
eCallByNeed :: Lens' Bool TCEnv Source #
eCheckpoints :: Lens' (Map CheckpointId Substitution) TCEnv Source #
eGeneralizedVars :: Lens' (Map QName GeneralizedValue) TCEnv Source #
Context
type Context = [ContextEntry] Source #
The Context
is a stack of ContextEntry
s.
Let bindings
Abstract mode
data AbstractMode Source #
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
Eq AbstractMode Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
Data AbstractMode Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AbstractMode -> c AbstractMode gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AbstractMode toConstr :: AbstractMode -> Constr dataTypeOf :: AbstractMode -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AbstractMode) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AbstractMode) gmapT :: (forall b. Data b => b -> b) -> AbstractMode -> AbstractMode gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AbstractMode -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AbstractMode -> r gmapQ :: (forall d. Data d => d -> u) -> AbstractMode -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> AbstractMode -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> AbstractMode -> m AbstractMode gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AbstractMode -> m AbstractMode gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AbstractMode -> m AbstractMode | |
Show AbstractMode Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> AbstractMode -> ShowS show :: AbstractMode -> String showList :: [AbstractMode] -> ShowS |
aDefToMode :: IsAbstract -> AbstractMode Source #
aModeToDef :: AbstractMode -> IsAbstract Source #
Insertion of implicit arguments
data ExpandHidden Source #
Constructors
ExpandLast | Add implicit arguments in the end until type is no longer hidden |
DontExpandLast | Do not append implicit arguments. |
Instances
Eq ExpandHidden Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
Data ExpandHidden Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExpandHidden -> c ExpandHidden gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExpandHidden toConstr :: ExpandHidden -> Constr dataTypeOf :: ExpandHidden -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExpandHidden) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExpandHidden) gmapT :: (forall b. Data b => b -> b) -> ExpandHidden -> ExpandHidden gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExpandHidden -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExpandHidden -> r gmapQ :: (forall d. Data d => d -> u) -> ExpandHidden -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ExpandHidden -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExpandHidden -> m ExpandHidden gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExpandHidden -> m ExpandHidden gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExpandHidden -> m ExpandHidden |
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
|
Instances
Eq Candidate | |
Data Candidate Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Candidate -> c Candidate gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Candidate toConstr :: Candidate -> Constr dataTypeOf :: Candidate -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Candidate) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Candidate) gmapT :: (forall b. Data b => b -> b) -> Candidate -> Candidate gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Candidate -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Candidate -> r gmapQ :: (forall d. Data d => d -> u) -> Candidate -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Candidate -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Candidate -> m Candidate gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Candidate -> m Candidate gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Candidate -> m Candidate | |
Show Candidate Source # | |
Free Candidate Source # | |
InstantiateFull Candidate Source # | |
Defined in Agda.TypeChecking.Reduce | |
Normalise Candidate Source # | |
Defined in Agda.TypeChecking.Reduce | |
Simplify Candidate Source # | |
Reduce Candidate Source # | |
Instantiate Candidate Source # | |
Defined in Agda.TypeChecking.Reduce | |
Subst Term Candidate Source # | |
Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Candidate -> Candidate Source # |
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
NicifierIssue DeclarationWarning | |
TerminationIssue [TerminationError] | |
UnreachableClauses QName [[NamedArg DeBruijnPattern]] | |
CoverageIssue QName [(Telescope, [NamedArg DeBruijnPattern])] | `CoverageIssue f pss` means that |
CoverageNoExactSplit QName [Clause] | |
NotStrictlyPositive QName (Seq OccursWhere) | |
UnsolvedMetaVariables [Range] | Do not use directly with |
UnsolvedInteractionMetas [Range] | Do not use directly with |
UnsolvedConstraints Constraints | Do not use directly with |
CantGeneralizeOverSorts [MetaId] | |
AbsurdPatternRequiresNoRHS [NamedArg DeBruijnPattern] | |
OldBuiltin String String | In `OldBuiltin old new`, the BUILTIN old has been replaced by new |
EmptyRewritePragma | If the user wrote just |
IllformedAsClause String | If the user wrote something other than an unqualified name
in the |
UselessPublic | If the user opens a module public before the module header. (See issue #2377.) |
UselessInline QName | |
WrongInstanceDeclaration | |
InstanceWithExplicitArg QName | An instance was declared with an implicit argument, which means it will never actually be considered by instance search. |
InstanceNoOutputTypeName Doc | The type of an instance argument doesn't end in a named or variable type, so it will never be considered by instance search. |
InstanceArgWithExplicitArg Doc | As InstanceWithExplicitArg, but for local bindings rather than top-level instances. |
InversionDepthReached QName | The --inversion-max-depth was reached. Generic warnings for one-off things |
GenericWarning Doc | Harmless generic warning (not an error) |
GenericNonFatalError Doc | Generic error which doesn't abort proceedings (not a warning) Safe flag errors |
SafeFlagPostulate Name | |
SafeFlagPragma [String] | |
SafeFlagNonTerminating | |
SafeFlagTerminating | |
SafeFlagWithoutKFlagPrimEraseEquality | |
WithoutKFlagPrimEraseEquality | |
SafeFlagNoPositivityCheck | |
SafeFlagPolarity | |
SafeFlagNoUniverseCheck | |
ParseWarning ParseWarning | |
LibraryWarning LibWarning | |
DeprecationWarning String String String | `DeprecationWarning old new version`:
|
UserWarning String | User-defined warning (e.g. to mention that a name is deprecated) |
ModuleDoesntExport QName [ImportedName] | Some imported names are not actually exported by the source module |
InfectiveImport String ModuleName | Importing a file using an infective option into one which doesn't |
CoInfectiveImport String ModuleName | Importing a file not using a coinfective option from one which does |
Instances
Data Warning Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Warning -> c Warning gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Warning dataTypeOf :: Warning -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Warning) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Warning) gmapT :: (forall b. Data b => b -> b) -> Warning -> Warning gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Warning -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Warning -> r gmapQ :: (forall d. Data d => d -> u) -> Warning -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Warning -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Warning -> m Warning gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Warning -> m Warning gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Warning -> m Warning | |
Show Warning Source # | |
EmbPrj Warning Source # | |
PrettyTCM Warning Source # | |
warningName :: Warning -> WarningName Source #
Constructors
TCWarning | |
Fields
|
tcWarningOrigin :: TCWarning -> SrcFile Source #
equalHeadConstructors :: Warning -> Warning -> Bool Source #
getPartialDefs :: ReadTCState tcm => tcm [QName] Source #
Type checking errors
Information about a call.
Constructors
CallInfo | |
Fields
|
Instances
Data CallInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CallInfo -> c CallInfo gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CallInfo toConstr :: CallInfo -> Constr dataTypeOf :: CallInfo -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CallInfo) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CallInfo) gmapT :: (forall b. Data b => b -> b) -> CallInfo -> CallInfo gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CallInfo -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CallInfo -> r gmapQ :: (forall d. Data d => d -> u) -> CallInfo -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> CallInfo -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> CallInfo -> m CallInfo gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CallInfo -> m CallInfo gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CallInfo -> m CallInfo | |
Show CallInfo Source # | |
Pretty CallInfo Source # | We only |
AllNames CallInfo Source # | |
PrettyTCM CallInfo Source # | |
data TerminationError Source #
Information about a mutual block which did not pass the termination checker.
Constructors
TerminationError | |
Fields
|
Instances
Data TerminationError Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TerminationError -> c TerminationError gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TerminationError toConstr :: TerminationError -> Constr dataTypeOf :: TerminationError -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TerminationError) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TerminationError) gmapT :: (forall b. Data b => b -> b) -> TerminationError -> TerminationError gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TerminationError -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TerminationError -> r gmapQ :: (forall d. Data d => d -> u) -> TerminationError -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TerminationError -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TerminationError -> m TerminationError gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TerminationError -> m TerminationError gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TerminationError -> m TerminationError | |
Show TerminationError Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> TerminationError -> ShowS show :: TerminationError -> String showList :: [TerminationError] -> ShowS |
data SplitError Source #
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. |
ErasedDatatype (Closure Type) | Data type, but in erased position. |
CoinductiveDatatype (Closure Type) | Split on codata not allowed. UNUSED, but keep! -- | NoRecordConstructor Type -- ^ record type, but no constructor |
UnificationStuck | |
Fields
| |
CosplitCatchall | Copattern split with a catchall |
CosplitNoTarget | We do not know the target type of the clause. |
CosplitNoRecordType (Closure Type) | Target type is not a record type. |
CannotCreateMissingClause QName (Telescope, [NamedArg DeBruijnPattern]) Doc (Closure (Abs Type)) | |
GenericSplitError String |
Instances
Show SplitError Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> SplitError -> ShowS show :: SplitError -> String showList :: [SplitError] -> ShowS | |
PrettyTCM SplitError Source # | |
Defined in Agda.TypeChecking.Errors |
data NegativeUnification Source #
Constructors
UnifyConflict Telescope Term Term | |
UnifyCycle Telescope Int Term |
Instances
Show NegativeUnification Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> NegativeUnification -> ShowS show :: NegativeUnification -> String showList :: [NegativeUnification] -> ShowS | |
PrettyTCM NegativeUnification Source # | |
Defined in Agda.TypeChecking.Errors |
data UnificationFailure Source #
Constructors
UnifyIndicesNotVars Telescope Type Term Term Args | Failed to apply injectivity to constructor of indexed datatype |
UnifyRecursiveEq Telescope Type Int Term | Can't solve equation because variable occurs in (type of) lhs |
UnifyReflexiveEq Telescope Type Term | Can't solve reflexive equation because --without-K is enabled |
Instances
Show UnificationFailure Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> UnificationFailure -> ShowS show :: UnificationFailure -> String showList :: [UnificationFailure] -> ShowS | |
PrettyTCM UnificationFailure Source # | |
Defined in Agda.TypeChecking.Errors |
data UnquoteError Source #
Constructors
BadVisibility String (Arg Term) | |
ConInsteadOfDef QName String String | |
DefInsteadOfCon QName String String | |
NonCanonical String Term | |
BlockedOnMeta TCState MetaId | |
UnquotePanic String |
Instances
Show UnquoteError Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> UnquoteError -> ShowS show :: UnquoteError -> String showList :: [UnquoteError] -> ShowS |
Constructors
data LHSOrPatSyn Source #
Distinguish error message when parsing lhs or pattern synonym, resp.
Instances
Eq LHSOrPatSyn Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
Show LHSOrPatSyn Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> LHSOrPatSyn -> ShowS show :: LHSOrPatSyn -> String showList :: [LHSOrPatSyn] -> ShowS |
Type-checking errors.
Constructors
TypeError | |
Fields
| |
Exception Range Doc | |
IOException TCState Range IOException | The first argument is the state in which the error was raised. |
PatternErr | The exception which is usually caught.
Raised for pattern violations during unification ( |
Instances
Show TCErr Source # | |
Exception TCErr Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods toException :: TCErr -> SomeException fromException :: SomeException -> Maybe TCErr displayException :: TCErr -> String | |
Error TCErr Source # | |
HasRange TCErr Source # | |
PrettyTCM TCErr Source # | |
MonadError TCErr IM Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
MonadError TCErr TerM Source # | |
Defined in Agda.Termination.Monad | |
MonadError TCErr (TCMT IO) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods throwError :: TCErr -> TCMT IO a # catchError :: TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a # |
Accessing options
class (Functor m, Applicative m, Monad m) => HasOptions m where Source #
Methods
pragmaOptions :: m PragmaOptions Source #
Returns the pragma options which are currently in effect.
commandLineOptions :: m CommandLineOptions Source #
Returns the command line options which are currently in effect.
Instances
sizedTypesOption :: HasOptions m => m Bool Source #
guardednessOption :: HasOptions m => m Bool Source #
withoutKOption :: HasOptions m => m Bool Source #
The reduce monad
Environment of the reduce monad.
Instances
fmapReduce :: (a -> b) -> ReduceM a -> ReduceM b Source #
runReduceM :: ReduceM a -> TCM a Source #
runReduceF :: (a -> ReduceM b) -> TCM (a -> b) Source #
class (Applicative m, MonadTCEnv m, ReadTCState m, HasOptions m) => MonadReduce m where Source #
Methods
liftReduce :: ReduceM a -> m a Source #
Instances
Monad with read-only TCEnv
class Monad m => MonadTCEnv m where Source #
MonadTCEnv
made into its own dedicated service class.
This allows us to use MonadReader
for ReaderT
extensions of TCM
.
Instances
MonadTCEnv ReduceM Source # | |
MonadTCEnv TerM Source # | |
MonadTCEnv m => MonadTCEnv (MaybeT m) Source # | |
MonadTCEnv m => MonadTCEnv (ListT m) Source # | |
MonadIO m => MonadTCEnv (TCMT m) Source # | |
MonadTCEnv m => MonadTCEnv (NamesT m) Source # | |
MonadTCEnv m => MonadTCEnv (ExceptT err m) Source # | |
MonadTCEnv m => MonadTCEnv (ReaderT r m) Source # | |
MonadTCEnv m => MonadTCEnv (StateT s m) Source # | |
(Monoid w, MonadTCEnv m) => MonadTCEnv (WriterT w m) Source # | |
asksTC :: MonadTCEnv m => (TCEnv -> a) -> m a Source #
locallyTC :: MonadTCEnv m => Lens' a TCEnv -> (a -> a) -> m b -> m b Source #
Modify the lens-indicated part of the TCEnv
in a subcomputation.
Monad with mutable TCState
class Monad m => MonadTCState m where Source #
MonadTCState
made into its own dedicated service class.
This allows us to use MonadState
for StateT
extensions of TCM
.
Instances
MonadTCState TerM Source # | |
MonadTCState m => MonadTCState (MaybeT m) Source # | |
MonadTCState m => MonadTCState (ListT m) Source # | |
MonadIO m => MonadTCState (TCMT m) Source # | |
MonadTCState m => MonadTCState (NamesT m) Source # | |
MonadTCState m => MonadTCState (ExceptT err m) Source # | |
MonadTCState m => MonadTCState (ReaderT r m) Source # | |
MonadTCState m => MonadTCState (StateT s m) Source # | |
(Monoid w, MonadTCState m) => MonadTCState (WriterT w m) Source # | |
TCState
accessors (no lenses)
getsTC :: MonadTCState m => (TCState -> a) -> m a Source #
modifyTC' :: MonadTCState m => (TCState -> TCState) -> m () Source #
A variant of modifyTC
in which the computation is strict in the
new state.
TCState
accessors via lenses
setTCLens :: MonadTCState m => Lens' a TCState -> a -> m () infix 4 Source #
Overwrite the part of the TCState
focused on by the lens.
modifyTCLens :: MonadTCState m => Lens' a TCState -> (a -> a) -> m () Source #
Modify the part of the TCState
focused on by the lens.
modifyTCLensM :: MonadTCState m => Lens' a TCState -> (a -> m a) -> m () Source #
Modify a part of the state monadically.
locallyTCState :: MonadTCState m => Lens' a TCState -> (a -> a) -> m b -> m b Source #
Modify the lens-indicated part of the TCState
locally.
Type checking monad transformer
Instances
class (Applicative tcm, MonadIO tcm, MonadTCEnv tcm, MonadTCState tcm, HasOptions tcm) => MonadTCM tcm where Source #
Instances
MonadTCM TerM Source # | |
MonadTCM tcm => MonadTCM (MaybeT tcm) Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
MonadTCM tcm => MonadTCM (ListT tcm) Source # | |
MonadIO m => MonadTCM (TCMT m) Source # | |
MonadTCM m => MonadTCM (NamesT m) Source # | |
MonadTCM tcm => MonadTCM (ExceptT err tcm) Source # | |
MonadTCM tcm => MonadTCM (ReaderT r tcm) Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
MonadTCM tcm => MonadTCM (StateT s tcm) Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
(Monoid w, MonadTCM tcm) => MonadTCM (WriterT w tcm) Source # | |
Defined in Agda.TypeChecking.Monad.Base |
catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a Source #
Preserve the state of the failing computation.
finally_ :: TCM a -> TCM b -> TCM a Source #
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 Source #
patternViolation :: TCM a Source #
internalError :: MonadTCM tcm => String -> tcm a Source #
genericError :: MonadTCM tcm => String -> tcm a Source #
genericDocError :: MonadTCM tcm => Doc -> tcm a Source #
runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState) Source #
Running the type checking monad (most general form).
runTCMTop :: TCM a -> IO (Either TCErr a) Source #
Running the type checking monad on toplevel (with initial state).
runTCMTop' :: MonadIO m => TCMT m a -> m a Source #
runSafeTCM :: TCM a -> TCState -> IO (a, TCState) Source #
runSafeTCM
runs a safe TCMT
action (a TCMT
action which cannot fail)
in the initial environment.
forkTCM :: TCM a -> TCM () Source #
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 Source #
Base name for extended lambda patterns
isExtendedLambdaName :: QName -> Bool Source #
Check whether we have an definition from an extended lambda.
absurdLambdaName :: String Source #
Name of absurdLambda definitions.
isAbsurdLambdaName :: QName -> Bool Source #
Check whether we have an definition from an absurd lambda.
generalizedFieldName :: String Source #
Base name for generalized variable projections
getGeneralizedFieldName :: QName -> Maybe String Source #
Check whether we have a generalized variable field