From 90dba868e33ee0b85236688bf54d56db295fb3e9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 14 Oct 2014 17:37:20 -0700
Subject: [PATCH] feat(library/tactic/proof_state): apply substitutions when
 pretty printing state

---
 src/library/tactic/goal.cpp         | 11 +++++++++--
 src/library/tactic/goal.h           |  1 +
 src/library/tactic/proof_state.cpp  |  5 +++--
 tests/lean/goals1.lean              |  9 +++++++++
 tests/lean/goals1.lean.expected.out |  5 +++++
 5 files changed, 27 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/goals1.lean
 create mode 100644 tests/lean/goals1.lean.expected.out

diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp
index 969e3f772..7701b43c2 100644
--- a/src/library/tactic/goal.cpp
+++ b/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);
 }
 
diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h
index 0689accb0..5763b86ba 100644
--- a/src/library/tactic/goal.h
+++ b/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;
 };
 
diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp
index 54b779c66..91d8b0592 100644
--- a/src/library/tactic/proof_state.cpp
+++ b/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");
diff --git a/tests/lean/goals1.lean b/tests/lean/goals1.lean
new file mode 100644
index 000000000..9fe667a05
--- /dev/null
+++ b/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
diff --git a/tests/lean/goals1.lean.expected.out b/tests/lean/goals1.lean.expected.out
new file mode 100644
index 000000000..1d0423a75
--- /dev/null
+++ b/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