From b27ba6288d995a25dd59eec5de146e60007123bd Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 10 Aug 2016 13:00:54 -0400 Subject: [PATCH] feat(frontends/lean/print_cmd): implement 'print attributes' --- extras/latex/lstlean.tex | 2 +- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/print_cmd.cpp | 11 ++++++++++- src/frontends/lean/tokens.cpp | 4 ++++ src/frontends/lean/tokens.h | 1 + src/frontends/lean/tokens.txt | 1 + src/library/attribute_manager.h | 1 + src/vim/syntax/lean.vim | 2 +- 8 files changed, 20 insertions(+), 4 deletions(-) diff --git a/extras/latex/lstlean.tex b/extras/latex/lstlean.tex index d28462d636..ca24aefcea 100644 --- a/extras/latex/lstlean.tex +++ b/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 diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 8add00261b..398603b385 100644 --- a/src/emacs/lean-syntax.el +++ b/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") diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp index b8d6bcf080..b2e5c0d87c 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/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 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 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); diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 95ab0850ec..e9fed914cb 100644 --- a/src/frontends/lean/tokens.cpp +++ b/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; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index a1fc2bdf8d..55dc619676 100644 --- a/src/frontends/lean/tokens.h +++ b/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(); diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt index d008a194e1..33250b6daa 100644 --- a/src/frontends/lean/tokens.txt +++ b/src/frontends/lean/tokens.txt @@ -56,6 +56,7 @@ options options commands commands instances instances classes classes +attributes attributes arrow -> larrow <- hiding hiding diff --git a/src/library/attribute_manager.h b/src/library/attribute_manager.h index 83f4d6a835..944ebd8358 100644 --- a/src/library/attribute_manager.h +++ b/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; diff --git a/src/vim/syntax/lean.vim b/src/vim/syntax/lean.vim index ec1ff6ce2a..19673143b4 100644 --- a/src/vim/syntax/lean.vim +++ b/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 ":"