{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Move brackets to avoid $" #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TupleSections #-}
module Test.IOTasks.Trace (
AbstractTrace,
OptFlag(..),
progRead, progWrite,
terminate, outOfInputs,
Trace,
ordinaryTrace,
pattern ProgRead, pattern ProgReadString, pattern ProgWrite,
pattern Terminate, pattern OutOfInputs,
inputSequence, isTerminating,
NTrace,
normalizedTrace,
pattern NProgRead, pattern NProgReadString, pattern NProgWrite,
pattern NTerminate, pattern NOutOfInputs,
inputSequenceN, isTerminatingN,
showTrace, showTraceSimple,
showTraceN, showTraceNSimple,
showTrace', showTraceSimple',
showTraceN', showTraceNSimple',
covers,
MatchResult,
isSuccessfulMatch, isInputMismatch, isOutputMismatch, isAlignmentMismatch, isTerminationMismatch,
pPrintMatchResult, pPrintMatchResultSimple,
) where
import Test.IOTasks.OutputPattern hiding (text)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Function (fix)
import Data.Bifunctor (second)
import Text.PrettyPrint hiding ((<>))
import Data.List.NonEmpty (NonEmpty(..))
import Data.Functor.Classes (Show1, showsPrec1, Eq1, eq1)
import Text.Show.Deriving (deriveShow1)
import Data.Eq.Deriving (deriveEq1)
import Text.PrettyPrint.HughesPJClass (Pretty (..))
data OptFlag = Optional | Mandatory deriving (OptFlag -> OptFlag -> Bool
(OptFlag -> OptFlag -> Bool)
-> (OptFlag -> OptFlag -> Bool) -> Eq OptFlag
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: OptFlag -> OptFlag -> Bool
== :: OptFlag -> OptFlag -> Bool
$c/= :: OptFlag -> OptFlag -> Bool
/= :: OptFlag -> OptFlag -> Bool
Eq, Eq OptFlag
Eq OptFlag =>
(OptFlag -> OptFlag -> Ordering)
-> (OptFlag -> OptFlag -> Bool)
-> (OptFlag -> OptFlag -> Bool)
-> (OptFlag -> OptFlag -> Bool)
-> (OptFlag -> OptFlag -> Bool)
-> (OptFlag -> OptFlag -> OptFlag)
-> (OptFlag -> OptFlag -> OptFlag)
-> Ord OptFlag
OptFlag -> OptFlag -> Bool
OptFlag -> OptFlag -> Ordering
OptFlag -> OptFlag -> OptFlag
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: OptFlag -> OptFlag -> Ordering
compare :: OptFlag -> OptFlag -> Ordering
$c< :: OptFlag -> OptFlag -> Bool
< :: OptFlag -> OptFlag -> Bool
$c<= :: OptFlag -> OptFlag -> Bool
<= :: OptFlag -> OptFlag -> Bool
$c> :: OptFlag -> OptFlag -> Bool
> :: OptFlag -> OptFlag -> Bool
$c>= :: OptFlag -> OptFlag -> Bool
>= :: OptFlag -> OptFlag -> Bool
$cmax :: OptFlag -> OptFlag -> OptFlag
max :: OptFlag -> OptFlag -> OptFlag
$cmin :: OptFlag -> OptFlag -> OptFlag
min :: OptFlag -> OptFlag -> OptFlag
Ord, Int -> OptFlag -> ShowS
[OptFlag] -> ShowS
OptFlag -> String
(Int -> OptFlag -> ShowS)
-> (OptFlag -> String) -> ([OptFlag] -> ShowS) -> Show OptFlag
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> OptFlag -> ShowS
showsPrec :: Int -> OptFlag -> ShowS
$cshow :: OptFlag -> String
show :: OptFlag -> String
$cshowList :: [OptFlag] -> ShowS
showList :: [OptFlag] -> ShowS
Show)
data U a = U deriving (U a -> U a -> Bool
(U a -> U a -> Bool) -> (U a -> U a -> Bool) -> Eq (U a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (a :: k). U a -> U a -> Bool
$c== :: forall k (a :: k). U a -> U a -> Bool
== :: U a -> U a -> Bool
$c/= :: forall k (a :: k). U a -> U a -> Bool
/= :: U a -> U a -> Bool
Eq,Int -> U a -> ShowS
[U a] -> ShowS
U a -> String
(Int -> U a -> ShowS)
-> (U a -> String) -> ([U a] -> ShowS) -> Show (U a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (a :: k). Int -> U a -> ShowS
forall k (a :: k). [U a] -> ShowS
forall k (a :: k). U a -> String
$cshowsPrec :: forall k (a :: k). Int -> U a -> ShowS
showsPrec :: Int -> U a -> ShowS
$cshow :: forall k (a :: k). U a -> String
show :: U a -> String
$cshowList :: forall k (a :: k). [U a] -> ShowS
showList :: [U a] -> ShowS
Show)
newtype I a = I a deriving (I a -> I a -> Bool
(I a -> I a -> Bool) -> (I a -> I a -> Bool) -> Eq (I a)
forall a. Eq a => I a -> I a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => I a -> I a -> Bool
== :: I a -> I a -> Bool
$c/= :: forall a. Eq a => I a -> I a -> Bool
/= :: I a -> I a -> Bool
Eq, Int -> I a -> ShowS
[I a] -> ShowS
I a -> String
(Int -> I a -> ShowS)
-> (I a -> String) -> ([I a] -> ShowS) -> Show (I a)
forall a. Show a => Int -> I a -> ShowS
forall a. Show a => [I a] -> ShowS
forall a. Show a => I a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> I a -> ShowS
showsPrec :: Int -> I a -> ShowS
$cshow :: forall a. Show a => I a -> String
show :: I a -> String
$cshowList :: forall a. Show a => [I a] -> ShowS
showList :: [I a] -> ShowS
Show)
deriveShow1 ''U
deriveShow1 ''I
deriveEq1 ''U
deriveEq1 ''I
newtype AbstractTrace = AbstractTrace (NonEmpty (Trace' U))
deriving NonEmpty AbstractTrace -> AbstractTrace
AbstractTrace -> AbstractTrace -> AbstractTrace
(AbstractTrace -> AbstractTrace -> AbstractTrace)
-> (NonEmpty AbstractTrace -> AbstractTrace)
-> (forall b. Integral b => b -> AbstractTrace -> AbstractTrace)
-> Semigroup AbstractTrace
forall b. Integral b => b -> AbstractTrace -> AbstractTrace
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
$c<> :: AbstractTrace -> AbstractTrace -> AbstractTrace
<> :: AbstractTrace -> AbstractTrace -> AbstractTrace
$csconcat :: NonEmpty AbstractTrace -> AbstractTrace
sconcat :: NonEmpty AbstractTrace -> AbstractTrace
$cstimes :: forall b. Integral b => b -> AbstractTrace -> AbstractTrace
stimes :: forall b. Integral b => b -> AbstractTrace -> AbstractTrace
Semigroup via (NonEmpty (Trace' U))
deriving Int -> AbstractTrace -> ShowS
[AbstractTrace] -> ShowS
AbstractTrace -> String
(Int -> AbstractTrace -> ShowS)
-> (AbstractTrace -> String)
-> ([AbstractTrace] -> ShowS)
-> Show AbstractTrace
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AbstractTrace -> ShowS
showsPrec :: Int -> AbstractTrace -> ShowS
$cshow :: AbstractTrace -> String
show :: AbstractTrace -> String
$cshowList :: [AbstractTrace] -> ShowS
showList :: [AbstractTrace] -> ShowS
Show
foldMapSemi :: Semigroup m => (a -> m) -> NonEmpty a -> m
foldMapSemi :: forall m a. Semigroup m => (a -> m) -> NonEmpty a -> m
foldMapSemi a -> m
f (a
x :| []) = a -> m
f a
x
foldMapSemi a -> m
f (a
x :| (a
y:[a]
xs)) = a -> m
f a
x m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (a -> m) -> NonEmpty a -> m
forall m a. Semigroup m => (a -> m) -> NonEmpty a -> m
foldMapSemi a -> m
f (a
y a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
xs)
concreteTrace :: Semigroup t => (Trace' I -> t) -> AbstractTrace -> t
concreteTrace :: forall t. Semigroup t => (Trace' I -> t) -> AbstractTrace -> t
concreteTrace Trace' I -> t
c (AbstractTrace NonEmpty (Trace' U)
xs) = (Trace' U -> t) -> NonEmpty (Trace' U) -> t
forall m a. Semigroup m => (a -> m) -> NonEmpty a -> m
foldMapSemi (Trace' I -> t
c (Trace' I -> t) -> (Trace' U -> Trace' I) -> Trace' U -> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Trace' U -> Trace' I
f) NonEmpty (Trace' U)
xs where
f :: Trace' U -> Trace' I
f :: Trace' U -> Trace' I
f (ProgReadC Char
c U (Trace' U)
U) = Char -> I (Trace' I) -> Trace' I
forall (f :: * -> *). Char -> f (Trace' f) -> Trace' f
ProgReadC Char
c (I (Trace' I) -> Trace' I) -> I (Trace' I) -> Trace' I
forall a b. (a -> b) -> a -> b
$ Trace' I -> I (Trace' I)
forall a. a -> I a
I Trace' I
forall (f :: * -> *). Trace' f
TerminateC
f (ProgWriteC OptFlag
opt Set (OutputPattern 'TraceP)
os U (Trace' U)
U) = OptFlag -> Set (OutputPattern 'TraceP) -> I (Trace' I) -> Trace' I
forall (f :: * -> *).
OptFlag -> Set (OutputPattern 'TraceP) -> f (Trace' f) -> Trace' f
ProgWriteC OptFlag
opt Set (OutputPattern 'TraceP)
os (I (Trace' I) -> Trace' I) -> I (Trace' I) -> Trace' I
forall a b. (a -> b) -> a -> b
$ Trace' I -> I (Trace' I)
forall a. a -> I a
I Trace' I
forall (f :: * -> *). Trace' f
TerminateC
f Trace' U
TerminateC = Trace' I
forall (f :: * -> *). Trace' f
TerminateC
f Trace' U
OutOfInputsC = Trace' I
forall (f :: * -> *). Trace' f
OutOfInputsC
ordinaryTrace :: AbstractTrace -> Trace
ordinaryTrace :: AbstractTrace -> Trace
ordinaryTrace = (Trace' I -> Trace) -> AbstractTrace -> Trace
forall t. Semigroup t => (Trace' I -> t) -> AbstractTrace -> t
concreteTrace Trace' I -> Trace
Trace
normalizedTrace :: AbstractTrace -> NTrace
normalizedTrace :: AbstractTrace -> NTrace
normalizedTrace = (Trace' I -> NTrace) -> AbstractTrace -> NTrace
forall t. Semigroup t => (Trace' I -> t) -> AbstractTrace -> t
concreteTrace Trace' I -> NTrace
NTrace
instance Semigroup Trace where
ProgRead Char
c Trace
t <> :: Trace -> Trace -> Trace
<> Trace
t' = Char -> Trace -> Trace
ProgRead Char
c (Trace -> Trace) -> Trace -> Trace
forall a b. (a -> b) -> a -> b
$ Trace
t Trace -> Trace -> Trace
forall a. Semigroup a => a -> a -> a
<> Trace
t'
ProgWrite OptFlag
o Set (OutputPattern 'TraceP)
ts Trace
t <> Trace
t' = OptFlag -> Set (OutputPattern 'TraceP) -> Trace -> Trace
ProgWrite OptFlag
o Set (OutputPattern 'TraceP)
ts (Trace -> Trace) -> Trace -> Trace
forall a b. (a -> b) -> a -> b
$ Trace
t Trace -> Trace -> Trace
forall a. Semigroup a => a -> a -> a
<> Trace
t'
Trace
Terminate <> Trace
t' = Trace
t'
Trace
OutOfInputs <> Trace
_ = Trace
OutOfInputs
instance Semigroup NTrace where
NProgRead Char
c NTrace
t <> :: NTrace -> NTrace -> NTrace
<> NTrace
t' = Char -> NTrace -> NTrace
NProgRead Char
c (NTrace -> NTrace) -> NTrace -> NTrace
forall a b. (a -> b) -> a -> b
$ NTrace
t NTrace -> NTrace -> NTrace
forall a. Semigroup a => a -> a -> a
<> NTrace
t'
NProgWrite OptFlag
o1 Set (OutputPattern 'TraceP)
ts1 NTrace
t <> NProgWrite OptFlag
o2 Set (OutputPattern 'TraceP)
ts2 NTrace
t'
= OptFlag -> Set (OutputPattern 'TraceP) -> NTrace -> NTrace
NProgWrite
(OptFlag -> OptFlag -> OptFlag
forall a. Ord a => a -> a -> a
max OptFlag
o1 OptFlag
o2)
([Set (OutputPattern 'TraceP)] -> Set (OutputPattern 'TraceP)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set (OutputPattern 'TraceP)] -> Set (OutputPattern 'TraceP))
-> [Set (OutputPattern 'TraceP)] -> Set (OutputPattern 'TraceP)
forall a b. (a -> b) -> a -> b
$
[ Set (OutputPattern 'TraceP)
ts1 | OptFlag
o2 OptFlag -> OptFlag -> Bool
forall a. Eq a => a -> a -> Bool
== OptFlag
Optional ] [Set (OutputPattern 'TraceP)]
-> [Set (OutputPattern 'TraceP)] -> [Set (OutputPattern 'TraceP)]
forall a. [a] -> [a] -> [a]
++
[ Set (OutputPattern 'TraceP)
ts2 | OptFlag
o1 OptFlag -> OptFlag -> Bool
forall a. Eq a => a -> a -> Bool
== OptFlag
Optional ] [Set (OutputPattern 'TraceP)]
-> [Set (OutputPattern 'TraceP)] -> [Set (OutputPattern 'TraceP)]
forall a. [a] -> [a] -> [a]
++
[((OutputPattern 'TraceP, OutputPattern 'TraceP)
-> OutputPattern 'TraceP)
-> Set (OutputPattern 'TraceP, OutputPattern 'TraceP)
-> Set (OutputPattern 'TraceP)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((OutputPattern 'TraceP
-> OutputPattern 'TraceP -> OutputPattern 'TraceP)
-> (OutputPattern 'TraceP, OutputPattern 'TraceP)
-> OutputPattern 'TraceP
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry OutputPattern 'TraceP
-> OutputPattern 'TraceP -> OutputPattern 'TraceP
forall a. Semigroup a => a -> a -> a
(<>)) (Set (OutputPattern 'TraceP, OutputPattern 'TraceP)
-> Set (OutputPattern 'TraceP))
-> Set (OutputPattern 'TraceP, OutputPattern 'TraceP)
-> Set (OutputPattern 'TraceP)
forall a b. (a -> b) -> a -> b
$ Set (OutputPattern 'TraceP)
-> Set (OutputPattern 'TraceP)
-> Set (OutputPattern 'TraceP, OutputPattern 'TraceP)
forall a b. Set a -> Set b -> Set (a, b)
Set.cartesianProduct Set (OutputPattern 'TraceP)
ts1 Set (OutputPattern 'TraceP)
ts2]) NTrace
t
NTrace -> NTrace -> NTrace
forall a. Semigroup a => a -> a -> a
<> NTrace
t'
NProgWrite OptFlag
o Set (OutputPattern 'TraceP)
ts NTrace
t <> NTrace
t' = OptFlag -> Set (OutputPattern 'TraceP) -> NTrace -> NTrace
NProgWrite OptFlag
o Set (OutputPattern 'TraceP)
ts (NTrace -> NTrace) -> NTrace -> NTrace
forall a b. (a -> b) -> a -> b
$ NTrace
t NTrace -> NTrace -> NTrace
forall a. Semigroup a => a -> a -> a
<> NTrace
t'
NTrace
NTerminate <> NTrace
t' = NTrace
t'
NTrace
NOutOfInputs <> NTrace
_ = NTrace
NOutOfInputs
newtype Trace = Trace (Trace' I) deriving (Trace -> Trace -> Bool
(Trace -> Trace -> Bool) -> (Trace -> Trace -> Bool) -> Eq Trace
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Trace -> Trace -> Bool
== :: Trace -> Trace -> Bool
$c/= :: Trace -> Trace -> Bool
/= :: Trace -> Trace -> Bool
Eq, Int -> Trace -> ShowS
[Trace] -> ShowS
Trace -> String
(Int -> Trace -> ShowS)
-> (Trace -> String) -> ([Trace] -> ShowS) -> Show Trace
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Trace -> ShowS
showsPrec :: Int -> Trace -> ShowS
$cshow :: Trace -> String
show :: Trace -> String
$cshowList :: [Trace] -> ShowS
showList :: [Trace] -> ShowS
Show)
newtype NTrace = NTrace (Trace' I) deriving (NTrace -> NTrace -> Bool
(NTrace -> NTrace -> Bool)
-> (NTrace -> NTrace -> Bool) -> Eq NTrace
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NTrace -> NTrace -> Bool
== :: NTrace -> NTrace -> Bool
$c/= :: NTrace -> NTrace -> Bool
/= :: NTrace -> NTrace -> Bool
Eq, Int -> NTrace -> ShowS
[NTrace] -> ShowS
NTrace -> String
(Int -> NTrace -> ShowS)
-> (NTrace -> String) -> ([NTrace] -> ShowS) -> Show NTrace
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NTrace -> ShowS
showsPrec :: Int -> NTrace -> ShowS
$cshow :: NTrace -> String
show :: NTrace -> String
$cshowList :: [NTrace] -> ShowS
showList :: [NTrace] -> ShowS
Show)
data Trace' f
= ProgReadC Char (f (Trace' f))
| ProgWriteC OptFlag (Set (OutputPattern 'TraceP)) (f (Trace' f))
| TerminateC
| OutOfInputsC
instance Eq1 f => Eq (Trace' f) where
ProgReadC Char
c1 f (Trace' f)
t1 == :: Trace' f -> Trace' f -> Bool
== ProgReadC Char
c2 f (Trace' f)
t2 = Char
c1 Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
c2 Bool -> Bool -> Bool
&& f (Trace' f)
t1 f (Trace' f) -> f (Trace' f) -> Bool
forall (f :: * -> *) a. (Eq1 f, Eq a) => f a -> f a -> Bool
`eq1` f (Trace' f)
t2
ProgWriteC OptFlag
o1 Set (OutputPattern 'TraceP)
os1 f (Trace' f)
t1 == ProgWriteC OptFlag
o2 Set (OutputPattern 'TraceP)
os2 f (Trace' f)
t2 = OptFlag
o1 OptFlag -> OptFlag -> Bool
forall a. Eq a => a -> a -> Bool
== OptFlag
o2 Bool -> Bool -> Bool
&& Set (OutputPattern 'TraceP)
os1 Set (OutputPattern 'TraceP) -> Set (OutputPattern 'TraceP) -> Bool
forall a. Eq a => a -> a -> Bool
== Set (OutputPattern 'TraceP)
os2 Bool -> Bool -> Bool
&& f (Trace' f)
t1 f (Trace' f) -> f (Trace' f) -> Bool
forall (f :: * -> *) a. (Eq1 f, Eq a) => f a -> f a -> Bool
`eq1` f (Trace' f)
t2
Trace' f
OutOfInputsC == Trace' f
OutOfInputsC = Bool
True
Trace' f
TerminateC == Trace' f
TerminateC = Bool
True
Trace' f
_ == Trace' f
_ = Bool
False
instance Show1 f => Show (Trace' f) where
showsPrec :: Int -> Trace' f -> ShowS
showsPrec Int
prec (ProgReadC Char
c f (Trace' f)
t) = String -> ShowS
showString String
"ProgReadC " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
forall a. Show a => a -> ShowS
shows Char
c ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> f (Trace' f) -> ShowS
forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1 Int
prec f (Trace' f)
t
showsPrec Int
prec (ProgWriteC OptFlag
opt Set (OutputPattern 'TraceP)
os f (Trace' f)
t) = String -> ShowS
showString String
"ProgWriteC " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OptFlag -> ShowS
forall a. Show a => a -> ShowS
shows OptFlag
opt ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (OutputPattern 'TraceP) -> ShowS
forall a. Show a => a -> ShowS
shows Set (OutputPattern 'TraceP)
os ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' ' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> f (Trace' f) -> ShowS
forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1 Int
prec f (Trace' f)
t
showsPrec Int
_ Trace' f
TerminateC = String -> ShowS
showString String
"TerminateC"
showsPrec Int
_ Trace' f
OutOfInputsC = String -> ShowS
showString String
"OutOfInputsC"
progRead :: Char -> AbstractTrace
progRead :: Char -> AbstractTrace
progRead Char
c = NonEmpty (Trace' U) -> AbstractTrace
AbstractTrace (NonEmpty (Trace' U) -> AbstractTrace)
-> NonEmpty (Trace' U) -> AbstractTrace
forall a b. (a -> b) -> a -> b
$ Char -> U (Trace' U) -> Trace' U
forall (f :: * -> *). Char -> f (Trace' f) -> Trace' f
ProgReadC Char
c U (Trace' U)
forall {k} (a :: k). U a
U Trace' U -> [Trace' U] -> NonEmpty (Trace' U)
forall a. a -> [a] -> NonEmpty a
:| []
progWrite :: OptFlag -> Set (OutputPattern 'TraceP) -> AbstractTrace
progWrite :: OptFlag -> Set (OutputPattern 'TraceP) -> AbstractTrace
progWrite OptFlag
o Set (OutputPattern 'TraceP)
ts = NonEmpty (Trace' U) -> AbstractTrace
AbstractTrace (NonEmpty (Trace' U) -> AbstractTrace)
-> NonEmpty (Trace' U) -> AbstractTrace
forall a b. (a -> b) -> a -> b
$ OptFlag -> Set (OutputPattern 'TraceP) -> U (Trace' U) -> Trace' U
forall (f :: * -> *).
OptFlag -> Set (OutputPattern 'TraceP) -> f (Trace' f) -> Trace' f
ProgWriteC OptFlag
o Set (OutputPattern 'TraceP)
ts U (Trace' U)
forall {k} (a :: k). U a
U Trace' U -> [Trace' U] -> NonEmpty (Trace' U)
forall a. a -> [a] -> NonEmpty a
:| []
terminate :: AbstractTrace
terminate :: AbstractTrace
terminate = NonEmpty (Trace' U) -> AbstractTrace
AbstractTrace (NonEmpty (Trace' U) -> AbstractTrace)
-> NonEmpty (Trace' U) -> AbstractTrace
forall a b. (a -> b) -> a -> b
$ Trace' U
forall (f :: * -> *). Trace' f
TerminateC Trace' U -> [Trace' U] -> NonEmpty (Trace' U)
forall a. a -> [a] -> NonEmpty a
:| []
outOfInputs :: AbstractTrace
outOfInputs :: AbstractTrace
outOfInputs = NonEmpty (Trace' U) -> AbstractTrace
AbstractTrace (NonEmpty (Trace' U) -> AbstractTrace)
-> NonEmpty (Trace' U) -> AbstractTrace
forall a b. (a -> b) -> a -> b
$ Trace' U
forall (f :: * -> *). Trace' f
OutOfInputsC Trace' U -> [Trace' U] -> NonEmpty (Trace' U)
forall a. a -> [a] -> NonEmpty a
:| []
data MatchResult
= MatchSuccessful
| InputMismatch NTrace NTrace
| OutputMismatch NTrace NTrace
| AlignmentMismatch NTrace (Maybe NTrace) NTrace
| TerminationMismatch NTrace (Maybe NTrace) NTrace
deriving (MatchResult -> MatchResult -> Bool
(MatchResult -> MatchResult -> Bool)
-> (MatchResult -> MatchResult -> Bool) -> Eq MatchResult
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MatchResult -> MatchResult -> Bool
== :: MatchResult -> MatchResult -> Bool
$c/= :: MatchResult -> MatchResult -> Bool
/= :: MatchResult -> MatchResult -> Bool
Eq,Int -> MatchResult -> ShowS
[MatchResult] -> ShowS
MatchResult -> String
(Int -> MatchResult -> ShowS)
-> (MatchResult -> String)
-> ([MatchResult] -> ShowS)
-> Show MatchResult
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MatchResult -> ShowS
showsPrec :: Int -> MatchResult -> ShowS
$cshow :: MatchResult -> String
show :: MatchResult -> String
$cshowList :: [MatchResult] -> ShowS
showList :: [MatchResult] -> ShowS
Show)
isSuccessfulMatch :: MatchResult -> Bool
isSuccessfulMatch :: MatchResult -> Bool
isSuccessfulMatch MatchResult
MatchSuccessful = Bool
True
isSuccessfulMatch MatchResult
_ = Bool
False
isInputMismatch :: MatchResult -> Bool
isInputMismatch :: MatchResult -> Bool
isInputMismatch InputMismatch{} = Bool
True
isInputMismatch MatchResult
_ = Bool
False
isOutputMismatch :: MatchResult -> Bool
isOutputMismatch :: MatchResult -> Bool
isOutputMismatch OutputMismatch{} = Bool
True
isOutputMismatch MatchResult
_ = Bool
False
isAlignmentMismatch :: MatchResult -> Bool
isAlignmentMismatch :: MatchResult -> Bool
isAlignmentMismatch AlignmentMismatch{} = Bool
True
isAlignmentMismatch MatchResult
_ = Bool
False
isTerminationMismatch :: MatchResult -> Bool
isTerminationMismatch :: MatchResult -> Bool
isTerminationMismatch TerminationMismatch{} = Bool
True
isTerminationMismatch MatchResult
_ = Bool
False
instance Semigroup MatchResult where
MatchResult
a <> :: MatchResult -> MatchResult -> MatchResult
<> MatchResult
b = case MatchResult -> MatchResult -> Either MatchResult MatchResult
choose MatchResult
a MatchResult
b of
Left MatchResult
x -> MatchResult
x
Right MatchResult
x -> MatchResult
x
choose :: MatchResult -> MatchResult -> Either MatchResult MatchResult
choose :: MatchResult -> MatchResult -> Either MatchResult MatchResult
choose MatchResult
MatchSuccessful MatchResult
_ = MatchResult -> Either MatchResult MatchResult
forall a b. a -> Either a b
Left MatchResult
MatchSuccessful
choose MatchResult
_ MatchResult
MatchSuccessful = MatchResult -> Either MatchResult MatchResult
forall a b. b -> Either a b
Right MatchResult
MatchSuccessful
choose MatchResult
r MatchResult
_ = MatchResult -> Either MatchResult MatchResult
forall a b. a -> Either a b
Left MatchResult
r
addExpect :: NTrace -> (MatchResult,HasConsumed) -> (MatchResult,HasConsumed)
addExpect :: NTrace -> (MatchResult, Bool) -> (MatchResult, Bool)
addExpect NTrace
s' (AlignmentMismatch NTrace
t Maybe NTrace
Nothing NTrace
s,Bool
False) = (NTrace -> Maybe NTrace -> NTrace -> MatchResult
AlignmentMismatch NTrace
t (NTrace -> Maybe NTrace
forall a. a -> Maybe a
Just NTrace
s') NTrace
s,Bool
False)
addExpect NTrace
s' (TerminationMismatch NTrace
t Maybe NTrace
Nothing NTrace
s,Bool
False) = (NTrace -> Maybe NTrace -> NTrace -> MatchResult
TerminationMismatch NTrace
t (NTrace -> Maybe NTrace
forall a. a -> Maybe a
Just NTrace
s') NTrace
s,Bool
False)
addExpect NTrace
_ (MatchResult, Bool)
r = (MatchResult, Bool)
r
type HasConsumed = Bool
covers :: NTrace -> NTrace -> MatchResult
covers :: NTrace -> NTrace -> MatchResult
covers NTrace
s NTrace
t = (MatchResult, Bool) -> MatchResult
forall a b. (a, b) -> a
fst ((MatchResult, Bool) -> MatchResult)
-> (MatchResult, Bool) -> MatchResult
forall a b. (a -> b) -> a -> b
$ NTrace -> NTrace -> (MatchResult, Bool)
covers' NTrace
s NTrace
t
where
covers' :: NTrace -> NTrace -> (MatchResult, HasConsumed)
covers' :: NTrace -> NTrace -> (MatchResult, Bool)
covers' s :: NTrace
s@(NProgRead Char
i NTrace
t1) t :: NTrace
t@(NProgRead Char
j NTrace
t2)
| Char
i Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
j = (MatchResult, Bool) -> (MatchResult, Bool)
hasConsumed ((MatchResult, Bool) -> (MatchResult, Bool))
-> (MatchResult, Bool) -> (MatchResult, Bool)
forall a b. (a -> b) -> a -> b
$ NTrace
t1 NTrace -> NTrace -> (MatchResult, Bool)
`covers'` NTrace
t2
| Bool
otherwise = MatchResult -> (MatchResult, Bool)
noConsume (MatchResult -> (MatchResult, Bool))
-> MatchResult -> (MatchResult, Bool)
forall a b. (a -> b) -> a -> b
$ NTrace -> NTrace -> MatchResult
InputMismatch NTrace
s NTrace
t
covers' s :: NTrace
s@(NProgWrite OptFlag
Mandatory Set (OutputPattern 'TraceP)
is NTrace
t1) t :: NTrace
t@(NProgWrite OptFlag
Mandatory Set (OutputPattern 'TraceP)
js NTrace
t2)
| (OutputPattern 'TraceP -> Bool)
-> Set (OutputPattern 'TraceP) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\OutputPattern 'TraceP
j -> (OutputPattern 'TraceP -> Bool)
-> Set (OutputPattern 'TraceP) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (OutputPattern 'TraceP -> OutputPattern 'TraceP -> Bool
>: OutputPattern 'TraceP
j) Set (OutputPattern 'TraceP)
is) Set (OutputPattern 'TraceP)
js = (MatchResult, Bool) -> (MatchResult, Bool)
hasConsumed ((MatchResult, Bool) -> (MatchResult, Bool))
-> (MatchResult, Bool) -> (MatchResult, Bool)
forall a b. (a -> b) -> a -> b
$ NTrace
t1 NTrace -> NTrace -> (MatchResult, Bool)
`covers'` NTrace
t2
| Bool
otherwise = MatchResult -> (MatchResult, Bool)
noConsume (MatchResult -> (MatchResult, Bool))
-> MatchResult -> (MatchResult, Bool)
forall a b. (a -> b) -> a -> b
$ NTrace -> NTrace -> MatchResult
OutputMismatch NTrace
s NTrace
t
covers' s :: NTrace
s@(NProgWrite OptFlag
Optional Set (OutputPattern 'TraceP)
is NTrace
t1) NTrace
t =
let
(MatchResult
r1,Bool
c1) = NTrace -> (MatchResult, Bool) -> (MatchResult, Bool)
addExpect NTrace
s (NTrace
t1 NTrace -> NTrace -> (MatchResult, Bool)
`covers'` NTrace
t)
(MatchResult
r2,Bool
c2) = (OptFlag -> Set (OutputPattern 'TraceP) -> NTrace -> NTrace
NProgWrite OptFlag
Mandatory Set (OutputPattern 'TraceP)
is NTrace
t1 NTrace -> NTrace -> (MatchResult, Bool)
`covers'` NTrace
t)
in case MatchResult -> MatchResult -> Either MatchResult MatchResult
choose MatchResult
r1 MatchResult
r2 of
Left MatchResult
_ -> (MatchResult
r1,Bool
c1)
Right MatchResult
_ -> (MatchResult
r2,Bool
c2)
covers' NTrace
s t :: NTrace
t@(NProgWrite OptFlag
Optional Set (OutputPattern 'TraceP)
_ NTrace
_) = MatchResult -> (MatchResult, Bool)
noConsume (MatchResult -> (MatchResult, Bool))
-> MatchResult -> (MatchResult, Bool)
forall a b. (a -> b) -> a -> b
$ NTrace -> NTrace -> MatchResult
OutputMismatch NTrace
s NTrace
t
covers' NTrace
NTerminate NTrace
NTerminate = (MatchResult
MatchSuccessful,Bool
True)
covers' s :: NTrace
s@NTrace
NTerminate NTrace
t = MatchResult -> (MatchResult, Bool)
noConsume (MatchResult -> (MatchResult, Bool))
-> MatchResult -> (MatchResult, Bool)
forall a b. (a -> b) -> a -> b
$ NTrace -> Maybe NTrace -> NTrace -> MatchResult
TerminationMismatch NTrace
s Maybe NTrace
forall a. Maybe a
Nothing NTrace
t
covers' NTrace
NOutOfInputs NTrace
NOutOfInputs = (MatchResult
MatchSuccessful,Bool
True)
covers' NTrace
s NTrace
t = MatchResult -> (MatchResult, Bool)
noConsume (MatchResult -> (MatchResult, Bool))
-> MatchResult -> (MatchResult, Bool)
forall a b. (a -> b) -> a -> b
$ NTrace -> Maybe NTrace -> NTrace -> MatchResult
AlignmentMismatch NTrace
s Maybe NTrace
forall a. Maybe a
Nothing NTrace
t
noConsume :: MatchResult -> (MatchResult,HasConsumed)
noConsume :: MatchResult -> (MatchResult, Bool)
noConsume = (,Bool
False)
hasConsumed :: (MatchResult,HasConsumed) -> (MatchResult,HasConsumed)
hasConsumed :: (MatchResult, Bool) -> (MatchResult, Bool)
hasConsumed = (Bool -> Bool) -> (MatchResult, Bool) -> (MatchResult, Bool)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True)
instance Pretty MatchResult where
pPrint :: MatchResult -> Doc
pPrint = (Doc -> Doc -> Doc) -> MatchResult -> Doc
pPrintMatchResult Doc -> Doc -> Doc
(<+>)
instance Pretty NTrace where
pPrint :: NTrace -> Doc
pPrint = NTrace -> Doc
showTraceN
instance Pretty Trace where
pPrint :: Trace -> Doc
pPrint = Trace -> Doc
showTrace
pPrintMatchResult :: (Doc -> Doc -> Doc) -> MatchResult -> Doc
pPrintMatchResult :: (Doc -> Doc -> Doc) -> MatchResult -> Doc
pPrintMatchResult = Bool -> (Doc -> Doc -> Doc) -> MatchResult -> Doc
pPrintMatchResult' Bool
False
pPrintMatchResultSimple :: (Doc -> Doc -> Doc) -> MatchResult -> Doc
pPrintMatchResultSimple :: (Doc -> Doc -> Doc) -> MatchResult -> Doc
pPrintMatchResultSimple = Bool -> (Doc -> Doc -> Doc) -> MatchResult -> Doc
pPrintMatchResult' Bool
True
pPrintMatchResult' :: Bool -> (Doc -> Doc -> Doc) -> MatchResult -> Doc
pPrintMatchResult' :: Bool -> (Doc -> Doc -> Doc) -> MatchResult -> Doc
pPrintMatchResult' Bool
_ Doc -> Doc -> Doc
_ MatchResult
MatchSuccessful = String -> Doc
text String
"MatchSuccessful"
pPrintMatchResult' Bool
simple Doc -> Doc -> Doc
f (InputMismatch NTrace
s NTrace
t) = String -> Doc
text String
"InputMismatch:" Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (Bool
-> (Doc -> Doc -> Doc) -> NTrace -> Maybe NTrace -> NTrace -> Doc
reportMismatch Bool
simple Doc -> Doc -> Doc
f NTrace
s Maybe NTrace
forall a. Maybe a
Nothing NTrace
t)
pPrintMatchResult' Bool
simple Doc -> Doc -> Doc
f (OutputMismatch NTrace
s NTrace
t) = String -> Doc
text String
"OutputMismatch:" Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (Bool -> (Doc -> Doc -> Doc) -> NTrace -> NTrace -> Doc
reportOutputMismatch Bool
simple Doc -> Doc -> Doc
f NTrace
s NTrace
t)
pPrintMatchResult' Bool
simple Doc -> Doc -> Doc
f (AlignmentMismatch NTrace
s Maybe NTrace
s' NTrace
t) = String -> Doc
text String
"AlignmentMismatch:" Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (Bool
-> (Doc -> Doc -> Doc) -> NTrace -> Maybe NTrace -> NTrace -> Doc
reportMismatch Bool
simple Doc -> Doc -> Doc
f NTrace
s Maybe NTrace
s' NTrace
t)
pPrintMatchResult' Bool
simple Doc -> Doc -> Doc
f (TerminationMismatch NTrace
s Maybe NTrace
s' NTrace
t) = String -> Doc
text String
"TerminationMismatch:" Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (Bool
-> (Doc -> Doc -> Doc) -> NTrace -> Maybe NTrace -> NTrace -> Doc
reportMismatch Bool
simple Doc -> Doc -> Doc
f NTrace
s Maybe NTrace
s' NTrace
t)
reportMismatch :: Bool -> (Doc -> Doc -> Doc) -> NTrace -> Maybe NTrace -> NTrace -> Doc
reportMismatch :: Bool
-> (Doc -> Doc -> Doc) -> NTrace -> Maybe NTrace -> NTrace -> Doc
reportMismatch Bool
simple Doc -> Doc -> Doc
f NTrace
s Maybe NTrace
s' NTrace
t = [Doc] -> Doc
vcat
[ String -> Doc
text String
"Expected:"
, Int -> Doc -> Doc
nest Int
2 (Doc -> (NTrace -> Doc) -> Maybe NTrace -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
forall a. Monoid a => a
mempty ((Doc -> Doc -> Doc
`f` String -> Doc
text String
"or") (Doc -> Doc) -> (NTrace -> Doc) -> NTrace -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> NTrace -> Doc
pPrintTraceNHead Bool
simple) Maybe NTrace
s' Doc -> Doc -> Doc
<+> Bool -> NTrace -> Doc
pPrintTraceNHead Bool
simple NTrace
s)
, String -> Doc
text String
"Got:"
, Int -> Doc -> Doc
nest Int
2 (Bool -> NTrace -> Doc
pPrintTraceNHead Bool
simple NTrace
t)
]
reportOutputMismatch :: Bool -> (Doc -> Doc -> Doc) -> NTrace -> NTrace -> Doc
reportOutputMismatch :: Bool -> (Doc -> Doc -> Doc) -> NTrace -> NTrace -> Doc
reportOutputMismatch Bool
simple Doc -> Doc -> Doc
f NTrace
s NTrace
t = Bool -> NTrace -> Doc
pPrintTraceNHead Bool
simple NTrace
t Doc -> Doc -> Doc
`f` String -> Doc
text String
"is not covered by" Doc -> Doc -> Doc
`f` Bool -> NTrace -> Doc
pPrintTraceNHead Bool
simple NTrace
s
pPrintTraceNHead :: Bool -> NTrace -> Doc
pPrintTraceNHead :: Bool -> NTrace -> Doc
pPrintTraceNHead Bool
simple (NTrace Trace' I
t) = Bool -> (Doc -> Doc -> Doc) -> (Trace' I -> Doc) -> Trace' I -> Doc
showConcreteTraceHead Bool
simple Doc -> Doc -> Doc
(<+>) (Doc -> Trace' I -> Doc
forall a b. a -> b -> a
const (Doc -> Trace' I -> Doc) -> Doc -> Trace' I -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"") Trace' I
t
showTraceN :: NTrace -> Doc
showTraceN :: NTrace -> Doc
showTraceN = (Doc -> Doc -> Doc) -> NTrace -> Doc
showTraceN' Doc -> Doc -> Doc
(<+>)
showTraceN' :: (Doc -> Doc -> Doc) -> NTrace -> Doc
showTraceN' :: (Doc -> Doc -> Doc) -> NTrace -> Doc
showTraceN' Doc -> Doc -> Doc
op (NTrace Trace' I
t) = Bool -> (Doc -> Doc -> Doc) -> Trace' I -> Doc
showDeep Bool
False Doc -> Doc -> Doc
op Trace' I
t
showTraceNSimple :: NTrace -> Doc
showTraceNSimple :: NTrace -> Doc
showTraceNSimple = (Doc -> Doc -> Doc) -> NTrace -> Doc
showTraceNSimple' Doc -> Doc -> Doc
(<+>)
showTraceNSimple' :: (Doc -> Doc -> Doc) -> NTrace -> Doc
showTraceNSimple' :: (Doc -> Doc -> Doc) -> NTrace -> Doc
showTraceNSimple' Doc -> Doc -> Doc
op (NTrace Trace' I
t) = Bool -> (Doc -> Doc -> Doc) -> Trace' I -> Doc
showDeep Bool
True Doc -> Doc -> Doc
op Trace' I
t
showTrace :: Trace -> Doc
showTrace :: Trace -> Doc
showTrace = (Doc -> Doc -> Doc) -> Trace -> Doc
showTrace' Doc -> Doc -> Doc
(<+>)
showTrace' :: (Doc -> Doc -> Doc) -> Trace -> Doc
showTrace' :: (Doc -> Doc -> Doc) -> Trace -> Doc
showTrace' Doc -> Doc -> Doc
op (Trace Trace' I
t) = Bool -> (Doc -> Doc -> Doc) -> Trace' I -> Doc
showDeep Bool
False Doc -> Doc -> Doc
op Trace' I
t
showTraceSimple :: Trace -> Doc
showTraceSimple :: Trace -> Doc
showTraceSimple = (Doc -> Doc -> Doc) -> Trace -> Doc
showTraceSimple' Doc -> Doc -> Doc
(<+>)
showTraceSimple' :: (Doc -> Doc -> Doc) -> Trace -> Doc
showTraceSimple' :: (Doc -> Doc -> Doc) -> Trace -> Doc
showTraceSimple' Doc -> Doc -> Doc
op (Trace Trace' I
t) = Bool -> (Doc -> Doc -> Doc) -> Trace' I -> Doc
showDeep Bool
True Doc -> Doc -> Doc
op Trace' I
t
showDeep :: Bool -> (Doc -> Doc -> Doc) -> Trace' I -> Doc
showDeep :: Bool -> (Doc -> Doc -> Doc) -> Trace' I -> Doc
showDeep Bool
simple Doc -> Doc -> Doc
f = ((Trace' I -> Doc) -> Trace' I -> Doc) -> Trace' I -> Doc
forall a. (a -> a) -> a
fix (Bool -> (Doc -> Doc -> Doc) -> (Trace' I -> Doc) -> Trace' I -> Doc
showConcreteTraceHead Bool
simple Doc -> Doc -> Doc
f)
showConcreteTraceHead :: Bool -> (Doc -> Doc -> Doc) -> (Trace' I -> Doc) -> Trace' I -> Doc
showConcreteTraceHead :: Bool -> (Doc -> Doc -> Doc) -> (Trace' I -> Doc) -> Trace' I -> Doc
showConcreteTraceHead Bool
simple Doc -> Doc -> Doc
op Trace' I -> Doc
f (ProgWriteC OptFlag
Optional Set (OutputPattern 'TraceP)
ts (I Trace' I
t'))
| Bool
simple = Trace' I -> Doc
f Trace' I
t'
| Bool
otherwise = (Doc
"(!{"Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
hcat (Doc -> [Doc] -> [Doc]
punctuate Doc
"," (String -> Doc
text (String -> Doc)
-> (OutputPattern 'TraceP -> String)
-> OutputPattern 'TraceP
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OutputPattern 'TraceP -> String
forall (k :: PatternKind). OutputPattern k -> String
showPattern (OutputPattern 'TraceP -> Doc) -> [OutputPattern 'TraceP] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (OutputPattern 'TraceP) -> [OutputPattern 'TraceP]
forall a. Set a -> [a]
Set.toList Set (OutputPattern 'TraceP)
ts)) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"})") Doc -> Doc -> Doc
`op` Trace' I -> Doc
f Trace' I
t'
showConcreteTraceHead Bool
simple Doc -> Doc -> Doc
op Trace' I -> Doc
f (ProgWriteC OptFlag
Mandatory Set (OutputPattern 'TraceP)
ts (I Trace' I
t'))
| Bool
simple = (Doc
"!\""Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> ([Doc] -> Doc
forall a. HasCallStack => [a] -> a
head ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (String -> Doc)
-> (OutputPattern 'TraceP -> String)
-> OutputPattern 'TraceP
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OutputPattern 'TraceP -> String
forall (k :: PatternKind). OutputPattern k -> String
showPatternSimple (OutputPattern 'TraceP -> Doc) -> [OutputPattern 'TraceP] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (OutputPattern 'TraceP) -> [OutputPattern 'TraceP]
forall a. Set a -> [a]
Set.toList Set (OutputPattern 'TraceP)
ts) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"\"") Doc -> Doc -> Doc
`op` Trace' I -> Doc
f Trace' I
t'
| Bool
otherwise = (Doc
"!{"Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
hcat (Doc -> [Doc] -> [Doc]
punctuate Doc
"," (String -> Doc
text (String -> Doc)
-> (OutputPattern 'TraceP -> String)
-> OutputPattern 'TraceP
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OutputPattern 'TraceP -> String
forall (k :: PatternKind). OutputPattern k -> String
showPattern (OutputPattern 'TraceP -> Doc) -> [OutputPattern 'TraceP] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (OutputPattern 'TraceP) -> [OutputPattern 'TraceP]
forall a. Set a -> [a]
Set.toList Set (OutputPattern 'TraceP)
ts)) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"}" ) Doc -> Doc -> Doc
`op` Trace' I -> Doc
f Trace' I
t'
showConcreteTraceHead Bool
_ Doc -> Doc -> Doc
_ Trace' I -> Doc
_ Trace' I
TerminateC = Doc
"stop"
showConcreteTraceHead Bool
_ Doc -> Doc -> Doc
_ Trace' I -> Doc
_ Trace' I
OutOfInputsC = Doc
"?<unknown input>"
showConcreteTraceHead Bool
simple Doc -> Doc -> Doc
op Trace' I -> Doc
f (ProgReadC Char
x I (Trace' I)
t') = Bool -> (Trace' I -> Doc) -> Trace' I -> String -> Doc
showConcreteTraceRead Bool
simple Trace' I -> Doc
f (Char -> I (Trace' I) -> Trace' I
forall (f :: * -> *). Char -> f (Trace' f) -> Trace' f
ProgReadC Char
x I (Trace' I)
t') String
""
where
showConcreteTraceRead :: Bool -> (Trace' I -> Doc) -> Trace' I -> String -> Doc
showConcreteTraceRead :: Bool -> (Trace' I -> Doc) -> Trace' I -> String -> Doc
showConcreteTraceRead Bool
simple Trace' I -> Doc
f (ProgReadC Char
'\n' (I Trace' I
t)) String
s = (Doc
"?" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text (ShowS
forall a. [a] -> [a]
reverse String
s) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (if Bool
simple then Doc
"" else Doc
"\\n")) Doc -> Doc -> Doc
`op` Trace' I -> Doc
f Trace' I
t
showConcreteTraceRead Bool
simple Trace' I -> Doc
f (ProgReadC Char
x (I Trace' I
t)) String
s = Bool -> (Trace' I -> Doc) -> Trace' I -> String -> Doc
showConcreteTraceRead Bool
simple Trace' I -> Doc
f Trace' I
t (Char
xChar -> ShowS
forall a. a -> [a] -> [a]
:String
s)
showConcreteTraceRead Bool
simple Trace' I -> Doc
f Trace' I
t String
"" = Bool -> (Doc -> Doc -> Doc) -> (Trace' I -> Doc) -> Trace' I -> Doc
showConcreteTraceHead Bool
simple Doc -> Doc -> Doc
op Trace' I -> Doc
f Trace' I
t
showConcreteTraceRead Bool
_ Trace' I -> Doc
f Trace' I
t String
s = (Doc
"?" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
s) Doc -> Doc -> Doc
`op` Trace' I -> Doc
f Trace' I
t
isTerminating :: Trace -> Bool
isTerminating :: Trace -> Bool
isTerminating (ProgRead Char
_ Trace
t) = Trace -> Bool
isTerminating Trace
t
isTerminating (ProgWrite OptFlag
_ Set (OutputPattern 'TraceP)
_ Trace
t) = Trace -> Bool
isTerminating Trace
t
isTerminating Trace
Terminate = Bool
True
isTerminating Trace
OutOfInputs = Bool
False
isTerminatingN :: NTrace -> Bool
isTerminatingN :: NTrace -> Bool
isTerminatingN (NProgRead Char
_ NTrace
t) = NTrace -> Bool
isTerminatingN NTrace
t
isTerminatingN (NProgWrite OptFlag
_ Set (OutputPattern 'TraceP)
_ NTrace
t) = NTrace -> Bool
isTerminatingN NTrace
t
isTerminatingN NTrace
NTerminate = Bool
True
isTerminatingN NTrace
NOutOfInputs = Bool
False
inputSequence :: Trace -> [String]
inputSequence :: Trace -> [String]
inputSequence = String -> Trace -> [String]
go String
"" where
go :: String -> Trace -> [String]
go String
cs (ProgRead Char
'\n' Trace
t) = ShowS
forall a. [a] -> [a]
reverse String
cs String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String -> Trace -> [String]
go String
"" Trace
t
go String
cs (ProgRead Char
c Trace
t) = String -> Trace -> [String]
go (Char
cChar -> ShowS
forall a. a -> [a] -> [a]
:String
cs) Trace
t
go String
"" (ProgWrite OptFlag
_ Set (OutputPattern 'TraceP)
_ Trace
t) = String -> Trace -> [String]
go String
"" Trace
t
go String
cs (ProgWrite OptFlag
_ Set (OutputPattern 'TraceP)
_ Trace
t) = ShowS
forall a. [a] -> [a]
reverse String
cs String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String -> Trace -> [String]
go String
"" Trace
t
go String
"" Trace
Terminate = []
go String
cs Trace
Terminate = [ShowS
forall a. [a] -> [a]
reverse String
cs]
go String
"" Trace
OutOfInputs = []
go String
cs Trace
OutOfInputs = [ShowS
forall a. [a] -> [a]
reverse String
cs]
inputSequenceN :: NTrace -> [String]
inputSequenceN :: NTrace -> [String]
inputSequenceN = String -> NTrace -> [String]
go String
"" where
go :: String -> NTrace -> [String]
go String
cs (NProgRead Char
'\n' NTrace
t) = ShowS
forall a. [a] -> [a]
reverse String
cs String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String -> NTrace -> [String]
go String
"" NTrace
t
go String
cs (NProgRead Char
c NTrace
t) = String -> NTrace -> [String]
go (Char
cChar -> ShowS
forall a. a -> [a] -> [a]
:String
cs) NTrace
t
go String
"" (NProgWrite OptFlag
_ Set (OutputPattern 'TraceP)
_ NTrace
t) = String -> NTrace -> [String]
go String
"" NTrace
t
go String
cs (NProgWrite OptFlag
_ Set (OutputPattern 'TraceP)
_ NTrace
t) = ShowS
forall a. [a] -> [a]
reverse String
cs String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String -> NTrace -> [String]
go String
"" NTrace
t
go String
"" NTrace
NTerminate = []
go String
cs NTrace
NTerminate = [ShowS
forall a. [a] -> [a]
reverse String
cs]
go String
"" NTrace
NOutOfInputs = []
go String
cs NTrace
NOutOfInputs = [ShowS
forall a. [a] -> [a]
reverse String
cs]
nextInput :: Trace -> Maybe (String,Trace)
nextInput :: Trace -> Maybe (String, Trace)
nextInput (ProgRead Char
'\n' Trace
t) = (String, Trace) -> Maybe (String, Trace)
forall a. a -> Maybe a
Just (String
"\n",Trace
t)
nextInput (ProgRead Char
c Trace
t) = case Trace -> Maybe (String, Trace)
nextInput Trace
t of
Just (String
s,Trace
t) -> (String, Trace) -> Maybe (String, Trace)
forall a. a -> Maybe a
Just (Char
cChar -> ShowS
forall a. a -> [a] -> [a]
:String
s,Trace
t)
Maybe (String, Trace)
Nothing -> (String, Trace) -> Maybe (String, Trace)
forall a. a -> Maybe a
Just ([Char
c],Trace
t)
nextInput Trace
_ = Maybe (String, Trace)
forall a. Maybe a
Nothing
nextInputN :: NTrace -> Maybe (String,NTrace)
nextInputN :: NTrace -> Maybe (String, NTrace)
nextInputN (NProgRead Char
'\n' NTrace
t) = (String, NTrace) -> Maybe (String, NTrace)
forall a. a -> Maybe a
Just (String
"\n",NTrace
t)
nextInputN (NProgRead Char
c NTrace
t) = case NTrace -> Maybe (String, NTrace)
nextInputN NTrace
t of
Just (String
s,NTrace
t) -> (String, NTrace) -> Maybe (String, NTrace)
forall a. a -> Maybe a
Just (Char
cChar -> ShowS
forall a. a -> [a] -> [a]
:String
s,NTrace
t)
Maybe (String, NTrace)
Nothing -> (String, NTrace) -> Maybe (String, NTrace)
forall a. a -> Maybe a
Just ([Char
c],NTrace
t)
nextInputN NTrace
_ = Maybe (String, NTrace)
forall a. Maybe a
Nothing
pattern Terminate :: Trace
pattern $mTerminate :: forall {r}. Trace -> ((# #) -> r) -> ((# #) -> r) -> r
$bTerminate :: Trace
Terminate = Trace TerminateC
pattern OutOfInputs :: Trace
pattern $mOutOfInputs :: forall {r}. Trace -> ((# #) -> r) -> ((# #) -> r) -> r
$bOutOfInputs :: Trace
OutOfInputs = Trace OutOfInputsC
{-# COMPLETE ProgReadString, ProgWrite, Terminate, OutOfInputs #-}
pattern ProgReadString :: String -> Trace -> Trace
pattern $mProgReadString :: forall {r}. Trace -> (String -> Trace -> r) -> ((# #) -> r) -> r
$bProgReadString :: String -> Trace -> Trace
ProgReadString s t <- (nextInput -> Just (s,t)) where
ProgReadString String
s Trace
t = (Char -> Trace -> Trace) -> Trace -> String -> Trace
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Char -> Trace -> Trace
ProgRead Trace
t String
s
{-# COMPLETE ProgRead, ProgWrite, Terminate, OutOfInputs #-}
pattern ProgRead :: Char -> Trace -> Trace
pattern $mProgRead :: forall {r}. Trace -> (Char -> Trace -> r) -> ((# #) -> r) -> r
$bProgRead :: Char -> Trace -> Trace
ProgRead c t <- Trace (ProgReadC c (I (Trace -> t))) where
ProgRead Char
c (Trace Trace' I
t) = Trace' I -> Trace
Trace (Trace' I -> Trace) -> Trace' I -> Trace
forall a b. (a -> b) -> a -> b
$ Char -> I (Trace' I) -> Trace' I
forall (f :: * -> *). Char -> f (Trace' f) -> Trace' f
ProgReadC Char
c (I (Trace' I) -> Trace' I) -> I (Trace' I) -> Trace' I
forall a b. (a -> b) -> a -> b
$ Trace' I -> I (Trace' I)
forall a. a -> I a
I Trace' I
t
pattern ProgWrite :: OptFlag -> Set (OutputPattern 'TraceP) -> Trace -> Trace
pattern $mProgWrite :: forall {r}.
Trace
-> (OptFlag -> Set (OutputPattern 'TraceP) -> Trace -> r)
-> ((# #) -> r)
-> r
$bProgWrite :: OptFlag -> Set (OutputPattern 'TraceP) -> Trace -> Trace
ProgWrite opt os t <- Trace (ProgWriteC opt os (I (Trace -> t))) where
ProgWrite OptFlag
opt Set (OutputPattern 'TraceP)
os (Trace Trace' I
t) = Trace' I -> Trace
Trace (Trace' I -> Trace) -> Trace' I -> Trace
forall a b. (a -> b) -> a -> b
$ OptFlag -> Set (OutputPattern 'TraceP) -> I (Trace' I) -> Trace' I
forall (f :: * -> *).
OptFlag -> Set (OutputPattern 'TraceP) -> f (Trace' f) -> Trace' f
ProgWriteC OptFlag
opt Set (OutputPattern 'TraceP)
os (I (Trace' I) -> Trace' I) -> I (Trace' I) -> Trace' I
forall a b. (a -> b) -> a -> b
$ Trace' I -> I (Trace' I)
forall a. a -> I a
I Trace' I
t
pattern NTerminate :: NTrace
pattern $mNTerminate :: forall {r}. NTrace -> ((# #) -> r) -> ((# #) -> r) -> r
$bNTerminate :: NTrace
NTerminate = NTrace TerminateC
pattern NOutOfInputs :: NTrace
pattern $mNOutOfInputs :: forall {r}. NTrace -> ((# #) -> r) -> ((# #) -> r) -> r
$bNOutOfInputs :: NTrace
NOutOfInputs = NTrace OutOfInputsC
{-# COMPLETE NProgReadString, NProgWrite, NTerminate, NOutOfInputs #-}
pattern NProgReadString :: String -> NTrace -> NTrace
pattern $mNProgReadString :: forall {r}. NTrace -> (String -> NTrace -> r) -> ((# #) -> r) -> r
$bNProgReadString :: String -> NTrace -> NTrace
NProgReadString s t <- (nextInputN -> Just (s,t)) where
NProgReadString String
s NTrace
t = (Char -> NTrace -> NTrace) -> NTrace -> String -> NTrace
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Char -> NTrace -> NTrace
NProgRead NTrace
t String
s
{-# COMPLETE NProgRead, NProgWrite, NTerminate, NOutOfInputs #-}
pattern NProgRead :: Char -> NTrace -> NTrace
pattern $mNProgRead :: forall {r}. NTrace -> (Char -> NTrace -> r) -> ((# #) -> r) -> r
$bNProgRead :: Char -> NTrace -> NTrace
NProgRead c t <- NTrace (ProgReadC c (I (NTrace -> t))) where
NProgRead Char
c (NTrace Trace' I
t) = Trace' I -> NTrace
NTrace (Trace' I -> NTrace) -> Trace' I -> NTrace
forall a b. (a -> b) -> a -> b
$ Char -> I (Trace' I) -> Trace' I
forall (f :: * -> *). Char -> f (Trace' f) -> Trace' f
ProgReadC Char
c (I (Trace' I) -> Trace' I) -> I (Trace' I) -> Trace' I
forall a b. (a -> b) -> a -> b
$ Trace' I -> I (Trace' I)
forall a. a -> I a
I Trace' I
t
pattern NProgWrite :: OptFlag -> Set (OutputPattern 'TraceP) -> NTrace -> NTrace
pattern $mNProgWrite :: forall {r}.
NTrace
-> (OptFlag -> Set (OutputPattern 'TraceP) -> NTrace -> r)
-> ((# #) -> r)
-> r
$bNProgWrite :: OptFlag -> Set (OutputPattern 'TraceP) -> NTrace -> NTrace
NProgWrite opt os t <- NTrace (ProgWriteC opt os (I (NTrace -> t))) where
NProgWrite OptFlag
opt Set (OutputPattern 'TraceP)
os (NTrace Trace' I
t) = Trace' I -> NTrace
NTrace (Trace' I -> NTrace) -> Trace' I -> NTrace
forall a b. (a -> b) -> a -> b
$ OptFlag -> Set (OutputPattern 'TraceP) -> I (Trace' I) -> Trace' I
forall (f :: * -> *).
OptFlag -> Set (OutputPattern 'TraceP) -> f (Trace' f) -> Trace' f
ProgWriteC OptFlag
opt Set (OutputPattern 'TraceP)
os (I (Trace' I) -> Trace' I) -> I (Trace' I) -> Trace' I
forall a b. (a -> b) -> a -> b
$ Trace' I -> I (Trace' I)
forall a. a -> I a
I Trace' I
t