From 2279807baf63dc85e27aaef75016ad0f5bd12fc9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 14 Jun 2016 11:28:52 -0700 Subject: [PATCH] chore(frontends/lean): remove #tactic command --- src/frontends/lean/builtin_cmds.cpp | 21 --------------------- src/frontends/lean/token_table.cpp | 2 +- 2 files changed, 1 insertion(+), 22 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 807ca7b715..1ee7125970 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -709,26 +709,6 @@ static environment vm_eval_cmd(parser & p) { return p.env(); } -static environment tactic_cmd(parser & p) { - expr goal; level_param_names goal_ls; - std::tie(goal, goal_ls) = parse_local_expr(p); - p.check_token_next(get_comma_tk(), "invalid #tactic command, ',' expected"); - - name tactic_name("_tactic"); - expr tactic_type = mk_app(mk_constant("tactic"), mk_constant("unit")); - expr tactic = p.parse_expr(); - level_param_names tactic_ls; - std::tie(tactic_type, tactic, tactic_ls) = p.old_elaborate_definition(tactic_name, tactic_type, tactic); - - /* compile tactic */ - environment new_env = compile_expr(p.env(), tactic_name, tactic_ls, tactic_type, tactic); - vm_state s(new_env); - vm_obj initial_state = to_obj(mk_tactic_state_for(p.env(), p.get_options(), local_context(), goal)); - vm_eval_core(s, tactic_name, optional(initial_state)); - - return p.env(); -} - static environment elab_cmd(parser & p) { expr e = p.parse_expr(); expr new_e; level_param_names ls; @@ -766,7 +746,6 @@ void init_cmd_table(cmd_table & r) { add_cmd(r, cmd_info("#normalizer", "(for debugging purposes)", normalizer_cmd)); add_cmd(r, cmd_info("#unify", "(for debugging purposes)", unify_cmd)); add_cmd(r, cmd_info("#compile", "(for debugging purposes)", compile_cmd)); - add_cmd(r, cmd_info("#tactic", "(for debugging purposes)", tactic_cmd)); add_cmd(r, cmd_info("#elab", "(for debugging purposes)", elab_cmd)); add_cmd(r, cmd_info("#simplify", "(for debugging purposes) simplify given expression", simplify_cmd)); add_cmd(r, cmd_info("#defeq_simplify", "(for debugging purposes) defeq-simplify given expression", defeq_simplify_cmd)); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index b59bed7d3b..0d28b8cdb1 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -119,7 +119,7 @@ void init_token_table(token_table & t) { "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "multiple_instances", "find_decl", "attribute", "persistent", "inline", "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", - "#compile", "#simplify", "#normalizer", "#unify", "#tactic", "#defeq_simplify", "#elab", "#compile", nullptr}; + "#compile", "#simplify", "#normalizer", "#unify", "#defeq_simplify", "#elab", "#compile", nullptr}; pair aliases[] = {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},