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

feat(library/blast): use new type_inference module in blast

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-30 17:45:27 -07:00
parent 52eb787288
commit fd917effad
7 changed files with 260 additions and 655 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/blast/CMakeLists.txt
View file

@ -1,2 +1,2 @@
add_library(blast OBJECT expr.cpp branch.cpp state.cpp infer_type.cpp blast.cpp
add_library(blast OBJECT expr.cpp branch.cpp state.cpp blast.cpp
blast_tactic.cpp init_module.cpp)

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

@ -4,18 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <vector>
#include "util/sstream.h"
#include "kernel/for_each_fn.h"
#include "kernel/type_checker.h"
#include "library/replace_visitor.h"
#include "library/util.h"
#include "library/reducible.h"
#include "library/normalize.h"
#include "library/class.h"
#include "library/type_inference.h"
#include "library/projection.h"
#include "library/tactic/goal.h"
#include "library/blast/expr.h"
#include "library/blast/state.h"
#include "library/blast/infer_type.h"
#include "library/blast/blast.h"
#include "library/blast/blast_context.h"
#include "library/blast/blast_exception.h"
namespace lean {
@ -23,16 +26,148 @@ namespace blast {
static name * g_prefix = nullptr;
class blastenv {
friend class scope;
environment m_env;
io_state m_ios;
name_generator m_ngen;
name_set m_lemma_hints;
name_set m_unfold_hints;
name_map<level> m_uvar2uref; // map global universe metavariables to blast uref's
name_map<pair<expr, expr>> m_mvar2meta_mref; // map global metavariables to blast mref's
name_predicate m_not_reducible_pred;
name_predicate m_class_pred;
name_predicate m_instance_pred;
name_map<projection_info> m_projection_info;
state m_curr_state; // current state
class ti : public type_inference {
blastenv & m_benv;
std::vector<state> m_stack;
public:
ti(blastenv & benv):
type_inference(benv.m_env, benv.m_ios),
m_benv(benv) {}
virtual bool is_extra_opaque(name const & n) const {
// TODO(Leo): class and instances
return m_benv.m_not_reducible_pred(n) || m_benv.m_projection_info.contains(n);
}
virtual expr mk_tmp_local(expr const & type, binder_info const & bi) {
name n = m_benv.m_ngen.next();
return blast::mk_local(n, n, type, bi);
}
virtual bool is_tmp_local(expr const & e) const {
return blast::is_local(e);
}
virtual bool is_uvar(level const & l) const {
return blast::is_uref(l);
}
virtual bool is_mvar(expr const & e) const {
return blast::is_mref(e);
}
virtual level const * get_assignment(level const & u) const {
return m_benv.m_curr_state.get_uref_assignment(u);
}
virtual expr const * get_assignment(expr const & m) const {
return m_benv.m_curr_state.get_mref_assignment(m);
}
virtual void update_assignment(level const & u, level const & v) {
m_benv.m_curr_state.assign_uref(u, v);
}
virtual void update_assignment(expr const & m, expr const & v) {
m_benv.m_curr_state.assign_mref(m, v);
}
virtual bool validate_assignment(expr const & m, buffer<expr> const & locals, expr const & v) {
// We must check
// 1. All href in new_v are in the context of m.
// 2. The context of any (unassigned) mref in new_v must be a subset of the context of m.
// If it is not we force it to be.
// 3. Any local constant occurring in new_v occurs in locals
// 4. m does not occur in new_v
state & s = m_benv.m_curr_state;
metavar_decl const * d = s.get_metavar_decl(m);
lean_assert(d);
bool ok = true;
for_each(v, [&](expr const & e, unsigned) {
if (!ok)
return false; // stop search
if (is_href(e)) {
if (!d->contains_href(e)) {
ok = false; // failed 1
return false;
}
} else if (blast::is_local(e)) {
if (std::all_of(locals.begin(), locals.end(), [&](expr const & a) {
return local_index(a) != local_index(e); })) {
ok = false; // failed 3
return false;
}
} else if (is_mref(e)) {
if (m == e) {
ok = false; // failed 4
return false;
}
s.restrict_mref_context_using(e, m); // enforce 2
return false;
}
return true;
});
return ok;
}
/** \brief Return the type of a local constant (local or not).
\remark This method allows the customer to store the type of local constants
in a different place. */
virtual expr infer_local(expr const & e) const {
if (is_href(e)) {
branch const & b = m_benv.m_curr_state.get_main_branch();
hypothesis const * h = b.get(e);
lean_assert(h);
return h->get_type();
} else {
return mlocal_type(e);
}
}
virtual expr infer_metavar(expr const & m) const {
state const & s = m_benv.m_curr_state;
metavar_decl const * d = s.get_metavar_decl(m);
lean_assert(d);
return d->get_type();
}
virtual level mk_uvar() {
return m_benv.m_curr_state.mk_uref();
}
virtual expr mk_mvar(expr const & type) {
return m_benv.m_curr_state.mk_metavar(type);
}
virtual void push() {
// TODO(Leo): we only need to save the assignment and metavar_decls.
m_stack.push_back(m_benv.m_curr_state);
}
virtual void pop() {
m_benv.m_curr_state = m_stack.back();
m_stack.pop_back();
}
virtual void commit() {
m_stack.pop_back();
}
};
class to_blast_expr_fn : public replace_visitor {
type_checker m_tc;
state & m_state;
@ -219,15 +354,22 @@ class blastenv {
return s;
}
ti m_ti;
public:
blastenv(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds):
m_env(env), m_ios(ios), m_lemma_hints(to_name_set(ls)), m_unfold_hints(to_name_set(ds)),
m_not_reducible_pred(mk_not_reducible_pred(env)) {
m_env(env), m_ios(ios), m_ngen(*g_prefix), m_lemma_hints(to_name_set(ls)), m_unfold_hints(to_name_set(ds)),
m_not_reducible_pred(mk_not_reducible_pred(env)),
m_class_pred(mk_class_pred(env)),
m_instance_pred(mk_instance_pred(env)),
m_ti(*this) {
}
optional<expr> operator()(goal const & g) {
m_curr_state = to_state(g);
// TODO(Leo): set local context for type class resolution at ti
// TODO(Leo): blast main loop
display("Blast tactic initial state\n");
display_curr_state();
@ -250,6 +392,17 @@ public:
projection_info const * get_projection_info(name const & n) const {
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);
}
expr whnf(expr const & e) { return m_ti.whnf(e); }
expr infer_type(expr const & e) { return m_ti.infer(e); }
bool is_prop(expr const & e) { return m_ti.is_prop(e); }
bool is_def_eq(expr const & e1, expr const & e2) { return m_ti.is_def_eq(e1, e2); }
optional<expr> mk_class_instance(expr const & e) { return m_ti.mk_class_instance(e); }
};
LEAN_THREAD_PTR(blastenv, g_blastenv);
@ -285,6 +438,41 @@ projection_info const * get_projection_info(name const & n) {
return g_blastenv->get_projection_info(n);
}
expr whnf(expr const & e) {
lean_assert(g_blastenv);
return g_blastenv->whnf(e);
}
expr infer_type(expr const & e) {
lean_assert(g_blastenv);
return g_blastenv->infer_type(e);
}
bool is_prop(expr const & e) {
lean_assert(g_blastenv);
return g_blastenv->is_prop(e);
}
bool is_def_eq(expr const & e1, expr const & e2) {
lean_assert(g_blastenv);
return g_blastenv->is_def_eq(e1, e2);
}
optional<expr> mk_class_instance(expr const & e) {
lean_assert(g_blastenv);
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);
}
void display_curr_state() {
curr_state().display(env(), ios());
display("\n");
@ -298,58 +486,27 @@ void display(sstream const & msg) {
ios().get_diagnostic_channel() << msg.str();
}
/** \brief Auxiliary object to interface blast state with existing kernel extensions */
class ext_context : public extension_context {
name_generator m_ngen;
public:
virtual environment const & env() const { return env(); }
virtual pair<expr, constraint_seq> whnf(expr const & e) {
return mk_pair(blast::whnf(e), constraint_seq());
}
virtual pair<bool, constraint_seq> is_def_eq(expr const & e1, expr const & e2, delayed_justification &) {
return mk_pair(blast::is_def_eq(e1, e2), constraint_seq());
}
virtual pair<expr, constraint_seq> check_type(expr const & e, bool) {
return mk_pair(blast::infer_type(e), constraint_seq());
}
virtual name mk_fresh_name() {
return m_ngen.next();
}
virtual optional<expr> is_stuck(expr const &) {
return none_expr();
}
};
LEAN_THREAD_PTR(ext_context, g_ext_context);
struct scope_ext_context {
ext_context * m_prev_context;
public:
scope_ext_context(ext_context & c):m_prev_context(g_ext_context) { g_ext_context = &c; }
~scope_ext_context() { g_ext_context = m_prev_context; }
};
extension_context & ext_ctx() {
lean_assert(g_ext_context);
return *g_ext_context;
scope::scope():m_keep(false) {
lean_assert(g_blastenv);
g_blastenv->m_ti.push();
}
name mk_fresh_local_name() {
lean_assert(g_ext_context);
return g_ext_context->mk_fresh_name();
scope::~scope() {
if (m_keep)
g_blastenv->m_ti.commit();
else
g_blastenv->m_ti.pop();
}
void scope::commit() {
m_keep = true;
}
}
optional<expr> blast_goal(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds,
goal const & g) {
blast::scope_hash_consing scope1;
blast::blastenv b(env, ios, ls, ds);
blast::ext_context x;
blast::scope_blastenv scope2(b);
blast::scope_ext_context scope3(x);
return b(g);
}
void initialize_blast() {

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

@ -5,9 +5,63 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "library/tactic/goal.h"
#include "kernel/environment.h"
#include "library/io_state.h"
#include "library/blast/state.h"
namespace lean {
struct projection_info;
class goal;
namespace blast {
/** \brief Return the thread local environment being used by the blast tactic. */
environment const & env();
/** \brief Return the thread local io_state being used by the blast tactic. */
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();
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);
/** \brief Return a nonnull projection_info object if \c n is the name of a projection in env() */
projection_info const * get_projection_info(name const & n);
/** \brief Put the given expression in weak-head-normal-form with respect to the
current state being processed by the blast tactic. */
expr whnf(expr const & e);
/** \brief Return the type of the given expression with respect to the current state being
processed by the blast tactic.
\remark: (potential side-effect) this procedure may update the meta-variable assignment
associated with the current state. */
expr infer_type(expr const & e);
/** \brief Return true if \c e is a Proposition */
bool is_prop(expr const & e);
/** \brief Return true iff the two expressions are definitionally equal in the
current state being processed by the blast tactic.
\remark: (potential side-effect) this procedure may update the meta-variable assignment
associated with the current state. */
bool is_def_eq(expr const & e1, expr const & e2);
/** \brief Try to synthesize an element of the given type class with respect to the blast local context. */
optional<expr> mk_class_instance(expr const & e);
/** \brief Display the current state of the blast tactic in the diagnostic channel. */
void display_curr_state();
/** \brief Display message in the blast tactic diagnostic channel. */
void display(char const * msg);
void display(sstream const & msg);
/**
\brief Create a local scope for saving the assignment and
metavariable declarations at curr_state() */
class scope {
bool m_keep;
public:
scope();
~scope();
void commit();
};
}
optional<expr> blast_goal(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds,
goal const & g);
void initialize_blast();

39
src/library/blast/blast_context.h
View file

@ -1,39 +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
API for accessing the thread local context used by the blast tactic.
These procedures can only be invoked while the blast tactic is being executed.
Remark: the API is implemented in the file blast.cpp
*/
#pragma once
#include "util/sstream.h"
#include "library/projection.h"
#include "library/blast/state.h"
namespace lean {
namespace blast {
/** \brief Return the thread local environment being used by the blast tactic. */
environment const & env();
/** \brief Return the thread local io_state being used by the blast tactic. */
io_state const & ios();
/** \brief Return the thread local current state begin processed by the blast tactic. */
state & curr_state();
/** \brief Return the thead local extension context associated with the blast tactic. */
extension_context & ext_ctx();
/** \brief Return a thread local fresh name meant to be used to name local constants. */
name mk_fresh_local_name();
/** \brief Return true iff the given constant name is marked as reducible in env() */
bool is_reducible(name const & n);
/** \brief Return a nonnull projection_info object if \c n is the name of a projection in env() */
projection_info const * get_projection_info(name const & n);
/** \brief Display the current state of the blast tactic in the diagnostic channel. */
void display_curr_state();
/** \brief Display message in the blast tactic diagnostic channel. */
void display(char const * msg);
void display(sstream const & msg);
}}

534
src/library/blast/infer_type.cpp
View file

@ -1,534 +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/interrupt.h"
#include "kernel/instantiate.h"
#include "kernel/abstract.h"
#include "kernel/for_each_fn.h"
#include "library/normalize.h"
#include "library/blast/infer_type.h"
#include "library/blast/blast_context.h"
#include "library/blast/blast_exception.h"
namespace lean {
namespace blast {
static optional<expr> expand_macro(expr const & m) {
lean_assert(is_macro(m));
return macro_def(m).expand(m, ext_ctx());
}
static optional<expr> reduce_projection(expr const & e) {
expr const & f = get_app_fn(e);
if (!is_constant(f))
return none_expr();
projection_info const * info = get_projection_info(const_name(f));
if (!info)
return none_expr();
buffer<expr> args;
get_app_args(e, args);
if (args.size() <= info->m_nparams)
return none_expr();
unsigned mkidx = info->m_nparams;
expr const & mk = args[mkidx];
expr new_mk = whnf(mk);
expr const & new_mk_fn = get_app_fn(new_mk);
if (!is_constant(new_mk_fn) || const_name(new_mk_fn) != info->m_constructor)
return none_expr();
buffer<expr> mk_args;
get_app_args(new_mk, mk_args);
unsigned i = info->m_nparams + info->m_i;
if (i >= mk_args.size())
none_expr();
expr r = mk_args[i];
r = blast::mk_app(r, args.size() - mkidx - 1, args.data() + mkidx + 1);
return some_expr(r);
}
static optional<expr> norm_ext(expr const & e) {
if (auto r = reduce_projection(e)) {
return r;
} else if (auto r = env().norm_ext()(e, ext_ctx())) {
return some_expr(r->first);
} else {
return none_expr();
}
}
static expr whnf_core(expr const & e) {
check_system("whnf");
switch (e.kind()) {
case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local:
case expr_kind::Pi: case expr_kind::Lambda:
return e;
case expr_kind::Constant:
if (blast::is_reducible(const_name(e)))
return whnf_core(instantiate_value_univ_params(env().get(const_name(e)), const_levels(e)));
else
return e;
case expr_kind::Macro:
if (auto m = expand_macro(e))
return whnf_core(*m);
else
return e;
case expr_kind::App: {
buffer<expr> args;
expr f0 = get_app_rev_args(e, args);
expr f = whnf_core(f0);
if (is_lambda(f)) {
unsigned m = 1;
unsigned num_args = args.size();
while (is_lambda(binding_body(f)) && m < num_args) {
f = binding_body(f);
m++;
}
lean_assert(m <= num_args);
return whnf_core(blast::mk_rev_app(instantiate(binding_body(f), m, args.data() + (num_args - m)),
num_args - m, args.data()));
} else {
return f == f0 ? e : whnf_core(blast::mk_rev_app(f, args.size(), args.data()));
}
}}
lean_unreachable();
}
expr whnf(expr const & e) {
expr t = e;
while (true) {
expr t1 = whnf_core(t);
if (auto new_t = norm_ext(t1)) {
t = *new_t;
} else {
return t1;
}
}
}
static expr infer_constant(expr const & e) {
declaration d = env().get(const_name(e));
auto const & ps = d.get_univ_params();
auto const & ls = const_levels(e);
if (length(ps) != length(ls))
throw blast_exception("infer type failed, incorrect number of universe levels", e);
return instantiate_type_univ_params(d, ls);
}
static expr infer_macro(expr const & e) {
auto def = macro_def(e);
bool infer_only = true;
// Remark: we are ignoring constraints generated by the macro definition.
return def.check_type(e, ext_ctx(), infer_only).first;
}
static expr infer_lambda(expr e) {
buffer<expr> es, ds, ls;
while (is_lambda(e)) {
es.push_back(e);
ds.push_back(binding_domain(e));
expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data());
expr l = blast::mk_local(mk_fresh_local_name(), binding_name(e), d, binding_info(e));
ls.push_back(l);
e = binding_body(e);
}
expr t = infer_type(instantiate_rev(e, ls.size(), ls.data()));
expr r = abstract_locals(t, ls.size(), ls.data());
unsigned i = es.size();
while (i > 0) {
--i;
r = blast::mk_pi(binding_name(es[i]), ds[i], r, binding_info(es[i]));
}
return r;
}
/** \brief Make sure \c e is a sort, if it is not throw an exception using \c ref as a reference */
static void ensure_sort(expr const & e, expr const & ref) {
// Remark: for simplicity reasons, we just fail if \c e is not a sort.
if (!is_sort(e))
throw blast_exception("infer type failed, sort expected", ref);
}
static expr infer_pi(expr const & e0) {
buffer<expr> ls;
buffer<level> us;
expr e = e0;
while (is_pi(e)) {
expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data());
expr d_type = whnf(infer_type(d));
ensure_sort(d_type, e0);
us.push_back(sort_level(d_type));
expr l = blast::mk_local(mk_fresh_local_name(), binding_name(e), d, binding_info(e));
ls.push_back(l);
e = binding_body(e);
}
e = instantiate_rev(e, ls.size(), ls.data());
expr e_type = whnf(infer_type(e));
ensure_sort(e_type, e0);
level r = sort_level(e_type);
unsigned i = ls.size();
bool imp = env().impredicative();
while (i > 0) {
--i;
r = imp ? blast::mk_imax(us[i], r) : blast::mk_max(us[i], r);
}
return blast::mk_sort(r);
}
/** \brief Make sure \c e is a Pi-expression, if it is not throw an exception using \c ref as a reference */
static void ensure_pi(expr const & e, expr const & ref) {
// Remark: for simplicity reasons, we just fail if \c e is not a Pi.
if (!is_pi(e))
throw blast_exception("infer type failed, Pi expected", ref);
// Potential problem: e is of the form (f ...) where f is a constant that is not marked as reducible.
// So, whnf does not reduce it, and we fail to detect that e is can be reduced to a Pi-expression.
}
static expr infer_app(expr const & e) {
buffer<expr> args;
expr const & f = get_app_args(e, args);
expr f_type = infer_type(f);
unsigned j = 0;
unsigned nargs = args.size();
for (unsigned i = 0; i < nargs; i++) {
if (is_pi(f_type)) {
f_type = binding_body(f_type);
} else {
f_type = whnf(instantiate_rev(f_type, i-j, args.data()+j));
ensure_pi(f_type, e);
f_type = binding_body(f_type);
j = i;
}
}
return instantiate_rev(f_type, nargs-j, args.data()+j);
}
expr infer_type(expr const & e) {
lean_assert(!is_var(e));
lean_assert(closed(e));
check_system("infer_type");
expr r;
switch (e.kind()) {
case expr_kind::Local:
if (is_href(e)) {
if (hypothesis const * h = curr_state().get_main_branch().get(e)) {
r = h->get_type();
} else {
throw blast_exception("infer type failed, unknown hypothesis", e);
}
} else {
r = mlocal_type(e);
}
break;
case expr_kind::Meta:
if (is_mref(e)) {
if (metavar_decl const * d = curr_state().get_metavar_decl(mref_index(e))) {
r = d->get_type();
break;
}
}
throw blast_exception("infer type failed, invalid occurrence of metavariable", e);
case expr_kind::Var:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Sort:
r = blast::mk_sort(blast::mk_succ(sort_level(e)));
break;
case expr_kind::Constant:
r = infer_constant(e);
break;
case expr_kind::Macro:
r = infer_macro(e);
break;
case expr_kind::Lambda:
r = infer_lambda(e);
break;
case expr_kind::Pi:
r = infer_pi(e);
break;
case expr_kind::App:
r = infer_app(e);
break;
}
// TODO(Leo): cache results if we have performance problems
return r;
}
bool is_prop(expr const & e) {
if (env().impredicative()) {
expr t = whnf(infer_type(e));
return t == mk_Prop();
} else {
return false;
}
}
bool is_def_eq(level const & l1, level const & l2) {
if (is_equivalent(l1, l2)) {
return true;
} else {
state & s = curr_state();
if (is_uref(l1)) {
if (s.is_uref_assigned(l1)) {
return is_def_eq(*s.get_uref_assignment(l1), l2);
} else {
s.assign_uref(l1, l2);
return true;
}
}
if (is_uref(l2)) {
if (s.is_uref_assigned(l2)) {
return is_def_eq(l1, *s.get_uref_assignment(l2));
} else {
s.assign_uref(l2, l1);
return true;
}
}
return false;
}
}
bool is_def_eq(levels const & ls1, levels const & ls2) {
if (is_nil(ls1) && is_nil(ls2)) {
return true;
} else if (!is_nil(ls1) && !is_nil(ls2)) {
return
is_def_eq(head(ls1), head(ls2)) &&
is_def_eq(tail(ls1), tail(ls2));
} else {
return false;
}
}
static bool is_def_eq_core(expr const & e1, expr const & e2);
/** \brief Given \c e of the form <tt>?m t_1 ... t_n</tt>, where
?m is an assigned mref, substitute \c ?m with its assignment. */
static expr subst_mref(expr const & e) {
buffer<expr> args;
expr const & u = get_app_args(e, args);
expr const * v = curr_state().get_mref_assignment(u);
lean_assert(v);
return apply_beta(*v, args.size(), args.data());
}
/** \brief Given \c ma of the form <tt>?m t_1 ... t_n</tt>, (try to) assign
?m to (an abstraction of) v. Return true if success and false otherwise. */
static bool assign_mref_core(expr const & ma, expr const & v) {
buffer<expr> args;
expr const & m = get_app_args(ma, args);
buffer<expr> locals;
for (expr const & arg : args) {
if (!blast::is_local(arg))
break; // is not local
if (std::any_of(locals.begin(), locals.end(), [&](expr const & local) { return local_index(local) == local_index(arg); }))
break; // duplicate local
locals.push_back(arg);
}
lean_assert(is_mref(m));
state & s = curr_state();
metavar_decl const * d = s.get_metavar_decl(m);
lean_assert(d);
expr new_v = s.instantiate_urefs_mrefs(v);
// We must check
// 1. All href in new_v are in the context of m.
// 2. The context of any (unassigned) mref in new_v must be a subset of the context of m.
// If it is not we force it to be.
// 3. Any local constant occurring in new_v occurs in locals
// 4. m does not occur in new_v
bool ok = true;
for_each(new_v, [&](expr const & e, unsigned) {
if (!ok)
return false; // stop search
if (is_href(e)) {
if (!d->contains_href(e)) {
ok = false; // failed 1
return false;
}
} else if (blast::is_local(e)) {
if (std::all_of(locals.begin(), locals.end(), [&](expr const & a) { return local_index(a) != local_index(e); })) {
ok = false; // failed 3
return false;
}
} else if (is_mref(e)) {
if (m == e) {
ok = false; // failed 4
return false;
}
s.restrict_mref_context_using(e, m); // enforce 2
return false;
}
return true;
});
if (!ok)
return false;
if (args.empty()) {
// easy case
s.assign_mref(m, new_v);
return true;
} else if (args.size() == locals.size()) {
s.assign_mref(m, Fun(locals, new_v));
return true;
} else {
// This case is imprecise since it is not a higher order pattern.
// That the term \c ma is of the form (?m t_1 ... t_n) and the t_i's are not pairwise
// distinct local constants.
expr m_type = d->get_type();
for (unsigned i = 0; i < args.size(); i++) {
m_type = whnf(m_type);
if (!is_pi(m_type))
return false;
lean_assert(i <= locals.size());
if (i == locals.size())
locals.push_back(blast::mk_local(mk_fresh_local_name(), binding_name(m_type), binding_domain(m_type), binding_info(m_type)));
lean_assert(i < locals.size());
m_type = instantiate(binding_body(m_type), locals[i]);
}
lean_assert(locals.size() == args.size());
s.assign_mref(m, Fun(locals, new_v));
return true;
}
}
/** \brief Given \c ma of the form <tt>?m t_1 ... t_n</tt>, (try to) assign
?m to (an abstraction of) v. Return true if success and false otherwise. */
static bool assign_mref(expr const & ma, expr const & v) {
if (assign_mref_core(ma, v))
return true;
expr const & f = get_app_fn(v);
if (is_mref(f) && curr_state().is_mref_assigned(f))
return assign_mref_core(v, ma);
return false;
}
static bool is_def_eq_binding(expr e1, expr e2) {
lean_assert(e1.kind() == e2.kind());
lean_assert(is_binding(e1));
expr_kind k = e1.kind();
buffer<expr> subst;
do {
optional<expr> var_e1_type;
if (binding_domain(e1) != binding_domain(e2)) {
var_e1_type = instantiate_rev(binding_domain(e1), subst.size(), subst.data());
expr var_e2_type = instantiate_rev(binding_domain(e2), subst.size(), subst.data());
if (!is_def_eq_core(var_e2_type, *var_e1_type))
return false;
}
if (!closed(binding_body(e1)) || !closed(binding_body(e2))) {
// local is used inside t or s
if (!var_e1_type)
var_e1_type = instantiate_rev(binding_domain(e1), subst.size(), subst.data());
subst.push_back(blast::mk_local(mk_fresh_local_name(), binding_name(e1),
*var_e1_type, binding_info(e1)));
} else {
expr const & dont_care = mk_Prop();
subst.push_back(dont_care);
}
e1 = binding_body(e1);
e2 = binding_body(e2);
} while (e1.kind() == k && e2.kind() == k);
return is_def_eq_core(instantiate_rev(e1, subst.size(), subst.data()),
instantiate_rev(e2, subst.size(), subst.data()));
}
static bool is_def_eq_app(expr const & e1, expr const & e2) {
lean_assert(is_app(e1) && is_app(e2));
buffer<expr> args1, args2;
expr const & f1 = get_app_args(e1, args1);
expr const & f2 = get_app_args(e2, args2);
if (args1.size() != args2.size() || !is_def_eq_core(f1, f2))
return false;
for (unsigned i = 0; i < args1.size(); i++) {
if (!is_def_eq_core(args1[i], args2[i]))
return false;
}
return true;
}
static bool is_def_eq_eta(expr const & e1, expr const & e2) {
expr new_e1 = try_eta(e1);
expr new_e2 = try_eta(e2);
if (e1 != new_e1 || e2 != new_e2)
return is_def_eq_core(new_e1, new_e2);
return false;
}
static bool is_def_eq_proof_irrel(expr const & e1, expr const & e2) {
if (!env().prop_proof_irrel())
return false;
expr e1_type = infer_type(e1);
expr e2_type = infer_type(e2);
return is_prop(e1_type) && is_def_eq_core(e1_type, e2_type);
}
static bool is_def_eq_core(expr const & e1, expr const & e2) {
check_system("is_def_eq");
if (e1 == e2)
return true;
expr const & f1 = get_app_fn(e1);
if (is_mref(f1)) {
if (curr_state().is_mref_assigned(f1)) {
return is_def_eq_core(subst_mref(e1), e2);
} else {
return assign_mref(e1, e2);
}
}
expr const & f2 = get_app_fn(e2);
if (is_mref(f2)) {
if (curr_state().is_mref_assigned(f2)) {
return is_def_eq_core(e1, subst_mref(e2));
} else {
return assign_mref(e2, e1);
}
}
expr e1_n = whnf(e1);
expr e2_n = whnf(e2);
if (e1 != e1_n || e2 != e2_n)
return is_def_eq_core(e1_n, e2_n);
if (e1.kind() == e2.kind()) {
switch (e1.kind()) {
case expr_kind::Lambda:
case expr_kind::Pi:
if (is_def_eq_binding(e1, e2))
return true;
break;
case expr_kind::Sort:
if (is_def_eq(sort_level(e1), sort_level(e2)))
return true;
break;
case expr_kind::Meta:
case expr_kind::Var:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Local:
case expr_kind::Macro:
break;
case expr_kind::Constant:
if (const_name(e1) == const_name(e2) &&
is_def_eq(const_levels(e1), const_levels(e2)))
return true;
break;
case expr_kind::App:
if (is_def_eq_app(e1, e2))
return true;
break;
}
}
if (is_def_eq_eta(e1, e2))
return true;
return is_def_eq_proof_irrel(e1, e2);
}
/** \remark Precision of is_def_eq can be improved if mrefs and urefs in e1 and e2 are instantiated
before we invoke is_def_eq */
bool is_def_eq(expr const & e1, expr const & e2) {
if (e1 == e2)
return true; // quick check
state & s = curr_state();
state::assignment_snapshot saved(s);
bool r = is_def_eq_core(e1, e2);
if (!r)
saved.restore();
return r;
}
}}

31
src/library/blast/infer_type.h
View file

@ -1,31 +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/expr.h"
namespace lean {
namespace blast {
/** \brief Put the given expression in weak-head-normal-form with respect to the
current state being processed by the blast tactic. */
expr whnf(expr const & e);
/** \brief Return the type of the given expression with respect to the current state being
processed by the blast tactic.
\remark: (potential side-effect) this procedure may update the meta-variable assignment
associated with the current state. */
expr infer_type(expr const & e);
/** \brief Return true if \c e is a Proposition */
bool is_prop(expr const & e);
/** \brief Return true iff the two expressions are definitionally equal in the
current state being processed by the blast tactic.
\remark: (potential side-effect) this procedure may update the meta-variable assignment
associated with the current state. */
bool is_def_eq(expr const & e1, expr const & e2);
bool is_def_eq(level const & l1, level const & l2);
bool is_def_eq(levels const & l1, levels const & l2);
}}

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

@ -75,7 +75,6 @@ public:
// u := l
void assign_uref(level const & u, level const & l) {
lean_assert(!is_uref_assigned(u));
m_uassignment.insert(uref_index(u), l);
}
@ -116,7 +115,6 @@ public:
// m := e
void assign_mref(expr const & m, expr const & e) {
lean_assert(!is_mref_assigned(m));
m_eassignment.insert(mref_index(m), e);
}