| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Monad.Base
Contents
Synopsis
- data Constraint
- = ValueCmp Comparison CompareAs Term Term
- | ValueCmpOnFace Comparison Term Type Term Term
- | ElimCmp [Polarity] [IsForced] Type Term [Elim] [Elim]
- | SortCmp Comparison Sort Sort
- | LevelCmp Comparison Level Level
- | HasBiggerSort Sort
- | HasPTSRule (Dom Type) (Abs Sort)
- | CheckDataSort QName Sort
- | CheckMetaInst MetaId
- | CheckType Type
- | UnBlock MetaId
- | IsEmpty Range Type
- | CheckSizeLtSat Term
- | FindInstance MetaId (Maybe [Candidate])
- | ResolveInstanceHead QName
- | CheckFunDef DefInfo QName [Clause] TCErr
- | UnquoteTactic Term Term Type
- | CheckLockedVars Term Type (Arg Term) Type
- | UsableAtModality WhyCheckModality (Maybe Sort) Modality Term
- 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 (List1 QName)
- | DoesNotConstructAnElementOf QName Type
- | WrongHidingInLHS
- | WrongHidingInLambda Type
- | WrongHidingInApplication Type
- | WrongHidingInProjection QName
- | IllegalHidingInPostfixProjection (NamedArg Expr)
- | WrongNamedArgument (NamedArg Expr) [NamedName]
- | WrongIrrelevanceInLambda
- | WrongQuantityInLambda
- | WrongCohesionInLambda
- | QuantityMismatch Quantity Quantity
- | HidingMismatch Hiding Hiding
- | RelevanceMismatch Relevance Relevance
- | UninstantiatedDotPattern Expr
- | ForcedConstructorNotInstantiated Pattern
- | IllformedProjectionPatternAbstract Pattern
- | IllformedProjectionPatternConcrete Pattern
- | CannotEliminateWithPattern (Maybe Blocker) (NamedArg Pattern) Type
- | CannotEliminateWithProjection (Arg Type) Bool QName
- | 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
- | SplitOnCoinductive
- | SplitOnIrrelevant (Dom Type)
- | SplitOnUnusableCohesion (Dom Type)
- | SplitOnNonVariable Term Type
- | SplitOnNonEtaRecord QName
- | SplitOnAbstract QName
- | SplitOnUnchecked QName
- | SplitOnPartial (Dom Type)
- | SplitInProp DataOrRecordE
- | DefinitionIsIrrelevant QName
- | DefinitionIsErased QName
- | ProjectionIsIrrelevant QName
- | VariableIsIrrelevant Name
- | VariableIsErased Name
- | VariableIsOfUnusableCohesion Name Cohesion
- | UnequalLevel Comparison Level Level
- | UnequalTerms Comparison Term Term CompareAs
- | UnequalTypes Comparison Type Type
- | UnequalRelevance Comparison Term Term
- | UnequalQuantity Comparison Term Term
- | UnequalCohesion Comparison Term Term
- | UnequalFiniteness Comparison Term Term
- | UnequalHiding Term Term
- | UnequalSorts Sort Sort
- | UnequalBecauseOfUniverseConflict Comparison Term Term
- | NotLeqSort Sort Sort
- | MetaCannotDependOn MetaId Nat
- | MetaOccursInItself MetaId
- | MetaIrrelevantSolution MetaId Term
- | MetaErasedSolution MetaId Term
- | GenericError String
- | GenericDocError Doc
- | SortOfSplitVarError (Maybe Blocker) Doc
- | BuiltinMustBeConstructor BuiltinId Expr
- | NoSuchBuiltinName String
- | DuplicateBuiltinBinding BuiltinId Term Term
- | NoBindingForBuiltin BuiltinId
- | NoBindingForPrimitive PrimitiveId
- | NoSuchPrimitiveFunction String
- | DuplicatePrimitiveBinding PrimitiveId QName QName
- | WrongArgInfoForPrimitive PrimitiveId ArgInfo ArgInfo
- | ShadowedModule Name [ModuleName]
- | BuiltinInParameterisedModule BuiltinId
- | IllegalDeclarationInDataDefinition [Declaration]
- | IllegalLetInTelescope TypedBinding
- | IllegalPatternInTelescope Binder
- | NoRHSRequiresAbsurdPattern [NamedArg Pattern]
- | TooManyFields QName [Name] [Name]
- | DuplicateFields [Name]
- | DuplicateConstructors [Name]
- | DuplicateOverlapPragma QName OverlapMode OverlapMode
- | WithOnFreeVariable Expr Term
- | UnexpectedWithPatterns [Pattern]
- | WithClausePatternMismatch Pattern (NamedArg DeBruijnPattern)
- | IllTypedPatternAfterWithAbstraction Pattern
- | FieldOutsideRecord
- | ModuleArityMismatch ModuleName Telescope [NamedArg Expr]
- | GeneralizeCyclicDependency
- | GeneralizeUnsolvedMeta
- | ReferencesFutureVariables Term (NonEmpty Int) (Arg Term) Int
- | DoesNotMentionTicks Term Type (Arg Term)
- | MismatchedProjectionsError QName QName
- | AttributeKindNotEnabled String String String
- | InvalidProjectionParameter (NamedArg Expr)
- | TacticAttributeNotAllowed
- | CannotRewriteByNonEquation Type
- | MacroResultTypeMismatch Type
- | NamedWhereModuleInRefinedContext [Term] [String]
- | CubicalPrimitiveNotFullyApplied QName
- | TooManyArgumentsToLeveledSort QName
- | TooManyArgumentsToUnivOmega QName
- | ComatchingDisabledForRecord QName
- | BuiltinMustBeIsOne Term
- | IncorrectTypeForRewriteRelation Term IncorrectTypeForRewriteRelationReason
- | UnexpectedParameter LamBinding
- | NoParameterOfName ArgName
- | UnexpectedModalityAnnotationInParameter LamBinding
- | ExpectedBindingForParameter (Dom Type) (Abs Type)
- | UnexpectedTypeSignatureForParameter (List1 (NamedArg Binder))
- | SortDoesNotAdmitDataDefinitions QName Sort
- | SortCannotDependOnItsIndex QName Type
- | UnusableAtModality WhyCheckModality Modality Term
- | SplitError SplitError
- | ImpossibleConstructor QName NegativeUnification
- | TooManyPolarities QName Int
- | RecursiveRecordNeedsInductivity QName
- | CannotSolveSizeConstraints (List1 (ProblemConstraint, HypSizeConstraint)) Doc
- | ContradictorySizeConstraint (ProblemConstraint, HypSizeConstraint)
- | EmptyTypeOfSizes Term
- | FunctionTypeInSizeUniv Term
- | LibraryError LibErrors
- | 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
- | InvalidFileName AbsolutePath InvalidFileNameReason
- | BothWithAndRHS
- | AbstractConstructorNotInScope QName
- | NotInScope [QName]
- | NoSuchModule QName
- | AmbiguousName QName AmbiguousNameReason
- | AmbiguousModule QName (List1 ModuleName)
- | AmbiguousField Name [ModuleName]
- | AmbiguousConstructor QName [QName]
- | ClashingDefinition QName QName (Maybe NiceDeclaration)
- | ClashingModule ModuleName ModuleName
- | ClashingImport Name QName
- | ClashingModuleImport Name ModuleName
- | DefinitionInDifferentModule QName
- | DuplicateImports QName [ImportedName]
- | InvalidPattern Pattern
- | RepeatedVariablesInPattern [Name]
- | GeneralizeNotSupportedHere QName
- | GeneralizedVarInLetOpenedModule QName
- | MultipleFixityDecls [(Name, [Fixity'])]
- | MultiplePolarityPragmas [Name]
- | NotAModuleExpr Expr
- | NotAnExpression Expr
- | NotAValidLetBinding NiceDeclaration
- | NotValidBeforeField NiceDeclaration
- | NothingAppliedToHiddenArg Expr
- | NothingAppliedToInstanceArg Expr
- | AsPatternInPatternSynonym
- | DotPatternInPatternSynonym
- | BadArgumentsToPatternSynonym AmbiguousQName
- | TooFewArgumentsToPatternSynonym AmbiguousQName
- | CannotResolveAmbiguousPatternSynonym (List1 (QName, PatternSynDefn))
- | IllegalInstanceVariableInPatternSynonym Name
- | PatternSynonymArgumentShadowsConstructorOrPatternSynonym LHSOrPatSyn Name (List1 AbstractName)
- | UnusedVariableInPatternSynonym Name
- | UnboundVariablesInPatternSynonym [Name]
- | NoParseForApplication (List2 Expr)
- | AmbiguousParseForApplication (List2 Expr) (List1 Expr)
- | NoParseForLHS LHSOrPatSyn [Pattern] Pattern
- | AmbiguousParseForLHS LHSOrPatSyn Pattern [Pattern]
- | AmbiguousProjection QName [QName]
- | AmbiguousOverloadedProjection (List1 QName) Doc
- | OperatorInformation [NotationSection] TypeError
- | InstanceNoCandidate Type [(Term, TCErr)]
- | UnquoteFailed UnquoteError
- | DeBruijnIndexOutOfScope Nat Telescope [Name]
- | NeedOptionCopatterns
- | NeedOptionRewriting
- | NeedOptionProp
- | NeedOptionTwoLevel
- | NonFatalErrors [TCWarning]
- | InstanceSearchDepthExhausted Term Type Int
- | TriedToCopyConstrainedPrim QName
- | CustomBackendError String Doc
- data Comparison
- data ModuleInfo = ModuleInfo {}
- 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 InstanceInfo
- defCopy :: Bool
- defMatchable :: Set QName
- defNoCompilation :: Bool
- defInjective :: Bool
- defCopatternLHS :: Bool
- defBlocked :: Blocked_
- defLanguage :: !Language
- theDef :: Defn
- data Builtin pf
- data System = System {
- systemTel :: Telescope
- systemClauses :: [(Face, Term)]
- type TCM = TCMT IO
- newtype ReduceM a = ReduceM {}
- data HighlightingLevel
- data HighlightingMethod
- data Polarity
- data Open a = OpenThing {}
- data MetaInfo = MetaInfo {}
- type Constraints = [ProblemConstraint]
- data WarningsAndNonFatalErrors = WarningsAndNonFatalErrors {
- tcWarnings :: [TCWarning]
- nonFatalErrors :: [TCWarning]
- data Signature = Sig {}
- data Warning
- = NicifierIssue DeclarationWarning
- | TerminationIssue [TerminationError]
- | UnreachableClauses QName [Range]
- | CoverageIssue QName [(Telescope, [NamedArg DeBruijnPattern])]
- | CoverageNoExactSplit QName [Clause]
- | InlineNoExactSplit QName Clause
- | NotStrictlyPositive QName (Seq OccursWhere)
- | ConstructorDoesNotFitInData QName Sort Sort TCErr
- | CoinductiveEtaRecord QName
- | UnsolvedMetaVariables [Range]
- | UnsolvedInteractionMetas [Range]
- | UnsolvedConstraints Constraints
- | InteractionMetaBoundaries [Range]
- | CantGeneralizeOverSorts [MetaId]
- | AbsurdPatternRequiresNoRHS [NamedArg DeBruijnPattern]
- | OldBuiltin BuiltinId BuiltinId
- | BuiltinDeclaresIdentifier BuiltinId
- | DuplicateRecordDirective RecordDirective
- | EmptyRewritePragma
- | EmptyWhere
- | IllformedAsClause String
- | InvalidCharacterLiteral Char
- | ClashesViaRenaming NameOrModule [Name]
- | UselessPatternDeclarationForRecord String
- | UselessPragma Range Doc
- | UselessPublic
- | UselessHiding [ImportedName]
- | UselessInline QName
- | WrongInstanceDeclaration
- | InstanceWithExplicitArg QName
- | InstanceNoOutputTypeName Doc
- | InstanceArgWithExplicitArg Doc
- | InversionDepthReached QName
- | NoGuardednessFlag QName
- | SafeFlagPostulate Name
- | SafeFlagPragma [String]
- | SafeFlagWithoutKFlagPrimEraseEquality
- | WithoutKFlagPrimEraseEquality
- | ConflictingPragmaOptions String String
- | OptionWarning OptionWarning
- | ParseWarning ParseWarning
- | LibraryWarning LibWarning
- | DeprecationWarning String String String
- | UserWarning Text
- | DuplicateUsing (List1 ImportedName)
- | FixityInRenamingModule (List1 Range)
- | ModuleDoesntExport QName [Name] [Name] [ImportedName]
- | InfectiveImport Doc
- | CoInfectiveImport Doc
- | ConfluenceCheckingIncompleteBecauseOfMeta QName
- | ConfluenceForCubicalNotSupported
- | IllegalRewriteRule QName IllegalRewriteRuleReason
- | RewriteNonConfluent Term Term Term Doc
- | RewriteMaybeNonConfluent Term Term [Doc]
- | RewriteAmbiguousRules Term Term Term
- | RewriteMissingRule Term Term Term
- | PragmaCompileErased BackendName QName
- | PragmaCompileList
- | PragmaCompileMaybe
- | NoMain TopLevelModuleName
- | NotInScopeW [QName]
- | UnsupportedIndexedMatch Doc
- | AsPatternShadowsConstructorOrPatternSynonym LHSOrPatSyn
- | PatternShadowsConstructor Name QName
- | PlentyInHardCompileTimeMode QωOrigin
- | RecordFieldWarning RecordFieldWarning
- | MissingTypeSignatureForOpaque QName IsOpaque
- | NotAffectedByOpaque
- | UnfoldTransparentName QName
- | UselessOpaque
- | FaceConstraintCannotBeHidden ArgInfo
- | FaceConstraintCannotBeNamed NamedName
- | DuplicateInterfaceFiles AbsolutePath AbsolutePath
- | CustomBackendWarning String Doc
- data TCErr
- data TCWarning = TCWarning {}
- data NamedMeta = NamedMeta {}
- type ModuleToSource = Map TopLevelModuleName AbsolutePath
- type Definitions = HashMap QName Definition
- type InteractionOutputCallback = Response_boot TCErr TCWarning WarningsAndNonFatalErrors -> TCM ()
- data IPFace' t = IPFace' {}
- class Monad m => MonadTCEnv m where
- class (Applicative tcm, MonadIO tcm, MonadTCEnv tcm, MonadTCState tcm, HasOptions tcm) => MonadTCM tcm where
- class Monad m => MonadTCState m where
- class Monad m => ReadTCState m where
- getTCState :: m TCState
- locallyTCState :: Lens' TCState a -> (a -> a) -> m b -> m b
- withTCState :: (TCState -> TCState) -> m a -> m a
- newtype TCMT m a = TCM {}
- data LHSOrPatSyn
- data DisplayForm = Display {
- dfPatternVars :: Nat
- dfPats :: Elims
- dfRHS :: DisplayTerm
- data Call
- = CheckClause Type SpineClause
- | CheckLHS SpineLHS
- | CheckPattern Pattern Telescope Type
- | CheckPatternLinearityType Name
- | CheckPatternLinearityValue Name
- | CheckLetBinding LetBinding
- | InferExpr Expr
- | CheckExprCall Comparison Expr Type
- | CheckDotPattern Expr Term
- | CheckProjection Range QName Type
- | IsTypeCall Comparison Expr Sort
- | IsType_ Expr
- | InferVar Name
- | InferDef QName
- | CheckArguments Range [NamedArg Expr] Type (Maybe Type)
- | CheckMetaSolution Range MetaId Type Term
- | CheckTargetType Range Type Type
- | CheckDataDef Range QName [LamBinding] [Constructor]
- | CheckRecDef Range QName [LamBinding] [Constructor]
- | CheckConstructor QName Telescope Sort Constructor
- | CheckConArgFitsIn QName Bool Type Sort
- | CheckFunDefCall Range QName [Clause] Bool
- | CheckPragma Range Pragma
- | CheckPrimitive Range QName Expr
- | CheckIsEmpty Range Type
- | CheckConfluence QName QName
- | CheckModuleParameters ModuleName Telescope
- | CheckWithFunctionType Type
- | CheckSectionApplication Range Erased ModuleName ModuleApplication
- | CheckNamedWhere ModuleName
- | CheckIApplyConfluence Range QName Term Term Term Type
- | ScopeCheckExpr Expr
- | ScopeCheckDeclaration NiceDeclaration
- | ScopeCheckLHS QName Pattern
- | NoHighlighting
- | ModuleContents
- | SetRange Range
- data Closure a = Closure {}
- class (Applicative m, MonadTCEnv m, ReadTCState m, HasOptions m) => MonadReduce m where
- liftReduce :: ReduceM a -> m a
- type Statistics = Map String Integer
- data CompilerPragma = CompilerPragma Range String
- data TCEnv = TCEnv {
- envContext :: Context
- envLetBindings :: LetBindings
- envCurrentModule :: ModuleName
- envCurrentPath :: Maybe AbsolutePath
- envAnonymousModules :: [(ModuleName, Nat)]
- envImportPath :: [TopLevelModuleName]
- envMutualBlock :: Maybe MutualId
- envTerminationCheck :: TerminationCheck ()
- envCoverageCheck :: CoverageCheck
- envMakeCase :: Bool
- envSolvingConstraints :: Bool
- envCheckingWhere :: Bool
- envWorkingOnTypes :: Bool
- envAssignMetas :: Bool
- envActiveProblems :: Set ProblemId
- envUnquoteProblem :: Maybe ProblemId
- envAbstractMode :: AbstractMode
- envRelevance :: Relevance
- envQuantity :: Quantity
- envHardCompileTimeMode :: Bool
- envSplitOnStrict :: Bool
- envDisplayFormsEnabled :: Bool
- envFoldLetBindings :: Bool
- envRange :: Range
- envHighlightingRange :: Range
- envClause :: IPClause
- envCall :: Maybe (Closure Call)
- envHighlightingLevel :: HighlightingLevel
- envHighlightingMethod :: HighlightingMethod
- envExpandLast :: ExpandHidden
- envAppDef :: Maybe QName
- envSimplification :: Simplification
- envAllowedReductions :: AllowedReductions
- envReduceDefs :: ReduceDefs
- envReconstructed :: Bool
- 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
- envActiveBackendName :: Maybe BackendName
- envConflComputingOverlap :: Bool
- envCurrentlyElaborating :: Bool
- envSyntacticEqualityFuel :: !(Maybe Int)
- envCurrentOpaqueId :: !(Maybe OpaqueId)
- data Interface = Interface {
- iSourceHash :: !Hash
- iSource :: Text
- iFileType :: FileType
- iImportedModules :: [(TopLevelModuleName, Hash)]
- iModuleName :: ModuleName
- iTopLevelModuleName :: TopLevelModuleName
- iScope :: Map ModuleName Scope
- iInsideScope :: ScopeInfo
- iSignature :: Signature
- iMetaBindings :: RemoteMetaStore
- iDisplayForms :: DisplayForms
- iUserWarnings :: Map QName Text
- iImportWarning :: Maybe Text
- iBuiltin :: BuiltinThings (PrimitiveId, QName)
- iForeignCode :: Map BackendName ForeignCodeStack
- iHighlighting :: HighlightingInfo
- iDefaultPragmaOptions :: [OptionsPragma]
- iFilePragmaOptions :: [OptionsPragma]
- iOptionsUsed :: PragmaOptions
- iPatternSyns :: PatternSynDefns
- iWarnings :: [TCWarning]
- iPartialDefs :: Set QName
- iOpaqueBlocks :: Map OpaqueId OpaqueBlock
- iOpaqueNames :: Map QName OpaqueId
- type MonadTCError m = (MonadTCEnv m, ReadTCState m, MonadError TCErr m)
- type BackendName = String
- data TCState = TCSt {}
- type RewriteRules = [RewriteRule]
- data PrimFun = PrimFun {
- primFunName :: QName
- primFunArity :: Arity
- primFunArgOccurrences :: [Occurrence]
- primFunImplementation :: [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
- data RunMetaOccursCheck
- data CompareAs
- data CompareDirection
- data MetaVariable = MetaVar {}
- data InstanceInfo = InstanceInfo {}
- class Monad m => MonadBlock m where
- patternViolation :: Blocker -> m a
- catchPatternErr :: (Blocker -> m a) -> m a -> m a
- data Reduced no yes
- = NoReduction no
- | YesReduction Simplification yes
- data ProblemConstraint = PConstr {}
- newtype Fields = Fields [(Name, Type)]
- data ForeignCode = ForeignCode Range String
- data LetBinding = LetBinding {}
- newtype Section = Section {}
- data PreScopeState = PreScopeState {
- stPreTokens :: !HighlightingInfo
- stPreImports :: !Signature
- stPreImportedModules :: !(Set TopLevelModuleName)
- stPreModuleToSource :: !ModuleToSource
- stPreVisitedModules :: !VisitedModules
- stPreScope :: !ScopeInfo
- stPrePatternSyns :: !PatternSynDefns
- stPrePatternSynImports :: !PatternSynDefns
- stPreGeneralizedVars :: !(Maybe (Set QName))
- stPrePragmaOptions :: !PragmaOptions
- stPreImportedBuiltins :: !(BuiltinThings PrimFun)
- stPreImportedDisplayForms :: !DisplayForms
- stPreFreshInteractionId :: !InteractionId
- stPreImportedUserWarnings :: !(Map QName Text)
- stPreLocalUserWarnings :: !(Map QName Text)
- stPreWarningOnImport :: !(Maybe Text)
- stPreImportedPartialDefs :: !(Set QName)
- stPreProjectConfigs :: !(Map FilePath ProjectConfig)
- stPreAgdaLibFiles :: !(Map FilePath AgdaLibFile)
- stPreImportedMetaStore :: !RemoteMetaStore
- stPreCopiedNames :: !(HashMap QName QName)
- stPreNameCopies :: !(HashMap QName (HashSet QName))
- data PostScopeState = PostScopeState {
- stPostSyntaxInfo :: !HighlightingInfo
- stPostDisambiguatedNames :: !DisambiguatedNames
- stPostOpenMetaStore :: !LocalMetaStore
- stPostSolvedMetaStore :: !LocalMetaStore
- stPostInteractionPoints :: !InteractionPoints
- stPostAwakeConstraints :: !Constraints
- stPostSleepingConstraints :: !Constraints
- stPostDirty :: !Bool
- stPostOccursCheckDefs :: !(Set QName)
- stPostSignature :: !Signature
- stPostModuleCheckpoints :: !(Map ModuleName CheckpointId)
- stPostImportsDisplayForms :: !DisplayForms
- stPostForeignCode :: !(Map BackendName ForeignCodeStack)
- stPostCurrentModule :: !(Maybe (ModuleName, TopLevelModuleName))
- stPostPendingInstances :: !(Set QName)
- stPostTemporaryInstances :: !(Set QName)
- stPostConcreteNames :: !ConcreteNames
- stPostUsedNames :: !(Map RawName (DList RawName))
- stPostShadowingNames :: !(Map Name (DList RawName))
- stPostStatistics :: !Statistics
- stPostTCWarnings :: ![TCWarning]
- stPostMutualBlocks :: !(Map MutualId MutualBlock)
- stPostLocalBuiltins :: !(BuiltinThings PrimFun)
- stPostFreshMetaId :: !MetaId
- stPostFreshMutualId :: !MutualId
- stPostFreshProblemId :: !ProblemId
- stPostFreshCheckpointId :: !CheckpointId
- stPostFreshInt :: !Int
- stPostFreshNameId :: !NameId
- stPostFreshOpaqueId :: !OpaqueId
- stPostAreWeCaching :: !Bool
- stPostPostponeInstanceSearch :: !Bool
- stPostConsideringInstance :: !Bool
- stPostInstantiateBlocking :: !Bool
- stPostLocalPartialDefs :: !(Set QName)
- stPostOpaqueBlocks :: Map OpaqueId OpaqueBlock
- stPostOpaqueIds :: Map QName OpaqueId
- data PersistentTCState = PersistentTCSt {
- stDecodedModules :: !DecodedModules
- stPersistentTopLevelModuleNames :: !(BiMap RawTopLevelModuleName ModuleNameHash)
- stPersistentOptions :: CommandLineOptions
- stInteractionOutputCallback :: InteractionOutputCallback
- stBenchmark :: !Benchmark
- stAccumStatistics :: !Statistics
- stPersistLoadedFileCache :: !(Maybe LoadedFileCache)
- stPersistBackends :: [Backend_boot TCM]
- type VisitedModules = Map TopLevelModuleName ModuleInfo
- type BuiltinThings pf = Map SomeBuiltin (Builtin pf)
- type DisplayForms = HashMap QName [LocalDisplayForm]
- type RemoteMetaStore = HashMap MetaId RemoteMetaVariable
- data DisambiguatedName = DisambiguatedName NameKind QName
- type DisambiguatedNames = IntMap DisambiguatedName
- type ConcreteNames = Map Name [Name]
- type LocalMetaStore = Map MetaId MetaVariable
- type InteractionPoints = BiMap InteractionId InteractionPoint
- newtype CheckpointId = CheckpointId Int
- newtype ForeignCodeStack = ForeignCodeStack {}
- newtype MutualId = MutId Int32
- data MutualBlock = MutualBlock {}
- data OpaqueBlock = OpaqueBlock {}
- type DecodedModules = Map TopLevelModuleName ModuleInfo
- data LoadedFileCache = LoadedFileCache {}
- type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)]
- type CurrentTypeCheckLog = [(TypeCheckAction, PostScopeState)]
- data TypeCheckAction
- type TempInstanceTable = (InstanceTable, Set QName)
- class Enum i => HasFresh i where
- freshLens :: Lens' TCState i
- nextFresh' :: i -> i
- class Monad m => MonadFresh i m where
- fresh :: m i
- class FreshName a where
- freshName_ :: MonadFresh NameId m => a -> m Name
- class Monad m => MonadStConcreteNames m where
- runStConcreteNames :: StateT ConcreteNames m a -> m a
- useConcreteNames :: m ConcreteNames
- modifyConcreteNames :: (ConcreteNames -> ConcreteNames) -> m ()
- data ModuleCheckMode
- class LensClosure b a | b -> a where
- lensClosure :: Lens' b (Closure a)
- class LensTCEnv a where
- data WhyCheckModality
- data IsForced
- data Candidate = Candidate {}
- data Judgement a
- = HasType {
- jMetaId :: a
- jComparison :: Comparison
- jMetaType :: Type
- | IsSort { }
- = HasType {
- data DoGeneralize
- data GeneralizedValue = GeneralizedValue {}
- newtype MetaPriority = MetaPriority Int
- data MetaInstantiation
- data Listener
- data Frozen
- data Instantiation = Instantiation {}
- data TypeCheckingProblem
- = CheckExpr Comparison Expr Type
- | CheckArgs Comparison ExpandHidden Range [NamedArg Expr] Type Type (ArgsCheckState CheckedTarget -> TCM Term)
- | CheckProjAppToKnownPrincipalArg Comparison Expr ProjOrigin (List1 QName) Args Type Int Term Type PrincipalArgTypeMetas
- | CheckLambda Comparison (Arg (List1 (WithHiding Name), Maybe Type)) Expr Type
- | DoQuoteTerm Comparison Term Type
- data RemoteMetaVariable = RemoteMetaVariable {}
- data CheckedTarget
- data PrincipalArgTypeMetas = PrincipalArgTypeMetas {
- patmMetas :: Args
- patmRemainder :: Type
- data ExpandHidden
- data ArgsCheckState a = ACState {}
- data InteractionPoint = InteractionPoint {}
- data IPClause
- = IPClause {
- ipcQName :: QName
- ipcClauseNo :: Int
- ipcType :: Type
- ipcWithSub :: Maybe Substitution
- ipcClause :: SpineClause
- ipcClosure :: Closure ()
- | IPNoClause
- = IPClause {
- type IPBoundary = IPBoundary' Term
- data Overapplied
- newtype IPBoundary' t = IPBoundary {
- getBoundary :: Map (IntMap Bool) t
- type Sections = Map ModuleName Section
- type RewriteRuleMap = HashMap QName RewriteRules
- data InstanceTable = InstanceTable {}
- type LocalDisplayForm = Open DisplayForm
- data DisplayTerm
- data NLPat
- type PElims = [Elim' NLPat]
- data NLPType = NLPType {}
- data NLPSort
- data RewriteRule = RewriteRule {}
- data Defn
- data NumGeneralizableArgs
- type CompiledRepresentation = Map BackendName [CompilerPragma]
- type Face = [(Term, Bool)]
- data ExtLamInfo = ExtLamInfo {
- extLamModule :: ModuleName
- extLamAbsurd :: Bool
- extLamSys :: !(Maybe System)
- data Projection = Projection {}
- newtype ProjLams = ProjLams {
- getProjLams :: [Arg ArgName]
- data EtaEquality
- = Specified {
- theEtaEquality :: !HasEta
- | Inferred {
- theEtaEquality :: !HasEta
- = Specified {
- data FunctionFlag
- data CompKit = CompKit {}
- data AxiomData = AxiomData {}
- data DataOrRecSigData = DataOrRecSigData {
- _datarecPars :: Int
- data FunctionData = FunctionData {
- _funClauses :: [Clause]
- _funCompiled :: Maybe CompiledClauses
- _funSplitTree :: Maybe SplitTree
- _funTreeless :: Maybe Compiled
- _funCovering :: [Clause]
- _funInv :: FunctionInverse
- _funMutual :: Maybe [QName]
- _funProjection :: Either ProjectionLikenessMissing Projection
- _funFlags :: SmallSet FunctionFlag
- _funTerminates :: Maybe Bool
- _funExtLam :: Maybe ExtLamInfo
- _funWith :: Maybe QName
- _funIsKanOp :: Maybe QName
- _funOpaque :: IsOpaque
- data DatatypeData = DatatypeData {
- _dataPars :: Nat
- _dataIxs :: Nat
- _dataClause :: Maybe Clause
- _dataCons :: [QName]
- _dataSort :: Sort
- _dataMutual :: Maybe [QName]
- _dataAbstr :: IsAbstract
- _dataPathCons :: [QName]
- _dataTranspIx :: Maybe QName
- _dataTransp :: Maybe QName
- data RecordData = RecordData {
- _recPars :: Nat
- _recClause :: Maybe Clause
- _recConHead :: ConHead
- _recNamedCon :: Bool
- _recFields :: [Dom QName]
- _recTel :: Telescope
- _recMutual :: Maybe [QName]
- _recEtaEquality' :: EtaEquality
- _recPatternMatching :: PatternOrCopattern
- _recInduction :: Maybe Induction
- _recTerminates :: Maybe Bool
- _recAbstr :: IsAbstract
- _recComp :: CompKit
- data ConstructorData = ConstructorData {
- _conPars :: Int
- _conArity :: Int
- _conSrcCon :: ConHead
- _conData :: QName
- _conAbstr :: IsAbstract
- _conComp :: CompKit
- _conProj :: Maybe [QName]
- _conForced :: [IsForced]
- _conErased :: Maybe [Bool]
- _conErasure :: !Bool
- _conInline :: !Bool
- data PrimitiveData = PrimitiveData {}
- data PrimitiveSortData = PrimitiveSortData {}
- data ProjectionLikenessMissing
- type FunctionInverse = FunctionInverse' Clause
- data BuiltinSort
- data FunctionInverse' c
- = NotInjective
- | Inverse (InversionMap c)
- data Simplification
- data IsReduced
- = NotReduced
- | Reduced (Blocked ())
- data MaybeReduced a = MaybeRed {
- isReduced :: IsReduced
- ignoreReduced :: a
- type MaybeReducedArgs = [MaybeReduced (Arg Term)]
- type MaybeReducedElims = [MaybeReduced Elim]
- data AllowedReduction
- type AllowedReductions = SmallSet AllowedReduction
- data ReduceDefs
- = OnlyReduceDefs (Set QName)
- | DontReduceDefs (Set QName)
- data PrimitiveImpl = PrimImpl Type PrimFun
- type InversionMap c = Map TermHead [c]
- data TermHead
- data BuiltinDescriptor
- = BuiltinData (TCM Type) [BuiltinId]
- | BuiltinDataCons (TCM Type)
- | BuiltinPrim PrimitiveId (Term -> TCM ())
- | BuiltinSort BuiltinSort
- | BuiltinPostulate Relevance (TCM Type)
- | BuiltinUnknown (Maybe (TCM Type)) (Term -> Type -> TCM ())
- data BuiltinInfo = BuiltinInfo {}
- type LetBindings = Map Name (Open LetBinding)
- data AbstractMode
- data UnquoteFlags = UnquoteFlags {}
- data CandidateKind
- data TerminationError = TerminationError {
- termErrFunctions :: [QName]
- termErrCalls :: [CallInfo]
- data IllegalRewriteRuleReason
- = LHSNotDefinitionOrConstructor
- | VariablesNotBoundByLHS IntSet
- | VariablesBoundMoreThanOnce IntSet
- | LHSReduces Term Term
- | HeadSymbolIsProjection QName
- | HeadSymbolIsProjectionLikeFunction QName
- | HeadSymbolIsTypeConstructor QName
- | HeadSymbolContainsMetas QName
- | ConstructorParametersNotGeneral ConHead Args
- | ContainsUnsolvedMetaVariables (Set MetaId)
- | BlockedOnProblems (Set ProblemId)
- | RequiresDefinitions (Set QName)
- | DoesNotTargetRewriteRelation
- | BeforeFunctionDefinition
- | BeforeMutualFunctionDefinition QName
- | DuplicateRewriteRule
- data CallInfo = CallInfo {}
- data ErasedDatatypeReason
- data SplitError
- = NotADatatype (Closure Type)
- | BlockedType Blocker (Closure Type)
- | ErasedDatatype ErasedDatatypeReason (Closure Type)
- | CoinductiveDatatype (Closure Type)
- | UnificationStuck { }
- | CosplitCatchall
- | CosplitNoTarget
- | CosplitNoRecordType (Closure Type)
- | CannotCreateMissingClause QName (Telescope, [NamedArg DeBruijnPattern]) Doc (Closure (Abs Type))
- | GenericSplitError String
- data UnificationFailure
- data NegativeUnification
- data UnquoteError
- type DataOrRecordE = DataOrRecord' InductionAndEta
- data IncorrectTypeForRewriteRelationReason
- data InvalidFileNameReason
- data InductionAndEta = InductionAndEta {}
- data ReduceEnv = ReduceEnv {}
- newtype BlockT m a = BlockT {}
- pattern Function :: [Clause] -> Maybe CompiledClauses -> Maybe SplitTree -> Maybe Compiled -> [Clause] -> FunctionInverse -> Maybe [QName] -> Either ProjectionLikenessMissing Projection -> SmallSet FunctionFlag -> Maybe Bool -> Maybe ExtLamInfo -> Maybe QName -> Maybe QName -> IsOpaque -> Defn
- pattern Constructor :: Int -> Int -> ConHead -> QName -> IsAbstract -> CompKit -> Maybe [QName] -> [IsForced] -> Maybe [Bool] -> Bool -> Bool -> Defn
- pattern Datatype :: Nat -> Nat -> Maybe Clause -> [QName] -> Sort -> Maybe [QName] -> IsAbstract -> [QName] -> Maybe QName -> Maybe QName -> Defn
- pattern Primitive :: IsAbstract -> PrimitiveId -> [Clause] -> FunctionInverse -> Maybe CompiledClauses -> IsOpaque -> Defn
- pattern Record :: Nat -> Maybe Clause -> ConHead -> Bool -> [Dom QName] -> Telescope -> Maybe [QName] -> EtaEquality -> PatternOrCopattern -> Maybe Induction -> Maybe Bool -> IsAbstract -> CompKit -> Defn
- pattern Axiom :: Bool -> Defn
- pattern DDot :: Term -> DisplayTerm
- pattern DTerm :: Term -> DisplayTerm
- pattern PType :: NLPat -> NLPSort
- pattern PProp :: NLPat -> NLPSort
- pattern PSSet :: NLPat -> NLPSort
- pattern DataOrRecSig :: Int -> Defn
- pattern PrimitiveSort :: BuiltinSort -> Sort -> Defn
- pattern SortProp :: BuiltinSort
- pattern SortSet :: BuiltinSort
- pattern SortStrictSet :: BuiltinSort
- pattern SortPropOmega :: BuiltinSort
- pattern SortSetOmega :: BuiltinSort
- pattern SortStrictSetOmega :: BuiltinSort
- typeError :: (HasCallStack, MonadTCError m) => TypeError -> m a
- internalError :: (HasCallStack, MonadTCM tcm) => String -> tcm a
- runReduceM :: ReduceM a -> TCM a
- initState :: TCState
- defaultInteractionOutputCallback :: InteractionOutputCallback
- mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a
- askR :: ReduceM ReduceEnv
- defAbstract :: Definition -> IsAbstract
- genericError :: (HasCallStack, MonadTCError m) => String -> m a
- stModuleToSource :: Lens' TCState ModuleToSource
- useTC :: ReadTCState m => Lens' TCState a -> m a
- defOpaque :: Definition -> IsOpaque
- initPersistentState :: PersistentTCState
- initialMetaId :: MetaId
- initPreScopeState :: PreScopeState
- emptySignature :: Signature
- initPostScopeState :: PostScopeState
- stTokens :: Lens' TCState HighlightingInfo
- stImports :: Lens' TCState Signature
- stImportedModules :: Lens' TCState (Set TopLevelModuleName)
- stVisitedModules :: Lens' TCState VisitedModules
- stScope :: Lens' TCState ScopeInfo
- stPatternSyns :: Lens' TCState PatternSynDefns
- stPatternSynImports :: Lens' TCState PatternSynDefns
- stGeneralizedVars :: Lens' TCState (Maybe (Set QName))
- stPragmaOptions :: Lens' TCState PragmaOptions
- stImportedBuiltins :: Lens' TCState (BuiltinThings PrimFun)
- stForeignCode :: Lens' TCState (Map BackendName ForeignCodeStack)
- stFreshInteractionId :: Lens' TCState InteractionId
- stImportedUserWarnings :: Lens' TCState (Map QName Text)
- stLocalUserWarnings :: Lens' TCState (Map QName Text)
- getUserWarnings :: ReadTCState m => m (Map QName Text)
- useR :: ReadTCState m => Lens' TCState a -> m a
- stWarningOnImport :: Lens' TCState (Maybe Text)
- stImportedPartialDefs :: Lens' TCState (Set QName)
- stLocalPartialDefs :: Lens' TCState (Set QName)
- getPartialDefs :: ReadTCState m => m (Set QName)
- stLoadedFileCache :: Lens' TCState (Maybe LoadedFileCache)
- stBackends :: Lens' TCState [Backend_boot TCM]
- stProjectConfigs :: Lens' TCState (Map FilePath ProjectConfig)
- stAgdaLibFiles :: Lens' TCState (Map FilePath AgdaLibFile)
- stTopLevelModuleNames :: Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
- stImportedMetaStore :: Lens' TCState RemoteMetaStore
- stCopiedNames :: Lens' TCState (HashMap QName QName)
- stNameCopies :: Lens' TCState (HashMap QName (HashSet QName))
- stFreshNameId :: Lens' TCState NameId
- stFreshOpaqueId :: Lens' TCState OpaqueId
- stOpaqueBlocks :: Lens' TCState (Map OpaqueId OpaqueBlock)
- stOpaqueIds :: Lens' TCState (Map QName OpaqueId)
- stSyntaxInfo :: Lens' TCState HighlightingInfo
- stDisambiguatedNames :: Lens' TCState DisambiguatedNames
- stOpenMetaStore :: Lens' TCState LocalMetaStore
- stSolvedMetaStore :: Lens' TCState LocalMetaStore
- stInteractionPoints :: Lens' TCState InteractionPoints
- stAwakeConstraints :: Lens' TCState Constraints
- stSleepingConstraints :: Lens' TCState Constraints
- stDirty :: Lens' TCState Bool
- stOccursCheckDefs :: Lens' TCState (Set QName)
- stSignature :: Lens' TCState Signature
- stModuleCheckpoints :: Lens' TCState (Map ModuleName CheckpointId)
- stImportsDisplayForms :: Lens' TCState DisplayForms
- stImportedDisplayForms :: Lens' TCState DisplayForms
- stCurrentModule :: Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
- stInstanceDefs :: Lens' TCState TempInstanceTable
- sigInstances :: Lens' Signature InstanceTable
- stTemporaryInstances :: Lens' TCState (Set QName)
- stInstanceTree :: Lens' TCState (DiscrimTree QName)
- itableTree :: Lens' InstanceTable (DiscrimTree QName)
- stConcreteNames :: Lens' TCState ConcreteNames
- stUsedNames :: Lens' TCState (Map RawName (DList RawName))
- stShadowingNames :: Lens' TCState (Map Name (DList RawName))
- stStatistics :: Lens' TCState Statistics
- stTCWarnings :: Lens' TCState [TCWarning]
- stMutualBlocks :: Lens' TCState (Map MutualId MutualBlock)
- stLocalBuiltins :: Lens' TCState (BuiltinThings PrimFun)
- stFreshMetaId :: Lens' TCState MetaId
- stFreshMutualId :: Lens' TCState MutualId
- stFreshProblemId :: Lens' TCState ProblemId
- stFreshCheckpointId :: Lens' TCState CheckpointId
- stFreshInt :: Lens' TCState Int
- stAreWeCaching :: Lens' TCState Bool
- stPostponeInstanceSearch :: Lens' TCState Bool
- stConsideringInstance :: Lens' TCState Bool
- stInstantiateBlocking :: Lens' TCState Bool
- stBuiltinThings :: TCState -> BuiltinThings PrimFun
- unionBuiltin :: Builtin a -> Builtin a -> Builtin a
- nextFresh :: HasFresh i => TCState -> (i, TCState)
- freshName :: MonadFresh NameId m => Range -> String -> m Name
- freshNoName :: MonadFresh NameId m => Range -> m Name
- freshNoName_ :: MonadFresh NameId m => m Name
- freshRecordName :: MonadFresh NameId m => m Name
- stateTCLensM :: MonadTCState m => Lens' TCState a -> (a -> m (r, a)) -> m r
- iFullHash :: Interface -> Hash
- intSignature :: Lens' Interface Signature
- buildClosure :: (MonadTCEnv m, ReadTCState m) => a -> m (Closure a)
- fromCmp :: Comparison -> CompareDirection
- flipCmp :: CompareDirection -> CompareDirection
- dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
- suffixNameSuggestion :: MetaNameSuggestion -> ArgName -> MetaNameSuggestion
- getMetaInfo :: MetaVariable -> Closure Range
- normalMetaPriority :: MetaPriority
- lowMetaPriority :: MetaPriority
- highMetaPriority :: MetaPriority
- getMetaScope :: MetaVariable -> ScopeInfo
- getMetaEnv :: MetaVariable -> TCEnv
- getMetaSig :: MetaVariable -> Signature
- metaFrozen :: Lens' MetaVariable Frozen
- _mvInfo :: Lens' MetaVariable MetaInfo
- aModeToDef :: AbstractMode -> Maybe IsAbstract
- aDefToMode :: IsAbstract -> AbstractMode
- sigSections :: Lens' Signature Sections
- sigDefinitions :: Lens' Signature Definitions
- sigRewriteRules :: Lens' Signature RewriteRuleMap
- secTelescope :: Lens' Section Telescope
- defaultDisplayForm :: QName -> [LocalDisplayForm]
- lensTheDef :: Lens' Definition Defn
- defaultDefn :: ArgInfo -> QName -> Type -> Language -> Defn -> Definition
- noCompiledRep :: CompiledRepresentation
- jsBackendName :: BackendName
- ghcBackendName :: BackendName
- modifySystem :: (System -> System) -> ExtLamInfo -> ExtLamInfo
- projDropPars :: Projection -> ProjOrigin -> Term
- projArgInfo :: Projection -> ArgInfo
- setEtaEquality :: EtaEquality -> HasEta -> EtaEquality
- emptyCompKit :: CompKit
- defaultAxiom :: Defn
- constTranspAxiom :: Defn
- axiomConstTransp :: Defn -> Bool
- datarecPars :: Defn -> Int
- funClauses :: Defn -> [Clause]
- funCompiled :: Defn -> Maybe CompiledClauses
- funSplitTree :: Defn -> Maybe SplitTree
- funTreeless :: Defn -> Maybe Compiled
- funCovering :: Defn -> [Clause]
- funInv :: Defn -> FunctionInverse
- funMutual :: Defn -> Maybe [QName]
- funProjection :: Defn -> Either ProjectionLikenessMissing Projection
- funFlags :: Defn -> SmallSet FunctionFlag
- funTerminates :: Defn -> Maybe Bool
- funExtLam :: Defn -> Maybe ExtLamInfo
- funWith :: Defn -> Maybe QName
- funIsKanOp :: Defn -> Maybe QName
- funOpaque :: Defn -> IsOpaque
- dataPars :: Defn -> Nat
- dataIxs :: Defn -> Nat
- dataClause :: Defn -> Maybe Clause
- dataCons :: Defn -> [QName]
- dataSort :: Defn -> Sort
- dataMutual :: Defn -> Maybe [QName]
- dataAbstr :: Defn -> IsAbstract
- dataPathCons :: Defn -> [QName]
- dataTranspIx :: Defn -> Maybe QName
- dataTransp :: Defn -> Maybe QName
- recPars :: Defn -> Nat
- recClause :: Defn -> Maybe Clause
- recConHead :: Defn -> ConHead
- recNamedCon :: Defn -> Bool
- recFields :: Defn -> [Dom QName]
- recTel :: Defn -> Telescope
- recMutual :: Defn -> Maybe [QName]
- recEtaEquality' :: Defn -> EtaEquality
- recPatternMatching :: Defn -> PatternOrCopattern
- recInduction :: Defn -> Maybe Induction
- recTerminates :: Defn -> Maybe Bool
- recAbstr :: Defn -> IsAbstract
- recComp :: Defn -> CompKit
- conPars :: Defn -> Int
- conArity :: Defn -> Int
- conSrcCon :: Defn -> ConHead
- conData :: Defn -> QName
- conAbstr :: Defn -> IsAbstract
- conComp :: Defn -> CompKit
- conProj :: Defn -> Maybe [QName]
- conForced :: Defn -> [IsForced]
- conErased :: Defn -> Maybe [Bool]
- conErasure :: Defn -> Bool
- conInline :: Defn -> Bool
- primAbstr :: Defn -> IsAbstract
- primName :: Defn -> PrimitiveId
- primClauses :: Defn -> [Clause]
- primInv :: Defn -> FunctionInverse
- primCompiled :: Defn -> Maybe CompiledClauses
- primOpaque :: Defn -> IsOpaque
- primSortName :: Defn -> BuiltinSort
- primSortSort :: Defn -> Sort
- lensFunction :: Lens' Defn FunctionData
- lensConstructor :: Lens' Defn ConstructorData
- lensRecord :: Lens' Defn RecordData
- lensRecTel :: Lens' RecordData Telescope
- lensRecEta :: Lens' RecordData EtaEquality
- recRecursive :: Defn -> Bool
- recRecursive_ :: RecordData -> Bool
- recEtaEquality :: Defn -> HasEta
- _recEtaEquality :: RecordData -> HasEta
- emptyFunctionData :: HasOptions m => m FunctionData
- emptyFunctionData_ :: Bool -> FunctionData
- emptyFunction :: HasOptions m => m Defn
- emptyFunction_ :: Bool -> Defn
- funFlag_ :: FunctionFlag -> Lens' FunctionData Bool
- funFlag :: FunctionFlag -> Lens' Defn Bool
- funStatic :: Lens' Defn Bool
- funInline :: Lens' Defn Bool
- funMacro :: Lens' Defn Bool
- funMacro_ :: Lens' FunctionData Bool
- funFirstOrder :: Lens' Defn Bool
- funErasure :: Lens' Defn Bool
- funAbstract :: Lens' Defn Bool
- funAbstr :: Lens' Defn IsAbstract
- funAbstract_ :: Lens' FunctionData Bool
- funAbstr_ :: Lens' FunctionData IsAbstract
- funProj :: Lens' Defn Bool
- funProj_ :: Lens' FunctionData Bool
- isMacro :: Defn -> Bool
- isEmptyFunction :: Defn -> Bool
- isExtendedLambda :: Defn -> Bool
- isWithFunction :: Defn -> Bool
- isCopatternLHS :: [Clause] -> Bool
- recCon :: Defn -> QName
- defIsRecord :: Defn -> Bool
- defIsDataOrRecord :: Defn -> Bool
- defConstructors :: Defn -> [QName]
- redReturn :: a -> ReduceM (Reduced a' a)
- redBind :: ReduceM (Reduced a a') -> (a -> b) -> (a' -> ReduceM (Reduced b b')) -> ReduceM (Reduced b b')
- notReduced :: a -> MaybeReduced a
- reduced :: Blocked (Arg Term) -> MaybeReduced (Arg Term)
- allReductions :: AllowedReductions
- reallyAllReductions :: AllowedReductions
- reduceAllDefs :: ReduceDefs
- locallyReduceDefs :: MonadTCEnv m => ReduceDefs -> m a -> m a
- locallyTC :: MonadTCEnv m => Lens' TCEnv a -> (a -> a) -> m b -> m b
- eReduceDefs :: Lens' TCEnv ReduceDefs
- locallyReduceAllDefs :: MonadTCEnv m => m a -> m a
- shouldReduceDef :: MonadTCEnv m => QName -> m Bool
- asksTC :: MonadTCEnv m => (TCEnv -> a) -> m a
- toReduceDefs :: (Bool, [QName]) -> ReduceDefs
- fromReduceDefs :: ReduceDefs -> (Bool, [QName])
- locallyReconstructed :: MonadTCEnv m => m a -> m a
- eReconstructed :: Lens' TCEnv Bool
- isReconstructed :: MonadTCEnv m => m Bool
- 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]
- defNonterminating :: Definition -> Bool
- defTerminationUnconfirmed :: Definition -> Bool
- defForced :: Definition -> [IsForced]
- itableCounts :: Lens' InstanceTable (Map QName Int)
- ifTopLevelAndHighlightingLevelIsOr :: MonadTCEnv tcm => HighlightingLevel -> Bool -> tcm () -> tcm ()
- ifTopLevelAndHighlightingLevelIs :: MonadTCEnv tcm => HighlightingLevel -> tcm () -> tcm ()
- initEnv :: TCEnv
- defaultUnquoteFlags :: UnquoteFlags
- unquoteNormalise :: Lens' UnquoteFlags Bool
- eUnquoteNormalise :: Lens' TCEnv Bool
- eUnquoteFlags :: Lens' TCEnv UnquoteFlags
- eContext :: Lens' TCEnv Context
- eLetBindings :: Lens' TCEnv LetBindings
- eCurrentModule :: Lens' TCEnv ModuleName
- eCurrentPath :: Lens' TCEnv (Maybe AbsolutePath)
- eAnonymousModules :: Lens' TCEnv [(ModuleName, Nat)]
- eImportPath :: Lens' TCEnv [TopLevelModuleName]
- eMutualBlock :: Lens' TCEnv (Maybe MutualId)
- eTerminationCheck :: Lens' TCEnv (TerminationCheck ())
- eCoverageCheck :: Lens' TCEnv CoverageCheck
- eMakeCase :: Lens' TCEnv Bool
- eSolvingConstraints :: Lens' TCEnv Bool
- eCheckingWhere :: Lens' TCEnv Bool
- eWorkingOnTypes :: Lens' TCEnv Bool
- eAssignMetas :: Lens' TCEnv Bool
- eActiveProblems :: Lens' TCEnv (Set ProblemId)
- eAbstractMode :: Lens' TCEnv AbstractMode
- eRelevance :: Lens' TCEnv Relevance
- eQuantity :: Lens' TCEnv Quantity
- eHardCompileTimeMode :: Lens' TCEnv Bool
- eSplitOnStrict :: Lens' TCEnv Bool
- eDisplayFormsEnabled :: Lens' TCEnv Bool
- eFoldLetBindings :: Lens' TCEnv Bool
- eRange :: Lens' TCEnv Range
- eHighlightingRange :: Lens' TCEnv Range
- eCall :: Lens' TCEnv (Maybe (Closure Call))
- eHighlightingLevel :: Lens' TCEnv HighlightingLevel
- eHighlightingMethod :: Lens' TCEnv HighlightingMethod
- eExpandLast :: Lens' TCEnv ExpandHidden
- eExpandLastBool :: Lens' TCEnv Bool
- isExpandLast :: ExpandHidden -> Bool
- toExpandLast :: Bool -> ExpandHidden
- eAppDef :: Lens' TCEnv (Maybe QName)
- eSimplification :: Lens' TCEnv Simplification
- eAllowedReductions :: Lens' TCEnv AllowedReductions
- eReduceDefsPair :: Lens' TCEnv (Bool, [QName])
- eInjectivityDepth :: Lens' TCEnv Int
- eCompareBlocked :: Lens' TCEnv Bool
- ePrintDomainFreePi :: Lens' TCEnv Bool
- ePrintMetasBare :: Lens' TCEnv Bool
- eInsideDotPattern :: Lens' TCEnv Bool
- eInstanceDepth :: Lens' TCEnv Int
- eIsDebugPrinting :: Lens' TCEnv Bool
- ePrintingPatternLambdas :: Lens' TCEnv [QName]
- eCallByNeed :: Lens' TCEnv Bool
- eCurrentCheckpoint :: Lens' TCEnv CheckpointId
- eCheckpoints :: Lens' TCEnv (Map CheckpointId Substitution)
- eGeneralizeMetas :: Lens' TCEnv DoGeneralize
- eGeneralizedVars :: Lens' TCEnv (Map QName GeneralizedValue)
- eActiveBackendName :: Lens' TCEnv (Maybe BackendName)
- eConflComputingOverlap :: Lens' TCEnv Bool
- eCurrentlyElaborating :: Lens' TCEnv Bool
- currentModality :: MonadTCEnv m => m Modality
- viewTC :: MonadTCEnv m => Lens' TCEnv a -> m a
- onLetBindingType :: (Dom Type -> Dom Type) -> LetBinding -> LetBinding
- isDontExpandLast :: ExpandHidden -> Bool
- recordFieldWarningToError :: RecordFieldWarning -> TypeError
- warningName :: Warning -> WarningName
- illegalRewriteWarningName :: IllegalRewriteRuleReason -> WarningName
- isSourceCodeWarning :: WarningName -> Bool
- tcWarningOrigin :: TCWarning -> SrcFile
- sizedTypesOption :: HasOptions m => m Bool
- guardednessOption :: HasOptions m => m Bool
- withoutKOption :: HasOptions m => m Bool
- cubicalOption :: HasOptions m => m (Maybe Cubical)
- cubicalCompatibleOption :: HasOptions m => m Bool
- enableCaching :: HasOptions m => m Bool
- mapRedEnv :: (TCEnv -> TCEnv) -> ReduceEnv -> ReduceEnv
- mapRedSt :: (TCState -> TCState) -> ReduceEnv -> ReduceEnv
- mapRedEnvSt :: (TCEnv -> TCEnv) -> (TCState -> TCState) -> ReduceEnv -> ReduceEnv
- reduceEnv :: Lens' ReduceEnv TCEnv
- reduceSt :: Lens' ReduceEnv TCState
- unKleisli :: (a -> ReduceM b) -> ReduceM (a -> b)
- onReduceEnv :: (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a
- fmapReduce :: (a -> b) -> ReduceM a -> ReduceM b
- apReduce :: ReduceM (a -> b) -> ReduceM a -> ReduceM b
- thenReduce :: ReduceM a -> ReduceM b -> ReduceM b
- beforeReduce :: ReduceM a -> ReduceM b -> ReduceM a
- bindReduce :: ReduceM a -> (a -> ReduceM b) -> ReduceM b
- runReduceF :: (a -> ReduceM b) -> TCM (a -> b)
- localR :: (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a
- getsTC :: ReadTCState m => (TCState -> a) -> m a
- modifyTC' :: MonadTCState m => (TCState -> TCState) -> m ()
- setTCLens :: MonadTCState m => Lens' TCState a -> a -> m ()
- setTCLens' :: MonadTCState m => Lens' TCState a -> a -> m ()
- modifyTCLens :: MonadTCState m => Lens' TCState a -> (a -> a) -> m ()
- modifyTCLens' :: MonadTCState m => Lens' TCState a -> (a -> a) -> m ()
- modifyTCLensM :: MonadTCState m => Lens' TCState a -> (a -> m a) -> m ()
- stateTCLens :: MonadTCState m => Lens' TCState a -> (a -> (r, a)) -> m r
- runBlocked :: Monad m => BlockT m a -> m (Either Blocker a)
- pureTCM :: MonadIO m => (TCState -> TCEnv -> a) -> TCMT m a
- returnTCMT :: Applicative m => a -> TCMT m a
- bindTCMT :: Monad m => TCMT m a -> (a -> TCMT m b) -> TCMT m b
- thenTCMT :: Applicative m => TCMT m a -> TCMT m b -> TCMT m b
- fmapTCMT :: Functor m => (a -> b) -> TCMT m a -> TCMT m b
- apTCMT :: Applicative m => TCMT m (a -> b) -> TCMT m a -> TCMT m b
- catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a
- finally_ :: TCM a -> TCM b -> TCM a
- typeError' :: MonadTCError m => CallStack -> TypeError -> m a
- locatedTypeError :: MonadTCError m => (a -> TypeError) -> HasCallStack => a -> m b
- genericDocError :: (HasCallStack, MonadTCError m) => Doc -> m a
- typeError'_ :: (MonadTCEnv m, ReadTCState m) => CallStack -> TypeError -> m TCErr
- typeError_ :: (HasCallStack, MonadTCEnv m, ReadTCState m) => TypeError -> m 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 ()
- patternInTeleName :: String
- extendedLambdaName :: String
- isExtendedLambdaName :: QName -> Bool
- absurdLambdaName :: String
- isAbsurdLambdaName :: QName -> Bool
- generalizedFieldName :: String
- getGeneralizedFieldName :: QName -> Maybe String
- module Agda.TypeChecking.Monad.Base.Types
- class (Functor m, Applicative m, Monad m) => HasOptions m where
- data RecordFieldWarning
Documentation
data Constraint Source #
Constructors
| ValueCmp Comparison CompareAs Term Term | |
| ValueCmpOnFace Comparison Term Type Term Term | |
| ElimCmp [Polarity] [IsForced] Type Term [Elim] [Elim] | |
| SortCmp Comparison Sort Sort | |
| LevelCmp Comparison Level Level | |
| HasBiggerSort Sort | |
| HasPTSRule (Dom Type) (Abs Sort) | |
| CheckDataSort QName Sort | Check that the sort |
| CheckMetaInst MetaId | |
| CheckType Type | |
| UnBlock MetaId | Meta created for a term blocked by a postponed type checking problem or unsolved
constraints. The |
| IsEmpty Range Type | The range is the one of the absurd pattern. |
| CheckSizeLtSat Term | Check that the |
| FindInstance MetaId (Maybe [Candidate]) | the first argument is the instance argument and the second one is the list of candidates (or Nothing if we haven’t determined the list of candidates yet) |
| ResolveInstanceHead QName | Resolve the head symbol of the type that the given instance targets |
| CheckFunDef DefInfo QName [Clause] TCErr | Last argument is the error causing us to postpone. |
| UnquoteTactic Term Term Type | First argument is computation and the others are hole and goal type |
| CheckLockedVars Term Type (Arg Term) Type |
|
| UsableAtModality WhyCheckModality (Maybe Sort) Modality Term | Is the term usable at the given modality?
This check should run if the |
Instances
Constructors
Instances
data Comparison Source #
Instances
| 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 Methods prettyTCM :: MonadPretty m => Comparison -> m Doc Source # | |
| EmbPrj Comparison Source # | |
| Generic Comparison Source # | |
Defined in Agda.TypeChecking.Monad.Base Associated Types type Rep Comparison :: Type -> Type # | |
| Show Comparison Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Comparison -> ShowS # show :: Comparison -> String # showList :: [Comparison] -> ShowS # | |
| NFData Comparison Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: Comparison -> () # | |
| Eq Comparison Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| type Rep Comparison Source # | |
data ModuleInfo Source #
Constructors
| ModuleInfo | |
Fields
| |
Instances
| Generic ModuleInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base Associated Types type Rep ModuleInfo :: Type -> Type # | |
| NFData ModuleInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: ModuleInfo -> () # | |
| type Rep ModuleInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base type Rep ModuleInfo = D1 ('MetaData "ModuleInfo" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "ModuleInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "miInterface") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Interface) :*: S1 ('MetaSel ('Just "miWarnings") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TCWarning])) :*: (S1 ('MetaSel ('Just "miPrimitive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "miMode") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleCheckMode)))) | |
data Definition Source #
Constructors
| Defn | |
Fields
| |
Instances
Constructors
| Builtin Term | |
| Prim pf | |
| BuiltinRewriteRelations (Set QName) |
|
Instances
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
| NamesIn System Source # | |
Defined in Agda.Syntax.Internal.Names | |
| KillRange System Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| InstantiateFull System Source # | |
Defined in Agda.TypeChecking.Reduce | |
| EmbPrj System Source # | |
| Abstract System Source # | |
| Apply System Source # | |
| Generic System Source # | |
| Show System Source # | |
| NFData System Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| Reify (QNamed System) Source # | |
| type Rep System Source # | |
Defined in Agda.TypeChecking.Monad.Base type Rep System = D1 ('MetaData "System" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "System" 'PrefixI 'True) (S1 ('MetaSel ('Just "systemTel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope) :*: S1 ('MetaSel ('Just "systemClauses") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Face, Term)]))) | |
| type ReifiesTo (QNamed System) Source # | |
Defined in Agda.Syntax.Translation.InternalToAbstract | |
Instances
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
Polarity for equality and subtype checking.
Constructors
| Covariant | monotone |
| Contravariant | antitone |
| Invariant | no information (mixed variance) |
| Nonvariant | constant |
Instances
| Pretty Polarity Source # | |
| KillRange Polarity Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| PrettyTCM Polarity Source # | |
Defined in Agda.TypeChecking.Pretty | |
| EmbPrj Polarity Source # | |
| Generic Polarity Source # | |
| Show Polarity Source # | |
| NFData Polarity Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| Eq Polarity Source # | |
| Abstract [Polarity] Source # | |
| Apply [Polarity] Source # | |
| type Rep Polarity Source # | |
Defined in Agda.TypeChecking.Monad.Base type Rep Polarity = D1 ('MetaData "Polarity" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) ((C1 ('MetaCons "Covariant" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Contravariant" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Invariant" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Nonvariant" 'PrefixI 'False) (U1 :: Type -> Type))) | |
A thing tagged with the context it came from. Also keeps the substitution from previous checkpoints. This lets us handle the case when an open thing was created in a context that we have since exited. Remember which module it's from to make sure we don't get confused by checkpoints from other files.
Constructors
| OpenThing | |
Instances
MetaInfo is cloned from one meta to the next during pruning.
Constructors
| MetaInfo | |
Fields
| |
Instances
type Constraints = [ProblemConstraint] Source #
data WarningsAndNonFatalErrors Source #
Assorted warnings and errors to be displayed to the user
Constructors
| WarningsAndNonFatalErrors | |
Fields
| |
Constructors
| Sig | |
Fields
| |
Instances
| KillRange Signature Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| InstantiateFull Signature Source # | |
Defined in Agda.TypeChecking.Reduce | |
| EmbPrj Signature Source # | |
| Generic Signature Source # | |
| Show Signature Source # | |
| NFData Signature Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| type Rep Signature Source # | |
Defined in Agda.TypeChecking.Monad.Base type Rep Signature = D1 ('MetaData "Signature" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "Sig" 'PrefixI 'True) ((S1 ('MetaSel ('Just "_sigSections") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sections) :*: S1 ('MetaSel ('Just "_sigDefinitions") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Definitions)) :*: (S1 ('MetaSel ('Just "_sigRewriteRules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RewriteRuleMap) :*: S1 ('MetaSel ('Just "_sigInstances") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InstanceTable)))) | |
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 [Range] | `UnreachableClauses f rs` means that the clauses in |
| CoverageIssue QName [(Telescope, [NamedArg DeBruijnPattern])] | `CoverageIssue f pss` means that |
| CoverageNoExactSplit QName [Clause] | |
| InlineNoExactSplit QName Clause |
|
| NotStrictlyPositive QName (Seq OccursWhere) | |
| ConstructorDoesNotFitInData QName Sort Sort TCErr | Checking whether constructor |
| CoinductiveEtaRecord QName | A record type declared as both |
| UnsolvedMetaVariables [Range] | Do not use directly with |
| UnsolvedInteractionMetas [Range] | Do not use directly with |
| UnsolvedConstraints Constraints | Do not use directly with |
| InteractionMetaBoundaries [Range] | Do not use directly with |
| CantGeneralizeOverSorts [MetaId] | |
| AbsurdPatternRequiresNoRHS [NamedArg DeBruijnPattern] | |
| OldBuiltin BuiltinId BuiltinId | In `OldBuiltin old new`, the BUILTIN old has been replaced by new. |
| BuiltinDeclaresIdentifier BuiltinId | The builtin declares a new identifier, so it should not be in scope. |
| DuplicateRecordDirective RecordDirective | The given record directive is conflicting with a prior one in the same record declaration. |
| EmptyRewritePragma | If the user wrote just |
| EmptyWhere | An empty |
| IllformedAsClause String | If the user wrote something other than an unqualified name
in the |
| InvalidCharacterLiteral Char | A character literal Agda does not support, e.g. surrogate code points. |
| ClashesViaRenaming NameOrModule [Name] | If a |
| UselessPatternDeclarationForRecord String | The 'pattern' declaration is useless in the presence
of either |
| UselessPragma Range Doc | Warning when pragma is useless and thus ignored.
|
| UselessPublic | If the user opens a module public before the module header. (See issue #2377.) |
| UselessHiding [ImportedName] | Names in |
| 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. |
| NoGuardednessFlag QName | A coinductive record was declared but neither --guardedness nor --sized-types is enabled. |
| SafeFlagPostulate Name | |
| SafeFlagPragma [String] | Unsafe OPTIONS. |
| SafeFlagWithoutKFlagPrimEraseEquality | |
| WithoutKFlagPrimEraseEquality | |
| ConflictingPragmaOptions String String | `ConflictingPragmaOptions a b`: Inconsistent options `--a` and `--no-b`, since `--a` implies `--b`. Ignoring `--no-b`. |
| OptionWarning OptionWarning | |
| ParseWarning ParseWarning | |
| LibraryWarning LibWarning | |
| DeprecationWarning String String String | `DeprecationWarning old new version`:
|
| UserWarning Text | User-defined warning (e.g. to mention that a name is deprecated) |
| DuplicateUsing (List1 ImportedName) | Duplicate mentions of the same name in |
| FixityInRenamingModule (List1 Range) | Fixity of modules cannot be changed via renaming (since modules have no fixity). |
| ModuleDoesntExport QName [Name] [Name] [ImportedName] | Some imported names are not actually exported by the source module. The second argument is the names that could be exported. The third argument is the module names that could be exported. |
| InfectiveImport Doc | Importing a file using an infective option into one which doesn't |
| CoInfectiveImport Doc | Importing a file not using a coinfective option from one which does |
| ConfluenceCheckingIncompleteBecauseOfMeta QName | Confluence checking incomplete because the definition of the |
| ConfluenceForCubicalNotSupported | Confluence checking with |
| IllegalRewriteRule QName IllegalRewriteRuleReason | |
| RewriteNonConfluent Term Term Term Doc | Confluence checker found critical pair and equality checking resulted in a type error |
| RewriteMaybeNonConfluent Term Term [Doc] | Confluence checker got stuck on computing overlap between two rewrite rules |
| RewriteAmbiguousRules Term Term Term | The global confluence checker found a term |
| RewriteMissingRule Term Term Term | The global confluence checker found a term |
| PragmaCompileErased BackendName QName | COMPILE directive for an erased symbol. |
| PragmaCompileList |
|
| PragmaCompileMaybe |
|
| NoMain TopLevelModuleName | Compiler run on module that does not have a |
| NotInScopeW [QName] | Out of scope error we can recover from. |
| UnsupportedIndexedMatch Doc | Was not able to compute a full equivalence when splitting. |
| AsPatternShadowsConstructorOrPatternSynonym LHSOrPatSyn | The as-name in an as-pattern may not shadow a constructor ( |
| PatternShadowsConstructor Name QName | A pattern variable has the name of a constructor (data constructor or matchable record constructor). |
| PlentyInHardCompileTimeMode QωOrigin | Explicit use of @ |
| RecordFieldWarning RecordFieldWarning | |
| MissingTypeSignatureForOpaque QName IsOpaque | An |
| NotAffectedByOpaque | |
| UnfoldTransparentName QName | |
| UselessOpaque | |
| FaceConstraintCannotBeHidden ArgInfo | Face constraint patterns |
| FaceConstraintCannotBeNamed NamedName | Face constraint patterns |
| DuplicateInterfaceFiles AbsolutePath AbsolutePath | `DuplicateInterfaceFiles selectedInterfaceFile ignoredInterfaceFile` |
| CustomBackendWarning String Doc | Used for backend-specific warnings. The string is the backend name. |
Instances
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 Blocker | The exception which is usually caught.
Raised for pattern violations during unification ( |
Instances
Constructors
| TCWarning | |
Fields
| |
Instances
For printing, we couple a meta with its name suggestion.
Constructors
| NamedMeta | |
Fields | |
type ModuleToSource = Map TopLevelModuleName AbsolutePath Source #
Maps top-level module names to the corresponding source file names.
type Definitions = HashMap QName Definition Source #
type InteractionOutputCallback = Response_boot TCErr TCWarning WarningsAndNonFatalErrors -> TCM () Source #
Callback fuction to call when there is a response to give to the interactive frontend.
Note that the response is given in pieces and incrementally, so the user can have timely response even during long computations.
Typical InteractionOutputCallback functions:
- Convert the response into a
Stringrepresentation and print it on standard output (suitable for inter-process communication). - Put the response into a mutable variable stored in the
closure of the
InteractionOutputCallbackfunction. (suitable for intra-process communication).
Datatype representing a single boundary condition: x_0 = u_0, ... ,x_n = u_n ⊢ t = ?n es
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.
Minimal complete definition
Nothing
Methods
default askTC :: (MonadTrans t, MonadTCEnv n, t n ~ m) => m TCEnv Source #
localTC :: (TCEnv -> TCEnv) -> m a -> m a Source #
default localTC :: (MonadTransControl t, MonadTCEnv n, t n ~ m) => (TCEnv -> TCEnv) -> m a -> m a Source #
Instances
| MonadTCEnv IM Source # | |
| MonadTCEnv AbsToCon Source # | |
| MonadTCEnv TerM Source # | |
| MonadTCEnv ReduceM Source # | |
| MonadTCEnv NLM Source # | |
| MonadTCEnv m => MonadTCEnv (PureConversionT m) Source # | |
Defined in Agda.TypeChecking.Conversion.Pure Methods askTC :: PureConversionT m TCEnv Source # localTC :: (TCEnv -> TCEnv) -> PureConversionT m a -> PureConversionT m a Source # | |
| MonadTCEnv m => MonadTCEnv (BlockT m) Source # | |
| MonadIO m => MonadTCEnv (TCMT m) Source # | |
| MonadTCEnv m => MonadTCEnv (NamesT m) Source # | |
| MonadTCEnv m => MonadTCEnv (ListT m) Source # | |
| MonadTCEnv m => MonadTCEnv (ChangeT m) Source # | |
| MonadTCEnv m => MonadTCEnv (MaybeT m) Source # | |
| MonadTCEnv m => MonadTCEnv (ExceptT err m) Source # | |
| MonadTCEnv m => MonadTCEnv (IdentityT 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 # | |
class (Applicative tcm, MonadIO tcm, MonadTCEnv tcm, MonadTCState tcm, HasOptions tcm) => MonadTCM tcm where Source #
Embedding a TCM computation.
Minimal complete definition
Nothing
Methods
Instances
| MonadTCM IM Source # | |
| MonadTCM TerM Source # | |
| MonadTCM m => MonadTCM (BlockT m) Source # | |
| MonadIO m => MonadTCM (TCMT m) Source # | |
| MonadTCM m => MonadTCM (NamesT m) Source # | |
| MonadTCM tcm => MonadTCM (ListT tcm) Source # | |
| MonadTCM tcm => MonadTCM (ChangeT tcm) Source # | |
| MonadTCM tcm => MonadTCM (MaybeT tcm) Source # | |
| MonadTCM tcm => MonadTCM (ExceptT err tcm) Source # | |
| MonadTCM tcm => MonadTCM (IdentityT tcm) Source # | |
| MonadTCM tcm => MonadTCM (ReaderT r tcm) Source # | |
| MonadTCM tcm => MonadTCM (StateT s tcm) Source # | |
| (Monoid w, MonadTCM tcm) => MonadTCM (WriterT w tcm) Source # | |
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.
Minimal complete definition
Nothing
Methods
default getTC :: (MonadTrans t, MonadTCState n, t n ~ m) => m TCState Source #
putTC :: TCState -> m () Source #
default putTC :: (MonadTrans t, MonadTCState n, t n ~ m) => TCState -> m () Source #
modifyTC :: (TCState -> TCState) -> m () Source #
default modifyTC :: (MonadTrans t, MonadTCState n, t n ~ m) => (TCState -> TCState) -> m () Source #
Instances
| MonadTCState IM Source # | |
| MonadTCState TerM Source # | |
| MonadTCState m => MonadTCState (BlockT m) Source # | |
| MonadIO m => MonadTCState (TCMT m) Source # | |
| MonadTCState m => MonadTCState (NamesT m) Source # | |
| MonadTCState m => MonadTCState (ListT m) Source # | |
| MonadTCState m => MonadTCState (ChangeT m) Source # | |
| MonadTCState m => MonadTCState (MaybeT m) Source # | |
| MonadTCState m => MonadTCState (ExceptT err m) Source # | |
| MonadTCState m => MonadTCState (IdentityT 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 # | |
class Monad m => ReadTCState m where Source #
Minimal complete definition
Nothing
Methods
getTCState :: m TCState Source #
default getTCState :: (MonadTrans t, ReadTCState n, t n ~ m) => m TCState Source #
locallyTCState :: Lens' TCState a -> (a -> a) -> m b -> m b Source #
default locallyTCState :: (MonadTransControl t, ReadTCState n, t n ~ m) => Lens' TCState a -> (a -> a) -> m b -> m b Source #
withTCState :: (TCState -> TCState) -> m a -> m a Source #
Instances
Instances
data LHSOrPatSyn Source #
Distinguish error message when parsing lhs or pattern synonym, resp.
Instances
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 the first dfPatternVars variables are pattern variables
that matches any term.
Constructors
| Display | |
Fields
| |
Instances
Constructors
Instances
Constructors
| Closure | |
Fields
| |
Instances
class (Applicative m, MonadTCEnv m, ReadTCState m, HasOptions m) => MonadReduce m where Source #
Minimal complete definition
Nothing
Methods
liftReduce :: ReduceM a -> m a Source #
default liftReduce :: (MonadTrans t, MonadReduce n, t n ~ m) => ReduceM a -> m a Source #
Instances
data CompilerPragma Source #
The backends are responsible for parsing their own pragmas.
Constructors
| CompilerPragma Range String |
Instances
Constructors
| TCEnv | |
Fields
| |
Instances
Constructors
| Interface | |
Fields
| |
Instances
type MonadTCError m = (MonadTCEnv m, ReadTCState m, MonadError TCErr m) Source #
The constraints needed for typeError and similar.
type BackendName = String Source #
Constructors
| TCSt | |
Fields
| |
Instances
type RewriteRules = [RewriteRule] Source #
Constructors
| PrimFun | |
Fields
| |
Instances
| NamesIn PrimFun Source # | Note that the |
Defined in Agda.Syntax.Internal.Names | |
| Abstract PrimFun Source # | |
| Apply PrimFun Source # | |
| Generic PrimFun Source # | |
| NFData PrimFun Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| type Rep PrimFun Source # | |
Defined in Agda.TypeChecking.Monad.Base type Rep PrimFun = D1 ('MetaData "PrimFun" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "PrimFun" 'PrefixI 'True) ((S1 ('MetaSel ('Just "primFunName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "primFunArity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Arity)) :*: (S1 ('MetaSel ('Just "primFunArgOccurrences") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Occurrence]) :*: S1 ('MetaSel ('Just "primFunImplementation") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ([Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)))))) | |
data RunMetaOccursCheck Source #
Constructors
| RunMetaOccursCheck | |
| DontRunMetaOccursCheck |
Instances
We can either compare two terms at a given type, or compare two types without knowing (or caring about) their sorts.
Constructors
| AsTermsOf Type |
|
| AsSizes | Replaces |
| AsTypes |
Instances
data CompareDirection Source #
An extension of Comparison to >=.
Instances
| Pretty CompareDirection Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods pretty :: CompareDirection -> Doc Source # prettyPrec :: Int -> CompareDirection -> Doc Source # prettyList :: [CompareDirection] -> Doc Source # | |
| Show CompareDirection Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> CompareDirection -> ShowS # show :: CompareDirection -> String # showList :: [CompareDirection] -> ShowS # | |
| Eq CompareDirection Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods (==) :: CompareDirection -> CompareDirection -> Bool # (/=) :: CompareDirection -> CompareDirection -> Bool # | |
data MetaVariable Source #
Information about local meta-variables.
Constructors
| MetaVar | |
Fields
| |
Instances
data InstanceInfo Source #
Information about an instance definition.
Constructors
| InstanceInfo | |
Fields
| |
Instances
| KillRange InstanceInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| EmbPrj InstanceInfo Source # | |
| Generic InstanceInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base Associated Types type Rep InstanceInfo :: Type -> Type # | |
| Show InstanceInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> InstanceInfo -> ShowS # show :: InstanceInfo -> String # showList :: [InstanceInfo] -> ShowS # | |
| NFData InstanceInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: InstanceInfo -> () # | |
| type Rep InstanceInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base type Rep InstanceInfo = D1 ('MetaData "InstanceInfo" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "InstanceInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "instanceClass") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "instanceOverlap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OverlapMode))) | |
class Monad m => MonadBlock m where Source #
Minimal complete definition
Methods
patternViolation :: Blocker -> m a Source #
`patternViolation b` aborts the current computation
default patternViolation :: (MonadTrans t, MonadBlock n, m ~ t n) => Blocker -> m a Source #
catchPatternErr :: (Blocker -> m a) -> m a -> m a Source #
`catchPatternErr handle m` runs m, handling pattern violations
with handle (doesn't roll back the state)
Instances
| MonadBlock TCM Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| MonadBlock NLM Source # | |
Defined in Agda.TypeChecking.Rewriting.NonLinMatch | |
| Monad m => MonadBlock (PureConversionT m) Source # | |
Defined in Agda.TypeChecking.Conversion.Pure Methods patternViolation :: Blocker -> PureConversionT m a Source # catchPatternErr :: (Blocker -> PureConversionT m a) -> PureConversionT m a -> PureConversionT m a Source # | |
| Monad m => MonadBlock (BlockT m) Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| MonadBlock m => MonadBlock (MaybeT m) Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| Monad m => MonadBlock (ExceptT TCErr m) Source # | |
| MonadBlock m => MonadBlock (ReaderT e m) Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
Constructors
| NoReduction no | |
| YesReduction Simplification yes |
data ProblemConstraint Source #
Constructors
| PConstr | |
Fields | |
Instances
data ForeignCode Source #
Constructors
| ForeignCode Range String |
Instances
| EmbPrj ForeignCode Source # | |
| Generic ForeignCode Source # | |
Defined in Agda.TypeChecking.Monad.Base Associated Types type Rep ForeignCode :: Type -> Type # | |
| Show ForeignCode Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> ForeignCode -> ShowS # show :: ForeignCode -> String # showList :: [ForeignCode] -> ShowS # | |
| NFData ForeignCode Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: ForeignCode -> () # | |
| type Rep ForeignCode Source # | |
Defined in Agda.TypeChecking.Monad.Base type Rep ForeignCode = D1 ('MetaData "ForeignCode" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "ForeignCode" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) | |
data LetBinding Source #
Instances
Constructors
| Section | |
Fields | |
Instances
| Pretty Section Source # | |
| NamesIn Section Source # | |
Defined in Agda.Syntax.Internal.Names | |
| KillRange Section Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| KillRange Sections Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| InstantiateFull Section Source # | |
Defined in Agda.TypeChecking.Reduce | |
| EmbPrj Section Source # | |
| Show Section Source # | |
| NFData Section Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| Eq Section Source # | |
data PreScopeState Source #
Constructors
| PreScopeState | |
Fields
| |
Instances
data PostScopeState Source #
Constructors
| PostScopeState | |
Fields
| |
Instances
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
type BuiltinThings pf = Map SomeBuiltin (Builtin pf) Source #
type DisplayForms = HashMap QName [LocalDisplayForm] Source #
type RemoteMetaStore = HashMap MetaId RemoteMetaVariable Source #
Used for meta-variables from other modules (and in Interfaces).
data DisambiguatedName Source #
Name disambiguation for the sake of highlighting.
Constructors
| DisambiguatedName NameKind QName |
Instances
| Generic DisambiguatedName Source # | |
Defined in Agda.TypeChecking.Monad.Base Associated Types type Rep DisambiguatedName :: Type -> Type # Methods from :: DisambiguatedName -> Rep DisambiguatedName x # to :: Rep DisambiguatedName x -> DisambiguatedName # | |
| NFData DisambiguatedName Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: DisambiguatedName -> () # | |
| type Rep DisambiguatedName Source # | |
Defined in Agda.TypeChecking.Monad.Base type Rep DisambiguatedName = D1 ('MetaData "DisambiguatedName" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "DisambiguatedName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NameKind) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) | |
type LocalMetaStore = Map MetaId MetaVariable Source #
Used for meta-variables from the current module.
type InteractionPoints = BiMap 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)
newtype CheckpointId Source #
Constructors
| CheckpointId Int |
Instances
newtype ForeignCodeStack Source #
Foreign code fragments are stored in reversed order to support efficient appending: head points to the latest pragma in module.
Constructors
| ForeignCodeStack | |
Fields | |
Instances
| EmbPrj ForeignCodeStack Source # | |
| Generic ForeignCodeStack Source # | |
Defined in Agda.TypeChecking.Monad.Base Associated Types type Rep ForeignCodeStack :: Type -> Type # Methods from :: ForeignCodeStack -> Rep ForeignCodeStack x # to :: Rep ForeignCodeStack x -> ForeignCodeStack # | |
| Show ForeignCodeStack Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> ForeignCodeStack -> ShowS # show :: ForeignCodeStack -> String # showList :: [ForeignCodeStack] -> ShowS # | |
| NFData ForeignCodeStack Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: ForeignCodeStack -> () # | |
| type Rep ForeignCodeStack Source # | |
Defined in Agda.TypeChecking.Monad.Base type Rep ForeignCodeStack = D1 ('MetaData "ForeignCodeStack" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'True) (C1 ('MetaCons "ForeignCodeStack" 'PrefixI 'True) (S1 ('MetaSel ('Just "getForeignCodeStack") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ForeignCode]))) | |
Instances
| KillRange MutualId Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| HasFresh MutualId Source # | |
| EmbPrj MutualId Source # | |
| Enum MutualId Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| Num MutualId Source # | |
| Show MutualId Source # | |
| NFData MutualId Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| Eq MutualId Source # | |
| Ord MutualId Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
data MutualBlock Source #
A mutual block of names in the signature.
Constructors
| MutualBlock | |
Fields
| |
Instances
data OpaqueBlock Source #
A block of opaque definitions.
Constructors
| OpaqueBlock | |
Fields
| |
Instances
data LoadedFileCache Source #
Constructors
| LoadedFileCache | |
Fields | |
Instances
| Generic LoadedFileCache Source # | |
Defined in Agda.TypeChecking.Monad.Base Associated Types type Rep LoadedFileCache :: Type -> Type # Methods from :: LoadedFileCache -> Rep LoadedFileCache x # to :: Rep LoadedFileCache x -> LoadedFileCache # | |
| NFData LoadedFileCache Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: LoadedFileCache -> () # | |
| type Rep LoadedFileCache Source # | |
Defined in Agda.TypeChecking.Monad.Base type Rep LoadedFileCache = D1 ('MetaData "LoadedFileCache" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "LoadedFileCache" 'PrefixI 'True) (S1 ('MetaSel ('Just "lfcCached") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 CachedTypeCheckLog) :*: S1 ('MetaSel ('Just "lfcCurrent") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 CurrentTypeCheckLog))) | |
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:
PragmasEnterSection, entering the main module.DeclEnterSectionLeaveSection, for declarations and nested modulesLeaveSection, leaving the main module.
Constructors
| EnterSection !Erased !ModuleName !Telescope | |
| LeaveSection !ModuleName | |
| Decl !Declaration | Never a Section or ScopeDecl |
| Pragmas !PragmaOptions |
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.
class Enum i => HasFresh i where Source #
Minimal complete definition
Instances
class Monad m => MonadFresh i m where Source #
Minimal complete definition
Nothing
Methods
default fresh :: (MonadTrans t, MonadFresh i n, t n ~ m) => m i Source #
Instances
| MonadFresh NameId AbsToCon Source # | |
| HasFresh i => MonadFresh i TCM Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| Monad m => MonadFresh NameId (PureConversionT m) Source # | |
Defined in Agda.TypeChecking.Conversion.Pure Methods fresh :: PureConversionT m NameId Source # | |
| Monad m => MonadFresh ProblemId (PureConversionT m) Source # | |
Defined in Agda.TypeChecking.Conversion.Pure Methods fresh :: PureConversionT m ProblemId Source # | |
| Monad m => MonadFresh Int (PureConversionT m) Source # | |
Defined in Agda.TypeChecking.Conversion.Pure Methods fresh :: PureConversionT m Int Source # | |
| MonadFresh i m => MonadFresh i (ListT m) Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| MonadFresh i m => MonadFresh i (IdentityT m) Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| MonadFresh i m => MonadFresh i (ReaderT r m) Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| MonadFresh i m => MonadFresh i (StateT s m) Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
class FreshName a where Source #
Create a fresh name from a.
Methods
freshName_ :: MonadFresh NameId m => a -> m Name Source #
Instances
| FreshName Range Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadFresh NameId m => Range -> m Name Source # | |
| FreshName String Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadFresh NameId m => String -> m Name Source # | |
| FreshName () Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadFresh NameId m => () -> m Name Source # | |
| FreshName (Range, String) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadFresh NameId m => (Range, String) -> m Name Source # | |
class Monad m => MonadStConcreteNames m where Source #
A monad that has read and write access to the stConcreteNames part of the TCState. Basically, this is a synonym for `MonadState ConcreteNames m` (which cannot be used directly because of the limitations of Haskell's typeclass system).
Minimal complete definition
Methods
runStConcreteNames :: StateT ConcreteNames m a -> m a Source #
useConcreteNames :: m ConcreteNames Source #
modifyConcreteNames :: (ConcreteNames -> ConcreteNames) -> m () Source #
Instances
data ModuleCheckMode Source #
Distinguishes between type-checked and scope-checked interfaces
when stored in the map of VisitedModules.
Constructors
| ModuleScopeChecked | |
| ModuleTypeChecked |
Instances
class LensClosure b a | b -> a where Source #
Methods
lensClosure :: Lens' b (Closure a) Source #
Instances
| LensClosure MetaInfo Range Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| LensClosure MetaVariable Range Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| LensClosure (Closure a) a Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
data WhyCheckModality Source #
Why are we performing a modality check?
Constructors
| ConstructorType | Because --without-K is enabled, so the types of data constructors must be usable at the context's modality. |
| IndexedClause | Because --without-K is enabled, so the result type of clauses must be usable at the context's modality. |
| IndexedClauseArg Name Name | Because --without-K is enabled, so any argument (second name) which mentions a dotted argument (first name) must have a type which is usable at the context's modality. |
| GeneratedClause | Because we double-check the --cubical-compatible clauses. This is an internal error! |
Instances
Information about whether an argument is forced by the type of a function.
Instances
| KillRange IsForced Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| PrettyTCM IsForced Source # | |
Defined in Agda.TypeChecking.Pretty | |
| ChooseFlex IsForced Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: IsForced -> IsForced -> FlexChoice Source # | |
| EmbPrj IsForced Source # | |
| Generic IsForced Source # | |
| Show IsForced Source # | |
| NFData IsForced Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| Eq IsForced Source # | |
| type Rep IsForced Source # | |
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
Parametrized since it is used without MetaId when creating a new meta.
Constructors
| HasType | |
Fields
| |
| IsSort | |
Instances
data DoGeneralize Source #
Constructors
| YesGeneralizeVar | Generalize because it is a generalizable variable. |
| YesGeneralizeMeta | Generalize because it is a metavariable and we're currently checking the type of a generalizable variable (this should get the default modality). |
| NoGeneralize | Don't generalize. |
Instances
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
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
| Show MetaPriority Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> MetaPriority -> ShowS # show :: MetaPriority -> String # showList :: [MetaPriority] -> ShowS # | |
| NFData MetaPriority Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: MetaPriority -> () # | |
| 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 # | |
data MetaInstantiation Source #
Solution status of meta.
Constructors
| InstV Instantiation | Solved by |
| OpenMeta MetaKind | Unsolved (open to solutions). |
| BlockedConst Term | Solved, but solution blocked by unsolved constraints. |
| PostponedTypeCheckingProblem (Closure TypeCheckingProblem) | Meta stands for value of the expression that is still to be type checked. |
Instances
Constructors
| EtaExpand MetaId | |
| CheckConstraint Nat ProblemConstraint |
Instances
| Generic Listener Source # | |
| NFData Listener Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| Eq Listener Source # | |
| Ord Listener Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| type Rep Listener Source # | |
Defined in Agda.TypeChecking.Monad.Base type Rep Listener = D1 ('MetaData "Listener" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "EtaExpand" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaId)) :+: C1 ('MetaCons "CheckConstraint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Nat) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 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 Instantiation Source #
Meta-variable instantiations.
Constructors
| Instantiation | |
Instances
data TypeCheckingProblem Source #
Constructors
| CheckExpr Comparison Expr Type | |
| CheckArgs Comparison ExpandHidden Range [NamedArg Expr] Type Type (ArgsCheckState CheckedTarget -> TCM Term) | |
| CheckProjAppToKnownPrincipalArg Comparison Expr ProjOrigin (List1 QName) Args Type Int Term Type PrincipalArgTypeMetas | |
| CheckLambda Comparison (Arg (List1 (WithHiding Name), Maybe Type)) Expr Type |
|
| DoQuoteTerm Comparison Term Type | Quote the given term and check type against |
Instances
data RemoteMetaVariable Source #
Information about remote meta-variables.
Remote meta-variables are meta-variables originating in other modules. These meta-variables are always instantiated. We do not retain all the information about a local meta-variable when creating an interface:
- The
mvPriorityfield is not needed, because the meta-variable cannot be instantiated. - The
mvFrozenfield is not needed, because there is no point in freezing instantiated meta-variables. - The
mvListenersfield is not needed, because no meta-variable should be listening to this one. - The
mvTwinfield is not needed, because the meta-variable has already been instantiated. - The
mvPermutationis currently removed, but could be retained if it turns out to be useful for something. - The only part of the
mvInfofield that is kept is themiModalityfield. ThemiMetaOccursCheckandmiGeneralizablefields are omitted, because the meta-variable has already been instantiated. TheRange'that is part of themiClosRangefield and themiNameSuggestionfield are omitted because instantiated meta-variables are typically not presented to users. Finally theClosurepart of themiClosRangefield is omitted because it can be large (at least if we ignore potential sharing).
Constructors
| RemoteMetaVariable | |
Fields | |
Instances
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 PrincipalArgTypeMetas Source #
Constructors
| PrincipalArgTypeMetas | |
Fields
| |
Instances
| Generic PrincipalArgTypeMetas Source # | |
Defined in Agda.TypeChecking.Monad.Base Associated Types type Rep PrincipalArgTypeMetas :: Type -> Type # Methods from :: PrincipalArgTypeMetas -> Rep PrincipalArgTypeMetas x # to :: Rep PrincipalArgTypeMetas x -> PrincipalArgTypeMetas # | |
| NFData PrincipalArgTypeMetas Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: PrincipalArgTypeMetas -> () # | |
| type Rep PrincipalArgTypeMetas Source # | |
Defined in Agda.TypeChecking.Monad.Base type Rep PrincipalArgTypeMetas = D1 ('MetaData "PrincipalArgTypeMetas" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "PrincipalArgTypeMetas" 'PrefixI 'True) (S1 ('MetaSel ('Just "patmMetas") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Args) :*: S1 ('MetaSel ('Just "patmRemainder") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) | |
data ExpandHidden Source #
Constructors
| ExpandLast | Add implicit arguments in the end until type is no longer hidden |
| DontExpandLast | Do not append implicit arguments. |
| ReallyDontExpandLast | Makes |
Instances
| Generic ExpandHidden Source # | |
Defined in Agda.TypeChecking.Monad.Base Associated Types type Rep ExpandHidden :: Type -> Type # | |
| NFData ExpandHidden Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: ExpandHidden -> () # | |
| Eq ExpandHidden Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| type Rep ExpandHidden Source # | |
Defined in Agda.TypeChecking.Monad.Base type Rep ExpandHidden = D1 ('MetaData "ExpandHidden" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "ExpandLast" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DontExpandLast" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ReallyDontExpandLast" 'PrefixI 'False) (U1 :: Type -> Type))) | |
data ArgsCheckState a Source #
Constructors
| ACState | |
Fields
| |
Instances
| Show a => Show (ArgsCheckState a) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> ArgsCheckState a -> ShowS # show :: ArgsCheckState a -> String # showList :: [ArgsCheckState a] -> ShowS # | |
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 | |
Fields
| |
Instances
Which clause is an interaction point located in?
Constructors
| IPClause | |
Fields
| |
| IPNoClause | The interaction point is not in the rhs of a clause. |
Instances
type IPBoundary = IPBoundary' Term Source #
data Overapplied Source #
Flag to indicate whether the meta is overapplied in the constraint. A meta is overapplied if it has more arguments than the size of the telescope in its creation environment (as stored in MetaInfo).
Constructors
| Overapplied | |
| NotOverapplied |
Instances
| Generic Overapplied Source # | |
Defined in Agda.TypeChecking.Monad.Base Associated Types type Rep Overapplied :: Type -> Type # | |
| Show Overapplied Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Overapplied -> ShowS # show :: Overapplied -> String # showList :: [Overapplied] -> ShowS # | |
| NFData Overapplied Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: Overapplied -> () # | |
| Eq Overapplied Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| type Rep Overapplied Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
newtype IPBoundary' t Source #
Constructors
| IPBoundary | |
Fields
| |
Instances
type RewriteRuleMap = HashMap QName RewriteRules Source #
data InstanceTable Source #
Records information about the instances in the signature. Does not deal with local instances.
Constructors
| InstanceTable | |
Fields
| |
Instances
type LocalDisplayForm = Open DisplayForm Source #
data DisplayTerm Source #
Constructors
| DWithApp DisplayTerm [DisplayTerm] Elims |
|
| DCon ConHead ConInfo [Arg DisplayTerm] |
|
| DDef QName [Elim' DisplayTerm] |
|
| DDot' Term Elims |
|
| DTerm' Term Elims |
|
Instances
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. |
| PDef QName PElims | Matches |
| PLam ArgInfo (Abs NLPat) | Matches |
| PPi (Dom NLPType) (Abs NLPType) | Matches |
| PSort NLPSort | Matches a sort of the given shape. |
| PBoundVar !Int PElims | Matches |
| PTerm Term | Matches the term modulo β (ideally βη). |
Instances
Constructors
| NLPType | |
Fields
| |
Instances
Constructors
| PUniv Univ NLPat | |
| PInf Univ Integer | |
| PSizeUniv | |
| PLockUniv | |
| PLevelUniv | |
| PIntervalUniv |
Instances
data RewriteRule Source #
Rewrite rules can be added independently from function clauses.
Constructors
| RewriteRule | |
Fields
| |
Instances
Constructors
| AxiomDefn AxiomData | Postulate. |
| DataOrRecSigDefn DataOrRecSigData | Data or record type signature that doesn't yet have a definition. |
| GeneralizableVar | Generalizable variable (introduced in |
| AbstractDefn Defn | Returned by |
| FunctionDefn FunctionData | |
| DatatypeDefn DatatypeData | |
| RecordDefn RecordData | |
| ConstructorDefn ConstructorData | |
| PrimitiveDefn PrimitiveData | Primitive or builtin functions. |
| PrimitiveSortDefn PrimitiveSortData |
Instances
data NumGeneralizableArgs Source #
Constructors
| NoGeneralizableArgs | |
| SomeGeneralizableArgs !Int | When lambda-lifting new args are generalizable if
|
Instances
| KillRange NumGeneralizableArgs Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| EmbPrj NumGeneralizableArgs Source # | |
| Abstract NumGeneralizableArgs Source # | |
Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> NumGeneralizableArgs -> NumGeneralizableArgs Source # | |
| Apply NumGeneralizableArgs Source # | |
Defined in Agda.TypeChecking.Substitute Methods apply :: NumGeneralizableArgs -> Args -> NumGeneralizableArgs Source # applyE :: NumGeneralizableArgs -> Elims -> NumGeneralizableArgs Source # | |
| Show NumGeneralizableArgs Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> NumGeneralizableArgs -> ShowS # show :: NumGeneralizableArgs -> String # showList :: [NumGeneralizableArgs] -> ShowS # | |
| NFData NumGeneralizableArgs Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: NumGeneralizableArgs -> () # | |
data ExtLamInfo Source #
Additional information for extended lambdas.
Constructors
| ExtLamInfo | |
Fields
| |
Instances
data Projection Source #
Additional information for projection Functions.
Constructors
| Projection | |
Fields
| |
Instances
Abstractions to build projection function (dropping parameters).
Constructors
| ProjLams | |
Fields
| |
Instances
| Pretty ProjLams Source # | |
| KillRange ProjLams Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| EmbPrj ProjLams Source # | |
| Abstract ProjLams Source # | |
| Apply ProjLams Source # | |
| Null ProjLams Source # | |
| Generic ProjLams Source # | |
| Show ProjLams Source # | |
| NFData ProjLams Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| type Rep ProjLams Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
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
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? |
| FunFirstOrder | Is this function |
| FunErasure | Was |
| FunAbstract | Is the function abstract? |
| FunProj | Is this function a descendant of a field (typically, a projection)? |
Instances
Constructors
| CompKit | |
Fields
| |
Instances
| NamesIn CompKit Source # | |
Defined in Agda.Syntax.Internal.Names | |
| KillRange CompKit Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods | |
| EmbPrj CompKit Source # | |
| Generic CompKit Source # | |
| Show CompKit Source # | |
| NFData CompKit Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| Eq CompKit Source # | |
| Ord CompKit Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| type Rep CompKit Source # | |
Defined in Agda.TypeChecking.Monad.Base type Rep CompKit = D1 ('MetaData "CompKit" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "CompKit" 'PrefixI 'True) (S1 ('MetaSel ('Just "nameOfHComp") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe QName)) :*: S1 ('MetaSel ('Just "nameOfTransp") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe QName)))) | |
Constructors
| AxiomData | |
Fields
| |
data DataOrRecSigData Source #
Constructors
| DataOrRecSigData | |
Fields
| |
Instances
data FunctionData Source #
Constructors
| FunctionData | |
Fields
| |
Instances
data DatatypeData Source #
Constructors
| DatatypeData | |
Fields
| |
Instances
data RecordData Source #
Constructors
| RecordData | |
Fields
| |
Instances
data ConstructorData Source #
Constructors
| ConstructorData | |
Fields
| |
Instances
data PrimitiveData Source #
Constructors
| PrimitiveData | |
Fields
| |
Instances
data PrimitiveSortData Source #
Constructors
| PrimitiveSortData | |
Fields | |
Instances
data ProjectionLikenessMissing Source #
Indicates the reason behind a function having not been marked projection-like.
Constructors
| MaybeProjection | Projection-likeness analysis has not run on this function yet. It may do so in the future. |
| NeverProjection | The user has requested that this function be not be marked projection-like. The analysis may already have run on this function, but the results have been discarded, and it will not be run again. |
Instances
type FunctionInverse = FunctionInverse' Clause Source #
data BuiltinSort Source #
Constructors
| SortUniv Univ | |
| SortOmega Univ | |
| SortIntervalUniv | |
| SortLevelUniv |
Instances
data FunctionInverse' c Source #
Constructors
| NotInjective | |
| Inverse (InversionMap c) |
Instances
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
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 Methods prettyTCM :: MonadPretty m => MaybeReduced a -> m Doc Source # | |
type MaybeReducedArgs = [MaybeReduced (Arg Term)] Source #
type MaybeReducedElims = [MaybeReduced Elim] 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 |
| TypeLevelReductions | Allow |
| UnconfirmedReductions | Functions whose termination has not (yet) been confirmed. |
| NonTerminatingReductions | Functions that have failed termination checking. |
Instances
data ReduceDefs Source #
Constructors
| OnlyReduceDefs (Set QName) | |
| DontReduceDefs (Set QName) |
Instances
| Generic ReduceDefs Source # | |
Defined in Agda.TypeChecking.Monad.Base Associated Types type Rep ReduceDefs :: Type -> Type # | |
| NFData ReduceDefs Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: ReduceDefs -> () # | |
| type Rep ReduceDefs Source # | |
Defined in Agda.TypeChecking.Monad.Base type Rep ReduceDefs = D1 ('MetaData "ReduceDefs" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "OnlyReduceDefs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set QName))) :+: C1 ('MetaCons "DontReduceDefs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set QName)))) | |
type InversionMap c = Map TermHead [c] Source #
Instances
data BuiltinDescriptor Source #
Constructors
| BuiltinData (TCM Type) [BuiltinId] | |
| BuiltinDataCons (TCM Type) | |
| BuiltinPrim PrimitiveId (Term -> TCM ()) | |
| BuiltinSort BuiltinSort | |
| 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 LetBindings = Map Name (Open LetBinding) Source #
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
| Generic AbstractMode Source # | |
Defined in Agda.TypeChecking.Monad.Base Associated Types type Rep AbstractMode :: Type -> Type # | |
| Show AbstractMode Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> AbstractMode -> ShowS # show :: AbstractMode -> String # showList :: [AbstractMode] -> ShowS # | |
| NFData AbstractMode Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: AbstractMode -> () # | |
| Eq AbstractMode Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| type Rep AbstractMode Source # | |
Defined in Agda.TypeChecking.Monad.Base type Rep AbstractMode = D1 ('MetaData "AbstractMode" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "AbstractMode" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ConcreteMode" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IgnoreAbstractMode" 'PrefixI 'False) (U1 :: Type -> Type))) | |
data UnquoteFlags Source #
Constructors
| UnquoteFlags | |
Fields | |
Instances
| Generic UnquoteFlags Source # | |
Defined in Agda.TypeChecking.Monad.Base Associated Types type Rep UnquoteFlags :: Type -> Type # | |
| NFData UnquoteFlags Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: UnquoteFlags -> () # | |
| type Rep UnquoteFlags Source # | |
Defined in Agda.TypeChecking.Monad.Base type Rep UnquoteFlags = D1 ('MetaData "UnquoteFlags" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "UnquoteFlags" 'PrefixI 'True) (S1 ('MetaSel ('Just "_unquoteNormalise") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) | |
data CandidateKind Source #
Constructors
| LocalCandidate | |
| GlobalCandidate QName |
Instances
data TerminationError Source #
Information about a mutual block which did not pass the termination checker.
Constructors
| TerminationError | |
Fields
| |
Instances
data IllegalRewriteRuleReason Source #
Constructors
Instances
Information about a call.
Constructors
| CallInfo | |
Fields
| |
Instances
| Pretty CallInfo Source # | We only |
| HasRange CallInfo Source # | |
| PrettyTCM CallInfo Source # | |
Defined in Agda.TypeChecking.Pretty.Call | |
| Generic CallInfo Source # | |
| Show CallInfo Source # | |
| NFData CallInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| type Rep CallInfo Source # | |
Defined in Agda.TypeChecking.Monad.Base type Rep CallInfo = D1 ('MetaData "CallInfo" "Agda.TypeChecking.Monad.Base" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "CallInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "callInfoTarget") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "callInfoCall") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Closure Term)))) | |
data ErasedDatatypeReason Source #
The reason for an ErasedDatatype error.
Constructors
| SeveralConstructors | There are several constructors. |
| NoErasedMatches | The flag |
| NoK | The K rule is not activated. |
Instances
data SplitError Source #
Error when splitting a pattern variable into possible constructor patterns.
Constructors
| NotADatatype (Closure Type) | Neither data type nor record. |
| BlockedType Blocker (Closure Type) | Type could not be sufficiently reduced. |
| ErasedDatatype ErasedDatatypeReason (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
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 |
| UnifyUnusableModality Telescope Type Int Term Modality | Can't solve equation because solution modality is less "usable" |
Instances
data NegativeUnification Source #
Constructors
| UnifyConflict Telescope Term Term | |
| UnifyCycle Telescope Int Term |
Instances
data UnquoteError Source #
Constructors
Instances
data IncorrectTypeForRewriteRelationReason Source #
Constructors
| ShouldAcceptAtLeastTwoArguments | |
| FinalTwoArgumentsNotVisible | |
| TypeDoesNotEndInSort Type Telescope |
Instances
data InvalidFileNameReason Source #
Extra information for InvalidFileName error.
Instances
data InductionAndEta Source #
Constructors
| InductionAndEta | |
Fields | |
Instances
Environment of the reduce monad.
Constructors
| ReduceEnv | |
Instances
pattern Function :: [Clause] -> Maybe CompiledClauses -> Maybe SplitTree -> Maybe Compiled -> [Clause] -> FunctionInverse -> Maybe [QName] -> Either ProjectionLikenessMissing Projection -> SmallSet FunctionFlag -> Maybe Bool -> Maybe ExtLamInfo -> Maybe QName -> Maybe QName -> IsOpaque -> Defn Source #
pattern Constructor :: Int -> Int -> ConHead -> QName -> IsAbstract -> CompKit -> Maybe [QName] -> [IsForced] -> Maybe [Bool] -> Bool -> Bool -> Defn Source #
pattern Datatype :: Nat -> Nat -> Maybe Clause -> [QName] -> Sort -> Maybe [QName] -> IsAbstract -> [QName] -> Maybe QName -> Maybe QName -> Defn Source #
pattern Primitive :: IsAbstract -> PrimitiveId -> [Clause] -> FunctionInverse -> Maybe CompiledClauses -> IsOpaque -> Defn Source #
pattern Record :: Nat -> Maybe Clause -> ConHead -> Bool -> [Dom QName] -> Telescope -> Maybe [QName] -> EtaEquality -> PatternOrCopattern -> Maybe Induction -> Maybe Bool -> IsAbstract -> CompKit -> Defn Source #
pattern DDot :: Term -> DisplayTerm Source #
pattern DTerm :: Term -> DisplayTerm Source #
pattern DataOrRecSig :: Int -> Defn Source #
pattern PrimitiveSort :: BuiltinSort -> Sort -> Defn Source #
pattern SortProp :: BuiltinSort Source #
pattern SortSet :: BuiltinSort Source #
pattern SortStrictSet :: BuiltinSort Source #
pattern SortPropOmega :: BuiltinSort Source #
pattern SortSetOmega :: BuiltinSort Source #
pattern SortStrictSetOmega :: BuiltinSort Source #
typeError :: (HasCallStack, MonadTCError m) => TypeError -> m a Source #
internalError :: (HasCallStack, MonadTCM tcm) => String -> tcm a Source #
runReduceM :: ReduceM a -> TCM a Source #
defaultInteractionOutputCallback :: InteractionOutputCallback Source #
The default InteractionOutputCallback function prints certain
things to stdout (other things generate internal errors).
defAbstract :: Definition -> IsAbstract Source #
genericError :: (HasCallStack, MonadTCError m) => String -> m a Source #
defOpaque :: Definition -> IsOpaque Source #
initPersistentState :: PersistentTCState Source #
Empty persistent state.
initialMetaId :: MetaId Source #
An initial MetaId.
initPreScopeState :: PreScopeState Source #
Empty state of type checker.
getUserWarnings :: ReadTCState m => m (Map QName Text) Source #
getPartialDefs :: ReadTCState m => m (Set QName) Source #
stBackends :: Lens' TCState [Backend_boot TCM] Source #
stCurrentModule :: Lens' TCState (Maybe (ModuleName, TopLevelModuleName)) Source #
Note that the lens is "strict".
unionBuiltin :: Builtin a -> Builtin a -> Builtin a Source #
Union two Builtins. Only defined for BuiltinRewriteRelations.
freshNoName :: MonadFresh NameId m => Range -> m Name Source #
freshNoName_ :: MonadFresh NameId m => m Name Source #
freshRecordName :: MonadFresh NameId m => m Name Source #
stateTCLensM :: MonadTCState m => Lens' TCState a -> (a -> m (r, a)) -> m r Source #
Modify a part of the state monadically, and return some result.
iFullHash :: Interface -> Hash Source #
Combines the source hash and the (full) hashes of the imported modules.
intSignature :: Lens' Interface Signature Source #
A lens for the iSignature field of the Interface type.
buildClosure :: (MonadTCEnv m, ReadTCState m) => a -> m (Closure a) 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
suffixNameSuggestion :: MetaNameSuggestion -> ArgName -> MetaNameSuggestion Source #
Append an ArgName to a MetaNameSuggestion, for computing the
name suggestions of eta-expansion metas. If the MetaNameSuggestion
is empty or an underscore, the field name is taken as the suggestion.
getMetaInfo :: MetaVariable -> Closure Range Source #
getMetaScope :: MetaVariable -> ScopeInfo Source #
getMetaEnv :: MetaVariable -> TCEnv Source #
getMetaSig :: MetaVariable -> Signature Source #
aModeToDef :: AbstractMode -> Maybe IsAbstract Source #
aDefToMode :: IsAbstract -> AbstractMode Source #
defaultDisplayForm :: QName -> [LocalDisplayForm] Source #
By default, we have no display form.
defaultDefn :: ArgInfo -> QName -> Type -> Language -> Defn -> Definition Source #
Create a definition with sensible defaults.
modifySystem :: (System -> System) -> ExtLamInfo -> ExtLamInfo 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.
setEtaEquality :: EtaEquality -> HasEta -> EtaEquality Source #
Make sure we do not overwrite a user specification.
defaultAxiom :: Defn Source #
axiomConstTransp :: Defn -> Bool Source #
datarecPars :: Defn -> Int Source #
funClauses :: Defn -> [Clause] Source #
funCompiled :: Defn -> Maybe CompiledClauses Source #
funCovering :: Defn -> [Clause] Source #
funInv :: Defn -> FunctionInverse Source #
dataAbstr :: Defn -> IsAbstract Source #
dataPathCons :: Defn -> [QName] Source #
recConHead :: Defn -> ConHead Source #
recNamedCon :: Defn -> Bool Source #
recEtaEquality' :: Defn -> EtaEquality Source #
recAbstr :: Defn -> IsAbstract Source #
conAbstr :: Defn -> IsAbstract Source #
conErasure :: Defn -> Bool Source #
primAbstr :: Defn -> IsAbstract Source #
primName :: Defn -> PrimitiveId Source #
primClauses :: Defn -> [Clause] Source #
primInv :: Defn -> FunctionInverse Source #
primCompiled :: Defn -> Maybe CompiledClauses Source #
primOpaque :: Defn -> IsOpaque Source #
primSortName :: Defn -> BuiltinSort Source #
primSortSort :: Defn -> Sort Source #
recRecursive :: Defn -> Bool Source #
Is the record type recursive?
recRecursive_ :: RecordData -> Bool Source #
recEtaEquality :: Defn -> HasEta Source #
_recEtaEquality :: RecordData -> HasEta Source #
emptyFunctionData :: HasOptions m => m FunctionData Source #
A template for creating Function definitions, with sensible
defaults.
emptyFunction :: HasOptions m => m Defn Source #
emptyFunction_ :: Bool -> Defn Source #
funFlag_ :: FunctionFlag -> Lens' FunctionData Bool Source #
funFirstOrder :: Lens' Defn Bool Source #
Toggle the FunFirstOrder flag.
funErasure :: Lens' Defn Bool Source #
Toggle the FunErasure flag.
funAbstract :: Lens' Defn Bool Source #
Toggle the FunAbstract flag.
funAbstr :: Lens' Defn IsAbstract Source #
Toggle the FunAbstract flag.
funAbstract_ :: Lens' FunctionData Bool Source #
Toggle the FunAbstract flag.
funAbstr_ :: Lens' FunctionData IsAbstract Source #
Toggle the FunAbstract flag.
isEmptyFunction :: Defn -> Bool Source #
Checking whether we are dealing with a function yet to be defined.
isExtendedLambda :: Defn -> Bool Source #
isWithFunction :: Defn -> Bool Source #
isCopatternLHS :: [Clause] -> Bool Source #
defIsRecord :: Defn -> Bool Source #
defIsDataOrRecord :: Defn -> Bool Source #
defConstructors :: Defn -> [QName] Source #
redBind :: ReduceM (Reduced a a') -> (a -> b) -> (a' -> ReduceM (Reduced b b')) -> ReduceM (Reduced b b') Source #
Conceptually: redBind m f k = either (return . Left . f) k =<< m
notReduced :: a -> MaybeReduced a Source #
allReductions :: AllowedReductions Source #
Not quite all reductions (skip non-terminating reductions)
locallyReduceDefs :: MonadTCEnv m => ReduceDefs -> m a -> m a Source #
locallyTC :: MonadTCEnv m => Lens' TCEnv a -> (a -> a) -> m b -> m b Source #
Modify the lens-indicated part of the TCEnv in a subcomputation.
locallyReduceAllDefs :: MonadTCEnv m => m a -> m a Source #
shouldReduceDef :: MonadTCEnv m => QName -> m Bool Source #
asksTC :: MonadTCEnv m => (TCEnv -> a) -> m a Source #
toReduceDefs :: (Bool, [QName]) -> ReduceDefs Source #
fromReduceDefs :: ReduceDefs -> (Bool, [QName]) Source #
locallyReconstructed :: MonadTCEnv m => m a -> m a Source #
isReconstructed :: MonadTCEnv m => m Bool Source #
primFun :: QName -> Arity -> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun Source #
defClauses :: Definition -> [Clause] Source #
defParameters :: Definition -> Maybe Nat Source #
defCompilerPragmas :: BackendName -> Definition -> [CompilerPragma] Source #
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?
defForced :: Definition -> [IsForced] Source #
itableCounts :: Lens' InstanceTable (Map QName Int) Source #
ifTopLevelAndHighlightingLevelIsOr :: MonadTCEnv tcm => HighlightingLevel -> Bool -> tcm () -> tcm () Source #
ifTopLevelAndHighlightingLevelIs l b m runs m when we're
type-checking the top-level module (or before we've started doing
this) and either the highlighting level is at least l or b is
True.
ifTopLevelAndHighlightingLevelIs :: MonadTCEnv tcm => HighlightingLevel -> tcm () -> tcm () Source #
ifTopLevelAndHighlightingLevelIs l m runs m when we're
type-checking the top-level module (or before we've started doing
this) and the highlighting level is at least l.
eAnonymousModules :: Lens' TCEnv [(ModuleName, Nat)] Source #
eTerminationCheck :: Lens' TCEnv (TerminationCheck ()) Source #
eQuantity :: Lens' TCEnv Quantity Source #
Note that this lens does not satisfy all lens laws: If hard
compile-time mode is enabled, then quantities other than zero are
replaced by __IMPOSSIBLE__.
isExpandLast :: ExpandHidden -> Bool Source #
toExpandLast :: Bool -> ExpandHidden Source #
currentModality :: MonadTCEnv m => m Modality Source #
The current modality.
Note that the returned cohesion component is always unitCohesion.
onLetBindingType :: (Dom Type -> Dom Type) -> LetBinding -> LetBinding Source #
isDontExpandLast :: ExpandHidden -> Bool Source #
warningName :: Warning -> WarningName Source #
isSourceCodeWarning :: WarningName -> Bool Source #
Should warnings of that type be serialized?
Only when changes in the source code can silence or influence the warning.
tcWarningOrigin :: TCWarning -> SrcFile Source #
sizedTypesOption :: HasOptions m => m Bool Source #
guardednessOption :: HasOptions m => m Bool Source #
withoutKOption :: HasOptions m => m Bool Source #
cubicalOption :: HasOptions m => m (Maybe Cubical) Source #
cubicalCompatibleOption :: HasOptions m => m Bool Source #
enableCaching :: HasOptions m => m Bool Source #
fmapReduce :: (a -> b) -> ReduceM a -> ReduceM b Source #
runReduceF :: (a -> ReduceM b) -> TCM (a -> b) Source #
getsTC :: ReadTCState 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.
setTCLens :: MonadTCState m => Lens' TCState a -> a -> m () infix 4 Source #
Overwrite the part of the TCState focused on by the lens.
setTCLens' :: MonadTCState m => Lens' TCState a -> a -> m () Source #
Overwrite the part of the TCState focused on by the lens
(strictly).
modifyTCLens :: MonadTCState m => Lens' TCState a -> (a -> a) -> m () Source #
Modify the part of the TCState focused on by the lens.
modifyTCLens' :: MonadTCState m => Lens' TCState a -> (a -> a) -> m () Source #
Modify the part of the TCState focused on by the lens
(strictly).
modifyTCLensM :: MonadTCState m => Lens' TCState a -> (a -> m a) -> m () Source #
Modify a part of the state monadically.
stateTCLens :: MonadTCState m => Lens' TCState a -> (a -> (r, a)) -> m r Source #
Modify the part of the TCState focused on by the lens, and return some result.
returnTCMT :: Applicative m => a -> TCMT m a Source #
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.
typeError' :: MonadTCError m => CallStack -> TypeError -> m a Source #
locatedTypeError :: MonadTCError m => (a -> TypeError) -> HasCallStack => a -> m b Source #
Utility function for 1-arg constructed type errors.
Note that the HasCallStack constraint is on the *resulting* function.
genericDocError :: (HasCallStack, MonadTCError m) => Doc -> m a Source #
typeError'_ :: (MonadTCEnv m, ReadTCState m) => CallStack -> TypeError -> m TCErr Source #
typeError_ :: (HasCallStack, MonadTCEnv m, ReadTCState m) => TypeError -> m TCErr 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, except that it might raise IOExceptions) 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.
patternInTeleName :: String Source #
Base name for patterns in telescopes
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
class (Functor m, Applicative m, Monad m) => HasOptions m where Source #
Minimal complete definition
Nothing
Methods
pragmaOptions :: m PragmaOptions Source #
Returns the pragma options which are currently in effect.
default pragmaOptions :: (HasOptions n, MonadTrans t, m ~ t n) => m PragmaOptions Source #
commandLineOptions :: m CommandLineOptions Source #
Returns the command line options which are currently in effect.
default commandLineOptions :: (HasOptions n, MonadTrans t, m ~ t n) => m CommandLineOptions Source #
Instances
data RecordFieldWarning Source #
Instances
Orphan instances
| NFData RecordFieldWarning Source # | |
Methods rnf :: RecordFieldWarning -> () # | |
| NFData (BiMap RawTopLevelModuleName ModuleNameHash) Source # | |
Methods rnf :: BiMap RawTopLevelModuleName ModuleNameHash -> () # | |