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

refactor(library/blast/simplifier): move simplifier module into blast

Browse source
This commit is contained in:
Daniel Selsam 2015-11-19 15:30:38 -08:00 committed by Leonardo de Moura
parent 2c72f46adc
commit 21cb409e6c
29 changed files with 86 additions and 631 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/CMakeLists.txt
View file

@ -341,8 +341,6 @@ add_subdirectory(kernel/hits)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:hits>)
add_subdirectory(library)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:library>)
add_subdirectory(library/simplifier)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:simplifier>)
add_subdirectory(library/tactic)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:tactic>)
add_subdirectory(library/definitional)
@ -353,6 +351,8 @@ add_subdirectory(library/blast/backward)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:backward>)
add_subdirectory(library/blast/forward)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:forward>)
add_subdirectory(library/blast/simplifier)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:simplifier>)
add_subdirectory(library/error_handling)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:error_handling>)
add_subdirectory(compiler)

2
src/frontends/lean/CMakeLists.txt
View file

@ -10,4 +10,4 @@ init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp
parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp
type_util.cpp elaborator_exception.cpp migrate_cmd.cpp local_ref_info.cpp
obtain_expr.cpp decl_attributes.cpp nested_declaration.cpp
parse_with_options_tactic.cpp parse_simp_tactic.cpp opt_cmd.cpp prenum.cpp)
parse_with_options_tactic.cpp opt_cmd.cpp prenum.cpp)

4
src/frontends/lean/builtin_cmds.cpp
View file

@ -45,9 +45,9 @@ Author: Leonardo de Moura
#include "library/congr_lemma_manager.h"
#include "library/abstract_expr_manager.h"
#include "library/definitional/projection.h"
#include "library/simplifier/simp_rule_set.h"
#include "library/blast/simplifier/simp_rule_set.h"
#include "library/blast/blast.h"
#include "library/blast/simplifier.h"
#include "library/blast/simplifier/simplifier.h"
#include "library/blast/backward/backward_rule_set.h"
#include "compiler/preprocess_rec.h"
#include "frontends/lean/util.h"

6
src/frontends/lean/builtin_tactics.cpp
View file

@ -10,7 +10,6 @@ Author: Leonardo de Moura
#include "frontends/lean/parser.h"
#include "frontends/lean/parse_rewrite_tactic.h"
#include "frontends/lean/parse_with_options_tactic.h"
#include "frontends/lean/parse_simp_tactic.h"
namespace lean {
namespace notation {
@ -53,10 +52,6 @@ static expr parse_with_options_tactic_expr(parser & p, unsigned, expr const *, p
return p.save_pos(parse_with_options_tactic(p), pos);
}
static expr parse_simp_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
return p.save_pos(parse_simp_tactic(p), pos);
}
static expr parse_generalize_tactic(parser & p, unsigned, expr const *, pos_info const & pos) {
expr e = p.parse_tactic_expr_arg();
name id;
@ -88,7 +83,6 @@ parse_table init_tactic_nud_table() {
r = r.add({transition("fold", mk_ext_action(parse_fold_tactic_expr))}, x0);
r = r.add({transition("let", mk_ext_action(parse_let_tactic))}, x0);
r = r.add({transition("with_options", mk_ext_action(parse_with_options_tactic_expr))}, x0);
r = r.add({transition("simp", mk_ext_action(parse_simp_tactic_expr))}, x0);
return r;
}

2
src/frontends/lean/decl_attributes.cpp
View file

@ -11,7 +11,7 @@ Author: Leonardo de Moura
#include "library/relation_manager.h"
#include "library/user_recursors.h"
#include "library/coercion.h"
#include "library/simplifier/simp_rule_set.h"
#include "library/blast/simplifier/simp_rule_set.h"
#include "library/blast/backward/backward_rule_set.h"
#include "frontends/lean/decl_attributes.h"
#include "frontends/lean/parser.h"

75
src/frontends/lean/parse_simp_tactic.cpp
View file

@ -1,75 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/sstream.h"
#include "library/scoped_ext.h"
#include "library/tactic/exact_tactic.h"
#include "library/tactic/expr_to_tactic.h"
#include "library/simplifier/simp_rule_set.h"
#include "library/simplifier/simp_tactic.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/parse_tactic_location.h"
#include "frontends/lean/tokens.h"
namespace lean {
expr parse_simp_tactic(parser & p) {
buffer<expr> lemmas;
buffer<name> ns;
buffer<name> hiding;
optional<expr> tac;
while (true) {
if (p.curr_is_token(get_lbracket_tk())) {
p.next();
while (true) {
if (p.curr_is_identifier()) {
auto id_pos = p.pos();
name id = p.get_name_val();
p.next();
optional<name> real_ns = to_valid_namespace_name(p.env(), id);
if (real_ns) {
ns.push_back(*real_ns);
} else {
expr left = p.id_to_expr(id, id_pos);
unsigned rbp = 0;
while (rbp < p.curr_expr_lbp()) {
left = p.parse_led(left);
}
lemmas.push_back(left);
}
} else {
lemmas.push_back(p.parse_expr());
}
if (!p.curr_is_token(get_comma_tk()))
break;
p.next();
}
p.check_token_next(get_rbracket_tk(), "invalid 'simp' tactic, ']' expected");
} else if (p.curr_is_token_or_id(get_hiding_tk())) {
p.next();
p.check_token_next(get_lbracket_tk(), "invalid 'simp' tactic, '[' expected");
while (true) {
name id = p.check_constant_next("invalid 'simp' tactic, constant expected");
hiding.push_back(id);
if (!p.curr_is_token(get_comma_tk()))
break;
p.next();
}
p.check_token_next(get_rbracket_tk(), "invalid 'simp' tactic, ']' expected");
} else if (p.curr_is_token_or_id(get_using_tk())) {
if (tac)
throw parser_error("invalid 'simp' tactic, auxiliary tactic was already specified", p.pos());
p.next();
tac = p.parse_tactic(get_max_prec());
} else {
break;
}
}
location loc = parse_tactic_location(p);
// Remark: simp_tac is the actual result
return mk_simp_tactic_expr(lemmas, ns, hiding, tac, loc);
}
}

13
src/frontends/lean/parse_simp_tactic.h
View file

@ -1,13 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/expr.h"
namespace lean {
class parser;
expr parse_simp_tactic(parser & p);
}

3
src/init/init.cpp
View file

@ -14,7 +14,6 @@ Author: Leonardo de Moura
#include "kernel/quotient/quotient.h"
#include "kernel/hits/hits.h"
#include "library/init_module.h"
#include "library/simplifier/init_module.h"
#include "library/blast/init_module.h"
#include "library/tactic/init_module.h"
#include "library/definitional/init_module.h"
@ -37,7 +36,6 @@ void initialize() {
init_default_print_fn();
initialize_library_module();
initialize_tactic_module();
initialize_simplifier_module();
initialize_blast_module();
initialize_definitional_module();
initialize_compiler_module();
@ -50,7 +48,6 @@ void finalize() {
finalize_compiler_module();
finalize_definitional_module();
finalize_blast_module();
finalize_simplifier_module();
finalize_tactic_module();
finalize_library_module();
finalize_hits_module();

4
src/library/blast/CMakeLists.txt
View file

@ -1,6 +1,6 @@
add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp
init_module.cpp simplifier.cpp simple_actions.cpp intros_action.cpp proof_expr.cpp
init_module.cpp simple_actions.cpp intros_action.cpp proof_expr.cpp
options.cpp choice_point.cpp simple_strategy.cpp util.cpp
gexpr.cpp revert.cpp subst_action.cpp no_confusion_action.cpp
simplify_actions.cpp strategy.cpp recursor_action.cpp congruence_closure.cpp
strategy.cpp recursor_action.cpp congruence_closure.cpp
trace.cpp assert_cc_action.cpp)

2
src/library/blast/congruence_closure.cpp
View file

@ -6,7 +6,7 @@ Author: Leonardo de Moura
*/
#include <vector>
#include "library/constants.h"
#include "library/simplifier/simp_rule_set.h"
#include "library/blast/simplifier/simp_rule_set.h"
#include "library/blast/congruence_closure.h"
#include "library/blast/util.h"
#include "library/blast/blast.h"

6
src/library/blast/init_module.cpp
View file

@ -8,11 +8,11 @@ Author: Leonardo de Moura
#include "library/blast/state.h"
#include "library/blast/blast.h"
#include "library/blast/blast_tactic.h"
#include "library/blast/simplifier.h"
#include "library/blast/options.h"
#include "library/blast/congruence_closure.h"
#include "library/blast/recursor_action.h"
#include "library/blast/assert_cc_action.h"
#include "library/blast/simplifier/init_module.h"
#include "library/blast/backward/init_module.h"
#include "library/blast/forward/init_module.h"
@ -22,7 +22,7 @@ void initialize_blast_module() {
blast::initialize_expr();
blast::initialize_state();
initialize_blast();
blast::initialize_simplifier();
blast::initialize_simplifier_module();
blast::initialize_backward_module();
blast::initialize_forward_module();
initialize_blast_tactic();
@ -37,7 +37,7 @@ void finalize_blast_module() {
finalize_blast_tactic();
blast::finalize_forward_module();
blast::finalize_backward_module();
blast::finalize_simplifier();
blast::finalize_simplifier_module();
finalize_blast();
blast::finalize_state();
blast::finalize_expr();

6
src/library/blast/simple_strategy.cpp
View file

@ -15,7 +15,7 @@ Author: Leonardo de Moura
#include "library/blast/backward/backward_strategy.h"
#include "library/blast/forward/forward_action.h"
#include "library/blast/no_confusion_action.h"
#include "library/blast/simplify_actions.h"
#include "library/blast/simplifier/simplifier_actions.h"
#include "library/blast/recursor_action.h"
#include "library/blast/assert_cc_action.h"
#include "library/blast/strategy.h"
@ -48,10 +48,6 @@ class simple_strategy : public strategy {
Return an expression if the goal has been proved during preprocessing step. */
virtual optional<expr> preprocess() {
trace("* Preprocess");
// TODO(dhs): make a branch extension
curr_state().set_simp_rule_sets(get_simp_rule_sets(env()));
while (true) {
if (!failed(intros_action()))
continue;

1
src/library/blast/simplifier/CMakeLists.txt Normal file
View file

@ -0,0 +1 @@
add_library(simplifier OBJECT init_module.cpp simp_rule_set.cpp ceqv.cpp simplifier.cpp simplifier_actions.cpp)

2
src/library/simplifier/ceqv.cpp → src/library/blast/simplifier/ceqv.cpp
View file

@ -11,7 +11,7 @@ Author: Leonardo de Moura
#include "library/util.h"
#include "library/relation_manager.h"
#include "library/occurs.h"
#include "library/simplifier/ceqv.h"
#include "library/blast/simplifier/ceqv.h"
namespace lean {
bool is_ceqv(tmp_type_context & tctx, expr e);

0
src/library/simplifier/ceqv.h → src/library/blast/simplifier/ceqv.h
View file

24
src/library/blast/simplifier/init_module.cpp Normal file
View file

@ -0,0 +1,24 @@
/*
Copyright (c) 2015 Daniel Selsam. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Daniel Selsam
*/
#include "library/blast/simplifier/simplifier_actions.h"
#include "library/blast/simplifier/simp_rule_set.h"
#include "library/blast/simplifier/simplifier.h"
namespace lean {
namespace blast {
void initialize_simplifier_module() {
initialize_simplifier();
initialize_simplifier_rule_set();
initialize_simplifier_actions();
}
void finalize_simplifier_module() {
finalize_simplifier_actions();
finalize_simplifier_rule_set();
finalize_simplifier();
}
}}

7
src/library/simplifier/init_module.h → src/library/blast/simplifier/init_module.h
View file

@ -1,12 +1,13 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Copyright (c) 2015 Daniel Selsam. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
Author: Daniel Selsam
*/
#pragma once
namespace lean {
namespace blast {
void initialize_simplifier_module();
void finalize_simplifier_module();
}
}

8
src/library/simplifier/simp_rule_set.cpp → src/library/blast/simplifier/simp_rule_set.cpp
View file

@ -12,8 +12,8 @@ Author: Leonardo de Moura
#include "library/scoped_ext.h"
#include "library/expr_pair.h"
#include "library/relation_manager.h"
#include "library/simplifier/ceqv.h"
#include "library/simplifier/simp_rule_set.h"
#include "library/blast/simplifier/ceqv.h"
#include "library/blast/simplifier/simp_rule_set.h"
#include <vector>
namespace lean {
@ -562,14 +562,14 @@ io_state_stream const & operator<<(io_state_stream const & out, simp_rule_sets c
return out;
}
void initialize_simp_rule_set() {
void initialize_simplifier_rule_set() {
g_prefix = new name(name::mk_internal_unique_name());
g_class_name = new name("rrs");
g_key = new std::string("rrs");
rrs_ext::initialize();
}
void finalize_simp_rule_set() {
void finalize_simplifier_rule_set() {
rrs_ext::finalize();
delete g_key;
delete g_class_name;

4
src/library/simplifier/simp_rule_set.h → src/library/blast/simplifier/simp_rule_set.h
View file

@ -149,6 +149,6 @@ simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios,
io_state_stream const & operator<<(io_state_stream const & out, simp_rule_sets const & s);
void initialize_simp_rule_set();
void finalize_simp_rule_set();
void initialize_simplifier_rule_set();
void finalize_simplifier_rule_set();
}

6
src/library/blast/simplifier.cpp → src/library/blast/simplifier/simplifier.cpp
View file

@ -13,9 +13,9 @@
#include "library/blast/expr.h"
#include "library/blast/blast_exception.h"
#include "library/blast/blast.h"
#include "library/blast/simplifier.h"
#include "library/simplifier/simp_rule_set.h"
#include "library/simplifier/ceqv.h"
#include "library/blast/simplifier/simplifier.h"
#include "library/blast/simplifier/simp_rule_set.h"
#include "library/blast/simplifier/ceqv.h"
#include "library/app_builder.h"
#include "library/num.h"
#include "library/norm_num.h"

2
src/library/blast/simplifier.h → src/library/blast/simplifier/simplifier.h
View file

@ -6,7 +6,7 @@ Author: Daniel Selsam
#pragma once
#include "kernel/expr_pair.h"
#include "library/blast/state.h"
#include "library/simplifier/simp_rule_set.h"
#include "library/blast/simplifier/simp_rule_set.h"
namespace lean {
namespace blast {

29
src/library/blast/simplify_actions.cpp → src/library/blast/simplifier/simplifier_actions.cpp
View file

@ -7,11 +7,36 @@ Author: Leonardo de Moura
#include "library/constants.h"
#include "library/blast/simple_actions.h"
#include "library/blast/blast.h"
#include "library/blast/simplifier.h"
#include "library/blast/trace.h"
#include "library/blast/simplifier/simplifier.h"
namespace lean {
namespace blast {
static unsigned g_ext_id = 0;
struct simplifier_branch_extension : public branch_extension {
simp_rule_sets m_srss;
simplifier_branch_extension() {}
simplifier_branch_extension(simplifier_branch_extension const & b):
m_srss(b.m_srss) {}
virtual ~simplifier_branch_extension() {}
virtual branch_extension * clone() override { return new simplifier_branch_extension(*this); }
virtual void initialized() override { m_srss = ::lean::get_simp_rule_sets(env()); }
virtual void hypothesis_activated(hypothesis const & h, hypothesis_idx hidx) override { }
virtual void hypothesis_deleted(hypothesis const & h, hypothesis_idx) override { }
simp_rule_sets const & get_simp_rule_sets() const { return m_srss; }
};
void initialize_simplifier_actions() {
g_ext_id = register_branch_extension(new simplifier_branch_extension());
}
void finalize_simplifier_actions() {
}
static simplifier_branch_extension & get_extension() {
return static_cast<simplifier_branch_extension&>(curr_state().get_extension(g_ext_id));
}
static bool use_iff(expr const & target) {
return is_standard(env()) && is_prop(target);
}
@ -43,7 +68,7 @@ action_result simplify_target_action() {
expr target = s.get_target();
bool iff = use_iff(target);
name rname = iff ? get_iff_name() : get_eq_name();
auto r = simplify(rname, target, s.get_simp_rule_sets());
auto r = simplify(rname, target, get_extension().get_simp_rule_sets());
if (!r.has_proof())
return action_result::failed(); // did nothing
s.push_proof_step(new simplify_target_proof_step_cell(iff, r.get_proof()));

4
src/library/blast/simplify_actions.h → src/library/blast/simplifier/simplifier_actions.h
View file

@ -6,9 +6,13 @@ Author: Leonardo de Moura
*/
#pragma once
#include "library/blast/hypothesis.h"
#include "library/blast/action_result.h"
namespace lean {
namespace blast {
optional<hypothesis_idx> simplify_hypothesis_action(hypothesis_idx hidx);
bool add_simp_rule_action(hypothesis_idx hidx);
action_result simplify_target_action();
void initialize_simplifier_actions();
void finalize_simplifier_actions();
}}

7
src/library/blast/state.cpp
View file

@ -94,8 +94,7 @@ branch::branch(branch const & b):
m_head_to_hyps(b.m_head_to_hyps),
m_forward_deps(b.m_forward_deps),
m_target(b.m_target),
m_target_deps(b.m_target_deps),
m_simp_rule_sets(b.m_simp_rule_sets) {
m_target_deps(b.m_target_deps) {
unsigned n = get_extension_manager().get_num_extensions();
m_extensions = new branch_extension*[n];
for (unsigned i = 0; i < n; i++) {
@ -113,8 +112,7 @@ branch::branch(branch && b):
m_head_to_hyps(std::move(b.m_head_to_hyps)),
m_forward_deps(std::move(b.m_forward_deps)),
m_target(std::move(b.m_target)),
m_target_deps(std::move(b.m_target_deps)),
m_simp_rule_sets(std::move(b.m_simp_rule_sets)) {
m_target_deps(std::move(b.m_target_deps)) {
unsigned n = get_extension_manager().get_num_extensions();
m_extensions = new branch_extension*[n];
for (unsigned i = 0; i < n; i++) {
@ -132,7 +130,6 @@ void branch::swap(branch & b) {
std::swap(m_forward_deps, b.m_forward_deps);
std::swap(m_target, b.m_target);
std::swap(m_target_deps, b.m_target_deps);
std::swap(m_simp_rule_sets, b.m_simp_rule_sets);
std::swap(m_extensions, b.m_extensions);
}

13
src/library/blast/state.h
View file

@ -9,8 +9,6 @@ Author: Leonardo de Moura
#include "kernel/expr.h"
#include "library/head_map.h"
#include "library/tactic/goal.h"
#include "library/simplifier/simp_rule_set.h"
#include "library/blast/backward/backward_rule_set.h"
#include "library/blast/action_result.h"
#include "library/blast/hypothesis.h"
@ -155,7 +153,6 @@ class branch {
forward_deps m_forward_deps; // given an entry (h -> {h_1, ..., h_n}), we have that each h_i uses h.
expr m_target;
hypothesis_idx_set m_target_deps;
simp_rule_sets m_simp_rule_sets;
branch_extension ** m_extensions;
public:
branch();
@ -445,16 +442,6 @@ public:
assignment_snapshot save_assignment();
void restore_assignment(assignment_snapshot const & s);
/************************
Simplification rules
*************************/
void set_simp_rule_sets(simp_rule_sets const & s) {
m_branch.m_simp_rule_sets = s;
}
simp_rule_sets get_simp_rule_sets() const {
return m_branch.m_simp_rule_sets;
}
/************************
Branch extensions
*************************/

1
src/library/simplifier/CMakeLists.txt
View file

@ -1 +0,0 @@
add_library(simplifier OBJECT ceqv.cpp simp_rule_set.cpp init_module.cpp simp_tactic.cpp)

19
src/library/simplifier/init_module.cpp
View file

@ -1,19 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/simplifier/simp_rule_set.h"
#include "library/simplifier/simp_tactic.h"
namespace lean {
void initialize_simplifier_module() {
initialize_simp_rule_set();
initialize_simp_tactic();
}
void finalize_simplifier_module() {
finalize_simp_tactic();
finalize_simp_rule_set();
}
}

439
src/library/simplifier/simp_tactic.cpp
View file

@ -1,439 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/sexpr/option_declarations.h"
#include "kernel/instantiate.h"
#include "library/constants.h"
#include "library/util.h"
#include "library/relation_manager.h"
#include "library/tactic/expr_to_tactic.h"
#include "library/simplifier/ceqv.h"
#include "library/simplifier/simp_tactic.h"
#include "library/simplifier/simp_rule_set.h"
#ifndef LEAN_DEFAULT_SIMP_SINGLE_PASS
#define LEAN_DEFAULT_SIMP_SINGLE_PASS false
#endif
#ifndef LEAN_DEFAULT_SIMP_BOTTOM_UP
#define LEAN_DEFAULT_SIMP_BOTTOM_UP true
#endif
#ifndef LEAN_DEFAULT_SIMP_BETA_ETA
#define LEAN_DEFAULT_SIMP_BETA_ETA true
#endif
#ifndef LEAN_DEFAULT_SIMP_IOTA
#define LEAN_DEFAULT_SIMP_IOTA true
#endif
#ifndef LEAN_DEFAULT_SIMP_MEMOIZE
#define LEAN_DEFAULT_SIMP_MEMOIZE true
#endif
#ifndef LEAN_DEFAULT_SIMP_MAX_STEPS
#define LEAN_DEFAULT_SIMP_MAX_STEPS 10000
#endif
#ifndef LEAN_DEFAULT_SIMP_TRACE
#define LEAN_DEFAULT_SIMP_TRACE false
#endif
#ifndef LEAN_DEFAULT_SIMP_ASSUMPTIONS
#define LEAN_DEFAULT_SIMP_ASSUMPTIONS false
#endif
#ifndef LEAN_DEFAULT_SIMP_FUNEXT
#define LEAN_DEFAULT_SIMP_FUNEXT true
#endif
#ifndef LEAN_DEFAULT_SIMP_PROPEXT
#define LEAN_DEFAULT_SIMP_PROPEXT true
#endif
namespace lean {
name const * g_simp_single_pass = nullptr;
name const * g_simp_bottom_up = nullptr;
name const * g_simp_beta_eta = nullptr;
name const * g_simp_iota = nullptr;
name const * g_simp_memoize = nullptr;
name const * g_simp_max_steps = nullptr;
name const * g_simp_trace = nullptr;
name const * g_simp_assumptions = nullptr;
name const * g_simp_funext = nullptr;
name const * g_simp_propext = nullptr;
bool get_simp_single_pass(options const & opts) {
return opts.get_bool(*g_simp_single_pass, LEAN_DEFAULT_SIMP_SINGLE_PASS);
}
bool get_simp_bottom_up(options const & opts) {
return opts.get_bool(*g_simp_bottom_up, LEAN_DEFAULT_SIMP_BOTTOM_UP);
}
bool get_simp_beta_eta(options const & opts) {
return opts.get_bool(*g_simp_beta_eta, LEAN_DEFAULT_SIMP_BETA_ETA);
}
bool get_simp_iota(options const & opts) {
return opts.get_bool(*g_simp_iota, LEAN_DEFAULT_SIMP_IOTA);
}
bool get_simp_memoize(options const & opts) {
return opts.get_bool(*g_simp_memoize, LEAN_DEFAULT_SIMP_MEMOIZE);
}
unsigned get_simp_max_steps(options const & opts) {
return opts.get_bool(*g_simp_max_steps, LEAN_DEFAULT_SIMP_MAX_STEPS);
}
bool get_simp_trace(options const & opts) {
return opts.get_bool(*g_simp_trace, LEAN_DEFAULT_SIMP_TRACE);
}
bool get_simp_assumptions(options const & opts) {
return opts.get_bool(*g_simp_assumptions, LEAN_DEFAULT_SIMP_ASSUMPTIONS);
}
bool get_simp_funext(options const & opts) {
return opts.get_bool(*g_simp_funext, LEAN_DEFAULT_SIMP_FUNEXT);
}
bool get_simp_propext(options const & opts) {
return opts.get_bool(*g_simp_propext, LEAN_DEFAULT_SIMP_PROPEXT);
}
expr const * g_simp_tactic = nullptr;
expr mk_simp_tactic_expr(buffer<expr> const & ls, buffer<name> const & ns,
buffer<name> const & ex, optional<expr> const & pre_tac,
location const & loc) {
expr e = mk_expr_list(ls.size(), ls.data());
expr n = ids_to_tactic_expr(ns);
expr x = ids_to_tactic_expr(ex);
expr t;
if (pre_tac) {
t = mk_app(mk_constant(get_option_some_name()), *pre_tac);
} else {
t = mk_constant(get_option_none_name());
}
expr l = mk_location_expr(loc);
expr r = mk_app({*g_simp_tactic, e, n, x, t, l});
return r;
}
#if 0
class simp_tactic_fn {
public:
enum res_kind { Simplified, Solved, DidNothing };
private:
environment m_env;
io_state m_ios;
name_generator m_ngen;
elaborate_fn m_elab;
optional<tactic> m_tactic;
type_checker m_elab_tc;
app_builder m_app_builder;
// transient state
unsigned m_steps;
goal m_g;
substitution m_subst;
// Remark: the following buffer contains pre-terms that need to be elaborated.
// The 'simp at *' is not very efficient in the current implementation.
// If we have N hypotheses, then m_lemmas_to_process will be processed N+1 times.
buffer<expr> m_lemmas_to_process;
simp_rule_sets m_simp_sets;
// configuration options
bool m_single_pass;
bool m_bottom_up;
bool m_beta_eta;
bool m_iota;
bool m_memoize;
unsigned m_max_steps;
bool m_trace;
bool m_assumptions;
bool m_funext;
bool m_propext;
bool m_standard;
io_state_stream out() const { return regular(m_env, m_ios); }
void set_options(environment const & env, options const & o) {
m_single_pass = get_simp_single_pass(o);
m_bottom_up = get_simp_bottom_up(o);
m_beta_eta = get_simp_beta_eta(o);
m_iota = get_simp_iota(o);
m_memoize = get_simp_memoize(o);
m_max_steps = get_simp_max_steps(o);
m_trace = get_simp_trace(o);
m_assumptions = get_simp_assumptions(o);
if (is_standard(env)) {
m_funext = get_simp_funext(o) && env.find(get_funext_name());
m_propext = get_simp_propext(o) && env.find(get_propext_name());
m_standard = true;
} else {
// TODO(Leo): add support for function extensionality in HoTT mode
m_funext = false;
m_propext = false;
m_standard = false;
}
}
// Add lemmas and assumptions to m_simp_set.
// If hidx is none, then we are elaborating the conclusion, otherwise we are elaborating hypothesis hidx.
// This method destructively updates m_simp_set
void elaborate_lemmas(optional<unsigned> hidx) {
name user("user");
for (expr const & l : m_lemmas_to_process) {
try {
expr new_l; constraints cs;
bool report_unassigned = true;
std::tie(new_l, m_subst, cs) = m_elab(m_g, m_ios.get_options(), m_ngen.mk_child(), l, none_expr(), m_subst, report_unassigned);
if (cs)
throw tactic_exception("invalid 'simp' tactic, fail to resolve generated constraints");
expr new_e = head_beta_reduce(m_elab_tc.infer(new_l).first);
m_simp_sets = add(m_elab_tc, m_simp_sets, user, new_e, new_l);
} catch (exception &) {
if (!hidx) {
// processing conclusion, then report the error
throw;
}
}
}
if (m_assumptions) {
name assump("assumption");
buffer<expr> hyps;
m_g.get_hyps(hyps);
unsigned end = hidx ? *hidx : hyps.size();
for (unsigned i = 0; i < end; i++) {
expr H = hyps[i];
expr H_type = mlocal_type(H);
expr rel, lhs, rhs;
if (is_simp_relation(m_env, H_type, rel, lhs, rhs)) {
// TODO(Leo): we are currently flipping equations when lhs < rhs.
// Should we remove this automatic flipping?
if (get_weight(lhs) >= get_weight(rhs)) {
m_simp_sets = add(m_elab_tc, m_simp_sets, assump, H_type, H);
} else {
// lhs is "smaller" than rhs
// so we try to apply symmetry if available
if (!is_constant(rel))
continue;
name op = const_name(rel);
auto rel_info = get_relation_info(m_env, op);
auto info = get_symm_extra_info(m_env, op);
if (!info || !rel_info)
continue; // relation is not symmetric
buffer<expr> args;
get_app_args(H_type, args);
expr tmp = args[rel_info->get_lhs_pos()];
args[rel_info->get_lhs_pos()] = args[rel_info->get_rhs_pos()];
args[rel_info->get_rhs_pos()] = tmp;
H_type = mk_app(rel, args);
if (auto new_H = m_app_builder.mk_app(info->m_name, H)) {
H = *new_H;
m_simp_sets = add(m_elab_tc, m_simp_sets, assump, H_type, H);
}
}
}
}
}
}
res_kind simp_conclusion() {
elaborate_lemmas(optional<unsigned>());
if (m_trace) {
out() << m_simp_sets;
}
// TODO(Leo)
return DidNothing;
}
bool simp_hyp(unsigned hidx) {
flet<simp_rule_sets> save(m_simp_sets, m_simp_sets);
elaborate_lemmas(optional<unsigned>(hidx));
// TODO(Leo)
return false;
}
// Initialize m_simp_set with information that is context independent
void init_simp_set(buffer<name> const & ns, buffer<name> const & ex) {
// Remark: we cannot initialize explicitly provided lemmas here
// since some of them may depend on hypotheses.
m_simp_sets = get_simp_rule_sets(m_env);
for (name const & n : ns) {
simp_rule_sets tmp_simp_set = get_simp_rule_sets(m_env, n);
m_simp_sets = join(m_simp_sets, tmp_simp_set);
}
m_simp_sets.erase_simp(ex);
}
public:
simp_tactic_fn(environment const & env, io_state const & ios, name_generator && ngen, elaborate_fn const & elab,
buffer<expr> const & ls, buffer<name> const & ns, buffer<name> const & ex,
optional<tactic> const & tac):
m_env(env), m_ios(ios), m_ngen(ngen), m_elab(elab), m_tactic(tac), m_elab_tc(m_env), m_app_builder(m_elab_tc),
m_lemmas_to_process(ls) {
set_options(env, m_ios.get_options());
init_simp_set(ns, ex);
}
std::tuple<res_kind, goal, substitution> operator()(goal const & g, location const & loc, substitution const & s) {
m_g = g;
m_subst = s;
if (loc.is_goal_only()) {
res_kind k = simp_conclusion();
return std::make_tuple(k, m_g, m_subst);
} else {
buffer<expr> hyps;
m_g.get_hyps(hyps);
bool progress = false;
unsigned hidx = 0;
for (expr const & h : hyps) {
if (loc.includes_hypothesis(local_pp_name(h))) {
if (simp_hyp(hidx))
progress = true;
}
hidx++;
}
if (loc.includes_goal()) {
res_kind k = simp_conclusion();
if (k == DidNothing && progress)
k = Simplified;
return std::make_tuple(k, m_g, m_subst);
} else {
return std::make_tuple(progress ? Simplified : DidNothing, m_g, m_subst);
}
}
}
};
#endif
tactic mk_simp_tactic(elaborate_fn const & /* elab */, buffer<expr> const & /* ls */, buffer<name> const & /* ns */,
buffer<name> const & /* ex */, optional<tactic> /* tac */, location const & /* loc */) {
return tactic01([=](environment const & /* env */, io_state const & /* ios */, proof_state const & /* s */) {
// TODO(Leo): we should delete this file... it is subsumed by blast
return none_proof_state();
#if 0
goals const & gs = s.get_goals();
if (empty(gs)) {
throw_no_goal_if_enabled(s);
return none_proof_state();
}
goal const & g = head(gs);
name_generator new_ngen = s.get_ngen();
simp_tactic_fn simp(env, ios, new_ngen.mk_child(), elab, ls, ns, ex, tac);
goal new_g; simp_tactic_fn::res_kind k; substitution new_subst = s.get_subst();
std::tie(k, new_g, new_subst) = simp(g, loc, new_subst);
switch (k) {
case simp_tactic_fn::Simplified: {
proof_state new_s(s, cons(new_g, tail(gs)), new_subst, new_ngen);
return some_proof_state(new_s);
}
case simp_tactic_fn::Solved: {
proof_state new_s(s, tail(gs), new_subst, new_ngen);
return some_proof_state(new_s);
}
case simp_tactic_fn::DidNothing:
return none_proof_state();
}
#endif
});
}
void initialize_simp_tactic() {
name simp_name{"tactic", "simp_tac"};
g_simp_tactic = new expr(mk_constant(simp_name));
register_tac(simp_name,
[](type_checker & tc, elaborate_fn const & elab, expr const & e, pos_info_provider const * p) {
buffer<expr> args;
get_app_args(e, args);
if (args.size() != 5)
throw expr_to_tactic_exception(e, "invalid 'simp' tactic, incorrect number of arguments");
buffer<expr> lemmas;
get_tactic_expr_list_elements(args[0], lemmas, "invalid 'simp' tactic, invalid argument #1");
buffer<name> ns, ex;
get_tactic_id_list_elements(args[1], ns, "invalid 'simp' tactic, invalid argument #2");
get_tactic_id_list_elements(args[2], ex, "invalid 'simp' tactic, invalid argument #3");
optional<tactic> tac;
expr A, t;
if (is_some(args[3], A, t)) {
tac = expr_to_tactic(tc, elab, t, p);
} else if (is_none(args[3], A)) {
// do nothing
} else {
throw expr_to_tactic_exception(e, "invalid 'simp' tactic, invalid argument #4");
}
check_tactic_expr(args[4], "invalid 'simp' tactic, invalid argument #5");
expr loc_expr = get_tactic_expr_expr(args[4]);
if (!is_location_expr(loc_expr))
throw expr_to_tactic_exception(e, "invalid 'simp' tactic, invalid argument #5");
location loc = get_location_expr_location(loc_expr);
return mk_simp_tactic(elab, lemmas, ns, ex, tac, loc);
});
g_simp_single_pass = new name{"simp", "single_pass"};
register_bool_option(*g_simp_single_pass, LEAN_DEFAULT_SIMP_SINGLE_PASS,
"(simp tactic) if false then the simplifier keeps applying simplifications as long as possible");
g_simp_bottom_up = new name{"simp", "bottom_up"};
register_bool_option(*g_simp_bottom_up, LEAN_DEFAULT_SIMP_BOTTOM_UP,
"(simp tactic) if true the simplifier uses a bottom up rewriting strategy, otherwise it uses top down");
g_simp_beta_eta = new name{"simp", "beta_eta"};
register_bool_option(*g_simp_beta_eta, LEAN_DEFAULT_SIMP_BETA_ETA,
"(simp tactic) if true the simplifier applies beta and eta reduction");
g_simp_iota = new name{"simp", "iota"};
register_bool_option(*g_simp_iota, LEAN_DEFAULT_SIMP_IOTA,
"(simp tactic) if true the simplifier applies iota reduction");
g_simp_memoize = new name{"simp", "memoize"};
register_bool_option(*g_simp_memoize, LEAN_DEFAULT_SIMP_MEMOIZE,
"(simp tactic) if true the simplifier caches intermediate results");
g_simp_max_steps = new name{"simp", "max_steps"};
register_unsigned_option(*g_simp_max_steps, LEAN_DEFAULT_SIMP_MAX_STEPS,
"(simp tactic) maximum number of steps that can be performed by the simplifier");
g_simp_trace = new name{"simp", "trace"};
register_bool_option(*g_simp_trace, LEAN_DEFAULT_SIMP_TRACE,
"(simp tactic) if true the simplifier produces an execution trace for debugging purposes");
g_simp_assumptions = new name{"simp", "assumptions"};
register_bool_option(*g_simp_assumptions, LEAN_DEFAULT_SIMP_ASSUMPTIONS,
"(simp tactic) if true assumptions/hypotheses are automatically used as rewriting rules");
g_simp_funext = new name{"simp", "funext"};
register_bool_option(*g_simp_funext, LEAN_DEFAULT_SIMP_FUNEXT,
"(simp tactic) avoid function extensionality even if theorem/axiom is in the environment");
g_simp_propext = new name{"simp", "propext"};
register_bool_option(*g_simp_funext, LEAN_DEFAULT_SIMP_PROPEXT,
"(simp tactic) avoid proposition extensionality even if axiom is in the environment, this option is ignored in HoTT mode");
}
void finalize_simp_tactic() {
delete g_simp_tactic;
delete g_simp_single_pass;
delete g_simp_bottom_up;
delete g_simp_beta_eta;
delete g_simp_iota;
delete g_simp_memoize;
delete g_simp_max_steps;
delete g_simp_trace;
delete g_simp_assumptions;
delete g_simp_funext;
delete g_simp_propext;
}
}

24
src/library/simplifier/simp_tactic.h
View file

@ -1,24 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/expr.h"
#include "library/tactic/location.h"
namespace lean {
/** \brief Create a simp tactic expression where
- ls is a collection of pre-terms representing additional lemmas that should be used as rewriting rules.
- ns is a collection of namespaces that should provide rewriting rules for this tactic.
- ex is a collection of global rewriting rules that should be excluded.
- pre_tac (if provided) is a tactic used to discharge assumptions in conditional rewriting rules.
- loc is the scope of the tactic (i.e., which hypothesis and/or conclusion will be simplified).
*/
expr mk_simp_tactic_expr(buffer<expr> const & ls, buffer<name> const & ns, buffer<name> const & ex,
optional<expr> const & pre_tac, location const & loc);
void initialize_simp_tactic();
void finalize_simp_tactic();
}