From 6c015a4954ea26e68261ade6a19ee5df29b74893 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 10 Jan 2016 16:30:51 -0800
Subject: [PATCH] feat(library/blast/blast): use blast tmp_type_context to
 generate type class instances

---
 src/library/blast/blast.cpp | 14 +++++++++++++-
 src/library/blast/blast.h   |  2 ++
 2 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp
index 9f8e4f2f6..7414ae542 100644
--- a/src/library/blast/blast.cpp
+++ b/src/library/blast/blast.cpp
@@ -701,7 +701,14 @@ public:
     expr infer_type(expr const & e) { return m_tctx.infer(e); }
     bool is_prop(expr const & e) { return m_tctx.is_prop(e); }
     bool is_def_eq(expr const & e1, expr const & e2) { return m_tctx.is_def_eq(e1, e2); }
-    optional<expr> mk_class_instance(expr const & e) { return m_tctx.mk_class_instance(e); }
+    optional<expr> mk_class_instance(expr const & e) {
+        m_tmp_ctx->clear();
+        return m_tmp_ctx->mk_class_instance(e);
+    }
+    optional<expr> mk_subsingleton_instance(expr const & type) {
+        m_tmp_ctx->clear();
+        return m_tmp_ctx->mk_subsingleton_instance(type);
+    }
 
     tmp_type_context * mk_tmp_type_context();
 
@@ -1083,6 +1090,11 @@ optional<expr> mk_class_instance(expr const & e) {
     return g_blastenv->mk_class_instance(e);
 }
 
+optional<expr> mk_subsingleton_instance(expr const & type) {
+    lean_assert(g_blastenv);
+    return g_blastenv->mk_subsingleton_instance(type);
+}
+
 expr mk_fresh_local(expr const & type, binder_info const & bi) {
     lean_assert(g_blastenv);
     return g_blastenv->mk_fresh_local(type, bi);
diff --git a/src/library/blast/blast.h b/src/library/blast/blast.h
index d56c0f40d..8679fbc47 100644
--- a/src/library/blast/blast.h
+++ b/src/library/blast/blast.h
@@ -112,6 +112,8 @@ bool is_prop(expr const & e);
 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 Try to synthesize an instance of (subsingleton type) with respect to the blast local context. */
+optional<expr> mk_subsingleton_instance(expr const & type);
 
 /** \brief Create a congruence lemma for the given function.
     \pre num_args <= arity of fn