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

feat(library/blast/state): add mk_lambda/mk_pi for abstracting hrefs

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-09 14:20:19 -08:00
parent 973a5c4812
commit a14bb86148
2 changed files with 47 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -524,6 +524,36 @@ void state::restore_assignment(assignment_snapshot const & s) {
m_eassignment = s.m_eassignment;
}
expr state::mk_binding(bool is_lambda, unsigned num, expr const * hrefs, expr const & b) const {
expr r = abstract_locals(b, num, hrefs);
unsigned i = num;
while (i > 0) {
--i;
expr const & h = hrefs[i];
lean_assert(is_href(h));
hypothesis const * hdecl = get(h);
lean_assert(hdecl);
expr t = abstract_locals(hdecl->get_type(), i, hrefs);
if (is_lambda)
r = ::lean::mk_lambda(hdecl->get_name(), t, r);
else
r = ::lean::mk_pi(hdecl->get_name(), t, r);
}
return r;
}
expr state::mk_lambda(list<expr> const & hrefs, expr const & b) const {
buffer<expr> tmp;
to_buffer(hrefs, tmp);
return mk_lambda(tmp, b);
}
expr state::mk_pi(list<expr> const & hrefs, expr const & b) const {
buffer<expr> tmp;
to_buffer(hrefs, tmp);
return mk_pi(tmp, b);
}
void initialize_state() {
g_prefix = new name(name::mk_internal_unique_name());
}

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

@ -133,6 +133,8 @@ class state {
unsigned add_metavar_decl(metavar_decl const & decl);
goal to_goal(branch const &) const;
expr mk_binding(bool is_lambda, unsigned num, expr const * hrefs, expr const & b) const;
#ifdef LEAN_DEBUG
bool check_hypothesis(expr const & e, unsigned hidx, hypothesis const & h) const;
bool check_hypothesis(unsigned hidx, hypothesis const & h) const;
@ -280,6 +282,21 @@ public:
unsigned get_depth() const { return m_depth; }
expr mk_lambda(unsigned num, expr const * hrefs, expr const & b) const {
return mk_binding(false, num, hrefs, b);
}
expr mk_pi(unsigned num, expr const * hrefs, expr const & b) const {
return mk_binding(false, num, hrefs, b);
}
expr mk_lambda(buffer<expr> const & hrefs, expr const & b) const {
return mk_lambda(hrefs.size(), hrefs.data(), b);
}
expr mk_pi(buffer<expr> const & hrefs, expr const & b) const {
return mk_pi(hrefs.size(), hrefs.data(), b);
}
expr mk_lambda(list<expr> const & hrefs, expr const & b) const;
expr mk_pi(list<expr> const & hrefs, expr const & b) const;
#ifdef LEAN_DEBUG
bool check_invariant() const;
#endif