michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(frontends/lean): rename parser methods is_section* to is_local*

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-11 10:25:02 -07:00
parent b0f8d86f26
commit 1cc8007b9a
3 changed files with 12 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/decl_cmds.cpp
View file

@ -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) { static void check_parameter_type(parser & p, name const & n, expr const & type, pos_info const & pos) {
for_each(type, [&](expr const & e, unsigned) { 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 " << throw parser_error(sstream() << "invalid parameter declaration '" << n << "', it depends on " <<
"variable '" << local_pp_name(e) << "'", pos); "variable '" << local_pp_name(e) << "'", pos);
return true; return true;

10
src/frontends/lean/parser.h
View file

@ -61,8 +61,8 @@ struct snapshot {
environment m_env; environment m_env;
local_level_decls m_lds; local_level_decls m_lds;
local_expr_decls m_eds; local_expr_decls m_eds;
name_set m_lvars; // subset of m_lds that is tagged as section level 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 section 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 name_set m_include_vars; // subset of m_eds that must be included
options m_options; options m_options;
parser_scope_stack m_parser_scope_stack; 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_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(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); } 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_local_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_local_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_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 include_variable(name const & n) { m_include_vars.insert(n); }
void omit_variable(name const & n) { m_include_vars.erase(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); } bool is_include_variable(name const & n) const { return m_include_vars.contains(n); }

12
src/frontends/lean/util.cpp
View file

@ -49,11 +49,11 @@ void sort_section_params(expr_struct_set const & locals, parser const & p, buffe
for (expr const & l : locals) for (expr const & l : locals)
section_ps.push_back(l); section_ps.push_back(l);
std::sort(section_ps.begin(), section_ps.end(), [&](expr const & p1, expr const & p2) { 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_var1 = p.is_local_variable(p1);
bool is_sec_var2 = p.is_section_variable(p2); bool is_var2 = p.is_local_variable(p2);
if (!is_sec_var1 && is_sec_var2) if (!is_var1 && is_var2)
return true; return true;
else if (is_sec_var1 && !is_sec_var2) else if (is_var1 && !is_var2)
return false; return false;
else else
return p.get_local_index(p1) < p.get_local_index(p2); 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) { levels collect_section_nonvar_levels(parser & p, level_param_names const & ls) {
buffer<level> section_ls_buffer; buffer<level> section_ls_buffer;
for (name const & l : ls) { 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)); section_ls_buffer.push_back(mk_param_univ(l));
else else
break; break;
@ -90,7 +90,7 @@ void remove_section_variables(parser const & p, buffer<expr> & ps) {
unsigned j = 0; unsigned j = 0;
for (unsigned i = 0; i < ps.size(); i++) { for (unsigned i = 0; i < ps.size(); i++) {
expr const & param = ps[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; ps[j] = param;
j++; j++;
} }