From 1be72f1faa4bfa2f472f01d9dda08acd7d64442a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 28 Apr 2015 13:43:05 -0700
Subject: [PATCH] feat(frontends/lean): parse argument of unary tactis with
 rbp=0, tokens may have a different precedence in expression and tactic modes

---
 src/frontends/lean/notation_cmd.cpp  | 60 +++++++++++++++++++---------
 src/frontends/lean/parse_table.cpp   |  2 +-
 src/frontends/lean/parser.cpp        | 24 ++++++-----
 src/frontends/lean/parser.h          |  4 +-
 src/frontends/lean/parser_config.cpp | 18 ++++++---
 src/frontends/lean/parser_config.h   |  9 ++++-
 src/frontends/lean/pp.cpp            |  4 +-
 src/frontends/lean/token_table.cpp   | 48 ++++++++++++++--------
 src/frontends/lean/token_table.h     | 31 +++++++++-----
 src/tests/frontends/lean/scanner.cpp | 14 +++----
 tests/lean/run/tactic20.lean         |  2 -
 tests/lean/run/tactic31.lean         | 22 ++++++++++
 12 files changed, 164 insertions(+), 74 deletions(-)
 create mode 100644 tests/lean/run/tactic31.lean

diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index 978901842..5c9c6b7da 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -96,6 +96,28 @@ void check_not_forbidden(char const * tk) {
     }
 }
 
+static optional<unsigned> get_precedence(environment const & env, char const * tk, bool is_expr) {
+    if (is_expr)
+        return get_expr_precedence(get_token_table(env), tk);
+    else
+        return get_tactic_precedence(get_token_table(env), tk);
+}
+
+static optional<unsigned> get_precedence(environment const & env, char const * tk, notation_entry_group grp) {
+    return get_precedence(env, tk, grp != notation_entry_group::Tactic);
+}
+
+static token_entry mk_token_entry(std::string const & tk, unsigned prec, bool is_expr) {
+    if (is_expr)
+        return mk_expr_token_entry(tk, prec);
+    else
+        return mk_tactic_token_entry(tk, prec);
+}
+
+static token_entry mk_token_entry(std::string const & tk, unsigned prec, notation_entry_group grp) {
+    return mk_token_entry(tk, prec, grp != notation_entry_group::Tactic);
+}
+
 static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, notation_entry_group grp, bool parse_only)
 -> pair<notation_entry, optional<token_entry>> {
     std::string tk = parse_symbol(p, "invalid notation declaration, quoted symbol or identifier expected");
@@ -107,7 +129,7 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, nota
 
     optional<parse_table> reserved_pt;
     optional<action> reserved_action;
-    if (grp != notation_entry_group::Reserve) {
+    if (grp == notation_entry_group::Main) {
         if (k == mixfix_kind::prefix) {
             if (auto at = get_reserved_nud_table(p.env()).find(tks)) {
                 reserved_pt     = at->second;
@@ -134,18 +156,20 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, nota
 
     if (!prec) {
         if (reserved_action && k == mixfix_kind::prefix && reserved_action->kind() == notation::action_kind::Expr) {
+            lean_assert(grp == notation_entry_group::Main);
             prec = reserved_action->rbp();
         } else if (reserved_action && k == mixfix_kind::infixr && reserved_action->kind() == notation::action_kind::Expr) {
+            lean_assert(grp == notation_entry_group::Main);
             prec = reserved_action->rbp();
         } else {
-            prec = get_precedence(get_token_table(env), tk.c_str());
+            prec = get_precedence(env, tk.c_str(), grp);
             if (prec && k == mixfix_kind::infixr)
                 prec = *prec - 1;
         }
     } else {
-        auto old_prec = get_precedence(get_token_table(env), tk.c_str());
+        auto old_prec = get_precedence(env, tk.c_str(), grp);
         if (!old_prec || (k != mixfix_kind::prefix && old_prec != prec))
-            new_token = token_entry(tk.c_str(), *prec);
+            new_token = mk_token_entry(tk.c_str(), *prec, grp);
         if (k == mixfix_kind::infixr)
             prec = *prec - 1;
     }
@@ -231,7 +255,7 @@ static notation_entry parse_mixfix_notation(parser & p, mixfix_kind k, bool over
     return nt.first;
 }
 
-static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_tokens, bool & used_default) {
+static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_tokens, bool & used_default, notation_entry_group grp) {
     used_default = false;
     if (p.curr_is_quoted_symbol()) {
         environment const & env = p.env();
@@ -243,11 +267,11 @@ static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_t
         if (p.curr_is_token(get_colon_tk())) {
             p.next();
             unsigned prec = parse_precedence(p);
-            auto old_prec = get_precedence(get_token_table(env), tkcs);
+            auto old_prec = get_precedence(env, tkcs, grp);
             if (!old_prec || prec != *old_prec)
-                new_tokens.push_back(token_entry(tkcs, prec));
-        } else if (!get_precedence(get_token_table(env), tkcs)) {
-            new_tokens.push_back(token_entry(tkcs, LEAN_DEFAULT_PRECEDENCE));
+                new_tokens.push_back(mk_token_entry(tkcs, prec, grp));
+        } else if (!get_precedence(env, tkcs, grp)) {
+            new_tokens.push_back(mk_token_entry(tkcs, LEAN_DEFAULT_PRECEDENCE, grp));
             used_default = true;
         }
         return tk;
@@ -261,9 +285,9 @@ static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_t
     }
 }
 
-static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_tokens) {
+static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_tokens, notation_entry_group grp) {
     bool dummy;
-    return parse_quoted_symbol_or_token(p, new_tokens, dummy);
+    return parse_quoted_symbol_or_token(p, new_tokens, dummy, grp);
 }
 
 static expr parse_notation_expr(parser & p, buffer<expr> const & locals) {
@@ -293,7 +317,7 @@ static unsigned get_precedence(environment const & env, buffer<token_entry> cons
         if (e.m_token == token_str)
             return e.m_prec;
     }
-    auto prec = get_precedence(get_token_table(env), token_str.c_str());
+    auto prec = get_expr_precedence(get_token_table(env), token_str.c_str());
     if (prec)
         return *prec;
     else
@@ -301,7 +325,7 @@ static unsigned get_precedence(environment const & env, buffer<token_entry> cons
 }
 
 static action parse_action(parser & p, name const & prev_token, unsigned default_prec,
-                           buffer<expr> & locals, buffer<token_entry> & new_tokens) {
+                           buffer<expr> & locals, buffer<token_entry> & new_tokens, notation_entry_group grp) {
     if (p.curr_is_token(get_colon_tk())) {
         p.next();
         if (p.curr_is_numeral() || p.curr_is_token_or_id(get_max_tk())) {
@@ -323,7 +347,7 @@ static action parse_action(parser & p, name const & prev_token, unsigned default
                 bool is_fold_right = p.curr_is_token_or_id(get_foldr_tk());
                 p.next();
                 auto prec = parse_optional_precedence(p);
-                name sep  = parse_quoted_symbol_or_token(p, new_tokens);
+                name sep  = parse_quoted_symbol_or_token(p, new_tokens, grp);
                 expr rec;
                 {
                     parser::local_scope scope(p);
@@ -341,7 +365,7 @@ static action parse_action(parser & p, name const & prev_token, unsigned default
                     ini = parse_notation_expr(p, locals);
                 optional<name> terminator;
                 if (!p.curr_is_token(get_rparen_tk()))
-                    terminator = parse_quoted_symbol_or_token(p, new_tokens);
+                    terminator = parse_quoted_symbol_or_token(p, new_tokens, grp);
                 p.check_token_next(get_rparen_tk(), "invalid fold notation argument, ')' expected");
                 return mk_exprs_action(sep, rec, ini, terminator, is_fold_right, prec ? *prec : 0);
             } else if (p.curr_is_token_or_id(get_scoped_tk())) {
@@ -446,7 +470,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, notation_en
     bool used_default = false;
     while ((grp != notation_entry_group::Reserve && !p.curr_is_token(get_assign_tk())) ||
            (grp == notation_entry_group::Reserve && !p.curr_is_command() && !p.curr_is_eof())) {
-        name tk = parse_quoted_symbol_or_token(p, new_tokens, used_default);
+        name tk = parse_quoted_symbol_or_token(p, new_tokens, used_default, grp);
         if (auto at = find_next(reserved_pt, tk)) {
             action const & a = at->first;
             reserved_pt      = at->second;
@@ -499,7 +523,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, notation_en
                 unsigned default_prec = get_default_prec(pt, tk);
                 name n   = p.get_name_val();
                 p.next();
-                action a = parse_action(p, tk, default_prec, locals, new_tokens);
+                action a = parse_action(p, tk, default_prec, locals, new_tokens, grp);
                 expr local_type = mk_Prop(); // type used in notation local declarations, it is irrelevant
                 expr l = mk_local(n, local_type);
                 p.add_local(l);
@@ -606,7 +630,7 @@ static environment add_user_token(environment const & env, token_entry const & e
 
 static environment add_user_token(environment const & env, char const * val, unsigned prec) {
     check_token(val);
-    return add_token(env, val, prec);
+    return add_expr_token(env, val, prec);
 }
 
 struct notation_modifiers {
diff --git a/src/frontends/lean/parse_table.cpp b/src/frontends/lean/parse_table.cpp
index 2d5b76755..44c60d569 100644
--- a/src/frontends/lean/parse_table.cpp
+++ b/src/frontends/lean/parse_table.cpp
@@ -488,7 +488,7 @@ void display(io_state_stream & out, unsigned num, transition const * ts, list<ex
         if (i > 0) out << " ";
         out << "`" << ts[i].get_token() << "`";
         if (tt) {
-            if (auto prec = get_precedence(*tt, ts[i].get_token().to_string().c_str())) {
+            if (auto prec = get_expr_precedence(*tt, ts[i].get_token().to_string().c_str())) {
                 out << ":" << *prec;
             }
         }
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 972566d00..e0cbb1e4f 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1282,10 +1282,13 @@ expr parser::parse_led(expr left) {
     }
 }
 
-unsigned parser::curr_lbp() const {
+unsigned parser::curr_lbp_core(bool as_tactic) const {
     switch (curr()) {
     case scanner::token_kind::Keyword:
-        return get_token_info().precedence();
+        if (as_tactic)
+            return get_token_info().tactic_precedence();
+        else
+            return get_token_info().expr_precedence();
     case scanner::token_kind::CommandKeyword: case scanner::token_kind::Eof:
     case scanner::token_kind::ScriptBlock:    case scanner::token_kind::QuotedSymbol:
         return 0;
@@ -1298,7 +1301,7 @@ unsigned parser::curr_lbp() const {
 
 expr parser::parse_expr(unsigned rbp) {
     expr left = parse_nud();
-    while (rbp < curr_lbp()) {
+    while (rbp < curr_expr_lbp()) {
         left = parse_led(left);
     }
     return left;
@@ -1314,7 +1317,7 @@ pair<optional<name>, expr> parser::parse_id_tk_expr(name const & tk, unsigned rb
             return mk_pair(optional<name>(id), parse_expr(rbp));
         } else {
             expr left = id_to_expr(id, id_pos);
-            while (rbp < curr_lbp()) {
+            while (rbp < curr_expr_lbp()) {
                 left = parse_led(left);
             }
             return mk_pair(optional<name>(), left);
@@ -1448,8 +1451,9 @@ expr parser::parse_tactic_nud() {
         name id = get_name_val();
         if (optional<expr> tac_type = is_tactic_command(id)) {
             next();
-            expr type = *tac_type;
-            expr r = save_pos(mk_constant(id), id_pos);
+            expr type  = *tac_type;
+            bool unary = get_arity(type) == 1;
+            expr r     = save_pos(mk_constant(id), id_pos);
             while (is_pi(type)) {
                 expr d = binding_domain(type);
                 if (is_tactic_type(d)) {
@@ -1459,13 +1463,15 @@ expr parser::parse_tactic_nud() {
                 } else if (is_tactic_opt_expr_list_type(d)) {
                     r = mk_app(r, parse_tactic_opt_expr_list(), id_pos);
                 } else if (is_tactic_identifier_type(d)) {
-                    r = mk_app(r, mk_local(check_id_next("invalid tactic, identifier expected"), mk_expr_placeholder()), id_pos);
+                    r = mk_app(r, mk_local(check_id_next("invalid tactic, identifier expected"),
+                                           mk_expr_placeholder()), id_pos);
                 } else if (is_tactic_identifier_list_type(d)) {
                     r = mk_app(r, parse_tactic_id_list(), id_pos);
                 } else if (is_tactic_opt_identifier_list_type(d)) {
                     r = mk_app(r, parse_tactic_opt_id_list(), id_pos);
                 } else {
-                    r = mk_app(r, parse_expr(get_max_prec()), id_pos);
+                    unsigned prec = unary ? 1 : get_max_prec();
+                    r = mk_app(r, parse_expr(prec), id_pos);
                 }
                 type = binding_body(type);
             }
@@ -1490,7 +1496,7 @@ expr parser::parse_tactic_led(expr left) {
 
 expr parser::parse_tactic(unsigned rbp) {
     expr left = parse_tactic_nud();
-    while (rbp < curr_lbp()) {
+    while (rbp < curr_tactic_lbp()) {
         left = parse_tactic_led(left);
     }
     return left;
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index a882f4416..bff98d079 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -182,7 +182,9 @@ class parser {
     void parse_command();
     void parse_script(bool as_expr = false);
     bool parse_commands();
-    unsigned curr_lbp() const;
+    unsigned curr_lbp_core(bool as_tactic) const;
+    unsigned curr_expr_lbp() const { return curr_lbp_core(false); }
+    unsigned curr_tactic_lbp() const { return curr_lbp_core(true); }
     expr parse_notation_core(parse_table t, expr * left, bool as_tactic);
     expr parse_expr_or_tactic(unsigned rbp, bool as_tactic) {
         return as_tactic ? parse_tactic(rbp) : parse_expr(rbp);
diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp
index 491530372..7c7474662 100644
--- a/src/frontends/lean/parser_config.cpp
+++ b/src/frontends/lean/parser_config.cpp
@@ -83,7 +83,10 @@ struct token_config {
     static std::string * g_key;
 
     static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
-        s.m_table = add_token(s.m_table, e.m_token.c_str(), e.m_prec);
+        if (e.m_expr)
+            s.m_table = add_token(s.m_table, e.m_token.c_str(), e.m_prec);
+        else
+            s.m_table = add_tactic_token(s.m_table, e.m_token.c_str(), e.m_prec);
     }
     static name const & get_class_name() {
         return *g_class_name;
@@ -92,12 +95,13 @@ struct token_config {
         return *g_key;
     }
     static void  write_entry(serializer & s, entry const & e) {
-        s << e.m_token.c_str() << e.m_prec;
+        s << e.m_expr << e.m_token.c_str() << e.m_prec;
     }
     static entry read_entry(deserializer & d) {
+        bool is_expr   = d.read_bool();
         std::string tk = d.read_string();
         unsigned prec  = d.read_unsigned();
-        return entry(tk, prec);
+        return entry(is_expr, tk, prec);
     }
     static optional<unsigned> get_fingerprint(entry const &) {
         return optional<unsigned>();
@@ -113,8 +117,12 @@ environment add_token(environment const & env, token_entry const & e, bool persi
     return token_ext::add_entry(env, get_dummy_ios(), e, persistent);
 }
 
-environment add_token(environment const & env, char const * val, unsigned prec) {
-    return add_token(env, token_entry(val, prec));
+environment add_expr_token(environment const & env, char const * val, unsigned prec) {
+    return add_token(env, token_entry(true, val, prec));
+}
+
+environment add_tactic_token(environment const & env, char const * val, unsigned prec) {
+    return add_token(env, token_entry(false, val, prec));
 }
 
 token_table const & get_token_table(environment const & env) {
diff --git a/src/frontends/lean/parser_config.h b/src/frontends/lean/parser_config.h
index 6c3d43f6e..574cfa030 100644
--- a/src/frontends/lean/parser_config.h
+++ b/src/frontends/lean/parser_config.h
@@ -13,10 +13,13 @@ Author: Leonardo de Moura
 
 namespace lean {
 struct token_entry {
+    bool        m_expr; // true if it precedence for an expression token
     std::string m_token;
     unsigned    m_prec;
-    token_entry(std::string const & tk, unsigned prec):m_token(tk), m_prec(prec) {}
+    token_entry(bool e, std::string const & tk, unsigned prec):m_expr(e), m_token(tk), m_prec(prec) {}
 };
+inline token_entry mk_expr_token_entry(std::string const & tk, unsigned prec) { return token_entry(true, tk, prec); }
+inline token_entry mk_tactic_token_entry(std::string const & tk, unsigned prec) { return token_entry(false, tk, prec); }
 
 enum class notation_entry_kind { NuD, LeD, Numeral };
 enum class notation_entry_group { Main, Reserve, Tactic };
@@ -62,7 +65,9 @@ notation_entry replace(notation_entry const & e, std::function<expr(expr const &
 environment add_token(environment const & env, token_entry const & e, bool persistent = true);
 environment add_notation(environment const & env, notation_entry const & e, bool persistent = true);
 
-environment add_token(environment const & env, char const * val, unsigned prec);
+environment add_expr_token(environment const & env, char const * val, unsigned prec);
+environment add_tactic_token(environment const & env, char const * val, unsigned prec);
+
 environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a,
                              bool overload = true, notation_entry_group g = notation_entry_group::Main, bool parse_only = false);
 environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a,
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index f2a0fa5d1..ab28beb5c 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -845,10 +845,10 @@ bool pretty_fn::match(expr const & p, expr const & e, buffer<optional<expr>> & a
 
 static unsigned get_some_precedence(token_table const & t, name const & tk) {
     if (tk.is_atomic() && tk.is_string()) {
-        if (auto p = get_precedence(t, tk.get_string()))
+        if (auto p = get_expr_precedence(t, tk.get_string()))
             return *p;
     } else {
-        if (auto p = get_precedence(t, tk.to_string().c_str()))
+        if (auto p = get_expr_precedence(t, tk.to_string().c_str()))
             return *p;
     }
     return 0;
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 58e23d180..50245cc87 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -20,6 +20,20 @@ unsigned get_max_prec() { return g_max_prec; }
 unsigned get_Max_prec() { return g_Max_prec; }
 unsigned get_arrow_prec() { return g_arrow_prec; }
 unsigned get_decreasing_prec() { return g_decreasing_prec; }
+static token_table update(token_table const & s, char const * token, char const * val,
+                          optional<unsigned> expr_prec, optional<unsigned> tac_prec) {
+    lean_assert(expr_prec || tac_prec);
+    token_info info(token, val, 0, 0);
+    if (token_info const * old_info = find(s, token)) {
+        info = info.update_expr_precedence(old_info->expr_precedence());
+        info = info.update_tactic_precedence(old_info->tactic_precedence());
+    }
+    if (expr_prec)
+        info = info.update_expr_precedence(*expr_prec);
+    if (tac_prec)
+        info = info.update_tactic_precedence(*tac_prec);
+    return insert(s, token, info);
+}
 token_table add_command_token(token_table const & s, char const * token) {
     return insert(s, token, token_info(token));
 }
@@ -27,10 +41,16 @@ token_table add_command_token(token_table const & s, char const * token, char co
     return insert(s, token, token_info(token, val));
 }
 token_table add_token(token_table const & s, char const * token, unsigned prec) {
-    return insert(s, token, token_info(token, prec));
+    return update(s, token, token, optional<unsigned>(prec), optional<unsigned>());
 }
 token_table add_token(token_table const & s, char const * token, char const * val, unsigned prec) {
-    return insert(s, token, token_info(token, val, prec));
+    return update(s, token, val, optional<unsigned>(prec), optional<unsigned>());
+}
+token_table add_tactic_token(token_table const & s, char const * token, unsigned prec) {
+    return update(s, token, token, optional<unsigned>(), optional<unsigned>(prec));
+}
+token_table add_tactic_token(token_table const & s, char const * token, char const * val, unsigned prec) {
+    return update(s, token, val, optional<unsigned>(), optional<unsigned>(prec));
 }
 token_table const * find(token_table const & s, char c) {
     return s.find(c);
@@ -38,9 +58,13 @@ token_table const * find(token_table const & s, char c) {
 token_info const * value_of(token_table const & s) {
     return s.value();
 }
-optional<unsigned> get_precedence(token_table const & s, char const * token) {
+optional<unsigned> get_expr_precedence(token_table const & s, char const * token) {
     auto it = find(s, token);
-    return it ? optional<unsigned>(it->precedence()) : optional<unsigned>();
+    return it ? optional<unsigned>(it->expr_precedence()) : optional<unsigned>();
+}
+optional<unsigned> get_tactic_precedence(token_table const & s, char const * token) {
+    auto it = find(s, token);
+    return it ? optional<unsigned>(it->tactic_precedence()) : optional<unsigned>();
 }
 bool is_token(token_table const & s, char const * token) {
     return static_cast<bool>(find(s, token));
@@ -53,16 +77,6 @@ void for_each(token_table const & s, std::function<void(char const *, token_info
             fn(str.data(), info);
         });
 }
-void display(std::ostream & out, token_table const & s) {
-    for_each(s, [&](char const * token, token_info const & info) {
-            out << "`" << token << "`:" << info.precedence();
-            if (info.is_command())
-                out << " [command]";
-            if (info.value() != info.token())
-                out << " " << info.value();
-            out << "\n";
-        });
-}
 
 static char const * g_lambda_unicode     = "\u03BB";
 static char const * g_pi_unicode         = "\u03A0";
@@ -79,7 +93,7 @@ void init_token_table(token_table & t) {
          {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec},
          {"{|", g_max_prec}, {"|}", 0}, {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
-         {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0},  {"with", 0}, {"...", 0}, {",", 0}, {";", 1},
+         {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0},  {"with", 0}, {"...", 0}, {",", 0},
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"esimp", 0}, {"fold", 0}, {"unfold", 0},
          {":=", 0}, {"--", 0}, {"#", 0},
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec},
@@ -197,7 +211,7 @@ static int value_of(lua_State * L) {
     if (it) {
         push_boolean(L, it->is_command());
         push_name(L, it->value());
-        push_integer(L, it->precedence());
+        push_integer(L, it->expr_precedence());
         return 3;
     } else {
         push_nil(L);
@@ -212,7 +226,7 @@ static int for_each(lua_State * L) {
             lua_pushstring(L, k);
             lua_pushboolean(L, info.is_command());
             push_name(L, info.value());
-            lua_pushinteger(L, info.precedence());
+            lua_pushinteger(L, info.expr_precedence());
             pcall(L, 4, 0, 0);
         });
     return 0;
diff --git a/src/frontends/lean/token_table.h b/src/frontends/lean/token_table.h
index c32928bf1..cbcb2a7e2 100644
--- a/src/frontends/lean/token_table.h
+++ b/src/frontends/lean/token_table.h
@@ -26,21 +26,30 @@ class token_info {
     bool        m_command;
     name        m_token;
     name        m_value;
-    unsigned    m_precedence;
+    unsigned    m_expr_precedence;
+    unsigned    m_tactic_precedence;
+    token_info(bool c, name const & t, name const & v, unsigned ep, unsigned tp):
+        m_command(c), m_token(t), m_value(v), m_expr_precedence(ep), m_tactic_precedence(tp) {}
 public:
     token_info():m_command(true) {}
     token_info(char const * val):
-        m_command(true), m_token(val), m_value(val), m_precedence(LEAN_DEFAULT_PRECEDENCE) {}
+        m_command(true), m_token(val), m_value(val), m_expr_precedence(0), m_tactic_precedence(0) {}
     token_info(char const * token, char const * val):
-        m_command(true), m_token(token), m_value(val), m_precedence(LEAN_DEFAULT_PRECEDENCE) {}
-    token_info(char const * val, unsigned prec):
-        m_command(false), m_token(val), m_value(val), m_precedence(prec) {}
-    token_info(char const * token, char const * val, unsigned prec):
-        m_command(false), m_token(token), m_value(val), m_precedence(prec) {}
+        m_command(true), m_token(token), m_value(val), m_expr_precedence(0), m_tactic_precedence(0) {}
+    token_info(char const * token, char const * val, unsigned prec, unsigned tac_prec):
+        m_command(false), m_token(token), m_value(val),
+        m_expr_precedence(prec), m_tactic_precedence(tac_prec) {}
     bool is_command() const { return m_command; }
     name const & token() const { return m_token; }
     name const & value() const { return m_value; }
-    unsigned precedence() const { return m_precedence; }
+    unsigned expr_precedence() const { return m_expr_precedence; }
+    unsigned tactic_precedence() const { return m_tactic_precedence; }
+    token_info update_expr_precedence(unsigned prec) const {
+        return token_info(m_command, m_token, m_value, prec, m_tactic_precedence);
+    }
+    token_info update_tactic_precedence(unsigned prec) const {
+        return token_info(m_command, m_token, m_value, m_expr_precedence, prec);
+    }
 };
 
 typedef ctrie<token_info> token_table;
@@ -50,10 +59,12 @@ token_table add_command_token(token_table const & s, char const * token);
 token_table add_command_token(token_table const & s, char const * token, char const * val);
 token_table add_token(token_table const & s, char const * token, unsigned prec = LEAN_DEFAULT_PRECEDENCE);
 token_table add_token(token_table const & s, char const * token, char const * val, unsigned prec = LEAN_DEFAULT_PRECEDENCE);
+token_table add_tactic_token(token_table const & s, char const * token, unsigned prec = LEAN_DEFAULT_PRECEDENCE);
+token_table add_tactic_token(token_table const & s, char const * token, char const * val, unsigned prec = LEAN_DEFAULT_PRECEDENCE);
 void for_each(token_table const & s, std::function<void(char const *, token_info const&)> const & fn);
-void display(std::ostream & out, token_table const & s);
 token_table const * find(token_table const & s, char c);
-optional<unsigned> get_precedence(token_table const & s, char const * token);
+optional<unsigned> get_expr_precedence(token_table const & s, char const * token);
+optional<unsigned> get_tactic_precedence(token_table const & s, char const * token);
 bool is_token(token_table const & s, char const * token);
 token_info const * value_of(token_table const & s);
 void open_token_table(lua_State * L);
diff --git a/src/tests/frontends/lean/scanner.cpp b/src/tests/frontends/lean/scanner.cpp
index 834923beb..e86368a65 100644
--- a/src/tests/frontends/lean/scanner.cpp
+++ b/src/tests/frontends/lean/scanner.cpp
@@ -99,13 +99,13 @@ static void check_keyword(char const * str, name const & expected, environment c
 static void tst1() {
     environment env;
     token_table s = get_token_table(env);
-    env = add_token(env, "+", 0);
-    env = add_token(env, "=", 0);
+    env = add_expr_token(env, "+", 0);
+    env = add_expr_token(env, "=", 0);
     scan_success("a..a");
     check("a..a", {tk::Identifier, tk::Keyword, tk::Keyword, tk::Identifier});
     check("Type.{0}", {tk::Keyword, tk::Keyword, tk::Numeral, tk::Keyword});
-    env = add_token(env, "ab+cde", 0);
-    env = add_token(env, "+cd", 0);
+    env = add_expr_token(env, "ab+cde", 0);
+    env = add_expr_token(env, "+cd", 0);
     scan_success("ab+cd", env);
     check("ab+cd", {tk::Identifier, tk::Keyword}, env);
     scan_success("ab+cde", env);
@@ -139,9 +139,9 @@ static void tst2() {
     scan_error("***");
     environment env;
     token_table s = mk_default_token_table();
-    env = add_token(env, "***", 0);
+    env = add_expr_token(env, "***", 0);
     check_keyword("***", "***", env);
-    env = add_token(env, "+", 0);
+    env = add_expr_token(env, "+", 0);
     check("x+y", {tk::Identifier, tk::Keyword, tk::Identifier}, env);
     check("-- testing", {});
     check("/- testing -/", {});
@@ -152,7 +152,7 @@ static void tst2() {
     check("int -> int", {tk::Identifier, tk::Keyword, tk::Identifier});
     check("int->int", {tk::Identifier, tk::Keyword, tk::Identifier});
     check_keyword("->", "->");
-    env = add_token(env, "-+->", 0);
+    env = add_expr_token(env, "-+->", 0);
     check("Int -+-> Int", {tk::Identifier, tk::Keyword, tk::Identifier}, env);
     check("x := 10", {tk::Identifier, tk::Keyword, tk::Numeral});
     check("{x}", {tk::Keyword, tk::Identifier, tk::Keyword});
diff --git a/tests/lean/run/tactic20.lean b/tests/lean/run/tactic20.lean
index c509a25d2..9f7e5ac0a 100644
--- a/tests/lean/run/tactic20.lean
+++ b/tests/lean/run/tactic20.lean
@@ -1,8 +1,6 @@
 import logic
 open tactic
 
-infixl `;`:15 := tactic.and_then
-
 definition assump := eassumption
 
 theorem tst {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
diff --git a/tests/lean/run/tactic31.lean b/tests/lean/run/tactic31.lean
new file mode 100644
index 000000000..3cbc4b40b
--- /dev/null
+++ b/tests/lean/run/tactic31.lean
@@ -0,0 +1,22 @@
+import data.nat
+
+example (a b c : Prop) : a → b → c → a ∧ b ∧ c :=
+begin
+  intro Ha, intro Hb, intro Hc,
+  apply and.intro Ha,
+  apply and.intro Hb Hc
+end
+
+example (a b c : Prop) : a → b → c → a ∧ b ∧ c :=
+by intro Ha; intro Hb; intro Hc; apply and.intro Ha; apply and.intro Hb Hc
+
+open nat
+
+example (a b c : nat) : a = b → b = 0 + c → a = c + 0:=
+begin
+  intro ab, intro bc,
+  change a = c,
+  rewrite zero_add at bc,
+  rewrite -bc,
+  exact ab
+end