From 35022dbeca8baba9b6350bf5b9ff969d2e935fde Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 13 Jun 2016 12:26:41 -0700
Subject: [PATCH] feat(frontends/lean/pp): pp should not fail if infer_type
 fails for locals and/or metas

---
 src/frontends/lean/pp.cpp | 27 +++++++++++++++++++--------
 src/frontends/lean/pp.h   |  1 +
 2 files changed, 20 insertions(+), 8 deletions(-)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index f8b1c47271..c885b2a34c 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -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();
+            }
         });
 }
 
diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h
index 26569ebb5e..404f451dcf 100644
--- a/src/frontends/lean/pp.h
+++ b/src/frontends/lean/pp.h
@@ -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);