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

Safe Haskell | Safe-Infered

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 :: [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 :: Induction -> Telescope -> Permutation -> [Arg Pattern] -> Nat -> TCM (Either SplitError Covering)
- split' :: 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 :: [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

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

split'

Arguments

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