michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/tactic): name convention

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-27 18:42:59 -07:00
parent fa72e7b874
commit e408998e06
8 changed files with 36 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/tactic/cex_builder.cpp
View file

@ -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<counterexample> const & cex, substitution const &) -> counterexample {
cex_builder mk_cex_builder_for(name const & gname) {
return cex_builder([=](name const & n, optional<counterexample> 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<counterexample> const & cex, substitution const & s) {
return cex_builder([=](name const & n, optional<counterexample> const & cex, substitution const & s) {
lua_State * L = f.get_state();
f.push();
push_name(L, n);

6
src/library/tactic/cex_builder.h
View file

@ -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<counterexample(name const &, optional<counterexample> const &, substitution const &)> cex_builder_fn;
typedef std::function<counterexample(name const &, optional<counterexample> 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);
}

8
src/library/tactic/proof_builder.cpp
View file

@ -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<std::pair<name, expr>> const & prs) {
return proof_builder_fn([=](proof_map const & m, substitution const & s) -> expr {
proof_builder add_proofs(proof_builder const & pb, list<std::pair<name, expr>> 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);

6
src/library/tactic/proof_builder.h
View file

@ -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<expr(proof_map const &, substitution const &)> proof_builder_fn;
proof_builder_fn add_proofs(proof_builder_fn const & pb, list<std::pair<name, expr>> const & prs);
typedef std::function<expr(proof_map const &, substitution const &)> proof_builder;
proof_builder add_proofs(proof_builder const & pb, list<std::pair<name, expr>> 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);
}

4
src/library/tactic/proof_state.cpp
View file

@ -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<expr> const & locals) {
return proof_builder_fn([=](proof_map const & m, substitution const &) -> expr {
proof_builder mk_init_proof_builder(list<expr> 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);

18
src/library/tactic/proof_state.h
View file

@ -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<expr> 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<expr> const & ls = list<expr>()):
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<expr> const & ls = list<expr>()):
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<expr> 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 */

18
src/library/tactic/tactic.cpp
View file

@ -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<counterexample> const & cex, substitution const & a) -> counterexample {
for (auto p : renamed_goals) {
if (p.second == n)

4
src/library/tactic/tactic.h
View file

@ -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<bool(environment const & env, io_state const & ios, proof_state const & s)> proof_state_pred;
typedef std::function<bool(environment const & env, io_state const & ios, proof_state const & s)> 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.