Agda.TypeChecking.Coverage.SplitClause

SplitClause and CoverResult types.

Documentation

data SplitClause

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

PrettyTCM SplitClause

For debugging only.

Defined in Agda.TypeChecking.Coverage

Methods

prettyTCM :: MonadPretty m => SplitClause -> m Doc

data UnifyEquiv

Constructors

UE

Fields

• infoTel0 :: Telescope
• infoTel :: Telescope
• infoEqTel :: Telescope
• infoEqLHS :: [Term]
• infoEqRHS :: [Term]
• infoRho :: PatternSubstitution
• infoTau :: Substitution
• infoLeftInv :: Substitution

Instances

Show UnifyEquiv

Defined in Agda.TypeChecking.Coverage.SplitClause

Methods

showsPrec :: Int -> UnifyEquiv -> ShowS

show :: UnifyEquiv -> String

showList :: [UnifyEquiv] -> ShowS

data IInfo

Constructors

TheInfo UnifyEquiv

NoInfo

Instances

Show IInfo

Defined in Agda.TypeChecking.Coverage.SplitClause

Methods

showsPrec :: Int -> IInfo -> ShowS

show :: IInfo -> String

showList :: [IInfo] -> ShowS

data Covering

A Covering is the result of splitting a SplitClause.

Constructors

Covering

Fields

• covSplitArg :: Arg Nat

  De Bruijn level (counting dot patterns) of argument we split on.

• covSplitClauses :: [(SplitTag, (SplitClause, IInfo))]

  Covering clauses, indexed by constructor/literal 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. Used by make-case.

data CoverResult

Constructors

CoverResult

Fields

• coverSplitTree :: SplitTree
• coverUsedClauses :: IntSet
• coverMissingClauses :: [(Telescope, [NamedArg DeBruijnPattern])]
• coverPatterns :: [Clause]

  The set of patterns used as cover.

• coverNoExactClauses :: IntSet