From a14bb861484f66d3186b43d06b0f1817559e4812 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 9 Nov 2015 14:20:19 -0800
Subject: [PATCH] feat(library/blast/state): add mk_lambda/mk_pi for
 abstracting hrefs

---
 src/library/blast/state.cpp | 30 ++++++++++++++++++++++++++++++
 src/library/blast/state.h   | 17 +++++++++++++++++
 2 files changed, 47 insertions(+)

diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp
index 7aa3935d1..27efb29f2 100644
--- a/src/library/blast/state.cpp
+++ b/src/library/blast/state.cpp
@@ -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());
 }
diff --git a/src/library/blast/state.h b/src/library/blast/state.h
index 129b011b6..612f6c4dc 100644
--- a/src/library/blast/state.h
+++ b/src/library/blast/state.h
@@ -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