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, [SplitAssignment]))

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