max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(frontends/lean/pp): pp should not fail if infer_type fails for locals and/or metas

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-13 12:26:41 -07:00
parent 695bba6291
commit 35022dbeca
2 changed files with 20 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -242,6 +242,15 @@ level pretty_fn::purify(level const & l) {
});
}
expr pretty_fn::infer_type(expr const & e) {
try {
return m_ctx.infer(e);
} catch (exception &) {
expr dummy = mk_Prop();
return dummy;
}
}
/** \brief Make sure that all metavariables have reasonable names,
and for all local constants l1 l2, local_pp_name(l1) != local_pp_name(l2).
@ -252,18 +261,20 @@ expr pretty_fn::purify(expr const & e) {
if (!has_expr_metavar(e) && !has_local(e) && (!m_universes || !has_univ_metavar(e)))
return e;
return replace(e, [&](expr const & e, unsigned) {
if (!has_expr_metavar(e) && !has_local(e) && (!m_universes || !has_univ_metavar(e)))
if (!has_expr_metavar(e) && !has_local(e) && (!m_universes || !has_univ_metavar(e))) {
return some_expr(e);
else if (is_metavar(e) && m_purify_metavars)
return some_expr(mk_metavar(mk_metavar_name(mlocal_name(e)), m_ctx.infer(e)));
else if (is_local(e))
return some_expr(mk_local(mlocal_name(e), mk_local_name(mlocal_name(e), m_ctx.get_local_pp_name(e)), m_ctx.infer(e), local_info(e)));
else if (is_constant(e))
} else if (is_metavar(e) && m_purify_metavars) {
return some_expr(mk_metavar(mk_metavar_name(mlocal_name(e)), infer_type(e)));
} else if (is_local(e)) {
return some_expr(mk_local(mlocal_name(e), mk_local_name(mlocal_name(e), m_ctx.get_local_pp_name(e)),
infer_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))
} else if (is_sort(e)) {
return some_expr(update_sort(e, purify(sort_level(e))));
else
} else {
return none_expr();
}
});
}

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

@ -125,6 +125,7 @@ private:
result pp_abbreviation(expr const & e, name const & abbrev, bool fn, unsigned bp = 0, bool ignore_hide = false);
void set_options_core(options const & o);
expr infer_type(expr const & e);
public:
pretty_fn(environment const & env, options const & o, abstract_type_context & ctx);
result pp(expr const & e, bool ignore_hide = false);