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

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

Instances For

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

- Lean.Meta.Grind.EMatch.instInhabitedCnstr.default = Lean.Meta.Grind.EMatch.Cnstr.match default default default

Instances For

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

- Lean.Meta.Grind.EMatch.instInhabitedCnstr = { default := Lean.Meta.Grind.EMatch.instInhabitedCnstr.default }

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

Instances For

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

- Lean.Meta.Grind.EMatch.instInhabitedChoice = { default := Lean.Meta.Grind.EMatch.instInhabitedChoice.default }

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

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

Instances For

source
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 `EMatchTheorem`s.

- thm : EMatchTheorem

  `EMatchTheorem` being processed.

- initApp : Expr

  Initial application used to start E-matching

Instances For

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

- Lean.Meta.Grind.EMatch.instInhabitedContext.default = { useMT := default }

Instances For

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

- Lean.Meta.Grind.EMatch.instInhabitedContext = { default := Lean.Meta.Grind.EMatch.instInhabitedContext.default }

source
@[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 `uniqueId`s are created using `mkFreshId`.

Equations

- Lean.Meta.Grind.EMatch.InstanceMap = Std.HashMap Lean.Name Lean.Meta.Grind.EMatchTheorem

Instances For

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

Returns `some uniqueId` if `proof` was marked using `markTheoremInstanceProof`

Equations

- One or more equations did not get rendered due to their size.
- Lean.Meta.Grind.EMatch.isTheoremInstanceProof? proof = none

Instances For

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

Instances For

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

- Lean.Meta.Grind.EMatch.instInhabitedSearchState = { default := Lean.Meta.Grind.EMatch.instInhabitedSearchState.default }

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

- Lean.Meta.Grind.EMatch.instInhabitedSearchState.default = { choiceStack := default, instanceMap := default }

Instances For

source
@[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.SearchState Lean.Meta.Grind.GoalM)

Instances For

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

- x.run' = (x { }).run' { }

Instances For

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

- x.run = (x { }).run { }

Instances For

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

- genInfo.assign? c x = do let c ← Lean.Meta.Grind.EMatch.assign?✝ c genInfo.xIdx x let c ← Lean.Meta.Grind.EMatch.assignDelayedEqProof?✝ c genInfo.hIdx pure c

Instances For

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

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

Equations

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

Instances For

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

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

Instances For

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

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

Instances For

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

Equations

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

Instances For

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

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

Equations

- Lean.Meta.Grind.ematch extraThms = do let __do_lift ← Lean.Meta.Grind.ematch' extraThms pure __do_lift.fst

Instances For

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

Equations

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

Instances For