diff --git a/src/library/tactic/cex_builder.h b/src/library/tactic/cex_builder.h new file mode 100644 index 000000000..7e28ec0c3 --- /dev/null +++ b/src/library/tactic/cex_builder.h @@ -0,0 +1,68 @@ +/* +Copyright (c) 2013 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 "util/debug.h" +#include "util/name.h" +#include "util/rc.h" +#include "kernel/expr.h" +#include "kernel/environment.h" +#include "library/tactic/assignment.h" + +namespace lean { +/** + \brief In Lean, a counter-example is encoded using an environment object. +*/ +typedef environment counterexample; + +/** + \brief Base class for functors that build a counterexample for the main goal based on + a counterexample for a subgoal. +*/ +class cex_builder_cell { + void dealloc() { delete this; } + MK_LEAN_RC(); +public: + cex_builder_cell():m_rc(0) {} + virtual ~cex_builder_cell() {} + virtual counterexample operator()(name const & n, optional const & cex, assignment const & a) const = 0; +}; + +template +class cex_builder_tpl : public cex_builder_cell { + F m_f; +public: + cex_builder_tpl(F && f):m_f(f) {} + virtual counterexample operator()(name const & n, optional const & cex, assignment const & a) const { + return m_f(n, cex, a); + } +}; + +/** + \brief Smart pointer for a counterexample builder functor. +*/ +class cex_builder { +protected: + cex_builder_cell * m_ptr; +public: + cex_builder():m_ptr(nullptr) {} + explicit cex_builder(cex_builder_cell * ptr):m_ptr(ptr) { lean_assert(m_ptr); m_ptr->inc_ref(); } + cex_builder(cex_builder const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } + cex_builder(cex_builder && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } + ~cex_builder() { if (m_ptr) m_ptr->dec_ref(); } + friend void swap(cex_builder & a, cex_builder & b) { std::swap(a.m_ptr, b.m_ptr); } + cex_builder & operator=(cex_builder const & s) { LEAN_COPY_REF(cex_builder, s); } + cex_builder & operator=(cex_builder && s) { LEAN_MOVE_REF(cex_builder, s); } + + counterexample operator()(name const & n, optional const & cex, assignment const & a) const { return m_ptr->operator()(n, cex, a); } +}; + +template +cex_builder mk_cex_builder(F && f) { + return cex_builder(new cex_builder_tpl(std::forward(f))); +} +} diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index cabb6230c..f5789f487 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -8,6 +8,21 @@ Author: Leonardo de Moura #include "library/tactic/proof_state.h" namespace lean { +precision mk_union(precision p1, precision p2) { + if (p1 == p2) return p1; + else if (p1 == precision::Precise) return p2; + else if (p2 == precision::Precise) return p1; + else return precision::UnderOver; +} + +bool trust_proofs(precision p) { + return p == precision::Precise || p == precision::Over; +} + +bool trust_cex(precision p) { + return p == precision::Precise || p == precision::Under; +} + format proof_state::pp(formatter const & fmt, options const & opts) const { format r; bool first = true; @@ -29,11 +44,14 @@ proof_state to_proof_state(environment const & env, context const & ctx, expr co goal_proof_fn fn = gfn.second; proof_builder pr_builder = mk_proof_builder( [=](proof_map const & m, assignment const &) -> expr { - expr p = find(m, g_main); - if (!p) - throw exception(sstream() << "failed to find proof for '" << g_main << "' goal"); - return fn(p); + return fn(find(m, g_main)); }); - return proof_state(goals(mk_pair(g_main, g)), metavar_env(), pr_builder); + cex_builder cex_builder = mk_cex_builder( + [](name const & n, optional const & cex, assignment const &) -> counterexample { + if (n != g_main || !cex) + throw exception(sstream() << "failed to build counterexample for '" << g_main << "' goal"); + return *cex; + }); + return proof_state(goals(mk_pair(g_main, g)), metavar_env(), pr_builder, cex_builder); } } diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index a9d5c867a..e20e16af9 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -12,34 +12,55 @@ Author: Leonardo de Moura #include "util/optional.h" #include "library/tactic/goal.h" #include "library/tactic/proof_builder.h" +#include "library/tactic/cex_builder.h" namespace lean { typedef list> goals; + +enum class precision { + Precise, + Under, // counter-examples can be trusted + Over, // proofs can be trusted + UnderOver // proof_state is garbage: it was produced using under and over approximation steps. +}; + +precision mk_union(precision p1, precision p2); +bool trust_proofs(precision p); +bool trust_cex(precision p); + class proof_state { struct cell { MK_LEAN_RC(); + precision m_precision; goals m_goals; metavar_env m_menv; proof_builder m_proof_builder; + cex_builder m_cex_builder; void dealloc() { delete this; } cell():m_rc(1) {} - cell(goals const & gs, metavar_env const & menv, proof_builder const & p): - m_rc(1), m_goals(gs), m_menv(menv), m_proof_builder(p) {} + cell(precision prec, goals const & gs, metavar_env const & menv, proof_builder const & p, cex_builder const & c): + m_rc(1), m_precision(prec), m_goals(gs), m_menv(menv), m_proof_builder(p), m_cex_builder(c) {} + cell(goals const & gs, metavar_env const & menv, proof_builder const & p, cex_builder const & c): + m_rc(1), m_precision(precision::Precise), m_goals(gs), m_menv(menv), m_proof_builder(p), m_cex_builder(c) {} }; cell * m_ptr; public: proof_state():m_ptr(new cell()) {} proof_state(proof_state const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } proof_state(proof_state && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } - proof_state(goals const & gs, metavar_env const & menv, proof_builder const & p):m_ptr(new cell(gs, menv, p)) {} - proof_state(proof_state const & s, goals const & gs, proof_builder const & p):m_ptr(new cell(gs, s.m_ptr->m_menv, p)) {} + proof_state(goals const & gs, metavar_env const & menv, proof_builder const & p, cex_builder const & c): + m_ptr(new cell(gs, menv, p, c)) {} + proof_state(proof_state const & s, goals const & gs, proof_builder const & p): + m_ptr(new cell(s.get_precision(), gs, s.get_menv(), p, s.get_cex_builder())) {} ~proof_state() { if (m_ptr) m_ptr->dec_ref(); } friend void swap(proof_state & a, proof_state & b) { std::swap(a.m_ptr, b.m_ptr); } proof_state & operator=(proof_state const & s) { LEAN_COPY_REF(proof_state, s); } proof_state & operator=(proof_state && s) { LEAN_MOVE_REF(proof_state, s); } + precision get_precision() const { lean_assert(m_ptr); return m_ptr->m_precision; } goals const & get_goals() const { lean_assert(m_ptr); return m_ptr->m_goals; } metavar_env const & get_menv() const { lean_assert(m_ptr); return m_ptr->m_menv; } proof_builder const & get_proof_builder() const { lean_assert(m_ptr); return m_ptr->m_proof_builder; } + cex_builder const & get_cex_builder() const { lean_assert(m_ptr); return m_ptr->m_cex_builder; } format pp(formatter const & fmt, options const & opts) const; }; diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index fbe3a73ce..a3e1292bc 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -27,6 +27,8 @@ expr tactic::solve(environment const & env, io_state const & io, proof_state con if (!p) throw exception("tactic failed to solve input"); proof_state final = p->first; + if (!trust_proofs(final.get_precision())) + throw exception("tactic failed to solve input, final state is not precise"); assignment a(final.get_menv()); proof_map m; return final.get_proof_builder()(m, a);