Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Rules.Decl

Contents

- Debugging

Synopsis

- checkDeclCached :: Declaration -> TCM ()
- checkDecls :: [Declaration] -> TCM ()
- checkDecl :: Declaration -> TCM ()
- mutualChecks :: MutualInfo -> Declaration -> [Declaration] -> MutualId -> Set QName -> TCM ()
- revisitRecordPatternTranslation :: [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 ()
- data HighlightModuleContents
  - = DontHightlightModuleContents
  - | DoHighlightModuleContents
- highlight_ :: HighlightModuleContents -> Declaration -> TCM ()
- checkTermination_ :: Declaration -> TCM ()
- checkPositivity_ :: MutualInfo -> Set QName -> TCM ()
- checkInjectivity_ :: Set QName -> TCM ()
- checkProjectionLikeness_ :: Set QName -> TCM ()
- whenAbstractFreezeMetasAfter :: DefInfo -> TCM a -> TCM a
- checkGeneralize :: Set QName -> DefInfo -> ArgInfo -> QName -> Expr -> TCM ()
- checkAxiom :: KindOfName -> DefInfo -> ArgInfo -> Maybe PragmaPolarities -> QName -> Expr -> TCM ()
- checkAxiom' :: Maybe GeneralizeTelescope -> KindOfName -> DefInfo -> ArgInfo -> Maybe PragmaPolarities -> QName -> Expr -> TCM ()
- checkPrimitive :: DefInfo -> QName -> Arg Expr -> TCM ()
- checkPragma :: Range -> Pragma -> TCM ()
- checkMutual :: MutualInfo -> [Declaration] -> TCM (MutualId, Set QName)
- checkSig :: KindOfName -> DefInfo -> Erased -> QName -> GeneralizeTelescope -> Expr -> TCM ()
- checkTypeSignature :: TypeSignature -> TCM ()
- checkTypeSignature' :: Maybe GeneralizeTelescope -> TypeSignature -> TCM ()
- checkSection :: Erased -> ModuleName -> GeneralizeTelescope -> [Declaration] -> TCM ()
- checkModuleArity :: ModuleName -> Telescope -> [NamedArg Expr] -> TCM Telescope
- checkSectionApplication :: ModuleInfo -> Erased -> ModuleName -> ModuleApplication -> ScopeCopyInfo -> ImportDirective -> TCM ()
- checkSectionApplication' :: ModuleInfo -> Erased -> ModuleName -> ModuleApplication -> ScopeCopyInfo -> TCM ()
- checkImportDirective :: ImportDirective -> TCM ()
- class ShowHead a where
  - showHead :: a -> String
- 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 #

revisitRecordPatternTranslation :: [QName] -> TCM () Source #

Check if there is a inferred eta record type in the mutual block. If yes, repeat the record pattern translation for all function definitions in the block. This is necessary since the original record pattern translation will have skipped record patterns of the new record types (as eta was off for them). See issue #2308 (and #2197).

type FinalChecks = Maybe (TCM ()) Source #

checkUnquoteDecl :: MutualInfo -> [DefInfo] -> [QName] -> Expr -> TCM FinalChecks Source #

checkUnquoteDef :: [DefInfo] -> [QName] -> Expr -> TCM () 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.

data HighlightModuleContents Source #

Constructors

DontHightlightModuleContents |
DoHighlightModuleContents |

#### Instances

Instances details

Eq HighlightModuleContents Source # |
Instance details Defined in Agda.TypeChecking.Rules.Decl Methods (==) :: HighlightModuleContents -> HighlightModuleContents -> Bool Source # (/=) :: HighlightModuleContents -> HighlightModuleContents -> Bool Source #

highlight_ :: HighlightModuleContents -> Declaration -> TCM () Source #

Highlight a declaration. Called after checking a mutual block (to ensure we have the right definitions for all names). For modules inside mutual blocks we haven't highlighted their contents, but for modules not in a mutual block we have. Hence the flag.

checkTermination_ :: Declaration -> TCM () Source #

Termination check a declaration.

checkPositivity_ :: MutualInfo -> Set QName -> TCM () Source #

Check a set of mutual names for positivity.

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.

whenAbstractFreezeMetasAfter :: DefInfo -> TCM a -> TCM a Source #

Freeze metas created by given computation if in abstract mode.

checkGeneralize :: Set QName -> DefInfo -> ArgInfo -> QName -> Expr -> TCM () Source #

checkAxiom :: KindOfName -> DefInfo -> ArgInfo -> Maybe PragmaPolarities -> QName -> Expr -> TCM () Source #

Type check an axiom.

checkAxiom' :: Maybe GeneralizeTelescope -> KindOfName -> DefInfo -> ArgInfo -> Maybe PragmaPolarities -> QName -> Expr -> TCM () Source #

Data and record type signatures need to remember the generalized parameters for when checking the corresponding definition, so for these we pass in the parameter telescope separately.

checkPrimitive :: DefInfo -> QName -> Arg Expr -> TCM () Source #

Type check a primitive function declaration.

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.

checkSig :: KindOfName -> DefInfo -> Erased -> QName -> GeneralizeTelescope -> Expr -> TCM () Source #

checkTypeSignature :: TypeSignature -> TCM () Source #

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

checkTypeSignature' :: Maybe GeneralizeTelescope -> TypeSignature -> TCM () Source #

checkSection :: Erased -> ModuleName -> GeneralizeTelescope -> [Declaration] -> TCM () Source #

Type check a module.

checkModuleArity Source #

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 |
-> Erased | Should "everything" be treated as erased?
-> ModuleName | Name `m1` of module defined by the module macro.
-> ModuleApplication | The module macro `λ tel → m2 args`.
-> ScopeCopyInfo | Imported names and modules
-> ImportDirective |
-> TCM () |

Check an application of a section.

checkSectionApplication' Source #

Arguments

:: ModuleInfo |
-> Erased |
-> ModuleName | Name `m1` of module defined by the module macro.
-> ModuleApplication | The module macro `λ tel → m2 args`.
-> ScopeCopyInfo | Imported names and modules
-> TCM () |

Check an application of a section. (Do not invoke this procedure directly, use `checkSectionApplication`.)

checkImportDirective :: ImportDirective -> TCM () Source #

Checks that `open public` is not used in hard compile-time mode.

# Debugging

class ShowHead a where Source #

Methods

showHead :: a -> String Source #

#### Instances

Instances details

ShowHead Declaration Source # |
Instance details Defined in Agda.TypeChecking.Rules.Decl Methods showHead :: Declaration -> String Source #

debugPrintDecl :: Declaration -> TCM () Source #