Agda-2.6.2.1.20220320: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Coverage

Description

Coverage checking, case splitting, and splitting for refine tactics.

Synopsis

Documentation

data SplitClause Source #

Constructors

SClause 

Fields

  • scTel :: Telescope

    Type of variables in scPats.

  • scPats :: [NamedArg SplitPattern]

    The patterns leading to the currently considered branch of the split tree.

  • scSubst :: Substitution' SplitPattern

    Substitution from scTel to old context. Only needed directly after split on variable: * To update scTarget * To rename other split variables when splitting on multiple variables. scSubst is not `transitive', i.e., does not record the substitution from the original context to scTel over a series of splits. It is freshly computed after each split by computeNeighborhood; also splitResult, which does not split on a variable, should reset it to the identity idS, lest it be applied to scTarget again, leading to Issue 1294.

  • scCheckpoints :: Map CheckpointId Substitution

    We need to keep track of the module parameter checkpoints for the clause for the purpose of inferring missing instance clauses.

  • scTarget :: Maybe (Dom Type)

    The type of the rhs, living in context scTel. fixTargetType computes the new scTarget by applying substitution scSubst.

Instances

Instances details
PrettyTCM SplitClause Source #

For debugging only.

Instance details

Defined in Agda.TypeChecking.Coverage

clauseToSplitClause :: Clause -> SplitClause Source #

Create a split clause from a clause in internal syntax. Used by make-case.

insertTrailingArgs :: SplitClause -> TCM (Telescope, SplitClause) Source #

Add more patterns to split clause if the target type is a function type. Returns the domains of the function type (if any).

data Covering Source #

A Covering is the result of splitting a SplitClause.

Constructors

Covering 

Fields

splitClauses :: Covering -> [SplitClause] Source #

Project the split clauses out of a covering.

coverageCheck Source #

Arguments

:: QName

Name f of definition.

-> Type

Absolute type (including the full parameter telescope).

-> [Clause]

Clauses of f. These are the very clauses of f in the signature.

-> TCM SplitTree 

Top-level function for checking pattern coverage.

Effects:

  • Marks unreachable clauses as such in the signature.
  • Adds missing instances clauses to the signature.

isCovered :: QName -> [Clause] -> SplitClause -> TCM Bool Source #

Top-level function for eliminating redundant clauses in the interactive case splitter

splitClauseWithAbsurd :: SplitClause -> Nat -> TCM (Either SplitError (Either SplitClause Covering)) Source #

Entry point from Interaction.MakeCase.

splitLast :: Induction -> Telescope -> [NamedArg DeBruijnPattern] -> TCM (Either SplitError Covering) Source #

Entry point from TypeChecking.Empty and Interaction.BasicOps. splitLast CoInductive is used in the refine tactics.

splitResult :: QName -> SplitClause -> TCM (Either SplitError [SplitClause]) Source #

splitResult for MakeCase, tries to introduce IApply or ProjP copatterns