Safe Haskell | None |
---|---|
Language | Haskell98 |
- checkDecls :: [Declaration] -> TCM ()
- checkDecl :: Declaration -> TCM ()
- mutualChecks :: MutualInfo -> Declaration -> [Declaration] -> Set QName -> TCM ()
- type FinalChecks = Maybe (TCM ())
- checkUnquoteDecl :: MutualInfo -> DefInfo -> QName -> Expr -> TCM FinalChecks
- instantiateDefinitionType :: QName -> TCM ()
- highlight_ :: Declaration -> TCM ()
- checkTermination_ :: Declaration -> TCM ()
- checkPositivity_ :: 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 ()
- checkPragma :: Range -> Pragma -> TCM ()
- checkMutual :: MutualInfo -> [Declaration] -> TCM (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
checkDecls :: [Declaration] -> TCM () Source
Type check a sequence of declarations.
checkDecl :: Declaration -> TCM () Source
Type check a single declaration.
mutualChecks :: MutualInfo -> Declaration -> [Declaration] -> Set QName -> TCM () Source
type FinalChecks = Maybe (TCM ()) Source
checkUnquoteDecl :: MutualInfo -> DefInfo -> QName -> Expr -> TCM FinalChecks Source
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_ :: Declaration -> TCM () Source
Termination check a declaration.
checkPositivity_ :: 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.
checkPragma :: Range -> Pragma -> TCM () Source
Check a pragma.
checkMutual :: MutualInfo -> [Declaration] -> TCM (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.
:: 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
:: 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
:: 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
debugPrintDecl :: Declaration -> TCM () Source