From aaa7960b75f50f9ba450b4b23b9a346a74d98e3f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 27 Jun 2014 11:11:12 -0700 Subject: [PATCH] refactor(library/tactic/goal): use local names for hypotheses Signed-off-by: Leonardo de Moura --- src/frontends/lua/register_modules.cpp | 7 +- src/kernel/formatter.h | 2 + src/library/tactic/goal.cpp | 166 +++++++++++++++++++++---- src/library/tactic/goal.h | 23 +++- src/library/tactic/register_module.h | 28 ++--- tests/lua/goal1.lua | 16 +++ 6 files changed, 197 insertions(+), 45 deletions(-) create mode 100644 tests/lua/goal1.lua diff --git a/src/frontends/lua/register_modules.cpp b/src/frontends/lua/register_modules.cpp index ee451a049..85ddfa1ea 100644 --- a/src/frontends/lua/register_modules.cpp +++ b/src/frontends/lua/register_modules.cpp @@ -1,5 +1,5 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura @@ -8,9 +8,8 @@ Author: Leonardo de Moura #include "util/numerics/register_module.h" #include "util/sexpr/register_module.h" #include "library/register_module.h" -// #include "library/io_state_stream.h" // #include "library/simplifier/register_module.h" -// #include "library/tactic/register_module.h" +#include "library/tactic/register_module.h" #include "frontends/lean/register_module.h" namespace lean { @@ -19,7 +18,7 @@ void register_modules() { register_sexpr_module(); register_core_module(); // register_simplifier_module(); - // register_tactic_module(); + register_tactic_module(); register_frontend_lean_module(); } } diff --git a/src/kernel/formatter.h b/src/kernel/formatter.h index 38cdd79ce..e4b209ce1 100644 --- a/src/kernel/formatter.h +++ b/src/kernel/formatter.h @@ -11,6 +11,8 @@ Author: Leonardo de Moura #include "kernel/expr.h" namespace lean { +/** \brief Return true iff \c t contains a constant named \c n or a local constant with named (pp or not) \c n */ +bool is_used_name(expr const & t, name const & n); /** \brief Return the body of the binding \c b, where variable #0 is replaced by a local constant with a "fresh" name. The name is considered fresh if it is not used by a constant or local constant occuring in the body of \c b. diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp index 95273ebc3..a042fd7f8 100644 --- a/src/library/tactic/goal.cpp +++ b/src/library/tactic/goal.cpp @@ -6,47 +6,164 @@ Author: Leonardo de Moura */ #include #include "util/buffer.h" +#include "util/sstream.h" +#include "kernel/replace_fn.h" +#include "kernel/for_each_fn.h" +#include "kernel/abstract.h" #include "library/kernel_bindings.h" #include "library/tactic/goal.h" namespace lean { goal::goal(hypotheses const & hs, expr const & c):m_hypotheses(hs), m_conclusion(c) {} +static bool is_used_pp_name(hypothesis const * begin, hypothesis const * end, name const & n) { + return std::any_of(begin, end, [&](hypothesis const & h) { return local_pp_name(h.first) == n; }); +} + +static expr pick_unused_pp_name(hypothesis const * begin, hypothesis const * end, expr const & l) { + expr r = l; + unsigned i = 1; + while (is_used_pp_name(begin, end, local_pp_name(r))) { + name new_pp_name = local_pp_name(l); + new_pp_name = new_pp_name.append_after(i); + r = mk_local(new_pp_name, mlocal_type(l)); + i++; + } + return r; +} + +static void update_local(expr & t, expr const & old_local, expr const & new_local) { + t = replace(t, [&](expr const & e, unsigned) { + if (!has_local(e)) + return some_expr(e); + if (e == old_local) + return some_expr(new_local); + return none_expr(); + }); +} + +static void update_local(hypothesis * begin, hypothesis * end, expr & conclusion, + expr const & old_local, expr const & new_local) { + for (auto it = begin; it != end; ++it) + update_local(it->first, old_local, new_local); + update_local(conclusion, old_local, new_local); +} + format goal::pp(environment const & env, formatter const & fmt, options const & opts) const { unsigned indent = get_pp_indent(opts); bool unicode = get_pp_unicode(opts); format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-"); + expr conclusion = m_conclusion; buffer tmp; to_buffer(m_hypotheses, tmp); + std::reverse(tmp.begin(), tmp.end()); bool first = true; format r; - for (auto const & p : tmp) { - if (first) { - first = false; - } else { - r += compose(comma(), line()); - } - r += format{format(p.first), space(), colon(), nest(indent, compose(line(), fmt(env, p.second, opts)))}; + auto end = tmp.end(); + for (auto it = tmp.begin(); it != end; ++it) { + if (first) first = false; else r += compose(comma(), line()); + expr l = it->first; + expr new_l = pick_unused_pp_name(tmp.begin(), it, l); + if (!is_eqp(l, new_l)) + update_local(it+1, end, conclusion, l, new_l); + r += format{format(local_pp_name(new_l)), space(), colon(), nest(indent, compose(line(), fmt(env, mlocal_type(new_l), opts)))}; } - r = group(r); - r += format{line(), turnstile, space(), nest(indent, fmt(env, m_conclusion, opts))}; + r += format{line(), turnstile, space(), nest(indent, fmt(env, conclusion, opts))}; return group(r); } +expr goal::mk_meta(name const & n, expr const & type) const { + if (has_local(type)) { + bool failed = false; + name missing; + for_each(type, [&](expr const & e, unsigned) { + if (!has_local(e) || failed) return false; + if (is_local(e)) { + bool found = false; + for (hypothesis const & h : m_hypotheses) { + if (h.second && h.first == e) { + found = true; + break; + } + } + if (!found) { + failed = true; + missing = local_pp_name(e); + return false; + } + } + return true; + }); + if (failed) { + throw exception(sstream() << "invalid metavariable for goal, metavariable type contains local constant '" + << missing << "' which is not a hypothesis for this goal"); + } + } + expr t = type; + buffer args; + for (hypothesis const & h : m_hypotheses) { + if (h.second) { + t = Pi(h.first, t); + args.push_back(h.first); + } + } + std::reverse(args.begin(), args.end()); + return mk_app(mk_metavar(n, t), args); +} + +static bool validate(expr const & r, hypotheses const & hs) { + bool failed = false; + for_each(r, [&](expr const & e, unsigned) { + if (!has_local(e) || failed) return false; + if (is_local(e) && + !std::any_of(hs.begin(), hs.end(), [&](hypothesis const & h) { return h.first == e; })) { + failed = true; + return false; + } + return true; + }); + return !failed; +} + +bool goal::validate() const { + if (!::lean::validate(m_conclusion, m_hypotheses)) + return false; + hypotheses const * h = &m_hypotheses; + while (!is_nil(*h)) { + if (!::lean::validate(mlocal_type(head(*h).first), tail(*h))) + return false; + h = &tail(*h); + } + return true; +} + DECL_UDATA(hypotheses) static int mk_hypotheses(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 0) { - return push_hypotheses(L, hypotheses()); - } else if (nargs == 2) { - return push_hypotheses(L, hypotheses(mk_pair(to_name_ext(L, 1), to_expr(L, 2)), hypotheses())); - } else if (nargs == 3) { - return push_hypotheses(L, hypotheses(mk_pair(to_name_ext(L, 1), to_expr(L, 2)), to_hypotheses(L, 3))); - } else { - throw exception("hypotheses functions expects 0 (empty list), 2 (name & expr for singleton hypotheses list), or 3 (name & expr & hypotheses list) arguments"); + int i = lua_gettop(L); + hypotheses r; + if (i > 0 && is_hypotheses(L, i)) { + r = to_hypotheses(L, i); + i--; } + while (i > 0) { + if (is_expr(L, i)) { + expr const & l = to_expr(L, i); + if (!is_local(l)) + throw exception(sstream() << "arg #" << i << " must be a local constant or a pair"); + r = hypotheses(hypothesis(l, true), r); + } else { + lua_rawgeti(L, i, 1); + lua_rawgeti(L, i, 2); + if (!is_expr(L, -2) || !is_local(to_expr(L, -2)) || !lua_isboolean(L, -1)) + throw exception(sstream() << "arg #" << i << " must be a pair: local constant, Boolean"); + r = hypotheses(hypothesis(to_expr(L, -2), lua_toboolean(L, -1)), r); + lua_pop(L, 2); + } + i--; + } + return push_hypotheses(L, r); } static int hypotheses_is_nil(lua_State * L) { @@ -58,8 +175,8 @@ static int hypotheses_head(lua_State * L) { hypotheses const & hs = to_hypotheses(L, 1); if (!hs) throw exception("head method expects a non-empty hypotheses list"); - push_name(L, head(hs).first); - push_expr(L, head(hs).second); + push_expr(L, head(hs).first); + push_boolean(L, head(hs).second); return 2; } @@ -76,8 +193,8 @@ static int hypotheses_next(lua_State * L) { if (hs) { push_hypotheses(L, tail(hs)); lua_replace(L, lua_upvalueindex(1)); - push_name(L, head(hs).first); - push_expr(L, head(hs).second); + push_expr(L, head(hs).first); + push_boolean(L, head(hs).second); return 2; } else { lua_pushnil(L); @@ -124,7 +241,7 @@ static int goal_tostring(lua_State * L) { lua_pushstring(L, out.str().c_str()); return 1; } - +static int goal_mk_meta(lua_State * L) { return push_expr(L, to_goal(L, 1).mk_meta(to_name_ext(L, 2), to_expr(L, 3))); } static int goal_pp(lua_State * L) { int nargs = lua_gettop(L); goal & g = to_goal(L, 1); @@ -138,6 +255,7 @@ static int goal_pp(lua_State * L) { return push_format(L, g.pp(to_environment(L, 2), to_formatter(L, 3), to_options(L, 4))); } } +static int goal_validate(lua_State * L) { return push_boolean(L, to_goal(L, 1).validate()); } static const struct luaL_Reg goal_m[] = { {"__gc", goal_gc}, // never throws @@ -145,7 +263,9 @@ static const struct luaL_Reg goal_m[] = { {"hypotheses", safe_function}, {"hyps", safe_function}, {"conclusion", safe_function}, + {"mk_meta", safe_function}, {"pp", safe_function}, + {"validate", safe_function}, {0, 0} }; diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h index 20e19561c..187605584 100644 --- a/src/library/tactic/goal.h +++ b/src/library/tactic/goal.h @@ -14,7 +14,11 @@ Author: Leonardo de Moura #include "library/io_state_stream.h" namespace lean { -typedef std::pair hypothesis; +/** + \brief A hypothesis is a local variable + a flag indicating whether it is "contextual" or not. + Only contextual ones are used to build the context of new metavariables. +*/ +typedef std::pair hypothesis; typedef list hypotheses; class goal { hypotheses m_hypotheses; @@ -24,14 +28,27 @@ public: goal(hypotheses const & hs, expr const & c); hypotheses const & get_hypotheses() const { return m_hypotheses; } expr const & get_conclusion() const { return m_conclusion; } + /** + \brief Create a metavarible application (m l_1 ... l_n) with type \c type, + where \c l_1 ... \c l_n are the contextual hypotheses of this goal, and + \c m is a metavariable with name \c n. + */ + expr mk_meta(name const & n, expr const & type) const; + /** + brief Return true iff this is a valid goal. + We say a goal is valid when the conclusion only contains local constants that are in hypotheses, + and each hypothesis only contains local constants that occur in the previous hypotheses. + */ + bool validate() const; format pp(environment const & env, formatter const & fmt, options const & opts) const; }; inline goal update(goal const & g, expr const & c) { return goal(g.get_hypotheses(), c); } inline goal update(goal const & g, hypotheses const & hs) { return goal(hs, g.get_conclusion()); } inline goal update(goal const & g, buffer const & hs) { return goal(to_list(hs.begin(), hs.end()), g.get_conclusion()); } -inline hypotheses add_hypothesis(name const & h_name, expr const & h, hypotheses const & hs) { - return cons(mk_pair(h_name, h), hs); +inline hypotheses add_hypothesis(expr const & l, hypotheses const & hs) { + lean_assert(is_local(l)); + return cons(hypothesis(l, true), hs); } inline hypotheses add_hypothesis(hypothesis const & h, hypotheses const & hs) { return cons(h, hs); diff --git a/src/library/tactic/register_module.h b/src/library/tactic/register_module.h index 5af048863..25c6882a4 100644 --- a/src/library/tactic/register_module.h +++ b/src/library/tactic/register_module.h @@ -1,5 +1,5 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura @@ -7,24 +7,22 @@ Author: Leonardo de Moura #pragma once #include "util/script_state.h" #include "library/tactic/goal.h" -#include "library/tactic/proof_builder.h" -#include "library/tactic/cex_builder.h" -#include "library/tactic/proof_state.h" -#include "library/tactic/tactic.h" -#include "library/tactic/boolean_tactics.h" -#include "library/tactic/apply_tactic.h" -#include "library/tactic/simplify_tactic.h" +// #include "library/tactic/proof_builder.h" +// #include "library/tactic/cex_builder.h" +// #include "library/tactic/proof_state.h" +// #include "library/tactic/tactic.h" +// #include "library/tactic/apply_tactic.h" +// #include "library/tactic/simplify_tactic.h" namespace lean { inline void open_tactic_module(lua_State * L) { open_goal(L); - open_proof_builder(L); - open_cex_builder(L); - open_proof_state(L); - open_tactic(L); - open_boolean_tactics(L); - open_apply_tactic(L); - open_simplify_tactic(L); + // open_proof_builder(L); + // open_cex_builder(L); + // open_proof_state(L); + // open_tactic(L); + // open_apply_tactic(L); + // open_simplify_tactic(L); } inline void register_tactic_module() { script_state::register_module(open_tactic_module); diff --git a/tests/lua/goal1.lua b/tests/lua/goal1.lua new file mode 100644 index 000000000..05f639a45 --- /dev/null +++ b/tests/lua/goal1.lua @@ -0,0 +1,16 @@ +local env = environment() +local A = Local("A", Type) +env = add_decl(env, mk_var_decl("eq", Pi(A, mk_arrow(A, A, Bool)))) +local eq = Const("eq") +local a = Local("a", A) +local b = mk_local("b", "a", A) +local H = Local("H", eq(A, a, b)) +local hs = hypotheses(H, a, b, A) +local g = goal(hs, eq(A, b, a)) +print(g) +assert(g:validate()) +local m1 = g:mk_meta("m1", Bool) +print(tostring(m1)) +print(env:type_check(m1)) + +assert(not goal(hypotheses(H, A, a, b), eq(A, b, a)):validate())