Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Coverage.Match

Description

Given

the function clauses cs
the patterns ps of the split clause

we want to compute a variable index (in the split clause) to split on next.

The matcher here checks whether the split clause is covered by one of the given clauses cs or whether further splitting is needed (and when yes, where).

Synopsis

data Match a
- = Yes a
- | No
- | Block {
  - blockedOnResult :: BlockedOnResult
  - blockedOnVars :: BlockingVars
  }
match :: PureTCM m => [Clause] -> [NamedArg SplitPattern] -> m (Match (Nat, SplitInstantiation))
matchClause :: PureTCM m => [NamedArg SplitPattern] -> Clause -> m MatchResult
type SplitPattern = Pattern' SplitPatVar
data SplitPatVar = SplitPatVar {
- splitPatVarName :: PatVarName
- splitPatVarIndex :: Int
- splitExcludedLits :: [Literal]
}
fromSplitPattern :: NamedArg SplitPattern -> NamedArg DeBruijnPattern
fromSplitPatterns :: [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
toSplitPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern]
toSplitPSubst :: PatternSubstitution -> SplitPSubstitution
applySplitPSubst :: TermSubst a => SplitPSubstitution -> a -> a
isTrivialPattern :: HasConstInfo m => Pattern' a -> m Bool
data BlockingVar = BlockingVar {
- blockingVarNo :: Nat
- blockingVarCons :: [ConHead]
- blockingVarLits :: [Literal]
- blockingVarOverlap :: Bool
- blockingVarLazy :: Bool
}
type BlockingVars = [BlockingVar]
data BlockedOnResult
- = BlockedOnProj {
  - blockedOnResultOverlap :: Bool
  }
- | BlockedOnApply {
  - blockedOnResultIApply :: ApplyOrIApply
  }
- | NotBlockedOnResult
setBlockingVarOverlap :: BlockingVar -> BlockingVar
data ApplyOrIApply
- = IsApply
- | IsIApply

Documentation

data Match a Source #

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

Instances details

Functor Match Source #
Instance details Defined in Agda.TypeChecking.Coverage.Match Methods fmap :: (a -> b) -> Match a -> Match b # (<$) :: a -> Match b -> Match a #

match Source #

Arguments

:: PureTCM m
=> [Clause]	Search for clause that covers the patterns.
-> [NamedArg SplitPattern]	Patterns of the current `SplitClause`.
-> m (Match (Nat, SplitInstantiation))

Match the given patterns against a list of clauses.

If successful, return the index of the covering clause.

matchClause Source #

Arguments

:: PureTCM m
=> [NamedArg SplitPattern]	Split clause patterns `qs`.
-> Clause	Clause `c` to cover split clause.
-> m MatchResult	Result. If `Yes` the instantiation `rs` such that `(namedClausePats c)[rs] == qs`.

type SplitPattern = Pattern' SplitPatVar Source #

data SplitPatVar Source #

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

Instances details

Pretty SplitPatVar Source #

Instance details

Defined in Agda.TypeChecking.Coverage.Match

Methods

pretty :: SplitPatVar -> Doc Source #

prettyPrec :: Int -> SplitPatVar -> Doc Source #

prettyList :: [SplitPatVar] -> Doc Source #

PrettyTCM SplitPatVar Source #

Instance details

Defined in Agda.TypeChecking.Coverage.Match

Methods

prettyTCM :: MonadPretty m => SplitPatVar -> m Doc Source #

Subst SplitPattern Source #

Instance details

Defined in Agda.TypeChecking.Coverage.Match

Associated Types

type SubstArg SplitPattern
Instance details Defined in Agda.TypeChecking.Coverage.Match type SubstArg SplitPattern = SplitPattern

Methods

applySubst :: Substitution' (SubstArg SplitPattern) -> SplitPattern -> SplitPattern Source #

DeBruijn SplitPatVar Source #

Instance details

Defined in Agda.TypeChecking.Coverage.Match

Methods

deBruijnVar :: Int -> SplitPatVar Source #

debruijnNamedVar :: String -> Int -> SplitPatVar Source #

deBruijnView :: SplitPatVar -> Maybe Int Source #

Show SplitPatVar Source #

Instance details

Defined in Agda.TypeChecking.Coverage.Match

Methods

showsPrec :: Int -> SplitPatVar -> ShowS #

show :: SplitPatVar -> String #

showList :: [SplitPatVar] -> ShowS #

type SubstArg SplitPattern Source #

Instance details

Defined in Agda.TypeChecking.Coverage.Match

type SubstArg SplitPattern = SplitPattern

fromSplitPattern :: NamedArg SplitPattern -> NamedArg DeBruijnPattern Source #

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

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

toSplitPSubst :: PatternSubstitution -> SplitPSubstitution Source #

applySplitPSubst :: TermSubst a => SplitPSubstitution -> a -> a Source #

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

A pattern that matches anything (modulo eta).

data BlockingVar Source #

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. blockingVarLazy :: Bool True if at least one clause has a lazy pattern in this position.

Instances

Instances details

Pretty BlockingVar Source #
Instance details Defined in Agda.TypeChecking.Coverage.Match Methods pretty :: BlockingVar -> Doc Source # prettyPrec :: Int -> BlockingVar -> Doc Source # prettyList :: [BlockingVar] -> Doc Source #
Show BlockingVar Source #
Instance details Defined in Agda.TypeChecking.Coverage.Match Methods showsPrec :: Int -> BlockingVar -> ShowS # show :: BlockingVar -> String # showList :: [BlockingVar] -> ShowS #

type BlockingVars = [BlockingVar] Source #

data BlockedOnResult Source #

Missing elimination blocking a match.

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 Is the unintroduced argument an `IApply` pattern?
NotBlockedOnResult

setBlockingVarOverlap :: BlockingVar -> BlockingVar Source #

data ApplyOrIApply Source #

Constructors

IsApply
IsIApply