Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

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

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

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.

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.

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

data BlockedOnResult Source #

Missing elimination blocking a match.

Constructors

BlockedOnProj

Blocked on unsplit projection.

Fields

BlockedOnApply

Blocked on unintroduced argument.

Fields

NotBlockedOnResult