From 1e8a975daa193b95d1d66dcb6d9b4570ab2c5315 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 6 Feb 2015 15:22:34 -0800
Subject: [PATCH] feat(frontends/lean): extend parser: rewrite "fold" step

---
 src/frontends/lean/parse_rewrite_tactic.cpp |  6 ++++++
 src/frontends/lean/tokens.cpp               |  4 ++++
 src/frontends/lean/tokens.h                 |  1 +
 tests/lean/run/rewriter17.lean              |  9 +++++++++
 tests/lean/run/rewriter18.lean              | 10 ++++++++++
 5 files changed, 30 insertions(+)
 create mode 100644 tests/lean/run/rewriter17.lean
 create mode 100644 tests/lean/run/rewriter18.lean

diff --git a/src/frontends/lean/parse_rewrite_tactic.cpp b/src/frontends/lean/parse_rewrite_tactic.cpp
index ca8b54643..5343097aa 100644
--- a/src/frontends/lean/parse_rewrite_tactic.cpp
+++ b/src/frontends/lean/parse_rewrite_tactic.cpp
@@ -55,6 +55,12 @@ static expr parse_rewrite_unfold(parser & p) {
 expr parse_rewrite_element(parser & p) {
     if (p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk()))
         return parse_rewrite_unfold(p);
+    if (p.curr_is_token(get_down_tk())) {
+        p.next();
+        expr e = p.parse_expr();
+        location loc = parse_tactic_location(p);
+        return mk_rewrite_fold(e, loc);
+    }
     bool symm = false;
     if (p.curr_is_token(get_sub_tk())) {
         p.next();
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index 056e3e9a4..a8af626f5 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -27,6 +27,7 @@ static name * g_rangle       = nullptr;
 static name * g_triangle     = nullptr;
 static name * g_caret        = nullptr;
 static name * g_up           = nullptr;
+static name * g_down         = nullptr;
 static name * g_bar          = nullptr;
 static name * g_comma        = nullptr;
 static name * g_add          = nullptr;
@@ -142,6 +143,7 @@ void initialize_tokens() {
     g_triangle     = new name("▸");
     g_caret        = new name("^");
     g_up           = new name("↑");
+    g_down         = new name("<d");
     g_bar          = new name("|");
     g_comma        = new name(",");
     g_add          = new name("+");
@@ -336,6 +338,7 @@ void finalize_tokens() {
     delete g_triangle;
     delete g_caret;
     delete g_up;
+    delete g_down;
     delete g_rbracket;
     delete g_lbracket;
     delete g_rdcurly;
@@ -362,6 +365,7 @@ name const & get_rangle_tk() { return *g_rangle; }
 name const & get_triangle_tk() { return *g_triangle; }
 name const & get_caret_tk() { return *g_caret; }
 name const & get_up_tk() { return *g_up; }
+name const & get_down_tk() { return *g_down; }
 name const & get_lparen_tk() { return *g_lparen; }
 name const & get_rparen_tk() { return *g_rparen; }
 name const & get_llevel_curly_tk() { return *g_llevel_curly; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index 70e25e8ba..d7a2eb60f 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -29,6 +29,7 @@ name const & get_rangle_tk();
 name const & get_triangle_tk();
 name const & get_caret_tk();
 name const & get_up_tk();
+name const & get_down_tk();
 name const & get_bar_tk();
 name const & get_comma_tk();
 name const & get_add_tk();
diff --git a/tests/lean/run/rewriter17.lean b/tests/lean/run/rewriter17.lean
new file mode 100644
index 000000000..6d448f0d4
--- /dev/null
+++ b/tests/lean/run/rewriter17.lean
@@ -0,0 +1,9 @@
+open nat
+
+definition foo [irreducible] (x : nat) := x + 1
+
+example (a b : nat) (H : foo a = b) : a + 1 = b :=
+begin
+  rewrite ↓foo a,
+  exact H
+end
diff --git a/tests/lean/run/rewriter18.lean b/tests/lean/run/rewriter18.lean
new file mode 100644
index 000000000..14988f547
--- /dev/null
+++ b/tests/lean/run/rewriter18.lean
@@ -0,0 +1,10 @@
+import algebra.ring
+open algebra
+
+definition foo {A : Type} [s : monoid A] (a : A) :=
+a * a
+
+example {A : Type} [s : comm_ring A] (a b : A) (H : foo a = a) : a * a = a :=
+begin
+  rewrite [↓foo a, H]
+end