{-# 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)

-- "polymorphic" unit type
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

-- free semigroup over single trace actions
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
    -- HasConsume tracks if the result has consumed at least one step from t
    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 -- This is r1 <> r2 + bookkeeping for the consumption status
        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
(<+>)

-- | like 'showTraceN' but trace steps are combined with the user supplied function
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
(<+>)

-- | like 'showTraceNSimple' but trace steps are combined with the user supplied function
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
(<+>)

-- | like 'showTrace' but trace steps are combined with the user supplied function
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
(<+>)

-- | like 'showTraceSimple' but trace steps are combined with the user supplied function
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' -- omit optional outputs in simplified version
  | 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
  -- technically this might add an additional line break on the last line that might not be there in the Trace
  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
  -- technically this might add an additional line break on the last line that might not be there in the Trace
  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

-- Trace patterns
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

-- NTrace patterns
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