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

refactor(library/tactic): move 'tracing' tactics to separate module

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-22 14:07:24 -07:00
parent ef60e6abd2
commit 323715e951
9 changed files with 116 additions and 102 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/tactic/CMakeLists.txt
View file

@ -1,4 +1,5 @@
add_library(tactic goal.cpp proof_state.cpp tactic.cpp apply_tactic.cpp
intros_tactic.cpp rename_tactic.cpp expr_to_tactic.cpp init_module.cpp)
add_library(tactic goal.cpp proof_state.cpp tactic.cpp
apply_tactic.cpp intros_tactic.cpp rename_tactic.cpp trace_tactic.cpp
expr_to_tactic.cpp init_module.cpp)
target_link_libraries(tactic ${LEAN_LIBS})

20
src/library/tactic/expr_to_tactic.cpp
View file

@ -342,26 +342,6 @@ void initialize_expr_to_tactic() {
[](tactic const & t1, tactic const & t2) { return orelse(t1, t2); });
register_unary_tac(repeat_tac_name,
[](tactic const & t1) { return repeat(t1); });
register_tac(name(*g_tactic_name, "state"),
[](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const * p) {
if (p)
if (auto it = p->get_pos_info(e))
return trace_state_tactic(std::string(p->get_file_name()), *it);
return trace_state_tactic();
});
register_tac(name(*g_tactic_name, "trace"),
[](type_checker & tc, elaborate_fn const &, expr const & e, pos_info_provider const *) {
buffer<expr> args;
get_app_args(e, args);
if (args.size() != 1)
throw expr_to_tactic_exception(e, "invalid trace tactic, argument expected");
if (auto str = to_string(args[0]))
return trace_tactic(*str);
else if (auto str = to_string(tc.whnf(args[0]).first))
return trace_tactic(*str);
else
throw expr_to_tactic_exception(e, "invalid trace tactic, string value expected");
});
register_tac(exact_tac_name,
[](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
// TODO(Leo): use elaborate_fn

3
src/library/tactic/init_module.cpp
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include "library/tactic/apply_tactic.h"
#include "library/tactic/rename_tactic.h"
#include "library/tactic/intros_tactic.h"
#include "library/tactic/trace_tactic.h"
namespace lean {
void initialize_tactic_module() {
@ -17,9 +18,11 @@ void initialize_tactic_module() {
initialize_apply_tactic();
initialize_rename_tactic();
initialize_intros_tactic();
initialize_trace_tactic();
}
void finalize_tactic_module() {
finalize_trace_tactic();
finalize_intros_tactic();
finalize_rename_tactic();
finalize_apply_tactic();

46
src/library/tactic/tactic.cpp
View file

@ -88,48 +88,6 @@ tactic cond(proof_state_pred p, tactic const & t1, tactic const & t2) {
});
}
tactic trace_tactic(std::string const & msg) {
return tactic1([=](environment const &, io_state const & ios, proof_state const & s) -> proof_state {
ios.get_diagnostic_channel() << msg << "\n";
ios.get_diagnostic_channel().get_stream().flush();
return s;
});
}
tactic trace_tactic(sstream const & msg) {
return trace_tactic(msg.str());
}
tactic trace_tactic(char const * msg) {
return trace_tactic(std::string(msg));
}
tactic trace_state_tactic(std::string const & fname, pair<unsigned, unsigned> const & pos) {
return tactic1([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state {
diagnostic(env, ios) << fname << ":" << pos.first << ":" << pos.second << ": proof state\n"
<< s << endl;
ios.get_diagnostic_channel().get_stream().flush();
return s;
});
}
tactic trace_state_tactic() {
return tactic1([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state {
diagnostic(env, ios) << "proof state\n" << s << endl;
ios.get_diagnostic_channel().get_stream().flush();
return s;
});
}
tactic suppress_trace(tactic const & t) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
io_state new_ios(ios);
std::shared_ptr<output_channel> out(std::make_shared<string_output_channel>());
new_ios.set_diagnostic_channel(out);
return t(env, new_ios, s);
});
}
tactic then(tactic const & t1, tactic const & t2) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s1) -> proof_state_seq {
return map_append(t1(env, ios, s1), [=](proof_state const & s2) {
@ -473,7 +431,6 @@ static int tactic_par(lua_State * L) { return push_tactic(L, par(to_
static int tactic_repeat(lua_State * L) { return push_tactic(L, repeat(to_tactic(L, 1))); }
static int tactic_repeat_at_most(lua_State * L) { return push_tactic(L, repeat_at_most(to_tactic(L, 1), luaL_checkinteger(L, 2))); }
static int tactic_take(lua_State * L) { return push_tactic(L, take(to_tactic(L, 1), luaL_checkinteger(L, 2))); }
static int tactic_suppress_trace(lua_State * L) { return push_tactic(L, suppress_trace(to_tactic(L, 1))); }
static int tactic_try_for(lua_State * L) { return push_tactic(L, try_for(to_tactic(L, 1), luaL_checkinteger(L, 2))); }
static int tactic_using_params(lua_State * L) { return push_tactic(L, using_params(to_tactic(L, 1), to_options(L, 2))); }
static int tactic_focus(lua_State * L) {
@ -528,7 +485,6 @@ static int mk_lua_when_tactic(lua_State * L) { return mk_lua_cond_tactic(L, to_t
static int mk_id_tactic(lua_State * L) { return push_tactic(L, id_tactic()); }
static int mk_now_tactic(lua_State * L) { return push_tactic(L, now_tactic()); }
static int mk_fail_tactic(lua_State * L) { return push_tactic(L, fail_tactic()); }
static int mk_trace_tactic(lua_State * L) { return push_tactic(L, trace_tactic(luaL_checkstring(L, 1))); }
static int mk_assumption_tactic(lua_State * L) { return push_tactic(L, assumption_tactic()); }
static int mk_unfold_tactic(lua_State * L) {
int nargs = lua_gettop(L);
@ -552,7 +508,6 @@ static const struct luaL_Reg tactic_m[] = {
{"repeat", safe_function<tactic_repeat>},
{"repeat_at_most", safe_function<tactic_repeat_at_most>},
{"take", safe_function<tactic_take>},
{"suppress_trace", safe_function<tactic_suppress_trace>},
{"try_for", safe_function<tactic_try_for>},
{"using_params", safe_function<tactic_using_params>},
{"using", safe_function<tactic_using_params>},
@ -573,7 +528,6 @@ void open_tactic(lua_State * L) {
setfuncs(L, tactic_m, 0);
SET_GLOBAL_FUN(tactic_pred, "is_tactic");
SET_GLOBAL_FUN(mk_trace_tactic, "trace_tac");
SET_GLOBAL_FUN(mk_id_tactic, "id_tac");
SET_GLOBAL_FUN(mk_now_tactic, "now_tac");
SET_GLOBAL_FUN(mk_fail_tactic, "fail_tac");

10
src/library/tactic/tactic.h
View file

@ -51,16 +51,6 @@ tactic fail_tactic();
tactic now_tactic();
/** \brief Return a tactic that solves any goal of the form <tt>..., H : A, ... |- A</tt>. */
tactic assumption_tactic();
/** \brief Return a tactic that just returns the input state, and display the given message in the diagnostic channel. */
tactic trace_tactic(char const * msg);
class sstream;
tactic trace_tactic(sstream const & msg);
tactic trace_tactic(std::string const & msg);
/** \brief Return a tactic that just displays the input state in the diagnostic channel. */
tactic trace_state_tactic(std::string const & fname, pair<unsigned, unsigned> const & pos);
tactic trace_state_tactic();
/** \brief Create a tactic that applies \c t, but suppressing diagnostic messages. */
tactic suppress_trace(tactic const & t);
/** \brief Return a tactic that performs \c t1 followed by \c t2. */
tactic then(tactic const & t1, tactic const & t2);
inline tactic operator<<(tactic const & t1, tactic const & t2) { return then(t1, t2); }

84
src/library/tactic/trace_tactic.cpp Normal file
View file

@ -0,0 +1,84 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <string>
#include "util/sstream.h"
#include "kernel/type_checker.h"
#include "library/string.h"
#include "library/tactic/tactic.h"
#include "library/tactic/expr_to_tactic.h"
namespace lean {
tactic trace_tactic(std::string const & msg) {
return tactic1([=](environment const &, io_state const & ios, proof_state const & s) -> proof_state {
ios.get_diagnostic_channel() << msg << "\n";
ios.get_diagnostic_channel().get_stream().flush();
return s;
});
}
tactic trace_tactic(sstream const & msg) {
return trace_tactic(msg.str());
}
tactic trace_tactic(char const * msg) {
return trace_tactic(std::string(msg));
}
tactic trace_state_tactic(std::string const & fname, pair<unsigned, unsigned> const & pos) {
return tactic1([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state {
diagnostic(env, ios) << fname << ":" << pos.first << ":" << pos.second << ": proof state\n"
<< s << endl;
ios.get_diagnostic_channel().get_stream().flush();
return s;
});
}
tactic trace_state_tactic() {
return tactic1([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state {
diagnostic(env, ios) << "proof state\n" << s << endl;
ios.get_diagnostic_channel().get_stream().flush();
return s;
});
}
tactic suppress_trace(tactic const & t) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
io_state new_ios(ios);
std::shared_ptr<output_channel> out(std::make_shared<string_output_channel>());
new_ios.set_diagnostic_channel(out);
return t(env, new_ios, s);
});
}
void initialize_trace_tactic() {
register_tac(name({"tactic", "state"}),
[](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const * p) {
if (p)
if (auto it = p->get_pos_info(e))
return trace_state_tactic(std::string(p->get_file_name()), *it);
return trace_state_tactic();
});
register_tac(name({"tactic", "trace"}),
[](type_checker & tc, elaborate_fn const &, expr const & e, pos_info_provider const *) {
buffer<expr> args;
get_app_args(e, args);
if (args.size() != 1)
throw expr_to_tactic_exception(e, "invalid trace tactic, argument expected");
if (auto str = to_string(args[0]))
return trace_tactic(*str);
else if (auto str = to_string(tc.whnf(args[0]).first))
return trace_tactic(*str);
else
throw expr_to_tactic_exception(e, "invalid trace tactic, string value expected");
});
}
void finalize_trace_tactic() {
}
}

25
src/library/tactic/trace_tactic.h Normal file
View file

@ -0,0 +1,25 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <string>
#include "library/tactic/tactic.h"
namespace lean {
/** \brief Return a tactic that just returns the input state, and display the given message in the diagnostic channel. */
tactic trace_tactic(char const * msg);
class sstream;
tactic trace_tactic(sstream const & msg);
tactic trace_tactic(std::string const & msg);
/** \brief Return a tactic that just displays the input state in the diagnostic channel. */
tactic trace_state_tactic(std::string const & fname, pair<unsigned, unsigned> const & pos);
tactic trace_state_tactic();
/** \brief Create a tactic that applies \c t, but suppressing diagnostic messages. */
tactic suppress_trace(tactic const & t);
void initialize_trace_tactic();
void finalize_trace_tactic();
}

21
tests/lua/old/tactic1.lua
View file

@ -15,24 +15,3 @@ local ltac = tactic(function(env, ios, s)
print("FIRST tactic in Lua, current state: " .. tostring(s));
return s
end)
local t = (trace_tac("hello") .. trace_tac("world")) + (trace_tac("again") .. ltac .. assumption_tac())
for s in t(env, ios, ps) do
if s:is_proof_final_state() then
local m = proof_map()
local a = assignment(s:get_menv())
print(s:proof_builder()(m, a))
else
print(s)
end
end
print("-------------------")
print(t:solve(env, ios, ps))
print(t:solve(env, ios, ctx, p))
assert(t:solve(env, ios, ps) == Var(1))
assert(t:solve(env, ios, ctx, q) == Var(0))
local t2 = id_tac() + id_tac() + id_tac()
local r = t2:solve(env, ios, ps)
assert(#r == 3)
for i, out_state in ipairs(r) do
print(i, out_state)
end

4
tests/lua/tactic1.lua
View file

@ -7,9 +7,7 @@ local b = Local("b", A)
local H = Local("H", eq(A, a, b))
local m = mk_metavar("m", Pi(A, a, b, H, eq(A, a, b)))(A, a, b, H)
local s = to_proof_state(m, eq(A, a, b))
local t = Then(Append(trace_tac("tst1a"), trace_tac("tst1b")),
trace_tac("tst2"),
Append(trace_tac("tst3"), assumption_tac()))
local t = assumption_tac()
for r in t(env, s) do
print("Solution:")
print(r)