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

feat(frontends/lean): add '[rewrite]' attribute

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-01 17:53:25 -07:00
parent d547698a56
commit 0fbc944cdd
12 changed files with 113 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -123,7 +123,7 @@
"\[irreducible\]" "\[semireducible\]" "\[quasireducible\]" "\[wf\]"
"\[whnf\]" "\[multiple-instances\]" "\[none\]"
"\[decls\]" "\[declarations\]" "\[coercions\]" "\[classes\]"
"\[symm\]" "\[subst\]" "\[refl\]" "\[trans\]"
"\[symm\]" "\[subst\]" "\[refl\]" "\[trans\]" "\[rewrite\]"
"\[notations\]" "\[abbreviations\]" "\[begin-end-hints\]" "\[tactic-hints\]"
"\[reduce-hints\]" "\[unfold-hints\]" "\[aliases\]" "\[eqv\]" "\[localrefinfo\]"))
. 'font-lock-doc-face)

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

@ -1,5 +1,5 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Copyright (c) 2014-2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
@ -31,6 +31,7 @@ Author: Leonardo de Moura
#include "library/user_recursors.h"
#include "library/pp_options.h"
#include "library/definitional/projection.h"
#include "library/simplifier/rewrite_rule_set.h"
#include "frontends/lean/util.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/calc.h"
@ -188,6 +189,8 @@ void print_attributes(parser & p, name const & n) {
out << " [class]";
if (is_instance(env, n))
out << " [instance]";
if (is_rewrite_rule(env, n))
out << " [rewrite]";
switch (get_reducible_status(env, n)) {
case reducible_status::Reducible: out << " [reducible]"; break;
case reducible_status::Irreducible: out << " [irreducible]"; break;
@ -366,6 +369,19 @@ static void print_reducible_info(parser & p, reducible_status s1) {
out << n << "\n";
}
static void print_rewrite_sets(parser & p) {
io_state_stream out = p.regular_stream();
rewrite_rule_sets s = get_rewrite_rule_sets(p.env());
name prev_eqv;
s.for_each([&](name const & eqv, rewrite_rule const & rw) {
if (prev_eqv != eqv) {
out << "rewrite rules for " << eqv << "\n";
prev_eqv = eqv;
}
out << rw.pp(out.get_formatter()) << "\n";
});
}
environment print_cmd(parser & p) {
flycheck_information info(p.regular_stream());
if (info.enabled()) {
@ -462,6 +478,9 @@ environment print_cmd(parser & p) {
p.next();
p.check_token_next(get_rbracket_tk(), "invalid 'print [recursor]', ']' expected");
print_recursor_info(p);
} else if (p.curr_is_token(get_rewrite_attr_tk())) {
p.next();
print_rewrite_sets(p);
} else if (print_polymorphic(p)) {
} else {
throw parser_error("invalid print command", p.pos());

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

@ -30,6 +30,7 @@ Author: Leonardo de Moura
#include "library/relation_manager.h"
#include "library/user_recursors.h"
#include "library/unfold_macros.h"
#include "library/simplifier/rewrite_rule_set.h"
#include "library/definitional/equations.h"
#include "library/error_handling/error_handling.h"
#include "frontends/lean/parser.h"
@ -367,6 +368,7 @@ struct decl_attributes {
bool m_refl;
bool m_subst;
bool m_recursor;
bool m_rewrite;
optional<unsigned> m_recursor_major_pos;
optional<unsigned> m_priority;
optional<unsigned> m_unfold_c_hint;
@ -392,6 +394,7 @@ struct decl_attributes {
m_refl = false;
m_subst = false;
m_recursor = false;
m_rewrite = false;
}
struct elim_choice_fn : public replace_visitor {
@ -518,6 +521,9 @@ struct decl_attributes {
} else if (p.curr_is_token(get_subst_tk())) {
p.next();
m_subst = true;
} else if (p.curr_is_token(get_rewrite_attr_tk())) {
p.next();
m_rewrite = true;
} else if (p.curr_is_token(get_recursor_tk())) {
p.next();
if (!p.curr_is_token(get_rbracket_tk())) {
@ -587,6 +593,8 @@ struct decl_attributes {
env = add_user_recursor(env, d, m_recursor_major_pos, m_persistent);
if (m_is_class)
env = add_class(env, d, m_persistent);
if (m_rewrite)
env = add_rewrite_rule(env, d, m_persistent);
if (m_has_multiple_instances)
env = mark_multiple_instances(env, d, m_persistent);
return env;

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

@ -108,7 +108,7 @@ void init_token_table(token_table & t) {
"definition", "example", "coercion", "abbreviation",
"variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
"[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]",
"[parsing-only]", "[multiple-instances]", "[symm]", "[trans]", "[refl]", "[subst]", "[recursor",
"[rewrite]", "[parsing-only]", "[multiple-instances]", "[symm]", "[trans]", "[refl]", "[subst]", "[recursor",
"evaluate", "check", "eval", "[wf]", "[whnf]", "[priority", "[unfold-f]",
"[constructor]", "[unfold-c", "print",
"end", "namespace", "section", "prelude", "help",

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

@ -111,6 +111,7 @@ static name const * g_symm_tk = nullptr;
static name const * g_trans_tk = nullptr;
static name const * g_refl_tk = nullptr;
static name const * g_subst_tk = nullptr;
static name const * g_rewrite_attr_tk = nullptr;
static name const * g_recursor_tk = nullptr;
static name const * g_attribute_tk = nullptr;
static name const * g_with_tk = nullptr;
@ -246,6 +247,7 @@ void initialize_tokens() {
g_trans_tk = new name{"[trans]"};
g_refl_tk = new name{"[refl]"};
g_subst_tk = new name{"[subst]"};
g_rewrite_attr_tk = new name{"[rewrite]"};
g_recursor_tk = new name{"[recursor"};
g_attribute_tk = new name{"attribute"};
g_with_tk = new name{"with"};
@ -382,6 +384,7 @@ void finalize_tokens() {
delete g_trans_tk;
delete g_refl_tk;
delete g_subst_tk;
delete g_rewrite_attr_tk;
delete g_recursor_tk;
delete g_attribute_tk;
delete g_with_tk;
@ -517,6 +520,7 @@ name const & get_symm_tk() { return *g_symm_tk; }
name const & get_trans_tk() { return *g_trans_tk; }
name const & get_refl_tk() { return *g_refl_tk; }
name const & get_subst_tk() { return *g_subst_tk; }
name const & get_rewrite_attr_tk() { return *g_rewrite_attr_tk; }
name const & get_recursor_tk() { return *g_recursor_tk; }
name const & get_attribute_tk() { return *g_attribute_tk; }
name const & get_with_tk() { return *g_with_tk; }

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

@ -113,6 +113,7 @@ name const & get_symm_tk();
name const & get_trans_tk();
name const & get_refl_tk();
name const & get_subst_tk();
name const & get_rewrite_attr_tk();
name const & get_recursor_tk();
name const & get_attribute_tk();
name const & get_with_tk();

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

@ -106,6 +106,7 @@ symm [symm]
trans [trans]
refl [refl]
subst [subst]
rewrite_attr [rewrite]
recursor [recursor
attribute attribute
with with

49
src/library/simplifier/rewrite_rule_set.cpp
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#include <string>
#include "kernel/instantiate.h"
#include "kernel/error_msgs.h"
#include "library/scoped_ext.h"
#include "library/expr_pair.h"
#include "library/relation_manager.h"
@ -17,12 +18,20 @@ bool operator==(rewrite_rule const & r1, rewrite_rule const & r2) {
return r1.m_lhs == r2.m_lhs && r1.m_rhs == r2.m_rhs;
}
rewrite_rule::rewrite_rule(name const & id, list<expr> const & metas,
expr const & lhs, expr const & rhs, constraint_seq const & cs,
expr const & proof, bool is_perm):
m_id(id), m_metas(metas), m_lhs(lhs), m_rhs(rhs), m_cs(cs), m_proof(proof),
rewrite_rule::rewrite_rule(name const & id, levels const & univ_metas, list<expr> const & metas,
expr const & lhs, expr const & rhs, expr const & proof, bool is_perm):
m_id(id), m_univ_metas(univ_metas), m_metas(metas), m_lhs(lhs), m_rhs(rhs), m_proof(proof),
m_is_permutation(is_perm) {}
format rewrite_rule::pp(formatter const & fmt) const {
format r;
r += format("#") + format(length(m_metas));
if (m_is_permutation)
r += space() + format("perm");
r += group(space() + fmt(m_lhs) + space() + format("↦") + pp_indent_expr(fmt, m_rhs));
return r;
}
rewrite_rule_set::rewrite_rule_set(name const & eqv):
m_eqv(eqv) {}
@ -88,7 +97,8 @@ void rewrite_rule_sets::for_each(std::function<void(name const &, rewrite_rule c
static name * g_prefix = nullptr;
rewrite_rule_sets add(type_checker & tc, rewrite_rule_sets const & s, name const & id, expr const & e, expr const & h) {
rewrite_rule_sets add_core(type_checker & tc, rewrite_rule_sets const & s,
name const & id, levels const & univ_metas, expr const & e, expr const & h) {
list<expr_pair> ceqvs = to_ceqvs(tc, e, h);
environment const & env = tc.env();
rewrite_rule_sets new_s = s;
@ -97,23 +107,25 @@ rewrite_rule_sets add(type_checker & tc, rewrite_rule_sets const & s, name const
expr new_h = p.second;
bool is_perm = is_permutation_ceqv(env, new_e);
buffer<expr> metas;
constraint_seq cs;
unsigned idx = 0;
while (is_pi(new_e)) {
expr mvar = mk_metavar(name(*g_prefix, idx), binding_domain(new_e));
idx++;
metas.push_back(mvar);
// TODO(Leo): type class constraints
new_e = instantiate(binding_body(new_e), mvar);
}
expr rel, lhs, rhs;
if (is_equivalence(env, new_e, rel, lhs, rhs) && is_constant(rel)) {
new_s.insert(const_name(rel), rewrite_rule(id, to_list(metas), lhs, rhs, cs, new_h, is_perm));
new_s.insert(const_name(rel), rewrite_rule(id, univ_metas, to_list(metas), lhs, rhs, new_h, is_perm));
}
}
return new_s;
}
rewrite_rule_sets add(type_checker & tc, rewrite_rule_sets const & s, name const & id, expr const & e, expr const & h) {
return add_core(tc, s, id, list<level>(), e, h);
}
rewrite_rule_sets join(rewrite_rule_sets const & s1, rewrite_rule_sets const & s2) {
rewrite_rule_sets new_s1 = s1;
s2.for_each([&](name const & eqv, rewrite_rule const & r) {
@ -127,16 +139,23 @@ static std::string * g_key = nullptr;
struct rrs_state {
rewrite_rule_sets m_sets;
name_set m_rnames;
name_map<rewrite_rule_sets> m_namespace_cache;
void add(environment const & env, name const & cname) {
// TODO(Leo): universe variables
// TODO(Leo): invalide cache for current namespace
type_checker tc(env);
declaration const & d = env.get(cname);
expr e = d.get_type();
expr h = mk_constant(cname);
m_sets = ::lean::add(tc, m_sets, cname, e, h);
buffer<level> us;
unsigned num_univs = d.get_num_univ_params();
for (unsigned i = 0; i < num_univs; i++) {
us.push_back(mk_meta_univ(name(*g_prefix, i)));
}
levels ls = to_list(us);
expr e = instantiate_type_univ_params(d, ls);
expr h = mk_constant(cname, ls);
m_sets = add_core(tc, m_sets, cname, ls, e, h);
m_rnames.insert(cname);
m_namespace_cache.erase(get_namespace(env));
}
};
@ -170,6 +189,10 @@ environment add_rewrite_rule(environment const & env, name const & n, bool persi
return rrs_ext::add_entry(env, get_dummy_ios(), n, persistent);
}
bool is_rewrite_rule(environment const & env, name const & n) {
return rrs_ext::get_state(env).m_rnames.contains(n);
}
rewrite_rule_sets get_rewrite_rule_sets(environment const & env) {
return rrs_ext::get_state(env).m_sets;
}

16
src/library/simplifier/rewrite_rule_set.h
View file

@ -13,26 +13,26 @@ class rewrite_rule_sets;
class rewrite_rule {
name m_id;
levels m_univ_metas;
list<expr> m_metas;
expr m_lhs;
expr m_rhs;
constraint_seq m_cs;
expr m_proof;
bool m_is_permutation;
rewrite_rule(name const & id, list<expr> const & metas,
expr const & lhs, expr const & rhs, constraint_seq const & cs,
expr const & proof, bool is_perm);
friend rewrite_rule_sets add(type_checker & tc, rewrite_rule_sets const & s, name const & id,
expr const & e, expr const & h);
rewrite_rule(name const & id, levels const & univ_metas, list<expr> const & metas,
expr const & lhs, expr const & rhs, expr const & proof, bool is_perm);
friend rewrite_rule_sets add_core(type_checker & tc, rewrite_rule_sets const & s, name const & id,
levels const & univ_metas, expr const & e, expr const & h);
public:
name const & get_id() const { return m_id; }
levels const & get_univ_metas() const { return m_univ_metas; }
list<expr> const & get_metas() const { return m_metas; }
expr const & get_lhs() const { return m_lhs; }
expr const & get_rhs() const { return m_rhs; }
constraint_seq const & get_cs() const { return m_cs; }
expr const & get_proof() const { return m_proof; }
bool is_perm() const { return m_is_permutation; }
friend bool operator==(rewrite_rule const & r1, rewrite_rule const & r2);
format pp(formatter const & fmt) const;
};
bool operator==(rewrite_rule const & r1, rewrite_rule const & r2);
@ -69,6 +69,8 @@ rewrite_rule_sets add(type_checker & tc, rewrite_rule_sets const & s, name const
rewrite_rule_sets join(rewrite_rule_sets const & s1, rewrite_rule_sets const & s2);
environment add_rewrite_rule(environment const & env, name const & n, bool persistent = true);
/** \brief Return true if \c n is an active rewrite rule in \c env */
bool is_rewrite_rule(environment const & env, name const & n);
/** \brief Get current rewrite rule sets */
rewrite_rule_sets get_rewrite_rule_sets(environment const & env);
/** \brief Get rewrite rule sets in the given namespace. */

16
tests/lean/run/rw_set1.lean Normal file
View file

@ -0,0 +1,16 @@
import data.nat
namespace foo
attribute nat.add.assoc [rewrite]
print nat.add.assoc
end foo
print nat.add.assoc
namespace foo
print nat.add.assoc
attribute nat.add.comm [rewrite]
open nat
print "---------"
print [rewrite]
end foo

12
tests/lean/rw_set2.lean Normal file
View file

@ -0,0 +1,12 @@
open nat
constant f : nat → nat
constant g : nat → nat
axiom foo : ∀ x, x > 0 → f x = 0 ∧ g x = 1
axiom bla : ∀ x, g x = f x + 1
attribute foo [rewrite]
attribute bla [rewrite]
print [rewrite]

4
tests/lean/rw_set2.lean.expected.out Normal file
View file

@ -0,0 +1,4 @@
rewrite rules for eq
#1 g ?M_1 ↦ f ?M_1 + 1
#2 g ?M_1 ↦ 1
#2 f ?M_1 ↦ 0