Discrimination Tree for the Symbolic Simulation Framework

This module provides pattern insertion into discrimination trees for the symbolic simulation framework. Unlike the standard DiscrTree insertion which works with arbitrary expressions, this module converts Pattern values (see Sym/Pattern.lean) into discrimination tree keys. Pattern values have been preprocessed and use de Bruijn variables for wildcards instead of metavariables.

Key Design Decisions

The conversion from Pattern to Array Key respects the structural matching semantics of Sym:

1. Proof and instance arguments are wildcards. When building keys for a function application, arguments marked as proofs or instances in ProofInstInfo are replaced with Key.star. This ensures that during retrieval, terms differing only in proof/instance arguments will match the same entries.

2. Bound variables are wildcards. Pattern variables (represented as de Bruijn indices in Pattern.pattern) become Key.star, allowing them to match any subterm during retrieval.

3. noindex annotations are respected. Subterms annotated with noindex become Key.star.

Usage

Use insertPattern to add a pattern to a discrimination tree:

let tree := insertPattern tree pattern value

Retrieval should use the standard DiscrTree.getMatch or similar, which will find all patterns whose key sequence is compatible with the query term.

def Lean.Meta.Sym.Pattern.mkDiscrTreeKeys (p : Pattern) : Array DiscrTree.Key

Converts a Pattern into a discrimination tree key sequence.

Equations

• p.mkDiscrTreeKeys = Lean.Meta.Sym.mkPathAux✝ true p.fnInfos ((Array.mkEmpty Lean.Meta.Sym.initCapacity✝).push p.pattern) (Array.mkEmpty Lean.Meta.Sym.initCapacity✝¹)

def Lean.Meta.Sym.insertPattern {α : Type} [BEq α] (d : DiscrTree α) (p : Pattern) (v : α) : DiscrTree α

Inserts a pattern into a discrimination tree, associating it with value v.

Equations

• Lean.Meta.Sym.insertPattern d p v = d.insertKeyValue p.mkDiscrTreeKeys v

def Lean.Meta.Sym.getMatch {α : Type} (d : DiscrTree α) (e : Expr) : Array α

Retrieves all values whose patterns match the expression e.

Equations

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

def Lean.Meta.Sym.getMatchWithExtra {α : Type} (d : DiscrTree α) (e : Expr) : Array (α × Nat)

Retrieves all values whose patterns match a prefix of e, along with the number of extra (ignored) arguments.

This is useful for rewriting: if a pattern matches f x but e is f x y z, we can still apply the rewrite and return (value, 2) indicating 2 extra arguments.

Equations

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