From a2f43212d669880c520fbcd028bb6d23349135dc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 Nov 2015 15:22:21 -0800 Subject: [PATCH] feat(frontends/lean): add '[no_pattern]' attribute --- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/builtin_cmds.cpp | 3 +++ src/frontends/lean/decl_attributes.cpp | 12 ++++++++++-- src/frontends/lean/decl_attributes.h | 1 + src/frontends/lean/token_table.cpp | 2 +- src/frontends/lean/tokens.cpp | 4 ++++ src/frontends/lean/tokens.h | 1 + src/frontends/lean/tokens.txt | 1 + 8 files changed, 22 insertions(+), 4 deletions(-) diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 9c7f6f643..f51d38be3 100644 --- a/src/emacs/lean-syntax.el +++ b/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") diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index d4837332b..c3431a349 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/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; diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index b9d759bbe..63b4475e3 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/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(d); } } diff --git a/src/frontends/lean/decl_attributes.h b/src/frontends/lean/decl_attributes.h index d5d874d06..2e316063b 100644 --- a/src/frontends/lean/decl_attributes.h +++ b/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 m_recursor_major_pos; optional m_priority; list m_unfold_hint; diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 83aebb2f3..cd2ab553c 100644 --- a/src/frontends/lean/token_table.cpp +++ b/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", diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 8f27100e3..b83322ceb 100644 --- a/src/frontends/lean/tokens.cpp +++ b/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; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 6d026d145..3ddda8e16 100644 --- a/src/frontends/lean/tokens.h +++ b/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(); diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt index e8ad550ca..a561f7644 100644 --- a/src/frontends/lean/tokens.txt +++ b/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