This module implements a simple E-matching procedure as a backtracking search.

inductive Lean.Meta.Grind.EMatch.Cnstr : Type

We represent an E-matching problem as a list of constraints.

• match (pat e : Lean.Expr) : Lean.Meta.Grind.EMatch.Cnstr

  Matches pattern pat with term e

• continue (pat : Lean.Expr) : Lean.Meta.Grind.EMatch.Cnstr

  This constraint is used to encode multi-patterns.

instance Lean.Meta.Grind.EMatch.instInhabitedCnstr : Inhabited Lean.Meta.Grind.EMatch.Cnstr

Equations

• Lean.Meta.Grind.EMatch.instInhabitedCnstr = { default := Lean.Meta.Grind.EMatch.Cnstr.match default default }

structure Lean.Meta.Grind.EMatch.Choice : Type

Choice point for the backtracking search. The state of the procedure contains a stack of choices.

• cnstrs : List Lean.Meta.Grind.EMatch.Cnstr

  Contraints to be processed.

• gen : Nat

  Maximum term generation found so far.

• assignment : Array Lean.Expr

  Partial assignment so far. Recall that pattern variables are encoded as de-Bruijn variables.

instance Lean.Meta.Grind.EMatch.instInhabitedChoice : Inhabited Lean.Meta.Grind.EMatch.Choice

Equations

• Lean.Meta.Grind.EMatch.instInhabitedChoice = { default := { cnstrs := default, gen := default, assignment := default } }

structure Lean.Meta.Grind.EMatch.Context : Type

Context for the E-matching monad.

• useMT : Bool

  useMT is true if we are using the mod-time optimization. It is always set to false for new EMatchTheorems.

• thm : Lean.Meta.Grind.EMatchTheorem

  EMatchTheorem being processed.

instance Lean.Meta.Grind.EMatch.instInhabitedContext : Inhabited Lean.Meta.Grind.EMatch.Context

Equations

• Lean.Meta.Grind.EMatch.instInhabitedContext = { default := { useMT := default, thm := default } }

structure Lean.Meta.Grind.EMatch.State : Type

State for the E-matching monad

• choiceStack : List Lean.Meta.Grind.EMatch.Choice

  Choices that still have to be processed.

instance Lean.Meta.Grind.EMatch.instInhabitedState : Inhabited Lean.Meta.Grind.EMatch.State

Equations

• Lean.Meta.Grind.EMatch.instInhabitedState = { default := { choiceStack := default } }

@[reducible, inline]

abbrev Lean.Meta.Grind.EMatch.M (α : Type) : Type

Equations

• Lean.Meta.Grind.EMatch.M = ReaderT Lean.Meta.Grind.EMatch.Context (StateRefT' IO.RealWorld Lean.Meta.Grind.EMatch.State Lean.Meta.Grind.GoalM)

def Lean.Meta.Grind.EMatch.M.run' {α : Type} (x : Lean.Meta.Grind.EMatch.M α) : Lean.Meta.Grind.GoalM α

Equations

• x.run' = (x { useMT := true, thm := default }).run' { choiceStack := [] }

def Lean.Meta.Grind.EMatch.ematchTheorem (thm : Lean.Meta.Grind.EMatchTheorem) : Lean.Meta.Grind.EMatch.M Unit

Equations

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

def Lean.Meta.Grind.EMatch.ematchTheorem.tryAll (ps : List Lean.Expr) (cs : List Lean.Meta.Grind.EMatch.Cnstr) : Lean.Meta.Grind.EMatch.M Unit

When using the mod-time optimization with multi-patterns, we must start ematching at each different pattern. That is, if we have [p₁, p₂, p₃], we must execute

• main p₁ [.continue p₂, .continue p₃]
• main p₂ [.continue p₁, .continue p₃]
• main p₃ [.continue p₁, .continue p₂]

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.EMatch.ematchTheorem.tryAll [] cs = pure ()

def Lean.Meta.Grind.EMatch.ematchTheorems (thms : Lean.PArray Lean.Meta.Grind.EMatchTheorem) : Lean.Meta.Grind.EMatch.M Unit

Equations

• Lean.Meta.Grind.EMatch.ematchTheorems thms = Lean.PersistentArray.forM thms Lean.Meta.Grind.EMatch.ematchTheorem

def Lean.Meta.Grind.ematch : Lean.Meta.Grind.GoalM Unit

Performs one round of E-matching, and returns new instances.

Equations

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

def Lean.Meta.Grind.ematchAndAssert? (goal : Lean.Meta.Grind.Goal) : Lean.Meta.Grind.GrindM (Option (List Lean.Meta.Grind.Goal))

Performs one round of E-matching, and assert new instances.

Equations

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

def Lean.Meta.Grind.ematchStar (goal : Lean.Meta.Grind.Goal) : Lean.Meta.Grind.GrindM (List Lean.Meta.Grind.Goal)

Equations

• Lean.Meta.Grind.ematchStar goal = Lean.Meta.Grind.iterate goal Lean.Meta.Grind.ematchAndAssert?