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

feat(library/defeq_simplifier): new simplifier that uses only definitional equalities

Browse source
This commit is contained in:
Daniel Selsam 2016-02-13 10:52:25 -08:00 committed by Leonardo de Moura
parent 20f70035dd
commit d521063dfb
22 changed files with 779 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/emacs/lean-syntax.el
View file

@ -57,7 +57,7 @@
"whnf" "multiple_instances" "none" "decl" "declaration"
"relation" "symm" "subst" "refl" "trans" "simp" "congr"
"backward" "forward" "no_pattern" "begin_end" "tactic" "abbreviation"
"reducible" "unfold" "alias" "eqv" "intro" "intro!" "elim" "grinder" "unify"
"reducible" "unfold" "alias" "eqv" "intro" "intro!" "elim" "grinder" "unify" "defeq"
"localrefinfo" "recursor"))
"lean modifiers")
(defconst lean-modifiers-regexp

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

@ -25,6 +25,8 @@ Author: Leonardo de Moura
#include "library/fun_info_manager.h"
#include "library/congr_lemma_manager.h"
#include "library/abstract_expr_manager.h"
#include "library/defeq_simp_lemmas.h"
#include "library/defeq_simplifier.h"
#include "library/definitional/projection.h"
#include "library/blast/blast.h"
#include "library/blast/simplifier/simplifier.h"
@ -796,6 +798,38 @@ static environment unify_cmd(parser & p) {
return env;
}
static environment defeq_simplify_cmd(parser & p) {
auto pos = p.pos();
environment const & env = p.env();
name ns = p.check_id_next("invalid #simplify command, namespace or 'env' expected");
defeq_simp_lemmas sls;
if (ns == name("null")) {
} else if (ns == name("env")) {
sls = get_defeq_simp_lemmas(env);
} else {
sls = get_defeq_simp_lemmas(env, ns);
}
expr e; level_param_names ls;
std::tie(e, ls) = parse_local_expr(p);
auto tc = mk_type_checker(p.env());
expr e_simp = defeq_simplify(env, p.get_options(), sls, e);
if (!tc->is_def_eq(e, e_simp).first) {
throw parser_error("defeq_simplify result not definitionally equal to input expression", pos);
}
flycheck_information info(p.regular_stream());
if (info.enabled()) {
p.display_information_pos(p.cmd_pos());
p.regular_stream() << "defeq_simplify result:\n";
}
p.regular_stream() << e_simp << endl;
return env;
}
static environment abstract_expr_cmd(parser & p) {
unsigned o = p.parse_small_nat();
default_type_context ctx(p.env(), p.get_options());
@ -861,6 +895,7 @@ void init_cmd_table(cmd_table & r) {
add_cmd(r, cmd_info("#unify", "(for debugging purposes)", unify_cmd));
add_cmd(r, cmd_info("#accessible", "(for debugging purposes) display number of accessible declarations for blast tactic", accessible_cmd));
add_cmd(r, cmd_info("#simplify", "(for debugging purposes) simplify given expression", simplify_cmd));
add_cmd(r, cmd_info("#defeq_simplify", "(for debugging purposes) defeq-simplify given expression", defeq_simplify_cmd));
add_cmd(r, cmd_info("#abstract_expr", "(for debugging purposes) call abstract expr methods", abstract_expr_cmd));
register_decl_cmds(r);

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

@ -27,6 +27,7 @@ Author: Leonardo de Moura
#include "library/relation_manager.h"
#include "library/noncomputable.h"
#include "library/unification_hint.h"
#include "library/defeq_simp_lemmas.h"
#include "library/definitional/projection.h"
#include "library/blast/blast.h"
#include "library/blast/simplifier/simplifier.h"
@ -524,6 +525,23 @@ static void print_unification_hints(parser & p) {
out << pp_unification_hints(hints, out.get_formatter(), header);
}
static void print_defeq_lemmas(parser & p) {
io_state_stream out = p.regular_stream();
defeq_simp_lemmas lemmas;
name ns;
if (p.curr_is_identifier()) {
ns = p.get_name_val();
p.next();
lemmas = get_defeq_simp_lemmas(p.env(), ns);
} else {
lemmas = get_defeq_simp_lemmas(p.env());
}
format header;
if (!ns.is_anonymous())
header = format(" at namespace '") + format(ns) + format("'");
out << pp_defeq_simp_lemmas(lemmas, out.get_formatter(), header);
}
static void print_simp_rules(parser & p) {
io_state_stream out = p.regular_stream();
blast::scope_debug scope(p.env(), p.ios());
@ -720,6 +738,9 @@ environment print_cmd(parser & p) {
} else if (p.curr_is_token(get_unify_attr_tk())) {
p.next();
print_unification_hints(p);
} else if (p.curr_is_token(get_defeq_attr_tk())) {
p.next();
print_defeq_lemmas(p);
} else if (p.curr_is_token(get_simp_attr_tk())) {
p.next();
print_simp_rules(p);

3
src/frontends/lean/token_table.cpp
View file

@ -120,7 +120,8 @@ void init_token_table(token_table & t) {
"multiple_instances", "find_decl", "attribute", "persistent",
"include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq",
"#compile", "#accessible", "#decl_stats", "#relevant_thms", "#simplify", "#app_builder", "#refl", "#symm",
"#trans", "#congr", "#hcongr", "#congr_simp", "#congr_rel", "#normalizer", "#abstract_expr", "#unify", nullptr};
"#trans", "#congr", "#hcongr", "#congr_simp", "#congr_rel", "#normalizer", "#abstract_expr", "#unify",
"#defeq_simplify", nullptr};
pair<char const *, char const *> aliases[] =
{{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},

8
src/frontends/lean/tokens.cpp
View file

@ -120,6 +120,7 @@ static name const * g_intro_bang_attr_tk = nullptr;
static name const * g_elim_attr_tk = nullptr;
static name const * g_recursor_tk = nullptr;
static name const * g_unify_attr_tk = nullptr;
static name const * g_defeq_attr_tk = nullptr;
static name const * g_attribute_tk = nullptr;
static name const * g_with_tk = nullptr;
static name const * g_class_tk = nullptr;
@ -142,7 +143,6 @@ static name const * g_tactic_infixr_tk = nullptr;
static name const * g_tactic_postfix_tk = nullptr;
static name const * g_tactic_prefix_tk = nullptr;
static name const * g_tactic_notation_tk = nullptr;
static name const * g_call_tk = nullptr;
static name const * g_calc_tk = nullptr;
static name const * g_obtain_tk = nullptr;
static name const * g_root_tk = nullptr;
@ -271,6 +271,7 @@ void initialize_tokens() {
g_elim_attr_tk = new name{"[elim]"};
g_recursor_tk = new name{"[recursor"};
g_unify_attr_tk = new name{"[unify]"};
g_defeq_attr_tk = new name{"[defeq]"};
g_attribute_tk = new name{"attribute"};
g_with_tk = new name{"with"};
g_class_tk = new name{"[class]"};
@ -293,7 +294,6 @@ void initialize_tokens() {
g_tactic_postfix_tk = new name{"tactic_postfix"};
g_tactic_prefix_tk = new name{"tactic_prefix"};
g_tactic_notation_tk = new name{"tactic_notation"};
g_call_tk = new name{"call"};
g_calc_tk = new name{"calc"};
g_obtain_tk = new name{"obtain"};
g_root_tk = new name{"_root_"};
@ -423,6 +423,7 @@ void finalize_tokens() {
delete g_elim_attr_tk;
delete g_recursor_tk;
delete g_unify_attr_tk;
delete g_defeq_attr_tk;
delete g_attribute_tk;
delete g_with_tk;
delete g_class_tk;
@ -445,7 +446,6 @@ void finalize_tokens() {
delete g_tactic_postfix_tk;
delete g_tactic_prefix_tk;
delete g_tactic_notation_tk;
delete g_call_tk;
delete g_calc_tk;
delete g_obtain_tk;
delete g_root_tk;
@ -574,6 +574,7 @@ name const & get_intro_bang_attr_tk() { return *g_intro_bang_attr_tk; }
name const & get_elim_attr_tk() { return *g_elim_attr_tk; }
name const & get_recursor_tk() { return *g_recursor_tk; }
name const & get_unify_attr_tk() { return *g_unify_attr_tk; }
name const & get_defeq_attr_tk() { return *g_defeq_attr_tk; }
name const & get_attribute_tk() { return *g_attribute_tk; }
name const & get_with_tk() { return *g_with_tk; }
name const & get_class_tk() { return *g_class_tk; }
@ -596,7 +597,6 @@ name const & get_tactic_infixr_tk() { return *g_tactic_infixr_tk; }
name const & get_tactic_postfix_tk() { return *g_tactic_postfix_tk; }
name const & get_tactic_prefix_tk() { return *g_tactic_prefix_tk; }
name const & get_tactic_notation_tk() { return *g_tactic_notation_tk; }
name const & get_call_tk() { return *g_call_tk; }
name const & get_calc_tk() { return *g_calc_tk; }
name const & get_obtain_tk() { return *g_obtain_tk; }
name const & get_root_tk() { return *g_root_tk; }

2
src/frontends/lean/tokens.h
View file

@ -122,6 +122,7 @@ name const & get_intro_bang_attr_tk();
name const & get_elim_attr_tk();
name const & get_recursor_tk();
name const & get_unify_attr_tk();
name const & get_defeq_attr_tk();
name const & get_attribute_tk();
name const & get_with_tk();
name const & get_class_tk();
@ -144,7 +145,6 @@ name const & get_tactic_infixr_tk();
name const & get_tactic_postfix_tk();
name const & get_tactic_prefix_tk();
name const & get_tactic_notation_tk();
name const & get_call_tk();
name const & get_calc_tk();
name const & get_obtain_tk();
name const & get_root_tk();

1
src/frontends/lean/tokens.txt
View file

@ -115,6 +115,7 @@ intro_bang_attr [intro!]
elim_attr [elim]
recursor [recursor
unify_attr [unify]
defeq_attr [defeq]
attribute attribute
with with
class [class]

3
src/library/CMakeLists.txt
View file

@ -18,4 +18,5 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
aux_recursors.cpp norm_num.cpp norm_num.cpp class_instance_resolution.cpp type_context.cpp
tmp_type_context.cpp fun_info_manager.cpp congr_lemma_manager.cpp
abstract_expr_manager.cpp light_lt_manager.cpp trace.cpp
attribute_manager.cpp error_handling.cpp unification_hint.cpp)
attribute_manager.cpp error_handling.cpp unification_hint.cpp defeq_simp_lemmas.cpp
defeq_simplifier.cpp)

4
src/library/constants.cpp
View file

@ -189,6 +189,7 @@ name const * g_prod_pr2 = nullptr;
name const * g_propext = nullptr;
name const * g_rat_divide = nullptr;
name const * g_rat_of_num = nullptr;
name const * g_rfl = nullptr;
name const * g_right_distrib = nullptr;
name const * g_ring = nullptr;
name const * g_semiring = nullptr;
@ -463,6 +464,7 @@ void initialize_constants() {
g_propext = new name{"propext"};
g_rat_divide = new name{"rat", "divide"};
g_rat_of_num = new name{"rat", "of_num"};
g_rfl = new name{"rfl"};
g_right_distrib = new name{"right_distrib"};
g_ring = new name{"ring"};
g_semiring = new name{"semiring"};
@ -738,6 +740,7 @@ void finalize_constants() {
delete g_propext;
delete g_rat_divide;
delete g_rat_of_num;
delete g_rfl;
delete g_right_distrib;
delete g_ring;
delete g_semiring;
@ -1012,6 +1015,7 @@ name const & get_prod_pr2_name() { return *g_prod_pr2; }
name const & get_propext_name() { return *g_propext; }
name const & get_rat_divide_name() { return *g_rat_divide; }
name const & get_rat_of_num_name() { return *g_rat_of_num; }
name const & get_rfl_name() { return *g_rfl; }
name const & get_right_distrib_name() { return *g_right_distrib; }
name const & get_ring_name() { return *g_ring; }
name const & get_semiring_name() { return *g_semiring; }

1
src/library/constants.h
View file

@ -191,6 +191,7 @@ name const & get_prod_pr2_name();
name const & get_propext_name();
name const & get_rat_divide_name();
name const & get_rat_of_num_name();
name const & get_rfl_name();
name const & get_right_distrib_name();
name const & get_ring_name();
name const & get_semiring_name();

1
src/library/constants.txt
View file

@ -184,6 +184,7 @@ prod.pr2
propext
rat.divide
rat.of_num
rfl
right_distrib
ring
semiring

191
src/library/defeq_simp_lemmas.cpp Normal file
View file

@ -0,0 +1,191 @@
/*
Copyright (c) 2015 Daniel Selsam. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Daniel Selsam
*/
#include <string>
#include "util/sexpr/format.h"
#include "kernel/expr.h"
#include "kernel/error_msgs.h"
#include "kernel/instantiate.h"
#include "library/attribute_manager.h"
#include "library/constants.h"
#include "library/defeq_simp_lemmas.h"
#include "library/util.h"
#include "library/expr_lt.h"
#include "library/scoped_ext.h"
#include "library/tmp_type_context.h"
namespace lean {
/* defeq simp lemmas */
defeq_simp_lemma::defeq_simp_lemma(name const & id, levels const & umetas, list<expr> const & emetas,
list<bool> const & instances, expr const & lhs, expr const & rhs, unsigned priority):
m_id(id), m_umetas(umetas), m_emetas(emetas), m_instances(instances), m_lhs(lhs), m_rhs(rhs), m_priority(priority) {}
bool operator==(defeq_simp_lemma const & sl1, defeq_simp_lemma const & sl2) {
return sl1.get_lhs() == sl2.get_lhs() && sl1.get_rhs() == sl2.get_rhs();
}
/* Environment extension */
static name * g_class_name = nullptr;
static std::string * g_key = nullptr;
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) {
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()) {
throw exception("invalid [defeq] simp lemma: must be a definition so that definitional equality can be verified");
}
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());
}
levels ls = to_list(us);
expr type = instantiate_type_univ_params(d, ls);
expr proof = instantiate_value_univ_params(d, ls);
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,
expr const & type, expr const & proof, unsigned priority) {
m_decl_name_to_prio.insert(decl_name, priority);
expr rule = type;
expr pf = proof;
buffer<expr> emetas;
buffer<bool> instances;
while (is_pi(rule)) {
expr mvar = tctx.mk_mvar(binding_domain(rule));
emetas.push_back(mvar);
instances.push_back(binding_info(rule).is_inst_implicit());
rule = instantiate(binding_body(rule), mvar);
pf = binding_body(pf);
}
expr lhs, rhs;
if (!is_eq(rule, lhs, rhs))
throw exception("invalid [defeq] simp lemma: body must be an equality");
if (!is_app_of(pf, get_eq_refl_name(), 2) && !is_app_of(pf, get_rfl_name(), 2))
throw exception("invalid [defeq] simp lemma: proof must be an application of either 'eq.refl' or 'rfl' to two arguments");
if (lhs == rhs)
throw exception("invalid [defeq] simp lemma: the two sides of the equality cannot be structurally equal");
defeq_simp_lemma lemma(decl_name, umetas, to_list(emetas), to_list(instances), lhs, rhs, priority);
m_defeq_simp_lemmas.insert(lhs, lemma);
}
};
struct defeq_simp_lemmas_entry {
name m_decl_name;
unsigned m_priority;
defeq_simp_lemmas_entry(name const & decl_name, unsigned priority):
m_decl_name(decl_name), m_priority(priority) {}
};
struct defeq_simp_lemmas_config {
typedef defeq_simp_lemmas_entry entry;
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());
s.register_defeq_simp_lemma(tctx, e.m_decl_name, e.m_priority);
}
static name const & get_class_name() {
return *g_class_name;
}
static std::string const & get_serialization_key() {
return *g_key;
}
static void write_entry(serializer & s, entry const & e) {
s << e.m_decl_name << e.m_priority;
}
static entry read_entry(deserializer & d) {
name decl_name; unsigned prio;
d >> decl_name >> prio;
return entry(decl_name, prio);
}
static optional<unsigned> get_fingerprint(entry const & e) {
return some(hash(e.m_decl_name.hash(), e.m_priority));
}
};
typedef scoped_ext<defeq_simp_lemmas_config> defeq_simp_lemmas_ext;
environment add_defeq_simp_lemma(environment const & env, io_state const & ios, name const & decl_name, unsigned prio, name const & ns, bool persistent) {
return defeq_simp_lemmas_ext::add_entry(env, ios, defeq_simp_lemmas_entry(decl_name, prio), ns, persistent);
}
bool is_defeq_simp_lemma(environment const & env, name const & decl_name) {
return defeq_simp_lemmas_ext::get_state(env).m_decl_name_to_prio.contains(decl_name);
}
defeq_simp_lemmas get_defeq_simp_lemmas(environment const & env) {
return defeq_simp_lemmas_ext::get_state(env).m_defeq_simp_lemmas;
}
defeq_simp_lemmas get_defeq_simp_lemmas(environment const & env, name const & ns) {
list<defeq_simp_lemmas_entry> const * entries = defeq_simp_lemmas_ext::get_entries(env, ns);
defeq_simp_lemmas_state s;
if (entries) {
for (auto const & e : *entries) {
tmp_type_context tctx(env, get_dummy_ios().get_options());
s.register_defeq_simp_lemma(tctx, e.m_decl_name, e.m_priority);
}
}
return s.m_defeq_simp_lemmas;
}
/* Pretty printing */
format defeq_simp_lemma::pp(formatter const & fmt) const {
format r;
r += format("#") + format(get_num_emeta());
if (get_priority() != LEAN_DEFAULT_PRIORITY)
r += space() + paren(format(get_priority()));
format r1 = comma() + space() + fmt(get_lhs());
r1 += space() + format("↦") + pp_indent_expr(fmt, get_rhs());
r += group(r1);
return r;
}
format pp_defeq_simp_lemmas(defeq_simp_lemmas const & lemmas, formatter const & fmt, format const & header) {
format r;
r += format("defeq simp lemmas");
r += header + colon() + line();
lemmas.for_each_entry([&](head_index const &, defeq_simp_lemma const & lemma) {
r += lemma.pp(fmt) + line();
});
return r;
}
/* Setup and teardown */
void initialize_defeq_simp_lemmas() {
g_class_name = new name("defeq_simp_lemmas");
g_key = new std::string("DEFEQ_SIMP_LEMMAS");
defeq_simp_lemmas_ext::initialize();
register_prio_attribute("defeq", "defeq simp lemma",
add_defeq_simp_lemma,
is_defeq_simp_lemma,
[](environment const & env, name const & decl_name) {
if (auto p = defeq_simp_lemmas_ext::get_state(env).m_decl_name_to_prio.find(decl_name))
return *p;
else
return LEAN_DEFAULT_PRIORITY;
});
}
void finalize_defeq_simp_lemmas() {
defeq_simp_lemmas_ext::finalize();
delete g_key;
delete g_class_name;
}
}

58
src/library/defeq_simp_lemmas.h Normal file
View file

@ -0,0 +1,58 @@
/*
Copyright (c) 2015 Daniel Selsam. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Daniel Selsam
*/
#pragma once
#include "kernel/environment.h"
#include "library/io_state.h"
#include "library/head_map.h"
namespace lean {
class defeq_simp_lemma {
name m_id;
levels m_umetas;
list<expr> m_emetas;
list<bool> m_instances;
expr m_lhs;
expr m_rhs;
unsigned m_priority;
public:
defeq_simp_lemma() {}
defeq_simp_lemma(name const & id, levels const & umetas, list<expr> const & emetas,
list<bool> const & instances, expr const & lhs, expr const & rhs, unsigned priority);
name const & get_id() const { return m_id; }
unsigned get_num_umeta() const { return length(m_umetas); }
unsigned get_num_emeta() const { return length(m_emetas); }
/** \brief Return a list containing the expression metavariables in reverse order. */
list<expr> const & get_emetas() const { return m_emetas; }
/** \brief Return a list of bools indicating whether or not each expression metavariable
in <tt>get_emetas()</tt> is an instance. */
list<bool> const & get_instances() const { return m_instances; }
expr const & get_lhs() const { return m_lhs; }
expr const & get_rhs() const { return m_rhs; }
unsigned get_priority() const { return m_priority; }
format pp(formatter const & fmt) const;
};
bool operator==(defeq_simp_lemma const & sl1, defeq_simp_lemma const & sl2);
inline bool operator!=(defeq_simp_lemma const & sl1, defeq_simp_lemma const & sl2) { return !operator==(sl1, sl2); }
struct defeq_simp_lemma_prio_fn { unsigned operator()(defeq_simp_lemma const & sl) const { return sl.get_priority(); } };
typedef head_map_prio<defeq_simp_lemma, defeq_simp_lemma_prio_fn> defeq_simp_lemmas;
defeq_simp_lemmas get_defeq_simp_lemmas(environment const & env);
defeq_simp_lemmas get_defeq_simp_lemmas(environment const & env, name const & ns);
format pp_defeq_simp_lemmas(defeq_simp_lemmas const & lemmas, formatter const & fmt, format const & header);
void initialize_defeq_simp_lemmas();
void finalize_defeq_simp_lemmas();
}

312
src/library/defeq_simplifier.cpp Normal file
View file

@ -0,0 +1,312 @@
/*
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/defeq_simplifier.h"
#include "util/interrupt.h"
#include "util/sexpr/option_declarations.h"
#include "kernel/expr_maps.h"
#include "kernel/instantiate.h"
#include "kernel/abstract.h"
#include "library/trace.h"
#include "library/tmp_type_context.h"
#include "library/normalize.h"
#ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS
#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS 1000
#endif
#ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_REWRITE_ROUNDS
#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_REWRITE_ROUNDS 1000
#endif
#ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_TOP_DOWN
#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_TOP_DOWN false
#endif
#ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXHAUSTIVE
#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXHAUSTIVE true
#endif
#ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_MEMOIZE
#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_MEMOIZE true
#endif
#ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXPAND_MACROS
#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXPAND_MACROS false
#endif
namespace lean {
/* Options */
static name * g_simplify_max_simp_rounds = nullptr;
static name * g_simplify_max_rewrite_rounds = nullptr;
static name * g_simplify_top_down = nullptr;
static name * g_simplify_exhaustive = nullptr;
static name * g_simplify_memoize = nullptr;
static name * g_simplify_expand_macros = nullptr;
static unsigned get_simplify_max_simp_rounds(options const & o) {
return o.get_unsigned(*g_simplify_max_simp_rounds, LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS);
}
static unsigned get_simplify_max_rewrite_rounds(options const & o) {
return o.get_unsigned(*g_simplify_max_rewrite_rounds, LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_REWRITE_ROUNDS);
}
static bool get_simplify_top_down(options const & o) {
return o.get_bool(*g_simplify_top_down, LEAN_DEFAULT_DEFEQ_SIMPLIFY_TOP_DOWN);
}
static bool get_simplify_exhaustive(options const & o) {
return o.get_bool(*g_simplify_exhaustive, LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXHAUSTIVE);
}
static bool get_simplify_memoize(options const & o) {
return o.get_bool(*g_simplify_memoize, LEAN_DEFAULT_DEFEQ_SIMPLIFY_MEMOIZE);
}
static bool get_simplify_expand_macros(options const & o) {
return o.get_bool(*g_simplify_expand_macros, LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXPAND_MACROS);
}
/* Main simplifier class */
class defeq_simplify_fn {
tmp_type_context m_tmp_tctx;
defeq_simp_lemmas m_simp_lemmas;
unsigned m_num_simp_rounds{0};
unsigned m_num_rewrite_rounds{0};
options const & m_options;
/* Options */
unsigned m_max_simp_rounds;
unsigned m_max_rewrite_rounds;
bool m_top_down;
bool m_exhaustive;
bool m_memoize;
bool m_expand_macros;
/* Cache */
expr_struct_map<expr> m_cache;
optional<expr> cache_lookup(expr const & e) {
auto it = m_cache.find(e);
if (it == m_cache.end()) return none_expr();
else return some_expr(it->second);
}
void cache_save(expr const & e, expr const & e_simp) {
m_cache.insert(mk_pair(e, e_simp));
}
/* Simplification */
expr defeq_simplify(expr const & _e) {
expr e = _e;
lean_trace_inc_depth("defeq_simplifier");
lean_trace_d("defeq_simplifier", tout() << e << "\n";);
while (true) {
expr e_start = e;
check_system("defeq_simplifier");
m_num_simp_rounds++;
if (m_num_simp_rounds > m_max_simp_rounds)
throw exception("defeq_simplifier failed, maximum number of simp rounds exceeded");
if (m_memoize) {
if (auto it = cache_lookup(e)) return *it;
}
if (m_top_down) e = rewrite(whnf_eta(e));
e = whnf_eta(e);
switch (e.kind()) {
case expr_kind::Local:
case expr_kind::Meta:
case expr_kind::Sort:
case expr_kind::Constant:
break;
case expr_kind::Var:
lean_unreachable();
case expr_kind::Macro:
if (m_expand_macros) {
if (auto m = m_tmp_tctx.expand_macro(e)) e = defeq_simplify(whnf_eta(*m));
}
break;
case expr_kind::Lambda:
case expr_kind::Pi:
e = defeq_simplify_binding(e);
break;
case expr_kind::App:
e = defeq_simplify_app(e);
break;
}
if (!m_top_down) e = rewrite(whnf_eta(e));
if (!m_exhaustive || e == e_start) break;
}
if (m_memoize) cache_save(_e, e);
return e;
}
expr defeq_simplify_binding(expr const & e) {
expr d = defeq_simplify(binding_domain(e));
expr l = m_tmp_tctx.mk_tmp_local(binding_name(e), d, binding_info(e));
expr b = abstract(defeq_simplify(instantiate(binding_body(e), l)), l);
return update_binding(e, d, b);
}
expr defeq_simplify_app(expr const & e) {
buffer<expr> args;
expr f = defeq_simplify(get_app_args(e, args));
for (unsigned i = 0; i < args.size(); ++i) args[i] = defeq_simplify(args[i]);
return mk_app(f, args);
}
/* Rewriting */
expr rewrite(expr const & _e) {
expr e = _e;
while (true) {
check_system("defeq_simplifier");
m_num_rewrite_rounds++;
if (m_num_rewrite_rounds > m_max_rewrite_rounds)
throw exception("defeq_simplifier failed, maximum number of rewrite rounds exceeded");
list<defeq_simp_lemma> const * simp_lemmas_ptr = m_simp_lemmas.find(e);
if (!simp_lemmas_ptr) return e;
buffer<defeq_simp_lemma> simp_lemmas;
to_buffer(*simp_lemmas_ptr, simp_lemmas);
expr e_start = e;
for (defeq_simp_lemma const & sl : simp_lemmas) e = rewrite(e, sl);
if (e == e_start) break;
}
return e;
}
expr rewrite(expr const & e, defeq_simp_lemma const & sl) {
tmp_type_context tmp_tctx(m_tmp_tctx.env(), m_options);
tmp_tctx.clear();
tmp_tctx.set_next_uvar_idx(sl.get_num_umeta());
tmp_tctx.set_next_mvar_idx(sl.get_num_emeta());
if (!tmp_tctx.is_def_eq(e, sl.get_lhs())) return e;
lean_trace(name({"defeq_simplifier", "rewrite"}),
expr new_lhs = tmp_tctx.instantiate_uvars_mvars(sl.get_lhs());
expr new_rhs = tmp_tctx.instantiate_uvars_mvars(sl.get_rhs());
tout() << "(" << sl.get_id() << ") "
<< "[" << new_lhs << " --> " << new_rhs << "]\n";);
if (!instantiate_emetas(tmp_tctx, sl.get_emetas(), sl.get_instances())) return e;
for (unsigned i = 0; i < sl.get_num_umeta(); i++) {
if (!tmp_tctx.is_uvar_assigned(i)) return e;
}
expr new_rhs = tmp_tctx.instantiate_uvars_mvars(sl.get_rhs());
return new_rhs;
}
bool instantiate_emetas(tmp_type_context & tmp_tctx, list<expr> const & _emetas, list<bool> const & _instances) {
buffer<expr> emetas;
buffer<bool> instances;
to_buffer(_emetas, emetas);
to_buffer(_instances, instances);
lean_assert(emetas.size() == instances.size());
for (unsigned i = 0; i < emetas.size(); ++i) {
expr m = emetas[i];
unsigned mvar_idx = emetas.size() - 1 - i;
expr m_type = tmp_tctx.instantiate_uvars_mvars(tmp_tctx.infer(m));
lean_assert(!has_metavar(m_type));
if (tmp_tctx.is_mvar_assigned(mvar_idx)) continue;
if (instances[i]) {
if (auto v = tmp_tctx.mk_class_instance(m_type)) {
if (!tmp_tctx.assign(m, *v)) {
lean_trace(name({"defeq_simplifier", "failure"}),
tout() << "unable to assign instance for: " << m_type << "\n";);
return false;
} else {
lean_assert(tmp_tctx.is_mvar_assigned(mvar_idx));
continue;
}
} else {
lean_trace(name({"defeq_simplifier", "failure"}),
tout() << "unable to synthesize instance for: " << m_type << "\n";);
return false;
}
} else {
lean_trace(name({"defeq_simplifier", "failure"}),
tout() << "failed to assign: " << m << " : " << m_type << "\n";);
return false;
}
}
return true;
}
expr whnf_eta(expr const & e) {
return try_eta(m_tmp_tctx.whnf(e));
}
public:
defeq_simplify_fn(environment const & env, options const & o, defeq_simp_lemmas const & simp_lemmas):
m_tmp_tctx(env, o),
m_simp_lemmas(simp_lemmas),
m_options(o),
m_max_simp_rounds(get_simplify_max_simp_rounds(o)),
m_max_rewrite_rounds(get_simplify_max_rewrite_rounds(o)),
m_top_down(get_simplify_top_down(o)),
m_exhaustive(get_simplify_exhaustive(o)),
m_memoize(get_simplify_memoize(o)),
m_expand_macros(get_simplify_expand_macros(o)) {}
expr operator()(expr const & e) { return defeq_simplify(e); }
};
/* Setup and teardown */
void initialize_defeq_simplifier() {
register_trace_class("defeq_simplifier");
register_trace_class(name({"defeq_simplifier", "rewrite"}));
register_trace_class(name({"defeq_simplifier", "failure"}));
g_simplify_max_simp_rounds = new name{"defeq_simplify", "max_simp_rounds"};
g_simplify_max_rewrite_rounds = new name{"defeq_simplify", "max_rewrite_rounds"};
g_simplify_top_down = new name{"defeq_simplify", "top_down"};
g_simplify_exhaustive = new name{"defeq_simplify", "exhaustive"};
g_simplify_memoize = new name{"defeq_simplify", "memoize"};
g_simplify_expand_macros = new name{"defeq_simplify", "expand_macros"};
register_unsigned_option(*g_simplify_max_simp_rounds, LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS,
"(defeq_simplify) max allowed simplification rounds");
register_unsigned_option(*g_simplify_max_rewrite_rounds, LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_REWRITE_ROUNDS,
"(defeq_simplify) max allowed rewrite rounds");
register_bool_option(*g_simplify_top_down, LEAN_DEFAULT_DEFEQ_SIMPLIFY_TOP_DOWN,
"(defeq_simplify) use top-down rewriting instead of bottom-up");
register_bool_option(*g_simplify_exhaustive, LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXHAUSTIVE,
"(defeq_simplify) simplify exhaustively");
register_bool_option(*g_simplify_memoize, LEAN_DEFAULT_DEFEQ_SIMPLIFY_MEMOIZE,
"(defeq_simplify) memoize simplifications");
register_bool_option(*g_simplify_expand_macros, LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXPAND_MACROS,
"(defeq_simplify) expand macros");
}
void finalize_defeq_simplifier() {
delete g_simplify_expand_macros;
delete g_simplify_memoize;
delete g_simplify_exhaustive;
delete g_simplify_top_down;
delete g_simplify_max_rewrite_rounds;
delete g_simplify_max_simp_rounds;
}
/* Entry point */
expr defeq_simplify(environment const & env, options const & o, defeq_simp_lemmas const & simp_lemmas, expr const & e) {
return defeq_simplify_fn(env, o, simp_lemmas)(e);
}
}

17
src/library/defeq_simplifier.h Normal file
View file

@ -0,0 +1,17 @@
/*
Copyright (c) 2015 Daniel Selsam. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Daniel Selsam
*/
#pragma once
#include "kernel/expr.h"
#include "library/defeq_simp_lemmas.h"
namespace lean {
expr defeq_simplify(environment const & env, options const & o, defeq_simp_lemmas const & simp_lemmas, expr const & e);
void initialize_defeq_simplifier();
void finalize_defeq_simplifier();
}

6
src/library/init_module.cpp
View file

@ -48,6 +48,8 @@ Author: Leonardo de Moura
#include "library/attribute_manager.h"
#include "library/fun_info_manager.h"
#include "library/unification_hint.h"
#include "library/defeq_simp_lemmas.h"
#include "library/defeq_simplifier.h"
namespace lean {
void initialize_library_module() {
@ -95,9 +97,13 @@ void initialize_library_module() {
initialize_app_builder();
initialize_fun_info_manager();
initialize_unification_hint();
initialize_defeq_simp_lemmas();
initialize_defeq_simplifier();
}
void finalize_library_module() {
finalize_defeq_simplifier();
finalize_defeq_simp_lemmas();
finalize_unification_hint();
finalize_fun_info_manager();
finalize_app_builder();

15
tests/lean/defeq_simp_lemmas1.lean Normal file
View file

@ -0,0 +1,15 @@
universe l
constants (A : Type.{l})
definition q (x : A) := x
definition h (x : A) : A := q x
definition g (x y : A) := h y
definition f (x y z : A) := g (g x y) z
definition d (x y z w : A) := f (f x y z) (f y z w) (f x w z)
definition h.def [defeq] (x : A) : h x = q x := rfl
definition g.def [defeq] (x y : A) : g x y = h y := rfl
definition f.def [defeq] (x y z : A) : f x y z = g (g x y) z := rfl
definition d.def [defeq] (x y z w : A) : d x y z w = f (f x y z) (f y z w) (f x w z) := rfl
print [defeq]

5
tests/lean/defeq_simp_lemmas1.lean.expected.out Normal file
View file

@ -0,0 +1,5 @@
defeq simp lemmas:
#2, g ?M_1 ?M_2 ↦ h ?M_2
#4, d ?M_1 ?M_2 ?M_3 ?M_4 ↦ f (f ?M_1 ?M_2 ?M_3) (f ?M_2 ?M_3 ?M_4) (f ?M_1 ?M_4 ?M_3)
#3, f ?M_1 ?M_2 ?M_3 ↦ g (g ?M_1 ?M_2) ?M_3
#1, h ?M_1 ↦ q ?M_1

37
tests/lean/defeq_simp_lemmas2.lean Normal file
View file

@ -0,0 +1,37 @@
universe l
constants (A : Type.{l})
definition q (x : A) := x
definition h (x : A) : A := q x
definition g (x y : A) := h y
definition f (x y z : A) := g (g x y) z
definition d (x y z w : A) := f (f x y z) (f y z w) (f x w z)
definition h.rfl [defeq] (x : A) : h x = x := rfl
definition g.rfl [defeq] (x y : A) : g x y = y := rfl
definition f.rfl [defeq] (x y z : A) : f x y z = z := rfl
definition d.rfl [defeq] (x y z w : A) : d x y z w = z := rfl
definition h.def [defeq] (x : A) : h x = q x := rfl
definition g.def [defeq] (x y : A) : g x y = h y := rfl
definition f.def [defeq] (x y z : A) : f x y z = g (g x y) z := rfl
definition d.def [defeq] (x y z w : A) : d x y z w = f (f x y z) (f y z w) (f x w z) := rfl
-- Confirm that more recent annotations get priority
print [defeq]
attribute h.rfl [defeq] [priority 1001]
attribute g.rfl [defeq] [priority 1001]
attribute f.rfl [defeq] [priority 1001]
attribute d.rfl [defeq] [priority 1001]
-- Confirm that priority annotations override
print [defeq]
attribute h.def [defeq] [priority 1001]
attribute g.def [defeq] [priority 1001]
attribute f.def [defeq] [priority 1001]
attribute d.def [defeq] [priority 1001]
-- Confirm that most recent annotations get priority to break explicit priority ties
print [defeq]

27
tests/lean/defeq_simp_lemmas2.lean.expected.out Normal file
View file

@ -0,0 +1,27 @@
defeq simp lemmas:
#2, g ?M_1 ?M_2 ↦ h ?M_2
#2, g ?M_1 ?M_2 ↦ ?M_2
#4, d ?M_1 ?M_2 ?M_3 ?M_4 ↦ f (f ?M_1 ?M_2 ?M_3) (f ?M_2 ?M_3 ?M_4) (f ?M_1 ?M_4 ?M_3)
#4, d ?M_1 ?M_2 ?M_3 ?M_4 ↦ ?M_3
#3, f ?M_1 ?M_2 ?M_3 ↦ g (g ?M_1 ?M_2) ?M_3
#3, f ?M_1 ?M_2 ?M_3 ↦ ?M_3
#1, h ?M_1 ↦ q ?M_1
#1, h ?M_1 ↦ ?M_1
defeq simp lemmas:
#2 (1001), g ?M_1 ?M_2 ↦ ?M_2
#2, g ?M_1 ?M_2 ↦ h ?M_2
#4 (1001), d ?M_1 ?M_2 ?M_3 ?M_4 ↦ ?M_3
#4, d ?M_1 ?M_2 ?M_3 ?M_4 ↦ f (f ?M_1 ?M_2 ?M_3) (f ?M_2 ?M_3 ?M_4) (f ?M_1 ?M_4 ?M_3)
#3 (1001), f ?M_1 ?M_2 ?M_3 ↦ ?M_3
#3, f ?M_1 ?M_2 ?M_3 ↦ g (g ?M_1 ?M_2) ?M_3
#1 (1001), h ?M_1 ↦ ?M_1
#1, h ?M_1 ↦ q ?M_1
defeq simp lemmas:
#2 (1001), g ?M_1 ?M_2 ↦ h ?M_2
#2 (1001), g ?M_1 ?M_2 ↦ ?M_2
#4 (1001), d ?M_1 ?M_2 ?M_3 ?M_4 ↦ f (f ?M_1 ?M_2 ?M_3) (f ?M_2 ?M_3 ?M_4) (f ?M_1 ?M_4 ?M_3)
#4 (1001), d ?M_1 ?M_2 ?M_3 ?M_4 ↦ ?M_3
#3 (1001), f ?M_1 ?M_2 ?M_3 ↦ g (g ?M_1 ?M_2) ?M_3
#3 (1001), f ?M_1 ?M_2 ?M_3 ↦ ?M_3
#1 (1001), h ?M_1 ↦ q ?M_1
#1 (1001), h ?M_1 ↦ ?M_1

30
tests/lean/defeq_simplifier1.lean Normal file
View file

@ -0,0 +1,30 @@
universe l
constants (A : Type.{l})
definition q (x : A) : A := x
definition h (x : A) : A := q x
definition g (x y : A) := h y
definition f (x y z : A) := g (g x y) z
definition d (x y z w : A) := f (f x y z) (f y z w) (f x w z)
definition h.def [defeq] (x : A) : h x = q x := rfl
definition g.def [defeq] (x y : A) : g x y = h y := rfl
definition f.def [defeq] (x y z : A) : f x y z = g (g x y) z := rfl
definition d.def [defeq] (x y z w : A) : d x y z w = f (f x y z) (f y z w) (f x w z) := rfl
#defeq_simplify env λ x y z w, (λ x, d x) (g (f x y z) (f z y x)) (g x z) (f y z w) (q (g x z))
#defeq_simplify env Π x y z w, (λ x, d x) (g (f x y z) (f z y x)) (g x z) (f y z w) (q (g x z)) = (λ x, x) w
set_option defeq_simplify.exhaustive false
#defeq_simplify env λ x y z w, (λ x, d x) (g (f x y z) (f z y x)) (g x z) (f y z w) (q (g x z))
#defeq_simplify env Π x y z w, (λ x, d x) (g (f x y z) (f z y x)) (g x z) (f y z w) (q (g x z)) = (λ x, x) w
set_option defeq_simplify.top_down true
#defeq_simplify env λ x y z w, (λ x, d x) (g (f x y z) (f z y x)) (g x z) (f y z w) (q (g x z))
#defeq_simplify env Π x y z w, (λ x, d x) (g (f x y z) (f z y x)) (g x z) (f y z w) (q (g x z)) = (λ x, x) w
attribute q [reducible]
set_option defeq_simplify.exhaustive true
set_option defeq_simplify.top_down false
#defeq_simplify env λ x y z w, (λ x, d x) (g (f x y z) (f z y x)) (g x z) (f y z w) (q (g x z))
#defeq_simplify env Π x y z w, (λ x, d x) (g (f x y z) (f z y x)) (g x z) (f y z w) (q (g x z)) = (λ x, x) w

8
tests/lean/defeq_simplifier1.lean.expected.out Normal file
View file

@ -0,0 +1,8 @@
λ (x y z w : A), q (q (q w))
A → A → A → (∀ (w : A), q (q (q w)) = w)
λ (x y z w : A), q (f (q (q x)) (q (q z)) (q w))
∀ (x : A), A → (∀ (z w : A), q (f (q (q x)) (q (q z)) (q w)) = w)
λ (x y z w : A), q (q (q w))
A → A → A → (∀ (w : A), q (q (q w)) = w)
λ (x y z w : A), w
A → A → A → (∀ (w : A), w = w)