Safe Haskell | None |
---|
- data SplitClause = SClause {}
- data Covering = Covering {
- covSplitArg :: Nat
- covSplitClauses :: [(QName, SplitClause)]
- splitClauses :: Covering -> [SplitClause]
- clauseToSplitClause :: Clause -> SplitClause
- type CoverM = ExceptionT SplitError TCM
- checkCoverage :: QName -> TCM ()
- coverageCheck :: QName -> Type -> [Clause] -> TCM SplitTree
- cover :: QName -> [Clause] -> SplitClause -> TCM (SplitTree, Set Nat, [[NamedArg Pattern]])
- splitStrategy :: BlockingVars -> Telescope -> TCM BlockingVars
- isDatatype :: (MonadTCM tcm, MonadException SplitError tcm) => Induction -> Dom Type -> tcm (QName, [Arg Term], [Arg Term], [QName])
- fixTarget :: SplitClause -> TCM SplitClause
- computeNeighbourhood :: Telescope -> String -> Telescope -> Permutation -> QName -> Args -> Args -> Nat -> OneHolePatterns -> QName -> CoverM (Maybe SplitClause)
- splitClauseWithAbs :: Clause -> Nat -> TCM (Either SplitError (Either SplitClause Covering))
- splitLast :: Induction -> Telescope -> [NamedArg Pattern] -> TCM (Either SplitError Covering)
- split :: Induction -> SplitClause -> BlockingVar -> TCM (Either SplitError Covering)
- blendInAbsurdClause :: Nat -> Either SplitClause Covering -> Covering
- splitDbIndexToLevel :: SplitClause -> BlockingVar -> Nat
- dbIndexToLevel :: (Enum a1, Num a1, Ord a1, Sized a) => a -> Permutation -> Int -> a1
- split' :: Induction -> SplitClause -> BlockingVar -> TCM (Either SplitError (Either SplitClause Covering))
Documentation
data SplitClause Source
SClause | |
|
A Covering
is the result of splitting a SplitClause
.
Covering | |
|
splitClauses :: Covering -> [SplitClause]Source
Project the split clauses out of a covering.
clauseToSplitClause :: Clause -> SplitClauseSource
Create a split clause from a clause in internal syntax.
type CoverM = ExceptionT SplitError TCMSource
checkCoverage :: QName -> TCM ()Source
Old top-level function for checking pattern coverage. DEPRECATED
coverageCheck :: QName -> Type -> [Clause] -> TCM SplitTreeSource
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
.
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 SplitClauseSource
update the target type, add more patterns to split clause if target becomes a function type.
:: Telescope | Telescope before split point. |
-> String | 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
splitClauseWithAbs :: Clause -> Nat -> TCM (Either SplitError (Either SplitClause Covering))Source
Entry point from Interaction.MakeCase
.
Abs
is for absurd clause.
splitLast :: Induction -> Telescope -> [NamedArg Pattern] -> TCM (Either SplitError Covering)Source
Entry point from TypeChecking.Empty
and Interaction.BasicOps
.
:: Induction | Coinductive constructors are allowed if this argument is
|
-> SplitClause | |
-> BlockingVar | |
-> TCM (Either SplitError Covering) |
split _ Δ π ps
. FIXME: Δ ⊢ ps, x ∈ Δ (deBruijn inde
dbIndexToLevel :: (Enum a1, Num a1, Ord a1, Sized a) => a -> Permutation -> Int -> a1Source
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!).
:: Induction | Coinductive constructors are allowed if this argument is
|
-> SplitClause | |
-> BlockingVar | |
-> TCM (Either SplitError (Either SplitClause Covering)) |