Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Coverage.SplitClause

Description

SplitClause and CoverResult types.

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

data UnifyEquiv Source #

Instances

Instances details
Show UnifyEquiv Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitClause

Methods

showsPrec :: Int -> UnifyEquiv -> ShowS

show :: UnifyEquiv -> String

showList :: [UnifyEquiv] -> ShowS

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

show :: IInfo -> String

showList :: [IInfo] -> ShowS

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.

clauseToSplitClause :: Clause -> SplitClause Source #

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

data CoverResult Source #

Constructors

CoverResult 

Fields