Skip to content

Commit e4e0d98

Browse files
ana-pantilieana-pantilie
committed
Handle WithConfiguration in kore-repl
1 parent ec02c41 commit e4e0d98

File tree

2 files changed

+135
-123
lines changed

2 files changed

+135
-123
lines changed

‎kore/src/Kore/Repl.hs

Lines changed: 98 additions & 86 deletions
Original file line numberDiff line numberDiff line change
@@ -12,95 +12,95 @@ module Kore.Repl (
1212
) where
1313

1414
import Control.Concurrent.MVar
15-
import Control.Exception (
16-
AsyncException (UserInterrupt),
17-
fromException,
18-
)
15+
import Control.Exception
16+
( AsyncException (UserInterrupt)
17+
)
1918
import qualified Control.Lens as Lens
20-
import Control.Monad (
21-
forever,
22-
void,
23-
)
24-
import Control.Monad.Catch (
25-
MonadMask,
26-
)
19+
import Control.Monad
20+
( forever
21+
, void
22+
)
23+
import Control.Monad.Catch
24+
( MonadMask
25+
)
2726
import qualified Control.Monad.Catch as Exception
28-
import Control.Monad.RWS.Strict (
29-
RWST,
30-
execRWST,
31-
)
32-
import Control.Monad.Reader (
33-
ReaderT (..),
34-
)
35-
import Control.Monad.State.Strict (
36-
MonadState,
37-
StateT,
38-
evalStateT,
39-
)
27+
import Control.Monad.Reader
28+
( ReaderT (..)
29+
)
30+
import Control.Monad.RWS.Strict
31+
( RWST
32+
, execRWST
33+
)
34+
import Control.Monad.State.Strict
35+
( MonadState
36+
, StateT
37+
, evalStateT
38+
)
4039
import Data.Generics.Product
4140
import Data.Generics.Wrapped
4241
import qualified Data.Graph.Inductive.Graph as Graph
43-
import Data.List (
44-
findIndex,
45-
)
42+
import Data.List
43+
( findIndex
44+
)
4645
import qualified Data.Map.Strict as Map
4746
import qualified Data.Sequence as Seq
4847
import qualified Data.Text as Text
49-
import Kore.Attribute.RuleIndex (
50-
RuleIndex (..),
51-
)
48+
import Kore.Attribute.RuleIndex
49+
( RuleIndex (..)
50+
)
5251
import qualified Kore.Attribute.RuleIndex as Attribute
53-
import Kore.Internal.TermLike (
54-
TermLike,
55-
mkSortVariable,
56-
mkTop,
57-
)
52+
import Kore.Internal.TermLike
53+
( TermLike
54+
, mkSortVariable
55+
, mkTop
56+
)
5857
import qualified Kore.Log as Log
59-
import Kore.Log.ErrorException (
60-
errorException,
61-
)
62-
import Kore.Reachability (
63-
SomeClaim,
64-
lensClaimPattern,
65-
)
58+
import Kore.Log.ErrorException
59+
( errorException
60+
)
61+
import Kore.Reachability
62+
( SomeClaim
63+
, lensClaimPattern
64+
)
6665
import Kore.Reachability.Claim
66+
import qualified Kore.Reachability.Claim as Claim
6767
import Kore.Reachability.Prove
6868
import Kore.Repl.Data
6969
import Kore.Repl.Interpreter
7070
import Kore.Repl.Parser
7171
import Kore.Repl.State
72-
import Kore.Step.Simplification.Data (
73-
MonadSimplify,
74-
)
72+
import Kore.Step.Simplification.Data
73+
( MonadSimplify
74+
)
7575
import qualified Kore.Step.Strategy as Strategy
76-
import Kore.Syntax.Module (
77-
ModuleName (..),
78-
)
76+
import Kore.Syntax.Module
77+
( ModuleName (..)
78+
)
7979
import Kore.Syntax.Variable
80-
import Kore.Unification.Procedure (
81-
unificationProcedure,
82-
)
83-
import Kore.Unparser (
84-
unparseToString,
85-
)
80+
import Kore.Unification.Procedure
81+
( unificationProcedure
82+
)
83+
import Kore.Unparser
84+
( unparseToString
85+
)
8686
import Prelude.Kore
87-
import Prof (
88-
MonadProf,
89-
)
90-
import System.Clock (
91-
Clock (Monotonic),
92-
TimeSpec,
93-
getTime,
94-
)
95-
import System.IO (
96-
hFlush,
97-
hPutStrLn,
98-
stderr,
99-
stdout,
100-
)
101-
import Text.Megaparsec (
102-
parseMaybe,
103-
)
87+
import Prof
88+
( MonadProf
89+
)
90+
import System.Clock
91+
( Clock (Monotonic)
92+
, TimeSpec
93+
, getTime
94+
)
95+
import System.IO
96+
( hFlush
97+
, hPutStrLn
98+
, stderr
99+
, stdout
100+
)
101+
import Text.Megaparsec
102+
( parseMaybe
103+
)
104104

105105
{- | Runs the repl for proof mode. It requires all the tooling and simplifiers
106106
that would otherwise be required in the proof and allows for step-by-step
@@ -263,25 +263,37 @@ runRepl
263263
if Graph.outdeg (Strategy.graph graph) node == 0
264264
then
265265
proveClaimStep claims axioms graph node
266-
& catchInterruptWithDefault graph
267-
& catchEverything graph
266+
& Exception.handle (userInterruptHandler graph)
267+
& Exception.handle (withConfigurationHandler graph)
268+
& Exception.handle (someExceptionHandler graph)
268269
else pure graph
269270

270-
catchInterruptWithDefault :: a -> m a -> m a
271-
catchInterruptWithDefault a =
272-
Exception.handle $ \case
273-
UserInterrupt -> do
274-
liftIO $ hPutStrLn stderr "Step evaluation interrupted."
275-
pure a
276-
e -> Exception.throwM e
271+
userInterruptHandler :: a -> AsyncException -> m a
272+
userInterruptHandler a UserInterrupt = do
273+
liftIO $ hPutStrLn stderr "Step evaluation interrupted."
274+
pure a
275+
userInterruptHandler _ asyncException =
276+
Exception.throwM asyncException
277277

278-
catchEverything :: a -> m a -> m a
279-
catchEverything a =
280-
Exception.handleAll $ \e -> do
281-
case fromException e of
282-
Just (Log.SomeEntry entry) -> Log.logEntry entry
283-
Nothing -> errorException e
284-
pure a
278+
withConfigurationHandler :: a -> Claim.WithConfiguration -> m a
279+
withConfigurationHandler
280+
_
281+
(Claim.WithConfiguration lastConfiguration someException)
282+
= do
283+
liftIO $
284+
hPutStrLn
285+
stderr
286+
("// Last configuration:\n" <> unparseToString lastConfiguration)
287+
Exception.throwM someException
288+
289+
someExceptionHandler :: a -> Exception.SomeException -> m a
290+
someExceptionHandler a someException = do
291+
case Exception.fromException someException of
292+
Just (Log.SomeEntry entry) ->
293+
Log.logEntry entry
294+
Nothing ->
295+
errorException someException
296+
pure a
285297

286298
replGreeting :: m ()
287299
replGreeting =

‎kore/src/Kore/Repl/Parser.hs

Lines changed: 37 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
{- |
44
Module : Kore.Repl.Parser
55
Description : REPL parser.
6-
Copyright : (c) Runtime Verification, 219
6+
Copyright : (c) Runtime Verification, 2019
77
License : NCSA
88
Maintainer : [email protected]
99
-}
@@ -13,51 +13,51 @@ module Kore.Repl.Parser (
1313
ReplParseError (..),
1414
) where
1515

16-
import Data.Functor (
17-
void,
18-
)
19-
import Data.GraphViz (
20-
GraphvizOutput,
21-
)
16+
import Data.Functor
17+
( void
18+
)
19+
import Data.GraphViz
20+
( GraphvizOutput
21+
)
2222
import qualified Data.GraphViz as Graph
2323
import qualified Data.HashSet as HashSet
24-
import Data.List (
25-
nub,
26-
)
24+
import Data.List
25+
( nub
26+
)
2727
import qualified Data.Set as Set
28-
import Data.String (
29-
IsString (..),
30-
)
31-
import Data.Text (
32-
Text,
33-
)
28+
import Data.String
29+
( IsString (..)
30+
)
31+
import Data.Text
32+
( Text
33+
)
3434
import qualified Data.Text as Text
35-
import Kore.Log (
36-
EntryTypes,
37-
)
35+
import Kore.Log
36+
( EntryTypes
37+
)
3838
import qualified Kore.Log as Log
3939
import qualified Kore.Log.Registry as Log
4040
import Kore.Repl.Data
41-
import Prelude.Kore hiding (
42-
many,
43-
)
44-
import Text.Megaparsec (
45-
Parsec,
46-
ShowErrorComponent (..),
47-
customFailure,
48-
eof,
49-
many,
50-
manyTill,
51-
noneOf,
52-
oneOf,
53-
option,
54-
try,
55-
)
41+
import Prelude.Kore hiding
42+
( many
43+
)
44+
import Text.Megaparsec
45+
( Parsec
46+
, ShowErrorComponent (..)
47+
, customFailure
48+
, eof
49+
, many
50+
, manyTill
51+
, noneOf
52+
, oneOf
53+
, option
54+
, try
55+
)
5656
import qualified Text.Megaparsec.Char as Char
5757
import qualified Text.Megaparsec.Char.Lexer as L
58-
import Type.Reflection (
59-
SomeTypeRep,
60-
)
58+
import Type.Reflection
59+
( SomeTypeRep
60+
)
6161

6262
type Parser = Parsec ReplParseError Text
6363

0 commit comments

Comments
 (0)