chore(library/old_tactic/tactic): remove dead code
This commit is contained in:
Leonardo de Moura
parent
a30603405c
commit
e945db8306
10 changed files with 0 additions and 1107 deletions
|
|
@ -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<constraint> 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<proof_state>(rseq, [=](pair<substitution, constraints> 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() {
|
||||
}
|
||||
}
|
||||
|
|
@ -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();
|
||||
}
|
||||
|
|
@ -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 <algorithm>
|
||||
#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<expr> mk_congr_subsingleton_thm(old_type_checker & tc, io_state const & ios, expr const & fn, optional<unsigned> const & expected_num_args,
|
||||
buffer<congr_arg_kind> & arg_kinds, constraint_seq & cs) {
|
||||
expr fn_type = tc.infer(fn, cs);
|
||||
buffer<expr> hyps;
|
||||
collected_locals ctx_buffer;
|
||||
collect_locals(fn_type, ctx_buffer);
|
||||
collect_locals(fn, ctx_buffer);
|
||||
hyps.append(ctx_buffer.get_collected());
|
||||
list<expr> ctx = to_list(hyps);
|
||||
|
||||
buffer<expr> domain;
|
||||
expr codomain = to_telescope(tc, fn_type, domain, optional<binder_info>(), 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<bool> prop; // pp[i] iff i-th arg is a proposition
|
||||
buffer<bool> ss; // ss[i] is not none iff i-th arg is a subsingleton
|
||||
buffer<bool> 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<bool>(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<expr> new_domain;
|
||||
buffer<expr> 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<expr> lhss, rhss;
|
||||
buffer<optional<expr>> eqs;
|
||||
buffer<bool> ss_elim; // true if equality proof should be synthesized using singletion elimination
|
||||
buffer<expr> 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<expr> 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<expr> 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<expr> 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<proof_state> {
|
||||
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<expr> 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<goal> new_goals;
|
||||
optional<expr> 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<congr_arg_kind> 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() {}
|
||||
}
|
||||
|
|
@ -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<expr> mk_congr_subsingleton_thm(type_checker & tc, io_state const & ios,
|
||||
expr const & fn, optional<unsigned> const & expected_num_args,
|
||||
buffer<congr_arg_kind> & arg_kinds, constraint_seq & cs);
|
||||
void initialize_congruence_tactic();
|
||||
void finalize_congruence_tactic();
|
||||
}
|
||||
|
|
@ -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 <unordered_map>
|
||||
#include <string>
|
||||
#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<name, expr_to_tactic_fn, name_hash, name_eq> 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<expr> 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<name> const & args) {
|
||||
buffer<expr> 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<expr> & 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<name> & r, char const * error_msg) {
|
||||
buffer<expr> 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<declaration> 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<expr> 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<level> 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<mpz> 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<expr> 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<unsigned> 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<unsigned>(get_unsigned(tc, app_arg(e), e));
|
||||
} else if (const_name(get_app_fn(e)) == get_option_none_name()) {
|
||||
return optional<unsigned>();
|
||||
}
|
||||
}
|
||||
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<old_converter>(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<tactic()> 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<tactic(tactic const &, tactic const &)> f) {
|
||||
register_tac(n, [=](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
|
||||
buffer<expr> 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<tactic(tactic const &)> f) {
|
||||
register_tac(n, [=](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
|
||||
buffer<expr> 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<tactic(tactic const &, unsigned k)> f) {
|
||||
register_tac(n, [=](old_type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) {
|
||||
buffer<expr> 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<tactic(unsigned k)> f) {
|
||||
register_tac(n, [=](old_type_checker & tc, elaborate_fn const &, expr const & e, pos_info_provider const *) {
|
||||
buffer<expr> 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;
|
||||
}
|
||||
}
|
||||
|
|
@ -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<unsigned> 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<expr> & r, char const * error_msg);
|
||||
void get_tactic_id_list_elements(expr l, buffer<name> & r, char const * error_msg);
|
||||
expr ids_to_tactic_expr(buffer<name> 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<tactic(old_type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *)>
|
||||
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<tactic()> f);
|
||||
void register_bin_tac(name const & n, std::function<tactic(tactic const &, tactic const &)> f);
|
||||
void register_unary_tac(name const & n, std::function<tactic(tactic const &)> f);
|
||||
void register_unary_num_tac(name const & n, std::function<tactic(tactic const &, unsigned)> f);
|
||||
void register_num_tac(name const & n, std::function<tactic(unsigned k)> f);
|
||||
|
||||
void initialize_expr_to_tactic();
|
||||
void finalize_expr_to_tactic();
|
||||
}
|
||||
|
|
@ -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 <string>
|
||||
#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<unsigned, unsigned> 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<output_channel> out(std::make_shared<string_output_channel>());
|
||||
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<expr> 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() {
|
||||
}
|
||||
}
|
||||
|
|
@ -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 <string>
|
||||
#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<unsigned, unsigned> 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();
|
||||
}
|
||||
|
|
@ -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;
|
||||
}
|
||||
}
|
||||
|
|
@ -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);
|
||||
}
|
||||
Loading…
Add table
Reference in a new issue