From 110ca84984c9934f68e74972924a3b43a253dbd7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 31 Jan 2014 13:49:24 -0800 Subject: [PATCH] feat(library/simplifier): allow the user to associate a simplifier monitor with the lua_State object Signed-off-by: Leonardo de Moura --- src/library/simplifier/simplifier.cpp | 44 +++++++++++++++++ src/library/simplifier/simplifier.h | 17 +++++++ src/library/tactic/simplify_tactic.cpp | 15 +++--- src/library/tactic/simplify_tactic.h | 4 +- tests/lean/map.lean | 27 ++++++++++ tests/lean/map.lean.expected.out | 68 ++++++++++++++++++++++++++ 6 files changed, 167 insertions(+), 8 deletions(-) create mode 100644 tests/lean/map.lean create mode 100644 tests/lean/map.lean.expected.out diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp index 47a557fee..89c0db2be 100644 --- a/src/library/simplifier/simplifier.cpp +++ b/src/library/simplifier/simplifier.cpp @@ -1815,6 +1815,48 @@ static int simplify(lua_State * L) { return simplify_core(L, ro_shared_environment(L, 4)); } +static char g_set_simplifier_monitor_key; + +void set_global_simplifier_monitor(lua_State * L, std::shared_ptr const & monitor) { + lua_pushlightuserdata(L, static_cast(&g_set_simplifier_monitor_key)); + push_simplifier_monitor_ptr(L, monitor); + lua_settable(L, LUA_REGISTRYINDEX); +} + +std::shared_ptr get_global_simplifier_monitor(lua_State * L) { + lua_pushlightuserdata(L, static_cast(&g_set_simplifier_monitor_key)); + lua_gettable(L, LUA_REGISTRYINDEX); + if (lua_isnil(L, -1)) { + lua_pop(L, 1); + return std::shared_ptr(); + } else { + std::shared_ptr r(to_simplifier_monitor_ptr(L, -1)); + lua_pop(L, 1); + return r; + } +} + +std::shared_ptr get_simplifier_monitor(lua_State * L, int i) { + if (i > lua_gettop(L) || lua_isnil(L, i)) + return get_global_simplifier_monitor(L); + else + return to_simplifier_monitor_ptr(L, 3); +} + +static int set_simplifier_monitor(lua_State * L) { + set_global_simplifier_monitor(L, to_simplifier_monitor_ptr(L, 1)); + return 0; +} + +static int get_simplifier_monitor(lua_State * L) { + auto r = get_global_simplifier_monitor(L); + if (r) + push_simplifier_monitor_ptr(L, r); + else + lua_pushnil(L); + return 1; +} + void open_simplifier(lua_State * L) { luaL_newmetatable(L, simplifier_mt); lua_pushvalue(L, -1); @@ -1848,5 +1890,7 @@ void open_simplifier(lua_State * L) { lua_setglobal(L, "simplifier_failure"); SET_GLOBAL_FUN(simplify, "simplify"); + SET_GLOBAL_FUN(set_simplifier_monitor, "set_simplifier_monitor"); + SET_GLOBAL_FUN(get_simplifier_monitor, "get_simplifier_monitor"); } } diff --git a/src/library/simplifier/simplifier.h b/src/library/simplifier/simplifier.h index 3569a1cb7..a6f83c31e 100644 --- a/src/library/simplifier/simplifier.h +++ b/src/library/simplifier/simplifier.h @@ -145,4 +145,21 @@ simplifier::result simplify(expr const & e, ro_environment const & env, options optional const & menv = none_ro_menv(), std::shared_ptr const & monitor = std::shared_ptr()); void open_simplifier(lua_State * L); +/** + \brief Associate the given simplifier monitor with the lua_State object \c L. +*/ +void set_global_simplifier_monitor(lua_State * L, std::shared_ptr const & monitor); +/** + \brief Return the simplifier monitor associated with the given lua_State. + The result is nullptr if the lua_State object does not have a monitor associated with it. +*/ +std::shared_ptr get_global_simplifier_monitor(lua_State * L); +/** + \brief Return a simplifier object at position \c i on the Lua stack. If there is a nil stored + on this position of the stack, then return \c get_global_simplifier_monitor. + + \remark This procedure throws an exception if the object stored at position \c i not a + simplifier monitor nor nil. +*/ +std::shared_ptr get_simplifier_monitor(lua_State * L, int i); } diff --git a/src/library/tactic/simplify_tactic.cpp b/src/library/tactic/simplify_tactic.cpp index 279d2ec5e..4a23a1fe6 100644 --- a/src/library/tactic/simplify_tactic.cpp +++ b/src/library/tactic/simplify_tactic.cpp @@ -25,7 +25,8 @@ bool get_simp_tac_assumptions(options const & opts) { return opts.get_bool(g_sim static name g_assumption("assump"); static optional simplify_tactic(ro_environment const & env, io_state const & ios, proof_state const & s, - unsigned num_ns, name const * ns, options const & extra_opts) { + unsigned num_ns, name const * ns, options const & extra_opts, + std::shared_ptr const & monitor) { if (empty(s.get_goals())) return none_proof_state(); options opts = join(extra_opts, ios.get_options()); @@ -53,7 +54,7 @@ static optional simplify_tactic(ro_environment const & env, io_stat } expr conclusion = g.get_conclusion(); - auto r = simplify(conclusion, env, opts, rule_sets.size(), rule_sets.data(), some_ro_menv(menv)); + auto r = simplify(conclusion, env, opts, rule_sets.size(), rule_sets.data(), some_ro_menv(menv), monitor); expr new_conclusion = r.get_expr(); if (new_conclusion == g.get_conclusion()) return optional(s); @@ -86,19 +87,19 @@ static optional simplify_tactic(ro_environment const & env, io_stat return some(proof_state(s, new_gs, new_pb)); } -tactic simplify_tactic(unsigned num_ns, name const * ns, options const & opts) { +tactic simplify_tactic(unsigned num_ns, name const * ns, options const & opts, std::shared_ptr const & monitor) { std::vector names(ns, ns + num_ns); return mk_tactic01([=](ro_environment const & env, io_state const & ios, proof_state const & s) -> optional { - return simplify_tactic(env, ios, s, names.size(), names.data(), opts); + return simplify_tactic(env, ios, s, names.size(), names.data(), opts, monitor); }); } static int mk_simplify_tactic(lua_State * L) { int nargs = lua_gettop(L); if (nargs == 0) { - return push_tactic(L, simplify_tactic(1, &get_default_rewrite_rule_set_id(), options())); + return push_tactic(L, simplify_tactic(1, &get_default_rewrite_rule_set_id(), options(), get_global_simplifier_monitor(L))); } else if (nargs == 1 && is_options(L, 1)) { - return push_tactic(L, simplify_tactic(1, &get_default_rewrite_rule_set_id(), to_options(L, 1))); + return push_tactic(L, simplify_tactic(1, &get_default_rewrite_rule_set_id(), to_options(L, 1), get_global_simplifier_monitor(L))); } else { buffer rs; if (lua_isstring(L, 1)) { @@ -116,7 +117,7 @@ static int mk_simplify_tactic(lua_State * L) { options opts; if (nargs >= 2) opts = to_options(L, 2); - return push_tactic(L, simplify_tactic(rs.size(), rs.data(), opts)); + return push_tactic(L, simplify_tactic(rs.size(), rs.data(), opts, get_simplifier_monitor(L, 3))); } } diff --git a/src/library/tactic/simplify_tactic.h b/src/library/tactic/simplify_tactic.h index 5e552836e..ddfdde717 100644 --- a/src/library/tactic/simplify_tactic.h +++ b/src/library/tactic/simplify_tactic.h @@ -5,8 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include #include "library/tactic/tactic.h" +#include "library/simplifier/simplifier.h" namespace lean { -tactic simplify_tactic(options const & opts, unsigned num_ns, name const * ns); +tactic simplify_tactic(options const & opts, unsigned num_ns, name const * ns, std::shared_ptr const & monitor); void open_simplify_tactic(lua_State * L); } diff --git a/tests/lean/map.lean b/tests/lean/map.lean new file mode 100644 index 000000000..db968f9f5 --- /dev/null +++ b/tests/lean/map.lean @@ -0,0 +1,27 @@ +import tactic +variable list : Type → Type +variable nil {A : Type} : list A +variable cons {A : Type} : A → list A → list A +variable map {A B : Type} : (A → B) → list A → list B +axiom map_cons {A B : Type} (f : A → B) (a : A) (l : list A) : map f (cons a l) = cons (f a) (map f l) +axiom map_nil {A B : Type} (f : A → B) : (map f nil) = nil + +add_rewrite map_cons map_nil + +(* +local m = simplifier_monitor(function(s, e) + print("Visit, depth: " .. s:depth() .. ", " .. tostring(e)) + end, + function(s, e, new_e, pr) + print("Step: " .. tostring(e) .. " ===> " .. tostring(new_e)) + end, + function(s, e, new_e, ceq, ceq_id) + print("Rewrite using: " .. tostring(ceq_id)) + print(" " .. tostring(e) .. " ===> " .. tostring(new_e)) + end +) +set_simplifier_monitor(m) +*) + +theorem T1 : map (λ x, x + 1) (cons 1 (cons 2 nil)) = cons 2 (cons 3 nil) +:= by simp diff --git a/tests/lean/map.lean.expected.out b/tests/lean/map.lean.expected.out new file mode 100644 index 000000000..165af9ac7 --- /dev/null +++ b/tests/lean/map.lean.expected.out @@ -0,0 +1,68 @@ + Set: pp::colors + Set: pp::unicode + Imported 'tactic' + Assumed: list + Assumed: nil + Assumed: cons + Assumed: map + Assumed: map_cons + Assumed: map_nil +Visit, depth: 1, map (λ x : ℕ, x + 1) (cons 1 (cons 2 nil)) = cons 2 (cons 3 nil) +Visit, depth: 2, @eq +Visit, depth: 2, map (λ x : ℕ, x + 1) (cons 1 (cons 2 nil)) +Visit, depth: 3, @map +Step: @map ===> @map +Visit, depth: 3, λ x : ℕ, x + 1 +Visit, depth: 4, 3::1 + 1 +Visit, depth: 5, Nat::add +Visit, depth: 5, 3::1 +Step: 3::1 ===> 3::1 +Visit, depth: 5, 1 +Step: 3::1 + 1 ===> 3::1 + 1 +Step: λ x : ℕ, x + 1 ===> λ x : ℕ, x + 1 +Visit, depth: 3, cons 1 (cons 2 nil) +Visit, depth: 4, @cons +Step: @cons ===> @cons +Visit, depth: 4, 1 +Visit, depth: 4, cons 2 nil +Visit, depth: 5, 2 +Visit, depth: 5, nil +Visit, depth: 6, @nil +Step: @nil ===> @nil +Step: nil ===> nil +Step: cons 2 nil ===> cons 2 nil +Step: cons 1 (cons 2 nil) ===> cons 1 (cons 2 nil) +Rewrite using: map_cons + map (λ x : ℕ, x + 1) (cons 1 (cons 2 nil)) ===> cons ((λ x : ℕ, x + 1) 1) (map (λ x : ℕ, x + 1) (cons 2 nil)) +Visit, depth: 3, cons ((λ x : ℕ, x + 1) 1) (map (λ x : ℕ, x + 1) (cons 2 nil)) +Visit, depth: 4, (λ x : ℕ, x + 1) 1 +Visit, depth: 5, 1 +Visit, depth: 5, 2 +Step: (λ x : ℕ, x + 1) 1 ===> 2 +Visit, depth: 4, map (λ x : ℕ, x + 1) (cons 2 nil) +Rewrite using: map_cons + map (λ x : ℕ, x + 1) (cons 2 nil) ===> cons ((λ x : ℕ, x + 1) 2) (map (λ x : ℕ, x + 1) nil) +Visit, depth: 5, cons ((λ x : ℕ, x + 1) 2) (map (λ x : ℕ, x + 1) nil) +Visit, depth: 6, (λ x : ℕ, x + 1) 2 +Visit, depth: 7, 2 +Visit, depth: 7, 3 +Step: (λ x : ℕ, x + 1) 2 ===> 3 +Visit, depth: 6, map (λ x : ℕ, x + 1) nil +Rewrite using: map_nil + map (λ x : ℕ, x + 1) nil ===> nil +Step: map (λ x : ℕ, x + 1) nil ===> nil +Visit, depth: 6, cons 3 nil +Visit, depth: 7, 3 +Step: cons 3 nil ===> cons 3 nil +Step: cons ((λ x : ℕ, x + 1) 2) (map (λ x : ℕ, x + 1) nil) ===> cons 3 nil +Step: map (λ x : ℕ, x + 1) (cons 2 nil) ===> cons 3 nil +Visit, depth: 4, cons 2 (cons 3 nil) +Visit, depth: 5, 2 +Step: cons 2 (cons 3 nil) ===> cons 2 (cons 3 nil) +Step: cons ((λ x : ℕ, x + 1) 1) (map (λ x : ℕ, x + 1) (cons 2 nil)) ===> cons 2 (cons 3 nil) +Step: map (λ x : ℕ, x + 1) (cons 1 (cons 2 nil)) ===> cons 2 (cons 3 nil) +Rewrite using: eq_id + cons 2 (cons 3 nil) = cons 2 (cons 3 nil) ===> ⊤ +Visit, depth: 2, ⊤ +Step: map (λ x : ℕ, x + 1) (cons 1 (cons 2 nil)) = cons 2 (cons 3 nil) ===> ⊤ + Proved: T1