5042c8cc37
This PR implements `isDefEqS`, a lightweight structural definitional equality for the symbolic simulation framework. Unlike the full `isDefEq`, it avoids expensive operations while still supporting Miller pattern unification. **Key features:** - Structural matching with optional zeta-delta reduction for let-declarations - Miller pattern detection and assignment (`?m x y z := rhs` → `?m := fun x y z => rhs`) - Scope checking via `maxFVar` to prevent out-of-scope assignments - Proof arguments skipped via proof irrelevance - Instance arguments delegated to full `isDefEq` (need TC machinery) - Universe levels treated structurally (`max`/`imax` as uninterpreted)
67 lines
1.6 KiB
Text
67 lines
1.6 KiB
Text
import Lean.Meta.Sym
|
|
set_option grind.debug true
|
|
open Lean Meta Grind Sym
|
|
|
|
def tst1 : SymM Unit := do
|
|
let f ← mkConstS `f
|
|
let e ← mkAppS (← mkAppS (← mkAppS f (← mkBVarS 0)) (← mkBVarS 1)) (← shareCommon (mkNatLit 1))
|
|
let a ← mkConstS `a
|
|
let b ← mkConstS `b
|
|
let r ← instantiateRevS e #[a, b]
|
|
assert! r == e.instantiateRev #[a, b]
|
|
logInfo r
|
|
let r ← instantiateS e #[a, b]
|
|
assert! r == e.instantiate #[a, b]
|
|
logInfo r
|
|
let e ← mkLambdaS `x .default (← mkConstS ``Nat) e
|
|
let r ← instantiateRevS e #[a, b]
|
|
assert! r == e.instantiateRev #[a, b]
|
|
logInfo r
|
|
let r ← instantiateS e #[a, b]
|
|
assert! r == e.instantiate #[a, b]
|
|
logInfo r
|
|
|
|
/--
|
|
info: f b a 1
|
|
---
|
|
info: f a b 1
|
|
---
|
|
info: fun x => f x b 1
|
|
---
|
|
info: fun x => f x a 1
|
|
-/
|
|
#guard_msgs in
|
|
#eval SymM.run' tst1
|
|
|
|
def tst2 : SymM Unit := do
|
|
let f ← mkConstS `f
|
|
withLocalDeclD `w (← mkConstS ``Nat) fun w => do
|
|
let w ← shareCommon w
|
|
let e ← mkAppS (← mkAppS (← mkAppS f (← mkBVarS 0)) (← mkBVarS 1)) w
|
|
withLocalDeclD `x (← mkConstS ``Nat) fun x => do
|
|
withLocalDeclD `y (← mkConstS ``Nat) fun y => do
|
|
let x ← shareCommon x
|
|
let y ← shareCommon y
|
|
logInfo e
|
|
let r ← instantiateRevS e #[x, y]
|
|
logInfo r
|
|
assert! isSameExpr (← abstractFVars r #[x, y]) e
|
|
logInfo (← abstractFVars r #[x, y])
|
|
logInfo (← abstractFVarsRange r 1 #[x, y])
|
|
logInfo (← mkLambdaFVarsS #[x, y] e)
|
|
|
|
|
|
set_option pp.funBinderTypes true in
|
|
/--
|
|
info: f #0 #1 w
|
|
---
|
|
info: f y x w
|
|
---
|
|
info: f #0 #1 w
|
|
---
|
|
info: f #0 x w
|
|
---
|
|
info: fun (x y : Nat) => f y x w
|
|
-/
|
|
#guard_msgs in
|
|
#eval SymM.run' tst2
|