feat(library/tactic/proof_state): apply substitutions when pretty printing state

src/library/tactic/goal.cpp

@@ -11,11 +11,17 @@ Author: Leonardo de Moura
 #include "kernel/for_each_fn.h"
 #include "kernel/abstract.h"
 #include "kernel/type_checker.h"
+#include "kernel/metavar.h"
 #include "library/kernel_bindings.h"
 #include "library/tactic/goal.h"
 
 namespace lean {
 format goal::pp(formatter const & fmt) const {
+    return pp(fmt, substitution());
+}
+
+format goal::pp(formatter const & fmt, substitution const & s) const {
+    substitution tmp_subst(s);
     options const & opts = fmt.get_options();
     unsigned indent  = get_pp_indent(opts);
     bool unicode     = get_pp_unicode(opts);
@@ -29,10 +35,11 @@ format goal::pp(formatter const & fmt) const {
     for (auto it = tmp.begin(); it != end; ++it) {
         if (first) first = false; else r += compose(comma(), line());
         expr l     = *it;
-        r += fmt(l) + space() + colon() + nest(indent, line() + fmt(mlocal_type(l)));
+        expr t     = tmp_subst.instantiate(mlocal_type(l));
+        r += fmt(l) + space() + colon() + nest(indent, line() + fmt(t));
     }
     r = group(r);
-    r += line() + turnstile + space() + nest(indent, fmt(conclusion));
+    r += line() + turnstile + space() + nest(indent, fmt(tmp_subst.instantiate(conclusion)));
     return group(r);
 }
 

src/library/tactic/goal.h

@@ -72,6 +72,7 @@ public:
     */
     list<expr> to_context() const;
 
+    format pp(formatter const & fmt, substitution const & s) const;
     format pp(formatter const & fmt) const;
 };
 

src/library/tactic/proof_state.cpp

@@ -45,12 +45,13 @@ format proof_state::pp(formatter const & fmt) const {
     unsigned indent      = get_pp_indent(opts);
     format r;
     bool first = true;
+
     for (auto const & g : get_goals()) {
         if (first) first = false; else r += line();
         if (show_goal_names) {
-            r += group(format(g.get_name()) + colon() + nest(indent, line() + g.pp(fmt)));
+            r += group(format(g.get_name()) + colon() + nest(indent, line() + g.pp(fmt, m_subst)));
         } else {
-            r += g.pp(fmt);
+            r += g.pp(fmt, m_subst);
         }
     }
     if (first) r = format("no goals");

tests/lean/goals1.lean

@@ -0,0 +1,9 @@
+import tools.tactic
+open tactic
+set_option pp.notation false
+
+theorem foo (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c :=
+begin
+  apply eq.trans,
+  apply Hbc
+end

tests/lean/goals1.lean.expected.out

@@ -0,0 +1,5 @@
+goals1.lean:9:0: error: unsolved placeholder, unsolved subgoals
+A : Type, a : A, b : A, c : A, Hab : eq a b, Hbc : eq b c ⊢ eq a b
+goals1.lean:9:0: error: failed to add declaration 'foo' to environment, value has metavariables
+  λ (A : Type) (a b c : A) (Hab : eq a b) (Hbc : eq b c),
+    ?M_1