From dfe1874365693367ae0b0c5161a772fc2de61d87 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 23 Feb 2017 00:58:56 +0100
Subject: [PATCH] refactor(frontends/lean/{parser,util}): extract `quote`
 functions

Also fixes ``f when f is private
---
 src/frontends/lean/builtin_exprs.cpp |  2 +-
 src/frontends/lean/parser.cpp        | 22 +---------------------
 src/frontends/lean/util.cpp          | 28 +++++++++++++++++++---------
 src/frontends/lean/util.h            |  4 +++-
 tests/lean/run/quote1.lean           |  3 +++
 5 files changed, 27 insertions(+), 32 deletions(-)

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 3aa599a79d..f4cc8c364d 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -682,7 +682,7 @@ static expr parse_quoted_name(parser_state & p, unsigned, expr const *, pos_info
         }
     }
     lean_assert(id.is_string());
-    expr e  = quote_name(id);
+    expr e  = quote(id);
     return p.rec_save_pos(e, pos);
 }
 
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 168a07c3a5..fa5680f8a2 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1000,7 +1000,7 @@ static expr mk_opt_param(expr const & t, expr const & val) {
 }
 
 static expr mk_auto_param(expr const & t, name const & tac_name) {
-    return copy_tag(t, mk_app(copy_tag(t, mk_constant(get_auto_param_name())), t, quote_name(tac_name)));
+    return copy_tag(t, mk_app(copy_tag(t, mk_constant(get_auto_param_name())), t, quote(tac_name)));
 }
 
 static bool is_tactic_unit(environment const & env, expr const & c) {
@@ -1715,26 +1715,6 @@ struct to_pattern_fn {
     }
 };
 
-static expr quote(unsigned u) {
-    return mk_app(mk_constant(get_char_of_nat_name()), mk_prenum(mpz(u)));
-}
-
-static expr quote(char const * str) {
-    return from_string(str);
-}
-
-static expr quote(name const & n) {
-    switch (n.kind()) {
-        case name_kind::ANONYMOUS:
-            return mk_constant({"name", "anonymous"});
-        case name_kind::NUMERAL:
-            return mk_app(mk_constant({"name", "mk_numeral"}), quote(n.get_numeral()), quote(n.get_prefix()));
-        case name_kind::STRING:
-            return mk_app(mk_constant({"name", "mk_string"}), quote(n.get_string()), quote(n.get_prefix()));
-    }
-    lean_unreachable();
-}
-
 static expr quote(expr const & e) {
     switch (e.kind()) {
         case expr_kind::Var:
diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index 78ba639e79..a2c3926530 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -31,6 +31,8 @@ Author: Leonardo de Moura
 #include "frontends/lean/parser.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/decl_util.h" // TODO(Leo): remove
+#include "frontends/lean/prenum.h"
+
 namespace lean {
 void consume_until_end_or_command(parser & p) {
     while (!p.curr_is_command() && !p.curr_is_eof() && !p.curr_is_token(get_period_tk())) {
@@ -341,16 +343,24 @@ expr mk_tactic_unit() {
     return mk_app(mk_constant(get_tactic_name(), {mk_level_zero()}), mk_constant(get_unit_name()));
 }
 
-expr quote_name(name const & n) {
-    if (n.is_anonymous()) {
-        return mk_constant(get_name_anonymous_name());
-    } else if (n.is_string()) {
-        expr prefix = quote_name(n.get_prefix());
-        expr str    = from_string(n.get_string());
-        return mk_app(mk_constant(get_name_mk_string_name()), str, prefix);
-    } else {
-        lean_unreachable();
+expr quote(unsigned u) {
+    return mk_app(mk_constant(get_char_of_nat_name()), mk_prenum(mpz(u)));
+}
+
+expr quote(char const * str) {
+    return from_string(str);
+}
+
+expr quote(name const & n) {
+    switch (n.kind()) {
+        case name_kind::ANONYMOUS:
+            return mk_constant(get_name_anonymous_name());
+        case name_kind::NUMERAL:
+            return mk_app(mk_constant(get_name_mk_numeral_name()), quote(n.get_numeral()), quote(n.get_prefix()));
+        case name_kind::STRING:
+            return mk_app(mk_constant(get_name_mk_string_name()), quote(n.get_string()), quote(n.get_prefix()));
     }
+    lean_unreachable();
 }
 
 static name * g_no_info = nullptr;
diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h
index 9f7c4961fc..1da7ecff5e 100644
--- a/src/frontends/lean/util.h
+++ b/src/frontends/lean/util.h
@@ -106,7 +106,9 @@ pair<name, option_kind> parse_option_name(parser & p, char const * error_msg);
 /** Create (tactic unit) type */
 expr mk_tactic_unit();
 
-expr quote_name(name const & n);
+expr quote(unsigned u);
+expr quote(char const * str);
+expr quote(name const & n);
 
 expr mk_no_info(expr const & e);
 bool is_no_info(expr const & e);
diff --git a/tests/lean/run/quote1.lean b/tests/lean/run/quote1.lean
index b01ad8f587..e4b633f552 100644
--- a/tests/lean/run/quote1.lean
+++ b/tests/lean/run/quote1.lean
@@ -11,3 +11,6 @@ by do
    trace t2,
    r ← mk_app (`eq.refl) [a],
    exact r
+
+private def f := unit
+check ``f