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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Coverage

Description

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

Synopsis

Documentation

data SplitClause

Constructors

SClause 

Fields

scTel :: Telescope

Type of variables in scPats.

scPerm :: Permutation

How to get from the variables in the patterns to the telescope.

scPats :: [NamedArg Pattern]

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

scSubst :: Substitution

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.

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.

clauseToSplitClause :: Clause -> SplitClause

Create a split clause from a clause in internal syntax.

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

Update the target type, add more patterns to split clause if target becomes a function type. Returns True if new patterns were added.

data Covering

A Covering is the result of splitting a SplitClause.

Constructors

Covering 

Fields

covSplitArg :: Nat

De Bruijn level of argument we split on.

covSplitClauses :: [(QName, SplitClause)]

Covering clauses, indexed by constructor these clauses share.

splitClauses :: Covering -> [SplitClause]

Project the split clauses out of a covering.

coverageCheck :: QName -> Type -> [Clause] -> TCM SplitTree

Top-level function for checking pattern coverage.

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

Entry point from Interaction.MakeCase.

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

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

splitResult :: QName -> SplitClause -> TCM (Maybe Covering)

splitResult f sc = return res

If the target type of sc is a record type, a covering set of split clauses is returned (sc extended by all valid projection patterns), otherwise res == Nothing. Note that the empty set of split clauses is returned if the record has no fields.