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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Coverage

Description

Coverage checking, case splitting, and splitting for refine tactics.

Synopsis

- data SplitClause = SClause {
  - scTel :: Telescope
  - scPats :: [NamedArg SplitPattern]
  - scSubst :: Substitution' SplitPattern
  - scCheckpoints :: Map CheckpointId Substitution
  - scTarget :: Maybe (Arg Type)
  }
- clauseToSplitClause :: Clause -> SplitClause
- fixTarget :: SplitClause -> TCM (Telescope, SplitClause)
- data Covering = Covering {
  - covSplitArg :: Arg Nat
  - covSplitClauses :: [(SplitTag, SplitClause)]
  }
- splitClauses :: Covering -> [SplitClause]
- coverageCheck :: QName -> Type -> [Clause] -> TCM SplitTree
- isCovered :: QName -> [Clause] -> SplitClause -> TCM Bool
- splitClauseWithAbsurd :: SplitClause -> Nat -> TCM (Either SplitError (Either SplitClause Covering))
- splitLast :: Induction -> Telescope -> [NamedArg DeBruijnPattern] -> TCM (Either SplitError Covering)
- splitResult :: QName -> SplitClause -> TCM (Either SplitError [SplitClause])
- normaliseProjP :: (NormaliseProjP a, HasConstInfo m) => a -> m a

# Documentation

data SplitClause Source #

Constructors

SClause |

Fields

- scTel :: Telescope

  Type of variables in `scPats`.

- scPats :: [NamedArg SplitPattern]

  The patterns leading to the currently considered branch of the split tree.

- scSubst :: Substitution' SplitPattern

  Substitution from `scTel` to old context. Only needed directly after split on variable: * To update `scTarget` * To rename other split variables when splitting on multiple variables. `scSubst` is not ``transitive'`, i.e., does not record the substitution from the original context to `scTel` over a series of splits. It is freshly computed after each split by `computeNeighborhood`; also `splitResult`, which does not split on a variable, should reset it to the identity `idS`, lest it be applied to `scTarget` again, leading to Issue 1294.

- scCheckpoints :: Map CheckpointId Substitution

  We need to keep track of the module parameter checkpoints for the clause for the purpose of inferring missing instance clauses.

- scTarget :: Maybe (Arg Type)

  The type of the rhs, living in context `scTel`. This invariant is broken before calls to `fixTarget`; there, `scTarget` lives in the old context. `fixTarget` moves `scTarget` to the new context by applying substitution `scSubst`.

Instances

PrettyTCM SplitClause Source # | For debugging only.
Instance details Defined in Agda.TypeChecking.Coverage Methods prettyTCM :: SplitClause -> TCM Doc Source #

clauseToSplitClause :: Clause -> SplitClause Source #

Create a split clause from a clause in internal syntax. Used by make-case.

fixTarget :: SplitClause -> TCM (Telescope, SplitClause) Source #

Update the target type, add more patterns to split clause if target becomes a function type. Returns the domains of the function type (if any).

data Covering Source #

A `Covering` is the result of splitting a `SplitClause`.

Constructors

Covering |

Fields

- covSplitArg :: Arg Nat

  De Bruijn level (counting dot patterns) of argument we split on.

- covSplitClauses :: [(SplitTag, SplitClause)]

  Covering clauses, indexed by constructor/literal these clauses share.

splitClauses :: Covering -> [SplitClause] Source #

Project the split clauses out of a covering.

coverageCheck Source #

Arguments

:: QName | Name `f` of definition.
-> Type | Absolute type (including the full parameter telescope).
-> [Clause] | Clauses of `f`. These are the very clauses of `f` in the signature.
-> TCM SplitTree |

Top-level function for checking pattern coverage.

Effects:

- Marks unreachable clauses as such in the signature.
- Adds missing instances clauses to the signature.

isCovered :: QName -> [Clause] -> SplitClause -> TCM Bool Source #

Top-level function for eliminating redundant clauses in the interactive case splitter

splitClauseWithAbsurd :: SplitClause -> Nat -> TCM (Either SplitError (Either SplitClause Covering)) Source #

Entry point from `Interaction.MakeCase`.

splitLast :: Induction -> Telescope -> [NamedArg DeBruijnPattern] -> TCM (Either SplitError Covering) Source #

Entry point from `TypeChecking.Empty` and `Interaction.BasicOps`. `splitLast CoInductive` is used in the `refine` tactics.

splitResult :: QName -> SplitClause -> TCM (Either SplitError [SplitClause]) Source #

splitResult for MakeCase, tries to introduce IApply or ProjP copatterns

normaliseProjP :: (NormaliseProjP a, HasConstInfo m) => a -> m a Source #