Documentation

Fields

• unTCM :: IORef TCState -> TCEnv -> m a
   

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.

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]

  The module stack with the entry being the top-level module as Agda chases modules. It will be empty if there is no main module, will have a single entry for the top level module, or more when descending past the main module. This is used to detect import cycles and in some cases highlighting behavior. 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.

• envMutualBlock :: Maybe MutualId

  the current (if any) mutual block

• envTerminationCheck :: TerminationCheck ()

  are we inside the scope of a termination pragma

• envCoverageCheck :: CoverageCheck

  are we inside the scope of a coverage pragma

• envMakeCase :: Bool

  are we inside a make-case (if so, ignore forcing analysis in unifier)

• 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.

• envModality :: Modality

  Relevance component: Are we checking an irrelevant argument? (=Irrelevant) Then top-level irrelevant declarations are enabled. Other value: Relevant, then only relevant decls. are available.

  Quantity component: Are we checking a runtime-irrelevant thing? (=Quantity0) Then runtime-irrelevant things are usable. Other value: Quantity1, runtime relevant. Quantityω is not allowed here, see Bob Atkey, LiCS 2018.

• envSplitOnStrict :: Bool

  Are we currently case-splitting on a strict datatype (i.e. in SSet)? If yes, the pattern-matching unifier will solve reflexive equations even --without-K.

• 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
   
• 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
   
• envReduceDefs :: ReduceDefs
   
• envReconstructed :: Bool
   
• envInjectivityDepth :: Int

  Injectivity can cause non-termination for unsolvable contraints (#431, #3067). Keep a limit on the nesting depth of injectivity uses.

• envCompareBlocked :: Bool

  When True, the conversion checker will consider all term constructors as injective, including blocked function applications and metas. Warning: this should only be used when not assigning any metas (e.g. when envAssignMetas is False or when running pureEqualTerms) or else we get non-unique meta solutions.

• 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.

• envGeneralizeMetas :: DoGeneralize

  Should new metas generalized over.

• envGeneralizedVars :: Map QName GeneralizedValue

  Values for used generalizable variables.

• envActiveBackendName :: Maybe BackendName

  Is some backend active at the moment, and if yes, which? NB: we only store the BackendName here, otherwise instance Data TCEnv is not derivable. The actual backend can be obtained from the name via stBackends.

• envConflComputingOverlap :: Bool

  Are we currently computing the overlap between two rewrite rules for the purpose of confluence checking?

• envCurrentlyElaborating :: Bool

  Are we currently in the process of executing an elaborate-and-give interactive command?