@[reducible, inline]

abbrev Aesop.RulePatternSubstMap : Type

A map from rule names to rule pattern substitutions. When run on a goal, the rule pattern index returns such a map.

Equations

• Aesop.RulePatternSubstMap = Std.HashMap Aesop.RuleName (Std.HashSet Aesop.Substitution)

def Aesop.RulePatternSubstMap.insertArray (xs : Array (RuleName × Substitution)) (m : RulePatternSubstMap) : RulePatternSubstMap

Insert an array of rule pattern substitutions into a rule pattern substitution map.

Equations

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

def Aesop.RulePatternSubstMap.ofArray (xs : Array (RuleName × Substitution)) : RulePatternSubstMap

Build a rule pattern substitution map from an array of substitutions.

Equations

• Aesop.RulePatternSubstMap.ofArray xs = Aesop.RulePatternSubstMap.insertArray xs ∅

def Aesop.RulePatternSubstMap.toFlatArray (m : RulePatternSubstMap) : Array (RuleName × Substitution)

Convert a rule pattern substitution map to a flat array of substitutions.

Equations

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

structure Aesop.RulePatternIndex.Entry : Type

An entry of the rule pattern index.

• name : RuleName

  The name of the rule to which the pattern belongs.

• pattern : RulePattern

  The rule's pattern. We assume that there is at most one pattern per rule.

instance Aesop.RulePatternIndex.instInhabitedEntry : Inhabited Entry

Equations

• Aesop.RulePatternIndex.instInhabitedEntry = { default := { name := default, pattern := default } }

instance Aesop.instBEqEntry : BEq RulePatternIndex.Entry

Equations

• Aesop.instBEqEntry = { beq := fun (e₁ e₂ : Aesop.RulePatternIndex.Entry) => e₁.name == e₂.name }

structure Aesop.RulePatternIndex : Type

A rule pattern index. Maps expressions e to rule patterns that likely unify with e.

• tree : Lean.Meta.DiscrTree Entry

  The index.

• isEmpty : Bool

  true iff the index contains no patterns.

instance Aesop.instInhabitedRulePatternIndex : Inhabited RulePatternIndex

Equations

• Aesop.instInhabitedRulePatternIndex = { default := { tree := default, isEmpty := default } }

instance Aesop.RulePatternIndex.instEmptyCollection : EmptyCollection RulePatternIndex

Equations

• Aesop.RulePatternIndex.instEmptyCollection = { emptyCollection := { tree := { }, isEmpty := true } }

def Aesop.RulePatternIndex.add (name : RuleName) (pattern : RulePattern) (idx : RulePatternIndex) : RulePatternIndex

Add a rule pattern to the index.

Equations

• Aesop.RulePatternIndex.add name pattern idx = { tree := idx.tree.insertCore pattern.discrTreeKeys { name := name, pattern := pattern }, isEmpty := false }

def Aesop.RulePatternIndex.merge (idx₁ idx₂ : RulePatternIndex) : RulePatternIndex

Merge two rule pattern indices. Patterns that appear in both indices appear twice in the result.

Equations

• idx₁.merge idx₂ = if idx₁.isEmpty = true then idx₂ else if idx₂.isEmpty = true then idx₁ else { tree := idx₁.tree.mergePreservingDuplicates idx₂.tree, isEmpty := false }

def Aesop.RulePatternIndex.getSingle (e : Lean.Expr) (idx : RulePatternIndex) : BaseM (Array (RuleName × Substitution))

Get rule pattern substitutions for the patterns that match e.

Equations

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

def Aesop.RulePatternIndex.getCore (e : Lean.Expr) (idx : RulePatternIndex) : BaseM (Array (RuleName × Substitution))

Get all substitutions of the rule patterns that match a subexpression of e. Subexpressions containing bound variables are not considered. The returned array may contain duplicates.

Equations

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

def Aesop.RulePatternIndex.getCore.getSubexpr (idx : RulePatternIndex) (e : Lean.Expr) : StateRefT' IO.RealWorld (Array (RuleName × Substitution)) BaseM Unit

Equations

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

def Aesop.RulePatternIndex.get (e : Lean.Expr) (idx : RulePatternIndex) : BaseM RulePatternSubstMap

Get all substitutions of the rule patterns that match a subexpression of e. Subexpressions containing bound variables are not considered. The returned array may contain duplicates.

Equations

• Aesop.RulePatternIndex.get e idx = Aesop.RulePatternSubstMap.ofArray <$> Aesop.RulePatternIndex.getCore e idx

def Aesop.RulePatternIndex.getInLocalDeclCore (acc : RulePatternSubstMap) (ldecl : Lean.LocalDecl) (idx : RulePatternIndex) : BaseM RulePatternSubstMap

Get all substitutions of the rule patterns that match a subexpression of the given local declaration. Subexpressions containing bound variables are not considered.

Equations

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

def Aesop.RulePatternIndex.getInLocalDecl (ldecl : Lean.LocalDecl) (idx : RulePatternIndex) : BaseM RulePatternSubstMap

Get all substitutions of the rule patterns that match a subexpression of the given local declaration. Subexpressions containing bound variables are not considered.

Equations

• Aesop.RulePatternIndex.getInLocalDecl ldecl idx = Aesop.RulePatternIndex.getInLocalDeclCore ∅ ldecl idx

def Aesop.RulePatternIndex.getInGoal (goal : Lean.MVarId) (idx : RulePatternIndex) : BaseM RulePatternSubstMap

Get all substitutions of the rule patterns that match a subexpression of a hypothesis or the target. Subexpressions containing bound variables are not considered.

Equations

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