max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/old_tactic/tactic): remove old code

Browse source 
It has already been ported to new tactic framework.
This commit is contained in:
Leonardo de Moura 2016-07-06 07:34:34 -07:00
parent b390521b30
commit c379783c84
2 changed files with 0 additions and 443 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

432
src/library/old_tactic/tactic/induction_tactic.cpp
View file

@ -1,432 +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/abstract.h"
#include "kernel/instantiate.h"
#include "kernel/inductive/inductive.h"
#include "library/util.h"
#include "library/old_util.h"
#include "library/user_recursors.h"
#include "library/constants.h"
#include "library/reducible.h"
#include "library/locals.h"
#include "library/class_instance_resolution.h"
#include "library/tactic/tactic.h"
#include "library/tactic/expr_to_tactic.h"
#include "library/tactic/generalize_tactic.h"
namespace lean {
class induction_tac {
environment const & m_env;
io_state const & m_ios;
old_type_checker & m_tc;
name m_h_name;
optional<name> m_rec_name;
list<name> m_ids;
substitution m_subst;
bool m_throw_ex;
bool m_standard;
constraint_seq m_cs;
expr m_ref; // reference expression for location information
void assign(goal const & g, expr const & val) {
::lean::assign(m_subst, g, val);
}
/** \brief Split hyps into two "telescopes".
- non_deps : hypotheses that do not depend on H nor its indices
- deps : hypotheses that depend on H or its indices (directly or indirectly)
*/
void split_deps(buffer<expr> const & hyps, expr const & h, buffer<expr> const & indices,
buffer<expr> & non_deps, buffer<expr> & deps) {
for (expr const & hyp : hyps) {
if (hyp == h) {
// we clear h
} else if (std::find(indices.begin(), indices.end(), hyp) != indices.end()) {
// hyp is an index
non_deps.push_back(hyp);
} else if (depends_on(hyp, h) || depends_on_any(hyp, indices) || depends_on_any(hyp, deps)) {
deps.push_back(hyp);
} else {
non_deps.push_back(hyp);
}
}
}
void throw_ill_formed_recursor(recursor_info const & rec_info) {
throw tactic_exception(sstream() << "invalid 'induction' tactic, recursor '" << rec_info.get_name()
<< "' is ill-formed");
}
expr mk_type_class_param(goal const & g, expr const & type) {
bool use_local_insts = true;
bool is_strict = false;
old_local_context ctx = g.to_local_context();
auto mc = mk_class_instance_elaborator(
m_env, m_ios, ctx, optional<name>(),
use_local_insts, is_strict,
some_expr(type), m_ref.get_tag(), nullptr);
m_cs += mc.second;
return mc.first;
}
expr mk_type_class_param(goal const & g, expr const & rec, recursor_info const & rec_info) {
expr rec_type = m_tc.whnf(m_tc.infer(rec, m_cs), m_cs);
if (!is_pi(rec_type)) {
throw_ill_formed_recursor(rec_info);
}
return mk_type_class_param(g, binding_domain(rec_type));
}
goals apply_recursor(goal const & g, unsigned num_deps, expr const & h, expr const & h_type,
buffer<optional<expr>> const & params, buffer<expr> const & indices,
recursor_info const & rec_info) {
expr const & g_type = g.get_type();
level g_lvl = sort_level(m_tc.ensure_type(g_type, m_cs));
buffer<level> rec_lvls;
expr const & I = get_app_fn(h_type);
buffer<level> I_lvls;
to_buffer(const_levels(I), I_lvls);
bool found_g_lvl = false;
for (unsigned idx : rec_info.get_universe_pos()) {
if (idx == recursor_info::get_motive_univ_idx()) {
rec_lvls.push_back(g_lvl);
found_g_lvl = true;
} else {
if (idx >= I_lvls.size())
throw_ill_formed_recursor(rec_info);
rec_lvls.push_back(I_lvls[idx]);
}
}
if (!found_g_lvl && !is_zero(g_lvl)) {
throw tactic_exception(sstream() << "invalid 'induction' tactic, recursor '" << rec_info.get_name()
<< "' can only eliminate into Prop");
}
expr rec = mk_constant(rec_info.get_name(), to_list(rec_lvls));
for (optional<expr> const & p : params) {
if (p) {
rec = mk_app(rec, *p);
} else {
rec = mk_app(rec, mk_type_class_param(g, rec, rec_info));
}
}
expr motive = g_type;
if (rec_info.has_dep_elim())
motive = Fun(h, motive);
motive = Fun(indices, motive);
rec = mk_app(rec, motive);
buffer<expr> hyps;
g.get_hyps(hyps);
buffer<expr> new_hyps;
for (expr const & curr_h : hyps) {
if (mlocal_name(curr_h) != mlocal_name(h) &&
std::all_of(indices.begin(), indices.end(),
[&](expr const & idx) { return mlocal_name(curr_h) != mlocal_name(idx); })) {
new_hyps.push_back(curr_h);
}
}
expr rec_type = m_tc.whnf(m_tc.infer(rec, m_cs), m_cs);
unsigned curr_pos = params.size() + 1 /* motive */;
unsigned first_idx_pos = rec_info.get_first_index_pos();
bool consumed_major = false;
buffer<goal> new_goals;
list<bool> produce_motive = rec_info.get_produce_motive();
while (is_pi(rec_type) && curr_pos < rec_info.get_num_args()) {
if (first_idx_pos == curr_pos) {
for (expr const & idx : indices) {
rec = mk_app(rec, idx);
rec_type = m_tc.whnf(instantiate(binding_body(rec_type), idx), m_cs);
if (!is_pi(rec_type)) {
throw_ill_formed_recursor(rec_info);
}
curr_pos++;
}
rec = mk_app(rec, h);
rec_type = m_tc.whnf(instantiate(binding_body(rec_type), h), m_cs);
consumed_major = true;
curr_pos++;
} else {
if (!produce_motive)
throw_ill_formed_recursor(rec_info);
buffer<expr> new_goal_hyps;
new_goal_hyps.append(new_hyps);
expr new_type = binding_domain(rec_type);
expr rec_arg;
if (binding_info(rec_type).is_inst_implicit()) {
rec_arg = mk_type_class_param(g, binding_domain(rec_type));
} else {
unsigned arity = get_arity(new_type);
// introduce minor arguments
buffer<expr> minor_args;
for (unsigned i = 0; i < arity; i++) {
expr arg_type = head_beta_reduce(binding_domain(new_type));
name arg_name;
if (m_ids) {
arg_name = head(m_ids);
m_ids = tail(m_ids);
} else {
arg_name = binding_name(new_type);
}
expr new_h = mk_local(mk_fresh_name(), get_unused_name(arg_name, new_goal_hyps),
arg_type, binder_info());
minor_args.push_back(new_h);
new_goal_hyps.push_back(new_h);
new_type = instantiate(binding_body(new_type), new_h);
}
new_type = head_beta_reduce(new_type);
buffer<expr> new_deps;
if (head(produce_motive)) {
// introduce deps
for (unsigned i = 0; i < num_deps; i++) {
if (!is_pi(new_type)) {
throw_ill_formed_recursor(rec_info);
}
expr dep_type = binding_domain(new_type);
expr new_dep = mk_local(mk_fresh_name(),
get_unused_name(binding_name(new_type), new_goal_hyps),
dep_type, binder_info());
new_deps.push_back(new_dep);
new_goal_hyps.push_back(new_dep);
new_type = instantiate(binding_body(new_type), new_dep);
}
}
expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(new_goal_hyps, new_type)), new_goal_hyps);
goal new_g(new_meta, new_type);
new_goals.push_back(new_g);
rec_arg = Fun(minor_args, Fun(new_deps, new_meta));
}
produce_motive = tail(produce_motive);
rec = mk_app(rec, rec_arg);
rec_type = m_tc.whnf(instantiate(binding_body(rec_type), rec_arg), m_cs);
curr_pos++;
}
}
if (!consumed_major) {
throw_ill_formed_recursor(rec_info);
}
assign(g, rec);
return to_list(new_goals);
}
optional<goals> execute(goal const & g, expr const & h, expr const & h_type, name const & rec) {
try {
recursor_info rec_info = get_recursor_info(m_env, rec);
buffer<expr> h_type_args;
get_app_args(h_type, h_type_args);
buffer<optional<expr>> params;
for (optional<unsigned> const & pos : rec_info.get_params_pos()) {
if (!pos) {
params.push_back(none_expr());
} else if (*pos >= h_type_args.size()) {
throw tactic_exception("invalid 'induction' tactic, major premise type is ill-formed");
} else {
params.push_back(some_expr(h_type_args[*pos]));
}
}
buffer<expr> indices;
list<unsigned> const & idx_pos = rec_info.get_indices_pos();
for (unsigned pos : idx_pos) {
if (pos >= h_type_args.size()) {
throw tactic_exception("invalid 'induction' tactic, major premise type is ill-formed");
}
expr const & idx = h_type_args[pos];
if (!is_local(idx)) {
throw tactic_exception(sstream() << "invalid 'induction' tactic, argument #"
<< pos+1 << " of major premise '" << h << "' type is not a variable");
}
for (unsigned i = 0; i < h_type_args.size(); i++) {
if (i != pos && is_local(h_type_args[i]) && mlocal_name(h_type_args[i]) == mlocal_name(idx)) {
throw tactic_exception(sstream() << "invalid 'induction' tactic, argument #"
<< pos+1 << " of major premise '" << h << "' type is an index, "
<< "but it occurs more than once");
}
if (i < pos && depends_on(h_type_args[i], idx)) {
throw tactic_exception(sstream() << "invalid 'induction' tactic, argument #"
<< pos+1 << " of major premise '" << h << "' type is an index, "
<< "but it occurs in previous arguments");
}
if (i > pos && // occurs after idx
std::find(idx_pos.begin(), idx_pos.end(), i) != idx_pos.end() && // it is also an index
is_local(h_type_args[i]) && // if it is not an index, it will fail anyway.
depends_on(mlocal_type(idx), h_type_args[i])) {
throw tactic_exception(sstream() << "invalid 'induction' tactic, argument #"
<< pos+1 << " of major premise '" << h << "' type is an index, "
<< "but its type depends on the index at position #" << i+1);
}
}
indices.push_back(idx);
}
if (!rec_info.has_dep_elim() && depends_on(g.get_type(), h)) {
throw tactic_exception(sstream() << "invalid 'induction' tactic, recursor '" << rec
<< "' does not support dependent elimination, but conclusion "
<< "depends on major premise '" << h << "'");
}
buffer<expr> hyps, non_deps, deps;
g.get_hyps(hyps);
split_deps(hyps, h, indices, non_deps, deps);
buffer<expr> & new_hyps = non_deps;
new_hyps.push_back(h);
expr new_type = Pi(deps, g.get_type());
expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(new_hyps, new_type)), new_hyps);
goal new_g(new_meta, new_type);
expr val = mk_app(new_meta, deps);
assign(g, val);
return optional<goals>(apply_recursor(new_g, deps.size(), h, h_type, params, indices, rec_info));
} catch (exception const & ex) {
throw tactic_exception(sstream() << "invalid 'induction' tactic, " << ex.what());
}
}
public:
induction_tac(environment const & env, io_state const & ios,
old_type_checker & tc, substitution const & subst, name const & h_name,
optional<name> const & rec_name, list<name> const & ids,
bool throw_ex, expr const & ref):
m_env(env), m_ios(ios), m_tc(tc), m_h_name(h_name), m_rec_name(rec_name), m_ids(ids),
m_subst(subst), m_throw_ex(throw_ex), m_ref(ref) {
m_standard = is_standard(env);
}
substitution const & get_subst() const { return m_subst; }
constraint_seq get_new_constraints() const { return m_cs; }
expr normalize_H_type(expr const & H) {
lean_assert(is_local(H));
expr H_type = m_subst.instantiate_all(mlocal_type(H));
if (m_rec_name) {
recursor_info info = get_recursor_info(m_env, *m_rec_name);
name tname = info.get_type_name();
old_type_checker_ptr aux_tc = mk_type_checker(m_env, [=](name const & n) { return n == tname; });
return aux_tc->whnf(H_type).first;
} else {
has_recursors_pred pred(m_env);
old_type_checker_ptr aux_tc = mk_type_checker(m_env, pred);
return aux_tc->whnf(H_type).first;
}
}
optional<goals> execute(goal const & g) {
try {
auto p = g.find_hyp(m_h_name);
if (!p)
throw tactic_exception(sstream() << "invalid 'induction' tactic, unknown hypothesis '" << m_h_name << "'");
expr H = p->first;
expr H_type = normalize_H_type(H);
expr I = get_app_fn(H_type);
if (is_constant(I)) {
if (m_rec_name) {
return execute(g, H, H_type, *m_rec_name);
} else if (inductive::is_inductive_decl(m_env, const_name(I))) {
return execute(g, H, H_type, inductive::get_elim_name(const_name(I)));
} else if (list<name> rs = get_recursors_for(m_env, const_name(I))) {
while (rs) {
name r = head(rs);
rs = tail(rs);
if (!rs) {
// last one
return execute(g, H, H_type, r);
} else {
list<name> saved_ids = m_ids;
constraint_seq saved_cs = m_cs;
substitution saved_subst = m_subst;
try {
return execute(g, H, H_type, r);
} catch (exception &) {
m_ids = saved_ids;
m_cs = saved_cs;
m_subst = saved_subst;
}
}
}
}
}
throw tactic_exception(sstream() << "invalid 'induction' tactic, hypothesis '" << m_h_name
<< "' must have a type that is associated with a recursor");
} catch (tactic_exception & ex) {
if (m_throw_ex)
throw;
return optional<goals>();
} catch (exception & ex) {
if (m_throw_ex)
throw tactic_exception(sstream() << "invalid 'induction' tactic, " << ex.what());
return optional<goals>();
}
}
};
tactic induction_tactic(name const & H, optional<name> rec, list<name> const & ids, expr const & ref) {
auto fn = [=](environment const & env, io_state const & ios, proof_state const & ps) -> optional<proof_state> {
goals const & gs = ps.get_goals();
if (empty(gs)) {
throw_no_goal_if_enabled(ps);
return none_proof_state();
}
goal g = head(gs);
goals tail_gs = tail(gs);
std::unique_ptr<old_type_checker> tc = mk_type_checker(env);
induction_tac tac(env, ios, *tc, ps.get_subst(), H, rec, ids, ps.report_failure(), ref);
if (auto res = tac.execute(g)) {
proof_state new_s(ps, append(*res, tail_gs), tac.get_subst());
if (solve_constraints(env, ios, new_s, tac.get_new_constraints()))
return some_proof_state(new_s);
else
return none_proof_state();
} else {
return none_proof_state();
}
};
return tactic01(fn);
}
tactic induction_tactic(elaborate_fn const & elab, expr const & H, optional<name> rec, list<name> const & ids, expr const & ref) {
auto fn = [=](environment const & env, io_state const & ios, proof_state const & ps) {
name Haux{"H", "ind"};
auto new_ps = generalize_core(env, ios, elab, H, Haux, ps, "induction", true);
if (!new_ps)
return proof_state_seq();
goal g = head(new_ps->get_goals());
expr new_H = app_arg(g.get_meta());
lean_assert(is_local(new_H));
name H_name = local_pp_name(new_H);
return induction_tactic(H_name, rec, ids, ref)(env, ios, *new_ps);
};
return tactic(fn);
}
void initialize_induction_tactic() {
register_tac(name{"tactic", "induction"},
[](old_type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
buffer<expr> args;
get_app_args(e, args);
if (args.size() != 3)
throw expr_to_tactic_exception(e, "invalid 'induction' tactic, insufficient number of arguments");
check_tactic_expr(args[0], "invalid 'induction' tactic, argument must be an expression");
expr H = get_tactic_expr_expr(args[0]);
buffer<name> ids;
get_tactic_id_list_elements(args[2], ids, "invalid 'induction' tactic, list of identifiers expected");
check_tactic_expr(args[1], "invalid 'induction' tactic, invalid argument");
expr rec = get_tactic_expr_expr(args[1]);
if (!is_constant(rec)) {
throw expr_to_tactic_exception(args[1], "invalid 'induction' tactic, constant expected");
}
name const & cname = const_name(rec);
if (cname == get_tactic_none_expr_name()) {
if (is_local(H))
return induction_tactic(local_pp_name(H), optional<name>(), to_list(ids.begin(), ids.end()), e);
else
return induction_tactic(elab, H, optional<name>(), to_list(ids.begin(), ids.end()), e);
} else {
if (is_local(H))
return induction_tactic(local_pp_name(H), optional<name>(cname), to_list(ids.begin(), ids.end()), e);
else
return induction_tactic(elab, H, optional<name>(), to_list(ids.begin(), ids.end()), e);
}
});
}
void finalize_induction_tactic() {
}
}

11
src/library/old_tactic/tactic/induction_tactic.h
View file

@ -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_induction_tactic();
void finalize_induction_tactic();
}