Encoding an Expr as a sequence of Keys

We compute the encoding of an expression in a lazy way. This means computing only one Key at a time and storing the state of the remaining computation in a LazyEntry.

Each step is computed by evalLazyEntryWithEta : LazyEntry → MetaM (Option (List (Key × LazyEntry))). It returns none when the last Key has already been reached.

The first step, which is used when initializing the tree, is computed by initializeLazyEntryWithEta.

To compute all the keys at once, we have

• encodeExprWithEta, which computes all possible key sequences.
• encodeExpr, which computes the canonical key sequence. This will be used for expressions that are looked up in a RefinedDiscrTree using getMatch.

@[inline]

def Lean.Meta.RefinedDiscrTree.initializeLazyEntryWithEtaAux (e : Expr) (labelledStars : Bool) : MetaM (List (Key × LazyEntry))

Encode e as a sequence of keys, computing only the first Key.

Equations

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

def Lean.Meta.RefinedDiscrTree.initializeLazyEntryWithEta (e : Expr) (labelledStars : Bool := true) : MetaM (List (Key × LazyEntry))

Encode e as a sequence of keys, computing only the first Key.

Equations

• Lean.Meta.RefinedDiscrTree.initializeLazyEntryWithEta e labelledStars = Lean.Meta.withReducible (Lean.Meta.RefinedDiscrTree.initializeLazyEntryWithEtaAux e labelledStars)

def Lean.Meta.RefinedDiscrTree.evalLazyEntry (entry : LazyEntry) (eta : Bool) : MetaM (Option (List (Key × LazyEntry)))

A single step in evaluating a LazyEntry. Allow multiple different outcomes.

Equations

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

def Lean.Meta.RefinedDiscrTree.encodeExprWithEta (e : Expr) (labelledStars : Bool) : MetaM (Array (Array Key))

Return all encodings of e as a Array Key. This is used for testing.

Equations

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

partial def Lean.Meta.RefinedDiscrTree.encodeExprWithEta.go (todo : Array (Array Key × LazyEntry)) (result : Array (Array Key)) : MetaM (Array (Array Key))

The main loop for encodeExpr.

partial def Lean.Meta.RefinedDiscrTree.encodeExprWithEta.go.fold (keys : Array Key) (xs : List (Key × LazyEntry)) (todo : Array (Array Key × LazyEntry)) : Array (Array Key × LazyEntry)

This variation on List.fold ensures that the array keys isn't copied unnecessarily.

partial def Lean.Meta.RefinedDiscrTree.LazyEntry.toList (entry : LazyEntry) (result : List Key := []) : MetaM (List Key)

Completely evaluate a LazyEntry.

def Lean.Meta.RefinedDiscrTree.encodeExpr (e : Expr) (labelledStars : Bool) : MetaM (Key × List Key)

Return the canonical encoding of e as a Array Key. This is used for looking up e in a RefinedDiscrTree.

Equations

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