diff --git a/src/library/tactic/cex_builder.cpp b/src/library/tactic/cex_builder.cpp index 2fd9a828ff..c1c3e59e2f 100644 --- a/src/library/tactic/cex_builder.cpp +++ b/src/library/tactic/cex_builder.cpp @@ -11,18 +11,18 @@ Author: Leonardo de Moura #include "library/tactic/cex_builder.h" namespace lean { -cex_builder_fn mk_cex_builder_for(name const & gname) { - return cex_builder_fn([=](name const & n, optional const & cex, substitution const &) -> counterexample { +cex_builder mk_cex_builder_for(name const & gname) { + return cex_builder([=](name const & n, optional const & cex, substitution const &) -> counterexample { if (n != gname || !cex) throw exception(sstream() << "failed to build counterexample for '" << gname << "' goal"); return *cex; }); } -cex_builder_fn to_cex_builder(lua_State * L, int idx) { +cex_builder to_cex_builder(lua_State * L, int idx) { luaL_checktype(L, idx, LUA_TFUNCTION); // user-fun luaref f(L, idx); - return cex_builder_fn([=](name const & n, optional const & cex, substitution const & s) { + return cex_builder([=](name const & n, optional const & cex, substitution const & s) { lua_State * L = f.get_state(); f.push(); push_name(L, n); diff --git a/src/library/tactic/cex_builder.h b/src/library/tactic/cex_builder.h index 237ac30a93..6df4a1937b 100644 --- a/src/library/tactic/cex_builder.h +++ b/src/library/tactic/cex_builder.h @@ -15,10 +15,10 @@ Author: Leonardo de Moura namespace lean { /** \brief In Lean, a counter-example is encoded using an environment object. */ typedef environment counterexample; -typedef std::function const &, substitution const &)> cex_builder_fn; +typedef std::function const &, substitution const &)> cex_builder; /** \brief Return a counterexample builder that expects a counterexample for the given goal. */ -cex_builder_fn mk_cex_builder_for(name const & gname); +cex_builder mk_cex_builder_for(name const & gname); /** \brief Convert a Lua function on position \c idx (on the Lua stack) to a cex_builder_fn */ -cex_builder_fn to_cex_builder(lua_State * L, int idx); +cex_builder to_cex_builder(lua_State * L, int idx); } diff --git a/src/library/tactic/proof_builder.cpp b/src/library/tactic/proof_builder.cpp index a7361a0522..9f680f0953 100644 --- a/src/library/tactic/proof_builder.cpp +++ b/src/library/tactic/proof_builder.cpp @@ -19,8 +19,8 @@ expr find(proof_map const & m, name const & n) { throw exception(sstream() << "proof for goal '" << n << "' not found"); } -proof_builder_fn add_proofs(proof_builder_fn const & pb, list> const & prs) { - return proof_builder_fn([=](proof_map const & m, substitution const & s) -> expr { +proof_builder add_proofs(proof_builder const & pb, list> const & prs) { + return proof_builder([=](proof_map const & m, substitution const & s) -> expr { proof_map new_m(m); for (auto const & np : prs) { new_m.insert(np.first, np.second); @@ -61,10 +61,10 @@ static const struct luaL_Reg proof_map_m[] = { {0, 0} }; -proof_builder_fn to_proof_builder(lua_State * L, int idx) { +proof_builder to_proof_builder(lua_State * L, int idx) { luaL_checktype(L, idx, LUA_TFUNCTION); // user-fun luaref f(L, idx); - return proof_builder_fn([=](proof_map const & m, substitution const & s) { + return proof_builder([=](proof_map const & m, substitution const & s) { lua_State * L = f.get_state(); f.push(); push_proof_map(L, m); diff --git a/src/library/tactic/proof_builder.h b/src/library/tactic/proof_builder.h index c2c8318bbc..8530ee1f3c 100644 --- a/src/library/tactic/proof_builder.h +++ b/src/library/tactic/proof_builder.h @@ -23,11 +23,11 @@ expr find(proof_map const & m, name const & n); \brief A proof builder creates an inhabitant a goal type (aka conclusion) using the inhabitants for its subgoals. */ -typedef std::function proof_builder_fn; -proof_builder_fn add_proofs(proof_builder_fn const & pb, list> const & prs); +typedef std::function proof_builder; +proof_builder add_proofs(proof_builder const & pb, list> const & prs); /** \brief Convert a Lua function on position \c idx (on the Lua stack) into a proof_builder_fn */ -proof_builder_fn to_proof_builder(lua_State * L, int idx); +proof_builder to_proof_builder(lua_State * L, int idx); UDATA_DEFS_CORE(proof_map) void open_proof_builder(lua_State * L); } diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index ee016fcb29..bb62a393f7 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -93,8 +93,8 @@ void proof_state::get_goal_names(name_set & r) const { } static name g_main("main"); -proof_builder_fn mk_init_proof_builder(list const & locals) { - return proof_builder_fn([=](proof_map const & m, substitution const &) -> expr { +proof_builder mk_init_proof_builder(list const & locals) { + return proof_builder([=](proof_map const & m, substitution const &) -> expr { expr r = find(m, g_main); for (expr const & l : locals) r = Fun(l, r); diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 8d4d79ea15..14aa6e46bf 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -33,27 +33,27 @@ bool trust_cex(precision p); class proof_state { precision m_precision; goals m_goals; - proof_builder_fn m_proof_builder; - cex_builder_fn m_cex_builder; + proof_builder m_proof_builder; + cex_builder m_cex_builder; name_generator m_ngen; list m_init_locals; public: - proof_state(precision prec, goals const & gs, proof_builder_fn const & pb, cex_builder_fn const & cb, + proof_state(precision prec, goals const & gs, proof_builder const & pb, cex_builder const & cb, name_generator const & ngen, list const & ls = list()): m_precision(prec), m_goals(gs), m_proof_builder(pb), m_cex_builder(cb), m_ngen(ngen), m_init_locals(ls) {} - proof_state(goals const & gs, proof_builder_fn const & pb, cex_builder_fn const & cb, + proof_state(goals const & gs, proof_builder const & pb, cex_builder const & cb, name_generator const & ngen, list const & ls = list()): proof_state(precision::Precise, gs, pb, cb, ngen, ls) {} - proof_state(proof_state const & s, goals const & gs, proof_builder_fn const & pb, cex_builder_fn const & cb): + proof_state(proof_state const & s, goals const & gs, proof_builder const & pb, cex_builder const & cb): proof_state(s.m_precision, gs, pb, cb, s.m_ngen, s.m_init_locals) {} - proof_state(proof_state const & s, goals const & gs, proof_builder_fn const & pb, name_generator const & ngen): + proof_state(proof_state const & s, goals const & gs, proof_builder const & pb, name_generator const & ngen): proof_state(s.m_precision, gs, pb, s.m_cex_builder, ngen, s.m_init_locals) {} - proof_state(proof_state const & s, goals const & gs, proof_builder_fn const & pb):proof_state(s, gs, pb, s.m_ngen) {} + proof_state(proof_state const & s, goals const & gs, proof_builder const & pb):proof_state(s, gs, pb, s.m_ngen) {} proof_state(proof_state const & s, goals const & gs):proof_state(s, gs, s.m_proof_builder) {} precision get_precision() const { return m_precision; } goals const & get_goals() const { return m_goals; } - proof_builder_fn const & get_pb() const { return m_proof_builder; } - cex_builder_fn const & get_cb() const { return m_cex_builder; } + proof_builder const & get_pb() const { return m_proof_builder; } + cex_builder const & get_cb() const { return m_cex_builder; } name_generator const & ngen() const { return m_ngen; } list const & get_init_locals() const { return m_init_locals; } /** \brief Return true iff this state does not have any goals left, and the precision is \c Precise or \c Over */ diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 050760ba8b..8d555d31af 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.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 @@ -219,8 +219,8 @@ tactic beta_tactic() { proof_state_seq focus_core(tactic const & t, name const & gname, environment const & env, io_state const & ios, proof_state const & s) { for (auto const & p : s.get_goals()) { if (p.first == gname) { - proof_builder_fn pb = proof_builder_fn([=](proof_map const & m, substitution const &) -> expr { return find(m, gname); }); - cex_builder_fn cb = mk_cex_builder_for(gname); + proof_builder pb = proof_builder([=](proof_map const & m, substitution const &) -> expr { return find(m, gname); }); + cex_builder cb = mk_cex_builder_for(gname); proof_state new_s(s, goals(p), pb, cb); // new state with singleton goal return map(t(env, ios, new_s), [=](proof_state const & s2) { // we have to put back the goals that were not selected @@ -240,9 +240,9 @@ proof_state_seq focus_core(tactic const & t, name const & gname, environment con return goals(p); } }); - proof_builder_fn pb1 = s.get_pb(); - proof_builder_fn pb2 = s2.get_pb(); - proof_builder_fn new_pb = proof_builder_fn( + proof_builder pb1 = s.get_pb(); + proof_builder pb2 = s2.get_pb(); + proof_builder new_pb = proof_builder( [=](proof_map const & m, substitution const & a) -> expr { proof_map m1(m); // map for pb1 proof_map m2; // map for pb2 @@ -253,9 +253,9 @@ proof_state_seq focus_core(tactic const & t, name const & gname, environment con m1.insert(gname, pb2(m2, a)); return pb1(m1, a); }); - cex_builder_fn cb1 = s.get_cb(); - cex_builder_fn cb2 = s2.get_cb(); - cex_builder_fn new_cb = cex_builder_fn( + cex_builder cb1 = s.get_cb(); + cex_builder cb2 = s2.get_cb(); + cex_builder new_cb = cex_builder( [=](name const & n, optional const & cex, substitution const & a) -> counterexample { for (auto p : renamed_goals) { if (p.second == n) diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index fbd0384e52..ef1f61361b 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.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 @@ -110,7 +110,7 @@ tactic repeat_at_most(tactic const & t, unsigned k); tactic take(tactic const & t, unsigned k); /** \brief Syntax sugar for take(t, 1) */ inline tactic determ(tactic const & t) { return take(t, 1); } -typedef std::function proof_state_pred; +typedef std::function proof_state_pred; // NOLINT /** \brief Return a tactic that applies the predicate \c p to the input state. If \c p returns true, then applies \c t1. Otherwise, applies \c t2.