feat(frontends/lean): persistent notation in sections

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

library/data/list/basic.lean

@@ -276,10 +276,5 @@ nat.rec (λl, head x l) (λm f l, f (tail l)) n l
 theorem nth_zero {x : T} {l : list T} : nth x l 0 = head x l
 
 theorem nth_succ {x : T} {l : list T} {n : ℕ} : nth x l (succ n) = nth x (tail l) n
-
 end
-
--- declare global notation outside the section
-infixl `++` := concat
-
 end list

library/struc/binary.lean

@@ -5,32 +5,30 @@ import logic.core.eq
 open eq_ops
 
 namespace binary
-section
-  parameter {A : Type}
-  parameter f : A → A → A
-  infixl `*`:75 := f
+  context
+    parameter {A : Type}
+    parameter f : A → A → A
+    infixl `*`:75 := f
+    abbreviation commutative := ∀{a b}, a*b = b*a
+    abbreviation associative := ∀{a b c}, (a*b)*c = a*(b*c)
+  end
 
-  abbreviation commutative := ∀a b, a*b = b*a
-  abbreviation associative := ∀a b c, (a*b)*c = a*(b*c)
-end
+  context
+    parameter {A : Type}
+    parameter {f : A → A → A}
+    hypothesis H_comm : commutative f
+    hypothesis H_assoc : associative f
+    infixl `*`:75 := f
+    theorem left_comm : ∀a b c, a*(b*c) = b*(a*c) :=
+    take a b c, calc
+      a*(b*c) = (a*b)*c  : H_assoc⁻¹
+        ...   = (b*a)*c  : {H_comm}
+        ...   = b*(a*c)  : H_assoc
 
-section
-  parameter {A : Type}
-  parameter {f : A → A → A}
-  infixl `*`:75 := f
-  hypothesis H_comm : commutative f
-  hypothesis H_assoc : associative f
-
-  theorem left_comm : ∀a b c, a*(b*c) = b*(a*c) :=
-  take a b c, calc
-    a*(b*c) = (a*b)*c  : (H_assoc _ _ _)⁻¹
-      ...   = (b*a)*c  : {H_comm _ _}
-      ...   = b*(a*c)  : H_assoc _ _ _
-
-  theorem right_comm : ∀a b c, (a*b)*c = (a*c)*b :=
-  take a b c, calc
-    (a*b)*c = a*(b*c) : H_assoc _ _ _
-      ...   = a*(c*b) : {H_comm _ _}
-      ...   = (a*c)*b : (H_assoc _ _ _)⁻¹
-end
+    theorem right_comm : ∀a b c, (a*b)*c = (a*c)*b :=
+    take a b c, calc
+      (a*b)*c = a*(b*c) : H_assoc
+        ...   = a*(c*b) : {H_comm}
+        ...   = (a*c)*b : H_assoc⁻¹
+  end
 end binary

src/frontends/lean/notation_cmd.cpp

@@ -7,7 +7,11 @@ Author: Leonardo de Moura
 #include <utility>
 #include <limits>
 #include <string>
+#include "util/sstream.h"
 #include "kernel/abstract.h"
+#include "kernel/replace_fn.h"
+#include "library/scoped_ext.h"
+#include "library/explicit.h"
 #include "frontends/lean/parser.h"
 
 namespace lean {
@@ -69,6 +73,54 @@ environment precedence_cmd(parser & p) {
     return add_token(p.env(), tk.c_str(), prec);
 }
 
+/** \brief Auxiliary function for #cleanup_section_notation. */
+expr cleanup_section_notation_core(parser & p, expr const & e) {
+    if (is_implicit(e)) {
+        return cleanup_section_notation_core(p, get_implicit_arg(e));
+    } else if (is_explicit(e)) {
+        return cleanup_section_notation_core(p, get_explicit_arg(e));
+    } else if (is_app(e)) {
+        buffer<expr> args;
+        expr const & f = get_app_args(e, args);
+        for (expr arg : args) {
+            if (!is_explicit(arg))
+                throw parser_error("unexpected expression in (section) notation", p.pos_of(arg));
+            arg = get_explicit_arg(arg);
+            if (!is_local(arg))
+                throw parser_error("unexpected expression in (section) notation", p.pos_of(arg));
+            binder_info bi = local_info(arg);
+            if (!bi.is_strict_implicit() && !bi.is_implicit())
+                throw parser_error(sstream() << "invalid occurrence of local parameter '" << local_pp_name(arg)
+                                   << "' in (section) notation that is not implicit", p.pos_of(e));
+        }
+        return cleanup_section_notation_core(p, f);
+    } else if (is_constant(e)) {
+        return p.save_pos(mk_constant(const_name(e)), p.pos_of(e));
+    } else if (is_local(e)) {
+        throw parser_error(sstream() << "invalid occurrence of local parameter '" << local_pp_name(e)
+                           << "' in (section) notation", p.pos_of(e));
+    } else {
+        throw parser_error("unexpected expression in (section) notation", p.pos_of(e));
+    }
+}
+
+/** \brief Replace reference to implicit section local constants and universes with placeholders.
+
+    \remark Throws an exception if \c e contains a local constant that is not implicit.
+*/
+expr cleanup_section_notation(parser & p, expr const & e) {
+    if (!in_section(p.env()))
+        return e;
+    return replace(e, [&](expr const & e) {
+            if (is_local(e))
+                throw parser_error(sstream() << "invalid occurrence of local parameter '" << local_pp_name(e)
+                                   << "' in (section) notation", p.pos_of(e));
+            if (is_implicit(e))
+                return some_expr(cleanup_section_notation_core(p, e));
+            return none_expr();
+        });
+}
+
 enum class mixfix_kind { infixl, infixr, postfix, prefix };
 
 using notation::mk_expr_action;
@@ -102,7 +154,7 @@ static pair<notation_entry, optional<token_entry>> parse_mixfix_notation(parser
     if (k == mixfix_kind::infixr && *prec == 0)
         throw parser_error("invalid infixr declaration, precedence must be greater than zero", p.pos());
     p.check_token_next(g_assign, "invalid notation declaration, ':=' expected");
-    expr f = p.parse_expr();
+    expr f = cleanup_section_notation(p, p.parse_expr());
     char const * tks = tk.c_str();
     switch (k) {
     case mixfix_kind::infixl:
@@ -166,7 +218,7 @@ static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_t
 
 static expr parse_notation_expr(parser & p, buffer<expr> const & locals) {
     expr r = p.parse_expr();
-    return abstract(r, locals.size(), locals.data());
+    return cleanup_section_notation(p, abstract(r, locals.size(), locals.data()));
 }
 
 static expr g_local_type = mk_Prop(); // type used in notation local declarations, it is irrelevant

src/frontends/lean/parser_config.cpp

@@ -54,8 +54,8 @@ struct token_config {
     }
 };
 
-template class scoped_ext<token_config, true>;
-typedef scoped_ext<token_config, true> token_ext;
+template class scoped_ext<token_config>;
+typedef scoped_ext<token_config> token_ext;
 
 environment add_token(environment const & env, token_entry const & e) {
     return token_ext::add_entry(env, get_dummy_ios(), e);
@@ -188,8 +188,8 @@ struct notation_config {
     }
 };
 
-template class scoped_ext<notation_config, true>;
-typedef scoped_ext<notation_config, true> notation_ext;
+template class scoped_ext<notation_config>;
+typedef scoped_ext<notation_config> notation_ext;
 
 environment add_notation(environment const & env, notation_entry const & e) {
     return notation_ext::add_entry(env, get_dummy_ios(), e);

src/library/scoped_ext.h

@@ -38,6 +38,7 @@ name const & get_namespace(environment const & env);
 list<name> const & get_namespaces(environment const & env);
 bool in_section_or_context(environment const & env);
 bool in_context(environment const & env);
+inline bool in_section(environment const & env) { return in_section_or_context(env) && !in_context(env); }
 
 /** \brief Check if \c n may be a reference to a namespace, if it is return it.
     The procedure checks if \c n is a registered namespace, if it is not, it tries

tests/lean/run/algebra1.lean

@@ -2,7 +2,7 @@ import logic
 
 abbreviation Type1 := Type.{1}
 
-section
+context
   parameter {A  : Type}
   parameter f   : A → A → A
   parameter one : A

tests/lean/run/cody1.lean

@@ -2,7 +2,7 @@ import logic
 
 abbreviation subsets (P : Type) := P → Prop.
 
-section
+context
 
 hypothesis A : Type.
 

tests/lean/run/cody2.lean

@@ -2,7 +2,7 @@ import logic
 open eq
 abbreviation subsets (P : Type) := P → Prop.
 
-section
+context
 
 hypothesis A : Type.
 

tests/lean/run/group.lean

@@ -1,6 +1,6 @@
 import logic
 
-section
+context
   parameter {A  : Type}
   parameter f   : A → A → A
   parameter one : A

tests/lean/run/group2.lean

@@ -1,6 +1,6 @@
 import logic
 
-section
+context
   parameter {A  : Type}
   parameter f   : A → A → A
   parameter one : A

tests/lean/run/n4.lean

@@ -1,5 +1,5 @@
 definition Prop [inline] : Type.{1} := Type.{0}
-section
+context
   variable N : Type.{1}
   variables a b c : N
   variable and : Prop → Prop → Prop

tests/lean/run/secnot.lean

@@ -0,0 +1,25 @@
+import data.num
+
+section
+parameter {A : Type}
+definition f (a b : A) := a
+infixl `◀`:65 := f
+parameters a b : A
+check a ◀ b
+end
+
+inductive list (T : Type) : Type :=
+nil {} : list T,
+cons   : T → list T → list T
+
+namespace list
+section
+variable {T : Type}
+notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
+check [10, 20, 30]
+end
+end list
+
+open list
+check [10, 20, 40]
+check 10 ◀ 20