source
structure Aesop.ForwardIndex :
Type

Index for forward rules.

- tree : Lean.Meta.DiscrTree (ForwardRule × PremiseIndex)

  Maps expressions `T` to all tuples `(r, i)` where `r : ForwardRule`, `i : PremiseIndex` and the `i`-th argument of the type of `r.expr` (counting from zero) likely unifies with `T`.

- nameToRule : Lean.PHashMap RuleName ForwardRule

  Indexes the forward rules contained in `tree` by name.

- constRules : Lean.PHashSet ForwardRule

  Constant forward rules, i.e. forward rules that have no premises and no rule pattern.

Instances For

source
instance Aesop.instInhabitedForwardIndex :
Inhabited ForwardIndex
Equations

- Aesop.instInhabitedForwardIndex = { default := Aesop.instInhabitedForwardIndex.default }

source
def Aesop.instInhabitedForwardIndex.default :
ForwardIndex
Equations

- Aesop.instInhabitedForwardIndex.default = { tree := default, nameToRule := default, constRules := default }

Instances For

source
instance Aesop.ForwardIndex.instEmptyCollection :
EmptyCollection ForwardIndex
Equations

- Aesop.ForwardIndex.instEmptyCollection = { emptyCollection := { tree := { }, nameToRule := { }, constRules := ∅ } }

source
def Aesop.ForwardIndex.trace (traceOpt : TraceOption) (idx : ForwardIndex) :
Lean.CoreM Unit

Trace the rules contained in `idx` if `traceOpt` is enabled.

Equations

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

Instances For

source
def Aesop.ForwardIndex.merge (idx₁ idx₂ : ForwardIndex) :
ForwardIndex

Merge two indices.

Equations

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

Instances For

source
def Aesop.ForwardIndex.insert (r : ForwardRule) (idx : ForwardIndex) :
ForwardIndex

Insert a forward rule into the `ForwardIndex`.

Equations

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

Instances For

source
def Aesop.ForwardIndex.get (idx : ForwardIndex) (e : Lean.Expr) :
Lean.MetaM (Array (ForwardRule × PremiseIndex))

Get the forward rules whose maximal premises likely unify with `e`. Each returned pair `(r, i)` contains a rule `r` and the index `i` of the premise of `r` that likely unifies with `e`.

Equations

- idx.get e = Aesop.getUnify idx.tree e

Instances For

source
def Aesop.ForwardIndex.getRuleWithName? (n : RuleName) (idx : ForwardIndex) :
Option ForwardRule

Get the forward rule with the given rule name.

Equations

- Aesop.ForwardIndex.getRuleWithName? n idx = idx.nameToRule[n]

Instances For

source
def Aesop.ForwardIndex.getConstRuleMatches (idx : ForwardIndex) :
Array ForwardRuleMatch

Get forward rule matches for the constant forward rules (i.e., those with no premises and no rule pattern). Accordingly, the returned matches contain no hypotheses.

Equations

- idx.getConstRuleMatches = Lean.PersistentHashSet.fold (fun (ms : Array Aesop.ForwardRuleMatch) (r : Aesop.ForwardRule) => ms.push { rule := r, «match» := ∅ }) #[] idx.constRules

Instances For