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

fix(frontends/lean/pp): purify procedure for local names

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-10 14:13:51 +01:00
parent fc8ddcb0ce
commit 49bc3fffbd
3 changed files with 14 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/frontends/lean/pp.cpp
View file

@ -39,14 +39,17 @@ name pretty_fn::mk_metavar_name(name const & m) {
return new_m;
}
name pretty_fn::mk_local_name(name const & m) {
name pretty_fn::mk_local_name(name const & n, name const & suggested) {
if (auto it = m_purify_local_table.find(n))
return *it;
unsigned i = 1;
name r = m;
while (m_purify_locals.contains(r)) {
r = m.append_after(i);
name r = suggested;
while (m_purify_used_locals.contains(r)) {
r = suggested.append_after(i);
i++;
}
m_purify_locals.insert(r);
m_purify_used_locals.insert(r);
m_purify_local_table.insert(n, r);
return r;
}
@ -77,7 +80,7 @@ expr pretty_fn::purify(expr const & e) {
else if (is_metavar(e))
return some_expr(mk_metavar(mk_metavar_name(mlocal_name(e)), mlocal_type(e)));
else if (is_local(e))
return some_expr(mk_local(mlocal_name(e), mk_local_name(local_pp_name(e)), mlocal_type(e), local_info(e)));
return some_expr(mk_local(mlocal_name(e), mk_local_name(mlocal_name(e), local_pp_name(e)), mlocal_type(e), local_info(e)));
else if (is_constant(e))
return some_expr(update_constant(e, map(const_levels(e), [&](level const & l) { return purify(l); })));
else if (is_sort(e))

5
src/frontends/lean/pp.h
View file

@ -26,7 +26,8 @@ private:
name m_meta_prefix;
unsigned m_next_meta_idx;
name_map<name> m_purify_meta_table;
name_set m_purify_locals;
name_map<name> m_purify_local_table;
name_set m_purify_used_locals;
// cached configuration
unsigned m_indent;
unsigned m_max_depth;
@ -41,7 +42,7 @@ private:
unsigned max_bp() const { return std::numeric_limits<unsigned>::max(); }
name mk_metavar_name(name const & m);
name mk_local_name(name const & m);
name mk_local_name(name const & n, name const & suggested);
level purify(level const & l);
expr purify(expr const & e);
result mk_result(format const & e, unsigned rbp) const { return mk_pair(e, rbp); }

4
tests/lean/t4.lean.expected.out
View file

@ -5,8 +5,8 @@ F : Type → Type
F : Type → Type
f : N → N → N
len : Π (A : Type) (n : N), vec A n → N
B → B_1 : Bool
A → A_1 : Type
B → B : Bool
A → A : Type
C : Type
t4.lean:25:6: error: unknown identifier 'A'
R : Type → Bool