From 459f31f28bb6db72f6756f345100451cbe4efa05 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 29 Sep 2015 09:02:58 -0700
Subject: [PATCH] feat(library/blast): add basic blast_exception

---
 src/library/blast/blast.cpp         |  8 +++++---
 src/library/blast/blast_exception.h | 22 ++++++++++++++++++++++
 src/library/blast/blast_tactic.cpp  | 20 +++++++++++++-------
 3 files changed, 40 insertions(+), 10 deletions(-)
 create mode 100644 src/library/blast/blast_exception.h

diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp
index 9c9eca333..af566377e 100644
--- a/src/library/blast/blast.cpp
+++ b/src/library/blast/blast.cpp
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "library/blast/expr.h"
 #include "library/blast/state.h"
 #include "library/blast/blast.h"
+#include "library/blast/blast_exception.h"
 
 namespace lean {
 namespace blast {
@@ -66,9 +67,10 @@ class context {
             return blast::mk_var(var_idx(e));
         }
 
-        void throw_unsupported_metavar_occ(expr const &) {
+        void throw_unsupported_metavar_occ(expr const & e) {
             // TODO(Leo): improve error message
-            throw exception("'blast' tactic failed, goal contains a meta-variable application that is not supported");
+            throw blast_exception("'blast' tactic failed, goal contains a "
+                                  "meta-variable application that is not supported", e);
         }
 
         expr mk_mref_app(expr const & mref, unsigned nargs, expr const * args) {
@@ -146,7 +148,7 @@ class context {
             if (auto r = m_local2lref.find(mlocal_name(e)))
                 return * r;
             else
-                throw exception("blast tactic failed, ill-formed input goal");
+                throw blast_exception("blast tactic failed, ill-formed input goal", e);
         }
 
         virtual expr visit_app(expr const & e) {
diff --git a/src/library/blast/blast_exception.h b/src/library/blast/blast_exception.h
new file mode 100644
index 000000000..9ee19b5de
--- /dev/null
+++ b/src/library/blast/blast_exception.h
@@ -0,0 +1,22 @@
+/*
+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 <string>
+#include "util/exception.h"
+#include "kernel/expr.h"
+
+namespace lean {
+class blast_exception : public exception {
+    expr m_expr;
+public:
+    blast_exception(char const * msg, expr const & e):exception(msg), m_expr(e) {}
+    blast_exception(std::string const & msg, expr const & e):exception(msg), m_expr(e) {}
+    virtual ~blast_exception() {}
+    virtual throwable * clone() const { return new blast_exception(m_msg, m_expr); }
+    virtual void rethrow() const { throw *this; }
+};
+}
diff --git a/src/library/blast/blast_tactic.cpp b/src/library/blast/blast_tactic.cpp
index 530e85f3e..6843a52bd 100644
--- a/src/library/blast/blast_tactic.cpp
+++ b/src/library/blast/blast_tactic.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "library/tactic/expr_to_tactic.h"
 #include "library/blast/blast.h"
+#include "library/blast/blast_exception.h"
 
 namespace lean {
 tactic mk_blast_tactic(list<name> const & ls, list<name> const & ds) {
@@ -17,13 +18,18 @@ tactic mk_blast_tactic(list<name> const & ls, list<name> const & ds) {
                 return none_proof_state();
             }
             goal const & g = head(gs);
-            if (auto pr = blast_goal(env, ios, ls, ds, g)) {
-                goals new_gs           = tail(gs);
-                substitution new_subst = s.get_subst();
-                assign(new_subst, g, *pr);
-                return some_proof_state(proof_state(s, new_gs, new_subst));
-            } else {
-                throw_tactic_exception_if_enabled(s, "blast tactic failed");
+            try {
+                if (auto pr = blast_goal(env, ios, ls, ds, g)) {
+                    goals new_gs           = tail(gs);
+                    substitution new_subst = s.get_subst();
+                    assign(new_subst, g, *pr);
+                    return some_proof_state(proof_state(s, new_gs, new_subst));
+                } else {
+                    throw_tactic_exception_if_enabled(s, "blast tactic failed");
+                    return none_proof_state();
+                }
+            } catch (blast_exception & ex) {
+                throw_tactic_exception_if_enabled(s, ex.what());
                 return none_proof_state();
             }
         });