Skip to content

Commit

Permalink
Merge pull request #49 from jasagredo/js/pp-and-forall
Browse files Browse the repository at this point in the history
Use `prettyprinter` and rename `forall` to `forAll`
  • Loading branch information
stevana authored May 28, 2024
2 parents bce278e + 7658c79 commit af5a2bb
Show file tree
Hide file tree
Showing 9 changed files with 116 additions and 110 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/main.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ jobs:
fail-fast: false
matrix:
os: [ubuntu-22.04]
ghc-version: ['8.8.4', '8.10.7', '9.2.8', '9.4.7', '9.6.3', '9.8.1']
ghc-version: ['8.8.4', '8.10.7', '9.2.8', '9.4.8', '9.6.5', '9.8.2']

steps:
- uses: actions/checkout@v3
Expand Down
22 changes: 12 additions & 10 deletions quickcheck-state-machine.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ extra-doc-files:
README.md

tested-with:
GHC ==8.8.4 || ==8.10.7 || ==9.2.8 || ==9.4.7 || ==9.6.3 || ==9.8.1
GHC ==8.8.4 || ==8.10.7 || ==9.2.8 || ==9.4.8 || ==9.6.5 || ==9.8.2

-- Due to `tree-diff` being `GPL`, this library makes use of an interface
-- (@CanDiff@) to diff models. This can be implemented with the vendored
Expand Down Expand Up @@ -70,14 +70,15 @@ library no-vendored-treediff
, time >=1.7 && <1.13

build-depends:
, ansi-wl-pprint >=0.6.7.3 && <1.1
, graphviz >=2999.20.0.3 && <2999.21
, pretty-show >=1.6.16 && <1.11
, QuickCheck >=2.12 && <2.15
, random >=1.1 && <1.3
, sop-core >=0.5.0.2 && <0.6
, split >=0.2.3.5 && <0.3
, unliftio >=0.2.7.0 && <0.3
, graphviz >=2999.20.0.3 && <2999.21
, pretty-show >=1.6.16 && <1.11
, prettyprinter ^>=1.7.1
, prettyprinter-ansi-terminal ^>=1.1.3
, QuickCheck >=2.12 && <2.15
, random >=1.1 && <1.3
, sop-core >=0.5.0.2 && <0.6
, split >=0.2.3.5 && <0.3
, unliftio >=0.2.7.0 && <0.3

default-language: Haskell2010

Expand Down Expand Up @@ -124,7 +125,8 @@ library
, time

build-depends:
, ansi-wl-pprint
, prettyprinter
, prettyprinter-ansi-terminal
, QuickCheck
, sop-core

Expand Down
8 changes: 4 additions & 4 deletions src/Test/StateMachine/BoxDrawer.hs
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,8 @@ module Test.StateMachine.BoxDrawer
) where

import Prelude
import Text.PrettyPrint.ANSI.Leijen
(Doc, text, vsep)
import Prettyprinter
(Doc, pretty, vsep)

import Test.StateMachine.Types
(Pid(..))
Expand Down Expand Up @@ -99,8 +99,8 @@ data Fork a = Fork a a a
deriving stock Functor

-- | Given a history, and output from processes generate Doc with boxes
exec :: [(EventType, Pid)] -> Fork [String] -> Doc
exec evT (Fork lops pops rops) = vsep $ map text (preBoxes ++ parBoxes)
exec :: [(EventType, Pid)] -> Fork [String] -> Doc ann
exec evT (Fork lops pops rops) = vsep $ map pretty (preBoxes ++ parBoxes)
where
preBoxes = let pref = compilePrefix pops
in map (adjust $ maximum $ map ((2+) . size) pref ++ map ((2+) . length) (take 1 parBoxes)) pref
Expand Down
9 changes: 5 additions & 4 deletions src/Test/StateMachine/Diffing.hs
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,8 @@ module Test.StateMachine.Diffing (CanDiff(..), ediff) where

import Data.Proxy
(Proxy(..))
import qualified Text.PrettyPrint.ANSI.Leijen as WL
import qualified Prettyprinter as PP
import qualified Prettyprinter.Render.Terminal as PP

class CanDiff x where
-- | Expressions that will be diffed
Expand All @@ -27,13 +28,13 @@ class CanDiff x where
exprDiff :: Proxy x -> AnExpr x -> AnExpr x -> ADiff x

-- | Output a diff in compact form
diffToDocCompact :: Proxy x -> ADiff x -> WL.Doc
diffToDocCompact :: Proxy x -> ADiff x -> PP.Doc PP.AnsiStyle

-- | Output a diff
diffToDoc :: Proxy x -> ADiff x -> WL.Doc
diffToDoc :: Proxy x -> ADiff x -> PP.Doc PP.AnsiStyle

-- | Output an expression
exprToDoc :: Proxy x -> AnExpr x -> WL.Doc
exprToDoc :: Proxy x -> AnExpr x -> PP.Doc PP.AnsiStyle

ediff :: forall x. CanDiff x => x -> x -> ADiff x
ediff x y = exprDiff (Proxy @x) (toDiff x) (toDiff y)
10 changes: 5 additions & 5 deletions src/Test/StateMachine/Logic.hs
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ module Test.StateMachine.Logic
, (.&&)
, (.||)
, (.=>)
, forall
, forAll
, exists
)
where
Expand Down Expand Up @@ -193,10 +193,10 @@ evalLogicPredicate p0 = let b = go p0 in case p0 of
-- >>> gatherAnnotations (Bot .// "bot" .&& Top .// "top")
-- []
--
-- >>> gatherAnnotations (forall [1,2,3] (\i -> 0 .< i .// "positive"))
-- >>> gatherAnnotations (forAll [1,2,3] (\i -> 0 .< i .// "positive"))
-- ["positive","positive","positive"]
--
-- >>> gatherAnnotations (forall [0,1,2,3] (\i -> 0 .< i .// "positive"))
-- >>> gatherAnnotations (forAll [0,1,2,3] (\i -> 0 .< i .// "positive"))
-- []
--
-- >>> gatherAnnotations (exists [1,2,3] (\i -> 0 .< i .// "positive"))
Expand Down Expand Up @@ -280,8 +280,8 @@ l .// s = Annotate s l
(.=>) :: Logic -> Logic -> Logic
(.=>) = (:=>)

forall :: Show a => [a] -> (a -> Logic) -> Logic
forall = Forall
forAll :: Show a => [a] -> (a -> Logic) -> Logic
forAll = Forall

exists :: Show a => [a] -> (a -> Logic) -> Logic
exists = Exists
33 changes: 17 additions & 16 deletions src/Test/StateMachine/Parallel.hs
Original file line number Diff line number Diff line change
Expand Up @@ -81,19 +81,21 @@ import qualified Data.Set as S
import Data.Tree
(Tree(Node))
import Prelude
import Prettyprinter
(Doc)
import Test.QuickCheck
(Gen, Property, Testable, choose, forAllShrinkShow,
property, sized, (.&&.))
import Test.QuickCheck.Monadic
(PropertyM, run)
import Text.PrettyPrint.ANSI.Leijen
(Doc)
import Text.Show.Pretty
(ppShow)
import UnliftIO
(MonadIO, MonadUnliftIO, TChan, concurrently,
forConcurrently, newTChanIO)

import qualified Prettyprinter as PP
import qualified Prettyprinter.Render.Terminal as PP
import Test.StateMachine.BoxDrawer
import Test.StateMachine.ConstructorName
import Test.StateMachine.DotDrawing
Expand All @@ -102,7 +104,6 @@ import Test.StateMachine.Sequential
import Test.StateMachine.Types
import qualified Test.StateMachine.Types.Rank2 as Rank2
import Test.StateMachine.Utils
import qualified Text.PrettyPrint.ANSI.Leijen as PP

------------------------------------------------------------------------

Expand Down Expand Up @@ -547,7 +548,7 @@ executeParallelCommands :: (Show (cmd Concrete), Show (resp Concrete))
-> TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason, Reason)
executeParallelCommands sm@StateMachine{ initModel, cleanup } (ParallelCommands prefix suffixes) hchan stopOnError = do
executeParallelCommands sm@StateMachine{ initModel } (ParallelCommands prefix suffixes) hchan stopOnError = do
(reason0, (env0, _smodel, _counter, _cmodel)) <-
runStateT
(executeCommands sm hchan (Pid 0) CheckEverything prefix)
Expand Down Expand Up @@ -669,7 +670,7 @@ executeNParallelCommands :: (Rank2.Traversable cmd, Show (cmd Concrete), Rank2.F
-> TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason)
executeNParallelCommands sm@StateMachine{ initModel, cleanup } (ParallelCommands prefix suffixes) hchan stopOnError = do
executeNParallelCommands sm@StateMachine{ initModel } (ParallelCommands prefix suffixes) hchan stopOnError = do
(reason0, (env0, _smodel, _counter, _cmodel)) <-
runStateT
(executeCommands sm hchan (Pid 0) CheckEverything prefix)
Expand Down Expand Up @@ -760,8 +761,8 @@ prettyParallelCommandsWithOpts cmds mGraphOptions (h, _, l) = do
PP.putDoc $
mconcat
[ PP.line
, PP.string (show $ toBoxDrawings cmds hist')
, PP.string (show $ simplify ce)
, PP.pretty (show $ toBoxDrawings cmds hist')
, PP.pretty (show $ simplify ce)
, PP.line
]
case mGraphOptions of
Expand All @@ -777,8 +778,8 @@ simplify (ExistsC [] []) = BotC
simplify (ExistsC _ [Fst ce]) = ce
simplify (ExistsC x (Fst ce : ces)) = ce `EitherC` simplify (ExistsC x ces)
simplify (ExistsC _ (Snd ce : _)) = simplify ce
simplify _ = error "simplify: impossible,\
\ because of the structure of linearise."
simplify _ = error "simplify: impossible, \
\because of the structure of linearise."

prettyParallelCommands :: (Show (cmd Concrete), Show (resp Concrete))
=> MonadIO m
Expand All @@ -804,7 +805,7 @@ prettyNParallelCommandsWithOpts cmds mGraphOptions (h, _, l) =
PP.putDoc $
mconcat
[ PP.line
, PP.string (show $ simplify ce)
, PP.pretty (show $ simplify ce)
, PP.line
]
case mGraphOptions of
Expand All @@ -823,15 +824,15 @@ prettyNParallelCommands cmds = prettyNParallelCommandsWithOpts cmds Nothing

-- | Draw an ASCII diagram of the history of a parallel program. Useful for
-- seeing how a race condition might have occured.
toBoxDrawings :: forall cmd resp. Rank2.Foldable cmd
toBoxDrawings :: forall cmd resp ann. Rank2.Foldable cmd
=> (Show (cmd Concrete), Show (resp Concrete))
=> ParallelCommands cmd resp -> History cmd resp -> Doc
=> ParallelCommands cmd resp -> History cmd resp -> Doc ann
toBoxDrawings (ParallelCommands prefix suffixes) = toBoxDrawings'' allVars
where
allVars = getAllUsedVars prefix `S.union`
foldMap (foldMap getAllUsedVars) suffixes

toBoxDrawings'' :: Set Var -> History cmd resp -> Doc
toBoxDrawings'' :: Set Var -> History cmd resp -> Doc ann
toBoxDrawings'' knownVars (History h) = mconcat
([ exec evT (fmap (out . snd) <$> Fork l p r)
, PP.line
Expand Down Expand Up @@ -869,11 +870,11 @@ toBoxDrawings (ParallelCommands prefix suffixes) = toBoxDrawings'' allVars
evT :: [(EventType, Pid)]
evT = toEventType (filter (\e -> fst e `Prelude.elem` map Pid [1, 2]) h)

ppException :: (Int, String) -> Doc
ppException :: (Int, String) -> Doc ann
ppException (idx, err) = mconcat
[ PP.string $ "Exception " <> show idx <> ":"
[ PP.pretty $ "Exception " <> show idx <> ":"
, PP.line
, PP.indent 2 $ PP.string err
, PP.indent 2 $ PP.pretty err
, PP.line
, PP.line
]
Expand Down
79 changes: 40 additions & 39 deletions src/Test/StateMachine/Sequential.hs
Original file line number Diff line number Diff line change
Expand Up @@ -86,6 +86,10 @@ import qualified Data.Set as S
import Data.Time
(defaultTimeLocale, formatTime, getZonedTime)
import Prelude
import Prettyprinter
(Doc)
import qualified Prettyprinter as PP
import qualified Prettyprinter.Render.Terminal as PP
import System.Directory
(createDirectoryIfMissing)
import System.FilePath
Expand All @@ -101,9 +105,6 @@ import Test.QuickCheck.Monadic
(PropertyM, run)
import Test.QuickCheck.Random
(mkQCGen)
import qualified Text.PrettyPrint.ANSI.Leijen as PP
import Text.PrettyPrint.ANSI.Leijen
(Doc)
import Text.Show.Pretty
(ppShow)
import UnliftIO
Expand Down Expand Up @@ -456,7 +457,7 @@ executeCommands StateMachine {..} hchan pid check =
getUsedConcrete :: Rank2.Foldable f => f Concrete -> [Dynamic]
getUsedConcrete = Rank2.foldMap (\(Concrete x) -> [toDyn x])

modelDiff :: forall model r. CanDiff (model r) => model r -> Maybe (model r) -> Doc
modelDiff :: forall model r. CanDiff (model r) => model r -> Maybe (model r) -> Doc PP.AnsiStyle
modelDiff model = diffToDocCompact p . flip ediff model . fromMaybe model
where
p = Proxy @(model r)
Expand All @@ -472,35 +473,35 @@ prettyPrintHistory StateMachine { initModel, transition }
. makeOperations
. unHistory
where
go :: model Concrete -> Maybe (model Concrete) -> [Operation cmd resp] -> Doc
go :: model Concrete -> Maybe (model Concrete) -> [Operation cmd resp] -> Doc PP.AnsiStyle
go current previous [] =
PP.line <> modelDiff current previous <> PP.line <> PP.line
go current previous [Crash cmd err pid] =
mconcat
[ PP.line
, modelDiff current previous
, PP.line, PP.line
, PP.string " == "
, PP.string (ppShow cmd)
, PP.string " ==> "
, PP.string err
, PP.string " [ "
, PP.int (unPid pid)
, PP.string " ]"
, PP.pretty " == "
, PP.pretty (ppShow cmd)
, PP.pretty " ==> "
, PP.pretty err
, PP.pretty " [ "
, PP.pretty (unPid pid)
, PP.pretty " ]"
, PP.line
]
go current previous (Operation cmd resp pid : ops) =
mconcat
[ PP.line
, modelDiff current previous
, PP.line, PP.line
, PP.string " == "
, PP.string (ppShow cmd)
, PP.string " ==> "
, PP.string (ppShow resp)
, PP.string " [ "
, PP.int (unPid pid)
, PP.string " ]"
, PP.pretty " == "
, PP.pretty (ppShow cmd)
, PP.pretty " ==> "
, PP.pretty (ppShow resp)
, PP.pretty " [ "
, PP.pretty (unPid pid)
, PP.pretty " ]"
, PP.line
, go (transition current cmd resp) (Just current) ops
]
Expand All @@ -527,46 +528,46 @@ prettyPrintHistory' sm@StateMachine { initModel, transition } tag cmds
. makeOperations
. unHistory
where
tagsDiff :: [tag] -> [tag] -> Doc
tagsDiff :: [tag] -> [tag] -> Doc PP.AnsiStyle
tagsDiff old new = diffToDocCompact (Proxy @[tag]) (ediff old new)

go :: model Concrete -> Maybe (model Concrete) -> [tag] -> [[tag]]
-> [Operation cmd resp] -> Doc
-> [Operation cmd resp] -> Doc PP.AnsiStyle
go current previous _seen _tags [] =
PP.line <> modelDiff current previous <> PP.line <> PP.line
go current previous seen (tags : _) [Crash cmd err pid] =
mconcat
[ PP.line
, modelDiff current previous
, PP.line, PP.line
, PP.string " == "
, PP.string (ppShow cmd)
, PP.string " ==> "
, PP.string err
, PP.string " [ "
, PP.int (unPid pid)
, PP.string " ]"
, PP.pretty " == "
, PP.pretty (ppShow cmd)
, PP.pretty " ==> "
, PP.pretty err
, PP.pretty " [ "
, PP.pretty (unPid pid)
, PP.pretty " ]"
, PP.line
, if not (null tags)
then PP.line <> PP.string " " <> tagsDiff seen tags <> PP.line
else PP.empty
then PP.line <> PP.pretty " " <> tagsDiff seen tags <> PP.line
else PP.emptyDoc
]
go current previous seen (tags : tagss) (Operation cmd resp pid : ops) =
mconcat
[ PP.line
, modelDiff current previous
, PP.line, PP.line
, PP.string " == "
, PP.string (ppShow cmd)
, PP.string " ==> "
, PP.string (ppShow resp)
, PP.string " [ "
, PP.int (unPid pid)
, PP.string " ]"
, PP.pretty " == "
, PP.pretty (ppShow cmd)
, PP.pretty " ==> "
, PP.pretty (ppShow resp)
, PP.pretty " [ "
, PP.pretty (unPid pid)
, PP.pretty " ]"
, PP.line
, if not (null tags)
then PP.line <> PP.string " " <> tagsDiff seen tags <> PP.line
else PP.empty
then PP.line <> PP.pretty " " <> tagsDiff seen tags <> PP.line
else PP.emptyDoc
, go (transition current cmd resp) (Just current) tags tagss ops
]
go _ _ _ _ _ = error "prettyPrintHistory': impossible."
Expand Down
Loading

0 comments on commit af5a2bb

Please sign in to comment.