From 3b40b09a3661b63a864712ea576213b88b27ea46 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 5 Dec 2015 13:25:20 -0800 Subject: [PATCH] refactor(library/blast): rename strategy to strategy_fn --- .../blast/backward/backward_strategy.cpp | 13 ++++++----- .../blast/backward/backward_strategy.h | 5 ++--- src/library/blast/blast.cpp | 2 +- .../blast/strategies/simple_strategy.cpp | 8 +++---- .../blast/strategies/simple_strategy.h | 4 ++-- src/library/blast/strategy.cpp | 22 ++++++++++++++----- src/library/blast/strategy.h | 17 +++++++++----- 7 files changed, 44 insertions(+), 27 deletions(-) diff --git a/src/library/blast/backward/backward_strategy.cpp b/src/library/blast/backward/backward_strategy.cpp index 9ce5e85a2..062a488c4 100644 --- a/src/library/blast/backward/backward_strategy.cpp +++ b/src/library/blast/backward/backward_strategy.cpp @@ -49,7 +49,7 @@ static backward_branch_extension & get_extension() { } /** \brief Basic backwards chaining, inspired by Coq's [auto]. */ -class backward_strategy : public strategy { +class backward_strategy_fn : public strategy_fn { virtual optional preprocess() override { return none_expr(); } virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override { @@ -75,10 +75,13 @@ class backward_strategy : public strategy { } }; -optional apply_backward_strategy() { +strategy mk_backward_strategy() { if (!get_config().m_backward) - return none_expr(); - flet disable_show_failure(get_config().m_show_failure, false); - return backward_strategy()(); + return []() { return none_expr(); }; + else + return []() { + flet disable_show_failure(get_config().m_show_failure, false); + return backward_strategy_fn()(); + }; } }} diff --git a/src/library/blast/backward/backward_strategy.h b/src/library/blast/backward/backward_strategy.h index 0085982c2..344cd339b 100644 --- a/src/library/blast/backward/backward_strategy.h +++ b/src/library/blast/backward/backward_strategy.h @@ -4,11 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Daniel Selsam */ #pragma once -#include "kernel/expr.h" - +#include "library/blast/strategy.h" namespace lean { namespace blast { -optional apply_backward_strategy(); +strategy mk_backward_strategy(); void initialize_backward_strategy(); void finalize_backward_strategy(); diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index 203606574..74e82efee 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -531,7 +531,7 @@ public: optional operator()(goal const & g) { init_state(g); - if (auto r = apply_simple_strategy()) { + if (auto r = mk_simple_strategy()()) { return some_expr(to_tactic_proof(*r)); } else { return none_expr(); diff --git a/src/library/blast/strategies/simple_strategy.cpp b/src/library/blast/strategies/simple_strategy.cpp index e7a8c630b..d68636b79 100644 --- a/src/library/blast/strategies/simple_strategy.cpp +++ b/src/library/blast/strategies/simple_strategy.cpp @@ -28,7 +28,7 @@ namespace lean { namespace blast { /** \brief Implement a simple proof strategy for blast. 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 { Try(assumption_contradiction_actions(hidx)); Try(simplify_hypothesis_action(hidx)); @@ -72,7 +72,7 @@ class simple_strategy : public strategy { Try(constructor_action()); Try(ematch_action()); Try(by_contradiction_action()); - TryStrategy(apply_backward_strategy()); + TryStrategy(mk_backward_strategy()); Try(qfc_action(list())); // TODO(Leo): add more actions... @@ -81,7 +81,7 @@ class simple_strategy : public strategy { } }; -optional apply_simple_strategy() { - return simple_strategy()(); +strategy mk_simple_strategy() { + return []() { return simple_strategy_fn()(); }; } }} diff --git a/src/library/blast/strategies/simple_strategy.h b/src/library/blast/strategies/simple_strategy.h index 274bb26f0..a2b2c1060 100644 --- a/src/library/blast/strategies/simple_strategy.h +++ b/src/library/blast/strategies/simple_strategy.h @@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/expr.h" +#include "library/blast/strategy.h" namespace lean { namespace blast { -optional apply_simple_strategy(); +strategy mk_simple_strategy(); }} diff --git a/src/library/blast/strategy.cpp b/src/library/blast/strategy.cpp index c62e8a5c0..535f23778 100644 --- a/src/library/blast/strategy.cpp +++ b/src/library/blast/strategy.cpp @@ -13,9 +13,9 @@ Author: Leonardo de Moura namespace lean { 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); auto hidx = curr_state().select_hypothesis_to_activate(); 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()) { proof_step s = curr_state().top_proof_step(); 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); } -optional strategy::search_upto(unsigned depth) { +optional strategy_fn::search_upto(unsigned depth) { if (is_trace_enabled()) { ios().get_diagnostic_channel() << "* Search upto depth " << depth << "\n\n"; } @@ -88,7 +88,7 @@ optional strategy::search_upto(unsigned depth) { } } -optional strategy::invoke_preprocess() { +optional strategy_fn::invoke_preprocess() { if (auto pr = preprocess()) { auto r = next_branch(*pr); if (!solved(r)) { @@ -101,7 +101,7 @@ optional strategy::invoke_preprocess() { } } -optional strategy::search() { +optional strategy_fn::init_search() { scope_choice_points scope1; curr_state().clear_proof_steps(); m_init_num_choices = get_num_choice_points(); @@ -109,6 +109,10 @@ optional strategy::search() { return pr; if (get_num_choice_points() > m_init_num_choices) throw exception("invalid blast preprocessing action, preprocessing actions should not create choice points"); + return none_expr(); +} + +optional strategy_fn::iterative_deepening() { state s = curr_state(); unsigned d = get_config().m_init_depth; while (true) { @@ -124,4 +128,10 @@ optional strategy::search() { shrink_choice_points(m_init_num_choices); } } + +optional strategy_fn::search() { + if (auto r = init_search()) + return r; + return iterative_deepening(); +} }} diff --git a/src/library/blast/strategy.h b/src/library/blast/strategy.h index 6136c16ad..f7a3a3723 100644 --- a/src/library/blast/strategy.h +++ b/src/library/blast/strategy.h @@ -18,27 +18,32 @@ namespace blast { 1- Preprocessing (preprocess method) 2- Next action to be performed (next_action method) */ -class strategy { +class strategy_fn { unsigned m_init_num_choices; optional invoke_preprocess(); protected: virtual optional preprocess() = 0; virtual action_result next_action() = 0; + virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) = 0; virtual action_result hypothesis_post_activation(hypothesis_idx hidx) = 0; - action_result activate_hypothesis(bool preprocess = false); + action_result next_branch(expr pr); optional search_upto(unsigned depth); - optional search(); + optional init_search(); + optional iterative_deepening(); + virtual optional search(); public: - strategy(); + strategy_fn(); optional operator()() { return search(); } }; -#define TryStrategy(Code) {\ +#define TryStrategy(S) {\ flet save_state(curr_state(), curr_state());\ curr_state().clear_proof_steps();\ - if (optional pf = Code) { return action_result::solved(*pf); }\ + if (optional pf = S()) { return action_result::solved(*pf); } \ } + +typedef std::function()> strategy; }}