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

feat(library/tactic/subst_tactic): use substitutions instead of name_map<name> in the subst_tactic (low level) API

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-28 13:29:44 -07:00
parent f0f9880ece
commit 206bf613d5
4 changed files with 65 additions and 66 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

48
src/library/tactic/cases_tactic.cpp
View file

@ -21,43 +21,6 @@ Author: Leonardo de Moura
#include "library/tactic/subst_tactic.h"
namespace lean {
expr apply_substitutions(expr const & e, substitutions const & s) {
if (s.empty()) return e;
if (!has_local(e)) return e;
return replace(e, [&](expr const & e, unsigned) {
if (!has_local(e)) return some_expr(e);
if (is_local(e)) {
if (auto r = s.find(mlocal_name(e)))
return some_expr(*r);
}
return none_expr();
});
}
list<expr> apply_substitutions(list<expr> const & es, substitutions const & s) {
if (s.empty()) return es;
return map(es, [&](expr const & e) { return apply_substitutions(e, s); });
}
substitutions apply_substitutions(substitutions const & s1, substitutions const & s2) {
if (s2.empty()) return s1;
substitutions R;
s1.for_each([&](name const & x, expr const & e) {
R.insert(x, apply_substitutions(e, s2));
});
return R;
}
substitutions merge(substitutions const & s1, substitutions const & s2) {
if (s1.empty()) return s2;
if (s2.empty()) return s1;
substitutions R = s1;
s2.for_each([&](name const & x, expr const & e) {
R.insert(x, e);
});
return R;
}
struct cases_tactic_exception : public exception {
tactic_state m_state;
cases_tactic_exception(tactic_state const & s, char const * msg):exception(msg), m_state(s) {}
@ -410,17 +373,10 @@ struct cases_tactic_fn {
} else if (is_eq(H_type, A, lhs, rhs)) {
if (is_local(rhs) || is_local(lhs)) {
lean_cases_trace(mvar, tout() << "substitute\n";);
name_map<name> extra_renames;
substitutions extra_substs;
bool symm = !is_local(lhs) && is_local(rhs);
expr mvar2 = subst(m_env, m_opts, m_mode, m_mctx, *mvar1, H, symm,
updating ? &extra_renames : nullptr);
substitutions extra_substs = to_substitutions(mvar2, extra_renames);
if (updating) {
if (symm)
extra_substs.insert(mlocal_name(rhs), apply_substitutions(lhs, extra_substs));
else
extra_substs.insert(mlocal_name(lhs), apply_substitutions(rhs, extra_substs));
}
updating ? &extra_substs : nullptr);
new_intros = apply_substitutions(new_intros, extra_substs);
substs = merge(apply_substitutions(substs, extra_substs), extra_substs);
return unify_eqs(mvar2, num_eqs - 1, updating, new_intros, substs);

13
src/library/tactic/cases_tactic.h
View file

@ -6,23 +6,12 @@ Author: Leonardo de Moura
*/
#pragma once
#include "library/tactic/induction_tactic.h"
#include "library/tactic/subst_tactic.h"
namespace lean {
typedef list<list<expr>> xintros_list;
typedef name_map<expr> substitutions;
typedef list<substitutions> substitutions_list;
/* \brief Given `e`, for each (x := v) in `s` replace `x` with `v` in `e` */
expr apply_substitutions(expr const & e, substitutions const & s);
list<expr> apply_substitutions(list<expr> const & es, substitutions const & s);
/* \brief Return a new set of substitutions containing (x := apply_substitutions(v, s2)) for
each (x := v) in `s1`. */
substitutions apply_substitutions(substitutions const & s1, substitutions const & s2);
/* \brief Return a new set of substitutions containing the entries of `s1` and `s2`. */
substitutions merge(substitutions const & s1, substitutions const & s2);
/** \brief Similar to induction, but applies 'cases_on' and has bettern support for dependent types. Failures are reported using exceptions.
\c ids (if available) provides the names for new hypotheses.
If ilist and slist are not nullptr, then

51
src/library/tactic/subst_tactic.cpp
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <algorithm>
#include "kernel/replace_fn.h"
#include "kernel/abstract.h"
#include "kernel/instantiate.h"
#include "library/util.h"
@ -20,6 +21,43 @@ Author: Leonardo de Moura
#include "library/tactic/app_builder_tactics.h"
namespace lean {
expr apply_substitutions(expr const & e, substitutions const & s) {
if (s.empty()) return e;
if (!has_local(e)) return e;
return replace(e, [&](expr const & e, unsigned) {
if (!has_local(e)) return some_expr(e);
if (is_local(e)) {
if (auto r = s.find(mlocal_name(e)))
return some_expr(*r);
}
return none_expr();
});
}
list<expr> apply_substitutions(list<expr> const & es, substitutions const & s) {
if (s.empty()) return es;
return map(es, [&](expr const & e) { return apply_substitutions(e, s); });
}
substitutions apply_substitutions(substitutions const & s1, substitutions const & s2) {
if (s2.empty()) return s1;
substitutions R;
s1.for_each([&](name const & x, expr const & e) {
R.insert(x, apply_substitutions(e, s2));
});
return R;
}
substitutions merge(substitutions const & s1, substitutions const & s2) {
if (s1.empty()) return s2;
if (s2.empty()) return s1;
substitutions R = s1;
s2.for_each([&](name const & x, expr const & e) {
R.insert(x, e);
});
return R;
}
/* For debugging purposes, make sure H is in the local context for mvar */
bool check_hypothesis_in_context(metavar_context const & mctx, expr const & mvar, name const & H) {
local_context lctx = mctx.get_metavar_decl(mvar)->get_context();
@ -31,7 +69,7 @@ bool check_hypothesis_in_context(metavar_context const & mctx, expr const & mvar
}
expr subst(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx,
expr const & mvar, expr const & H, bool symm, name_map<name> * renames) {
expr const & mvar, expr const & H, bool symm, substitutions * substs) {
#define lean_subst_trace(CODE) lean_trace(name({"tactic", "subst"}), CODE)
#define lean_subst_trace_state(MVAR, MSG) lean_trace(name({"tactic", "subst"}), tactic_state S(env, opts, mctx, to_list(MVAR), MVAR); type_context TMP_CTX = mk_type_context_for(S, m); scope_trace_env _scope1(env, TMP_CTX); tout() << MSG << S.pp() << "\n";)
@ -43,6 +81,7 @@ expr subst(environment const & env, options const & opts, transparency_mode cons
expr lhs, rhs;
lean_verify(is_eq(H_type, lhs, rhs));
if (symm) std::swap(lhs, rhs);
expr init_lhs = lhs;
buffer<expr> to_revert;
to_revert.push_back(lhs);
to_revert.push_back(H);
@ -86,14 +125,16 @@ expr subst(environment const & env, options const & opts, transparency_mode cons
optional<expr> mvar6 = intron(env, opts, mctx, mvar5, to_revert.size() - 2, new_Hnames);
if (!mvar6) throw exception("subst tactic failed, unexpected failure when re-introducing dependencies");
lean_assert(new_Hnames.size() == to_revert.size() - 2);
if (renames) {
name_map<name> rmap;
if (substs) {
local_context lctx = mctx.get_metavar_decl(*mvar6)->get_context();
substitutions new_substs;
for (unsigned i = 0; i < to_revert.size() - 2; i++) {
lean_assert(check_hypothesis_in_context(mctx, mvar, mlocal_name(to_revert[i+2])));
lean_assert(check_hypothesis_in_context(mctx, *mvar6, new_Hnames[i]));
rmap.insert(mlocal_name(to_revert[i+2]), new_Hnames[i]);
new_substs.insert(mlocal_name(to_revert[i+2]), lctx.get_local_decl(new_Hnames[i])->mk_ref());
}
*renames = rmap;
new_substs.insert(mlocal_name(init_lhs), apply_substitutions(rhs, new_substs));
*substs = new_substs;
}
lean_subst_trace_state(*mvar6, "after intro remaining reverted hypotheses:\n");
return *mvar6;

19
src/library/tactic/subst_tactic.h
View file

@ -8,9 +8,22 @@ Author: Leonardo de Moura
#include "library/tactic/tactic_state.h"
namespace lean {
typedef name_map<expr> substitutions;
/* \brief Given `e`, for each (x := v) in `s` replace `x` with `v` in `e` */
expr apply_substitutions(expr const & e, substitutions const & s);
list<expr> apply_substitutions(list<expr> const & es, substitutions const & s);
/* \brief Return a new set of substitutions containing (x := apply_substitutions(v, s2)) for
each (x := v) in `s1`. */
substitutions apply_substitutions(substitutions const & s1, substitutions const & s2);
/* \brief Return a new set of substitutions containing the entries of `s1` and `s2`. */
substitutions merge(substitutions const & s1, substitutions const & s2);
/** \brief Given (H : lhs = rhs), replace lhs with rhs in the goal \c mvar. If symm == true, then replace rhs with lhs.
The replaced term must be a local constant. If renames is not nullptr, then hypotheses renamed by revert/intro
are stored in \c renames.
The replaced term must be a local constant. If substs is not nullptr, then hypotheses renamed by revert/intro
are stored in \c substs, and the actual substitution.
\pre is_metavar(mvar)
\pre is_local(H)
@ -19,7 +32,7 @@ namespace lean {
\pre symm == false ==> is_local(lhs(typeof(H)))
\pre symm == false ==> is_local(rhs(typeof(H))) */
expr subst(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx,
expr const & mvar, expr const & H, bool symm, name_map<name> * renames);
expr const & mvar, expr const & H, bool symm, substitutions * substs);
void initialize_subst_tactic();
void finalize_subst_tactic();