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

fix(kernel/formatter): make sure simple formatter output is not sensitive to internal names

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-26 14:58:59 -07:00
parent 150d285b39
commit 340dc622c6
3 changed files with 27 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/kernel/formatter.cpp
View file

@ -37,6 +37,24 @@ std::pair<expr, expr> binding_body_fresh(expr const & b, bool preserve_type) {
return mk_pair(instantiate(binding_body(b), c), c);
}
static name g_internal("M");
name fix_internal_name(name const & a) {
if (a.is_atomic()) {
if (a.is_numeral())
return g_internal;
else
return a;
} else {
name p = fix_internal_name(a.get_prefix());
if (p == a.get_prefix())
return a;
else if (a.is_numeral())
return name(p, a.get_numeral());
else
return name(p, a.get_string());
}
}
/**
\brief Very basic printer for expressions.
It is mainly used when debugging code.
@ -176,10 +194,10 @@ struct print_expr_fn {
void print(expr const & a) {
switch (a.kind()) {
case expr_kind::Meta:
out() << "?" << mlocal_name(a);
out() << "?" << fix_internal_name(mlocal_name(a));
break;
case expr_kind::Local:
out() << local_pp_name(a);
out() << fix_internal_name(local_pp_name(a));
break;
case expr_kind::Var:
out() << "#" << var_idx(a);

6
tests/lean/t6.lean.expected.out
View file

@ -1,3 +1,3 @@
id.{2} ?2.1 : ?2.1 -> ?2.1
refl.{1} ?2.1 : (?2.1 -> ?2.1 -> Bool) -> Bool
symm.{1} ?2.1 : (?2.1 -> ?2.1 -> Bool) -> Bool
id.{2} ?M.1 : ?M.1 -> ?M.1
refl.{1} ?M.1 : (?M.1 -> ?M.1 -> Bool) -> Bool
symm.{1} ?M.1 : (?M.1 -> ?M.1 -> Bool) -> Bool

8
tests/lean/t7.lean.expected.out
View file

@ -1,5 +1,5 @@
id.{2} ?2.1 : ?2.1 -> ?2.1
trans.{1} ?2.1 : (?2.1 -> ?2.1 -> Bool) -> Bool
symm.{1} ?2.1 : (?2.1 -> ?2.1 -> Bool) -> Bool
equivalence.{1} ?2.1 : (?2.1 -> ?2.1 -> Bool) -> Bool
id.{2} ?M.1 : ?M.1 -> ?M.1
trans.{1} ?M.1 : (?M.1 -> ?M.1 -> Bool) -> Bool
symm.{1} ?M.1 : (?M.1 -> ?M.1 -> Bool) -> Bool
equivalence.{1} ?M.1 : (?M.1 -> ?M.1 -> Bool) -> Bool
fun {A : Type.{l_1}} (R : A -> A -> Bool), (and (and (private.3808308840.refl.{l_1} A R) (symm.{l_1} A R)) (trans.{l_1} A R))