Agda.TypeChecking.Coverage

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

Documentation

data SplitClause

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

  The type of the rhs, living in context scTel. fixTargetType computes the new scTarget by applying substitution scSubst.

Instances

PrettyTCM SplitClause

For debugging only.

Defined in Agda.TypeChecking.Coverage

Methods

prettyTCM :: MonadPretty m => SplitClause -> m Doc

clauseToSplitClause :: Clause -> SplitClause

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

insertTrailingArgs

Arguments

:: Bool

Force insertion even when there is a domTactic?

-> SplitClause

-> TCM (Telescope, SplitClause)

Add more patterns to split clause if the target type is a function type. Returns the domains of the function type (if any).

data Covering

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, IInfo))]

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

splitClauses :: Covering -> [SplitClause]

Project the split clauses out of a covering.

coverageCheck

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

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

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

Entry point from Interaction.MakeCase.

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

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

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

splitResult for MakeCase, tries to introduce IApply or ProjP copatterns

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

Orphan instances

PrettyTCM SplitClause

For debugging only.

Methods

prettyTCM :: MonadPretty m => SplitClause -> m Doc