feat(library/tactic): add 'with_options' tactical

see issue #494

src/library/tactic/CMakeLists.txt

@@ -6,6 +6,6 @@ expr_to_tactic.cpp location.cpp rewrite_tactic.cpp util.cpp
 init_module.cpp change_tactic.cpp check_expr_tactic.cpp let_tactic.cpp
 contradiction_tactic.cpp exfalso_tactic.cpp constructor_tactic.cpp
 injection_tactic.cpp congruence_tactic.cpp relation_tactics.cpp
-induction_tactic.cpp subst_tactic.cpp unfold_rec.cpp)
+induction_tactic.cpp subst_tactic.cpp unfold_rec.cpp with_options_tactic.cpp)
 
 target_link_libraries(tactic ${LEAN_LIBS})

src/library/tactic/expr_to_tactic.h

@@ -26,6 +26,8 @@ bool has_tactic_decls(environment const & env);
    \c register_expr_to_tactic.
 */
 tactic expr_to_tactic(environment const & env, elaborate_fn const & fn, expr const & e, pos_info_provider const * p);
+// auxiliary procedure used to compile nested tactic in tacticals
+tactic expr_to_tactic(type_checker & tc, elaborate_fn const & fn, expr e, pos_info_provider const * p);
 
 name const & get_tactic_name();
 

src/library/tactic/init_module.cpp

@@ -31,6 +31,7 @@ Author: Leonardo de Moura
 #include "library/tactic/induction_tactic.h"
 #include "library/tactic/subst_tactic.h"
 #include "library/tactic/location.h"
+#include "library/tactic/with_options_tactic.h"
 
 namespace lean {
 void initialize_tactic_module() {
@@ -60,9 +61,11 @@ void initialize_tactic_module() {
     initialize_induction_tactic();
     initialize_subst_tactic();
     initialize_location();
+    initialize_with_options_tactic();
 }
 
 void finalize_tactic_module() {
+    finalize_with_options_tactic();
     finalize_location();
     finalize_subst_tactic();
     finalize_induction_tactic();

src/library/tactic/with_options_tactic.cpp

@@ -0,0 +1,99 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/type_checker.h"
+#include "library/kernel_serializer.h"
+#include "library/tactic/tactic.h"
+#include "library/tactic/expr_to_tactic.h"
+
+namespace lean {
+static name * g_options_name             = nullptr;
+static std::string * g_options_opcode    = nullptr;
+
+[[ noreturn ]] static void throw_ex() { throw exception("unexpected occurrence of 'options' expression"); }
+
+// Auxiliary macro for wrapping a options object as an expression
+class options_macro_cell : public macro_definition_cell {
+    options m_info;
+public:
+    options_macro_cell(options const & info):m_info(info) {}
+    virtual name get_name() const { return *g_options_name; }
+    virtual void write(serializer & s) const {
+        s << *g_options_opcode << m_info;
+    }
+    virtual pair<expr, constraint_seq> check_type(expr const &, extension_context &, bool) const { throw_ex(); }
+    virtual optional<expr> expand(expr const &, extension_context &) const { throw_ex(); }
+    virtual bool operator==(macro_definition_cell const & other) const {
+        if (auto o = dynamic_cast<options_macro_cell const *>(&other))
+            return m_info == o->m_info;
+        return false;
+    }
+    options const & get_info() const { return m_info; }
+};
+
+expr mk_options_expr(options const & loc) {
+    macro_definition def(new options_macro_cell(loc));
+    return mk_macro(def);
+}
+
+bool is_options_expr(expr const & e) {
+    return is_macro(e) && macro_def(e).get_name() == *g_options_name;
+}
+
+options const & get_options_expr_options(expr const & e) {
+    lean_assert(is_options_expr(e));
+    return static_cast<options_macro_cell const*>(macro_def(e).raw())->get_info();
+}
+
+static expr * g_with_options_tac = nullptr;
+
+expr mk_with_options_tactic_expr(options const & o, expr const & t) {
+    return mk_app(*g_with_options_tac, mk_options_expr(o), t);
+}
+
+tactic with_options(options const & o, tactic const & t) {
+    return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
+            options c = ios.get_options();
+            io_state new_ios(ios, join(c, o));
+            return t(env, new_ios, s);
+        });
+}
+
+void initialize_with_options_tactic() {
+    g_options_name     = new name("options");
+    g_options_opcode   = new std::string("OPTM");
+    register_macro_deserializer(*g_options_opcode,
+                                [](deserializer & d, unsigned num, expr const *) {
+                                    if (num > 0)
+                                        throw corrupted_stream_exception();
+                                    options info;
+                                    d >> info;
+                                    return mk_options_expr(info);
+                                });
+
+    name with_options_tac_name{"tactic", "with_options_tac"};
+    g_with_options_tac = new expr(Const(with_options_tac_name));
+    register_tac(with_options_tac_name,
+                 [=](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
+                     buffer<expr> args;
+                     get_app_args(e, args);
+                     if (args.size() != 2)
+                         throw expr_to_tactic_exception(e, "invalid 'with_options' tactical, it must have two arguments");
+                     check_tactic_expr(args[0], "invalid 'with_options' tactical, invalid argument");
+                     expr opts = get_tactic_expr_expr(args[0]);
+                     if (!is_options_expr(opts))
+                         throw expr_to_tactic_exception(args[0], "invalid 'with_options' tactical, invalid argument");
+                     tactic t  = expr_to_tactic(tc, fn, args[1], p);
+                     return with_options(get_options_expr_options(opts), t);
+                 });
+}
+
+void finalize_with_options_tactic() {
+    delete g_options_name;
+    delete g_options_opcode;
+    delete g_with_options_tac;
+}
+}

src/library/tactic/with_options_tactic.h

@@ -0,0 +1,14 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/expr.h"
+
+namespace lean {
+expr mk_with_options_tactic_expr(options const & o, expr const & t);
+void initialize_with_options_tactic();
+void finalize_with_options_tactic();
+}