Clean-up: factor out handlers in kore-repl

Author: ana-pantilie

kore/app/repl/Main.hs

@@ -6,10 +6,7 @@ module Main (main) where
 
 import Control.Concurrent.MVar
 import Control.Monad.Catch
-    ( SomeException
-    , fromException
-    , handle
-    , throwM
+    ( handle
     )
 import Data.Reflection
 import GlobalMain
@@ -22,30 +19,25 @@ import qualified Kore.IndexedModule.MetadataToolsBuilder as MetadataTools
     )
 import Kore.Log
     ( KoreLogOptions (..)
-    , SomeEntry (..)
-    , logEntry
     , runLoggerT
     , swappableLogger
     , withLogger
     )
-import Kore.Log.ErrorException
-    ( errorException
-    )
 import Kore.Log.KoreLogOptions
     ( parseKoreLogOptions
     )
 import Kore.Log.WarnIfLowProductivity
     ( warnIfLowProductivity
     )
-import qualified Kore.Reachability.Claim as Claim
+import Kore.Repl
+    ( someExceptionHandler
+    , withConfigurationHandler
+    )
 import Kore.Repl.Data
 import Kore.Step.SMT.Lemma
 import Kore.Syntax.Module
     ( ModuleName (..)
     )
-import Kore.Unparser
-    ( unparseToString
-    )
 import Options.Applicative
     ( InfoMod
     , Parser
@@ -278,23 +270,6 @@ mainWithOptions
         exitReplHandler :: ExitCode -> Main ExitCode
         exitReplHandler = pure
 
-        someExceptionHandler :: SomeException -> Main ExitCode
-        someExceptionHandler someException = do
-            case fromException someException of
-                Just (SomeEntry entry) -> logEntry entry
-                Nothing -> errorException someException
-            throwM someException
-
-        withConfigurationHandler :: Claim.WithConfiguration -> Main ExitCode
-        withConfigurationHandler
-            (Claim.WithConfiguration lastConfiguration someException) =
-                do
-                    liftIO $
-                        hPutStrLn
-                            stderr
-                            ("// Last configuration:\n" <> unparseToString lastConfiguration)
-                    throwM someException
-
         mainModuleName :: ModuleName
         mainModuleName = moduleName definitionModule
 

kore/src/Kore/Repl.hs

@@ -9,6 +9,8 @@ Maintainer  : [email protected]
 -}
 module Kore.Repl (
     runRepl,
+    someExceptionHandler,
+    withConfigurationHandler
 ) where
 
 import Control.Concurrent.MVar
@@ -260,28 +262,16 @@ runRepl
             if Graph.outdeg (Strategy.graph graph) node == 0
                 then
                     proveClaimStep claims axioms graph node
-                        & Exception.handle (withConfigurationHandler graph)
-                        & Exception.handle (someExceptionHandler graph)
+                        & Exception.handle (withConfigurationHandler' graph)
+                        & Exception.handle (someExceptionHandler' graph)
                 else pure graph
 
-        withConfigurationHandler :: a -> Claim.WithConfiguration -> m a
-        withConfigurationHandler
-            _
-            (Claim.WithConfiguration lastConfiguration someException)
-          = do
-            liftIO $
-                hPutStrLn
-                    stderr
-                    ("// Last configuration:\n" <> unparseToString lastConfiguration)
-            Exception.throwM someException
+        withConfigurationHandler' :: a -> Claim.WithConfiguration -> m a
+        withConfigurationHandler' _ = withConfigurationHandler
 
-        someExceptionHandler :: a -> Exception.SomeException -> m a
-        someExceptionHandler a someException = do
-            case Exception.fromException someException of
-                Just (Log.SomeEntry entry) ->
-                    Log.logEntry entry
-                Nothing ->
-                    errorException someException
+        someExceptionHandler' :: a -> Exception.SomeException -> m a
+        someExceptionHandler' a someException = do
+            someExceptionHandler someException
             pure a
 
         replGreeting :: m ()
@@ -296,3 +286,27 @@ runRepl
                 putStr $ "Kore (" <> show (unReplNode node) <> ")> "
                 hFlush stdout
                 getLine
+
+someExceptionHandler
+    :: MonadIO m
+    => Log.MonadLog m
+    => Exception.MonadThrow m
+    => Exception.SomeException -> m a
+someExceptionHandler someException = do
+    case Exception.fromException someException of
+        Just (Log.SomeEntry entry) -> Log.logEntry entry
+        Nothing -> errorException someException
+    Exception.throwM someException
+
+withConfigurationHandler
+    :: MonadIO m
+    => Exception.MonadThrow m
+    => Claim.WithConfiguration -> m a
+withConfigurationHandler
+    (Claim.WithConfiguration lastConfiguration someException) =
+        do
+            liftIO $
+                hPutStrLn
+                    stderr
+                    ("// Last configuration:\n" <> unparseToString lastConfiguration)
+            Exception.throwM someException