|
Agda.TypeChecking.Monad.Base |
|
|
|
|
|
Synopsis |
|
|
|
|
Type checking state
|
|
|
|
|
|
|
|
|
|
|
|
Interface
|
|
|
Constructors | ModuleInfo | | miInterface :: Interface | | miWarnings :: Bool | True if warnings were encountered when the module was type
checked.
| miTimeStamp :: ClockTime | The modification time stamp of the interface file when the
interface was read or written. Alternatively, if warnings were
encountered (in which case there may not be any up-to-date
interface file), the time at which the interface was produced
(approximately).
|
|
|
|
|
|
|
|
|
|
|
|
Closure
|
|
|
|
|
|
|
Constraints
|
|
|
|
|
|
|
|
|
|
|
|
Open things
|
|
|
A thing tagged with the context it came from.
| Constructors | |
|
|
Judgements
|
|
|
|
|
Meta variables
|
|
|
|
|
|
|
|
|
|
|
|
TODO: Not so nice.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Interaction meta variables
|
|
|
|
|
|
|
Signature
|
|
|
|
|
|
|
|
|
|
Constructors | Section | | secTelescope :: Telescope | | secFreeVars :: Nat | This is the number of parameters when
we're inside the section and 0
outside. It's used to know how much of
the context to apply function from the
section to when translating from
abstract to internal syntax.
|
|
|
|
|
|
|
|
Constructors | Display Nat [Term] DisplayTerm | The three arguments are:
- n: number of free variables;
- Patterns for arguments, one extra free var which
represents pattern vars. There should n of them.
- Display form. n free variables.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
data HaskellRepresentation | Source |
|
|
|
|
Constructors | Covariant | | Contravariant | | Invariant | |
|
|
|
|
Positive means strictly positive and Negative means not strictly
positive.
| Constructors | |
|
|
|
Constructors | Axiom | | | Function | | | Datatype | | | Record | | | Constructor | | | Primitive | Primitive or builtin functions.
| |
|
|
|
|
|
|
|
Constructors | NoReduction no | | YesReduction yes | |
|
|
|
|
|
|
|
|
|
Used to specify whether something should be delayed.
| Constructors | |
|
|
|
Are the clauses of this definition delayed?
|
|
|
|
Injectivity
|
|
|
|
|
|
Constructors | SortHead | | PiHead | | ConHead QName | |
|
|
|
Mutual blocks
|
|
|
|
|
Statistics
|
|
|
|
Trace
|
|
|
|
|
|
|
|
|
Builtin things
|
|
|
|
|
|
|
Type checking environment
|
|
|
Constructors | TCEnv | | envContext :: Context | | envLetBindings :: LetBindings | | envCurrentModule :: ModuleName | | 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
| 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.
| envReplace :: Bool | Coinductive constructor applications c args get
replaced by a function application f tel, where
tel corresponds to the current telescope and f is
defined as f tel = c args. The initial occurrence
of c in the body of f should not be replaced by
yet another function application, though. To avoid
that this happens the envReplace flag is set to
False when f is checked.
| envDisplayFormsEnabled :: Bool | Sometimes we want to disable display forms.
| envReifyInteractionPoints :: Bool | should we try to recover interaction points when reifying?
disabled when generating types for with functions
|
|
|
|
|
|
|
Context
|
|
|
|
|
|
|
|
|
|
Let bindings
|
|
|
|
Abstract mode
|
|
|
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
|
|
|
|
Type checking errors
|
|
|
|
|
|
|
|
|
|
|
|
Type-checking errors.
| Constructors | |
|
|
|
Type-checking errors, potentially paired with relevant syntax
highlighting information.
| Constructors | |
|
|
Type checking monad transformer
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Running the type checking monad
|
|
|
|
Produced by Haddock version 2.6.0 |