From e945db83060517b39bbd976b52b48fd2f53208b4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 16 Jul 2016 13:37:54 -0400 Subject: [PATCH] chore(library/old_tactic/tactic): remove dead code --- .../old_tactic/tactic/change_tactic.cpp | 81 ---- src/library/old_tactic/tactic/change_tactic.h | 13 - .../old_tactic/tactic/congruence_tactic.cpp | 286 ----------- .../old_tactic/tactic/congruence_tactic.h | 16 - .../old_tactic/tactic/expr_to_tactic.cpp | 450 ------------------ .../old_tactic/tactic/expr_to_tactic.h | 102 ---- .../old_tactic/tactic/trace_tactic.cpp | 89 ---- src/library/old_tactic/tactic/trace_tactic.h | 25 - src/library/old_tactic/tactic/util.cpp | 33 -- src/library/old_tactic/tactic/util.h | 12 - 10 files changed, 1107 deletions(-) delete mode 100644 src/library/old_tactic/tactic/change_tactic.cpp delete mode 100644 src/library/old_tactic/tactic/change_tactic.h delete mode 100644 src/library/old_tactic/tactic/congruence_tactic.cpp delete mode 100644 src/library/old_tactic/tactic/congruence_tactic.h delete mode 100644 src/library/old_tactic/tactic/expr_to_tactic.cpp delete mode 100644 src/library/old_tactic/tactic/expr_to_tactic.h delete mode 100644 src/library/old_tactic/tactic/trace_tactic.cpp delete mode 100644 src/library/old_tactic/tactic/trace_tactic.h delete mode 100644 src/library/old_tactic/tactic/util.cpp delete mode 100644 src/library/old_tactic/tactic/util.h diff --git a/src/library/old_tactic/tactic/change_tactic.cpp b/src/library/old_tactic/tactic/change_tactic.cpp deleted file mode 100644 index 1a45edc521..0000000000 --- a/src/library/old_tactic/tactic/change_tactic.cpp +++ /dev/null @@ -1,81 +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 "util/fresh_name.h" -#include "kernel/type_checker.h" -#include "kernel/error_msgs.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 { -tactic change_goal_tactic(elaborate_fn const & elab, expr const & e) { - return tactic([=](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; - 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); - substitution subst = new_s.get_subst(); - auto tc = mk_type_checker(env); - constraint_seq cs; - if (tc->is_def_eq(t, *new_e, justification(), cs)) { - 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 final_e = new_subst.instantiate_all(*new_e); - expr M = g.mk_meta(mk_fresh_name(), final_e); - goal new_g(M, final_e); - 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_e); - goal new_g(M, *new_e); - 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 'change' tactic, the given type"); - r += pp_indent_expr(fmt, *new_e); - r += compose(line(), format("does not match the goal type")); - r += pp_indent_expr(fmt, t); - return r; - }); - return proof_state_seq(); - } - } - return proof_state_seq(); - }); -} - -void initialize_change_tactic() { - register_tac(get_tactic_change_name(), - [](old_type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - check_tactic_expr(app_arg(e), "invalid 'change' tactic, invalid argument"); - return change_goal_tactic(fn, get_tactic_expr_expr(app_arg(e))); - }); -} -void finalize_change_tactic() { -} -} diff --git a/src/library/old_tactic/tactic/change_tactic.h b/src/library/old_tactic/tactic/change_tactic.h deleted file mode 100644 index 5e849a4940..0000000000 --- a/src/library/old_tactic/tactic/change_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/tactic.h" - -namespace lean { -void initialize_change_tactic(); -void finalize_change_tactic(); -} diff --git a/src/library/old_tactic/tactic/congruence_tactic.cpp b/src/library/old_tactic/tactic/congruence_tactic.cpp deleted file mode 100644 index 4050c8f91d..0000000000 --- a/src/library/old_tactic/tactic/congruence_tactic.cpp +++ /dev/null @@ -1,286 +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 "library/util.h" -#include "library/locals.h" -#include "library/constants.h" -#include "library/reducible.h" -#include "library/class_instance_resolution.h" -#include "library/tactic/util.h" -#include "library/tactic/intros_tactic.h" -#include "library/tactic/subst_tactic.h" -#include "library/tactic/expr_to_tactic.h" - -namespace lean { -enum class congr_arg_kind { Fixed, Singleton, Eq }; - -optional mk_congr_subsingleton_thm(old_type_checker & tc, io_state const & ios, expr const & fn, optional const & expected_num_args, - buffer & arg_kinds, constraint_seq & cs) { - expr fn_type = tc.infer(fn, cs); - buffer hyps; - collected_locals ctx_buffer; - collect_locals(fn_type, ctx_buffer); - collect_locals(fn, ctx_buffer); - hyps.append(ctx_buffer.get_collected()); - list ctx = to_list(hyps); - - buffer domain; - expr codomain = to_telescope(tc, fn_type, domain, optional(), cs); - if (expected_num_args && *expected_num_args != domain.size()) { - if (*expected_num_args > domain.size()) - return none_expr(); - lean_assert(*expected_num_args < domain.size()); - while (domain.size() > *expected_num_args) { - codomain = Pi(domain.back(), codomain); - domain.pop_back(); - } - } - - buffer prop; // pp[i] iff i-th arg is a proposition - buffer ss; // ss[i] is not none iff i-th arg is a subsingleton - buffer codomain_deps_on; // codomain_deps_on[i] iff codomain depends on i-th argument - for (expr const & d : domain) { - prop.push_back(tc.is_prop(mlocal_type(d), cs) && tc.env().prop_proof_irrel()); - if (prop.back()) { - ss.push_back(true); - } else { - ss.push_back(static_cast(mk_subsingleton_instance(tc.env(), ios.get_options(), ctx, mlocal_type(d)))); - } - codomain_deps_on.push_back(depends_on(codomain, d)); - ctx = cons(d, ctx); - } - - buffer new_domain; - buffer conclusion_lhs; - for (unsigned i = 0; i < domain.size(); i++) { - lean_assert(i == new_domain.size()); - expr const & d_i = domain[i]; - expr new_type = replace_locals(mlocal_type(d_i), i, domain.data(), new_domain.data()); - expr new_d_i = mk_local(get_unused_name(local_pp_name(d_i), hyps), new_type); - hyps.push_back(new_d_i); - conclusion_lhs.push_back(new_d_i); - new_domain.push_back(new_d_i); - } - - buffer lhss, rhss; - buffer> eqs; - buffer ss_elim; // true if equality proof should be synthesized using singletion elimination - buffer conclusion_rhs; - name h("he"); - unsigned eqidx = 1; - for (unsigned i = 0; i < new_domain.size(); i++) { - expr const & d_i = new_domain[i]; - if (ss[i]) { - arg_kinds.push_back(congr_arg_kind::Singleton); - expr new_type = replace_locals(mlocal_type(d_i), rhss, lhss); - expr new_d_i = mk_local(get_unused_name(local_pp_name(d_i).append_after("new"), hyps), new_type); - hyps.push_back(new_d_i); - rhss.push_back(d_i); - lhss.push_back(new_d_i); - conclusion_rhs.push_back(new_d_i); - ss_elim.push_back(!prop[i]); - eqs.push_back(none_expr()); - } else { - unsigned j = i+1; - for (; j < new_domain.size(); j++) { - expr t_j = mlocal_type(new_domain[j]); - if (depends_on(t_j, d_i) && !ss[j]) - break; - } - if (j < new_domain.size() || codomain_deps_on[i]) { - arg_kinds.push_back(congr_arg_kind::Fixed); - conclusion_rhs.push_back(d_i); - } else { - arg_kinds.push_back(congr_arg_kind::Eq); - expr new_type = replace_locals(mlocal_type(d_i), rhss, lhss); - expr new_d_i = mk_local(get_unused_name(local_pp_name(d_i).append_after("new"), hyps), new_type); - name new_h_name = get_unused_name(name(h, eqidx), hyps); - eqidx++; - expr new_eq = mk_local(new_h_name, mk_eq(tc, new_d_i, d_i)); - hyps.push_back(new_d_i); - rhss.push_back(d_i); - lhss.push_back(new_d_i); - conclusion_rhs.push_back(new_d_i); - ss_elim.push_back(false); - eqs.push_back(some_expr(new_eq)); - } - } - } - for (optional const & eq : eqs) { - if (eq) - hyps.push_back(*eq); - } - expr conclusion = mk_eq(tc, mk_app(fn, conclusion_lhs), mk_app(fn, conclusion_rhs)); - expr mvar_type = Pi(hyps, conclusion); - expr mvar = mk_metavar(mk_fresh_name(), mvar_type); - expr meta = mk_app(mvar, hyps); - proof_state ps = to_proof_state(meta, conclusion).update_report_failure(false); - for (unsigned i = 0; i < eqs.size(); i++) { - goal const & g = head(ps.get_goals()); - optional const & eq = eqs[i]; - if (eq) { - auto new_eq = g.find_hyp(local_pp_name(*eq)); - if (auto new_ps = subst(tc.env(), mlocal_name(new_eq->first), false, ps)) { - ps = *new_ps; - } else { - return none_expr(); - } - } else if (ss_elim[i]) { - expr lhs = lhss[i]; - expr rhs = rhss[i]; - expr new_lhs, new_rhs; - if (auto it = g.find_hyp(local_pp_name(lhs))) - new_lhs = it->first; - else - return none_expr(); - if (auto it = g.find_hyp(local_pp_name(rhs))) - new_rhs = it->first; - else - return none_expr(); - buffer hyps; - g.get_hyps(hyps); - auto spr = mk_subsingleton_instance(tc.env(), ios.get_options(), to_list(hyps), mlocal_type(new_lhs)); - if (!spr) - return none_expr(); - expr new_eq = mk_local(get_unused_name(name(h, eqidx), hyps), mk_eq(tc, new_rhs, new_lhs)); - eqidx++; - expr new_eq_pr = mk_subsingleton_elim(tc, *spr, new_rhs, new_lhs); - expr aux_mvar = mk_metavar(mk_fresh_name(), Pi(hyps, g.get_type())); - expr aux_meta_core = mk_app(aux_mvar, hyps); - goal aux_g(mk_app(aux_meta_core, new_eq), g.get_type()); - substitution new_subst = ps.get_subst(); - assign(new_subst, g, mk_app(aux_meta_core, new_eq_pr)); - proof_state aux_ps = proof_state(ps, goals(aux_g), new_subst); - if (auto new_ps = subst(tc.env(), mlocal_name(new_eq), false, aux_ps)) { - ps = *new_ps; - } else { - return none_expr(); - } - } else { - // do nothing, it is a proposition - } - } - - substitution subst = ps.get_subst(); - goal const & g = head(ps.get_goals()); - assign(subst, g, mk_refl(tc, app_arg(g.get_type()))); - expr result = subst.instantiate_all(mvar); - try { - check_term(tc, result); - } catch (exception &) { - return none_expr(); - } - for (expr const & ctx_local : ctx_buffer.get_collected()) { - result = mk_app(result, ctx_local); - mvar_type = instantiate(binding_body(mvar_type), ctx_local); - } - result = head_beta_reduce(result); - return some_expr(result); -} - -tactic congruence_tactic() { - auto fn = [=](environment const & env, io_state const & ios, 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); - expr t = g.get_type(); - substitution subst = s.get_subst(); - auto tc = mk_type_checker(env); - constraint_seq cs; - t = tc->whnf(t, cs); - expr lhs, rhs; - if (!is_eq(t, lhs, rhs)) { - throw_tactic_exception_if_enabled(s, "invalid 'congruence' tactic, goal is not an equality"); - return none_proof_state(); - } - - if (!is_app(lhs) || !is_app(rhs)) { - throw_tactic_exception_if_enabled(s, "invalid 'congruence' tactic, left and right hand side of equation must be a function application"); - return none_proof_state(); - } - - buffer lhs_args, rhs_args; - expr lhs_fn = get_app_args(lhs, lhs_args); - expr rhs_fn = get_app_args(rhs, rhs_args); - - if (lhs_args.size() != rhs_args.size()) { - throw_tactic_exception_if_enabled(s, "invalid 'congruence' tactic, left and right hand side of equation must have the same number of arguments"); - return none_proof_state(); - } - - expr lhs_fn_type = tc->whnf(tc->infer(lhs_fn, cs), cs); - expr rhs_fn_type = tc->whnf(tc->infer(rhs_fn, cs), cs); - if (!tc->is_def_eq(lhs_fn_type, rhs_fn_type, justification(), cs)) { - throw_tactic_exception_if_enabled(s, "invalid 'congruence' tactic, functions do not have the same type"); - return none_proof_state(); - } - - buffer new_goals; - optional fn_pr; - if (!tc->is_def_eq(lhs_fn, rhs_fn, justification(), cs)) { - expr new_type = mk_eq(*tc, lhs_fn, rhs_fn); - expr new_meta = g.mk_meta(mk_fresh_name(), new_type); - new_goals.push_back(goal(new_meta, new_type)); - fn_pr = new_meta; - } - - buffer arg_kinds; - auto cg_proof = mk_congr_subsingleton_thm(*tc, ios, lhs_fn, some(lhs_args.size()), arg_kinds, cs); - if (!cg_proof) { - throw_tactic_exception_if_enabled(s, "invalid 'congruence' tactic, tactic does not support this kind of dependent function"); - return none_proof_state(); - } - - expr pr = mk_app(*cg_proof, lhs_args); - for (unsigned i = 0; i < arg_kinds.size(); i++) { - if (arg_kinds[i] == congr_arg_kind::Fixed) { - if (!tc->is_def_eq(lhs_args[i], rhs_args[i], justification(), cs)) { - throw_tactic_exception_if_enabled(s, sstream() << "invalid 'congruence' tactic, argument #" << (i+1) - << " must be the same in the left and right hand sides"); - return none_proof_state(); - } - } else { - pr = mk_app(pr, rhs_args[i]); - } - } - - for (unsigned i = 0; i < arg_kinds.size(); i++) { - if (arg_kinds[i] == congr_arg_kind::Eq) { - if (tc->is_def_eq(lhs_args[i], rhs_args[i], justification(), cs)) { - pr = mk_app(pr, mk_refl(*tc, lhs_args[i])); - } else { - expr new_type = mk_eq(*tc, lhs_args[i], rhs_args[i]); - expr new_meta = g.mk_meta(mk_fresh_name(), new_type); - new_goals.push_back(goal(new_meta, new_type)); - pr = mk_app(pr, mk_symm(*tc, new_meta)); - } - } - } - - if (fn_pr) { - expr motive_rhs = mk_app(mk_var(0), rhs_args); - expr motive = mk_lambda("f", lhs_fn_type, mk_app(app_fn(app_fn(g.get_type())), lhs, motive_rhs)); - pr = mk_subst(*tc, motive, lhs_fn, rhs_fn, *fn_pr, pr); - } - - assign(subst, g, pr); - proof_state new_ps(s, to_list(new_goals.begin(), new_goals.end(), tail(gs)), subst); - if (solve_constraints(env, ios, new_ps, cs)) - return some_proof_state(new_ps); - return none_proof_state(); - }; - return tactic01(fn); -} -void initialize_congruence_tactic() { register_simple_tac(name{"tactic", "congruence"}, congruence_tactic); } -void finalize_congruence_tactic() {} -} diff --git a/src/library/old_tactic/tactic/congruence_tactic.h b/src/library/old_tactic/tactic/congruence_tactic.h deleted file mode 100644 index 6ee7d46f07..0000000000 --- a/src/library/old_tactic/tactic/congruence_tactic.h +++ /dev/null @@ -1,16 +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/type_checker.h" -namespace lean { -enum class congr_arg_kind { Fixed, Singleton, Eq }; -optional mk_congr_subsingleton_thm(type_checker & tc, io_state const & ios, - expr const & fn, optional const & expected_num_args, - buffer & arg_kinds, constraint_seq & cs); -void initialize_congruence_tactic(); -void finalize_congruence_tactic(); -} diff --git a/src/library/old_tactic/tactic/expr_to_tactic.cpp b/src/library/old_tactic/tactic/expr_to_tactic.cpp deleted file mode 100644 index 84b086c665..0000000000 --- a/src/library/old_tactic/tactic/expr_to_tactic.cpp +++ /dev/null @@ -1,450 +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 -#include -#include "util/sstream.h" -#include "util/optional.h" -#include "kernel/instantiate.h" -#include "library/annotation.h" -#include "library/string.h" -#include "library/explicit.h" -#include "library/placeholder.h" -#include "library/old_type_checker.h" -#include "library/num.h" -#include "library/constants.h" -#include "library/projection.h" -#include "library/kernel_serializer.h" -#include "library/tactic/expr_to_tactic.h" - -namespace lean { -static expr * g_and_then_tac_fn = nullptr; -static expr * g_or_else_tac_fn = nullptr; -static expr * g_id_tac_fn = nullptr; -static expr * g_repeat_tac_fn = nullptr; -static expr * g_determ_tac_fn = nullptr; -static expr * g_tac_type = nullptr; -static expr * g_builtin_tac = nullptr; -static expr * g_fixpoint_tac = nullptr; -expr const & get_and_then_tac_fn() { return *g_and_then_tac_fn; } -expr const & get_or_else_tac_fn() { return *g_or_else_tac_fn; } -expr const & get_id_tac_fn() { return *g_id_tac_fn; } -expr const & get_determ_tac_fn() { return *g_determ_tac_fn; } -expr const & get_repeat_tac_fn() { return *g_repeat_tac_fn; } -expr const & get_tactic_type() { return *g_tac_type; } -expr const & get_builtin_tac() { return *g_builtin_tac; } - -typedef std::unordered_map expr_to_tactic_map; -static expr_to_tactic_map * g_map = nullptr; - -expr_to_tactic_map & get_expr_to_tactic_map() { - return *g_map; -} - -void register_tac(name const & n, expr_to_tactic_fn const & fn) { - get_expr_to_tactic_map().insert(mk_pair(n, fn)); -} - -bool has_tactic_decls(environment const & env) { - try { - old_type_checker tc(env); - return - tc.infer(*g_builtin_tac).first == *g_tac_type && - tc.infer(*g_and_then_tac_fn).first == *g_tac_type >> (*g_tac_type >> *g_tac_type) && - tc.infer(*g_or_else_tac_fn).first == *g_tac_type >> (*g_tac_type >> *g_tac_type) && - tc.infer(*g_repeat_tac_fn).first == *g_tac_type >> *g_tac_type; - } catch (exception &) { - return false; - } -} - -static expr * g_tactic_expr_type = nullptr; -static expr * g_tactic_expr_builtin = nullptr; -static expr * g_tactic_expr_list_type = nullptr; -static expr * g_tactic_identifier_type = nullptr; -static expr * g_tactic_using_expr_type = nullptr; -static expr * g_tactic_location_type = nullptr; -static expr * g_tactic_with_expr_type = nullptr; - -expr const & get_tactic_expr_type() { return *g_tactic_expr_type; } -expr const & get_tactic_expr_builtin() { return *g_tactic_expr_builtin; } -expr const & get_tactic_expr_list_type() { return *g_tactic_expr_list_type; } -expr const & get_tactic_identifier_type() { return *g_tactic_identifier_type; } -expr const & get_tactic_using_expr_type() { return *g_tactic_using_expr_type; } -expr const & get_tactic_location_type() { return *g_tactic_location_type; } -expr const & get_tactic_with_expr_type() { return *g_tactic_with_expr_type; } - -static std::string * g_tactic_expr_opcode = nullptr; -static std::string * g_tactic_opcode = nullptr; - -std::string const & get_tactic_expr_opcode() { return *g_tactic_expr_opcode; } -std::string const & get_tactic_opcode() { return *g_tactic_opcode; } - -class tactic_expr_macro_definition_cell : public macro_definition_cell { -public: - tactic_expr_macro_definition_cell() {} - virtual name get_name() const { return get_tactic_expr_name(); } - virtual expr check_type(expr const &, abstract_type_context &, bool) const { - return get_tactic_expr_type(); - } - virtual optional expand(expr const &, abstract_type_context &) const { - return some_expr(get_tactic_expr_builtin()); - } - virtual void write(serializer & s) const { - s.write_string(get_tactic_expr_opcode()); - } -}; - -static macro_definition * g_tactic_expr_macro = nullptr; - -expr mk_tactic_expr(expr const & e) { - return mk_macro(*g_tactic_expr_macro, 1, &e, e.get_tag()); -} - -bool is_tactic_expr(expr const & e) { - return is_macro(e) && macro_def(e).get_name() == get_tactic_expr_name(); -} - -expr const & get_tactic_expr_expr(expr const & e) { - lean_assert(is_tactic_expr(e)); - expr const * it = &e; - while (is_tactic_expr(*it)) - it = ¯o_arg(*it, 0); - return *it; -} - -void check_tactic_expr(expr const & e, char const * error_msg) { - if (!is_tactic_expr(e)) - throw expr_to_tactic_exception(e, error_msg); -} - -name const & tactic_expr_to_id(expr e, char const * error_msg) { - if (is_tactic_expr(e)) - e = get_tactic_expr_expr(e); - - if (is_constant(e)) { - return const_name(e); - } else if (is_local(e)) { - return local_pp_name(e); - } else if (is_as_atomic(e)) { - e = get_app_fn(get_as_atomic_arg(e)); - if (is_explicit(e)) - e = get_explicit_arg(e); - return tactic_expr_to_id(e, error_msg); - } else { - throw expr_to_tactic_exception(e, error_msg); - } -} - -static expr * g_expr_list_cons = nullptr; -static expr * g_expr_list_nil = nullptr; - -expr mk_expr_list(unsigned num, expr const * args) { - expr r = *g_expr_list_nil; - unsigned i = num; - while (i > 0) { - --i; - r = mk_app(*g_expr_list_cons, args[i], r); - } - return r; -} - -expr ids_to_tactic_expr(buffer const & args) { - buffer es; - for (name const & id : args) { - es.push_back(mk_local(id, mk_expr_placeholder())); - } - return mk_expr_list(es.size(), es.data()); -} - -void get_tactic_expr_list_elements(expr l, buffer & r, char const * error_msg) { - while (true) { - if (l == *g_expr_list_nil) - return; - if (!is_app(l) || - !is_app(app_fn(l)) || - app_fn(app_fn(l)) != *g_expr_list_cons || - !is_tactic_expr(app_arg(app_fn(l)))) - throw expr_to_tactic_exception(l, error_msg); - r.push_back(get_tactic_expr_expr(app_arg(app_fn(l)))); - l = app_arg(l); - } -} - -void get_tactic_id_list_elements(expr l, buffer & r, char const * error_msg) { - buffer es; - get_tactic_expr_list_elements(l, es, error_msg); - for (unsigned i = 0; i < es.size(); i++) { - r.push_back(tactic_expr_to_id(es[i], error_msg)); - } -} - -static void throw_failed(expr const & e) { - throw expr_to_tactic_exception(e, "failed to convert expression into tactic"); -} - -/** \brief Return true if v is the constant tactic.builtin or the constant function that returns tactic.builtin_tactic */ -static bool is_builtin_tactic(expr const & v) { - if (is_lambda(v)) - return is_builtin_tactic(binding_body(v)); - else if (v == *g_builtin_tac) - return true; - else - return false; -} - -tactic expr_to_tactic(old_type_checker & tc, elaborate_fn const & fn, expr e, pos_info_provider const * p) { - e = copy_tag(e, tc.whnf(e).first); - expr f = get_app_fn(e); - if (!is_constant(f)) - throw_failed(e); - optional it = tc.env().find(const_name(f)); - if (!it || !it->is_definition()) - throw_failed(e); - expr v = it->get_value(); - if (is_builtin_tactic(v)) { - auto const & map = get_expr_to_tactic_map(); - auto it2 = map.find(const_name(f)); - if (it2 != map.end()) - return it2->second(tc, fn, e, p); - else - throw expr_to_tactic_exception(e, sstream() << "implementation for builtin tactic '" << - const_name(f) << "' was not found"); - } else { - // unfold definition - buffer locals; - get_app_rev_args(e, locals); - level_param_names const & ps = it->get_univ_params(); - levels ls = const_levels(f); - unsigned num_ps = length(ps); - unsigned num_ls = length(ls); - if (num_ls > num_ps) - throw expr_to_tactic_exception(e, sstream() << "invalid number of universes"); - if (num_ls < num_ps) { - buffer extra_ls; - for (unsigned i = num_ls; i < num_ps; i++) - extra_ls.push_back(mk_meta_univ(mk_fresh_name())); - ls = append(ls, to_list(extra_ls.begin(), extra_ls.end())); - } - v = instantiate_univ_params(v, ps, ls); - v = apply_beta(v, locals.size(), locals.data()); - return expr_to_tactic(tc, fn, v, p); - } -} - -unsigned get_unsigned(old_type_checker & tc, expr const & e, expr const & ref) { - optional k = to_num(e); - if (!k) - k = to_num(tc.whnf(e).first); - if (!k) - throw expr_to_tactic_exception(ref, "invalid tactic, second argument must be a numeral"); - if (!k->is_unsigned_int()) - throw expr_to_tactic_exception(ref, - "invalid tactic, second argument does not fit in " - "a machine unsigned integer"); - return k->get_unsigned_int(); -} - -unsigned get_unsigned_arg(old_type_checker & tc, expr const & e, unsigned i) { - buffer args; - get_app_args(e, args); - if (i >= args.size()) - throw expr_to_tactic_exception(e, "invalid tactic, insufficient number of arguments"); - return get_unsigned(tc, args[i], e); -} - -optional get_optional_unsigned(old_type_checker & tc, expr const & e) { - if (is_app(e) && is_constant(get_app_fn(e))) { - if (const_name(get_app_fn(e)) == get_option_some_name()) { - return optional(get_unsigned(tc, app_arg(e), e)); - } else if (const_name(get_app_fn(e)) == get_option_none_name()) { - return optional(); - } - } - throw expr_to_tactic_exception(e, "invalid tactic, argument is not an option num"); -} - -class tac_builtin_opaque_converter : public projection_converter { -public: - tac_builtin_opaque_converter(environment const & env):projection_converter(env) {} - virtual bool is_opaque(declaration const & d) const { - name n = d.get_name(); - if (!is_prefix_of(get_tactic_name(), n)) - return projection_converter::is_opaque(d); - expr v = d.get_value(); - while (is_lambda(v)) - v = binding_body(v); - if (is_constant(v) && const_name(v) == get_tactic_builtin_name()) - return true; - return projection_converter::is_opaque(d); - } -}; - -tactic expr_to_tactic(environment const & env, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) { - bool memoize = false; - old_type_checker tc(env, std::unique_ptr(new tac_builtin_opaque_converter(env)), memoize); - return expr_to_tactic(tc, fn, e, p); -} - -tactic fixpoint(expr const & b, elaborate_fn const & fn) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq { - return expr_to_tactic(env, fn, b, nullptr)(env, ios, s); - }); -} - -void register_simple_tac(name const & n, std::function f) { - register_tac(n, [=](old_type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - if (!is_constant(e)) - throw expr_to_tactic_exception(e, "invalid constant tactic"); - return f(); - }); -} - -void register_bin_tac(name const & n, std::function f) { - register_tac(n, [=](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) { - buffer args; - get_app_args(e, args); - if (args.size() != 2) - throw expr_to_tactic_exception(e, "invalid binary tactic, it must have two arguments"); - tactic t1 = expr_to_tactic(tc, fn, args[0], p); - tactic t2 = expr_to_tactic(tc, fn, args[1], p); - return f(t1, t2); - }); -} - -void register_unary_tac(name const & n, std::function f) { - register_tac(n, [=](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) { - buffer args; - get_app_args(e, args); - if (args.size() != 1) - throw expr_to_tactic_exception(e, "invalid unary tactic, it must have one argument"); - return f(expr_to_tactic(tc, fn, args[0], p)); - }); -} - -void register_unary_num_tac(name const & n, std::function f) { - register_tac(n, [=](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) { - buffer args; - get_app_args(e, args); - if (args.size() != 2) - throw expr_to_tactic_exception(e, "invalid tactic, it must have two arguments"); - tactic t = expr_to_tactic(tc, fn, args[0], p); - return f(t, get_unsigned_arg(tc, e, 1)); - }); -} - -void register_num_tac(name const & n, std::function f) { - register_tac(n, [=](old_type_checker & tc, elaborate_fn const &, expr const & e, pos_info_provider const *) { - buffer args; - get_app_args(e, args); - if (args.size() != 1) - throw expr_to_tactic_exception(e, "invalid tactic, it must have one argument"); - return f(get_unsigned_arg(tc, e, 0)); - }); -} - -static name * g_by_name = nullptr; - -expr mk_by(expr const & e) { return mk_annotation(*g_by_name, e); } -bool is_by(expr const & e) { return is_annotation(e, *g_by_name); } -expr const & get_by_arg(expr const & e) { lean_assert(is_by(e)); return get_annotation_arg(e); } - -void initialize_expr_to_tactic() { - g_by_name = new name("by"); - register_annotation(*g_by_name); - - g_map = new expr_to_tactic_map(); - - g_tactic_expr_type = new expr(mk_constant(get_tactic_expr_name())); - g_tactic_expr_builtin = new expr(mk_constant(get_tactic_expr_builtin_name())); - g_tactic_expr_list_type = new expr(mk_constant(get_tactic_expr_list_name())); - g_tactic_identifier_type = new expr(mk_constant(get_tactic_identifier_name())); - g_tactic_using_expr_type = new expr(mk_constant(get_tactic_using_expr_name())); - g_tactic_location_type = new expr(mk_constant(get_tactic_location_name())); - g_tactic_with_expr_type = new expr(mk_constant(get_tactic_with_expr_name())); - g_tactic_expr_opcode = new std::string("TACE"); - g_tactic_expr_macro = new macro_definition(new tactic_expr_macro_definition_cell()); - - register_macro_deserializer(*g_tactic_expr_opcode, - [](deserializer &, unsigned num, expr const * args) { - if (num != 1) - throw corrupted_stream_exception(); - return mk_tactic_expr(args[0]); - }); - - g_expr_list_cons = new expr(mk_constant(get_tactic_expr_list_cons_name())); - g_expr_list_nil = new expr(mk_constant(get_tactic_expr_list_nil_name())); - - g_and_then_tac_fn = new expr(Const(get_tactic_and_then_name())); - g_or_else_tac_fn = new expr(Const(get_tactic_or_else_name())); - g_id_tac_fn = new expr(Const(get_tactic_id_name())); - g_repeat_tac_fn = new expr(Const(get_tactic_repeat_name())); - g_determ_tac_fn = new expr(Const(get_tactic_determ_name())); - g_tac_type = new expr(Const(get_tactic_name())); - g_builtin_tac = new expr(Const(get_tactic_builtin_name())); - g_fixpoint_tac = new expr(Const(get_tactic_fixpoint_name())); - - register_simple_tac(get_tactic_id_name(), - []() { return id_tactic(); }); - register_simple_tac(get_tactic_now_name(), - []() { return now_tactic(); }); - register_simple_tac(get_tactic_fail_name(), - []() { return fail_tactic(); }); - register_bin_tac(get_tactic_and_then_name(), - [](tactic const & t1, tactic const & t2) { return then(t1, t2); }); - register_bin_tac(get_tactic_par_name(), - [](tactic const & t1, tactic const & t2) { return par(t1, t2); }); - register_bin_tac(get_tactic_or_else_name(), - [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); }); - register_unary_tac(get_tactic_repeat_name(), - [](tactic const & t1) { return repeat(t1); }); - register_unary_tac(get_tactic_all_goals_name(), - [](tactic const & t1) { return all_goals(t1); }); - register_unary_num_tac(get_tactic_at_most_name(), - [](tactic const & t, unsigned k) { return take(t, k); }); - register_unary_num_tac(get_tactic_discard_name(), - [](tactic const & t, unsigned k) { return discard(t, k); }); - register_unary_num_tac(get_tactic_focus_at_name(), - [](tactic const & t, unsigned k) { return focus(t, k); }); - register_unary_num_tac(get_tactic_try_for_name(), - [](tactic const & t, unsigned k) { return try_for(t, k); }); - register_num_tac(get_tactic_rotate_left_name(), [](unsigned k) { return rotate_left(k); }); - register_num_tac(get_tactic_rotate_right_name(), [](unsigned k) { return rotate_right(k); }); - - register_tac(get_tactic_fixpoint_name(), - [](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - if (!is_constant(app_fn(e))) - throw expr_to_tactic_exception(e, "invalid fixpoint tactic, it must have one argument"); - expr r = tc.whnf(mk_app(app_arg(e), e)).first; - return fixpoint(r, fn); - }); -} - -void finalize_expr_to_tactic() { - delete g_expr_list_cons; - delete g_expr_list_nil; - delete g_tactic_expr_type; - delete g_tactic_expr_builtin; - delete g_tactic_expr_list_type; - delete g_tactic_identifier_type; - delete g_tactic_using_expr_type; - delete g_tactic_location_type; - delete g_tactic_with_expr_type; - delete g_tactic_expr_opcode; - delete g_tactic_expr_macro; - delete g_fixpoint_tac; - delete g_builtin_tac; - delete g_tac_type; - delete g_determ_tac_fn; - delete g_repeat_tac_fn; - delete g_or_else_tac_fn; - delete g_and_then_tac_fn; - delete g_id_tac_fn; - delete g_map; - delete g_tactic_opcode; - delete g_by_name; -} -} diff --git a/src/library/old_tactic/tactic/expr_to_tactic.h b/src/library/old_tactic/tactic/expr_to_tactic.h deleted file mode 100644 index 0a945e9eda..0000000000 --- a/src/library/old_tactic/tactic/expr_to_tactic.h +++ /dev/null @@ -1,102 +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 "kernel/pos_info_provider.h" -#include "library/old_type_checker.h" -#include "library/tactic/tactic.h" -#include "library/tactic/elaborate.h" - -namespace lean { -/** - \brief Return true iff the environment \c env contains the following declarations - in the namespace 'tactic' - tactic.builtin : tactic - and_then : tactic -> tactic -> tactic - or_else : tactic -> tactic -> tactic - repeat : tactic -> tactic -*/ -bool has_tactic_decls(environment const & env); - -/** - \brief Creates a tactic by 'executing' \c e. Definitions are unfolded, whnf procedure is invoked, - and definitions marked as 'tactic.builtin' are handled by the code registered using - \c register_expr_to_tactic. -*/ -tactic expr_to_tactic(environment const & env, elaborate_fn const & fn, expr const & e, pos_info_provider const * p); -// auxiliary procedure used to compile nested tactic in tacticals -tactic expr_to_tactic(old_type_checker & tc, elaborate_fn const & fn, expr e, pos_info_provider const * p); - -name const & get_tactic_name(); - -unsigned get_unsigned_arg(old_type_checker & tc, expr const & e, unsigned i); -optional get_optional_unsigned(old_type_checker & tc, expr const & e); - -expr const & get_tactic_expr_type(); -expr const & get_tactic_identifier_type(); -expr const & get_tactic_with_expr_type(); -expr const & get_tactic_location_type(); -expr const & get_tactic_with_expr_type(); -expr mk_tactic_expr(expr const & e); -bool is_tactic_expr(expr const & e); -expr const & get_tactic_expr_expr(expr const & e); -void check_tactic_expr(expr const & e, char const * msg); -expr const & get_tactic_expr_list_type(); -expr const & get_tactic_using_expr_type(); - -expr mk_expr_list(unsigned num, expr const * args); - -name const & tactic_expr_to_id(expr e, char const * error_msg); -void get_tactic_expr_list_elements(expr l, buffer & r, char const * error_msg); -void get_tactic_id_list_elements(expr l, buffer & r, char const * error_msg); -expr ids_to_tactic_expr(buffer const & ids); - -/** - \brief Create an expression `by t`, where \c t is an expression of type `tactic`. - This kind of expression only affects the elaborator, the kernel will reject - any declaration that contains it. - - \post get_by_arg(mk_by(t)) == t - \post is_by(mk_by(t)) -*/ -expr mk_by(expr const & t); -/** \brief Return true iff \c t is an expression created using \c mk_by */ -bool is_by(expr const & t); -/** \see mk_by */ -expr const & get_by_arg(expr const & t); - -expr const & get_tactic_type(); -expr const & get_and_then_tac_fn(); -expr const & get_or_else_tac_fn(); -expr const & get_id_tac_fn(); -expr const & get_repeat_tac_fn(); -expr const & get_determ_tac_fn(); - -/** \brief Exception used to report a problem when an expression is being converted into a tactic. */ -class expr_to_tactic_exception : public exception { - expr m_expr; -public: - expr_to_tactic_exception(expr const & e, char const * msg):exception(msg), m_expr(e) {} - expr_to_tactic_exception(expr const & e, sstream const & strm):exception(strm), m_expr(e) {} - expr const & get_expr() const { return m_expr; } -}; - -typedef std::function -expr_to_tactic_fn; - -/** \brief Register a new "procedural attachment" for expr_to_tactic. */ -void register_tac(name const & n, expr_to_tactic_fn const & fn); -// remark: we cannot use "std::function <...> const &" in the following procedures, for some obscure reason it produces -// memory leaks when we compile using clang 3.3 -void register_simple_tac(name const & n, std::function f); -void register_bin_tac(name const & n, std::function f); -void register_unary_tac(name const & n, std::function f); -void register_unary_num_tac(name const & n, std::function f); -void register_num_tac(name const & n, std::function f); - -void initialize_expr_to_tactic(); -void finalize_expr_to_tactic(); -} diff --git a/src/library/old_tactic/tactic/trace_tactic.cpp b/src/library/old_tactic/tactic/trace_tactic.cpp deleted file mode 100644 index 82ddf05b9b..0000000000 --- a/src/library/old_tactic/tactic/trace_tactic.cpp +++ /dev/null @@ -1,89 +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 -#include "util/sstream.h" -#include "kernel/type_checker.h" -#include "library/constants.h" -#include "library/string.h" -#include "library/tactic/tactic.h" -#include "library/tactic/expr_to_tactic.h" - -namespace lean { - -tactic trace_tactic(std::string const & msg) { - return tactic1([=](environment const &, io_state const & ios, proof_state const & s) -> proof_state { - ios.get_diagnostic_channel() << msg << "\n"; - ios.get_diagnostic_channel().get_stream().flush(); - return s; - }); -} - -tactic trace_tactic(sstream const & msg) { - return trace_tactic(msg.str()); -} - -tactic trace_tactic(char const * msg) { - return trace_tactic(std::string(msg)); -} - -tactic trace_state_tactic(std::string const & fname, pair const & pos) { - return tactic1([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state { - type_checker tc(env); - auto out = diagnostic(env, ios, tc); - out << fname << ":" << pos.first << ":" << pos.second << ": proof state\n" - << s.pp(out.get_formatter()) << endl; - ios.get_diagnostic_channel().get_stream().flush(); - return s; - }); -} - -tactic trace_state_tactic() { - return tactic1([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state { - type_checker tc(env); - auto out = diagnostic(env, ios, tc); - out << "proof state\n" << s.pp(out.get_formatter()) << endl; - ios.get_diagnostic_channel().get_stream().flush(); - return s; - }); -} - -tactic suppress_trace(tactic const & t) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq { - io_state new_ios(ios); - std::shared_ptr out(std::make_shared()); - new_ios.set_diagnostic_channel(out); - return t(env, new_ios, s); - }); -} - -void initialize_trace_tactic() { - register_tac(get_tactic_state_name(), - [](old_type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const * p) { - if (p) - if (auto it = p->get_pos_info(e)) - return trace_state_tactic(std::string(p->get_file_name()), *it); - return trace_state_tactic(); - }); - - register_tac(get_tactic_trace_name(), - [](old_type_checker & tc, elaborate_fn const &, expr const & e, pos_info_provider const *) { - buffer args; - get_app_args(e, args); - if (args.size() != 1) - throw expr_to_tactic_exception(e, "invalid trace tactic, argument expected"); - if (auto str = to_string(args[0])) - return trace_tactic(*str); - else if (auto str = to_string(tc.whnf(args[0]).first)) - return trace_tactic(*str); - else - throw expr_to_tactic_exception(e, "invalid trace tactic, string value expected"); - }); -} - -void finalize_trace_tactic() { -} -} diff --git a/src/library/old_tactic/tactic/trace_tactic.h b/src/library/old_tactic/tactic/trace_tactic.h deleted file mode 100644 index efd56ef52a..0000000000 --- a/src/library/old_tactic/tactic/trace_tactic.h +++ /dev/null @@ -1,25 +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 -#include "library/tactic/tactic.h" - -namespace lean { -/** \brief Return a tactic that just returns the input state, and display the given message in the diagnostic channel. */ -tactic trace_tactic(char const * msg); -class sstream; -tactic trace_tactic(sstream const & msg); -tactic trace_tactic(std::string const & msg); -/** \brief Return a tactic that just displays the input state in the diagnostic channel. */ -tactic trace_state_tactic(std::string const & fname, pair const & pos); -tactic trace_state_tactic(); -/** \brief Create a tactic that applies \c t, but suppressing diagnostic messages. */ -tactic suppress_trace(tactic const & t); - -void initialize_trace_tactic(); -void finalize_trace_tactic(); -} diff --git a/src/library/old_tactic/tactic/util.cpp b/src/library/old_tactic/tactic/util.cpp deleted file mode 100644 index 12db3551ef..0000000000 --- a/src/library/old_tactic/tactic/util.cpp +++ /dev/null @@ -1,33 +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 "library/aliases.h" -#include "library/constants.h" -#include "library/util.h" -#include "library/tactic/util.h" -#include "library/tactic/proof_state.h" - -namespace lean { -bool is_tactic_namespace_open(environment const & env) { - for (name const & a : get_expr_aliases(env, "apply")) { - if (a == get_tactic_apply_name()) { - // make sure the type is the expected one - if (auto d = env.find(a)) { - expr t = d->get_type(); - if (is_pi(t)) { - expr b = binding_body(t); - if (!is_constant(b) || const_name(b) != get_tactic_name()) - throw exception("tactic namespace declarations have been modified, " - "function 'tactic.apply' is expected to return a 'tactic'"); - } - } - return true; - } - } - return false; -} -} diff --git a/src/library/old_tactic/tactic/util.h b/src/library/old_tactic/tactic/util.h deleted file mode 100644 index cfbd9eb506..0000000000 --- a/src/library/old_tactic/tactic/util.h +++ /dev/null @@ -1,12 +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 "kernel/environment.h" -namespace lean { -/** \brief Return true iff the tactic namespace is open in given environment. */ -bool is_tactic_namespace_open(environment const & env); -}