max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(simplifier): port skeleton to new tactic framework

Browse source 
Conflicts:
	library/init/meta/tactic.lean
	src/library/tactic/tactic_state.cpp
This commit is contained in:
Daniel Selsam 2016-06-24 10:36:06 -07:00 • committed by Leonardo de Moura
parent 490a116baa
commit e1bc0a68e6
44 changed files with 1251 additions and 1784 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
library/init/meta/tactic.lean
View file

@ -94,6 +94,7 @@ meta_constant unify_core : expr → expr → transparency → tactic unit
/- Infer the type of the given expression.
Remark: transparency does not affect type inference -/
meta_constant infer_type : expr → tactic expr
meta_constant get_local : name → tactic expr
/- Return the hypothesis in the main goal. Fail if tactic_state does not have any goal left. -/
meta_constant local_context : tactic (list expr)
@ -133,6 +134,11 @@ meta_constant mk_instance : expr → tactic expr
/- Simplify the given expression using [defeq] lemmas.
The resulting expression is definitionally equal to the input. -/
meta_constant defeq_simp_core : expr → transparency → tactic expr
/- Simplify the given expression using [simp] and [congr] lemmas.
The result is the simplified expression along with a proof that the new
expression is equivalent to the old one.
Fails if no simplifications can be performed. -/
meta_constant simplify : expr → tactic (prod expr expr)
/- Change the target of the main goal.
The input expression must be definitionally equal to the current target. -/
meta_constant change : expr → tactic unit
@ -234,6 +240,28 @@ defeq_simp_core e transparency.reducible
meta_definition dsimp : tactic unit :=
target >>= defeq_simp >>= change
set_option unifier.conservative true
meta_definition simp : tactic unit :=
do gs ← get_goals,
match gs with
| (g :: rest) := do
tgt ← target,
r ← simplify tgt,
new_tgt ← return (prod.pr1 r),
pf ← return (prod.pr2 r),
pf_type ← infer_type pf,
new_g ← mk_meta_var new_tgt,
ns ← return (match expr.is_eq pf_type with
| (option.some _) := "eq"
| option.none := "iff"
end),
g_pf ← mk_app (ns <.> "mpr") [pf, new_g],
g_pf_type ← infer_type g_pf,
unify g g_pf,
set_goals (new_g :: rest)
| _ := fail "simp called but no goals"
end
/- Return the number of goals that need to be solved -/
meta_definition num_goals : tactic nat :=
do gs ← get_goals,
@ -348,4 +376,6 @@ private meta_definition get_arity_aux : expr → tactic nat
meta_definition get_arity (fn : expr) : tactic nat :=
infer_type fn >>= whnf >>= get_arity_aux
meta_definition triv : tactic unit := mk_const "trivial" >>= exact
end tactic

4
src/CMakeLists.txt
View file

@ -333,6 +333,8 @@ add_subdirectory(library/tactic)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:tactic>)
add_subdirectory(library/tactic/defeq_simplifier)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:defeq_simplifier>)
add_subdirectory(library/tactic/simplifier)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:simplifier>)
add_subdirectory(library/definitional)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:definitional>)
# add_subdirectory(library/blast)
@ -349,8 +351,6 @@ set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:definitional>)
# set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:blast_recursor>)
# add_subdirectory(library/blast/grinder)
# set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:blast_grinder>)
# add_subdirectory(library/blast/simplifier)
# set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:simplifier>)
# add_subdirectory(library/blast/forward)
# set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:forward>)
add_subdirectory(library/vm)

16
src/frontends/lean/old_attributes.cpp
View file

@ -29,22 +29,6 @@ void initialize_old_attributes() {
return env;
},
[](environment const &, name const &) { return false; });
register_prio_attribute("simp", "simplification lemma",
[](environment const & env, io_state const & ios, name const & d, unsigned prio, name const & ns, bool persistent) {
return env;
},
[](environment const &, name const &) { return false; },
[](environment const & env, name const & n) {
return LEAN_DEFAULT_PRIORITY;
});
register_prio_attribute("congr", "congruence lemma",
[](environment const & env, io_state const & ios, name const & d, unsigned prio, name const & ns, bool persistent) {
return env;
},
[](environment const &, name const &) { return false; },
[](environment const & env, name const & n) {
return LEAN_DEFAULT_PRIORITY;
});
register_prio_attribute("forward", "forward chaining",
[](environment const & env, io_state const & ios, name const & d, unsigned prio, name const & ns, bool persistent) {
return env;

19
src/frontends/lean/print_cmd.cpp
View file

@ -30,6 +30,7 @@ Author: Leonardo de Moura
#include "library/legacy_type_context.h"
#include "library/unification_hint.h"
#include "library/tactic/defeq_simplifier/defeq_simp_lemmas.h"
#include "library/tactic/simplifier/simp_lemmas.h"
#include "library/reducible.h"
#include "library/definitional/projection.h"
#include "frontends/lean/parser.h"
@ -554,34 +555,28 @@ static void print_defeq_lemmas(parser & p) {
}
static void print_simp_rules(parser & p) {
/*
type_checker tc(p.env());
auto out = regular(p.env(), p.ios(), tc);
blast::scope_debug scope(p.env(), p.ios());
blast::simp_lemmas s;
simp_lemmas slss;
name ns;
if (p.curr_is_identifier()) {
ns = p.get_name_val();
p.next();
s = blast::get_simp_lemmas(ns);
slss = get_simp_lemmas(p.env(), ns);
} else {
s = blast::get_simp_lemmas();
slss = get_simp_lemmas(p.env());
}
format header;
if (!ns.is_anonymous())
header = format(" at namespace '") + format(ns) + format("'");
out << s.pp_simp(out.get_formatter(), header);
*/
out << slss.pp_simp(out.get_formatter(), header);
}
static void print_congr_rules(parser & p) {
/*
type_checker tc(p.env());
auto out = regular(p.env(), p.ios(), tc);
blast::scope_debug scope(p.env(), p.ios());
blast::simp_lemmas s = blast::get_simp_lemmas();
out << s.pp_congr(out.get_formatter());
*/
simp_lemmas slss = get_simp_lemmas(p.env());
out << slss.pp_congr(out.get_formatter());
}
static void print_light_rules(parser & p) {

2
src/library/CMakeLists.txt
View file

@ -19,7 +19,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
unifier.cpp match.cpp class_instance_resolution.cpp old_type_context.cpp
legacy_type_context.cpp old_type_checker.cpp old_converter.cpp old_default_converter.cpp
old_util.cpp let.cpp metavar_closure.cpp old_local_context.cpp choice_iterator.cpp
tmp_type_context.cpp
old_tmp_type_context.cpp
# light_lt_manager.cpp
# proof_irrel_expr_manager.cpp

2
src/library/app_builder.cpp
View file

@ -14,7 +14,7 @@ Author: Leonardo de Moura
#include "library/constants.h"
#include "library/cache_helper.h"
#include "library/app_builder.h"
#include "library/tmp_type_context.h"
#include "library/old_tmp_type_context.h"
#include "library/relation_manager.h"
namespace lean {

2
src/library/blast/actions/by_contradiction_action.cpp
View file

@ -35,7 +35,7 @@ action_result by_contradiction_action() {
s.set_target(mk_arrow(not_target, mk_constant(get_false_name())));
return intros_action(1);
}
blast_tmp_type_context tmp_tctx;
blast_old_tmp_type_context tmp_tctx;
optional<expr> target_decidable = tmp_tctx->mk_class_instance(mk_app(mk_constant(get_decidable_name()), target));
if (!target_decidable) return action_result::failed();
expr href = s.mk_hypothesis(get_app_builder().mk_not(target));

14
src/library/blast/backward/backward_lemmas.cpp
View file

@ -11,7 +11,7 @@ Author: Leonardo de Moura
#include "library/trace.h"
#include "library/scoped_ext.h"
#include "library/user_recursors.h"
#include "library/tmp_type_context.h"
#include "library/old_tmp_type_context.h"
#include "library/attribute_manager.h"
#include "library/blast/blast.h"
#include "library/blast/backward/backward_lemmas.h"
@ -57,7 +57,7 @@ struct backward_config {
typedef scoped_ext<backward_config> backward_ext;
static optional<head_index> get_backward_target(tmp_type_context & ctx, expr type) {
static optional<head_index> get_backward_target(old_tmp_type_context & ctx, expr type) {
while (is_pi(type)) {
expr local = ctx.mk_tmp_local(binding_domain(type));
type = ctx.whnf(instantiate(binding_body(type), local));
@ -69,7 +69,7 @@ static optional<head_index> get_backward_target(tmp_type_context & ctx, expr typ
return optional<head_index>();
}
static optional<head_index> get_backward_target(tmp_type_context & ctx, name const & c) {
static optional<head_index> get_backward_target(old_tmp_type_context & ctx, name const & c) {
declaration const & d = ctx.env().get(c);
buffer<level> us;
unsigned num_us = d.get_num_univ_params();
@ -80,7 +80,7 @@ static optional<head_index> get_backward_target(tmp_type_context & ctx, name con
}
environment add_backward_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent) {
tmp_type_context ctx(env, ios.get_options());
old_tmp_type_context ctx(env, ios.get_options());
auto index = get_backward_target(ctx, c);
if (!index || index->kind() != expr_kind::Constant)
throw exception(sstream() << "invalid [intro] attribute for '" << c << "', head symbol of resulting type must be a constant");
@ -130,7 +130,7 @@ unsigned backward_lemma_prio_fn::operator()(backward_lemma const & r) const {
void backward_lemma_index::init() {
m_index.clear();
buffer<name> lemmas;
blast_tmp_type_context ctx;
blast_old_tmp_type_context ctx;
auto const & s = backward_ext::get_state(env());
s.to_buffer(lemmas);
unsigned i = lemmas.size();
@ -148,7 +148,7 @@ void backward_lemma_index::init() {
}
void backward_lemma_index::insert(expr const & href) {
blast_tmp_type_context ctx;
blast_old_tmp_type_context ctx;
expr href_type = ctx->infer(href);
if (optional<head_index> target = get_backward_target(*ctx, href_type)) {
m_index.insert(*target, backward_lemma(gexpr(href)));
@ -156,7 +156,7 @@ void backward_lemma_index::insert(expr const & href) {
}
void backward_lemma_index::erase(expr const & href) {
blast_tmp_type_context ctx;
blast_old_tmp_type_context ctx;
expr href_type = ctx->infer(href);
if (optional<head_index> target = get_backward_target(*ctx, href_type)) {
m_index.erase(*target, backward_lemma(gexpr(href)));

48
src/library/blast/blast.cpp
View file

@ -75,17 +75,17 @@ struct imp_extension_entry {
unsigned proof_irrel_hash(expr const & e);
bool proof_irrel_is_equal(expr const & e1, expr const & e2);
class tmp_tctx_pool : public tmp_type_context_pool {
class tmp_tctx_pool : public old_tmp_type_context_pool {
public:
virtual tmp_type_context * mk_tmp_type_context() override;
virtual void recycle_tmp_type_context(tmp_type_context * tmp_tctx) override;
virtual old_tmp_type_context * mk_old_tmp_type_context() override;
virtual void recycle_old_tmp_type_context(old_tmp_type_context * tmp_tctx) override;
};
class blastenv {
friend class scope_assignment;
friend class scope_unfold_macro_pred;
typedef std::vector<tmp_type_context *> tmp_type_context_pool;
typedef std::unique_ptr<tmp_type_context> tmp_type_context_ptr;
typedef std::vector<old_tmp_type_context *> old_tmp_type_context_pool;
typedef std::unique_ptr<old_tmp_type_context> old_tmp_type_context_ptr;
typedef std::vector<imp_extension_entry> imp_extension_entries;
environment m_env;
@ -111,8 +111,8 @@ class blastenv {
name_map<projection_info> m_projection_info;
is_relation_pred m_is_relation_pred;
state m_curr_state; // current state
tmp_type_context_pool m_tmp_ctx_pool;
tmp_type_context_ptr m_tmp_ctx; // for app_builder and congr_lemma_manager
old_tmp_type_context_pool m_tmp_ctx_pool;
old_tmp_type_context_ptr m_tmp_ctx; // for app_builder and congr_lemma_manager
app_builder m_app_builder;
fun_info_manager m_fun_info_manager;
congr_lemma_manager m_congr_lemma_manager;
@ -674,7 +674,7 @@ public:
m_class_pred(mk_class_pred(env)),
m_instance_pred(mk_instance_pred(env)),
m_is_relation_pred(mk_is_relation_pred(env)),
m_tmp_ctx(mk_tmp_type_context()),
m_tmp_ctx(mk_old_tmp_type_context()),
m_app_builder(*m_tmp_ctx),
m_fun_info_manager(*m_tmp_ctx),
m_congr_lemma_manager(m_app_builder, m_fun_info_manager),
@ -777,9 +777,9 @@ public:
return m_tmp_ctx->mk_subsingleton_instance(type);
}
tmp_type_context * mk_tmp_type_context();
old_tmp_type_context * mk_old_tmp_type_context();
void recycle_tmp_type_context(tmp_type_context * ctx) {
void recycle_old_tmp_type_context(old_tmp_type_context * ctx) {
lean_assert(ctx);
ctx->clear();
m_tmp_ctx_pool.push_back(ctx);
@ -1446,10 +1446,10 @@ scope_debug::~scope_debug() {}
/** \brief We need to redefine infer_local and infer_metavar, because the types of hypotheses
and blast meta-variables are stored in the blast state */
class tmp_tctx : public tmp_type_context {
class tmp_tctx : public old_tmp_type_context {
public:
tmp_tctx(environment const & env, options const & o):
tmp_type_context(env, o) {}
old_tmp_type_context(env, o) {}
virtual bool should_unfold_macro(expr const & e) const override {
return get_unfold_macro_pred()(e);
@ -1483,8 +1483,8 @@ public:
}
};
tmp_type_context * blastenv::mk_tmp_type_context() {
tmp_type_context * r;
old_tmp_type_context * blastenv::mk_old_tmp_type_context() {
old_tmp_type_context * r;
if (m_tmp_ctx_pool.empty()) {
r = new tmp_tctx(m_env, m_ios.get_options());
// Design decision: in the blast tactic, we only consider the instances that were
@ -1500,31 +1500,31 @@ tmp_type_context * blastenv::mk_tmp_type_context() {
return r;
}
tmp_type_context * tmp_tctx_pool::mk_tmp_type_context() {
old_tmp_type_context * tmp_tctx_pool::mk_old_tmp_type_context() {
lean_assert(g_blastenv);
return g_blastenv->mk_tmp_type_context();
return g_blastenv->mk_old_tmp_type_context();
}
void tmp_tctx_pool::recycle_tmp_type_context(tmp_type_context * tmp_tctx) {
void tmp_tctx_pool::recycle_old_tmp_type_context(old_tmp_type_context * tmp_tctx) {
lean_assert(g_blastenv);
g_blastenv->recycle_tmp_type_context(tmp_tctx);
g_blastenv->recycle_old_tmp_type_context(tmp_tctx);
}
blast_tmp_type_context::blast_tmp_type_context(unsigned num_umeta, unsigned num_emeta) {
blast_old_tmp_type_context::blast_old_tmp_type_context(unsigned num_umeta, unsigned num_emeta) {
lean_assert(g_blastenv);
m_ctx = g_blastenv->mk_tmp_type_context();
m_ctx = g_blastenv->mk_old_tmp_type_context();
m_ctx->clear();
m_ctx->set_next_uvar_idx(num_umeta);
m_ctx->set_next_mvar_idx(num_emeta);
}
blast_tmp_type_context::blast_tmp_type_context() {
blast_old_tmp_type_context::blast_old_tmp_type_context() {
lean_assert(g_blastenv);
m_ctx = g_blastenv->mk_tmp_type_context();
m_ctx = g_blastenv->mk_old_tmp_type_context();
}
blast_tmp_type_context::~blast_tmp_type_context() {
g_blastenv->recycle_tmp_type_context(m_ctx);
blast_old_tmp_type_context::~blast_old_tmp_type_context() {
g_blastenv->recycle_old_tmp_type_context(m_ctx);
}
expr internalize(expr const & e) {

22
src/library/blast/blast.h
View file

@ -8,7 +8,7 @@ Author: Leonardo de Moura
#include <memory>
#include "kernel/environment.h"
#include "library/io_state.h"
#include "library/tmp_type_context.h"
#include "library/old_tmp_type_context.h"
#include "library/relation_manager.h"
#include "library/congr_lemma_manager.h"
#include "library/fun_info_manager.h"
@ -18,7 +18,7 @@ Author: Leonardo de Moura
namespace lean {
struct projection_info;
class goal;
typedef std::unique_ptr<tmp_type_context> tmp_type_context_ptr;
typedef std::unique_ptr<old_tmp_type_context> old_tmp_type_context_ptr;
namespace blast {
/** \brief Create a blast-state universe meta-variable */
level mk_uref(unsigned idx);
@ -245,17 +245,17 @@ public:
/** \brief Create a temporary type_context that is compatible with blast.
This temporary type context can acces the type of blast hypotheses
and meta-variables. */
class blast_tmp_type_context {
tmp_type_context * m_ctx;
class blast_old_tmp_type_context {
old_tmp_type_context * m_ctx;
public:
blast_tmp_type_context(unsigned num_umeta, unsigned num_emeta);
blast_tmp_type_context();
~blast_tmp_type_context();
blast_old_tmp_type_context(unsigned num_umeta, unsigned num_emeta);
blast_old_tmp_type_context();
~blast_old_tmp_type_context();
tmp_type_context const * operator->() const { return m_ctx; }
tmp_type_context * operator->() { return m_ctx; }
tmp_type_context const & operator*() const { return *m_ctx; }
tmp_type_context & operator*() { return *m_ctx; }
old_tmp_type_context const * operator->() const { return m_ctx; }
old_tmp_type_context * operator->() { return m_ctx; }
old_tmp_type_context const & operator*() const { return *m_ctx; }
old_tmp_type_context & operator*() { return *m_ctx; }
};
class scope_curr_state {

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

@ -293,7 +293,7 @@ static optional<ext_congr_lemma> to_ext_congr_lemma(name const & R, expr const &
if (!all_distinct(lhs_args) || !all_distinct(rhs_args)) {
return optional<ext_congr_lemma>();
}
blast_tmp_type_context ctx(r.get_num_umeta(), r.get_num_emeta());
blast_old_tmp_type_context ctx(r.get_num_umeta(), r.get_num_emeta());
if (!ctx->is_def_eq(fn, lhs_fn) || !ctx->is_def_eq(fn, rhs_fn)) {
return optional<ext_congr_lemma>();
}

2
src/library/blast/forward/ematch.cpp
View file

@ -253,7 +253,7 @@ void finalize_ematch() {}
struct ematch_fn {
ematch_branch_extension_core & m_ext;
instances_branch_extension & m_inst_ext;
blast_tmp_type_context m_ctx;
blast_old_tmp_type_context m_ctx;
congruence_closure & m_cc;
enum frame_kind { DefEqOnly, EqvOnly, Match, MatchSS /* match subsingleton */, Continue };

16
src/library/blast/forward/pattern.cpp
View file

@ -14,7 +14,7 @@ Author: Leonardo de Moura
#include "kernel/instantiate.h"
#include "library/kernel_serializer.h"
#include "library/generic_exception.h"
#include "library/tmp_type_context.h"
#include "library/old_tmp_type_context.h"
#include "library/annotation.h"
#include "library/util.h"
#include "library/scoped_ext.h"
@ -191,7 +191,7 @@ name_set const & get_no_patterns(environment const & env) {
namespace blast {
typedef rb_tree<unsigned, unsigned_cmp> idx_metavar_set;
static bool is_higher_order(tmp_type_context & ctx, expr const & e) {
static bool is_higher_order(old_tmp_type_context & ctx, expr const & e) {
/* Remark: it is too expensive to use ctx.relaxed_whnf here. */
return is_pi(ctx.whnf(ctx.infer(e)));
}
@ -200,7 +200,7 @@ static bool is_higher_order(tmp_type_context & ctx, expr const & e) {
create n idx_metavars (one for each a_i), store the meta-variables in mvars,
and store in trackable and residue the subsets of these meta-variables as
described in the beginning of this file. Then returns B (instantiated with the new meta-variables) */
expr extract_trackable(tmp_type_context & ctx, expr const & type,
expr extract_trackable(old_tmp_type_context & ctx, expr const & type,
buffer<expr> & mvars,
buffer<bool> & inst_implicit_flags,
idx_metavar_set & trackable, idx_metavar_set & residue) {
@ -286,7 +286,7 @@ expr extract_trackable(tmp_type_context & ctx, expr const & type,
}
struct mk_hi_lemma_fn {
tmp_type_context & m_ctx;
old_tmp_type_context & m_ctx;
name_set const & m_no_patterns;
expr m_H;
unsigned m_num_uvars;
@ -301,7 +301,7 @@ struct mk_hi_lemma_fn {
idx_metavar_set m_residue;
unsigned m_num_steps;
mk_hi_lemma_fn(tmp_type_context & ctx, expr const & H,
mk_hi_lemma_fn(old_tmp_type_context & ctx, expr const & H,
unsigned num_uvars, unsigned prio, unsigned max_steps, bool simp):
m_ctx(ctx), m_no_patterns(no_pattern_ext::get_state(ctx.env())),
m_H(H), m_num_uvars(num_uvars), m_priority(prio), m_max_steps(max_steps),
@ -623,7 +623,7 @@ struct mk_hi_lemma_fn {
}
};
hi_lemma mk_hi_lemma_core(tmp_type_context & ctx, expr const & H, unsigned num_uvars,
hi_lemma mk_hi_lemma_core(old_tmp_type_context & ctx, expr const & H, unsigned num_uvars,
unsigned priority, unsigned max_steps, bool simp) {
try {
bool erase_hints = false;
@ -640,14 +640,14 @@ hi_lemma mk_hi_lemma_core(tmp_type_context & ctx, expr const & H, unsigned num_u
}
hi_lemma mk_hi_lemma(expr const & H) {
blast_tmp_type_context ctx;
blast_old_tmp_type_context ctx;
unsigned max_steps = get_config().m_pattern_max_steps;
bool simp = false;
return mk_hi_lemma_core(*ctx, H, 0, LEAN_DEFAULT_PRIORITY, max_steps, simp);
}
hi_lemma mk_hi_lemma(name const & c, unsigned priority, bool simp) {
blast_tmp_type_context ctx;
blast_old_tmp_type_context ctx;
unsigned max_steps = get_config().m_pattern_max_steps;
declaration const & d = env().get(c);
buffer<level> us;

2
src/library/blast/forward/pattern.h
View file

@ -8,7 +8,7 @@ Author: Leonardo de Moura
#include "util/rb_multi_map.h"
#include "kernel/environment.h"
#include "library/expr_lt.h"
#include "library/tmp_type_context.h"
#include "library/old_tmp_type_context.h"
namespace lean {
/** \brief Annotate \c e as a pattern hint */

8
src/library/blast/grinder/intro_elim_lemmas.cpp
View file

@ -11,7 +11,7 @@ Author: Leonardo de Moura
#include "library/trace.h"
#include "library/scoped_ext.h"
#include "library/user_recursors.h"
#include "library/tmp_type_context.h"
#include "library/old_tmp_type_context.h"
#include "library/attribute_manager.h"
#include "library/blast/blast.h"
#include "library/blast/grinder/intro_elim_lemmas.h"
@ -70,7 +70,7 @@ environment add_elim_lemma(environment const & env, io_state const & ios, name c
return intro_elim_ext::add_entry(env, ios, intro_elim_entry(true, prio, c), ns, persistent);
}
optional<name> get_intro_target(tmp_type_context & ctx, name const & c) {
optional<name> get_intro_target(old_tmp_type_context & ctx, name const & c) {
declaration const & d = ctx.env().get(c);
buffer<level> us;
unsigned num_us = d.get_num_univ_params();
@ -90,7 +90,7 @@ optional<name> get_intro_target(tmp_type_context & ctx, name const & c) {
}
environment add_intro_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent) {
tmp_type_context ctx(env, ios.get_options());
old_tmp_type_context ctx(env, ios.get_options());
if (!get_intro_target(ctx, c))
throw exception(sstream() << "invalid [intro!] attribute for '" << c << "', head symbol of resulting type must be a constant");
return intro_elim_ext::add_entry(env, ios, intro_elim_entry(false, prio, c), ns, persistent);
@ -148,7 +148,7 @@ namespace blast {
head_map<gexpr> mk_intro_lemma_index() {
head_map<gexpr> r;
buffer<name> lemmas;
blast_tmp_type_context ctx;
blast_old_tmp_type_context ctx;
get_intro_lemmas(env(), lemmas);
unsigned i = lemmas.size();
while (i > 0) {

2
src/library/blast/simplifier/CMakeLists.txt
View file

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

1216
src/library/blast/simplifier/simplifier.cpp
View file

File diff suppressed because it is too large Load diff

149
src/library/blast/simplifier/simplifier_actions.cpp
View file

@ -1,149 +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/attribute_manager.h"
#include "library/constants.h"
#include "library/util.h"
#include "library/blast/blast.h"
#include "library/blast/trace.h"
#include "library/blast/options.h"
#include "library/blast/simplifier/simplifier.h"
#include "library/blast/simplifier/ceqv.h"
namespace lean {
namespace blast {
static unsigned g_ext_id = 0;
struct simplifier_branch_extension : public branch_extension {
simp_lemmas m_simp_lemmas;
bool m_simp_target{false}; // true if target needs to be simplified again
simplifier_branch_extension() {}
simplifier_branch_extension(simplifier_branch_extension const & b):
m_simp_lemmas(b.m_simp_lemmas) {}
virtual ~simplifier_branch_extension() {}
virtual branch_extension * clone() override { return new simplifier_branch_extension(*this); }
virtual void initialized() override { m_simp_lemmas = ::lean::blast::get_simp_lemmas(); }
virtual void target_updated() override { m_simp_target = true; }
virtual void hypothesis_activated(hypothesis const &, hypothesis_idx) override { }
virtual void hypothesis_deleted(hypothesis const &, hypothesis_idx) override { }
simp_lemmas const & get_simp_lemmas() const { return m_simp_lemmas; }
};
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);
}
class simplify_target_proof_step_cell : public proof_step_cell {
bool m_iff;
expr m_eq_pr;
public:
simplify_target_proof_step_cell(bool iff, expr const & eq_pr):
m_iff(iff), m_eq_pr(eq_pr) {}
virtual ~simplify_target_proof_step_cell() {}
virtual action_result resolve(expr const & pr) const override {
try {
app_builder & b = get_app_builder();
if (m_iff)
return action_result::solved(b.mk_app(get_iff_mpr_name(), m_eq_pr, pr));
else
return action_result::solved(b.mk_app(get_eq_mpr_name(), m_eq_pr, pr));
} catch (app_builder_exception &) {
return action_result::failed();
}
}
};
action_result simplify_target_action() {
if (!get_config().m_simp)
return action_result::failed();
auto & ext = get_extension();
if (!ext.m_simp_target)
return action_result::failed(); // nothing to be done
ext.m_simp_target = false;
state & s = curr_state();
expr target = s.get_target();
bool iff = use_iff(target);
name rname = iff ? get_iff_name() : get_eq_name();
auto r = simplify(rname, target, ext.get_simp_lemmas());
if (r.get_new() == target)
return action_result::failed(); // did nothing
if (r.has_proof()) {
// Remark: we only need to create the proof step if a proof was generated.
// If a proof was not generated and the resulting expression is not
// structurally equal, then they are definitionally equal and no proof is
// needed
s.push_proof_step(new simplify_target_proof_step_cell(iff, r.get_proof()));
}
s.set_target(r.get_new());
trace_action("simplify");
return action_result::new_branch();
}
action_result simplify_hypothesis_action(hypothesis_idx hidx) {
if (!get_config().m_simp)
return action_result::failed();
state & s = curr_state();
if (s.has_target_forward_deps(hidx)) {
// We currently do not try to simplify a hypothesis if other
// hypotheses or target depends on it.
return action_result::failed();
}
hypothesis const & h = s.get_hypothesis_decl(hidx);
if (!is_prop(h.get_type())) {
// We currently only simplify propositions.
return action_result::failed();
}
auto & ext = get_extension();
auto r = simplify(get_iff_name(), h.get_type(), ext.get_simp_lemmas());
if (r.get_new() == h.get_type())
return action_result::failed(); // did nothing
expr new_h_proof;
if (r.has_proof()) {
new_h_proof = get_app_builder().mk_app(get_iff_mp_name(), r.get_proof(), h.get_self());
} else {
// they are definitionally equal
new_h_proof = h.get_self();
}
if (!is_true(r.get_new()))
s.mk_hypothesis(r.get_new(), new_h_proof);
s.del_hypothesis(hidx);
return action_result::new_branch();
}
action_result add_simp_lemma_action(hypothesis_idx hidx) {
if (!get_config().m_simp)
return action_result::failed();
blast_tmp_type_context ctx;
state & s = curr_state();
hypothesis const & h = s.get_hypothesis_decl(hidx);
list<expr_pair> ps = to_ceqvs(*ctx, h.get_type(), h.get_self());
if (!ps)
return action_result::failed();
auto & ext = get_extension();
bool added = false;
for (auto const & p : ps) {
try {
ext.m_simp_lemmas = add(*ctx, ext.m_simp_lemmas, h.get_name(), p.first, p.second, LEAN_DEFAULT_PRIORITY);
added = true;
} catch (exception &) {
// TODO(Leo, Daniel): store event
}
}
return added ? action_result::new_branch() : action_result::failed();
}
}}

18
src/library/blast/simplifier/simplifier_actions.h
View file

@ -1,18 +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 "library/blast/hypothesis.h"
#include "library/blast/action_result.h"
namespace lean {
namespace blast {
action_result simplify_hypothesis_action(hypothesis_idx hidx);
action_result simplify_target_action();
action_result add_simp_lemma_action(hypothesis_idx hidx);
void initialize_simplifier_actions();
void finalize_simplifier_actions();
}}

71
src/library/blast/simplifier/simplifier_strategies.cpp
View file

@ -1,71 +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/blast/strategy.h"
#include "library/blast/simplifier/simplifier_actions.h"
#include "library/blast/actions/simple_actions.h"
#include "library/blast/actions/intros_action.h"
#include "library/blast/actions/subst_action.h"
#include "library/blast/actions/no_confusion_action.h"
namespace lean {
namespace blast {
class simplifier_strategy_fn : public strategy_fn {
bool m_simp_target;
bool m_simp_hyps;
bool m_use_hyps;
virtual char const * get_name() const override { return "simp"; }
virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override {
Try(assumption_contradiction_actions(hidx));
if (m_simp_hyps) {
Try(simplify_hypothesis_action(hidx));
}
Try(no_confusion_action(hidx));
Try(discard_action(hidx));
if (m_use_hyps)
Try(subst_action(hidx));
return action_result::new_branch();
}
virtual action_result hypothesis_post_activation(hypothesis_idx hidx) override {
if (m_use_hyps)
add_simp_lemma_action(hidx);
return action_result::new_branch();
}
virtual action_result next_action() override {
if (m_simp_hyps || m_use_hyps) {
Try(intros_action());
Try(assumption_action());
Try(activate_hypothesis());
}
if (m_simp_target) {
Try(simplify_target_action());
}
Try(trivial_action());
return action_result::failed();
}
public:
simplifier_strategy_fn(bool simp_target, bool simp_hyps, bool use_hyps):
m_simp_target(simp_target), m_simp_hyps(simp_hyps),
m_use_hyps(use_hyps) {}
};
strategy mk_simplify_target_strategy() {
return []() { return simplifier_strategy_fn(true, false, false)(); }; // NOLINT
}
strategy mk_simplify_all_strategy() {
return []() { return simplifier_strategy_fn(true, true, false)(); }; // NOLINT
}
strategy mk_simplify_using_hypotheses_strategy() {
return []() { return simplifier_strategy_fn(true, true, true)(); }; // NOLINT
}
}}

15
src/library/blast/simplifier/simplifier_strategies.h
View file

@ -1,15 +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 "library/blast/strategy.h"
namespace lean {
namespace blast {
strategy mk_simplify_target_strategy();
strategy mk_simplify_all_strategy();
strategy mk_simplify_using_hypotheses_strategy();
}}

12
src/library/local_context.cpp
View file

@ -181,16 +181,16 @@ void local_context::clear(local_decl const & d) {
bool local_context::is_subset_of(name_set const & ls) const {
// TODO(Leo): we can improve performance by implementing the subset operation in the rb_map/rb_tree class
return !m_name2local_decl.find_if([&](name const & n, local_decl const &) {
return !ls.contains(n);
});
return !static_cast<bool>(m_name2local_decl.find_if([&](name const & n, local_decl const &) {
return !ls.contains(n);
}));
}
bool local_context::is_subset_of(local_context const & ctx) const {
// TODO(Leo): we can improve performance by implementing the subset operation in the rb_map/rb_tree class
return !m_name2local_decl.find_if([&](name const & n, local_decl const &) {
return !ctx.m_name2local_decl.contains(n);
});
return !static_cast<bool>(m_name2local_decl.find_if([&](name const & n, local_decl const &) {
return !ctx.m_name2local_decl.contains(n);
}));
}
local_context local_context::remove(buffer<expr> const & locals) const {

4
src/library/old_tactic/tactic/norm_num_tactic.cpp
View file

@ -8,7 +8,7 @@ Author: Robert Y. Lewis
#include "library/reducible.h"
#include "library/normalize.h"
#include "library/norm_num.h"
#include "library/tmp_type_context.h"
#include "library/old_tmp_type_context.h"
#include "library/tactic/expr_to_tactic.h"
namespace lean {
@ -32,7 +32,7 @@ tactic norm_num_tactic() {
buffer<expr> hyps;
g.get_hyps(hyps);
try {
tmp_type_context ctx(env, ios.get_options());
old_tmp_type_context ctx(env, ios.get_options());
ctx.set_local_instances(to_list(hyps));
pair<expr, expr> p = mk_norm_num(ctx, lhs);
expr new_lhs = p.first;

38
src/library/tmp_type_context.cpp → src/library/old_tmp_type_context.cpp
View file

@ -4,26 +4,26 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/tmp_type_context.h"
#include "library/old_tmp_type_context.h"
#include "library/idx_metavar.h"
namespace lean {
void tmp_type_context::init(environment const & env, reducible_behavior b) {
void old_tmp_type_context::init(environment const & env, reducible_behavior b) {
switch (b) {
case UnfoldReducible: m_opaque_pred = mk_not_reducible_pred(env); break;
case UnfoldSemireducible: m_opaque_pred = mk_irreducible_pred(env); break;
}
}
tmp_type_context::tmp_type_context(environment const & env, options const & o, reducible_behavior b):
old_tmp_type_context::old_tmp_type_context(environment const & env, options const & o, reducible_behavior b):
old_type_context(env, o) {
init(env, b);
}
tmp_type_context::~tmp_type_context() {
old_tmp_type_context::~old_tmp_type_context() {
}
void tmp_type_context::clear() {
void old_tmp_type_context::clear() {
m_uassignment.clear();
m_eassignment.clear();
m_trail.clear();
@ -31,27 +31,27 @@ void tmp_type_context::clear() {
clear_infer_cache();
}
void tmp_type_context::set_next_uvar_idx(unsigned next_idx) {
void old_tmp_type_context::set_next_uvar_idx(unsigned next_idx) {
lean_assert(m_uassignment.empty());
lean_assert(m_scopes.empty());
m_uassignment.resize(next_idx);
}
void tmp_type_context::set_next_mvar_idx(unsigned next_idx) {
void old_tmp_type_context::set_next_mvar_idx(unsigned next_idx) {
lean_assert(m_eassignment.empty());
lean_assert(m_scopes.empty());
m_eassignment.resize(next_idx);
}
bool tmp_type_context::is_uvar(level const & l) const {
bool old_tmp_type_context::is_uvar(level const & l) const {
return is_idx_metauniv(l);
}
bool tmp_type_context::is_mvar(expr const & e) const {
bool old_tmp_type_context::is_mvar(expr const & e) const {
return is_idx_metavar(e);
}
optional<level> tmp_type_context::get_assignment(level const & u) const {
optional<level> old_tmp_type_context::get_assignment(level const & u) const {
unsigned idx = to_meta_idx(u);
// if the following assetion is violated, we have two options:
// 1- We should create the meta-variable using mk_uvar
@ -61,7 +61,7 @@ optional<level> tmp_type_context::get_assignment(level const & u) const {
return m_uassignment[idx];
}
optional<expr> tmp_type_context::get_assignment(expr const & m) const {
optional<expr> old_tmp_type_context::get_assignment(expr const & m) const {
unsigned idx = to_meta_idx(m);
// if the following assetion is violated, we have two options:
// 1- We should create the meta-variable using mk_mvar
@ -71,7 +71,7 @@ optional<expr> tmp_type_context::get_assignment(expr const & m) const {
return m_eassignment[idx];
}
void tmp_type_context::update_assignment(level const & u, level const & v) {
void old_tmp_type_context::update_assignment(level const & u, level const & v) {
unsigned idx = to_meta_idx(u);
lean_assert(idx < m_uassignment.size()); // see comments above
lean_assert(!m_uassignment[idx]);
@ -80,7 +80,7 @@ void tmp_type_context::update_assignment(level const & u, level const & v) {
m_trail.emplace_back(trail_kind::Level, idx);
}
void tmp_type_context::update_assignment(expr const & m, expr const & v) {
void old_tmp_type_context::update_assignment(expr const & m, expr const & v) {
unsigned idx = to_meta_idx(m);
lean_assert(idx < m_eassignment.size()); // see comments above
// Remark: type class resolution may update an already assigned meta-variable with a
@ -93,19 +93,19 @@ void tmp_type_context::update_assignment(expr const & m, expr const & v) {
m_trail.emplace_back(trail_kind::Expr, idx);
}
level tmp_type_context::mk_uvar() {
level old_tmp_type_context::mk_uvar() {
unsigned idx = m_uassignment.size();
m_uassignment.push_back(none_level());
return mk_idx_metauniv(idx);
}
expr tmp_type_context::mk_mvar(expr const & type) {
expr old_tmp_type_context::mk_mvar(expr const & type) {
unsigned idx = m_eassignment.size();
m_eassignment.push_back(none_expr());
return mk_idx_metavar(idx, type);
}
void tmp_type_context::push_core() {
void old_tmp_type_context::push_core() {
m_scopes.push_back(scope());
scope & s = m_scopes.back();
s.m_uassignment_sz = m_uassignment.size();
@ -113,7 +113,7 @@ void tmp_type_context::push_core() {
s.m_trail_sz = m_trail.size();
}
void tmp_type_context::pop_core() {
void old_tmp_type_context::pop_core() {
lean_assert(!m_scopes.empty());
scope const & s = m_scopes.back();
unsigned old_sz = s.m_trail_sz;
@ -133,11 +133,11 @@ void tmp_type_context::pop_core() {
m_scopes.pop_back();
}
unsigned tmp_type_context::get_num_check_points() const {
unsigned old_tmp_type_context::get_num_check_points() const {
return m_scopes.size();
}
void tmp_type_context::commit() {
void old_tmp_type_context::commit() {
lean_assert(!m_scopes.empty());
m_scopes.pop_back();
}

22
src/library/tmp_type_context.h → src/library/old_tmp_type_context.h
View file

@ -28,7 +28,7 @@ namespace lean {
\remark The local context is set using the method set_context from type_context.
*/
class tmp_type_context : public old_type_context {
class old_tmp_type_context : public old_type_context {
name_predicate m_opaque_pred;
std::vector<optional<level>> m_uassignment;
std::vector<optional<expr>> m_eassignment;
@ -43,8 +43,8 @@ class tmp_type_context : public old_type_context {
std::vector<scope> m_scopes;
void init(environment const & env, reducible_behavior b);
public:
tmp_type_context(environment const & env, options const & o, reducible_behavior b = UnfoldReducible);
virtual ~tmp_type_context();
old_tmp_type_context(environment const & env, options const & o, reducible_behavior b = UnfoldReducible);
virtual ~old_tmp_type_context();
/** \brief Reset the state: backtracking stack, indices and assignment. */
void clear();
@ -91,23 +91,23 @@ public:
}
};
class tmp_type_context_pool {
class old_tmp_type_context_pool {
public:
virtual tmp_type_context * mk_tmp_type_context() =0;
virtual void recycle_tmp_type_context(tmp_type_context * tmp_tctx) =0;
virtual old_tmp_type_context * mk_old_tmp_type_context() =0;
virtual void recycle_old_tmp_type_context(old_tmp_type_context * tmp_tctx) =0;
virtual ~tmp_type_context_pool() {}
virtual ~old_tmp_type_context_pool() {}
};
class default_tmp_type_context_pool : public tmp_type_context_pool {
class default_old_tmp_type_context_pool : public old_tmp_type_context_pool {
environment m_env;
options m_options;
public:
default_tmp_type_context_pool(environment const & env, options const & o):
default_old_tmp_type_context_pool(environment const & env, options const & o):
m_env(env), m_options(o) {}
virtual tmp_type_context * mk_tmp_type_context() override { return new tmp_type_context(m_env, m_options); }
virtual void recycle_tmp_type_context(tmp_type_context * tmp_tctx) override { delete tmp_tctx; }
virtual old_tmp_type_context * mk_old_tmp_type_context() override { return new old_tmp_type_context(m_env, m_options); }
virtual void recycle_old_tmp_type_context(old_tmp_type_context * tmp_tctx) override { delete tmp_tctx; }
};
}

10
src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp
View file

@ -13,8 +13,8 @@ Author: Daniel Selsam
#include "library/util.h"
#include "library/expr_lt.h"
#include "library/scoped_ext.h"
#include "library/tmp_type_context.h"
#include "library/tactic/defeq_simplifier/defeq_simp_lemmas.h"
#include "library/old_tmp_type_context.h"
namespace lean {
@ -37,7 +37,7 @@ struct defeq_simp_lemmas_state {
defeq_simp_lemmas m_defeq_simp_lemmas;
name_map<unsigned> m_decl_name_to_prio; // Note: redundant but convenient
void register_defeq_simp_lemma(tmp_type_context & tctx, name const & decl_name, unsigned priority) {
void register_defeq_simp_lemma(old_tmp_type_context & tctx, name const & decl_name, unsigned priority) {
declaration const & d = tctx.env().get(decl_name);
// TODO(dhs): once we refactor to register this attribute as "definitions-only", this can be an assert
if (!d.is_definition()) {
@ -54,7 +54,7 @@ struct defeq_simp_lemmas_state {
return register_defeq_simp_lemma_core(tctx, decl_name, ls, type, proof, priority);
}
void register_defeq_simp_lemma_core(tmp_type_context & tctx, name const & decl_name, levels const & umetas,
void register_defeq_simp_lemma_core(old_tmp_type_context & tctx, name const & decl_name, levels const & umetas,
expr const & type, expr const & proof, unsigned priority) {
m_decl_name_to_prio.insert(decl_name, priority);
expr rule = type;
@ -92,7 +92,7 @@ struct defeq_simp_lemmas_config {
typedef defeq_simp_lemmas_state state;
static void add_entry(environment const & env, io_state const & ios, state & s, entry const & e) {
tmp_type_context tctx(env, ios.get_options());
old_tmp_type_context tctx(env, ios.get_options());
s.register_defeq_simp_lemma(tctx, e.m_decl_name, e.m_priority);
}
static name const & get_class_name() {
@ -134,7 +134,7 @@ defeq_simp_lemmas get_defeq_simp_lemmas(environment const & env, name const & ns
if (_entries) {
list<defeq_simp_lemmas_entry> entries = reverse(*_entries);
for (auto const & e : entries) {
tmp_type_context tctx(env, get_dummy_ios().get_options());
old_tmp_type_context tctx(env, get_dummy_ios().get_options());
s.register_defeq_simp_lemma(tctx, e.m_decl_name, e.m_priority);
}
}

3
src/library/tactic/init_module.cpp
View file

@ -19,6 +19,7 @@ Author: Leonardo de Moura
#include "library/tactic/congr_lemma_tactics.h"
#include "library/tactic/elaborate.h"
#include "library/tactic/defeq_simplifier/init_module.h"
#include "library/tactic/simplifier/init_module.h"
namespace lean {
void initialize_tactic_module() {
@ -37,9 +38,11 @@ void initialize_tactic_module() {
initialize_congr_lemma_tactics();
initialize_elaborate();
initialize_defeq_simplifier_module();
initialize_simplifier_module();
}
void finalize_tactic_module() {
finalize_defeq_simplifier_module();
finalize_simplifier_module();
finalize_elaborate();
finalize_congr_lemma_tactics();
finalize_fun_info_tactics();

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

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

26
src/library/blast/simplifier/ceqv.cpp → src/library/tactic/simplifier/ceqv.cpp
View file

@ -10,10 +10,10 @@ Author: Leonardo de Moura
#include "library/constants.h"
#include "library/util.h"
#include "library/relation_manager.h"
#include "library/blast/simplifier/ceqv.h"
#include "library/tactic/simplifier/ceqv.h"
namespace lean {
bool is_ceqv(tmp_type_context & tctx, expr e);
bool is_ceqv(type_context & tctx, expr e);
bool is_simp_relation(environment const & env, name const & n) {
return is_trans_relation(env, n) && is_refl_relation(env, n);
@ -22,7 +22,7 @@ bool is_simp_relation(environment const & env, name const & n) {
/** \brief Auxiliary functional object for creating "conditional equations" */
class to_ceqvs_fn {
environment const & m_env;
tmp_type_context & m_tctx;
type_context & m_tctx;
static list<expr_pair> mk_singleton(expr const & e, expr const & H) {
return list<expr_pair>(mk_pair(e, H));
@ -41,7 +41,7 @@ class to_ceqvs_fn {
list<expr_pair> lift(expr const & local, list<expr_pair> const & l) {
lean_assert(is_local(local));
return map(l, [&](expr_pair const & e_H) {
return mk_pair(Pi(local, e_H.first), Fun(local, e_H.second));
return mk_pair(m_tctx.mk_pi({local}, e_H.first), m_tctx.mk_lambda({local}, e_H.second));
});
}
@ -66,8 +66,8 @@ class to_ceqvs_fn {
auto r2 = apply(arg2, H2, restricted);
return append(r1, r2);
} else if (is_pi(e)) {
// TODO(dhs): keep name?
expr local = m_tctx.mk_tmp_local(binding_domain(e), binding_info(e));
type_context::tmp_locals local_factory(m_tctx);
expr local = local_factory.push_local_from_binding(e);
expr new_e = instantiate(binding_body(e), local);
expr new_H = mk_app(H, local);
auto r = apply(new_e, new_H, restricted);
@ -82,8 +82,9 @@ class to_ceqvs_fn {
} else if (is_standard(m_env) && is_ite(e, c, Hdec, A, arg1, arg2) && is_prop(e)) {
// TODO(Leo): support HoTT mode if users request
expr not_c = mk_app(mk_constant(get_not_name()), c);
expr Hc = m_tctx.mk_tmp_local(c);
expr Hnc = m_tctx.mk_tmp_local(not_c);
type_context::tmp_locals local_factory(m_tctx);
expr Hc = local_factory.push_local(name(), c);
expr Hnc = local_factory.push_local(name(), not_c);
expr H1 = mk_app({mk_constant(get_implies_of_if_pos_name()),
c, arg1, arg2, Hdec, e, Hc});
expr H2 = mk_app({mk_constant(get_implies_of_if_neg_name()),
@ -109,7 +110,7 @@ class to_ceqvs_fn {
}
}
public:
to_ceqvs_fn(tmp_type_context & tctx):m_env(tctx.env()), m_tctx(tctx) {}
to_ceqvs_fn(type_context & tctx):m_env(tctx.env()), m_tctx(tctx) {}
list<expr_pair> operator()(expr const & e, expr const & H) {
bool restricted = false;
@ -118,7 +119,7 @@ public:
}
};
list<expr_pair> to_ceqvs(tmp_type_context & tctx, expr const & e, expr const & H) {
list<expr_pair> to_ceqvs(type_context & tctx, expr const & e, expr const & H) {
return to_ceqvs_fn(tctx)(e, H);
}
@ -140,7 +141,7 @@ bool is_simp_relation(environment const & env, expr const & e, expr & lhs, expr
return is_simp_relation(env, e, rel, lhs, rhs);
}
bool is_ceqv(tmp_type_context & tctx, expr e) {
bool is_ceqv(type_context & tctx, expr e) {
if (has_expr_metavar(e))
return false;
name_set to_find;
@ -158,6 +159,7 @@ bool is_ceqv(tmp_type_context & tctx, expr e) {
environment const & env = tctx.env();
bool is_std = is_standard(env);
buffer<expr> hypotheses; // arguments that are propositions
type_context::tmp_locals local_factory(tctx);
while (is_pi(e)) {
if (!to_find.empty()) {
// Support for dependent types.
@ -165,7 +167,7 @@ bool is_ceqv(tmp_type_context & tctx, expr e) {
// by matching the type.
for_each(binding_domain(e), visitor_fn);
}
expr local = tctx.mk_tmp_local(binding_domain(e));
expr local = local_factory.push_local(name(), binding_domain(e));
if (binding_info(e).is_inst_implicit()) {
// If the argument can be instantiated by type class resolution, then
// we don't need to find it in the lhs

6
src/library/blast/simplifier/ceqv.h → src/library/tactic/simplifier/ceqv.h
View file

@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "library/tmp_type_context.h"
#include "library/type_context.h"
#include "library/expr_pair.h"
namespace lean {
@ -14,7 +14,7 @@ bool is_simp_relation(environment const & env, expr const & e, expr & rel, expr
a "conditional" rewriting rule. Any equivalence relation registered using
the relation_manager is considered.
*/
list<expr_pair> to_ceqvs(tmp_type_context & tctx, expr const & e, expr const & H);
bool is_ceqv(tmp_type_context & tctx, expr e);
list<expr_pair> to_ceqvs(type_context & tctx, expr const & e, expr const & H);
bool is_ceqv(type_context & tctx, expr e);
bool is_permutation_ceqv(environment const & env, expr e);
}

10
src/library/blast/simplifier/init_module.cpp → src/library/tactic/simplifier/init_module.cpp
View file

@ -3,22 +3,18 @@ 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_lemmas.h"
#include "library/blast/simplifier/simplifier.h"
#include "library/tactic/simplifier/simp_lemmas.h"
#include "library/tactic/simplifier/simplifier.h"
namespace lean {
namespace blast {
void initialize_simplifier_module() {
initialize_simp_lemmas();
initialize_simplifier();
initialize_simplifier_actions();
}
void finalize_simplifier_module() {
finalize_simplifier_actions();
finalize_simplifier();
finalize_simp_lemmas();
}
}}
}

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

@ -6,8 +6,6 @@ Author: Daniel Selsam
#pragma once
namespace lean {
namespace blast {
void initialize_simplifier_module();
void finalize_simplifier_module();
}
}

225
src/library/blast/simplifier/simp_lemmas.cpp → src/library/tactic/simplifier/simp_lemmas.cpp
View file

@ -8,17 +8,21 @@ Author: Leonardo de Moura
#include <string>
#include "util/priority_queue.h"
#include "util/sstream.h"
#include "util/flet.h"
#include "kernel/error_msgs.h"
#include "kernel/find_fn.h"
#include "kernel/instantiate.h"
#include "library/trace.h"
#include "library/scoped_ext.h"
#include "library/attribute_manager.h"
#include "library/blast/blast.h"
#include "library/blast/simplifier/ceqv.h"
#include "library/blast/simplifier/simp_lemmas.h"
#include "library/type_context.h"
#include "library/tactic/tactic_state.h"
#include "library/tactic/simplifier/ceqv.h"
#include "library/tactic/simplifier/simp_lemmas.h"
namespace lean {
/* The environment extension */
static name * g_class_name = nullptr;
static std::string * g_key = nullptr;
@ -67,22 +71,29 @@ struct simp_config {
typedef scoped_ext<simp_config> simp_ext;
void validate_simp(environment const & env, io_state const & ios, name const & n);
void validate_congr(environment const & env, io_state const & ios, name const & n);
/* Validation */
LEAN_THREAD_VALUE(bool, g_throw_ex, false);
void validate_simp(type_context & tctx, name const & n);
void validate_congr(type_context & tctx, name const & n);
/* Registering simp/congr lemmas */
environment add_simp_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent) {
validate_simp(env, ios, c);
aux_type_context aux_ctx(env);
type_context & tctx = aux_ctx.get();
validate_simp(tctx, c);
return simp_ext::add_entry(env, ios, simp_entry(true, prio, c), ns, persistent);
}
environment add_congr_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent) {
validate_congr(env, ios, c);
aux_type_context aux_ctx(env);
type_context & tctx = aux_ctx.get();
validate_congr(tctx, c);
return simp_ext::add_entry(env, ios, simp_entry(false, prio, c), ns, persistent);
}
bool is_simp_lemma(environment const & env, name const & c) {
return simp_ext::get_state(env).m_simp_lemmas.contains(c);
}
/* Getters/checkers */
unsigned get_simp_lemma_priority(environment const & env, name const & n) {
if (auto r = simp_ext::get_state(env).m_simp_lemmas.get_prio(n))
@ -91,29 +102,22 @@ unsigned get_simp_lemma_priority(environment const & env, name const & n) {
return LEAN_DEFAULT_PRIORITY;
}
bool is_simp_lemma(environment const & env, name const & c) {
return simp_ext::get_state(env).m_simp_lemmas.contains(c);
}
bool is_congr_lemma(environment const & env, name const & c) {
return simp_ext::get_state(env).m_congr_lemmas.contains(c);
}
void get_simp_lemmas(environment const & env, buffer<name> & r) {
void get_simp_lemma_names(environment const & env, buffer<name> & r) {
return simp_ext::get_state(env).m_simp_lemmas.to_buffer(r);
}
void get_congr_lemmas(environment const & env, buffer<name> & r) {
void get_congr_lemma_names(environment const & env, buffer<name> & r) {
return simp_ext::get_state(env).m_congr_lemmas.to_buffer(r);
}
static std::vector<std::vector<name>> * g_simp_lemma_ns = nullptr;
unsigned register_simp_lemmas(std::initializer_list<name> const & nss) {
unsigned r = g_simp_lemma_ns->size();
g_simp_lemma_ns->push_back(std::vector<name>(nss));
return r;
}
namespace blast {
LEAN_THREAD_VALUE(bool, g_throw_ex, false);
static void report_failure(sstream const & strm) {
if (g_throw_ex){
throw exception(strm);
@ -123,26 +127,29 @@ static void report_failure(sstream const & strm) {
}
}
simp_lemmas add_core(tmp_type_context & tctx, simp_lemmas const & s,
simp_lemmas add_core(tmp_type_context & tmp_tctx, simp_lemmas const & s,
name const & id, levels const & univ_metas, expr const & e, expr const & h,
unsigned priority) {
list<expr_pair> ceqvs = to_ceqvs(tctx, e, h);
list<expr_pair> ceqvs = to_ceqvs(tmp_tctx.tctx(), e, h);
if (is_nil(ceqvs)) {
report_failure(sstream() << "invalid [simp] lemma '" << id << "'");
}
environment const & env = tctx.env();
environment const & env = tmp_tctx.tctx().env();
simp_lemmas new_s = s;
for (expr_pair const & p : ceqvs) {
expr rule = normalizer(tctx)(p.first);
expr proof = tctx.whnf(p.second);
/* We only clear the eassignment since we want to reuse the temporary universe metavariables associated
with the declaration. */
tmp_tctx.clear_eassignment();
expr rule = tmp_tctx.whnf(p.first);
expr proof = tmp_tctx.whnf(p.second);
bool is_perm = is_permutation_ceqv(env, rule);
buffer<expr> emetas;
buffer<bool> instances;
while (is_pi(rule)) {
expr mvar = tctx.mk_mvar(binding_domain(rule));
expr mvar = tmp_tctx.mk_tmp_mvar(binding_domain(rule));
emetas.push_back(mvar);
instances.push_back(binding_info(rule).is_inst_implicit());
rule = tctx.whnf(instantiate(binding_body(rule), mvar));
rule = tmp_tctx.whnf(instantiate(binding_body(rule), mvar));
proof = mk_app(proof, mvar);
}
expr rel, lhs, rhs;
@ -154,8 +161,9 @@ simp_lemmas add_core(tmp_type_context & tctx, simp_lemmas const & s,
return new_s;
}
simp_lemmas add(tmp_type_context & tctx, simp_lemmas const & s, name const & id, expr const & e, expr const & h, unsigned priority) {
return add_core(tctx, s, id, list<level>(), e, h, priority);
simp_lemmas add(type_context & tctx, simp_lemmas const & s, name const & id, expr const & e, expr const & h, unsigned priority) {
tmp_type_context tmp_tctx(tctx);
return add_core(tmp_tctx, s, id, list<level>(), e, h, priority);
}
simp_lemmas join(simp_lemmas const & s1, simp_lemmas const & s2) {
@ -166,17 +174,17 @@ simp_lemmas join(simp_lemmas const & s1, simp_lemmas const & s2) {
return new_s1;
}
static simp_lemmas add_core(tmp_type_context & tctx, simp_lemmas const & s, name const & cname, unsigned priority) {
declaration const & d = tctx.env().get(cname);
static simp_lemmas add_core(tmp_type_context & tmp_tctx, simp_lemmas const & s, name const & cname, unsigned priority) {
declaration const & d = tmp_tctx.tctx().env().get(cname);
buffer<level> us;
unsigned num_univs = d.get_num_univ_params();
for (unsigned i = 0; i < num_univs; i++) {
us.push_back(tctx.mk_uvar());
us.push_back(tmp_tctx.mk_tmp_univ_mvar());
}
levels ls = to_list(us);
expr e = tctx.whnf(instantiate_type_univ_params(d, ls));
expr e = tmp_tctx.whnf(instantiate_type_univ_params(d, ls));
expr h = mk_constant(cname, ls);
return add_core(tctx, s, cname, ls, e, h, priority);
return add_core(tmp_tctx, s, cname, ls, e, h, priority);
}
// Return true iff lhs is of the form (B (x : ?m1), ?m2) or (B (x : ?m1), ?m2 x),
@ -222,30 +230,30 @@ static bool is_valid_congr_hyp_rhs(expr const & rhs, name_set & found_mvars) {
return true;
}
simp_lemmas add_congr_core(tmp_type_context & tctx, simp_lemmas const & s, name const & n, unsigned prio) {
declaration const & d = tctx.env().get(n);
simp_lemmas add_congr_core(tmp_type_context & tmp_tctx, simp_lemmas const & s, name const & n, unsigned prio) {
declaration const & d = tmp_tctx.tctx().env().get(n);
buffer<level> us;
unsigned num_univs = d.get_num_univ_params();
for (unsigned i = 0; i < num_univs; i++) {
us.push_back(tctx.mk_uvar());
us.push_back(tmp_tctx.mk_tmp_univ_mvar());
}
levels ls = to_list(us);
expr rule = normalizer(tctx)(instantiate_type_univ_params(d, ls));
expr rule = tmp_tctx.whnf(instantiate_type_univ_params(d, ls));
expr proof = mk_constant(n, ls);
buffer<expr> emetas;
buffer<bool> instances, explicits;
while (is_pi(rule)) {
expr mvar = tctx.mk_mvar(binding_domain(rule));
expr mvar = tmp_tctx.mk_tmp_mvar(binding_domain(rule));
emetas.push_back(mvar);
explicits.push_back(is_explicit(binding_info(rule)));
instances.push_back(binding_info(rule).is_inst_implicit());
rule = tctx.whnf(instantiate(binding_body(rule), mvar));
rule = tmp_tctx.whnf(instantiate(binding_body(rule), mvar));
proof = mk_app(proof, mvar);
}
expr rel, lhs, rhs;
if (!is_simp_relation(tctx.env(), rule, rel, lhs, rhs) || !is_constant(rel)) {
if (!is_simp_relation(tmp_tctx.tctx().env(), rule, rel, lhs, rhs) || !is_constant(rel)) {
report_failure(sstream() << "invalid [congr] lemma, '" << n
<< "' resulting type is not of the form t ~ s, where '~' is a transitive and reflexive relation");
}
@ -292,13 +300,14 @@ simp_lemmas add_congr_core(tmp_type_context & tctx, simp_lemmas const & s, name
if (explicits[i] && !found_mvars.contains(mlocal_name(mvar))) {
buffer<expr> locals;
expr type = mlocal_type(mvar);
type_context::tmp_locals local_factory(tmp_tctx.tctx());
while (is_pi(type)) {
expr local = tctx.mk_tmp_local(binding_domain(type));
expr local = local_factory.push_local_from_binding(type);
locals.push_back(local);
type = instantiate(binding_body(type), local);
}
expr h_rel, h_lhs, h_rhs;
if (!is_simp_relation(tctx.env(), type, h_rel, h_lhs, h_rhs) || !is_constant(h_rel))
if (!is_simp_relation(tmp_tctx.tctx().env(), type, h_rel, h_lhs, h_rhs) || !is_constant(h_rel))
continue;
unsigned j = 0;
for (expr const & local : locals) {
@ -330,6 +339,20 @@ simp_lemmas add_congr_core(tmp_type_context & tctx, simp_lemmas const & s, name
return new_s;
}
void validate_simp(type_context & tctx, name const & n) {
simp_lemmas s;
flet<bool> set_ex(g_throw_ex, true);
tmp_type_context tmp_tctx(tctx);
add_core(tmp_tctx, s, n, LEAN_DEFAULT_PRIORITY);
}
void validate_congr(type_context & tctx, name const & n) {
simp_lemmas s;
flet<bool> set_ex(g_throw_ex, true);
tmp_type_context tmp_tctx(tctx);
add_congr_core(tmp_tctx, s, n, LEAN_DEFAULT_PRIORITY);
}
simp_lemma_core::simp_lemma_core(name const & id, levels const & umetas, list<expr> const & emetas,
list<bool> const & instances, expr const & lhs, expr const & rhs, expr const & proof,
unsigned priority):
@ -573,70 +596,43 @@ format simp_lemmas::pp(formatter const & fmt) const {
return pp(fmt, format(), true, true);
}
struct simp_lemmas_cache {
simp_lemmas m_main_cache;
std::vector<optional<simp_lemmas>> m_key_cache;
};
LEAN_THREAD_PTR(simp_lemmas_cache, g_simp_lemmas_cache);
scope_simp::scope_simp() {
m_old_cache = g_simp_lemmas_cache;
g_simp_lemmas_cache = nullptr;
}
scope_simp::~scope_simp() {
delete g_simp_lemmas_cache;
g_simp_lemmas_cache = m_old_cache;
}
simp_lemmas get_simp_lemmas_core() {
simp_lemmas get_simp_lemmas(environment const & env) {
simp_lemmas r;
buffer<name> simp_lemmas, congr_lemmas;
blast_tmp_type_context ctx;
auto const & s = simp_ext::get_state(env());
aux_type_context aux_ctx(env);
type_context & tctx = aux_ctx.get();
auto const & s = simp_ext::get_state(env);
s.m_simp_lemmas.to_buffer(simp_lemmas);
s.m_congr_lemmas.to_buffer(congr_lemmas);
unsigned i = simp_lemmas.size();
while (i > 0) {
--i;
ctx->clear();
r = add_core(*ctx, r, simp_lemmas[i], *s.m_simp_lemmas.get_prio(simp_lemmas[i]));
tmp_type_context tmp_tctx(tctx);
r = add_core(tmp_tctx, r, simp_lemmas[i], *s.m_simp_lemmas.get_prio(simp_lemmas[i]));
}
i = congr_lemmas.size();
while (i > 0) {
--i;
ctx->clear();
r = add_congr_core(*ctx, r, congr_lemmas[i], *s.m_congr_lemmas.get_prio(congr_lemmas[i]));
tmp_type_context tmp_tctx(tctx);
r = add_congr_core(tmp_tctx, r, congr_lemmas[i], *s.m_congr_lemmas.get_prio(congr_lemmas[i]));
}
return r;
}
static simp_lemmas_cache & get_cache() {
if (!g_simp_lemmas_cache) {
g_simp_lemmas_cache = new simp_lemmas_cache();
g_simp_lemmas_cache->m_main_cache = get_simp_lemmas_core();
}
return *g_simp_lemmas_cache;
}
simp_lemmas get_simp_lemmas() {
return get_cache().m_main_cache;
}
template<typename NSS>
simp_lemmas get_simp_lemmas_core(NSS const & nss) {
simp_lemmas get_simp_lemmas_core(environment const & env, NSS const & nss) {
simp_lemmas r;
blast_tmp_type_context ctx;
aux_type_context aux_ctx(env);
type_context & tctx = aux_ctx.get();
for (name const & ns : nss) {
list<simp_entry> const * entries = simp_ext::get_entries(env(), ns);
list<simp_entry> const * entries = simp_ext::get_entries(env, ns);
if (entries) {
for (auto const & e : *entries) {
bool is_simp; unsigned prio; name n;
std::tie(is_simp, prio, n) = e;
if (is_simp) {
ctx->clear();
r = add_core(*ctx, r, n, prio);
tmp_type_context tmp_tctx(tctx);
r = add_core(tmp_tctx, r, n, prio);
}
}
}
@ -644,44 +640,38 @@ simp_lemmas get_simp_lemmas_core(NSS const & nss) {
return r;
}
simp_lemmas get_simp_lemmas(std::initializer_list<name> const & nss) {
return get_simp_lemmas_core(nss);
simp_lemmas get_simp_lemmas(environment const & env, std::initializer_list<name> const & nss) {
return get_simp_lemmas_core(env, nss);
}
simp_lemmas get_simp_lemmas(name const & ns) {
return get_simp_lemmas({ns});
simp_lemmas get_simp_lemmas(environment const & env, name const & ns) {
return get_simp_lemmas(env, {ns});
}
simp_lemmas get_simp_lemmas(unsigned key) {
simp_lemmas_cache & cache = get_cache();
if (key >= g_simp_lemma_ns->size())
throw exception("invalid simp lemma cache key");
if (key >= cache.m_key_cache.size())
cache.m_key_cache.resize(key+1);
if (!cache.m_key_cache[key])
cache.m_key_cache[key] = get_simp_lemmas_core((*g_simp_lemma_ns)[key]);
return *cache.m_key_cache[key];
}
}
void validate_simp(environment const & env, io_state const & ios, name const & n) {
blast::simp_lemmas s;
tmp_type_context ctx(env, ios.get_options());
flet<bool> set_ex(blast::g_throw_ex, true);
blast::add_core(ctx, s, n, LEAN_DEFAULT_PRIORITY);
}
void validate_congr(environment const & env, io_state const & ios, name const & n) {
blast::simp_lemmas s;
tmp_type_context ctx(env, ios.get_options());
flet<bool> set_ex(blast::g_throw_ex, true);
blast::add_congr_core(ctx, s, n, LEAN_DEFAULT_PRIORITY);
vm_obj tactic_simp(vm_obj const & e, vm_obj const & s0) {
tactic_state const & s = to_tactic_state(s0);
try {
// TODO(dhs): use type_context_scope for this
metavar_context mctx_tmp = s.mctx();
type_context tctx = mk_type_context_for(s, mctx_tmp, transparency_mode::Reducible);
simp_lemmas lemmas = get_simp_lemmas(s.env());
expr target = *(s.get_main_goal());
// name rel = (is_standard(s.env()) && tctx.is_prop(target)) ? get_iff_name() : get_eq_name();
name rel = get_iff_name();
simp_result result = simplify(tctx, rel, lemmas, to_expr(e));
if (result.has_proof()) {
return mk_tactic_success(mk_vm_pair(to_obj(result.get_new()), to_obj(result.get_proof())), s);
} else {
return mk_tactic_exception("simp tactic failed to simplify", s);
}
} catch (exception & e) {
return mk_tactic_exception(e, s);
}
}
void initialize_simp_lemmas() {
g_class_name = new name("simp");
g_key = new std::string("SIMP");
g_simp_lemma_ns = new std::vector<std::vector<name>>();
simp_ext::initialize();
register_prio_attribute("simp", "simplification lemma",
@ -704,13 +694,12 @@ void initialize_simp_lemmas() {
return LEAN_DEFAULT_PRIORITY;
});
blast::g_simp_lemmas_cache = nullptr;
DECLARE_VM_BUILTIN(name({"tactic", "simplify"}), tactic_simp);
}
void finalize_simp_lemmas() {
simp_ext::finalize();
delete g_key;
delete g_class_name;
delete g_simp_lemma_ns;
}
}

27
src/library/blast/simplifier/simp_lemmas.h → src/library/tactic/simplifier/simp_lemmas.h
View file

@ -7,25 +7,26 @@ Author: Leonardo de Moura
#pragma once
#include "kernel/environment.h"
#include "library/io_state.h"
#include "library/tmp_type_context.h"
#include "library/type_context.h"
#include "library/head_map.h"
#include "library/blast/gexpr.h"
namespace lean {
environment add_simp_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent);
environment add_congr_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent);
unsigned get_simp_lemma_priority(environment const & env, name const & n);
bool is_simp_lemma(environment const & env, name const & n);
bool is_congr_lemma(environment const & env, name const & n);
void get_simp_lemmas(environment const & env, buffer<name> & r);
void get_congr_lemmas(environment const & env, buffer<name> & r);
void get_simp_lemma_names(environment const & env, buffer<name> & r);
void get_congr_lemma_names(environment const & env, buffer<name> & r);
void initialize_simp_lemmas();
void finalize_simp_lemmas();
/** Generate a unique id for a set of namespaces containing [simp] and [congr] lemmas */
unsigned register_simp_lemmas(std::initializer_list<name> const & nss);
namespace blast {
class simp_lemmas;
class simp_lemma_core {
protected:
@ -66,7 +67,7 @@ class simp_lemma : public simp_lemma_core {
list<bool> const & instances, expr const & lhs, expr const & rhs, expr const & proof,
bool is_perm, unsigned priority);
friend simp_lemmas add_core(tmp_type_context & tctx, simp_lemmas const & s, name const & id,
friend simp_lemmas add_core(tmp_type_context & tmp_tctx, simp_lemmas const & s, name const & id,
levels const & univ_metas, expr const & e, expr const & h, unsigned priority);
public:
friend bool operator==(simp_lemma const & r1, simp_lemma const & r2);
@ -154,19 +155,11 @@ public:
~scope_simp();
};
simp_lemmas add(tmp_type_context & tctx, simp_lemmas const & s, name const & id, expr const & e, expr const & h, unsigned priority);
simp_lemmas add(type_context & tctx, simp_lemmas const & s, name const & id, expr const & e, expr const & h, unsigned priority);
simp_lemmas join(simp_lemmas const & s1, simp_lemmas const & s2);
/** \brief Get (active) simplification lemmas. */
simp_lemmas get_simp_lemmas();
simp_lemmas get_simp_lemmas(environment const & env);
/** \brief Get simplification lemmas in the given namespace. */
simp_lemmas get_simp_lemmas(name const & ns);
/** \brief Get simplification lemmas in the given namespaces. */
// simp_lemmas get_simp_lemmas(std::initializer_list<name> const & nss);
/** \brief Get simplification lemmas in the namespaces registered at key.
The key is created using procedure #register_simp_lemmas at initialization time.
This is more efficient than get_simp_lemmas(std::initializer_list<name> const & nss), because
results are cached. */
simp_lemmas get_simp_lemmas(unsigned key);
}
simp_lemmas get_simp_lemmas(environment const & env, name const & ns);
}

807
src/library/tactic/simplifier/simplifier.cpp Normal file
View file

@ -0,0 +1,807 @@
/*
Copyright (c) 2015 Daniel Selsam. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Daniel Selsam
*/
#include <functional>
#include <iostream>
#include "util/flet.h"
#include "util/freset.h"
#include "util/pair.h"
#include "util/optional.h"
#include "util/interrupt.h"
#include "util/sexpr/option_declarations.h"
#include "kernel/abstract.h"
#include "kernel/expr_maps.h"
#include "kernel/instantiate.h"
#include "library/trace.h"
#include "library/constants.h"
#include "library/normalize.h"
#include "library/expr_lt.h"
#include "library/num.h"
#include "library/util.h"
#include "library/norm_num.h"
#include "library/attribute_manager.h"
#include "library/class_instance_resolution.h"
#include "library/relation_manager.h"
#include "library/app_builder.h"
#include "library/congr_lemma.h"
#include "library/fun_info.h"
#include "library/tactic/simplifier/simplifier.h"
#include "library/tactic/simplifier/simp_lemmas.h"
#include "library/tactic/simplifier/ceqv.h"
#include "library/tactic/app_builder_tactics.h"
#ifndef LEAN_DEFAULT_SIMPLIFY_MAX_STEPS
#define LEAN_DEFAULT_SIMPLIFY_MAX_STEPS 1000
#endif
#ifndef LEAN_DEFAULT_SIMPLIFY_TOP_DOWN
#define LEAN_DEFAULT_SIMPLIFY_TOP_DOWN false
#endif
#ifndef LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE
#define LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE true
#endif
#ifndef LEAN_DEFAULT_SIMPLIFY_MEMOIZE
#define LEAN_DEFAULT_SIMPLIFY_MEMOIZE true
#endif
#ifndef LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL
#define LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL true
#endif
#ifndef LEAN_DEFAULT_SIMPLIFY_NUMERALS
#define LEAN_DEFAULT_SIMPLIFY_NUMERALS false
#endif
namespace lean {
/* Options */
static name * g_simplify_max_steps = nullptr;
static name * g_simplify_top_down = nullptr;
static name * g_simplify_exhaustive = nullptr;
static name * g_simplify_memoize = nullptr;
static name * g_simplify_contextual = nullptr;
static name * g_simplify_numerals = nullptr;
unsigned get_simplify_max_steps(options const & o) {
return o.get_unsigned(*g_simplify_max_steps, LEAN_DEFAULT_SIMPLIFY_MAX_STEPS);
}
bool get_simplify_top_down(options const & o) {
return o.get_bool(*g_simplify_top_down, LEAN_DEFAULT_SIMPLIFY_TOP_DOWN);
}
bool get_simplify_exhaustive(options const & o) {
return o.get_bool(*g_simplify_exhaustive, LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE);
}
bool get_simplify_memoize(options const & o) {
return o.get_bool(*g_simplify_memoize, LEAN_DEFAULT_SIMPLIFY_MEMOIZE);
}
bool get_simplify_contextual(options const & o) {
return o.get_bool(*g_simplify_contextual, LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL);
}
bool get_simplify_numerals(options const & o) {
return o.get_bool(*g_simplify_numerals, LEAN_DEFAULT_SIMPLIFY_NUMERALS);
}
/* Main simplifier class */
class simplifier {
type_context m_tctx;
name m_rel;
simp_lemmas m_slss;
simp_lemmas m_ctx_slss;
/* Logging */
unsigned m_num_steps{0};
/* Options */
unsigned m_max_steps;
bool m_top_down;
bool m_exhaustive;
bool m_memoize;
bool m_contextual;
bool m_numerals;
/* Cache */
struct key {
name m_rel;
expr m_e;
unsigned m_hash;
key(name const & rel, expr const & e):
m_rel(rel), m_e(e), m_hash(hash(rel.hash(), e.hash())) { }
};
struct key_hash_fn {
unsigned operator()(key const & k) const { return k.m_hash; }
};
struct key_eq_fn {
bool operator()(key const & k1, key const & k2) const {
return k1.m_rel == k2.m_rel && k1.m_e == k2.m_e;
}
};
typedef std::unordered_map<key, simp_result, key_hash_fn, key_eq_fn> simplify_cache;
simplify_cache m_cache;
optional<simp_result> cache_lookup(expr const & e);
void cache_save(expr const & e, simp_result const & r);
/* Basic helpers */
bool using_eq() { return m_rel == get_eq_name(); }
bool is_dependent_fn(expr const & f) {
expr f_type = m_tctx.whnf(m_tctx.infer(f));
lean_assert(is_pi(f_type));
return has_free_vars(binding_body(f_type));
}
simp_lemmas add_to_slss(simp_lemmas const & _slss, buffer<expr> const & ls) {
simp_lemmas slss = _slss;
for (unsigned i = 0; i < ls.size(); i++) {
expr const & l = ls[i];
try {
// TODO(Leo,Daniel): should we allow the user to set the priority of local lemmas?
slss = add(m_tctx, slss, mlocal_name(l), m_tctx.infer(l), l, LEAN_DEFAULT_PRIORITY);
} catch (exception e) {
}
}
return slss;
}
bool instantiate_emetas(tmp_type_context & tmp_tctx, unsigned num_emeta, list<expr> const & emetas, list<bool> const & instances);
/* Simp_Results */
simp_result lift_from_eq(expr const & e_old, simp_result const & r_eq);
simp_result join(simp_result const & r1, simp_result const & r2);
simp_result finalize(simp_result const & r);
/* Simplification */
simp_result simplify(expr const & e);
simp_result simplify_lambda(expr const & e);
simp_result simplify_pi(expr const & e);
simp_result simplify_app(expr const & e);
simp_result simplify_fun(expr const & e);
optional<simp_result> simplify_numeral(expr const & e);
/* Proving */
optional<expr> prove(expr const & thm);
/* Rewriting */
simp_result rewrite(expr const & e);
simp_result rewrite(expr const & e, simp_lemmas const & slss);
simp_result rewrite(expr const & e, simp_lemma const & sr);
/* Congruence */
simp_result congr_fun_arg(simp_result const & r_f, simp_result const & r_arg);
simp_result congr(simp_result const & r_f, simp_result const & r_arg);
simp_result congr_fun(simp_result const & r_f, expr const & arg);
simp_result congr_arg(expr const & f, simp_result const & r_arg);
simp_result congr_funs(simp_result const & r_f, buffer<expr> const & args);
simp_result try_congrs(expr const & e);
simp_result try_congr(expr const & e, user_congr_lemma const & cr);
template<typename F>
optional<simp_result> synth_congr(expr const & e, F && simp);
expr remove_unnecessary_casts(expr const & e);
/* Apply whnf and eta-reduction
\remark We want (Sum n (fun x, f x)) and (Sum n f) to be the same.
\remark We may want to switch to eta-expansion later (see paper: "The Virtues of Eta-expansion").
TODO(Daniel, Leo): should we add an option for disabling/enabling eta? */
expr whnf_eta(expr const & e);
public:
simplifier(type_context & tctx, name const & rel, simp_lemmas const & slss):
m_tctx(tctx), m_rel(rel), m_slss(slss),
/* Options */
m_max_steps(get_simplify_max_steps(tctx.get_options())),
m_top_down(get_simplify_top_down(tctx.get_options())),
m_exhaustive(get_simplify_exhaustive(tctx.get_options())),
m_memoize(get_simplify_memoize(tctx.get_options())),
m_contextual(get_simplify_contextual(tctx.get_options())),
m_numerals(get_simplify_numerals(tctx.get_options()))
{ }
simp_result operator()(expr const & e) { return simplify(e); }
};
/* Cache */
optional<simp_result> simplifier::cache_lookup(expr const & e) {
auto it = m_cache.find(key(m_rel, e));
if (it == m_cache.end()) return optional<simp_result>();
return optional<simp_result>(it->second);
}
void simplifier::cache_save(expr const & e, simp_result const & r) {
m_cache.insert(mk_pair(key(m_rel, e), r));
}
/* Simp_Results */
simp_result simplifier::lift_from_eq(expr const & e_old, simp_result const & r_eq) {
if (!r_eq.has_proof()) return r_eq;
lean_assert(r_eq.has_proof());
/* r_eq.get_proof() : e_old = r_eq.get_new() */
/* goal : e_old <m_rel> r_eq.get_new() */
type_context::tmp_locals local_factory(m_tctx);
expr local = local_factory.push_local(name(), m_tctx.infer(e_old));
expr motive_local = mk_app(m_tctx, m_rel, e_old, local);
/* motive = fun y, e_old <m_rel> y */
expr motive = local_factory.mk_lambda(motive_local);
/* Rxx = x <m_rel> x */
expr Rxx = mk_refl(m_tctx, m_rel, e_old);
expr pf = mk_eq_rec(m_tctx, motive, Rxx, r_eq.get_proof());
return simp_result(r_eq.get_new(), pf);
}
simp_result simplifier::join(simp_result const & r1, simp_result const & r2) {
/* Assumes that both simp_results are with respect to the same relation */
if (!r1.has_proof()) {
return r2;
} else if (!r2.has_proof()) {
lean_assert(r1.has_proof());
return simp_result(r2.get_new(), r1.get_proof());
} else {
/* If they both have proofs, we need to glue them together with transitivity. */
lean_assert(r1.has_proof() && r2.has_proof());
lean_trace(name({"simplifier"}),
expr pf1_type = m_tctx.infer(r1.get_proof());
expr pf2_type = m_tctx.infer(r2.get_proof());
tout() << "JOIN(" << r1.get_proof() << " : " << pf1_type
<< ", " << r2.get_proof() << " : " << pf2_type << ")\n";);
expr trans = mk_trans(m_tctx, m_rel, r1.get_proof(), r2.get_proof());
return simp_result(r2.get_new(), trans);
}
}
/* Whnf + Eta */
expr simplifier::whnf_eta(expr const & e) {
return try_eta(m_tctx.whnf(e));
}
/* Simplification */
simp_result simplifier::simplify(expr const & e) {
check_system("simplifier");
m_num_steps++;
lean_trace_inc_depth("simplifier");
lean_trace_d("simplifier", tout() << m_rel << ": " << e << "\n";);
if (m_num_steps > m_max_steps)
throw exception("simplifier failed, maximum number of steps exceeded");
if (m_memoize) {
if (auto it = cache_lookup(e)) return *it;
}
if (m_numerals && using_eq()) {
if (auto r = simplify_numeral(e)) {
return *r;
}
}
simp_result r(e);
if (m_top_down) r = join(r, rewrite(whnf_eta(r.get_new())));
r.update(whnf_eta(r.get_new()));
switch (r.get_new().kind()) {
case expr_kind::Local:
case expr_kind::Meta:
case expr_kind::Sort:
case expr_kind::Constant:
// no-op
break;
case expr_kind::Var:
lean_unreachable();
case expr_kind::Macro:
break;
case expr_kind::Lambda:
if (using_eq()) r = join(r, simplify_lambda(r.get_new()));
break;
case expr_kind::Pi:
r = join(r, simplify_pi(r.get_new()));
break;
case expr_kind::App:
r = join(r, simplify_app(r.get_new()));
break;
case expr_kind::Let:
// whnf unfolds let-expressions
lean_unreachable();
}
if (!m_top_down) r = join(r, rewrite(whnf_eta(r.get_new())));
if (r.get_new() == e && !using_eq()) {
simp_result r_eq;
{
flet<name> use_eq(m_rel, get_eq_name());
r_eq = simplify(r.get_new());
}
r = join(r, lift_from_eq(r.get_new(), r_eq));
}
if (m_exhaustive && r.has_proof()) r = join(r, simplify(r.get_new()));
if (m_memoize) cache_save(e, r);
return r;
}
simp_result simplifier::simplify_lambda(expr const & e) {
lean_assert(is_lambda(e));
expr t = e;
type_context::tmp_locals local_factory(m_tctx);
expr l = local_factory.push_local_from_binding(t);
t = instantiate(binding_body(t), l);
simp_result r = simplify(t);
expr new_t = local_factory.mk_lambda(r.get_new());
if (r.has_proof()) {
expr lam_pf = local_factory.mk_lambda(r.get_proof());
expr funext_pf = mk_app(m_tctx, get_funext_name(), lam_pf);
return simp_result(new_t, funext_pf);
} else {
return simp_result(new_t);
}
}
simp_result simplifier::simplify_pi(expr const & e) {
lean_assert(is_pi(e));
return try_congrs(e);
}
simp_result simplifier::simplify_app(expr const & _e) {
lean_assert(is_app(_e));
// TODO(dhs): normalize instances and subsingletons
expr e = _e;
// (1) Try user-defined congruences
simp_result r_user = try_congrs(e);
if (r_user.has_proof()) {
if (using_eq()) return join(r_user, simplify_fun(r_user.get_new()));
else return r_user;
}
// TODO(dhs): (2) Synthesize congruence lemma
// (3) Fall back on generic binary congruence
if (using_eq()) {
expr const & f = app_fn(e);
expr const & arg = app_arg(e);
simp_result r_f = simplify(f);
if (is_dependent_fn(f)) {
if (r_f.has_proof()) return congr_fun(r_f, arg);
else return mk_app(r_f.get_new(), arg);
} else {
simp_result r_arg = simplify(arg);
return congr_fun_arg(r_f, r_arg);
}
}
return simp_result(e);
}
simp_result simplifier::simplify_fun(expr const & e) {
lean_assert(is_app(e));
buffer<expr> args;
expr const & f = get_app_args(e, args);
simp_result r_f = simplify(f);
return congr_funs(r_f, args);
}
optional<simp_result> simplifier::simplify_numeral(expr const & e) {
if (is_num(e)) { return optional<simp_result>(simp_result(e)); }
try {
expr_pair r = mk_norm_num(m_tctx, e);
return optional<simp_result>(simp_result(r.first, r.second));
} catch (exception e) {
return optional<simp_result>();
}
}
/* Proving */
simp_result simplifier::finalize(simp_result const & r) {
if (r.has_proof()) return r;
expr pf = mk_refl(m_tctx, m_rel, r.get_new());
return simp_result(r.get_new(), pf);
}
optional<expr> simplifier::prove(expr const & thm) {
flet<name> set_name(m_rel, get_iff_name());
simp_result r_cond = simplify(thm);
if (is_constant(r_cond.get_new()) && const_name(r_cond.get_new()) == get_true_name()) {
expr pf = mk_app(m_tctx, get_iff_elim_right_name(),
finalize(r_cond).get_proof(),
mk_constant(get_true_intro_name()));
return some_expr(pf);
}
return none_expr();
}
/* Rewriting */
simp_result simplifier::rewrite(expr const & e) {
simp_result r(e);
while (true) {
simp_result r_ctx = rewrite(r.get_new(), m_ctx_slss);
simp_result r_new = rewrite(r_ctx.get_new(), m_slss);
if (!r_ctx.has_proof() && !r_new.has_proof()) break;
r = join(join(r, r_ctx), r_new);
}
return r;
}
simp_result simplifier::rewrite(expr const & e, simp_lemmas const & slss) {
simp_result r(e);
simp_lemmas_for const * sr = slss.find(m_rel);
if (!sr) return r;
list<simp_lemma> const * srs = sr->find_simp(e);
if (!srs) {
lean_trace(name({"simplifier", "try_rewrite"}), tout() << "no simp lemmas for: " << e << "\n";);
return r;
}
for_each(*srs, [&](simp_lemma const & sr) {
simp_result r_new = rewrite(r.get_new(), sr);
if (!r_new.has_proof()) return;
r = join(r, r_new);
});
return r;
}
simp_result simplifier::rewrite(expr const & e, simp_lemma const & sl) {
tmp_type_context tmp_tctx(m_tctx, sl.get_num_umeta(), sl.get_num_emeta());
lean_trace(name({"simplifier", "try_rewrite"}), tout() << e << " =?= " << sl.get_lhs() << "\n";);
if (!tmp_tctx.is_def_eq(e, sl.get_lhs())) return simp_result(e);
lean_trace(name({"simplifier", "rewrite"}),
expr new_lhs = tmp_tctx.instantiate_mvars(sl.get_lhs());
expr new_rhs = tmp_tctx.instantiate_mvars(sl.get_rhs());
tout() << "(" << sl.get_id() << ") "
<< "[" << new_lhs << " --> " << new_rhs << "]\n";);
if (!instantiate_emetas(tmp_tctx, sl.get_num_emeta(), sl.get_emetas(), sl.get_instances())) return simp_result(e);
for (unsigned i = 0; i < sl.get_num_umeta(); i++) {
if (!tmp_tctx.is_uassigned(i)) return simp_result(e);
}
expr new_lhs = tmp_tctx.instantiate_mvars(sl.get_lhs());
expr new_rhs = tmp_tctx.instantiate_mvars(sl.get_rhs());
if (sl.is_perm()) {
// TODO(dhs): restore light-lt
if (!is_lt(new_rhs, new_lhs, false)) {
lean_trace(name({"simplifier", "perm"}),
tout() << "perm rejected: " << new_rhs << " !< " << new_lhs << "\n";);
return simp_result(e);
}
}
expr pf = tmp_tctx.instantiate_mvars(sl.get_proof());
return simp_result(new_rhs, pf);
}
/* Congruence */
simp_result simplifier::congr_fun_arg(simp_result const & r_f, simp_result const & r_arg) {
if (!r_f.has_proof() && !r_arg.has_proof()) return simp_result(mk_app(r_f.get_new(), r_arg.get_new()));
else if (!r_f.has_proof()) return congr_arg(r_f.get_new(), r_arg);
else if (!r_arg.has_proof()) return congr_fun(r_f, r_arg.get_new());
else return congr(r_f, r_arg);
}
simp_result simplifier::congr(simp_result const & r_f, simp_result const & r_arg) {
lean_assert(r_f.has_proof() && r_arg.has_proof());
// theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂
expr e = mk_app(r_f.get_new(), r_arg.get_new());
expr pf = mk_congr(m_tctx, r_f.get_proof(), r_arg.get_proof());
return simp_result(e, pf);
}
simp_result simplifier::congr_fun(simp_result const & r_f, expr const & arg) {
lean_assert(r_f.has_proof());
// theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a
expr e = mk_app(r_f.get_new(), arg);
expr pf = mk_congr_fun(m_tctx, r_f.get_proof(), arg);
return simp_result(e, pf);
}
simp_result simplifier::congr_arg(expr const & f, simp_result const & r_arg) {
lean_assert(r_arg.has_proof());
// theorem congr_arg {A B : Type} {a₁ a₂ : A} (f : A → B) : a₁ = a₂ → f a₁ = f a₂
expr e = mk_app(f, r_arg.get_new());
expr pf = mk_congr_arg(m_tctx, f, r_arg.get_proof());
return simp_result(e, pf);
}
/* Note: handles reflexivity */
simp_result simplifier::congr_funs(simp_result const & r_f, buffer<expr> const & args) {
// congr_fun : ∀ {A : Type} {B : A → Type} {f g : Π (x : A), B x}, f = g → (∀ (a : A), f a = g a)
expr e = r_f.get_new();
for (unsigned i = 0; i < args.size(); ++i) {
e = mk_app(e, args[i]);
}
if (!r_f.has_proof()) return simp_result(e);
expr pf = r_f.get_proof();
for (unsigned i = 0; i < args.size(); ++i) {
pf = mk_app(m_tctx, get_congr_fun_name(), pf, args[i]);
}
return simp_result(e, pf);
}
simp_result simplifier::try_congrs(expr const & e) {
simp_lemmas_for const * sls = m_slss.find(m_rel);
if (!sls) return simp_result(e);
list<user_congr_lemma> const * cls = sls->find_congr(e);
if (!cls) return simp_result(e);
simp_result r(e);
for_each(*cls, [&](user_congr_lemma const & cl) {
if (r.has_proof()) return;
r = try_congr(e, cl);
});
return r;
}
simp_result simplifier::try_congr(expr const & e, user_congr_lemma const & cl) {
tmp_type_context tmp_tctx(m_tctx, cl.get_num_umeta(), cl.get_num_emeta());
if (!tmp_tctx.is_def_eq(e, cl.get_lhs())) return simp_result(e);
lean_trace(name({"simplifier", "congruence"}),
expr new_lhs = tmp_tctx.instantiate_mvars(cl.get_lhs());
expr new_rhs = tmp_tctx.instantiate_mvars(cl.get_rhs());
diagnostic(m_tctx.env(), get_dummy_ios(), m_tctx)
<< "(" << cl.get_id() << ") "
<< "[" << new_lhs << " =?= " << new_rhs << "]\n";);
/* First, iterate over the congruence hypotheses */
bool failed = false;
bool simplified = false;
list<expr> const & congr_hyps = cl.get_congr_hyps();
for_each(congr_hyps, [&](expr const & m) {
if (failed) return;
type_context::tmp_locals local_factory(m_tctx);
expr m_type = tmp_tctx.instantiate_mvars(tmp_tctx.infer(m));
while (is_pi(m_type)) {
expr l = local_factory.push_local_from_binding(m_type);
lean_assert(!has_metavar(l));
m_type = instantiate(binding_body(m_type), l);
}
expr h_rel, h_lhs, h_rhs;
lean_verify(is_simp_relation(m_tctx.env(), m_type, h_rel, h_lhs, h_rhs) && is_constant(h_rel));
{
flet<name> set_name(m_rel, const_name(h_rel));
flet<simp_lemmas> set_ctx_slss(m_ctx_slss, m_contextual ? add_to_slss(m_ctx_slss, local_factory.as_buffer()) : m_ctx_slss);
h_lhs = tmp_tctx.instantiate_mvars(h_lhs);
lean_assert(!has_metavar(h_lhs));
// TODO(dhs): freset cache?
simp_result r_congr_hyp = simplify(h_lhs);
if (r_congr_hyp.has_proof()) simplified = true;
r_congr_hyp = finalize(r_congr_hyp);
expr hyp = finalize(r_congr_hyp).get_proof();
if (!tmp_tctx.is_def_eq(m, local_factory.mk_lambda(hyp))) failed = true;
}
});
if (failed || !simplified) return simp_result(e);
if (!instantiate_emetas(tmp_tctx, cl.get_num_emeta(), cl.get_emetas(), cl.get_instances())) return simp_result(e);
for (unsigned i = 0; i < cl.get_num_umeta(); i++) {
if (!tmp_tctx.is_uassigned(i)) return simp_result(e);
}
expr e_s = tmp_tctx.instantiate_mvars(cl.get_rhs());
expr pf = tmp_tctx.instantiate_mvars(cl.get_proof());
return simp_result(e_s, pf);
}
bool simplifier::instantiate_emetas(tmp_type_context & tmp_tctx, unsigned num_emeta, list<expr> const & emetas, list<bool> const & instances) {
bool failed = false;
unsigned i = num_emeta;
for_each2(emetas, instances, [&](expr const & m, bool const & is_instance) {
i--;
if (failed) return;
expr m_type = tmp_tctx.instantiate_mvars(m_tctx.infer(m));
lean_assert(!has_metavar(m_type));
if (tmp_tctx.is_eassigned(i)) return;
if (is_instance) {
if (auto v = m_tctx.mk_class_instance(m_type)) {
if (!tmp_tctx.is_def_eq(m, *v)) {
lean_trace(name({"simplifier", "failure"}),
tout() << "unable to assign instance for: " << m_type << "\n";);
failed = true;
return;
}
} else {
lean_trace(name({"simplifier", "failure"}),
tout() << "unable to synthesize instance for: " << m_type << "\n";);
failed = true;
return;
}
}
if (tmp_tctx.is_eassigned(i)) return;
if (m_tctx.is_prop(m_type)) {
if (auto pf = prove(m_type)) {
lean_verify(tmp_tctx.is_def_eq(m, *pf));
return;
}
}
lean_trace(name({"simplifier", "failure"}),
tout() << "failed to assign: " << m << " : " << m_type << "\n";);
failed = true;
return;
});
return !failed;
}
template<typename F>
optional<simp_result> simplifier::synth_congr(expr const & e, F && simp) {
static_assert(std::is_same<typename std::result_of<F(expr const & e)>::type, simp_result>::value,
"synth_congr: simp must take expressions to simp_results");
lean_assert(is_app(e));
buffer<expr> args;
expr f = get_app_args(e, args);
auto congr_lemma = mk_specialized_congr_simp(m_tctx, e);
if (!congr_lemma) return optional<simp_result>();
expr proof = congr_lemma->get_proof();
expr type = congr_lemma->get_type();
unsigned i = 0;
bool has_proof = false;
bool has_cast = false;
for_each(congr_lemma->get_arg_kinds(), [&](congr_arg_kind const & ckind) {
switch (ckind) {
case congr_arg_kind::HEq:
lean_unreachable();
case congr_arg_kind::Fixed:
proof = mk_app(proof, args[i]);
type = instantiate(binding_body(type), args[i]);
break;
case congr_arg_kind::FixedNoParam:
break;
case congr_arg_kind::Eq:
proof = mk_app(proof, args[i]);
type = instantiate(binding_body(type), args[i]);
{
simp_result r_arg = simp(args[i]);
if (r_arg.has_proof()) has_proof = true;
r_arg = finalize(r_arg);
proof = mk_app(proof, r_arg.get_new(), r_arg.get_proof());
type = instantiate(binding_body(type), r_arg.get_new());
type = instantiate(binding_body(type), r_arg.get_proof());
}
break;
case congr_arg_kind::Cast:
proof = mk_app(proof, args[i]);
type = instantiate(binding_body(type), args[i]);
has_cast = true;
break;
}
i++;
});
lean_assert(is_eq(type));
buffer<expr> type_args;
get_app_args(type, type_args);
expr e_new = remove_unnecessary_casts(type_args[2]);
simp_result r;
if (has_proof) r = simp_result(e_new, proof);
else r = simp_result(e_new);
/* TODO(dhs): re-integrate
if (has_cast) {
if (auto r_norm = normalize_subsingleton_args(e_new))
r = join(r, *r_norm);
}
*/
return optional<simp_result>(r);
}
expr simplifier::remove_unnecessary_casts(expr const & e) {
buffer<expr> args;
expr f = get_app_args(e, args);
fun_info f_info = get_specialized_fun_info(m_tctx, e);
int i = -1;
for_each(f_info.get_params_info(), [&](param_info const & p_info) {
i++;
if (p_info.is_subsingleton()) {
while (is_constant(get_app_fn(args[i]))) {
buffer<expr> cast_args;
expr f_cast = get_app_args(args[i], cast_args);
name n_f = const_name(f_cast);
if (n_f == get_eq_rec_name() || n_f == get_eq_drec_name() || n_f == get_eq_nrec_name()) {
lean_assert(cast_args.size() == 6);
expr major_premise = cast_args[5];
expr f_major_premise = get_app_fn(major_premise);
if (is_constant(f_major_premise) && const_name(f_major_premise) == get_eq_refl_name())
args[i] = cast_args[3];
else
return;
} else {
return;
}
}
}
});
return mk_app(f, args);
}
/* Setup and teardown */
void initialize_simplifier() {
register_trace_class("simplifier");
register_trace_class(name({"simplifier", "rewrite"}));
register_trace_class(name({"simplifier", "congruence"}));
register_trace_class(name({"simplifier", "failure"}));
register_trace_class(name({"simplifier", "perm"}));
register_trace_class(name({"simplifier", "try_rewrite"}));
g_simplify_max_steps = new name{"simplify", "max_steps"};
g_simplify_top_down = new name{"simplify", "top_down"};
g_simplify_exhaustive = new name{"simplify", "exhaustive"};
g_simplify_memoize = new name{"simplify", "memoize"};
g_simplify_contextual = new name{"simplify", "contextual"};
g_simplify_numerals = new name{"simplify", "numerals"};
register_unsigned_option(*g_simplify_max_steps, LEAN_DEFAULT_SIMPLIFY_MAX_STEPS,
"(simplify) max allowed steps in simplification");
register_bool_option(*g_simplify_top_down, LEAN_DEFAULT_SIMPLIFY_TOP_DOWN,
"(simplify) use top-down rewriting instead of bottom-up");
register_bool_option(*g_simplify_exhaustive, LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE,
"(simplify) rewrite exhaustively");
register_bool_option(*g_simplify_memoize, LEAN_DEFAULT_SIMPLIFY_MEMOIZE,
"(simplify) memoize simplifications");
register_bool_option(*g_simplify_contextual, LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL,
"(simplify) use contextual simplification");
register_bool_option(*g_simplify_numerals, LEAN_DEFAULT_SIMPLIFY_NUMERALS,
"(simplify) simplify (+, *, -, /) over numerals");
}
void finalize_simplifier() {
delete g_simplify_numerals;
delete g_simplify_contextual;
delete g_simplify_memoize;
delete g_simplify_exhaustive;
delete g_simplify_top_down;
delete g_simplify_max_steps;
}
/* Entry point */
simp_result simplify(type_context & ctx, name const & rel, simp_lemmas const & simp_lemmas, expr const & e) {
return simplifier(ctx, rel, simp_lemmas)(e);
}
}

27
src/library/blast/simplifier/simplifier.h → src/library/tactic/simplifier/simplifier.h
View file

@ -5,27 +5,22 @@ Author: Daniel Selsam
*/
#pragma once
#include "kernel/expr_pair.h"
#include "library/blast/state.h"
#include "library/blast/simplifier/simp_lemmas.h"
#include "library/type_context.h"
#include "library/tactic/simplifier/simp_lemmas.h"
namespace lean {
namespace blast {
namespace simp {
/* Struct to store results of simplification */
struct result {
struct simp_result {
/* Invariant [m_pf : m_orig <rel> m_new] */
expr m_new;
/* If proof is not provided, it is assumed to be reflexivity */
optional<expr> m_proof;
public:
result() {}
result(expr const & e): m_new(e) {}
result(expr const & e, expr const & proof): m_new(e), m_proof(proof) {}
result(expr const & e, optional<expr> const & proof): m_new(e), m_proof(proof) {}
simp_result() {}
simp_result(expr const & e): m_new(e) {}
simp_result(expr const & e, expr const & proof): m_new(e), m_proof(proof) {}
simp_result(expr const & e, optional<expr> const & proof): m_new(e), m_proof(proof) {}
bool has_proof() const { return static_cast<bool>(m_proof); }
@ -35,16 +30,10 @@ public:
/* The following assumes that [e] and [m_new] are definitionally equal */
void update(expr const & e) { m_new = e; }
};
}
// TODO(dhs): put this outside of blast module
typedef std::function<bool(expr const &)> expr_predicate; // NOLINT
simp::result simplify(name const & rel, expr const & e, simp_lemmas const & srss);
simp::result simplify(name const & rel, expr const & e, simp_lemmas const & srss, expr_predicate const & simp_pred);
simp_result simplify(type_context & ctx, name const & rel, simp_lemmas const & simp_lemmas, expr const & e);
void initialize_simplifier();
void finalize_simplifier();
}
}

1
src/library/tactic/tactic_state.cpp
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include "library/type_context.h"
#include "library/pp_options.h"
#include "library/trace.h"
#include "library/util.h"
#include "library/vm/vm_environment.h"
#include "library/vm/vm_exceptional.h"
#include "library/vm/vm_format.h"

52
src/library/type_context.cpp
View file

@ -1357,7 +1357,7 @@ bool type_context::process_assignment(expr const & m, expr const & v) {
For every metavariable `?M'@C'` occurring in `t`, `C'` is a subset of `C`
*/
optional<metavar_decl> const & e_decl = m_mctx.get_metavar_decl(e);
if (!e_decl || e_decl->get_context().is_subset_of(mvar_decl->get_context())) {
if (!e_decl || !e_decl->get_context().is_subset_of(mvar_decl->get_context())) {
ok = false;
return false;
}
@ -2489,6 +2489,56 @@ optional<expr> type_context::mk_subsingleton_instance(expr const & type) {
return r;
}
tmp_type_context::tmp_type_context(type_context & tctx, unsigned num_umeta, unsigned num_emeta): m_tctx(tctx) {
m_tmp_uassignment.resize(num_umeta, none_level());
m_tmp_eassignment.resize(num_emeta, none_expr());
}
bool tmp_type_context::is_def_eq(expr const & e1, expr const & e2) {
type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment);
return m_tctx.is_def_eq(e1, e2);
}
expr tmp_type_context::infer(expr const & e) {
type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment);
return m_tctx.infer(e);
}
expr tmp_type_context::whnf(expr const & e) {
// TODO(dhs): do I need to set the buffers for whnf?
type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment);
return m_tctx.whnf(e);
}
level tmp_type_context::mk_tmp_univ_mvar() {
type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment);
return m_tctx.mk_tmp_univ_mvar();
}
expr tmp_type_context::mk_tmp_mvar(expr const & type) {
type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment);
return m_tctx.mk_tmp_mvar(type);
}
bool tmp_type_context::is_uassigned(unsigned i) {
lean_assert(i < m_tmp_uassignment.size());
return static_cast<bool>(m_tmp_uassignment[i]);
}
bool tmp_type_context::is_eassigned(unsigned i) {
lean_assert(i < m_tmp_eassignment.size());
return static_cast<bool>(m_tmp_eassignment[i]);
}
void tmp_type_context::clear_eassignment() {
m_tmp_eassignment.clear();
}
expr tmp_type_context::instantiate_mvars(expr const & e) {
type_context::tmp_mode_scope_with_buffers tmp_scope(m_tctx, m_tmp_uassignment, m_tmp_eassignment);
return m_tctx.instantiate_mvars(e);
}
void initialize_type_context() {
register_trace_class("class_instances");
register_trace_class(name({"type_context", "unification_hint"}));

19
src/library/type_context.h
View file

@ -492,6 +492,25 @@ public:
type_context * operator->() { return &m_ctx; }
};
class tmp_type_context {
type_context & m_tctx;
buffer<optional<level>> m_tmp_uassignment;
buffer<optional<expr>> m_tmp_eassignment;
public:
tmp_type_context(type_context & tctx, unsigned num_umeta = 0, unsigned num_emeta = 0);
type_context & tctx() const { return m_tctx; }
expr infer(expr const & e);
expr whnf(expr const & e);
bool is_def_eq(expr const & e1, expr const & e2);
level mk_tmp_univ_mvar();
expr mk_tmp_mvar(expr const & type);
bool is_uassigned(unsigned i);
bool is_eassigned(unsigned i);
void clear_eassignment();
expr instantiate_mvars(expr const & e);
};
void initialize_type_context();
void finalize_type_context();
}

2
tests/lean/congr_print.lean.expected.out
View file

@ -1,2 +1,2 @@
theorem perm.perm_erase_dup_of_perm : ∀ {A : Type} [H : decidable_eq A] {l₁ l₂ : list A}, l₁ ~ l₂ → erase_dup l₁ ~ erase_dup l₂ :=
theorem perm.perm_erase_dup_of_perm [congr] : ∀ {A : Type} [H : decidable_eq A] {l₁ l₂ : list A}, l₁ ~ l₂ → erase_dup l₁ ~ erase_dup l₂ :=
λ A H l₁ l₂, sorry

8
tests/lean/run/simp1.lean Normal file
View file

@ -0,0 +1,8 @@
constants (A : Type.{1}) (f : A → A → A) (x y z : A) (g : A → A)
lemma foo [simp] : f x y = y := sorry
lemma bar [simp] : g y = z := sorry
open tactic
set_option trace.simplifier true
example : g (f x y) = z := by simp >> triv
example : g (f x (f x y)) = z := by simp >> triv

13
tests/lean/run/simp2.lean Normal file
View file

@ -0,0 +1,13 @@
import algebra.group
constants (A : Type.{1}) (A_cg : comm_group A) (x y z w : A)
attribute A_cg [instance]
open tactic
open simplifier.ac
example : x * y = y * x := by simp >> triv
example : x * y * z * w = ((w * z) * y) * x := by simp >> triv
example : x * y * z * w = ((z * w) * x) * y := by simp >> triv
open simplifier.unit
example : x * y * z * 1 * w = ((z * w * 1) * x) * y := by simp >> triv

9
tests/lean/run/simp3.lean Normal file
View file

@ -0,0 +1,9 @@
import algebra.ring
constants (A : Type.{1}) (A_cr : comm_ring A) (x y z w : A)
attribute A_cr [instance]
open tactic
open simplifier.unit simplifier.ac simplifier.distrib
example : (x + y) * (z + w) = x * z + x * w + y * z + y * w * 1 + 0 :=
by simp >> trace_state >> triv

51
tests/lean/rw_set2.lean.expected.out
View file

@ -0,0 +1,51 @@
simplification rules for iff
#1, ?M_1 ↔ ?M_1 ↦ true
#1, false ↔ ?M_1 ↦ ¬?M_1
#1, ?M_1 ↔ false ↦ ¬?M_1
#1, true ↔ ?M_1 ↦ ?M_1
#1, ?M_1 ↔ true ↦ ?M_1
#0, false ↔ true ↦ false
#0, true ↔ false ↦ false
#1, ¬?M_1 ↔ ?M_1 ↦ false
#1, ?M_1 ↔ ¬?M_1 ↦ false
#2, ?M_1 - ?M_2 ≤ ?M_1 ↦ true
#1, 0 ≤ ?M_1 ↦ true
#1, succ ?M_1 ≤ ?M_1 ↦ false
#1, pred ?M_1 ≤ ?M_1 ↦ true
#1, ?M_1 ≤ succ ?M_1 ↦ true
#1, ?M_1 ∧ ?M_1 ↦ ?M_1
#1, ?M_1 ∧ ¬?M_1 ↦ false
#1, ¬?M_1 ∧ ?M_1 ↦ false
#1, false ∧ ?M_1 ↦ false
#1, ?M_1 ∧ false ↦ false
#1, true ∧ ?M_1 ↦ ?M_1
#1, ?M_1 ∧ true ↦ ?M_1
#3 perm, ?M_1 ∧ ?M_2 ∧ ?M_3 ↦ ?M_2 ∧ ?M_1 ∧ ?M_3
#3, (?M_1 ∧ ?M_2) ∧ ?M_3 ↦ ?M_1 ∧ ?M_2 ∧ ?M_3
#2 perm, ?M_1 ∧ ?M_2 ↦ ?M_2 ∧ ?M_1
#2, ?M_2 == ?M_2 ↦ true
#2, ?M_1 - ?M_2 < succ ?M_1 ↦ true
#1, ?M_1 < 0 ↦ false
#1, ?M_1 < succ ?M_1 ↦ true
#1, 0 < succ ?M_1 ↦ true
#1, ?M_1 ∨ ?M_1 ↦ ?M_1
#1, false ∨ ?M_1 ↦ ?M_1
#1, ?M_1 ∨ false ↦ ?M_1
#1, true ∨ ?M_1 ↦ true
#1, ?M_1 ∨ true ↦ true
#3 perm, ?M_1 ∨ ?M_2 ∨ ?M_3 ↦ ?M_2 ∨ ?M_1 ∨ ?M_3
#3, (?M_1 ∨ ?M_2) ∨ ?M_3 ↦ ?M_1 ∨ ?M_2 ∨ ?M_3
#2 perm, ?M_1 ∨ ?M_2 ↦ ?M_2 ∨ ?M_1
#2, ?M_2 = ?M_2 ↦ true
#2, ¬?M_2 = ?M_2 ↦ false
#0, ¬false ↦ true
#0, ¬true ↦ false
simplification rules for eq
#1, g ?M_1 ↦ f ?M_1 + 1
#2, g ?M_1 ↦ 1
#2, f ?M_1 ↦ 0
#3, ite false ?M_2 ?M_3 ↦ ?M_3
#3, ite true ?M_2 ?M_3 ↦ ?M_2
#4, ite ?M_1 ?M_4 ?M_4 ↦ ?M_4
#1, 0 - ?M_1 ↦ 0
#2, succ ?M_1 - succ ?M_2 ↦ ?M_1 - ?M_2