Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




data SplitClause Source




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 Source

A Covering is the result of splitting a SplitClause.




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

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 CoInductive.

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

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

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 CoInductive.

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