Merge pull request #1075 from GaloisInc/jvm-setup-error

Embed JVMSetupError inside TopLevelException datatype.

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -98,6 +98,7 @@ import Verifier.SAW.TypedTerm
 
 import Verifier.SAW.Simulator.What4.ReturnTrip
 
+import SAWScript.Exceptions
 import SAWScript.Proof
 import SAWScript.Prover.SolverStats
 import SAWScript.TopLevel
@@ -813,7 +814,9 @@ data JVMSetupError
   | JVMReturnUnexpected J.Type -- found
   | JVMReturnTypeMismatch J.Type J.Type -- expected, found
 
-instance X.Exception JVMSetupError
+instance X.Exception JVMSetupError where
+  toException = topLevelExceptionToException
+  fromException = topLevelExceptionFromException
 
 instance Show JVMSetupError where
   show err =

src/SAWScript/Exceptions.hs

@@ -1,11 +1,16 @@
+{-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+
 module SAWScript.Exceptions
   ( TypeErrors(..), failTypecheck
   , TopLevelException(..)
   , TraceException(..)
+  , topLevelExceptionToException
+  , topLevelExceptionFromException
   ) where
 
 import Control.Exception
+import Data.Typeable (cast)
 
 import What4.ProgramLoc (ProgramLoc)
 
@@ -31,13 +36,31 @@ data TopLevelException
   | CrucibleSetupException ProgramLoc String
   | OverrideMatcherException ProgramLoc String
   | LLVMMethodSpecException ProgramLoc String
+  | forall e. Exception e => SomeTopLevelException e
 
 instance Show TopLevelException where
   show (TopLevelException _ msg) = msg
   show (JavaException _ msg) = msg
   show (CrucibleSetupException _ msg) = msg
   show (OverrideMatcherException _ msg) = msg
   show (LLVMMethodSpecException _ msg) = msg
+  show (SomeTopLevelException e) = show e
+
+-- | To use a custom structured exception type that works with the
+-- saw-script REPL's exception handlers and stack tracing, define
+-- 'toException' as 'topLevelExceptionToException' in the custom
+-- exception type's 'Exception' class instance.
+topLevelExceptionToException :: Exception e => e -> SomeException
+topLevelExceptionToException = toException . SomeTopLevelException
+
+-- | To use a custom structured exception type that works with the
+-- saw-script REPL's exception handlers and stack tracing, define
+-- 'fromException' as 'topLevelExceptionFromException' in the custom
+-- exception type's 'Exception' class instance.
+topLevelExceptionFromException :: Exception e => SomeException -> Maybe e
+topLevelExceptionFromException x =
+  do SomeTopLevelException a <- fromException x
+     cast a
 
 instance Exception TopLevelException