feat(frontends/lean): add '[no_pattern]' attribute

src/emacs/lean-syntax.el

@@ -56,7 +56,7 @@
            "reducible" "irreducible" "semireducible" "quasireducible" "wf"
            "whnf" "multiple_instances" "none" "decls" "declarations"
            "coercions" "classes" "symm" "subst" "refl" "trans" "simp" "congr" "backward"
-           "notations" "abbreviations" "begin_end_hints" "tactic_hints"
+           "no_pattern" "notations" "abbreviations" "begin_end_hints" "tactic_hints"
            "reduce_hints" "unfold_hints" "aliases" "eqv"
            "localrefinfo" "recursor"))
   "lean modifiers")

src/frontends/lean/builtin_cmds.cpp

@@ -49,6 +49,7 @@ Author: Leonardo de Moura
 #include "library/blast/blast.h"
 #include "library/blast/simplifier/simplifier.h"
 #include "library/blast/backward/backward_rule_set.h"
+#include "library/blast/forward/pattern.h"
 #include "compiler/preprocess_rec.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/parser.h"
@@ -260,6 +261,8 @@ static void print_attributes(parser const & p, name const & n) {
         out << " [congr]";
     if (is_backward_rule(env, n))
         out << " [backward]";
+    if (is_no_pattern(env, n))
+        out << " [no_pattern]";
     switch (get_reducible_status(env, n)) {
     case reducible_status::Reducible:      out << " [reducible]"; break;
     case reducible_status::Irreducible:    out << " [irreducible]"; break;

src/frontends/lean/decl_attributes.cpp

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "library/coercion.h"
 #include "library/blast/simplifier/simp_rule_set.h"
 #include "library/blast/backward/backward_rule_set.h"
+#include "library/blast/forward/pattern.h"
 #include "frontends/lean/decl_attributes.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/tokens.h"
@@ -43,6 +44,7 @@ decl_attributes::decl_attributes(bool is_abbrev, bool persistent):
     m_simp                   = false;
     m_congr                  = false;
     m_backward               = false;
+    m_no_pattern             = false;
 }
 
 void decl_attributes::parse(parser & p) {
@@ -138,6 +140,9 @@ void decl_attributes::parse(parser & p) {
         } else if (p.curr_is_token(get_backward_attr_tk())) {
             p.next();
             m_backward = true;
+        } else if (p.curr_is_token(get_no_pattern_attr_tk())) {
+            p.next();
+            m_no_pattern = true;
         } else if (p.curr_is_token(get_recursor_tk())) {
             p.next();
             if (!p.curr_is_token(get_rbracket_tk())) {
@@ -224,6 +229,9 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c
         else
             env = add_backward_rule(env, d, LEAN_BACKWARD_DEFAULT_PRIORITY, m_persistent);
     }
+    if (m_no_pattern) {
+        env = add_no_pattern(env, d, m_persistent);
+    }
     if (m_has_multiple_instances)
         env = mark_multiple_instances(env, d, m_persistent);
     return env;
@@ -234,7 +242,7 @@ void decl_attributes::write(serializer & s) const {
       << m_is_reducible << m_is_irreducible << m_is_semireducible << m_is_quasireducible
       << m_is_class << m_is_parsing_only << m_has_multiple_instances << m_unfold_full_hint
       << m_constructor_hint << m_symm << m_trans << m_refl << m_subst << m_recursor
-      << m_simp << m_congr << m_recursor_major_pos << m_priority;
+      << m_simp << m_congr << m_recursor_major_pos << m_priority << m_backward << m_no_pattern;
     write_list(s, m_unfold_hint);
 }
 
@@ -243,7 +251,7 @@ void decl_attributes::read(deserializer & d) {
       >> m_is_reducible >> m_is_irreducible >> m_is_semireducible >> m_is_quasireducible
       >> m_is_class >> m_is_parsing_only >> m_has_multiple_instances >> m_unfold_full_hint
       >> m_constructor_hint >> m_symm >> m_trans >> m_refl >> m_subst >> m_recursor
-      >> m_simp >> m_congr >> m_recursor_major_pos >> m_priority;
+      >> m_simp >> m_congr >> m_recursor_major_pos >> m_priority >> m_backward >> m_no_pattern;
     m_unfold_hint = read_list<unsigned>(d);
 }
 }

src/frontends/lean/decl_attributes.h

@@ -32,6 +32,7 @@ class decl_attributes {
     bool               m_simp;
     bool               m_congr;
     bool               m_backward;
+    bool               m_no_pattern;
     optional<unsigned> m_recursor_major_pos;
     optional<unsigned> m_priority;
     list<unsigned>     m_unfold_hint;

src/frontends/lean/token_table.cpp

@@ -111,7 +111,7 @@ void init_token_table(token_table & t) {
          "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]",
          "[simp]", "[congr]", "[parsing_only]", "[multiple_instances]", "[symm]", "[trans]", "[refl]", "[subst]", "[recursor",
          "evaluate", "check", "eval", "[wf]", "[whnf]", "[priority", "[unfold_full]", "[unfold_hints]", "[backward]",
-         "[constructor]", "[unfold", "print",
+         "[no_pattern]", "[constructor]", "[unfold", "print",
          "end", "namespace", "section", "prelude", "help",
          "import", "inductive", "record", "structure", "module", "universe", "universes", "local",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation",

src/frontends/lean/tokens.cpp

@@ -121,6 +121,7 @@ static name const * g_subst_tk = nullptr;
 static name const * g_simp_attr_tk = nullptr;
 static name const * g_congr_attr_tk = nullptr;
 static name const * g_backward_attr_tk = nullptr;
+static name const * g_no_pattern_attr_tk = nullptr;
 static name const * g_recursor_tk = nullptr;
 static name const * g_attribute_tk = nullptr;
 static name const * g_with_tk = nullptr;
@@ -276,6 +277,7 @@ void initialize_tokens() {
     g_simp_attr_tk = new name{"[simp]"};
     g_congr_attr_tk = new name{"[congr]"};
     g_backward_attr_tk = new name{"[backward]"};
+    g_no_pattern_attr_tk = new name{"[no_pattern]"};
     g_recursor_tk = new name{"[recursor"};
     g_attribute_tk = new name{"attribute"};
     g_with_tk = new name{"with"};
@@ -432,6 +434,7 @@ void finalize_tokens() {
     delete g_simp_attr_tk;
     delete g_congr_attr_tk;
     delete g_backward_attr_tk;
+    delete g_no_pattern_attr_tk;
     delete g_recursor_tk;
     delete g_attribute_tk;
     delete g_with_tk;
@@ -587,6 +590,7 @@ name const & get_subst_tk() { return *g_subst_tk; }
 name const & get_simp_attr_tk() { return *g_simp_attr_tk; }
 name const & get_congr_attr_tk() { return *g_congr_attr_tk; }
 name const & get_backward_attr_tk() { return *g_backward_attr_tk; }
+name const & get_no_pattern_attr_tk() { return *g_no_pattern_attr_tk; }
 name const & get_recursor_tk() { return *g_recursor_tk; }
 name const & get_attribute_tk() { return *g_attribute_tk; }
 name const & get_with_tk() { return *g_with_tk; }

src/frontends/lean/tokens.h

@@ -123,6 +123,7 @@ name const & get_subst_tk();
 name const & get_simp_attr_tk();
 name const & get_congr_attr_tk();
 name const & get_backward_attr_tk();
+name const & get_no_pattern_attr_tk();
 name const & get_recursor_tk();
 name const & get_attribute_tk();
 name const & get_with_tk();

src/frontends/lean/tokens.txt

@@ -116,6 +116,7 @@ subst        [subst]
 simp_attr    [simp]
 congr_attr   [congr]
 backward_attr [backward]
+no_pattern_attr [no_pattern]
 recursor     [recursor
 attribute    attribute
 with         with