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

feat(library/blast/recursor/recursor_strategy): add new options to control recursor/recursion strategy

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-06 17:30:38 -08:00
parent 4e8ae94aba
commit 3c22a9d4e1
1 changed files with 31 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/library/blast/recursor/recursor_strategy.cpp
View file

@ -18,22 +18,48 @@ Author: Leonardo de Moura
#define LEAN_DEFAULT_BLAST_RECURSION_MAX_ROUNDS 3 #define LEAN_DEFAULT_BLAST_RECURSION_MAX_ROUNDS 3
#endif #endif
#ifndef LEAN_DEFAULT_BLAST_RECURSION_STRUCTURE
#define LEAN_DEFAULT_BLAST_RECURSION_STRUCTURE false
#endif
#ifndef LEAN_DEFAULT_BLAST_RECURSION_CLASS
#define LEAN_DEFAULT_BLAST_RECURSION_CLASS false
#endif
namespace lean { namespace lean {
namespace blast { namespace blast {
static name * g_blast_recursion_max_rounds = nullptr; static name * g_blast_recursion_max_rounds = nullptr;
static name * g_blast_recursion_structure = nullptr;
static name * g_blast_recursion_class = nullptr;
unsigned get_blast_recursion_max_rounds(options const & o) { unsigned get_blast_recursion_max_rounds(options const & o) {
return o.get_unsigned(*g_blast_recursion_max_rounds, LEAN_DEFAULT_BLAST_RECURSION_MAX_ROUNDS); return o.get_unsigned(*g_blast_recursion_max_rounds, LEAN_DEFAULT_BLAST_RECURSION_MAX_ROUNDS);
} }
bool get_blast_recursion_structure(options const & o) {
return o.get_bool(*g_blast_recursion_structure, LEAN_DEFAULT_BLAST_RECURSION_STRUCTURE);
}
bool get_blast_recursion_class(options const & o) {
return o.get_bool(*g_blast_recursion_class, LEAN_DEFAULT_BLAST_RECURSION_CLASS);
}
void initialize_recursor_strategy() { void initialize_recursor_strategy() {
g_blast_recursion_max_rounds = new name{"blast", "recursion", "max_rounds"}; g_blast_recursion_max_rounds = new name{"blast", "recursion", "max_rounds"};
g_blast_recursion_structure = new name{"blast", "recursion", "structure"};
g_blast_recursion_class = new name{"blast", "recursion", "class"};
register_unsigned_option(*blast::g_blast_recursion_max_rounds, LEAN_DEFAULT_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"); "(blast) maximum number of nested recursion/induction steps");
register_bool_option(*blast::g_blast_recursion_structure, LEAN_DEFAULT_BLAST_RECURSION_STRUCTURE,
"(blast) if true recursion strategy also considers inductive types with only one constructor");
register_bool_option(*blast::g_blast_recursion_class, LEAN_DEFAULT_BLAST_RECURSION_CLASS,
"(blast) if true recursion strategy also considers inductive types that are marked as type classes");
} }
void finalize_recursor_strategy() { void finalize_recursor_strategy() {
delete g_blast_recursion_max_rounds; delete g_blast_recursion_max_rounds;
delete g_blast_recursion_structure;
delete g_blast_recursion_class;
} }
static action_result try_hypothesis(hypothesis_idx hidx) { static action_result try_hypothesis(hypothesis_idx hidx) {
@ -159,6 +185,8 @@ strategy rec_and_then(strategy const & S, rec_candidate_selector const & selecto
static void default_selector(hypothesis_idx_buffer & r) { static void default_selector(hypothesis_idx_buffer & r) {
// TODO(Leo): add options to control selection // TODO(Leo): add options to control selection
state & s = curr_state(); state & s = curr_state();
bool classes = get_blast_recursion_class(ios().get_options());
bool structures = get_blast_recursion_structure(ios().get_options());
s.for_each_hypothesis([&](hypothesis_idx hidx, hypothesis const & h) { s.for_each_hypothesis([&](hypothesis_idx hidx, hypothesis const & h) {
expr const & type = h.get_type(); expr const & type = h.get_type();
if (!is_app(type) && !is_constant(type)) if (!is_app(type) && !is_constant(type))
@ -167,13 +195,13 @@ static void default_selector(hypothesis_idx_buffer & r) {
return; return;
if (is_relation_app(type)) if (is_relation_app(type))
return; // we don't apply recursors to equivalence relations: =, ~, <->, etc. return; // we don't apply recursors to equivalence relations: =, ~, <->, etc.
if (get_type_context().is_class(type)) if (!classes && get_type_context().is_class(type))
return; // ignore type classes return; // ignore type classes
expr const & I = get_app_fn(type); expr const & I = get_app_fn(type);
if (!is_constant(I)) if (!is_constant(I))
return; return;
name const & I_name = const_name(I); name const & I_name = const_name(I);
if (inductive::is_inductive_decl(env(), I_name) && *inductive::get_num_intro_rules(env(), I_name) > 1) { if (inductive::is_inductive_decl(env(), I_name) && (structures || *inductive::get_num_intro_rules(env(), I_name) > 1)) {
// builtin recursive datatype with more than one constructor // builtin recursive datatype with more than one constructor
r.push_back(hidx); r.push_back(hidx);
return; return;