From 1cc8007b9a4da714abe3450e796eb47ff2d191e0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 11 Oct 2014 10:25:02 -0700 Subject: [PATCH] refactor(frontends/lean): rename parser methods is_section* to is_local* --- src/frontends/lean/decl_cmds.cpp | 2 +- src/frontends/lean/parser.h | 10 +++++----- src/frontends/lean/util.cpp | 12 ++++++------ 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index d22e77132..e3198da26 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -84,7 +84,7 @@ enum class variable_kind { Constant, Parameter, Variable, Axiom }; static void check_parameter_type(parser & p, name const & n, expr const & type, pos_info const & pos) { for_each(type, [&](expr const & e, unsigned) { - if (is_local(e) && p.is_section_variable(e)) + if (is_local(e) && p.is_local_variable(e)) throw parser_error(sstream() << "invalid parameter declaration '" << n << "', it depends on " << "variable '" << local_pp_name(e) << "'", pos); return true; diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index dfc4bca8a..e960e8d83 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -61,8 +61,8 @@ struct snapshot { environment m_env; local_level_decls m_lds; local_expr_decls m_eds; - name_set m_lvars; // subset of m_lds that is tagged as section level variable - name_set m_vars; // subset of m_eds that is tagged as section variable + name_set m_lvars; // subset of m_lds that is tagged as level variable + name_set m_vars; // subset of m_eds that is tagged as variable name_set m_include_vars; // subset of m_eds that must be included options m_options; parser_scope_stack m_parser_scope_stack; @@ -343,9 +343,9 @@ public: void add_local_level(name const & n, level const & l, bool is_variable = false); void add_local_expr(name const & n, expr const & p, bool is_variable = false); void add_local(expr const & p) { return add_local_expr(local_pp_name(p), p); } - bool is_section_level_variable(name const & n) const { return m_level_variables.contains(n); } - bool is_section_variable(name const & n) const { return m_variables.contains(n); } - bool is_section_variable(expr const & e) const { return is_section_variable(local_pp_name(e)); } + bool is_local_level_variable(name const & n) const { return m_level_variables.contains(n); } + bool is_local_variable(name const & n) const { return m_variables.contains(n); } + bool is_local_variable(expr const & e) const { return is_local_variable(local_pp_name(e)); } void include_variable(name const & n) { m_include_vars.insert(n); } void omit_variable(name const & n) { m_include_vars.erase(n); } bool is_include_variable(name const & n) const { return m_include_vars.contains(n); } diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 87798e058..a97263c13 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -49,11 +49,11 @@ void sort_section_params(expr_struct_set const & locals, parser const & p, buffe for (expr const & l : locals) section_ps.push_back(l); std::sort(section_ps.begin(), section_ps.end(), [&](expr const & p1, expr const & p2) { - bool is_sec_var1 = p.is_section_variable(p1); - bool is_sec_var2 = p.is_section_variable(p2); - if (!is_sec_var1 && is_sec_var2) + bool is_var1 = p.is_local_variable(p1); + bool is_var2 = p.is_local_variable(p2); + if (!is_var1 && is_var2) return true; - else if (is_sec_var1 && !is_sec_var2) + else if (is_var1 && !is_var2) return false; else return p.get_local_index(p1) < p.get_local_index(p2); @@ -64,7 +64,7 @@ void sort_section_params(expr_struct_set const & locals, parser const & p, buffe levels collect_section_nonvar_levels(parser & p, level_param_names const & ls) { buffer section_ls_buffer; for (name const & l : ls) { - if (p.get_local_level_index(l) && !p.is_section_level_variable(l)) + if (p.get_local_level_index(l) && !p.is_local_level_variable(l)) section_ls_buffer.push_back(mk_param_univ(l)); else break; @@ -90,7 +90,7 @@ void remove_section_variables(parser const & p, buffer & ps) { unsigned j = 0; for (unsigned i = 0; i < ps.size(); i++) { expr const & param = ps[i]; - if (!is_local(param) || !p.is_section_variable(param)) { + if (!is_local(param) || !p.is_local_variable(param)) { ps[j] = param; j++; }