{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE LambdaCase #-}
module Test.IOTasks.Random.Testing (
  taskCheck, taskCheckWith, taskCheckOutcome, taskCheckWithOutcome,
  Args (..), stdArgs,
  -- | = pre-computed test suites
  taskCheckOn,
  genInput,
  ) where

import Test.IOTasks.Testing hiding (taskCheck, taskCheckWith, taskCheckOutcome, taskCheckWithOutcome, Args, stdArgs)

import Data.Set as Set hiding (foldr)
import Data.Functor (void)
import Data.Bifunctor (first)

import Test.IOTasks.IOrep (IOrep, runProgram)
import Test.IOTasks.Internal.Specification
import Test.IOTasks.Trace
import Test.IOTasks.Term
import Test.IOTasks.Var (someVar)
import Test.IOTasks.OutputPattern
import Test.IOTasks.ValueSet
import Test.IOTasks.ValueMap
import Test.IOTasks.Internal.Output
import Test.IOTasks.Overflow (OverflowWarning(..))

import Test.QuickCheck (Gen, generate, frequency)

import System.IO (stdout)
import System.Timeout (timeout)
import Control.Monad (when, foldM)
import Debug.Trace (traceShowId)
import Test.IOTasks.Internal.Term (showResult)

taskCheck :: IOrep () -> Specification -> IO ()
taskCheck :: IOrep () -> Specification -> IO ()
taskCheck = Args -> IOrep () -> Specification -> IO ()
taskCheckWith Args
stdArgs

data Args
  = Args
  -- | maximum length of input sequences, unbounded if 'Nothing'
  { Args -> Maybe Int
maxInputLength :: Maybe Int
  -- | size of randomly generated input candidates (the solver might find bigger solutions)
  , Args -> Integer
valueSize :: Integer
  -- | maximum number of generated tests
  , Args -> Int
numberOfTests :: Int
  -- | maximum number of negative inputs per path (for 'InputMode' 'UntilValid')
  , Args -> Int
maxNegative :: Int
  -- | print extra information
  , Args -> Bool
terminalOutput :: Bool
  -- | cleanup feedback for educational use
  , Args -> FeedbackStyle
feedbackStyle :: FeedbackStyle
  -- | timeout for restarting input search, in milliseconds
  , Args -> Int
searchTimeout :: Int
  -- | maximum number timeouts before giving up
  , Args -> Int
maxSearchTimeouts :: Int
  }

stdArgs :: Args
stdArgs :: Args
stdArgs = Args
  { maxInputLength :: Maybe Int
maxInputLength = Maybe Int
forall a. Maybe a
Nothing
  , valueSize :: Integer
valueSize = Integer
100
  , numberOfTests :: Int
numberOfTests = Int
100
  , maxNegative :: Int
maxNegative = Int
5
  , terminalOutput :: Bool
terminalOutput = Bool
True
  , feedbackStyle :: FeedbackStyle
feedbackStyle = FeedbackStyle
defaultFeedback
  , searchTimeout :: Int
searchTimeout = Int
3000 -- 3 sec
  , maxSearchTimeouts :: Int
maxSearchTimeouts = Int
5
  }

taskCheckWith :: Args -> IOrep () -> Specification -> IO ()
taskCheckWith :: Args -> IOrep () -> Specification -> IO ()
taskCheckWith Args
args IOrep ()
p Specification
s = IO Outcome -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO Outcome -> IO ()) -> IO Outcome -> IO ()
forall a b. (a -> b) -> a -> b
$ Args -> IOrep () -> Specification -> IO Outcome
taskCheckWithOutcome Args
args IOrep ()
p Specification
s

taskCheckOutcome :: IOrep () -> Specification -> IO Outcome
taskCheckOutcome :: IOrep () -> Specification -> IO Outcome
taskCheckOutcome = Args -> IOrep () -> Specification -> IO Outcome
taskCheckWithOutcome Args
stdArgs

taskCheckWithOutcome :: Args -> IOrep () -> Specification -> IO Outcome
taskCheckWithOutcome :: Args -> IOrep () -> Specification -> IO Outcome
taskCheckWithOutcome Args{Bool
Int
Integer
Maybe Int
FeedbackStyle
maxInputLength :: Args -> Maybe Int
valueSize :: Args -> Integer
numberOfTests :: Args -> Int
maxNegative :: Args -> Int
terminalOutput :: Args -> Bool
feedbackStyle :: Args -> FeedbackStyle
searchTimeout :: Args -> Int
maxSearchTimeouts :: Args -> Int
maxInputLength :: Maybe Int
valueSize :: Integer
numberOfTests :: Int
maxNegative :: Int
terminalOutput :: Bool
feedbackStyle :: FeedbackStyle
searchTimeout :: Int
maxSearchTimeouts :: Int
..} IOrep ()
prog Specification
spec  = do
  Output
output <- Handle -> IO Output
newOutput Handle
stdout
  (Outcome
outcome, Int
_to) <- ((Outcome, Int) -> Int -> IO (Outcome, Int))
-> (Outcome, Int) -> [Int] -> IO (Outcome, Int)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\(Outcome
o',Int
to) Int
n -> (Outcome -> Outcome) -> (Outcome, Int) -> (Outcome, Int)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Outcome
o' <>) ((Outcome, Int) -> (Outcome, Int))
-> IO (Outcome, Int) -> IO (Outcome, Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Output -> Int -> Int -> IO (Outcome, Int)
test Output
output Int
n Int
to) (Outcome
forall a. Monoid a => a
mempty,Int
0) [Int
0..Int
numberOfTestsInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]
  Output -> Doc -> IO ()
forall a. Show a => Output -> a -> IO ()
printP Output
output (Doc -> IO ()) -> Doc -> IO ()
forall a b. (a -> b) -> a -> b
$ FeedbackStyle -> Outcome -> Doc
printOutcomeWith FeedbackStyle
feedbackStyle Outcome
outcome
  Outcome -> IO Outcome
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Outcome
outcome

  where
    test :: Output -> Int -> Int -> IO (Outcome, Int)
    test :: Output -> Int -> Int -> IO (Outcome, Int)
test Output
o Int
n Int
to
      | Int
to Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxSearchTimeouts = (Outcome, Int) -> IO (Outcome, Int)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CoreOutcome -> OutcomeHints -> Outcome
Outcome CoreOutcome
GaveUp OutcomeHints
NoHints,Int
to)
      | Bool
otherwise = do
        Inputs
input <- Gen Inputs -> IO Inputs
forall a. Gen a -> IO a
generate (Gen Inputs -> IO Inputs) -> Gen Inputs -> IO Inputs
forall a b. (a -> b) -> a -> b
$ Specification -> Maybe Int -> Size -> Int -> Gen Inputs
genInput Specification
spec Maybe Int
maxInputLength (Integer -> Int -> Size
Size Integer
valueSize (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Integer
valueSize Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
5)) Int
maxNegative
        Maybe Outcome
mOutcome <- Int -> IO Outcome -> IO (Maybe Outcome)
forall a. Int -> IO a -> IO (Maybe a)
timeout (Int
searchTimeout Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
1000) (IO Outcome -> IO (Maybe Outcome))
-> IO Outcome -> IO (Maybe Outcome)
forall a b. (a -> b) -> a -> b
$ do
          let outcome :: Outcome
outcome = IOrep () -> Specification -> Inputs -> Outcome
runTest IOrep ()
prog Specification
spec Inputs
input
          Bool -> IO Outcome -> IO Outcome
forall a b. a -> b -> b
seq (Outcome -> Bool
isSuccess Outcome
outcome) (IO Outcome -> IO Outcome) -> IO Outcome -> IO Outcome
forall a b. (a -> b) -> a -> b
$ Outcome -> IO Outcome
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Outcome
outcome -- force outcome
        case Maybe Outcome
mOutcome of
          Just Outcome
outcome -> do
            Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
terminalOutput (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
              Output -> String -> IO ()
putT Output
o (Inputs -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"(",Int -> String
forall a. Show a => a -> String
show Int
n,String
" tests)"]) IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Output -> IO ()
oFlush Output
o
              Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Outcome -> Int
overflowWarnings Outcome
outcome Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Output -> String -> IO ()
putLnP Output
o String
"Overflow of Int range detected."
            (Outcome, Int) -> IO (Outcome, Int)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Outcome
outcome,Int
to)
          Maybe Outcome
Nothing -> do
            Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
terminalOutput (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Output -> String -> IO ()
putLnP Output
o String
"input search: timeout"
            Output -> Int -> Int -> IO (Outcome, Int)
test Output
o Int
n (Int
toInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)

genInput :: Specification -> Maybe Int -> Size -> Int -> Gen Inputs
genInput :: Specification -> Maybe Int -> Size -> Int -> Gen Inputs
genInput Specification
s Maybe Int
depth Size
sz Int
maxNeg = do
  Trace
t <- Specification -> Maybe Int -> Size -> Int -> Gen Trace
genTrace Specification
s Maybe Int
depth Size
sz Int
maxNeg
  if Trace -> Bool
isTerminating Trace
t
    then Inputs -> Gen Inputs
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Inputs -> Gen Inputs) -> Inputs -> Gen Inputs
forall a b. (a -> b) -> a -> b
$ Trace -> Inputs
inputSequence Trace
t
    else Specification -> Maybe Int -> Size -> Int -> Gen Inputs
genInput Specification
s Maybe Int
depth Size
sz Int
maxNeg -- repeat sampling until a terminating trace is found

genTrace :: Specification -> Maybe Int -> Size -> Int -> Gen Trace
genTrace :: Specification -> Maybe Int -> Size -> Int -> Gen Trace
genTrace Specification
spec Maybe Int
depth Size
sz Int
maxNeg =
  (forall v.
 (Typeable v, Read v, Show v) =>
 (ValueMap, Int, Int)
 -> Var v
 -> ValueSet v
 -> InputMode
 -> Gen
      (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace))
-> (RecStruct String () Trace Trace -> Gen Trace)
-> (forall (k :: PatternKind).
    (ValueMap, Int, Int)
    -> OptFlag -> Set (OutputPattern k) -> Gen Trace -> Gen Trace)
-> ((ValueMap, Int, Int)
    -> Term 'Transparent Bool -> Gen Trace -> Gen Trace -> Gen Trace)
-> (Action -> Gen Trace -> Gen Trace)
-> (Gen Trace -> Gen Trace)
-> Gen Trace
-> (ValueMap, Int, Int)
-> Specification
-> Gen Trace
forall (m :: * -> *) st p a.
Monad m =>
(forall v.
 (Typeable v, Read v, Show v) =>
 st
 -> Var v
 -> ValueSet v
 -> InputMode
 -> m (RecStruct p (a -> a) st a))
-> (RecStruct p () a a -> m a)
-> (forall (k :: PatternKind).
    st -> OptFlag -> Set (OutputPattern k) -> m a -> m a)
-> (st -> Term 'Transparent Bool -> m a -> m a -> m a)
-> (Action -> m a -> m a)
-> (m a -> m a)
-> m a
-> st
-> Specification
-> m a
semM
    (\(ValueMap
e,Int
d,Int
n) Var v
x ValueSet v
vs InputMode
mode ->
      (if Bool -> (Int -> Bool) -> Maybe Int -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Int
d >) Maybe Int
depth then RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace
-> Gen
     (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace
 -> Gen
      (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace))
-> RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace
-> Gen
     (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace)
forall a b. (a -> b) -> a -> b
$ Trace
-> RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace
forall p x a r. r -> RecStruct p x a r
NoRec Trace
OutOfInputs
      else do
        [(Int,
  Gen
    (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace))]
-> Gen
     (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace)
forall a. [(Int, Gen a)] -> Gen a
frequency ([(Int,
   Gen
     (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace))]
 -> Gen
      (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace))
-> [(Int,
     Gen
       (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace))]
-> Gen
     (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace)
forall a b. (a -> b) -> a -> b
$
            (Int
5, Var v -> ValueMap -> ValueSet v -> Size -> Gen v
forall a. Var a -> ValueMap -> ValueSet a -> Size -> Gen a
valueOf Var v
x ValueMap
e ValueSet v
vs Size
sz Gen v
-> (v
    -> Gen
         (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace))
-> Gen
     (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\v
i -> RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace
-> Gen
     (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace
 -> Gen
      (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace))
-> RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace
-> Gen
     (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace)
forall a b. (a -> b) -> a -> b
$ String
-> (Trace -> Trace)
-> (ValueMap, Int, Int)
-> RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace
forall p x a r. p -> x -> a -> RecStruct p x a r
RecSub (v -> String
forall a. (Show a, Typeable a) => a -> String
showResult v
i) Trace -> Trace
forall a. a -> a
id (Value -> SomeVar -> ValueMap -> ValueMap
insertValue (v -> Value
forall a. Typeable a => a -> Value
wrapValue v
i) (Var v -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var v
x) ValueMap
e,Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1,Int
n)))
          (Int,
 Gen (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace))
-> [(Int,
     Gen
       (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace))]
-> [(Int,
     Gen
       (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace))]
forall a. a -> [a] -> [a]
: [(Int
1, Var v -> ValueMap -> ValueSet v -> Size -> Gen v
forall a. Var a -> ValueMap -> ValueSet a -> Size -> Gen a
valueOf Var v
x ValueMap
e (ValueSet v -> ValueSet v
forall a. ValueSet a -> ValueSet a
complement ValueSet v
vs) Size
sz Gen v
-> (v
    -> Gen
         (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace))
-> Gen
     (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\v
i -> RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace
-> Gen
     (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace
 -> Gen
      (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace))
-> RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace
-> Gen
     (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace)
forall a b. (a -> b) -> a -> b
$ String
-> (Trace -> Trace)
-> (ValueMap, Int, Int)
-> RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace
forall p x a r. p -> x -> a -> RecStruct p x a r
RecSame (v -> String
forall a. (Show a, Typeable a) => a -> String
showResult v
i) Trace -> Trace
forall a. a -> a
id (ValueMap
e,Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1,Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1))) | InputMode
mode InputMode -> InputMode -> Bool
forall a. Eq a => a -> a -> Bool
== InputMode
UntilValid Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
maxNeg]
          [(Int,
  Gen
    (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace))]
-> [(Int,
     Gen
       (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace))]
-> [(Int,
     Gen
       (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace))]
forall a. [a] -> [a] -> [a]
++ [(Int
1, Var v -> ValueMap -> ValueSet v -> Size -> Gen v
forall a. Var a -> ValueMap -> ValueSet a -> Size -> Gen a
valueOf Var v
x ValueMap
e (ValueSet v -> ValueSet v
forall a. ValueSet a -> ValueSet a
complement ValueSet v
vs) Size
sz Gen v
-> (v
    -> Gen
         (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace))
-> Gen
     (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\v
i -> RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace
-> Gen
     (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace
 -> Gen
      (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace))
-> RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace
-> Gen
     (RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace)
forall a b. (a -> b) -> a -> b
$ Trace
-> RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace
forall p x a r. r -> RecStruct p x a r
NoRec (Trace
 -> RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace)
-> Trace
-> RecStruct String (Trace -> Trace) (ValueMap, Int, Int) Trace
forall a b. (a -> b) -> a -> b
$ (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
Terminate (v -> String
forall a. Show a => a -> String
show v
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"))) | InputMode
mode InputMode -> InputMode -> Bool
forall a. Eq a => a -> a -> Bool
== InputMode
ElseAbort Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
maxNeg]
    ))
    (Trace -> Gen Trace
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Trace -> Gen Trace)
-> (RecStruct String () Trace Trace -> Trace)
-> RecStruct String () Trace Trace
-> Gen Trace
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      NoRec Trace
r -> Trace
r
      RecSub String
i () Trace
t' -> do
        (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
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n")
      RecSame String
i () Trace
t' -> do
        (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
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n")
      RecBoth{} -> String -> Trace
forall a. HasCallStack => String -> a
error String
"genTrace: impossible"
    )
    (\(ValueMap
e,Int
_,Int
_) OptFlag
o Set (OutputPattern k)
ts Gen Trace
t' -> OptFlag -> Set (OutputPattern 'TraceP) -> Trace -> Trace
ProgWrite OptFlag
o ((OutputPattern k -> OutputPattern 'TraceP)
-> Set (OutputPattern k) -> Set (OutputPattern 'TraceP)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((OverflowWarning, OutputPattern 'TraceP) -> OutputPattern 'TraceP
forall a b. (a, b) -> b
snd ((OverflowWarning, OutputPattern 'TraceP) -> OutputPattern 'TraceP)
-> (OutputPattern k -> (OverflowWarning, OutputPattern 'TraceP))
-> OutputPattern k
-> OutputPattern 'TraceP
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValueMap
-> OutputPattern k -> (OverflowWarning, OutputPattern 'TraceP)
forall (k :: PatternKind).
ValueMap
-> OutputPattern k -> (OverflowWarning, OutputPattern 'TraceP)
evalPattern ValueMap
e) Set (OutputPattern k)
ts) (Trace -> Trace) -> Gen Trace -> Gen Trace
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Trace
t')
    (\(ValueMap
e,Int
_,Int
_) Term 'Transparent Bool
c Gen Trace
l Gen Trace
r -> if (OverflowWarning, Bool) -> Bool
forall a b. (a, b) -> b
snd ((OverflowWarning, Bool) -> Bool)
-> (OverflowWarning, Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ ValueMap -> Term 'Transparent Bool -> (OverflowWarning, Bool)
forall a (k :: TermKind).
Typeable a =>
ValueMap -> Term k a -> (OverflowWarning, a)
oEval ValueMap
e Term 'Transparent Bool
c then Gen Trace
l else Gen Trace
r)
    ((Gen Trace -> Gen Trace) -> Action -> Gen Trace -> Gen Trace
forall a b. a -> b -> a
const Gen Trace -> Gen Trace
forall a. a -> a
id)
    Gen Trace -> Gen Trace
forall a. a -> a
id
    (Trace -> Gen Trace
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Trace
Terminate)
    ([SomeVar] -> ValueMap
emptyValueMap ([SomeVar] -> ValueMap) -> [SomeVar] -> ValueMap
forall a b. (a -> b) -> a -> b
$ Specification -> [SomeVar]
readVars Specification
spec,Int
1,Int
0)
    Specification
spec

runTest :: IOrep () -> Specification -> Inputs -> Outcome
runTest :: IOrep () -> Specification -> Inputs -> Outcome
runTest IOrep ()
p Specification
spec Inputs
i =
  let
    (NTrace
specTrace,OverflowWarning
warn) = (AbstractTrace -> NTrace)
-> (AbstractTrace, OverflowWarning) -> (NTrace, OverflowWarning)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first AbstractTrace -> NTrace
normalizedTrace ((AbstractTrace, OverflowWarning) -> (NTrace, OverflowWarning))
-> (AbstractTrace, OverflowWarning) -> (NTrace, OverflowWarning)
forall a b. (a -> b) -> a -> b
$ Specification -> Inputs -> (AbstractTrace, OverflowWarning)
runSpecification Specification
spec Inputs
i
    progTrace :: NTrace
progTrace = IOrep () -> Inputs -> NTrace
runProgram IOrep ()
p Inputs
i
    o :: OutcomeHints
o = case OverflowWarning
warn of
      OverflowWarning
OverflowOccurred -> Int -> OutcomeHints
OverflowHint Int
1
      OverflowWarning
_ -> OutcomeHints
forall a. Monoid a => a
mempty
  in case NTrace
specTrace NTrace -> NTrace -> MatchResult
`covers` NTrace
progTrace of
    MatchResult
result | MatchResult -> Bool
isSuccessfulMatch MatchResult
result -> CoreOutcome -> OutcomeHints -> Outcome
Outcome (Int -> CoreOutcome
Success Int
1) OutcomeHints
o
    MatchResult
failure -> CoreOutcome -> OutcomeHints -> Outcome
Outcome (Inputs -> NTrace -> NTrace -> MatchResult -> CoreOutcome
Failure Inputs
i NTrace
specTrace NTrace
progTrace MatchResult
failure) OutcomeHints
o