Safe Haskell	None
Language	Haskell98

Agda.TypeChecking.Coverage

Synopsis

Documentation

data SplitClause Source

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. scTarget :: Maybe (Arg Type) The type of the rhs.

data Covering Source

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] Source

Project the split clauses out of a covering.

clauseToSplitClause :: Clause -> SplitClause Source

Create a split clause from a clause in internal syntax.

type CoverM = ExceptionT SplitError TCM Source

checkCoverage :: QName -> TCM () Source

Old top-level function for checking pattern coverage. DEPRECATED

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

Top-level function for checking pattern coverage.

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

cover f 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 Source

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

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.

fixTarget :: SplitClause -> TCM SplitClause Source

update the target type, add more patterns to split clause if target becomes a function type.

computeNeighbourhood Source

Arguments

:: Telescope	Telescope before split point.
-> PatVarName	Name of pattern variable at split point.
-> Telescope	Telescope after split point.
-> Permutation
-> QName	Name of datatype to split at.
-> Args	Data type parameters.
-> Args	Data type indices.
-> Nat	Index of split variable.
-> OneHolePatterns	Patterns with hole at split point.
-> QName	Constructor to fit into hole.
-> CoverM (Maybe SplitClause)	New split clause if successful.

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

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

Entry point from Interaction.MakeCase.

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

Entry point from TypeChecking.Empty and Interaction.BasicOps.

split Source

Arguments

:: Induction	Coinductive constructors are allowed if this argument is `CoInductive`.
-> SplitClause
-> BlockingVar
-> TCM (Either SplitError Covering)

split ind splitClause x = return res splits splitClause at pattern var x (de Bruijn index).

Possible results res are:

Left err: Splitting failed.
Right covering: A covering set of split clauses, one for each valid constructor. This could be the empty set (denoting an absurd clause).

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

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' Source

Arguments

:: Induction	Coinductive constructors are allowed if this argument is `CoInductive`.
-> SplitClause
-> BlockingVar
-> TCM (Either SplitError (Either SplitClause Covering))

split' ind splitClause x = return res splits splitClause at pattern var x (de Bruijn index).

Possible results res are:

Left err: Splitting failed.
Right (Left splitClause'): Absurd clause (type of x has 0 valid constructors).
Right (Right covering): A covering set of split clauses, one for each valid constructor.

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

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.