From 3a62ca058167608293c83650f809bf166a91b214 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 4 Jan 2017 09:36:50 -0800
Subject: [PATCH] refactor(library/init/meta): move smt tactics to
 library/init/meta/smt, and add interactive definitions

---
 library/init/meta/default.lean                |  3 +-
 library/init/meta/interactive.lean            |  2 +-
 .../meta/{ => smt}/congruence_tactics.lean    |  0
 library/init/meta/smt/default.lean            |  8 +++
 library/init/meta/smt/interactive.lean        | 70 +++++++++++++++++++
 library/init/meta/{ => smt}/smt_tactic.lean   |  3 +-
 src/frontends/lean/tactic_notation.cpp        | 15 ++--
 7 files changed, 90 insertions(+), 11 deletions(-)
 rename library/init/meta/{ => smt}/congruence_tactics.lean (100%)
 create mode 100644 library/init/meta/smt/default.lean
 create mode 100644 library/init/meta/smt/interactive.lean
 rename library/init/meta/{ => smt}/smt_tactic.lean (98%)

diff --git a/library/init/meta/default.lean b/library/init/meta/default.lean
index 2755361d37..3e64ddbfc4 100644
--- a/library/init/meta/default.lean
+++ b/library/init/meta/default.lean
@@ -13,5 +13,4 @@ import init.meta.backward init.meta.rewrite_tactic
 import init.meta.mk_dec_eq_instance init.meta.mk_inhabited_instance
 import init.meta.simp_tactic init.meta.set_get_option_tactics
 import init.meta.interactive init.meta.converter init.meta.vm
-import init.meta.comp_value_tactics init.meta.congruence_tactics
-import init.meta.smt_tactic init.cc_lemmas
+import init.meta.comp_value_tactics init.meta.smt
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 48b3e40621..167e67adba 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.meta.tactic init.meta.rewrite_tactic init.meta.simp_tactic
-import init.meta.congruence_tactics
+import init.meta.smt.congruence_tactics
 
 namespace interactive
 namespace types
diff --git a/library/init/meta/congruence_tactics.lean b/library/init/meta/smt/congruence_tactics.lean
similarity index 100%
rename from library/init/meta/congruence_tactics.lean
rename to library/init/meta/smt/congruence_tactics.lean
diff --git a/library/init/meta/smt/default.lean b/library/init/meta/smt/default.lean
new file mode 100644
index 0000000000..9247eb6434
--- /dev/null
+++ b/library/init/meta/smt/default.lean
@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.meta.smt.congruence_tactics init.meta.smt.smt_tactic
+import init.meta.smt.interactive init.cc_lemmas
diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean
new file mode 100644
index 0000000000..8b805501b4
--- /dev/null
+++ b/library/init/meta/smt/interactive.lean
@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.meta.smt.smt_tactic init.meta.interactive
+
+namespace smt_tactic
+meta def skip : smt_tactic unit :=
+return ()
+
+meta def step {α : Type} (tac : smt_tactic α) : smt_tactic unit :=
+tac >> return ()
+
+namespace interactive
+open interactive.types
+
+meta def intros : smt_tactic unit :=
+smt_tactic.intros
+
+meta def close : smt_tactic unit :=
+smt_tactic.close
+
+meta def apply (q : qexpr0) : smt_tactic unit :=
+tactic.interactive.apply q
+
+meta def fapply (q : qexpr0) : smt_tactic unit :=
+tactic.interactive.fapply q
+
+meta def apply_instance : smt_tactic unit :=
+tactic.apply_instance
+
+meta def change (q : qexpr0) : smt_tactic unit :=
+tactic.interactive.change q
+
+meta def exact (q : qexpr0) : smt_tactic unit :=
+tactic.interactive.exact q
+
+meta def assert (h : ident) (c : colon_tk) (q : qexpr0) : smt_tactic unit :=
+do e ← tactic.to_expr_strict q,
+   smt_tactic.assert h e
+
+meta def define (h : ident) (c : colon_tk) (q : qexpr0) : smt_tactic unit :=
+do e ← tactic.to_expr_strict q,
+   smt_tactic.define h e
+
+meta def assertv (h : ident) (c : colon_tk) (q₁ : qexpr0) (a : assign_tk) (q₂ : qexpr0) : smt_tactic unit :=
+do t ← tactic.to_expr_strict q₁,
+   v ← tactic.to_expr_strict `((%%q₂ : %%t)),
+   smt_tactic.assertv h t v
+
+meta def definev (h : ident) (c : colon_tk) (q₁ : qexpr0) (a : assign_tk) (q₂ : qexpr0) : smt_tactic unit :=
+do t ← tactic.to_expr_strict q₁,
+   v ← tactic.to_expr_strict `((%%q₂ : %%t)),
+   smt_tactic.definev h t v
+
+meta def note (h : ident) (a : assign_tk) (q : qexpr0) : smt_tactic unit :=
+do p ← tactic.to_expr_strict q,
+   smt_tactic.note h p
+
+meta def pose (h : ident) (a : assign_tk) (q : qexpr0) : smt_tactic unit :=
+do p ← tactic.to_expr_strict q,
+   smt_tactic.pose h p
+
+meta def trace_state : smt_tactic unit :=
+smt_tactic.trace_state
+
+end interactive
+end smt_tactic
diff --git a/library/init/meta/smt_tactic.lean b/library/init/meta/smt/smt_tactic.lean
similarity index 98%
rename from library/init/meta/smt_tactic.lean
rename to library/init/meta/smt/smt_tactic.lean
index 3722ed3d9e..2c46b61801 100644
--- a/library/init/meta/smt_tactic.lean
+++ b/library/init/meta/smt/smt_tactic.lean
@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.meta.congruence_tactics init.category.transformers
-import init.meta.simp_tactic
+import init.meta.simp_tactic init.meta.smt.congruence_tactics
 
 universe variables u
 
diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp
index 2065e88948..70944a2944 100644
--- a/src/frontends/lean/tactic_notation.cpp
+++ b/src/frontends/lean/tactic_notation.cpp
@@ -30,7 +30,10 @@ Author: Leonardo de Moura
 
    5) Extend is_tactic_class.
 
-   6) TODO(Leo): add elaborator interface */
+   6) Extend tactic_evaluator execute_begin_end method
+
+   TODO(Leo): improve the "recipe" above. It is too ad hoc.
+*/
 namespace lean {
 static name * g_begin_end = nullptr;
 static name * g_begin_end_element = nullptr;
@@ -223,7 +226,7 @@ static expr parse_location(parser & p) {
     }
 }
 
-expr parse_begin_end_block(parser & p, pos_info const & start_pos, name const & end_token, bool nested, name tac_class);
+static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name const & end_token, bool nested, name const & tac_class);
 
 static expr parse_nested_auto_quote_tactic(parser & p, name const & tac_class) {
     auto pos = p.pos();
@@ -354,9 +357,8 @@ static expr mk_tactic_skip(environment const & env, name const & tac_class) {
         return mk_app(mk_constant("return"), mk_constant(get_unit_star_name()));
 }
 
-expr parse_begin_end_block(parser & p, pos_info const & start_pos, name const & end_token, bool nested, name tac_class) {
+static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name const & end_token, bool nested, name const & tac_class) {
     p.next();
-    tac_class = parse_tactic_class(p, tac_class);
     expr r = p.save_pos(mk_begin_end_element(mk_tactic_skip(p.env(), tac_class)), start_pos);
     try {
         while (!p.curr_is_token(end_token)) {
@@ -402,7 +404,8 @@ expr parse_begin_end_expr_core(parser & p, pos_info const & pos, name const & en
     parser::local_scope _(p);
     p.clear_expr_locals();
     bool nested = false;
-    return parse_begin_end_block(p, pos, end_token, nested, get_tactic_name());
+    name tac_class = parse_tactic_class(p, get_tactic_name());
+    return parse_begin_end_block(p, pos, end_token, nested, tac_class);
 }
 
 expr parse_begin_end_expr(parser & p, pos_info const & pos) {
@@ -434,7 +437,7 @@ expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
 }
 
 expr parse_auto_quote_tactic_block(parser & p, unsigned, expr const *, pos_info const & pos) {
-    name tac_class = parse_tactic_class(p, get_tactic_name());
+    name const & tac_class = get_tactic_name();
     expr r = parse_tactic(p, tac_class);
     while (p.curr_is_token(get_comma_tk())) {
         p.next();