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

feat(frontends/lean/bultin_cmds): add 'print [congr]' command for displaying active congruence rules

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-23 16:11:37 -07:00
parent 3329dc0ec7
commit 844caf32e4
3 changed files with 26 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -379,7 +379,7 @@ static void print_reducible_info(parser & p, reducible_status s1) {
out << n << "\n";
}
static void print_simp_sets(parser & p) {
static void print_simp_rules(parser & p) {
io_state_stream out = p.regular_stream();
simp_rule_sets s;
name ns;
@ -403,6 +403,19 @@ static void print_simp_sets(parser & p) {
});
}
static void print_congr_rules(parser & p) {
io_state_stream out = p.regular_stream();
simp_rule_sets s = get_simp_rule_sets(p.env());
name prev_eqv;
s.for_each_congr([&](name const & eqv, congr_rule const & cr) {
if (prev_eqv != eqv) {
out << "congruencec rules for " << eqv << "\n";
prev_eqv = eqv;
}
out << cr.pp(out.get_formatter()) << "\n";
});
}
environment print_cmd(parser & p) {
flycheck_information info(p.regular_stream());
if (info.enabled()) {
@ -507,7 +520,10 @@ environment print_cmd(parser & p) {
print_recursor_info(p);
} else if (p.curr_is_token(get_simp_attr_tk())) {
p.next();
print_simp_sets(p);
print_simp_rules(p);
} else if (p.curr_is_token(get_congr_attr_tk())) {
p.next();
print_congr_rules(p);
} else if (print_polymorphic(p)) {
} else {
throw parser_error("invalid print command", p.pos());

6
src/library/simplifier/simp_rule_set.cpp
View file

@ -54,12 +54,12 @@ format congr_rule::pp(formatter const & fmt) const {
r += format("#") + format(length(m_metas));
format r1;
for (expr const & h : m_congr_hyps) {
r1 += space() + paren(pp_indent_expr(fmt, mlocal_type(h)));
r1 += space() + paren(fmt(mlocal_type(h)));
}
r += group(r1);
r += space() + format(":") + space();
format r2 = fmt(m_lhs);
r2 += space() + format("↦") + pp_indent_expr(fmt, m_rhs);
format r2 = paren(fmt(m_lhs));
r2 += space() + format("↦") + space() + paren(fmt(m_rhs));
r += group(r2);
return r;
}

5
tests/lean/run/congr.lean Normal file
View file

@ -0,0 +1,5 @@
import data.equiv
open equiv
open contextual
print [congr]