From d58c3e498d7caedf4a57e84c48ceed92d555f9eb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 4 Nov 2014 08:40:32 -0800
Subject: [PATCH] feat(frontends/lean/builtin_cmds): add 'print prefix' command

---
 src/frontends/lean/builtin_cmds.cpp | 20 ++++++++++++++++++++
 tests/lean/run/group4.lean          | 26 ++++++++++++++------------
 tests/lean/run/record7.lean         |  9 +++++++++
 3 files changed, 43 insertions(+), 12 deletions(-)
 create mode 100644 tests/lean/run/record7.lean

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 7b3bc360a..3f87b5090 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -73,6 +73,23 @@ static void print_axioms(parser & p) {
         p.regular_stream() << "no axioms" << endl;
 }
 
+static void print_prefix(parser & p) {
+    name prefix = p.check_id_next("invalid 'print prefix' command, identifier expected");
+    environment const & env = p.env();
+    buffer<declaration> to_print;
+    env.for_each_declaration([&](declaration const & d) {
+            if (is_prefix_of(prefix, d.get_name())) {
+                to_print.push_back(d);
+            }
+        });
+    std::sort(to_print.begin(), to_print.end(), [](declaration const & d1, declaration const & d2) { return d1.get_name() < d2.get_name(); });
+    for (declaration const & d : to_print) {
+        p.regular_stream() << d.get_name() << " : " << d.get_type() << endl;
+    }
+    if (to_print.empty())
+        p.regular_stream() << "no declaration starting with prefix '" << prefix << "'" << endl;
+}
+
 environment print_cmd(parser & p) {
     if (p.curr() == scanner::token_kind::String) {
         p.regular_stream() << p.get_str_val() << endl;
@@ -112,6 +129,9 @@ environment print_cmd(parser & p) {
         for (name const & c : classes) {
             p.regular_stream() << c << " : " << env.get(c).get_type() << endl;
         }
+    } else if (p.curr_is_token_or_id(get_prefix_tk())) {
+        p.next();
+        print_prefix(p);
     } else if (p.curr_is_token_or_id(get_coercions_tk())) {
         p.next();
         optional<name> C;
diff --git a/tests/lean/run/group4.lean b/tests/lean/run/group4.lean
index 585340080..33e8ab0ec 100644
--- a/tests/lean/run/group4.lean
+++ b/tests/lean/run/group4.lean
@@ -75,6 +75,8 @@ end
 
 structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A
 
+print prefix algebra.comm_monoid
+
 structure Semigroup :=
 mk :: (carrier : Type) (struct : semigroup carrier)
 
@@ -107,15 +109,15 @@ section examples
 
 theorem test1 {S : Semigroup} (a b c d : S) : a * (b * c) * d = a * b * (c * d) :=
 calc
-  a * (b * c) * d = a * b * c * d   : {symm !mul_assoc}
-              ... = a * b * (c * d) : !mul_assoc
+  a * (b * c) * d = a * b * c * d   : mul_assoc
+              ... = a * b * (c * d) : mul_assoc
 
 theorem test2 {M : CommSemigroup} (a b : M) : a * b = a * b := rfl
 
 theorem test3 {M : Monoid} (a b c d : M) : a * (b * c) * d = a * b * (c * d) :=
 calc
-  a * (b * c) * d = a * b * c * d   : {symm !mul_assoc}
-              ... = a * b * (c * d) : !mul_assoc
+  a * (b * c) * d = a * b * c * d   : mul_assoc
+              ... = a * b * (c * d) : mul_assoc
 
 -- for test4b to work, we need instances at the level of the bundled structures as well
 definition Monoid_Semigroup [coercion] (M : Monoid) : Semigroup :=
@@ -126,21 +128,21 @@ test1 a b c d
 
 theorem test5 {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
 calc
-  a * 1 * b * c = a * b * c   : {!mul_right_id}
-            ... = a * (b * c) : !mul_assoc
+  a * 1 * b * c = a * b * c   : mul_right_id
+            ... = a * (b * c) : mul_assoc
 
 theorem test5a {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
 calc
-  a * 1 * b * c = a * b * c   : {!mul_right_id}
-            ... = a * (b * c) : !mul_assoc
+  a * 1 * b * c = a * b * c   : mul_right_id
+            ... = a * (b * c) : mul_assoc
 
 theorem test5b {A : Type} {M : monoid A} (a b c : A) : a * 1 * b * c = a * (b * c) :=
 calc
-  a * 1 * b * c = a * b * c   : {!mul_right_id}
-            ... = a * (b * c) : !mul_assoc
+  a * 1 * b * c = a * b * c   : mul_right_id
+            ... = a * (b * c) : mul_assoc
 
 theorem test6 {M : CommMonoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
 calc
-  a * 1 * b * c = a * b * c   : {!mul_right_id}
-            ... = a * (b * c) : !mul_assoc
+  a * 1 * b * c = a * b * c   : mul_right_id
+            ... = a * (b * c) : mul_assoc
 end examples
diff --git a/tests/lean/run/record7.lean b/tests/lean/run/record7.lean
new file mode 100644
index 000000000..60031b31e
--- /dev/null
+++ b/tests/lean/run/record7.lean
@@ -0,0 +1,9 @@
+import logic data.unit
+
+structure point (A : Type) (B : Type) :=
+mk :: (x : A) (y : B)
+
+structure point2 (A : Type) (B : Type) extends point A B :=
+make
+
+print prefix point2