From a1006073d44b92277b8dcd56fb262f33383bffa6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 19 Oct 2014 13:39:06 -0700
Subject: [PATCH] feat(frontends/lean/notation_cmd): do not allow user to
 define new tokes containing '(', ')', ',' or change their precedence

---
 src/frontends/lean/notation_cmd.cpp    | 43 ++++++++++++++++++++++++--
 tests/lean/notation5.lean              | 11 +++++++
 tests/lean/notation5.lean.expected.out |  5 +++
 3 files changed, 56 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/notation5.lean
 create mode 100644 tests/lean/notation5.lean.expected.out

diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index 0681e87d4..d4c19699e 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <limits>
 #include <string>
 #include "util/sstream.h"
+#include "util/utf8.h"
 #include "kernel/abstract.h"
 #include "kernel/replace_fn.h"
 #include "library/scoped_ext.h"
@@ -356,13 +357,49 @@ notation_entry parse_notation(parser & p, bool overload, buffer<token_entry> & n
     }
 }
 
+static char g_reserved_chars[] = {'(', ')', ',', 0};
+
+static void check_token(char const * tk) {
+    while (tk && *tk) {
+        unsigned sz = get_utf8_size(*tk);
+        if (sz == 0) {
+            throw exception(sstream() << "invalid token `" << tk << "`, contains invalid utf-8 character");
+        } else if (sz > 1) {
+            // multi-size unicode character
+            for (unsigned i = 0; i < sz; i++) {
+                if (!*tk)
+                    throw exception(sstream() << "invalid token `" << tk << "`, contains invalid utf-8 character");
+                ++tk;
+            }
+        } else {
+            auto it = g_reserved_chars;
+            while (*it) {
+                if (*tk == *it)
+                    throw exception(sstream() << "invalid token `" << tk << "`, it contains reserved character `" << *it << "`");
+                ++it;
+            }
+            ++tk;
+        }
+    }
+}
+
+static environment add_user_token(environment const & env, token_entry const & e) {
+    check_token(e.m_token.c_str());
+    return add_token(env, e);
+}
+
+static environment add_user_token(environment const & env, char const * val, unsigned prec) {
+    check_token(val);
+    return add_token(env, val, prec);
+}
+
 static environment notation_cmd_core(parser & p, bool overload) {
     flet<bool> set_allow_local(g_allow_local, in_context(p.env()));
     environment env = p.env();
     buffer<token_entry> new_tokens;
     auto ne = parse_notation_core(p, overload, new_tokens);
     for (auto const & te : new_tokens)
-        env = add_token(env, te);
+        env = add_user_token(env, te);
     env = add_notation(env, ne);
     return env;
 }
@@ -371,7 +408,7 @@ static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload) {
     auto nt = parse_mixfix_notation(p, k, overload);
     environment env = p.env();
     if (nt.second)
-        env = add_token(env, *nt.second);
+        env = add_user_token(env, *nt.second);
     env = add_notation(env, nt.first);
     return env;
 }
@@ -389,7 +426,7 @@ static environment precedence_cmd(parser & p) {
     std::string tk = parse_symbol(p, "invalid precedence declaration, quoted symbol or identifier expected");
     p.check_token_next(get_colon_tk(), "invalid precedence declaration, ':' expected");
     unsigned prec = parse_precedence(p, "invalid precedence declaration, numeral or 'max' expected");
-    return add_token(p.env(), tk.c_str(), prec);
+    return add_user_token(p.env(), tk.c_str(), prec);
 }
 
 void register_notation_cmds(cmd_table & r) {
diff --git a/tests/lean/notation5.lean b/tests/lean/notation5.lean
new file mode 100644
index 000000000..59646ea79
--- /dev/null
+++ b/tests/lean/notation5.lean
@@ -0,0 +1,11 @@
+import data.num
+
+notation `((` := 1
+
+precedence `(` : 30
+
+notation `))` := 1
+
+notation `,,` := 1
+
+precedence `,` : 10
diff --git a/tests/lean/notation5.lean.expected.out b/tests/lean/notation5.lean.expected.out
new file mode 100644
index 000000000..9234397c5
--- /dev/null
+++ b/tests/lean/notation5.lean.expected.out
@@ -0,0 +1,5 @@
+notation5.lean:3:0: error: invalid token `((`, it contains reserved character `(`
+notation5.lean:5:0: error: invalid token `(`, it contains reserved character `(`
+notation5.lean:7:0: error: invalid token `))`, it contains reserved character `)`
+notation5.lean:9:0: error: invalid token `,,`, it contains reserved character `,`
+notation5.lean:11:0: error: invalid token `,`, it contains reserved character `,`