feat(frontends/lean): allow parameters only in contexts

src/frontends/lean/builtin_cmds.cpp

@@ -121,7 +121,7 @@ static void redeclare_aliases(parser & p,
                               list<pair<name, level>> old_level_entries,
                               list<pair<name, expr>> old_entries) {
     environment const & env = p.env();
-    if (!in_section_or_context(env))
+    if (!in_context(env))
         return;
     list<pair<name, expr>> new_entries = p.get_local_entries();
     buffer<pair<name, expr>> to_redeclare;

src/frontends/lean/decl_cmds.cpp

@@ -25,7 +25,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 static environment declare_universe(parser & p, environment env, name const & n, bool local) {
-    if (in_section_or_context(env) || local) {
+    if (in_context(env) || local) {
         p.add_local_level(n, mk_param_univ(n));
     } else {
         name const & ns = get_namespace(env);
@@ -112,7 +112,7 @@ static environment declare_var(parser & p, environment env,
     if (_bi) bi = *_bi;
     if (k == variable_kind::Parameter || k == variable_kind::Variable) {
         if (k == variable_kind::Parameter) {
-            check_in_section_or_context(p);
+            check_in_context(p);
             check_parameter_type(p, n, type, pos);
         }
         if (p.get_local(n))

src/frontends/lean/notation_cmd.cpp

@@ -49,7 +49,7 @@ static unsigned parse_precedence(parser & p, char const * msg) {
 
 LEAN_THREAD_VALUE(bool, g_allow_local, false);
 
-static void check_notation_expr(parser & p, expr const & e, pos_info const & pos) {
+static void check_notation_expr(expr const & e, pos_info const & pos) {
     if (!g_allow_local && (has_local(e) || has_param_univ(e)))
         throw parser_error("invalid notation declaration, contains reference to local variables", pos);
 }
@@ -89,7 +89,7 @@ static pair<notation_entry, optional<token_entry>> parse_mixfix_notation(parser
     p.check_token_next(get_assign_tk(), "invalid notation declaration, ':=' expected");
     auto f_pos = p.pos();
     expr f     = p.parse_expr();
-    check_notation_expr(p, f, f_pos);
+    check_notation_expr(f, f_pos);
     char const * tks = tk.c_str();
     switch (k) {
     case mixfix_kind::infixl:
@@ -145,7 +145,7 @@ static expr parse_notation_expr(parser & p, buffer<expr> const & locals) {
     auto pos = p.pos();
     expr r = p.parse_expr();
     r = abstract(r, locals.size(), locals.data());
-    check_notation_expr(p, r, pos);
+    check_notation_expr(r, pos);
     return r;
 }
 
@@ -273,7 +273,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, buffer<toke
         p.check_token_next(get_assign_tk(), "invalid numeral notation, `:=` expected");
         auto e_pos = p.pos();
         expr e     = p.parse_expr();
-        check_notation_expr(p, e, e_pos);
+        check_notation_expr(e, e_pos);
         return notation_entry(num, e, overload);
     } else if (p.curr_is_identifier()) {
         parse_notation_local(p, locals);

src/frontends/lean/parser.cpp

@@ -1074,7 +1074,7 @@ name parser::check_constant_next(char const * msg) {
     name id = check_id_next(msg);
     expr e  = id_to_expr(id, p);
 
-    if (in_section_or_context(m_env) && is_as_atomic(e)) {
+    if (in_context(m_env) && is_as_atomic(e)) {
         e = get_app_fn(get_as_atomic_arg(e));
         if (is_explicit(e))
             e = get_explicit_arg(e);

src/frontends/lean/structure_cmd.cpp

@@ -114,9 +114,9 @@ struct structure_cmd_fn {
         }
     }
 
-    /** \brief Include in m_level_names any section level referenced m_type and m_fields */
+    /** \brief Include in m_level_names any local level referenced m_type and m_fields */
-    void include_section_levels() {
+    void include_local_levels() {
-        if (!in_section_or_context(m_env))
+        if (!in_context(m_env))
             return;
         name_set all_lvl_params;
         all_lvl_params = collect_univ_params(m_type);
@@ -144,11 +144,11 @@ struct structure_cmd_fn {
         collect_locals(tmp, ls);
     }
 
-    /** \brief Include the used section parameters as additional arguments.
+    /** \brief Include the used parameters as additional arguments.
         The section parameters are stored in section_params
     */
     void abstract_section_locals(buffer<expr> & section_params) {
-        if (!in_section_or_context(m_env))
+        if (!in_context(m_env))
             return;
         expr_struct_set section_locals;
         collect_section_locals(section_locals);
@@ -265,7 +265,7 @@ struct structure_cmd_fn {
         m_p.check_token_next(get_dcolon_tk(), "invalid 'structure', '::' expected");
         m_p.parse_binders(m_fields, m_nentries);
         m_type = Pi(m_params, m_type, m_p);
-        include_section_levels();
+        include_local_levels();
         buffer<expr> section_params;
         abstract_section_locals(section_params);
         elaborate_type();

src/frontends/lean/util.cpp

@@ -33,9 +33,9 @@ void check_atomic(name const & n) {
         throw exception(sstream() << "invalid declaration name '" << n << "', identifier must be atomic");
 }
 
-void check_in_section_or_context(parser const & p) {
+void check_in_context(parser const & p) {
-    if (!in_section_or_context(p.env()))
+    if (!in_context(p.env()))
-        throw exception(sstream() << "invalid command, it must be used in a section");
+        throw exception(sstream() << "invalid command, it must be used in a (local) context");
 }
 bool is_root_namespace(name const & n) {
     return n == get_root_tk();

src/frontends/lean/util.h

@@ -19,7 +19,7 @@ typedef std::unique_ptr<type_checker> type_checker_ptr;
 bool parse_persistent(parser & p, bool & persistent);
 
 void check_atomic(name const & n);
-void check_in_section_or_context(parser const & p);
+void check_in_context(parser const & p);
 bool is_root_namespace(name const & n);
 name remove_root_prefix(name const & n);
 /** \brief Return the local levels in \c ls that are not tagged as variables.

tests/lean/crash.lean

@@ -1,6 +1,6 @@
 import logic
 
-section
+context
 hypothesis P : Prop.
 
 definition crash

tests/lean/interactive/sec_info_bug.input

@@ -3,7 +3,7 @@ SYNC 10
 import logic
 constant category : Type -> Type
 namespace category
-  section
+  context
   parameters {ob : Type} {C : category ob}
   variables {a b c d : ob}
   definition hom : ob → ob → Type := let aux := C in sorry

tests/lean/run/basic.lean

@@ -36,7 +36,7 @@ infix `=`:50 := eq
 
 check eq.{1}
 
-section
+context
   universe l
   universe u
   variable {T1 : Type.{l}}

tests/lean/run/univ1.lean

@@ -19,7 +19,7 @@ end S2
 
 
 namespace S3
-section
+context
   hypothesis I : Type
   definition F (X : Type) : Type := (X → Prop) → Prop
   hypothesis unfold : I → F I

tests/lean/run/univs.lean

@@ -1,7 +1,7 @@
 import algebra.category.basic
 
 set_option pp.universes true
-section
+context
   universes l₁ l₂ l₃ l₄
   parameter C : Category.{l₁ l₂}
   parameter f : Category.{l₁ l₂} → Category.{l₃ l₄}

tests/lean/t3.lean

@@ -7,13 +7,13 @@ namespace tst
 end tst
 print raw Type.{tst.v}
 print raw Type.{v}  -- Error: alias 'v' is not available anymore
-section
+context
   universe z        -- Remark: this is a local universe
   print raw Type.{z}
 end
 print raw Type.{z}  -- Error: local universe 'z' is gone
-section
+context
-  namespace foo -- Error: we cannot create a namespace inside a section
+  namespace foo -- Error: we cannot create a namespace inside a context
 end
 namespace tst
   print raw Type.{v} -- Remark: alias 'v' is available again