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

refactor(library/blast): we don't require maximally shared terms anymore in blast

Browse source 
This commit also removes the blast::mk_* expr and level functions.
They were just noops.

I kept only mk_uref, mk_href and mk_mref
This commit is contained in:
Leonardo de Moura 2015-11-05 16:18:49 -08:00
parent 45c02cb65c
commit 8d9d84f33c
7 changed files with 28 additions and 272 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
src/library/blast/blast.cpp
View file

@ -109,7 +109,7 @@ class blastenv {
}
} else if (is_local(e) && !is_tmp_local(e)) {
if (std::all_of(locals.begin(), locals.end(), [&](expr const & a) {
return local_index(a) != local_index(e); })) {
return mlocal_name(a) != mlocal_name(e); })) {
ok = false; // failed 3
return false;
}
@ -183,16 +183,16 @@ class blastenv {
level to_blast_level(level const & l) {
level lhs;
switch (l.kind()) {
case level_kind::Succ: return blast::mk_succ(to_blast_level(succ_of(l)));
case level_kind::Zero: return blast::mk_level_zero();
case level_kind::Param: return blast::mk_param_univ(param_id(l));
case level_kind::Global: return blast::mk_global_univ(global_id(l));
case level_kind::Succ: return mk_succ(to_blast_level(succ_of(l)));
case level_kind::Zero: return mk_level_zero();
case level_kind::Param: return mk_param_univ(param_id(l));
case level_kind::Global: return mk_global_univ(global_id(l));
case level_kind::Max:
lhs = to_blast_level(max_lhs(l));
return blast::mk_max(lhs, to_blast_level(max_rhs(l)));
return mk_max(lhs, to_blast_level(max_rhs(l)));
case level_kind::IMax:
lhs = to_blast_level(imax_lhs(l));
return blast::mk_imax(lhs, to_blast_level(imax_rhs(l)));
return mk_imax(lhs, to_blast_level(imax_rhs(l)));
case level_kind::Meta:
if (auto r = m_uvar2uref.find(meta_id(l))) {
return *r;
@ -206,7 +206,7 @@ class blastenv {
}
virtual expr visit_sort(expr const & e) {
return blast::mk_sort(to_blast_level(sort_level(e)));
return mk_sort(to_blast_level(sort_level(e)));
}
virtual expr visit_macro(expr const & e) {
@ -214,16 +214,16 @@ class blastenv {
for (unsigned i = 0; i < macro_num_args(e); i++) {
new_args.push_back(visit(macro_arg(e, i)));
}
return blast::mk_macro(macro_def(e), new_args.size(), new_args.data());
return mk_macro(macro_def(e), new_args.size(), new_args.data());
}
virtual expr visit_constant(expr const & e) {
levels new_ls = map(const_levels(e), [&](level const & l) { return to_blast_level(l); });
return blast::mk_constant(const_name(e), new_ls);
return mk_constant(const_name(e), new_ls);
}
virtual expr visit_var(expr const & e) {
return blast::mk_var(var_idx(e));
return mk_var(var_idx(e));
}
void throw_unsupported_metavar_occ(expr const & e) {
@ -238,7 +238,7 @@ class blastenv {
for (unsigned i = 0; i < nargs; i++) {
new_args.push_back(visit(args[i]));
}
return blast::mk_app(mref, new_args.size(), new_args.data());
return mk_app(mref, new_args.size(), new_args.data());
}
expr visit_meta_app(expr const & e) {
@ -316,18 +316,18 @@ class blastenv {
return visit_meta_app(e);
} else {
expr f = visit(app_fn(e));
return blast::mk_app(f, visit(app_arg(e)));
return mk_app(f, visit(app_arg(e)));
}
}
virtual expr visit_lambda(expr const & e) {
expr d = visit(binding_domain(e));
return blast::mk_lambda(binding_name(e), d, visit(binding_body(e)), binding_info(e));
return mk_lambda(binding_name(e), d, visit(binding_body(e)), binding_info(e));
}
virtual expr visit_pi(expr const & e) {
expr d = visit(binding_domain(e));
return blast::mk_pi(binding_name(e), d, visit(binding_body(e)), binding_info(e));
return mk_pi(binding_name(e), d, visit(binding_body(e)), binding_info(e));
}
public:
@ -406,10 +406,8 @@ public:
return m_projection_info.find(n);
}
name mk_fresh_local_name() { return m_ngen.next(); }
expr mk_fresh_local(expr const & type, binder_info const & bi) {
name n = m_ngen.next();
return blast::mk_local(n, n, type, bi);
return m_tmp_local_generator.mk_tmp_local(type, bi);
}
expr whnf(expr const & e) { return m_tctx.whnf(e); }
expr infer_type(expr const & e) { return m_tctx.infer(e); }
@ -493,11 +491,6 @@ optional<expr> mk_class_instance(expr const & e) {
return g_blastenv->mk_class_instance(e);
}
name mk_fresh_local_name() {
lean_assert(g_blastenv);
return g_blastenv->mk_fresh_local_name();
}
expr mk_fresh_local(expr const & type, binder_info const & bi) {
lean_assert(g_blastenv);
return g_blastenv->mk_fresh_local(type, bi);

3
src/library/blast/blast.h
View file

@ -22,8 +22,7 @@ environment const & env();
io_state const & ios();
/** \brief Return the thread local current state begin processed by the blast tactic. */
state & curr_state();
/** \brief Return a thread local fresh name meant to be used to name local constants. */
name mk_fresh_local_name();
/** \brief Return a thread local fresh local constant. */
expr mk_fresh_local(expr const & type, binder_info const & bi = binder_info());
/** \brief Return true iff the given constant name is marked as reducible in env() */
bool is_reducible(name const & n);

2
src/library/blast/branch.cpp
View file

@ -69,7 +69,7 @@ void branch::add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user) {
void branch::add_deps(hypothesis & h_user, unsigned hidx_user) {
add_deps(h_user.m_type, h_user, hidx_user);
if (!blast::is_local(h_user.m_value)) {
if (!is_local_non_href(h_user.m_value)) {
add_deps(h_user.m_value, h_user, hidx_user);
}
}

190
src/library/blast/expr.cpp
View file

@ -23,62 +23,24 @@ static name * g_prefix = nullptr;
static expr * g_dummy_type = nullptr; // dummy type for href/mref
typedef typename std::vector<expr> expr_array;
LEAN_THREAD_PTR(expr_array, g_var_array);
LEAN_THREAD_PTR(expr_array, g_mref_array);
LEAN_THREAD_PTR(expr_array, g_href_array);
scope_hash_consing::scope_hash_consing():
scoped_expr_caching(true) {
lean_assert(g_var_array == nullptr);
lean_assert(g_mref_array == nullptr);
lean_assert(g_href_array == nullptr);
g_var_array = new expr_array();
g_mref_array = new expr_array();
g_href_array = new expr_array();
}
scope_hash_consing::~scope_hash_consing() {
delete g_var_array;
delete g_mref_array;
delete g_href_array;
g_var_array = nullptr;
g_mref_array = nullptr;
g_href_array = nullptr;
}
level mk_level_zero() {
return lean::mk_level_zero();
}
level mk_level_one() {
return lean::mk_level_one();
}
level mk_max(level const & l1, level const & l2) {
lean_assert(is_cached(l1));
lean_assert(is_cached(l2));
return lean::mk_max(l1, l2);
}
level mk_imax(level const & l1, level const & l2) {
lean_assert(is_cached(l1));
lean_assert(is_cached(l2));
return lean::mk_max(l1, l2);
}
level mk_succ(level const & l) {
lean_assert(is_cached(l));
return lean::mk_succ(l);
}
level mk_param_univ(name const & n) {
return lean::mk_param_univ(n);
}
level mk_global_univ(name const & n) {
return lean::mk_global_univ(n);
}
level mk_uref(unsigned idx) {
return lean::mk_meta_univ(name(*g_prefix, idx));
}
@ -92,27 +54,6 @@ unsigned uref_index(level const & l) {
return meta_id(l).get_numeral();
}
level update_succ(level const & l, level const & new_arg) {
if (is_eqp(succ_of(l), new_arg))
return l;
else
return blast::mk_succ(new_arg);
}
level update_max(level const & l, level const & new_lhs, level const & new_rhs) {
if (is_max(l)) {
if (is_eqp(max_lhs(l), new_lhs) && is_eqp(max_rhs(l), new_rhs))
return l;
else
return blast::mk_max(new_lhs, new_rhs);
} else {
if (is_eqp(imax_lhs(l), new_lhs) && is_eqp(imax_rhs(l), new_rhs))
return l;
else
return blast::mk_imax(new_lhs, new_rhs);
}
}
static expr mk_href_core(unsigned idx) {
return lean::mk_local(name(*g_prefix, idx), *g_dummy_type);
}
@ -169,137 +110,6 @@ bool has_mref(expr const & e) {
return lean::has_expr_metavar(e);
}
expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi) {
lean_assert(is_cached(t));
return lean::mk_local(n, pp_n, t, bi);
}
bool is_local(expr const & e) {
return lean::is_local(e) && mlocal_type(e) != *g_dummy_type;
}
bool has_local(expr const & e) {
return lean::has_local(e);
}
unsigned local_index(expr const & e) {
lean_assert(blast::is_local(e));
return mlocal_name(e).get_numeral();
}
expr const & local_type(expr const & e) {
lean_assert(blast::is_local(e));
return mlocal_type(e);
}
expr mk_var(unsigned idx) {
lean_assert(g_var_array);
while (g_var_array->size() <= idx) {
unsigned j = g_var_array->size();
expr new_var = lean::mk_var(j);
g_var_array->push_back(new_var);
}
lean_assert(idx < g_var_array->size());
return (*g_var_array)[idx];
}
expr mk_app(expr const & f, expr const & a) {
lean_assert(is_cached(f) && is_cached(a));
return lean::mk_app(f, a);
}
bool is_cached(unsigned num, expr const * args) {
return std::all_of(args, args+num, [](expr const & e) { return is_cached(e); });
}
expr mk_app(expr const & f, unsigned num_args, expr const * args) {
lean_assert(is_cached(f) && is_cached(num_args, args));
return lean::mk_app(f, num_args, args);
}
expr mk_app(unsigned num_args, expr const * args) {
lean_assert(num_args >= 2);
return blast::mk_app(blast::mk_app(args[0], args[1]), num_args - 2, args+2);
}
expr mk_rev_app(expr const & f, unsigned num_args, expr const * args) {
lean_assert(is_cached(f) && is_cached(num_args, args));
return lean::mk_rev_app(f, num_args, args);
}
expr mk_rev_app(unsigned num_args, expr const * args) {
lean_assert(num_args >= 2);
return blast::mk_rev_app(blast::mk_app(args[num_args-1], args[num_args-2]), num_args-2, args);
}
expr mk_sort(level const & l) {
lean_assert(is_cached(l));
return lean::mk_sort(l);
}
expr mk_constant(name const & n, levels const & ls) {
lean_assert(std::all_of(ls.begin(), ls.end(), [](level const & l) { return is_cached(l); }));
return lean::mk_constant(n, ls);
}
expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & bi) {
lean_assert(is_cached(t) && is_cached(e));
return lean::mk_binding(k, n, t, e, bi);
}
expr mk_macro(macro_definition const & m, unsigned num, expr const * args) {
lean_assert(is_cached(num, args));
return lean::mk_macro(m, num, args);
}
expr update_app(expr const & e, expr const & new_fn, expr const & new_arg) {
if (!is_eqp(app_fn(e), new_fn) || !is_eqp(app_arg(e), new_arg))
return blast::mk_app(new_fn, new_arg);
else
return e;
}
expr update_binding(expr const & e, expr const & new_domain, expr const & new_body) {
if (!is_eqp(binding_domain(e), new_domain) || !is_eqp(binding_body(e), new_body))
return blast::mk_binding(e.kind(), binding_name(e), new_domain, new_body, binding_info(e));
else
return e;
}
expr update_sort(expr const & e, level const & new_level) {
if (!is_eqp(sort_level(e), new_level))
return blast::mk_sort(new_level);
else
return e;
}
expr update_constant(expr const & e, levels const & new_levels) {
if (!is_eqp(const_levels(e), new_levels))
return blast::mk_constant(const_name(e), new_levels);
else
return e;
}
expr update_local(expr const & e, expr const & new_type) {
if (!is_eqp(mlocal_type(e), new_type))
return blast::mk_local(mlocal_name(e), local_pp_name(e), new_type, local_info(e));
else
return e;
}
expr update_macro(expr const & e, unsigned num, expr const * args) {
if (num == macro_num_args(e)) {
unsigned i = 0;
for (i = 0; i < num; i++) {
if (!is_eqp(macro_arg(e, i), args[i]))
break;
}
if (i == num)
return e;
}
return blast::mk_macro(to_macro(e)->get_def(), num, args);
}
void initialize_expr() {
g_prefix = new name(name::mk_internal_unique_name());
g_dummy_type = new expr(mk_constant(*g_prefix));

51
src/library/blast/expr.h
View file

@ -26,48 +26,15 @@ public:
~scope_hash_consing();
};
level mk_level_zero();
level mk_level_one();
level mk_max(level const & l1, level const & l2);
level mk_imax(level const & l1, level const & l2);
level mk_succ(level const & l);
level mk_param_univ(name const & n);
level mk_global_univ(name const & n);
level mk_uref(unsigned idx);
bool is_uref(level const & l);
unsigned uref_index(level const & l);
expr mk_var(unsigned idx);
// mk_href and mk_mref are helper functions for creating hypotheses and meta-variables used in the blast tactic.
// Remark: the local constants and metavariables manipulated by the blast tactic do **not** store their types.
expr mk_href(unsigned idx);
expr mk_mref(unsigned idx);
expr mk_sort(level const & l);
expr mk_constant(name const & n, levels const & ls);
expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi);
expr mk_app(expr const & f, expr const & a);
expr mk_app(expr const & f, unsigned num_args, expr const * args);
expr mk_app(unsigned num_args, expr const * args);
expr mk_rev_app(expr const & f, unsigned num_args, expr const * args);
expr mk_rev_app(unsigned num_args, expr const * args);
expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & bi);
inline expr mk_pi(name const & n, expr const & t, expr const & e, binder_info const & bi) {
return blast::mk_binding(expr_kind::Pi, n, t, e, bi);
}
inline expr mk_lambda(name const & n, expr const & t, expr const & e, binder_info const & bi) {
return blast::mk_binding(expr_kind::Lambda, n, t, e, bi);
}
inline expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e) {
return blast::mk_binding(k, n, t, e, binder_info());
}
inline expr mk_pi(name const & n, expr const & t, expr const & e) {
return blast::mk_pi(n, t, e, binder_info());
}
inline expr mk_lambda(name const & n, expr const & t, expr const & e) {
return blast::mk_lambda(n, t, e, binder_info());
}
expr mk_macro(macro_definition const & m, unsigned num, expr const * args);
bool is_href(expr const & e);
unsigned href_index(expr const & e);
@ -78,21 +45,9 @@ bool has_href(expr const & e);
/** \brief Return true iff \c e contain mref's */
bool has_mref(expr const & e);
bool is_local(expr const & e);
unsigned local_index(expr const & e);
expr const & local_type(expr const & e);
bool has_local(expr const & e);
level update_succ(level const & l, level const & new_arg);
level update_max(level const & l, level const & new_lhs, level const & new_rhs);
expr update_app(expr const & e, expr const & new_fn, expr const & new_arg);
expr update_metavar(expr const & e, expr const & new_type);
expr update_binding(expr const & e, expr const & new_domain, expr const & new_body);
expr update_sort(expr const & e, level const & new_level);
expr update_constant(expr const & e, levels const & new_levels);
expr update_local(expr const & e, expr const & new_type);
expr update_macro(expr const & e, unsigned num, expr const * args);
inline bool is_local_non_href(expr const & e) {
return is_local(e) && !is_href(e);
}
void initialize_expr();
void finalize_expr();

2
src/library/blast/hypothesis.h
View file

@ -40,6 +40,6 @@ public:
expr const & get_value() const { return m_value; }
/** \brief Return true iff this hypothesis depends on \c h. */
bool depends_on(expr const & h) const { return m_deps.contains(href_index(h)); }
bool is_assumption() const { return blast::is_local(m_value); }
bool is_assumption() const { return is_local_non_href(m_value); }
};
}}

13
src/library/blast/state.cpp
View file

@ -233,19 +233,18 @@ struct instantiate_urefs_mrefs_fn : public replace_visitor {
}
virtual expr visit_sort(expr const & s) {
return blast::update_sort(s, visit_level(sort_level(s)));
return update_sort(s, visit_level(sort_level(s)));
}
virtual expr visit_constant(expr const & c) {
return blast::update_constant(c, visit_levels(const_levels(c)));
return update_constant(c, visit_levels(const_levels(c)));
}
virtual expr visit_local(expr const & e) {
if (blast::is_local(e)) {
return blast::update_local(e, visit(mlocal_type(e)));
} else {
lean_assert(is_href(e));
if (is_href(e)) {
return e;
} else {
return update_mlocal(e, visit(mlocal_type(e)));
}
}
@ -297,7 +296,7 @@ struct instantiate_urefs_mrefs_fn : public replace_visitor {
buffer<expr> new_args;
for (unsigned i = 0; i < macro_num_args(e); i++)
new_args.push_back(visit(macro_arg(e, i)));
return blast::update_macro(e, new_args.size(), new_args.data());
return update_macro(e, new_args.size(), new_args.data());
}
virtual expr visit(expr const & e) {