Agda.TypeChecking.Coverage.Match

Documentation

data Match a

If matching is inconclusive (Block) we want to know which variables or projections are blocking the match.

Constructors

Yes a

Matches unconditionally.

No

Definitely does not match.

Block

Fields

• blockedOnResult :: BlockedOnResult

  BlockedOnProj o if the clause has a result split

• blockedOnVars :: BlockingVars

  BlockingVar i cs ls o means variable i is blocked on constructors cs and literals ls.

Instances

Functor Match

Defined in Agda.TypeChecking.Coverage.Match

Methods

fmap :: (a -> b) -> Match a -> Match b

(<$) :: a -> Match b -> Match a

match :: (MonadReduce m, HasConstInfo m, HasBuiltins m) => [Clause] -> [NamedArg SplitPattern] -> m (Match (Nat, [SplitPattern]))

Given

1. the function clauses cs
2. the patterns ps

we want to compute a variable index of the split clause to split on next.

First, we find the set cs' of all the clauses that are instances (via substitutions rhos) of the split clause.

In these substitutions, we look for a column that has only constructor patterns. We try to split on this column first.

Match the given patterns against a list of clauses

type SplitPattern = Pattern' SplitPatVar

data SplitPatVar

For each variable in the patterns of a split clause, we remember the de Bruijn-index and the literals excluded by previous matches.

Constructors

SplitPatVar

Fields

• splitPatVarName :: PatVarName
• splitPatVarIndex :: Int
• splitExcludedLits :: [Literal]

Instances

Show SplitPatVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

showsPrec :: Int -> SplitPatVar -> ShowS

show :: SplitPatVar -> String

showList :: [SplitPatVar] -> ShowS

Pretty SplitPatVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

pretty :: SplitPatVar -> Doc

prettyPrec :: Int -> SplitPatVar -> Doc

prettyList :: [SplitPatVar] -> Doc

DeBruijn SplitPattern

Defined in Agda.TypeChecking.Coverage.Match

Methods

deBruijnVar :: Int -> SplitPattern

debruijnNamedVar :: String -> Int -> SplitPattern

deBruijnView :: SplitPattern -> Maybe Int

DeBruijn SplitPatVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

deBruijnVar :: Int -> SplitPatVar

debruijnNamedVar :: String -> Int -> SplitPatVar

deBruijnView :: SplitPatVar -> Maybe Int

PrettyTCM SplitPatVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

prettyTCM :: SplitPatVar -> TCM Doc

Subst SplitPattern SplitPattern

Defined in Agda.TypeChecking.Coverage.Match

Methods

applySubst :: Substitution' SplitPattern -> SplitPattern -> SplitPattern

fromSplitPatterns :: [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]

toSplitPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern]

toSplitPSubst :: PatternSubstitution -> SplitPSubstitution

applySplitPSubst :: Subst Term a => SplitPSubstitution -> a -> a

isTrivialPattern :: HasConstInfo m => Pattern' a -> m Bool

A pattern that matches anything (modulo eta).

data BlockingVar

Variable blocking a match.

Constructors

BlockingVar

Fields

• blockingVarNo :: Nat

  De Bruijn index of variable blocking the match.

• blockingVarCons :: [ConHead]

  Constructors in this position.

• blockingVarLits :: [Literal]

  Literals in this position.

• blockingVarOverlap :: Bool

  True if at least one clause has a variable pattern in this position.

Instances

Show BlockingVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

showsPrec :: Int -> BlockingVar -> ShowS

show :: BlockingVar -> String

showList :: [BlockingVar] -> ShowS

Pretty BlockingVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

pretty :: BlockingVar -> Doc

prettyPrec :: Int -> BlockingVar -> Doc

prettyList :: [BlockingVar] -> Doc

type BlockingVars = [BlockingVar]

data BlockedOnResult

Constructors

BlockedOnProj

Blocked on unsplit projection

Fields

• blockedOnResultOverlap :: Bool

  True if there are also matching clauses without an unsplit copattern.

BlockedOnApply

Blocked on unintroduced argument

Fields

• blockedOnResultIApply :: ApplyOrIApply

  True if the unintroduced argument was an IApply pattern

NotBlockedOnResult

setBlockingVarOverlap :: BlockingVar -> BlockingVar

data ApplyOrIApply

Constructors

IsApply

IsIApply