From 50c147cd0ea338b065e387eb562fec6a0ac4fd15 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 18 Aug 2016 20:57:06 -0700
Subject: [PATCH] feat(frontends/lean/parser): allow string literals in
 patterns

---
 library/init/char.lean        | 1 +
 library/init/string.lean      | 4 ++++
 src/frontends/lean/parser.cpp | 4 ++--
 src/library/string.h          | 2 ++
 4 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/library/init/char.lean b/library/init/char.lean
index 0efe078552..f5b0d5bae7 100644
--- a/library/init/char.lean
+++ b/library/init/char.lean
@@ -11,6 +11,7 @@ definition char := fin 256
 
 namespace char
 
+attribute [pattern]
 definition of_nat (n : nat) : char :=
 if H : n < 256 then fin.mk n H else fin.mk 0 dec_trivial
 
diff --git a/library/init/string.lean b/library/init/string.lean
index db755a0a9b..0cb4a208e7 100644
--- a/library/init/string.lean
+++ b/library/init/string.lean
@@ -10,7 +10,11 @@ attribute [reducible]
 definition string := list char
 
 namespace string
+
+attribute [pattern]
 definition empty : string := list.nil
+
+attribute [pattern]
 definition str : char → string → string := list.cons
 
 definition concat (a b : string) : string :=
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index e1bd332836..f666c4b472 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1709,7 +1709,7 @@ struct to_pattern_fn {
     void collect_new_locals(expr const & e, bool skip_main_fn) {
         if (is_typed_expr(e)) {
             collect_new_locals(get_typed_expr_expr(e), false);
-        } else if (is_prenum(e)) {
+        } else if (is_prenum(e) || is_string_macro(e)) {
             // do nothing
         } else if (is_inaccessible(e)) {
             // do nothing
@@ -1754,7 +1754,7 @@ struct to_pattern_fn {
             expr new_v = visit(get_typed_expr_expr(e));
             expr new_t = to_expr(get_typed_expr_type(e));
             return copy_tag(e, mk_typed_expr(new_t, new_v));
-        } else if (is_prenum(e)) {
+        } else if (is_prenum(e) || is_string_macro(e)) {
             return e;
         } else if (is_inaccessible(e)) {
             return to_expr(e);
diff --git a/src/library/string.h b/src/library/string.h
index 792afccfba..70743be21e 100644
--- a/src/library/string.h
+++ b/src/library/string.h
@@ -17,6 +17,8 @@ expr from_string(std::string const & s);
     \see from_string */
 optional<std::string> to_string(expr const & e);
 
+bool is_string_macro(expr const & e);
+
 optional<char> to_char(expr const & e);
 
 format pp_string_literal(std::string const & s);