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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Rules.Def

Contents

- Definitions by pattern matching
- Info that is needed after all clauses have been processed.

Synopsis

- checkFunDef :: Delayed -> DefInfo -> QName -> [Clause] -> TCM ()
- checkMacroType :: Type -> TCM ()
- isAlias :: [Clause] -> Type -> Maybe (Expr, Maybe Expr, MetaId)
- checkAlias :: Type -> ArgInfo -> Delayed -> DefInfo -> QName -> Expr -> Maybe Expr -> TCM ()
- checkFunDef' :: Type -> ArgInfo -> Delayed -> Maybe ExtLamInfo -> Maybe QName -> DefInfo -> QName -> [Clause] -> TCM ()
- checkFunDefS :: Type -> ArgInfo -> Delayed -> Maybe ExtLamInfo -> Maybe QName -> DefInfo -> QName -> Maybe Substitution -> [Clause] -> TCM ()
- useTerPragma :: Definition -> TCM Definition
- mapLHSCores :: (LHSCore -> LHSCore) -> RHS -> RHS
- insertNames :: [Arg (Maybe BindName)] -> RHS -> RHS
- insertInspects :: [Arg (Maybe BindName)] -> LHSCore -> LHSCore
- insertPatterns :: [Arg Pattern] -> RHS -> RHS
- insertPatternsLHSCore :: [Arg Pattern] -> LHSCore -> LHSCore
- data WithFunctionProblem
  - = NoWithFunction
  - | WithFunction {
    - wfParentName :: QName
    - wfName :: QName
    - wfParentType :: Type
    - wfParentTel :: Telescope
    - wfBeforeTel :: Telescope
    - wfAfterTel :: Telescope
    - wfExprs :: [Arg (Term, EqualityView)]
    - wfRHSType :: Type
    - wfParentPats :: [NamedArg DeBruijnPattern]
    - wfParentParams :: Nat
    - wfPermSplit :: Permutation
    - wfPermParent :: Permutation
    - wfPermFinal :: Permutation
    - wfClauses :: [Clause]
    - wfCallSubst :: Substitution
    }
- checkSystemCoverage :: QName -> [Int] -> Type -> [Clause] -> TCM System
- data ClausesPostChecks = CPC {
  - cpcPartialSplits :: IntSet
  }
- checkClauseLHS :: Type -> Maybe Substitution -> SpineClause -> (LHSResult -> TCM a) -> TCM a
- checkClause :: Type -> Maybe Substitution -> SpineClause -> TCM (Clause, ClausesPostChecks)
- getReflPattern :: TCM Pattern
- checkRHS :: LHSInfo -> QName -> [NamedArg Pattern] -> Type -> LHSResult -> RHS -> TCM (Maybe Term, WithFunctionProblem)
- checkWithRHS :: QName -> QName -> Type -> LHSResult -> [Arg (Term, EqualityView)] -> [Clause] -> TCM (Maybe Term, WithFunctionProblem)
- checkWithFunction :: [Name] -> WithFunctionProblem -> TCM (Maybe Term)
- checkWhere :: WhereDeclarations -> TCM a -> TCM a
- newSection :: ModuleName -> GeneralizeTelescope -> TCM a -> TCM a
- atClause :: QName -> Int -> Type -> Maybe Substitution -> SpineClause -> TCM a -> TCM a

# Definitions by pattern matching

checkFunDef :: Delayed -> DefInfo -> QName -> [Clause] -> TCM () Source #

checkMacroType :: Type -> TCM () Source #

isAlias :: [Clause] -> Type -> Maybe (Expr, Maybe Expr, MetaId) Source #

A single clause without arguments and without type signature is an alias.

checkAlias :: Type -> ArgInfo -> Delayed -> DefInfo -> QName -> Expr -> Maybe Expr -> TCM () Source #

Check a trivial definition of the form `f = e`

checkFunDef' Source #

Arguments

:: Type | the type we expect the function to have
-> ArgInfo | is it irrelevant (for instance)
-> Delayed | are the clauses delayed (not unfolded willy-nilly)
-> Maybe ExtLamInfo | does the definition come from an extended lambda (if so, we need to know some stuff about lambda-lifted args)
-> Maybe QName | is it a with function (if so, what's the name of the parent function)
-> DefInfo | range info
-> QName | the name of the function
-> [Clause] | the clauses to check
-> TCM () |

Type check a definition by pattern matching.

checkFunDefS Source #

Arguments

:: Type | the type we expect the function to have
-> ArgInfo | is it irrelevant (for instance)
-> Delayed | are the clauses delayed (not unfolded willy-nilly)
-> Maybe ExtLamInfo | does the definition come from an extended lambda (if so, we need to know some stuff about lambda-lifted args)
-> Maybe QName | is it a with function (if so, what's the name of the parent function)
-> DefInfo | range info
-> QName | the name of the function
-> Maybe Substitution | substitution (from with abstraction) that needs to be applied to module parameters
-> [Clause] | the clauses to check
-> TCM () |

Type check a definition by pattern matching.

useTerPragma :: Definition -> TCM Definition Source #

Set `funTerminates` according to termination info in `TCEnv`, which comes from a possible termination pragma.

mapLHSCores :: (LHSCore -> LHSCore) -> RHS -> RHS Source #

Modify all the LHSCore of the given RHS. (Used to insert patterns for `rewrite` or the inspect idiom)

insertNames :: [Arg (Maybe BindName)] -> RHS -> RHS Source #

Insert some names into the with-clauses LHS of the given RHS. (Used for the inspect idiom)

insertInspects :: [Arg (Maybe BindName)] -> LHSCore -> LHSCore Source #

insertPatterns :: [Arg Pattern] -> RHS -> RHS Source #

Insert some with-patterns into the with-clauses LHS of the given RHS. (Used for `rewrite`)

insertPatternsLHSCore :: [Arg Pattern] -> LHSCore -> LHSCore Source #

Insert with-patterns before the trailing with patterns. If there are none, append the with-patterns.

data WithFunctionProblem Source #

Parameters for creating a `with`-function.

Constructors

NoWithFunction |
WithFunction |

Fields

- wfParentName :: QName

  Parent function name.

- wfName :: QName

  With function name.

- wfParentType :: Type

  Type of the parent function.

- wfParentTel :: Telescope

  Context of the parent patterns.

- wfBeforeTel :: Telescope

  Types of arguments to the with function before the with expressions (needed vars).

- wfAfterTel :: Telescope

  Types of arguments to the with function after the with expressions (unneeded vars).

- wfExprs :: [Arg (Term, EqualityView)]

  With and rewrite expressions and their types.

- wfRHSType :: Type

  Type of the right hand side.

- wfParentPats :: [NamedArg DeBruijnPattern]

  Parent patterns.

- wfParentParams :: Nat

  Number of module parameters in parent patterns

- wfPermSplit :: Permutation

  Permutation resulting from splitting the telescope into needed and unneeded vars.

- wfPermParent :: Permutation

  Permutation reordering the variables in the parent pattern.

- wfPermFinal :: Permutation

  Final permutation (including permutation for the parent clause).

- wfClauses :: [Clause]

  The given clauses for the with function

- wfCallSubst :: Substitution

  Subtsitution to generate call for the parent.

checkSystemCoverage :: QName -> [Int] -> Type -> [Clause] -> TCM System Source #

# Info that is needed after all clauses have been processed.

data ClausesPostChecks Source #

Constructors

CPC |

Fields

- cpcPartialSplits :: IntSet

  Which argument indexes have a partial split.

#### Instances

Instances details

Monoid ClausesPostChecks Source # |
Instance details Defined in Agda.TypeChecking.Rules.Def Methods mempty :: ClausesPostChecks Source # mappend :: ClausesPostChecks -> ClausesPostChecks -> ClausesPostChecks Source # mconcat :: [ClausesPostChecks] -> ClausesPostChecks Source #
Semigroup ClausesPostChecks Source # |
Instance details Defined in Agda.TypeChecking.Rules.Def Methods (<>) :: ClausesPostChecks -> ClausesPostChecks -> ClausesPostChecks Source # sconcat :: NonEmpty ClausesPostChecks -> ClausesPostChecks Source # stimes :: Integral b => b -> ClausesPostChecks -> ClausesPostChecks Source #

checkClauseLHS :: Type -> Maybe Substitution -> SpineClause -> (LHSResult -> TCM a) -> TCM a Source #

The LHS part of checkClause.

checkClause Source #

Arguments

:: Type | Type of function defined by this clause.
-> Maybe Substitution | Module parameter substitution arising from with-abstraction.
-> SpineClause | Clause.
-> TCM (Clause, ClausesPostChecks) | Type-checked clause

Type check a function clause.

getReflPattern :: TCM Pattern Source #

Generate the abstract pattern corresponding to Refl

checkRHS Source #

Arguments

:: LHSInfo | Range of lhs.
-> QName | Name of function.
-> [NamedArg Pattern] | Patterns in lhs.
-> Type | Top-level type of function.
-> LHSResult | Result of type-checking patterns
-> RHS | Rhs to check.
-> TCM (Maybe Term, WithFunctionProblem) |

Type check the `with` and `rewrite` lhss and/or the rhs.

checkWithRHS Source #

Arguments

:: QName | Name of function.
-> QName | Name of the with-function.
-> Type | Type of function.
-> LHSResult | Result of type-checking patterns
-> [Arg (Term, EqualityView)] | Expressions and types of with-expressions.
-> [Clause] | With-clauses to check.
-> TCM (Maybe Term, WithFunctionProblem) |

checkWithFunction :: [Name] -> WithFunctionProblem -> TCM (Maybe Term) Source #

Invoked in empty context.

checkWhere Source #

Arguments

:: WhereDeclarations | Where-declarations to check.
-> TCM a | Continuation.
-> TCM a |

Type check a where clause.

newSection :: ModuleName -> GeneralizeTelescope -> TCM a -> TCM a Source #

Enter a new section during type-checking.

atClause :: QName -> Int -> Type -> Maybe Substitution -> SpineClause -> TCM a -> TCM a Source #

Set the current clause number.