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

Agda.TypeChecking.Coverage

Synopsis

- data SplitClause = SClause {
  - scTel :: Telescope
  - scPerm :: Permutation
  - scPats :: [Arg Pattern]
  - scSubst :: [Term]
  }
- type Covering = [SplitClause]
- data SplitError
  - = NotADatatype Type
  - | IrrelevantDatatype Type
  - | CoinductiveDatatype Type
  - | NoRecordConstructor Type
  - | CantSplit QName Telescope Args Args [Term]
  - | GenericSplitError String
- type CoverM = ExceptionT SplitError TCM
- typeOfVar :: Telescope -> Nat -> Arg Type
- checkCoverage :: QName -> TCM ()
- cover :: MonadTCM tcm => [Clause] -> SplitClause -> tcm (Set Nat, [[Arg Pattern]])
- isDatatype :: (MonadTCM tcm, MonadException SplitError tcm) => Induction -> Arg Type -> tcm (QName, [Arg Term], [Arg Term], [QName])
- computeNeighbourhood :: Telescope -> Telescope -> Permutation -> QName -> Args -> Args -> Nat -> OneHolePatterns -> QName -> CoverM [SplitClause]
- splitClause :: Clause -> Nat -> TCM (Either SplitError Covering)
- splitClauseWithAbs :: Clause -> Nat -> TCM (Either SplitError (Either SplitClause Covering))
- split :: MonadTCM tcm => Induction -> Telescope -> Permutation -> [Arg Pattern] -> Nat -> tcm (Either SplitError Covering)
- split' :: MonadTCM tcm => Induction -> Telescope -> Permutation -> [Arg Pattern] -> Nat -> 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]
scSubst :: [Term]

  substitution from scTel to old context

type Covering = [SplitClause]

data SplitError

Constructors

NotADatatype Type | neither data type nor record
IrrelevantDatatype Type | data type, but in irrelevant position
CoinductiveDatatype Type | coinductive data type
NoRecordConstructor Type | record type, but no constructor
CantSplit QName Telescope Args Args [Term] |
GenericSplitError String |

Instances

Show SplitError |
Error SplitError |
PrettyTCM SplitError |

type CoverM = ExceptionT SplitError TCM

typeOfVar :: Telescope -> Nat -> Arg Type

checkCoverage :: QName -> TCM ()

Top-level function for checking pattern coverage.

cover :: MonadTCM tcm => [Clause] -> SplitClause -> tcm (Set Nat, [[Arg Pattern]])

Check that the list of clauses covers the given split clause. Returns the missing cases.

isDatatype :: (MonadTCM tcm, MonadException SplitError tcm) => Induction -> Arg 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 -> Telescope -> Permutation -> QName -> Args -> Args -> Nat -> OneHolePatterns -> QName -> CoverM [SplitClause]

    dtype == d pars ixs

splitClause :: Clause -> Nat -> TCM (Either SplitError Covering)

split x ps. ps, x (deBruijn index)

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

split

Arguments

:: MonadTCM tcm |
=> Induction | Coinductive constructors are allowed if this argument is `CoInductive`.
-> Telescope |
-> Permutation |
-> [Arg Pattern] |
-> Nat |
-> tcm (Either SplitError Covering) |

split'

Arguments

:: MonadTCM tcm |
=> Induction | Coinductive constructors are allowed if this argument is `CoInductive`.
-> Telescope |
-> Permutation |
-> [Arg Pattern] |
-> Nat |
-> tcm (Either SplitError (Either SplitClause Covering)) |