This module implements the backend of match compilation. The elaborator has already elaborated the patterns and the the expected type of the matcher is known.

The match compilation task is represented as a Problem, which is then processed interatively by the process function. It has various “moves” which it tries in a particular order, to make progress on the problem, possibly splitting it.

The high-level overview of moves are

• If no variables are left, process as leaf
  • If there is an alternative, solve its constraints
  • Else use contradiction to prove completeness of the match
• Process “independent prefixes” of patterns. These are patterns that can be processed without affecting the aother alternatives, and without side effects in the sense of updating the mvarId. These are
  • variable patterns; substitute
  • inaccessible patterns; add equality constraints
  • as-patterns: substitute value and equality After thes have been processed, we use .inaccessible x where x is the variable being matched to mark them as “done”.
• If all patterns start with “done”, drop the first variable
• The first alt has only “done” patterns, drop remaining alts (they're overlapped)
• If the first alternative has its first refutable pattern not at the front, move it to the front.
• If we have both constructor and value patterns, expand the values to constructors.
• If next pattern is not a variable, but an expression, then
  • if it is a constructor, behave a bit as if we just did a case split
  • else move it to constraints
• If we have constructor patterns, or no alternatives, split by constructor Use sparse splitting if not all constructors are present
• If match is empty (no alts), drop the variable
• If we have value patterns (e.g. strings), split by value
• If we have array literal patterns, split by array

If we reach this point, the match is not supported. If only nat value patterns exist, we expand them for better error messages. Throw error.

opaque Lean.Meta.Match.backward.match.sparseCases : Lean.Option Bool

opaque Lean.Meta.Match.backward.match.rowMajor : Lean.Option Bool

def Lean.Meta.Match.throwIncorrectNumberOfPatternsAt {α : Type} [ToMessageData α] (ref : Syntax) (discrepancyKind : String) (expected actual : Nat) (pats : List α) : MetaM Unit

Throws an error indicating that the alternative at ref contains an unexpected number of patterns. Remark: we allow α to be arbitrary because this error may be thrown before or after elaborating pattern syntax.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Match.logIncorrectNumberOfPatternsAt {α : Type} [ToMessageData α] (ref : Syntax) (discrepancyKind : String) (expected actual : Nat) (pats : List α) : MetaM Unit

Logs an error indicating that the alternative at ref contains an unexpected number of patterns. Remark: we allow α to be arbitrary because this error may be thrown before or after elaborating pattern syntax.

Equations

• Lean.Meta.Match.logIncorrectNumberOfPatternsAt ref discrepancyKind expected actual pats = Lean.logErrorAt ref (Lean.Meta.Match.mkIncorrectNumberOfPatternsMsg✝ discrepancyKind expected actual pats)

structure Lean.Meta.Match.State : Type

• used : Std.HashSet Nat

  Used alternatives

• overlaps : Overlaps

  Overlapped alternatives. Stored as ordered pairs (overlapping,overlapped) ∈ overlaps. Used during splitter generation to avoid going through all pairs of patterns.

• counterExamples : List (List Example)

def Lean.Meta.Match.isCurrVarInductive (p : Problem) : MetaM Bool

Equations

• One or more equations did not get rendered due to their size.

Note that we decided to store pending constraints to address issues exposed by #1279 and #1361. Here is a simplified version of the example on this issue (see test: 1279_simplified.lean)

inductive Arrow : Type → Type → Type 1
  | id   : Arrow a a
  | unit : Arrow Unit Unit
  | comp : Arrow β γ → Arrow α β → Arrow α γ
deriving Repr

def Arrow.compose (f : Arrow β γ) (g : Arrow α β) : Arrow α γ :=
  match f, g with
  | id, g => g
  | f, id => f
  | f, g => comp f g

The initial state for the match-expression above is

[Meta.Match.match] remaining variables: [β✝:(Type), γ✝:(Type), f✝:(Arrow β✝ γ✝), g✝:(Arrow α β✝)]
alternatives:
  [β:(Type), g:(Arrow α β)] |- [β, .(β), (Arrow.id .(β)), g] => h_1 β g
  [γ:(Type), f:(Arrow α γ)] |- [.(α), γ, f, (Arrow.id .(α))] => h_2 γ f
  [β:(Type), γ:(Type), f:(Arrow β γ), g:(Arrow α β)] |- [β, γ, f, g] => h_3 β γ f g

The first step is a variable-transition which replaces β with β✝ in the first and third alternatives. The constraint β✝ ≋ α in the second alternative used to be discarded. We now store it at the alternative cnstrs field.

def Lean.Meta.Match.isExFalsoTransition (p : Problem) : MetaM Bool

Equations

• Lean.Meta.Match.isExFalsoTransition p = if p.alts.isEmpty = true then Lean.Meta.Match.withGoalOf p do let targetType ← p.mvarId.getType pure !targetType.isFalse else pure false

def Lean.Meta.Match.processExFalso (p : Problem) : MetaM Problem

Equations

• Lean.Meta.Match.processExFalso p = do let mvarId' ← p.mvarId.exfalso pure { mvarId := mvarId', vars := p.vars, alts := p.alts, examples := p.examples }

def Lean.Meta.Match.hasIndependentPatterns (p : Problem) : Bool

Does any alternative have a pattern that can be independently handled (variable, inaccessible, as-pattern) before any refutable pattern?

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Match.processIndependentPatterns (p : Problem) : MetaM Problem

Equations

• One or more equations did not get rendered due to their size.

opaque Lean.Meta.Match.bootstrap.genMatcherCode : Lean.Option Bool

def Lean.Meta.Match.mkMatcherAuxDefinition (name : Name) (type value : Expr) (isSplitter : Bool) : MetaM (Expr × Option (MatcherInfo → MetaM Unit))

Similar to mkAuxDefinition, but uses the cache matcherExt. It also returns an Boolean that indicates whether a new matcher function was added to the environment or not.

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Meta.Match.MkMatcherInput : Type

• matcherName : Name
• matchType : Expr
• discrInfos : Array DiscrInfo
• lhss : List AltLHS
• isSplitter : Option Overlaps

def Lean.Meta.Match.MkMatcherInput.numDiscrs (m : MkMatcherInput) : Nat

Equations

• m.numDiscrs = m.discrInfos.size

def Lean.Meta.Match.MkMatcherInput.collectFVars (m : MkMatcherInput) : StateRefT' IO.RealWorld CollectFVars.State MetaM Unit

Equations

• m.collectFVars = do m.matchType.collectFVars m.lhss.forM fun (alt : Lean.Meta.Match.AltLHS) => alt.collectFVars

def Lean.Meta.Match.MkMatcherInput.collectDependencies (m : MkMatcherInput) : MetaM FVarIdSet

Equations

• m.collectDependencies = do let __discr ← m.collectFVars.run { } match __discr with | (fst, s) => do let s ← s.addDependencies pure s.fvarSet

def Lean.Meta.Match.withCleanLCtxFor {α : Type} (m : MkMatcherInput) (k : MetaM α) : MetaM α

Auxiliary method used at mkMatcher. It executes k in a local context that contains only the local declarations m depends on. This is important because otherwise dependent elimination may "refine" the types of unnecessary declarations and accidentally introduce unnecessary dependencies in the auto-generated auxiliary declaration. Note that this is not just an optimization because the unnecessary dependencies may prevent the termination checker from succeeding. For an example, see issue #1237.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Match.mkMatcher (input : MkMatcherInput) : MetaM MatcherResult

Create a dependent matcher for matchType where matchType is of the form (a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> B[a_1, ..., a_n] where n = numDiscrs, and the lhss are the left-hand-sides of the match-expression alternatives. Each AltLHS has a list of local declarations and a list of patterns. The number of patterns must be the same in each AltLHS. The generated matcher has the structure described at MatcherInfo. The motive argument is of the form (motive : (a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> Sort v) where v is a universe parameter or 0 if B[a_1, ..., a_n] is a proposition.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Match.getMkMatcherInputInContext (matcherApp : MatcherApp) (unfoldNamed : Bool) : MetaM MkMatcherInput

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Match.withMkMatcherInput {α : Type} (matcherName : Name) (unfoldNamed : Bool) (k : MkMatcherInput → MetaM α) : MetaM α

Equations

• One or more equations did not get rendered due to their size.