From d8572e249d7005a629092e2916cf5051534fb086 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Oct 2014 17:28:26 -0700 Subject: [PATCH] feat(frontends/lean/builtin_cmds): add 'print classes' command --- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/builtin_cmds.cpp | 9 +++++++++ src/frontends/lean/class.cpp | 7 +++++++ src/frontends/lean/class.h | 2 ++ src/frontends/lean/tokens.cpp | 4 ++++ src/frontends/lean/tokens.h | 1 + tests/lean/run/print.lean | 2 ++ 7 files changed, 26 insertions(+), 1 deletion(-) diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 81abade8d..67f4bda3e 100644 --- a/src/emacs/lean-syntax.el +++ b/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 diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index fbfcf70e6..3c903e54d 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/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 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 C; diff --git a/src/frontends/lean/class.cpp b/src/frontends/lean/class.cpp index d10bfdcd8..ccca79f5f 100644 --- a/src/frontends/lean/class.cpp +++ b/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 & classes) { + class_state const & s = class_ext::get_state(env); + s.m_instances.for_each([&](name const & c, list 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); diff --git a/src/frontends/lean/class.h b/src/frontends/lean/class.h index 08f3ac003..ac632bd3a 100644 --- a/src/frontends/lean/class.h +++ b/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 get_class_instances(environment const & env, name const & c); +/** \brief Return the classes in the given environment. */ +void get_classes(environment const & env, buffer & classes); name get_class_name(environment const & env, expr const & e); /** \brief Parse priority for an class instance */ optional parse_instance_priority(parser & p); diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index c2e99c328..0acdeb32d 100644 --- a/src/frontends/lean/tokens.cpp +++ b/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; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 533772030..104c07492 100644 --- a/src/frontends/lean/tokens.h +++ b/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(); diff --git a/tests/lean/run/print.lean b/tests/lean/run/print.lean index 2a2e4c5c9..de0892c7c 100644 --- a/tests/lean/run/print.lean +++ b/tests/lean/run/print.lean @@ -7,3 +7,5 @@ print options print coercions functor print "-----------" print coercions +print "-----------" +print classes