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

feat(library/blast): convert goal into blast state

Browse source
This commit is contained in:
Leonardo de Moura 2015-09-25 14:43:42 -07:00
parent 33f46fd137
commit f01fd744cf
10 changed files with 220 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1 +1 @@
add_library(blast OBJECT state.cpp expr.cpp blast_tactic.cpp init_module.cpp blast.cpp)
add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp init_module.cpp)

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

@ -4,22 +4,188 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/type_checker.h"
#include "library/replace_visitor.h"
#include "library/blast/expr.h"
#include "library/blast/state.h"
#include "library/blast/blast.h"
namespace lean {
namespace blast {
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::Meta: return blast::mk_meta_univ(meta_id(l));
case level_kind::Global: return blast::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)));
case level_kind::IMax:
lhs = to_blast_level(imax_lhs(l));
return blast::mk_imax(lhs, to_blast_level(imax_rhs(l)));
}
lean_unreachable();
}
class context {
environment m_env;
io_state m_ios;
name_set m_lemma_hints;
name_set m_unfold_hints;
class to_blast_expr_fn : public replace_visitor {
type_checker m_tc;
state & m_state;
// We map each metavariable to a metavariable application that contains only pairwise
// distinct local constants (that have been converted into lrefs).
name_map<pair<expr, expr>> & m_mvar2meta_mref;
name_map<expr> & m_local2lref;
expr visit_sort(expr const & e) {
return blast::mk_sort(to_blast_level(sort_level(e)));
}
virtual expr visit_macro(expr const & e) {
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::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);
}
virtual expr visit_var(expr const & e) {
return blast::mk_var(var_idx(e));
}
void throw_unsupported_metavar_occ(expr const &) {
// TODO(Leo): improve error message
throw exception("'blast' tactic failed, goal contains a meta-variable application that is not supported");
}
expr mk_mref_app(expr const & mref, unsigned nargs, expr const * args) {
lean_assert(is_mref(mref));
buffer<expr> new_args;
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());
}
expr visit_meta_app(expr const & e) {
lean_assert(is_meta(e));
buffer<expr> args;
expr const & mvar = get_app_args(e, args);
if (pair<expr, expr> const * meta_mref = m_mvar2meta_mref.find(mlocal_name(mvar))) {
lean_assert(is_meta(meta_mref->first));
lean_assert(is_mref(meta_mref->second));
buffer<expr> decl_args;
get_app_args(meta_mref->first, decl_args);
if (decl_args.size() > args.size())
throw_unsupported_metavar_occ(e);
for (unsigned i = 0; i < decl_args.size(); i++) {
lean_assert(is_local(decl_args[i]));
if (!is_local(args[i]) || mlocal_name(args[i]) != mlocal_name(decl_args[i]))
throw_unsupported_metavar_occ(e);
}
return mk_mref_app(meta_mref->second, args.size() - decl_args.size(), args.data() + decl_args.size());
} else {
unsigned i = 0;
hypothesis_set ctx;
// find prefix of pair-wise distinct local constants that have already been processed.
for (; i < args.size(); i++) {
if (!is_local(args[i]))
break;
expr const & l = args[i];
if (!std::all_of(args.begin(), args.begin() + i,
[&](expr const & prev) { return mlocal_name(prev) != mlocal_name(l); }))
break;
if (auto lref = m_local2lref.find(mlocal_name(l))) {
ctx.insert(lref_index(*lref));
} else {
break;
}
}
unsigned prefix_sz = i;
expr aux = e;
for (; i < args.size(); i++)
aux = app_fn(aux);
lean_assert(is_meta(aux));
expr type = visit(m_tc.infer(aux).first);
unsigned mref_index = m_state.add_metavar_decl(metavar_decl(ctx, type));
expr mref = blast::mk_mref(mref_index);
m_mvar2meta_mref.insert(mlocal_name(mvar), mk_pair(aux, mref));
return mk_mref_app(mref, args.size() - prefix_sz, args.data() + prefix_sz);
}
}
virtual expr visit_meta(expr const & e) {
return visit_meta_app(e);
}
virtual expr visit_local(expr const & e) {
if (auto r = m_local2lref.find(mlocal_name(e)))
return * r;
else
throw exception("blast tactic failed, ill-formed input goal");
}
virtual expr visit_app(expr const & e) {
if (is_meta(e)) {
return visit_meta_app(e);
} else {
expr f = visit(app_fn(e));
return blast::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));
}
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));
}
public:
to_blast_expr_fn(environment const & env, state & s, name_map<pair<expr, expr>> & mvar2meta_mref,
name_map<expr> & local2lref):
m_tc(env), m_state(s), m_mvar2meta_mref(mvar2meta_mref), m_local2lref(local2lref) {}
};
state to_state(goal const & g) {
state s;
branch b;
name_map<pair<expr, expr>> mvar2meta_mref;
name_map<expr> local2lref;
to_blast_expr_fn to_blast_expr(m_env, s, mvar2meta_mref, local2lref);
buffer<expr> hs;
g.get_hyps(hs);
for (expr const & h : hs) {
expr new_type = to_blast_expr(mlocal_type(h));
// TODO(Leo): create hypothesis using new_type
}
expr new_target = to_blast_expr(g.get_type());
// TODO(Leo): create branch and store in the state.
return s;
}
public:
context(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)) {
}
optional<expr> operator()(goal const &) {
optional<expr> operator()(goal const & g) {
state s = to_state(g);
return none_expr();
}
};
@ -30,4 +196,6 @@ optional<expr> blast_goal(environment const & env, io_state const & ios, list<na
blast::context c(env, ios, ls, ds);
return c(g);
}
void initialize_blast() {}
void finalize_blast() {}
}

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

@ -10,4 +10,6 @@ Author: Leonardo de Moura
namespace lean {
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();
void finalize_blast();
}

4
src/library/blast/branch.h
View file

@ -21,11 +21,11 @@ class branch {
expr m_target;
metavar_set m_mvars;
public:
goal():m_next(0) {}
branch():m_next(0) {}
hypothesis const * get(unsigned idx) const { return m_context.find(idx); }
hypothesis const * get(expr const & e) const {
lean_assert(is_lref(e));
return get(get_lmindex(e));
return get(lref_index(e));
}
};
}}

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

@ -78,7 +78,7 @@ bool is_mref(expr const & e) {
return is_lmref(e) && !is_lref(e);
}
unsigned get_lmindex(expr const & e) {
unsigned lmref_index(expr const & e) {
lean_assert(is_lmref(e));
return static_cast<ref_definition_cell const *>(macro_def(e).raw())->get_index();
}
@ -254,6 +254,18 @@ expr mk_app(expr const & f, expr const & a) {
return cache(lean::mk_app(f, a));
}
expr mk_app(expr const & f, unsigned num_args, expr const * args) {
expr r = f;
for (unsigned i = 0; i < num_args; i++)
r = blast::mk_app(r, args[i]);
return r;
}
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_sort(level const & l) {
lean_assert(is_cached(l));
return cache(lean::mk_sort(l));
@ -572,7 +584,7 @@ expr abstract_lrefs(expr const & e, unsigned n, expr const * subst) {
unsigned i = n;
while (i > 0) {
--i;
if (get_lmindex(subst[i]) == get_lmindex(m))
if (lref_index(subst[i]) == lref_index(m))
return some_expr(blast::mk_var(offset + n - i - 1));
}
return none_expr();

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

@ -47,6 +47,8 @@ expr mk_mref(unsigned idx);
expr mk_sort(level const & l);
expr mk_constant(name const & n, levels const & ls);
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_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);
@ -71,7 +73,9 @@ bool is_mref(expr const & e);
bool is_lref(expr const & e);
/** \brief Return the index of the give lref/mref.
\pre is_mref(e) || is_lref(e) */
unsigned get_lmindex(expr const & e);
unsigned lmref_index(expr const & e);
inline unsigned mref_index(expr const & e) { return lmref_index(e); }
inline unsigned lref_index(expr const & e) { return lmref_index(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);

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

@ -19,6 +19,7 @@ typedef rb_tree<unsigned, unsigned_cmp> hypothesis_set;
class hypothesis {
friend class branch;
name m_name; // for pretty printing
bool m_active;
unsigned m_depth;
hypothesis_set m_backward_deps;
@ -27,7 +28,7 @@ class hypothesis {
optional<expr> m_value;
optional<expr> m_justification;
public:
hypothesis();
hypothesis():m_active(0), m_depth(0) {}
bool is_active() const { return m_active; }
unsigned get_depth() const { return m_depth; }
hypothesis_set const & get_backward_deps() const { return m_backward_deps; }

3
src/library/blast/init_module.cpp
View file

@ -4,13 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/blast/blast.h"
#include "library/blast/blast_tactic.h"
namespace lean {
void initialize_blast_module() {
initialize_blast();
initialize_blast_tactic();
}
void finalize_blast_module() {
finalize_blast();
finalize_blast_tactic();
}
}

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

@ -5,3 +5,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/blast/state.h"
namespace lean {
namespace blast {
state::state():m_next_mref_index(0) {}
unsigned state::add_metavar_decl(metavar_decl const & decl) {
unsigned r = m_next_mref_index;
m_next_mref_index++;
m_metavar_decls.insert(r, decl);
return r;
}
}}

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

@ -8,18 +8,29 @@ Author: Leonardo de Moura
#include "util/rb_map.h"
#include "kernel/expr.h"
#include "library/blast/hypothesis.h"
#include "library/blast/branch.h"
namespace lean {
namespace blast {
class metavar_decl {
hypothesis_set m_context;
expr m_type;
public:
metavar_decl() {}
metavar_decl(hypothesis_set const & c, expr const & t):m_context(c), m_type(t) {}
};
class state {
friend class context;
unsigned m_next_mref_index;
typedef rb_map<unsigned, metavar_decl, unsigned_cmp> metavar_decls;
typedef rb_map<unsigned, expr, unsigned_cmp> assignment;
metavar_decls m_metavar_decls;
assignment m_assignment;
public:
state();
unsigned add_metavar_decl(metavar_decl const & decl);
metavar_decl const * get_metavar_decl(unsigned idx) const { return m_metavar_decls.find(idx); }
metavar_decl const * get_metavar_decl(expr const & e) const { return get_metavar_decl(mref_index(e)); }
};
}}