Add SBVException handler to prover calls. Fixes #444.

src/Cryptol/REPL/Command.hs

@@ -525,9 +525,10 @@ showProverStats mprover stat = rPutStrLn msg
         maybe "" (\p -> ", using " ++ show p) mprover ++ ")"
 
 rethrowErrorCall :: REPL a -> REPL a
-rethrowErrorCall m = REPL (\r -> unREPL m r `X.catch` handler)
+rethrowErrorCall m = REPL (\r -> unREPL m r `X.catch` handler `X.catch` handler')
   where
     handler (X.ErrorCallWithLocation s _) = X.throwIO (SBVError s)
+    handler' e = X.throwIO (SBVException e)
 
 
 -- | Console-specific version of 'proveSat'. Prints output to the

src/Cryptol/REPL/Monad.hs

@@ -114,6 +114,7 @@ import qualified Data.Map as Map
 import qualified Data.Set as Set
 import Text.Read (readMaybe)
 
+import Data.SBV (SBVException)
 import Data.SBV.Dynamic (sbvCheckSolverInstallation)
 
 import Prelude ()
@@ -273,6 +274,7 @@ data REPLException
   | TypeNotTestable T.Type
   | EvalInParamModule [M.Name]
   | SBVError String
+  | SBVException SBVException
     deriving (Show,Typeable)
 
 instance X.Exception REPLException
@@ -300,6 +302,7 @@ instance PP REPLException where
       text "Expression depends on definitions from a parameterized module:"
         $$ nest 2 (vcat (map pp xs))
     SBVError s           -> text "SBV error:" $$ text s
+    SBVException e       -> text "SBV exception:" $$ text (show e)
 
 -- | Raise an exception.
 raise :: REPLException -> REPL a