feat(frontends/lean): enforce rule section parameters cannot depend on section variables

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<name> & 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<binder_info> 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) {

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<int>(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()));
 }
 

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> 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. */

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

tests/lean/var.lean.expected.out

@@ -0,0 +1 @@
+var.lean:6:12: error: invalid parameter declaration 'a', it depends on section variable 'A'