feat(frontends/lean): parse rewrite tactic

hott/init/reserved_notation.hlean

@@ -56,6 +56,7 @@ reserve infixl `-`:65
 reserve infixl `*`:70
 reserve infixl `div`:70
 reserve infixl `mod`:70
+reserve infixl `/`:70
 reserve prefix `-`:100
 
 reserve infix `<=`:50

hott/init/tactic.hlean

@@ -62,6 +62,9 @@ opaque definition unfold     (e : expr)   : tactic := builtin
 opaque definition exact      (e : expr)   : tactic := builtin
 opaque definition trace      (s : string) : tactic := builtin
 opaque definition inversion  (id : expr)  : tactic := builtin
+-- rewrite_tac is just a marker for the builtin 'rewrite' notation
+-- used to create instances of this tactic.
+opaque definition rewrite_tac (e : expr)  : tactic := builtin
 
 notation a `↦` b:max := rename a b
 

library/init/reserved_notation.lean

@@ -65,6 +65,7 @@ reserve infixl `-`:65
 reserve infixl `*`:70
 reserve infixl `div`:70
 reserve infixl `mod`:70
+reserve infixl `/`:70
 reserve prefix `-`:100
 
 reserve infix `<=`:50

library/init/tactic.lean

@@ -63,6 +63,9 @@ opaque definition unfold     (e : expr)   : tactic := builtin
 opaque definition exact      (e : expr)   : tactic := builtin
 opaque definition trace      (s : string) : tactic := builtin
 opaque definition inversion  (id : expr)  : tactic := builtin
+-- rewrite_tac is just a marker for the builtin 'rewrite' notation
+-- used to create instances of this tactic.
+opaque definition rewrite_tac (e : expr)  : tactic := builtin
 
 notation a `↦` b:max := rename a b
 

src/emacs/lean-syntax.el

@@ -96,7 +96,7 @@
 
 (defconst lean-font-lock-defaults
   `((;; Keywords
-     (,(rx word-start (or "calc" "have" "obtains" "show" "by" "in" "let" "forall" "fun"
+     (,(rx word-start (or "calc" "have" "obtains" "show" "by" "in" "at" "let" "forall" "fun"
                             "exists" "if" "dif" "then" "else" "assume" "take" "obtain" "from") word-end)
       . font-lock-keyword-face)
      ;; String
@@ -126,7 +126,7 @@
      (,(rx (not (any "\.")) word-start
            (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply" "apply" "fapply" "rename" "intro" "intros"
                "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "repeat"
-               "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "assert")
+               "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "assert" "rewrite")
            word-end)
       . 'font-lock-constant-face)
      ;; Types

src/frontends/lean/CMakeLists.txt

@@ -7,6 +7,7 @@ begin_end_ext.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
 structure_cmd.cpp info_manager.cpp info_annotation.cpp find_cmd.cpp
 coercion_elaborator.cpp info_tactic.cpp proof_qed_elaborator.cpp
 init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp
+parse_tactic_location.cpp parse_rewrite_tactic.cpp
 type_util.cpp elaborator_exception.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/builtin_exprs.cpp

@@ -31,6 +31,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/info_tactic.h"
 #include "frontends/lean/info_annotation.h"
 #include "frontends/lean/structure_cmd.h"
+#include "frontends/lean/parse_rewrite_tactic.h"
 
 namespace lean {
 namespace notation {
@@ -419,6 +420,10 @@ static expr parse_calc_expr(parser & p, unsigned, expr const *, pos_info const &
     return parse_calc(p);
 }
 
+static expr parse_rewrite_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
+    return p.save_pos(parse_rewrite_tactic(p), pos);
+}
+
 static expr parse_overwrite_notation(parser & p, unsigned, expr const *, pos_info const &) {
     name n = p.check_id_next("invalid '#' local notation, identifier expected");
     environment env = overwrite_notation(p.env(), n);
@@ -488,6 +493,7 @@ parse_table init_nud_table() {
     r = r.add({transition("Type", mk_ext_action(parse_Type))}, x0);
     r = r.add({transition("let", mk_ext_action(parse_let_expr))}, x0);
     r = r.add({transition("calc", mk_ext_action(parse_calc_expr))}, x0);
+    r = r.add({transition("rewrite", mk_ext_action(parse_rewrite_tactic_expr))}, x0);
     r = r.add({transition("#", mk_ext_action(parse_overwrite_notation))}, x0);
     r = r.add({transition("@", mk_ext_action(parse_explicit_expr))}, x0);
     r = r.add({transition("!", mk_ext_action(parse_consume_args_expr))}, x0);

src/frontends/lean/parse_rewrite_tactic.cpp

@@ -0,0 +1,64 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/tactic/rewrite_tactic.h"
+#include "frontends/lean/parser.h"
+#include "frontends/lean/tokens.h"
+#include "frontends/lean/parse_tactic_location.h"
+
+namespace lean {
+name parse_rewrite_element_id(parser & p) {
+    return p.check_id_next("invalid rewrite tactic step, identifier expected");
+}
+
+rewrite_element parse_rewrite_element(parser & p) {
+    if (p.curr_is_token(get_slash_tk())) {
+        p.next();
+        return rewrite_element::mk_unfold(p.check_id_next("invalid unfold rewrite step, identifier expected"));
+    }
+    bool symm = false;
+    if (p.curr_is_token(get_sub_tk())) {
+        p.next();
+        symm = true;
+    }
+    if (p.curr_is_numeral()) {
+        unsigned n = p.parse_small_nat();
+        if (p.curr_is_token(get_question_tk())) {
+            p.next();
+            return rewrite_element::mk_at_most_n(parse_rewrite_element_id(p), n, symm);
+        } else if (p.curr_is_token(get_bang_tk())) {
+            p.next();
+            return rewrite_element::mk_exactly_n(parse_rewrite_element_id(p), n, symm);
+        } else {
+            return rewrite_element::mk_exactly_n(parse_rewrite_element_id(p), n, symm);
+        }
+    } else if (p.curr_is_token(get_question_tk())) {
+        p.next();
+        return rewrite_element::mk_zero_or_more(parse_rewrite_element_id(p), symm);
+    } else if (p.curr_is_token(get_bang_tk())) {
+        p.next();
+        return rewrite_element::mk_one_or_more(parse_rewrite_element_id(p), symm);
+    } else {
+        return rewrite_element::mk_once(parse_rewrite_element_id(p), symm);
+    }
+}
+
+expr parse_rewrite_tactic(parser & p) {
+    buffer<rewrite_element> elems;
+    while (true) {
+        elems.push_back(parse_rewrite_element(p));
+        if (!p.curr_is_token(get_sub_tk()) &&
+            !p.curr_is_numeral() &&
+            !p.curr_is_token(get_bang_tk()) &&
+            !p.curr_is_token(get_question_tk()) &&
+            !p.curr_is_token(get_slash_tk()) &&
+            !p.curr_is_identifier())
+            break;
+    }
+    location loc = parse_tactic_location(p);
+    return mk_rewrite_tactic_expr(elems, loc);
+}
+}

src/frontends/lean/parse_rewrite_tactic.h

@@ -0,0 +1,13 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/expr.h"
+
+namespace lean {
+class parser;
+expr parse_rewrite_tactic(parser & p);
+}

src/frontends/lean/parse_tactic_location.cpp

@@ -11,7 +11,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 static occurrence parse_occurrence(parser & p) {
-    if (p.curr_is_token(get_at_tk())) {
+    if (p.curr_is_token(get_lcurly_tk())) {
         p.next();
         bool has_pos = false;
         bool has_neg = false;
@@ -30,9 +30,10 @@ static occurrence parse_occurrence(parser & p) {
                     throw parser_error("invalid tactic location, cannot mix positive and negative occurrences", pos);
                 has_pos = true;
             }
-            if (!p.curr_is_token(get_sub_tk()) && !p.curr_is_numeral())
+            if (p.curr_is_token(get_rcurly_tk()))
                 break;
         }
+        p.next();
         if (has_pos)
             return occurrence::mk_occurrences(occs);
         else
@@ -43,44 +44,42 @@ static occurrence parse_occurrence(parser & p) {
 }
 
 location parse_tactic_location(parser & p) {
-    if (p.curr_is_token(get_in_tk())) {
+    if (p.curr_is_token(get_at_tk())) {
         p.next();
         if (p.curr_is_token(get_star_tk())) {
             p.next();
             if (p.curr_is_token(get_turnstile_tk())) {
                 p.next();
                 if (p.curr_is_token(get_star_tk())) {
-                    // in * |- *
+                    // at * |- *
                     return location::mk_everywhere();
                 } else {
-                    // in * |-
+                    // at * |-
                     return location::mk_all_hypotheses();
                 }
             } else {
-                // in *
+                // at *
                 return location::mk_everywhere();
             }
         } else {
             buffer<name>       hyps;
             buffer<occurrence> hyp_occs;
-            while (true) {
+            while (p.curr_is_identifier()) {
                 hyps.push_back(p.get_name_val());
                 p.next();
                 hyp_occs.push_back(parse_occurrence(p));
-                if (!p.curr_is_token(get_comma_tk()))
-                    break;
-                p.next();
             }
-            if (p.curr_is_token(get_turnstile_tk())) {
+            if (hyps.empty()) {
+                occurrence o = parse_occurrence(p);
+                return location::mk_goal_at(o);
+            } else if (p.curr_is_token(get_turnstile_tk())) {
+                p.next();
                 occurrence goal_occ = parse_occurrence(p);
                 return location::mk_at(goal_occ, hyps, hyp_occs);
             } else {
                 return location::mk_hypotheses_at(hyps, hyp_occs);
             }
         }
-    } else if (p.curr_is_token(get_at_tk())) {
-        occurrence o = parse_occurrence(p);
-        return location::mk_goal_at(o);
     } else {
         return location::mk_goal_only();
     }

src/frontends/lean/token_table.cpp

@@ -74,13 +74,13 @@ static char const * g_decreasing_unicode = "↓";
 
 void init_token_table(token_table & t) {
     pair<char const *, unsigned> builtin[] =
-        {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"obtain", 0},
+        {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"at", 0}, {"have", 0}, {"show", 0}, {"obtain", 0},
          {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0},
          {"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},
+         {"{|", g_max_prec}, {"|}", 0}, {"⊢", 0},
-         {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"with", 0}, {"...", 0}, {",", 0},
+         {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0},  {"with", 0}, {"...", 0}, {",", 0},
-         {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
+         {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {":=", 0}, {"--", 0}, {"#", 0},
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec},
          {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec},
          {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0},

src/frontends/lean/tokens.cpp

@@ -25,6 +25,12 @@ static name * g_rbracket     = nullptr;
 static name * g_bar          = nullptr;
 static name * g_comma        = nullptr;
 static name * g_add          = nullptr;
+static name * g_sub          = nullptr;
+static name * g_question     = nullptr;
+static name * g_bang         = nullptr;
+static name * g_slash        = nullptr;
+static name * g_star         = nullptr;
+static name * g_turnstile    = nullptr;
 static name * g_max          = nullptr;
 static name * g_imax         = nullptr;
 static name * g_cup          = nullptr;
@@ -58,6 +64,7 @@ static name * g_whnf         = nullptr;
 static name * g_wf           = nullptr;
 static name * g_strict       = nullptr;
 static name * g_in           = nullptr;
+static name * g_at           = nullptr;
 static name * g_assign       = nullptr;
 static name * g_visible      = nullptr;
 static name * g_from         = nullptr;
@@ -124,6 +131,12 @@ void initialize_tokens() {
     g_bar          = new name("|");
     g_comma        = new name(",");
     g_add          = new name("+");
+    g_sub          = new name("-");
+    g_question     = new name("?");
+    g_bang         = new name("!");
+    g_slash        = new name("/");
+    g_star         = new name("*");
+    g_turnstile    = new name("⊢");
     g_max          = new name("max");
     g_imax         = new name("imax");
     g_cup          = new name("\u2294");
@@ -157,6 +170,7 @@ void initialize_tokens() {
     g_wf           = new name("[wf]");
     g_strict       = new name("[strict]");
     g_in           = new name("in");
+    g_at           = new name("at");
     g_assign       = new name(":=");
     g_visible      = new name("[visible]");
     g_from         = new name("from");
@@ -242,6 +256,7 @@ void finalize_tokens() {
     delete g_attribute;
     delete g_parsing_only;
     delete g_in;
+    delete g_at;
     delete g_assign;
     delete g_visible;
     delete g_from;
@@ -286,6 +301,12 @@ void finalize_tokens() {
     delete g_imax;
     delete g_max;
     delete g_add;
+    delete g_sub;
+    delete g_question;
+    delete g_bang;
+    delete g_slash;
+    delete g_star;
+    delete g_turnstile;
     delete g_comma;
     delete g_bar;
     delete g_rbracket;
@@ -323,6 +344,12 @@ name const & get_rbracket_tk() { return *g_rbracket; }
 name const & get_bar_tk() { return *g_bar; }
 name const & get_comma_tk() { return *g_comma; }
 name const & get_add_tk() { return *g_add; }
+name const & get_sub_tk() { return *g_sub; }
+name const & get_question_tk() { return *g_question; }
+name const & get_bang_tk() { return *g_bang; }
+name const & get_slash_tk() { return *g_slash; }
+name const & get_star_tk() { return *g_star; }
+name const & get_turnstile_tk() { return *g_turnstile; }
 name const & get_max_tk() { return *g_max; }
 name const & get_imax_tk() { return *g_imax; }
 name const & get_cup_tk() { return *g_cup; }
@@ -356,6 +383,7 @@ name const & get_whnf_tk() { return *g_whnf; }
 name const & get_wf_tk() { return *g_wf; }
 name const & get_strict_tk() { return *g_strict; }
 name const & get_in_tk() { return *g_in; }
+name const & get_at_tk() { return *g_at; }
 name const & get_assign_tk() { return *g_assign; }
 name const & get_visible_tk() { return *g_visible; }
 name const & get_from_tk() { return *g_from; }

src/frontends/lean/tokens.h

@@ -27,6 +27,12 @@ name const & get_rbracket_tk();
 name const & get_bar_tk();
 name const & get_comma_tk();
 name const & get_add_tk();
+name const & get_sub_tk();
+name const & get_question_tk();
+name const & get_bang_tk();
+name const & get_slash_tk();
+name const & get_star_tk();
+name const & get_turnstile_tk();
 name const & get_max_tk();
 name const & get_imax_tk();
 name const & get_cup_tk();
@@ -60,6 +66,7 @@ name const & get_whnf_tk();
 name const & get_wf_tk();
 name const & get_strict_tk();
 name const & get_in_tk();
+name const & get_at_tk();
 name const & get_assign_tk();
 name const & get_visible_tk();
 name const & get_from_tk();

src/library/tactic/rewrite_tactic.cpp

@@ -108,6 +108,10 @@ location get_rewrite_location(expr const & e) {
     return static_cast<rewrite_elements_macro_cell const*>(macro_def(e).raw())->get_location();
 }
 
+expr mk_rewrite_tactic_expr(buffer<rewrite_element> const & elems, location const & loc) {
+    return mk_app(*g_rewrite_tac, mk_rewrite_elements(elems, loc));
+}
+
 tactic mk_rewrite_tactic(buffer<rewrite_element> const & elems, location const & loc) {
     // TODO(Leo)
     for (auto const & e : elems)
@@ -133,11 +137,13 @@ void initialize_rewrite_tactic() {
 
     register_tac(rewrite_tac_name,
                  [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
-                     if (!is_rewrite_elements(app_arg(e)))
+                     check_tactic_expr(app_arg(e), "invalid 'rewrite' tactic, invalid argument");
-                         throw expr_to_tactic_exception(e, "invalid 'rewrite' tactic, argument is ill-formed");
+                     expr arg = get_tactic_expr_expr(app_arg(e));
+                     if (!is_rewrite_elements(arg))
+                         throw expr_to_tactic_exception(e, "invalid 'rewrite' tactic, invalid argument");
                      buffer<rewrite_element> elems;
-                     get_rewrite_elements(app_arg(e), elems);
+                     get_rewrite_elements(arg, elems);
-                     location loc = get_rewrite_location(app_arg(e));
+                     location loc = get_rewrite_location(arg);
                      return mk_rewrite_tactic(elems, loc);
                  });
 }