7120d9aef5
This PR adds eta reduction to the sym discrimination tree lookup functions (`getMatch`, `getMatchWithExtra`, `getMatchLoop`). Without this, expressions like `StateM Nat` that unfold to eta-expanded forms `(fun α => StateT Nat Id α)` fail to match discrimination tree entries for the eta-reduced form `(StateT Nat Id)`. Also optimizes `etaReduce` with an early exit for non-lambda expressions and removes a redundant `n == 0` check. Includes a test verifying that `P (StateM Nat)` matches a disc tree entry for `P (StateT Nat Id)`. Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
20 lines
663 B
Text
20 lines
663 B
Text
import Lean.Meta.Sym
|
||
|
||
open Lean Meta Sym
|
||
|
||
opaque P : (Type → Type) → Prop
|
||
axiom stateT_P : P (StateT Nat Id)
|
||
|
||
/--
|
||
info: disc tree lookup match count: 1
|
||
-/
|
||
#guard_msgs in
|
||
#eval show MetaM Unit from do
|
||
-- `StateM Nat` unfolds to `fun α => StateT Nat Id α` (an eta redex)
|
||
let e ← Sym.unfoldReducible (mkApp (mkConst ``P) (mkApp (mkConst ``StateM [0]) (mkConst ``Nat)))
|
||
-- Verify the eta redex is present
|
||
assert! e.appArg!.isLambda
|
||
let pat ← mkPatternFromDecl ``stateT_P
|
||
let dt := Sym.insertPattern (Lean.Meta.DiscrTree.empty (α := Unit)) pat ()
|
||
let nMatches := (Sym.getMatch dt e).size
|
||
logInfo m!"disc tree lookup match count: {nMatches}"
|