refactor(library/init/meta): move smt tactics to library/init/meta/smt, and add interactive definitions

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

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

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

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

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
 

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();