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 :: (MonadReduce m, HasConstInfo m, HasBuiltins m) => [Clause] -> [NamedArg SplitPattern] -> m (Match (Nat, SplitInstantiation))
matchClause :: (MonadReduce m, HasConstInfo m, HasBuiltins m) => [NamedArg SplitPattern] -> Clause -> m MatchResult
type SplitPattern = Pattern' SplitPatVar
data SplitPatVar = SplitPatVar {
- splitPatVarName :: PatVarName
- splitPatVarIndex :: Int
- splitExcludedLits :: [Literal]
}
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
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

:: (MonadReduce m, HasConstInfo m, HasBuiltins 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

:: (MonadReduce m, HasConstInfo m, HasBuiltins 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`.

matchClause qs i c checks whether clause c covers a split clause with patterns 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

Show SplitPatVar Source #
Instance details Defined in Agda.TypeChecking.Coverage.Match Methods showsPrec :: Int -> SplitPatVar -> ShowS # show :: SplitPatVar -> String # showList :: [SplitPatVar] -> ShowS #
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 #
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 #
PrettyTCM SplitPatVar Source #
Instance details Defined in Agda.TypeChecking.Coverage.Match Methods prettyTCM :: MonadPretty m => SplitPatVar -> m Doc Source #
Subst SplitPattern SplitPattern Source #
Instance details Defined in Agda.TypeChecking.Coverage.Match Methods applySubst :: Substitution' SplitPattern -> SplitPattern -> SplitPattern Source #

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

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

toSplitPSubst :: PatternSubstitution -> SplitPSubstitution Source #

applySplitPSubst :: Subst Term 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

Show BlockingVar Source #
Instance details Defined in Agda.TypeChecking.Coverage.Match Methods showsPrec :: Int -> BlockingVar -> ShowS # show :: BlockingVar -> String # showList :: [BlockingVar] -> ShowS #
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 #

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