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

For debugging only.

Defined in Agda.TypeChecking.Coverage

Methods

prettyTCM :: SplitClause -> TCM Doc

clauseToSplitClause :: Clause -> SplitClause

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

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

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

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]

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