michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(library/tactic/rewrite_tactic): modify param name

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-05 10:04:03 -08:00
parent 0abfa30ead
commit 941b493835
1 changed files with 22 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

44
src/library/tactic/rewrite_tactic.cpp
View file

@ -499,9 +499,9 @@ class rewrite_fn {
// When successful, the result is the pair (H, new_t) where // When successful, the result is the pair (H, new_t) where
// (H : new_t = t) if is_goal == true // (H : new_t = t) if is_goal == true
// (H : t = new_t) if is_goal == false // (H : t = new_t) if is_goal == false
unify_result unify_target(expr const & t, expr const & pre_elem, bool is_goal) { unify_result unify_target(expr const & t, expr const & orig_elem, bool is_goal) {
try { try {
expr rule = get_rewrite_rule(pre_elem); expr rule = get_rewrite_rule(orig_elem);
auto rcs = m_elab(m_g, m_ngen.mk_child(), rule, false); auto rcs = m_elab(m_g, m_ngen.mk_child(), rule, false);
rule = rcs.first; rule = rcs.first;
buffer<constraint> cs; buffer<constraint> cs;
@ -521,7 +521,7 @@ class rewrite_fn {
rule = mk_app(rule, meta); rule = mk_app(rule, meta);
} }
lean_assert(is_eq(rule_type)); lean_assert(is_eq(rule_type));
bool symm = get_rewrite_info(pre_elem).symm(); bool symm = get_rewrite_info(orig_elem).symm();
expr src; expr src;
if (symm) if (symm)
src = app_arg(rule_type); src = app_arg(rule_type);
@ -569,13 +569,13 @@ class rewrite_fn {
typedef optional<std::tuple<expr, expr, expr>> find_result; typedef optional<std::tuple<expr, expr, expr>> find_result;
// Search for \c pattern in \c e. If \c t is a match, then try to unify the type of the rule // Search for \c pattern in \c e. If \c t is a match, then try to unify the type of the rule
// in the rewrite step \c pre_elem with \c t. // in the rewrite step \c orig_elem with \c t.
// When successful, this method returns the target \c t, the fully elaborated rule \c r, // When successful, this method returns the target \c t, the fully elaborated rule \c r,
// and the new value \c new_t (i.e., the expression that will replace \c t). // and the new value \c new_t (i.e., the expression that will replace \c t).
// //
// \remark is_goal == true if \c e is the type of a goal. Otherwise, it is assumed to be the type // \remark is_goal == true if \c e is the type of a goal. Otherwise, it is assumed to be the type
// of a hypothesis. This flag affects the equality proof built by this method. // of a hypothesis. This flag affects the equality proof built by this method.
find_result find_target(expr const & e, expr const & pattern, expr const & pre_elem, bool is_goal) { find_result find_target(expr const & e, expr const & pattern, expr const & orig_elem, bool is_goal) {
find_result result; find_result result;
for_each(e, [&](expr const & t, unsigned) { for_each(e, [&](expr const & t, unsigned) {
if (result) if (result)
@ -587,7 +587,7 @@ class rewrite_fn {
if (assigned) if (assigned)
reset_subst(); reset_subst();
if (r) { if (r) {
if (auto p = unify_target(t, pre_elem, is_goal)) { if (auto p = unify_target(t, orig_elem, is_goal)) {
result = std::make_tuple(t, p->second, p->first); result = std::make_tuple(t, p->second, p->first);
return false; return false;
} }
@ -598,10 +598,10 @@ class rewrite_fn {
return result; return result;
} }
bool process_rewrite_hypothesis(expr const & hyp, expr const & pre_elem, expr const & pattern, occurrence const & occ) { bool process_rewrite_hypothesis(expr const & hyp, expr const & orig_elem, expr const & pattern, occurrence const & occ) {
expr Pa = mlocal_type(hyp); expr Pa = mlocal_type(hyp);
bool is_goal = false; bool is_goal = false;
if (auto it = find_target(Pa, pattern, pre_elem, is_goal)) { if (auto it = find_target(Pa, pattern, orig_elem, is_goal)) {
expr a, Heq, b; // Heq is a proof of a = b expr a, Heq, b; // Heq is a proof of a = b
std::tie(a, b, Heq) = *it; std::tie(a, b, Heq) = *it;
@ -647,10 +647,10 @@ class rewrite_fn {
return false; return false;
} }
bool process_rewrite_goal(expr const & pre_elem, expr const & pattern, occurrence const & occ) { bool process_rewrite_goal(expr const & orig_elem, expr const & pattern, occurrence const & occ) {
expr Pa = m_g.get_type(); expr Pa = m_g.get_type();
bool is_goal = true; bool is_goal = true;
if (auto it = find_target(Pa, pattern, pre_elem, is_goal)) { if (auto it = find_target(Pa, pattern, orig_elem, is_goal)) {
expr a, Heq, b; expr a, Heq, b;
std::tie(a, b, Heq) = *it; std::tie(a, b, Heq) = *it;
@ -684,12 +684,12 @@ class rewrite_fn {
return false; return false;
} }
bool process_rewrite_single_step(expr const & pre_elem, expr const & pattern) { bool process_rewrite_single_step(expr const & orig_elem, expr const & pattern) {
check_system("rewrite tactic"); check_system("rewrite tactic");
rewrite_info const & info = get_rewrite_info(pre_elem); rewrite_info const & info = get_rewrite_info(orig_elem);
location const & loc = info.get_location(); location const & loc = info.get_location();
if (loc.is_goal_only()) if (loc.is_goal_only())
return process_rewrite_goal(pre_elem, pattern, *loc.includes_goal()); return process_rewrite_goal(orig_elem, pattern, *loc.includes_goal());
bool progress = false; bool progress = false;
buffer<expr> hyps; buffer<expr> hyps;
m_g.get_hyps(hyps); m_g.get_hyps(hyps);
@ -697,11 +697,11 @@ class rewrite_fn {
auto occ = loc.includes_hypothesis(local_pp_name(h)); auto occ = loc.includes_hypothesis(local_pp_name(h));
if (!occ) if (!occ)
continue; continue;
if (process_rewrite_hypothesis(h, pre_elem, pattern, *occ)) if (process_rewrite_hypothesis(h, orig_elem, pattern, *occ))
progress = true; progress = true;
} }
if (auto occ = loc.includes_goal()) { if (auto occ = loc.includes_goal()) {
if (process_rewrite_goal(pre_elem, pattern, *occ)) if (process_rewrite_goal(orig_elem, pattern, *occ))
progress = true; progress = true;
} }
return progress; return progress;
@ -712,7 +712,7 @@ class rewrite_fn {
throw_max_iter_exceeded(); throw_max_iter_exceeded();
} }
bool process_rewrite_step(expr const & elem, expr const & pre_elem) { bool process_rewrite_step(expr const & elem, expr const & orig_elem) {
lean_assert(is_rewrite_step(elem)); lean_assert(is_rewrite_step(elem));
expr pattern = get_pattern(elem); expr pattern = get_pattern(elem);
// regular(m_env, m_ios) << "pattern: " << pattern << "\n"; // regular(m_env, m_ios) << "pattern: " << pattern << "\n";
@ -720,11 +720,11 @@ class rewrite_fn {
unsigned i, num; unsigned i, num;
switch (info.get_multiplicity()) { switch (info.get_multiplicity()) {
case rewrite_info::Once: case rewrite_info::Once:
return process_rewrite_single_step(pre_elem, pattern); return process_rewrite_single_step(orig_elem, pattern);
case rewrite_info::AtMostN: case rewrite_info::AtMostN:
num = info.num(); num = info.num();
for (i = 0; i < std::min(num, m_max_iter); i++) { for (i = 0; i < std::min(num, m_max_iter); i++) {
if (!process_rewrite_single_step(pre_elem, pattern)) if (!process_rewrite_single_step(orig_elem, pattern))
return true; return true;
} }
check_max_iter(i); check_max_iter(i);
@ -732,22 +732,22 @@ class rewrite_fn {
case rewrite_info::ExactlyN: case rewrite_info::ExactlyN:
num = info.num(); num = info.num();
for (i = 0; i < std::min(num, m_max_iter); i++) { for (i = 0; i < std::min(num, m_max_iter); i++) {
if (!process_rewrite_single_step(pre_elem, pattern)) if (!process_rewrite_single_step(orig_elem, pattern))
return false; return false;
} }
check_max_iter(i); check_max_iter(i);
return true; return true;
case rewrite_info::ZeroOrMore: case rewrite_info::ZeroOrMore:
for (i = 0; i < m_max_iter; i++) { for (i = 0; i < m_max_iter; i++) {
if (!process_rewrite_single_step(pre_elem, pattern)) if (!process_rewrite_single_step(orig_elem, pattern))
return true; return true;
} }
throw_max_iter_exceeded(); throw_max_iter_exceeded();
case rewrite_info::OneOrMore: case rewrite_info::OneOrMore:
if (!process_rewrite_single_step(pre_elem, pattern)) if (!process_rewrite_single_step(orig_elem, pattern))
return false; return false;
for (i = 0; i < m_max_iter; i++) { for (i = 0; i < m_max_iter; i++) {
if (!process_rewrite_single_step(pre_elem, pattern)) if (!process_rewrite_single_step(orig_elem, pattern))
return true; return true;
} }
throw_max_iter_exceeded(); throw_max_iter_exceeded();