From 4d41b0316840bf6d971251af355a3e291ecbe0bf Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 16 Feb 2017 23:10:35 +0100 Subject: [PATCH] chore(frontends/lean,library/tactic): remove old tactic_state functions --- src/frontends/lean/elaborator.cpp | 18 +- src/frontends/lean/info_manager.cpp | 6 +- src/frontends/lean/tactic_evaluator.cpp | 18 +- src/frontends/lean/tactic_notation.cpp | 4 +- src/frontends/smt2/parser.cpp | 2 +- src/library/tactic/ac_tactics.cpp | 6 +- src/library/tactic/app_builder_tactics.cpp | 18 +- src/library/tactic/apply_tactic.cpp | 12 +- src/library/tactic/assert_tactic.cpp | 18 +- .../tactic/backward/backward_chaining.cpp | 10 +- .../tactic/backward/backward_lemmas.cpp | 6 +- src/library/tactic/cases_tactic.cpp | 8 +- src/library/tactic/change_tactic.cpp | 10 +- src/library/tactic/clear_tactic.cpp | 12 +- src/library/tactic/congr_lemma_tactics.cpp | 8 +- src/library/tactic/destruct_tactic.cpp | 6 +- src/library/tactic/dsimplify.cpp | 14 +- src/library/tactic/elaborate.cpp | 16 +- src/library/tactic/eqn_lemmas.cpp | 6 +- src/library/tactic/eval.cpp | 10 +- src/library/tactic/exact_tactic.cpp | 8 +- src/library/tactic/fun_info_tactics.cpp | 10 +- src/library/tactic/generalize_tactic.cpp | 8 +- src/library/tactic/induction_tactic.cpp | 8 +- src/library/tactic/intro_tactic.cpp | 18 +- src/library/tactic/kabstract.cpp | 4 +- src/library/tactic/match_tactic.cpp | 14 +- src/library/tactic/norm_num_tactic.cpp | 6 +- src/library/tactic/rename_tactic.cpp | 6 +- src/library/tactic/revert_tactic.cpp | 6 +- src/library/tactic/rewrite_tactic.cpp | 26 +- src/library/tactic/simp_lemmas.cpp | 52 +-- src/library/tactic/simplify.cpp | 20 +- src/library/tactic/smt/congruence_tactics.cpp | 42 +-- src/library/tactic/smt/ematch.cpp | 12 +- src/library/tactic/smt/hinst_lemmas.cpp | 12 +- src/library/tactic/smt/smt_state.cpp | 94 +++--- src/library/tactic/subst_tactic.cpp | 14 +- src/library/tactic/tactic_state.cpp | 297 ++++++------------ src/library/tactic/tactic_state.h | 29 +- src/library/tactic/unfold_tactic.cpp | 30 +- src/library/tactic/user_attribute.cpp | 38 +-- src/library/tactic/vm_monitor.cpp | 12 +- src/library/vm/interaction_state.h | 51 +-- src/library/vm/vm_parser.cpp | 8 +- 45 files changed, 454 insertions(+), 579 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index e6b80e582b..aa9efc2915 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -2945,7 +2945,7 @@ void elaborator::invoke_tactic(expr const & mvar, expr const & tactic) { try { vm_obj r = tactic_evaluator(m_ctx, m_opts, ref)(tactic, s); - if (auto new_s = is_tactic_success(r)) { + if (auto new_s = tactic::is_success(r)) { metavar_context mctx = new_s->mctx(); expr val = mctx.instantiate_mvars(new_s->main()); if (has_expr_metavar(val)) { @@ -3410,15 +3410,15 @@ static expr resolve_local_name(environment const & env, local_context const & lc vm_obj tactic_resolve_local_name(vm_obj const & vm_id, vm_obj const & vm_s) { name const & id = to_name(vm_id); - tactic_state const & s = to_tactic_state(vm_s); + tactic_state const & s = tactic::to_state(vm_s); try { optional g = s.get_main_goal_decl(); if (!g) return mk_no_goals_exception(s); expr src; // dummy bool ignore_aliases = false; - return mk_tactic_success(to_obj(resolve_local_name(s.env(), g->get_context(), id, src, ignore_aliases)), s); + return tactic::mk_success(to_obj(resolve_local_name(s.env(), g->get_context(), id, src, ignore_aliases)), s); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } @@ -3491,10 +3491,10 @@ expr resolve_names(environment const & env, local_context const & lctx, expr con static vm_obj tactic_save_type_info(vm_obj const & _e, vm_obj const & ref, vm_obj const & _s) { expr const & e = to_expr(_e); - tactic_state const & s = to_tactic_state(_s); - if (!get_global_info_manager() || !get_pos_info_provider()) return mk_tactic_success(s); + tactic_state const & s = tactic::to_state(_s); + if (!get_global_info_manager() || !get_pos_info_provider()) return tactic::mk_success(s); auto pos = get_pos_info_provider()->get_pos_info(to_expr(ref)); - if (!pos) return mk_tactic_success(s); + if (!pos) return tactic::mk_success(s); type_context ctx = mk_type_context_for(s); try { expr type = ctx.infer(e); @@ -3504,9 +3504,9 @@ static vm_obj tactic_save_type_info(vm_obj const & _e, vm_obj const & ref, vm_ob else if (is_local(e)) get_global_info_manager()->add_identifier_info(pos->first, pos->second, local_pp_name(e)); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } - return mk_tactic_success(s); + return tactic::mk_success(s); } void initialize_elaborator() { diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index fc3e22ff79..430fef4ba8 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -154,11 +154,11 @@ info_manager * get_global_info_manager() { vm_obj tactic_save_info_thunk(vm_obj const & line, vm_obj const & col, vm_obj const & thunk, vm_obj const & s) { try { if (g_info_m) { - g_info_m->add_vm_obj_format_info(force_to_unsigned(line), force_to_unsigned(col), to_tactic_state(s).env(), thunk); + g_info_m->add_vm_obj_format_info(force_to_unsigned(line), force_to_unsigned(col), tactic::to_state(s).env(), thunk); } - return mk_tactic_success(to_tactic_state(s)); + return tactic::mk_success(tactic::to_state(s)); } catch (exception & ex) { - return mk_tactic_exception(ex, to_tactic_state(s)); + return tactic::mk_exception(ex, tactic::to_state(s)); } } diff --git a/src/frontends/lean/tactic_evaluator.cpp b/src/frontends/lean/tactic_evaluator.cpp index e75cbb6043..b837fa8490 100644 --- a/src/frontends/lean/tactic_evaluator.cpp +++ b/src/frontends/lean/tactic_evaluator.cpp @@ -10,7 +10,6 @@ Author: Leonardo de Moura #include "library/annotation.h" #include "library/util.h" #include "library/constants.h" -#include "kernel/scope_pos_info_provider.h" #include "library/vm/vm_list.h" #include "library/compiler/vm_compiler.h" #include "library/tactic/smt/smt_state.h" @@ -37,23 +36,22 @@ elaborator_exception unsolved_tactic_state(tactic_state const & ts, char const * } void tactic_evaluator::process_failure(vm_state & S, vm_obj const & r) { - pos_info_provider * provider = get_pos_info_provider(); - if (optional ex = is_tactic_exception(S, r)) { - format fmt = std::get<0>(*ex); - optional ref1 = std::get<1>(*ex); - tactic_state s1 = std::get<2>(*ex); - if (ref1 && provider && provider->get_pos_info(*ref1)) - throw elaborator_exception(*ref1, fmt); + if (optional ex = tactic::is_exception(S, r)) { + format fmt = std::get<0>(*ex); + optional pos = std::get<1>(*ex); + tactic_state s1 = std::get<2>(*ex); + if (pos) + throw elaborator_exception(pos, fmt); else throw_unsolved_tactic_state(s1, fmt, m_ref); } /* Do nothing if it is a silent failure */ - lean_assert(is_tactic_silent_exception(r)); + lean_assert(tactic::is_silent_exception(r)); } vm_obj tactic_evaluator::operator()(expr const & tactic, tactic_state const & s) { vm_obj r = tactic::evaluator::operator()(tactic, s); - if (auto s = is_tactic_success(r)) + if (auto s = tactic::is_success(r)) if (s->goals()) throw_unsolved_tactic_state(*s, "tactic failed, there are unsolved goals", m_ref); return r; diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp index 8f01ad4b7f..a1b06f5eed 100644 --- a/src/frontends/lean/tactic_notation.cpp +++ b/src/frontends/lean/tactic_notation.cpp @@ -526,7 +526,7 @@ expr parse_auto_quote_tactic_block(parser & p, unsigned, expr const *, pos_info } vm_obj tactic_report_error(vm_obj const & line, vm_obj const & col, vm_obj const & fmt, vm_obj const & _s) { - tactic_state s = to_tactic_state(_s); + tactic_state s = tactic::to_state(_s); pos_info pos(force_to_unsigned(line), force_to_unsigned(col)); pos_info_provider * pip = get_pos_info_provider(); if (pip) { @@ -535,7 +535,7 @@ vm_obj tactic_report_error(vm_obj const & line, vm_obj const & col, vm_obj const out << mk_pair(to_format(fmt), s.get_options()); out.report(); } - return mk_tactic_success(s); + return tactic::mk_success(s); } void initialize_tactic_notation() { diff --git a/src/frontends/smt2/parser.cpp b/src/frontends/smt2/parser.cpp index 642a5890ee..fe669cbe36 100644 --- a/src/frontends/smt2/parser.cpp +++ b/src/frontends/smt2/parser.cpp @@ -483,7 +483,7 @@ private: vm_state state(env(), ios().get_options()); scope_vm_state scope(state); vm_obj result = state.invoke(get_smt_prove_name(), s); - if (optional s_new = is_tactic_success(result)) { + if (optional s_new = tactic::is_success(result)) { mctx = s_new->mctx(); expr proof = mctx.instantiate_mvars(goal_mvar); if (has_expr_metavar(proof)) { diff --git a/src/library/tactic/ac_tactics.cpp b/src/library/tactic/ac_tactics.cpp index f88bfbb518..0e9e6d84d1 100644 --- a/src/library/tactic/ac_tactics.cpp +++ b/src/library/tactic/ac_tactics.cpp @@ -662,13 +662,13 @@ expr mk_perm_ac_macro(abstract_type_context & ctx, expr const & assoc, expr cons } #define TRY LEAN_TACTIC_TRY -#define CATCH LEAN_TACTIC_CATCH(to_tactic_state(s)) +#define CATCH LEAN_TACTIC_CATCH(tactic::to_state(s)) vm_obj tactic_flat_assoc(vm_obj const & op, vm_obj const & assoc, vm_obj const & e, vm_obj const & s) { TRY; type_context ctx = mk_type_context_for(s); pair p = flat_assoc_fn(ctx, to_expr(op), to_expr(assoc)).flat(to_expr(e)); - return mk_tactic_success(mk_vm_pair(to_obj(p.first), to_obj(p.second)), to_tactic_state(s)); + return tactic::mk_success(mk_vm_pair(to_obj(p.first), to_obj(p.second)), tactic::to_state(s)); CATCH; } @@ -676,7 +676,7 @@ vm_obj tactic_perm_ac(vm_obj const & op, vm_obj const & assoc, vm_obj const & co TRY; type_context ctx = mk_type_context_for(s); expr H = perm_ac_fn(ctx, to_expr(op), to_expr(assoc), to_expr(comm)).perm(to_expr(e1), to_expr(e2)); - return mk_tactic_success(to_obj(H), to_tactic_state(s)); + return tactic::mk_success(to_obj(H), tactic::to_state(s)); CATCH; } diff --git a/src/library/tactic/app_builder_tactics.cpp b/src/library/tactic/app_builder_tactics.cpp index 9be21af81f..d73213ad21 100644 --- a/src/library/tactic/app_builder_tactics.cpp +++ b/src/library/tactic/app_builder_tactics.cpp @@ -14,26 +14,26 @@ Author: Leonardo de Moura namespace lean { vm_obj tactic_mk_app(vm_obj const & c, vm_obj const & as, vm_obj const & tmode, vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); try { type_context ctx = mk_type_context_for(s, to_transparency_mode(tmode)); buffer args; to_buffer_expr(as, args); expr r = mk_app(ctx, to_name(c), args.size(), args.data()); - return mk_tactic_success(to_obj(r), s); + return tactic::mk_success(to_obj(r), s); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } #define MK_APP(CODE) { \ - tactic_state const & s = to_tactic_state(_s); \ + tactic_state const & s = tactic::to_state(_s); \ try { \ type_context ctx = mk_type_context_for(s); \ expr r = CODE; \ - return mk_tactic_success(to_obj(r), s); \ + return tactic::mk_success(to_obj(r), s); \ } catch (exception & ex) { \ - return mk_tactic_exception(ex, s); \ + return tactic::mk_exception(ex, s); \ } \ } @@ -70,7 +70,7 @@ vm_obj tactic_mk_eq_mp(vm_obj const & h1, vm_obj const & h2, vm_obj const & _s) } vm_obj tactic_mk_mapp(vm_obj const & c, vm_obj const & as, vm_obj const & tmode, vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); try { type_context ctx = mk_type_context_for(s, to_transparency_mode(tmode)); buffer mask; @@ -87,9 +87,9 @@ vm_obj tactic_mk_mapp(vm_obj const & c, vm_obj const & as, vm_obj const & tmode, it = tail(it); } expr r = mk_app(ctx, to_name(c), mask.size(), mask.data(), args.data()); - return mk_tactic_success(to_obj(r), s); + return tactic::mk_success(to_obj(r), s); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index daccf9796f..9d4f106c9c 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -84,7 +84,7 @@ optional apply_core(type_context & ctx, bool add_all, bool use_ins msg += pp_indented_expr(s, e_type); return msg; }; - *out_error_obj = mk_tactic_exception(thunk, s); + *out_error_obj = tactic::mk_exception(thunk, s); } return none_tactic_state(); } @@ -106,7 +106,7 @@ optional apply_core(type_context & ctx, bool add_all, bool use_ins msg += space() + format("argument"); return msg; }; - *out_error_obj = mk_tactic_exception(thunk, s); + *out_error_obj = tactic::mk_exception(thunk, s); } return none_tactic_state(); } @@ -118,7 +118,7 @@ optional apply_core(type_context & ctx, bool add_all, bool use_ins msg += space() + format("argument"); return msg; }; - *out_error_obj = mk_tactic_exception(thunk, s); + *out_error_obj = tactic::mk_exception(thunk, s); } return none_tactic_state(); } @@ -158,9 +158,9 @@ vm_obj apply_core(transparency_mode md, bool approx, bool add_all, bool use_inst optional new_s = apply_core(ctx, add_all, use_instances, &error_obj, e, &all_metas, s); if (!new_s) return error_obj; - return mk_tactic_success(to_obj(all_metas), *new_s); + return tactic::mk_success(to_obj(all_metas), *new_s); } catch(exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } @@ -176,7 +176,7 @@ vm_obj tactic_apply_core(vm_obj const & e, vm_obj const & cfg, vm_obj const & s) vm_obj const & approx = cfield(cfg, 1); vm_obj const & all = cfield(cfg, 2); vm_obj const & insts = cfield(cfg, 3); - return apply_core(static_cast(cidx(md)), to_bool(approx), to_bool(all), to_bool(insts), to_expr(e), to_tactic_state(s)); + return apply_core(static_cast(cidx(md)), to_bool(approx), to_bool(all), to_bool(insts), to_expr(e), tactic::to_state(s)); } void initialize_apply_tactic() { diff --git a/src/library/tactic/assert_tactic.cpp b/src/library/tactic/assert_tactic.cpp index bdc7c212a9..9e8cb6b589 100644 --- a/src/library/tactic/assert_tactic.cpp +++ b/src/library/tactic/assert_tactic.cpp @@ -20,7 +20,7 @@ vm_obj assert_define_core(bool is_assert, name const & n, expr const & t, tactic if (is_assert) msg += format("assert"); else msg += format("define"); msg += format(" tactic, expression is not a type"); msg += pp_indented_expr(s, t); - return mk_tactic_exception(msg, s); + return tactic::mk_exception(msg, s); } local_context lctx = g->get_context(); metavar_context mctx = ctx.mctx(); @@ -37,15 +37,15 @@ vm_obj assert_define_core(bool is_assert, name const & n, expr const & t, tactic } mctx.assign(head(s.goals()), new_val); list new_gs = cons(new_M_1, cons(new_M_2, tail(s.goals()))); - return mk_tactic_success(set_mctx_goals(s, mctx, new_gs)); + return tactic::mk_success(set_mctx_goals(s, mctx, new_gs)); } vm_obj tactic_assert_core(vm_obj const & n, vm_obj const & t, vm_obj const & s) { - return assert_define_core(true, to_name(n), to_expr(t), to_tactic_state(s)); + return assert_define_core(true, to_name(n), to_expr(t), tactic::to_state(s)); } vm_obj tactic_define_core(vm_obj const & n, vm_obj const & t, vm_obj const & s) { - return assert_define_core(false, to_name(n), to_expr(t), to_tactic_state(s)); + return assert_define_core(false, to_name(n), to_expr(t), tactic::to_state(s)); } vm_obj assertv_definev_core(bool is_assert, name const & n, expr const & t, expr const & v, tactic_state const & s) { @@ -63,7 +63,7 @@ vm_obj assertv_definev_core(bool is_assert, name const & n, expr const & t, expr msg += pp_indented_expr(s, t); return msg; }; - return mk_tactic_exception(thunk, s); + return tactic::mk_exception(thunk, s); } local_context lctx = g->get_context(); metavar_context mctx = ctx.mctx(); @@ -79,20 +79,20 @@ vm_obj assertv_definev_core(bool is_assert, name const & n, expr const & t, expr } mctx.assign(head(s.goals()), new_val); list new_gs = cons(new_M, tail(s.goals())); - return mk_tactic_success(set_mctx_goals(s, mctx, new_gs)); + return tactic::mk_success(set_mctx_goals(s, mctx, new_gs)); } vm_obj tactic_assertv_core(vm_obj const & n, vm_obj const & e, vm_obj const & pr, vm_obj const & s) { - return assertv_definev_core(true, to_name(n), to_expr(e), to_expr(pr), to_tactic_state(s)); + return assertv_definev_core(true, to_name(n), to_expr(e), to_expr(pr), tactic::to_state(s)); } vm_obj tactic_definev_core(vm_obj const & n, vm_obj const & e, vm_obj const & pr, vm_obj const & s) { - return assertv_definev_core(false, to_name(n), to_expr(e), to_expr(pr), to_tactic_state(s)); + return assertv_definev_core(false, to_name(n), to_expr(e), to_expr(pr), tactic::to_state(s)); } vm_obj assertv_definev(bool is_assert, name const & n, expr const & t, expr const & v, tactic_state const & s) { vm_obj r = assertv_definev_core(is_assert, n, t, v, s); - if (optional const & s2 = is_tactic_success(r)) { + if (optional const & s2 = tactic::is_success(r)) { return intro(n, *s2); } else { return r; diff --git a/src/library/tactic/backward/backward_chaining.cpp b/src/library/tactic/backward/backward_chaining.cpp index 1cf3ba6524..645d594c39 100644 --- a/src/library/tactic/backward/backward_chaining.cpp +++ b/src/library/tactic/backward/backward_chaining.cpp @@ -69,7 +69,7 @@ struct back_chaining_fn { lbool invoke_pre_tactic() { vm_obj r = invoke_tactic(m_pre_tactic); - if (optional new_s = is_tactic_success(r)) { + if (optional new_s = tactic::is_success(r)) { if (new_s->goals()) { return l_undef; } else { @@ -85,7 +85,7 @@ struct back_chaining_fn { bool invoke_leaf_tactic() { vm_obj r = invoke_tactic(m_leaf_tactic); - if (optional new_s = is_tactic_success(r)) { + if (optional new_s = tactic::is_success(r)) { m_state = set_goals(*new_s, tail(m_state.goals())); return true; } else { @@ -166,9 +166,9 @@ struct back_chaining_fn { m_state = set_goals(m_initial_state, to_list(head(goals))); if (run()) { tactic_state final_state = set_goals(m_state, tail(goals)); - return mk_tactic_success(final_state); + return tactic::mk_success(final_state); } else { - return mk_tactic_exception("back_chaining failed, use command 'set_option trace.tactic.back_chaining true' to obtain more details", m_initial_state); + return tactic::mk_exception("back_chaining failed, use command 'set_option trace.tactic.back_chaining true' to obtain more details", m_initial_state); } } }; @@ -185,7 +185,7 @@ vm_obj tactic_backward_chaining(vm_obj const & md, vm_obj const & use_instances, vm_obj const & lemmas, vm_obj const & s) { return back_chaining(to_transparency_mode(md), to_bool(use_instances), force_to_unsigned(max_depth), - pre_tactics, leaf_tactic, to_backward_lemmas(lemmas), to_tactic_state(s)); + pre_tactics, leaf_tactic, to_backward_lemmas(lemmas), tactic::to_state(s)); } void initialize_backward_chaining() { diff --git a/src/library/tactic/backward/backward_lemmas.cpp b/src/library/tactic/backward/backward_lemmas.cpp index 35e9a64cf6..70d1c26f25 100644 --- a/src/library/tactic/backward/backward_lemmas.cpp +++ b/src/library/tactic/backward/backward_lemmas.cpp @@ -150,20 +150,20 @@ vm_obj to_obj(backward_lemma_index const & idx) { vm_obj tactic_mk_backward_lemmas(vm_obj const & m, vm_obj const & s) { type_context ctx = mk_type_context_for(s, m); - return mk_tactic_success(to_obj(backward_lemma_index(ctx)), to_tactic_state(s)); + return tactic::mk_success(to_obj(backward_lemma_index(ctx)), tactic::to_state(s)); } vm_obj tactic_backward_lemmas_insert(vm_obj const & m, vm_obj const & lemmas, vm_obj const & lemma, vm_obj const & s) { type_context ctx = mk_type_context_for(s, m); backward_lemma_index new_lemmas = to_backward_lemmas(lemmas); new_lemmas.insert(ctx, to_expr(lemma)); - return mk_tactic_success(to_obj(new_lemmas), to_tactic_state(s)); + return tactic::mk_success(to_obj(new_lemmas), tactic::to_state(s)); } vm_obj tactic_backward_lemmas_find(vm_obj const & lemmas, vm_obj const & h, vm_obj const & s) { list r = map2(to_backward_lemmas(lemmas).find(head_index(to_expr(h))), [](backward_lemma const & lemma) -> expr { return lemma.to_bare_expr(); }); - return mk_tactic_success(to_obj(r), to_tactic_state(s)); + return tactic::mk_success(to_obj(r), tactic::to_state(s)); } void initialize_backward_lemmas() { diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp index e38a633dbc..0171d3c9e1 100644 --- a/src/library/tactic/cases_tactic.cpp +++ b/src/library/tactic/cases_tactic.cpp @@ -486,7 +486,7 @@ cases(environment const & env, options const & opts, transparency_mode const & m } vm_obj tactic_cases_core(vm_obj const & H, vm_obj const & ns, vm_obj const & m, vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); try { if (!s.goals()) return mk_no_goals_exception(s); list ids = to_list_name(ns); @@ -507,11 +507,11 @@ vm_obj tactic_cases_core(vm_obj const & H, vm_obj const & ns, vm_obj const & m, substs = tail(substs); constrs = tail(constrs); } - return mk_tactic_success(to_obj(info_objs), set_mctx_goals(s, mctx, append(info.first, tail(s.goals())))); + return tactic::mk_success(to_obj(info_objs), set_mctx_goals(s, mctx, append(info.first, tail(s.goals())))); } catch (cases_tactic_exception & ex) { - return mk_tactic_exception(ex.what(), ex.m_state); + return tactic::mk_exception(ex.what(), ex.m_state); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } diff --git a/src/library/tactic/change_tactic.cpp b/src/library/tactic/change_tactic.cpp index d1c0a46a98..27d90aeddb 100644 --- a/src/library/tactic/change_tactic.cpp +++ b/src/library/tactic/change_tactic.cpp @@ -15,7 +15,7 @@ vm_obj change(expr const & e, tactic_state const & s) { try { optional g = s.get_main_goal_decl(); if (!g) return mk_no_goals_exception(s); - if (e == g->get_type()) return mk_tactic_success(s); + if (e == g->get_type()) return tactic::mk_success(s); type_context ctx = mk_type_context_for(s); if (ctx.is_def_eq(e, g->get_type())) { auto mctx = ctx.mctx(); @@ -30,7 +30,7 @@ vm_obj change(expr const & e, tactic_state const & s) { expr pr = mk_id_locked(ctx, g->get_type(), new_M); mctx.assign(head(s.goals()), pr); list new_gs(new_M, tail(s.goals())); - return mk_tactic_success(set_mctx_goals(s, mctx, new_gs)); + return tactic::mk_success(set_mctx_goals(s, mctx, new_gs)); } else { auto thunk = [=]() { format m("tactic.change failed, given type"); @@ -39,15 +39,15 @@ vm_obj change(expr const & e, tactic_state const & s) { m += pp_indented_expr(s, g->get_type()); return m; }; - return mk_tactic_exception(thunk, s); + return tactic::mk_exception(thunk, s); } } catch (exception & e) { - return mk_tactic_exception(e, s); + return tactic::mk_exception(e, s); } } vm_obj tactic_change(vm_obj const & e, vm_obj const & s) { - return change(to_expr(e), to_tactic_state(s)); + return change(to_expr(e), tactic::to_state(s)); } void initialize_change_tactic() { diff --git a/src/library/tactic/clear_tactic.cpp b/src/library/tactic/clear_tactic.cpp index e8936753b8..392da57b00 100644 --- a/src/library/tactic/clear_tactic.cpp +++ b/src/library/tactic/clear_tactic.cpp @@ -56,9 +56,9 @@ vm_obj clear(expr const & H, tactic_state const & s) { if (!mvar) return mk_no_goals_exception(s); metavar_context mctx = s.mctx(); expr new_mvar = clear(mctx, *mvar, H); - return mk_tactic_success(set_mctx_goals(s, mctx, cons(new_mvar, tail(s.goals())))); + return tactic::mk_success(set_mctx_goals(s, mctx, cons(new_mvar, tail(s.goals())))); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } @@ -69,16 +69,16 @@ vm_obj clear_internal(name const & n, tactic_state const & s) { local_context lctx = g->get_context(); optional d = lctx.find_local_decl(n); if (!d) - return mk_tactic_exception(sstream() << "clear tactic failed, unknown '" << n << "' hypothesis", s); + return tactic::mk_exception(sstream() << "clear tactic failed, unknown '" << n << "' hypothesis", s); return clear(d->mk_ref(), s); } vm_obj tactic_clear(vm_obj const & e0, vm_obj const & s) { expr const & e = to_expr(e0); if (!is_local(e)) - return mk_tactic_exception(sstream() << "clear tactic failed, given expression is not a local constant", - to_tactic_state(s)); - return clear(e, to_tactic_state(s)); + return tactic::mk_exception(sstream() << "clear tactic failed, given expression is not a local constant", + tactic::to_state(s)); + return clear(e, tactic::to_state(s)); } void initialize_clear_tactic() { diff --git a/src/library/tactic/congr_lemma_tactics.cpp b/src/library/tactic/congr_lemma_tactics.cpp index 0416db3257..d5e83b2f55 100644 --- a/src/library/tactic/congr_lemma_tactics.cpp +++ b/src/library/tactic/congr_lemma_tactics.cpp @@ -30,15 +30,15 @@ vm_obj to_obj(congr_lemma const & c) { static vm_obj mk_result(optional const & l, vm_obj const & s) { if (l) - return mk_tactic_success(to_obj(*l), to_tactic_state(s)); + return tactic::mk_success(to_obj(*l), tactic::to_state(s)); else - return mk_tactic_exception("failed to generate congruence lemma, " + return tactic::mk_exception("failed to generate congruence lemma, " "use 'set_option trace.congr_lemma true' to obtain additional information", - to_tactic_state(s)); + tactic::to_state(s)); } #define TRY LEAN_TACTIC_TRY -#define CATCH LEAN_TACTIC_CATCH(to_tactic_state(s)) +#define CATCH LEAN_TACTIC_CATCH(tactic::to_state(s)) vm_obj tactic_mk_congr_lemma_simp(vm_obj const & fn, vm_obj const & nargs, vm_obj const & m, vm_obj const & s) { TRY; diff --git a/src/library/tactic/destruct_tactic.cpp b/src/library/tactic/destruct_tactic.cpp index 7955841644..6be1431483 100644 --- a/src/library/tactic/destruct_tactic.cpp +++ b/src/library/tactic/destruct_tactic.cpp @@ -155,13 +155,13 @@ tactic_state destruct(transparency_mode md, expr const & e, tactic_state const & } vm_obj tactic_destruct(vm_obj const & e, vm_obj const & md, vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); try { if (!s.goals()) return mk_no_goals_exception(s); tactic_state new_s = destruct(to_transparency_mode(md), to_expr(e), s); - return mk_tactic_success(new_s); + return tactic::mk_success(new_s); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } diff --git a/src/library/tactic/dsimplify.cpp b/src/library/tactic/dsimplify.cpp index bd021b582c..9ac24a803b 100644 --- a/src/library/tactic/dsimplify.cpp +++ b/src/library/tactic/dsimplify.cpp @@ -270,7 +270,7 @@ class tactic_dsimplify_fn : public dsimplify_core_fn { optional> invoke_fn(vm_obj const & fn, expr const & e) { m_s = set_mctx_lctx_dcs(m_s, m_ctx.mctx(), m_ctx.lctx(), m_defeq_canonizer.get_state()); vm_obj r = invoke(fn, m_a, to_obj(e), to_obj(m_s)); - if (optional new_s = is_tactic_success(r)) { + if (optional new_s = tactic::is_success(r)) { m_s = *new_s; m_ctx.set_mctx(m_s.mctx()); m_defeq_canonizer.set_state(m_s.dcs()); @@ -309,7 +309,7 @@ public: vm_obj tactic_dsimplify_core(vm_obj const &, vm_obj const & a, vm_obj const & max_steps, vm_obj const & visit_instances, vm_obj const & pre, vm_obj const & post, vm_obj const & e, vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); try { type_context ctx = mk_type_context_for(s, transparency_mode::Reducible); defeq_can_state dcs = s.dcs(); @@ -317,15 +317,15 @@ vm_obj tactic_dsimplify_core(vm_obj const &, vm_obj const & a, to_bool(visit_instances), a, pre, post, s); expr new_e = F(to_expr(e)); tactic_state new_s = set_mctx_dcs(s, F.mctx(), dcs); - return mk_tactic_success(mk_vm_pair(F.get_a(), to_obj(new_e)), new_s); + return tactic::mk_success(mk_vm_pair(F.get_a(), to_obj(new_e)), new_s); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } vm_obj simp_lemmas_dsimplify_core(vm_obj const & max_steps, vm_obj const & visit_instances, vm_obj const & lemmas, vm_obj const & e, vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); try { type_context ctx = mk_type_context_for(s, transparency_mode::Reducible); defeq_can_state dcs = s.dcs(); @@ -337,9 +337,9 @@ vm_obj simp_lemmas_dsimplify_core(vm_obj const & max_steps, vm_obj const & visit to_bool(visit_instances), dlemmas, use_eta); expr new_e = F(to_expr(e)); tactic_state new_s = set_mctx_dcs(s, F.mctx(), dcs); - return mk_tactic_success(to_obj(new_e), new_s); + return tactic::mk_success(to_obj(new_e), new_s); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } diff --git a/src/library/tactic/elaborate.cpp b/src/library/tactic/elaborate.cpp index 68716cadac..b887a76c16 100644 --- a/src/library/tactic/elaborate.cpp +++ b/src/library/tactic/elaborate.cpp @@ -37,7 +37,7 @@ static bool report_failure(elaborator_exception const & ex, expr const & mvar, c } vm_obj tactic_to_expr_core(vm_obj const & qe, vm_obj const & relaxed, vm_obj const & report_errors, vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); optional g = s.get_main_goal_decl(); if (!g) return mk_no_goals_exception(s); metavar_context mctx = s.mctx(); @@ -66,22 +66,22 @@ vm_obj tactic_to_expr_core(vm_obj const & qe, vm_obj const & relaxed, vm_obj con return true; }); list new_gs = cons(head(s.goals()), to_list(new_goals.begin(), new_goals.end(), tail(s.goals()))); - return mk_tactic_success(to_obj(r), set_env_mctx_goals(s, env, mctx, new_gs)); + return tactic::mk_success(to_obj(r), set_env_mctx_goals(s, env, mctx, new_gs)); } else { - return mk_tactic_success(to_obj(r), set_env_mctx(s, env, mctx)); + return tactic::mk_success(to_obj(r), set_env_mctx(s, env, mctx)); } } catch (failed_to_synthesize_placeholder_exception & ex) { if (to_bool(report_errors) && report_failure(ex, ex.get_mvar(), "context:", ex.get_tactic_state())) - return mk_tactic_silent_exception(s); + return tactic::mk_silent_exception(s); else - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } catch (elaborator_exception & ex) { if (to_bool(report_errors) && report_failure(ex, *s.get_main_goal(), "state:", s)) - return mk_tactic_silent_exception(s); + return tactic::mk_silent_exception(s); else - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } diff --git a/src/library/tactic/eqn_lemmas.cpp b/src/library/tactic/eqn_lemmas.cpp index 65797ee9d5..6ffe57f2a3 100644 --- a/src/library/tactic/eqn_lemmas.cpp +++ b/src/library/tactic/eqn_lemmas.cpp @@ -134,11 +134,11 @@ void get_ext_eqn_lemmas_for(environment const & env, name const & cname, buffer< vm_obj tactic_get_eqn_lemmas_for(vm_obj const & all, vm_obj const & n, vm_obj const & s) { buffer result; if (to_bool(all)) { - get_ext_eqn_lemmas_for(to_tactic_state(s).env(), to_name(n), result); + get_ext_eqn_lemmas_for(tactic::to_state(s).env(), to_name(n), result); } else { - get_eqn_lemmas_for(to_tactic_state(s).env(), to_name(n), result); + get_eqn_lemmas_for(tactic::to_state(s).env(), to_name(n), result); } - return mk_tactic_success(to_obj(result), to_tactic_state(s)); + return tactic::mk_success(to_obj(result), tactic::to_state(s)); } bool has_eqn_lemmas(environment const & env, name const & cname) { diff --git a/src/library/tactic/eval.cpp b/src/library/tactic/eval.cpp index b9ec36ad67..ed5c0d3112 100644 --- a/src/library/tactic/eval.cpp +++ b/src/library/tactic/eval.cpp @@ -17,13 +17,13 @@ static vm_obj eval(expr const & A, expr a, tactic_state const & s) { metavar_context mctx = s.mctx(); a = mctx.instantiate_mvars(a); if (has_local(a) || !closed(a)) - return mk_tactic_exception("invalid eval_expr, expression must be closed", s); + return tactic::mk_exception("invalid eval_expr, expression must be closed", s); if (is_constant(a)) { type_context ctx = mk_type_context_for(s); if (!ctx.is_def_eq(A, ctx.infer(a))) - return mk_tactic_exception("invalid eval_expr, type mismatch", s); + return tactic::mk_exception("invalid eval_expr, type mismatch", s); vm_obj r = get_vm_state().get_constant(const_name(a)); - return mk_tactic_success(r, s); + return tactic::mk_success(r, s); } else { vm_state & S = get_vm_state(); environment aux_env = S.env(); @@ -33,13 +33,13 @@ static vm_obj eval(expr const & A, expr a, tactic_state const & s) { aux_env = vm_compile(aux_env, aux_env.get(eval_aux_name)); S.update_env(aux_env); vm_obj r = S.get_constant(eval_aux_name); - return mk_tactic_success(r, s); + return tactic::mk_success(r, s); } LEAN_TACTIC_CATCH(s); } static vm_obj tactic_eval_expr(vm_obj const &, vm_obj const & A, vm_obj const & a, vm_obj const & s) { - return eval(to_expr(A), to_expr(a), to_tactic_state(s)); + return eval(to_expr(A), to_expr(a), tactic::to_state(s)); } void initialize_eval() { diff --git a/src/library/tactic/exact_tactic.cpp b/src/library/tactic/exact_tactic.cpp index bc169751f2..172ff0eaa7 100644 --- a/src/library/tactic/exact_tactic.cpp +++ b/src/library/tactic/exact_tactic.cpp @@ -25,18 +25,18 @@ vm_obj exact(expr const & e, transparency_mode const & m, tactic_state const & s r += nest(indent, line() + pp_expr(s, g->get_type())); return r; }; - return mk_tactic_exception(thunk, s); + return tactic::mk_exception(thunk, s); } auto mctx = ctx.mctx(); mctx.assign(head(s.goals()), e); - return mk_tactic_success(set_mctx_goals(s, mctx, tail(s.goals()))); + return tactic::mk_success(set_mctx_goals(s, mctx, tail(s.goals()))); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } vm_obj tactic_exact(vm_obj const & e, vm_obj const & m, vm_obj const & s) { - return exact(to_expr(e), to_transparency_mode(m), to_tactic_state(s)); + return exact(to_expr(e), to_transparency_mode(m), tactic::to_state(s)); } void initialize_exact_tactic() { diff --git a/src/library/tactic/fun_info_tactics.cpp b/src/library/tactic/fun_info_tactics.cpp index 34a0a63757..7e34904627 100644 --- a/src/library/tactic/fun_info_tactics.cpp +++ b/src/library/tactic/fun_info_tactics.cpp @@ -50,14 +50,14 @@ vm_obj to_obj(list const & ls) { } #define TRY LEAN_TACTIC_TRY -#define CATCH LEAN_TACTIC_CATCH(to_tactic_state(s)) +#define CATCH LEAN_TACTIC_CATCH(tactic::to_state(s)) static vm_obj mk_result(fun_info const & info, vm_obj const & s) { - return mk_tactic_success(to_obj(info), to_tactic_state(s)); + return tactic::mk_success(to_obj(info), tactic::to_state(s)); } static vm_obj mk_result(list const & info, vm_obj const & s) { - return mk_tactic_success(to_obj(info), to_tactic_state(s)); + return tactic::mk_success(to_obj(info), tactic::to_state(s)); } vm_obj tactic_get_fun_info(vm_obj const & fn, vm_obj const & n, vm_obj const & m, vm_obj const & s) { @@ -92,8 +92,8 @@ vm_obj tactic_get_spec_subsingleton_info(vm_obj const & app, vm_obj const & m, v vm_obj tactic_get_spec_prefix_size(vm_obj const & fn, vm_obj const & n, vm_obj const & m, vm_obj const & s) { TRY; type_context ctx = mk_type_context_for(s, m); - return mk_tactic_success(mk_vm_nat(get_specialization_prefix_size(ctx, to_expr(fn), force_to_unsigned(n, 0))), - to_tactic_state(s)); + return tactic::mk_success(mk_vm_nat(get_specialization_prefix_size(ctx, to_expr(fn), force_to_unsigned(n, 0))), + tactic::to_state(s)); CATCH; } diff --git a/src/library/tactic/generalize_tactic.cpp b/src/library/tactic/generalize_tactic.cpp index bad0ac5018..f2e8879330 100644 --- a/src/library/tactic/generalize_tactic.cpp +++ b/src/library/tactic/generalize_tactic.cpp @@ -19,22 +19,22 @@ vm_obj generalize(transparency_mode m, expr const & e, name const & id, tactic_s expr target = ctx.instantiate_mvars(g->get_type()); expr target_abst = kabstract(ctx, target, e); if (closed(target_abst)) - return mk_tactic_exception("generalize tactic failed, failed to find expression in the target", s); + return tactic::mk_exception("generalize tactic failed, failed to find expression in the target", s); expr e_type = ctx.infer(e); expr new_type = mk_pi(id, e_type, target_abst); try { check(ctx, new_type); } catch (exception & ex) { - return mk_tactic_exception(nested_exception("generalize tactic failed, result is not type correct", ex), s); + return tactic::mk_exception(nested_exception("generalize tactic failed, result is not type correct", ex), s); } metavar_context mctx = ctx.mctx(); expr mvar = mctx.mk_metavar_decl(g->get_context(), new_type); mctx.assign(head(s.goals()), mk_app(mvar, e)); - return mk_tactic_success(set_mctx_goals(s, mctx, cons(mvar, tail(s.goals())))); + return tactic::mk_success(set_mctx_goals(s, mctx, cons(mvar, tail(s.goals())))); } vm_obj tactic_generalize(vm_obj const & e, vm_obj const & n, vm_obj const & m, vm_obj const & s) { - return generalize(to_transparency_mode(m), to_expr(e), to_name(n), to_tactic_state(s)); + return generalize(to_transparency_mode(m), to_expr(e), to_name(n), tactic::to_state(s)); } void initialize_generalize_tactic() { diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp index 996ee4d68f..35186235d9 100644 --- a/src/library/tactic/induction_tactic.cpp +++ b/src/library/tactic/induction_tactic.cpp @@ -316,7 +316,7 @@ list induction(environment const & env, options const & opts, transparency vm_obj induction_tactic_core(transparency_mode const & m, expr const & H, name const & rec_name, list const & ns, tactic_state const & s) { if (!s.goals()) return mk_no_goals_exception(s); - if (!is_local(H)) return mk_tactic_exception("induction tactic failed, argument is not a hypothesis", s); + if (!is_local(H)) return tactic::mk_exception("induction tactic failed, argument is not a hypothesis", s); try { metavar_context mctx = s.mctx(); list tmp_ns = ns; @@ -338,14 +338,14 @@ vm_obj induction_tactic_core(transparency_mode const & m, expr const & H, name c hyps = tail(hyps); substs = tail(substs); } - return mk_tactic_success(to_obj(info), new_s); + return tactic::mk_success(to_obj(info), new_s); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } vm_obj tactic_induction(vm_obj const & H, vm_obj const & rec, vm_obj const & ns, vm_obj const & m, vm_obj const & s) { - return induction_tactic_core(to_transparency_mode(m), to_expr(H), to_name(rec), to_list_name(ns), to_tactic_state(s)); + return induction_tactic_core(to_transparency_mode(m), to_expr(H), to_name(rec), to_list_name(ns), tactic::to_state(s)); } void initialize_induction_tactic() { diff --git a/src/library/tactic/intro_tactic.cpp b/src/library/tactic/intro_tactic.cpp index 8852399d2e..eb4c2ac7b7 100644 --- a/src/library/tactic/intro_tactic.cpp +++ b/src/library/tactic/intro_tactic.cpp @@ -114,13 +114,13 @@ optional intron(unsigned n, tactic_state const & s) { } vm_obj tactic_intron(vm_obj const & num, vm_obj const & s) { - optional g = to_tactic_state(s).get_main_goal_decl(); - if (!g) return mk_no_goals_exception(to_tactic_state(s)); + optional g = tactic::to_state(s).get_main_goal_decl(); + if (!g) return mk_no_goals_exception(tactic::to_state(s)); buffer new_Hs; - if (auto new_s = intron(force_to_unsigned(num, 0), to_tactic_state(s), new_Hs)) - return mk_tactic_success(*new_s); + if (auto new_s = intron(force_to_unsigned(num, 0), tactic::to_state(s), new_Hs)) + return tactic::mk_success(*new_s); else - return mk_tactic_exception("intron tactic failed, insufficient binders", to_tactic_state(s)); + return tactic::mk_exception("intron tactic failed, insufficient binders", tactic::to_state(s)); } vm_obj intro(name const & n, tactic_state const & s) { @@ -131,7 +131,7 @@ vm_obj intro(name const & n, tactic_state const & s) { if (!is_pi(type) && !is_let(type)) { type = ctx.whnf(type); if (!is_pi(type)) - return mk_tactic_exception("intro tactic failed, Pi/let expression expected", s); + return tactic::mk_exception("intro tactic failed, Pi/let expression expected", s); } local_context lctx = g->get_context(); metavar_context mctx = ctx.mctx(); @@ -143,7 +143,7 @@ vm_obj intro(name const & n, tactic_state const & s) { expr new_val = mk_lambda(n1, binding_domain(type), mk_delayed_abstraction(new_M, mlocal_name(H))); mctx.assign(head(s.goals()), new_val); list new_gs(new_M, tail(s.goals())); - return mk_tactic_success(to_obj(H), set_mctx_goals(s, mctx, new_gs)); + return tactic::mk_success(to_obj(H), set_mctx_goals(s, mctx, new_gs)); } else { lean_assert(is_let(type)); name n1 = n == "_" ? lctx.get_unused_name(let_name(type)) : n; @@ -153,12 +153,12 @@ vm_obj intro(name const & n, tactic_state const & s) { expr new_val = mk_let(n1, let_type(type), let_value(type), mk_delayed_abstraction(new_M, mlocal_name(H))); mctx.assign(head(s.goals()), new_val); list new_gs(new_M, tail(s.goals())); - return mk_tactic_success(to_obj(H), set_mctx_goals(s, mctx, new_gs)); + return tactic::mk_success(to_obj(H), set_mctx_goals(s, mctx, new_gs)); } } vm_obj tactic_intro(vm_obj const & n, vm_obj const & s) { - return intro(to_name(n), to_tactic_state(s)); + return intro(to_name(n), tactic::to_state(s)); } void initialize_intro_tactic() { diff --git a/src/library/tactic/kabstract.cpp b/src/library/tactic/kabstract.cpp index a7d52a5991..7cd11d91d6 100644 --- a/src/library/tactic/kabstract.cpp +++ b/src/library/tactic/kabstract.cpp @@ -204,9 +204,9 @@ bool kdepends_on(type_context & ctx, expr const & e, expr const & t) { vm_obj tactic_kdepends_on(vm_obj const & e, vm_obj const & t, vm_obj const & md, vm_obj const & s) { try { type_context ctx = mk_type_context_for(s, md); - return mk_tactic_success(mk_vm_bool(kdepends_on(ctx, to_expr(e), to_expr(t))), to_tactic_state(s)); + return tactic::mk_success(mk_vm_bool(kdepends_on(ctx, to_expr(e), to_expr(t))), tactic::to_state(s)); } catch (exception & ex) { - return mk_tactic_exception(ex, to_tactic_state(s)); + return tactic::mk_exception(ex, tactic::to_state(s)); } } diff --git a/src/library/tactic/match_tactic.cpp b/src/library/tactic/match_tactic.cpp index 6024e0b49e..09f0ccaef4 100644 --- a/src/library/tactic/match_tactic.cpp +++ b/src/library/tactic/match_tactic.cpp @@ -122,15 +122,15 @@ struct mk_pattern_fn { }; #define TRY LEAN_TACTIC_TRY -#define CATCH LEAN_TACTIC_CATCH(to_tactic_state(s)) +#define CATCH LEAN_TACTIC_CATCH(tactic::to_state(s)) /* meta_constant mk_pattern : list level → list expr → expr → list expr → tactic pattern */ vm_obj tactic_mk_pattern(vm_obj const & ls, vm_obj const & es, vm_obj const & t, vm_obj const & os, vm_obj const & s) { TRY; - vm_obj pattern = mk_pattern_fn(to_tactic_state(s)).mk(to_list_level(ls), to_list_expr(es), to_expr(t), to_list_expr(os)); - return mk_tactic_success(pattern, to_tactic_state(s)); + vm_obj pattern = mk_pattern_fn(tactic::to_state(s)).mk(to_list_level(ls), to_list_expr(es), to_expr(t), to_list_expr(os)); + return tactic::mk_success(pattern, tactic::to_state(s)); CATCH; } @@ -146,19 +146,19 @@ vm_obj tactic_match_pattern_core(vm_obj const & m, vm_obj const & p, vm_obj cons if (ctx.is_def_eq(t, to_expr(e))) { for (unsigned i = 0; i < nuvars; i++) { if (!ctx.get_tmp_uvar_assignment(i)) - return mk_tactic_exception(sstream() << "match_pattern failed, universe meta-variable #" << i << " has not been assigned.", to_tactic_state(s)); + return tactic::mk_exception(sstream() << "match_pattern failed, universe meta-variable #" << i << " has not been assigned.", tactic::to_state(s)); } for (unsigned i = 0; i < nmvars; i++) { if (!ctx.get_tmp_mvar_assignment(i)) - return mk_tactic_exception(sstream() << "match_pattern failed, meta-variable #" << i << " has not been assigned.", to_tactic_state(s)); + return tactic::mk_exception(sstream() << "match_pattern failed, meta-variable #" << i << " has not been assigned.", tactic::to_state(s)); } buffer inst_os; for (expr const & o : os) { inst_os.push_back(ctx.instantiate_mvars(o)); } - return mk_tactic_success(to_obj(to_list(inst_os)), to_tactic_state(s)); + return tactic::mk_success(to_obj(to_list(inst_os)), tactic::to_state(s)); } else { - return mk_tactic_exception("match_pattern failed", to_tactic_state(s)); + return tactic::mk_exception("match_pattern failed", tactic::to_state(s)); } CATCH; } diff --git a/src/library/tactic/norm_num_tactic.cpp b/src/library/tactic/norm_num_tactic.cpp index 765bb91ecc..93a0c2ecfb 100644 --- a/src/library/tactic/norm_num_tactic.cpp +++ b/src/library/tactic/norm_num_tactic.cpp @@ -10,13 +10,13 @@ Authors: Robert Y. Lewis, Leonardo de Moura namespace lean { vm_obj tactic_norm_num(vm_obj const & e, vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); type_context ctx = mk_type_context_for(s); try { pair p = mk_norm_num(ctx, to_expr(e)); - return mk_tactic_success(mk_vm_pair(to_obj(p.first), to_obj(p.second)), s); + return tactic::mk_success(mk_vm_pair(to_obj(p.first), to_obj(p.second)), s); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } diff --git a/src/library/tactic/rename_tactic.cpp b/src/library/tactic/rename_tactic.cpp index 6a1b9d827c..78f59dcc38 100644 --- a/src/library/tactic/rename_tactic.cpp +++ b/src/library/tactic/rename_tactic.cpp @@ -14,15 +14,15 @@ vm_obj rename(name const & from, name const & to, tactic_state const & s) { metavar_context mctx = s.mctx(); local_context lctx = g->get_context(); if (!lctx.rename_user_name(from, to)) { - return mk_tactic_exception(sstream() << "rename tactic failed, unknown '" << from << "' hypothesis", s); + return tactic::mk_exception(sstream() << "rename tactic failed, unknown '" << from << "' hypothesis", s); } expr new_g = mctx.mk_metavar_decl(lctx, g->get_type()); mctx.assign(head(s.goals()), new_g); - return mk_tactic_success(set_mctx_goals(s, mctx, cons(new_g, tail(s.goals())))); + return tactic::mk_success(set_mctx_goals(s, mctx, cons(new_g, tail(s.goals())))); } vm_obj tactic_rename(vm_obj const & from, vm_obj const & to, vm_obj const & s) { - return rename(to_name(from), to_name(to), to_tactic_state(s)); + return rename(to_name(from), to_name(to), tactic::to_state(s)); } void initialize_rename_tactic() { diff --git a/src/library/tactic/revert_tactic.cpp b/src/library/tactic/revert_tactic.cpp index 4623d740ef..79a2d5e7d1 100644 --- a/src/library/tactic/revert_tactic.cpp +++ b/src/library/tactic/revert_tactic.cpp @@ -35,16 +35,16 @@ vm_obj revert(list const & ls, tactic_state const & s) { if (lctx.find_local_decl(l)) { locals.push_back(l); } else { - return mk_tactic_exception(sstream() << "revert tactic failed, unknown '" + return tactic::mk_exception(sstream() << "revert tactic failed, unknown '" << local_pp_name(l) << "' hypothesis", s); } } tactic_state new_s = revert(locals, s); - return mk_tactic_success(mk_vm_nat(locals.size()), new_s); + return tactic::mk_success(mk_vm_nat(locals.size()), new_s); } vm_obj tactic_revert_lst(vm_obj const & ns, vm_obj const & s) { - return revert(to_list_expr(ns), to_tactic_state(s)); + return revert(to_list_expr(ns), tactic::to_state(s)); } void initialize_revert_tactic() { diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index 55b1882c25..a9419c594f 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -49,9 +49,9 @@ vm_obj rewrite(transparency_mode const & m, bool approx, bool use_instances, occ } H_type = annotated_head_beta_reduce(H_type); if (!is_eq(H_type, A, lhs, rhs)) - return mk_tactic_exception("rewrite tactic failed, lemma is not an equality nor a iff", s); + return tactic::mk_exception("rewrite tactic failed, lemma is not an equality nor a iff", s); if (is_metavar(lhs)) - return mk_tactic_exception("rewrite tactic failed, lemma lhs is a metavariable", s); + return tactic::mk_exception("rewrite tactic failed, lemma lhs is a metavariable", s); if (!target) symm = !symm; if (symm) { @@ -73,7 +73,7 @@ vm_obj rewrite(transparency_mode const & m, bool approx, bool use_instances, occ msg += pp_indented_expr(new_s, pattern); return msg; }; - return mk_tactic_exception(thunk, new_s); + return tactic::mk_exception(thunk, new_s); } /* Synthesize type class instances */ if (use_instances) { @@ -86,11 +86,11 @@ vm_obj rewrite(transparency_mode const & m, bool approx, bool use_instances, occ expr meta_type = ctx.instantiate_mvars(ctx.infer(meta)); optional inst = ctx.mk_class_instance(meta_type); if (!inst) { - return mk_tactic_exception(sstream() << "rewrite tactic failed, failed to synthesize type class instance for #" + return tactic::mk_exception(sstream() << "rewrite tactic failed, failed to synthesize type class instance for #" << (i+1) << " argument", s); } if (!ctx.is_def_eq(meta, *inst)) { - return mk_tactic_exception(sstream() << "rewrite tactic failed, failed to assign type class instance for #" + return tactic::mk_exception(sstream() << "rewrite tactic failed, failed to assign type class instance for #" << (i+1) << " argument", s); } } @@ -116,38 +116,38 @@ vm_obj rewrite(transparency_mode const & m, bool approx, bool use_instances, occ name Hname = is_local(*target) ? local_pp_name(*target) : name("H"); tactic_state s1 = set_mctx_goals(s, ctx.mctx(), cons(head(s.goals()), append(to_list(unassigned_mvars), tail(s.goals())))); vm_obj r2 = assertv_definev(true, Hname, new_e, prf, s1); - if (optional const & s2 = is_tactic_success(r2)) { + if (optional const & s2 = tactic::is_success(r2)) { if (is_local(*target)) { /* Try to clear target */ vm_obj r3 = clear_internal(mlocal_name(*target), *s2); - if (is_tactic_success(r3)) + if (tactic::is_success(r3)) return r3; } return r2; } else { - return mk_tactic_exception(sstream() << "rewrite tactic failed, failed to create new hypothesis", s); + return tactic::mk_exception(sstream() << "rewrite tactic failed, failed to create new hypothesis", s); } } else { expr new_mvar = ctx.mk_metavar_decl(ctx.lctx(), new_e); expr prf = mk_eq_rec(ctx, motive, new_mvar, H); ctx.assign(head(s.goals()), prf); - return mk_tactic_success(set_mctx_goals(s, ctx.mctx(), cons(new_mvar, append(to_list(unassigned_mvars), tail(s.goals()))))); + return tactic::mk_success(set_mctx_goals(s, ctx.mctx(), cons(new_mvar, append(to_list(unassigned_mvars), tail(s.goals()))))); } } vm_obj tactic_rewrite(vm_obj const & m, vm_obj const & approx, vm_obj const & use_instances, vm_obj const & occs, vm_obj const & symm, vm_obj const & H, vm_obj const & s) { LEAN_TACTIC_TRY; return rewrite(to_transparency_mode(m), to_bool(approx), to_bool(use_instances), - to_occurrences(occs), to_bool(symm), to_expr(H), none_expr(), to_tactic_state(s)); - LEAN_TACTIC_CATCH(to_tactic_state(s)); + to_occurrences(occs), to_bool(symm), to_expr(H), none_expr(), tactic::to_state(s)); + LEAN_TACTIC_CATCH(tactic::to_state(s)); } vm_obj tactic_rewrite_at(vm_obj const & m, vm_obj const & approx, vm_obj const & use_instances, vm_obj const & occs, vm_obj const & symm, vm_obj const & H1, vm_obj const & H2, vm_obj const & s) { LEAN_TACTIC_TRY; return rewrite(to_transparency_mode(m), to_bool(approx), to_bool(use_instances), to_occurrences(occs), - to_bool(symm), to_expr(H1), some_expr(to_expr(H2)), to_tactic_state(s)); - LEAN_TACTIC_CATCH(to_tactic_state(s)); + to_bool(symm), to_expr(H1), some_expr(to_expr(H2)), tactic::to_state(s)); + LEAN_TACTIC_CATCH(tactic::to_state(s)); } void initialize_rewrite_tactic() { diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp index d6a59770cb..454c51a30d 100644 --- a/src/library/tactic/simp_lemmas.cpp +++ b/src/library/tactic/simp_lemmas.cpp @@ -1259,10 +1259,10 @@ vm_obj to_obj(simp_lemmas const & idx) { vm_obj simp_lemmas_mk_default_core(vm_obj const & m, vm_obj const & s) { LEAN_TACTIC_TRY; - environment const & env = to_tactic_state(s).env(); + environment const & env = tactic::to_state(s).env(); simp_lemmas r = get_default_simp_lemmas(env, to_transparency_mode(m)); - return mk_tactic_success(to_obj(r), to_tactic_state(s)); - LEAN_TACTIC_CATCH(to_tactic_state(s)); + return tactic::mk_success(to_obj(r), tactic::to_state(s)); + LEAN_TACTIC_CATCH(tactic::to_state(s)); } vm_obj simp_lemmas_add_core(vm_obj const & m, vm_obj const & lemmas, vm_obj const & lemma, vm_obj const & s) { @@ -1279,24 +1279,24 @@ vm_obj simp_lemmas_add_core(vm_obj const & m, vm_obj const & lemmas, vm_obj cons // TODO(dhs): accept priority as an argument // Reason for postponing: better plumbing of numerals through the vm simp_lemmas new_lemmas = add(tctx, to_simp_lemmas(lemmas), id, tctx.infer(e), e, LEAN_DEFAULT_PRIORITY); - return mk_tactic_success(to_obj(new_lemmas), to_tactic_state(s)); - LEAN_TACTIC_CATCH(to_tactic_state(s)); + return tactic::mk_success(to_obj(new_lemmas), tactic::to_state(s)); + LEAN_TACTIC_CATCH(tactic::to_state(s)); } vm_obj simp_lemmas_add_simp(vm_obj const & m, vm_obj const & lemmas, vm_obj const & lemma_name, vm_obj const & s) { LEAN_TACTIC_TRY; type_context ctx = mk_type_context_for(s, m); simp_lemmas new_lemmas = add(ctx, to_simp_lemmas(lemmas), to_name(lemma_name), LEAN_DEFAULT_PRIORITY); - return mk_tactic_success(to_obj(new_lemmas), to_tactic_state(s)); - LEAN_TACTIC_CATCH(to_tactic_state(s)); + return tactic::mk_success(to_obj(new_lemmas), tactic::to_state(s)); + LEAN_TACTIC_CATCH(tactic::to_state(s)); } vm_obj simp_lemmas_add_congr(vm_obj const & m, vm_obj const & lemmas, vm_obj const & lemma_name, vm_obj const & s) { LEAN_TACTIC_TRY; type_context ctx = mk_type_context_for(s, m); simp_lemmas new_lemmas = add_congr(ctx, to_simp_lemmas(lemmas), to_name(lemma_name), LEAN_DEFAULT_PRIORITY); - return mk_tactic_success(to_obj(new_lemmas), to_tactic_state(s)); - LEAN_TACTIC_CATCH(to_tactic_state(s)); + return tactic::mk_success(to_obj(new_lemmas), tactic::to_state(s)); + LEAN_TACTIC_CATCH(tactic::to_state(s)); } vm_obj simp_lemmas_mk() { @@ -1319,7 +1319,7 @@ vm_obj simp_lemmas_erase(vm_obj const & lemmas, vm_obj const & lemma_list) { static optional prove(type_context & ctx, vm_obj const & prove_fn, expr const & e, tactic_state s) { s = mk_tactic_state_for(s.env(), s.get_options(), s.decl_name(), ctx.lctx(), e); vm_obj r_obj = invoke(prove_fn, to_obj(s)); - optional s_new = is_tactic_success(r_obj); + optional s_new = tactic::is_success(r_obj); if (!s_new || s_new->goals()) return none_expr(); metavar_context mctx = s_new->mctx(); expr result = mctx.instantiate_mvars(s_new->main()); @@ -1417,10 +1417,10 @@ vm_obj simp_lemmas_rewrite_core(transparency_mode const & m, simp_lemmas const & name const & R, expr const & e, tactic_state const & s) { LEAN_TACTIC_TRY; simp_lemmas_for const * sr = sls.find(R); - if (!sr) return mk_tactic_exception("failed to apply simp_lemmas, no lemmas for the given relation", s); + if (!sr) return tactic::mk_exception("failed to apply simp_lemmas, no lemmas for the given relation", s); list const * srs = sr->find(e); - if (!srs) return mk_tactic_exception("failed to apply simp_lemmas, no simp lemma", s); + if (!srs) return tactic::mk_exception("failed to apply simp_lemmas, no simp lemma", s); type_context ctx = mk_type_context_for(s, m); @@ -1431,26 +1431,26 @@ vm_obj simp_lemmas_rewrite_core(transparency_mode const & m, simp_lemmas const & tout() << "[" << lemma.get_id() << "]: " << e << " ==> " << r.get_new() << "\n";); vm_obj new_e = to_obj(r.get_new()); vm_obj new_pr = to_obj(r.get_proof()); - return mk_tactic_success(mk_vm_pair(new_e, new_pr), s); + return tactic::mk_success(mk_vm_pair(new_e, new_pr), s); } } - return mk_tactic_exception("failed to apply simp_lemmas, no simp lemma", s); + return tactic::mk_exception("failed to apply simp_lemmas, no simp lemma", s); LEAN_TACTIC_CATCH(s); } vm_obj simp_lemmas_rewrite(vm_obj const & m, vm_obj const & sls, vm_obj const & prove_fn, vm_obj const & R, vm_obj const & e, vm_obj const & s) { return simp_lemmas_rewrite_core(to_transparency_mode(m), to_simp_lemmas(sls), prove_fn, - to_name(R), to_expr(e), to_tactic_state(s)); + to_name(R), to_expr(e), tactic::to_state(s)); } vm_obj simp_lemmas_drewrite_core(transparency_mode const & m, simp_lemmas const & sls, expr const & e, tactic_state const & s) { LEAN_TACTIC_TRY; simp_lemmas_for const * sr = sls.find(get_eq_name()); - if (!sr) return mk_tactic_exception("failed to apply simp_lemmas, no lemmas for 'eq' relation", s); + if (!sr) return tactic::mk_exception("failed to apply simp_lemmas, no lemmas for 'eq' relation", s); list const * srs = sr->find(e); - if (!srs) return mk_tactic_exception("failed to apply simp_lemmas, no simp lemma", s); + if (!srs) return tactic::mk_exception("failed to apply simp_lemmas, no simp lemma", s); type_context ctx = mk_type_context_for(s, m); @@ -1458,15 +1458,15 @@ vm_obj simp_lemmas_drewrite_core(transparency_mode const & m, simp_lemmas const if (lemma.is_refl()) { expr new_e = refl_lemma_rewrite(ctx, e, lemma); if (new_e != e) - return mk_tactic_success(to_obj(new_e), s); + return tactic::mk_success(to_obj(new_e), s); } } - return mk_tactic_exception("failed to apply simp_lemmas, no simp lemma", s); + return tactic::mk_exception("failed to apply simp_lemmas, no simp lemma", s); LEAN_TACTIC_CATCH(s); } vm_obj simp_lemmas_drewrite(vm_obj const & m, vm_obj const & sls, vm_obj const & e, vm_obj const & s) { - return simp_lemmas_drewrite_core(to_transparency_mode(m), to_simp_lemmas(sls), to_expr(e), to_tactic_state(s)); + return simp_lemmas_drewrite_core(to_transparency_mode(m), to_simp_lemmas(sls), to_expr(e), tactic::to_state(s)); } static bool is_valid_simp_lemma_cnst_core(transparency_mode const & m, name const & cname, tactic_state const & s) { @@ -1484,8 +1484,8 @@ static bool is_valid_simp_lemma_cnst_core(transparency_mode const & m, name cons } vm_obj is_valid_simp_lemma_cnst(vm_obj const & m, vm_obj const & n, vm_obj const & s) { - return mk_tactic_success(mk_vm_bool(is_valid_simp_lemma_cnst_core(to_transparency_mode(m), to_name(n), to_tactic_state(s))), - to_tactic_state(s)); + return tactic::mk_success(mk_vm_bool(is_valid_simp_lemma_cnst_core(to_transparency_mode(m), to_name(n), tactic::to_state(s))), + tactic::to_state(s)); } static bool is_valid_simp_lemma_core(transparency_mode const & m, expr const & e, tactic_state const & s) { @@ -1499,8 +1499,8 @@ static bool is_valid_simp_lemma_core(transparency_mode const & m, expr const & e } vm_obj is_valid_simp_lemma(vm_obj const & m, vm_obj const & e, vm_obj const & s) { - return mk_tactic_success(mk_vm_bool(is_valid_simp_lemma_core(to_transparency_mode(m), to_expr(e), to_tactic_state(s))), - to_tactic_state(s)); + return tactic::mk_success(mk_vm_bool(is_valid_simp_lemma_core(to_transparency_mode(m), to_expr(e), tactic::to_state(s))), + tactic::to_state(s)); } static name * g_refl_lemma_attr = nullptr; @@ -1515,11 +1515,11 @@ environment mark_rfl_lemma(environment const & env, name const & cname) { vm_obj simp_lemmas_pp(vm_obj const & S, vm_obj const & _s) { formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); type_context ctx = mk_type_context_for(s); formatter fmt = fmtf(s.env(), s.get_options(), ctx); format r = to_simp_lemmas(S).pp(fmt); - return mk_tactic_success(to_obj(r), s); + return tactic::mk_success(to_obj(r), s); } void initialize_simp_lemmas() { diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp index 6893fd1231..4a1e4866a5 100644 --- a/src/library/tactic/simplify.cpp +++ b/src/library/tactic/simplify.cpp @@ -1093,7 +1093,7 @@ class vm_simplify_fn : public simplify_ext_core_fn { m_s = set_mctx_lctx_dcs(m_s, m_ctx.mctx(), m_ctx.lctx(), m_defeq_canonizer.get_state()); vm_obj r = invoke(fn, m_a, to_obj(m_slss), to_obj(m_rel), to_obj(parent), to_obj(e), to_obj(m_s)); /* r : tactic_state (A × expr × option expr × bool) */ - if (optional new_s = is_tactic_success(r)) { + if (optional new_s = tactic::is_success(r)) { m_s = *new_s; m_ctx.set_mctx(m_s.mctx()); m_defeq_canonizer.set_state(m_s.dcs()); @@ -1125,7 +1125,7 @@ class vm_simplify_fn : public simplify_ext_core_fn { virtual optional prove(expr const & e) override { auto s = mk_tactic_state_for(m_ctx.env(), m_ctx.get_options(), m_s.decl_name(), m_ctx.lctx(), e); vm_obj r_obj = invoke(m_prove, m_a, to_obj(s)); - optional s_new = is_tactic_success(r_obj); + optional s_new = tactic::is_success(r_obj); if (!s_new || s_new->goals()) return none_expr(); metavar_context mctx = s_new->mctx(); expr result = mctx.instantiate_mvars(s_new->main()); @@ -1180,7 +1180,7 @@ meta constant simplify_core expr → tactic (expr × expr) */ vm_obj tactic_simplify_core(vm_obj const & c, vm_obj const & slss, vm_obj const & rel, vm_obj const & e, vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); try { unsigned max_steps; bool contextual, lift_eq, canonize_instances, canonize_proofs, use_axioms; get_simplify_config(c, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs, use_axioms); @@ -1192,12 +1192,12 @@ vm_obj tactic_simplify_core(vm_obj const & c, vm_obj const & slss, vm_obj const if (result.get_new() != to_expr(e)) { result = finalize(ctx, to_name(rel), result); tactic_state new_s = set_dcs(s, dcs); - return mk_tactic_success(mk_vm_pair(to_obj(result.get_new()), to_obj(result.get_proof())), new_s); + return tactic::mk_success(mk_vm_pair(to_obj(result.get_new()), to_obj(result.get_proof())), new_s); } else { - return mk_tactic_exception("simplify tactic failed to simplify", s); + return tactic::mk_exception("simplify tactic failed to simplify", s); } } catch (exception & e) { - return mk_tactic_exception(e, s); + return tactic::mk_exception(e, s); } } @@ -1216,12 +1216,12 @@ static vm_obj ext_simplify_core(vm_obj const & a, vm_obj const & c, simp_lemmas vm_obj const & a = p.first; simp_result result = finalize(ctx, r, p.second); tactic_state new_s = set_dcs(s, dcs); - return mk_tactic_success(mk_vm_pair(a, mk_vm_pair(to_obj(result.get_new()), to_obj(result.get_proof()))), new_s); + return tactic::mk_success(mk_vm_pair(a, mk_vm_pair(to_obj(result.get_new()), to_obj(result.get_proof()))), new_s); } else { - return mk_tactic_exception("simplify tactic failed to simplify", s); + return tactic::mk_exception("simplify tactic failed to simplify", s); } } catch (exception & e) { - return mk_tactic_exception(e, s); + return tactic::mk_exception(e, s); } } @@ -1240,7 +1240,7 @@ meta constant ext_simplify_core vm_obj tactic_ext_simplify_core(unsigned DEBUG_CODE(num), vm_obj const * args) { lean_assert(num == 10); return ext_simplify_core(args[1], args[2], to_simp_lemmas(args[3]), args[4], args[5], args[6], - to_name(args[7]), to_expr(args[8]), to_tactic_state(args[9])); + to_name(args[7]), to_expr(args[8]), tactic::to_state(args[9])); } void initialize_simplify() { diff --git a/src/library/tactic/smt/congruence_tactics.cpp b/src/library/tactic/smt/congruence_tactics.cpp index 13ab07ba24..aeeb5cdaaf 100644 --- a/src/library/tactic/smt/congruence_tactics.cpp +++ b/src/library/tactic/smt/congruence_tactics.cpp @@ -79,7 +79,7 @@ vm_obj cc_state_mk_core(vm_obj const & cfg) { } vm_obj cc_state_mk_using_hs_core(vm_obj const & cfg, vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); optional g = s.get_main_goal_decl(); if (!g) return mk_no_goals_exception(s); try { @@ -94,28 +94,28 @@ vm_obj cc_state_mk_using_hs_core(vm_obj const & cfg, vm_obj const & _s) { } }); tactic_state new_s = set_dcs(s, dcs); - return mk_tactic_success(to_obj(r), new_s); + return tactic::mk_success(to_obj(r), new_s); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } vm_obj cc_state_pp_core(vm_obj const & ccs, vm_obj const & nonsingleton, vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); type_context ctx = mk_type_context_for(s); formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); formatter fmt = fmtf(s.env(), s.get_options(), ctx); format r = to_cc_state(ccs).pp_eqcs(fmt, to_bool(nonsingleton)); - return mk_tactic_success(to_obj(r), s); + return tactic::mk_success(to_obj(r), s); } vm_obj cc_state_pp_eqc(vm_obj const & ccs, vm_obj const & e, vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); type_context ctx = mk_type_context_for(s); formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); formatter fmt = fmtf(s.env(), s.get_options(), ctx); format r = to_cc_state(ccs).pp_eqc(fmt, to_expr(e)); - return mk_tactic_success(to_obj(r), s); + return tactic::mk_success(to_obj(r), s); } vm_obj cc_state_next(vm_obj const & ccs, vm_obj const & e) { @@ -155,7 +155,7 @@ vm_obj cc_state_inc_gmt(vm_obj const & ccs) { } #define cc_state_proc(CODE) \ - tactic_state const & s = to_tactic_state(_s); \ + tactic_state const & s = tactic::to_state(_s); \ try { \ type_context ctx = mk_type_context_for(s); \ congruence_closure::state S = to_cc_state(ccs); \ @@ -163,16 +163,16 @@ vm_obj cc_state_inc_gmt(vm_obj const & ccs) { congruence_closure cc(ctx, S, dcs); \ CODE \ } catch (exception & ex) { \ - return mk_tactic_exception(ex, s); \ + return tactic::mk_exception(ex, s); \ } -#define cc_state_updt_proc(CODE) cc_state_proc({ CODE; return mk_tactic_success(to_obj(S), set_dcs(s, dcs)); }) +#define cc_state_updt_proc(CODE) cc_state_proc({ CODE; return tactic::mk_success(to_obj(S), set_dcs(s, dcs)); }) vm_obj cc_state_add(vm_obj const & ccs, vm_obj const & H, vm_obj const & _s) { cc_state_updt_proc({ expr type = ctx.infer(to_expr(H)); if (ctx.is_prop(type)) - return mk_tactic_exception("cc_state.add failed, given expression is not a proof term", s); + return tactic::mk_exception("cc_state.add failed, given expression is not a proof term", s); cc.add(type, to_expr(H), 0); }); } @@ -186,23 +186,23 @@ vm_obj cc_state_internalize(vm_obj const & ccs, vm_obj const & e, vm_obj const & vm_obj cc_state_is_eqv(vm_obj const & ccs, vm_obj const & e1, vm_obj const & e2, vm_obj const & _s) { cc_state_proc({ bool r = cc.is_eqv(to_expr(e1), to_expr(e2)); - return mk_tactic_success(mk_vm_bool(r), s); + return tactic::mk_success(mk_vm_bool(r), s); }); } vm_obj cc_state_is_not_eqv(vm_obj const & ccs, vm_obj const & e1, vm_obj const & e2, vm_obj const & _s) { cc_state_proc({ bool r = cc.is_not_eqv(to_expr(e1), to_expr(e2)); - return mk_tactic_success(mk_vm_bool(r), s); + return tactic::mk_success(mk_vm_bool(r), s); }); } vm_obj cc_state_eqv_proof(vm_obj const & ccs, vm_obj const & e1, vm_obj const & e2, vm_obj const & _s) { cc_state_proc({ if (optional r = cc.get_proof(to_expr(e1), to_expr(e2))) { - return mk_tactic_success(to_obj(*r), s); + return tactic::mk_success(to_obj(*r), s); } else { - return mk_tactic_exception("cc_state.eqv_proof failed to build proof", s); + return tactic::mk_exception("cc_state.eqv_proof failed to build proof", s); } }); } @@ -210,9 +210,9 @@ vm_obj cc_state_eqv_proof(vm_obj const & ccs, vm_obj const & e1, vm_obj const & vm_obj cc_state_proof_for(vm_obj const & ccs, vm_obj const & e, vm_obj const & _s) { cc_state_proc({ if (optional r = cc.get_eq_proof(to_expr(e), mk_true())) { - return mk_tactic_success(to_obj(mk_of_eq_true(cc.ctx(), *r)), s); + return tactic::mk_success(to_obj(mk_of_eq_true(cc.ctx(), *r)), s); } else { - return mk_tactic_exception("cc_state.get_proof_for failed to build proof", s); + return tactic::mk_exception("cc_state.get_proof_for failed to build proof", s); } }); } @@ -220,9 +220,9 @@ vm_obj cc_state_proof_for(vm_obj const & ccs, vm_obj const & e, vm_obj const & _ vm_obj cc_state_refutation_for(vm_obj const & ccs, vm_obj const & e, vm_obj const & _s) { cc_state_proc({ if (optional r = cc.get_eq_proof(to_expr(e), mk_false())) { - return mk_tactic_success(to_obj(mk_not_of_eq_false(cc.ctx(), *r)), s); + return tactic::mk_success(to_obj(mk_not_of_eq_false(cc.ctx(), *r)), s); } else { - return mk_tactic_exception("cc_state.get_refutation_for failed to build proof", s); + return tactic::mk_exception("cc_state.get_refutation_for failed to build proof", s); } }); } @@ -230,9 +230,9 @@ vm_obj cc_state_refutation_for(vm_obj const & ccs, vm_obj const & e, vm_obj cons vm_obj cc_state_proof_for_false(vm_obj const & ccs, vm_obj const & _s) { cc_state_proc({ if (auto pr = cc.get_inconsistency_proof()) { - return mk_tactic_success(to_obj(*pr), s); + return tactic::mk_success(to_obj(*pr), s); } else { - return mk_tactic_exception("cc_state.false_proof failed, state is not inconsistent", s); + return tactic::mk_exception("cc_state.false_proof failed, state is not inconsistent", s); } }); } diff --git a/src/library/tactic/smt/ematch.cpp b/src/library/tactic/smt/ematch.cpp index d14ee6e890..27747c72ab 100644 --- a/src/library/tactic/smt/ematch.cpp +++ b/src/library/tactic/smt/ematch.cpp @@ -1084,8 +1084,8 @@ vm_obj ematch_state_internalize(vm_obj const & ems, vm_obj const & e, vm_obj con ematch_state S = to_ematch_state(ems); type_context ctx = mk_type_context_for(s); S.internalize(ctx, to_expr(e)); - return mk_tactic_success(to_obj(S), to_tactic_state(s)); - LEAN_TACTIC_CATCH(to_tactic_state(s)); + return tactic::mk_success(to_obj(S), tactic::to_state(s)); + LEAN_TACTIC_CATCH(tactic::to_state(s)); } vm_obj mk_ematch_result(buffer const & new_inst_buffer, congruence_closure::state const & ccs, @@ -1100,7 +1100,7 @@ vm_obj mk_ematch_result(buffer const & new_inst_buffer, congruence } vm_obj ematch_core(vm_obj const & md, vm_obj const & _ccs, vm_obj const & _ems, vm_obj const & hlemma, vm_obj const & t, vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); LEAN_TACTIC_TRY; type_context ctx = mk_type_context_for(_s, md); ematch_state ems = to_ematch_state(_ems); @@ -1111,12 +1111,12 @@ vm_obj ematch_core(vm_obj const & md, vm_obj const & _ccs, vm_obj const & _ems, ematch(ctx, ems, cc, to_hinst_lemma(hlemma), to_expr(t), new_inst_buffer); vm_obj r = mk_ematch_result(new_inst_buffer, ccs, ems); tactic_state new_s = set_dcs(s, dcs); - return mk_tactic_success(r, new_s); + return tactic::mk_success(r, new_s); LEAN_TACTIC_CATCH(s); } vm_obj ematch_all_core(vm_obj const & md, vm_obj const & _ccs, vm_obj const & _ems, vm_obj const & hlemma, vm_obj const & filter, vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); LEAN_TACTIC_TRY; type_context ctx = mk_type_context_for(_s, md); ematch_state ems = to_ematch_state(_ems); @@ -1127,7 +1127,7 @@ vm_obj ematch_all_core(vm_obj const & md, vm_obj const & _ccs, vm_obj const & _e ematch(ctx, ems, cc, to_hinst_lemma(hlemma), to_bool(filter), new_inst_buffer); vm_obj r = mk_ematch_result(new_inst_buffer, ccs, ems); tactic_state new_s = set_dcs(s, dcs); - return mk_tactic_success(r, new_s); + return tactic::mk_success(r, new_s); LEAN_TACTIC_CATCH(s); } diff --git a/src/library/tactic/smt/hinst_lemmas.cpp b/src/library/tactic/smt/hinst_lemmas.cpp index 1d758352ff..be8cdbbd0b 100644 --- a/src/library/tactic/smt/hinst_lemmas.cpp +++ b/src/library/tactic/smt/hinst_lemmas.cpp @@ -704,26 +704,26 @@ vm_obj hinst_lemma_mk_core(vm_obj const & m, vm_obj const & lemma, vm_obj const LEAN_TACTIC_TRY; type_context ctx = mk_type_context_for(s); hinst_lemma h = mk_hinst_lemma(ctx, to_transparency_mode(m), to_expr(lemma), to_bool(simp)); - return mk_tactic_success(to_obj(h), to_tactic_state(s)); - LEAN_TACTIC_CATCH(to_tactic_state(s)); + return tactic::mk_success(to_obj(h), tactic::to_state(s)); + LEAN_TACTIC_CATCH(tactic::to_state(s)); } vm_obj hinst_lemma_mk_from_decl_core(vm_obj const & m, vm_obj const & lemma_name, vm_obj const & simp, vm_obj const & s) { LEAN_TACTIC_TRY; type_context ctx = mk_type_context_for(s); hinst_lemma h = mk_hinst_lemma(ctx, to_transparency_mode(m), to_name(lemma_name), to_bool(simp)); - return mk_tactic_success(to_obj(h), to_tactic_state(s)); - LEAN_TACTIC_CATCH(to_tactic_state(s)); + return tactic::mk_success(to_obj(h), tactic::to_state(s)); + LEAN_TACTIC_CATCH(tactic::to_state(s)); } vm_obj hinst_lemma_pp(vm_obj const & h, vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); LEAN_TACTIC_TRY; formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); type_context ctx = mk_type_context_for(s); formatter fmt = fmtf(s.env(), s.get_options(), ctx); format r = pp_hinst_lemma(fmt, to_hinst_lemma(h)); - return mk_tactic_success(to_obj(r), s); + return tactic::mk_success(to_obj(r), s); LEAN_TACTIC_CATCH(s); } diff --git a/src/library/tactic/smt/smt_state.cpp b/src/library/tactic/smt/smt_state.cpp index e9c483dcf1..56cfa04ee4 100644 --- a/src/library/tactic/smt/smt_state.cpp +++ b/src/library/tactic/smt/smt_state.cpp @@ -138,7 +138,7 @@ vm_obj to_obj(smt_goal const & s) { } vm_obj tactic_result_to_smt_tactic_result(vm_obj const & r, vm_obj const & ss) { - return mk_tactic_result(mk_vm_pair(get_tactic_result_value(r), ss), get_tactic_result_state(r)); + return tactic::mk_result(mk_vm_pair(tactic::get_result_value(r), ss), tactic::get_result_state(r)); } vm_obj mk_smt_tactic_success(vm_obj const & a, vm_obj const & ss, vm_obj const & ts) { @@ -241,7 +241,7 @@ static vm_obj preprocess(tactic_state s, smt_pre_config const & cfg) { metavar_context mctx = ctx.mctx(); mctx.assign(head(s.goals()), h); tactic_state new_s = set_mctx_goals_dcs(s, mctx, cons(new_M, tail(s.goals())), dcs); - return mk_tactic_success(new_s); + return tactic::mk_success(new_s); } } @@ -384,8 +384,8 @@ vm_obj mk_smt_state(tactic_state s, smt_config const & cfg) { smt_goal new_goal(cfg); vm_obj r = preprocess(s, cfg.m_pre_config); - if (is_tactic_result_exception(r)) return r; - s = to_tactic_state(get_tactic_result_state(r)); + if (tactic::is_result_exception(r)) return r; + s = tactic::to_state(tactic::get_result_state(r)); metavar_context mctx = s.mctx(); bool use_unused_names = true; @@ -397,16 +397,16 @@ vm_obj mk_smt_state(tactic_state s, smt_config const & cfg) { s = set_mctx_goals_dcs(s, mctx, cons(new_M, tail(s.goals())), dcs); s = add_em_facts(s, new_goal); - return mk_tactic_success(mk_vm_cons(to_obj(new_goal), mk_vm_nil()), s); + return tactic::mk_success(mk_vm_cons(to_obj(new_goal), mk_vm_nil()), s); } static hinst_lemmas get_hinst_lemmas(name const & attr_name, tactic_state const & s) { auto & S = get_vm_state(); vm_obj attr = S.get_constant(attr_name); vm_obj r = caching_user_attribute_get_cache(mk_vm_unit(), attr, to_obj(s)); - if (is_tactic_result_exception(r)) + if (tactic::is_result_exception(r)) throw exception(sstream() << "failed to initialize sm_state, failed to retrieve attribute '" << attr_name << "'"); - vm_obj lemmas = get_tactic_result_value(r); + vm_obj lemmas = tactic::get_result_value(r); if (!is_hinst_lemmas(lemmas)) throw exception(sstream() << "failed to initialize smt_state, attribute '" << attr_name << "' is not a hinst_lemmas"); return to_hinst_lemmas(lemmas); @@ -416,9 +416,9 @@ static simp_lemmas get_simp_lemmas(name const & attr_name, tactic_state const & auto & S = get_vm_state(); vm_obj attr = S.get_constant(attr_name); vm_obj r = caching_user_attribute_get_cache(mk_vm_unit(), attr, to_obj(s)); - if (is_tactic_result_exception(r)) + if (tactic::is_result_exception(r)) throw exception(sstream() << "failed to initialize sm_state, failed to retrieve attribute '" << attr_name << "'"); - vm_obj lemmas = get_tactic_result_value(r); + vm_obj lemmas = tactic::get_result_value(r); if (!is_simp_lemmas(lemmas)) throw exception(sstream() << "failed to initialize smt_state, attribute '" << attr_name << "' is not a simp_lemmas"); return to_simp_lemmas(lemmas); @@ -456,8 +456,8 @@ static smt_config to_smt_config(vm_obj const & cfg, tactic_state const & s) { vm_obj smt_state_mk(vm_obj const & cfg, vm_obj const & s) { LEAN_TACTIC_TRY; - return mk_smt_state(to_tactic_state(s), to_smt_config(cfg, to_tactic_state(s))); - LEAN_TACTIC_CATCH(to_tactic_state(s)); + return mk_smt_state(tactic::to_state(s), to_smt_config(cfg, tactic::to_state(s))); + LEAN_TACTIC_CATCH(tactic::to_state(s)); } bool same_hyps(metavar_context const & mctx, expr const & mvar1, expr const & mvar2) { @@ -470,7 +470,7 @@ bool same_hyps(metavar_context const & mctx, expr const & mvar1, expr const & mv vm_obj tactic_to_smt_tactic(vm_obj const &, vm_obj const & tac, vm_obj const & ss, vm_obj const & ts) { vm_obj r1 = invoke(tac, ts); - if (is_tactic_result_exception(r1)) { + if (tactic::is_result_exception(r1)) { /* Tactic failed */ return r1; } @@ -493,13 +493,13 @@ vm_obj tactic_to_smt_tactic(vm_obj const &, vm_obj const & tac, vm_obj const & s (s_1, ..., s_1, s_2, ..., s_k) n copies of s_1 */ - vm_obj new_ts = get_tactic_result_state(r1); - if (is_eqp(to_tactic_state(ts), to_tactic_state(new_ts))) { + vm_obj new_ts = tactic::get_result_state(r1); + if (is_eqp(tactic::to_state(ts), tactic::to_state(new_ts))) { /* The tactic_state was not modified */ return tactic_result_to_smt_tactic_result(r1, ss); } - list goals = to_tactic_state(ts).goals(); - list new_goals = to_tactic_state(new_ts).goals(); + list goals = tactic::to_state(ts).goals(); + list new_goals = tactic::to_state(new_ts).goals(); if (goals == new_goals) { /* Set of goals did not change. */ return tactic_result_to_smt_tactic_result(r1, ss); @@ -509,7 +509,7 @@ vm_obj tactic_to_smt_tactic(vm_obj const &, vm_obj const & tac, vm_obj const & s return tactic_result_to_smt_tactic_result(r1, mk_vm_nil()); } if (!goals) { - return mk_tactic_exception("failed to lift tactic to smt_tactic, there were no goals to be solved", to_tactic_state(ts)); + return tactic::mk_exception("failed to lift tactic to smt_tactic, there were no goals to be solved", tactic::to_state(ts)); } if (new_goals == tail(goals)) { /* Main goal was solved */ @@ -517,7 +517,7 @@ vm_obj tactic_to_smt_tactic(vm_obj const &, vm_obj const & tac, vm_obj const & s vm_obj new_ss = tail(ss); return tactic_result_to_smt_tactic_result(r1, new_ss); } - metavar_context const & mctx = to_tactic_state(new_ts).mctx(); + metavar_context const & mctx = tactic::to_state(new_ts).mctx(); if (tail(new_goals) == tail(goals) && same_hyps(mctx, head(new_goals), head(goals))) { /* The set of hypotheses in the main goal did not change */ return tactic_result_to_smt_tactic_result(r1, ss); @@ -525,8 +525,8 @@ vm_obj tactic_to_smt_tactic(vm_obj const &, vm_obj const & tac, vm_obj const & s vm_obj new_ss = ss; while (true) { if (!same_hyps(mctx, head(new_goals), head(goals))) { - return mk_tactic_exception("failed to lift tactic to smt_tactic, set of hypotheses has been modified, at least one of the used tactics has to be lifted manually", - to_tactic_state(ts)); + return tactic::mk_exception("failed to lift tactic to smt_tactic, set of hypotheses has been modified, at least one of the used tactics has to be lifted manually", + tactic::to_state(ts)); } if (tail(new_goals) == tail(goals)) { return tactic_result_to_smt_tactic_result(r1, new_ss); @@ -537,8 +537,8 @@ vm_obj tactic_to_smt_tactic(vm_obj const &, vm_obj const & tac, vm_obj const & s /* Move to next */ new_goals = tail(new_goals); if (!new_goals) { - return mk_tactic_exception("failed to lift tactic to smt_tactic, only tactics that modify a prefix of the list of goals can be automatically lifted", - to_tactic_state(ts)); + return tactic::mk_exception("failed to lift tactic to smt_tactic, only tactics that modify a prefix of the list of goals can be automatically lifted", + tactic::to_state(ts)); } } } @@ -670,17 +670,17 @@ format smt_state_pp(vm_obj const & ss, tactic_state const & ts) { vm_obj smt_state_to_format(vm_obj const & ss, vm_obj const & ts) { LEAN_TACTIC_TRY; - return to_obj(smt_state_to_format_core(ss, to_tactic_state(ts))); - LEAN_TACTIC_CATCH(to_tactic_state(ts)); + return to_obj(smt_state_to_format_core(ss, tactic::to_state(ts))); + LEAN_TACTIC_CATCH(tactic::to_state(ts)); } vm_obj mk_smt_state_empty_exception(tactic_state const & ts) { - return mk_tactic_exception("tactic failed, smt_state is empty", ts); + return tactic::mk_exception("tactic failed, smt_state is empty", ts); } vm_obj mk_smt_state_empty_exception(vm_obj const & ts) { - lean_assert(is_tactic_state(ts)); - return mk_smt_state_empty_exception(to_tactic_state(ts)); + lean_assert(tactic::is_state(ts)); + return mk_smt_state_empty_exception(tactic::to_state(ts)); } vm_obj exact_core(expr const & e, vm_obj const & ss, tactic_state const & ts) { @@ -694,7 +694,7 @@ vm_obj exact_core(expr const & e, vm_obj const & ss, tactic_state const & ts) { } vm_obj smt_tactic_close(vm_obj const & ss, vm_obj const & _ts) { - tactic_state const & ts = to_tactic_state(_ts); + tactic_state const & ts = tactic::to_state(_ts); LEAN_TACTIC_TRY; if (is_nil(ss)) return mk_smt_state_empty_exception(ts); @@ -723,7 +723,7 @@ vm_obj smt_tactic_close(vm_obj const & ss, vm_obj const & _ts) { return exact_core(*pr, ss, ts); } LEAN_TACTIC_CATCH(ts); - return mk_tactic_exception("smt_tactic.close failed", ts); + return tactic::mk_exception("smt_tactic.close failed", ts); } vm_obj smt_tactic_intros_core(list const & ids, optional const & num, vm_obj const & ss, tactic_state ts) { @@ -734,8 +734,8 @@ vm_obj smt_tactic_intros_core(list const & ids, optional const & smt_goal new_sgoal = to_smt_goal(head(ss)); vm_obj r = preprocess(ts, new_sgoal.get_pre_config()); - if (is_tactic_result_exception(r)) return r; - ts = to_tactic_state(get_tactic_result_state(r)); + if (tactic::is_result_exception(r)) return r; + ts = tactic::to_state(tactic::get_result_state(r)); metavar_context mctx = ts.mctx(); defeq_can_state dcs = ts.dcs(); @@ -749,20 +749,20 @@ vm_obj smt_tactic_intros_core(list const & ids, optional const & } vm_obj smt_tactic_intros(vm_obj const & ss, vm_obj const & ts) { - return smt_tactic_intros_core(list(), optional(), ss, to_tactic_state(ts)); + return smt_tactic_intros_core(list(), optional(), ss, tactic::to_state(ts)); } vm_obj smt_tactic_intron(vm_obj const & n, vm_obj const & ss, vm_obj const & ts) { - return smt_tactic_intros_core(list(), optional(force_to_unsigned(n)), ss, to_tactic_state(ts)); + return smt_tactic_intros_core(list(), optional(force_to_unsigned(n)), ss, tactic::to_state(ts)); } vm_obj smt_tactic_intro_lst(vm_obj const & _ids, vm_obj const & ss, vm_obj const & ts) { list const & ids = to_list_name(_ids); - return smt_tactic_intros_core(list(ids), optional(length(ids)), ss, to_tactic_state(ts)); + return smt_tactic_intros_core(list(ids), optional(length(ids)), ss, tactic::to_state(ts)); } vm_obj smt_tactic_intros_core(vm_obj const & _ids, vm_obj const & ss, vm_obj const & _ts) { - tactic_state ts = to_tactic_state(_ts); + tactic_state ts = tactic::to_state(_ts); if (is_nil(ss)) return mk_smt_state_empty_exception(ts); LEAN_TACTIC_TRY; @@ -770,8 +770,8 @@ vm_obj smt_tactic_intros_core(vm_obj const & _ids, vm_obj const & ss, vm_obj con smt_goal new_sgoal = to_smt_goal(head(ss)); vm_obj r = preprocess(ts, new_sgoal.get_pre_config()); - if (is_tactic_result_exception(r)) return r; - ts = to_tactic_state(get_tactic_result_state(r)); + if (tactic::is_result_exception(r)) return r; + ts = tactic::to_state(tactic::get_result_state(r)); metavar_context mctx = ts.mctx(); defeq_can_state dcs = ts.dcs(); @@ -797,7 +797,7 @@ vm_obj smt_state_classical(vm_obj const & ss) { } vm_obj smt_tactic_ematch_core(vm_obj const & pred, vm_obj const & ss, vm_obj const & _ts) { - tactic_state ts = to_tactic_state(_ts); + tactic_state ts = tactic::to_state(_ts); if (is_nil(ss)) return mk_smt_state_empty_exception(ts); lean_assert(ts.goals()); LEAN_TACTIC_TRY; @@ -810,7 +810,7 @@ vm_obj smt_tactic_ematch_core(vm_obj const & pred, vm_obj const & ss, vm_obj con buffer new_instances; S.ematch(new_instances); if (new_instances.empty()) - return mk_tactic_exception("ematch failed, no new instance was produced", ts); + return tactic::mk_exception("ematch failed, no new instance was produced", ts); for (new_instance const & p : new_instances) { expr type = p.m_instance; expr proof = p.m_proof; @@ -830,7 +830,7 @@ vm_obj smt_tactic_ematch_core(vm_obj const & pred, vm_obj const & ss, vm_obj con } vm_obj smt_tactic_mk_ematch_eqn_lemmas_for_core(vm_obj const & md, vm_obj const & decl_name, vm_obj const & ss, vm_obj const & _ts) { - tactic_state ts = to_tactic_state(_ts); + tactic_state ts = tactic::to_state(_ts); if (is_nil(ss)) return mk_smt_state_empty_exception(ts); lean_assert(ts.goals()); LEAN_TACTIC_TRY; @@ -838,7 +838,7 @@ vm_obj smt_tactic_mk_ematch_eqn_lemmas_for_core(vm_obj const & md, vm_obj const buffer eqns; get_ext_eqn_lemmas_for(ts.env(), to_name(decl_name), eqns); if (eqns.empty()) - return mk_tactic_exception(sstream() << "tactic failed, '" << to_name(decl_name) << "' does not have equation lemmas", ts); + return tactic::mk_exception(sstream() << "tactic failed, '" << to_name(decl_name) << "' does not have equation lemmas", ts); hinst_lemmas hs; for (name const & eqn : eqns) { declaration eqn_decl = ctx.env().get(eqn); @@ -861,7 +861,7 @@ vm_obj smt_tactic_to_em_state(vm_obj const & ss, vm_obj const & ts) { } vm_obj smt_tactic_preprocess(vm_obj const & e, vm_obj const & ss, vm_obj const & _ts) { - tactic_state ts = to_tactic_state(_ts); + tactic_state ts = tactic::to_state(_ts); if (is_nil(ss)) return mk_smt_state_empty_exception(ts); lean_assert(ts.goals()); LEAN_TACTIC_TRY; @@ -876,7 +876,7 @@ vm_obj smt_tactic_preprocess(vm_obj const & e, vm_obj const & ss, vm_obj const & } vm_obj smt_tactic_get_lemmas(vm_obj const & ss, vm_obj const & _ts) { - tactic_state ts = to_tactic_state(_ts); + tactic_state ts = tactic::to_state(_ts); if (is_nil(ss)) return mk_smt_state_empty_exception(ts); smt_goal g = to_smt_goal(head(ss)); hinst_lemmas s = g.get_em_state().get_lemmas(); @@ -886,7 +886,7 @@ vm_obj smt_tactic_get_lemmas(vm_obj const & ss, vm_obj const & _ts) { } vm_obj smt_tactic_set_lemmas(vm_obj const & lemmas, vm_obj const & ss, vm_obj const & _ts) { - tactic_state ts = to_tactic_state(_ts); + tactic_state ts = tactic::to_state(_ts); if (is_nil(ss)) return mk_smt_state_empty_exception(ts); smt_goal g = to_smt_goal(head(ss)); g.set_lemmas(to_hinst_lemmas(lemmas)); @@ -895,7 +895,7 @@ vm_obj smt_tactic_set_lemmas(vm_obj const & lemmas, vm_obj const & ss, vm_obj co } vm_obj smt_tactic_add_lemmas(vm_obj const & lemmas, vm_obj const & ss, vm_obj const & _ts) { - tactic_state ts = to_tactic_state(_ts); + tactic_state ts = tactic::to_state(_ts); if (is_nil(ss)) return mk_smt_state_empty_exception(ts); type_context ctx = mk_type_context_for(ts); defeq_can_state dcs = ts.dcs(); @@ -915,7 +915,7 @@ vm_obj smt_tactic_add_lemmas(vm_obj const & lemmas, vm_obj const & ss, vm_obj co } vm_obj smt_tactic_ematch_using(vm_obj const & hs, vm_obj const & ss, vm_obj const & _ts) { - tactic_state ts = to_tactic_state(_ts); + tactic_state ts = tactic::to_state(_ts); if (is_nil(ss)) return mk_smt_state_empty_exception(ts); lean_assert(ts.goals()); LEAN_TACTIC_TRY; @@ -935,7 +935,7 @@ vm_obj smt_tactic_ematch_using(vm_obj const & hs, vm_obj const & ss, vm_obj cons } }); if (!added_facts && new_instances.empty()) - return mk_tactic_exception("ematch_using failed, no instance was produced", ts); + return tactic::mk_exception("ematch_using failed, no instance was produced", ts); for (new_instance const & p : new_instances) { expr type = p.m_instance; expr proof = p.m_proof; diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp index b2a0fc8d8c..d6560f8dd9 100644 --- a/src/library/tactic/subst_tactic.cpp +++ b/src/library/tactic/subst_tactic.cpp @@ -110,9 +110,9 @@ vm_obj tactic_subst_core(name const & n, bool symm, tactic_state const & s) { expr mvar = head(s.goals()); expr H = mctx.get_local(mvar, n); expr new_mvar = subst(s.env(), s.get_options(), transparency_mode::Semireducible, mctx, mvar, H, symm, nullptr); - return mk_tactic_success(set_mctx_goals(s, mctx, cons(new_mvar, tail(s.goals())))); + return tactic::mk_success(set_mctx_goals(s, mctx, cons(new_mvar, tail(s.goals())))); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } @@ -121,10 +121,10 @@ vm_obj tactic_subst(expr const & l, tactic_state const & s) { if (!g) return mk_no_goals_exception(s); local_context lctx = g->get_context(); if (!is_local(l)) - return mk_tactic_exception(sstream() << "subst tactic failed, given expression is not a local constant", s); + return tactic::mk_exception(sstream() << "subst tactic failed, given expression is not a local constant", s); optional d = lctx.find_local_decl(l); if (!d) - return mk_tactic_exception(sstream() << "subst tactic failed, unknown '" << local_pp_name(l) << "' hypothesis", s); + return tactic::mk_exception(sstream() << "subst tactic failed, unknown '" << local_pp_name(l) << "' hypothesis", s); expr const & type = d->get_type(); expr lhs, rhs; if (is_eq(type, lhs, rhs)) { @@ -133,7 +133,7 @@ vm_obj tactic_subst(expr const & l, tactic_state const & s) { } else if (is_local(lhs) && !depends_on(rhs, lhs)) { return tactic_subst_core(d->get_name(), false, s); } else { - return mk_tactic_exception(sstream() << "subst tactic failed, hypothesis '" + return tactic::mk_exception(sstream() << "subst tactic failed, hypothesis '" << local_pp_name(l) << "' is not of the form (x = t) or (t = x)", s); } } else { @@ -155,14 +155,14 @@ vm_obj tactic_subst(expr const & l, tactic_state const & s) { if (found) { return r; } else { - return mk_tactic_exception(sstream() << "subst tactic failed, hypothesis '" + return tactic::mk_exception(sstream() << "subst tactic failed, hypothesis '" << local_pp_name(l) << "' is not a variable nor an equation of the form (x = t) or (t = x)", s); } } } vm_obj tactic_subst(vm_obj const & e, vm_obj const & s) { - return tactic_subst(to_expr(e), to_tactic_state(s)); + return tactic_subst(to_expr(e), tactic::to_state(s)); } void initialize_subst_tactic() { diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index af5bbe434b..e3692cd908 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -199,14 +199,6 @@ format tactic_state::pp_goal(expr const & g) const { return pp_goal(fmtf, g); } -bool is_tactic_state(vm_obj const & o) { - return tactic::is_State(o); -} - -tactic_state const & to_tactic_state(vm_obj const & o) { - return tactic::to_State(o); -} - vm_obj to_obj(tactic_state const & s) { return tactic::to_obj(s); } @@ -221,11 +213,11 @@ vm_obj to_obj(transparency_mode m) { vm_obj tactic_state_env(vm_obj const & s) { - return to_obj(to_tactic_state(s).env()); + return to_obj(tactic::to_state(s).env()); } vm_obj tactic_state_to_format(vm_obj const & s) { - return to_obj(to_tactic_state(s).pp_core()); + return to_obj(tactic::to_state(s).pp_core()); } format pp_expr(tactic_state const & s, expr const & e) { @@ -242,129 +234,36 @@ format pp_indented_expr(tactic_state const & s, expr const & e) { } vm_obj tactic_state_format_expr(vm_obj const & s, vm_obj const & e) { - return to_obj(pp_expr(to_tactic_state(s), to_expr(e))); -} - -optional is_tactic_success(vm_obj const & o) { - if (is_constructor(o) && cidx(o) == 0) { - return optional(to_tactic_state(cfield(o, 1))); - } else { - return optional(); - } -} - -optional is_tactic_exception(vm_state & S, vm_obj const & ex) { - if (is_constructor(ex) && cidx(ex) == 1 && !is_none(cfield(ex, 0))) { - vm_obj fmt = S.invoke(get_some_value(cfield(ex, 0)), mk_vm_unit()); - optional ref; - if (!is_none(cfield(ex, 1))) - ref = to_expr(get_some_value(cfield(ex, 1))); - return optional(to_format(fmt), ref, to_tactic_state(cfield(ex, 2))); - } else { - return optional(); - } -} - -bool is_tactic_silent_exception(vm_obj const & ex) { - return is_constructor(ex) && cidx(ex) == 1 && is_none(cfield(ex, 0)); -} - -vm_obj mk_tactic_result(vm_obj const & a, vm_obj const & s) { - lean_assert(is_tactic_state(s)); - return mk_vm_constructor(0, a, s); -} - -bool is_tactic_result_exception(vm_obj const & r) { - return is_constructor(r) && cidx(r) == 1; -} - -bool is_tactic_result_success(vm_obj const & r) { - return is_constructor(r) && cidx(r) == 0; -} - -vm_obj get_tactic_result_value(vm_obj const & r) { - lean_assert(is_tactic_result_success(r)); - return cfield(r, 0); -} - -vm_obj get_tactic_result_state(vm_obj const & r) { - lean_assert(is_tactic_result_success(r)); - return cfield(r, 1); -} - -vm_obj mk_tactic_success(vm_obj const & a, tactic_state const & s) { - return mk_vm_constructor(0, a, to_obj(s)); -} - -vm_obj mk_tactic_success(tactic_state const & s) { - return mk_tactic_success(mk_vm_unit(), s); -} - -vm_obj mk_tactic_exception(vm_obj const & fn, tactic_state const & s) { - return mk_vm_constructor(1, mk_vm_some(fn), mk_vm_none(), to_obj(s)); -} - -vm_obj mk_tactic_silent_exception(tactic_state const & s) { - return mk_vm_constructor(1, mk_vm_none(), mk_vm_none(), to_obj(s)); -} - -vm_obj mk_tactic_exception(vm_obj const & fn, vm_obj const & ref, tactic_state const & s) { - return mk_vm_constructor(1, mk_vm_some(fn), ref, to_obj(s)); -} - -vm_obj mk_tactic_exception(throwable const & ex, tactic_state const & s) { - return tactic::mk_exception(ex, s); -} - -vm_obj mk_tactic_exception(format const & fmt, tactic_state const & s) { - vm_state const & S = get_vm_state(); - if (optional K = S.get_decl(get_combinator_K_name())) { - return mk_tactic_exception(mk_vm_closure(K->get_idx(), to_obj(fmt), mk_vm_unit(), mk_vm_unit()), s); - } else { - throw exception("failed to create tactic exceptional result, combinator.K is not in the environment, " - "this can happen when users are hacking the init folder"); - } -} - -vm_obj mk_tactic_exception(char const * msg, tactic_state const & s) { - return mk_tactic_exception(format(msg), s); -} - -vm_obj mk_tactic_exception(sstream const & strm, tactic_state const & s) { - return mk_tactic_exception(strm.str().c_str(), s); -} - -vm_obj mk_tactic_exception(std::function const & thunk, tactic_state const & s) { - return mk_tactic_exception(mk_vm_format_thunk(thunk), s); + return to_obj(pp_expr(tactic::to_state(s), to_expr(e))); } vm_obj mk_no_goals_exception(tactic_state const & s) { - return mk_tactic_exception("tactic failed, there are no goals to be solved", s); + return tactic::mk_exception("tactic failed, there are no goals to be solved", s); } vm_obj tactic_result(vm_obj const & o) { - tactic_state const & s = to_tactic_state(o); + tactic_state const & s = tactic::to_state(o); metavar_context mctx = s.mctx(); expr r = mctx.instantiate_mvars(s.main()); - return mk_tactic_success(to_obj(r), set_mctx(s, mctx)); + return tactic::mk_success(to_obj(r), set_mctx(s, mctx)); } vm_obj tactic_format_result(vm_obj const & o) { - tactic_state const & s = to_tactic_state(o); + tactic_state const & s = tactic::to_state(o); metavar_context mctx = s.mctx(); expr r = mctx.instantiate_mvars(s.main()); metavar_decl main_decl = mctx.get_metavar_decl(s.main()); type_context ctx(s.env(), s.get_options(), mctx, main_decl.get_context(), transparency_mode::All); formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); formatter fmt = fmtf(s.env(), s.get_options(), ctx); - return mk_tactic_success(to_obj(fmt(r)), s); + return tactic::mk_success(to_obj(fmt(r)), s); } vm_obj tactic_target(vm_obj const & o) { - tactic_state const & s = to_tactic_state(o); + tactic_state const & s = tactic::to_state(o); optional g = s.get_main_goal_decl(); if (!g) return mk_no_goals_exception(s); - return mk_tactic_success(to_obj(g->get_type()), s); + return tactic::mk_success(to_obj(g->get_type()), s); } MK_THREAD_LOCAL_GET_DEF(type_context_cache_manager, get_tcm); @@ -385,11 +284,11 @@ type_context mk_type_context_for(tactic_state const & s, transparency_mode m) { } type_context mk_type_context_for(vm_obj const & s) { - return mk_type_context_for(to_tactic_state(s)); + return mk_type_context_for(tactic::to_state(s)); } type_context mk_type_context_for(vm_obj const & s, vm_obj const & m) { - return mk_type_context_for(to_tactic_state(s), to_transparency_mode(m)); + return mk_type_context_for(tactic::to_state(s), to_transparency_mode(m)); } static void check_closed(char const * tac_name, expr const & e) { @@ -400,123 +299,123 @@ static void check_closed(char const * tac_name, expr const & e) { } vm_obj tactic_infer_type(vm_obj const & e, vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); + tactic_state const & s = tactic::to_state(s0); type_context ctx = mk_type_context_for(s); try { check_closed("infer_type", to_expr(e)); - return mk_tactic_success(to_obj(ctx.infer(to_expr(e))), s); + return tactic::mk_success(to_obj(ctx.infer(to_expr(e))), s); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } vm_obj tactic_whnf(vm_obj const & e, vm_obj const & t, vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); + tactic_state const & s = tactic::to_state(s0); type_context ctx = mk_type_context_for(s, to_transparency_mode(t)); try { check_closed("whnf", to_expr(e)); - return mk_tactic_success(to_obj(ctx.whnf(to_expr(e))), s); + return tactic::mk_success(to_obj(ctx.whnf(to_expr(e))), s); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } vm_obj tactic_eta_expand(vm_obj const & e, vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); + tactic_state const & s = tactic::to_state(s0); type_context ctx = mk_type_context_for(s); try { check_closed("eta_expand", to_expr(e)); - return mk_tactic_success(to_obj(ctx.eta_expand(to_expr(e))), s); + return tactic::mk_success(to_obj(ctx.eta_expand(to_expr(e))), s); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } vm_obj tactic_eta(vm_obj const & e, vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); + tactic_state const & s = tactic::to_state(s0); try { - return mk_tactic_success(to_obj(try_eta(to_expr(e))), s); + return tactic::mk_success(to_obj(try_eta(to_expr(e))), s); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } vm_obj tactic_beta(vm_obj const & e, vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); + tactic_state const & s = tactic::to_state(s0); try { - return mk_tactic_success(to_obj(annotated_head_beta_reduce(to_expr(e))), s); + return tactic::mk_success(to_obj(annotated_head_beta_reduce(to_expr(e))), s); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } vm_obj tactic_zeta(vm_obj const & e0, vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); + tactic_state const & s = tactic::to_state(s0); try { expr const & e = to_expr(e0); check_closed("zeta", e); - if (!is_local(e)) return mk_tactic_success(e0, s); + if (!is_local(e)) return tactic::mk_success(e0, s); optional mdecl = s.get_main_goal_decl(); - if (!mdecl) return mk_tactic_success(e0, s); + if (!mdecl) return tactic::mk_success(e0, s); local_context lctx = mdecl->get_context(); optional ldecl = lctx.find_local_decl(e); - if (!ldecl || !ldecl->get_value()) return mk_tactic_success(e0, s); - return mk_tactic_success(to_obj(*ldecl->get_value()), s); + if (!ldecl || !ldecl->get_value()) return tactic::mk_success(e0, s); + return tactic::mk_success(to_obj(*ldecl->get_value()), s); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } vm_obj tactic_is_class(vm_obj const & e, vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); + tactic_state const & s = tactic::to_state(s0); type_context ctx = mk_type_context_for(s); try { check_closed("is_class", to_expr(e)); - return mk_tactic_success(mk_vm_bool(static_cast(ctx.is_class(to_expr(e)))), s); + return tactic::mk_success(mk_vm_bool(static_cast(ctx.is_class(to_expr(e)))), s); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } vm_obj tactic_mk_instance(vm_obj const & e, vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); + tactic_state const & s = tactic::to_state(s0); type_context ctx = mk_type_context_for(s); try { check_closed("mk_instance", to_expr(e)); if (auto r = ctx.mk_class_instance(to_expr(e))) { tactic_state new_s = set_mctx(s, ctx.mctx()); - return mk_tactic_success(to_obj(*r), new_s); + return tactic::mk_success(to_obj(*r), new_s); } else { auto thunk = [=]() { format m("tactic.mk_instance failed to generate instance for"); m += pp_indented_expr(s, to_expr(e)); return m; }; - return mk_tactic_exception(thunk, s); + return tactic::mk_exception(thunk, s); } } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } vm_obj tactic_unify(vm_obj const & e1, vm_obj const & e2, vm_obj const & t, vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); + tactic_state const & s = tactic::to_state(s0); type_context ctx = mk_type_context_for(s, to_transparency_mode(t)); try { check_closed("unify", to_expr(e1)); check_closed("unify", to_expr(e2)); bool r = ctx.is_def_eq(to_expr(e1), to_expr(e2)); if (r) - return mk_tactic_success(set_mctx(s, ctx.mctx())); + return tactic::mk_success(set_mctx(s, ctx.mctx())); else - return mk_tactic_exception("unify tactic failed", s); + return tactic::mk_exception("unify tactic failed", s); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } vm_obj tactic_is_def_eq(vm_obj const & e1, vm_obj const & e2, vm_obj const & t, vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); + tactic_state const & s = tactic::to_state(s0); type_context ctx = mk_type_context_for(s, to_transparency_mode(t)); type_context::tmp_mode_scope scope(ctx); try { @@ -524,36 +423,36 @@ vm_obj tactic_is_def_eq(vm_obj const & e1, vm_obj const & e2, vm_obj const & t, check_closed("is_def_eq", to_expr(e2)); bool r = ctx.is_def_eq(to_expr(e1), to_expr(e2)); if (r) - return mk_tactic_success(s); + return tactic::mk_success(s); else - return mk_tactic_exception("is_def_eq failed", s); + return tactic::mk_exception("is_def_eq failed", s); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } vm_obj tactic_get_local(vm_obj const & n, vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); + tactic_state const & s = tactic::to_state(s0); optional g = s.get_main_goal_decl(); if (!g) return mk_no_goals_exception(s); local_context lctx = g->get_context(); optional d = lctx.find_local_decl_from_user_name(to_name(n)); - if (!d) return mk_tactic_exception(sstream() << "get_local tactic failed, unknown '" << to_name(n) << "' local", s); - return mk_tactic_success(to_obj(d->mk_ref()), s); + if (!d) return tactic::mk_exception(sstream() << "get_local tactic failed, unknown '" << to_name(n) << "' local", s); + return tactic::mk_success(to_obj(d->mk_ref()), s); } vm_obj tactic_local_context(vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); + tactic_state const & s = tactic::to_state(s0); optional g = s.get_main_goal_decl(); if (!g) return mk_no_goals_exception(s); local_context lctx = g->get_context(); buffer r; lctx.for_each([&](local_decl const & d) { r.push_back(d.mk_ref()); }); - return mk_tactic_success(to_obj(to_list(r)), s); + return tactic::mk_success(to_obj(to_list(r)), s); } vm_obj tactic_get_unused_name(vm_obj const & n, vm_obj const & vm_i, vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); + tactic_state const & s = tactic::to_state(s0); optional g = s.get_main_goal_decl(); if (!g) return mk_no_goals_exception(s); name unused_name; @@ -563,7 +462,7 @@ vm_obj tactic_get_unused_name(vm_obj const & n, vm_obj const & vm_i, vm_obj cons unsigned i = force_to_unsigned(get_some_value(vm_i), 0); unused_name = g->get_context().get_unused_name(to_name(n), i); } - return mk_tactic_success(to_obj(unused_name), s); + return tactic::mk_success(to_obj(unused_name), s); } vm_obj rotate_left(unsigned n, tactic_state const & s) { @@ -571,19 +470,19 @@ vm_obj rotate_left(unsigned n, tactic_state const & s) { to_buffer(s.goals(), gs); unsigned sz = gs.size(); if (sz == 0) - return mk_tactic_success(s); + return tactic::mk_success(s); n = n%sz; std::rotate(gs.begin(), gs.begin() + n, gs.end()); - return mk_tactic_success(set_goals(s, to_list(gs))); + return tactic::mk_success(set_goals(s, to_list(gs))); } vm_obj tactic_rotate_left(vm_obj const & n, vm_obj const & s) { - return rotate_left(force_to_unsigned(n, 0), to_tactic_state(s)); + return rotate_left(force_to_unsigned(n, 0), tactic::to_state(s)); } vm_obj tactic_get_goals(vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); - return mk_tactic_success(to_obj(s.goals()), s); + tactic_state const & s = tactic::to_state(s0); + return tactic::mk_success(to_obj(s.goals()), s); } vm_obj set_goals(list const & gs, tactic_state const & s) { @@ -591,70 +490,70 @@ vm_obj set_goals(list const & gs, tactic_state const & s) { metavar_context const & mctx = s.mctx(); for (expr const & g : gs) { if (!mctx.find_metavar_decl(g)) { - return mk_tactic_exception("invalid set_goals tactic, expressions must be meta-variables " + return tactic::mk_exception("invalid set_goals tactic, expressions must be meta-variables " "that have been declared in the current tactic_state", s); } if (!mctx.is_assigned(g)) new_gs.push_back(g); } - return mk_tactic_success(set_goals(s, to_list(new_gs))); + return tactic::mk_success(set_goals(s, to_list(new_gs))); } vm_obj tactic_set_goals(vm_obj const & gs, vm_obj const & s) { - return set_goals(to_list_expr(gs), to_tactic_state(s)); + return set_goals(to_list_expr(gs), tactic::to_state(s)); } vm_obj tactic_mk_meta_univ(vm_obj const & s) { - metavar_context mctx = to_tactic_state(s).mctx(); + metavar_context mctx = tactic::to_state(s).mctx(); level u = mctx.mk_univ_metavar_decl(); - return mk_tactic_success(to_obj(u), set_mctx(to_tactic_state(s), mctx)); + return tactic::mk_success(to_obj(u), set_mctx(tactic::to_state(s), mctx)); } vm_obj tactic_mk_meta_var(vm_obj const & t, vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); + tactic_state const & s = tactic::to_state(s0); metavar_context mctx = s.mctx(); local_context lctx; if (optional g = s.get_main_goal_decl()) { lctx = g->get_context(); } expr m = mctx.mk_metavar_decl(lctx, to_expr(t)); - return mk_tactic_success(to_obj(m), set_mctx(s, mctx)); + return tactic::mk_success(to_obj(m), set_mctx(s, mctx)); } vm_obj tactic_get_univ_assignment(vm_obj const & u, vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); + tactic_state const & s = tactic::to_state(s0); metavar_context mctx = s.mctx(); if (!is_meta(to_level(u))) { - return mk_tactic_exception("get_univ_assignment tactic failed, argument is not an universe metavariable", s); + return tactic::mk_exception("get_univ_assignment tactic failed, argument is not an universe metavariable", s); } else if (auto r = mctx.get_assignment(to_level(u))) { - return mk_tactic_success(to_obj(*r), s); + return tactic::mk_success(to_obj(*r), s); } else { - return mk_tactic_exception("get_univ_assignment tactic failed, universe metavariable is not assigned", s); + return tactic::mk_exception("get_univ_assignment tactic failed, universe metavariable is not assigned", s); } } vm_obj tactic_get_assignment(vm_obj const & e, vm_obj const & s0) { - tactic_state const & s = to_tactic_state(s0); + tactic_state const & s = tactic::to_state(s0); metavar_context mctx = s.mctx(); if (!is_metavar(to_expr(e))) { - return mk_tactic_exception("get_assignment tactic failed, argument is not an universe metavariable", s); + return tactic::mk_exception("get_assignment tactic failed, argument is not an universe metavariable", s); } else if (auto r = mctx.get_assignment(to_expr(e))) { - return mk_tactic_success(to_obj(*r), s); + return tactic::mk_success(to_obj(*r), s); } else { - return mk_tactic_exception("get_assignment tactic failed, metavariable is not assigned", s); + return tactic::mk_exception("get_assignment tactic failed, metavariable is not assigned", s); } } vm_obj tactic_state_get_options(vm_obj const & s) { - return to_obj(to_tactic_state(s).get_options()); + return to_obj(tactic::to_state(s).get_options()); } vm_obj tactic_state_set_options(vm_obj const & s, vm_obj const & o) { - return to_obj(set_options(to_tactic_state(s), to_options(o))); + return to_obj(set_options(tactic::to_state(s), to_options(o))); } vm_obj tactic_mk_fresh_name(vm_obj const & s) { - return mk_tactic_success(to_obj(mk_fresh_name()), to_tactic_state(s)); + return tactic::mk_success(to_obj(mk_fresh_name()), tactic::to_state(s)); } vm_obj tactic_is_trace_enabled_for(vm_obj const & n) { @@ -662,54 +561,54 @@ vm_obj tactic_is_trace_enabled_for(vm_obj const & n) { } vm_obj tactic_instantiate_mvars(vm_obj const & e, vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); metavar_context mctx = s.mctx(); expr r = mctx.instantiate_mvars(to_expr(e)); - return mk_tactic_success(to_obj(r), set_mctx(s, mctx)); + return tactic::mk_success(to_obj(r), set_mctx(s, mctx)); } vm_obj tactic_add_decl(vm_obj const & _d, vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); try { declaration d = to_declaration(_d); environment new_env = module::add(s.env(), check(s.env(), d)); new_env = vm_compile(new_env, d); - return mk_tactic_success(set_env(s, new_env)); + return tactic::mk_success(set_env(s, new_env)); } catch (throwable & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } vm_obj tactic_open_namespaces(vm_obj const & s) { - environment env = to_tactic_state(s).env(); + environment env = tactic::to_state(s).env(); buffer b; to_buffer(get_namespaces(env), b); get_opened_namespaces(env).to_buffer(b); - return mk_tactic_success(to_obj(b), to_tactic_state(s)); + return tactic::mk_success(to_obj(b), tactic::to_state(s)); } vm_obj tactic_doc_string(vm_obj const & n, vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); if (optional doc = get_doc_string(s.env(), to_name(n))) { - return mk_tactic_success(to_obj(*doc), s); + return tactic::mk_success(to_obj(*doc), s); } else { - return mk_tactic_exception(sstream() << "no doc string for '" << to_name(n) << "'", s); + return tactic::mk_exception(sstream() << "no doc string for '" << to_name(n) << "'", s); } } vm_obj tactic_add_doc_string(vm_obj const & n, vm_obj const & doc, vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); try { environment new_env = add_doc_string(s.env(), to_name(n), to_string(doc)); - return mk_tactic_success(set_env(s, new_env)); + return tactic::mk_success(set_env(s, new_env)); } catch (throwable & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } /* meta constant module_doc_strings : tactic (list (option name × string)) */ vm_obj tactic_module_doc_strings(vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); buffer entries; get_module_doc_strings(s.env(), entries); unsigned i = entries.size(); @@ -725,12 +624,12 @@ vm_obj tactic_module_doc_strings(vm_obj const & _s) { vm_obj e = mk_vm_pair(decl_name, doc); r = mk_vm_constructor(1, e, r); } - return mk_tactic_success(r, s); + return tactic::mk_success(r, s); } vm_obj tactic_decl_name(vm_obj const & _s) { - auto & s = to_tactic_state(_s); - return mk_tactic_success(to_obj(s.decl_name()), s); + auto & s = tactic::to_state(_s); + return tactic::mk_success(to_obj(s.decl_name()), s); } format tactic_state::pp() const { @@ -761,7 +660,7 @@ format tactic_state::pp() const { } vm_obj tactic_add_aux_decl(vm_obj const & n, vm_obj const & type, vm_obj const & val, vm_obj const & lemma, vm_obj const & _s) { - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); optional g = s.get_main_goal_decl(); if (!g) return mk_no_goals_exception(s); try { @@ -769,9 +668,9 @@ vm_obj tactic_add_aux_decl(vm_obj const & n, vm_obj const & type, vm_obj const & to_bool(lemma) ? mk_aux_lemma(s.env(), s.mctx(), g->get_context(), to_name(n), to_expr(type), to_expr(val)) : mk_aux_definition(s.env(), s.mctx(), g->get_context(), to_name(n), to_expr(type), to_expr(val)); - return mk_tactic_success(to_obj(r.second), set_env(s, r.first)); + return tactic::mk_success(to_obj(r.second), set_env(s, r.first)); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h index c80174c0d5..3d83fe0171 100644 --- a/src/library/tactic/tactic_state.h +++ b/src/library/tactic/tactic_state.h @@ -125,43 +125,16 @@ template tactic_state update_option_if_undef(tactic_state const & s, template class interaction_monad; typedef interaction_monad tactic; -bool is_tactic_state(vm_obj const & o); -tactic_state const & to_tactic_state(vm_obj const & o); vm_obj to_obj(tactic_state const & s); transparency_mode to_transparency_mode(vm_obj const & o); vm_obj to_obj(transparency_mode m); -bool is_tactic_result_exception(vm_obj const & r); -bool is_tactic_result_success(vm_obj const & r); -vm_obj get_tactic_result_value(vm_obj const & r); -vm_obj get_tactic_result_state(vm_obj const & r); -vm_obj mk_tactic_result(vm_obj const & a, vm_obj const & s); - -vm_obj mk_tactic_success(vm_obj const & a, tactic_state const & s); -vm_obj mk_tactic_success(tactic_state const & s); -vm_obj mk_tactic_exception(vm_obj const & fn, tactic_state const & s); -vm_obj mk_tactic_exception(throwable const & ex, tactic_state const & s); -vm_obj mk_tactic_exception(format const & fmt, tactic_state const & s); -vm_obj mk_tactic_exception(sstream const & strm, tactic_state const & s); -vm_obj mk_tactic_exception(char const * msg, tactic_state const & s); -vm_obj mk_tactic_exception(std::function const & thunk, tactic_state const & s); -vm_obj mk_tactic_silent_exception(tactic_state const & s); vm_obj mk_no_goals_exception(tactic_state const & s); format pp_expr(tactic_state const & s, expr const & e); format pp_indented_expr(tactic_state const & s, expr const & e); -/* If r is (base_tactic_result.success a s), then return s */ -optional is_tactic_success(vm_obj const & r); - -typedef std::tuple, tactic_state> tactic_exception_info; - -/* If ex is (base_tactic_result.exception fn), then return (fn ()). - The vm_state S is used to execute (fn ()). */ -optional is_tactic_exception(vm_state & S, vm_obj const & ex); -bool is_tactic_silent_exception(vm_obj const & ex); - type_context mk_type_context_for(tactic_state const & s, transparency_mode m = transparency_mode::Semireducible); type_context mk_type_context_for(tactic_state const & s, local_context const & lctx, transparency_mode m = transparency_mode::Semireducible); type_context mk_type_context_for(environment const & env, options const & o, @@ -176,7 +149,7 @@ type_context mk_type_context_for(vm_obj const & s, vm_obj const & m); }) #define LEAN_TACTIC_TRY try { -#define LEAN_TACTIC_CATCH(S) } catch (exception const & ex) { return mk_tactic_exception(ex, S); } +#define LEAN_TACTIC_CATCH(S) } catch (exception const & ex) { return tactic::mk_exception(ex, S); } void initialize_tactic_state(); void finalize_tactic_state(); diff --git a/src/library/tactic/unfold_tactic.cpp b/src/library/tactic/unfold_tactic.cpp index 7621d04155..375523d23c 100644 --- a/src/library/tactic/unfold_tactic.cpp +++ b/src/library/tactic/unfold_tactic.cpp @@ -17,17 +17,17 @@ Author: Leonardo de Moura namespace lean { vm_obj tactic_unfold_projection_core(vm_obj const & m, vm_obj const & _e, vm_obj const & _s) { expr const & e = to_expr(_e); - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); try { expr const & fn = get_app_fn(e); type_context ctx = mk_type_context_for(s, to_transparency_mode(m)); if (!is_constant(fn) || !is_projection(s.env(), const_name(fn))) - return mk_tactic_exception("unfold projection failed, expression is not a projection application", s); + return tactic::mk_exception("unfold projection failed, expression is not a projection application", s); if (auto new_e = ctx.reduce_projection(e)) - return mk_tactic_success(to_obj(*new_e), s); - return mk_tactic_exception("unfold projection failed, failed to unfold", s); + return tactic::mk_success(to_obj(*new_e), s); + return tactic::mk_exception("unfold projection failed, failed to unfold", s); } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } @@ -59,37 +59,37 @@ optional dunfold(type_context & ctx, expr const & e) { vm_obj tactic_dunfold_expr_core(vm_obj const & m, vm_obj const & _e, vm_obj const & _s) { expr const & e = to_expr(_e); - tactic_state const & s = to_tactic_state(_s); + tactic_state const & s = tactic::to_state(_s); try { environment const & env = s.env(); expr const & fn = get_app_fn(e); if (!is_constant(fn)) - return mk_tactic_exception("dunfold_expr failed, expression is not a constant nor a constant application", s); + return tactic::mk_exception("dunfold_expr failed, expression is not a constant nor a constant application", s); if (is_projection(s.env(), const_name(fn))) { type_context ctx = mk_type_context_for(s, to_transparency_mode(m)); if (auto new_e = ctx.reduce_projection(e)) - return mk_tactic_success(to_obj(*new_e), s); - return mk_tactic_exception("dunfold_expr failed, failed to unfold projection", s); + return tactic::mk_success(to_obj(*new_e), s); + return tactic::mk_exception("dunfold_expr failed, failed to unfold projection", s); } else if (has_eqn_lemmas(env, const_name(fn))) { type_context ctx = mk_type_context_for(s, to_transparency_mode(m)); if (auto new_e = dunfold(ctx, e)) { - return mk_tactic_success(to_obj(*new_e), s); + return tactic::mk_success(to_obj(*new_e), s); } else { - return mk_tactic_exception("dunfold_expr failed, none of the rfl lemmas is applicable", s); + return tactic::mk_exception("dunfold_expr failed, none of the rfl lemmas is applicable", s); } } else { declaration d = env.get(const_name(fn)); if (!d.is_definition()) - return mk_tactic_exception(sstream() << "dunfold_expr failed, '" << d.get_name() << "' is not a definition", s); + return tactic::mk_exception(sstream() << "dunfold_expr failed, '" << d.get_name() << "' is not a definition", s); if (d.get_num_univ_params() != length(const_levels(fn))) - return mk_tactic_exception("dunfold_expr failed, incorrect number of universe levels", s); + return tactic::mk_exception("dunfold_expr failed, incorrect number of universe levels", s); buffer args; get_app_args(e, args); expr new_e = annotated_head_beta_reduce(mk_app(instantiate_value_univ_params(d, const_levels(fn)), args.size(), args.data())); - return mk_tactic_success(to_obj(new_e), s); + return tactic::mk_success(to_obj(new_e), s); } } catch (exception & ex) { - return mk_tactic_exception(ex, s); + return tactic::mk_exception(ex, s); } } diff --git a/src/library/tactic/user_attribute.cpp b/src/library/tactic/user_attribute.cpp index 8ba2ab2e54..42ef4d56a5 100644 --- a/src/library/tactic/user_attribute.cpp +++ b/src/library/tactic/user_attribute.cpp @@ -109,32 +109,32 @@ struct user_attr_modification : public modification { /* VM builtins */ vm_obj attribute_get_instances(vm_obj const & vm_n, vm_obj const & vm_s) { - auto const & s = to_tactic_state(vm_s); + auto const & s = tactic::to_state(vm_s); auto const & n = to_name(vm_n); buffer b; LEAN_TACTIC_TRY; get_attribute(s.env(), n).get_instances(s.env(), b); LEAN_TACTIC_CATCH(s); - return mk_tactic_success(to_obj(b), s); + return tactic::mk_success(to_obj(b), s); } vm_obj attribute_register(vm_obj const & vm_n, vm_obj const & vm_s) { - auto const & s = to_tactic_state(vm_s); + auto const & s = tactic::to_state(vm_s); auto const & n = to_name(vm_n); LEAN_TACTIC_TRY; auto env = module::add_and_perform(s.env(), std::make_shared(n)); - return mk_tactic_success(set_env(s, env)); + return tactic::mk_success(set_env(s, env)); LEAN_TACTIC_CATCH(s); } vm_obj attribute_fingerprint(vm_obj const & vm_n, vm_obj const & vm_s) { - auto const & s = to_tactic_state(vm_s); + auto const & s = tactic::to_state(vm_s); auto const & n = to_name(vm_n); unsigned h; LEAN_TACTIC_TRY; h = get_attribute(s.env(), n).get_fingerprint(s.env()); LEAN_TACTIC_CATCH(s); - return mk_tactic_success(mk_vm_nat(h), s); + return tactic::mk_success(mk_vm_nat(h), s); } /* Caching */ @@ -163,7 +163,7 @@ static bool check_dep_fingerprints(environment const & env, list const & d } vm_obj caching_user_attribute_get_cache(vm_obj const &, vm_obj const & vm_attr, vm_obj const & vm_s) { - tactic_state const & s = to_tactic_state(vm_s); + tactic_state const & s = tactic::to_state(vm_s); name const & n = to_name(cfield(vm_attr, 0)); vm_obj const & cache_handler = cfield(vm_attr, 2); list const & deps = to_list_name(cfield(vm_attr, 3)); @@ -176,7 +176,7 @@ vm_obj caching_user_attribute_get_cache(vm_obj const &, vm_obj const & vm_attr, if (it->second.m_fingerprint == attr.get_fingerprint(env) && check_dep_fingerprints(env, deps, it->second.m_dep_fingerprints) && env.is_descendant(it->second.m_env)) { - return mk_tactic_success(it->second.m_val, s); + return tactic::mk_success(it->second.m_val, s); } lean_trace("user_attributes_cache", tout() << "cached result for [" << attr.get_name() << "] " << "has been found, but cache fingerprint does not match\n";); @@ -194,7 +194,7 @@ vm_obj caching_user_attribute_get_cache(vm_obj const &, vm_obj const & vm_attr, result = invoke(cache_handler, to_obj(to_list(instances)), to_obj(s0)); was_updated = get_vm_state().env_was_updated(); } - if (is_tactic_success(result)) { + if (tactic::is_success(result)) { if (!was_updated) { user_attr_cache::entry entry; entry.m_env = env; @@ -205,12 +205,12 @@ vm_obj caching_user_attribute_get_cache(vm_obj const &, vm_obj const & vm_attr, entry.m_val = cfield(result, 0); cache.m_cache.erase(attr.get_name()); cache.m_cache.insert(mk_pair(attr.get_name(), entry)); - return mk_tactic_success(entry.m_val, s); + return tactic::mk_success(entry.m_val, s); } else { lean_trace("user_attributes_cache", tout() << "did not cache result for [" << attr.get_name() << "] " "because VM environment has been updated with temporary declarations\n";); vm_obj r = cfield(result, 0); - return mk_tactic_success(r, s); + return tactic::mk_success(r, s); } } else { return result; @@ -226,15 +226,15 @@ vm_obj set_basic_attribute(vm_obj const & vm_attr_n, vm_obj const & vm_n, vm_obj prio = LEAN_DEFAULT_PRIORITY; else prio = force_to_unsigned(get_some_value(vm_prio), std::numeric_limits::max()); - tactic_state const & s = to_tactic_state(vm_s); + tactic_state const & s = tactic::to_state(vm_s); LEAN_TACTIC_TRY; attribute const & attr = get_attribute(s.env(), attr_n); if (basic_attribute const * basic_attr = dynamic_cast(&attr)) { bool persistent = to_bool(p); environment new_env = basic_attr->set(s.env(), get_global_ios(), n, prio, persistent); - return mk_tactic_success(set_env(s, new_env)); + return tactic::mk_success(set_env(s, new_env)); } else { - return mk_tactic_exception(sstream() << "set_basic_attribute tactic failed, '" << attr_n << "' is not a basic attribute", s); + return tactic::mk_exception(sstream() << "set_basic_attribute tactic failed, '" << attr_n << "' is not a basic attribute", s); } LEAN_TACTIC_CATCH(s); } @@ -242,26 +242,26 @@ vm_obj set_basic_attribute(vm_obj const & vm_attr_n, vm_obj const & vm_n, vm_obj vm_obj unset_attribute(vm_obj const & vm_attr_n, vm_obj const & vm_n, vm_obj const & vm_s) { name const & attr_n = to_name(vm_attr_n); name const & n = to_name(vm_n); - tactic_state const & s = to_tactic_state(vm_s); + tactic_state const & s = tactic::to_state(vm_s); LEAN_TACTIC_TRY; attribute const & attr = get_attribute(s.env(), attr_n); bool persistent = false; environment new_env = attr.unset(s.env(), get_global_ios(), n, persistent); - return mk_tactic_success(set_env(s, new_env)); + return tactic::mk_success(set_env(s, new_env)); LEAN_TACTIC_CATCH(s); } vm_obj has_attribute(vm_obj const & vm_attr_n, vm_obj const & vm_n, vm_obj const & vm_s) { name const & attr_n = to_name(vm_attr_n); name const & n = to_name(vm_n); - tactic_state const & s = to_tactic_state(vm_s); + tactic_state const & s = tactic::to_state(vm_s); LEAN_TACTIC_TRY; attribute const & attr = get_attribute(s.env(), attr_n); if (attr.is_instance(s.env(), n)) { unsigned prio = attr.get_prio(s.env(), n); - return mk_tactic_success(mk_vm_nat(prio), s); + return tactic::mk_success(mk_vm_nat(prio), s); } else { - return mk_tactic_exception(sstream() << "'" << n << "' is not tagged with attribute '" << attr_n << "'", s); + return tactic::mk_exception(sstream() << "'" << n << "' is not tagged with attribute '" << attr_n << "'", s); } LEAN_TACTIC_CATCH(s); } diff --git a/src/library/tactic/vm_monitor.cpp b/src/library/tactic/vm_monitor.cpp index 719a3602df..bf55e856db 100644 --- a/src/library/tactic/vm_monitor.cpp +++ b/src/library/tactic/vm_monitor.cpp @@ -29,10 +29,10 @@ Author: Leonardo de Moura namespace lean { vm_obj _vm_monitor_register(vm_obj const & vm_n, vm_obj const & vm_s) { - auto const & s = to_tactic_state(vm_s); + auto const & s = tactic::to_state(vm_s); auto const & n = to_name(vm_n); LEAN_TACTIC_TRY; - return mk_tactic_success(set_env(s, vm_monitor_register(s.env(), n))); + return tactic::mk_success(set_env(s, vm_monitor_register(s.env(), n))); LEAN_TACTIC_CATCH(s); } @@ -69,7 +69,7 @@ vm_obj _vm_obj_kind(vm_obj const & o) { else if (is_expr(o)) return mk_vm_simple(7); else if (is_declaration(o)) return mk_vm_simple(8); else if (is_env(o)) return mk_vm_simple(9); - else if (is_tactic_state(o)) return mk_vm_simple(10); + else if (tactic::is_state(o)) return mk_vm_simple(10); else if (is_format(o)) return mk_vm_simple(11); else if (is_options(o)) return mk_vm_simple(12); else return mk_vm_simple(13); @@ -158,7 +158,7 @@ vm_obj vm_obj_to_environment(vm_obj const & o) { } vm_obj vm_obj_to_tactic_state(vm_obj const & o) { - if (is_tactic_state(o)) + if (tactic::is_state(o)) return o; else return to_obj(mk_tactic_state_for(environment(), options(), {}, local_context(), mk_Prop())); @@ -318,8 +318,8 @@ vm_obj vm_pp_stack_obj(vm_obj const & i, vm_obj const & /*s*/) { } catch (exception &) { r = default_format(vm, idx); } - } else if (is_tactic_state(o)) { - r = to_tactic_state(o).pp_core(); + } else if (tactic::is_state(o)) { + r = tactic::to_state(o).pp_core(); } else if (is_env(o)) { r = format("[environment]"); } else { diff --git a/src/library/vm/interaction_state.h b/src/library/vm/interaction_state.h index c47e709756..adc80660a5 100644 --- a/src/library/vm/interaction_state.h +++ b/src/library/vm/interaction_state.h @@ -64,11 +64,11 @@ struct interaction_monad { } }; - static bool is_State(vm_obj const & o) { + static bool is_state(vm_obj const & o) { return is_external(o) && dynamic_cast(to_external(o)); } - static State const & to_State(vm_obj const & o) { + static State const & to_state(vm_obj const & o) { lean_vm_check(dynamic_cast(to_external(o))); return static_cast(to_external(o))->m_val; } @@ -77,32 +77,12 @@ struct interaction_monad { return mk_vm_external(new(get_vm_allocator().allocate(sizeof(vm_State))) vm_State(s)); } - static bool is_success(vm_obj const & o) { - return is_constructor(o) && cidx(o) == 0; - } - - typedef std::tuple, State> exception_info; - - static optional is_exception(vm_state & S, vm_obj const & ex) { - if (is_constructor(ex) && cidx(ex) == 1 && !is_none(cfield(ex, 0))) { - vm_obj fmt = S.invoke(get_some_value(cfield(ex, 0)), mk_vm_unit()); - optional pos; - if (!is_none(cfield(ex, 1))) { - auto vm_pos = get_some_value(cfield(ex, 1)); - pos = some(mk_pair(to_unsigned(cfield(vm_pos, 0)), to_unsigned(cfield(vm_pos, 1)))); - } - return optional(to_format(fmt), pos, to_State(cfield(ex, 2))); - } else { - return optional(); - } - } - static bool is_silent_exception(vm_obj const & ex) { return is_constructor(ex) && cidx(ex) == 1 && is_none(cfield(ex, 0)); } static vm_obj mk_result(vm_obj const & a, vm_obj const & s) { - lean_assert(is_State(s)); + lean_assert(is_state(s)); return mk_vm_constructor(0, a, s); } @@ -184,6 +164,31 @@ struct interaction_monad { } } + /* If r is (interaction_monad.result.success a s), then return s */ + static optional is_success(vm_obj const & r) { + if (is_result_success(r)) + return some(to_state(cfield(r, 1))); + return {}; + } + + typedef std::tuple, State> exception_info; + + /* If ex is (interaction_monad.result.exception (some fn) _ _), then return (fn ()). + The vm_state S is used to execute (fn ()). */ + static optional is_exception(vm_state & S, vm_obj const & ex) { + if (is_result_exception(ex) && !is_none(cfield(ex, 0))) { + vm_obj fmt = S.invoke(get_some_value(cfield(ex, 0)), mk_vm_unit()); + optional p; + if (!is_none(cfield(ex, 1))) { + auto vm_p = get_some_value(cfield(ex, 1)); + p = some(mk_pair(to_unsigned(cfield(vm_p, 0)), to_unsigned(cfield(vm_p, 1)))); + } + return optional(to_format(fmt), p, to_state(cfield(ex, 2))); + } else { + return {}; + } + } + class evaluator { type_context & m_ctx; options const & m_opts; diff --git a/src/library/vm/vm_parser.cpp b/src/library/vm/vm_parser.cpp index a808c3e599..23417b9255 100644 --- a/src/library/vm/vm_parser.cpp +++ b/src/library/vm/vm_parser.cpp @@ -41,13 +41,13 @@ vm_obj run_parser(parser & p, expr const & spec) { } vm_obj vm_parser_state_cur_pos(vm_obj const & o) { - auto const & s = lean_parser::to_State(o); + auto const & s = lean_parser::to_state(o); auto pos = s.m_p->pos(); return mk_vm_pair(mk_vm_nat(pos.first), mk_vm_nat(pos.second)); } vm_obj vm_parser_ident(vm_obj const & o) { - auto const & s = lean_parser::to_State(o); + auto const & s = lean_parser::to_state(o); TRY; name ident = s.m_p->check_id_next("identifier expected"); return lean_parser::mk_success(to_obj(ident), s); @@ -55,7 +55,7 @@ vm_obj vm_parser_ident(vm_obj const & o) { } vm_obj vm_parser_tk(vm_obj const & vm_tk, vm_obj const & o) { - auto const & s = lean_parser::to_State(o); + auto const & s = lean_parser::to_state(o); TRY; name tk = to_string(vm_tk); if (!s.m_p->curr_is_token(tk)) @@ -66,7 +66,7 @@ vm_obj vm_parser_tk(vm_obj const & vm_tk, vm_obj const & o) { } vm_obj vm_parser_qexpr(vm_obj const & vm_rbp, vm_obj const & o) { - auto const & s = lean_parser::to_State(o); + auto const & s = lean_parser::to_state(o); TRY; auto rbp = to_unsigned(vm_rbp); parser::quote_scope scope(*s.m_p, true);