From 6c442b250cda62806ac2ed37c924ed3f1107ebab Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 14 Jul 2014 03:47:49 +0100 Subject: [PATCH] refactor(frontends/lean): minor code reorg Signed-off-by: Leonardo de Moura --- src/frontends/lean/decl_cmds.cpp | 28 ---------------------------- src/frontends/lean/decl_cmds.h | 9 --------- src/frontends/lean/util.cpp | 29 +++++++++++++++++++++++++++++ src/frontends/lean/util.h | 8 ++++++++ 4 files changed, 37 insertions(+), 37 deletions(-) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index af13c7478..e6c5a06e9 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -149,22 +149,6 @@ environment axiom_cmd(parser & p) { return variable_cmd_core(p, true); } -// Sort local_names by order of occurrence in the section, and copy the associated parameters to section_ps -void mk_section_params(name_set const & local_names, parser const & p, buffer & section_ps) { - local_names.for_each([&](name const & n) { - section_ps.push_back(*p.get_local(n)); - }); - std::sort(section_ps.begin(), section_ps.end(), [&](expr const & p1, expr const & p2) { - return p.get_local_index(mlocal_name(p1)) < p.get_local_index(mlocal_name(p2)); - }); -} - -// Collect local (section) constants occurring in type and value, sort them, and store in section_ps -void collect_section_locals(expr const & type, expr const & value, parser const & p, buffer & section_ps) { - name_set ls = collect_locals(type, collect_locals(value)); - return mk_section_params(ls, p, section_ps); -} - struct decl_modifiers { bool m_is_private; bool m_is_opaque; @@ -198,18 +182,6 @@ struct decl_modifiers { } }; -// Return the levels in \c ls that are defined in the section -levels collect_section_levels(level_param_names const & ls, parser & p) { - buffer section_ls_buffer; - for (name const & l : ls) { - if (p.get_local_level_index(l)) - section_ls_buffer.push_back(mk_param_univ(l)); - else - break; - } - return to_list(section_ls_buffer.begin(), section_ls_buffer.end()); -} - environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) { name n = p.check_id_next("invalid declaration, identifier expected"); check_atomic(n); diff --git a/src/frontends/lean/decl_cmds.h b/src/frontends/lean/decl_cmds.h index c34eb9ffc..827e89017 100644 --- a/src/frontends/lean/decl_cmds.h +++ b/src/frontends/lean/decl_cmds.h @@ -21,14 +21,5 @@ bool parse_univ_params(parser & p, buffer & ps); Then sort \c ls_buffer (using the order in which the universe levels were declared). */ void update_univ_parameters(buffer & ls_buffer, name_set const & found_ls, parser const & p); -/** - \brief Copy the parameters associated with the local names in \c local_names to \c section_ps. - Then sort \c section_ps (using the order in which they were declared). -*/ -void mk_section_params(name_set const & local_names, parser const & p, buffer & section_ps); -/** - \brief Return the levels in \c ls that are defined in the section. -*/ -levels collect_section_levels(level_param_names const & ls, parser & p); void register_decl_cmds(cmd_table & r); } diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 29b212dfb..1dc82f3ce 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "util/sstream.h" #include "library/scoped_ext.h" +#include "library/locals.h" #include "frontends/lean/parser.h" namespace lean { @@ -25,4 +26,32 @@ bool is_root_namespace(name const & n) { name remove_root_prefix(name const & n) { return n.replace_prefix(g_root, name()); } + +// Sort local_names by order of occurrence in the section, and copy the associated parameters to section_ps +void mk_section_params(name_set const & local_names, parser const & p, buffer & section_ps) { + local_names.for_each([&](name const & n) { + section_ps.push_back(*p.get_local(n)); + }); + std::sort(section_ps.begin(), section_ps.end(), [&](expr const & p1, expr const & p2) { + return p.get_local_index(mlocal_name(p1)) < p.get_local_index(mlocal_name(p2)); + }); +} + +// Return the levels in \c ls that are defined in the section +levels collect_section_levels(level_param_names const & ls, parser & p) { + buffer section_ls_buffer; + for (name const & l : ls) { + if (p.get_local_level_index(l)) + section_ls_buffer.push_back(mk_param_univ(l)); + else + break; + } + return to_list(section_ls_buffer.begin(), section_ls_buffer.end()); +} + +// Collect local (section) constants occurring in type and value, sort them, and store in section_ps +void collect_section_locals(expr const & type, expr const & value, parser const & p, buffer & section_ps) { + name_set ls = collect_locals(type, collect_locals(value)); + return mk_section_params(ls, p, section_ps); +} } diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index 440f00d23..df98f21d6 100644 --- a/src/frontends/lean/util.h +++ b/src/frontends/lean/util.h @@ -12,4 +12,12 @@ void check_atomic(name const & n); void check_in_section(parser const & p); bool is_root_namespace(name const & n); name remove_root_prefix(name const & n); +/** \brief Copy the parameters associated with the local names in \c local_names to \c section_ps. + Then sort \c section_ps (using the order in which they were declared). +*/ +void mk_section_params(name_set const & local_names, parser const & p, buffer & section_ps); +/** \brief Return the levels in \c ls that are defined in the section. */ +levels collect_section_levels(level_param_names const & ls, parser & p); +/** \brief Collect local (section) constants occurring in type and value, sort them, and store in section_ps */ +void collect_section_locals(expr const & type, expr const & value, parser const & p, buffer & section_ps); }