From f1d8d8dcf931ad1b6cf105f0f019da8864c08725 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 27 Jun 2014 06:59:17 -0700 Subject: [PATCH] chore(library/tactic): update goal objects Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 4 +- src/library/kernel_bindings.cpp | 4 +- src/library/kernel_bindings.h | 1 + src/library/tactic/CMakeLists.txt | 8 +- src/library/tactic/goal.cpp | 185 +++--------------------------- src/library/tactic/goal.h | 58 +--------- 6 files changed, 30 insertions(+), 230 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e56b56430..d6bc1c602 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -236,8 +236,8 @@ set(LEAN_LIBS ${LEAN_LIBS} library) # set(LEAN_LIBS ${LEAN_LIBS} rewriter) # add_subdirectory(library/simplifier) # set(LEAN_LIBS ${LEAN_LIBS} simplifier) -# add_subdirectory(library/tactic) -# set(LEAN_LIBS ${LEAN_LIBS} tactic) +add_subdirectory(library/tactic) +set(LEAN_LIBS ${LEAN_LIBS} tactic) add_subdirectory(library/error_handling) set(LEAN_LIBS ${LEAN_LIBS} error_handling) add_subdirectory(frontends/lean) diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 853e739e9..f7aee290e 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -43,7 +43,7 @@ Author: Leonardo de Moura #endif namespace lean { -static environment get_global_environment(lua_State * L); +environment get_global_environment(lua_State * L); io_state * get_io_state_ptr(lua_State * L); io_state get_tmp_io_state(lua_State * L); io_state get_io_state(lua_State * L) { @@ -1217,7 +1217,7 @@ static void set_global_environment_ptr(lua_State * L, environment * env) { lua_pushlightuserdata(L, static_cast(env)); lua_settable(L, LUA_REGISTRYINDEX); } -static environment get_global_environment(lua_State * L) { +environment get_global_environment(lua_State * L) { environment * env = get_global_environment_ptr(L); if (env == nullptr) throw exception("Lua state does not have an environment object"); diff --git a/src/library/kernel_bindings.h b/src/library/kernel_bindings.h index 5bd291dff..a1d809b0a 100644 --- a/src/library/kernel_bindings.h +++ b/src/library/kernel_bindings.h @@ -48,6 +48,7 @@ void set_global_formatter(lua_State * L, formatter const & fmt); /** \brief Set the Lua registry of a Lua state with an environment object. */ void set_global_environment(lua_State * L, environment const & env); +environment get_global_environment(lua_State * L); /** \brief Auxiliary class for temporarily setting the Lua registry of a Lua state with an environment object. diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 8c799aaae..d61ca81b1 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -1,5 +1,7 @@ -add_library(tactic goal.cpp proof_builder.cpp cex_builder.cpp -proof_state.cpp tactic.cpp boolean_tactics.cpp apply_tactic.cpp -simplify_tactic.cpp) +add_library(tactic goal.cpp) + +# proof_builder.cpp cex_builder.cpp +# proof_state.cpp tactic.cpp boolean_tactics.cpp apply_tactic.cpp +# simplify_tactic.cpp) target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp index 4be27a0a5..95273ebc3 100644 --- a/src/library/tactic/goal.cpp +++ b/src/library/tactic/goal.cpp @@ -1,53 +1,18 @@ /* -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 */ #include -#include -#include -#include "util/name_set.h" #include "util/buffer.h" -#include "kernel/for_each_fn.h" -#include "kernel/replace_fn.h" -#include "kernel/abstract.h" -#include "kernel/type_checker.h" #include "library/kernel_bindings.h" #include "library/tactic/goal.h" namespace lean { - -name mk_unique_hypothesis_name(hypotheses const & hs, name const & suggestion) { - name n = suggestion; - unsigned i = 0; - // TODO(Leo): investigate if this method is a performance bottleneck - while (true) { - bool ok = true; - for (auto const & p : hs) { - if (is_prefix_of(n, p.first)) { - ok = false; - break; - } - } - if (ok) { - return n; - } else { - i++; - n = name(suggestion, i); - } - } -} - -name update_hypotheses_fn::operator()(name const & suggestion, expr const & t) { - name n = mk_unique_hypothesis_name(m_hypotheses, suggestion); - m_hypotheses.emplace_front(n, t); - return n; -} - goal::goal(hypotheses const & hs, expr const & c):m_hypotheses(hs), m_conclusion(c) {} -format goal::pp(formatter const & fmt, options const & opts) const { +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("|-"); @@ -61,118 +26,14 @@ format goal::pp(formatter const & fmt, options const & opts) const { } else { r += compose(comma(), line()); } - r += format{format(p.first), space(), colon(), nest(indent, compose(line(), fmt(p.second, opts)))}; + r += format{format(p.first), space(), colon(), nest(indent, compose(line(), fmt(env, p.second, opts)))}; } r = group(r); - r += format{line(), turnstile, space(), nest(indent, fmt(m_conclusion, opts))}; + r += format{line(), turnstile, space(), nest(indent, fmt(env, m_conclusion, opts))}; return group(r); } -name goal::mk_unique_hypothesis_name(name const & suggestion) const { - return ::lean::mk_unique_hypothesis_name(m_hypotheses, suggestion); -} - -goal_proof_fn::goal_proof_fn(std::vector && consts): - m_constants(consts) { -} - -expr goal_proof_fn::operator()(expr const & pr) const { - return abstract(pr, m_constants.size(), m_constants.data()); -} - -static name_set collect_used_names(context const & ctx, expr const & t) { - name_set r; - auto f = [&r](expr const & e, unsigned) { if (is_constant(e)) r.insert(const_name(e)); return true; }; - for_each_fn visitor(f); - for (auto const & e : ctx) { - if (optional const & d = e.get_domain()) - visitor(*d); - if (optional const & b = e.get_body()) - visitor(*b); - } - visitor(t); - return r; -} - -static name mk_unique_name(name_set & s, name const & suggestion) { - unsigned i = 1; - name n = suggestion; - while (true) { - if (s.find(n) == s.end()) { - s.insert(n); - return n; - } else { - n = name(suggestion, i); - i++; - } - } -} - -static name g_unused = name::mk_internal_unique_name(); -static expr g_unused_const = mk_constant(g_unused); - -std::pair to_goal(ro_environment const & env, context const & ctx, expr const & t) { - type_inferer inferer(env); - if (!inferer.is_proposition(t, ctx)) - throw type_is_not_proposition_exception(); - name_set used_names = collect_used_names(ctx, t); - buffer entries; - for (auto const & e : ctx) - entries.push_back(e); - std::reverse(entries.begin(), entries.end()); - buffer hypotheses; // normalized names and types of the entries processed so far - buffer> bodies; // normalized bodies of the entries processed so far - std::vector consts; // cached consts[i] == mk_constant(names[i], hypotheses[i]) - auto replace_vars = [&](expr const & e, unsigned offset) -> expr { - if (is_var(e)) { - unsigned vidx = var_idx(e); - if (vidx >= offset) { - unsigned nvidx = vidx - offset; - unsigned nfv = consts.size(); - if (nvidx >= nfv) - throw exception("failed to create goal, unknown free variable"); - unsigned lvl = nfv - nvidx - 1; - if (bodies[lvl]) - return *(bodies[lvl]); - else - return consts[lvl]; - } - } - return e; - }; - replace_fn replacer(replace_vars); - auto it = entries.begin(); - auto end = entries.end(); - for (; it != end; ++it) { - auto const & e = *it; - name n = mk_unique_name(used_names, e.get_name()); - optional d = e.get_domain(); - optional b = e.get_body(); - if (d) d = some_expr(replacer(*d)); - if (b) b = some_expr(replacer(*b)); - if (b && !d) { - d = some_expr(inferer(*b)); - } - replacer.clear(); - if (b && !inferer.is_proposition(*d)) { - bodies.push_back(b); - // Insert a dummy just to make sure consts has the right size. - // The dummy must be a closed term, and should not be used anywhere else. - consts.push_back(g_unused_const); - } else { - lean_assert(d); - hypotheses.emplace_back(n, *d); - bodies.push_back(none_expr()); - expr c = mk_constant(n, *d); - consts.push_back(c); - } - } - expr conclusion = replacer(t); - return mk_pair(goal(to_list(hypotheses.begin(), hypotheses.end()), conclusion), - goal_proof_fn(std::move(consts))); -} - DECL_UDATA(hypotheses) static int mk_hypotheses(lua_State * L) { @@ -250,28 +111,16 @@ static const struct luaL_Reg hypotheses_m[] = { DECL_UDATA(goal) -static int mk_goal(lua_State * L) { - return push_goal(L, goal(to_hypotheses(L, 1), to_expr(L, 2))); -} - -static int goal_hypotheses(lua_State * L) { - return push_hypotheses(L, to_goal(L, 1).get_hypotheses()); -} - -static int goal_conclusion(lua_State * L) { - return push_expr(L, to_goal(L, 1).get_conclusion()); -} - -static int goal_unique_name(lua_State * L) { - return push_name(L, to_goal(L, 1).mk_unique_hypothesis_name(to_name_ext(L, 2))); -} - +static int mk_goal(lua_State * L) { return push_goal(L, goal(to_hypotheses(L, 1), to_expr(L, 2))); } +static int goal_hypotheses(lua_State * L) { return push_hypotheses(L, to_goal(L, 1).get_hypotheses()); } +static int goal_conclusion(lua_State * L) { return push_expr(L, to_goal(L, 1).get_conclusion()); } static int goal_tostring(lua_State * L) { std::ostringstream out; goal & g = to_goal(L, 1); - formatter fmt = get_global_formatter(L); - options opts = get_global_options(L); - out << mk_pair(g.pp(fmt, opts), opts); + environment env = get_global_environment(L); + formatter fmt = get_global_formatter(L); + options opts = get_global_options(L); + out << mk_pair(g.pp(env, fmt, opts), opts); lua_pushstring(L, out.str().c_str()); return 1; } @@ -280,14 +129,13 @@ static int goal_pp(lua_State * L) { int nargs = lua_gettop(L); goal & g = to_goal(L, 1); if (nargs == 1) { - return push_format(L, g.pp(get_global_formatter(L), get_global_options(L))); + return push_format(L, g.pp(get_global_environment(L), get_global_formatter(L), get_global_options(L))); } else if (nargs == 2) { - if (is_formatter(L, 2)) - return push_format(L, g.pp(to_formatter(L, 2), get_global_options(L))); - else - return push_format(L, g.pp(get_global_formatter(L), to_options(L, 2))); + return push_format(L, g.pp(to_environment(L, 2), get_global_formatter(L), get_global_options(L))); + } else if (nargs == 3) { + return push_format(L, g.pp(to_environment(L, 2), to_formatter(L, 3), get_global_options(L))); } else { - return push_format(L, g.pp(to_formatter(L, 2), to_options(L, 3))); + return push_format(L, g.pp(to_environment(L, 2), to_formatter(L, 3), to_options(L, 4))); } } @@ -297,7 +145,6 @@ static const struct luaL_Reg goal_m[] = { {"hypotheses", safe_function}, {"hyps", safe_function}, {"conclusion", safe_function}, - {"unique_name", safe_function}, {"pp", safe_function}, {0, 0} }; diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h index ee1dcafd9..20e19561c 100644 --- a/src/library/tactic/goal.h +++ b/src/library/tactic/goal.h @@ -1,47 +1,21 @@ /* -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 */ #pragma once #include -#include #include "util/lua.h" #include "util/list.h" #include "util/name.h" -#include "util/exception.h" #include "kernel/formatter.h" -#include "kernel/expr.h" -#include "kernel/context.h" #include "kernel/environment.h" +#include "library/io_state_stream.h" namespace lean { -class type_is_not_proposition_exception : public exception { -public: - type_is_not_proposition_exception() {} - virtual ~type_is_not_proposition_exception() noexcept {} - virtual char const * what() const noexcept { return "type is not a propostion"; } - virtual exception * clone() const { return new type_is_not_proposition_exception(); } - virtual void rethrow() const { throw *this; } -}; - typedef std::pair hypothesis; typedef list hypotheses; - -class update_hypotheses_fn { - hypotheses m_hypotheses; -public: - update_hypotheses_fn(hypotheses const & hs):m_hypotheses(hs) {} - hypotheses const & get_hypotheses() const { return m_hypotheses; } - /** - \brief Add a new hypothesis, the name \c n is a suggestion. - The method checks if the given name collides with an existing name. - It returns the actual name used. - */ - name operator()(name const & n, expr const & t); -}; - class goal { hypotheses m_hypotheses; expr m_conclusion; @@ -50,8 +24,7 @@ public: goal(hypotheses const & hs, expr const & c); hypotheses const & get_hypotheses() const { return m_hypotheses; } expr const & get_conclusion() const { return m_conclusion; } - format pp(formatter const & fmt, options const & opts) const; - name mk_unique_hypothesis_name(name const & suggestion) 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); } @@ -64,30 +37,7 @@ inline hypotheses add_hypothesis(hypothesis const & h, hypotheses const & hs) { return cons(h, hs); } -/** - \brief Functor for converting a proof for a goal \c g produced using to_goal(env, ctx, T) - into a term of type \c t. - - That is, the goal was created to synthesize a proof term for a proposition/type \c T in a - context \c ctx. This functor allows us to convert a proof for \c g into a term/expression \c p - s.t. ctx |- p : T -*/ -class goal_proof_fn { - friend std::pair to_goal(ro_environment const & env, context const & ctx, expr const & t); - std::vector m_constants; - goal_proof_fn(std::vector && constants); -public: - expr operator()(expr const & pr) const; -}; - -/** - \brief Convert the synthesis problem ctx |- ?p : T into a goal, - where \c T is a proposition (i.e., has type Boolean), and \c ?p is a proof we want to synthesize. - - We can use tactics for solving the resultant goal, and the functor \c goal_proof_fn - to convert the proof for the goal into the proof term \c ?p. -*/ -std::pair to_goal(ro_environment const & env, context const & ctx, expr const & t); +io_state_stream const & operator<<(io_state_stream const & out, goal const & g); UDATA_DEFS_CORE(hypotheses) UDATA_DEFS(goal)