From 0a13e7863ae3a99b76edcad1e5cd5e29f39d0d17 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Oct 2014 17:29:22 -0700 Subject: [PATCH] feat(frontends/lean): enforce rule section parameters cannot depend on section variables --- src/frontends/lean/decl_cmds.cpp | 16 +++++++++++++++- src/frontends/lean/parser.cpp | 9 +++++++-- src/frontends/lean/parser.h | 10 +++++++--- tests/lean/var.lean | 12 ++++++++++++ tests/lean/var.lean.expected.out | 1 + 5 files changed, 42 insertions(+), 6 deletions(-) create mode 100644 tests/lean/var.lean create mode 100644 tests/lean/var.lean.expected.out diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 98ee92880..7132ad03e 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "util/sstream.h" #include "kernel/type_checker.h" #include "kernel/abstract.h" +#include "kernel/for_each_fn.h" #include "library/scoped_ext.h" #include "library/aliases.h" #include "library/private.h" @@ -66,17 +67,30 @@ void update_univ_parameters(buffer & ls_buffer, name_set const & found, pa 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(mlocal_name(e))) + throw parser_error(sstream() << "invalid parameter declaration '" << n << "', it depends on " << + "section variable '" << local_pp_name(e) << "'", pos); + return true; + }); +} + static environment declare_var(parser & p, environment env, name const & n, level_param_names const & ls, expr const & type, 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) + check_parameter_type(p, n, type, 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); + p.add_local_expr(n, l, k == variable_kind::Variable); return env; } else { + lean_assert(k == variable_kind::Constant || k == variable_kind::Axiom); name const & ns = get_namespace(env); name full_n = ns + n; if (k == variable_kind::Axiom) { diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 13511a8e8..10caed36e 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -95,6 +95,7 @@ parser::parser(environment const & env, io_state const & ios, if (s) { m_local_level_decls = s->m_lds; m_local_decls = s->m_eds; + m_variables = s->m_vars; m_options_stack = s->m_options_stack; } m_num_threads = num_threads; @@ -428,8 +429,12 @@ void parser::add_local_level(name const & n, level const & l) { m_local_level_decls.insert(n, l); } -void parser::add_local_expr(name const & n, expr const & p) { +void parser::add_local_expr(name const & n, expr const & p, bool is_variable) { m_local_decls.insert(n, p); + if (is_variable) { + lean_assert(is_local(p)); + m_variables.insert(mlocal_name(p)); + } } unsigned parser::get_local_level_index(name const & n) const { @@ -1347,7 +1352,7 @@ void parser::save_snapshot() { if (!m_snapshot_vector) return; if (m_snapshot_vector->empty() || static_cast(m_snapshot_vector->back().m_line) != m_scanner.get_line()) - m_snapshot_vector->push_back(snapshot(m_env, m_local_level_decls, m_local_decls, + m_snapshot_vector->push_back(snapshot(m_env, m_local_level_decls, m_local_decls, m_variables, m_options_stack, m_ios.get_options(), m_scanner.get_line())); } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index d8e399e62..1c02fc33b 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -51,14 +51,16 @@ struct snapshot { environment m_env; local_level_decls m_lds; local_expr_decls m_eds; + name_set m_vars; // subset of m_eds that is tagged as section variables options_stack m_options_stack; options m_options; unsigned m_line; snapshot():m_line(0) {} snapshot(environment const & env, options const & o):m_env(env), m_options(o), m_line(1) {} snapshot(environment const & env, local_level_decls const & lds, local_expr_decls const & eds, - options_stack const & os, options const & opts, unsigned line): - m_env(env), m_lds(lds), m_eds(eds), m_options_stack(os), m_options(opts), m_line(line) {} + name_set const & vars, options_stack const & os, options const & opts, + unsigned line): + m_env(env), m_lds(lds), m_eds(eds), m_vars(vars), m_options_stack(os), m_options(opts), m_line(line) {} }; typedef std::vector snapshot_vector; @@ -75,6 +77,7 @@ class parser { scanner::token_kind m_curr; local_level_decls m_local_level_decls; local_expr_decls m_local_decls; + name_set m_variables; // subset of m_local_decls that is marked as variables options_stack m_options_stack; pos_info m_last_cmd_pos; pos_info m_last_script_pos; @@ -309,8 +312,9 @@ public: struct local_scope { parser & m_p; environment m_env; local_scope(parser & p); ~local_scope(); }; void add_local_level(name const & n, level const & l); - void add_local_expr(name const & n, expr const & p); + 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_variable(name const & n) const { return m_variables.contains(n); } /** \brief Position of the local level declaration named \c n in the sequence of local level decls. */ unsigned get_local_level_index(name const & n) const; /** \brief Position of the local declaration named \c n in the sequence of local decls. */ diff --git a/tests/lean/var.lean b/tests/lean/var.lean new file mode 100644 index 000000000..e8109d8c4 --- /dev/null +++ b/tests/lean/var.lean @@ -0,0 +1,12 @@ +import logic + + +section + variable A : Type + parameter a : A +end + +section + variable A : Type + variable a : A +end diff --git a/tests/lean/var.lean.expected.out b/tests/lean/var.lean.expected.out new file mode 100644 index 000000000..6dc85136c --- /dev/null +++ b/tests/lean/var.lean.expected.out @@ -0,0 +1 @@ +var.lean:6:12: error: invalid parameter declaration 'a', it depends on section variable 'A'