diff --git a/src/library/old_tactic/tactic/apply_tactic.cpp b/src/library/old_tactic/tactic/apply_tactic.cpp deleted file mode 100644 index a532c26cf4..0000000000 --- a/src/library/old_tactic/tactic/apply_tactic.cpp +++ /dev/null @@ -1,258 +0,0 @@ -/* -Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "util/lazy_list_fn.h" -#include "util/sstream.h" -#include "util/name_map.h" -#include "util/sexpr/option_declarations.h" -#include "kernel/for_each_fn.h" -#include "kernel/replace_fn.h" -#include "kernel/instantiate.h" -#include "kernel/abstract.h" -#include "kernel/error_msgs.h" -#include "library/reducible.h" -#include "library/unifier.h" -#include "library/util.h" -#include "library/constants.h" -#include "library/class_instance_resolution.h" -#include "library/old_type_checker.h" -#include "library/tactic/expr_to_tactic.h" -#include "library/tactic/apply_tactic.h" - -#ifndef LEAN_DEFAULT_APPLY_CLASS_INSTANCE -#define LEAN_DEFAULT_APPLY_CLASS_INSTANCE true -#endif - -namespace lean { -static name * g_apply_class_instance = nullptr; -bool get_apply_class_instance(options const & opts) { - return opts.get_bool(*g_apply_class_instance, LEAN_DEFAULT_APPLY_CLASS_INSTANCE); -} - -/** - \brief Given a sequence metas: (?m_1 ...) (?m_2 ... ) ... (?m_k ...), - we say ?m_i is "redundant" if it occurs in the type of some ?m_j. - This procedure removes from metas any redundant element. -*/ -static void remove_redundant_metas(buffer & metas) { - buffer mvars; - for (expr const & m : metas) - mvars.push_back(get_app_fn(m)); - unsigned k = 0; - for (unsigned i = 0; i < metas.size(); i++) { - bool found = false; - for (unsigned j = 0; j < metas.size(); j++) { - if (j != i) { - if (occurs(mvars[i], mlocal_type(mvars[j]))) { - found = true; - break; - } - } - } - if (!found) { - metas[k] = metas[i]; - k++; - } - } - metas.shrink(k); -} - -enum subgoals_action_kind { IgnoreSubgoals, AddRevSubgoals, AddSubgoals, AddAllSubgoals }; - -enum add_meta_kind { DoNotAdd, AddDiff, AddAll }; - -static proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, - expr const & _e, buffer & cs, - add_meta_kind add_meta, subgoals_action_kind subgoals_action, - optional const & uk = optional()) { - goals const & gs = s.get_goals(); - if (empty(gs)) { - throw_no_goal_if_enabled(s); - return proof_state_seq(); - } - bool class_inst = get_apply_class_instance(ios.get_options()); - std::shared_ptr tc(mk_type_checker(env)); - goal g = head(gs); - goals tail_gs = tail(gs); - expr t = g.get_type(); - expr e = _e; - auto e_t_cs = tc->infer(e); - e_t_cs.second.linearize(cs); - expr e_t = e_t_cs.first; - buffer metas; - old_local_context ctx; - bool initialized_ctx = false; - unifier_config cfg(ios.get_options()); - if (uk) - cfg.m_kind = *uk; - if (add_meta != DoNotAdd) { - unsigned num_e_t = get_expect_num_args(tc->get_type_context(), e_t); - if (add_meta == AddDiff) { - unsigned num_t = get_expect_num_args(tc->get_type_context(), t); - if (num_t <= num_e_t) - num_e_t -= num_t; - else - num_e_t = 0; - } else { - lean_assert(add_meta == AddAll); - } - for (unsigned i = 0; i < num_e_t; i++) { - auto e_t_cs = tc->whnf(e_t); - e_t_cs.second.linearize(cs); - e_t = e_t_cs.first; - expr meta; - if (class_inst && binding_info(e_t).is_inst_implicit()) { - if (!initialized_ctx) { - ctx = g.to_local_context(); - initialized_ctx = true; - } - bool use_local_insts = true; - bool is_strict = false; - auto mc = mk_class_instance_elaborator( - env, ios, ctx, optional(), - use_local_insts, is_strict, - some_expr(head_beta_reduce(binding_domain(e_t))), e.get_tag(), nullptr); - meta = mc.first; - cs.push_back(mc.second); - } else { - meta = g.mk_meta(mk_fresh_name(), head_beta_reduce(binding_domain(e_t))); - } - e = mk_app(e, meta); - e_t = instantiate(binding_body(e_t), meta); - metas.push_back(meta); - } - } - pair dcs = tc->is_def_eq(t, e_t); - if (!dcs.first) { - throw_tactic_exception_if_enabled(s, [=](formatter const & fmt) { - format r = format("invalid 'apply' tactic, failed to unify"); - r += pp_indent_expr(fmt, t); - r += compose(line(), format("with")); - r += pp_indent_expr(fmt, e_t); - return r; - }); - return proof_state_seq(); - } - dcs.second.linearize(cs); - unify_result_seq rseq = unify(env, cs.size(), cs.data(), s.get_subst(), cfg); - list meta_lst = to_list(metas.begin(), metas.end()); - return map2(rseq, [=](pair const & p) -> proof_state { - substitution const & subst = p.first; - constraints const & postponed = p.second; - substitution new_subst = subst; - expr new_e = new_subst.instantiate_all(e); - assign(new_subst, g, new_e); - goals new_gs = tail_gs; - if (subgoals_action != IgnoreSubgoals) { - buffer metas; - for (auto m : meta_lst) { - if (!new_subst.is_assigned(get_app_fn(m))) - metas.push_back(m); - } - if (subgoals_action == AddRevSubgoals) { - for (unsigned i = 0; i < metas.size(); i++) - new_gs = cons(goal(metas[i], new_subst.instantiate_all(tc->infer(metas[i]).first)), new_gs); - } else { - lean_assert(subgoals_action == AddSubgoals || subgoals_action == AddAllSubgoals); - if (subgoals_action == AddSubgoals) - remove_redundant_metas(metas); - unsigned i = metas.size(); - while (i > 0) { - --i; - new_gs = cons(goal(metas[i], new_subst.instantiate_all(tc->infer(metas[i]).first)), new_gs); - } - } - } - return proof_state(s, new_gs, new_subst, postponed); - }); -} - -proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, constraint_seq const & cs) { - buffer tmp_cs; - cs.linearize(tmp_cs); - return apply_tactic_core(env, ios, s, e, tmp_cs, AddDiff, AddSubgoals); -} - -proof_state_seq fapply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, constraint_seq const & cs) { - buffer tmp_cs; - cs.linearize(tmp_cs); - return apply_tactic_core(env, ios, s, e, tmp_cs, AddDiff, AddAllSubgoals); -} - -tactic apply_tactic_core(expr const & e, constraint_seq const & cs) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { - return apply_tactic_core(env, ios, s, e, cs); - }); -} - -tactic apply_tactic_core(elaborate_fn const & elab, expr const & e, add_meta_kind add_meta, subgoals_action_kind k) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { - goals const & gs = s.get_goals(); - if (empty(gs)) { - throw_no_goal_if_enabled(s); - return proof_state_seq(); - } - goal const & g = head(gs); - expr new_e; substitution new_subst; constraints cs_; - try { - auto ecs = elab(g, ios.get_options(), e, none_expr(), s.get_subst(), false); - std::tie(new_e, new_subst, cs_) = ecs; - buffer cs; - to_buffer(cs_, cs); - to_buffer(s.get_postponed(), cs); - proof_state new_s(s, new_subst, constraints()); - return apply_tactic_core(env, ios, new_s, new_e, cs, add_meta, k); - } catch (exception &) { - if (s.report_failure()) - throw; - else - return proof_state_seq(); - } - }); -} - -tactic apply_tactic(elaborate_fn const & elab, expr const & e) { - return apply_tactic_core(elab, e, AddDiff, AddSubgoals); -} - -tactic fapply_tactic(elaborate_fn const & elab, expr const & e) { - return apply_tactic_core(elab, e, AddDiff, AddAllSubgoals); -} - -tactic eapply_tactic(elaborate_fn const & elab, expr const & e) { - return apply_tactic_core(elab, e, AddAll, AddSubgoals); -} - -void initialize_apply_tactic() { - g_apply_class_instance = new name{"apply", "class_instance"}; - register_bool_option(*g_apply_class_instance, LEAN_DEFAULT_APPLY_CLASS_INSTANCE, - "(apply tactic) if true apply tactic uses class-instances " - "resolution for instance implicit arguments"); - - register_tac(get_tactic_apply_name(), - [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - check_tactic_expr(app_arg(e), "invalid 'apply' tactic, invalid argument"); - return apply_tactic(fn, get_tactic_expr_expr(app_arg(e))); - }); - - register_tac(get_tactic_eapply_name(), - [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - check_tactic_expr(app_arg(e), "invalid 'eapply' tactic, invalid argument"); - return eapply_tactic(fn, get_tactic_expr_expr(app_arg(e))); - }); - - register_tac(get_tactic_fapply_name(), - [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - check_tactic_expr(app_arg(e), "invalid 'fapply' tactic, invalid argument"); - return fapply_tactic(fn, get_tactic_expr_expr(app_arg(e))); - }); -} - -void finalize_apply_tactic() { - delete g_apply_class_instance; -} -} diff --git a/src/library/old_tactic/tactic/apply_tactic.h b/src/library/old_tactic/tactic/apply_tactic.h deleted file mode 100644 index d2278762da..0000000000 --- a/src/library/old_tactic/tactic/apply_tactic.h +++ /dev/null @@ -1,19 +0,0 @@ -/* -Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "library/tactic/elaborate.h" -namespace lean { -proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, constraint_seq const & cs); -proof_state_seq fapply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, constraint_seq const & cs); -tactic apply_tactic_core(expr const & e, constraint_seq const & cs = constraint_seq()); -tactic apply_tactic(elaborate_fn const & fn, expr const & e); -tactic fapply_tactic(elaborate_fn const & fn, expr const & e); -tactic eassumption_tactic(); -tactic assumption_tactic(); -void initialize_apply_tactic(); -void finalize_apply_tactic(); -} diff --git a/src/library/old_tactic/tactic/assert_tactic.cpp b/src/library/old_tactic/tactic/assert_tactic.cpp deleted file mode 100644 index 26e653712e..0000000000 --- a/src/library/old_tactic/tactic/assert_tactic.cpp +++ /dev/null @@ -1,61 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "util/fresh_name.h" -#include "kernel/abstract.h" -#include "library/constants.h" -#include "library/tactic/tactic.h" -#include "library/tactic/elaborate.h" -#include "library/tactic/expr_to_tactic.h" - -namespace lean { -expr mk_assert_tactic_expr(name const & id, expr const & e) { - return mk_app(mk_constant(get_tactic_assert_hypothesis_name()), - mk_constant(id), e); -} - -tactic assert_tactic(elaborate_fn const & elab, name const & id, expr const & e) { - return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) { - proof_state new_s = s; - goals const & gs = new_s.get_goals(); - if (!gs) { - throw_no_goal_if_enabled(s); - return none_proof_state(); - } - bool report_unassigned = true; - if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, none_expr(), report_unassigned)) { - goals const & gs = new_s.get_goals(); - goal const & g = head(gs); - expr new_meta1 = g.mk_meta(mk_fresh_name(), *new_e); - goal new_goal1(new_meta1, *new_e); - expr new_local = mk_local(mk_fresh_name(), id, *new_e, binder_info()); - buffer hyps; - g.get_hyps(hyps); - hyps.push_back(new_local); - expr new_mvar2 = mk_metavar(mk_fresh_name(), Pi(hyps, g.get_type())); - hyps.pop_back(); - expr new_meta2_core = mk_app(new_mvar2, hyps); - expr new_meta2 = mk_app(new_meta2_core, new_local); - goal new_goal2(new_meta2, g.get_type()); - substitution new_subst = new_s.get_subst(); - assign(new_subst, g, mk_app(new_meta2_core, new_meta1)); - return some_proof_state(proof_state(new_s, cons(new_goal1, cons(new_goal2, tail(gs))), new_subst)); - } - return none_proof_state(); - }); -} - -void initialize_assert_tactic() { - register_tac(get_tactic_assert_hypothesis_name(), - [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - name id = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'assert' tactic, argument must be an identifier"); - check_tactic_expr(app_arg(e), "invalid 'assert' tactic, argument must be an expression"); - return assert_tactic(fn, id, get_tactic_expr_expr(app_arg(e))); - }); -} -void finalize_assert_tactic() { -} -} diff --git a/src/library/old_tactic/tactic/assert_tactic.h b/src/library/old_tactic/tactic/assert_tactic.h deleted file mode 100644 index a320479caf..0000000000 --- a/src/library/old_tactic/tactic/assert_tactic.h +++ /dev/null @@ -1,15 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "library/tactic/tactic.h" - -namespace lean { -expr mk_assert_tactic_expr(name const & id, expr const & e); -tactic assert_tactic(elaborate_fn const & elab, name const & id, expr const & e); -void initialize_assert_tactic(); -void finalize_assert_tactic(); -} diff --git a/src/library/old_tactic/tactic/clear_tactic.cpp b/src/library/old_tactic/tactic/clear_tactic.cpp deleted file mode 100644 index e4bd6584c3..0000000000 --- a/src/library/old_tactic/tactic/clear_tactic.cpp +++ /dev/null @@ -1,73 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "util/fresh_name.h" -#include "library/constants.h" -#include "kernel/abstract.h" -#include "library/locals.h" -#include "library/tactic/tactic.h" -#include "library/tactic/expr_to_tactic.h" - -namespace lean { -tactic clear_tactic(name const & n) { - auto fn = [=](environment const &, io_state const &, proof_state const & _s) -> optional { - if (!_s.get_goals()) { - throw_no_goal_if_enabled(_s); - return none_proof_state(); - } - proof_state s = apply_substitution(_s); - goals const & gs = s.get_goals(); - goal g = head(gs); - goals tail_gs = tail(gs); - if (auto p = g.find_hyp(n)) { - expr const & h = p->first; - unsigned i = p->second; - buffer hyps; - g.get_hyps(hyps); - hyps.erase(hyps.size() - i - 1); - if (depends_on(g.get_type(), h)) { - throw_tactic_exception_if_enabled(s, sstream() << "invalid 'clear' tactic, conclusion depends on '" - << n << "'"); - return none_proof_state(); - } - if (auto h2 = depends_on(i, hyps.end() - i, h)) { - throw_tactic_exception_if_enabled(s, sstream() << "invalid 'clear' tactic, hypothesis '" << *h2 - << "' depends on '" << n << "'"); - return none_proof_state(); - } - expr new_type = g.get_type(); - expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(hyps, new_type)), hyps); - goal new_g(new_meta, new_type); - substitution new_subst = s.get_subst(); - assign(new_subst, g, new_meta); - proof_state new_s(s, goals(new_g, tail_gs), new_subst); - return some_proof_state(new_s); - } else { - throw_tactic_exception_if_enabled(s, sstream() << "invalid 'clear' tactic, goal does not have a hypothesis " - << " named '" << n << "'"); - return none_proof_state(); - } - }; - return tactic01(fn); -} - -void initialize_clear_tactic() { - auto fn = [](old_type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - buffer ns; - get_tactic_id_list_elements(app_arg(e), ns, "invalid 'clears' tactic, list of identifiers expected"); - tactic r = clear_tactic(ns.back()); - ns.pop_back(); - while (!ns.empty()) { - r = then(clear_tactic(ns.back()), r); - ns.pop_back(); - } - return r; - }; - register_tac(get_tactic_clear_name(), fn); - register_tac(get_tactic_clears_name(), fn); -} -void finalize_clear_tactic() {} -} diff --git a/src/library/old_tactic/tactic/clear_tactic.h b/src/library/old_tactic/tactic/clear_tactic.h deleted file mode 100644 index 5ab66f97a3..0000000000 --- a/src/library/old_tactic/tactic/clear_tactic.h +++ /dev/null @@ -1,14 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "library/tactic/tactic.h" - -namespace lean { -tactic clear_tactic(name const & n); -void initialize_clear_tactic(); -void finalize_clear_tactic(); -} diff --git a/src/library/old_tactic/tactic/constructor_tactic.cpp b/src/library/old_tactic/tactic/constructor_tactic.cpp deleted file mode 100644 index ff4fde1383..0000000000 --- a/src/library/old_tactic/tactic/constructor_tactic.cpp +++ /dev/null @@ -1,142 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "util/lazy_list_fn.h" -#include "kernel/instantiate.h" -#include "kernel/inductive/inductive.h" -#include "library/constants.h" -#include "library/util.h" -#include "library/reducible.h" -#include "library/tactic/expr_to_tactic.h" -#include "library/tactic/apply_tactic.h" - -namespace lean { -/** - \brief Implement multiple variations of the constructor tactic. - It tries to solve the goal by applying the i-th constructor. - If \c num_constructors is not none, then the tactic checks wether the inductive datatype has - the expected number of constructors. - If \c given_args is provided, then the tactic fixes the given arguments. - It creates a subgoal for each remaining argument. -*/ -tactic constructor_tactic(elaborate_fn const & elab, optional _i, optional num_constructors, - list const & given_args, bool use_fapply = false) { - auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) { - goals const & gs = s.get_goals(); - if (empty(gs)) { - throw_no_goal_if_enabled(s); - return proof_state_seq(); - } - constraint_seq cs; - auto tc = mk_type_checker(env); - goal const & g = head(gs); - expr t = tc->whnf(g.get_type(), cs); - buffer I_args; - expr I = get_app_args(t, I_args); - if (!is_constant(I) || !inductive::is_inductive_decl(env, const_name(I))) { - throw_tactic_exception_if_enabled(s, "invalid 'constructor' tactic, goal is not an inductive datatype"); - return proof_state_seq(); - } - buffer c_names; - get_intro_rule_names(env, const_name(I), c_names); - if (num_constructors && c_names.size() != *num_constructors) { - throw_tactic_exception_if_enabled(s, sstream() << "invalid 'constructor' tactic, goal is an inductive datatype, " - << "but it does not have " << *num_constructors << " constructor(s)"); - return proof_state_seq(); - } - - auto try_constructor = [&](proof_state const & s, unsigned i) { - if (i >= c_names.size()) { - throw_tactic_exception_if_enabled(s, sstream() << "invalid 'constructor' tactic, goal is an inductive datatype, " - << "but it has only " << c_names.size() << " constructor(s)"); - return proof_state_seq(); - } - expr C = mk_constant(c_names[i], const_levels(I)); - unsigned num_params = *inductive::get_num_params(env, const_name(I)); - if (I_args.size() < num_params) - return proof_state_seq(); - proof_state new_s(s); - C = mk_app(C, num_params, I_args.data()); - expr C_type = tc->whnf(tc->infer(C, cs), cs); - bool report_unassigned = true; - bool enforce_type = true; - for (expr const & arg : given_args) { - if (!is_pi(C_type)) { - throw_tactic_exception_if_enabled(s, sstream() << "invalid 'constructor' tactic, " - << "too many arguments have been provided"); - return proof_state_seq(); - } - try { - if (auto new_arg = elaborate_with_respect_to(env, ios, elab, new_s, arg, some_expr(binding_domain(C_type)), - report_unassigned, enforce_type)) { - C = mk_app(C, *new_arg); - C_type = tc->whnf(instantiate(binding_body(C_type), *new_arg), cs); - } else { - return proof_state_seq(); - } - } catch (exception &) { - if (new_s.report_failure()) - throw; - return proof_state_seq(); - } - } - if (use_fapply) - return fapply_tactic_core(env, ios, new_s, C, cs); - else - return apply_tactic_core(env, ios, new_s, C, cs); - }; - - if (_i) { - if (*_i == 0) { - throw_tactic_exception_if_enabled(s, "invalid 'constructor' tactic, index must be greater than zero"); - return proof_state_seq(); - } - return try_constructor(s, *_i - 1); - } else { - proof_state new_s = s.update_report_failure(false); - proof_state_seq r; - for (unsigned i = 0; i < c_names.size(); i++) - r = append(r, try_constructor(new_s, i)); - return r; - } - }; - return tactic(fn); -} - -void initialize_constructor_tactic() { - register_tac(name{"tactic", "constructor"}, - [](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - auto i = get_optional_unsigned(tc, app_arg(e)); - return constructor_tactic(fn, i, optional(), list()); - }); - register_tac(name{"tactic", "fconstructor"}, - [](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - auto i = get_optional_unsigned(tc, app_arg(e)); - return constructor_tactic(fn, i, optional(), list(), true); - }); - register_tac(name{"tactic", "split"}, - [](old_type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) { - return constructor_tactic(fn, optional(1), optional(1), list()); - }); - register_tac(name{"tactic", "left"}, - [](old_type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) { - return constructor_tactic(fn, optional(1), optional(2), list()); - }); - register_tac(name{"tactic", "right"}, - [](old_type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) { - return constructor_tactic(fn, optional(2), optional(2), list()); - }); - register_tac(name{"tactic", "existsi"}, - [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - check_tactic_expr(app_arg(e), "invalid 'existsi' tactic, invalid argument"); - expr arg = get_tactic_expr_expr(app_arg(e)); - return constructor_tactic(fn, optional(1), optional(1), list(arg)); - }); -} - -void finalize_constructor_tactic() { -} -} diff --git a/src/library/old_tactic/tactic/constructor_tactic.h b/src/library/old_tactic/tactic/constructor_tactic.h deleted file mode 100644 index a5437f5424..0000000000 --- a/src/library/old_tactic/tactic/constructor_tactic.h +++ /dev/null @@ -1,11 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -namespace lean { -void initialize_constructor_tactic(); -void finalize_constructor_tactic(); -} diff --git a/src/library/old_tactic/tactic/contradiction_tactic.cpp b/src/library/old_tactic/tactic/contradiction_tactic.cpp deleted file mode 100644 index 19bfba0656..0000000000 --- a/src/library/old_tactic/tactic/contradiction_tactic.cpp +++ /dev/null @@ -1,94 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "kernel/inductive/inductive.h" -#include "library/constants.h" -#include "library/util.h" -#include "library/reducible.h" -#include "library/tactic/intros_tactic.h" -#include "library/tactic/expr_to_tactic.h" -#include "kernel/kernel_exception.h" - -namespace lean { -tactic contradiction_tactic() { - auto fn = [=](environment const & env, io_state const &, proof_state const & s) { - goals const & gs = s.get_goals(); - if (empty(gs)) { - throw_no_goal_if_enabled(s); - return optional(); - } - goal const & g = head(gs); - expr const & t = g.get_type(); - substitution subst = s.get_subst(); - auto tc = mk_type_checker(env); - auto conserv_tc = mk_type_checker(env, UnfoldReducible); - buffer hyps; - g.get_hyps(hyps); - for (expr const & h : hyps) { - expr h_type = mlocal_type(h); - h_type = tc->whnf(h_type).first; - expr lhs, rhs, arg; - if (is_false(env, h_type)) { - assign(subst, g, mk_false_rec(*tc, h, t)); - return some_proof_state(proof_state(s, tail(gs), subst)); - } else if (is_not(env, h_type, arg)) { - optional h_pos; - for (expr const & h_prime : hyps) { - constraint_seq cs; - if (conserv_tc->is_def_eq(arg, mlocal_type(h_prime), justification(), cs) && !cs) { - h_pos = h_prime; - break; - } - } - if (h_pos) { - assign(subst, g, mk_absurd(*tc, t, *h_pos, h)); - return some_proof_state(proof_state(s, tail(gs), subst)); - } - } else if (is_eq(h_type, lhs, rhs)) { - lhs = tc->whnf(lhs).first; - rhs = tc->whnf(rhs).first; - optional lhs_c = is_constructor_app(env, lhs); - optional rhs_c = is_constructor_app(env, rhs); - if (lhs_c && rhs_c && *lhs_c != *rhs_c) { - if (optional I_name = inductive::is_intro_rule(env, *lhs_c)) { - name no_confusion(*I_name, "no_confusion"); - try { - expr I = tc->whnf(tc->infer(lhs).first).first; - buffer args; - expr I_fn = get_app_args(I, args); - if (is_constant(I_fn)) { - level t_lvl = sort_level(tc->ensure_type(t).first); - expr V = mk_app(mk_app(mk_constant(no_confusion, cons(t_lvl, const_levels(I_fn))), args), - t, lhs, rhs, h); - if (auto r = lift_down_if_hott(*tc, V)) { - check_term(*tc, *r); - assign(subst, g, *r); - return some_proof_state(proof_state(s, tail(gs), subst)); - } - } - } catch (kernel_exception & ex) { - // TODO(Leo) - // regular(env, ios) << ex << "\n"; - } - } - } - } - } - return none_proof_state(); - }; - return tactic01(fn); -} - -void initialize_contradiction_tactic() { - register_tac(name{"tactic", "contradiction"}, - [](old_type_checker &, elaborate_fn const &, expr const &, pos_info_provider const *) { - list empty; - return then(orelse(intros_tactic(empty), id_tactic()), contradiction_tactic()); - }); -} -void finalize_contradiction_tactic() { -} -} diff --git a/src/library/old_tactic/tactic/contradiction_tactic.h b/src/library/old_tactic/tactic/contradiction_tactic.h deleted file mode 100644 index c21c85cb7c..0000000000 --- a/src/library/old_tactic/tactic/contradiction_tactic.h +++ /dev/null @@ -1,11 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -namespace lean { -void initialize_contradiction_tactic(); -void finalize_contradiction_tactic(); -} diff --git a/src/library/old_tactic/tactic/exact_tactic.cpp b/src/library/old_tactic/tactic/exact_tactic.cpp deleted file mode 100644 index 45c63967a4..0000000000 --- a/src/library/old_tactic/tactic/exact_tactic.cpp +++ /dev/null @@ -1,171 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "kernel/type_checker.h" -#include "kernel/for_each_fn.h" -#include "kernel/error_msgs.h" -#include "library/util.h" -#include "library/constants.h" -#include "library/reducible.h" -#include "library/tactic/tactic.h" -#include "library/tactic/elaborate.h" -#include "library/tactic/expr_to_tactic.h" - -namespace lean { -// Return true iff \c e is of the form (?m l_1 ... l_n), where ?m is a metavariable and l_i's local constants -bool is_meta_placeholder(expr const & e) { - if (!is_meta(e)) - return false; - buffer args; - get_app_args(e, args); - return std::all_of(args.begin(), args.end(), is_local); -} - -tactic exact_tactic(elaborate_fn const & elab, expr const & e, bool enforce_type_during_elaboration, bool allow_metavars, - bool conservative) { - return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) { - proof_state new_s = s; - goals const & gs = new_s.get_goals(); - if (!gs) { - throw_no_goal_if_enabled(s); - return none_proof_state(); - } - expr t = head(gs).get_type(); - bool report_unassigned = !allow_metavars && enforce_type_during_elaboration && s.report_failure(); - optional new_e; - try { - new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t), - report_unassigned, enforce_type_during_elaboration, - conservative); - } catch (exception &) { - if (s.report_failure()) - throw; - else - return none_proof_state(); - } - if (new_e) { - goals const & gs = new_s.get_goals(); - if (gs) { - goal const & g = head(gs); - if (!allow_metavars && has_expr_metavar_relaxed(*new_e)) { - throw_tactic_exception_if_enabled(s, [=](formatter const & fmt) { - format r = format("invalid 'exact' tactic, term still contains metavariables " - "after elaboration"); - r += pp_indent_expr(fmt, *new_e); - return r; - }); - return none_proof_state(); - } - substitution subst = new_s.get_subst(); - assign(subst, g, *new_e); - if (allow_metavars) { - buffer new_goals; - auto tc = mk_type_checker(env); - for_each(*new_e, [&](expr const & m, unsigned) { - if (!has_expr_metavar(m)) - return false; - if (is_meta_placeholder(m)) { - new_goals.push_back(goal(m, tc->infer(m).first)); - return false; - } - return !is_metavar(m) && !is_local(m); - }); - goals new_gs = to_list(new_goals.begin(), new_goals.end(), tail(gs)); - return some(proof_state(new_s, new_gs, subst)); - } else { - return some(proof_state(new_s, tail(gs), subst)); - } - } else { - return some_proof_state(new_s); - } - } - return none_proof_state(); - }); -} - -static tactic assumption_tactic_core(bool conservative) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { - goals const & gs = s.get_goals(); - if (empty(gs)) { - throw_no_goal_if_enabled(s); - return proof_state_seq(); - } - proof_state new_s = s.update_report_failure(false); - optional tac; - goal g = head(gs); - buffer hs; - g.get_hyps(hs); - auto elab = [](goal const &, options const &, expr const & H, - optional const &, substitution const & s, bool) -> elaborate_result { - return elaborate_result(H, s, constraints()); - }; - unsigned i = hs.size(); - while (i > 0) { - --i; - expr const & h = hs[i]; - tactic curr = exact_tactic(elab, h, false, false, conservative); - if (tac) { - tac = orelse(*tac, curr); - } else { - tac = curr; - } - } - if (tac) { - return (*tac)(env, ios, s); - } else { - return proof_state_seq(); - } - }); -} - -tactic eassumption_tactic() { - return assumption_tactic_core(false); -} - -tactic assumption_tactic() { - return assumption_tactic_core(true); -} - -static expr * g_exact_tac_fn = nullptr; -static expr * g_rexact_tac_fn = nullptr; -static expr * g_refine_tac_fn = nullptr; -expr const & get_exact_tac_fn() { return *g_exact_tac_fn; } -expr const & get_rexact_tac_fn() { return *g_rexact_tac_fn; } -expr const & get_refine_tac_fn() { return *g_refine_tac_fn; } -void initialize_exact_tactic() { - name const & exact_tac_name = get_tactic_exact_name(); - name const & rexact_tac_name = get_tactic_rexact_name(); - name const & refine_tac_name = get_tactic_refine_name(); - g_exact_tac_fn = new expr(Const(exact_tac_name)); - g_rexact_tac_fn = new expr(Const(rexact_tac_name)); - g_refine_tac_fn = new expr(Const(refine_tac_name)); - register_tac(exact_tac_name, - [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - check_tactic_expr(app_arg(e), "invalid 'exact' tactic, invalid argument"); - return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), true, false, false); - }); - register_tac(rexact_tac_name, - [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - check_tactic_expr(app_arg(e), "invalid 'rexact' tactic, invalid argument"); - return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), false, false, false); - }); - register_tac(refine_tac_name, - [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - check_tactic_expr(app_arg(e), "invalid 'refine' tactic, invalid argument"); - return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)), true, true, false); - }); - register_simple_tac(get_tactic_eassumption_name(), - []() { return eassumption_tactic(); }); - - register_simple_tac(get_tactic_assumption_name(), - []() { return assumption_tactic(); }); -} -void finalize_exact_tactic() { - delete g_exact_tac_fn; - delete g_rexact_tac_fn; - delete g_refine_tac_fn; -} -} diff --git a/src/library/old_tactic/tactic/exact_tactic.h b/src/library/old_tactic/tactic/exact_tactic.h deleted file mode 100644 index 6c42649637..0000000000 --- a/src/library/old_tactic/tactic/exact_tactic.h +++ /dev/null @@ -1,16 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "library/tactic/tactic.h" - -namespace lean { -expr const & get_exact_tac_fn(); -expr const & get_rexact_tac_fn(); -/** \brief Solve first goal iff it is definitionally equal to type of \c e */ -void initialize_exact_tactic(); -void finalize_exact_tactic(); -} diff --git a/src/library/old_tactic/tactic/exfalso_tactic.cpp b/src/library/old_tactic/tactic/exfalso_tactic.cpp deleted file mode 100644 index 890d7079a2..0000000000 --- a/src/library/old_tactic/tactic/exfalso_tactic.cpp +++ /dev/null @@ -1,43 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "kernel/inductive/inductive.h" -#include "library/constants.h" -#include "library/util.h" -#include "library/reducible.h" -#include "library/tactic/intros_tactic.h" -#include "library/tactic/expr_to_tactic.h" -#include "kernel/kernel_exception.h" - -namespace lean { -tactic exfalso_tactic() { - auto fn = [=](environment const & env, io_state const &, proof_state const & s) { - goals const & gs = s.get_goals(); - if (empty(gs)) { - throw_no_goal_if_enabled(s); - return optional(); - } - goal const & g = head(gs); - expr const & t = g.get_type(); - substitution subst = s.get_subst(); - auto tc = mk_type_checker(env); - expr false_expr = mk_false(env); - expr new_meta = g.mk_meta(mk_fresh_name(), false_expr); - goal new_goal(new_meta, false_expr); - assign(subst, g, mk_false_rec(*tc, new_meta, t)); - return some(proof_state(s, goals(new_goal, tail(gs)), subst)); - }; - return tactic01(fn); -} -void initialize_exfalso_tactic() { - register_tac(name{"tactic", "exfalso"}, - [](old_type_checker &, elaborate_fn const &, expr const &, pos_info_provider const *) { - return exfalso_tactic(); - }); -} -void finalize_exfalso_tactic() { -} -} diff --git a/src/library/old_tactic/tactic/exfalso_tactic.h b/src/library/old_tactic/tactic/exfalso_tactic.h deleted file mode 100644 index 40fe5d6559..0000000000 --- a/src/library/old_tactic/tactic/exfalso_tactic.h +++ /dev/null @@ -1,11 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -namespace lean { -void initialize_exfalso_tactic(); -void finalize_exfalso_tactic(); -} diff --git a/src/library/old_tactic/tactic/injection_tactic.cpp b/src/library/old_tactic/tactic/injection_tactic.cpp deleted file mode 100644 index be61d57bba..0000000000 --- a/src/library/old_tactic/tactic/injection_tactic.cpp +++ /dev/null @@ -1,246 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "util/fresh_name.h" -#include "kernel/instantiate.h" -#include "kernel/abstract.h" -#include "kernel/inductive/inductive.h" -#include "library/constants.h" -#include "library/util.h" -#include "library/old_util.h" -#include "library/reducible.h" -#include "library/tactic/elaborate.h" -#include "library/tactic/expr_to_tactic.h" -#include "library/tactic/apply_tactic.h" -#include "library/tactic/clear_tactic.h" - -namespace lean { -tactic injection_tactic_core(expr const & e, unsigned num, list const & ids, bool report_errors); - -// Return true iff lhs and rhs are of the form (f ...) f is a constructor -bool is_injection_target(old_type_checker & tc, expr lhs, expr rhs) { - environment const & env = tc.env(); - lhs = tc.whnf(lhs).first; - rhs = tc.whnf(rhs).first; - expr A = tc.whnf(tc.infer(lhs).first).first; - expr const & I = get_app_fn(A); - if (!is_constant(I) || !inductive::is_inductive_decl(env, const_name(I))) - return false; - expr lhs_fn = get_app_fn(lhs); - expr rhs_fn = get_app_fn(rhs); - return - is_constant(lhs_fn) && is_constant(rhs_fn) && - const_name(lhs_fn) == const_name(rhs_fn) && - inductive::is_intro_rule(env, const_name(lhs_fn)); -} - -/** \brief Introduce num hypotheses, if _ns is not nil use it to name the hypothesis, - - New hypothesis of the form (a = a) and (a == a) are discarded. - New hypothesis of the form (a == b) where (a b : A), are converted into (a = b). -*/ -tactic intros_num_tactic(unsigned num, list _ns) { - auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) { - if (num == 0) - return proof_state_seq(s); - list ns = _ns; - goals const & gs = s.get_goals(); - if (empty(gs)) - return proof_state_seq(); - goal const & g = head(gs); - auto tc = mk_type_checker(env); - expr t = g.get_type(); - expr m = g.get_meta(); - - auto mk_name = [&](name const & n) { - if (is_nil(ns)) { - return g.get_unused_name(n); - } else { - name r = head(ns); - ns = tail(ns); - return r; - } - }; - - auto keep_hyp = [&]() { - expr H = mk_local(mk_name(binding_name(t)), binding_domain(t)); - t = instantiate(binding_body(t), H); - m = mk_app(m, H); - proof_state new_s(s, cons(goal(m, t), tail(gs))); - return intros_num_tactic(num-1, ns)(env, ios, new_s); - }; - - auto discard_hyp = [&]() { - expr new_meta = g.mk_meta(mk_fresh_name(), binding_body(t)); - goal new_goal(new_meta, binding_body(t)); - substitution new_subst = s.get_subst(); - assign(new_subst, g, mk_lambda(binding_name(t), binding_domain(t), new_meta)); - proof_state new_s(s, cons(new_goal, tail(gs)), new_subst); - return intros_num_tactic(num-1, ns)(env, ios, new_s); - }; - - t = tc->ensure_pi(t).first; - - // if goal depends on hypothesis, we keep it - if (!closed(binding_body(t))) - return keep_hyp(); - - constraint_seq cs; - expr Htype = tc->whnf(binding_domain(t), cs); - - // new unification constraints were generated, so we keep hypothesis - if (cs) - return keep_hyp(); - - expr lhs, rhs; - if (is_eq(Htype, lhs, rhs)) { - // equalities of the form (a = a) are discarded - if (tc->is_def_eq(lhs, rhs, justification(), cs) && !cs) { - return discard_hyp(); - } else if (is_injection_target(*tc, lhs, rhs)) { - // apply injection recursively - name Hname = mk_fresh_name(); - expr H = mk_local(Hname, binding_domain(t)); - t = binding_body(t); - m = mk_app(m, H); - proof_state new_s(s, cons(goal(m, t), tail(gs))); - return then(injection_tactic_core(H, num-1, ns, false), - clear_tactic(Hname))(env, ios, new_s); - } else { - return keep_hyp(); - } - } - - expr A, B; - if (is_standard(env) && is_heq(Htype, A, lhs, B, rhs)) { - if (tc->is_def_eq(A, B, justification(), cs) && !cs) { - // since types A and B are definitionally equal, we convert to homogeneous - expr new_eq = mk_eq(*tc, lhs, rhs); - expr new_type = mk_pi(binding_name(t), new_eq, binding_body(t)); - expr new_meta = g.mk_meta(mk_fresh_name(), new_type); - goal new_goal(new_meta, new_type); - expr H = mk_local(mk_fresh_name(), binding_domain(t)); - levels heq_lvl = const_levels(get_app_fn(Htype)); - expr arg = mk_app(mk_constant(get_eq_of_heq_name(), heq_lvl), A, lhs, rhs, H); - expr V = Fun(H, mk_app(new_meta, arg)); - substitution new_subst = s.get_subst(); - assign(new_subst, g, V); - proof_state new_s(s, cons(new_goal, tail(gs)), new_subst); - return intros_num_tactic(num, ns)(env, ios, new_s); - } else { - return keep_hyp(); - } - } - - // hypothesis is not an equality - return keep_hyp(); - }; - return tactic(fn); -} - -tactic injection_tactic_core(expr const & e, unsigned num, list const & ids, bool report_errors) { - auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) { - goals const & gs = s.get_goals(); - if (!gs) { - throw_no_goal_if_enabled(s); - return proof_state_seq(); - } - expr t = head(gs).get_type(); - constraint_seq cs; - auto tc = mk_type_checker(env); - expr e_type = tc->whnf(tc->infer(e, cs), cs); - expr lhs, rhs; - if (!is_eq(e_type, lhs, rhs)) { - if (report_errors) { - throw_tactic_exception_if_enabled(s, "invalid 'injection' tactic, " - "given argument is not an equality proof"); - return proof_state_seq(); - } - return intros_num_tactic(num, ids)(env, ios, s); - } - lhs = tc->whnf(lhs, cs); - rhs = tc->whnf(rhs, cs); - expr A = tc->whnf(tc->infer(lhs, cs), cs); - buffer I_args; - expr I = get_app_args(A, I_args); - if (!is_constant(I) || !inductive::is_inductive_decl(env, const_name(I))) { - if (report_errors) { - throw_tactic_exception_if_enabled(s, "invalid 'injection' tactic, " - "it is not an equality between inductive values"); - return proof_state_seq(); - } - return intros_num_tactic(num, ids)(env, ios, s); - } - expr lhs_fn = get_app_fn(lhs); - expr rhs_fn = get_app_fn(rhs); - if (!is_constant(lhs_fn) || !is_constant(rhs_fn) || const_name(lhs_fn) != const_name(rhs_fn) || - !inductive::is_intro_rule(env, const_name(lhs_fn))) { - if (report_errors) { - throw_tactic_exception_if_enabled(s, "invalid 'injection' tactic, " - "the given equality is not of the form (f ...) = (f ...) " - "where f is a constructor"); - return proof_state_seq(); - } - return intros_num_tactic(num, ids)(env, ios, s); - } - unsigned num_params = *inductive::get_num_params(env, const_name(I)); - unsigned cnstr_arity = get_arity(env.get(const_name(lhs_fn)).get_type()); - lean_assert(cnstr_arity >= num_params); - unsigned num_new_eqs = cnstr_arity - num_params; - level t_lvl = sort_level(tc->ensure_type(t, cs)); - expr N = mk_constant(name(const_name(I), "no_confusion"), cons(t_lvl, const_levels(I))); - N = mk_app(mk_app(N, I_args), t, lhs, rhs, e); - proof_state new_s(s); - if (is_standard(env)) { - tactic tac = then(take(apply_tactic_core(N, cs), 1), - intros_num_tactic(num + num_new_eqs, ids)); - return tac(env, ios, new_s); - } else { - level n_lvl = mk_meta_univ(mk_fresh_name()); - expr lift_down = mk_app(mk_constant(get_lift_down_name(), {t_lvl, n_lvl}), t); - tactic tac = then(take(apply_tactic_core(lift_down), 1), - then(take(apply_tactic_core(N, cs), 1), - intros_num_tactic(num + num_new_eqs, ids))); - return tac(env, ios, new_s); - } - }; - return tactic(fn); -}; - -tactic injection_tactic(elaborate_fn const & elab, expr const & e, list const & ids) { - auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) { - proof_state new_s = s; - goals const & gs = new_s.get_goals(); - if (!gs) { - throw_no_goal_if_enabled(s); - return proof_state_seq(); - } - expr t = head(gs).get_type(); - bool report_unassigned = true; - bool enforce_type = false; - if (optional new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, none_expr(), - report_unassigned, enforce_type)) { - return injection_tactic_core(*new_e, 0, ids, true)(env, ios, new_s); - } else { - return proof_state_seq(); - } - }; - return tactic(fn); -} - -void initialize_injection_tactic() { - register_tac(name{"tactic", "injection"}, - [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - check_tactic_expr(app_arg(app_fn(e)), "invalid 'injection' tactic, invalid argument"); - buffer ids; - get_tactic_id_list_elements(app_arg(e), ids, "invalid 'injection' tactic, list of identifiers expected"); - return take(injection_tactic(fn, get_tactic_expr_expr(app_arg(app_fn(e))), to_list(ids)), 1); - }); -} - -void finalize_injection_tactic() { -} -} diff --git a/src/library/old_tactic/tactic/injection_tactic.h b/src/library/old_tactic/tactic/injection_tactic.h deleted file mode 100644 index 9b9d72fdb4..0000000000 --- a/src/library/old_tactic/tactic/injection_tactic.h +++ /dev/null @@ -1,11 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -namespace lean { -void initialize_injection_tactic(); -void finalize_injection_tactic(); -} diff --git a/src/library/old_tactic/tactic/intros_tactic.cpp b/src/library/old_tactic/tactic/intros_tactic.cpp deleted file mode 100644 index 22bf2abdcd..0000000000 --- a/src/library/old_tactic/tactic/intros_tactic.cpp +++ /dev/null @@ -1,92 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "util/fresh_name.h" -#include "kernel/instantiate.h" -#include "library/constants.h" -#include "library/reducible.h" -#include "library/tactic/intros_tactic.h" -#include "library/tactic/expr_to_tactic.h" - -namespace lean { -static tactic intro_intros_tactic(list _ns, bool is_intros) { - auto fn = [=](environment const & env, io_state const &, proof_state const & s) { - list ns = _ns; - goals const & gs = s.get_goals(); - if (empty(gs)) { - throw_no_goal_if_enabled(s); - return optional(); - } - goal const & g = head(gs); - auto tc = mk_type_checker(env); - expr t = g.get_type(); - expr m = g.get_meta(); - bool gen_names = is_intros && empty(ns); - bool gen_one_name = !is_intros && empty(ns); - bool first = true; - try { - while (true) { - if (!gen_names && (!gen_one_name || !first) && is_nil(ns)) - break; - if (!is_pi(t)) { - if (!is_nil(ns)) { - t = tc->ensure_pi(t).first; - } else { - expr new_t = tc->whnf(t).first; - if (!is_pi(new_t)) - break; - t = new_t; - } - } - name new_name; - if (!is_nil(ns)) { - new_name = head(ns); - if (new_name == "_") - new_name = get_unused_name(binding_name(t), m); - ns = tail(ns); - } else { - new_name = get_unused_name(binding_name(t), m); - } - expr new_local = mk_local(mk_fresh_name(), new_name, binding_domain(t), binding_info(t)); - t = instantiate(binding_body(t), new_local); - m = mk_app(m, new_local); - first = false; - } - goal new_g(m, t); - return some(proof_state(s, goals(new_g, tail(gs)))); - } catch (exception &) { - return optional(); - } - }; - return tactic01(fn); -} - -tactic intro_tactic(list const & ns) { - return intro_intros_tactic(ns, false); -} - -tactic intros_tactic(list const & ns) { - return intro_intros_tactic(ns, true); -} - -void initialize_intros_tactic() { - register_tac(get_tactic_intro_name(), - [](old_type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - buffer ns; - get_tactic_id_list_elements(app_arg(e), ns, "invalid 'intro' tactic, arguments must be identifiers"); - return intro_tactic(to_list(ns.begin(), ns.end())); - }); - register_tac(get_tactic_intros_name(), - [](old_type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - buffer ns; - get_tactic_id_list_elements(app_arg(e), ns, "invalid 'intros' tactic, arguments must be identifiers"); - return intros_tactic(to_list(ns.begin(), ns.end())); - }); -} - -void finalize_intros_tactic() { -} -} diff --git a/src/library/old_tactic/tactic/intros_tactic.h b/src/library/old_tactic/tactic/intros_tactic.h deleted file mode 100644 index a5d34f578e..0000000000 --- a/src/library/old_tactic/tactic/intros_tactic.h +++ /dev/null @@ -1,13 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "library/tactic/tactic.h" -namespace lean { -tactic intros_tactic(list const & ns); -void initialize_intros_tactic(); -void finalize_intros_tactic(); -} diff --git a/src/library/old_tactic/tactic/norm_num_tactic.cpp b/src/library/old_tactic/tactic/norm_num_tactic.cpp deleted file mode 100644 index 36c5ce4b33..0000000000 --- a/src/library/old_tactic/tactic/norm_num_tactic.cpp +++ /dev/null @@ -1,69 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Robert Y. Lewis -*/ -#include "kernel/type_checker.h" -#include "library/util.h" -#include "library/reducible.h" -#include "library/normalize.h" -#include "library/norm_num.h" -#include "library/old_tmp_type_context.h" -#include "library/tactic/expr_to_tactic.h" - -namespace lean { -tactic norm_num_tactic() { - return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) { - goals const & gs = s.get_goals(); - if (empty(gs)) { - throw_no_goal_if_enabled(s); - return none_proof_state(); - } - goal const & g = head(gs); - expr const & c = g.get_type(); - expr lhs, rhs; - if (!is_eq(c, lhs, rhs)) { - throw_tactic_exception_if_enabled(s, "norm_num tactic failed, conclusion is not an equality"); - return none_proof_state(); - } - old_type_checker_ptr rtc = mk_type_checker(env, UnfoldReducible); - lhs = normalize(*rtc, lhs); - rhs = normalize(*rtc, rhs); - buffer hyps; - g.get_hyps(hyps); - try { - old_tmp_type_context ctx(env, ios.get_options()); - ctx.set_local_instances(to_list(hyps)); - pair p = mk_norm_num(ctx, lhs); - expr new_lhs = p.first; - expr new_lhs_pr = p.second; - pair p2 = mk_norm_num(ctx, rhs); - expr new_rhs = p2.first; - expr new_rhs_pr = p2.second; - mpq v_lhs = mpq_of_expr(ctx, new_lhs), v_rhs = mpq_of_expr(ctx, new_rhs); - if (v_lhs == v_rhs) { - old_type_checker tc(env); - expr g_prf = mk_trans(tc, new_lhs_pr, mk_symm(tc, new_rhs_pr)); - substitution new_subst = s.get_subst(); - assign(new_subst, g, g_prf); - return some_proof_state(proof_state(s, tail(gs), new_subst)); - } else { - throw_tactic_exception_if_enabled(s, "norm_num tactic failed, lhs doesn't match rhs"); - return none_proof_state(); - } - } catch (exception & ex) { - throw_tactic_exception_if_enabled(s, ex.what()); - return none_proof_state(); - } - }); -} - -void initialize_norm_num_tactic() { - register_tac(name{"tactic", "norm_num"}, - [](old_type_checker &, elaborate_fn const &, expr const &, pos_info_provider const *) { - return norm_num_tactic(); - }); -} -void finalize_norm_num_tactic() { -} -} diff --git a/src/library/old_tactic/tactic/norm_num_tactic.h b/src/library/old_tactic/tactic/norm_num_tactic.h deleted file mode 100644 index 45871b6302..0000000000 --- a/src/library/old_tactic/tactic/norm_num_tactic.h +++ /dev/null @@ -1,12 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Rob Lewis -*/ -#pragma once - -namespace lean { -void initialize_norm_num_tactic(); -void finalize_norm_num_tactic(); -} diff --git a/src/library/old_tactic/tactic/note_tactic.cpp b/src/library/old_tactic/tactic/note_tactic.cpp deleted file mode 100644 index dea5bfb253..0000000000 --- a/src/library/old_tactic/tactic/note_tactic.cpp +++ /dev/null @@ -1,63 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "util/fresh_name.h" -#include "kernel/abstract.h" -#include "library/constants.h" -#include "library/reducible.h" -#include "library/unifier.h" -#include "library/tactic/tactic.h" -#include "library/tactic/elaborate.h" -#include "library/tactic/expr_to_tactic.h" - -namespace lean { -expr mk_note_tactic_expr(name const &id, expr const &e) { - return mk_app(mk_constant(get_tactic_note_tac_name()), - mk_constant(id), e); -} - -tactic note_tactic(elaborate_fn const & elab, name const & id, expr const & e) { - return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) { - proof_state new_s = s; - goals const & gs = new_s.get_goals(); - if (!gs) { - throw_no_goal_if_enabled(s); - return none_proof_state(); - } - goal const & g = head(gs); - bool report_unassigned = true; - elaborate_result esc = elab(g, ios.get_options(), e, none_expr(), new_s.get_subst(), report_unassigned); - expr new_e; substitution new_subst; constraints cs; - std::tie(new_e, new_subst, cs) = esc; - if (cs) - throw_tactic_exception_if_enabled(s, "invalid 'note' tactic, fail to resolve generated constraints"); - auto tc = mk_type_checker(env); - expr new_e_type = tc->infer(new_e).first; - expr new_local = mk_local(mk_fresh_name(), id, new_e_type, binder_info()); - buffer hyps; - g.get_hyps(hyps); - hyps.push_back(new_local); - expr new_mvar = mk_metavar(mk_fresh_name(), Pi(hyps, g.get_type())); - hyps.pop_back(); - expr new_meta_core = mk_app(new_mvar, hyps); - expr new_meta = mk_app(new_meta_core, new_local); - goal new_goal(new_meta, g.get_type()); - assign(new_subst, g, mk_app(new_meta_core, new_e)); - return some_proof_state(proof_state(s, cons(new_goal, tail(gs)), new_subst)); - }); -} - -void initialize_note_tactic() { - register_tac(get_tactic_note_tac_name(), - [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - name id = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'note' tactic, argument must be an identifier"); - check_tactic_expr(app_arg(e), "invalid 'note' tactic, argument must be an expression"); - return note_tactic(fn, id, get_tactic_expr_expr(app_arg(e))); - }); -} -void finalize_note_tactic() { -} -} diff --git a/src/library/old_tactic/tactic/note_tactic.h b/src/library/old_tactic/tactic/note_tactic.h deleted file mode 100644 index 2bc8237fa4..0000000000 --- a/src/library/old_tactic/tactic/note_tactic.h +++ /dev/null @@ -1,14 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "kernel/expr.h" - -namespace lean { -expr mk_note_tactic_expr(name const &id, expr const &e); -void initialize_note_tactic(); -void finalize_note_tactic(); -} diff --git a/src/library/old_tactic/tactic/relation_tactics.cpp b/src/library/old_tactic/tactic/relation_tactics.cpp deleted file mode 100644 index a07fee6151..0000000000 --- a/src/library/old_tactic/tactic/relation_tactics.cpp +++ /dev/null @@ -1,99 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "kernel/instantiate.h" -#include "library/relation_manager.h" -#include "library/explicit.h" -#include "library/placeholder.h" -#include "library/tactic/apply_tactic.h" -#include "library/tactic/expr_to_tactic.h" - -namespace lean { -// Remark: if no_meta == true, then return none if goal contains metavariables -static optional get_goal_op(proof_state const & s, bool no_meta = false) { - goals const & gs = s.get_goals(); - if (empty(gs)) { - throw_no_goal_if_enabled(s); - return optional(); - } - goal const & g = head(gs); - if (no_meta && has_metavar(g.get_type())) - return optional(); - expr op = get_app_fn(head_beta_reduce(g.get_type())); - if (is_constant(op)) - return optional(const_name(op)); - else - return optional(); -} - -tactic refl_tactic(elaborate_fn const & elab, bool no_meta = false) { - auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) { - auto op = get_goal_op(s, no_meta); - if (!op) - return proof_state_seq(); - if (auto refl = get_refl_info(env, *op)) { - return apply_tactic(elab, mk_constant(*refl))(env, ios, s); - } else { - throw_tactic_exception_if_enabled(s, sstream() << "invalid 'reflexivity' tactic, operator '" << *op << "' is not marked are reflexive"); - return proof_state_seq(); - } - }; - return tactic(fn); -} - -tactic symm_tactic(elaborate_fn const & elab) { - auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) { - auto op = get_goal_op(s); - if (!op) - return proof_state_seq(); - if (auto symm = get_symm_info(env, *op)) { - return apply_tactic(elab, mk_constant(*symm))(env, ios, s); - } else { - throw_tactic_exception_if_enabled(s, sstream() << "invalid 'symmetry' tactic, operator '" << *op << "' is not marked are symmetric"); - return proof_state_seq(); - } - }; - return tactic(fn); -} - -tactic trans_tactic(elaborate_fn const & elab, expr const & e) { - auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) { - auto op = get_goal_op(s); - if (!op) - return proof_state_seq(); - if (auto info = get_trans_extra_info(env, *op, *op)) { - expr pr = mk_explicit(mk_constant(info->m_name)); - unsigned nargs = info->m_num_args; - lean_assert(nargs >= 5); - for (unsigned i = 0; i < nargs - 4; i++) - pr = mk_app(pr, mk_expr_placeholder()); - pr = mk_app(pr, e); - return apply_tactic(elab, pr)(env, ios, s); - } else { - throw_tactic_exception_if_enabled(s, sstream() << "invalid 'transitivity' tactic, operator '" << *op << "' is not marked are transitive"); - return proof_state_seq(); - } - }; - return tactic(fn); -} - -void initialize_relation_tactics() { - register_tac(name{"tactic", "reflexivity"}, - [](old_type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) { - return refl_tactic(fn); - }); - register_tac(name{"tactic", "symmetry"}, - [](old_type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) { - return symm_tactic(fn); - }); - register_tac(name{"tactic", "transitivity"}, - [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - check_tactic_expr(app_arg(e), "invalid 'transitivity' tactic, invalid argument"); - return trans_tactic(fn, get_tactic_expr_expr(app_arg(e))); - }); -} -void finalize_relation_tactics() {} -} diff --git a/src/library/old_tactic/tactic/relation_tactics.h b/src/library/old_tactic/tactic/relation_tactics.h deleted file mode 100644 index d565dcd359..0000000000 --- a/src/library/old_tactic/tactic/relation_tactics.h +++ /dev/null @@ -1,12 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -namespace lean { -tactic refl_tactic(elaborate_fn const & elab, bool no_meta = false); -void initialize_relation_tactics(); -void finalize_relation_tactics(); -} diff --git a/src/library/old_tactic/tactic/rename_tactic.cpp b/src/library/old_tactic/tactic/rename_tactic.cpp deleted file mode 100644 index 279370d1f5..0000000000 --- a/src/library/old_tactic/tactic/rename_tactic.cpp +++ /dev/null @@ -1,62 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "library/constants.h" -#include "kernel/replace_fn.h" -#include "library/tactic/tactic.h" -#include "library/tactic/expr_to_tactic.h" - -namespace lean { -tactic rename_tactic(name const & from, name const & to) { - return tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { - goals const & gs = s.get_goals(); - if (empty(gs)) { - throw_no_goal_if_enabled(s); - return none_proof_state(); - } - goal const & g = head(gs); - goals const & rest_gs = tail(gs); - buffer locals; - get_app_args(g.get_meta(), locals); - unsigned i = locals.size(); - optional from_local; - while (i > 0) { - --i; - expr const & local = locals[i]; - if (local_pp_name(local) == from) { - from_local = local; - break; - } - } - if (!from_local) - return none_proof_state(); - expr to_local = mk_local(mlocal_name(*from_local), to, mlocal_type(*from_local), local_info(*from_local)); - auto fn = [&](expr const & e) { - if (is_local(e) && mlocal_name(e) == mlocal_name(*from_local)) - return some_expr(to_local); - else - return none_expr(); - }; - goal new_g(replace(g.get_meta(), fn), replace(g.get_type(), fn)); - return some(proof_state(s, goals(new_g, rest_gs))); - }); -} - -static name const & get_rename_arg(expr const & e) { - return tactic_expr_to_id(e, "invalid 'rename' tactic, arguments must be identifiers"); -} - -void initialize_rename_tactic() { - auto fn = [](old_type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - return rename_tactic(get_rename_arg(app_arg(app_fn(e))), - get_rename_arg(app_arg(e))); - }; - register_tac(get_tactic_rename_name(), fn); -} - -void finalize_rename_tactic() { -} -} diff --git a/src/library/old_tactic/tactic/rename_tactic.h b/src/library/old_tactic/tactic/rename_tactic.h deleted file mode 100644 index 3193e65634..0000000000 --- a/src/library/old_tactic/tactic/rename_tactic.h +++ /dev/null @@ -1,14 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "library/tactic/tactic.h" - -namespace lean { -tactic rename_tactic(name const & from, name const & to); -void initialize_rename_tactic(); -void finalize_rename_tactic(); -} diff --git a/src/library/old_tactic/tactic/replace_tactic.cpp b/src/library/old_tactic/tactic/replace_tactic.cpp deleted file mode 100644 index 45cfdec031..0000000000 --- a/src/library/old_tactic/tactic/replace_tactic.cpp +++ /dev/null @@ -1,124 +0,0 @@ - /* -Copyright (c) 2015 Robert Y. Lewis. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Robert Y. Lewis -*/ -#include "util/fresh_name.h" -#include "util/lazy_list_fn.h" -#include "kernel/error_msgs.h" -#include "kernel/instantiate.h" -#include "library/constants.h" -#include "library/reducible.h" -#include "library/unifier.h" -#include "library/tactic/replace_tactic.h" -#include "library/tactic/expr_to_tactic.h" - -namespace lean { - - -static expr * g_replace_tac = nullptr; - -expr substitute_at_occurrences(environment const & env, expr const & t, expr const & nexpr, expr const & oexpr, occurrence const & occ) { - bool has_dep_elim = inductive::has_dep_elim(env, get_eq_name()); - unsigned vidx = has_dep_elim ? 1 : 0; - optional nt = replace_occurrences(t, oexpr, occ, vidx); - if (!nt) { - return t; - } - expr t2 = instantiate(*nt, vidx, nexpr); - return t2; -} - -tactic mk_replace_tactic(elaborate_fn const & elab, expr const & e) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { - buffer e_args; - get_app_args(e, e_args); - expr t1, t2; // replace t2 with t1 - location loc; - if (e_args.size() == 3) { - t1 = get_tactic_expr_expr(e_args[1]); - t2 = get_tactic_expr_expr(e_args[0]); - if (is_location_expr(get_tactic_expr_expr(e_args[2]))) { - loc = get_location_expr_location(get_tactic_expr_expr(e_args[2])); - } else { - loc = location(); - } - } else { - throw_tactic_exception_if_enabled(s, "malformed arguments to replace"); - return proof_state_seq(); - } - proof_state new_s = s; - goals const & gs = new_s.get_goals(); - if (!gs) { - throw_no_goal_if_enabled(s); - return proof_state_seq(); - } - expr t = head(gs).get_type(); - bool report_unassigned = true; - auto new_t1 = elaborate_with_respect_to(env, ios, elab, new_s, t1, none_expr(), report_unassigned); - auto new_t2 = elaborate_with_respect_to(env, ios, elab, new_s, t2, none_expr(), report_unassigned); - if (new_t1 && new_t2) { - goals const & gs = new_s.get_goals(); - goal const & g = head(gs); - substitution subst = new_s.get_subst(); - auto tc = mk_type_checker(env); - constraint_seq cs; - if (tc->is_def_eq(*new_t1, *new_t2, justification(), cs)) { - auto nocc = loc.includes_goal(); - expr new_goal; - if (nocc) { - new_goal = substitute_at_occurrences(env, g.get_type(), *new_t1, *new_t2, *nocc); - } else { - throw_tactic_exception_if_enabled(s, "replacing in hypotheses not implemented"); - return proof_state_seq(); - } - if (cs) { - unifier_config cfg(ios.get_options()); - buffer cs_buf; - cs.linearize(cs_buf); - to_buffer(new_s.get_postponed(), cs_buf); - unify_result_seq rseq = unify(env, cs_buf.size(), cs_buf.data(), subst, cfg); - return map2(rseq, [=](pair const & p) -> proof_state { - substitution const & subst = p.first; - constraints const & postponed = p.second; - substitution new_subst = subst; - expr M = g.mk_meta(mk_fresh_name(), new_goal); - goal new_g(M, new_goal); - assign(new_subst, g, M); - return proof_state(new_s, cons(new_g, tail(gs)), new_subst, postponed); - }); - } - expr M = g.mk_meta(mk_fresh_name(), new_goal); - goal new_g(M, new_goal); - assign(subst, g, M); - return proof_state_seq(proof_state(new_s, cons(new_g, tail(gs)), subst)); - } else { - throw_tactic_exception_if_enabled(new_s, [=](formatter const & fmt) { - format r = format("invalid 'replace' tactic, the new type"); - r += pp_indent_expr(fmt, *new_t1); - r += compose(line(), format("does not match the old type")); - r += pp_indent_expr(fmt, *new_t2); - return r; - }); - return proof_state_seq(); - } - } - return proof_state_seq(); - }); -} - -void initialize_replace_tactic() { - name replace_tac_name{"tactic", "replace"}; - g_replace_tac = new expr(Const(replace_tac_name)); - register_tac(replace_tac_name, - [](old_type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) { - return mk_replace_tactic(elab, e); - }); -} - -void finalize_replace_tactic() { - delete g_replace_tac; -} - -} diff --git a/src/library/old_tactic/tactic/replace_tactic.h b/src/library/old_tactic/tactic/replace_tactic.h deleted file mode 100644 index a0cc17a85d..0000000000 --- a/src/library/old_tactic/tactic/replace_tactic.h +++ /dev/null @@ -1,15 +0,0 @@ - /* -Copyright (c) 2015 Robert Y. Lewis. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Robert Y. Lewis -*/ -#pragma once -#include "library/tactic/tactic.h" -#include "library/tactic/location.h" - -namespace lean { - -void initialize_replace_tactic(); -void finalize_replace_tactic(); -} diff --git a/src/library/old_tactic/tactic/revert_tactic.cpp b/src/library/old_tactic/tactic/revert_tactic.cpp deleted file mode 100644 index 741e450528..0000000000 --- a/src/library/old_tactic/tactic/revert_tactic.cpp +++ /dev/null @@ -1,63 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "util/fresh_name.h" -#include "kernel/abstract.h" -#include "library/constants.h" -#include "library/locals.h" -#include "library/tactic/tactic.h" -#include "library/tactic/expr_to_tactic.h" - -namespace lean { -tactic revert_tactic(name const & n) { - auto fn = [=](environment const &, io_state const &, proof_state const & s) -> optional { - goals const & gs = s.get_goals(); - if (empty(gs)) { - throw_no_goal_if_enabled(s); - return none_proof_state(); - } - goal g = head(gs); - goals tail_gs = tail(gs); - if (auto p = g.find_hyp(n)) { - expr const & h = p->first; - unsigned i = p->second; - buffer hyps; - g.get_hyps(hyps); - hyps.erase(hyps.size() - i - 1); - if (optional other_h = depends_on(i, hyps.end() - i, h)) { - throw_tactic_exception_if_enabled(s, sstream() << "invalid 'revert' tactic, hypothesis '" << local_pp_name(*other_h) - << "' depends on '" << local_pp_name(h) << "'"); - return none_proof_state(); // other hypotheses depend on h - } - expr new_type = Pi(h, g.get_type()); - expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(hyps, new_type)), hyps); - goal new_g(new_meta, new_type); - substitution new_subst = s.get_subst(); - assign(new_subst, g, mk_app(new_meta, h)); - proof_state new_s(s, goals(new_g, tail_gs), new_subst); - return some_proof_state(new_s); - } else { - throw_tactic_exception_if_enabled(s, sstream() << "invalid 'revert' tactic, unknown hypothesis '" << n << "'"); - return none_proof_state(); - } - }; - return tactic01(fn); -} - -void initialize_revert_tactic() { - auto fn = [](old_type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - buffer ns; - get_tactic_id_list_elements(app_arg(e), ns, "invalid 'reverts' tactic, list of identifiers expected"); - tactic r = revert_tactic(ns[0]); - for (unsigned i = 1; i < ns.size(); i++) - r = then(revert_tactic(ns[i]), r); - return r; - }; - register_tac(get_tactic_revert_name(), fn); - register_tac(get_tactic_reverts_name(), fn); -} -void finalize_revert_tactic() {} -} diff --git a/src/library/old_tactic/tactic/revert_tactic.h b/src/library/old_tactic/tactic/revert_tactic.h deleted file mode 100644 index ae3748e141..0000000000 --- a/src/library/old_tactic/tactic/revert_tactic.h +++ /dev/null @@ -1,14 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "library/tactic/tactic.h" - -namespace lean { -tactic revert_tactic(name const & n); -void initialize_revert_tactic(); -void finalize_revert_tactic(); -} diff --git a/src/library/old_tactic/tactic/subst_tactic.cpp b/src/library/old_tactic/tactic/subst_tactic.cpp deleted file mode 100644 index 6299a74e0b..0000000000 --- a/src/library/old_tactic/tactic/subst_tactic.cpp +++ /dev/null @@ -1,256 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "util/fresh_name.h" -#include "kernel/abstract.h" -#include "kernel/instantiate.h" -#include "kernel/inductive/inductive.h" -#include "kernel/kernel_exception.h" -#include "library/constants.h" -#include "library/reducible.h" -#include "library/util.h" -#include "library/locals.h" -#include "library/tactic/expr_to_tactic.h" -#include "library/tactic/relation_tactics.h" -#include "library/tactic/proof_state.h" - -namespace lean { -static void split_deps(buffer const & hyps, expr const & x, expr const & h, - buffer & non_deps, buffer & deps, bool & depends_on_h) { - for (expr const & hyp : hyps) { - if (hyp == h || hyp == x) { - // we clear h and x - } else if (depends_on(hyp, h)) { - deps.push_back(hyp); - depends_on_h = true; - } else if (depends_on(hyp, x) || depends_on_any(hyp, deps)) { - deps.push_back(hyp); - } else { - non_deps.push_back(hyp); - } - } -} - -optional subst(environment const & env, name const & h_name, bool symm, proof_state const & s) { - goals const & gs = s.get_goals(); - if (empty(gs)) - return none_proof_state(); - goal g = head(gs); - auto opt_h = g.find_hyp_from_internal_name(h_name); - if (!opt_h) - return none_proof_state(); - expr const & h = opt_h->first; - expr lhs, rhs; - if (!is_eq(mlocal_type(h), lhs, rhs)) - return none_proof_state(); - auto tc = mk_type_checker(env); - if (symm) - std::swap(lhs, rhs); - if (!is_local(lhs)) - return none_proof_state(); - if (depends_on(rhs, lhs)) { - throw_tactic_exception_if_enabled(s, sstream() << "invalid 'subst' tactic, '" << lhs - << "' occurs in the other side of the equation"); - return none_proof_state(); - } - buffer hyps, deps, non_deps; - g.get_hyps(hyps); - bool depends_on_h = depends_on(g.get_type(), h); - split_deps(hyps, lhs, h, non_deps, deps, depends_on_h); - // revert dependencies - expr type = Pi(deps, g.get_type()); - // substitute - bool has_dep_elim = inductive::has_dep_elim(env, get_eq_name()); - bool use_dep_elim = has_dep_elim; - if (depends_on_h) - use_dep_elim = true; - expr motive, new_type; - new_type = instantiate(abstract_local(type, mlocal_name(lhs)), rhs); - if (use_dep_elim) { - new_type = instantiate(abstract_local(new_type, mlocal_name(h)), mk_refl(*tc, rhs)); - if (symm) { - motive = Fun(lhs, Fun(h, type)); - } else { - expr Heq = mk_local(mk_fresh_name(), local_pp_name(h), mk_eq(*tc, rhs, lhs), binder_info()); - motive = Fun(lhs, Fun(Heq, type)); - } - } else { - motive = Fun(lhs, type); - } - buffer new_hyps; - buffer intros_hyps; - new_hyps.append(non_deps); - - // reintroduce dependencies - expr new_goal_type = new_type; - for (expr const & d : deps) { - if (!is_pi(new_goal_type)) - return none_proof_state(); - expr new_h = mk_local(mk_fresh_name(), local_pp_name(d), binding_domain(new_goal_type), binder_info()); - new_hyps.push_back(new_h); - intros_hyps.push_back(new_h); - new_goal_type = instantiate(binding_body(new_goal_type), new_h); - } - - // create new goal - expr new_metavar = mk_metavar(mk_fresh_name(), Pi(new_hyps, new_goal_type)); - expr new_meta_core = mk_app(new_metavar, non_deps); - expr new_meta = mk_app(new_meta_core, intros_hyps); - goal new_g(new_meta, new_goal_type); - // create eqrec term - substitution new_subst = s.get_subst(); - expr major = symm ? h : mk_symm(*tc, h); - expr minor = new_meta_core; - expr A = tc->infer(lhs).first; - level l1 = sort_level(tc->ensure_type(new_type).first); - level l2 = sort_level(tc->ensure_type(A).first); - name eq_rec_name; - if (!has_dep_elim && use_dep_elim) - eq_rec_name = get_eq_drec_name(); - else - eq_rec_name = get_eq_rec_name(); - expr eqrec = mk_app({mk_constant(eq_rec_name, {l1, l2}), A, rhs, motive, minor, lhs, major}); - if (use_dep_elim) { - try { - check_term(env, g.abstract(eqrec)); - } catch (kernel_exception & ex) { - if (!s.report_failure()) - return none_proof_state(); - std::shared_ptr saved_ex(static_cast(ex.clone())); - throw tactic_exception("rewrite step failed", none_expr(), s, - [=](formatter const & fmt) { - format r; - r += format("invalid 'subst' tactic, " - "produced type incorrect term, details: "); - r += saved_ex->pp(fmt); - r += line(); - return r; - }); - } - } - expr new_val = mk_app(eqrec, deps); - assign(new_subst, g, new_val); - lean_assert(new_subst.is_assigned(g.get_mvar())); - proof_state new_s(s, goals(new_g, tail(gs)), new_subst); - return some_proof_state(new_s); -} - -tactic mk_subst_tactic_core(name const & h_name, bool symm) { - auto fn = [=](environment const & env, io_state const &, proof_state const & s) { - return subst(env, h_name, symm, s); - }; - return tactic01(fn); -} - -tactic mk_subst_tactic(list const & ids) { - auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) { - if (!ids) - return proof_state_seq(s); - goals const & gs = s.get_goals(); - if (empty(gs)) - return proof_state_seq(); - goal const & g = head(gs); - name const & id = head(ids); - - auto apply_rewrite = [&](expr const & H, bool symm) { - tactic tac = then(mk_subst_tactic_core(mlocal_name(H), symm), mk_subst_tactic(tail(ids))); - return tac(env, ios, s); - }; - - optional> p = g.find_hyp(id); - if (!p) { - throw_tactic_exception_if_enabled(s, sstream() << "invalid 'subst' tactic, there is no hypothesis named '" - << id << "'"); - return proof_state_seq(); - } - expr const & H = p->first; - expr lhs, rhs; - if (is_eq(mlocal_type(H), lhs, rhs)) { - if (is_local(rhs)) { - return apply_rewrite(H, true); - } else if (is_local(lhs)) { - return apply_rewrite(H, false); - } else { - throw_tactic_exception_if_enabled(s, sstream() << "invalid 'subst' tactic, hypothesis '" - << id << "' is not of the form (x = t) or (t = x)"); - return proof_state_seq(); - } - } else if (is_local(H)) { - expr const & x = H; - buffer hyps; - g.get_hyps(hyps); - for (expr const & H : hyps) { - expr lhs, rhs; - if (is_eq(mlocal_type(H), lhs, rhs)) { - if (is_local(lhs) && mlocal_name(lhs) == mlocal_name(x) && !depends_on(rhs, lhs)) { - return apply_rewrite(H, false); - } else if (is_local(rhs) && mlocal_name(rhs) == mlocal_name(x) && !depends_on(lhs, rhs)) { - return apply_rewrite(H, true); - } - } - } - } - throw_tactic_exception_if_enabled(s, sstream() << "invalid 'subst' tactic, hypothesis '" - << id << "' is not a variable nor an equation of the form (x = t) or (t = x)"); - return proof_state_seq(); - }; - return tactic(fn); -} - -tactic mk_subst_vars_tactic(bool first, unsigned start) { - auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) { - goals const & gs = s.get_goals(); - if (empty(gs)) { - if (first) - return proof_state_seq(); - else - return proof_state_seq(s); - } - goal const & g = head(gs); - - auto apply_rewrite = [&](expr const & H, bool symm, unsigned i) { - tactic tac = orelse(then(mk_subst_tactic_core(mlocal_name(H), symm), mk_subst_vars_tactic(false, 0)), - mk_subst_vars_tactic(false, i+1)); - return tac(env, ios, s); - }; - - buffer hyps; - g.get_hyps(hyps); - for (unsigned i = start; i < hyps.size(); i++) { - expr const & h = hyps[i]; - expr lhs, rhs; - if (is_eq(mlocal_type(h), lhs, rhs)) { - if (is_local(rhs)) { - return apply_rewrite(h, true, i); - } else if (is_local(lhs)) { - return apply_rewrite(h, false, i); - } - } - } - if (first) - return proof_state_seq(); - else - return proof_state_seq(s); - }; - return tactic(fn); -} - -void initialize_subst_tactic() { - register_tac(name{"tactic", "subst"}, - [](old_type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) { - buffer ns; - get_tactic_id_list_elements(app_arg(e), ns, "invalid 'subst' tactic, list of identifiers expected"); - return then(mk_subst_tactic(to_list(ns)), try_tactic(refl_tactic(elab))); - }); - register_tac(name{"tactic", "substvars"}, - [](old_type_checker &, elaborate_fn const & elab, expr const &, pos_info_provider const *) { - return then(mk_subst_vars_tactic(true, 0), try_tactic(refl_tactic(elab))); - }); -} -void finalize_subst_tactic() { -} -} diff --git a/src/library/old_tactic/tactic/subst_tactic.h b/src/library/old_tactic/tactic/subst_tactic.h deleted file mode 100644 index bca1400bd5..0000000000 --- a/src/library/old_tactic/tactic/subst_tactic.h +++ /dev/null @@ -1,13 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "library/tactic/proof_state.h" -namespace lean { -optional subst(environment const & env, name const & h_name, bool symm, proof_state const & s); -void initialize_subst_tactic(); -void finalize_subst_tactic(); -} diff --git a/src/library/old_tactic/tactic/tactic.cpp b/src/library/old_tactic/tactic/tactic.cpp deleted file mode 100644 index 064c28f4e9..0000000000 --- a/src/library/old_tactic/tactic/tactic.cpp +++ /dev/null @@ -1,279 +0,0 @@ -/* -Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include -#include "util/sstream.h" -#include "util/interrupt.h" -#include "util/lazy_list_fn.h" -#include "util/list_fn.h" -#include "kernel/instantiate.h" -#include "kernel/type_checker.h" -#include "kernel/for_each_fn.h" -#include "kernel/replace_fn.h" -#include "library/normalize.h" -#include "library/util.h" -#include "library/old_util.h" -#include "library/tactic/tactic.h" -#include "library/io_state_stream.h" - -namespace lean { -/** \brief Throw an exception is \c v contains local constants, \c e is only used for position information. */ -void check_has_no_local(expr const & v, expr const & e, char const * tac_name) { - if (has_local(v)) { - for_each(v, [&](expr const & l, unsigned) { - if (is_local(l)) - throw tactic_exception(e, sstream() << "tactic '" << tac_name << "' contains reference to local '" << local_pp_name(l) - << "' which is not visible by this tactic " - << "possible causes: it was not marked as [visible]; it was destructued"); - return has_local(l); - }); - } -} - -tactic_exception::tactic_exception(char const * msg, optional const & m, pp_fn const & fn): - generic_exception(msg, m, fn) {} -tactic_exception::tactic_exception(char const * msg, optional const & m, proof_state const & ps, pp_fn const & fn): - generic_exception(msg, m, fn), m_ps(ps) {} -tactic_exception::tactic_exception(expr const & e, std::string const & msg): - generic_exception(msg.c_str(), some_expr(e), [=](formatter const &) { return format(msg); }) {} -tactic_exception::tactic_exception(std::string const & msg): - generic_exception(msg.c_str(), none_expr(), [=](formatter const &) { return format(msg); }) {} -tactic_exception::tactic_exception(char const * msg):tactic_exception(std::string(msg)) {} -tactic_exception::tactic_exception(sstream const & strm):tactic_exception(strm.str()) {} -tactic_exception::tactic_exception(expr const & e, char const * msg):tactic_exception(e, std::string(msg)) {} -tactic_exception::tactic_exception(expr const & e, sstream const & strm):tactic_exception(e, strm.str()) {} -tactic_exception::tactic_exception(expr const & e, pp_fn const & fn):generic_exception("tactic exception", some_expr(e), fn) {} -tactic_exception::tactic_exception(pp_fn const & fn):generic_exception("tactic exception", none_expr(), fn) {} - -void throw_no_goal_if_enabled(proof_state const & ps) { - throw_tactic_exception_if_enabled(ps, "invalid tactic, there are no goals to be solved"); -} - -tactic tactic01(std::function(environment const &, io_state const & ios, proof_state const &)> f) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { - return mk_proof_state_seq([=]() { - auto r = f(env, ios, s); - if (r) - return some(mk_pair(*r, proof_state_seq())); - else - return proof_state_seq::maybe_pair(); - }); - }); -} - -tactic tactic1(std::function f) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { - return mk_proof_state_seq([=]() { - auto r = f(env, ios, s); - return some(mk_pair(r, proof_state_seq())); - }); - }); -} - -tactic id_tactic() { - return tactic1([](environment const &, io_state const &, proof_state const & s) -> proof_state { return s; }); -} - -tactic fail_tactic() { - return tactic([](environment const &, io_state const &, proof_state const &) -> proof_state_seq { return proof_state_seq(); }); -} - -tactic now_tactic() { - return tactic01([](environment const &, io_state const &, proof_state const & s) -> optional { - if (!empty(s.get_goals())) - return none_proof_state(); - else - return some(s); - }); -} - -tactic cond(proof_state_pred p, tactic const & t1, tactic const & t2) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq { - return mk_proof_state_seq([=]() { - if (p(env, ios, s)) { - return t1(env, ios, s).pull(); - } else { - return t2(env, ios, s).pull(); - } - }); - }); -} - -tactic then(tactic const & t1, tactic const & t2) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s1) -> proof_state_seq { - return map_append(t1(env, ios, s1), [=](proof_state const & s2) { - check_interrupted(); - bool has_meta = false; - goals const & gs = s2.get_goals(); - for (goal const & g : gs) { - if (has_expr_metavar_relaxed(g.get_type())) { - has_meta = true; - break; - } - } - if (has_meta) { - buffer gs; - substitution subst = s2.get_subst(); - to_buffer(s2.get_goals(), gs); - for (unsigned i = 0; i < gs.size(); i++) { - gs[i] = gs[i].instantiate(subst); - } - proof_state new_s2(s2, to_list(gs)); - return t2(env, ios, new_s2); - } else { - return t2(env, ios, s2); - } - }, "THEN tactical"); - }); -} - -tactic orelse(tactic const & t1, tactic const & t2) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq { - proof_state s = _s.update_report_failure(false); - return orelse(t1(env, ios, s), t2(env, ios, s), "ORELSE tactical"); - }); -} - -tactic using_params(tactic const & t, options const & opts) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq { - io_state new_ios(ios); - new_ios.set_options(join(opts, ios.get_options())); - return t(env, new_ios, s); - }); -} - -proof_state rotate_left(proof_state const & s, unsigned n) { - buffer gs; - to_buffer(s.get_goals(), gs); - unsigned sz = gs.size(); - if (sz == 0) - return s; - n = n%sz; - std::rotate(gs.begin(), gs.begin() + n, gs.end()); - return proof_state(s, to_list(gs.begin(), gs.end())); -} - -tactic rotate_left(unsigned n) { - return tactic1([=](environment const &, io_state const &, proof_state const & s) -> proof_state { - return rotate_left(s, n); - }); -} - -tactic rotate_right(unsigned n) { - return tactic1([=](environment const &, io_state const &, proof_state const & s) -> proof_state { - unsigned ngoals = length(s.get_goals()); - if (ngoals == 0) - return s; - return rotate_left(s, ngoals - n%ngoals); - }); -} - -tactic try_for(tactic const & t, unsigned ms, unsigned check_ms) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq { - proof_state s = _s.update_report_failure(false); - return timeout(t(env, ios, s), ms, check_ms); - }); -} - -tactic par(tactic const & t1, tactic const & t2, unsigned check_ms) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq { - proof_state s = _s.update_report_failure(false); - return par(t1(env, ios, s), t2(env, ios, s), check_ms); - }); -} - -tactic repeat(tactic const & t) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & _s1) -> proof_state_seq { - proof_state s1 = _s1.update_report_failure(false); - return repeat(s1, [=](proof_state const & s2) { - return t(env, ios, s2); - }, "REPEAT tactical"); - }); -} - -tactic repeat_at_most(tactic const & t, unsigned k) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & _s1) -> proof_state_seq { - proof_state s1 = _s1.update_report_failure(false); - return repeat_at_most(s1, [=](proof_state const & s2) { - return t(env, ios, s2); - }, k, "REPEAT_AT_MOST tactical"); - }); -} - -tactic take(tactic const & t, unsigned k) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq { - proof_state s = _s.update_report_failure(false); - return take(k, t(env, ios, s)); - }); -} - -tactic discard(tactic const & t, unsigned k) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq { - proof_state s = _s.update_report_failure(false); - auto r = t(env, ios, s); - for (unsigned i = 0; i < k; i++) { - auto m = r.pull(); - if (!m) - return proof_state_seq(); - r = m->second; - } - return r; - }); -} - -tactic beta_tactic() { - return tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { - bool reduced = false; - goals new_gs = map_goals(s, [&](goal const & g) -> optional { - expr new_meta = beta_reduce(g.get_meta()); - expr new_type = beta_reduce(g.get_type()); - if (new_meta != g.get_meta() || new_type != g.get_type()) - reduced = true; - return some(goal(new_meta, new_type)); - }); - return reduced ? some(proof_state(s, new_gs)) : none_proof_state(); - }); -} - -proof_state_seq focus_core(tactic const & t, unsigned i, environment const & env, io_state const & ios, proof_state const & s) { - goals gs = s.get_goals(); - if (i >= length(gs)) - return proof_state_seq(); - goal const & g = get_ith(gs, i); - proof_state new_s(s, goals(g)); // singleton goal - return map(t(env, ios, new_s), [=](proof_state const & s2) { - // we have to put back the goals that were not selected - buffer tmp; - to_buffer(gs, tmp); - buffer new_gs; - new_gs.append(i, tmp.data()); - for (auto g : s2.get_goals()) - new_gs.push_back(g); - new_gs.append(tmp.size()-i-1, tmp.data()+i+1); - return proof_state(s2, to_list(new_gs.begin(), new_gs.end())); - }); -} - -tactic focus(tactic const & t, unsigned i) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq { - return focus_core(t, i, env, ios, s); - }); -} - -tactic all_goals(tactic const & t) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq { - tactic r = id_tactic(); - unsigned i = length(s.get_goals()); - while (i > 0) { - --i; - r = then(r, focus(t, i)); - } - return r(env, ios, s); - }); -} -} diff --git a/src/library/old_tactic/tactic/tactic.h b/src/library/old_tactic/tactic/tactic.h deleted file mode 100644 index 6596b57bf5..0000000000 --- a/src/library/old_tactic/tactic/tactic.h +++ /dev/null @@ -1,140 +0,0 @@ -/* -Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include -#include -#include -#include "util/lazy_list.h" -#include "library/io_state.h" -#include "library/generic_exception.h" -#include "library/tactic/proof_state.h" - -namespace lean { -/** \brief Throw an exception is \c v contains local constants, \c e is only used for position information. */ -void check_has_no_local(expr const & v, expr const & e, char const * tac_name); - -class tactic_exception : public generic_exception { - optional m_ps; -public: - tactic_exception(char const * msg, optional const & m, pp_fn const & fn); - tactic_exception(char const * msg, optional const & m, proof_state const & ps, pp_fn const & fn); - tactic_exception(expr const & e, std::string const & msg); - tactic_exception(expr const & e, char const * msg); - tactic_exception(expr const & e, sstream const & strm); - tactic_exception(expr const & e, pp_fn const & fn); - tactic_exception(std::string const & msg); - tactic_exception(char const * msg); - tactic_exception(sstream const & strm); - tactic_exception(pp_fn const & fn); - optional const & get_proof_state() const { return m_ps; } -}; - -#define throw_tactic_exception_if_enabled(ps, msg) if (ps.report_failure()) throw tactic_exception(msg); -void throw_no_goal_if_enabled(proof_state const & ps); - -typedef lazy_list proof_state_seq; - -typedef std::function tactic; - -inline optional none_tactic() { return optional(); } -inline optional some_tactic(tactic const & t) { return optional(t); } -inline optional some_tactic(tactic && t) { return optional(std::forward(t)); } - -template inline proof_state_seq mk_proof_state_seq(F && f) { return mk_lazy_list(std::forward(f)); } - -tactic tactic01(std::function(environment const &, io_state const & ios, proof_state const &)> f); -tactic tactic1(std::function f); - -/** \brief Return a "do nothing" tactic (aka skip). */ -tactic id_tactic(); -/** \brief Return a tactic the always fails. */ -tactic fail_tactic(); -/** \brief Return a tactic that fails if there are unsolved goals. */ -tactic now_tactic(); -/** \brief Return a tactic that performs \c t1 followed by \c t2. */ -tactic then(tactic const & t1, tactic const & t2); -inline tactic operator<<(tactic const & t1, tactic const & t2) { return then(t1, t2); } -/** \brief Return a tactic that applies \c t1, and if \c t1 returns the empty sequence of states, then applies \c t2. */ -tactic orelse(tactic const & t1, tactic const & t2); -inline tactic operator||(tactic const & t1, tactic const & t2) { return orelse(t1, t2); } -inline tactic try_tactic(tactic const & t) { return orelse(t, id_tactic()); } -/** \brief Return a tactic that appies \c t, but using the additional set of options \c opts. */ -tactic using_params(tactic const & t, options const & opts); -/** - \brief Return a tactic that tries the tactic \c t for at most \c ms milliseconds. - If the tactic does not terminate in \c ms milliseconds, then the empty - sequence is returned. - - \remark the tactic \c t is executed in a separate execution thread. - - \remark \c check_ms is how often the main thread checks whether the child - thread finished. -*/ -tactic try_for(tactic const & t, unsigned ms, unsigned check_ms = 1); - -/** \brief Return a tactic that rotate goals to the left n steps */ -tactic rotate_left(unsigned n); -/** \brief Return a tactic that rotate goals to the right n steps */ -tactic rotate_right(unsigned n); - -/** - \brief Return a tactic that executes \c t1 and \c t2 in parallel. - This is similar to \c append and \c interleave. The order of - the elements in the output sequence is not deterministic. - It depends on how fast \c t1 and \c t2 produce their output. - - \remark \c check_ms is how often the main thread checks whether the children - threads finished. -*/ -tactic par(tactic const & t1, tactic const & t2, unsigned check_ms); -inline tactic par(tactic const & t1, tactic const & t2) { return par(t1, t2, 1); } -/** - \brief Return a tactic that keeps applying \c t until it fails. -*/ -tactic repeat(tactic const & t); -/** - \brief Similar to \c repeat, but execute \c t at most \c k times. - - \remark The value \c k is the depth of the recursion. - For example, if tactic \c t always produce a sequence of size 2, - then tactic \c t will be applied 2^k times. -*/ -tactic repeat_at_most(tactic const & t, unsigned k); -/** - \brief Return a tactic that applies \c t, but takes at most \c - \c k elements from the sequence produced by \c t. -*/ -tactic take(tactic const & t, unsigned k); -/** - \brief Return a tactic that applies \c t, but discards the first - \c k elements from the sequence produced by \c t. -*/ -tactic discard(tactic const & t, unsigned k); - -/** \brief Return a tactic that renames hypothesis \c from into \c to in the current goal. */ -tactic rename_tactic(name const & from, name const & to); - -typedef std::function proof_state_pred; // NOLINT -/** - \brief Return a tactic that applies the predicate \c p to the input state. - If \c p returns true, then applies \c t1. Otherwise, applies \c t2. -*/ -tactic cond(proof_state_pred p, tactic const & t1, tactic const & t2); -/** \brief Syntax-sugar for cond(p, t, id_tactic()) */ -inline tactic when(proof_state_pred p, tactic const & t) { return cond(p, t, id_tactic()); } -/** - \brief Return a tactic that applies \c t only to the i-th goal. - The tactic fails if the input state does have at least i goals. -*/ -tactic focus(tactic const & t, unsigned i); -inline tactic focus(tactic const & t) { return focus(t, 0); } -/** \brief Return a tactic that applies beta-reduction. */ -tactic beta_tactic(); -/** \brief Apply \c t to all goals in the proof state */ -tactic all_goals(tactic const & t); -}