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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Coverage.SplitClause

Description

SplitClause and CoverResult types.

Synopsis

- data SplitClause = SClause {
  - scTel :: Telescope
  - scPats :: [NamedArg SplitPattern]
  - scSubst :: Substitution' SplitPattern
  - scCheckpoints :: Map CheckpointId Substitution
  - scTarget :: Maybe (Dom Type)
  }
- data UnifyEquiv = UE {
  - infoTel0 :: Telescope
  - infoTel :: Telescope
  - infoEqTel :: Telescope
  - infoEqLHS :: [Term]
  - infoEqRHS :: [Term]
  - infoRho :: PatternSubstitution
  - infoTau :: Substitution
  - infoLeftInv :: Substitution
  }
- data IInfo
  - = TheInfo UnifyEquiv
  - | NoInfo
- data Covering = Covering {
  - covSplitArg :: Arg Nat
  - covSplitClauses :: [(SplitTag, (SplitClause, IInfo))]
  }
- splitClauses :: Covering -> [SplitClause]
- clauseToSplitClause :: Clause -> SplitClause
- data CoverResult = CoverResult {
  - coverSplitTree :: SplitTree
  - coverUsedClauses :: IntSet
  - coverMissingClauses :: [(Telescope, [NamedArg DeBruijnPattern])]
  - coverPatterns :: [Clause]
  - coverNoExactClauses :: IntSet
  }

# 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 Methods prettyTCM :: MonadPretty m => SplitClause -> m Doc Source #

data UnifyEquiv Source #

Constructors

UE |

Fields

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

#### Instances

Instances details

Show UnifyEquiv Source # |
Instance details Defined in Agda.TypeChecking.Coverage.SplitClause Methods showsPrec :: Int -> UnifyEquiv -> ShowS Source # show :: UnifyEquiv -> String Source # showList :: [UnifyEquiv] -> ShowS Source #

data IInfo Source #

Constructors

TheInfo UnifyEquiv |
NoInfo |

#### Instances

Instances details

Show IInfo Source # |
Instance details Defined in Agda.TypeChecking.Coverage.SplitClause Methods showsPrec :: Int -> IInfo -> ShowS Source # show :: IInfo -> String Source # showList :: [IInfo] -> ShowS Source #

data Covering Source #

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] Source #

Project the split clauses out of a covering.

clauseToSplitClause :: Clause -> SplitClause Source #

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

data CoverResult Source #

Constructors

CoverResult |

Fields

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

  The set of patterns used as cover.

- coverNoExactClauses :: IntSet