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

refactor(library/tactic): remove justification_builder

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-21 17:25:19 -08:00
parent 41062fdf9f
commit 796fb3c3bf
6 changed files with 63 additions and 112 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

52
src/library/tactic/justification_builder.h
View file

@ -1,52 +0,0 @@
/*
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 <algorithm>
#include "util/name.h"
#include "util/rc.h"
#include "kernel/expr.h"
#include "kernel/justification.h"
#include "library/tactic/assignment.h"
namespace lean {
class justification_builder_cell {
void dealloc() { delete this; }
MK_LEAN_RC();
public:
virtual ~justification_builder_cell() {}
virtual justification operator()(name const & n, justification const & j, environment const & env, assignment const & a) const = 0;
};
class justification_builder {
protected:
justification_builder_cell * m_ptr;
public:
justification_builder():m_ptr(nullptr) {}
explicit justification_builder(justification_builder_cell * ptr):m_ptr(ptr) { lean_assert(m_ptr); m_ptr->inc_ref(); }
justification_builder(justification_builder const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
justification_builder(justification_builder && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
~justification_builder() { if (m_ptr) m_ptr->dec_ref(); }
friend void swap(justification_builder & a, justification_builder & b) { std::swap(a.m_ptr, b.m_ptr); }
justification_builder & operator=(justification_builder const & s) { LEAN_COPY_REF(justification_builder, s); }
justification_builder & operator=(justification_builder && s) { LEAN_MOVE_REF(justification_builder, s); }
justification operator()(name const & n, justification const & j, environment const & env, assignment const & a) const { return m_ptr->operator()(n, j, env, a); }
};
template<typename F>
class simple_justification_builder : public justification_builder_cell {
F m_f;
public:
simple_justification_builder(F && f):m_f(std::forward<F>(f)) {}
virtual justification operator()(name const & n, justification const & j, environment const & env, assignment const & a) const { return m_f(n, j, env, a); }
};
template<typename F>
justification_builder mk_justification_builder(F && f) {
return justification_builder(new simple_justification_builder<F>(std::forward<F>(f)));
}
}

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

@ -26,7 +26,6 @@ void swap(proof_state & s1, proof_state & s2) {
swap(s1.m_goals, s2.m_goals);
swap(s1.m_menv, s2.m_menv);
swap(s1.m_proof_builder, s2.m_proof_builder);
swap(s1.m_justification_builder, s2.m_justification_builder);
}
static name g_main("main");
@ -42,12 +41,6 @@ proof_state to_proof_state(environment const & env, context const & ctx, expr co
throw tactic_exception(sstream() << "failed to find proof for '" << g_main << "' goal");
return fn(p);
});
justification_builder j = mk_justification_builder(
[](name const & n, justification const & j, environment const &, assignment const &) -> justification {
if (n != g_main)
throw tactic_exception(sstream() << "unknown goal name '" << n << "'");
return j;
});
return proof_state(goals(mk_pair(g_main, g)), metavar_env(), p, j);
return proof_state(goals(mk_pair(g_main, g)), metavar_env(), p);
}
}

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

@ -8,7 +8,6 @@ Author: Leonardo de Moura
#include <utility>
#include "library/tactic/goal.h"
#include "library/tactic/proof_builder.h"
#include "library/tactic/justification_builder.h"
namespace lean {
typedef list<std::pair<name, goal>> goals;
@ -16,18 +15,16 @@ class proof_state {
goals m_goals;
metavar_env m_menv;
proof_builder m_proof_builder;
justification_builder m_justification_builder;
public:
proof_state() {}
proof_state(list<std::pair<name, goal>> const & gs, metavar_env const & menv, proof_builder const & p, justification_builder const & j):
m_goals(gs), m_menv(menv), m_proof_builder(p), m_justification_builder(j) {}
proof_state(list<std::pair<name, goal>> const & gs, metavar_env const & menv, proof_builder const & p):
m_goals(gs), m_menv(menv), m_proof_builder(p) {}
proof_state(proof_state const & s, goals const & gs, proof_builder const & p):
m_goals(gs), m_menv(s.m_menv), m_proof_builder(p), m_justification_builder(s.m_justification_builder) {}
m_goals(gs), m_menv(s.m_menv), m_proof_builder(p) {}
friend void swap(proof_state & s1, proof_state & s2);
list<std::pair<name, goal>> const & get_goals() const { return m_goals; }
metavar_env const & get_menv() const { return m_menv; }
proof_builder const & get_proof_builder() const { return m_proof_builder; }
justification_builder const & get_justification_builder() const { return m_justification_builder; }
format pp(formatter const & fmt, options const & opts) const;
};
void swap(proof_state & s1, proof_state & s2);

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

@ -60,6 +60,55 @@ expr tactic::solve(environment const & env, io_state const & io, proof_state con
return final->get_proof_builder()(m, env, a);
}
expr tactic::solve(environment const & env, io_state const & io, context const & ctx, expr const & t) {
proof_state s = to_proof_state(env, ctx, t);
return solve(env, io, s);
}
tactic id_tactic() { return mk_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state { return s; }); }
tactic fail_tactic() { return mk_tactic([](environment const &, io_state const &, proof_state const &) -> proof_state { throw tactic_exception("failed"); }); }
tactic now_tactic() {
return mk_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state {
if (!empty(s.get_goals()))
throw tactic_exception("nowtac failed");
return s;
});
}
tactic assumption_tactic() {
return mk_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state {
list<std::pair<name, expr>> proofs;
goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal {
expr const & c = g.get_conclusion();
expr pr;
for (auto const & p : g.get_hypotheses()) {
check_interrupted();
if (p.second == c) {
pr = mk_constant(p.first);
break;
}
}
if (pr) {
proofs.emplace_front(ng, pr);
return goal();
} else {
return g;
}
});
proof_builder p = s.get_proof_builder();
proof_builder new_p = mk_proof_builder([=](proof_map const & m, environment const & env, assignment const & a) -> expr {
proof_map new_m(m);
for (auto const & np : proofs) {
new_m.insert(np.first, np.second);
}
return p(new_m, env, a);
});
return proof_state(s, new_goals, new_p);
});
}
class then_tactic : public tactic_cell {
tactic m_t1;
tactic m_t2;
@ -106,48 +155,4 @@ public:
};
tactic then(tactic const & t1, tactic const & t2) { return tactic(new then_tactic(t1, t2)); }
tactic id_tactic() { return mk_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state { return s; }); }
tactic fail_tactic() { return mk_tactic([](environment const &, io_state const &, proof_state const &) -> proof_state { throw tactic_exception("failed"); }); }
tactic now_tactic() {
return mk_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state {
if (!empty(s.get_goals()))
throw tactic_exception("nowtac failed");
return s;
});
}
tactic assumption_tactic() {
return mk_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state {
list<std::pair<name, expr>> proofs;
goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal {
expr const & c = g.get_conclusion();
expr pr;
for (auto const & p : g.get_hypotheses()) {
check_interrupted();
if (p.second == c) {
pr = mk_constant(p.first);
break;
}
}
if (pr) {
proofs.emplace_front(ng, pr);
return goal();
} else {
return g;
}
});
proof_builder p = s.get_proof_builder();
proof_builder new_p = mk_proof_builder([=](proof_map const & m, environment const & env, assignment const & a) -> expr {
proof_map new_m(m);
for (auto const & np : proofs) {
new_m.insert(np.first, np.second);
}
return p(new_m, env, a);
});
return proof_state(s, new_goals, new_p);
});
}
}

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

@ -58,6 +58,7 @@ public:
tactic_result_ref operator()(proof_state const & s) { return m_ptr->operator()(s); }
expr solve(environment const & env, io_state const & io, proof_state const & s);
expr solve(environment const & env, io_state const & io, context const & ctx, expr const & t);
};
template<typename F>

11
src/tests/library/tactic/tactic.cpp
View file

@ -9,9 +9,9 @@ Author: Leonardo de Moura
#include "library/all/all.h"
#include "library/tactic/goal.h"
#include "library/tactic/proof_builder.h"
#include "library/tactic/justification_builder.h"
#include "library/tactic/proof_state.h"
#include "library/tactic/tactic.h"
#include "library/tactic/tactic_exception.h"
using namespace lean;
static void tst1() {
@ -28,7 +28,14 @@ static void tst1() {
proof_state s = to_proof_state(env, ctx, p);
std::cout << s.pp(mk_simple_formatter(), options()) << "\n";
tactic t = then(assumption_tactic(), now_tactic());
std::cout << "proof: " << t.solve(env, io, s) << "\n";
std::cout << "proof 1: " << t.solve(env, io, s) << "\n";
std::cout << "proof 2: " << t.solve(env, io, ctx, q) << "\n";
try {
now_tactic().solve(env, io, ctx, q);
lean_unreachable();
} catch (tactic_exception & ex) {
std::cout << "expected error: " << ex.what() << "\n";
}
}
int main() {