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

fix(frontends/lean/pp): do not invoke type checker on expressions

Browse source 
containing free variables.

This could happened when the pretty printer was used from Lua to print
nested subterms
This commit is contained in:
Leonardo de Moura 2014-09-26 09:38:36 -07:00
parent 8143b51c7e
commit 6bf905aea8
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -183,6 +183,10 @@ format pretty_fn::pp_level(level const & l) {
bool pretty_fn::is_implicit(expr const & f) {
if (m_implict)
return false; // showing implicit arguments
if (!closed(f)) {
// the Lean type checker assumes expressions are closed.
return false;
}
try {
binder_info bi = binding_info(m_tc.ensure_pi(m_tc.infer(f).first).first);
return bi.is_implicit() || bi.is_strict_implicit();
@ -320,6 +324,10 @@ auto pretty_fn::pp_local(expr const & e) -> result {
}
bool pretty_fn::has_implicit_args(expr const & f) {
if (!closed(f)) {
// the Lean type checker assumes expressions are closed.
return false;
}
name_generator ngen(*g_tmp_prefix);
try {
expr type = m_tc.whnf(m_tc.infer(f).first).first;