From 67a4cd3972b3f415928c6b05d4abe3d44b9d5323 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 24 Nov 2015 16:02:28 -0800
Subject: [PATCH] feat(frontends/lean): add `print [no_pattern]` command

---
 src/frontends/lean/builtin_cmds.cpp   | 16 ++++++++++++++++
 src/library/blast/forward/pattern.cpp |  4 ++++
 src/library/blast/forward/pattern.h   |  2 ++
 tests/lean/run/print_no_pattern.lean  |  1 +
 4 files changed, 23 insertions(+)
 create mode 100644 tests/lean/run/print_no_pattern.lean

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index c3431a349..c36422372 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -508,6 +508,19 @@ static void print_backward_rules(parser & p) {
     out << brs;
 }
 
+static void print_no_patterns(parser & p) {
+    io_state_stream out = p.regular_stream();
+    auto s = get_no_patterns(p.env());
+    buffer<name> ns;
+    s.to_buffer(ns);
+    std::sort(ns.begin(), ns.end());
+    for (unsigned i = 0; i < ns.size(); i++) {
+        if (i > 0) out << ", ";
+        out << ns[i];
+    }
+    out << "\n";
+}
+
 environment print_cmd(parser & p) {
     flycheck_information info(p.regular_stream());
     if (info.enabled()) {
@@ -524,6 +537,9 @@ environment print_cmd(parser & p) {
         options opts = out.get_options();
         opts = opts.update(get_pp_notation_option_name(), false);
         out.update_options(opts) << e << endl;
+    } else if (p.curr_is_token_or_id(get_no_pattern_attr_tk())) {
+        p.next();
+        print_no_patterns(p);
     } else if (p.curr_is_token_or_id(get_reducible_tk())) {
         p.next();
         print_reducible_info(p, reducible_status::Reducible);
diff --git a/src/library/blast/forward/pattern.cpp b/src/library/blast/forward/pattern.cpp
index 65a4aa48b..59fd2110c 100644
--- a/src/library/blast/forward/pattern.cpp
+++ b/src/library/blast/forward/pattern.cpp
@@ -69,6 +69,10 @@ environment add_no_pattern(environment const & env, name const & n, bool persist
     return no_pattern_ext::add_entry(env, get_dummy_ios(), n, persistent);
 }
 
+name_set const & get_no_patterns(environment const & env) {
+    return no_pattern_ext::get_state(env);
+}
+
 /** pattern_le */
 struct pattern_le_fn {
     tmp_type_context & m_ctx;
diff --git a/src/library/blast/forward/pattern.h b/src/library/blast/forward/pattern.h
index 32865000a..37f338d04 100644
--- a/src/library/blast/forward/pattern.h
+++ b/src/library/blast/forward/pattern.h
@@ -22,6 +22,8 @@ bool has_patterns(expr const & e);
 environment add_no_pattern(environment const & env, name const & n, bool persistent);
 /** \brief Return true if constant \c n is marked as [no_pattern] in the given environment. */
 bool is_no_pattern(environment const & env, name const & n);
+/** \brief Return the set of constants marked as no-patterns */
+name_set const & get_no_patterns(environment const & env);
 
 void initialize_pattern();
 void finalize_pattern();
diff --git a/tests/lean/run/print_no_pattern.lean b/tests/lean/run/print_no_pattern.lean
new file mode 100644
index 000000000..ac4db0ff7
--- /dev/null
+++ b/tests/lean/run/print_no_pattern.lean
@@ -0,0 +1 @@
+print [no_pattern]