Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.TypeChecking.Coverage

Synopsis

- data SplitClause = SClause {
  - scTel :: Telescope
  - scPerm :: Permutation
  - scPats :: [Arg Pattern]
  - scSubst :: Substitution
  - scTarget :: Maybe Type
  }
- data Covering = Covering {
  - covSplitArg :: Nat
  - covSplitClauses :: [(QName, SplitClause)]
  }
- splitClauses :: Covering -> [SplitClause]
- clauseToSplitClause :: Clause -> SplitClause
- data SplitError
  - = NotADatatype (Closure Type)
  - | IrrelevantDatatype (Closure Type)
  - | CoinductiveDatatype (Closure Type)
  - | CantSplit QName Telescope Args Args [Term]
  - | GenericSplitError String
- 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

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