remove(frontends/lean): begin_end pre-tactics

This was never used

src/frontends/lean/CMakeLists.txt

@@ -3,7 +3,7 @@ token_table.cpp scanner.cpp parse_table.cpp parser_config.cpp
 parser.cpp parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp
 server.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp
 inductive_cmd.cpp elaborator.cpp dependencies.cpp
-begin_end_ext.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
+begin_end_annotation.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
 structure_cmd.cpp info_manager.cpp info_annotation.cpp find_cmd.cpp
 coercion_elaborator.cpp info_tactic.cpp
 init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp

src/frontends/lean/begin_end_annotation.cpp

@@ -0,0 +1,30 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <string>
+#include "library/annotation.h"
+
+namespace lean {
+static name * g_begin_end = nullptr;
+static name * g_begin_end_element = nullptr;
+
+expr mk_begin_end_annotation(expr const & e) { return mk_annotation(*g_begin_end, e, nulltag); }
+expr mk_begin_end_element_annotation(expr const & e) { return mk_annotation(*g_begin_end_element, e, nulltag); }
+bool is_begin_end_annotation(expr const & e) { return is_annotation(e, *g_begin_end); }
+bool is_begin_end_element_annotation(expr const & e) { return is_annotation(e, *g_begin_end_element); }
+
+void initialize_begin_end_annotation() {
+    g_begin_end  = new name("begin_end");
+    g_begin_end_element = new name("begin_end_element");
+    register_annotation(*g_begin_end);
+    register_annotation(*g_begin_end_element);
+}
+
+void finalize_begin_end_annotation() {
+    delete g_begin_end;
+    delete g_begin_end_element;
+}
+}

src/frontends/lean/begin_end_annotation.h

@@ -9,16 +9,11 @@ Author: Leonardo de Moura
 #include "frontends/lean/cmd_table.h"
 
 namespace lean {
-environment add_begin_end_pre_tactic(environment const & env, expr const & pre_tac);
-environment reset_begin_end_pre_tactic(environment const & env, expr const & pre_tac);
-optional<expr> get_begin_end_pre_tactic(environment const & env);
-void register_begin_end_cmds(cmd_table & r);
-
 expr mk_begin_end_annotation(expr const & e);
 expr mk_begin_end_element_annotation(expr const & e);
 bool is_begin_end_annotation(expr const & e);
 bool is_begin_end_element_annotation(expr const & e);
 
-void initialize_begin_end_ext();
-void finalize_begin_end_ext();
+void initialize_begin_end_annotation();
+void finalize_begin_end_annotation();
 }

src/frontends/lean/begin_end_ext.cpp

@@ -1,133 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <string>
-#include "kernel/type_checker.h"
-#include "library/scoped_ext.h"
-#include "library/kernel_serializer.h"
-#include "library/annotation.h"
-#include "library/tactic/expr_to_tactic.h"
-#include "frontends/lean/parser.h"
-#include "frontends/lean/tactic_hint.h"
-
-namespace lean {
-// This (scoped) environment extension allows us to set a tactic to be applied before every element
-// in a <tt>begin ... end</tt> block
-struct be_entry {
-    bool m_accumulate; // if true, then accumulate the new tactic, if false replace
-    expr m_tac;
-    be_entry():m_accumulate(false) {}
-    be_entry(bool a, expr const & t):m_accumulate(a), m_tac(t) {}
-};
-
-struct be_state {
-    optional<expr> m_pre_tac;
-    optional<expr> m_pre_tac_body;
-};
-
-static name * g_class_name = nullptr;
-static std::string * g_key = nullptr;
-
-struct be_config {
-    typedef be_state state;
-    typedef be_entry entry;
-    static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
-        if (e.m_accumulate) {
-            if (s.m_pre_tac_body)
-                s.m_pre_tac_body = mk_app(get_or_else_tac_fn(), *s.m_pre_tac_body, e.m_tac);
-            else
-                s.m_pre_tac_body = e.m_tac;
-            s.m_pre_tac = mk_app(get_repeat_tac_fn(), *s.m_pre_tac_body);
-        } else {
-            // reset
-            s.m_pre_tac      = e.m_tac;
-            s.m_pre_tac_body = e.m_tac;
-        }
-    }
-    static name const & get_class_name() {
-        return *g_class_name;
-    }
-    static std::string const & get_serialization_key() {
-        return *g_key;
-    }
-    static void  write_entry(serializer & s, entry const & e) {
-        s << e.m_accumulate << e.m_tac;
-    }
-    static entry read_entry(deserializer & d) {
-        entry e;
-        d >> e.m_accumulate >> e.m_tac;
-        return e;
-    }
-    static optional<unsigned> get_fingerprint(entry const & e) {
-        return some(hash(e.m_accumulate, e.m_tac.hash()));
-    }
-};
-
-template class scoped_ext<be_config>;
-typedef scoped_ext<be_config> begin_end_ext;
-
-static name * g_begin_end = nullptr;
-static name * g_begin_end_element = nullptr;
-
-expr mk_begin_end_annotation(expr const & e) { return mk_annotation(*g_begin_end, e, nulltag); }
-expr mk_begin_end_element_annotation(expr const & e) { return mk_annotation(*g_begin_end_element, e, nulltag); }
-bool is_begin_end_annotation(expr const & e) { return is_annotation(e, *g_begin_end); }
-bool is_begin_end_element_annotation(expr const & e) { return is_annotation(e, *g_begin_end_element); }
-
-void initialize_begin_end_ext() {
-    g_class_name = new name("begin_end");
-    g_key        = new std::string("BEPRETAC");
-    begin_end_ext::initialize();
-    g_begin_end  = new name("begin_end");
-    g_begin_end_element = new name("begin_end_element");
-    register_annotation(*g_begin_end);
-    register_annotation(*g_begin_end_element);
-}
-
-void finalize_begin_end_ext() {
-    delete g_begin_end;
-    delete g_begin_end_element;
-    begin_end_ext::finalize();
-    delete g_key;
-    delete g_class_name;
-}
-
-static void check_valid_tactic(environment const & env, expr const & pre_tac) {
-    type_checker tc(env);
-    if (!tc.is_def_eq(tc.infer(pre_tac).first, get_tactic_type()).first)
-        throw exception("invalid begin_end pre-tactic update, argument is not a tactic");
-}
-
-environment add_begin_end_pre_tactic(environment const & env, expr const & pre_tac) {
-    check_valid_tactic(env, pre_tac);
-    return begin_end_ext::add_entry(env, get_dummy_ios(), be_entry(true, pre_tac), get_namespace(env), true);
-}
-
-environment set_begin_end_pre_tactic(environment const & env, expr const & pre_tac) {
-    check_valid_tactic(env, pre_tac);
-    return begin_end_ext::add_entry(env, get_dummy_ios(), be_entry(false, pre_tac), get_namespace(env), true);
-}
-
-optional<expr> get_begin_end_pre_tactic(environment const & env) {
-    be_state const & s = begin_end_ext::get_state(env);
-    return s.m_pre_tac;
-}
-
-environment add_begin_end_cmd(parser & p) {
-    return add_begin_end_pre_tactic(p.env(), parse_tactic_name(p));
-}
-
-environment set_begin_end_cmd(parser & p) {
-    return set_begin_end_pre_tactic(p.env(), parse_tactic_name(p));
-}
-
-void register_begin_end_cmds(cmd_table & r) {
-    add_cmd(r, cmd_info("add_begin_end_tactic", "add a new tactic to be automatically applied before every component in a 'begin-end' block",
-                        add_begin_end_cmd));
-    add_cmd(r, cmd_info("set_begin_end_tactic", "reset the tactic that is automatically applied before every component in a 'begin-end' block",
-                        set_begin_end_cmd));
-}
-}

src/frontends/lean/builtin_cmds.cpp

@@ -38,7 +38,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/structure_cmd.h"
 #include "frontends/lean/print_cmd.h"
 #include "frontends/lean/find_cmd.h"
-#include "frontends/lean/begin_end_ext.h"
+#include "frontends/lean/begin_end_annotation.h"
 #include "frontends/lean/decl_cmds.h"
 #include "frontends/lean/tactic_hint.h"
 #include "frontends/lean/tokens.h"
@@ -650,7 +650,6 @@ void init_cmd_table(cmd_table & r) {
     register_inductive_cmd(r);
     register_structure_cmd(r);
     register_notation_cmds(r);
-    register_begin_end_cmds(r);
     register_tactic_hint_cmd(r);
 }
 

src/frontends/lean/builtin_exprs.cpp

@@ -27,7 +27,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/decl_cmds.h"
 #include "frontends/lean/token_table.h"
 #include "frontends/lean/calc.h"
-#include "frontends/lean/begin_end_ext.h"
+#include "frontends/lean/begin_end_annotation.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/tokens.h"
@@ -151,13 +151,10 @@ static expr parse_begin_end_core(parser & p, pos_info const & start_pos,
     if (!p.has_tactic_decls())
         throw parser_error("invalid 'begin-end' expression, tactic module has not been imported", start_pos);
     p.next();
-    optional<expr> pre_tac = get_begin_end_pre_tactic(p.env());
     buffer<expr> tacs;
     bool first = true;
 
-    auto add_tac = [&](expr tac, pos_info const & pos) {
-        if (pre_tac)
-            tac = p.mk_app({get_and_then_tac_fn(), *pre_tac, tac}, pos);
+    auto add_tac = [&](expr tac) {
         tac = mk_begin_end_element_annotation(tac);
         tacs.push_back(tac);
     };
@@ -224,7 +221,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & start_pos,
                     t      = p.mk_app(get_rexact_tac_fn(), t, pos);
                     t      = p.save_pos(mk_begin_end_element_annotation(t), pos);
                     t      = p.save_pos(mk_begin_end_annotation(t), pos);
-                    add_tac(t, pos);
+                    add_tac(t);
                 } else {
                     p.check_token_next(get_comma_tk(), "invalid 'have' tactic, ',' expected");
                     if (p.curr_is_token(get_from_tk())) {
@@ -235,7 +232,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & start_pos,
                         t      = p.mk_app(get_exact_tac_fn(), t, pos);
                         t      = p.save_pos(mk_begin_end_element_annotation(t), pos);
                         t      = p.save_pos(mk_begin_end_annotation(t), pos);
-                        add_tac(t, pos);
+                        add_tac(t);
                     } else if (p.curr_is_token(get_proof_tk())) {
                         auto pos = p.pos();
                         p.next();
@@ -244,16 +241,15 @@ static expr parse_begin_end_core(parser & p, pos_info const & start_pos,
                         t      = p.mk_app(get_rexact_tac_fn(), t, pos);
                         t      = p.save_pos(mk_begin_end_element_annotation(t), pos);
                         t      = p.save_pos(mk_begin_end_annotation(t), pos);
-                        add_tac(t, pos);
+                        add_tac(t);
                     } else if (p.curr_is_token(get_begin_tk())) {
                         auto pos = p.pos();
                         tacs.push_back(parse_begin_end_core(p, pos, get_end_tk(), true));
                     } else if (p.curr_is_token(get_by_tk())) {
                         // parse: 'by' tactic
-                        auto pos = p.pos();
                         p.next();
                         expr t = p.parse_tactic();
-                        add_tac(t, pos);
+                        add_tac(t);
                     } else {
                         throw parser_error("invalid 'have' tactic, 'by', 'begin', 'proof', or 'from' expected", p.pos());
                     }
@@ -265,11 +261,10 @@ static expr parse_begin_end_core(parser & p, pos_info const & start_pos,
                 auto pos = p.pos();
                 expr t = p.parse_tactic_expr_arg();
                 t      = p.mk_app(get_exact_tac_fn(), t, pos);
-                add_tac(t, pos);
+                add_tac(t);
             } else {
-                auto pos = p.pos();
                 expr t   = p.parse_tactic();
-                add_tac(t, pos);
+                add_tac(t);
             }
         }
     } catch (exception & ex) {
@@ -281,8 +276,6 @@ static expr parse_begin_end_core(parser & p, pos_info const & start_pos,
     p.next();
     if (tacs.empty()) {
         expr tac = get_id_tac_fn();
-        if (pre_tac)
-            tac = p.mk_app({get_and_then_tac_fn(), *pre_tac, tac}, end_pos);
         tac = mk_begin_end_element_annotation(tac);
         tacs.push_back(tac);
     }

src/frontends/lean/calc.cpp

@@ -28,7 +28,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/tokens.h"
-#include "frontends/lean/begin_end_ext.h"
+#include "frontends/lean/begin_end_annotation.h"
 
 namespace lean {
 static name * g_calc_name  = nullptr;

src/frontends/lean/elaborator.cpp

@@ -54,7 +54,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/elaborator.h"
 #include "frontends/lean/calc_proof_elaborator.h"
 #include "frontends/lean/info_tactic.h"
-#include "frontends/lean/begin_end_ext.h"
+#include "frontends/lean/begin_end_annotation.h"
 #include "frontends/lean/elaborator_exception.h"
 #include "frontends/lean/nested_declaration.h"
 #include "frontends/lean/calc.h"

src/frontends/lean/init_module.cpp

@@ -12,7 +12,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/tactic_hint.h"
 #include "frontends/lean/parser_config.h"
 #include "frontends/lean/calc.h"
-#include "frontends/lean/begin_end_ext.h"
+#include "frontends/lean/begin_end_annotation.h"
 #include "frontends/lean/builtin_cmds.h"
 #include "frontends/lean/builtin_exprs.h"
 #include "frontends/lean/builtin_tactics.h"
@@ -51,7 +51,7 @@ void initialize_frontend_lean_module() {
     initialize_tactic_hint();
     initialize_parser_config();
     initialize_calc();
-    initialize_begin_end_ext();
+    initialize_begin_end_annotation();
     initialize_inductive_cmd();
     initialize_structure_cmd();
     initialize_info_manager();
@@ -80,7 +80,7 @@ void finalize_frontend_lean_module() {
     finalize_info_manager();
     finalize_structure_cmd();
     finalize_inductive_cmd();
-    finalize_begin_end_ext();
+    finalize_begin_end_annotation();
     finalize_calc();
     finalize_parser_config();
     finalize_tactic_hint();