refactor(library/blast): rename strategy to strategy_fn

This commit is contained in:
Leonardo de Moura 2015-12-05 13:25:20 -08:00
parent 7a117c45bf
commit 3b40b09a36
7 changed files with 44 additions and 27 deletions

View file

@ -49,7 +49,7 @@ static backward_branch_extension & get_extension() {
} }
/** \brief Basic backwards chaining, inspired by Coq's [auto]. */ /** \brief Basic backwards chaining, inspired by Coq's [auto]. */
class backward_strategy : public strategy { class backward_strategy_fn : public strategy_fn {
virtual optional<expr> preprocess() override { return none_expr(); } virtual optional<expr> preprocess() override { return none_expr(); }
virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override { virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override {
@ -75,10 +75,13 @@ class backward_strategy : public strategy {
} }
}; };
optional<expr> apply_backward_strategy() { strategy mk_backward_strategy() {
if (!get_config().m_backward) if (!get_config().m_backward)
return none_expr(); return []() { return none_expr(); };
flet<bool> disable_show_failure(get_config().m_show_failure, false); else
return backward_strategy()(); return []() {
flet<bool> disable_show_failure(get_config().m_show_failure, false);
return backward_strategy_fn()();
};
} }
}} }}

View file

@ -4,11 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Daniel Selsam Author: Daniel Selsam
*/ */
#pragma once #pragma once
#include "kernel/expr.h" #include "library/blast/strategy.h"
namespace lean { namespace lean {
namespace blast { namespace blast {
optional<expr> apply_backward_strategy(); strategy mk_backward_strategy();
void initialize_backward_strategy(); void initialize_backward_strategy();
void finalize_backward_strategy(); void finalize_backward_strategy();

View file

@ -531,7 +531,7 @@ public:
optional<expr> operator()(goal const & g) { optional<expr> operator()(goal const & g) {
init_state(g); init_state(g);
if (auto r = apply_simple_strategy()) { if (auto r = mk_simple_strategy()()) {
return some_expr(to_tactic_proof(*r)); return some_expr(to_tactic_proof(*r));
} else { } else {
return none_expr(); return none_expr();

View file

@ -28,7 +28,7 @@ namespace lean {
namespace blast { namespace blast {
/** \brief Implement a simple proof strategy for blast. /** \brief Implement a simple proof strategy for blast.
We use it mainly for testing new actions and the whole blast infra-structure. */ We use it mainly for testing new actions and the whole blast infra-structure. */
class simple_strategy : public strategy { class simple_strategy_fn : public strategy_fn {
action_result hypothesis_pre_activation(hypothesis_idx hidx) override { action_result hypothesis_pre_activation(hypothesis_idx hidx) override {
Try(assumption_contradiction_actions(hidx)); Try(assumption_contradiction_actions(hidx));
Try(simplify_hypothesis_action(hidx)); Try(simplify_hypothesis_action(hidx));
@ -72,7 +72,7 @@ class simple_strategy : public strategy {
Try(constructor_action()); Try(constructor_action());
Try(ematch_action()); Try(ematch_action());
Try(by_contradiction_action()); Try(by_contradiction_action());
TryStrategy(apply_backward_strategy()); TryStrategy(mk_backward_strategy());
Try(qfc_action(list<gexpr>())); Try(qfc_action(list<gexpr>()));
// TODO(Leo): add more actions... // TODO(Leo): add more actions...
@ -81,7 +81,7 @@ class simple_strategy : public strategy {
} }
}; };
optional<expr> apply_simple_strategy() { strategy mk_simple_strategy() {
return simple_strategy()(); return []() { return simple_strategy_fn()(); };
} }
}} }}

View file

@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura Author: Leonardo de Moura
*/ */
#pragma once #pragma once
#include "kernel/expr.h" #include "library/blast/strategy.h"
namespace lean { namespace lean {
namespace blast { namespace blast {
optional<expr> apply_simple_strategy(); strategy mk_simple_strategy();
}} }}

View file

@ -13,9 +13,9 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
namespace blast { namespace blast {
strategy::strategy() {} strategy_fn::strategy_fn() {}
action_result strategy::activate_hypothesis(bool preprocess) { action_result strategy_fn::activate_hypothesis(bool preprocess) {
scope_trace scope(!preprocess && get_config().m_trace); scope_trace scope(!preprocess && get_config().m_trace);
auto hidx = curr_state().select_hypothesis_to_activate(); auto hidx = curr_state().select_hypothesis_to_activate();
if (!hidx) return action_result::failed(); if (!hidx) return action_result::failed();
@ -28,7 +28,7 @@ action_result strategy::activate_hypothesis(bool preprocess) {
} }
} }
action_result strategy::next_branch(expr pr) { action_result strategy_fn::next_branch(expr pr) {
while (curr_state().has_proof_steps()) { while (curr_state().has_proof_steps()) {
proof_step s = curr_state().top_proof_step(); proof_step s = curr_state().top_proof_step();
action_result r = s.resolve(unfold_hypotheses_ge(curr_state(), pr)); action_result r = s.resolve(unfold_hypotheses_ge(curr_state(), pr));
@ -47,7 +47,7 @@ action_result strategy::next_branch(expr pr) {
return action_result::solved(pr); return action_result::solved(pr);
} }
optional<expr> strategy::search_upto(unsigned depth) { optional<expr> strategy_fn::search_upto(unsigned depth) {
if (is_trace_enabled()) { if (is_trace_enabled()) {
ios().get_diagnostic_channel() << "* Search upto depth " << depth << "\n\n"; ios().get_diagnostic_channel() << "* Search upto depth " << depth << "\n\n";
} }
@ -88,7 +88,7 @@ optional<expr> strategy::search_upto(unsigned depth) {
} }
} }
optional<expr> strategy::invoke_preprocess() { optional<expr> strategy_fn::invoke_preprocess() {
if (auto pr = preprocess()) { if (auto pr = preprocess()) {
auto r = next_branch(*pr); auto r = next_branch(*pr);
if (!solved(r)) { if (!solved(r)) {
@ -101,7 +101,7 @@ optional<expr> strategy::invoke_preprocess() {
} }
} }
optional<expr> strategy::search() { optional<expr> strategy_fn::init_search() {
scope_choice_points scope1; scope_choice_points scope1;
curr_state().clear_proof_steps(); curr_state().clear_proof_steps();
m_init_num_choices = get_num_choice_points(); m_init_num_choices = get_num_choice_points();
@ -109,6 +109,10 @@ optional<expr> strategy::search() {
return pr; return pr;
if (get_num_choice_points() > m_init_num_choices) if (get_num_choice_points() > m_init_num_choices)
throw exception("invalid blast preprocessing action, preprocessing actions should not create choice points"); throw exception("invalid blast preprocessing action, preprocessing actions should not create choice points");
return none_expr();
}
optional<expr> strategy_fn::iterative_deepening() {
state s = curr_state(); state s = curr_state();
unsigned d = get_config().m_init_depth; unsigned d = get_config().m_init_depth;
while (true) { while (true) {
@ -124,4 +128,10 @@ optional<expr> strategy::search() {
shrink_choice_points(m_init_num_choices); shrink_choice_points(m_init_num_choices);
} }
} }
optional<expr> strategy_fn::search() {
if (auto r = init_search())
return r;
return iterative_deepening();
}
}} }}

View file

@ -18,27 +18,32 @@ namespace blast {
1- Preprocessing (preprocess method) 1- Preprocessing (preprocess method)
2- Next action to be performed (next_action method) 2- Next action to be performed (next_action method)
*/ */
class strategy { class strategy_fn {
unsigned m_init_num_choices; unsigned m_init_num_choices;
optional<expr> invoke_preprocess(); optional<expr> invoke_preprocess();
protected: protected:
virtual optional<expr> preprocess() = 0; virtual optional<expr> preprocess() = 0;
virtual action_result next_action() = 0; virtual action_result next_action() = 0;
virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) = 0; virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) = 0;
virtual action_result hypothesis_post_activation(hypothesis_idx hidx) = 0; virtual action_result hypothesis_post_activation(hypothesis_idx hidx) = 0;
action_result activate_hypothesis(bool preprocess = false); action_result activate_hypothesis(bool preprocess = false);
action_result next_branch(expr pr); action_result next_branch(expr pr);
optional<expr> search_upto(unsigned depth); optional<expr> search_upto(unsigned depth);
optional<expr> search(); optional<expr> init_search();
optional<expr> iterative_deepening();
virtual optional<expr> search();
public: public:
strategy(); strategy_fn();
optional<expr> operator()() { return search(); } optional<expr> operator()() { return search(); }
}; };
#define TryStrategy(Code) {\ #define TryStrategy(S) {\
flet<state> save_state(curr_state(), curr_state());\ flet<state> save_state(curr_state(), curr_state());\
curr_state().clear_proof_steps();\ curr_state().clear_proof_steps();\
if (optional<expr> pf = Code) { return action_result::solved(*pf); }\ if (optional<expr> pf = S()) { return action_result::solved(*pf); } \
} }
typedef std::function<optional<expr>()> strategy;
}} }}