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.

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.

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.

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.

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.