From 52ec7e6d57f6ee10eb447d6d54dcac765ce06c02 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 1 Jan 2016 13:09:37 -0800 Subject: [PATCH] feat(library/blast/recursor): add 'blast.recursor.max_rounds' options and iterative deepening for recursor_strategy --- library/data/list/basic.lean | 12 +----- src/library/blast/recursor/init_module.cpp | 2 + .../blast/recursor/recursor_strategy.cpp | 39 ++++++++++++++++--- .../blast/recursor/recursor_strategy.h | 3 ++ 4 files changed, 41 insertions(+), 15 deletions(-) diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 494ff9eb70..a8a8867ee6 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -120,16 +120,8 @@ rfl theorem last_congr {l₁ l₂ : list T} (h₁ : l₁ ≠ []) (h₂ : l₂ ≠ []) (h₃ : l₁ = l₂) : last l₁ h₁ = last l₂ h₂ := by subst l₁ -theorem last_concat [simp] {x : T} : ∀ {l : list T} (h : concat x l ≠ []), last (concat x l) h = x -| [] h := rfl -| [a] h := rfl -| (a₁::a₂::l) h := - begin - change last (a₁::a₂::concat x l) !cons_ne_nil = x, - rewrite last_cons_cons, - change last (concat x (a₂::l)) !concat_ne_nil = x, - apply last_concat - end +theorem last_concat [simp] {x : T} : ∀ {l : list T} (h : concat x l ≠ []), last (concat x l) h = x := +by rec_simp -- add_rewrite append_nil append_cons diff --git a/src/library/blast/recursor/init_module.cpp b/src/library/blast/recursor/init_module.cpp index 820d96bc49..b5f8cb3e25 100644 --- a/src/library/blast/recursor/init_module.cpp +++ b/src/library/blast/recursor/init_module.cpp @@ -11,8 +11,10 @@ namespace lean { namespace blast { void initialize_recursor_module() { initialize_recursor_action(); + initialize_recursor_strategy(); } void finalize_recursor_module() { + finalize_recursor_strategy(); finalize_recursor_action(); } }} diff --git a/src/library/blast/recursor/recursor_strategy.cpp b/src/library/blast/recursor/recursor_strategy.cpp index 6ce6200694..2352462c51 100644 --- a/src/library/blast/recursor/recursor_strategy.cpp +++ b/src/library/blast/recursor/recursor_strategy.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/sexpr/option_declarations.h" #include "kernel/inductive/inductive.h" #include "library/user_recursors.h" #include "library/blast/blast.h" @@ -13,8 +14,28 @@ Author: Leonardo de Moura #include "library/blast/recursor/recursor_action.h" #include "library/blast/recursor/recursor_strategy.h" +#ifndef LEAN_DEFAULT_BLAST_RECURSION_MAX_ROUNDS +#define LEAN_DEFAULT_BLAST_RECURSION_MAX_ROUNDS 3 +#endif + namespace lean { namespace blast { +static name * g_blast_recursion_max_rounds = nullptr; + +unsigned get_blast_recursion_max_rounds(options const & o) { + return o.get_unsigned(*g_blast_recursion_max_rounds, LEAN_DEFAULT_BLAST_RECURSION_MAX_ROUNDS); +} + +void initialize_recursor_strategy() { + g_blast_recursion_max_rounds = new name{"blast", "recursion", "max_rounds"}; + register_unsigned_option(*blast::g_blast_recursion_max_rounds, LEAN_DEFAULT_BLAST_RECURSION_MAX_ROUNDS, + "(blast) maximum number of nested recursion/induction steps"); +} + +void finalize_recursor_strategy() { + delete g_blast_recursion_max_rounds; +} + static action_result try_hypothesis(hypothesis_idx hidx) { state & s = curr_state(); hypothesis const & h = s.get_hypothesis_decl(hidx); @@ -115,16 +136,24 @@ class rec_strategy_fn : public strategy_fn { } public: - rec_strategy_fn(strategy const & S, rec_candidate_selector const & sel): + rec_strategy_fn(strategy const & S, rec_candidate_selector const & sel, unsigned max_rounds): m_S(S), m_selector(sel), m_init_depth(curr_state().get_proof_depth()), - // TODO(Leo): use iterative deepening - // TODO(Leo): add option: max number of rounds (aka max depth) // TODO(Leo): add option: max number of steps - m_max_depth(m_init_depth + 1) {} + m_max_depth(m_init_depth + max_rounds) {} }; strategy rec_and_then(strategy const & S, rec_candidate_selector const & selector) { - return [=]() { return rec_strategy_fn(S, selector)(); }; // NOLINT + return [=]() { // NOLINT + state s = curr_state(); + unsigned max_rounds = get_blast_recursion_max_rounds(ios().get_options()); + for (unsigned i = 1; i <= max_rounds; i++) { + lean_trace_search(tout() << "starting recursor strategy with max #" << i << " round(s)\n";); + curr_state() = s; + if (auto pr = rec_strategy_fn(S, selector, i)()) + return pr; + } + return none_expr(); + }; } static void default_selector(hypothesis_idx_buffer & r) { diff --git a/src/library/blast/recursor/recursor_strategy.h b/src/library/blast/recursor/recursor_strategy.h index ed8c403a5e..d2568e50ee 100644 --- a/src/library/blast/recursor/recursor_strategy.h +++ b/src/library/blast/recursor/recursor_strategy.h @@ -46,4 +46,7 @@ strategy rec_and_then(strategy const & S, rec_candidate_selector const & selecto /* Use default selector */ strategy rec_and_then(strategy const & S); + +void initialize_recursor_strategy(); +void finalize_recursor_strategy(); }}