422920f643
This PR adds an experimental tactic `mvcgen'` that will soon replace `mvcgen`. It has been reimplemented from the ground up using the new `SymM`-based framework for efficient symbolic evaluation and can outperform `mvcgen` by a factor of >100x for some synthetic benchmarks. `mvcgen'` aspires to be feature-complete with `mvcgen`. Known exceptions currently are join point sharing, introduction of local specs and smaller bugs. The implementation of `mvgen'` used to live in the benchmark suite for rapid prototyping; this commit merely moves it into the Lean toolchain. Doing so results in an build time instruction count increase in seemingly unrelated tests such as `elab/delayed_assign//instructions`; the reason is that the builtin elaborator attribute now pulls in substantially more import code on startup. --------- Co-authored-by: Sebastian Graf <sg@lean-fro.org>
43 lines
842 B
Text
43 lines
842 B
Text
import Lean
|
|
import Std.Tactic.Do
|
|
|
|
open Lean Meta Elab Tactic Sym Std Do SpecAttr
|
|
|
|
namespace ReaderState
|
|
|
|
set_option mvcgen.warning false
|
|
|
|
abbrev M := ReaderT Nat <| StateM Nat
|
|
|
|
-- Partially evaluated specs for best performance.
|
|
|
|
@[spec high]
|
|
theorem Spec.M_read :
|
|
⦃fun r s => Q.fst r r s⦄ read (m := M) ⦃Q⦄ := by
|
|
mvcgen
|
|
|
|
@[spec high]
|
|
theorem Spec.M_get :
|
|
⦃fun r s => Q.fst s r s⦄ get (m := M) ⦃Q⦄ := by
|
|
mvcgen
|
|
|
|
@[spec high]
|
|
theorem Spec.M_set (n : Nat) :
|
|
⦃fun r _ => Q.fst () r n⦄ set (m := M) n ⦃Q⦄ := by
|
|
mvcgen
|
|
|
|
def step : M Unit := do
|
|
let r ← read
|
|
let s ← get
|
|
set (s + r)
|
|
let s ← get
|
|
set (s - r)
|
|
|
|
def loop (n : Nat) : M Unit := do
|
|
match n with
|
|
| 0 => pure ()
|
|
| n+1 => step; loop n
|
|
|
|
def Goal (n : Nat) : Prop := ∀ post, ⦃post⦄ loop n ⦃⇓_ => post⦄
|
|
|
|
end ReaderState
|