Safe Haskell | None |
---|
- data SplitClause = SClause {}
- data Covering = Covering {
- covSplitArg :: Nat
- covSplitClauses :: [(QName, SplitClause)]
- splitClauses :: Covering -> [SplitClause]
- clauseToSplitClause :: Clause -> SplitClause
- data SplitError
- type CoverM = ExceptionT SplitError TCM
- checkCoverage :: QName -> TCM ()
- coverageCheck :: QName -> Type -> [Clause] -> TCM SplitTree
- cover :: [Clause] -> SplitClause -> TCM (SplitTree, Set Nat, [[Arg Pattern]])
- splitStrategy :: BlockingVars -> Telescope -> TCM BlockingVars
- isDatatype :: (MonadTCM tcm, MonadException SplitError tcm) => Induction -> Dom Type -> tcm (QName, [Arg Term], [Arg Term], [QName])
- computeNeighbourhood :: Telescope -> String -> Telescope -> Permutation -> QName -> Args -> Args -> Nat -> OneHolePatterns -> QName -> CoverM [SplitClause]
- splitClauseWithAbs :: Clause -> Nat -> TCM (Either SplitError (Either SplitClause Covering))
- splitLast :: Induction -> Telescope -> [Arg 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.
data SplitError Source
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 |
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 :: [Clause] -> SplitClause -> TCM (SplitTree, Set Nat, [[Arg Pattern]])Source
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
.
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.
computeNeighbourhood :: Telescope -> String -> Telescope -> Permutation -> QName -> Args -> Args -> Nat -> OneHolePatterns -> QName -> CoverM [SplitClause]Source
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 -> [Arg 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)) |