feat(frontends/lean): allow a different location for each rewrite element

src/frontends/lean/parse_rewrite_tactic.cpp

@@ -10,14 +10,16 @@ Author: Leonardo de Moura
 #include "frontends/lean/parse_tactic_location.h"
 
 namespace lean {
-name parse_rewrite_element_id(parser & p) {
+static 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"));
+        name id = p.check_id_next("invalid unfold rewrite step, identifier expected");
+        location loc = parse_tactic_location(p);
+        return rewrite_element::mk_unfold(id, loc);
     }
     bool symm = false;
     if (p.curr_is_token(get_sub_tk())) {
@@ -28,37 +30,56 @@ rewrite_element parse_rewrite_element(parser & p) {
         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);
+            name id = parse_rewrite_element_id(p);
+            location loc = parse_tactic_location(p);
+            return rewrite_element::mk_at_most_n(id, n, symm, loc);
         } else if (p.curr_is_token(get_bang_tk())) {
             p.next();
-            return rewrite_element::mk_exactly_n(parse_rewrite_element_id(p), n, symm);
+            name id = parse_rewrite_element_id(p);
+            location loc = parse_tactic_location(p);
+            return rewrite_element::mk_exactly_n(id, n, symm, loc);
         } else {
-            return rewrite_element::mk_exactly_n(parse_rewrite_element_id(p), n, symm);
+            name id = parse_rewrite_element_id(p);
+            location loc = parse_tactic_location(p);
+            return rewrite_element::mk_exactly_n(id, n, symm, loc);
         }
     } else if (p.curr_is_token(get_question_tk())) {
         p.next();
-        return rewrite_element::mk_zero_or_more(parse_rewrite_element_id(p), symm);
+        name id = parse_rewrite_element_id(p);
+        location loc = parse_tactic_location(p);
+        return rewrite_element::mk_zero_or_more(id, symm, loc);
     } else if (p.curr_is_token(get_bang_tk())) {
         p.next();
-        return rewrite_element::mk_one_or_more(parse_rewrite_element_id(p), symm);
+        name id = parse_rewrite_element_id(p);
+        location loc = parse_tactic_location(p);
+        return rewrite_element::mk_one_or_more(id, symm, loc);
     } else {
-        return rewrite_element::mk_once(parse_rewrite_element_id(p), symm);
+        name id = parse_rewrite_element_id(p);
+        location loc = parse_tactic_location(p);
+        return rewrite_element::mk_once(id, symm, loc);
     }
 }
 
 expr parse_rewrite_tactic(parser & p) {
     buffer<rewrite_element> elems;
     while (true) {
+        bool has_paren = false;
+        if (p.curr_is_token(get_lparen_tk())) {
+            has_paren = true;
+            p.next();
+        }
         elems.push_back(parse_rewrite_element(p));
+        if (has_paren)
+            p.check_token_next(get_rparen_tk(), "invalid rewrite tactic element, ')' expected");
         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())
+            !p.curr_is_identifier() &&
+            !p.curr_is_token(get_lparen_tk()))
             break;
     }
-    location loc = parse_tactic_location(p);
+    return mk_rewrite_tactic_expr(elems);
-    return mk_rewrite_tactic_expr(elems, loc);
 }
 }

src/frontends/lean/parse_tactic_location.cpp

@@ -61,24 +61,35 @@ location parse_tactic_location(parser & p) {
                 // at *
                 return location::mk_everywhere();
             }
-        } else {
+        } else if (p.curr_is_token(get_lparen_tk())) {
+            p.next();
             buffer<name>       hyps;
             buffer<occurrence> hyp_occs;
-            while (p.curr_is_identifier()) {
+            while (true) {
                 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 (hyps.empty()) {
+            p.check_token_next(get_rparen_tk(), "invalid tactic location, ')' expected");
-                occurrence o = parse_occurrence(p);
+            if (p.curr_is_token(get_turnstile_tk())) {
-                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_lcurly_tk())) {
+            occurrence o = parse_occurrence(p);
+            return location::mk_goal_at(o);
+        } else {
+            buffer<name>       hyps;
+            buffer<occurrence> hyp_occs;
+            hyps.push_back(p.check_id_next("invalid tactic location, identifier expected"));
+            hyp_occs.push_back(parse_occurrence(p));
+            return location::mk_hypotheses_at(hyps, hyp_occs);
         }
     } else {
         return location::mk_goal_only();

src/library/tactic/rewrite_tactic.cpp

@@ -12,36 +12,36 @@ namespace lean {
 rewrite_element::rewrite_element():m_symm(false), m_unfold(true), m_multiplicity(rewrite_multiplicity::Once) {}
 
 rewrite_element::rewrite_element(name const & l, bool symm, bool unfold, rewrite_multiplicity m,
-                                 optional<unsigned> const & n):
+                                 optional<unsigned> const & n, location const & loc):
-    m_lemma(l), m_symm(symm), m_unfold(unfold), m_multiplicity(m), m_num(n) {
+    m_lemma(l), m_symm(symm), m_unfold(unfold), m_multiplicity(m), m_num(n), m_location(loc) {
 }
 
-rewrite_element rewrite_element::mk_unfold(name const & l) {
+rewrite_element rewrite_element::mk_unfold(name const & l, location const & loc) {
-    return rewrite_element(l, false, true, rewrite_multiplicity::Once, optional<unsigned>());
+    return rewrite_element(l, false, true, rewrite_multiplicity::Once, optional<unsigned>(), loc);
 }
 
-rewrite_element rewrite_element::mk_once(name const & l, bool symm) {
+rewrite_element rewrite_element::mk_once(name const & l, bool symm, location const & loc) {
-    return rewrite_element(l, symm, false, rewrite_multiplicity::Once, optional<unsigned>());
+    return rewrite_element(l, symm, false, rewrite_multiplicity::Once, optional<unsigned>(), loc);
 }
 
-rewrite_element rewrite_element::mk_at_most_n(name const & l, unsigned n, bool symm) {
+rewrite_element rewrite_element::mk_at_most_n(name const & l, unsigned n, bool symm, location const & loc) {
-    return rewrite_element(l, symm, false, rewrite_multiplicity::AtMostN, optional<unsigned>(n));
+    return rewrite_element(l, symm, false, rewrite_multiplicity::AtMostN, optional<unsigned>(n), loc);
 }
 
-rewrite_element rewrite_element::mk_exactly_n(name const & l, unsigned n, bool symm) {
+rewrite_element rewrite_element::mk_exactly_n(name const & l, unsigned n, bool symm, location const & loc) {
-    return rewrite_element(l, symm, false, rewrite_multiplicity::ExactlyN, optional<unsigned>(n));
+    return rewrite_element(l, symm, false, rewrite_multiplicity::ExactlyN, optional<unsigned>(n), loc);
 }
 
-rewrite_element rewrite_element::mk_zero_or_more(name const & l, bool symm) {
+rewrite_element rewrite_element::mk_zero_or_more(name const & l, bool symm, location const & loc) {
-    return rewrite_element(l, symm, false, rewrite_multiplicity::ZeroOrMore, optional<unsigned>());
+    return rewrite_element(l, symm, false, rewrite_multiplicity::ZeroOrMore, optional<unsigned>(), loc);
 }
 
-rewrite_element rewrite_element::mk_one_or_more(name const & l, bool symm) {
+rewrite_element rewrite_element::mk_one_or_more(name const & l, bool symm, location const & loc) {
-    return rewrite_element(l, symm, false, rewrite_multiplicity::ZeroOrMore, optional<unsigned>());
+    return rewrite_element(l, symm, false, rewrite_multiplicity::ZeroOrMore, optional<unsigned>(), loc);
 }
 
 serializer & operator<<(serializer & s, rewrite_element const & e) {
-    s << e.m_lemma << e.m_symm << e.m_unfold << static_cast<char>(e.m_multiplicity);
+    s << e.m_lemma << e.m_symm << e.m_unfold << static_cast<char>(e.m_multiplicity) << e.m_location;
     if (e.has_num())
         s << e.num();
     return s;
@@ -49,7 +49,7 @@ serializer & operator<<(serializer & s, rewrite_element const & e) {
 
 deserializer & operator>>(deserializer & d, rewrite_element & e) {
     char multp;
-    d >> e.m_lemma >> e.m_symm >> e.m_unfold >> multp;
+    d >> e.m_lemma >> e.m_symm >> e.m_unfold >> multp >> e.m_location;
     e.m_multiplicity = static_cast<rewrite_multiplicity>(multp);
     if (e.has_num())
         e.m_num = d.read_unsigned();
@@ -64,29 +64,27 @@ static std::string * g_rewrite_elems_opcode    = nullptr;
 
 class rewrite_elements_macro_cell : public macro_definition_cell {
     list<rewrite_element> m_elems;
-    location              m_loc;
 public:
-    rewrite_elements_macro_cell(list<rewrite_element> const & elems, location const & loc):m_elems(elems), m_loc(loc) {}
+    rewrite_elements_macro_cell(list<rewrite_element> const & elems):m_elems(elems) {}
     virtual name get_name() const { return *g_rewrite_elems_name; }
     virtual pair<expr, constraint_seq> get_type(expr const &, extension_context &) const { throw_re_ex(); }
     virtual optional<expr> expand(expr const &, extension_context &) const { throw_re_ex(); }
     virtual void write(serializer & s) const {
-        s << *g_rewrite_elems_opcode << m_loc;
+        s << *g_rewrite_elems_opcode;
         write_list<rewrite_element>(s, m_elems);
 
     }
     list<rewrite_element> const & get_elems() const { return m_elems; }
-    location const & get_location() const { return m_loc; }
 };
 
 /** \brief Create a macro expression to encapsulate a list of rewrite elements */
-expr mk_rewrite_elements(list<rewrite_element> const & e, location const & loc) {
+expr mk_rewrite_elements(list<rewrite_element> const & e) {
-    macro_definition def(new rewrite_elements_macro_cell(e, loc));
+    macro_definition def(new rewrite_elements_macro_cell(e));
     return mk_macro(def);
 }
 
-expr mk_rewrite_elements(buffer<rewrite_element> const & e, location const & loc) {
+expr mk_rewrite_elements(buffer<rewrite_element> const & e) {
-    return mk_rewrite_elements(to_list(e), loc);
+    return mk_rewrite_elements(to_list(e));
 }
 
 /** \brief Return true iff \c e is a "macro" that encapsulates a list of rewrite_elements */
@@ -103,20 +101,14 @@ void get_rewrite_elements(expr const & e, buffer<rewrite_element> & result) {
     to_buffer(l, result);
 }
 
-location get_rewrite_location(expr const & e) {
+expr mk_rewrite_tactic_expr(buffer<rewrite_element> const & elems) {
-    lean_assert(is_rewrite_elements(e));
+    return mk_app(*g_rewrite_tac, mk_rewrite_elements(elems));
-    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) {
+tactic mk_rewrite_tactic(buffer<rewrite_element> const & elems) {
-    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)
         std::cout << ">> " << e.get_name() << "\n";
-    std::cout << "include goal >> " << static_cast<bool>(loc.includes_goal()) << "\n";
     return id_tactic();
 }
 
@@ -129,10 +121,8 @@ void initialize_rewrite_tactic() {
                                 [](deserializer & d, unsigned num, expr const *) {
                                     if (num != 0)
                                         throw corrupted_stream_exception();
-                                    location loc;
-                                    d >> loc;
                                     list<rewrite_element> elems = read_list<rewrite_element>(d);
-                                    return mk_rewrite_elements(elems, loc);
+                                    return mk_rewrite_elements(elems);
                                 });
 
     register_tac(rewrite_tac_name,
@@ -143,8 +133,7 @@ void initialize_rewrite_tactic() {
                          throw expr_to_tactic_exception(e, "invalid 'rewrite' tactic, invalid argument");
                      buffer<rewrite_element> elems;
                      get_rewrite_elements(arg, elems);
-                     location loc = get_rewrite_location(arg);
+                     return mk_rewrite_tactic(elems);
-                     return mk_rewrite_tactic(elems, loc);
                  });
 }
 

src/library/tactic/rewrite_tactic.h

@@ -17,15 +17,17 @@ class rewrite_element {
     bool                 m_unfold;
     rewrite_multiplicity m_multiplicity;
     optional<unsigned>   m_num;
-    rewrite_element(name const & l, bool symm, bool unfold, rewrite_multiplicity m, optional<unsigned> const & n);
+    location             m_location;
+    rewrite_element(name const & l, bool symm, bool unfold, rewrite_multiplicity m, optional<unsigned> const & n,
+                    location const & loc);
 public:
     rewrite_element();
-    static rewrite_element mk_unfold(name const & l);
+    static rewrite_element mk_unfold(name const & l, location const & loc);
-    static rewrite_element mk_once(name const & l, bool symm = false);
+    static rewrite_element mk_once(name const & l, bool symm, location const & loc);
-    static rewrite_element mk_at_most_n(name const & l, unsigned n, bool symm = false);
+    static rewrite_element mk_at_most_n(name const & l, unsigned n, bool symm, location const & loc);
-    static rewrite_element mk_exactly_n(name const & l, unsigned n, bool symm = false);
+    static rewrite_element mk_exactly_n(name const & l, unsigned n, bool symm, location const & loc);
-    static rewrite_element mk_zero_or_more(name const & l, bool symm = false);
+    static rewrite_element mk_zero_or_more(name const & l, bool symm, location const & loc);
-    static rewrite_element mk_one_or_more(name const & l, bool symm = false);
+    static rewrite_element mk_one_or_more(name const & l, bool symm, location const & loc);
     name const & get_name() const { return m_lemma; }
     bool unfold() const { return m_unfold; }
     bool symm() const {
@@ -43,16 +45,17 @@ public:
         lean_assert(has_num());
         return *m_num;
     }
+    location get_location() const { return m_location; }
 
     friend serializer & operator<<(serializer & s, rewrite_element const & elem);
     friend deserializer & operator>>(deserializer & d, rewrite_element & e);
 };
 
 /** \brief Create a rewrite tactic expression, where elems was created using \c mk_rewrite_elements. */
-expr mk_rewrite_tactic_expr(buffer<rewrite_element> const & elems, location const & loc = location());
+expr mk_rewrite_tactic_expr(buffer<rewrite_element> const & elems);
 
 /** \brief Create rewrite tactic that applies the given rewrite elements */
-tactic mk_rewrite_tactic(buffer<rewrite_element> const & elems, location const & loc = location());
+tactic mk_rewrite_tactic(buffer<rewrite_element> const & elems);
 
 void initialize_rewrite_tactic();
 void finalize_rewrite_tactic();