Agda.TypeChecking.Rules.Decl

Documentation

checkDecls :: [Declaration] -> TCM ()

Type check a sequence of declarations.

checkDecl :: Declaration -> TCM ()

Type check a single declaration.

instantiateDefinitionType :: QName -> TCM ()

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.

checkTermination_ :: Declaration -> TCM [TerminationError]

Termination check a declaration and return a list of termination errors.

checkPositivity_ :: Set QName -> TCM ()

Check a set of mutual names for positivity.

checkCoinductiveRecords :: [Declaration] -> TCM ()

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 ()

Check a set of mutual names for constructor-headedness.

checkProjectionLikeness_ :: Set QName -> TCM ()

Check a set of mutual names for projection likeness.

checkAxiom :: Axiom -> DefInfo -> ArgInfo -> QName -> Expr -> TCM ()

Type check an axiom.

checkPrimitive :: DefInfo -> QName -> Expr -> TCM ()

Type check a primitive function declaration.

checkPragma :: Range -> Pragma -> TCM ()

Check a pragma.

checkMutual :: MutualInfo -> [Declaration] -> TCM (Set QName)

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 ()

Type check the type signature of an inductive or recursive definition.

checkSection :: ModuleInfo -> ModuleName -> Telescope -> [Declaration] -> TCM ()

Type check a module.

checkModuleArity

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

Arguments

:: ModuleInfo

-> ModuleName

Name m1 of module defined by the module macro.

-> ModuleApplication

The module macro λ tel → m2 ar.

-> Map QName QName

Imported names (given as renaming).

-> Map ModuleName ModuleName

Imported modules (given as renaming).

-> TCM ()

Check an application of a section (top-level function, includes traceCall).

checkSectionApplication'

Arguments

:: ModuleInfo

-> ModuleName

Name m1 of module defined by the module macro.

-> ModuleApplication

The module macro λ tel → m2 ar.

-> Map QName QName

Imported names (given as renaming).

-> Map ModuleName ModuleName

Imported modules (given as renaming).

-> TCM ()

Check an application of a section.

checkImport :: ModuleInfo -> ModuleName -> TCM ()

Type check an import declaration. Actually doesn't do anything, since all the work is done when scope checking.