michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/simplifier): allow the user to associate a simplifier monitor with the lua_State object

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-31 13:49:24 -08:00
parent 0ed35e2133
commit 110ca84984
6 changed files with 167 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

44
src/library/simplifier/simplifier.cpp
View file

@ -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<simplifier_monitor> const & monitor) {
lua_pushlightuserdata(L, static_cast<void *>(&g_set_simplifier_monitor_key));
push_simplifier_monitor_ptr(L, monitor);
lua_settable(L, LUA_REGISTRYINDEX);
}
std::shared_ptr<simplifier_monitor> get_global_simplifier_monitor(lua_State * L) {
lua_pushlightuserdata(L, static_cast<void *>(&g_set_simplifier_monitor_key));
lua_gettable(L, LUA_REGISTRYINDEX);
if (lua_isnil(L, -1)) {
lua_pop(L, 1);
return std::shared_ptr<simplifier_monitor>();
} else {
std::shared_ptr<simplifier_monitor> r(to_simplifier_monitor_ptr(L, -1));
lua_pop(L, 1);
return r;
}
}
std::shared_ptr<simplifier_monitor> 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");
}
}

17
src/library/simplifier/simplifier.h
View file

@ -145,4 +145,21 @@ simplifier::result simplify(expr const & e, ro_environment const & env, options
optional<ro_metavar_env> const & menv = none_ro_menv(),
std::shared_ptr<simplifier_monitor> const & monitor = std::shared_ptr<simplifier_monitor>());
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<simplifier_monitor> 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<simplifier_monitor> 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<simplifier_monitor> get_simplifier_monitor(lua_State * L, int i);
}

15
src/library/tactic/simplify_tactic.cpp
View file

@ -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<proof_state> 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<simplifier_monitor> 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<proof_state> 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<proof_state>(s);
@ -86,19 +87,19 @@ static optional<proof_state> 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<simplifier_monitor> const & monitor) {
std::vector<name> names(ns, ns + num_ns);
return mk_tactic01([=](ro_environment const & env, io_state const & ios, proof_state const & s) -> optional<proof_state> {
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<name> 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)));
}
}

4
src/library/tactic/simplify_tactic.h
View file

@ -5,8 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <memory>
#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<simplifier_monitor> const & monitor);
void open_simplify_tactic(lua_State * L);
}

27
tests/lean/map.lean Normal file
View file

@ -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

68
tests/lean/map.lean.expected.out Normal file
View file

@ -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