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 (gen? : Option GenPatternInfo) (pat e : Expr) : Cnstr

  Matches pattern pat with term e

• offset (gen? : Option GenPatternInfo) (pat : Expr) (k : Nat) (e : Expr) : Cnstr

  Matches offset pattern pat+k with term e

• continue (pat : Expr) : Cnstr

  This constraint is used to encode multi-patterns.

def Lean.Meta.Grind.EMatch.instInhabitedCnstr.default : Cnstr

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

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 Cnstr

  Constraints to be processed.

• gen : Nat

  Maximum term generation found so far.

• assignment : Array Expr

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

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

def Lean.Meta.Grind.EMatch.instInhabitedChoice.default : Choice

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 : EMatchTheorem

  EMatchTheorem being processed.

• initApp : Expr

  Initial application used to start E-matching

def Lean.Meta.Grind.EMatch.instInhabitedContext.default : Context

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

@[reducible, inline]

abbrev Lean.Meta.Grind.EMatch.InstanceMap : Type

A mapping uniqueId ↦ thm, where uniqueId is an auxiliary marker used to wrap a theorem instantiation proof of thm using a Expr.mdata. The uniqueIds are created using mkFreshId.

def Lean.Meta.Grind.EMatch.isTheoremInstanceProof? (proof : Expr) : Option Name

Returns some uniqueId if proof was marked using markTheoremInstanceProof

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

State for the E-matching monad

• choiceStack : List Choice

  Choices that still have to be processed.

• instanceMap : InstanceMap

  When tracing is enabled track instances here. See comment at InstanceMap

instance Lean.Meta.Grind.EMatch.instInhabitedSearchState : Inhabited SearchState

def Lean.Meta.Grind.EMatch.instInhabitedSearchState.default : SearchState

@[reducible, inline]

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

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

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

def Lean.Meta.Grind.GenPatternInfo.assign? (genInfo : GenPatternInfo) (c : EMatch.Choice) (x : Expr) : OptionT GoalM EMatch.Choice

def Lean.Meta.Grind.EMatch.doElemReportEMatchIssue!__ : ParserDescr

Similar to reportIssue!, but only reports issue if grind.debug is set to true

def Lean.Meta.Grind.EMatch.checkSize (e : Expr) (threshold : Nat) : MetaM Bool

Helper function for checking grind pattern constraints of the form size e < threshold Implicit arguments and type information in lambdas and let-expressions are ignored.

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

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

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

def Lean.Meta.Grind.ematch' (extraThms : Array EMatchTheorem := #[]) : GoalM (Bool × EMatch.InstanceMap)

Performs one round of E-matching, and returns true if new instances were generated. Recall that the mapping is nonempty only if tracing is enabled.

def Lean.Meta.Grind.ematch (extraThms : Array EMatchTheorem := #[]) : GoalM Bool

Performs one round of E-matching, and returns true if new instances were generated.

def Lean.Meta.Grind.ematchOnly (thms : Array EMatchTheorem) : GoalM Bool

Performs one round of E-matching using the giving theorems, and returns true if new instances were generated.