From c49f6f78732dc00587c119af41cd59966221dd33 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 1 Jun 2017 18:22:58 +0200
Subject: [PATCH] refactor(frontends/lean/user_notation): use parser instead of
 tactic monad

---
 src/frontends/lean/user_notation.cpp | 17 +++++++----------
 tests/lean/user_notation.lean        |  7 ++++---
 2 files changed, 11 insertions(+), 13 deletions(-)

diff --git a/src/frontends/lean/user_notation.cpp b/src/frontends/lean/user_notation.cpp
index 76710892fa..33d672dae8 100644
--- a/src/frontends/lean/user_notation.cpp
+++ b/src/frontends/lean/user_notation.cpp
@@ -46,24 +46,21 @@ static environment add_user_notation(environment const & env, name const & d, un
     return add_notation(env, notation_entry(is_nud, {notation::transition(tk, notation::mk_ext_action(
             [=](parser & p, unsigned num, expr const * args, pos_info const &) -> expr {
                 lean_assert(num == (is_nud ? 0 : 1));
-                expr tactic = mk_constant(d);
+                expr parser = mk_constant(d);
                 if (!is_nud)
-                    tactic = mk_app(tactic, mk_pexpr_quote(args[0]));
+                    parser = mk_app(parser, mk_pexpr_quote(args[0]));
                 // `parse (tk c)` arg
-                tactic = mk_app(tactic, mk_constant(get_unit_star_name()));
+                parser = mk_app(parser, mk_constant(get_unit_star_name()));
                 for (expr t = type; is_pi(t); t = binding_body(t)) {
                     expr arg_type = binding_domain(t);
                     if (is_app_of(arg_type, get_interactive_parse_name())) {
-                        tactic = mk_app(tactic, parse_interactive_param(p, arg_type));
+                        parser = mk_app(parser, parse_interactive_param(p, arg_type));
                     } else {
-                        tactic = mk_app(tactic, p.parse_expr(get_max_prec()));
+                        parser = mk_app(parser, p.parse_expr(get_max_prec()));
                     }
                 }
-                tactic = p.elaborate("_user_notation", {}, tactic).first;
-                tactic_state s = mk_tactic_state_for(p.env(), p.get_options(), "_user_notation", local_context(), dummy);
-                type_context ctx(p.env());
-                auto result = tactic::evaluator(ctx, p.get_options())(tactic, s);
-                return to_expr(tactic::get_result_value(result));
+                parser = p.elaborate("_user_notation", {}, parser).first;
+                return to_expr(run_parser(p, parser));
             }))}, Var(0), /* overload */ persistent, prio, notation_entry_group::Main, /* parse_only */ true));
 }
 
diff --git a/tests/lean/user_notation.lean b/tests/lean/user_notation.lean
index 95b26cd0db..f86c40d23b 100644
--- a/tests/lean/user_notation.lean
+++ b/tests/lean/user_notation.lean
@@ -1,11 +1,12 @@
+open lean (parser)
 open lean.parser
 open interactive
 open tactic
 
 reserve prefix `unquote! `:100
 @[user_notation]
-to_expr e >>= eval_expr pexpr
 meta def unquote_macro (_ : parse $ tk "unquote!") (e : parse lean.parser.pexpr) : parser pexpr :=
+↑(to_expr e >>= eval_expr pexpr)
 
 #eval unquote! ``(1 + 1)
 
@@ -19,17 +20,17 @@ private meta def parse_format : string → string → ℕ × pexpr
 
 reserve prefix `format! `:100
 @[user_notation]
-meta def format_macro (_ : parse $ tk "format!") (s : string) : tactic pexpr :=
 let (n, f) := parse_format "" s.reverse in
 pure $ n.repeat (λ _ e, expr.lam `_ binder_info.default pexpr.mk_placeholder e) f
+meta def format_macro (_ : parse $ tk "format!") (s : string) : parser pexpr :=
 
 #eval format! "a{}c" "b"
 -- #eval format! "{} {}" "a" "bla" -- TODO: delayed abstractions issue
 
 reserve infix ` +⋯+ `:65
 @[user_notation]
-do n₁ ← to_expr e₁ >>= eval_expr nat,
 meta def upto_notation (e₁ : parse lean.parser.pexpr) (_ : parse $ tk "+⋯+") (n₂ : ℕ) : parser pexpr :=
+do n₁ ← ↑(to_expr e₁ >>= eval_expr nat),
    pure $ (n₂+1-n₁).repeat (λ i e, ``(%%e + %%(reflect $ n₁ + i))) ``(0)
 
 #check 1 +⋯+ 10