From 70a90ca73e4d7cd8f5ccb7aa78546e76478c5246 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 1 Oct 2019 14:19:37 -0700
Subject: [PATCH] feat(library/init/lean/parser/identifier): allow `!` and `?`
 in the identifiers

---
 library/init/lean/parser/identifier.lean |  2 +-
 src/stage0/init/lean/parser/identifier.c | 78 ++++++++++++++++--------
 src/util/name.cpp                        |  2 +-
 3 files changed, 53 insertions(+), 29 deletions(-)

diff --git a/library/init/lean/parser/identifier.lean b/library/init/lean/parser/identifier.lean
index b0d170ef9a..701e430496 100644
--- a/library/init/lean/parser/identifier.lean
+++ b/library/init/lean/parser/identifier.lean
@@ -28,7 +28,7 @@ def isIdFirst (c : Char) : Bool :=
 c.isAlpha || c = '_' || isLetterLike c
 
 def isIdRest (c : Char) : Bool :=
-c.isAlphanum || c = '_' || c = '\'' || isLetterLike c || isSubScriptAlnum c
+c.isAlphanum || c = '_' || c = '\'' || c == '!' || c == '?' || isLetterLike c || isSubScriptAlnum c
 
 def idBeginEscape := '«'
 def idEndEscape   := '»'
diff --git a/src/stage0/init/lean/parser/identifier.c b/src/stage0/init/lean/parser/identifier.c
index 4d348a9e8a..05265d6aba 100644
--- a/src/stage0/init/lean/parser/identifier.c
+++ b/src/stage0/init/lean/parser/identifier.c
@@ -538,40 +538,64 @@ x_5 = 39;
 x_6 = x_1 == x_5;
 if (x_6 == 0)
 {
-uint8_t x_7; 
-x_7 = l_Lean_isLetterLike(x_1);
-if (x_7 == 0)
+uint32_t x_7; uint8_t x_8; 
+x_7 = 33;
+x_8 = x_1 == x_7;
+if (x_8 == 0)
 {
-uint8_t x_8; 
-x_8 = l_Lean_isSubScriptAlnum(x_1);
-return x_8;
-}
-else
-{
-uint8_t x_9; 
-x_9 = 1;
-return x_9;
-}
-}
-else
-{
-uint8_t x_10; 
-x_10 = 1;
-return x_10;
-}
-}
-else
+uint32_t x_9; uint8_t x_10; 
+x_9 = 63;
+x_10 = x_1 == x_9;
+if (x_10 == 0)
 {
 uint8_t x_11; 
-x_11 = 1;
-return x_11;
+x_11 = l_Lean_isLetterLike(x_1);
+if (x_11 == 0)
+{
+uint8_t x_12; 
+x_12 = l_Lean_isSubScriptAlnum(x_1);
+return x_12;
+}
+else
+{
+uint8_t x_13; 
+x_13 = 1;
+return x_13;
 }
 }
 else
 {
-uint8_t x_12; 
-x_12 = 1;
-return x_12;
+uint8_t x_14; 
+x_14 = 1;
+return x_14;
+}
+}
+else
+{
+uint8_t x_15; 
+x_15 = 1;
+return x_15;
+}
+}
+else
+{
+uint8_t x_16; 
+x_16 = 1;
+return x_16;
+}
+}
+else
+{
+uint8_t x_17; 
+x_17 = 1;
+return x_17;
+}
+}
+else
+{
+uint8_t x_18; 
+x_18 = 1;
+return x_18;
 }
 }
 }
diff --git a/src/util/name.cpp b/src/util/name.cpp
index c85fa7fafe..9f8d3257a9 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -106,7 +106,7 @@ bool is_id_first(unsigned char const * begin, unsigned char const * end) {
 }
 
 bool is_id_rest(unsigned char const * begin, unsigned char const * end) {
-    if (std::isalnum(*begin) || *begin == '_' || *begin == '\'')
+    if (std::isalnum(*begin) || *begin == '_' || *begin == '\'' || *begin == '?' || *begin == '!')
         return true;
     unsigned u = utf8_to_unicode(begin, end);
     return is_letter_like_unicode(u) || is_sub_script_alnum_unicode(u);