Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Monad.Base

Contents

Type checking state
st-prefixed lenses
Fresh things
Open things
Judgements
Highlighting levels
Type checking environment
e-prefixed lenses
Type checking warnings (aka non-fatal errors)
Type checking errors
Accessing options
The reduce monad
Type checking monad transformer
KillRange instances

Synopsis

data TCState = TCSt {
- stPreScopeState :: !PreScopeState
- stPostScopeState :: !PostScopeState
- stPersistentState :: !PersistentTCState
}
class Monad m => ReadTCState m where
data PreScopeState = PreScopeState {
- stPreTokens :: !CompressedFile
- stPreImports :: !Signature
- stPreImportedModules :: !(Set ModuleName)
- stPreModuleToSource :: !ModuleToSource
- stPreVisitedModules :: !VisitedModules
- stPreScope :: !ScopeInfo
- stPrePatternSyns :: !PatternSynDefns
- stPrePatternSynImports :: !PatternSynDefns
- stPrePragmaOptions :: !PragmaOptions
- stPreImportedBuiltins :: !(BuiltinThings PrimFun)
- stPreImportedDisplayForms :: !DisplayForms
- stPreImportedInstanceDefs :: !InstanceTable
- stPreForeignCode :: !(Map BackendName [ForeignCode])
- stPreFreshInteractionId :: !InteractionId
- stPreUserWarnings :: !(Map QName String)
}
type DisambiguatedNames = IntMap QName
data PostScopeState = PostScopeState {
- stPostSyntaxInfo :: !CompressedFile
- stPostDisambiguatedNames :: !DisambiguatedNames
- stPostMetaStore :: !MetaStore
- stPostInteractionPoints :: !InteractionPoints
- stPostAwakeConstraints :: !Constraints
- stPostSleepingConstraints :: !Constraints
- stPostDirty :: !Bool
- stPostOccursCheckDefs :: !(Set QName)
- stPostSignature :: !Signature
- stPostModuleCheckpoints :: !(Map ModuleName CheckpointId)
- stPostImportsDisplayForms :: !DisplayForms
- stPostCurrentModule :: !(Maybe ModuleName)
- stPostInstanceDefs :: !TempInstanceTable
- stPostStatistics :: !Statistics
- stPostTCWarnings :: ![TCWarning]
- stPostMutualBlocks :: !(Map MutualId MutualBlock)
- stPostLocalBuiltins :: !(BuiltinThings PrimFun)
- stPostFreshMetaId :: !MetaId
- stPostFreshMutualId :: !MutualId
- stPostFreshProblemId :: !ProblemId
- stPostFreshCheckpointId :: !CheckpointId
- stPostFreshInt :: !Int
- stPostFreshNameId :: !NameId
- stPostAreWeCaching :: !Bool
}
data MutualBlock = MutualBlock {
- mutualInfo :: MutualInfo
- mutualNames :: Set QName
}
data PersistentTCState = PersistentTCSt {
- stDecodedModules :: DecodedModules
- stPersistentOptions :: CommandLineOptions
- stInteractionOutputCallback :: InteractionOutputCallback
- stBenchmark :: !Benchmark
- stAccumStatistics :: !Statistics
- stLoadedFileCache :: !(Maybe LoadedFileCache)
- stPersistBackends :: [Backend]
}
data LoadedFileCache = LoadedFileCache {
- lfcCached :: !CachedTypeCheckLog
- lfcCurrent :: !CurrentTypeCheckLog
}
type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)]
type CurrentTypeCheckLog = [(TypeCheckAction, PostScopeState)]
data TypeCheckAction
- = EnterSection !ModuleInfo !ModuleName ![TypedBindings]
- | LeaveSection !ModuleName
- | Decl !Declaration
- | Pragmas !PragmaOptions
initPersistentState :: PersistentTCState
initPreScopeState :: PreScopeState
initPostScopeState :: PostScopeState
initState :: TCState
stTokens :: Lens' CompressedFile TCState
stImports :: Lens' Signature TCState
stImportedModules :: Lens' (Set ModuleName) TCState
stModuleToSource :: Lens' ModuleToSource TCState
stVisitedModules :: Lens' VisitedModules TCState
stScope :: Lens' ScopeInfo TCState
stPatternSyns :: Lens' PatternSynDefns TCState
stPatternSynImports :: Lens' PatternSynDefns TCState
stPragmaOptions :: Lens' PragmaOptions TCState
stImportedBuiltins :: Lens' (BuiltinThings PrimFun) TCState
stForeignCode :: Lens' (Map BackendName [ForeignCode]) TCState
stFreshInteractionId :: Lens' InteractionId TCState
stUserWarnings :: Lens' (Map QName String) TCState
stBackends :: Lens' [Backend] TCState
stFreshNameId :: Lens' NameId TCState
stSyntaxInfo :: Lens' CompressedFile TCState
stDisambiguatedNames :: Lens' DisambiguatedNames TCState
stMetaStore :: Lens' MetaStore TCState
stInteractionPoints :: Lens' InteractionPoints TCState
stAwakeConstraints :: Lens' Constraints TCState
stSleepingConstraints :: Lens' Constraints TCState
stDirty :: Lens' Bool TCState
stOccursCheckDefs :: Lens' (Set QName) TCState
stSignature :: Lens' Signature TCState
stModuleCheckpoints :: Lens' (Map ModuleName CheckpointId) TCState
stImportsDisplayForms :: Lens' DisplayForms TCState
stImportedDisplayForms :: Lens' DisplayForms TCState
stCurrentModule :: Lens' (Maybe ModuleName) TCState
stImportedInstanceDefs :: Lens' InstanceTable TCState
stInstanceDefs :: Lens' TempInstanceTable TCState
stStatistics :: Lens' Statistics TCState
stTCWarnings :: Lens' [TCWarning] TCState
stMutualBlocks :: Lens' (Map MutualId MutualBlock) TCState
stLocalBuiltins :: Lens' (BuiltinThings PrimFun) TCState
stFreshMetaId :: Lens' MetaId TCState
stFreshMutualId :: Lens' MutualId TCState
stFreshProblemId :: Lens' ProblemId TCState
stFreshCheckpointId :: Lens' CheckpointId TCState
stFreshInt :: Lens' Int TCState
stAreWeCaching :: Lens' Bool TCState
stBuiltinThings :: TCState -> BuiltinThings PrimFun
class Enum i => HasFresh i where
nextFresh :: HasFresh i => TCState -> (i, TCState)
fresh :: (HasFresh i, MonadState TCState m) => m i
newtype ProblemId = ProblemId Nat
newtype CheckpointId = CheckpointId Int
freshName :: MonadState TCState m => Range -> String -> m Name
freshNoName :: MonadState TCState m => Range -> m Name
freshNoName_ :: MonadState TCState m => m Name
class FreshName a where
type ModuleToSource = Map TopLevelModuleName AbsolutePath
type SourceToModule = Map AbsolutePath TopLevelModuleName
sourceToModule :: TCM SourceToModule
lookupModuleFromSource :: AbsolutePath -> TCM (Maybe TopLevelModuleName)
data ModuleInfo = ModuleInfo {
- miInterface :: Interface
- miWarnings :: Bool
}
type VisitedModules = Map TopLevelModuleName ModuleInfo
type DecodedModules = Map TopLevelModuleName Interface
data ForeignCode = ForeignCode Range String
data Interface = Interface {
- iSourceHash :: Hash
- iImportedModules :: [(ModuleName, Hash)]
- iModuleName :: ModuleName
- iScope :: Map ModuleName Scope
- iInsideScope :: ScopeInfo
- iSignature :: Signature
- iDisplayForms :: DisplayForms
- iUserWarnings :: Map QName String
- iBuiltin :: BuiltinThings (String, QName)
- iForeignCode :: Map BackendName [ForeignCode]
- iHighlighting :: HighlightingInfo
- iPragmaOptions :: [OptionsPragma]
- iPatternSyns :: PatternSynDefns
- iWarnings :: [TCWarning]
}
iFullHash :: Interface -> Hash
data Closure a = Closure {
- clSignature :: Signature
- clEnv :: TCEnv
- clScope :: ScopeInfo
- clModuleCheckpoints :: Map ModuleName CheckpointId
- clValue :: a
}
buildClosure :: a -> TCM (Closure a)
type Constraints = [ProblemConstraint]
data ProblemConstraint = PConstr {
- constraintProblems :: Set ProblemId
- theConstraint :: Closure Constraint
}
data Constraint
- = ValueCmp Comparison Type Term Term
- | ElimCmp [Polarity] [IsForced] Type Term [Elim] [Elim]
- | TypeCmp Comparison Type Type
- | TelCmp Type Type Comparison Telescope Telescope
- | SortCmp Comparison Sort Sort
- | LevelCmp Comparison Level Level
- | HasBiggerSort Sort
- | HasPTSRule Sort (Abs Sort)
- | UnBlock MetaId
- | Guarded Constraint ProblemId
- | IsEmpty Range Type
- | CheckSizeLtSat Term
- | FindInScope MetaId (Maybe MetaId) (Maybe [Candidate])
- | CheckFunDef Delayed DefInfo QName [Clause]
data Comparison
- = CmpEq
- | CmpLeq
data CompareDirection
- = DirEq
- | DirLeq
- | DirGeq
fromCmp :: Comparison -> CompareDirection
flipCmp :: CompareDirection -> CompareDirection
dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
data Open a = OpenThing {
- openThingCheckpoint :: CheckpointId
- openThing :: a
}
data Judgement a
- = HasType {
  - jMetaId :: a
  - jMetaType :: Type
  }
- | IsSort {
  - jMetaId :: a
  - jMetaType :: Type
  }
data MetaVariable = MetaVar {
- mvInfo :: MetaInfo
- mvPriority :: MetaPriority
- mvPermutation :: Permutation
- mvJudgement :: Judgement MetaId
- mvInstantiation :: MetaInstantiation
- mvListeners :: Set Listener
- mvFrozen :: Frozen
}
data Listener
- = EtaExpand MetaId
- | CheckConstraint Nat ProblemConstraint
data Frozen
- = Frozen
- | Instantiable
data MetaInstantiation
- = InstV [Arg String] Term
- | Open
- | OpenIFS
- | BlockedConst Term
- | PostponedTypeCheckingProblem (Closure TypeCheckingProblem) (TCM Bool)
data CheckedTarget
- = CheckedTarget (Maybe ProblemId)
- | NotCheckedTarget
data TypeCheckingProblem
- = CheckExpr Expr Type
- | CheckArgs ExpandHidden Range [NamedArg Expr] Type Type (Elims -> Type -> CheckedTarget -> TCM Term)
- | CheckLambda (Arg ([WithHiding Name], Maybe Type)) Expr Type
- | UnquoteTactic Term Term Type
newtype MetaPriority = MetaPriority Int
data RunMetaOccursCheck
- = RunMetaOccursCheck
- | DontRunMetaOccursCheck
data MetaInfo = MetaInfo {
- miClosRange :: Closure Range
- miMetaOccursCheck :: RunMetaOccursCheck
- miNameSuggestion :: MetaNameSuggestion
}
type MetaNameSuggestion = String
data NamedMeta = NamedMeta {
- nmSuggestion :: MetaNameSuggestion
- nmid :: MetaId
}
type MetaStore = Map MetaId MetaVariable
normalMetaPriority :: MetaPriority
lowMetaPriority :: MetaPriority
highMetaPriority :: MetaPriority
getMetaInfo :: MetaVariable -> Closure Range
getMetaScope :: MetaVariable -> ScopeInfo
getMetaEnv :: MetaVariable -> TCEnv
getMetaSig :: MetaVariable -> Signature
getMetaRelevance :: MetaVariable -> Relevance
data InteractionPoint = InteractionPoint {
- ipRange :: Range
- ipMeta :: Maybe MetaId
- ipSolved :: Bool
- ipClause :: IPClause
}
type InteractionPoints = Map InteractionId InteractionPoint
data IPClause
- = IPClause {
  - ipcQName :: QName
  - ipcClauseNo :: Int
  - ipcClause :: RHS
  }
- | IPNoClause
data Signature = Sig {
- _sigSections :: Sections
- _sigDefinitions :: Definitions
- _sigRewriteRules :: RewriteRuleMap
}
sigSections :: Lens' Sections Signature
sigDefinitions :: Lens' Definitions Signature
sigRewriteRules :: Lens' RewriteRuleMap Signature
type Sections = Map ModuleName Section
type Definitions = HashMap QName Definition
type RewriteRuleMap = HashMap QName RewriteRules
type DisplayForms = HashMap QName [LocalDisplayForm]
newtype Section = Section {
- _secTelescope :: Telescope
}
secTelescope :: Lens' Telescope Section
emptySignature :: Signature
data DisplayForm = Display {
- dfFreeVars :: Nat
- dfPats :: Elims
- dfRHS :: DisplayTerm
}
type LocalDisplayForm = Open DisplayForm
data DisplayTerm
- = DWithApp DisplayTerm [DisplayTerm] Elims
- | DCon ConHead ConInfo [Arg DisplayTerm]
- | DDef QName [Elim' DisplayTerm]
- | DDot Term
- | DTerm Term
defaultDisplayForm :: QName -> [LocalDisplayForm]
defRelevance :: Definition -> Relevance
data NLPat
- = PVar !Int [Arg Int]
- | PWild
- | PDef QName PElims
- | PLam ArgInfo (Abs NLPat)
- | PPi (Dom NLPType) (Abs NLPType)
- | PBoundVar !Int PElims
- | PTerm Term
type PElims = [Elim' NLPat]
data NLPType = NLPType {
- nlpTypeLevel :: NLPat
- nlpTypeUnEl :: NLPat
}
type RewriteRules = [RewriteRule]
data RewriteRule = RewriteRule {
- rewName :: QName
- rewContext :: Telescope
- rewHead :: QName
- rewPats :: PElims
- rewRHS :: Term
- rewType :: Type
}
data Definition = Defn {
- defArgInfo :: ArgInfo
- defName :: QName
- defType :: Type
- defPolarity :: [Polarity]
- defArgOccurrences :: [Occurrence]
- defDisplay :: [LocalDisplayForm]
- defMutual :: MutualId
- defCompiledRep :: CompiledRepresentation
- defInstance :: Maybe QName
- defCopy :: Bool
- defMatchable :: Bool
- defInjective :: Bool
- theDef :: Defn
}
theDefLens :: Lens' Defn Definition
defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition
data Polarity
- = Covariant
- | Contravariant
- | Invariant
- | Nonvariant
data IsForced
- = Forced
- | NotForced
data CompilerPragma = CompilerPragma Range String
type BackendName = String
jsBackendName :: BackendName
ghcBackendName :: BackendName
uhcBackendName :: BackendName
type CompiledRepresentation = Map BackendName [CompilerPragma]
noCompiledRep :: CompiledRepresentation
data ExtLamInfo = ExtLamInfo {
- extLamModule :: ModuleName
}
data Projection = Projection {
- projProper :: Maybe QName
- projOrig :: QName
- projFromType :: Arg QName
- projIndex :: Int
- projLams :: ProjLams
}
newtype ProjLams = ProjLams {
- getProjLams :: [Arg ArgName]
}
projDropPars :: Projection -> ProjOrigin -> Term
projArgInfo :: Projection -> ArgInfo
data EtaEquality
- = Specified {
  - theEtaEquality :: !HasEta
  }
- | Inferred {
  - theEtaEquality :: !HasEta
  }
setEtaEquality :: EtaEquality -> HasEta -> EtaEquality
data FunctionFlag
- = FunStatic
- | FunInline
- | FunMacro
data Defn
- = Axiom
- | AbstractDefn Defn
- | Function {
  - funClauses :: [Clause]
  - funCompiled :: Maybe CompiledClauses
  - funTreeless :: Maybe Compiled
  - funInv :: FunctionInverse
  - funMutual :: Maybe [QName]
  - funAbstr :: IsAbstract
  - funDelayed :: Delayed
  - funProjection :: Maybe Projection
  - funFlags :: Set FunctionFlag
  - funTerminates :: Maybe Bool
  - funExtLam :: Maybe ExtLamInfo
  - funWith :: Maybe QName
  - funCopatternLHS :: Bool
  }
- | Datatype {
  - dataPars :: Nat
  - dataIxs :: Nat
  - dataInduction :: Induction
  - dataClause :: Maybe Clause
  - dataCons :: [QName]
  - dataSort :: Sort
  - dataMutual :: Maybe [QName]
  - dataAbstr :: IsAbstract
  }
- | Record {
  - recPars :: Nat
  - recClause :: Maybe Clause
  - recConHead :: ConHead
  - recNamedCon :: Bool
  - recFields :: [Arg QName]
  - recTel :: Telescope
  - recMutual :: Maybe [QName]
  - recEtaEquality' :: EtaEquality
  - recInduction :: Maybe Induction
  - recAbstr :: IsAbstract
  }
- | Constructor {
  - conPars :: Int
  - conArity :: Int
  - conSrcCon :: ConHead
  - conData :: QName
  - conAbstr :: IsAbstract
  - conInd :: Induction
  - conForced :: [IsForced]
  - conErased :: [Bool]
  }
- | Primitive {
  - primAbstr :: IsAbstract
  - primName :: String
  - primClauses :: [Clause]
  - primInv :: FunctionInverse
  - primCompiled :: Maybe CompiledClauses
  }
recRecursive :: Defn -> Bool
recEtaEquality :: Defn -> HasEta
emptyFunction :: Defn
funFlag :: FunctionFlag -> Lens' Bool Defn
funStatic :: Lens' Bool Defn
funInline :: Lens' Bool Defn
funMacro :: Lens' Bool Defn
isMacro :: Defn -> Bool
isEmptyFunction :: Defn -> Bool
isCopatternLHS :: [Clause] -> Bool
recCon :: Defn -> QName
defIsRecord :: Defn -> Bool
defIsDataOrRecord :: Defn -> Bool
defConstructors :: Defn -> [QName]
newtype Fields = Fields [(Name, Type)]
data Simplification
- = YesSimplification
- | NoSimplification
data Reduced no yes
- = NoReduction no
- | YesReduction Simplification yes
data IsReduced
- = NotReduced
- | Reduced (Blocked ())
data MaybeReduced a = MaybeRed {
- isReduced :: IsReduced
- ignoreReduced :: a
}
type MaybeReducedArgs = [MaybeReduced (Arg Term)]
type MaybeReducedElims = [MaybeReduced Elim]
notReduced :: a -> MaybeReduced a
reduced :: Blocked (Arg Term) -> MaybeReduced (Arg Term)
data AllowedReduction
- = ProjectionReductions
- | InlineReductions
- | CopatternReductions
- | FunctionReductions
- | RecursiveReductions
- | LevelReductions
- | UnconfirmedReductions
- | NonTerminatingReductions
type AllowedReductions = [AllowedReduction]
allReductions :: AllowedReductions
data PrimFun = PrimFun {
- primFunName :: QName
- primFunArity :: Arity
- primFunImplementation :: [Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term)
}
defClauses :: Definition -> [Clause]
defCompiled :: Definition -> Maybe CompiledClauses
defParameters :: Definition -> Maybe Nat
defInverse :: Definition -> FunctionInverse
defCompilerPragmas :: BackendName -> Definition -> [CompilerPragma]
defDelayed :: Definition -> Delayed
defNonterminating :: Definition -> Bool
defTerminationUnconfirmed :: Definition -> Bool
defAbstract :: Definition -> IsAbstract
defForced :: Definition -> [IsForced]
type FunctionInverse = FunctionInverse' Clause
type InversionMap c = Map TermHead [c]
data FunctionInverse' c
- = NotInjective
- | Inverse (InversionMap c)
data TermHead
- = SortHead
- | PiHead
- | ConsHead QName
- | VarHead Nat
- | UnknownHead
newtype MutualId = MutId Int32
type Statistics = Map String Integer
data Call
- = CheckClause Type SpineClause
- | CheckPattern Pattern Telescope Type
- | CheckLetBinding LetBinding
- | InferExpr Expr
- | CheckExprCall Expr Type
- | CheckDotPattern Expr Term
- | CheckPatternShadowing SpineClause
- | CheckProjection Range QName Type
- | IsTypeCall Expr Sort
- | IsType_ Expr
- | InferVar Name
- | InferDef QName
- | CheckArguments Range [NamedArg Expr] Type (Maybe Type)
- | CheckTargetType Range Type Type
- | CheckDataDef Range Name [LamBinding] [Constructor]
- | CheckRecDef Range Name [LamBinding] [Constructor]
- | CheckConstructor QName Telescope Sort Constructor
- | CheckFunDefCall Range Name [Clause]
- | CheckPragma Range Pragma
- | CheckPrimitive Range Name Expr
- | CheckIsEmpty Range Type
- | CheckWithFunctionType Expr
- | CheckSectionApplication Range ModuleName ModuleApplication
- | CheckNamedWhere ModuleName
- | ScopeCheckExpr Expr
- | ScopeCheckDeclaration NiceDeclaration
- | ScopeCheckLHS QName Pattern
- | NoHighlighting
- | ModuleContents
- | SetRange Range
type InstanceTable = Map QName (Set QName)
type TempInstanceTable = (InstanceTable, Set QName)
data BuiltinDescriptor
- = BuiltinData (TCM Type) [String]
- | BuiltinDataCons (TCM Type)
- | BuiltinPrim String (Term -> TCM ())
- | BuiltinPostulate Relevance (TCM Type)
- | BuiltinUnknown (Maybe (TCM Type)) (Term -> Type -> TCM ())
data BuiltinInfo = BuiltinInfo {
- builtinName :: String
- builtinDesc :: BuiltinDescriptor
}
type BuiltinThings pf = Map String (Builtin pf)
data Builtin pf
- = Builtin Term
- | Prim pf
data HighlightingLevel
- = None
- | NonInteractive
- | Interactive
data HighlightingMethod
- = Direct
- | Indirect
ifTopLevelAndHighlightingLevelIsOr :: MonadTCM tcm => HighlightingLevel -> Bool -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs :: MonadTCM tcm => HighlightingLevel -> tcm () -> tcm ()
data TCEnv = TCEnv {
- envContext :: Context
- envLetBindings :: LetBindings
- envCurrentModule :: ModuleName
- envCurrentPath :: Maybe AbsolutePath
- envAnonymousModules :: [(ModuleName, Nat)]
- envImportPath :: [TopLevelModuleName]
- envMutualBlock :: Maybe MutualId
- envTerminationCheck :: TerminationCheck ()
- envSolvingConstraints :: Bool
- envCheckingWhere :: Bool
- envWorkingOnTypes :: Bool
- envAssignMetas :: Bool
- envActiveProblems :: Set ProblemId
- envAbstractMode :: AbstractMode
- envRelevance :: Relevance
- envDisplayFormsEnabled :: Bool
- envRange :: Range
- envHighlightingRange :: Range
- envClause :: IPClause
- envCall :: Maybe (Closure Call)
- envHighlightingLevel :: HighlightingLevel
- envHighlightingMethod :: HighlightingMethod
- envModuleNestingLevel :: !Int
- envAllowDestructiveUpdate :: Bool
- envExpandLast :: ExpandHidden
- envAppDef :: Maybe QName
- envSimplification :: Simplification
- envAllowedReductions :: AllowedReductions
- 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
}
initEnv :: TCEnv
disableDestructiveUpdate :: TCM a -> TCM a
data UnquoteFlags = UnquoteFlags {
- _unquoteNormalise :: Bool
}
defaultUnquoteFlags :: UnquoteFlags
unquoteNormalise :: Lens' Bool UnquoteFlags
eUnquoteNormalise :: Lens' Bool TCEnv
eContext :: Lens' Context TCEnv
eLetBindings :: Lens' LetBindings TCEnv
eCurrentModule :: Lens' ModuleName TCEnv
eCurrentPath :: Lens' (Maybe AbsolutePath) TCEnv
eAnonymousModules :: Lens' [(ModuleName, Nat)] TCEnv
eImportPath :: Lens' [TopLevelModuleName] TCEnv
eMutualBlock :: Lens' (Maybe MutualId) TCEnv
eTerminationCheck :: Lens' (TerminationCheck ()) TCEnv
eSolvingConstraints :: Lens' Bool TCEnv
eCheckingWhere :: Lens' Bool TCEnv
eWorkingOnTypes :: Lens' Bool TCEnv
eAssignMetas :: Lens' Bool TCEnv
eActiveProblems :: Lens' (Set ProblemId) TCEnv
eAbstractMode :: Lens' AbstractMode TCEnv
eRelevance :: Lens' Relevance TCEnv
eDisplayFormsEnabled :: Lens' Bool TCEnv
eRange :: Lens' Range TCEnv
eHighlightingRange :: Lens' Range TCEnv
eCall :: Lens' (Maybe (Closure Call)) TCEnv
eHighlightingLevel :: Lens' HighlightingLevel TCEnv
eHighlightingMethod :: Lens' HighlightingMethod TCEnv
eModuleNestingLevel :: Lens' Int TCEnv
eAllowDestructiveUpdate :: Lens' Bool TCEnv
eExpandLast :: Lens' ExpandHidden TCEnv
eAppDef :: Lens' (Maybe QName) TCEnv
eSimplification :: Lens' Simplification TCEnv
eAllowedReductions :: Lens' AllowedReductions TCEnv
eInjectivityDepth :: Lens' Int TCEnv
eCompareBlocked :: Lens' Bool TCEnv
ePrintDomainFreePi :: Lens' Bool TCEnv
eInsideDotPattern :: Lens' Bool TCEnv
eUnquoteFlags :: Lens' UnquoteFlags TCEnv
eInstanceDepth :: Lens' Int TCEnv
eIsDebugPrinting :: Lens' Bool TCEnv
ePrintingPatternLambdas :: Lens' [QName] TCEnv
eCallByNeed :: Lens' Bool TCEnv
eCurrentCheckpoint :: Lens' CheckpointId TCEnv
eCheckpoints :: Lens' (Map CheckpointId Substitution) TCEnv
type Context = [ContextEntry]
type ContextEntry = Dom (Name, Type)
type LetBindings = Map Name (Open (Term, Dom Type))
data AbstractMode
- = AbstractMode
- | ConcreteMode
- | IgnoreAbstractMode
aDefToMode :: IsAbstract -> AbstractMode
aModeToDef :: AbstractMode -> IsAbstract
data ExpandHidden
- = ExpandLast
- | DontExpandLast
data ExplicitToInstance
- = ExplicitToInstance
- | ExplicitStayExplicit
data Candidate = Candidate {
- candidateTerm :: Term
- candidateType :: Type
- candidateEti :: ExplicitToInstance
- candidateOverlappable :: Bool
}
data Warning
- = NicifierIssue DeclarationWarning
- | TerminationIssue [TerminationError]
- | UnreachableClauses QName [[NamedArg DeBruijnPattern]]
- | CoverageIssue QName [(Telescope, [NamedArg DeBruijnPattern])]
- | CoverageNoExactSplit QName [Clause]
- | NotStrictlyPositive QName OccursWhere
- | UnsolvedMetaVariables [Range]
- | UnsolvedInteractionMetas [Range]
- | UnsolvedConstraints Constraints
- | OldBuiltin String String
- | EmptyRewritePragma
- | UselessPublic
- | UselessInline QName
- | InversionDepthReached QName
- | GenericWarning Doc
- | GenericNonFatalError Doc
- | SafeFlagPostulate Name
- | SafeFlagPragma [String]
- | SafeFlagNonTerminating
- | SafeFlagTerminating
- | SafeFlagPrimTrustMe
- | SafeFlagNoPositivityCheck
- | SafeFlagPolarity
- | ParseWarning ParseWarning
- | DeprecationWarning String String String
- | UserWarning String
warningName :: Warning -> WarningName
data TCWarning = TCWarning {
- tcWarningRange :: Range
- tcWarning :: Warning
- tcWarningPrintedWarning :: Doc
- tcWarningCached :: Bool
}
tcWarningOrigin :: TCWarning -> SrcFile
equalHeadConstructors :: Warning -> Warning -> Bool
getPartialDefs :: ReadTCState tcm => tcm [QName]
data CallInfo = CallInfo {
- callInfoTarget :: QName
- callInfoRange :: Range
- callInfoCall :: Closure Term
}
data TerminationError = TerminationError {
- termErrFunctions :: [QName]
- termErrCalls :: [CallInfo]
}
data SplitError
- = NotADatatype (Closure Type)
- | IrrelevantDatatype (Closure Type)
- | CoinductiveDatatype (Closure Type)
- | UnificationStuck {
  - cantSplitConName :: QName
  - cantSplitTel :: Telescope
  - cantSplitConIdx :: Args
  - cantSplitGivenIdx :: Args
  - cantSplitFailures :: [UnificationFailure]
  }
- | GenericSplitError String
data NegativeUnification
- = UnifyConflict Telescope Term Term
- | UnifyCycle Telescope Int Term
data UnificationFailure
- = UnifyIndicesNotVars Telescope Type Term Term Args
- | UnifyRecursiveEq Telescope Type Int Term
- | UnifyReflexiveEq Telescope Type Term
data UnquoteError
- = BadVisibility String (Arg Term)
- | ConInsteadOfDef QName String String
- | DefInsteadOfCon QName String String
- | NonCanonical String Term
- | BlockedOnMeta TCState MetaId
- | UnquotePanic String
data TypeError
- = InternalError String
- | NotImplemented String
- | NotSupported String
- | CompilationError String
- | TerminationCheckFailed [TerminationError]
- | PropMustBeSingleton
- | DataMustEndInSort Term
- | ShouldEndInApplicationOfTheDatatype Type
- | ShouldBeAppliedToTheDatatypeParameters Term Term
- | ShouldBeApplicationOf Type QName
- | ConstructorPatternInWrongDatatype QName QName
- | CantResolveOverloadedConstructorsTargetingSameDatatype QName [QName]
- | DoesNotConstructAnElementOf QName Type
- | DifferentArities
- | WrongHidingInLHS
- | WrongHidingInLambda Type
- | WrongHidingInApplication Type
- | WrongNamedArgument (NamedArg Expr)
- | WrongIrrelevanceInLambda
- | WrongInstanceDeclaration
- | HidingMismatch Hiding Hiding
- | RelevanceMismatch Relevance Relevance
- | UninstantiatedDotPattern Expr
- | ForcedConstructorNotInstantiated Pattern
- | IlltypedPattern Pattern Type
- | IllformedProjectionPattern Pattern
- | CannotEliminateWithPattern (NamedArg Pattern) Type
- | WrongNumberOfConstructorArguments QName Nat Nat
- | ShouldBeEmpty Type [DeBruijnPattern]
- | ShouldBeASort Type
- | ShouldBePi Type
- | ShouldBeRecordType Type
- | ShouldBeRecordPattern DeBruijnPattern
- | NotAProjectionPattern (NamedArg Pattern)
- | NotAProperTerm
- | SetOmegaNotValidType
- | InvalidTypeSort Sort
- | InvalidType Term
- | FunctionTypeInSizeUniv Term
- | SplitOnIrrelevant (Dom Type)
- | SplitOnNonVariable Term Type
- | DefinitionIsIrrelevant QName
- | VariableIsIrrelevant Name
- | UnequalTerms Comparison Term Term Type
- | UnequalTypes Comparison Type Type
- | UnequalRelevance Comparison Term Term
- | UnequalHiding Term Term
- | UnequalSorts Sort Sort
- | UnequalBecauseOfUniverseConflict Comparison Term Term
- | NotLeqSort Sort Sort
- | MetaCannotDependOn MetaId [Nat] Nat
- | MetaOccursInItself MetaId
- | MetaIrrelevantSolution MetaId Term
- | GenericError String
- | GenericDocError Doc
- | BuiltinMustBeConstructor String Expr
- | NoSuchBuiltinName String
- | DuplicateBuiltinBinding String Term Term
- | NoBindingForBuiltin String
- | NoSuchPrimitiveFunction String
- | ShadowedModule Name [ModuleName]
- | BuiltinInParameterisedModule String
- | IllegalLetInTelescope TypedBinding
- | NoRHSRequiresAbsurdPattern [NamedArg Pattern]
- | AbsurdPatternRequiresNoRHS [NamedArg Pattern]
- | TooFewFields QName [Name]
- | TooManyFields QName [Name]
- | DuplicateFields [Name]
- | DuplicateConstructors [Name]
- | WithOnFreeVariable Expr Term
- | UnexpectedWithPatterns [Pattern]
- | WithClausePatternMismatch Pattern (NamedArg DeBruijnPattern)
- | FieldOutsideRecord
- | ModuleArityMismatch ModuleName Telescope [NamedArg Expr]
- | SplitError SplitError
- | ImpossibleConstructor QName NegativeUnification
- | TooManyPolarities QName Int
- | LocalVsImportedModuleClash ModuleName
- | SolvedButOpenHoles
- | CyclicModuleDependency [TopLevelModuleName]
- | FileNotFound TopLevelModuleName [AbsolutePath]
- | OverlappingProjects AbsolutePath TopLevelModuleName TopLevelModuleName
- | AmbiguousTopLevelModuleName TopLevelModuleName [AbsolutePath]
- | ModuleNameUnexpected TopLevelModuleName TopLevelModuleName
- | ModuleNameDoesntMatchFileName TopLevelModuleName [AbsolutePath]
- | ClashingFileNamesFor ModuleName [AbsolutePath]
- | ModuleDefinedInOtherFile TopLevelModuleName AbsolutePath AbsolutePath
- | BothWithAndRHS
- | AbstractConstructorNotInScope QName
- | NotInScope [QName]
- | NoSuchModule QName
- | AmbiguousName QName (NonemptyList QName)
- | AmbiguousModule QName (NonemptyList ModuleName)
- | UninstantiatedModule QName
- | ClashingDefinition QName QName
- | ClashingModule ModuleName ModuleName
- | ClashingImport Name QName
- | ClashingModuleImport Name ModuleName
- | PatternShadowsConstructor Name QName
- | ModuleDoesntExport QName [ImportedName]
- | DuplicateImports QName [ImportedName]
- | InvalidPattern Pattern
- | RepeatedVariablesInPattern [Name]
- | NotAModuleExpr Expr
- | NotAnExpression Expr
- | NotAValidLetBinding NiceDeclaration
- | NotValidBeforeField NiceDeclaration
- | NothingAppliedToHiddenArg Expr
- | NothingAppliedToInstanceArg Expr
- | BadArgumentsToPatternSynonym AmbiguousQName
- | TooFewArgumentsToPatternSynonym AmbiguousQName
- | CannotResolveAmbiguousPatternSynonym (NonemptyList (QName, PatternSynDefn))
- | UnusedVariableInPatternSynonym
- | NoParseForApplication [Expr]
- | AmbiguousParseForApplication [Expr] [Expr]
- | NoParseForLHS LHSOrPatSyn Pattern
- | AmbiguousParseForLHS LHSOrPatSyn Pattern [Pattern]
- | OperatorInformation [NotationSection] TypeError
- | IFSNoCandidateInScope Type
- | UnquoteFailed UnquoteError
- | DeBruijnIndexOutOfScope Nat Telescope [Name]
- | NeedOptionCopatterns
- | NeedOptionRewriting
- | NonFatalErrors [TCWarning]
- | InstanceSearchDepthExhausted Term Type Int
data LHSOrPatSyn
- = IsLHS
- | IsPatSyn
data TCErr
- = TypeError {
  - tcErrState :: TCState
  - tcErrClosErr :: Closure TypeError
  }
- | Exception Range Doc
- | IOException TCState Range IOException
- | PatternErr
class (Functor m, Applicative m, Monad m) => HasOptions m where
data ReduceEnv = ReduceEnv {
- redEnv :: TCEnv
- redSt :: TCState
}
mapRedEnv :: (TCEnv -> TCEnv) -> ReduceEnv -> ReduceEnv
mapRedSt :: (TCState -> TCState) -> ReduceEnv -> ReduceEnv
mapRedEnvSt :: (TCEnv -> TCEnv) -> (TCState -> TCState) -> ReduceEnv -> ReduceEnv
reduceEnv :: Lens' TCEnv ReduceEnv
reduceSt :: Lens' TCState ReduceEnv
newtype ReduceM a = ReduceM {
- unReduceM :: ReduceEnv -> a
}
onReduceEnv :: (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a
fmapReduce :: (a -> b) -> ReduceM a -> ReduceM b
apReduce :: ReduceM (a -> b) -> ReduceM a -> ReduceM b
bindReduce :: ReduceM a -> (a -> ReduceM b) -> ReduceM b
runReduceM :: ReduceM a -> TCM a
runReduceF :: (a -> ReduceM b) -> TCM (a -> b)
newtype TCMT m a = TCM {
- unTCM :: IORef TCState -> TCEnv -> m a
}
type TCM = TCMT IO
class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm, HasOptions tcm) => MonadTCM tcm where
type IM = TCMT (InputT IO)
runIM :: IM a -> TCM a
catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a
finally_ :: TCM a -> TCM b -> TCM a
mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a
pureTCM :: MonadIO m => (TCState -> TCEnv -> a) -> TCMT m a
returnTCMT :: MonadIO m => a -> TCMT m a
bindTCMT :: MonadIO m => TCMT m a -> (a -> TCMT m b) -> TCMT m b
thenTCMT :: MonadIO m => TCMT m a -> TCMT m b -> TCMT m b
fmapTCMT :: MonadIO m => (a -> b) -> TCMT m a -> TCMT m b
apTCMT :: MonadIO m => TCMT m (a -> b) -> TCMT m a -> TCMT m b
patternViolation :: TCM a
internalError :: MonadTCM tcm => String -> tcm a
genericError :: MonadTCM tcm => String -> tcm a
genericDocError :: MonadTCM tcm => Doc -> tcm a
typeError :: MonadTCM tcm => TypeError -> tcm a
typeError_ :: MonadTCM tcm => TypeError -> tcm TCErr
runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState)
runTCMTop :: TCM a -> IO (Either TCErr a)
runTCMTop' :: MonadIO m => TCMT m a -> m a
runSafeTCM :: TCM a -> TCState -> IO (a, TCState)
forkTCM :: TCM a -> TCM ()
extendedLambdaName :: String
absurdLambdaName :: String
isAbsurdLambdaName :: QName -> Bool

Type checking state

data TCState #

Constructors

TCSt
Fields stPreScopeState :: !PreScopeState The state which is frozen after scope checking. stPostScopeState :: !PostScopeState The state which is modified after scope checking. stPersistentState :: !PersistentTCState State which is forever, like a diamond.

Instances

Show TCState #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> TCState -> ShowS # show :: TCState -> String # showList :: [TCState] -> ShowS #
LensPersistentVerbosity TCState #
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPersistentVerbosity :: TCState -> PersistentVerbosity # setPersistentVerbosity :: PersistentVerbosity -> TCState -> TCState # mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> TCState -> TCState #
LensIncludePaths TCState #
Instance details Defined in Agda.Interaction.Options.Lenses Methods getIncludePaths :: TCState -> [FilePath] # setIncludePaths :: [FilePath] -> TCState -> TCState # mapIncludePaths :: ([FilePath] -> [FilePath]) -> TCState -> TCState # getAbsoluteIncludePaths :: TCState -> [AbsolutePath] # setAbsoluteIncludePaths :: [AbsolutePath] -> TCState -> TCState # mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> TCState -> TCState #
LensSafeMode TCState #
Instance details Defined in Agda.Interaction.Options.Lenses Methods getSafeMode :: TCState -> SafeMode # setSafeMode :: SafeMode -> TCState -> TCState # mapSafeMode :: (SafeMode -> SafeMode) -> TCState -> TCState #
LensCommandLineOptions TCState #
Instance details Defined in Agda.Interaction.Options.Lenses Methods getCommandLineOptions :: TCState -> CommandLineOptions # setCommandLineOptions :: CommandLineOptions -> TCState -> TCState # mapCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> TCState -> TCState #
LensVerbosity TCState #
Instance details Defined in Agda.Interaction.Options.Lenses Methods getVerbosity :: TCState -> Verbosity # setVerbosity :: Verbosity -> TCState -> TCState # mapVerbosity :: (Verbosity -> Verbosity) -> TCState -> TCState #
LensPragmaOptions TCState #
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPragmaOptions :: TCState -> PragmaOptions # setPragmaOptions :: PragmaOptions -> TCState -> TCState # mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> TCState -> TCState #
MonadState TCState TerM #
Instance details Defined in Agda.Termination.Monad Methods get :: TerM TCState # put :: TCState -> TerM () # state :: (TCState -> (a, TCState)) -> TerM a #
MonadIO m => MonadState TCState (TCMT m) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods get :: TCMT m TCState # put :: TCState -> TCMT m () # state :: (TCState -> (a, TCState)) -> TCMT m a #

class Monad m => ReadTCState m where #

Minimal complete definition

getTCState

Methods

getTCState :: m TCState #

Instances

ReadTCState ReduceM #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTCState :: ReduceM TCState #
MonadIO m => ReadTCState (TCMT m) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTCState :: TCMT m TCState #

data PreScopeState #

Constructors

PreScopeState

Fields

stPreTokens :: !CompressedFile
Highlighting info for tokens (but not those tokens for which highlighting exists in stSyntaxInfo).
stPreImports :: !Signature
Imported declared identifiers. Those most not be serialized!
stPreImportedModules :: !(Set ModuleName)
stPreModuleToSource :: !ModuleToSource
stPreVisitedModules :: !VisitedModules
stPreScope :: !ScopeInfo
stPrePatternSyns :: !PatternSynDefns
Pattern synonyms of the current file. Serialized.
stPrePatternSynImports :: !PatternSynDefns
Imported pattern synonyms. Must not be serialized!
stPrePragmaOptions :: !PragmaOptions
Options applying to the current file. OPTIONS pragmas only affect this field.
stPreImportedBuiltins :: !(BuiltinThings PrimFun)
stPreImportedDisplayForms :: !DisplayForms
Display forms added by someone else to imported identifiers
stPreImportedInstanceDefs :: !InstanceTable
stPreForeignCode :: !(Map BackendName [ForeignCode])
{--} code that should be included in the compiled output. Does not include code for imported modules.
stPreFreshInteractionId :: !InteractionId
stPreUserWarnings :: !(Map QName String)

type DisambiguatedNames = IntMap QName #

data PostScopeState #

Constructors

PostScopeState

Fields

stPostSyntaxInfo :: !CompressedFile
Highlighting info.
stPostDisambiguatedNames :: !DisambiguatedNames
Disambiguation carried out by the type checker. Maps position of first name character to disambiguated QName for each AmbiguousQName already passed by the type checker.
stPostMetaStore :: !MetaStore
stPostInteractionPoints :: !InteractionPoints
stPostAwakeConstraints :: !Constraints
stPostSleepingConstraints :: !Constraints
stPostDirty :: !Bool
Dirty when a constraint is added, used to prevent pointer update. Currently unused.
stPostOccursCheckDefs :: !(Set QName)
Definitions to be considered during occurs check. Initialized to the current mutual block before the check. During occurs check, we remove definitions from this set as soon we have checked them.
stPostSignature :: !Signature
Declared identifiers of the current file. These will be serialized after successful type checking.
stPostModuleCheckpoints :: !(Map ModuleName CheckpointId)
For each module remember the checkpoint corresponding to the orignal context of the module parameters.
stPostImportsDisplayForms :: !DisplayForms
Display forms we add for imported identifiers
stPostCurrentModule :: !(Maybe ModuleName)
The current module is available after it has been type checked.
stPostInstanceDefs :: !TempInstanceTable
stPostStatistics :: !Statistics
Counters to collect various statistics about meta variables etc. Only for current file.
stPostTCWarnings :: ![TCWarning]
stPostMutualBlocks :: !(Map MutualId MutualBlock)
stPostLocalBuiltins :: !(BuiltinThings PrimFun)
stPostFreshMetaId :: !MetaId
stPostFreshMutualId :: !MutualId
stPostFreshProblemId :: !ProblemId
stPostFreshCheckpointId :: !CheckpointId
stPostFreshInt :: !Int
stPostFreshNameId :: !NameId
stPostAreWeCaching :: !Bool

data MutualBlock #

A mutual block of names in the signature.

Constructors

MutualBlock
Fields mutualInfo :: MutualInfo The original info of the mutual block. mutualNames :: Set QName

Instances

Eq MutualBlock #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: MutualBlock -> MutualBlock -> Bool # (/=) :: MutualBlock -> MutualBlock -> Bool #
Show MutualBlock #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> MutualBlock -> ShowS # show :: MutualBlock -> String # showList :: [MutualBlock] -> ShowS #
Null MutualBlock #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: MutualBlock # null :: MutualBlock -> Bool #

data PersistentTCState #

A part of the state which is not reverted when an error is thrown or the state is reset.

Constructors

PersistentTCSt

Fields

stDecodedModules :: DecodedModules
stPersistentOptions :: CommandLineOptions
stInteractionOutputCallback :: InteractionOutputCallback
Callback function to call when there is a response to give to the interactive frontend. See the documentation of InteractionOutputCallback.
stBenchmark :: !Benchmark
Structure to track how much CPU time was spent on which Agda phase. Needs to be a strict field to avoid space leaks!
stAccumStatistics :: !Statistics
Should be strict field.
stLoadedFileCache :: !(Maybe LoadedFileCache)
Cached typechecking state from the last loaded file. Should be Nothing when checking imports.
stPersistBackends :: [Backend]
Current backends with their options

Instances

LensPersistentVerbosity PersistentTCState #
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPersistentVerbosity :: PersistentTCState -> PersistentVerbosity # setPersistentVerbosity :: PersistentVerbosity -> PersistentTCState -> PersistentTCState # mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> PersistentTCState -> PersistentTCState #
LensIncludePaths PersistentTCState #
Instance details Defined in Agda.Interaction.Options.Lenses Methods getIncludePaths :: PersistentTCState -> [FilePath] # setIncludePaths :: [FilePath] -> PersistentTCState -> PersistentTCState # mapIncludePaths :: ([FilePath] -> [FilePath]) -> PersistentTCState -> PersistentTCState # getAbsoluteIncludePaths :: PersistentTCState -> [AbsolutePath] # setAbsoluteIncludePaths :: [AbsolutePath] -> PersistentTCState -> PersistentTCState # mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> PersistentTCState -> PersistentTCState #
LensSafeMode PersistentTCState #
Instance details Defined in Agda.Interaction.Options.Lenses Methods getSafeMode :: PersistentTCState -> SafeMode # setSafeMode :: SafeMode -> PersistentTCState -> PersistentTCState # mapSafeMode :: (SafeMode -> SafeMode) -> PersistentTCState -> PersistentTCState #
LensCommandLineOptions PersistentTCState #
Instance details Defined in Agda.Interaction.Options.Lenses Methods getCommandLineOptions :: PersistentTCState -> CommandLineOptions # setCommandLineOptions :: CommandLineOptions -> PersistentTCState -> PersistentTCState # mapCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> PersistentTCState -> PersistentTCState #

data LoadedFileCache #

Constructors

LoadedFileCache
Fields lfcCached :: !CachedTypeCheckLog lfcCurrent :: !CurrentTypeCheckLog

type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)] #

A log of what the type checker does and states after the action is completed. The cached version is stored first executed action first.

type CurrentTypeCheckLog = [(TypeCheckAction, PostScopeState)] #

Like CachedTypeCheckLog, but storing the log for an ongoing type checking of a module. Stored in reverse order (last performed action first).

data TypeCheckAction #

A complete log for a module will look like this:

Pragmas
EnterSection, entering the main module.
'Decl'/'EnterSection'/'LeaveSection', for declarations and nested modules
LeaveSection, leaving the main module.

Constructors

EnterSection !ModuleInfo !ModuleName ![TypedBindings]
LeaveSection !ModuleName
Decl !Declaration	Never a Section or ScopeDecl
Pragmas !PragmaOptions

initPersistentState :: PersistentTCState #

Empty persistent state.

initPreScopeState :: PreScopeState #

Empty state of type checker.

initPostScopeState :: PostScopeState #

initState :: TCState #

st-prefixed lenses

stTokens :: Lens' CompressedFile TCState #

stImports :: Lens' Signature TCState #

stImportedModules :: Lens' (Set ModuleName) TCState #

stModuleToSource :: Lens' ModuleToSource TCState #

stVisitedModules :: Lens' VisitedModules TCState #

stScope :: Lens' ScopeInfo TCState #

stPatternSyns :: Lens' PatternSynDefns TCState #

stPatternSynImports :: Lens' PatternSynDefns TCState #

stPragmaOptions :: Lens' PragmaOptions TCState #

stImportedBuiltins :: Lens' (BuiltinThings PrimFun) TCState #

stForeignCode :: Lens' (Map BackendName [ForeignCode]) TCState #

stFreshInteractionId :: Lens' InteractionId TCState #

stUserWarnings :: Lens' (Map QName String) TCState #

stBackends :: Lens' [Backend] TCState #

stFreshNameId :: Lens' NameId TCState #

stSyntaxInfo :: Lens' CompressedFile TCState #

stDisambiguatedNames :: Lens' DisambiguatedNames TCState #

stMetaStore :: Lens' MetaStore TCState #

stInteractionPoints :: Lens' InteractionPoints TCState #

stAwakeConstraints :: Lens' Constraints TCState #

stSleepingConstraints :: Lens' Constraints TCState #

stDirty :: Lens' Bool TCState #

stOccursCheckDefs :: Lens' (Set QName) TCState #

stSignature :: Lens' Signature TCState #

stModuleCheckpoints :: Lens' (Map ModuleName CheckpointId) TCState #

stImportsDisplayForms :: Lens' DisplayForms TCState #

stImportedDisplayForms :: Lens' DisplayForms TCState #

stCurrentModule :: Lens' (Maybe ModuleName) TCState #

stImportedInstanceDefs :: Lens' InstanceTable TCState #

stInstanceDefs :: Lens' TempInstanceTable TCState #

stStatistics :: Lens' Statistics TCState #

stTCWarnings :: Lens' [TCWarning] TCState #

stMutualBlocks :: Lens' (Map MutualId MutualBlock) TCState #

stLocalBuiltins :: Lens' (BuiltinThings PrimFun) TCState #

stFreshMetaId :: Lens' MetaId TCState #

stFreshMutualId :: Lens' MutualId TCState #

stFreshProblemId :: Lens' ProblemId TCState #

stFreshCheckpointId :: Lens' CheckpointId TCState #

stFreshInt :: Lens' Int TCState #

stAreWeCaching :: Lens' Bool TCState #

stBuiltinThings :: TCState -> BuiltinThings PrimFun #

Fresh things

class Enum i => HasFresh i where #

Minimal complete definition

freshLens

Methods

freshLens :: Lens' i TCState #

nextFresh' :: i -> i #

Instances

HasFresh Int #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' Int TCState # nextFresh' :: Int -> Int #
HasFresh InteractionId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' InteractionId TCState # nextFresh' :: InteractionId -> InteractionId #
HasFresh MetaId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' MetaId TCState # nextFresh' :: MetaId -> MetaId #
HasFresh NameId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' NameId TCState # nextFresh' :: NameId -> NameId #
HasFresh MutualId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' MutualId TCState # nextFresh' :: MutualId -> MutualId #
HasFresh CheckpointId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' CheckpointId TCState # nextFresh' :: CheckpointId -> CheckpointId #
HasFresh ProblemId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' ProblemId TCState # nextFresh' :: ProblemId -> ProblemId #

nextFresh :: HasFresh i => TCState -> (i, TCState) #

fresh :: (HasFresh i, MonadState TCState m) => m i #

newtype ProblemId #

Constructors

ProblemId Nat

Instances

Enum ProblemId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods succ :: ProblemId -> ProblemId # pred :: ProblemId -> ProblemId # toEnum :: Int -> ProblemId # fromEnum :: ProblemId -> Int # enumFrom :: ProblemId -> [ProblemId] # enumFromThen :: ProblemId -> ProblemId -> [ProblemId] # enumFromTo :: ProblemId -> ProblemId -> [ProblemId] # enumFromThenTo :: ProblemId -> ProblemId -> ProblemId -> [ProblemId] #
Eq ProblemId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: ProblemId -> ProblemId -> Bool # (/=) :: ProblemId -> ProblemId -> Bool #
Integral ProblemId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods quot :: ProblemId -> ProblemId -> ProblemId # rem :: ProblemId -> ProblemId -> ProblemId # div :: ProblemId -> ProblemId -> ProblemId # mod :: ProblemId -> ProblemId -> ProblemId # quotRem :: ProblemId -> ProblemId -> (ProblemId, ProblemId) # divMod :: ProblemId -> ProblemId -> (ProblemId, ProblemId) # toInteger :: ProblemId -> Integer #
Data ProblemId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemId -> c ProblemId # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemId # toConstr :: ProblemId -> Constr # dataTypeOf :: ProblemId -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemId) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemId) # gmapT :: (forall b. Data b => b -> b) -> ProblemId -> ProblemId # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemId -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemId -> r # gmapQ :: (forall d. Data d => d -> u) -> ProblemId -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemId -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId #
Num ProblemId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (+) :: ProblemId -> ProblemId -> ProblemId # (-) :: ProblemId -> ProblemId -> ProblemId # (*) :: ProblemId -> ProblemId -> ProblemId # negate :: ProblemId -> ProblemId # abs :: ProblemId -> ProblemId # signum :: ProblemId -> ProblemId # fromInteger :: Integer -> ProblemId #
Ord ProblemId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods compare :: ProblemId -> ProblemId -> Ordering # (<) :: ProblemId -> ProblemId -> Bool # (<=) :: ProblemId -> ProblemId -> Bool # (>) :: ProblemId -> ProblemId -> Bool # (>=) :: ProblemId -> ProblemId -> Bool # max :: ProblemId -> ProblemId -> ProblemId # min :: ProblemId -> ProblemId -> ProblemId #
Real ProblemId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods toRational :: ProblemId -> Rational #
Show ProblemId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> ProblemId -> ShowS # show :: ProblemId -> String # showList :: [ProblemId] -> ShowS #
Pretty ProblemId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: ProblemId -> Doc # prettyPrec :: Int -> ProblemId -> Doc # prettyList :: [ProblemId] -> Doc #
HasFresh ProblemId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' ProblemId TCState # nextFresh' :: ProblemId -> ProblemId #
PrettyTCM ProblemId #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: ProblemId -> TCM Doc #

newtype CheckpointId #

Constructors

CheckpointId Int

Instances

Enum CheckpointId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods succ :: CheckpointId -> CheckpointId # pred :: CheckpointId -> CheckpointId # toEnum :: Int -> CheckpointId # fromEnum :: CheckpointId -> Int # enumFrom :: CheckpointId -> [CheckpointId] # enumFromThen :: CheckpointId -> CheckpointId -> [CheckpointId] # enumFromTo :: CheckpointId -> CheckpointId -> [CheckpointId] # enumFromThenTo :: CheckpointId -> CheckpointId -> CheckpointId -> [CheckpointId] #
Eq CheckpointId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: CheckpointId -> CheckpointId -> Bool # (/=) :: CheckpointId -> CheckpointId -> Bool #
Integral CheckpointId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods quot :: CheckpointId -> CheckpointId -> CheckpointId # rem :: CheckpointId -> CheckpointId -> CheckpointId # div :: CheckpointId -> CheckpointId -> CheckpointId # mod :: CheckpointId -> CheckpointId -> CheckpointId # quotRem :: CheckpointId -> CheckpointId -> (CheckpointId, CheckpointId) # divMod :: CheckpointId -> CheckpointId -> (CheckpointId, CheckpointId) # toInteger :: CheckpointId -> Integer #
Data CheckpointId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CheckpointId -> c CheckpointId # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CheckpointId # toConstr :: CheckpointId -> Constr # dataTypeOf :: CheckpointId -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CheckpointId) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CheckpointId) # gmapT :: (forall b. Data b => b -> b) -> CheckpointId -> CheckpointId # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CheckpointId -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CheckpointId -> r # gmapQ :: (forall d. Data d => d -> u) -> CheckpointId -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> CheckpointId -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> CheckpointId -> m CheckpointId # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CheckpointId -> m CheckpointId # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CheckpointId -> m CheckpointId #
Num CheckpointId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (+) :: CheckpointId -> CheckpointId -> CheckpointId # (-) :: CheckpointId -> CheckpointId -> CheckpointId # (*) :: CheckpointId -> CheckpointId -> CheckpointId # negate :: CheckpointId -> CheckpointId # abs :: CheckpointId -> CheckpointId # signum :: CheckpointId -> CheckpointId # fromInteger :: Integer -> CheckpointId #
Ord CheckpointId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods compare :: CheckpointId -> CheckpointId -> Ordering # (<) :: CheckpointId -> CheckpointId -> Bool # (<=) :: CheckpointId -> CheckpointId -> Bool # (>) :: CheckpointId -> CheckpointId -> Bool # (>=) :: CheckpointId -> CheckpointId -> Bool # max :: CheckpointId -> CheckpointId -> CheckpointId # min :: CheckpointId -> CheckpointId -> CheckpointId #
Real CheckpointId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods toRational :: CheckpointId -> Rational #
Show CheckpointId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> CheckpointId -> ShowS # show :: CheckpointId -> String # showList :: [CheckpointId] -> ShowS #
Pretty CheckpointId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: CheckpointId -> Doc # prettyPrec :: Int -> CheckpointId -> Doc # prettyList :: [CheckpointId] -> Doc #
HasFresh CheckpointId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' CheckpointId TCState # nextFresh' :: CheckpointId -> CheckpointId #
EmbPrj CheckpointId #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: CheckpointId -> S Int32 # icod_ :: CheckpointId -> S Int32 # value :: Int32 -> R CheckpointId #
PrettyTCM CheckpointId #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: CheckpointId -> TCM Doc #

freshName :: MonadState TCState m => Range -> String -> m Name #

freshNoName :: MonadState TCState m => Range -> m Name #

freshNoName_ :: MonadState TCState m => m Name #

class FreshName a where #

Create a fresh name from a.

Minimal complete definition

freshName_

Methods

freshName_ :: MonadState TCState m => a -> m Name #

Instances

FreshName () #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadState TCState m => () -> m Name #
FreshName String #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadState TCState m => String -> m Name #
FreshName Range #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadState TCState m => Range -> m Name #
FreshName (Range, String) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshName_ :: MonadState TCState m => (Range, String) -> m Name #

Managing file names

type ModuleToSource = Map TopLevelModuleName AbsolutePath #

Maps top-level module names to the corresponding source file names.

type SourceToModule = Map AbsolutePath TopLevelModuleName #

Maps source file names to the corresponding top-level module names.

sourceToModule :: TCM SourceToModule #

Creates a SourceToModule map based on stModuleToSource.

O(n log n).

For a single reverse lookup in stModuleToSource, rather use lookupModuleFromSourse.

lookupModuleFromSource :: AbsolutePath -> TCM (Maybe TopLevelModuleName) #

Lookup an AbsolutePath in sourceToModule.

O(n).

Interface

data ModuleInfo #

Constructors

ModuleInfo
Fields miInterface :: Interface miWarnings :: Bool `True` if warnings were encountered when the module was type checked.

type VisitedModules = Map TopLevelModuleName ModuleInfo #

type DecodedModules = Map TopLevelModuleName Interface #

data ForeignCode #

Constructors

ForeignCode Range String

Instances

Show ForeignCode #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> ForeignCode -> ShowS # show :: ForeignCode -> String # showList :: [ForeignCode] -> ShowS #
EmbPrj ForeignCode #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Compilers Methods icode :: ForeignCode -> S Int32 # icod_ :: ForeignCode -> S Int32 # value :: Int32 -> R ForeignCode #

data Interface #

Constructors

Interface

Fields

iSourceHash :: Hash
Hash of the source code.
iImportedModules :: [(ModuleName, Hash)]
Imported modules and their hashes.
iModuleName :: ModuleName
Module name of this interface.
iScope :: Map ModuleName Scope
Scope defined by this module.
Andreas, AIM XX: Too avoid duplicate serialization, this field is not serialized, so if you deserialize an interface, iScope will be empty. But constructIScope constructs iScope from iInsideScope.
iInsideScope :: ScopeInfo
Scope after we loaded this interface. Used in AtTopLevel and interactionLoop.
iSignature :: Signature
iDisplayForms :: DisplayForms
Display forms added for imported identifiers.
iUserWarnings :: Map QName String
User warnings for imported identifiers
iBuiltin :: BuiltinThings (String, QName)
iForeignCode :: Map BackendName [ForeignCode]
iHighlighting :: HighlightingInfo
iPragmaOptions :: [OptionsPragma]
Pragma options set in the file.
iPatternSyns :: PatternSynDefns
iWarnings :: [TCWarning]

Instances

Show Interface #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Interface -> ShowS # show :: Interface -> String # showList :: [Interface] -> ShowS #
Pretty Interface #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Interface -> Doc # prettyPrec :: Int -> Interface -> Doc # prettyList :: [Interface] -> Doc #
EmbPrj Interface #
Instance details Defined in Agda.TypeChecking.Serialise.Instances Methods icode :: Interface -> S Int32 # icod_ :: Interface -> S Int32 # value :: Int32 -> R Interface #
InstantiateFull Interface #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Interface -> ReduceM Interface #

iFullHash :: Interface -> Hash #

Combines the source hash and the (full) hashes of the imported modules.

Constraints

type Constraints = [ProblemConstraint] #

data ProblemConstraint #

Constructors

PConstr
Fields constraintProblems :: Set ProblemId theConstraint :: Closure Constraint

Instances

Data ProblemConstraint #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemConstraint -> c ProblemConstraint # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemConstraint # toConstr :: ProblemConstraint -> Constr # dataTypeOf :: ProblemConstraint -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemConstraint) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemConstraint) # gmapT :: (forall b. Data b => b -> b) -> ProblemConstraint -> ProblemConstraint # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemConstraint -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemConstraint -> r # gmapQ :: (forall d. Data d => d -> u) -> ProblemConstraint -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemConstraint -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemConstraint -> m ProblemConstraint # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemConstraint -> m ProblemConstraint # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemConstraint -> m ProblemConstraint #
Show ProblemConstraint #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> ProblemConstraint -> ShowS # show :: ProblemConstraint -> String # showList :: [ProblemConstraint] -> ShowS #
HasRange ProblemConstraint #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: ProblemConstraint -> Range #
PrettyTCM ProblemConstraint #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: ProblemConstraint -> TCM Doc #
MentionsMeta ProblemConstraint #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> ProblemConstraint -> Bool #
InstantiateFull ProblemConstraint #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ProblemConstraint -> ReduceM ProblemConstraint #
Normalise ProblemConstraint #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: ProblemConstraint -> ReduceM ProblemConstraint #
Simplify ProblemConstraint #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: ProblemConstraint -> ReduceM ProblemConstraint #
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) #
Instance details Defined in Agda.Interaction.BasicOps Methods reify :: ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) # reifyWhen :: Bool -> ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) #

data Constraint #

Constructors

ValueCmp Comparison Type Term Term
ElimCmp [Polarity] [IsForced] Type Term [Elim] [Elim]
TypeCmp Comparison Type Type
TelCmp Type Type Comparison Telescope Telescope	the two types are for the error message only
SortCmp Comparison Sort Sort
LevelCmp Comparison Level Level
HasBiggerSort Sort
HasPTSRule Sort (Abs Sort)
UnBlock MetaId
Guarded Constraint ProblemId
IsEmpty Range Type	The range is the one of the absurd pattern.
CheckSizeLtSat Term	Check that the `Term` is either not a SIZELT or a non-empty SIZELT.
FindInScope MetaId (Maybe MetaId) (Maybe [Candidate])	the first argument is the instance argument, the second one is the meta on which the constraint may be blocked on and the third one is the list of candidates (or Nothing if we haven’t determined the list of candidates yet)
CheckFunDef Delayed DefInfo QName [Clause]

Instances

Eq Constraint #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Constraint -> Constraint -> Bool # (/=) :: Constraint -> Constraint -> Bool #
Data Constraint #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Constraint -> c Constraint # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Constraint # toConstr :: Constraint -> Constr # dataTypeOf :: Constraint -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Constraint) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constraint) # gmapT :: (forall b. Data b => b -> b) -> Constraint -> Constraint # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Constraint -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Constraint -> r # gmapQ :: (forall d. Data d => d -> u) -> Constraint -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Constraint -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Constraint -> m Constraint # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Constraint -> m Constraint # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Constraint -> m Constraint #
Show Constraint #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Constraint -> ShowS # show :: Constraint -> String # showList :: [Constraint] -> ShowS #
HasRange Constraint #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: Constraint -> Range #
Free Constraint #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet c => Constraint -> FreeM c #
TermLike Constraint #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods traverseTermM :: Monad m => (Term -> m Term) -> Constraint -> m Constraint # foldTerm :: Monoid m => (Term -> m) -> Constraint -> m #
PrettyTCM Constraint #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Constraint -> TCM Doc #
MentionsMeta Constraint #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Constraint -> Bool #
InstantiateFull Constraint #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Constraint -> ReduceM Constraint #
Normalise Constraint #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Constraint -> ReduceM Constraint #
Simplify Constraint #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Constraint -> ReduceM Constraint #
Reduce Constraint #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Constraint -> ReduceM Constraint # reduceB' :: Constraint -> ReduceM (Blocked Constraint) #
Instantiate Constraint #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Constraint -> ReduceM Constraint #
Subst Term Constraint #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Constraint -> Constraint #
Reify Constraint (OutputConstraint Expr Expr) #
Instance details Defined in Agda.Interaction.BasicOps Methods reify :: Constraint -> TCM (OutputConstraint Expr Expr) # reifyWhen :: Bool -> Constraint -> TCM (OutputConstraint Expr Expr) #

data Comparison #

Constructors

CmpEq
CmpLeq

Instances

Eq Comparison #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: Comparison -> Comparison -> Bool # (/=) :: Comparison -> Comparison -> Bool #
Data Comparison #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Comparison -> c Comparison # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Comparison # toConstr :: Comparison -> Constr # dataTypeOf :: Comparison -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Comparison) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Comparison) # gmapT :: (forall b. Data b => b -> b) -> Comparison -> Comparison # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Comparison -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Comparison -> r # gmapQ :: (forall d. Data d => d -> u) -> Comparison -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Comparison -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison #
Show Comparison #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Comparison -> ShowS # show :: Comparison -> String # showList :: [Comparison] -> ShowS #
Pretty Comparison #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Comparison -> Doc # prettyPrec :: Int -> Comparison -> Doc # prettyList :: [Comparison] -> Doc #
PrettyTCM Comparison #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Comparison -> TCM Doc #

data CompareDirection #

An extension of Comparison to >=.

Constructors

DirEq
DirLeq
DirGeq

Instances

Eq CompareDirection #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: CompareDirection -> CompareDirection -> Bool # (/=) :: CompareDirection -> CompareDirection -> Bool #
Show CompareDirection #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> CompareDirection -> ShowS # show :: CompareDirection -> String # showList :: [CompareDirection] -> ShowS #
Pretty CompareDirection #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: CompareDirection -> Doc # prettyPrec :: Int -> CompareDirection -> Doc # prettyList :: [CompareDirection] -> Doc #

fromCmp :: Comparison -> CompareDirection #

Embed Comparison into CompareDirection.

flipCmp :: CompareDirection -> CompareDirection #

Flip the direction of comparison.

dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c #

Turn a Comparison function into a CompareDirection function.

Property: dirToCmp f (fromCmp cmp) = f cmp

Open things

data Open a #

A thing tagged with the context it came from.

Constructors

OpenThing
Fields openThingCheckpoint :: CheckpointId openThing :: a

Instances

Functor Open #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fmap :: (a -> b) -> Open a -> Open b # (<$) :: a -> Open b -> Open a #
Foldable Open #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fold :: Monoid m => Open m -> m # foldMap :: Monoid m => (a -> m) -> Open a -> m # foldr :: (a -> b -> b) -> b -> Open a -> b # foldr' :: (a -> b -> b) -> b -> Open a -> b # foldl :: (b -> a -> b) -> b -> Open a -> b # foldl' :: (b -> a -> b) -> b -> Open a -> b # foldr1 :: (a -> a -> a) -> Open a -> a # foldl1 :: (a -> a -> a) -> Open a -> a # toList :: Open a -> [a] # null :: Open a -> Bool # length :: Open a -> Int # elem :: Eq a => a -> Open a -> Bool # maximum :: Ord a => Open a -> a # minimum :: Ord a => Open a -> a # sum :: Num a => Open a -> a # product :: Num a => Open a -> a #
Traversable Open #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods traverse :: Applicative f => (a -> f b) -> Open a -> f (Open b) # sequenceA :: Applicative f => Open (f a) -> f (Open a) # mapM :: Monad m => (a -> m b) -> Open a -> m (Open b) # sequence :: Monad m => Open (m a) -> m (Open a) #
Decoration Open #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods traverseF :: Functor m => (a -> m b) -> Open a -> m (Open b) # distributeF :: Functor m => Open (m a) -> m (Open a) #
Data a => Data (Open a) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Open a -> c (Open a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Open a) # toConstr :: Open a -> Constr # dataTypeOf :: Open a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Open a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Open a)) # gmapT :: (forall b. Data b => b -> b) -> Open a -> Open a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Open a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Open a -> r # gmapQ :: (forall d. Data d => d -> u) -> Open a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Open a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Open a -> m (Open a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Open a -> m (Open a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Open a -> m (Open a) #
Show a => Show (Open a) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Open a -> ShowS # show :: Open a -> String # showList :: [Open a] -> ShowS #
KillRange a => KillRange (Open a) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT (Open a) #
EmbPrj a => EmbPrj (Open a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Open a -> S Int32 # icod_ :: Open a -> S Int32 # value :: Int32 -> R (Open a) #
NamesIn a => NamesIn (Open a) #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Open a -> Set QName #
InstantiateFull a => InstantiateFull (Open a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Open a -> ReduceM (Open a) #

Judgements

data Judgement a #

Parametrized since it is used without MetaId when creating a new meta.

Constructors

HasType
Fields jMetaId :: a jMetaType :: Type
IsSort
Fields jMetaId :: a jMetaType :: Type

Instances

Show a => Show (Judgement a) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Judgement a -> ShowS # show :: Judgement a -> String # showList :: [Judgement a] -> ShowS #
PrettyTCM a => PrettyTCM (Judgement a) #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Judgement a -> TCM Doc #

Meta variables

data MetaVariable #

Constructors

MetaVar

Fields

mvInfo :: MetaInfo
mvPriority :: MetaPriority
some metavariables are more eager to be instantiated
mvPermutation :: Permutation
a metavariable doesn't have to depend on all variables in the context, this "permutation" will throw away the ones it does not depend on
mvJudgement :: Judgement MetaId
mvInstantiation :: MetaInstantiation
mvListeners :: Set Listener
meta variables scheduled for eta-expansion but blocked by this one
mvFrozen :: Frozen
are we past the point where we can instantiate this meta variable?

Instances

SetRange MetaVariable #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods setRange :: Range -> MetaVariable -> MetaVariable #
HasRange MetaVariable #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: MetaVariable -> Range #

data Listener #

Constructors

EtaExpand MetaId
CheckConstraint Nat ProblemConstraint

Instances

Eq Listener #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: Listener -> Listener -> Bool # (/=) :: Listener -> Listener -> Bool #
Ord Listener #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods compare :: Listener -> Listener -> Ordering # (<) :: Listener -> Listener -> Bool # (<=) :: Listener -> Listener -> Bool # (>) :: Listener -> Listener -> Bool # (>=) :: Listener -> Listener -> Bool # max :: Listener -> Listener -> Listener # min :: Listener -> Listener -> Listener #

data Frozen #

Frozen meta variable cannot be instantiated by unification. This serves to prevent the completion of a definition by its use outside of the current block. (See issues 118, 288, 399).

Constructors

Frozen	Do not instantiate.
Instantiable

Instances

Eq Frozen #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: Frozen -> Frozen -> Bool # (/=) :: Frozen -> Frozen -> Bool #
Show Frozen #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Frozen -> ShowS # show :: Frozen -> String # showList :: [Frozen] -> ShowS #

data MetaInstantiation #

Constructors

InstV [Arg String] Term	solved by term (abstracted over some free variables)
Open	unsolved
OpenIFS	open, to be instantiated as "implicit from scope"
BlockedConst Term	solution blocked by unsolved constraints
PostponedTypeCheckingProblem (Closure TypeCheckingProblem) (TCM Bool)

Instances

Show MetaInstantiation #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> MetaInstantiation -> ShowS # show :: MetaInstantiation -> String # showList :: [MetaInstantiation] -> ShowS #

data CheckedTarget #

Solving a CheckArgs constraint may or may not check the target type. If it did, it returns a handle to any unsolved constraints.

Constructors

CheckedTarget (Maybe ProblemId)
NotCheckedTarget

data TypeCheckingProblem #

Constructors

CheckExpr Expr Type
CheckArgs ExpandHidden Range [NamedArg Expr] Type Type (Elims -> Type -> CheckedTarget -> TCM Term)
CheckLambda (Arg ([WithHiding Name], Maybe Type)) Expr Type	`(λ (xs : t₀) → e) : t` This is not an instance of `CheckExpr` as the domain type has already been checked. For example, when checking `(λ (x y : Fin _) → e) : (x : Fin n) → ?` we want to postpone `(λ (y : Fin n) → e) : ?` where `Fin n` is a `Type` rather than an `Expr`.
UnquoteTactic Term Term Type	First argument is computation and the others are hole and goal type

Instances

PrettyTCM TypeCheckingProblem #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: TypeCheckingProblem -> TCM Doc #

newtype MetaPriority #

Meta variable priority: When we have an equation between meta-variables, which one should be instantiated?

Higher value means higher priority to be instantiated.

Constructors

MetaPriority Int

Instances

Eq MetaPriority #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: MetaPriority -> MetaPriority -> Bool # (/=) :: MetaPriority -> MetaPriority -> Bool #
Ord MetaPriority #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods compare :: MetaPriority -> MetaPriority -> Ordering # (<) :: MetaPriority -> MetaPriority -> Bool # (<=) :: MetaPriority -> MetaPriority -> Bool # (>) :: MetaPriority -> MetaPriority -> Bool # (>=) :: MetaPriority -> MetaPriority -> Bool # max :: MetaPriority -> MetaPriority -> MetaPriority # min :: MetaPriority -> MetaPriority -> MetaPriority #
Show MetaPriority #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> MetaPriority -> ShowS # show :: MetaPriority -> String # showList :: [MetaPriority] -> ShowS #

data RunMetaOccursCheck #

Constructors

RunMetaOccursCheck
DontRunMetaOccursCheck

Instances

Eq RunMetaOccursCheck #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool # (/=) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool #
Ord RunMetaOccursCheck #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods compare :: RunMetaOccursCheck -> RunMetaOccursCheck -> Ordering # (<) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool # (<=) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool # (>) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool # (>=) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool # max :: RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck # min :: RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck #
Show RunMetaOccursCheck #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> RunMetaOccursCheck -> ShowS # show :: RunMetaOccursCheck -> String # showList :: [RunMetaOccursCheck] -> ShowS #

data MetaInfo #

MetaInfo is cloned from one meta to the next during pruning.

Constructors

MetaInfo
Fields miClosRange :: Closure Range miMetaOccursCheck :: RunMetaOccursCheck Run the extended occurs check that goes in definitions? miNameSuggestion :: MetaNameSuggestion Used for printing. `Just x` if meta-variable comes from omitted argument with name `x`.

Instances

SetRange MetaInfo #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods setRange :: Range -> MetaInfo -> MetaInfo #
HasRange MetaInfo #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: MetaInfo -> Range #

type MetaNameSuggestion = String #

Name suggestion for meta variable. Empty string means no suggestion.

data NamedMeta #

For printing, we couple a meta with its name suggestion.

Constructors

NamedMeta
Fields nmSuggestion :: MetaNameSuggestion nmid :: MetaId

Instances

Pretty NamedMeta #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: NamedMeta -> Doc # prettyPrec :: Int -> NamedMeta -> Doc # prettyList :: [NamedMeta] -> Doc #
ToConcrete NamedMeta Expr #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: NamedMeta -> AbsToCon Expr # bindToConcrete :: NamedMeta -> (Expr -> AbsToCon b) -> AbsToCon b #

type MetaStore = Map MetaId MetaVariable #

normalMetaPriority :: MetaPriority #

lowMetaPriority :: MetaPriority #

highMetaPriority :: MetaPriority #

getMetaInfo :: MetaVariable -> Closure Range #

getMetaScope :: MetaVariable -> ScopeInfo #

getMetaEnv :: MetaVariable -> TCEnv #

getMetaSig :: MetaVariable -> Signature #

getMetaRelevance :: MetaVariable -> Relevance #

Interaction meta variables

data InteractionPoint #

Interaction points are created by the scope checker who sets the range. The meta variable is created by the type checker and then hooked up to the interaction point.

Constructors

InteractionPoint
Fields ipRange :: Range The position of the interaction point. ipMeta :: Maybe MetaId The meta variable, if any, holding the type etc. ipSolved :: Bool Has this interaction point already been solved? ipClause :: IPClause The clause of the interaction point (if any). Used for case splitting.

Instances

Eq InteractionPoint #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: InteractionPoint -> InteractionPoint -> Bool # (/=) :: InteractionPoint -> InteractionPoint -> Bool #

type InteractionPoints = Map InteractionId InteractionPoint #

Data structure managing the interaction points.

We never remove interaction points from this map, only set their ipSolved to True. (Issue #2368)

data IPClause #

Which clause is an interaction point located in?

Constructors

IPClause
Fields ipcQName :: QName The name of the function. ipcClauseNo :: Int The number of the clause of this function. ipcClause :: RHS The original AST clause rhs.
IPNoClause	The interaction point is not in the rhs of a clause.

Instances

Eq IPClause #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: IPClause -> IPClause -> Bool # (/=) :: IPClause -> IPClause -> Bool #
Data IPClause #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IPClause -> c IPClause # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IPClause # toConstr :: IPClause -> Constr # dataTypeOf :: IPClause -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IPClause) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IPClause) # gmapT :: (forall b. Data b => b -> b) -> IPClause -> IPClause # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IPClause -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IPClause -> r # gmapQ :: (forall d. Data d => d -> u) -> IPClause -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> IPClause -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> IPClause -> m IPClause # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IPClause -> m IPClause # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IPClause -> m IPClause #

Signature

data Signature #

Constructors

Sig
Fields _sigSections :: Sections _sigDefinitions :: Definitions _sigRewriteRules :: RewriteRuleMap The rewrite rules defined in this file.

Instances

Data Signature #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Signature -> c Signature # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Signature # toConstr :: Signature -> Constr # dataTypeOf :: Signature -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Signature) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Signature) # gmapT :: (forall b. Data b => b -> b) -> Signature -> Signature # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Signature -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Signature -> r # gmapQ :: (forall d. Data d => d -> u) -> Signature -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Signature -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Signature -> m Signature # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Signature -> m Signature # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Signature -> m Signature #
Show Signature #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Signature -> ShowS # show :: Signature -> String # showList :: [Signature] -> ShowS #
KillRange Signature #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Signature #
EmbPrj Signature #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Signature -> S Int32 # icod_ :: Signature -> S Int32 # value :: Int32 -> R Signature #
InstantiateFull Signature #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Signature -> ReduceM Signature #

sigSections :: Lens' Sections Signature #

sigDefinitions :: Lens' Definitions Signature #

sigRewriteRules :: Lens' RewriteRuleMap Signature #

type Sections = Map ModuleName Section #

type Definitions = HashMap QName Definition #

type RewriteRuleMap = HashMap QName RewriteRules #

type DisplayForms = HashMap QName [LocalDisplayForm] #

newtype Section #

Constructors

Section
Fields _secTelescope :: Telescope

Instances

Eq Section #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Section -> Section -> Bool # (/=) :: Section -> Section -> Bool #
Data Section #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Section -> c Section # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Section # toConstr :: Section -> Constr # dataTypeOf :: Section -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Section) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Section) # gmapT :: (forall b. Data b => b -> b) -> Section -> Section # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Section -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Section -> r # gmapQ :: (forall d. Data d => d -> u) -> Section -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Section -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Section -> m Section # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Section -> m Section # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Section -> m Section #
Show Section #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Section -> ShowS # show :: Section -> String # showList :: [Section] -> ShowS #
Pretty Section #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Section -> Doc # prettyPrec :: Int -> Section -> Doc # prettyList :: [Section] -> Doc #
KillRange Section #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Section #
KillRange Sections #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Sections #
EmbPrj Section #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Section -> S Int32 # icod_ :: Section -> S Int32 # value :: Int32 -> R Section #
InstantiateFull Section #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Section -> ReduceM Section #

secTelescope :: Lens' Telescope Section #

emptySignature :: Signature #

data DisplayForm #

A DisplayForm is in essence a rewrite rule q ts --> dt for a defined symbol (could be a constructor as well) q. The right hand side is a DisplayTerm which is used to reify to a more readable Syntax.

The patterns ts are just terms, but var 0 is interpreted as a hole. Each occurrence of var 0 is a new hole (pattern var). For each *occurrence* of var0 the rhs dt has a free variable. These are instantiated when matching a display form against a term q vs succeeds.

Constructors

Display
Fields dfFreeVars :: Nat Number `n` of free variables in `dfRHS`. dfPats :: Elims Left hand side patterns, where `var 0` stands for a pattern variable. There should be `n` occurrences of `var0` in `dfPats`. The `ArgInfo` is ignored in these patterns. dfRHS :: DisplayTerm Right hand side, with `n` free variables.

Instances

Data DisplayForm #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DisplayForm -> c DisplayForm # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DisplayForm # toConstr :: DisplayForm -> Constr # dataTypeOf :: DisplayForm -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DisplayForm) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DisplayForm) # gmapT :: (forall b. Data b => b -> b) -> DisplayForm -> DisplayForm # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DisplayForm -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DisplayForm -> r # gmapQ :: (forall d. Data d => d -> u) -> DisplayForm -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DisplayForm -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DisplayForm -> m DisplayForm # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DisplayForm -> m DisplayForm # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DisplayForm -> m DisplayForm #
Show DisplayForm #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> DisplayForm -> ShowS # show :: DisplayForm -> String # showList :: [DisplayForm] -> ShowS #
KillRange DisplayForm #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT DisplayForm #
Free DisplayForm #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet c => DisplayForm -> FreeM c #
EmbPrj DisplayForm #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DisplayForm -> S Int32 # icod_ :: DisplayForm -> S Int32 # value :: Int32 -> R DisplayForm #
NamesIn DisplayForm #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: DisplayForm -> Set QName #
InstantiateFull DisplayForm #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: DisplayForm -> ReduceM DisplayForm #
Normalise DisplayForm #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: DisplayForm -> ReduceM DisplayForm #
Simplify DisplayForm #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: DisplayForm -> ReduceM DisplayForm #
Subst Term DisplayForm #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> DisplayForm -> DisplayForm #

type LocalDisplayForm = Open DisplayForm #

data DisplayTerm #

A structured presentation of a Term for reification into Syntax.

Constructors

DWithApp DisplayTerm [DisplayTerm] Elims	`(f vs \| ws) es`. The first `DisplayTerm` is the parent function `f` with its args `vs`. The list of `DisplayTerm`s are the with expressions `ws`. The `Elims` are additional arguments `es` (possible in case the with-application is of function type) or projections (if it is of record type).
DCon ConHead ConInfo [Arg DisplayTerm]	`c vs`.
DDef QName [Elim' DisplayTerm]	`d vs`.
DDot Term	`.v`.
DTerm Term	`v`.

Instances

Data DisplayTerm #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DisplayTerm -> c DisplayTerm # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DisplayTerm # toConstr :: DisplayTerm -> Constr # dataTypeOf :: DisplayTerm -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DisplayTerm) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DisplayTerm) # gmapT :: (forall b. Data b => b -> b) -> DisplayTerm -> DisplayTerm # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DisplayTerm -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DisplayTerm -> r # gmapQ :: (forall d. Data d => d -> u) -> DisplayTerm -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DisplayTerm -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DisplayTerm -> m DisplayTerm # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DisplayTerm -> m DisplayTerm # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DisplayTerm -> m DisplayTerm #
Show DisplayTerm #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> DisplayTerm -> ShowS # show :: DisplayTerm -> String # showList :: [DisplayTerm] -> ShowS #
Pretty DisplayTerm #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: DisplayTerm -> Doc # prettyPrec :: Int -> DisplayTerm -> Doc # prettyList :: [DisplayTerm] -> Doc #
KillRange DisplayTerm #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT DisplayTerm #
Free DisplayTerm #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet c => DisplayTerm -> FreeM c #
Apply DisplayTerm #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: DisplayTerm -> Args -> DisplayTerm # applyE :: DisplayTerm -> Elims -> DisplayTerm #
EmbPrj DisplayTerm #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DisplayTerm -> S Int32 # icod_ :: DisplayTerm -> S Int32 # value :: Int32 -> R DisplayTerm #
PrettyTCM DisplayTerm #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: DisplayTerm -> TCM Doc #
NamesIn DisplayTerm #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: DisplayTerm -> Set QName #
InstantiateFull DisplayTerm #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: DisplayTerm -> ReduceM DisplayTerm #
SubstWithOrigin DisplayTerm #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> DisplayTerm -> DisplayTerm #
Subst Term DisplayTerm #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> DisplayTerm -> DisplayTerm #
Reify DisplayTerm Expr #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: DisplayTerm -> TCM Expr # reifyWhen :: Bool -> DisplayTerm -> TCM Expr #
PrettyTCM (Elim' DisplayTerm) #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Elim' DisplayTerm -> TCM Doc #
SubstWithOrigin (Arg DisplayTerm) #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> Arg DisplayTerm -> Arg DisplayTerm #

defaultDisplayForm :: QName -> [LocalDisplayForm] #

By default, we have no display form.

defRelevance :: Definition -> Relevance #

data NLPat #

Non-linear (non-constructor) first-order pattern.

Constructors

PVar !Int [Arg Int]	Matches anything (modulo non-linearity) that only contains bound variables that occur in the given arguments.
PWild	Matches anything (e.g. irrelevant terms).
PDef QName PElims	Matches `f es`
PLam ArgInfo (Abs NLPat)	Matches `λ x → t`
PPi (Dom NLPType) (Abs NLPType)	Matches `(x : A) → B`
PBoundVar !Int PElims	Matches `x es` where x is a lambda-bound variable
PTerm Term	Matches the term modulo β (ideally βη).

Instances

Data NLPat #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NLPat -> c NLPat # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NLPat # toConstr :: NLPat -> Constr # dataTypeOf :: NLPat -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NLPat) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NLPat) # gmapT :: (forall b. Data b => b -> b) -> NLPat -> NLPat # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NLPat -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NLPat -> r # gmapQ :: (forall d. Data d => d -> u) -> NLPat -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> NLPat -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> NLPat -> m NLPat # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NLPat -> m NLPat # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NLPat -> m NLPat #
Show NLPat #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> NLPat -> ShowS # show :: NLPat -> String # showList :: [NLPat] -> ShowS #
KillRange NLPat #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT NLPat #
DeBruijn NLPat #
Instance details Defined in Agda.TypeChecking.Substitute Methods deBruijnVar :: Int -> NLPat # debruijnNamedVar :: String -> Int -> NLPat # deBruijnView :: NLPat -> Maybe Int #
Free NLPat #
Instance details Defined in Agda.TypeChecking.Rewriting Methods freeVars' :: IsVarSet c => NLPat -> FreeM c #
EmbPrj NLPat #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NLPat -> S Int32 # icod_ :: NLPat -> S Int32 # value :: Int32 -> R NLPat #
PrettyTCM NLPat #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: NLPat -> TCM Doc #
InstantiateFull NLPat #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: NLPat -> ReduceM NLPat #
GetMatchables NLPat #
Instance details Defined in Agda.TypeChecking.Rewriting Methods getMatchables :: NLPat -> [QName] #
NLPatVars NLPat #
Instance details Defined in Agda.TypeChecking.Rewriting Methods nlPatVarsUnder :: Int -> NLPat -> IntSet # nlPatVars :: NLPat -> IntSet #
Subst NLPat RewriteRule #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' NLPat -> RewriteRule -> RewriteRule #
Subst NLPat NLPType #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' NLPat -> NLPType -> NLPType #
Subst NLPat NLPat #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' NLPat -> NLPat -> NLPat #
Match NLPat Level #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> NLPat -> Level -> NLM () #
Match NLPat Sort #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> NLPat -> Sort -> NLM () #
Match NLPat Term #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> NLPat -> Term -> NLM () #
PatternFrom Sort NLPat #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> Sort -> TCM NLPat #
PatternFrom Term NLPat #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> Term -> TCM NLPat #
PrettyTCM (Type' NLPat) #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Type' NLPat -> TCM Doc #
PrettyTCM (Elim' NLPat) #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Elim' NLPat -> TCM Doc #
PatternFrom a NLPat => PatternFrom (Elim' a) (Elim' NLPat) #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> Elim' a -> TCM (Elim' NLPat) #

type PElims = [Elim' NLPat] #

data NLPType #

Constructors

NLPType
Fields nlpTypeLevel :: NLPat nlpTypeUnEl :: NLPat

Instances

Data NLPType #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NLPType -> c NLPType # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NLPType # toConstr :: NLPType -> Constr # dataTypeOf :: NLPType -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NLPType) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NLPType) # gmapT :: (forall b. Data b => b -> b) -> NLPType -> NLPType # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NLPType -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NLPType -> r # gmapQ :: (forall d. Data d => d -> u) -> NLPType -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> NLPType -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> NLPType -> m NLPType # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NLPType -> m NLPType # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NLPType -> m NLPType #
Show NLPType #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> NLPType -> ShowS # show :: NLPType -> String # showList :: [NLPType] -> ShowS #
KillRange NLPType #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT NLPType #
Free NLPType #
Instance details Defined in Agda.TypeChecking.Rewriting Methods freeVars' :: IsVarSet c => NLPType -> FreeM c #
EmbPrj NLPType #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NLPType -> S Int32 # icod_ :: NLPType -> S Int32 # value :: Int32 -> R NLPType #
PrettyTCM NLPType #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: NLPType -> TCM Doc #
InstantiateFull NLPType #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: NLPType -> ReduceM NLPType #
NLPatVars NLPType #
Instance details Defined in Agda.TypeChecking.Rewriting Methods nlPatVarsUnder :: Int -> NLPType -> IntSet # nlPatVars :: NLPType -> IntSet #
Subst NLPat NLPType #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' NLPat -> NLPType -> NLPType #
Match NLPType Type #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> NLPType -> Type -> NLM () #
PatternFrom Type NLPType #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods patternFrom :: Relevance -> Int -> Type -> TCM NLPType #

type RewriteRules = [RewriteRule] #

data RewriteRule #

Rewrite rules can be added independently from function clauses.

Constructors

RewriteRule
Fields rewName :: QName Name of rewrite rule `q : Γ → f ps ≡ rhs` where `≡` is the rewrite relation. rewContext :: Telescope `Γ`. rewHead :: QName `f`. rewPats :: PElims `Γ ⊢ f ps : t`. rewRHS :: Term `Γ ⊢ rhs : t`. rewType :: Type `Γ ⊢ t`.

Instances

Data RewriteRule #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RewriteRule -> c RewriteRule # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RewriteRule # toConstr :: RewriteRule -> Constr # dataTypeOf :: RewriteRule -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RewriteRule) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RewriteRule) # gmapT :: (forall b. Data b => b -> b) -> RewriteRule -> RewriteRule # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RewriteRule -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RewriteRule -> r # gmapQ :: (forall d. Data d => d -> u) -> RewriteRule -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RewriteRule -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RewriteRule -> m RewriteRule # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RewriteRule -> m RewriteRule # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RewriteRule -> m RewriteRule #
Show RewriteRule #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> RewriteRule -> ShowS # show :: RewriteRule -> String # showList :: [RewriteRule] -> ShowS #
KillRange RewriteRule #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT RewriteRule #
KillRange RewriteRuleMap #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT RewriteRuleMap #
Abstract RewriteRule #	`tel ⊢ (Γ ⊢ lhs ↦ rhs : t)` becomes `tel, Γ ⊢ lhs ↦ rhs : t)` we do not need to change lhs, rhs, and t since they live in Γ. See 'Abstract Clause'.
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> RewriteRule -> RewriteRule #
Apply RewriteRule #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: RewriteRule -> Args -> RewriteRule # applyE :: RewriteRule -> Elims -> RewriteRule #
EmbPrj RewriteRule #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: RewriteRule -> S Int32 # icod_ :: RewriteRule -> S Int32 # value :: Int32 -> R RewriteRule #
PrettyTCM RewriteRule #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: RewriteRule -> TCM Doc #
InstantiateFull RewriteRule #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: RewriteRule -> ReduceM RewriteRule #
GetMatchables RewriteRule #
Instance details Defined in Agda.TypeChecking.Rewriting Methods getMatchables :: RewriteRule -> [QName] #
Subst NLPat RewriteRule #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' NLPat -> RewriteRule -> RewriteRule #

data Definition #

Constructors

Defn

Fields

defArgInfo :: ArgInfo
Hiding should not be used.
defName :: QName
defType :: Type
Type of the lifted definition.
defPolarity :: [Polarity]
Variance information on arguments of the definition. Does not include info for dropped parameters to projection(-like) functions and constructors.
defArgOccurrences :: [Occurrence]
Positivity information on arguments of the definition. Does not include info for dropped parameters to projection(-like) functions and constructors.
defDisplay :: [LocalDisplayForm]
defMutual :: MutualId
defCompiledRep :: CompiledRepresentation
defInstance :: Maybe QName
Just q when this definition is an instance of class q
defCopy :: Bool
Has this function been created by a module instantiation?
defMatchable :: Bool
Is the def matched against in a rewrite rule?
defInjective :: Bool
Should the def be treated as injective by the pattern matching unifier?
theDef :: Defn

Instances

Data Definition #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Definition -> c Definition # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Definition # toConstr :: Definition -> Constr # dataTypeOf :: Definition -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Definition) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Definition) # gmapT :: (forall b. Data b => b -> b) -> Definition -> Definition # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Definition -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Definition -> r # gmapQ :: (forall d. Data d => d -> u) -> Definition -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Definition -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Definition -> m Definition # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Definition -> m Definition # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Definition -> m Definition #
Show Definition #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Definition -> ShowS # show :: Definition -> String # showList :: [Definition] -> ShowS #
Pretty Definition #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Definition -> Doc # prettyPrec :: Int -> Definition -> Doc # prettyList :: [Definition] -> Doc #
KillRange Definition #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Definition #
KillRange Definitions #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Definitions #
Abstract Definition #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Definition -> Definition #
Apply Definition #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Definition -> Args -> Definition # applyE :: Definition -> Elims -> Definition #
EmbPrj Definition #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Definition -> S Int32 # icod_ :: Definition -> S Int32 # value :: Int32 -> R Definition #
NamesIn Definition #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Definition -> Set QName #
InstantiateFull Definition #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Definition -> ReduceM Definition #

theDefLens :: Lens' Defn Definition #

defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition #

Create a definition with sensible defaults.

data Polarity #

Polarity for equality and subtype checking.

Constructors

Covariant	monotone
Contravariant	antitone
Invariant	no information (mixed variance)
Nonvariant	constant

Instances

Eq Polarity #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: Polarity -> Polarity -> Bool # (/=) :: Polarity -> Polarity -> Bool #
Data Polarity #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Polarity -> c Polarity # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Polarity # toConstr :: Polarity -> Constr # dataTypeOf :: Polarity -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Polarity) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Polarity) # gmapT :: (forall b. Data b => b -> b) -> Polarity -> Polarity # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Polarity -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Polarity -> r # gmapQ :: (forall d. Data d => d -> u) -> Polarity -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Polarity -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity #
Show Polarity #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Polarity -> ShowS # show :: Polarity -> String # showList :: [Polarity] -> ShowS #
Pretty Polarity #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Polarity -> Doc # prettyPrec :: Int -> Polarity -> Doc # prettyList :: [Polarity] -> Doc #
KillRange Polarity #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Polarity #
EmbPrj Polarity #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Polarity -> S Int32 # icod_ :: Polarity -> S Int32 # value :: Int32 -> R Polarity #
PrettyTCM Polarity #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Polarity -> TCM Doc #
Abstract [Polarity] #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> [Polarity] -> [Polarity] #
Apply [Polarity] #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: [Polarity] -> Args -> [Polarity] # applyE :: [Polarity] -> Elims -> [Polarity] #

data IsForced #

Information about whether an argument is forced by the type of a function.

Constructors

Forced
NotForced

Instances

Eq IsForced #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: IsForced -> IsForced -> Bool # (/=) :: IsForced -> IsForced -> Bool #
Data IsForced #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsForced -> c IsForced # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsForced # toConstr :: IsForced -> Constr # dataTypeOf :: IsForced -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsForced) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsForced) # gmapT :: (forall b. Data b => b -> b) -> IsForced -> IsForced # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsForced -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsForced -> r # gmapQ :: (forall d. Data d => d -> u) -> IsForced -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> IsForced -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsForced -> m IsForced # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsForced -> m IsForced # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsForced -> m IsForced #
Show IsForced #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> IsForced -> ShowS # show :: IsForced -> String # showList :: [IsForced] -> ShowS #
KillRange IsForced #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT IsForced #
EmbPrj IsForced #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: IsForced -> S Int32 # icod_ :: IsForced -> S Int32 # value :: Int32 -> R IsForced #
PrettyTCM IsForced #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: IsForced -> TCM Doc #

data CompilerPragma #

The backends are responsible for parsing their own pragmas.

Constructors

CompilerPragma Range String

Instances

Eq CompilerPragma #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: CompilerPragma -> CompilerPragma -> Bool # (/=) :: CompilerPragma -> CompilerPragma -> Bool #
Data CompilerPragma #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CompilerPragma -> c CompilerPragma # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CompilerPragma # toConstr :: CompilerPragma -> Constr # dataTypeOf :: CompilerPragma -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CompilerPragma) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CompilerPragma) # gmapT :: (forall b. Data b => b -> b) -> CompilerPragma -> CompilerPragma # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CompilerPragma -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CompilerPragma -> r # gmapQ :: (forall d. Data d => d -> u) -> CompilerPragma -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> CompilerPragma -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> CompilerPragma -> m CompilerPragma # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CompilerPragma -> m CompilerPragma # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CompilerPragma -> m CompilerPragma #
Show CompilerPragma #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> CompilerPragma -> ShowS # show :: CompilerPragma -> String # showList :: [CompilerPragma] -> ShowS #
KillRange CompiledRepresentation #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT CompiledRepresentation #
HasRange CompilerPragma #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: CompilerPragma -> Range #
EmbPrj CompilerPragma #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Compilers Methods icode :: CompilerPragma -> S Int32 # icod_ :: CompilerPragma -> S Int32 # value :: Int32 -> R CompilerPragma #

type BackendName = String #

jsBackendName :: BackendName #

ghcBackendName :: BackendName #

uhcBackendName :: BackendName #

type CompiledRepresentation = Map BackendName [CompilerPragma] #

noCompiledRep :: CompiledRepresentation #

data ExtLamInfo #

Additional information for extended lambdas.

Constructors

ExtLamInfo
Fields extLamModule :: ModuleName For complicated reasons the scope checker decides the QName of a pattern lambda, and thus its module. We really need to decide the module during type checking though, since if the lambda appears in a refined context the module picked by the scope checker has very much the wrong parameters.

Instances

Eq ExtLamInfo #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: ExtLamInfo -> ExtLamInfo -> Bool # (/=) :: ExtLamInfo -> ExtLamInfo -> Bool #
Data ExtLamInfo #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExtLamInfo -> c ExtLamInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExtLamInfo # toConstr :: ExtLamInfo -> Constr # dataTypeOf :: ExtLamInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExtLamInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExtLamInfo) # gmapT :: (forall b. Data b => b -> b) -> ExtLamInfo -> ExtLamInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExtLamInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExtLamInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> ExtLamInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ExtLamInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExtLamInfo -> m ExtLamInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExtLamInfo -> m ExtLamInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExtLamInfo -> m ExtLamInfo #
Ord ExtLamInfo #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods compare :: ExtLamInfo -> ExtLamInfo -> Ordering # (<) :: ExtLamInfo -> ExtLamInfo -> Bool # (<=) :: ExtLamInfo -> ExtLamInfo -> Bool # (>) :: ExtLamInfo -> ExtLamInfo -> Bool # (>=) :: ExtLamInfo -> ExtLamInfo -> Bool # max :: ExtLamInfo -> ExtLamInfo -> ExtLamInfo # min :: ExtLamInfo -> ExtLamInfo -> ExtLamInfo #
Show ExtLamInfo #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> ExtLamInfo -> ShowS # show :: ExtLamInfo -> String # showList :: [ExtLamInfo] -> ShowS #
KillRange ExtLamInfo #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT ExtLamInfo #
EmbPrj ExtLamInfo #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ExtLamInfo -> S Int32 # icod_ :: ExtLamInfo -> S Int32 # value :: Int32 -> R ExtLamInfo #

data Projection #

Additional information for projection Functions.

Constructors

Projection

Fields

projProper :: Maybe QName
Nothing if only projection-like, Just r if record projection. The r is the name of the record type projected from. This field is updated by module application.
projOrig :: QName
The original projection name (current name could be from module application).
projFromType :: Arg QName
Type projected from. Original record type if projProper = Just{}. Also stores ArgInfo of the principal argument. This field is unchanged by module application.
projIndex :: Int
Index of the record argument. Start counting with 1, because 0 means that it is already applied to the record value. This can happen in module instantiation, but then either the record value is var 0, or funProjection == Nothing.
projLams :: ProjLams
Term t to be be applied to record parameters and record value. The parameters will be dropped. In case of a proper projection, a postfix projection application will be created: t = pars r -> r .p (Invariant: the number of abstractions equals projIndex.) In case of a projection-like function, just the function symbol is returned as Def: t = pars -> f.

Instances

Data Projection #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Projection -> c Projection # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Projection # toConstr :: Projection -> Constr # dataTypeOf :: Projection -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Projection) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Projection) # gmapT :: (forall b. Data b => b -> b) -> Projection -> Projection # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Projection -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Projection -> r # gmapQ :: (forall d. Data d => d -> u) -> Projection -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Projection -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Projection -> m Projection # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Projection -> m Projection # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Projection -> m Projection #
Show Projection #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Projection -> ShowS # show :: Projection -> String # showList :: [Projection] -> ShowS #
KillRange Projection #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Projection #
Abstract Projection #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Projection -> Projection #
Apply Projection #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Projection -> Args -> Projection # applyE :: Projection -> Elims -> Projection #
EmbPrj Projection #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Projection -> S Int32 # icod_ :: Projection -> S Int32 # value :: Int32 -> R Projection #

newtype ProjLams #

Abstractions to build projection function (dropping parameters).

Constructors

ProjLams
Fields getProjLams :: [Arg ArgName]

Instances

Data ProjLams #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProjLams -> c ProjLams # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProjLams # toConstr :: ProjLams -> Constr # dataTypeOf :: ProjLams -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProjLams) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProjLams) # gmapT :: (forall b. Data b => b -> b) -> ProjLams -> ProjLams # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProjLams -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProjLams -> r # gmapQ :: (forall d. Data d => d -> u) -> ProjLams -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ProjLams -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProjLams -> m ProjLams # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProjLams -> m ProjLams # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProjLams -> m ProjLams #
Show ProjLams #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> ProjLams -> ShowS # show :: ProjLams -> String # showList :: [ProjLams] -> ShowS #
Null ProjLams #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: ProjLams # null :: ProjLams -> Bool #
KillRange ProjLams #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT ProjLams #
Abstract ProjLams #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> ProjLams -> ProjLams #
Apply ProjLams #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: ProjLams -> Args -> ProjLams # applyE :: ProjLams -> Elims -> ProjLams #
EmbPrj ProjLams #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ProjLams -> S Int32 # icod_ :: ProjLams -> S Int32 # value :: Int32 -> R ProjLams #

projDropPars :: Projection -> ProjOrigin -> Term #

Building the projection function (which drops the parameters).

projArgInfo :: Projection -> ArgInfo #

The info of the principal (record) argument.

data EtaEquality #

Should a record type admit eta-equality?

Constructors

Specified	User specifed 'eta-equality' or 'no-eta-equality'.
Fields theEtaEquality :: !HasEta
Inferred	Positivity checker inferred whether eta is safe.
Fields theEtaEquality :: !HasEta

Instances

Eq EtaEquality #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: EtaEquality -> EtaEquality -> Bool # (/=) :: EtaEquality -> EtaEquality -> Bool #
Data EtaEquality #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EtaEquality -> c EtaEquality # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EtaEquality # toConstr :: EtaEquality -> Constr # dataTypeOf :: EtaEquality -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EtaEquality) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EtaEquality) # gmapT :: (forall b. Data b => b -> b) -> EtaEquality -> EtaEquality # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EtaEquality -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EtaEquality -> r # gmapQ :: (forall d. Data d => d -> u) -> EtaEquality -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> EtaEquality -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> EtaEquality -> m EtaEquality # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EtaEquality -> m EtaEquality # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EtaEquality -> m EtaEquality #
Show EtaEquality #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> EtaEquality -> ShowS # show :: EtaEquality -> String # showList :: [EtaEquality] -> ShowS #
KillRange EtaEquality #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT EtaEquality #
EmbPrj EtaEquality #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: EtaEquality -> S Int32 # icod_ :: EtaEquality -> S Int32 # value :: Int32 -> R EtaEquality #

setEtaEquality :: EtaEquality -> HasEta -> EtaEquality #

Make sure we do not overwrite a user specification.

data FunctionFlag #

Constructors

FunStatic	Should calls to this function be normalised at compile-time?
FunInline	Should calls to this function be inlined by the compiler?
FunMacro	Is this function a macro?

Instances

Enum FunctionFlag #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods succ :: FunctionFlag -> FunctionFlag # pred :: FunctionFlag -> FunctionFlag # toEnum :: Int -> FunctionFlag # fromEnum :: FunctionFlag -> Int # enumFrom :: FunctionFlag -> [FunctionFlag] # enumFromThen :: FunctionFlag -> FunctionFlag -> [FunctionFlag] # enumFromTo :: FunctionFlag -> FunctionFlag -> [FunctionFlag] # enumFromThenTo :: FunctionFlag -> FunctionFlag -> FunctionFlag -> [FunctionFlag] #
Eq FunctionFlag #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: FunctionFlag -> FunctionFlag -> Bool # (/=) :: FunctionFlag -> FunctionFlag -> Bool #
Data FunctionFlag #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FunctionFlag -> c FunctionFlag # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FunctionFlag # toConstr :: FunctionFlag -> Constr # dataTypeOf :: FunctionFlag -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FunctionFlag) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunctionFlag) # gmapT :: (forall b. Data b => b -> b) -> FunctionFlag -> FunctionFlag # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunctionFlag -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunctionFlag -> r # gmapQ :: (forall d. Data d => d -> u) -> FunctionFlag -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> FunctionFlag -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> FunctionFlag -> m FunctionFlag # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FunctionFlag -> m FunctionFlag # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FunctionFlag -> m FunctionFlag #
Ord FunctionFlag #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods compare :: FunctionFlag -> FunctionFlag -> Ordering # (<) :: FunctionFlag -> FunctionFlag -> Bool # (<=) :: FunctionFlag -> FunctionFlag -> Bool # (>) :: FunctionFlag -> FunctionFlag -> Bool # (>=) :: FunctionFlag -> FunctionFlag -> Bool # max :: FunctionFlag -> FunctionFlag -> FunctionFlag # min :: FunctionFlag -> FunctionFlag -> FunctionFlag #
Show FunctionFlag #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> FunctionFlag -> ShowS # show :: FunctionFlag -> String # showList :: [FunctionFlag] -> ShowS #
KillRange FunctionFlag #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT FunctionFlag #
EmbPrj FunctionFlag #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: FunctionFlag -> S Int32 # icod_ :: FunctionFlag -> S Int32 # value :: Int32 -> R FunctionFlag #

data Defn #

Constructors

Axiom	Postulate.
AbstractDefn Defn	Returned by `getConstInfo` if definition is abstract.
Function
Fields funClauses :: [Clause] funCompiled :: Maybe CompiledClauses `Nothing` while function is still type-checked. `Just cc` after type and coverage checking and translation to case trees. funTreeless :: Maybe Compiled Intermediate representation for compiler backends. funInv :: FunctionInverse funMutual :: Maybe [QName] Mutually recursive functions, `data`s and `record`s. Does include this function. Empty list if not recursive. `Nothing` if not yet computed (by positivity checker). funAbstr :: IsAbstract funDelayed :: Delayed Are the clauses of this definition delayed? funProjection :: Maybe Projection Is it a record projection? If yes, then return the name of the record type and index of the record argument. Start counting with 1, because 0 means that it is already applied to the record. (Can happen in module instantiation.) This information is used in the termination checker. funFlags :: Set FunctionFlag funTerminates :: Maybe Bool Has this function been termination checked? Did it pass? funExtLam :: Maybe ExtLamInfo Is this function generated from an extended lambda? If yes, then return the number of hidden and non-hidden lambda-lifted arguments funWith :: Maybe QName Is this a generated with-function? If yes, then what's the name of the parent function. funCopatternLHS :: Bool Is this a function defined by copatterns?
Datatype
Fields dataPars :: Nat Number of parameters. dataIxs :: Nat Number of indices. dataInduction :: Induction `data` or `codata` (legacy). dataClause :: Maybe Clause This might be in an instantiated module. dataCons :: [QName] Constructor names. dataSort :: Sort dataMutual :: Maybe [QName] Mutually recursive functions, `data`s and `record`s. Does include this data type. Empty if not recursive. `Nothing` if not yet computed (by positivity checker). dataAbstr :: IsAbstract
Record
Fields recPars :: Nat Number of parameters. recClause :: Maybe Clause Was this record type created by a module application? If yes, the clause is its definition (linking back to the original record type). recConHead :: ConHead Constructor name and fields. recNamedCon :: Bool Does this record have a `constructor`? recFields :: [Arg QName] The record field names. recTel :: Telescope The record field telescope. (Includes record parameters.) Note: `TelV recTel _ == telView' recConType`. Thus, `recTel` is redundant. recMutual :: Maybe [QName] Mutually recursive functions, `data`s and `record`s. Does include this record. Empty if not recursive. `Nothing` if not yet computed (by positivity checker). recEtaEquality' :: EtaEquality Eta-expand at this record type? `False` for unguarded recursive records and coinductive records unless the user specifies otherwise. recInduction :: Maybe Induction `Inductive` or `CoInductive`? Matters only for recursive records. `Nothing` means that the user did not specify it, which is an error for recursive records. recAbstr :: IsAbstract
Constructor
Fields conPars :: Int Number of parameters. conArity :: Int Number of arguments (excluding parameters). conSrcCon :: ConHead Name of (original) constructor and fields. (This might be in a module instance.) conData :: QName Name of datatype or record type. conAbstr :: IsAbstract conInd :: Induction Inductive or coinductive? conForced :: [IsForced] Which arguments are forced (i.e. determined by the type of the constructor)? conErased :: [Bool] Which arguments are erased at runtime (computed during compilation to treeless)
Primitive	Primitive or builtin functions.
Fields primAbstr :: IsAbstract primName :: String primClauses :: [Clause] `null` for primitive functions, `not null` for builtin functions. primInv :: FunctionInverse Builtin functions can have inverses. For instance, natural number addition. primCompiled :: Maybe CompiledClauses `Nothing` for primitive functions, `Just something` for builtin functions.

Instances

Data Defn #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Defn -> c Defn # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Defn # toConstr :: Defn -> Constr # dataTypeOf :: Defn -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Defn) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn) # gmapT :: (forall b. Data b => b -> b) -> Defn -> Defn # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r # gmapQ :: (forall d. Data d => d -> u) -> Defn -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Defn -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Defn -> m Defn # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Defn -> m Defn # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Defn -> m Defn #
Show Defn #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Defn -> ShowS # show :: Defn -> String # showList :: [Defn] -> ShowS #
Pretty Defn #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Defn -> Doc # prettyPrec :: Int -> Defn -> Doc # prettyList :: [Defn] -> Doc #
KillRange Defn #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Defn #
Abstract Defn #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Defn -> Defn #
Apply Defn #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Defn -> Args -> Defn # applyE :: Defn -> Elims -> Defn #
EmbPrj Defn #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Defn -> S Int32 # icod_ :: Defn -> S Int32 # value :: Int32 -> R Defn #
NamesIn Defn #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Defn -> Set QName #
InstantiateFull Defn #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Defn -> ReduceM Defn #
Occurs Defn #
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Defn -> TCM Defn # metaOccurs :: MetaId -> Defn -> TCM () #

recRecursive :: Defn -> Bool #

Is the record type recursive?

recEtaEquality :: Defn -> HasEta #

emptyFunction :: Defn #

A template for creating Function definitions, with sensible defaults.

funFlag :: FunctionFlag -> Lens' Bool Defn #

funStatic :: Lens' Bool Defn #

funInline :: Lens' Bool Defn #

funMacro :: Lens' Bool Defn #

isMacro :: Defn -> Bool #

isEmptyFunction :: Defn -> Bool #

Checking whether we are dealing with a function yet to be defined.

isCopatternLHS :: [Clause] -> Bool #

recCon :: Defn -> QName #

defIsRecord :: Defn -> Bool #

defIsDataOrRecord :: Defn -> Bool #

defConstructors :: Defn -> [QName] #

newtype Fields #

Constructors

Fields [(Name, Type)]

Instances

Null Fields #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: Fields # null :: Fields -> Bool #

data Simplification #

Did we encounter a simplifying reduction? In terms of CIC, that would be a iota-reduction. In terms of Agda, this is a constructor or literal pattern that matched. Just beta-reduction (substitution) or delta-reduction (unfolding of definitions) does not count as simplifying?

Constructors

YesSimplification
NoSimplification

Instances

Eq Simplification #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: Simplification -> Simplification -> Bool # (/=) :: Simplification -> Simplification -> Bool #
Data Simplification #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Simplification -> c Simplification # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Simplification # toConstr :: Simplification -> Constr # dataTypeOf :: Simplification -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Simplification) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Simplification) # gmapT :: (forall b. Data b => b -> b) -> Simplification -> Simplification # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Simplification -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Simplification -> r # gmapQ :: (forall d. Data d => d -> u) -> Simplification -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Simplification -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Simplification -> m Simplification # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Simplification -> m Simplification # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Simplification -> m Simplification #
Show Simplification #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Simplification -> ShowS # show :: Simplification -> String # showList :: [Simplification] -> ShowS #
Semigroup Simplification #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (<>) :: Simplification -> Simplification -> Simplification # sconcat :: NonEmpty Simplification -> Simplification # stimes :: Integral b => b -> Simplification -> Simplification #
Monoid Simplification #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods mempty :: Simplification # mappend :: Simplification -> Simplification -> Simplification # mconcat :: [Simplification] -> Simplification #
Null Simplification #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: Simplification # null :: Simplification -> Bool #

data Reduced no yes #

Constructors

NoReduction no
YesReduction Simplification yes

Instances

Functor (Reduced no) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fmap :: (a -> b) -> Reduced no a -> Reduced no b # (<$) :: a -> Reduced no b -> Reduced no a #

data IsReduced #

Three cases: 1. not reduced, 2. reduced, but blocked, 3. reduced, not blocked.

Constructors

NotReduced
Reduced (Blocked ())

data MaybeReduced a #

Constructors

MaybeRed
Fields isReduced :: IsReduced ignoreReduced :: a

Instances

Functor MaybeReduced #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fmap :: (a -> b) -> MaybeReduced a -> MaybeReduced b # (<$) :: a -> MaybeReduced b -> MaybeReduced a #
IsProjElim e => IsProjElim (MaybeReduced e) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods isProjElim :: MaybeReduced e -> Maybe (ProjOrigin, QName) #
PrettyTCM a => PrettyTCM (MaybeReduced a) #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MaybeReduced a -> TCM Doc #

type MaybeReducedArgs = [MaybeReduced (Arg Term)] #

type MaybeReducedElims = [MaybeReduced Elim] #

notReduced :: a -> MaybeReduced a #

reduced :: Blocked (Arg Term) -> MaybeReduced (Arg Term) #

data AllowedReduction #

Controlling reduce.

Constructors

ProjectionReductions	(Projection and) projection-like functions may be reduced.
InlineReductions	Functions marked INLINE may be reduced.
CopatternReductions	Copattern definitions may be reduced.
FunctionReductions	Non-recursive functions and primitives may be reduced.
RecursiveReductions	Even recursive functions may be reduced.
LevelReductions	Reduce `Level` terms.
UnconfirmedReductions	Functions whose termination has not (yet) been confirmed.
NonTerminatingReductions	Functions that have failed termination checking.

Instances

Bounded AllowedReduction #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods minBound :: AllowedReduction # maxBound :: AllowedReduction #
Enum AllowedReduction #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods succ :: AllowedReduction -> AllowedReduction # pred :: AllowedReduction -> AllowedReduction # toEnum :: Int -> AllowedReduction # fromEnum :: AllowedReduction -> Int # enumFrom :: AllowedReduction -> [AllowedReduction] # enumFromThen :: AllowedReduction -> AllowedReduction -> [AllowedReduction] # enumFromTo :: AllowedReduction -> AllowedReduction -> [AllowedReduction] # enumFromThenTo :: AllowedReduction -> AllowedReduction -> AllowedReduction -> [AllowedReduction] #
Eq AllowedReduction #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: AllowedReduction -> AllowedReduction -> Bool # (/=) :: AllowedReduction -> AllowedReduction -> Bool #
Data AllowedReduction #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AllowedReduction -> c AllowedReduction # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AllowedReduction # toConstr :: AllowedReduction -> Constr # dataTypeOf :: AllowedReduction -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AllowedReduction) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AllowedReduction) # gmapT :: (forall b. Data b => b -> b) -> AllowedReduction -> AllowedReduction # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AllowedReduction -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AllowedReduction -> r # gmapQ :: (forall d. Data d => d -> u) -> AllowedReduction -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> AllowedReduction -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> AllowedReduction -> m AllowedReduction # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AllowedReduction -> m AllowedReduction # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AllowedReduction -> m AllowedReduction #
Ord AllowedReduction #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods compare :: AllowedReduction -> AllowedReduction -> Ordering # (<) :: AllowedReduction -> AllowedReduction -> Bool # (<=) :: AllowedReduction -> AllowedReduction -> Bool # (>) :: AllowedReduction -> AllowedReduction -> Bool # (>=) :: AllowedReduction -> AllowedReduction -> Bool # max :: AllowedReduction -> AllowedReduction -> AllowedReduction # min :: AllowedReduction -> AllowedReduction -> AllowedReduction #
Show AllowedReduction #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> AllowedReduction -> ShowS # show :: AllowedReduction -> String # showList :: [AllowedReduction] -> ShowS #

type AllowedReductions = [AllowedReduction] #

allReductions :: AllowedReductions #

Not quite all reductions (skip non-terminating reductions)

data PrimFun #

Constructors

PrimFun
Fields primFunName :: QName primFunArity :: Arity primFunImplementation :: [Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term)

Instances

Abstract PrimFun #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> PrimFun -> PrimFun #
Apply PrimFun #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: PrimFun -> Args -> PrimFun # applyE :: PrimFun -> Elims -> PrimFun #

defClauses :: Definition -> [Clause] #

defCompiled :: Definition -> Maybe CompiledClauses #

defParameters :: Definition -> Maybe Nat #

defInverse :: Definition -> FunctionInverse #

defCompilerPragmas :: BackendName -> Definition -> [CompilerPragma] #

defDelayed :: Definition -> Delayed #

Are the clauses of this definition delayed?

defNonterminating :: Definition -> Bool #

Has the definition failed the termination checker?

defTerminationUnconfirmed :: Definition -> Bool #

Has the definition not termination checked or did the check fail?

defAbstract :: Definition -> IsAbstract #

defForced :: Definition -> [IsForced] #

Injectivity

type FunctionInverse = FunctionInverse' Clause #

type InversionMap c = Map TermHead [c] #

data FunctionInverse' c #

Constructors

NotInjective
Inverse (InversionMap c)

Instances

Functor FunctionInverse' #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fmap :: (a -> b) -> FunctionInverse' a -> FunctionInverse' b # (<$) :: a -> FunctionInverse' b -> FunctionInverse' a #
Abstract FunctionInverse #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> FunctionInverse -> FunctionInverse #
Apply FunctionInverse #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: FunctionInverse -> Args -> FunctionInverse # applyE :: FunctionInverse -> Elims -> FunctionInverse #
DropArgs FunctionInverse #
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> FunctionInverse -> FunctionInverse #
InstantiateFull FunctionInverse #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: FunctionInverse -> ReduceM FunctionInverse #
Data c => Data (FunctionInverse' c) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c0 (d -> b) -> d -> c0 b) -> (forall g. g -> c0 g) -> FunctionInverse' c -> c0 (FunctionInverse' c) # gunfold :: (forall b r. Data b => c0 (b -> r) -> c0 r) -> (forall r. r -> c0 r) -> Constr -> c0 (FunctionInverse' c) # toConstr :: FunctionInverse' c -> Constr # dataTypeOf :: FunctionInverse' c -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c0 (t d)) -> Maybe (c0 (FunctionInverse' c)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c0 (t d e)) -> Maybe (c0 (FunctionInverse' c)) # gmapT :: (forall b. Data b => b -> b) -> FunctionInverse' c -> FunctionInverse' c # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunctionInverse' c -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunctionInverse' c -> r # gmapQ :: (forall d. Data d => d -> u) -> FunctionInverse' c -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> FunctionInverse' c -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> FunctionInverse' c -> m (FunctionInverse' c) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FunctionInverse' c -> m (FunctionInverse' c) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FunctionInverse' c -> m (FunctionInverse' c) #
Show c => Show (FunctionInverse' c) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> FunctionInverse' c -> ShowS # show :: FunctionInverse' c -> String # showList :: [FunctionInverse' c] -> ShowS #
KillRange c => KillRange (FunctionInverse' c) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT (FunctionInverse' c) #
EmbPrj a => EmbPrj (FunctionInverse' a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: FunctionInverse' a -> S Int32 # icod_ :: FunctionInverse' a -> S Int32 # value :: Int32 -> R (FunctionInverse' a) #

data TermHead #

Constructors

SortHead
PiHead
ConsHead QName
VarHead Nat
UnknownHead

Instances

Eq TermHead #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: TermHead -> TermHead -> Bool # (/=) :: TermHead -> TermHead -> Bool #
Data TermHead #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TermHead -> c TermHead # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TermHead # toConstr :: TermHead -> Constr # dataTypeOf :: TermHead -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TermHead) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TermHead) # gmapT :: (forall b. Data b => b -> b) -> TermHead -> TermHead # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TermHead -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TermHead -> r # gmapQ :: (forall d. Data d => d -> u) -> TermHead -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TermHead -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TermHead -> m TermHead # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TermHead -> m TermHead # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TermHead -> m TermHead #
Ord TermHead #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods compare :: TermHead -> TermHead -> Ordering # (<) :: TermHead -> TermHead -> Bool # (<=) :: TermHead -> TermHead -> Bool # (>) :: TermHead -> TermHead -> Bool # (>=) :: TermHead -> TermHead -> Bool # max :: TermHead -> TermHead -> TermHead # min :: TermHead -> TermHead -> TermHead #
Show TermHead #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> TermHead -> ShowS # show :: TermHead -> String # showList :: [TermHead] -> ShowS #
Pretty TermHead #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: TermHead -> Doc # prettyPrec :: Int -> TermHead -> Doc # prettyList :: [TermHead] -> Doc #
KillRange TermHead #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT TermHead #
EmbPrj TermHead #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: TermHead -> S Int32 # icod_ :: TermHead -> S Int32 # value :: Int32 -> R TermHead #

Mutual blocks

newtype MutualId #

Constructors

MutId Int32

Instances

Enum MutualId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods succ :: MutualId -> MutualId # pred :: MutualId -> MutualId # toEnum :: Int -> MutualId # fromEnum :: MutualId -> Int # enumFrom :: MutualId -> [MutualId] # enumFromThen :: MutualId -> MutualId -> [MutualId] # enumFromTo :: MutualId -> MutualId -> [MutualId] # enumFromThenTo :: MutualId -> MutualId -> MutualId -> [MutualId] #
Eq MutualId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: MutualId -> MutualId -> Bool # (/=) :: MutualId -> MutualId -> Bool #
Data MutualId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MutualId -> c MutualId # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MutualId # toConstr :: MutualId -> Constr # dataTypeOf :: MutualId -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MutualId) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MutualId) # gmapT :: (forall b. Data b => b -> b) -> MutualId -> MutualId # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MutualId -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MutualId -> r # gmapQ :: (forall d. Data d => d -> u) -> MutualId -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> MutualId -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> MutualId -> m MutualId # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MutualId -> m MutualId # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MutualId -> m MutualId #
Num MutualId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (+) :: MutualId -> MutualId -> MutualId # (-) :: MutualId -> MutualId -> MutualId # (*) :: MutualId -> MutualId -> MutualId # negate :: MutualId -> MutualId # abs :: MutualId -> MutualId # signum :: MutualId -> MutualId # fromInteger :: Integer -> MutualId #
Ord MutualId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods compare :: MutualId -> MutualId -> Ordering # (<) :: MutualId -> MutualId -> Bool # (<=) :: MutualId -> MutualId -> Bool # (>) :: MutualId -> MutualId -> Bool # (>=) :: MutualId -> MutualId -> Bool # max :: MutualId -> MutualId -> MutualId # min :: MutualId -> MutualId -> MutualId #
Show MutualId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> MutualId -> ShowS # show :: MutualId -> String # showList :: [MutualId] -> ShowS #
KillRange MutualId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT MutualId #
HasFresh MutualId #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' MutualId TCState # nextFresh' :: MutualId -> MutualId #
EmbPrj MutualId #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: MutualId -> S Int32 # icod_ :: MutualId -> S Int32 # value :: Int32 -> R MutualId #

Statistics

type Statistics = Map String Integer #

Trace

data Call #

Constructors

CheckClause Type SpineClause
CheckPattern Pattern Telescope Type
CheckLetBinding LetBinding
InferExpr Expr
CheckExprCall Expr Type
CheckDotPattern Expr Term
CheckPatternShadowing SpineClause
CheckProjection Range QName Type
IsTypeCall Expr Sort
IsType_ Expr
InferVar Name
InferDef QName
CheckArguments Range [NamedArg Expr] Type (Maybe Type)
CheckTargetType Range Type Type
CheckDataDef Range Name [LamBinding] [Constructor]
CheckRecDef Range Name [LamBinding] [Constructor]
CheckConstructor QName Telescope Sort Constructor
CheckFunDefCall Range Name [Clause]
CheckPragma Range Pragma
CheckPrimitive Range Name Expr
CheckIsEmpty Range Type
CheckWithFunctionType Expr
CheckSectionApplication Range ModuleName ModuleApplication
CheckNamedWhere ModuleName
ScopeCheckExpr Expr
ScopeCheckDeclaration NiceDeclaration
ScopeCheckLHS QName Pattern
NoHighlighting
ModuleContents	Interaction command: show module contents.
SetRange Range	used by `setCurrentRange`

Instances

Data Call #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Call -> c Call # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Call # toConstr :: Call -> Constr # dataTypeOf :: Call -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Call) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Call) # gmapT :: (forall b. Data b => b -> b) -> Call -> Call # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Call -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Call -> r # gmapQ :: (forall d. Data d => d -> u) -> Call -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Call -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Call -> m Call # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Call -> m Call # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Call -> m Call #
Pretty Call #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Call -> Doc # prettyPrec :: Int -> Call -> Doc # prettyList :: [Call] -> Doc #
HasRange Call #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: Call -> Range #
PrettyTCM Call #
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: Call -> TCM Doc #

Instance table

type InstanceTable = Map QName (Set QName) #

The instance table is a Map associating to every name of recorddata typepostulate its list of instances

type TempInstanceTable = (InstanceTable, Set QName) #

When typechecking something of the following form:

instance x : _ x = y

it's not yet known where to add x, so we add it to a list of unresolved instances and we'll deal with it later.

Builtin things

data BuiltinDescriptor #

Constructors

BuiltinData (TCM Type) [String]
BuiltinDataCons (TCM Type)
BuiltinPrim String (Term -> TCM ())
BuiltinPostulate Relevance (TCM Type)
BuiltinUnknown (Maybe (TCM Type)) (Term -> Type -> TCM ())	Builtin of any kind. Type can be checked (`Just t`) or inferred (`Nothing`). The second argument is the hook for the verification function.

data BuiltinInfo #

Constructors

BuiltinInfo
Fields builtinName :: String builtinDesc :: BuiltinDescriptor

type BuiltinThings pf = Map String (Builtin pf) #

data Builtin pf #

Constructors

Builtin Term
Prim pf

Instances

Functor Builtin #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fmap :: (a -> b) -> Builtin a -> Builtin b # (<$) :: a -> Builtin b -> Builtin a #
Foldable Builtin #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fold :: Monoid m => Builtin m -> m # foldMap :: Monoid m => (a -> m) -> Builtin a -> m # foldr :: (a -> b -> b) -> b -> Builtin a -> b # foldr' :: (a -> b -> b) -> b -> Builtin a -> b # foldl :: (b -> a -> b) -> b -> Builtin a -> b # foldl' :: (b -> a -> b) -> b -> Builtin a -> b # foldr1 :: (a -> a -> a) -> Builtin a -> a # foldl1 :: (a -> a -> a) -> Builtin a -> a # toList :: Builtin a -> [a] # null :: Builtin a -> Bool # length :: Builtin a -> Int # elem :: Eq a => a -> Builtin a -> Bool # maximum :: Ord a => Builtin a -> a # minimum :: Ord a => Builtin a -> a # sum :: Num a => Builtin a -> a # product :: Num a => Builtin a -> a #
Traversable Builtin #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods traverse :: Applicative f => (a -> f b) -> Builtin a -> f (Builtin b) # sequenceA :: Applicative f => Builtin (f a) -> f (Builtin a) # mapM :: Monad m => (a -> m b) -> Builtin a -> m (Builtin b) # sequence :: Monad m => Builtin (m a) -> m (Builtin a) #
Show pf => Show (Builtin pf) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Builtin pf -> ShowS # show :: Builtin pf -> String # showList :: [Builtin pf] -> ShowS #
EmbPrj a => EmbPrj (Builtin a) #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Builtin a -> S Int32 # icod_ :: Builtin a -> S Int32 # value :: Int32 -> R (Builtin a) #
InstantiateFull a => InstantiateFull (Builtin a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Builtin a -> ReduceM (Builtin a) #

Highlighting levels

data HighlightingLevel #

How much highlighting should be sent to the user interface?

Constructors

None
NonInteractive
Interactive	This includes both non-interactive highlighting and interactive highlighting of the expression that is currently being type-checked.

Instances

Eq HighlightingLevel #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: HighlightingLevel -> HighlightingLevel -> Bool # (/=) :: HighlightingLevel -> HighlightingLevel -> Bool #
Data HighlightingLevel #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HighlightingLevel -> c HighlightingLevel # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HighlightingLevel # toConstr :: HighlightingLevel -> Constr # dataTypeOf :: HighlightingLevel -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HighlightingLevel) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HighlightingLevel) # gmapT :: (forall b. Data b => b -> b) -> HighlightingLevel -> HighlightingLevel # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HighlightingLevel -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HighlightingLevel -> r # gmapQ :: (forall d. Data d => d -> u) -> HighlightingLevel -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> HighlightingLevel -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> HighlightingLevel -> m HighlightingLevel # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HighlightingLevel -> m HighlightingLevel # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HighlightingLevel -> m HighlightingLevel #
Ord HighlightingLevel #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods compare :: HighlightingLevel -> HighlightingLevel -> Ordering # (<) :: HighlightingLevel -> HighlightingLevel -> Bool # (<=) :: HighlightingLevel -> HighlightingLevel -> Bool # (>) :: HighlightingLevel -> HighlightingLevel -> Bool # (>=) :: HighlightingLevel -> HighlightingLevel -> Bool # max :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel # min :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel #
Read HighlightingLevel #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods readsPrec :: Int -> ReadS HighlightingLevel # readList :: ReadS [HighlightingLevel] # readPrec :: ReadPrec HighlightingLevel # readListPrec :: ReadPrec [HighlightingLevel] #
Show HighlightingLevel #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> HighlightingLevel -> ShowS # show :: HighlightingLevel -> String # showList :: [HighlightingLevel] -> ShowS #

data HighlightingMethod #

How should highlighting be sent to the user interface?

Constructors

Direct	Via stdout.
Indirect	Both via files and via stdout.

Instances

Eq HighlightingMethod #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: HighlightingMethod -> HighlightingMethod -> Bool # (/=) :: HighlightingMethod -> HighlightingMethod -> Bool #
Data HighlightingMethod #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HighlightingMethod -> c HighlightingMethod # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HighlightingMethod # toConstr :: HighlightingMethod -> Constr # dataTypeOf :: HighlightingMethod -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HighlightingMethod) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HighlightingMethod) # gmapT :: (forall b. Data b => b -> b) -> HighlightingMethod -> HighlightingMethod # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HighlightingMethod -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HighlightingMethod -> r # gmapQ :: (forall d. Data d => d -> u) -> HighlightingMethod -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> HighlightingMethod -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> HighlightingMethod -> m HighlightingMethod # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HighlightingMethod -> m HighlightingMethod # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HighlightingMethod -> m HighlightingMethod #
Read HighlightingMethod #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods readsPrec :: Int -> ReadS HighlightingMethod # readList :: ReadS [HighlightingMethod] # readPrec :: ReadPrec HighlightingMethod # readListPrec :: ReadPrec [HighlightingMethod] #
Show HighlightingMethod #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> HighlightingMethod -> ShowS # show :: HighlightingMethod -> String # showList :: [HighlightingMethod] -> ShowS #

ifTopLevelAndHighlightingLevelIsOr :: MonadTCM tcm => HighlightingLevel -> Bool -> tcm () -> tcm () #

ifTopLevelAndHighlightingLevelIs l b m runs m when we're type-checking the top-level module and either the highlighting level is at least l or b is True.

ifTopLevelAndHighlightingLevelIs :: MonadTCM tcm => HighlightingLevel -> tcm () -> tcm () #

ifTopLevelAndHighlightingLevelIs l m runs m when we're type-checking the top-level module and the highlighting level is at least l.

Type checking environment

data TCEnv #

Constructors

TCEnv

Fields

envContext :: Context
envLetBindings :: LetBindings
envCurrentModule :: ModuleName
envCurrentPath :: Maybe AbsolutePath
The path to the file that is currently being type-checked. Nothing if we do not have a file (like in interactive mode see CommandLine).
envAnonymousModules :: [(ModuleName, Nat)]
anonymous modules and their number of free variables
envImportPath :: [TopLevelModuleName]
to detect import cycles
envMutualBlock :: Maybe MutualId
the current (if any) mutual block
envTerminationCheck :: TerminationCheck ()
are we inside the scope of a termination pragma
envSolvingConstraints :: Bool
Are we currently in the process of solving active constraints?
envCheckingWhere :: Bool
Have we stepped into the where-declarations of a clause? Everything under a where will be checked with this flag on.
envWorkingOnTypes :: Bool
Are we working on types? Turned on by workOnTypes.
envAssignMetas :: Bool
Are we allowed to assign metas?
envActiveProblems :: Set ProblemId
envAbstractMode :: AbstractMode
When checking the typesignature of a public definition or the body of a non-abstract definition this is true. To prevent information about abstract things leaking outside the module.
envRelevance :: Relevance
Are we checking an irrelevant argument? (=Irrelevant) Then top-level irrelevant declarations are enabled. Other value: Relevant, then only relevant decls. are avail.
envDisplayFormsEnabled :: Bool
Sometimes we want to disable display forms.
envRange :: Range
envHighlightingRange :: Range
Interactive highlighting uses this range rather than envRange.
envClause :: IPClause
What is the current clause we are type-checking? Will be recorded in interaction points in this clause.
envCall :: Maybe (Closure Call)
what we're doing at the moment
envHighlightingLevel :: HighlightingLevel
Set to None when imported modules are type-checked.
envHighlightingMethod :: HighlightingMethod
envModuleNestingLevel :: !Int
This number indicates how far away from the top-level module Agda has come when chasing modules. The level of a given module is not necessarily the same as the length, in the module dependency graph, of the shortest path from the top-level module; it depends on in which order Agda chooses to chase dependencies.
envAllowDestructiveUpdate :: Bool
When True, allows destructively shared updating terms during evaluation or unification. This is disabled when doing speculative checking, like solve instance metas, or when updating might break abstraction, as is the case when checking abstract definitions.
envExpandLast :: ExpandHidden
When type-checking an alias f=e, we do not want to insert hidden arguments in the end, because these will become unsolved metas.
envAppDef :: Maybe QName
We are reducing an application of this function. (For debugging of incomplete matches only.)
envSimplification :: Simplification
Did we encounter a simplification (proper match) during the current reduction process?
envAllowedReductions :: AllowedReductions
envInjectivityDepth :: Int
Injectivity can cause non-termination for unsolvable contraints (3067). Keep a limit on the nesting depth of injectivity uses.
envCompareBlocked :: Bool
Can we compare blocked things during conversion? No by default. Yes for rewriting feature.
envPrintDomainFreePi :: Bool
When True, types will be omitted from printed pi types if they can be inferred.
envPrintMetasBare :: Bool
When True, throw away meta numbers and meta elims. This is used for reifying terms for feeding into the user's source code, e.g., for the interaction tactics solveAll.
envInsideDotPattern :: Bool
Used by the scope checker to make sure that certain forms of expressions are not used inside dot patterns: extended lambdas and let-expressions.
envUnquoteFlags :: UnquoteFlags
envInstanceDepth :: !Int
Until we get a termination checker for instance search (#1743) we limit the search depth to ensure termination.
envIsDebugPrinting :: Bool
envPrintingPatternLambdas :: [QName]
#3004: pattern lambdas with copatterns may refer to themselves. We don't have a good story for what to do in this case, but at least printing shouldn't loop. Here we keep track of which pattern lambdas we are currently in the process of printing.
envCallByNeed :: Bool
Use call-by-need evaluation for reductions.
envCurrentCheckpoint :: CheckpointId
Checkpoints track the evolution of the context as we go under binders or refine it by pattern matching.
envCheckpoints :: Map CheckpointId Substitution
Keeps the substitution from each previous checkpoint to the current context.

Instances

Data TCEnv #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TCEnv -> c TCEnv # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TCEnv # toConstr :: TCEnv -> Constr # dataTypeOf :: TCEnv -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TCEnv) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TCEnv) # gmapT :: (forall b. Data b => b -> b) -> TCEnv -> TCEnv # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TCEnv -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TCEnv -> r # gmapQ :: (forall d. Data d => d -> u) -> TCEnv -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TCEnv -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TCEnv -> m TCEnv # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TCEnv -> m TCEnv # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TCEnv -> m TCEnv #
MonadReader TCEnv ReduceM #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods ask :: ReduceM TCEnv # local :: (TCEnv -> TCEnv) -> ReduceM a -> ReduceM a # reader :: (TCEnv -> a) -> ReduceM a #
MonadReader TCEnv TerM #
Instance details Defined in Agda.Termination.Monad Methods ask :: TerM TCEnv # local :: (TCEnv -> TCEnv) -> TerM a -> TerM a # reader :: (TCEnv -> a) -> TerM a #
MonadIO m => MonadReader TCEnv (TCMT m) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods ask :: TCMT m TCEnv # local :: (TCEnv -> TCEnv) -> TCMT m a -> TCMT m a # reader :: (TCEnv -> a) -> TCMT m a #

initEnv :: TCEnv #

disableDestructiveUpdate :: TCM a -> TCM a #

data UnquoteFlags #

Constructors

UnquoteFlags
Fields _unquoteNormalise :: Bool

Instances

Data UnquoteFlags #

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UnquoteFlags -> c UnquoteFlags #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UnquoteFlags #

toConstr :: UnquoteFlags -> Constr #

dataTypeOf :: UnquoteFlags -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UnquoteFlags) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UnquoteFlags) #

gmapT :: (forall b. Data b => b -> b) -> UnquoteFlags -> UnquoteFlags #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UnquoteFlags -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UnquoteFlags -> r #

gmapQ :: (forall d. Data d => d -> u) -> UnquoteFlags -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> UnquoteFlags -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> UnquoteFlags -> m UnquoteFlags #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UnquoteFlags -> m UnquoteFlags #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UnquoteFlags -> m UnquoteFlags #

defaultUnquoteFlags :: UnquoteFlags #

unquoteNormalise :: Lens' Bool UnquoteFlags #

eUnquoteNormalise :: Lens' Bool TCEnv #

e-prefixed lenses

eContext :: Lens' Context TCEnv #

eLetBindings :: Lens' LetBindings TCEnv #

eCurrentModule :: Lens' ModuleName TCEnv #

eCurrentPath :: Lens' (Maybe AbsolutePath) TCEnv #

eAnonymousModules :: Lens' [(ModuleName, Nat)] TCEnv #

eImportPath :: Lens' [TopLevelModuleName] TCEnv #

eMutualBlock :: Lens' (Maybe MutualId) TCEnv #

eTerminationCheck :: Lens' (TerminationCheck ()) TCEnv #

eSolvingConstraints :: Lens' Bool TCEnv #

eCheckingWhere :: Lens' Bool TCEnv #

eWorkingOnTypes :: Lens' Bool TCEnv #

eAssignMetas :: Lens' Bool TCEnv #

eActiveProblems :: Lens' (Set ProblemId) TCEnv #

eAbstractMode :: Lens' AbstractMode TCEnv #

eRelevance :: Lens' Relevance TCEnv #

eDisplayFormsEnabled :: Lens' Bool TCEnv #

eRange :: Lens' Range TCEnv #

eHighlightingRange :: Lens' Range TCEnv #

eCall :: Lens' (Maybe (Closure Call)) TCEnv #

eHighlightingLevel :: Lens' HighlightingLevel TCEnv #

eHighlightingMethod :: Lens' HighlightingMethod TCEnv #

eModuleNestingLevel :: Lens' Int TCEnv #

eAllowDestructiveUpdate :: Lens' Bool TCEnv #

eExpandLast :: Lens' ExpandHidden TCEnv #

eAppDef :: Lens' (Maybe QName) TCEnv #

eSimplification :: Lens' Simplification TCEnv #

eAllowedReductions :: Lens' AllowedReductions TCEnv #

eInjectivityDepth :: Lens' Int TCEnv #

eCompareBlocked :: Lens' Bool TCEnv #

ePrintDomainFreePi :: Lens' Bool TCEnv #

eInsideDotPattern :: Lens' Bool TCEnv #

eUnquoteFlags :: Lens' UnquoteFlags TCEnv #

eInstanceDepth :: Lens' Int TCEnv #

eIsDebugPrinting :: Lens' Bool TCEnv #

ePrintingPatternLambdas :: Lens' [QName] TCEnv #

eCallByNeed :: Lens' Bool TCEnv #

eCurrentCheckpoint :: Lens' CheckpointId TCEnv #

eCheckpoints :: Lens' (Map CheckpointId Substitution) TCEnv #

Context

type Context = [ContextEntry] #

The Context is a stack of ContextEntrys.

type ContextEntry = Dom (Name, Type) #

Let bindings

type LetBindings = Map Name (Open (Term, Dom Type)) #

Abstract mode

data AbstractMode #

Constructors

AbstractMode	Abstract things in the current module can be accessed.
ConcreteMode	No abstract things can be accessed.
IgnoreAbstractMode	All abstract things can be accessed.

Instances

Eq AbstractMode #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: AbstractMode -> AbstractMode -> Bool # (/=) :: AbstractMode -> AbstractMode -> Bool #
Data AbstractMode #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AbstractMode -> c AbstractMode # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AbstractMode # toConstr :: AbstractMode -> Constr # dataTypeOf :: AbstractMode -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AbstractMode) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AbstractMode) # gmapT :: (forall b. Data b => b -> b) -> AbstractMode -> AbstractMode # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AbstractMode -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AbstractMode -> r # gmapQ :: (forall d. Data d => d -> u) -> AbstractMode -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> AbstractMode -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> AbstractMode -> m AbstractMode # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AbstractMode -> m AbstractMode # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AbstractMode -> m AbstractMode #
Show AbstractMode #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> AbstractMode -> ShowS # show :: AbstractMode -> String # showList :: [AbstractMode] -> ShowS #

aDefToMode :: IsAbstract -> AbstractMode #

aModeToDef :: AbstractMode -> IsAbstract #

Insertion of implicit arguments

data ExpandHidden #

Constructors

ExpandLast	Add implicit arguments in the end until type is no longer hidden `Pi`.
DontExpandLast	Do not append implicit arguments.

Instances

Eq ExpandHidden #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: ExpandHidden -> ExpandHidden -> Bool # (/=) :: ExpandHidden -> ExpandHidden -> Bool #
Data ExpandHidden #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExpandHidden -> c ExpandHidden # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExpandHidden # toConstr :: ExpandHidden -> Constr # dataTypeOf :: ExpandHidden -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExpandHidden) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExpandHidden) # gmapT :: (forall b. Data b => b -> b) -> ExpandHidden -> ExpandHidden # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExpandHidden -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExpandHidden -> r # gmapQ :: (forall d. Data d => d -> u) -> ExpandHidden -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ExpandHidden -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExpandHidden -> m ExpandHidden # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExpandHidden -> m ExpandHidden # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExpandHidden -> m ExpandHidden #

data ExplicitToInstance #

Constructors

ExplicitToInstance	Explicit arguments are considered as instance arguments
ExplicitStayExplicit

Instances

Eq ExplicitToInstance #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: ExplicitToInstance -> ExplicitToInstance -> Bool # (/=) :: ExplicitToInstance -> ExplicitToInstance -> Bool #
Data ExplicitToInstance #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExplicitToInstance -> c ExplicitToInstance # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExplicitToInstance # toConstr :: ExplicitToInstance -> Constr # dataTypeOf :: ExplicitToInstance -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExplicitToInstance) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExplicitToInstance) # gmapT :: (forall b. Data b => b -> b) -> ExplicitToInstance -> ExplicitToInstance # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExplicitToInstance -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExplicitToInstance -> r # gmapQ :: (forall d. Data d => d -> u) -> ExplicitToInstance -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ExplicitToInstance -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExplicitToInstance -> m ExplicitToInstance # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExplicitToInstance -> m ExplicitToInstance # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExplicitToInstance -> m ExplicitToInstance #
Show ExplicitToInstance #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> ExplicitToInstance -> ShowS # show :: ExplicitToInstance -> String # showList :: [ExplicitToInstance] -> ShowS #

data Candidate #

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 candidateTerm :: Term candidateType :: Type candidateEti :: ExplicitToInstance candidateOverlappable :: Bool

Instances

Eq Candidate #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Candidate -> Candidate -> Bool # (/=) :: Candidate -> Candidate -> Bool #
Data Candidate #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Candidate -> c Candidate # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Candidate # toConstr :: Candidate -> Constr # dataTypeOf :: Candidate -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Candidate) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Candidate) # gmapT :: (forall b. Data b => b -> b) -> Candidate -> Candidate # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Candidate -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Candidate -> r # gmapQ :: (forall d. Data d => d -> u) -> Candidate -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Candidate -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Candidate -> m Candidate # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Candidate -> m Candidate # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Candidate -> m Candidate #
Show Candidate #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Candidate -> ShowS # show :: Candidate -> String # showList :: [Candidate] -> ShowS #
Free Candidate #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet c => Candidate -> FreeM c #
InstantiateFull Candidate #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Candidate -> ReduceM Candidate #
Normalise Candidate #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Candidate -> ReduceM Candidate #
Simplify Candidate #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Candidate -> ReduceM Candidate #
Reduce Candidate #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Candidate -> ReduceM Candidate # reduceB' :: Candidate -> ReduceM (Blocked Candidate) #
Instantiate Candidate #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Candidate -> ReduceM Candidate #
Subst Term Candidate #
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Candidate -> Candidate #

Type checking warnings (aka non-fatal errors)

data Warning #

A non-fatal error is an error which does not prevent us from checking the document further and interacting with the user.

Constructors

NicifierIssue DeclarationWarning
TerminationIssue [TerminationError]
UnreachableClauses QName [[NamedArg DeBruijnPattern]]
CoverageIssue QName [(Telescope, [NamedArg DeBruijnPattern])]	`CoverageIssue f pss` means that `pss` are not covered in `f`
CoverageNoExactSplit QName [Clause]
NotStrictlyPositive QName OccursWhere
UnsolvedMetaVariables [Range]	Do not use directly with `warning`
UnsolvedInteractionMetas [Range]	Do not use directly with `warning`
UnsolvedConstraints Constraints	Do not use directly with `warning`
OldBuiltin String String	In `OldBuiltin old new`, the BUILTIN old has been replaced by new
EmptyRewritePragma	If the user wrote just `{--}`.
UselessPublic	If the user opens a module public before the module header. (See issue #2377.)
UselessInline QName
InversionDepthReached QName	The --inversion-max-depth was reached.
GenericWarning Doc	Harmless generic warning (not an error)
GenericNonFatalError Doc	Generic error which doesn't abort proceedings (not a warning) Safe flag errors
SafeFlagPostulate Name
SafeFlagPragma [String]
SafeFlagNonTerminating
SafeFlagTerminating
SafeFlagPrimTrustMe
SafeFlagNoPositivityCheck
SafeFlagPolarity
ParseWarning ParseWarning
DeprecationWarning String String String	`DeprecationWarning old new version`: `old` is deprecated, use `new` instead. This will be an error in Agda `version`.
UserWarning String	User-defined warning (e.g. to mention that a name is deprecated)

Instances

Data Warning #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Warning -> c Warning # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Warning # toConstr :: Warning -> Constr # dataTypeOf :: Warning -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Warning) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Warning) # gmapT :: (forall b. Data b => b -> b) -> Warning -> Warning # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Warning -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Warning -> r # gmapQ :: (forall d. Data d => d -> u) -> Warning -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Warning -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Warning -> m Warning # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Warning -> m Warning # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Warning -> m Warning #
Show Warning #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Warning -> ShowS # show :: Warning -> String # showList :: [Warning] -> ShowS #
EmbPrj Warning #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: Warning -> S Int32 # icod_ :: Warning -> S Int32 # value :: Int32 -> R Warning #
PrettyTCM Warning #
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: Warning -> TCM Doc #

warningName :: Warning -> WarningName #

data TCWarning #

Constructors

TCWarning
Fields tcWarningRange :: Range Range where the warning was raised tcWarning :: Warning The warning itself tcWarningPrintedWarning :: Doc The warning printed in the state and environment where it was raised tcWarningCached :: Bool Should the warning be affected by caching.

Instances

Eq TCWarning #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: TCWarning -> TCWarning -> Bool # (/=) :: TCWarning -> TCWarning -> Bool #
Show TCWarning #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> TCWarning -> ShowS # show :: TCWarning -> String # showList :: [TCWarning] -> ShowS #
HasRange TCWarning #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: TCWarning -> Range #
EmbPrj TCWarning #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: TCWarning -> S Int32 # icod_ :: TCWarning -> S Int32 # value :: Int32 -> R TCWarning #
PrettyTCM TCWarning #
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: TCWarning -> TCM Doc #

tcWarningOrigin :: TCWarning -> SrcFile #

equalHeadConstructors :: Warning -> Warning -> Bool #

getPartialDefs :: ReadTCState tcm => tcm [QName] #

Type checking errors

data CallInfo #

Information about a call.

Constructors

CallInfo
Fields callInfoTarget :: QName Target function name. callInfoRange :: Range Range of the target function. callInfoCall :: Closure Term To be formatted representation of the call.

Instances

Data CallInfo #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CallInfo -> c CallInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CallInfo # toConstr :: CallInfo -> Constr # dataTypeOf :: CallInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CallInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CallInfo) # gmapT :: (forall b. Data b => b -> b) -> CallInfo -> CallInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CallInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CallInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> CallInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> CallInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> CallInfo -> m CallInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CallInfo -> m CallInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CallInfo -> m CallInfo #
Show CallInfo #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> CallInfo -> ShowS # show :: CallInfo -> String # showList :: [CallInfo] -> ShowS #
Pretty CallInfo #	We only `show` the name of the callee.
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: CallInfo -> Doc # prettyPrec :: Int -> CallInfo -> Doc # prettyList :: [CallInfo] -> Doc #
AllNames CallInfo #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods allNames :: CallInfo -> Seq QName #
PrettyTCM CallInfo #
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: CallInfo -> TCM Doc #

data TerminationError #

Information about a mutual block which did not pass the termination checker.

Constructors

TerminationError
Fields termErrFunctions :: [QName] The functions which failed to check. (May not include automatically generated functions.) termErrCalls :: [CallInfo] The problematic call sites.

Instances

Data TerminationError #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TerminationError -> c TerminationError # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TerminationError # toConstr :: TerminationError -> Constr # dataTypeOf :: TerminationError -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TerminationError) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TerminationError) # gmapT :: (forall b. Data b => b -> b) -> TerminationError -> TerminationError # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TerminationError -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TerminationError -> r # gmapQ :: (forall d. Data d => d -> u) -> TerminationError -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TerminationError -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TerminationError -> m TerminationError # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TerminationError -> m TerminationError # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TerminationError -> m TerminationError #
Show TerminationError #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> TerminationError -> ShowS # show :: TerminationError -> String # showList :: [TerminationError] -> ShowS #

data SplitError #

Error when splitting a pattern variable into possible constructor patterns.

Constructors

NotADatatype (Closure Type)	Neither data type nor record.
IrrelevantDatatype (Closure Type)	Data type, but in irrelevant position.
CoinductiveDatatype (Closure Type)	Split on codata not allowed. UNUSED, but keep! -- \| NoRecordConstructor Type -- ^ record type, but no constructor
UnificationStuck
Fields cantSplitConName :: QName Constructor. cantSplitTel :: Telescope Context for indices. cantSplitConIdx :: Args Inferred indices (from type of constructor). cantSplitGivenIdx :: Args Expected indices (from checking pattern). cantSplitFailures :: [UnificationFailure] Reason(s) why unification got stuck.
GenericSplitError String

Instances

Show SplitError #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> SplitError -> ShowS # show :: SplitError -> String # showList :: [SplitError] -> ShowS #
PrettyTCM SplitError #
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: SplitError -> TCM Doc #

data NegativeUnification #

Constructors

UnifyConflict Telescope Term Term
UnifyCycle Telescope Int Term

Instances

Show NegativeUnification #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> NegativeUnification -> ShowS # show :: NegativeUnification -> String # showList :: [NegativeUnification] -> ShowS #
PrettyTCM NegativeUnification #
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: NegativeUnification -> TCM Doc #

data UnificationFailure #

Constructors

UnifyIndicesNotVars Telescope Type Term Term Args	Failed to apply injectivity to constructor of indexed datatype
UnifyRecursiveEq Telescope Type Int Term	Can't solve equation because variable occurs in (type of) lhs
UnifyReflexiveEq Telescope Type Term	Can't solve reflexive equation because --without-K is enabled

Instances

Show UnificationFailure #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> UnificationFailure -> ShowS # show :: UnificationFailure -> String # showList :: [UnificationFailure] -> ShowS #
PrettyTCM UnificationFailure #
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: UnificationFailure -> TCM Doc #

data UnquoteError #

Constructors

BadVisibility String (Arg Term)
ConInsteadOfDef QName String String
DefInsteadOfCon QName String String
NonCanonical String Term
BlockedOnMeta TCState MetaId
UnquotePanic String

Instances

Show UnquoteError #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> UnquoteError -> ShowS # show :: UnquoteError -> String # showList :: [UnquoteError] -> ShowS #

data TypeError #

Constructors

InternalError String
NotImplemented String
NotSupported String
CompilationError String
TerminationCheckFailed [TerminationError]
PropMustBeSingleton
DataMustEndInSort Term
ShouldEndInApplicationOfTheDatatype Type	The target of a constructor isn't an application of its datatype. The `Type` records what it does target.
ShouldBeAppliedToTheDatatypeParameters Term Term	The target of a constructor isn't its datatype applied to something that isn't the parameters. First term is the correct target and the second term is the actual target.
ShouldBeApplicationOf Type QName	Expected a type to be an application of a particular datatype.
ConstructorPatternInWrongDatatype QName QName	constructor, datatype
CantResolveOverloadedConstructorsTargetingSameDatatype QName [QName]	Datatype, constructors.
DoesNotConstructAnElementOf QName Type	constructor, type
DifferentArities	Varying number of arguments for a function.
WrongHidingInLHS	The left hand side of a function definition has a hidden argument where a non-hidden was expected.
WrongHidingInLambda Type	Expected a non-hidden function and found a hidden lambda.
WrongHidingInApplication Type	A function is applied to a hidden argument where a non-hidden was expected.
WrongNamedArgument (NamedArg Expr)	A function is applied to a hidden named argument it does not have.
WrongIrrelevanceInLambda	Wrong user-given relevance annotation in lambda.
WrongInstanceDeclaration	A term is declared as an instance but it’s not allowed
HidingMismatch Hiding Hiding	The given hiding does not correspond to the expected hiding.
RelevanceMismatch Relevance Relevance	The given relevance does not correspond to the expected relevane.
UninstantiatedDotPattern Expr
ForcedConstructorNotInstantiated Pattern
IlltypedPattern Pattern Type
IllformedProjectionPattern Pattern
CannotEliminateWithPattern (NamedArg Pattern) Type
WrongNumberOfConstructorArguments QName Nat Nat
ShouldBeEmpty Type [DeBruijnPattern]
ShouldBeASort Type	The given type should have been a sort.
ShouldBePi Type	The given type should have been a pi.
ShouldBeRecordType Type
ShouldBeRecordPattern DeBruijnPattern
NotAProjectionPattern (NamedArg Pattern)
NotAProperTerm
SetOmegaNotValidType
InvalidTypeSort Sort	This sort is not a type expression.
InvalidType Term	This term is not a type expression.
FunctionTypeInSizeUniv Term	This term, a function type constructor, lives in `SizeUniv`, which is not allowed.
SplitOnIrrelevant (Dom Type)
SplitOnNonVariable Term Type
DefinitionIsIrrelevant QName
VariableIsIrrelevant Name
UnequalTerms Comparison Term Term Type
UnequalTypes Comparison Type Type
UnequalRelevance Comparison Term Term	The two function types have different relevance.
UnequalHiding Term Term	The two function types have different hiding.
UnequalSorts Sort Sort
UnequalBecauseOfUniverseConflict Comparison Term Term
NotLeqSort Sort Sort
MetaCannotDependOn MetaId [Nat] Nat	The arguments are the meta variable, the parameters it can depend on and the paratemeter that it wants to depend on.
MetaOccursInItself MetaId
MetaIrrelevantSolution MetaId Term
GenericError String
GenericDocError Doc
BuiltinMustBeConstructor String Expr
NoSuchBuiltinName String
DuplicateBuiltinBinding String Term Term
NoBindingForBuiltin String
NoSuchPrimitiveFunction String
ShadowedModule Name [ModuleName]
BuiltinInParameterisedModule String
IllegalLetInTelescope TypedBinding
NoRHSRequiresAbsurdPattern [NamedArg Pattern]
AbsurdPatternRequiresNoRHS [NamedArg Pattern]
TooFewFields QName [Name]
TooManyFields QName [Name]
DuplicateFields [Name]
DuplicateConstructors [Name]
WithOnFreeVariable Expr Term
UnexpectedWithPatterns [Pattern]
WithClausePatternMismatch Pattern (NamedArg DeBruijnPattern)
FieldOutsideRecord
ModuleArityMismatch ModuleName Telescope [NamedArg Expr]
SplitError SplitError
ImpossibleConstructor QName NegativeUnification
TooManyPolarities QName Int
LocalVsImportedModuleClash ModuleName
SolvedButOpenHoles	Some interaction points (holes) have not been filled by user. There are not `UnsolvedMetas` since unification solved them. This is an error, since interaction points are never filled without user interaction.
CyclicModuleDependency [TopLevelModuleName]
FileNotFound TopLevelModuleName [AbsolutePath]
OverlappingProjects AbsolutePath TopLevelModuleName TopLevelModuleName
AmbiguousTopLevelModuleName TopLevelModuleName [AbsolutePath]
ModuleNameUnexpected TopLevelModuleName TopLevelModuleName	Found module name, expected module name.
ModuleNameDoesntMatchFileName TopLevelModuleName [AbsolutePath]
ClashingFileNamesFor ModuleName [AbsolutePath]
ModuleDefinedInOtherFile TopLevelModuleName AbsolutePath AbsolutePath	Module name, file from which it was loaded, file which the include path says contains the module. Scope errors
BothWithAndRHS
AbstractConstructorNotInScope QName
NotInScope [QName]
NoSuchModule QName
AmbiguousName QName (NonemptyList QName)
AmbiguousModule QName (NonemptyList ModuleName)
UninstantiatedModule QName
ClashingDefinition QName QName
ClashingModule ModuleName ModuleName
ClashingImport Name QName
ClashingModuleImport Name ModuleName
PatternShadowsConstructor Name QName
ModuleDoesntExport QName [ImportedName]
DuplicateImports QName [ImportedName]
InvalidPattern Pattern
RepeatedVariablesInPattern [Name]
NotAModuleExpr Expr	The expr was used in the right hand side of an implicit module definition, but it wasn't of the form `m Delta`.
NotAnExpression Expr
NotAValidLetBinding NiceDeclaration
NotValidBeforeField NiceDeclaration
NothingAppliedToHiddenArg Expr
NothingAppliedToInstanceArg Expr
BadArgumentsToPatternSynonym AmbiguousQName
TooFewArgumentsToPatternSynonym AmbiguousQName
CannotResolveAmbiguousPatternSynonym (NonemptyList (QName, PatternSynDefn))
UnusedVariableInPatternSynonym
NoParseForApplication [Expr]
AmbiguousParseForApplication [Expr] [Expr]
NoParseForLHS LHSOrPatSyn Pattern
AmbiguousParseForLHS LHSOrPatSyn Pattern [Pattern]
OperatorInformation [NotationSection] TypeError
IFSNoCandidateInScope Type
UnquoteFailed UnquoteError
DeBruijnIndexOutOfScope Nat Telescope [Name]
NeedOptionCopatterns
NeedOptionRewriting
NonFatalErrors [TCWarning]
InstanceSearchDepthExhausted Term Type Int

Instances

Show TypeError #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> TypeError -> ShowS # show :: TypeError -> String # showList :: [TypeError] -> ShowS #
PrettyTCM TypeError #
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: TypeError -> TCM Doc #

data LHSOrPatSyn #

Distinguish error message when parsing lhs or pattern synonym, resp.

Constructors

IsLHS
IsPatSyn

Instances

Eq LHSOrPatSyn #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: LHSOrPatSyn -> LHSOrPatSyn -> Bool # (/=) :: LHSOrPatSyn -> LHSOrPatSyn -> Bool #
Show LHSOrPatSyn #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> LHSOrPatSyn -> ShowS # show :: LHSOrPatSyn -> String # showList :: [LHSOrPatSyn] -> ShowS #

data TCErr #

Type-checking errors.

Constructors

TypeError
Fields tcErrState :: TCState The state in which the error was raised. tcErrClosErr :: Closure TypeError The environment in which the error as raised plus the error.
Exception Range Doc
IOException TCState Range IOException	The first argument is the state in which the error was raised.
PatternErr	The exception which is usually caught. Raised for pattern violations during unification (`assignV`) but also in other situations where we want to backtrack.

Instances

Show TCErr #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> TCErr -> ShowS # show :: TCErr -> String # showList :: [TCErr] -> ShowS #
Exception TCErr #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods toException :: TCErr -> SomeException # fromException :: SomeException -> Maybe TCErr # displayException :: TCErr -> String #
Error TCErr #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods noMsg :: TCErr # strMsg :: String -> TCErr #
HasRange TCErr #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: TCErr -> Range #
PrettyTCM TCErr #
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: TCErr -> TCM Doc #
MonadError TCErr IM #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods throwError :: TCErr -> IM a # catchError :: IM a -> (TCErr -> IM a) -> IM a #
MonadError TCErr TerM #
Instance details Defined in Agda.Termination.Monad Methods throwError :: TCErr -> TerM a # catchError :: TerM a -> (TCErr -> TerM a) -> TerM a #
MonadError TCErr (TCMT IO) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods throwError :: TCErr -> TCMT IO a # catchError :: TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a #

Accessing options

class (Functor m, Applicative m, Monad m) => HasOptions m where #

Minimal complete definition

pragmaOptions, commandLineOptions

Methods

pragmaOptions :: m PragmaOptions #

Returns the pragma options which are currently in effect.

commandLineOptions :: m CommandLineOptions #

Returns the command line options which are currently in effect.

Instances

HasOptions ReduceM #
Instance details Defined in Agda.TypeChecking.Reduce.Monad Methods pragmaOptions :: ReduceM PragmaOptions # commandLineOptions :: ReduceM CommandLineOptions #
HasOptions TerM #
Instance details Defined in Agda.Termination.Monad Methods pragmaOptions :: TerM PragmaOptions # commandLineOptions :: TerM CommandLineOptions #
HasOptions m => HasOptions (MaybeT m) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: MaybeT m PragmaOptions # commandLineOptions :: MaybeT m CommandLineOptions #
HasOptions m => HasOptions (ListT m) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: ListT m PragmaOptions # commandLineOptions :: ListT m CommandLineOptions #
MonadIO m => HasOptions (TCMT m) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: TCMT m PragmaOptions # commandLineOptions :: TCMT m CommandLineOptions #
HasOptions m => HasOptions (ExceptT e m) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: ExceptT e m PragmaOptions # commandLineOptions :: ExceptT e m CommandLineOptions #
HasOptions m => HasOptions (StateT s m) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: StateT s m PragmaOptions # commandLineOptions :: StateT s m CommandLineOptions #
(HasOptions m, Monoid w) => HasOptions (WriterT w m) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: WriterT w m PragmaOptions # commandLineOptions :: WriterT w m CommandLineOptions #
HasOptions m => HasOptions (ReaderT r m) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: ReaderT r m PragmaOptions # commandLineOptions :: ReaderT r m CommandLineOptions #

The reduce monad

data ReduceEnv #

Environment of the reduce monad.

Constructors

ReduceEnv
Fields redEnv :: TCEnv Read only access to environment. redSt :: TCState Read only access to state (signature, metas...).

mapRedEnv :: (TCEnv -> TCEnv) -> ReduceEnv -> ReduceEnv #

mapRedSt :: (TCState -> TCState) -> ReduceEnv -> ReduceEnv #

mapRedEnvSt :: (TCEnv -> TCEnv) -> (TCState -> TCState) -> ReduceEnv -> ReduceEnv #

reduceEnv :: Lens' TCEnv ReduceEnv #

reduceSt :: Lens' TCState ReduceEnv #

newtype ReduceM a #

Constructors

ReduceM
Fields unReduceM :: ReduceEnv -> a

Instances

Monad ReduceM #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (>>=) :: ReduceM a -> (a -> ReduceM b) -> ReduceM b # (>>) :: ReduceM a -> ReduceM b -> ReduceM b # return :: a -> ReduceM a # fail :: String -> ReduceM a #
Functor ReduceM #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fmap :: (a -> b) -> ReduceM a -> ReduceM b # (<$) :: a -> ReduceM b -> ReduceM a #
Applicative ReduceM #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pure :: a -> ReduceM a # (<>) :: ReduceM (a -> b) -> ReduceM a -> ReduceM b # liftA2 :: (a -> b -> c) -> ReduceM a -> ReduceM b -> ReduceM c # (>) :: ReduceM a -> ReduceM b -> ReduceM b # (<*) :: ReduceM a -> ReduceM b -> ReduceM a #
HasOptions ReduceM #
Instance details Defined in Agda.TypeChecking.Reduce.Monad Methods pragmaOptions :: ReduceM PragmaOptions # commandLineOptions :: ReduceM CommandLineOptions #
ReadTCState ReduceM #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTCState :: ReduceM TCState #
MonadDebug ReduceM #
Instance details Defined in Agda.TypeChecking.Reduce.Monad Methods displayDebugMessage :: Int -> String -> ReduceM () # traceDebugMessage :: Int -> String -> ReduceM a -> ReduceM a # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> ReduceM String #
HasBuiltins ReduceM #
Instance details Defined in Agda.TypeChecking.Reduce.Monad Methods getBuiltinThing :: String -> ReduceM (Maybe (Builtin PrimFun)) #
HasConstInfo ReduceM #
Instance details Defined in Agda.TypeChecking.Reduce.Monad Methods getConstInfo :: QName -> ReduceM Definition # getConstInfo' :: QName -> ReduceM (Either SigError Definition) # getRewriteRulesFor :: QName -> ReduceM RewriteRules #
MonadReader TCEnv ReduceM #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods ask :: ReduceM TCEnv # local :: (TCEnv -> TCEnv) -> ReduceM a -> ReduceM a # reader :: (TCEnv -> a) -> ReduceM a #

onReduceEnv :: (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a #

fmapReduce :: (a -> b) -> ReduceM a -> ReduceM b #

apReduce :: ReduceM (a -> b) -> ReduceM a -> ReduceM b #

bindReduce :: ReduceM a -> (a -> ReduceM b) -> ReduceM b #

runReduceM :: ReduceM a -> TCM a #

runReduceF :: (a -> ReduceM b) -> TCM (a -> b) #

Type checking monad transformer

newtype TCMT m a #

Constructors

TCM
Fields unTCM :: IORef TCState -> TCEnv -> m a

Instances

MonadTrans TCMT #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods lift :: Monad m => m a -> TCMT m a #
MonadError TCErr IM #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods throwError :: TCErr -> IM a # catchError :: IM a -> (TCErr -> IM a) -> IM a #
MonadBench Phase TCM #	We store benchmark statistics in an IORef. This enables benchmarking pure computation, see Agda.Benchmarking.
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getBenchmark :: TCM (Benchmark Phase) # getsBenchmark :: (Benchmark Phase -> c) -> TCM c # putBenchmark :: Benchmark Phase -> TCM () # modifyBenchmark :: (Benchmark Phase -> Benchmark Phase) -> TCM () # finally :: TCM b -> TCM c -> TCM b #
Conversion TOM Clause (Maybe ([Pat O], MExp O)) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) #
Conversion TOM Type (MExp O) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Type -> TOM (MExp O) #
Conversion TOM Term (MExp O) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Term -> TOM (MExp O) #
Conversion TOM Args (MM (ArgList O) (RefInfo O)) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) #
MonadIO m => MonadState TCState (TCMT m) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods get :: TCMT m TCState # put :: TCState -> TCMT m () # state :: (TCState -> (a, TCState)) -> TCMT m a #
MonadIO m => MonadReader TCEnv (TCMT m) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods ask :: TCMT m TCEnv # local :: (TCEnv -> TCEnv) -> TCMT m a -> TCMT m a # reader :: (TCEnv -> a) -> TCMT m a #
MonadError TCErr (TCMT IO) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods throwError :: TCErr -> TCMT IO a # catchError :: TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a #
Conversion TOM [Clause] [([Pat O], MExp O)] #
Instance details Defined in Agda.Auto.Convert Methods convert :: [Clause] -> TOM [([Pat O], MExp O)] #
Conversion TOM (Arg Pattern) (Pat O) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Arg Pattern -> TOM (Pat O) #
Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Arg a -> TOM (Hiding, b) #
MonadIO m => Monad (TCMT m) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (>>=) :: TCMT m a -> (a -> TCMT m b) -> TCMT m b # (>>) :: TCMT m a -> TCMT m b -> TCMT m b # return :: a -> TCMT m a # fail :: String -> TCMT m a #
MonadIO m => Functor (TCMT m) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fmap :: (a -> b) -> TCMT m a -> TCMT m b # (<$) :: a -> TCMT m b -> TCMT m a #
MonadIO m => Applicative (TCMT m) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pure :: a -> TCMT m a # (<>) :: TCMT m (a -> b) -> TCMT m a -> TCMT m b # liftA2 :: (a -> b -> c) -> TCMT m a -> TCMT m b -> TCMT m c # (>) :: TCMT m a -> TCMT m b -> TCMT m b # (<*) :: TCMT m a -> TCMT m b -> TCMT m a #
Semigroup (TCM Any) #	Short-cutting disjunction forms a monoid.
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (<>) :: TCM Any -> TCM Any -> TCM Any # sconcat :: NonEmpty (TCM Any) -> TCM Any # stimes :: Integral b => b -> TCM Any -> TCM Any #
Monoid (TCM Any) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods mempty :: TCM Any # mappend :: TCM Any -> TCM Any -> TCM Any # mconcat :: [TCM Any] -> TCM Any #
MonadIO m => MonadIO (TCMT m) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftIO :: IO a -> TCMT m a #
Null (TCM Doc) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: TCM Doc # null :: TCM Doc -> Bool #
MonadIO m => MonadTCM (TCMT m) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftTCM :: TCM a -> TCMT m a #
MonadIO m => HasOptions (TCMT m) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: TCMT m PragmaOptions # commandLineOptions :: TCMT m CommandLineOptions #
MonadIO m => ReadTCState (TCMT m) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getTCState :: TCMT m TCState #
MonadIO m => MonadDebug (TCMT m) #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods displayDebugMessage :: Int -> String -> TCMT m () # traceDebugMessage :: Int -> String -> TCMT m a -> TCMT m a # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> TCMT m String #
MonadIO m => HasBuiltins (TCMT m) #
Instance details Defined in Agda.TypeChecking.Monad.Builtin Methods getBuiltinThing :: String -> TCMT m (Maybe (Builtin PrimFun)) #
HasConstInfo (TCMT IO) #
Instance details Defined in Agda.TypeChecking.Monad.Signature Methods getConstInfo :: QName -> TCMT IO Definition # getConstInfo' :: QName -> TCMT IO (Either SigError Definition) # getRewriteRulesFor :: QName -> TCMT IO RewriteRules #

type TCM = TCMT IO #

class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm, HasOptions tcm) => MonadTCM tcm where #

Minimal complete definition

liftTCM

Methods

liftTCM :: TCM a -> tcm a #

Instances

MonadTCM TerM #
Instance details Defined in Agda.Termination.Monad Methods liftTCM :: TCM a -> TerM a #
MonadTCM tcm => MonadTCM (MaybeT tcm) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftTCM :: TCM a -> MaybeT tcm a #
MonadTCM tcm => MonadTCM (ListT tcm) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftTCM :: TCM a -> ListT tcm a #
MonadIO m => MonadTCM (TCMT m) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftTCM :: TCM a -> TCMT m a #
MonadTCM tcm => MonadTCM (ExceptT err tcm) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftTCM :: TCM a -> ExceptT err tcm a #
(Monoid w, MonadTCM tcm) => MonadTCM (WriterT w tcm) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods liftTCM :: TCM a -> WriterT w tcm a #

type IM = TCMT (InputT IO) #

Interaction monad.

runIM :: IM a -> TCM a #

catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a #

Preserve the state of the failing computation.

finally_ :: TCM a -> TCM b -> TCM a #

Execute a finalizer even when an exception is thrown. Does not catch any errors. In case both the regular computation and the finalizer throw an exception, the one of the finalizer is propagated.

mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a #

pureTCM :: MonadIO m => (TCState -> TCEnv -> a) -> TCMT m a #

returnTCMT :: MonadIO m => a -> TCMT m a #

bindTCMT :: MonadIO m => TCMT m a -> (a -> TCMT m b) -> TCMT m b #

thenTCMT :: MonadIO m => TCMT m a -> TCMT m b -> TCMT m b #

fmapTCMT :: MonadIO m => (a -> b) -> TCMT m a -> TCMT m b #

apTCMT :: MonadIO m => TCMT m (a -> b) -> TCMT m a -> TCMT m b #

patternViolation :: TCM a #

internalError :: MonadTCM tcm => String -> tcm a #

genericError :: MonadTCM tcm => String -> tcm a #

genericDocError :: MonadTCM tcm => Doc -> tcm a #

typeError :: MonadTCM tcm => TypeError -> tcm a #

typeError_ :: MonadTCM tcm => TypeError -> tcm TCErr #

runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState) #

Running the type checking monad (most general form).

runTCMTop :: TCM a -> IO (Either TCErr a) #

Running the type checking monad on toplevel (with initial state).

runTCMTop' :: MonadIO m => TCMT m a -> m a #

runSafeTCM :: TCM a -> TCState -> IO (a, TCState) #

runSafeTCM runs a safe TCM action (a TCM action which cannot fail) in the initial environment.

forkTCM :: TCM a -> TCM () #

Runs the given computation in a separate thread, with a copy of the current state and environment.

Note that Agda sometimes uses actual, mutable state. If the computation given to forkTCM tries to modify this state, then bad things can happen, because accesses are not mutually exclusive. The forkTCM function has been added mainly to allow the thread to read (a snapshot of) the current state in a convenient way.

Note also that exceptions which are raised in the thread are not propagated to the parent, so the thread should not do anything important.

extendedLambdaName :: String #

Base name for extended lambda patterns

absurdLambdaName :: String #

Name of absurdLambda definitions.

isAbsurdLambdaName :: QName -> Bool #

Check whether we have an definition from an absurd lambda.

Functor Closure #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fmap :: (a -> b) -> Closure a -> Closure b # (<$) :: a -> Closure b -> Closure a #
Foldable Closure #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods fold :: Monoid m => Closure m -> m # foldMap :: Monoid m => (a -> m) -> Closure a -> m # foldr :: (a -> b -> b) -> b -> Closure a -> b # foldr' :: (a -> b -> b) -> b -> Closure a -> b # foldl :: (b -> a -> b) -> b -> Closure a -> b # foldl' :: (b -> a -> b) -> b -> Closure a -> b # foldr1 :: (a -> a -> a) -> Closure a -> a # foldl1 :: (a -> a -> a) -> Closure a -> a # toList :: Closure a -> [a] # null :: Closure a -> Bool # length :: Closure a -> Int # elem :: Eq a => a -> Closure a -> Bool # maximum :: Ord a => Closure a -> a # minimum :: Ord a => Closure a -> a # sum :: Num a => Closure a -> a # product :: Num a => Closure a -> a #
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) #
Instance details Defined in Agda.Interaction.BasicOps Methods reify :: ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) # reifyWhen :: Bool -> ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) #
Data a => Data (Closure a) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Closure a -> c (Closure a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Closure a) # toConstr :: Closure a -> Constr # dataTypeOf :: Closure a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Closure a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Closure a)) # gmapT :: (forall b. Data b => b -> b) -> Closure a -> Closure a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Closure a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Closure a -> r # gmapQ :: (forall d. Data d => d -> u) -> Closure a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Closure a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Closure a -> m (Closure a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Closure a -> m (Closure a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Closure a -> m (Closure a) #
Show a => Show (Closure a) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Closure a -> ShowS # show :: Closure a -> String # showList :: [Closure a] -> ShowS #
HasRange a => HasRange (Closure a) #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getRange :: Closure a -> Range #
PrettyTCM a => PrettyTCM (Closure a) #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Closure a -> TCM Doc #
MentionsMeta a => MentionsMeta (Closure a) #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMeta :: MetaId -> Closure a -> Bool #
InstantiateFull a => InstantiateFull (Closure a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Closure a -> ReduceM (Closure a) #
Normalise a => Normalise (Closure a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Closure a -> ReduceM (Closure a) #
Simplify a => Simplify (Closure a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Closure a -> ReduceM (Closure a) #
Reduce a => Reduce (Closure a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Closure a -> ReduceM (Closure a) # reduceB' :: Closure a -> ReduceM (Blocked (Closure a)) #
Instantiate a => Instantiate (Closure a) #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Closure a -> ReduceM (Closure a) #

Closure
Fields clSignature :: Signature clEnv :: TCEnv clScope :: ScopeInfo clModuleCheckpoints :: Map ModuleName CheckpointId clValue :: a

Type checking state

st-prefixed lenses

Fresh things

Managing file names

Interface

Closure

Constraints

Open things

Judgements

Meta variables

Interaction meta variables

Signature

Injectivity

Mutual blocks

Statistics

Trace

Instance table

Builtin things

Highlighting levels

Type checking environment

e-prefixed lenses

Context

Let bindings

Abstract mode

Insertion of implicit arguments

Type checking warnings (aka non-fatal errors)

Type checking errors

Accessing options

The reduce monad

Type checking monad transformer

KillRange instances