175661b6c3
This PR reorganizes the monad hierarchy for symbolic computation in Lean. ## Motivation We want a clean layering where: 1. A foundational monad (`SymM`) provides maximally shared terms and structural/syntactic `isDefEq` 2. `GrindM` builds on this foundation, adding E-graphs, congruence closure, and decision procedures 3. Symbolic execution / VCGen uses `GrindM` directly without introducing a third monad ## Changes The core symbolic computation layer still lives in `Lean.Meta.Sym`. This monad (`SymM`) provides: - Maximally shared terms with pointer-based equality - Structural/syntactic `isDefEq` and matching (no reduction, predictable cost) - Monotonic local contexts (no `revert` or `clear`), enabling O(1) metavariable validation - Efficient `intro`, `apply`, and `simp` implementations The name "Sym" reflects that this is infrastructure for symbolic computation: symbolic simulation, verification condition generation, and decision procedures. ### Updated hierarchy ``` Lean.Meta.Sym -- SymM: shared terms, syntactic isDefEq, intro, apply, simp Lean.Meta.Grind -- GrindM: E-graphs, congruence closure (extends SymM) ``` Symbolic execution is a usage pattern of `GrindM` operating on `Grind.Goal`, not a separate monad. This keeps the API surface minimal: users learn two monads, and VCGen is "how you use `GrindM`" (for users that want to use `grind`) rather than a third abstraction to understand.
64 lines
1.8 KiB
Text
64 lines
1.8 KiB
Text
import Lean
|
||
open Lean Meta
|
||
opaque f : Nat → Nat
|
||
|
||
namespace SimpBench
|
||
/-!
|
||
## `SymM` Simplifier benchmarks
|
||
-/
|
||
|
||
def getProofSize (r : Sym.Simp.Result) : MetaM Nat :=
|
||
match r with
|
||
| .rfl _ => return 0
|
||
| .step _ p _ => p.numObjs
|
||
|
||
def mkSimpMethods : MetaM Sym.Simp.Methods := do
|
||
let thms : Sym.Simp.Theorems := {}
|
||
let thm ← Sym.Simp.mkTheoremFromDecl ``Nat.zero_add
|
||
let thms := thms.insert thm
|
||
return { post := thms.rewrite }
|
||
|
||
def simp (e : Expr) : MetaM (Sym.Simp.Result × Float) := Sym.SymM.run do
|
||
let e ← Grind.shareCommon e
|
||
let methods ← mkSimpMethods
|
||
let startTime ← IO.monoNanosNow
|
||
let r ← Sym.simp e methods { maxSteps := 100000000 }
|
||
let endTime ← IO.monoNanosNow
|
||
-- logInfo e
|
||
-- match r with
|
||
-- | .rfl => logInfo "rfl"
|
||
-- | .step e' h => logInfo e'; logInfo h; check h
|
||
let timeMs := (endTime - startTime).toFloat / 1000000.0
|
||
return (r, timeMs)
|
||
|
||
def mkLambdaBench (n : Nat) : MetaM Expr := do
|
||
let zero := mkNatLit 0
|
||
let rec go (n : Nat) (xs : Array Expr) (e : Expr) : MetaM Expr := do
|
||
match n with
|
||
| 0 => mkLambdaFVars xs e
|
||
| n+1 =>
|
||
withLocalDeclD `x (mkConst ``Nat) fun x =>
|
||
go n (xs.push x) (mkNatAdd zero (mkNatAdd e x))
|
||
go n #[] zero
|
||
|
||
def benchLambda (n : Nat) : MetaM Unit := do
|
||
let e ← mkLambdaBench n
|
||
let (r, timeMs) ← simp e
|
||
let proofSize ← getProofSize r
|
||
IO.println s!"lambda_{n}: {timeMs}ms, proof_size={proofSize}"
|
||
|
||
set_option maxRecDepth 100000
|
||
|
||
/-! ## Run all benchmarks -/
|
||
def runAllBenchmarks : MetaM Unit := do
|
||
IO.println "=== Simplifier Stress Tests ==="
|
||
IO.println ""
|
||
|
||
IO.println ""
|
||
IO.println "--- Benchmark 1: Lambda block ---"
|
||
for n in [10, 20, 30, 40, 50, 60, 70, 80, 90, 100, 110, 120, 130, 140, 150, 160, 170, 180, 190, 200] do
|
||
benchLambda n
|
||
|
||
#eval runAllBenchmarks
|
||
|
||
end SimpBench
|