| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.TypeChecking.Rules.Decl
Contents
- checkDeclCached :: Declaration -> TCM ()
- checkDecls :: [Declaration] -> TCM ()
- checkDecl :: Declaration -> TCM ()
- mutualChecks :: MutualInfo -> Declaration -> [Declaration] -> MutualId -> Set QName -> TCM ()
- type FinalChecks = Maybe (TCM ())
- checkUnquoteDecl :: MutualInfo -> [DefInfo] -> [QName] -> Expr -> TCM FinalChecks
- checkUnquoteDef :: [DefInfo] -> [QName] -> Expr -> TCM ()
- unquoteTop :: [QName] -> Expr -> TCM [QName]
- instantiateDefinitionType :: QName -> TCM ()
- highlight_ :: Declaration -> TCM ()
- checkTermination_ :: MutualId -> Declaration -> TCM ()
- checkPositivity_ :: MutualInfo -> Set QName -> TCM ()
- checkCoinductiveRecords :: [Declaration] -> TCM ()
- checkInjectivity_ :: Set QName -> TCM ()
- checkProjectionLikeness_ :: Set QName -> TCM ()
- checkAxiom :: Axiom -> DefInfo -> ArgInfo -> QName -> Expr -> TCM ()
- checkPrimitive :: DefInfo -> QName -> Expr -> TCM ()
- assertCurrentModule :: QName -> String -> TCM ()
- checkPragma :: Range -> Pragma -> TCM ()
- checkMutual :: MutualInfo -> [Declaration] -> TCM (MutualId, Set QName)
- checkTypeSignature :: TypeSignature -> TCM ()
- checkSection :: ModuleInfo -> ModuleName -> Telescope -> [Declaration] -> TCM ()
- checkModuleArity :: ModuleName -> Telescope -> [NamedArg Expr] -> TCM Telescope
- checkSectionApplication :: ModuleInfo -> ModuleName -> ModuleApplication -> Ren QName -> Ren ModuleName -> TCM ()
- checkSectionApplication' :: ModuleInfo -> ModuleName -> ModuleApplication -> Ren QName -> Ren ModuleName -> TCM ()
- checkImport :: ModuleInfo -> ModuleName -> TCM ()
- class ShowHead a where
- debugPrintDecl :: Declaration -> TCM ()
Documentation
checkDeclCached :: Declaration -> TCM () Source
Cached checkDecl
checkDecls :: [Declaration] -> TCM () Source
Type check a sequence of declarations.
checkDecl :: Declaration -> TCM () Source
Type check a single declaration.
mutualChecks :: MutualInfo -> Declaration -> [Declaration] -> MutualId -> Set QName -> TCM () Source
type FinalChecks = Maybe (TCM ()) Source
checkUnquoteDecl :: MutualInfo -> [DefInfo] -> [QName] -> Expr -> TCM FinalChecks Source
unquoteTop :: [QName] -> Expr -> TCM [QName] Source
Run a reflected TCM computatation expected to define a given list of names.
instantiateDefinitionType :: QName -> TCM () Source
Instantiate all metas in Definition associated to QName.
Makes sense after freezing metas. Some checks, like free variable
analysis, are not in TCM, so they will be more precise (see issue 1099)
after meta instantiation.
Precondition: name has been added to signature already.
highlight_ :: Declaration -> TCM () Source
Highlight a declaration.
checkTermination_ :: MutualId -> Declaration -> TCM () Source
Termination check a declaration.
checkPositivity_ :: MutualInfo -> Set QName -> TCM () Source
Check a set of mutual names for positivity.
checkCoinductiveRecords :: [Declaration] -> TCM () Source
Check that all coinductive records are actually recursive. (Otherwise, one can implement invalid recursion schemes just like for the old coinduction.)
checkInjectivity_ :: Set QName -> TCM () Source
Check a set of mutual names for constructor-headedness.
checkProjectionLikeness_ :: Set QName -> TCM () Source
Check a set of mutual names for projection likeness.
Only a single, non-abstract function can be projection-like. Making an abstract function projection-like would break the invariant that the type of the principle argument of a projection-like function is always inferable.
checkPrimitive :: DefInfo -> QName -> Expr -> TCM () Source
Type check a primitive function declaration.
assertCurrentModule :: QName -> String -> TCM () Source
checkPragma :: Range -> Pragma -> TCM () Source
Check a pragma.
checkMutual :: MutualInfo -> [Declaration] -> TCM (MutualId, Set QName) Source
Type check a bunch of mutual inductive recursive definitions.
All definitions which have so far been assigned to the given mutual block are returned.
checkTypeSignature :: TypeSignature -> TCM () Source
Type check the type signature of an inductive or recursive definition.
checkSection :: ModuleInfo -> ModuleName -> Telescope -> [Declaration] -> TCM () Source
Type check a module.
Arguments
| :: ModuleName | Name of applied module. |
| -> Telescope | The module parameters. |
| -> [NamedArg Expr] | The arguments this module is applied to. |
| -> TCM Telescope | The remaining module parameters (has free de Bruijn indices!). |
Helper for checkSectionApplication.
Matches the arguments of the module application with the module parameters.
Returns the remaining module parameters as an open telescope. Warning: the returned telescope is not the final result, an actual instantiation of the parameters does not occur.
checkSectionApplication Source
Arguments
| :: ModuleInfo | |
| -> ModuleName | Name |
| -> ModuleApplication | The module macro |
| -> Ren QName | Imported names (given as renaming). |
| -> Ren ModuleName | Imported modules (given as renaming). |
| -> TCM () |
Check an application of a section (top-level function, includes traceCall
checkSectionApplication' Source
Arguments
| :: ModuleInfo | |
| -> ModuleName | Name |
| -> ModuleApplication | The module macro |
| -> Ren QName | Imported names (given as renaming). |
| -> Ren ModuleName | Imported modules (given as renaming). |
| -> TCM () |
Check an application of a section.
checkImport :: ModuleInfo -> ModuleName -> TCM () Source
Type check an import declaration. Actually doesn't do anything, since all the work is done when scope checking.
Debugging
Instances
debugPrintDecl :: Declaration -> TCM () Source