From e4e9c30e66c55517c8c86ffbece7f9b10bb238ff Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 26 Nov 2015 12:59:21 -0800
Subject: [PATCH] fix(frontends/lean/builtin_cmds): print patterns

---
 src/frontends/lean/builtin_cmds.cpp | 32 ++++++++++++++++-------------
 tests/lean/run/pattern2.lean        | 17 +++++++++++++++
 tests/lean/run/pattern3.lean        |  6 ++++++
 3 files changed, 41 insertions(+), 14 deletions(-)
 create mode 100644 tests/lean/run/pattern2.lean
 create mode 100644 tests/lean/run/pattern3.lean

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 95ca2f33c..bd83225b7 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -231,6 +231,23 @@ static void print_metaclasses(parser const & p) {
         p.regular_stream() << "[" << n << "]" << endl;
 }
 
+static void print_patterns(io_state_stream const & out, environment const & env, name const & n) {
+    if (auto lemma = get_hi_lemma(env, n)) {
+        if (lemma->m_multi_patterns) {
+            out << "(multi-)patterns:\n";
+            for (multi_pattern const & mp : lemma->m_multi_patterns) {
+                out << "{";
+                bool first = true;
+                for (expr const & p : mp) {
+                    if (first) first = false; else out << ", ";
+                    out << p;
+                }
+                out << "}\n";
+            }
+        }
+    }
+}
+
 static void print_definition(parser const & p, name const & n, pos_info const & pos) {
     environment const & env = p.env();
     declaration d = env.get(n);
@@ -244,20 +261,6 @@ static void print_definition(parser const & p, name const & n, pos_info const &
     if (!d.is_definition())
         throw parser_error(sstream() << "invalid 'print definition', '" << n << "' is not a definition", pos);
     new_out << d.get_value() << endl;
-    if (auto lemma = get_hi_lemma(env, n)) {
-        if (lemma->m_multi_patterns) {
-            new_out << "(multi-)patterns:\n";
-            for (multi_pattern const & mp : lemma->m_multi_patterns) {
-                new_out << "{";
-                bool first = true;
-                for (expr const & p : mp) {
-                    if (first) first = false; else new_out << ", ";
-                    new_out << p;
-                }
-                new_out << "}\n";
-            }
-        }
-    }
 }
 
 static void print_attributes(parser const & p, name const & n) {
@@ -414,6 +417,7 @@ bool print_id_info(parser const & p, name const & id, bool show_value, pos_info
                     if (show_value)
                         print_definition(p, c, pos);
                 }
+                print_patterns(out, env, c);
             }
             return true;
         } catch (exception & ex) {}
diff --git a/tests/lean/run/pattern2.lean b/tests/lean/run/pattern2.lean
new file mode 100644
index 000000000..b9f4d1bd8
--- /dev/null
+++ b/tests/lean/run/pattern2.lean
@@ -0,0 +1,17 @@
+constant f : nat → nat → nat
+constant g : nat → nat → nat
+attribute g [no_pattern]
+
+namespace foo
+
+definition lemma1 [forward] {a b : nat} : f a b = g a b :=
+sorry
+
+end foo
+
+print foo.lemma1
+open foo
+print foo.lemma1
+attribute foo.lemma1 [forward]
+
+print foo.lemma1
diff --git a/tests/lean/run/pattern3.lean b/tests/lean/run/pattern3.lean
new file mode 100644
index 000000000..86d761ff7
--- /dev/null
+++ b/tests/lean/run/pattern3.lean
@@ -0,0 +1,6 @@
+constant Sum : (nat → nat) → nat → nat
+
+lemma l1 [forward] (f : nat → nat) : Sum f 0 = 0 :=
+sorry
+
+print l1