feat(frontends/lean): add '[parsing-only]' modifier to notation declarations, closes #305

library/type.lean

@@ -3,8 +3,8 @@
 -- Authors: Leonardo de Moura
 
 notation `Prop`  := Type.{0}
-notation `Type'` := Type.{_+1}
+notation [parsing-only] `Type'` := Type.{_+1}
-notation `Type₊` := Type.{_+1}
+notation [parsing-only] `Type₊` := Type.{_+1}
 notation `Type₁` := Type.{1}
 notation `Type₂` := Type.{2}
 notation `Type₃` := Type.{3}

src/emacs/lean-syntax.el

@@ -115,7 +115,7 @@
      ;; place holder
      (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
      ;; modifiers
-     (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]"
+     (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]" "\[parsing-only\]"
                "\[coercion\]" "\[reducible\]" "\[off\]" "\[none\]" "\[on\]")) . 'font-lock-doc-face)
      (,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
      ;; tactics

src/frontends/lean/notation_cmd.cpp

@@ -78,8 +78,21 @@ void check_not_forbidden(char const * tk) {
     }
 }
 
+struct notation_modifiers {
+    bool m_parse_only;
+    notation_modifiers():m_parse_only(false) {}
+    void parse(parser & p) {
+        if (p.curr_is_token(get_parsing_only_tk())) {
+            p.next();
+            m_parse_only = true;
+        }
+    }
+};
+
 static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool reserve)
 -> pair<notation_entry, optional<token_entry>> {
+    notation_modifiers mod;
+    mod.parse(p);
     std::string tk = parse_symbol(p, "invalid notation declaration, quoted symbol or identifier expected");
     char const * tks = tk.c_str();
     check_not_forbidden(tks);
@@ -156,16 +169,16 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool
         switch (k) {
         case mixfix_kind::infixl:
             return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))),
-                                          dummy, overload, reserve), new_token);
+                                          dummy, overload, reserve, mod.m_parse_only), new_token);
         case mixfix_kind::infixr:
             return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec-1))),
-                                          dummy, overload, reserve), new_token);
+                                          dummy, overload, reserve, mod.m_parse_only), new_token);
         case mixfix_kind::postfix:
             return mk_pair(notation_entry(false, to_list(transition(tks, mk_skip_action())),
-                                          dummy, overload, reserve), new_token);
+                                          dummy, overload, reserve, mod.m_parse_only), new_token);
         case mixfix_kind::prefix:
             return mk_pair(notation_entry(true, to_list(transition(tks, mk_expr_action(*prec))),
-                                          dummy, overload, reserve), new_token);
+                                          dummy, overload, reserve, mod.m_parse_only), new_token);
         }
     } else {
         p.check_token_next(get_assign_tk(), "invalid notation declaration, ':=' expected");
@@ -175,16 +188,16 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool
         switch (k) {
         case mixfix_kind::infixl:
             return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))),
-                                          mk_app(f, Var(1), Var(0)), overload, reserve), new_token);
+                                          mk_app(f, Var(1), Var(0)), overload, reserve, mod.m_parse_only), new_token);
         case mixfix_kind::infixr:
             return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec-1))),
-                                          mk_app(f, Var(1), Var(0)), overload, reserve), new_token);
+                                          mk_app(f, Var(1), Var(0)), overload, reserve, mod.m_parse_only), new_token);
         case mixfix_kind::postfix:
             return mk_pair(notation_entry(false, to_list(transition(tks, mk_skip_action())),
-                                          mk_app(f, Var(0)), overload, reserve), new_token);
+                                          mk_app(f, Var(0)), overload, reserve, mod.m_parse_only), new_token);
         case mixfix_kind::prefix:
             return mk_pair(notation_entry(true, to_list(transition(tks, mk_expr_action(*prec))),
-                                          mk_app(f, Var(0)), overload, reserve), new_token);
+                                          mk_app(f, Var(0)), overload, reserve, mod.m_parse_only), new_token);
         }
     }
     lean_unreachable(); // LCOV_EXCL_LINE
@@ -372,6 +385,8 @@ static notation_entry parse_notation_core(parser & p, bool overload, bool reserv
     bool is_nud = true;
     optional<parse_table> pt;
     optional<parse_table> reserved_pt;
+    notation_modifiers mod;
+    mod.parse(p);
     if (p.curr_is_numeral()) {
         lean_assert(p.curr_is_numeral());
         mpz num = p.get_num_val().get_numerator();
@@ -380,7 +395,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, bool reserv
         auto e_pos = p.pos();
         expr e     = p.parse_expr();
         check_notation_expr(e, e_pos);
-        return notation_entry(num, e, overload);
+        return notation_entry(num, e, overload, mod.m_parse_only);
     } else if (p.curr_is_identifier()) {
         parse_notation_local(p, locals);
         is_nud = false;
@@ -474,7 +489,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, bool reserv
             throw parser_error("invalid notation declaration, empty notation is not allowed", p.pos());
         n = parse_notation_expr(p, locals);
     }
-    return notation_entry(is_nud, to_list(ts.begin(), ts.end()), n, overload, reserve);
+    return notation_entry(is_nud, to_list(ts.begin(), ts.end()), n, overload, reserve, mod.m_parse_only);
 }
 
 bool curr_is_notation_decl(parser & p) {

src/frontends/lean/parser_config.cpp

@@ -20,26 +20,26 @@ using notation::action_kind;
 
 notation_entry replace(notation_entry const & e, std::function<expr(expr const &)> const & f) {
     if (e.is_numeral())
-        return notation_entry(e.get_num(), f(e.get_expr()), e.overload());
+        return notation_entry(e.get_num(), f(e.get_expr()), e.overload(), e.parse_only());
     else
         return notation_entry(e.is_nud(),
                               map(e.get_transitions(), [&](transition const & t) { return notation::replace(t, f); }),
-                              f(e.get_expr()), e.overload(), e.reserve());
+                              f(e.get_expr()), e.overload(), e.reserve(), e.parse_only());
 }
 
 notation_entry::notation_entry():m_kind(notation_entry_kind::NuD) {}
 notation_entry::notation_entry(notation_entry const & e):
     m_kind(e.m_kind), m_expr(e.m_expr), m_overload(e.m_overload),
-    m_safe_ascii(e.m_safe_ascii), m_reserve(e.m_reserve) {
+    m_safe_ascii(e.m_safe_ascii), m_reserve(e.m_reserve), m_parse_only(e.m_parse_only) {
     if (is_numeral())
         new (&m_num) mpz(e.m_num);
     else
         new (&m_transitions) list<transition>(e.m_transitions);
 }
 
-notation_entry::notation_entry(bool is_nud, list<transition> const & ts, expr const & e, bool overload, bool reserve):
+notation_entry::notation_entry(bool is_nud, list<transition> const & ts, expr const & e, bool overload, bool reserve, bool parse_only):
     m_kind(is_nud ? notation_entry_kind::NuD : notation_entry_kind::LeD),
-    m_expr(e), m_overload(overload), m_reserve(reserve) {
+    m_expr(e), m_overload(overload), m_reserve(reserve), m_parse_only(parse_only) {
     new (&m_transitions) list<transition>(ts);
     m_safe_ascii = std::all_of(ts.begin(), ts.end(), [](transition const & t) { return t.is_safe_ascii(); });
 }
@@ -47,8 +47,8 @@ notation_entry::notation_entry(notation_entry const & e, bool overload):
     notation_entry(e) {
     m_overload = overload;
 }
-notation_entry::notation_entry(mpz const & val, expr const & e, bool overload):
+notation_entry::notation_entry(mpz const & val, expr const & e, bool overload, bool parse_only):
-    m_kind(notation_entry_kind::Numeral), m_expr(e), m_overload(overload), m_safe_ascii(true), m_reserve(false) {
+    m_kind(notation_entry_kind::Numeral), m_expr(e), m_overload(overload), m_safe_ascii(true), m_reserve(false), m_parse_only(parse_only) {
     new (&m_num) mpz(val);
 }
 
@@ -61,7 +61,7 @@ notation_entry::~notation_entry() {
 
 bool operator==(notation_entry const & e1, notation_entry const & e2) {
     if (e1.kind() != e2.kind() || e1.overload() != e2.overload() || e1.get_expr() != e2.get_expr() ||
-        e1.reserve() != e2.reserve())
+        e1.reserve() != e2.reserve() || e1.parse_only() != e2.parse_only())
         return false;
     if (e1.is_numeral())
         return e1.get_num() == e2.get_num();
@@ -217,7 +217,8 @@ struct notation_config {
     static std::string * g_key;
 
     static void updt_inv_map(state & s, head_index const & idx, entry const & e) {
-        s.m_inv_map.insert(idx, e);
+        if (!e.parse_only())
+            s.m_inv_map.insert(idx, e);
     }
 
     static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
@@ -259,7 +260,7 @@ struct notation_config {
         return *g_key;
     }
     static void  write_entry(serializer & s, entry const & e) {
-        s << static_cast<char>(e.kind()) << e.overload() << e.get_expr();
+        s << static_cast<char>(e.kind()) << e.overload() << e.parse_only() << e.get_expr();
         if (e.is_numeral()) {
             s << e.get_num();
         } else {
@@ -270,12 +271,12 @@ struct notation_config {
     }
     static entry read_entry(deserializer & d) {
         notation_entry_kind k = static_cast<notation_entry_kind>(d.read_char());
-        bool overload; expr e;
+        bool overload, parse_only; expr e;
-        d >> overload >> e;
+        d >> overload >> parse_only >> e;
         if (k == notation_entry_kind::Numeral) {
             mpz val;
             d >> val;
-            return entry(val, e, overload);
+            return entry(val, e, overload, parse_only);
         } else {
             bool is_nud = k == notation_entry_kind::NuD;
             bool reserve;
@@ -284,7 +285,7 @@ struct notation_config {
             buffer<transition> ts;
             for (unsigned i = 0; i < sz; i++)
                 ts.push_back(read_transition(d));
-            return entry(is_nud, to_list(ts.begin(), ts.end()), e, overload, reserve);
+            return entry(is_nud, to_list(ts.begin(), ts.end()), e, overload, reserve, parse_only);
         }
     }
     static optional<unsigned> get_fingerprint(entry const &) {
@@ -302,25 +303,25 @@ environment add_notation(environment const & env, notation_entry const & e) {
 }
 
 environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts,
-                             expr const & a, bool overload, bool reserve) {
+                             expr const & a, bool overload, bool reserve, bool parse_only) {
-    return add_notation(env, notation_entry(true, to_list(ts, ts+num), a, overload, reserve));
+    return add_notation(env, notation_entry(true, to_list(ts, ts+num), a, overload, reserve, parse_only));
 }
 
 environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts,
-                             expr const & a, bool overload, bool reserve) {
+                             expr const & a, bool overload, bool reserve, bool parse_only) {
-    return add_notation(env, notation_entry(false, to_list(ts, ts+num), a, overload, reserve));
+    return add_notation(env, notation_entry(false, to_list(ts, ts+num), a, overload, reserve, parse_only));
 }
 
 environment add_nud_notation(environment const & env, std::initializer_list<notation::transition> const & ts,
-                             expr const & a, bool overload) {
+                             expr const & a, bool overload, bool parse_only) {
     bool reserve = false;
-    return add_nud_notation(env, ts.size(), ts.begin(), a, overload, reserve);
+    return add_nud_notation(env, ts.size(), ts.begin(), a, overload, reserve, parse_only);
 }
 
 environment add_led_notation(environment const & env, std::initializer_list<notation::transition> const & ts,
-                             expr const & a, bool overload) {
+                             expr const & a, bool overload, bool parse_only) {
     bool reserve = false;
-    return add_led_notation(env, ts.size(), ts.begin(), a, overload, reserve);
+    return add_led_notation(env, ts.size(), ts.begin(), a, overload, reserve, parse_only);
 }
 
 parse_table const & get_nud_table(environment const & env) {
@@ -339,8 +340,8 @@ parse_table const & get_reserved_led_table(environment const & env) {
     return notation_ext::get_state(env).m_reserved_led;
 }
 
-environment add_mpz_notation(environment const & env, mpz const & n, expr const & e, bool overload) {
+environment add_mpz_notation(environment const & env, mpz const & n, expr const & e, bool overload, bool parse_only) {
-    return add_notation(env, notation_entry(n, e, overload));
+    return add_notation(env, notation_entry(n, e, overload, parse_only));
 }
 
 list<expr> get_mpz_notation(environment const & env, mpz const & n) {

src/frontends/lean/parser_config.h

@@ -31,11 +31,12 @@ class notation_entry {
     bool                 m_overload;
     bool                 m_safe_ascii;
     bool                 m_reserve;
+    bool                 m_parse_only;
 public:
     notation_entry();
     notation_entry(notation_entry const & e);
-    notation_entry(bool is_nud, list<transition> const & ts, expr const & e, bool overload, bool reserve);
+    notation_entry(bool is_nud, list<transition> const & ts, expr const & e, bool overload, bool reserve, bool parse_only);
-    notation_entry(mpz const & val, expr const & e, bool overload);
+    notation_entry(mpz const & val, expr const & e, bool overload, bool parse_only);
     notation_entry(notation_entry const & e, bool overload);
     ~notation_entry();
     notation_entry_kind kind() const { return m_kind; }
@@ -47,6 +48,7 @@ public:
     bool overload() const { return m_overload; }
     bool is_safe_ascii() const { return m_safe_ascii; }
     bool reserve() const { return m_reserve; }
+    bool parse_only() const { return m_parse_only; }
 };
 bool operator==(notation_entry const & e1, notation_entry const & e2);
 inline bool operator!=(notation_entry const & e1, notation_entry const & e2) {
@@ -61,13 +63,13 @@ environment add_notation(environment const & env, notation_entry const & e);
 
 environment add_token(environment const & env, char const * val, unsigned prec);
 environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a,
-                             bool overload = true, bool reserve = false);
+                             bool overload = true, bool reserve = false, bool parse_only = false);
 environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a,
-                             bool overload = true, bool reserve = false);
+                             bool overload = true, bool reserve = false, bool parse_only = false);
 environment add_nud_notation(environment const & env, std::initializer_list<notation::transition> const & ts, expr const & a,
-                             bool overload = true);
+                             bool overload = true, bool parse_only = false);
 environment add_led_notation(environment const & env, std::initializer_list<notation::transition> const & ts, expr const & a,
-                             bool overload = true);
+                             bool overload = true, bool parse_only = false);
 token_table const & get_token_table(environment const & env);
 parse_table const & get_nud_table(environment const & env);
 parse_table const & get_led_table(environment const & env);
@@ -78,7 +80,7 @@ cmd_table const & get_cmd_table(environment const & env);
 environment overwrite_notation(environment const & env, name const & n);
 
 /** \brief Add \c n as notation for \c e */
-environment add_mpz_notation(environment const & env, mpz const & n, expr const & e, bool overload = true);
+environment add_mpz_notation(environment const & env, mpz const & n, expr const & e, bool overload = true, bool parse_only = false);
 /** \brief Return the additional interpretations for \c n in the current environment.
 
     \remark It does not include the default one based on the \c num inductive datatype.

src/frontends/lean/token_table.cpp

@@ -81,7 +81,7 @@ void init_token_table(token_table & t) {
     char const * commands[] =
         {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion",
          "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
-         "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "reducible", "irreducible",
+         "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[parsing-only]", "reducible", "irreducible",
          "evaluate", "check", "eval", "[priority", "print", "end", "namespace", "section", "import",
          "inductive", "record", "structure", "module", "universe", "universes",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",

src/frontends/lean/tokens.cpp

@@ -74,6 +74,7 @@ static name * g_instance     = nullptr;
 static name * g_priority     = nullptr;
 static name * g_coercion     = nullptr;
 static name * g_reducible    = nullptr;
+static name * g_parsing_only = nullptr;
 static name * g_with         = nullptr;
 static name * g_class        = nullptr;
 static name * g_prev         = nullptr;
@@ -161,6 +162,7 @@ void initialize_tokens() {
     g_priority     = new name("[priority");
     g_coercion     = new name("[coercion]");
     g_reducible    = new name("[reducible]");
+    g_parsing_only = new name("[parsing-only]");
     g_with         = new name("with");
     g_class        = new name("[class]");
     g_prev         = new name("prev");
@@ -212,6 +214,7 @@ void finalize_tokens() {
     delete g_priority;
     delete g_coercion;
     delete g_reducible;
+    delete g_parsing_only;
     delete g_in;
     delete g_assign;
     delete g_visible;
@@ -336,6 +339,7 @@ name const & get_instance_tk() { return *g_instance; }
 name const & get_priority_tk() { return *g_priority; }
 name const & get_coercion_tk() { return *g_coercion; }
 name const & get_reducible_tk() { return *g_reducible; }
+name const & get_parsing_only_tk() { return *g_parsing_only; }
 name const & get_class_tk() { return *g_class; }
 name const & get_with_tk() { return *g_with; }
 name const & get_prev_tk() { return *g_prev; }

src/frontends/lean/tokens.h

@@ -76,6 +76,7 @@ name const & get_instance_tk();
 name const & get_priority_tk();
 name const & get_coercion_tk();
 name const & get_reducible_tk();
+name const & get_parsing_only_tk();
 name const & get_class_tk();
 name const & get_with_tk();
 name const & get_prev_tk();

tests/lean/parsing_only.lean

@@ -0,0 +1,9 @@
+import logic
+
+constant f : num → num
+constant g : num → num
+notation a `+++` := f a
+notation [parsing-only] a `***` := g a
+check 10 +++
+check 10 ***
+check Type.{8}  -- Type₊ should not be used

tests/lean/parsing_only.lean.expected.out

@@ -0,0 +1,3 @@
+10 +++ : num
+g 10 : num
+Type : Type