From 5b25da8c43e39989d3ea5e735743634087db0a07 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 6 Feb 2015 14:13:32 -0800
Subject: [PATCH] feat(frontends/lean): add esimp tactic based on rewrite
 tactic

closes #358
---
 src/emacs/lean-syntax.el                    |  2 +-
 src/frontends/lean/builtin_exprs.cpp        |  5 +++
 src/frontends/lean/parse_rewrite_tactic.cpp | 45 ++++++++++++++-------
 src/frontends/lean/parse_rewrite_tactic.h   |  1 +
 src/frontends/lean/token_table.cpp          |  2 +-
 tests/lean/run/esimp1.lean                  | 28 +++++++++++++
 6 files changed, 66 insertions(+), 17 deletions(-)
 create mode 100644 tests/lean/run/esimp1.lean

diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index aef9bad4b..c20a69205 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -127,7 +127,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" "rewrite")
+               "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "assert" "rewrite" "esimp" "unfold")
            word-end)
       . 'font-lock-constant-face)
      ;; Types
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 77bda48a7..0dfd72b1c 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -415,6 +415,10 @@ static expr parse_rewrite_tactic_expr(parser & p, unsigned, expr const *, pos_in
     return p.save_pos(parse_rewrite_tactic(p), pos);
 }
 
+static expr parse_esimp_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
+    return p.save_pos(parse_esimp_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);
@@ -485,6 +489,7 @@ parse_table init_nud_table() {
     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("esimp", mk_ext_action(parse_esimp_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);
diff --git a/src/frontends/lean/parse_rewrite_tactic.cpp b/src/frontends/lean/parse_rewrite_tactic.cpp
index b29ef8851..ca8b54643 100644
--- a/src/frontends/lean/parse_rewrite_tactic.cpp
+++ b/src/frontends/lean/parse_rewrite_tactic.cpp
@@ -32,25 +32,29 @@ static expr parse_rule(parser & p) {
     }
 }
 
-expr parse_rewrite_element(parser & p) {
-    if (p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk())) {
+static expr parse_rewrite_unfold(parser & p) {
+    lean_assert(p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk()));
+    p.next();
+    buffer<name> to_unfold;
+    if (p.curr_is_token(get_lcurly_tk())) {
         p.next();
-        buffer<name> to_unfold;
-        if (p.curr_is_token(get_lcurly_tk())) {
+        while (true) {
+            to_unfold.push_back(p.check_constant_next("invalid unfold rewrite step, identifier expected"));
+            if (!p.curr_is_token(get_comma_tk()))
+                break;
             p.next();
-            while (true) {
-                to_unfold.push_back(p.check_constant_next("invalid unfold rewrite step, identifier expected"));
-                if (!p.curr_is_token(get_comma_tk()))
-                    break;
-                p.next();
-            }
-            p.check_token_next(get_rcurly_tk(), "invalid unfold rewrite step, ',' or '}' expected");
-        } else {
-            to_unfold.push_back(p.check_constant_next("invalid unfold rewrite step, identifier or '{' expected"));
         }
-        location loc = parse_tactic_location(p);
-        return mk_rewrite_unfold(to_list(to_unfold), loc);
+        p.check_token_next(get_rcurly_tk(), "invalid unfold rewrite step, ',' or '}' expected");
+    } else {
+        to_unfold.push_back(p.check_constant_next("invalid unfold rewrite step, identifier or '{' expected"));
     }
+    location loc = parse_tactic_location(p);
+    return mk_rewrite_unfold(to_list(to_unfold), loc);
+}
+
+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);
     bool symm = false;
     if (p.curr_is_token(get_sub_tk())) {
         p.next();
@@ -123,4 +127,15 @@ expr parse_rewrite_tactic(parser & p) {
     }
     return mk_rewrite_tactic_expr(elems);
 }
+
+expr parse_esimp_tactic(parser & p) {
+    buffer<expr> elems;
+    if (p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk())) {
+        elems.push_back(parse_rewrite_unfold(p));
+    } else {
+        location loc = parse_tactic_location(p);
+        elems.push_back(mk_rewrite_reduce(loc));
+    }
+    return mk_rewrite_tactic_expr(elems);
+}
 }
diff --git a/src/frontends/lean/parse_rewrite_tactic.h b/src/frontends/lean/parse_rewrite_tactic.h
index ab81f494a..353bcaf40 100644
--- a/src/frontends/lean/parse_rewrite_tactic.h
+++ b/src/frontends/lean/parse_rewrite_tactic.h
@@ -10,4 +10,5 @@ Author: Leonardo de Moura
 namespace lean {
 class parser;
 expr parse_rewrite_tactic(parser & p);
+expr parse_esimp_tactic(parser & p);
 }
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 3d5d4c698..26cc65beb 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -80,7 +80,7 @@ void init_token_table(token_table & t) {
          {"[", 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},
-         {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {":=", 0}, {"--", 0}, {"#", 0},
+         {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"esimp", 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},
diff --git a/tests/lean/run/esimp1.lean b/tests/lean/run/esimp1.lean
new file mode 100644
index 000000000..e52084b96
--- /dev/null
+++ b/tests/lean/run/esimp1.lean
@@ -0,0 +1,28 @@
+open nat
+
+example (x y : nat) (H : (fun (a : nat),  sigma.pr1 ⟨a, y⟩) x = 0) : x = 0 :=
+begin
+  esimp at H,
+  exact H
+end
+
+definition foo [irreducible] (a : nat) := a
+
+example (x y : nat) (H : (fun (a : nat), sigma.pr1 ⟨foo a, y⟩) x = 0) : x = 0 :=
+begin
+  esimp ↑foo at H,
+  exact H
+end
+
+example (x y : nat) (H : x = 0) : (fun (a : nat), sigma.pr1 ⟨foo a, y⟩) x = 0 :=
+begin
+  esimp ↑foo,
+  exact H
+end
+
+example (x y : nat) (H : x = 0) : (fun (a : nat), sigma.pr1 ⟨foo a, y⟩) x = 0 :=
+begin
+  esimp,
+  unfold foo,
+  exact H
+end