From 5b8ac6ba3016a59dd8749f77fe7aedbcd2f57672 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 14 Jun 2016 21:30:02 -0700
Subject: [PATCH] feat(library/tactic): add 'exact' tactic

---
 library/init/meta/tactic.lean       |  1 +
 src/library/tactic/CMakeLists.txt   |  3 +-
 src/library/tactic/exact_tactic.cpp | 44 +++++++++++++++++++++++++++++
 src/library/tactic/exact_tactic.h   | 11 ++++++++
 src/library/tactic/init_module.cpp  |  3 ++
 src/library/tactic/tactic_state.cpp |  8 ++++--
 src/library/tactic/tactic_state.h   |  2 ++
 tests/lean/run/exact_tac1.lean      | 18 ++++++++++++
 8 files changed, 87 insertions(+), 3 deletions(-)
 create mode 100644 src/library/tactic/exact_tactic.cpp
 create mode 100644 src/library/tactic/exact_tactic.h
 create mode 100644 tests/lean/run/exact_tac1.lean

diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index d9a3f8a2d6..72eee4c05a 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -100,6 +100,7 @@ meta_constant mk_app        : name → list expr → tactic expr
      @ite.{1} (a > b) (nat.decidable_gt a b) nat a b -/
 meta_constant mk_mapp       : name → list (option expr) → tactic expr
 meta_constant subst         : name → tactic unit
+meta_constant exact         : expr → tactic unit
 open list nat
 
 meta_definition intros : tactic unit :=
diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt
index e36f4263ab..e4e6da52ee 100644
--- a/src/library/tactic/CMakeLists.txt
+++ b/src/library/tactic/CMakeLists.txt
@@ -1,3 +1,4 @@
 add_library(tactic OBJECT tactic_state.cpp intro_tactic.cpp assumption_tactic.cpp
   revert_tactic.cpp rename_tactic.cpp clear_tactic.cpp
-  app_builder_tactics.cpp subst_tactic.cpp elaborate.cpp init_module.cpp)
+  app_builder_tactics.cpp subst_tactic.cpp exact_tactic.cpp
+  elaborate.cpp init_module.cpp)
diff --git a/src/library/tactic/exact_tactic.cpp b/src/library/tactic/exact_tactic.cpp
new file mode 100644
index 0000000000..650b02143f
--- /dev/null
+++ b/src/library/tactic/exact_tactic.cpp
@@ -0,0 +1,44 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/vm/vm_expr.h"
+#include "library/tactic/tactic_state.h"
+#include "library/tactic/app_builder_tactics.h"
+
+namespace lean {
+vm_obj exact(expr const & e, tactic_state const & s) {
+    try {
+        optional<metavar_decl> g = s.get_main_goal_decl();
+        if (!g) return mk_no_goals_exception(s);
+        metavar_context mctx = s.mctx();
+        type_context ctx     = mk_type_context_for(s, mctx);
+        expr e_type          = ctx.infer(e);
+        if (!ctx.is_def_eq(g->get_type(), e_type)) {
+            format r("exact tactic failed, type mismatch, given expression has type");
+            unsigned indent = get_pp_indent(s.get_options());
+            r += nest(indent, line() + pp_expr(s, e_type));
+            r += line() + format("but is expected to have type");
+            r += nest(indent, line() + pp_expr(s, g->get_type()));
+            return mk_tactic_exception(r, s);
+        }
+        mctx.assign(head(s.goals()), e);
+        return mk_tactic_success(set_mctx_goals(s, mctx, tail(s.goals())));
+    } catch (exception & ex) {
+        return mk_tactic_exception(ex, s);
+    }
+}
+
+vm_obj tactic_exact(vm_obj const & e, vm_obj const & s) {
+    return exact(to_expr(e), to_tactic_state(s));
+}
+
+void initialize_exact_tactic() {
+    DECLARE_VM_BUILTIN(name({"tactic", "exact"}), tactic_exact);
+}
+
+void finalize_exact_tactic() {
+}
+}
diff --git a/src/library/tactic/exact_tactic.h b/src/library/tactic/exact_tactic.h
new file mode 100644
index 0000000000..f39a27b83e
--- /dev/null
+++ b/src/library/tactic/exact_tactic.h
@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+namespace lean {
+void initialize_exact_tactic();
+void finalize_exact_tactic();
+}
diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp
index 8ac7575397..edb100fe24 100644
--- a/src/library/tactic/init_module.cpp
+++ b/src/library/tactic/init_module.cpp
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "library/tactic/clear_tactic.h"
 #include "library/tactic/app_builder_tactics.h"
 #include "library/tactic/subst_tactic.h"
+#include "library/tactic/exact_tactic.h"
 #include "library/tactic/elaborate.h"
 
 namespace lean {
@@ -24,10 +25,12 @@ void initialize_tactic_module() {
     initialize_clear_tactic();
     initialize_app_builder_tactics();
     initialize_subst_tactic();
+    initialize_exact_tactic();
     initialize_elaborate();
 }
 void finalize_tactic_module() {
     finalize_elaborate();
+    finalize_exact_tactic();
     finalize_subst_tactic();
     finalize_app_builder_tactics();
     finalize_clear_tactic();
diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp
index 2aa753fee8..e515ad55c2 100644
--- a/src/library/tactic/tactic_state.cpp
+++ b/src/library/tactic/tactic_state.cpp
@@ -137,9 +137,13 @@ vm_obj tactic_state_to_format(vm_obj const & s) {
     return to_obj(to_tactic_state(s).pp(fmtf));
 }
 
-vm_obj tactic_state_format_expr(vm_obj const & s, vm_obj const & e) {
+format pp_expr(tactic_state const & s, expr const & e) {
     formatter_factory const & fmtf = get_global_ios().get_formatter_factory();
-    return to_obj(to_tactic_state(s).pp_expr(fmtf, to_expr(e)));
+    return s.pp_expr(fmtf, e);
+}
+
+vm_obj tactic_state_format_expr(vm_obj const & s, vm_obj const & e) {
+    return to_obj(pp_expr(to_tactic_state(s), to_expr(e)));
 }
 
 optional<tactic_state> is_tactic_success(vm_obj const & o) {
diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h
index cffe46444b..7ec413ee7e 100644
--- a/src/library/tactic/tactic_state.h
+++ b/src/library/tactic/tactic_state.h
@@ -93,6 +93,8 @@ vm_obj mk_tactic_exception(sstream const & strm, tactic_state const & s);
 vm_obj mk_tactic_exception(char const * msg, tactic_state const & s);
 vm_obj mk_no_goals_exception(tactic_state const & s);
 
+format pp_expr(tactic_state const & s, expr const & e);
+
 /* If r is (base_tactic_result.success a s), then return s */
 optional<tactic_state> is_tactic_success(vm_obj const & r);
 
diff --git a/tests/lean/run/exact_tac1.lean b/tests/lean/run/exact_tac1.lean
new file mode 100644
index 0000000000..9cdd60e581
--- /dev/null
+++ b/tests/lean/run/exact_tac1.lean
@@ -0,0 +1,18 @@
+open tactic list
+
+example (a b : nat) : a = a :=
+by do
+  a ← get_local "a",
+  r ← mk_app ("eq" <.> "refl") [a],
+  exact r
+
+set_option pp.all true
+
+example (a b : nat) (f : nat → nat) : a = b → f a = f b :=
+by do
+  intro "H",
+  H ← get_local "H",
+  f ← get_local "f",
+  r ← mk_app "congr_arg" [f, H],
+  trace_expr r,
+  exact r