From 33ad41b93efad7546378f663df187efcf23601ef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 11 Oct 2014 15:33:31 -0700 Subject: [PATCH] refactor(frontends/lean): adjust function names to reflect how parameters/variables behave --- src/frontends/lean/builtin_cmds.cpp | 4 +- src/frontends/lean/decl_cmds.cpp | 26 ++++----- src/frontends/lean/inductive_cmd.cpp | 84 ++++++++++++++-------------- src/frontends/lean/structure_cmd.cpp | 2 +- src/frontends/lean/util.cpp | 40 ++++++------- src/frontends/lean/util.h | 34 +++++------ 6 files changed, 95 insertions(+), 95 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 16776f4c89..517f778921 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -128,7 +128,7 @@ static void redeclare_aliases(parser & p, name_set popped_locals; while (!is_eqp(old_entries, new_entries)) { pair entry = head(old_entries); - if (is_section_local_ref(entry.second)) + if (is_local_ref(entry.second)) to_redeclare.push_back(entry); else if (is_local(entry.second)) popped_locals.insert(mlocal_name(entry.second)); @@ -144,7 +144,7 @@ static void redeclare_aliases(parser & p, } for (auto const & entry : to_redeclare) { - expr new_ref = update_section_local_ref(entry.second, popped_levels, popped_locals); + expr new_ref = update_local_ref(entry.second, popped_levels, popped_locals); if (!is_constant(new_ref)) p.add_local_expr(entry.first, new_ref); } diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 25760be47e..e16f9a7c31 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -388,22 +388,22 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, boo } if (p.has_locals()) { - buffer section_ps; - collect_section_locals(type, value, p, section_ps); - type = Pi_as_is(section_ps, type, p); - buffer section_value_ps; - section_value_ps.append(section_ps); - erase_local_binder_info(section_value_ps); - value = Fun_as_is(section_value_ps, value, p); + buffer locals; + collect_locals(type, value, p, locals); + type = Pi_as_is(locals, type, p); + buffer new_locals; + new_locals.append(locals); + erase_local_binder_info(new_locals); + value = Fun_as_is(new_locals, value, p); update_univ_parameters(ls_buffer, collect_univ_params(value, collect_univ_params(type)), p); ls = to_list(ls_buffer.begin(), ls_buffer.end()); - levels section_ls = collect_local_nonvar_levels(p, ls); - remove_section_variables(p, section_ps); - if (!section_ps.empty()) { - expr ref = mk_section_local_ref(real_n, section_ls, section_ps); + levels local_ls = collect_local_nonvar_levels(p, ls); + remove_local_vars(p, locals); + if (!locals.empty()) { + expr ref = mk_local_ref(real_n, local_ls, locals); p.add_local_expr(n, ref); - } else if (section_ls) { - expr ref = mk_constant(real_n, section_ls); + } else if (local_ls) { + expr ref = mk_constant(real_n, local_ls); p.add_local_expr(n, ref); } } else { diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index 5879d91f3f..1c26f50f8c 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -385,8 +385,8 @@ struct inductive_cmd_fn { } } - /** \brief Include in m_levels any section level referenced by decls. */ - void include_section_levels(buffer const & decls) { + /** \brief Include in m_levels any local level referenced by decls. */ + void include_local_levels(buffer const & decls) { if (!m_p.has_locals()) return; name_set all_lvl_params; @@ -396,41 +396,41 @@ struct inductive_cmd_fn { all_lvl_params = collect_univ_params(intro_rule_type(ir), all_lvl_params); } } - buffer section_lvls; + buffer local_lvls; all_lvl_params.for_each([&](name const & l) { if (std::find(m_levels.begin(), m_levels.end(), l) == m_levels.end()) - section_lvls.push_back(l); + local_lvls.push_back(l); }); - std::sort(section_lvls.begin(), section_lvls.end(), [&](name const & n1, name const & n2) { + std::sort(local_lvls.begin(), local_lvls.end(), [&](name const & n1, name const & n2) { return m_p.get_local_level_index(n1) < m_p.get_local_level_index(n2); }); buffer new_levels; - new_levels.append(section_lvls); + new_levels.append(local_lvls); new_levels.append(m_levels); m_levels.clear(); m_levels.append(new_levels); } - /** \brief Collect section local parameters used in the inductive decls */ - void collect_section_locals(buffer const & decls, expr_struct_set & ls) { + /** \brief Collect local constants used in the inductive decls */ + void collect_locals(buffer const & decls, expr_struct_set & ls) { buffer include_vars; m_p.get_include_variables(include_vars); for (expr const & param : include_vars) { - collect_locals(mlocal_type(param), ls); + ::lean::collect_locals(mlocal_type(param), ls); ls.insert(param); } for (auto const & d : decls) { - collect_locals(inductive_decl_type(d), ls); + ::lean::collect_locals(inductive_decl_type(d), ls); for (auto const & ir : inductive_decl_intros(d)) - collect_locals(intro_rule_type(ir), ls); + ::lean::collect_locals(intro_rule_type(ir), ls); } } /** \brief Make sure that every occurrence of an inductive datatype (in decls) in \c type has - section parameters \c section_params as arguments. + locals as arguments. */ - expr fix_inductive_occs(expr const & type, buffer const & decls, buffer const & section_params) { - if (section_params.empty()) + expr fix_inductive_occs(expr const & type, buffer const & decls, buffer const & locals) { + if (locals.empty()) return type; return replace(type, [&](expr const & e) { if (!is_constant(e)) @@ -439,34 +439,34 @@ struct inductive_cmd_fn { [&](inductive_decl const & d) { return const_name(e) == inductive_decl_name(d); })) return none_expr(); // found target - expr r = mk_as_atomic(mk_app(mk_explicit(e), section_params)); + expr r = mk_as_atomic(mk_app(mk_explicit(e), locals)); return some_expr(r); }); } - /** \brief Include the used section parameters as additional arguments. - The section parameters are stored in section_params + /** \brief Include the used locals as additional arguments. + The locals are stored in \c locals */ - void abstract_section_locals(buffer & decls, buffer & section_params) { + void abstract_locals(buffer & decls, buffer & locals) { if (!m_p.has_locals()) return; - expr_struct_set section_locals; - collect_section_locals(decls, section_locals); - if (section_locals.empty()) + expr_struct_set local_set; + collect_locals(decls, local_set); + if (local_set.empty()) return; - sort_section_params(section_locals, m_p, section_params); - // First, add section_params to inductive types type. + sort_locals(local_set, m_p, locals); + // First, add locals to inductive types type. for (inductive_decl & d : decls) { - d = update_inductive_decl(d, Pi(section_params, inductive_decl_type(d), m_p)); + d = update_inductive_decl(d, Pi(locals, inductive_decl_type(d), m_p)); } - // Add section_params to introduction rules type, and also "fix" + // Add locals to introduction rules type, and also "fix" // occurrences of inductive types. for (inductive_decl & d : decls) { buffer new_irs; for (auto const & ir : inductive_decl_intros(d)) { expr type = intro_rule_type(ir); - type = fix_inductive_occs(type, decls, section_params); - type = Pi_as_is(section_params, type, m_p); + type = fix_inductive_occs(type, decls, locals); + type = Pi_as_is(locals, type, m_p); new_irs.push_back(update_intro_rule(ir, type)); } d = update_inductive_decl(d, new_irs); @@ -587,14 +587,14 @@ struct inductive_cmd_fn { /** \brief Create an alias for the fully qualified name \c full_id. */ environment create_alias(environment env, bool composite, name const & full_id, - levels const & section_levels, buffer const & section_params) { + levels const & ctx_levels, buffer const & ctx_params) { name id; if (composite) id = name(name(full_id.get_prefix().get_string()), full_id.get_string()); else id = name(full_id.get_string()); - if (!empty(section_levels) || !section_params.empty()) { - expr r = mk_section_local_ref(full_id, section_levels, section_params); + if (!empty(ctx_levels) || !ctx_params.empty()) { + expr r = mk_local_ref(full_id, ctx_levels, ctx_params); m_p.add_local_expr(id, r); } if (full_id != id) @@ -603,22 +603,22 @@ struct inductive_cmd_fn { } /** \brief Add aliases for the inductive datatype, introduction and elimination rules */ - environment add_aliases(environment env, level_param_names const & ls, buffer const & section_params, + environment add_aliases(environment env, level_param_names const & ls, buffer const & locals, buffer const & decls) { - buffer section_params_only(section_params); - remove_section_variables(m_p, section_params_only); + buffer params_only(locals); + remove_local_vars(m_p, params_only); // Create aliases/local refs - levels section_levels = collect_local_nonvar_levels(m_p, ls); + levels ctx_levels = collect_local_nonvar_levels(m_p, ls); for (auto & d : decls) { name d_name = inductive_decl_name(d); name d_short_name(d_name.get_string()); - env = create_alias(env, false, d_name, section_levels, section_params_only); + env = create_alias(env, false, d_name, ctx_levels, params_only); name rec_name = mk_rec_name(d_name); - env = create_alias(env, true, rec_name, section_levels, section_params_only); + env = create_alias(env, true, rec_name, ctx_levels, params_only); env = add_protected(env, rec_name); for (intro_rule const & ir : inductive_decl_intros(d)) { name ir_name = intro_rule_name(ir); - env = create_alias(env, true, ir_name, section_levels, section_params_only); + env = create_alias(env, true, ir_name, ctx_levels, params_only); } } return env; @@ -668,10 +668,10 @@ struct inductive_cmd_fn { parser::local_scope scope(m_p); parse_inductive_decls(decls); } - buffer section_params; - abstract_section_locals(decls, section_params); - include_section_levels(decls); - m_num_params += section_params.size(); + buffer locals; + abstract_locals(decls, locals); + include_local_levels(decls); + m_num_params += locals.size(); declare_inductive_types(decls); unsigned num_univ_params = m_levels.size(); buffer r_lvls; @@ -684,7 +684,7 @@ struct inductive_cmd_fn { level_param_names ls = to_list(m_levels.begin(), m_levels.end()); environment env = module::add_inductive(m_p.env(), ls, m_num_params, to_list(decls.begin(), decls.end())); update_declaration_index(env); - env = add_aliases(env, ls, section_params, decls); + env = add_aliases(env, ls, locals, decls); return apply_modifiers(env); } }; diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 5ed200578e..32ee2f58c9 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -154,7 +154,7 @@ struct structure_cmd_fn { collect_section_locals(section_locals); if (section_locals.empty()) return; - sort_section_params(section_locals, m_p, section_params); + sort_locals(section_locals, m_p, section_params); m_type = Pi_as_is(section_params, m_type, m_p); } diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 31efd87ae3..63cb957ddc 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -44,11 +44,11 @@ name remove_root_prefix(name const & n) { return n.replace_prefix(get_root_tk(), name()); } -// Sort local_names by order of occurrence in the section, and copy the associated parameters to section_ps -void sort_section_params(expr_struct_set const & locals, parser const & p, buffer & section_ps) { +// Sort local names by order of occurrence, and copy the associated parameters to ps +void sort_locals(expr_struct_set const & locals, parser const & p, buffer & ps) { for (expr const & l : locals) - section_ps.push_back(l); - std::sort(section_ps.begin(), section_ps.end(), [&](expr const & p1, expr const & p2) { + ps.push_back(l); + std::sort(ps.begin(), ps.end(), [&](expr const & p1, expr const & p2) { bool is_var1 = p.is_local_variable(p1); bool is_var2 = p.is_local_variable(p2); if (!is_var1 && is_var2) @@ -72,8 +72,8 @@ levels collect_local_nonvar_levels(parser & p, level_param_names const & ls) { 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) { +// Collect local constants occurring in type and value, sort them, and store in ctx_ps +void collect_locals(expr const & type, expr const & value, parser const & p, buffer & ctx_ps) { expr_struct_set ls; buffer include_vars; p.get_include_variables(include_vars); @@ -83,38 +83,38 @@ void collect_section_locals(expr const & type, expr const & value, parser const } collect_locals(type, ls); collect_locals(value, ls); - sort_section_params(ls, p, section_ps); + sort_locals(ls, p, ctx_ps); } -void remove_section_variables(parser const & p, buffer & ps) { +void remove_local_vars(parser const & p, buffer & locals) { unsigned j = 0; - for (unsigned i = 0; i < ps.size(); i++) { - expr const & param = ps[i]; + for (unsigned i = 0; i < locals.size(); i++) { + expr const & param = locals[i]; if (!is_local(param) || !p.is_local_variable(param)) { - ps[j] = param; + locals[j] = param; j++; } } - ps.shrink(j); + locals.shrink(j); } list locals_to_context(expr const & e, parser const & p) { expr_struct_set ls; collect_locals(e, ls); buffer locals; - sort_section_params(ls, p, locals); + sort_locals(ls, p, locals); std::reverse(locals.begin(), locals.end()); return to_list(locals.begin(), locals.end()); } -expr mk_section_local_ref(name const & n, levels const & sec_ls, unsigned num_sec_params, expr const * sec_params) { +expr mk_local_ref(name const & n, levels const & ctx_ls, unsigned num_ctx_params, expr const * ctx_params) { buffer params; - for (unsigned i = 0; i < num_sec_params; i++) - params.push_back(mk_explicit(sec_params[i])); - return mk_as_atomic(mk_app(mk_explicit(mk_constant(n, sec_ls)), params)); + for (unsigned i = 0; i < num_ctx_params; i++) + params.push_back(mk_explicit(ctx_params[i])); + return mk_as_atomic(mk_app(mk_explicit(mk_constant(n, ctx_ls)), params)); } -bool is_section_local_ref(expr const & e) { +bool is_local_ref(expr const & e) { if (!is_as_atomic(e)) return false; expr const & imp_arg = get_as_atomic_arg(e); @@ -131,8 +131,8 @@ bool is_section_local_ref(expr const & e) { }); } -expr update_section_local_ref(expr const & e, name_set const & lvls_to_remove, name_set const & locals_to_remove) { - lean_assert(is_section_local_ref(e)); +expr update_local_ref(expr const & e, name_set const & lvls_to_remove, name_set const & locals_to_remove) { + lean_assert(is_local_ref(e)); if (locals_to_remove.empty() && lvls_to_remove.empty()) return e; buffer locals; diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index 9269b3a235..0fdbd9cc0e 100644 --- a/src/frontends/lean/util.h +++ b/src/frontends/lean/util.h @@ -26,36 +26,36 @@ name remove_root_prefix(name const & n); A local level is tagged as variable if it associated with a variable. */ levels collect_local_nonvar_levels(parser & p, level_param_names const & ls); -/** \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); -/** \brief Copy the local parameters to \c section_ps, then sort \c section_ps (using the order in which they were declared). */ -void sort_section_params(expr_struct_set const & locals, parser const & p, buffer & section_ps); -/** \brief Remove from \c ps local constants that are tagged as section variables. */ -void remove_section_variables(parser const & p, buffer & ps); +/** \brief Collect local constants occurring in \c type and \c value, sort them, and store in ctx_ps */ +void collect_locals(expr const & type, expr const & value, parser const & p, buffer & ctx_ps); +/** \brief Copy the local names to \c ps, then sort \c ps (using the order in which they were declared). */ +void sort_locals(expr_struct_set const & locals, parser const & p, buffer & ps); +/** \brief Remove from \c ps local constants that are tagged as variables. */ +void remove_local_vars(parser const & p, buffer & ps); list locals_to_context(expr const & e, parser const & p); -/** \brief Create the term (@^-1 (@n.{sec_ls} @sec_params[0] ... @sec_params[num_sec_params-1])) - When we declare \c n inside of a section, the section parameters and universes are fixes. +/** \brief Create the term (as_atomic (@n.{ls} @params[0] ... @params[num_params-1])) + When we declare \c n inside of a context, the parameters and universes are fixed. That is, when the user writes \c n inside the section she is really getting the term returned by this function. */ -expr mk_section_local_ref(name const & n, levels const & sec_ls, unsigned num_sec_params, expr const * sec_params); -inline expr mk_section_local_ref(name const & n, levels const & sec_ls, buffer const & sec_params) { - return mk_section_local_ref(n, sec_ls, sec_params.size(), sec_params.data()); +expr mk_local_ref(name const & n, levels const & ctx_ls, unsigned num_ctx_params, expr const * ctx_params); +inline expr mk_local_ref(name const & n, levels const & ctx_ls, buffer const & ctx_params) { + return mk_local_ref(n, ctx_ls, ctx_params.size(), ctx_params.data()); } /** \brief Return true iff \c e is a term of the form - (@^-1 (@n.{ls} @l_1 ... @l_n)) where + (as_atomic (@n.{ls} @l_1 ... @l_n)) where \c n is a constant and l_i's are local constants. - \remark is_section_local_ref(mk_section_local_ref(n, ls, num_ps, ps)) always hold. + \remark is_local_ref(mk_local_ref(n, ls, num_ps, ps)) always hold. */ -bool is_section_local_ref(expr const & e); -/** \brief Given a term \c e s.t. is_section_local_ref(e) is true, remove all local constants in \c to_remove. +bool is_local_ref(expr const & e); +/** \brief Given a term \c e s.t. is_local_ref(e) is true, remove all local constants in \c to_remove. That is, if \c e is of the form - (@^-1 (@n.{u_1 ... u_k} @l_1 ... @l_n)) + (as_atomic (@n.{u_1 ... u_k} @l_1 ... @l_n)) Then, return a term s.t. 1) any l_i s.t. mlocal_name(l_i) in \c locals_to_remove is removed. 2) any level u_j in \c lvls_to_remove is removed */ -expr update_section_local_ref(expr const & e, name_set const & lvls_to_remove, name_set const & locals_to_remove); +expr update_local_ref(expr const & e, name_set const & lvls_to_remove, name_set const & locals_to_remove); /** \brief Fun(locals, e), but also propagate \c e position to result */ expr Fun(buffer const & locals, expr const & e, parser & p);