chore(library/tactic): update goal objects

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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)
+add_subdirectory(library/tactic)
-# set(LEAN_LIBS ${LEAN_LIBS} tactic)
+set(LEAN_LIBS ${LEAN_LIBS} tactic)
 add_subdirectory(library/error_handling)
 set(LEAN_LIBS ${LEAN_LIBS} error_handling)
 add_subdirectory(frontends/lean)

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<void *>(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");

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.

src/library/tactic/CMakeLists.txt

@@ -1,5 +1,7 @@
-add_library(tactic goal.cpp proof_builder.cpp cex_builder.cpp
+add_library(tactic goal.cpp)
-proof_state.cpp tactic.cpp boolean_tactics.cpp apply_tactic.cpp
+
-simplify_tactic.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})

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 <utility>
-#include <vector>
-#include <algorithm>
-#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<expr> && 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<decltype(f)> visitor(f);
-    for (auto const & e : ctx) {
-        if (optional<expr> const & d = e.get_domain())
-            visitor(*d);
-        if (optional<expr> 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<goal, goal_proof_fn> 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<context_entry> entries;
-    for (auto const & e : ctx)
-        entries.push_back(e);
-    std::reverse(entries.begin(), entries.end());
-    buffer<hypothesis> hypotheses;   // normalized names and types of the entries processed so far
-    buffer<optional<expr>> bodies;   // normalized bodies of the entries processed so far
-    std::vector<expr> 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<decltype(replace_vars)> 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<expr> d = e.get_domain();
-        optional<expr> 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) {
+static int mk_goal(lua_State * L) { return push_goal(L, goal(to_hypotheses(L, 1), to_expr(L, 2))); }
-    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_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 goal_tostring(lua_State * L) {
     std::ostringstream out;
     goal & g = to_goal(L, 1);
+    environment env = get_global_environment(L);
     formatter fmt   = get_global_formatter(L);
     options opts    = get_global_options(L);
-    out << mk_pair(g.pp(fmt, opts), opts);
+    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_environment(L, 2), get_global_formatter(L), get_global_options(L)));
-            return push_format(L, g.pp(to_formatter(L, 2), get_global_options(L)));
+    } else if (nargs == 3) {
-        else
+        return push_format(L, g.pp(to_environment(L, 2), to_formatter(L, 3), get_global_options(L)));
-            return push_format(L, g.pp(get_global_formatter(L), to_options(L, 2)));
     } 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<goal_hypotheses>},
     {"hyps",            safe_function<goal_hypotheses>},
     {"conclusion",      safe_function<goal_conclusion>},
-    {"unique_name",     safe_function<goal_unique_name>},
     {"pp",              safe_function<goal_pp>},
     {0, 0}
 };

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 <utility>
-#include <vector>
 #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<name, expr> hypothesis;
 typedef list<hypothesis>      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;
+    format pp(environment const & env, formatter const & fmt, options const & opts) const;
-    name mk_unique_hypothesis_name(name const & suggestion) 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);
 }
 
-/**
+io_state_stream const & operator<<(io_state_stream const & out, goal const & g);
-   \brief Functor for converting a proof for a goal \c g produced using <tt>to_goal(env, ctx, T)</tt>
-   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. <tt>ctx |- p : T</t>
-*/
-class goal_proof_fn {
-    friend std::pair<goal, goal_proof_fn> to_goal(ro_environment const & env, context const & ctx, expr const & t);
-    std::vector<expr> m_constants;
-    goal_proof_fn(std::vector<expr> && constants);
-public:
-    expr operator()(expr const & pr) const;
-};
-
-/**
-   \brief Convert the synthesis problem <tt>ctx |- ?p : T</tt> 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<goal, goal_proof_fn> to_goal(ro_environment const & env, context const & ctx, expr const & t);
 
 UDATA_DEFS_CORE(hypotheses)
 UDATA_DEFS(goal)