Agda.TypeChecking.Coverage

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 :: [Arg Pattern]

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

scSubst :: Substitution

Substitution from scTel to old context.

scTarget :: Maybe Type

The type of the rhs.

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.

clauseToSplitClause :: Clause -> SplitClause

Create a split clause from a clause in internal syntax.

data SplitError

Constructors

NotADatatype (Closure Type)

neither data type nor record

IrrelevantDatatype (Closure Type)

data type, but in irrelevant position

CoinductiveDatatype (Closure Type)

coinductive data type

CantSplit QName Telescope Args Args [Term]

GenericSplitError String

Instances

Show SplitError

Error SplitError

PrettyTCM SplitError

type CoverM = ExceptionT SplitError TCM

checkCoverage :: QName -> TCM ()

Old top-level function for checking pattern coverage. DEPRECATED

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

Top-level function for checking pattern coverage.

cover :: [Clause] -> SplitClause -> TCM (SplitTree, Set Nat, [[Arg Pattern]])

cover cs (SClause _ _ ps _) = return (splitTree, used, pss). checks that the list of clauses cs covers the given split clause. Returns the splitTree, the used clauses, and missing cases pss.

splitStrategy :: BlockingVars -> Telescope -> TCM BlockingVars

isDatatype :: (MonadTCM tcm, MonadException SplitError tcm) => Induction -> Dom Type -> tcm (QName, [Arg Term], [Arg Term], [QName])

Check that a type is a non-irrelevant datatype or a record with named constructor. Unless the Induction argument is CoInductive the data type must be inductive.

computeNeighbourhood :: Telescope -> String -> Telescope -> Permutation -> QName -> Args -> Args -> Nat -> OneHolePatterns -> QName -> CoverM [SplitClause]

computeNeighbourhood delta1 delta2 perm d pars ixs hix hps con

delta1 Telescope before split point n Name of pattern variable at split point delta2 Telescope after split point d Name of datatype to split at pars Data type parameters ixs Data type indices hix Index of split variable hps Patterns with hole at split point con Constructor to fit into hole dtype == d pars ixs

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

Entry point from Interaction.MakeCase. Abs is for absurd clause.

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

Entry point from TypeChecking.Empty and Interaction.BasicOps.

split

Arguments

:: Induction

Coinductive constructors are allowed if this argument is CoInductive.

-> SplitClause

-> BlockingVar

-> TCM (Either SplitError Covering)

split _ Δ π ps x. FIXME: Δ ⊢ ps, x ∈ Δ (deBruijn index)

blendInAbsurdClause :: Nat -> Either SplitClause Covering -> Covering

splitDbIndexToLevel :: SplitClause -> BlockingVar -> Nat

dbIndexToLevel :: (Enum a1, Num a1, Ord a1, Sized a) => a -> Permutation -> Int -> a1

Convert a de Bruijn index relative to a telescope to a de Buijn level. The result should be the argument (counted from left, starting with 0) to split at (dot patterns included!).

split'

Arguments

:: Induction

Coinductive constructors are allowed if this argument is CoInductive.

-> SplitClause

-> BlockingVar

-> TCM (Either SplitError (Either SplitClause Covering))