feat(frontends/lean/builtin_cmds): add 'print classes' command

src/emacs/lean-syntax.el

@@ -15,7 +15,7 @@
     "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl"
     "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"
     "using" "namespace" "instance" "class" "section"
-    "set_option" "add_rewrite" "extends" "include" "omit" "instances" "coercions" "raw")
+    "set_option" "add_rewrite" "extends" "include" "omit" "classes" "instances" "coercions" "raw")
   "lean keywords")
 
 (defconst lean-syntax-table

src/frontends/lean/builtin_cmds.cpp

@@ -70,6 +70,15 @@ environment print_cmd(parser & p) {
         for (name const & i : get_class_instances(env, c)) {
             p.regular_stream() << i << " : " << env.get(i).get_type() << endl;
         }
+    } else if (p.curr_is_token_or_id(get_classes_tk())) {
+        p.next();
+        environment const & env = p.env();
+        buffer<name> classes;
+        get_classes(env, classes);
+        std::sort(classes.begin(), classes.end());
+        for (name const & c : classes) {
+            p.regular_stream() << c << " : " << env.get(c).get_type() << endl;
+        }
     } else if (p.curr_is_token_or_id(get_coercions_tk())) {
         p.next();
         optional<name> C;

src/frontends/lean/class.cpp

@@ -136,6 +136,13 @@ environment add_class(environment const & env, name const & n, bool persistent)
     return class_ext::add_entry(env, get_dummy_ios(), class_entry(n), persistent);
 }
 
+void get_classes(environment const & env, buffer<name> & classes) {
+    class_state const & s = class_ext::get_state(env);
+    s.m_instances.for_each([&](name const & c, list<name> const &) {
+            classes.push_back(c);
+        });
+}
+
 static name * g_tmp_prefix = nullptr;
 environment add_instance(environment const & env, name const & n, unsigned priority, bool persistent) {
     declaration d = env.get(n);

src/frontends/lean/class.h

@@ -21,6 +21,8 @@ environment add_instance(environment const & env, name const & n, unsigned prior
 bool is_class(environment const & env, name const & c);
 /** \brief Return the instances of the given class. */
 list<name> get_class_instances(environment const & env, name const & c);
+/** \brief Return the classes in the given environment. */
+void get_classes(environment const & env, buffer<name> & classes);
 name get_class_name(environment const & env, expr const & e);
 /** \brief Parse priority for an class instance */
 optional<unsigned> parse_instance_priority(parser & p);

src/frontends/lean/tokens.cpp

@@ -38,6 +38,7 @@ static name * g_true         = nullptr;
 static name * g_false        = nullptr;
 static name * g_options      = nullptr;
 static name * g_instances    = nullptr;
+static name * g_classes      = nullptr;
 static name * g_coercions    = nullptr;
 static name * g_arrow        = nullptr;
 static name * g_declarations = nullptr;
@@ -119,6 +120,7 @@ void initialize_tokens() {
     g_false        = new name("false");
     g_options      = new name("options");
     g_instances    = new name("instances");
+    g_classes      = new name("classes");
     g_coercions    = new name("coercions");
     g_arrow        = new name("->");
     g_declarations = new name("declarations");
@@ -211,6 +213,7 @@ void finalize_tokens() {
     delete g_false;
     delete g_options;
     delete g_instances;
+    delete g_classes;
     delete g_coercions;
     delete g_arrow;
     delete g_declarations;
@@ -282,6 +285,7 @@ name const & get_true_tk() { return *g_true; }
 name const & get_false_tk() { return *g_false; }
 name const & get_options_tk() { return *g_options; }
 name const & get_instances_tk() { return *g_instances; }
+name const & get_classes_tk() { return *g_classes; }
 name const & get_coercions_tk() { return *g_coercions; }
 name const & get_arrow_tk() { return *g_arrow; }
 name const & get_declarations_tk() { return *g_declarations; }

src/frontends/lean/tokens.h

@@ -40,6 +40,7 @@ name const & get_true_tk();
 name const & get_false_tk();
 name const & get_options_tk();
 name const & get_instances_tk();
+name const & get_classes_tk();
 name const & get_coercions_tk();
 name const & get_arrow_tk();
 name const & get_declarations_tk();

tests/lean/run/print.lean

@@ -7,3 +7,5 @@ print options
 print coercions functor
 print "-----------"
 print coercions
+print "-----------"
+print classes