feat(frontends/lean/print_cmd): implement 'print attributes'

extras/latex/lstlean.tex

@@ -22,7 +22,7 @@ tactic_infix, tactic_infixl, tactic_infixr, tactic_notation, tactic_postfix, tac
 eval, check, coercion, end, reveal, this, suppose,
 using, namespace, section, fields, find_decl,
 attribute, local, set_option, extends, include, omit, classes,
-instances, coercions, metaclasses, raw, migrate, replacing,
+instances, coercions, attributes, raw, migrate, replacing,
 calc, have, obtains, show, suffices, by, by+, in, at, let, forall, Pi, fun,
 exists, if, dif, then, else, assume, assert, take,
 obtain, from, aliases

src/emacs/lean-syntax.el

@@ -18,7 +18,7 @@
     "eval" "vm_eval" "check" "end" "reveal" "this" "suppose"
     "using_well_founded" "namespace" "section" "fields" "find_decl"
     "attribute" "local" "set_option" "extends" "include" "omit" "classes"
-    "instances" "coercions" "metaclasses" "raw" "migrate" "replacing"
+    "instances" "coercions" "attributes" "raw" "migrate" "replacing"
     "calc" "have" "show" "suffices" "by" "in" "at" "do" "let" "forall" "Pi" "fun"
     "exists" "if" "dif" "then" "else" "assume" "take" "obtain" "from" "aliases" "register_simp_ext"
     "mutual_definition" "mutual_inductive" "def" "mutual_def")

src/frontends/lean/print_cmd.cpp

@@ -604,13 +604,22 @@ environment print_cmd(parser & p) {
         }
     } 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) {
             out << c << " : " << env.get(c).get_type() << endl;
         }
+    } else if (p.curr_is_token_or_id(get_attributes_tk())) {
+        p.next();
+        buffer<attribute const *> attrs;
+        get_attributes(attrs);
+        std::sort(attrs.begin(), attrs.end(), [](attribute const * a1, attribute const * a2) {
+            return a1->get_name() < a2->get_name();
+        });
+        for (auto attr : attrs) {
+            out << "[" << attr->get_name() << "] " << attr->get_description() << endl;
+        }
     } else if (p.curr_is_token_or_id(get_prefix_tk())) {
         p.next();
         print_prefix(p);

src/frontends/lean/tokens.cpp

@@ -61,6 +61,7 @@ static name const * g_options_tk = nullptr;
 static name const * g_commands_tk = nullptr;
 static name const * g_instances_tk = nullptr;
 static name const * g_classes_tk = nullptr;
+static name const * g_attributes_tk = nullptr;
 static name const * g_arrow_tk = nullptr;
 static name const * g_larrow_tk = nullptr;
 static name const * g_hiding_tk = nullptr;
@@ -201,6 +202,7 @@ void initialize_tokens() {
     g_commands_tk = new name{"commands"};
     g_instances_tk = new name{"instances"};
     g_classes_tk = new name{"classes"};
+    g_attributes_tk = new name{"attributes"};
     g_arrow_tk = new name{"->"};
     g_larrow_tk = new name{"<-"};
     g_hiding_tk = new name{"hiding"};
@@ -342,6 +344,7 @@ void finalize_tokens() {
     delete g_commands_tk;
     delete g_instances_tk;
     delete g_classes_tk;
+    delete g_attributes_tk;
     delete g_arrow_tk;
     delete g_larrow_tk;
     delete g_hiding_tk;
@@ -482,6 +485,7 @@ name const & get_options_tk() { return *g_options_tk; }
 name const & get_commands_tk() { return *g_commands_tk; }
 name const & get_instances_tk() { return *g_instances_tk; }
 name const & get_classes_tk() { return *g_classes_tk; }
+name const & get_attributes_tk() { return *g_attributes_tk; }
 name const & get_arrow_tk() { return *g_arrow_tk; }
 name const & get_larrow_tk() { return *g_larrow_tk; }
 name const & get_hiding_tk() { return *g_hiding_tk; }

src/frontends/lean/tokens.h

@@ -63,6 +63,7 @@ name const & get_options_tk();
 name const & get_commands_tk();
 name const & get_instances_tk();
 name const & get_classes_tk();
+name const & get_attributes_tk();
 name const & get_arrow_tk();
 name const & get_larrow_tk();
 name const & get_hiding_tk();

src/frontends/lean/tokens.txt

@@ -56,6 +56,7 @@ options      options
 commands     commands
 instances    instances
 classes      classes
+attributes   attributes
 arrow        ->
 larrow       <-
 hiding       hiding

src/library/attribute_manager.h

@@ -46,6 +46,7 @@ public:
     virtual ~attribute() {}
 
     std::string const & get_name() const { return m_id; }
+    std::string const & get_description() const { return m_descr; }
     std::string const & get_token() const { return m_token; }
 
     virtual attr_data_ptr get(environment const &, name const &) const;

src/vim/syntax/lean.vim

@@ -32,7 +32,7 @@ syn keyword leanKeyword precedence reserve match infix infixl infixr notation po
 syn keyword leanKeyword tactic_infix tactic_infixl tactic_infixr tactic_notation tactic_postfix
 syn keyword leanKeyword tactic_prefix eval check end reveal this suppose using namespace section
 syn keyword leanKeyword fields find_decl attribute local set_option extends include omit classes
-syn keyword leanKeyword instances coercions metaclasses raw migrate replacing calc have show suffices
+syn keyword leanKeyword instances coercions attributes raw migrate replacing calc have show suffices
 syn keyword leanKeyword by in at let forall fun exists if dif then else assume assert take obtain from
 
 syn match leanOp        ":"