Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Coverage.Match

Description

Given

1. the function clauses `cs`
2. 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]
  }
- 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 Source # (<$) :: a -> Match b -> Match a Source #

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`.

`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

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

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 Source # show :: BlockingVar -> String Source # showList :: [BlockingVar] -> ShowS 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 |