Documentation

instance Lean.Meta.Grind.instInhabitedOrigin :

Inhabited Origin

Equations

Lean.Meta.Grind.instInhabitedOrigin = { default := Lean.Meta.Grind.Origin.decl default }

instance Lean.Meta.Grind.instReprOrigin :

Repr Origin

Equations

Lean.Meta.Grind.instReprOrigin = { reprPrec := Lean.Meta.Grind.reprOrigin✝ }

instance Lean.Meta.Grind.instBEqOrigin :

BEq Origin

Equations

Lean.Meta.Grind.instBEqOrigin = { beq := Lean.Meta.Grind.beqOrigin✝ }

def Lean.Meta.Grind.Origin.key :

Origin → Name

A unique identifier corresponding to the origin.

Equations

(Lean.Meta.Grind.Origin.decl a).key = a
(Lean.Meta.Grind.Origin.fvar a).key = a.name
(Lean.Meta.Grind.Origin.stx a a_1).key = a
(Lean.Meta.Grind.Origin.local a).key = a

def Lean.Meta.Grind.Origin.pp {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (o : Origin) :

m MessageData

Equations

(Lean.Meta.Grind.Origin.decl a).pp = do let __do_lift ← Lean.mkConstWithLevelParams a pure (Lean.MessageData.ofConst __do_lift)
(Lean.Meta.Grind.Origin.fvar a).pp = pure (Lean.MessageData.ofExpr (Lean.mkFVar a))
(Lean.Meta.Grind.Origin.stx a a_1).pp = pure (Lean.MessageData.ofSyntax a_1)
(Lean.Meta.Grind.Origin.local a).pp = pure (Lean.MessageData.ofName a)

instance Lean.Meta.Grind.instBEqOrigin_1 :

BEq Origin

Equations

Lean.Meta.Grind.instBEqOrigin_1 = { beq := fun (a b : Lean.Meta.Grind.Origin) => a.key == b.key }

instance Lean.Meta.Grind.instHashableOrigin :

Hashable Origin

Equations

Lean.Meta.Grind.instHashableOrigin = { hash := fun (a : Lean.Meta.Grind.Origin) => hash a.key }

inductive Lean.Meta.Grind.EMatchTheoremKind :

Instances For

Inhabited EMatchTheoremKind

instance Lean.Meta.Grind.instInhabitedEMatchTheoremKind :

Equations

Lean.Meta.Grind.instInhabitedEMatchTheoremKind = { default := Lean.Meta.Grind.EMatchTheoremKind.eqLhs }

instance Lean.Meta.Grind.instBEqEMatchTheoremKind :

BEq EMatchTheoremKind

Equations

Lean.Meta.Grind.instBEqEMatchTheoremKind = { beq := Lean.Meta.Grind.beqEMatchTheoremKind✝ }

instance Lean.Meta.Grind.instReprEMatchTheoremKind :

Repr EMatchTheoremKind

Equations

Lean.Meta.Grind.instReprEMatchTheoremKind = { reprPrec := Lean.Meta.Grind.reprEMatchTheoremKind✝ }

Hashable EMatchTheoremKind

instance Lean.Meta.Grind.instHashableEMatchTheoremKind :

Equations

Lean.Meta.Grind.instHashableEMatchTheoremKind = { hash := Lean.Meta.Grind.hashEMatchTheoremKind✝ }

structure Lean.Meta.Grind.EMatchTheorem :

A theorem for heuristic instantiation based on E-matching.

levelParams : Array Name
It stores universe parameter names for universe polymorphic proofs. Recall that it is non-empty only when we elaborate an expression provided by the user. When proof is just a constant, we can use the universe parameter names stored in the declaration.
proof : Expr
numParams : Nat
patterns : List Expr
symbols : List HeadIndex
Contains all symbols used in pattterns.
origin : Origin
kind : EMatchTheoremKind
The kind is used for generating the patterns. We save it here to implement grind?.

Instances For

Lean.Meta.Grind.instInhabitedEMatchTheorem

instance Lean.Meta.Grind.instInhabitedEMatchTheorem :

Inhabited EMatchTheorem

Equations

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

structure Lean.Meta.Grind.EMatchTheorems :

Set of E-matching theorems.

smap : Lean.PHashMap Lean.Name (List Lean.Meta.Grind.EMatchTheorem)
The key is a symbol from EMatchTheorem.symbols.
origins : Lean.PHashSet Lean.Meta.Grind.Origin
Set of theorem ids that have been inserted using insert.
erased : Lean.PHashSet Lean.Meta.Grind.Origin
Theorems that have been marked as erased
omap : Lean.PHashMap Lean.Meta.Grind.Origin (List Lean.Meta.Grind.EMatchTheorem)
Mapping from origin to E-matching theorems associated with this origin.

Instances For

Lean.Meta.Grind.instInhabitedEMatchTheorems

instance Lean.Meta.Grind.instInhabitedEMatchTheorems :

Inhabited EMatchTheorems

Equations

Lean.Meta.Grind.instInhabitedEMatchTheorems = { default := { smap := default, origins := default, erased := default, omap := default } }

def Lean.Meta.Grind.EMatchTheorems.insert (s : EMatchTheorems) (thm : EMatchTheorem) :

EMatchTheorems

Inserts a thm with symbols [s_1, ..., s_n] to s. We add s_1 -> { thm with symbols := [s_2, ..., s_n] }. When grind internalizes a term containing symbol s, we process all theorems thm associated with key s. If their thm.symbols is empty, we say they are activated. Otherwise, we reinsert into map.

Equations

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

def Lean.Meta.Grind.EMatchTheorems.contains (s : EMatchTheorems) (origin : Origin) :

Bool

Returns true if s contains a theorem with the given origin.

Equations

s.contains origin = Lean.PersistentHashSet.contains (Lean.Meta.Grind.EMatchTheorems.origins✝ s) origin

def Lean.Meta.Grind.EMatchTheorems.erase (s : EMatchTheorems) (origin : Origin) :

EMatchTheorems

Mark the theorem with the given origin as erased

Equations

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

def Lean.Meta.Grind.EMatchTheorems.isErased (s : EMatchTheorems) (origin : Origin) :

Bool

Returns true if the theorem has been marked as erased.

Equations

s.isErased origin = Lean.PersistentHashSet.contains (Lean.Meta.Grind.EMatchTheorems.erased✝ s) origin

@[inline]

def Lean.Meta.Grind.EMatchTheorems.retrieve? (s : EMatchTheorems) (sym : Name) :

Option (List EMatchTheorem × EMatchTheorems)

Retrieves theorems from s associated with the given symbol. See EMatchTheorem.insert. The theorems are removed from s.

Equations

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

def Lean.Meta.Grind.EMatchTheorems.find (s : EMatchTheorems) (origin : Origin) :

List EMatchTheorem

Returns theorems associated with the given origin.

Equations

s.find origin = match Lean.PersistentHashMap.find? (Lean.Meta.Grind.EMatchTheorems.omap✝ s) origin with | some thms => thms | x => []

def Lean.Meta.Grind.EMatchTheorem.getProofWithFreshMVarLevels (thm : EMatchTheorem) :

MetaM Expr

Equations

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

def Lean.Meta.Grind.isEMatchTheorem (declName : Name) :

CoreM Bool

Returns true if declName has been tagged as an E-match theorem using [grind].

Equations

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

def Lean.Meta.Grind.resetEMatchTheoremsExt :

CoreM Unit

Equations

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

partial def Lean.Meta.Grind.splitWhileForbidden (pat : Expr) :

List Expr

Auxiliary function to expand a pattern containing forbidden application symbols into a multi-pattern.

This function enhances the usability of the [grind =] attribute by automatically handling forbidden pattern symbols. For example, consider the following theorem tagged with this attribute:

getLast?_eq_some_iff {xs : List α} {a : α} : xs.getLast? = some a ↔ ∃ ys, xs = ys ++ [a]

Here, the selected pattern is xs.getLast? = some a, but Eq is a forbidden pattern symbol. Instead of producing an error, this function converts the pattern into a multi-pattern, allowing the attribute to be used conveniently.

The function recursively expands patterns with forbidden symbols by splitting them into their sub-components. If the pattern does not contain forbidden symbols, it is returned as-is.

def Lean.Meta.Grind.mkGroundPattern (e : Expr) :

Expr

Equations

Lean.Meta.Grind.mkGroundPattern e = Lean.mkAnnotation `grind.ground_pat e

def Lean.Meta.Grind.groundPattern? (e : Expr) :

Option Expr

Equations

Lean.Meta.Grind.groundPattern? e = Lean.annotation? `grind.ground_pat e

def Lean.Meta.Grind.isPatternDontCare (e : Expr) :

Bool

Equations

Lean.Meta.Grind.isPatternDontCare e = (e == Lean.Meta.Grind.dontCare✝)

partial def Lean.Meta.Grind.ppPattern (pattern : Expr) :

MessageData

partial def Lean.Meta.Grind.ppPattern.ppArg (arg : Expr) :

MessageData

structure Lean.Meta.Grind.NormalizePattern.State :

symbols : Array HeadIndex
symbolSet : Std.HashSet HeadIndex
bvarsFound : Std.HashSet Nat

@[reducible, inline]

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

Equations

Lean.Meta.Grind.NormalizePattern.M = StateRefT' IO.RealWorld Lean.Meta.Grind.NormalizePattern.State Lean.MetaM

def Lean.Meta.Grind.NormalizePattern.getPatternSupportMask (f : Expr) (numArgs : Nat) :

MetaM (Array Bool)

Returns a bit-mask mask s.t. mask[i] is true if the corresponding argument is

a type (that is not a proposition) or type former (which has forward dependencies) or
a proof, or
an instance implicit argument

When mask[i], we say the corresponding argument is a "support" argument.

Equations

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

def Lean.Meta.Grind.NormalizePattern.main (patterns : List Expr) :

MetaM (List Expr × List HeadIndex × Std.HashSet Nat)

Equations

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

def Lean.Meta.Grind.NormalizePattern.normalizePattern (e : Expr) :

M Expr

Equations

Lean.Meta.Grind.NormalizePattern.normalizePattern e = Lean.Meta.Grind.NormalizePattern.go✝ e

inductive Lean.Meta.Grind.CheckCoverageResult :

Auxiliary type for the checkCoverage function.

ok : CheckCoverageResult
checkCoverage succeeded
missing (pos : List Nat) : CheckCoverageResult
checkCoverage failed because some of the theorem parameters are missing, pos contains their positions

def Lean.Meta.Grind.mkEMatchTheoremCore (origin : Origin) (levelParams : Array Name) (numParams : Nat) (proof : Expr) (patterns : List Expr) (kind : EMatchTheoremKind) :

Creates an E-matching theorem for a theorem with proof proof, numParams parameters, and the given set of patterns. Pattern variables are represented using de Bruijn indices.

Equations

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

def Lean.Meta.Grind.mkEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) (kind : EMatchTheoremKind) :

Creates an E-matching theorem for declName with numParams parameters, and the given set of patterns. Pattern variables are represented using de Bruijn indices.

Equations

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

def Lean.Meta.Grind.mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) (normalizePattern useLhs : Bool) :

Given a theorem with proof proof and type of the form ∀ (a_1 ... a_n), lhs = rhs, creates an E-matching pattern for it using addEMatchTheorem n [lhs] If normalizePattern is true, it applies the grind simplification theorems and simprocs to the pattern.

Equations

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

def Lean.Meta.Grind.mkEMatchEqBwdTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) :

Equations

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

def Lean.Meta.Grind.mkEMatchEqTheorem (declName : Name) (normalizePattern useLhs : Bool := true) :

Given theorem with name declName and type of the form ∀ (a_1 ... a_n), lhs = rhs, creates an E-matching pattern for it using addEMatchTheorem n [lhs]

If normalizePattern is true, it applies the grind simplification theorems and simprocs to the pattern.

Equations

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

def Lean.Meta.Grind.addEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) (kind : EMatchTheoremKind) :

MetaM Unit

Adds an E-matching theorem to the environment. See mkEMatchTheorem.

Equations

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

def Lean.Meta.Grind.addEMatchEqTheorem (declName : Name) :

MetaM Unit

Adds an E-matching equality theorem to the environment. See mkEMatchEqTheorem.

Equations

Lean.Meta.Grind.addEMatchEqTheorem declName = do let __do_lift ← Lean.Meta.Grind.mkEMatchEqTheorem declName Lean.ScopedEnvExtension.add Lean.Meta.Grind.ematchTheoremsExt✝ __do_lift

def Lean.Meta.Grind.getEMatchTheorems :

CoreM EMatchTheorems

Returns the E-matching theorems registered in the environment.

Equations

Lean.Meta.Grind.getEMatchTheorems = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.Grind.ematchTheoremsExt✝ __do_lift)