From 0641ee33ce3664c32e40e579755f88824097bf8b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 Oct 2014 20:48:20 -0700 Subject: [PATCH] feat(frontends/lean): allow variables anywhere --- src/frontends/lean/decl_cmds.cpp | 55 ++++++++++++++-------------- src/frontends/lean/inductive_cmd.cpp | 6 +-- src/frontends/lean/local_decls.h | 1 + src/frontends/lean/parser.h | 1 + tests/lean/run/vars_anywhere.lean | 11 ++++++ tests/lean/sec.lean.expected.out | 2 +- tests/lean/var.lean.expected.out | 2 +- 7 files changed, 46 insertions(+), 32 deletions(-) create mode 100644 tests/lean/run/vars_anywhere.lean diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 21faaaf72..c715c8139 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -86,7 +86,7 @@ static void check_parameter_type(parser & p, name const & n, expr const & type, for_each(type, [&](expr const & e, unsigned) { if (is_local(e) && p.is_section_variable(e)) throw parser_error(sstream() << "invalid parameter declaration '" << n << "', it depends on " << - "section variable '" << local_pp_name(e) << "'", pos); + "variable '" << local_pp_name(e) << "'", pos); return true; }); } @@ -96,12 +96,14 @@ static environment declare_var(parser & p, environment env, variable_kind k, optional const & _bi, pos_info const & pos) { binder_info bi; if (_bi) bi = *_bi; - if (in_section_or_context(p.env())) { - lean_assert(k == variable_kind::Parameter || k == variable_kind::Variable); - if (k == variable_kind::Parameter) + if (k == variable_kind::Parameter || k == variable_kind::Variable) { + if (k == variable_kind::Parameter) { + check_in_section_or_context(p); check_parameter_type(p, n, type, pos); + } if (p.get_local(n)) - throw parser_error(sstream() << "invalid declaration, section/context already contains '" << n << "'", pos); + throw parser_error(sstream() << "invalid parameter/variable declaration, '" + << n << "' has already been declared", pos); name u = p.mk_fresh_name(); expr l = p.save_pos(mk_local(u, n, type, bi), pos); p.add_local_expr(n, l, k == variable_kind::Variable); @@ -124,17 +126,15 @@ static environment declare_var(parser & p, environment env, } /** \brief If we are in a section, then add the new local levels to it. */ -static void update_section_local_levels(parser & p, level_param_names const & new_ls, bool is_variable) { - if (in_section_or_context(p.env())) { - for (auto const & l : new_ls) - p.add_local_level(l, mk_param_univ(l), is_variable); - } +static void update_local_levels(parser & p, level_param_names const & new_ls, bool is_variable) { + for (auto const & l : new_ls) + p.add_local_level(l, mk_param_univ(l), is_variable); } -optional parse_binder_info(parser & p) { +optional parse_binder_info(parser & p, variable_kind k) { optional bi = p.parse_optional_binder_info(); - if (bi) - check_in_section_or_context(p); + if (bi && k != variable_kind::Parameter && k != variable_kind::Variable) + parser_error("invalid binder annotation, it can only be used to declare variables/parameters", p.pos()); return bi; } @@ -144,8 +144,8 @@ static void check_variable_kind(parser & p, variable_kind k) { throw parser_error("invalid declaration, 'constant/axiom' cannot be used in sections/contexts", p.pos()); } else { - if (k == variable_kind::Parameter || k == variable_kind::Variable) - throw parser_error("invalid declaration, 'parameter/variable/hypothesis/conjecture' " + if (k == variable_kind::Parameter) + throw parser_error("invalid declaration, 'parameter/hypothesis/conjecture' " "can only be used in sections/contexts", p.pos()); } } @@ -153,13 +153,13 @@ static void check_variable_kind(parser & p, variable_kind k) { environment variable_cmd_core(parser & p, variable_kind k) { check_variable_kind(p, k); auto pos = p.pos(); - optional bi = parse_binder_info(p); + optional bi = parse_binder_info(p, k); name n = p.check_id_next("invalid declaration, identifier expected"); buffer ls_buffer; - if (p.curr_is_token(get_llevel_curly_tk()) && in_section_or_context(p.env())) - throw parser_error("invalid declaration, axioms/parameters occurring in sections cannot be universe polymorphic", p.pos()); + if (p.curr_is_token(get_llevel_curly_tk()) && (k == variable_kind::Parameter || k == variable_kind::Variable)) + throw parser_error("invalid declaration, only constants/axioms can be universe polymorphic", p.pos()); optional scope1; - if (!in_section_or_context(p.env())) + if (k == variable_kind::Constant || k == variable_kind::Axiom) scope1.emplace(p); parse_univ_params(p, ls_buffer); expr type; @@ -175,7 +175,7 @@ environment variable_cmd_core(parser & p, variable_kind k) { } p.parse_close_binder_info(bi); level_param_names ls; - if (in_section_or_context(p.env())) { + if (ls_buffer.empty()) { ls = to_level_param_names(collect_univ_params(type)); } else { update_univ_parameters(ls_buffer, collect_univ_params(type), p); @@ -184,7 +184,8 @@ environment variable_cmd_core(parser & p, variable_kind k) { level_param_names new_ls; list ctx = p.locals_to_context(); std::tie(type, new_ls) = p.elaborate_type(type, ctx); - update_section_local_levels(p, new_ls, k == variable_kind::Variable); + if (k == variable_kind::Variable || k == variable_kind::Parameter) + update_local_levels(p, new_ls, k == variable_kind::Variable); return declare_var(p, p.env(), n, append(ls, new_ls), type, k, bi, pos); } environment variable_cmd(parser & p) { @@ -205,7 +206,7 @@ static environment variables_cmd_core(parser & p, variable_kind k) { auto pos = p.pos(); environment env = p.env(); while (true) { - optional bi = parse_binder_info(p); + optional bi = parse_binder_info(p, k); buffer ids; while (!p.curr_is_token(get_colon_tk())) { name id = p.check_id_next("invalid parameters declaration, identifier expected"); @@ -213,7 +214,7 @@ static environment variables_cmd_core(parser & p, variable_kind k) { } p.next(); optional scope1; - if (!in_section_or_context(p.env())) + if (k == variable_kind::Constant || k == variable_kind::Axiom) scope1.emplace(p); expr type = p.parse_expr(); p.parse_close_binder_info(bi); @@ -225,7 +226,8 @@ static environment variables_cmd_core(parser & p, variable_kind k) { level_param_names new_ls; expr new_type; std::tie(new_type, new_ls) = p.elaborate_type(type, ctx); - update_section_local_levels(p, new_ls, k == variable_kind::Variable); + if (k == variable_kind::Variable || k == variable_kind::Parameter) + update_local_levels(p, new_ls, k == variable_kind::Variable); new_ls = append(ls, new_ls); env = declare_var(p, env, id, new_ls, new_type, k, bi, pos); } @@ -245,7 +247,6 @@ static environment constants_cmd(parser & p) { return variables_cmd_core(p, variable_kind::Constant); } - struct decl_modifiers { bool m_is_instance; bool m_is_coercion; @@ -365,7 +366,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, boo real_n = ns + n; } - if (in_section_or_context(env)) { + if (p.has_locals()) { buffer section_ps; collect_section_locals(type, value, p, section_ps); type = Pi_as_is(section_ps, type, p); @@ -515,7 +516,7 @@ environment include_cmd_core(parser & p, bool include) { name n = p.get_name_val(); p.next(); if (!p.get_local(n)) - throw parser_error(sstream() << "invalid include/omit command, '" << n << "' is not a section parameter/variable", pos); + throw parser_error(sstream() << "invalid include/omit command, '" << n << "' is not a parameter/variable", pos); if (include) { if (p.is_include_variable(n)) throw parser_error(sstream() << "invalid include command, '" << n << "' has already been included", pos); diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index e056be54d..753b381a5 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -387,7 +387,7 @@ struct inductive_cmd_fn { /** \brief Include in m_levels any section level referenced by decls. */ void include_section_levels(buffer const & decls) { - if (!in_section_or_context(m_env)) + if (!m_p.has_locals()) return; name_set all_lvl_params; for (auto const & d : decls) { @@ -448,7 +448,7 @@ struct inductive_cmd_fn { The section parameters are stored in section_params */ void abstract_section_locals(buffer & decls, buffer & section_params) { - if (!in_section_or_context(m_env)) + if (!m_p.has_locals()) return; expr_struct_set section_locals; collect_section_locals(decls, section_locals); @@ -593,7 +593,7 @@ struct inductive_cmd_fn { id = name(name(full_id.get_prefix().get_string()), full_id.get_string()); else id = name(full_id.get_string()); - if (in_section_or_context(env)) { + if (!empty(section_levels) || !section_params.empty()) { expr r = mk_section_local_ref(full_id, section_levels, section_params); m_p.add_local_expr(id, r); } diff --git a/src/frontends/lean/local_decls.h b/src/frontends/lean/local_decls.h index 407370c2a..a996469b4 100644 --- a/src/frontends/lean/local_decls.h +++ b/src/frontends/lean/local_decls.h @@ -46,6 +46,7 @@ public: std::tie(m_map, m_counter, m_entries) = head(m_scopes); m_scopes = tail(m_scopes); } + bool empty() const { return m_map.empty(); } struct mk_scope { local_decls & m_d; mk_scope(local_decls & d):m_d(d) { m_d.push(); } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 5ea6ee6fb..0284d6670 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -331,6 +331,7 @@ public: expr parse_scoped_expr(buffer & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); } struct local_scope { parser & m_p; environment m_env; local_scope(parser & p); ~local_scope(); }; + bool has_locals() const { return !m_local_decls.empty() || !m_local_level_decls.empty(); } 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); } diff --git a/tests/lean/run/vars_anywhere.lean b/tests/lean/run/vars_anywhere.lean new file mode 100644 index 000000000..fd48344ae --- /dev/null +++ b/tests/lean/run/vars_anywhere.lean @@ -0,0 +1,11 @@ +variable {A : Type} + +definition id (a : A) := a + +check @id + +inductive list := +nil : list, +cons : A → list → list + +check @list.cons diff --git a/tests/lean/sec.lean.expected.out b/tests/lean/sec.lean.expected.out index 5c89956cc..e49d1af06 100644 --- a/tests/lean/sec.lean.expected.out +++ b/tests/lean/sec.lean.expected.out @@ -1 +1 @@ -sec.lean:7:11: error: invalid declaration, section/context already contains 'A' +sec.lean:7:11: error: invalid parameter/variable declaration, 'A' has already been declared diff --git a/tests/lean/var.lean.expected.out b/tests/lean/var.lean.expected.out index 6dc85136c..bca60353a 100644 --- a/tests/lean/var.lean.expected.out +++ b/tests/lean/var.lean.expected.out @@ -1 +1 @@ -var.lean:6:12: error: invalid parameter declaration 'a', it depends on section variable 'A' +var.lean:6:12: error: invalid parameter declaration 'a', it depends on variable 'A'