{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}

-- |
-- Module      : Test.DejaFu.Refinement
-- Copyright   : (c) 2017--2021 Michael Walker
-- License     : MIT
-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
-- Stability   : experimental
-- Portability : FlexibleContexts, FlexibleInstances, GADTs, MultiWayIf, TupleSections, TypeFamilies
--
-- Properties about the side-effects of concurrent functions on some
-- shared state.
--
-- Consider this statement about @MVar@s: \"using @readMVar@ is better
-- than @takeMVar@ followed by @putMVar@ because the former is atomic
-- but the latter is not.\"
--
-- This module can test properties like that:
--
-- >>> import Control.Monad (void)
-- >>> :{
-- let sig e = Sig
--       { initialise = maybe newEmptyMVar newMVar
--       , observe    = \v _ -> tryReadMVar v
--       , interfere  = \v _ -> putMVar v 42
--       , expression = void . e
--       }
-- :}
--
-- >>> check $ sig readMVar === sig (\v -> takeMVar v >>= putMVar v)
-- *** Failure: (seed Just 0)
--     left:  [(Nothing,Just 0)]
--     right: [(Nothing,Just 0),(Just Deadlock,Just 42)]
-- False
--
-- The two expressions are not equivalent, and we get given the
-- counterexample!
--
-- There are quite a few things going on here, so let's unpack this:
--
-- (1) Properties are specified in terms of an __initialisation__
--     function, an __observation__ function, an __interference__
--     function, and the expression of interest.
--
-- (2) The initialisation function ('initialise') says how to
--     construct some __state__ value from a __seed__ value, which is
--     supplied by 'check'.  In this case the seed is of type @Maybe
--     a@ and the state @MVar ConcIO a@.
--
-- (3) The observation ('observe') function says how to take the state
--     and the seed, and produce some value which will be used to
--     compare the expressions.  In this case the observation value is
--     of type @Maybe a@.
--
-- (4) The interference ('interfere') function says what sort of
--     concurrent interference can happen.  In this case we just try
--     to set the @MVar@ to its original value.
--
-- The 'check' function takes a property, consisting of two signatures
-- and a way to compare them, evaluates all the results of each
-- signature, and then compares them in the appropriate way.
--
-- See the sections later in the documentation for what
-- \"refinement\", \"strict refinement\", and \"equivalence\" mean
-- exactly.
module Test.DejaFu.Refinement
  ( -- * Defining properties
    Sig(..)
  , RefinementProperty
  , expectFailure

  -- ** A refines B

  -- | Refinement (or \"weak refinement\") means that all of the
  -- results of the left are also results of the right.  If you think
  -- in terms of sets of results, refinement is subset.
  , refines, (=>=)

  -- ** A strictly refines B

  -- | Strict refinement means that the left refines the right, but
  -- the right does not refine the left.  If you think in terms of
  -- sets of results, strict refinement is proper subset.
  , strictlyRefines, (->-)

  -- ** A is equivalent to B

  -- | Equivalence means that the left and right refine each other.
  -- If you think in terms of sets of results, equivalence is
  -- equality.
  , equivalentTo, (===)

  -- * Testing properties
  , FailedProperty(..)
  , Testable(O,X)
  , check
  , check'
  , checkFor
  , counterExamples

  -- * Re-exports
  , Listable(..)
  ) where

import           Control.Arrow            (first)
import           Control.Monad.Conc.Class (fork)
import           Data.Kind                (Type)
import           Data.Maybe               (isNothing)
import           Data.Set                 (Set)
import qualified Data.Set                 as S
import           Test.LeanCheck           (Listable(..), concatMapT, mapT)

import           Test.DejaFu.Conc         (ConcIO, Condition,
                                           withSetupAndTeardown)
import           Test.DejaFu.SCT          (runSCT)
import           Test.DejaFu.Settings     (defaultMemType, defaultWay)

-- $setup
-- >>> import Control.Concurrent.Classy hiding (check)

-------------------------------------------------------------------------------
-- Specifying properties

-- | What to check.
data How = Weak | Equiv | Strict deriving How -> How -> Bool
(How -> How -> Bool) -> (How -> How -> Bool) -> Eq How
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: How -> How -> Bool
== :: How -> How -> Bool
$c/= :: How -> How -> Bool
/= :: How -> How -> Bool
Eq

-- | A property which can be given to 'check'.
--
-- @since 0.7.0.0
data RefinementProperty o x where
  RP  :: Ord o => How -> Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
  Neg :: RefinementProperty o x -> RefinementProperty o x

-- | A concurrent function and some information about how to execute
-- it and observe its effect.
--
-- * @s@ is the state type (@MVar ConcIO a@ in the example)
-- * @o@ is the observation type (@Maybe a@ in the example)
-- * @x@ is the seed type (@Maybe a@ in the example)
--
-- @since 0.7.0.0
data Sig s o x = Sig
  { forall s o x. Sig s o x -> x -> ConcIO s
initialise :: x -> ConcIO s
  -- ^ Create a new instance of the state variable.
  , forall s o x. Sig s o x -> s -> x -> ConcIO o
observe :: s -> x -> ConcIO o
  -- ^ The observation to make.
  , forall s o x. Sig s o x -> s -> x -> ConcIO ()
interfere :: s -> x -> ConcIO ()
  -- ^ Set the state value. This doesn't need to be atomic, or even
  -- guaranteed to work, its purpose is to cause interference.
  , forall s o x. Sig s o x -> s -> ConcIO ()
expression :: s -> ConcIO ()
  -- ^ The expression to evaluate.
  }

-- | Indicates that the property is supposed to fail.
expectFailure :: RefinementProperty o x -> RefinementProperty o x
expectFailure :: forall o x. RefinementProperty o x -> RefinementProperty o x
expectFailure = RefinementProperty o x -> RefinementProperty o x
forall o x. RefinementProperty o x -> RefinementProperty o x
Neg

-- | Observational refinement.
--
-- True iff the result-set of the left expression is a subset (not
-- necessarily proper) of the result-set of the right expression.
--
-- The two signatures can have different state types, this lets you
-- compare the behaviour of different data structures.  The
-- observation and seed types must match, however.
--
-- @since 0.7.0.0
refines :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
refines :: forall o s1 x s2.
Ord o =>
Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
refines = How -> Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
forall o s1 x s2.
Ord o =>
How -> Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
RP How
Weak

-- | Infix synonym for 'refines'.
--
-- You might think this should be '=<=', so it looks kind of like a
-- funny subset operator, with @A =<= B@ meaning \"the result-set of A
-- is a subset of the result-set of B\".  Unfortunately you would be
-- wrong.  The operator used in the literature for refinement has the
-- open end pointing at the LESS general term and the closed end at
-- the MORE general term.  It is read as \"is refined by\", not
-- \"refines\".  So for consistency with the literature, the open end
-- of @=>=@ points at the less general term, and the closed end at the
-- more general term, to give the same argument order as 'refines'.
--
-- @since 0.7.0.0
(=>=) :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
=>= :: forall o s1 x s2.
Ord o =>
Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
(=>=) = Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
forall o s1 x s2.
Ord o =>
Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
refines

-- | Observational equivalence.
--
-- True iff the result-set of the left expression is equal to the
-- result-set of the right expression.
--
-- The two signatures can have different state types, this lets you
-- compare the behaviour of different data structures.  The
-- observation and seed types must match, however.
--
-- @since 0.7.0.0
equivalentTo :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
equivalentTo :: forall o s1 x s2.
Ord o =>
Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
equivalentTo = How -> Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
forall o s1 x s2.
Ord o =>
How -> Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
RP How
Equiv

-- | Infix synonym for 'equivalentTo'.
--
-- @since 0.7.0.0
(===) :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
=== :: forall o s1 x s2.
Ord o =>
Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
(===) = Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
forall o s1 x s2.
Ord o =>
Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
equivalentTo

-- | Strict observational refinement.
--
-- True iff the result-set of the left expression is a proper subset
-- of the result-set of the right expression.
--
-- The two signatures can have different state types, this lets you
-- compare the behaviour of different data structures.  The
-- observation and seed types must match, however.
--
-- @since 0.7.0.0
strictlyRefines :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
strictlyRefines :: forall o s1 x s2.
Ord o =>
Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
strictlyRefines = How -> Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
forall o s1 x s2.
Ord o =>
How -> Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
RP How
Strict

-- | Infix synonym for 'strictlyRefines'
--
-- @since 0.7.0.0
(->-) :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
->- :: forall o s1 x s2.
Ord o =>
Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
(->-) = Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
forall o s1 x s2.
Ord o =>
Sig s1 o x -> Sig s2 o x -> RefinementProperty o x
strictlyRefines


-------------------------------------------------------------------------------
-- Property testing

-- | Things which can be tested.
--
-- @since 0.7.0.0
class Testable a where
  -- | The observation value type.  This is used to compare the
  -- results.
  type O a :: Type

  -- | The seed value type.  This is used to construct the concurrent
  -- states.
  type X a :: Type

  rpropTiers :: a -> [[([String], RefinementProperty (O a) (X a))]]

instance Testable (RefinementProperty o x) where
  type O (RefinementProperty o x) = o
  type X (RefinementProperty o x) = x

  rpropTiers :: RefinementProperty o x
-> [[([String],
      RefinementProperty
        (O (RefinementProperty o x)) (X (RefinementProperty o x)))]]
rpropTiers RefinementProperty o x
p = [[([], RefinementProperty o x
RefinementProperty
  (O (RefinementProperty o x)) (X (RefinementProperty o x))
p)]]

instance (Listable a, Show a, Testable b) => Testable (a -> b) where
  type O (a -> b) = O b
  type X (a -> b) = X b

  rpropTiers :: (a -> b)
-> [[([String], RefinementProperty (O (a -> b)) (X (a -> b)))]]
rpropTiers a -> b
p = (a -> [[([String], RefinementProperty (O b) (X b))]])
-> [[a]] -> [[([String], RefinementProperty (O b) (X b))]]
forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT a -> [[([String], RefinementProperty (O b) (X b))]]
resultiersFor [[a]]
forall a. Listable a => [[a]]
tiers where
    resultiersFor :: a -> [[([String], RefinementProperty (O b) (X b))]]
resultiersFor a
x = ([String] -> [String])
-> ([String], RefinementProperty (O b) (X b))
-> ([String], RefinementProperty (O b) (X b))
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (a -> String
forall a. Show a => a -> String
show a
xString -> [String] -> [String]
forall a. a -> [a] -> [a]
:) (([String], RefinementProperty (O b) (X b))
 -> ([String], RefinementProperty (O b) (X b)))
-> [[([String], RefinementProperty (O b) (X b))]]
-> [[([String], RefinementProperty (O b) (X b))]]
forall a b. (a -> b) -> [[a]] -> [[b]]
`mapT` b -> [[([String], RefinementProperty (O b) (X b))]]
forall a.
Testable a =>
a -> [[([String], RefinementProperty (O a) (X a))]]
rpropTiers (a -> b
p a
x)

-- | A counter example is a seed value and a list of variable
-- assignments.
--
-- @since 0.7.0.0
data FailedProperty o x
  = CounterExample
    { forall o x. FailedProperty o x -> x
failingSeed  :: x
    -- ^ The seed for this set of executions.
    , forall o x. FailedProperty o x -> [String]
failingArgs  :: [String]
    -- ^ The values of free variables, as strings.
    , forall o x. FailedProperty o x -> Set (Maybe Condition, o)
leftResults  :: Set (Maybe Condition, o)
    -- ^ The set of results of the left signature.
    , forall o x. FailedProperty o x -> Set (Maybe Condition, o)
rightResults :: Set (Maybe Condition, o)
    -- ^ The set of results of the right signature.
    }
  | NoExpectedFailure
  deriving Int -> FailedProperty o x -> ShowS
[FailedProperty o x] -> ShowS
FailedProperty o x -> String
(Int -> FailedProperty o x -> ShowS)
-> (FailedProperty o x -> String)
-> ([FailedProperty o x] -> ShowS)
-> Show (FailedProperty o x)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall o x. (Show x, Show o) => Int -> FailedProperty o x -> ShowS
forall o x. (Show x, Show o) => [FailedProperty o x] -> ShowS
forall o x. (Show x, Show o) => FailedProperty o x -> String
$cshowsPrec :: forall o x. (Show x, Show o) => Int -> FailedProperty o x -> ShowS
showsPrec :: Int -> FailedProperty o x -> ShowS
$cshow :: forall o x. (Show x, Show o) => FailedProperty o x -> String
show :: FailedProperty o x -> String
$cshowList :: forall o x. (Show x, Show o) => [FailedProperty o x] -> ShowS
showList :: [FailedProperty o x] -> ShowS
Show

-- | Check a refinement property with a variety of seed values and
-- variable assignments.
--
-- @since 0.7.0.0
check :: (Testable p, Listable (X p), Show (X p), Show (O p))
  => p
  -- ^ The property to check.
  -> IO Bool
check :: forall p.
(Testable p, Listable (X p), Show (X p), Show (O p)) =>
p -> IO Bool
check p
p = do
  Maybe (FailedProperty (O p) (X p))
ce <- p -> IO (Maybe (FailedProperty (O p) (X p)))
forall p.
(Testable p, Listable (X p)) =>
p -> IO (Maybe (FailedProperty (O p) (X p)))
check' p
p
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ case Maybe (FailedProperty (O p) (X p))
ce of
    Just FailedProperty (O p) (X p)
NoExpectedFailure -> String
"*** Failure: passed, but expected failure."
    Just FailedProperty (O p) (X p)
c -> ShowS
forall a. HasCallStack => [a] -> [a]
init ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
      [ String
"*** Failure: " String -> ShowS
forall a. [a] -> [a] -> [a]
++
        (if [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (FailedProperty (O p) (X p) -> [String]
forall o x. FailedProperty o x -> [String]
failingArgs FailedProperty (O p) (X p)
c) then String
"" else [String] -> String
unwords (FailedProperty (O p) (X p) -> [String]
forall o x. FailedProperty o x -> [String]
failingArgs FailedProperty (O p) (X p)
c) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ") String -> ShowS
forall a. [a] -> [a] -> [a]
++
        String
"(seed " String -> ShowS
forall a. [a] -> [a] -> [a]
++ X p -> String
forall a. Show a => a -> String
show (FailedProperty (O p) (X p) -> X p
forall o x. FailedProperty o x -> x
failingSeed FailedProperty (O p) (X p)
c) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
      , String
"    left:  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Maybe Condition, O p)] -> String
forall a. Show a => a -> String
show (Set (Maybe Condition, O p) -> [(Maybe Condition, O p)]
forall a. Set a -> [a]
S.toList (Set (Maybe Condition, O p) -> [(Maybe Condition, O p)])
-> Set (Maybe Condition, O p) -> [(Maybe Condition, O p)]
forall a b. (a -> b) -> a -> b
$ FailedProperty (O p) (X p) -> Set (Maybe Condition, O p)
forall o x. FailedProperty o x -> Set (Maybe Condition, o)
leftResults  FailedProperty (O p) (X p)
c)
      , String
"    right: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Maybe Condition, O p)] -> String
forall a. Show a => a -> String
show (Set (Maybe Condition, O p) -> [(Maybe Condition, O p)]
forall a. Set a -> [a]
S.toList (Set (Maybe Condition, O p) -> [(Maybe Condition, O p)])
-> Set (Maybe Condition, O p) -> [(Maybe Condition, O p)]
forall a b. (a -> b) -> a -> b
$ FailedProperty (O p) (X p) -> Set (Maybe Condition, O p)
forall o x. FailedProperty o x -> Set (Maybe Condition, o)
rightResults FailedProperty (O p) (X p)
c)
      ]
    Maybe (FailedProperty (O p) (X p))
Nothing -> String
"+++ OK"
  Bool -> IO Bool
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (FailedProperty (O p) (X p)) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (FailedProperty (O p) (X p))
ce)

-- | A version of 'check' that doesn't print, and returns the
-- counterexample.
--
-- @since 0.7.0.0
check' :: (Testable p, Listable (X p))
  => p
  -- ^ The property to check.
  -> IO (Maybe (FailedProperty (O p) (X p)))
check' :: forall p.
(Testable p, Listable (X p)) =>
p -> IO (Maybe (FailedProperty (O p) (X p)))
check' = Int -> Int -> p -> IO (Maybe (FailedProperty (O p) (X p)))
forall p.
(Testable p, Listable (X p)) =>
Int -> Int -> p -> IO (Maybe (FailedProperty (O p) (X p)))
checkFor Int
10 Int
100

-- | Like 'check', but take a number of cases to try, also returns the
-- counter example found rather than printing it.
--
-- If multiple counterexamples exist, this will be faster than
-- @listToMaybe@ composed with @counterExamples@.
--
-- @since 0.7.0.0
checkFor :: (Testable p, Listable (X p))
  => Int
  -- ^ Number of seed values per variable-assignment.
  -> Int
  -- ^ Number of variable assignments.
  -> p
  -- ^ The property to check.
  -> IO (Maybe (FailedProperty (O p) (X p)))
checkFor :: forall p.
(Testable p, Listable (X p)) =>
Int -> Int -> p -> IO (Maybe (FailedProperty (O p) (X p)))
checkFor Int
sn Int
vn p
p =  do
    let seeds :: [X p]
seeds = Int -> [X p] -> [X p]
forall a. Int -> [a] -> [a]
take Int
sn ([X p] -> [X p]) -> [X p] -> [X p]
forall a b. (a -> b) -> a -> b
$ [[X p]] -> [X p]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[X p]]
forall a. Listable a => [[a]]
tiers
    let cases :: [([String], RefinementProperty (O p) (X p))]
cases = Int
-> [([String], RefinementProperty (O p) (X p))]
-> [([String], RefinementProperty (O p) (X p))]
forall a. Int -> [a] -> [a]
take Int
vn ([([String], RefinementProperty (O p) (X p))]
 -> [([String], RefinementProperty (O p) (X p))])
-> [([String], RefinementProperty (O p) (X p))]
-> [([String], RefinementProperty (O p) (X p))]
forall a b. (a -> b) -> a -> b
$ [[([String], RefinementProperty (O p) (X p))]]
-> [([String], RefinementProperty (O p) (X p))]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (p -> [[([String], RefinementProperty (O p) (X p))]]
forall a.
Testable a =>
a -> [[([String], RefinementProperty (O a) (X a))]]
rpropTiers p
p)
    [X p]
-> [([String], RefinementProperty (O p) (X p))]
-> IO (Maybe (FailedProperty (O p) (X p)))
forall {x} {o}.
[x]
-> [([String], RefinementProperty o x)]
-> IO (Maybe (FailedProperty o x))
go [X p]
seeds [([String], RefinementProperty (O p) (X p))]
cases
  where
    go :: [x]
-> [([String], RefinementProperty o x)]
-> IO (Maybe (FailedProperty o x))
go [x]
seeds (([String]
vs, RefinementProperty o x
p'):[([String], RefinementProperty o x)]
rest) = do
      Maybe ([String] -> FailedProperty o x)
r <- [x]
-> RefinementProperty o x
-> IO (Maybe ([String] -> FailedProperty o x))
forall x o.
[x]
-> RefinementProperty o x
-> IO (Maybe ([String] -> FailedProperty o x))
checkWithSeeds [x]
seeds RefinementProperty o x
p'
      case Maybe ([String] -> FailedProperty o x)
r of
        Just [String] -> FailedProperty o x
cf -> Maybe (FailedProperty o x) -> IO (Maybe (FailedProperty o x))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FailedProperty o x -> Maybe (FailedProperty o x)
forall a. a -> Maybe a
Just ([String] -> FailedProperty o x
cf [String]
vs))
        Maybe ([String] -> FailedProperty o x)
Nothing -> [x]
-> [([String], RefinementProperty o x)]
-> IO (Maybe (FailedProperty o x))
go [x]
seeds [([String], RefinementProperty o x)]
rest
    go [x]
_ [] = Maybe (FailedProperty o x) -> IO (Maybe (FailedProperty o x))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (FailedProperty o x)
forall a. Maybe a
Nothing

-- | Find all counterexamples up to a limit.
--
-- @since 0.7.0.0
counterExamples :: (Testable p, Listable (X p))
  => Int
  -- ^ Number of seed values per variable-assignment.
  -> Int
  -- ^ Number of variable assignments
  -> p
  -- ^ The property to check.
  -> IO [FailedProperty (O p) (X p)]
counterExamples :: forall p.
(Testable p, Listable (X p)) =>
Int -> Int -> p -> IO [FailedProperty (O p) (X p)]
counterExamples Int
sn Int
vn p
p = do
  let seeds :: [X p]
seeds = Int -> [X p] -> [X p]
forall a. Int -> [a] -> [a]
take Int
sn ([X p] -> [X p]) -> [X p] -> [X p]
forall a b. (a -> b) -> a -> b
$ [[X p]] -> [X p]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[X p]]
forall a. Listable a => [[a]]
tiers
  let cases :: [([String], RefinementProperty (O p) (X p))]
cases = Int
-> [([String], RefinementProperty (O p) (X p))]
-> [([String], RefinementProperty (O p) (X p))]
forall a. Int -> [a] -> [a]
take Int
vn ([([String], RefinementProperty (O p) (X p))]
 -> [([String], RefinementProperty (O p) (X p))])
-> [([String], RefinementProperty (O p) (X p))]
-> [([String], RefinementProperty (O p) (X p))]
forall a b. (a -> b) -> a -> b
$ [[([String], RefinementProperty (O p) (X p))]]
-> [([String], RefinementProperty (O p) (X p))]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (p -> [[([String], RefinementProperty (O p) (X p))]]
forall a.
Testable a =>
a -> [[([String], RefinementProperty (O a) (X a))]]
rpropTiers p
p)
  [([String], Maybe ([String] -> FailedProperty (O p) (X p)))]
rs <- (([String], RefinementProperty (O p) (X p))
 -> IO ([String], Maybe ([String] -> FailedProperty (O p) (X p))))
-> [([String], RefinementProperty (O p) (X p))]
-> IO [([String], Maybe ([String] -> FailedProperty (O p) (X p)))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\([String]
vs, RefinementProperty (O p) (X p)
p') -> ([String]
vs,) (Maybe ([String] -> FailedProperty (O p) (X p))
 -> ([String], Maybe ([String] -> FailedProperty (O p) (X p))))
-> IO (Maybe ([String] -> FailedProperty (O p) (X p)))
-> IO ([String], Maybe ([String] -> FailedProperty (O p) (X p)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [X p]
-> RefinementProperty (O p) (X p)
-> IO (Maybe ([String] -> FailedProperty (O p) (X p)))
forall x o.
[x]
-> RefinementProperty o x
-> IO (Maybe ([String] -> FailedProperty o x))
checkWithSeeds [X p]
seeds RefinementProperty (O p) (X p)
p') [([String], RefinementProperty (O p) (X p))]
cases
  [FailedProperty (O p) (X p)] -> IO [FailedProperty (O p) (X p)]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ [String] -> FailedProperty (O p) (X p)
cf [String]
vs | ([String]
vs, Just [String] -> FailedProperty (O p) (X p)
cf) <- [([String], Maybe ([String] -> FailedProperty (O p) (X p)))]
rs ]


-------------------------------------------------------------------------------
-- Internal

-- | Three-valued sum, used in checking strict refinement.
data F x = Failing x | Unknown | Refuted

-- | Check a refinement property with given seed values.  Returns the
-- counterexample if the property is false.
checkWithSeeds
  :: [x]
  -- ^ Seed values to use.
  -> RefinementProperty o x
  -- ^ The property to check.
  -> IO (Maybe ([String] -> FailedProperty o x))
checkWithSeeds :: forall x o.
[x]
-> RefinementProperty o x
-> IO (Maybe ([String] -> FailedProperty o x))
checkWithSeeds [x]
seeds (RP How
how Sig s1 o x
l Sig s2 o x
r) = case How
how of
    How
Weak   -> (Set (Maybe Condition, o) -> Set (Maybe Condition, o) -> Bool)
-> [x] -> IO (Maybe ([String] -> FailedProperty o x))
go1 Set (Maybe Condition, o) -> Set (Maybe Condition, o) -> Bool
forall a. Ord a => Set a -> Set a -> Bool
S.isSubsetOf [x]
seeds
    How
Equiv  -> (Set (Maybe Condition, o) -> Set (Maybe Condition, o) -> Bool)
-> [x] -> IO (Maybe ([String] -> FailedProperty o x))
go1 Set (Maybe Condition, o) -> Set (Maybe Condition, o) -> Bool
forall a. Eq a => a -> a -> Bool
(==)         [x]
seeds
    How
Strict -> F ([String] -> FailedProperty o x)
-> [x] -> IO (Maybe ([String] -> FailedProperty o x))
go2 F ([String] -> FailedProperty o x)
forall x. F x
Unknown      [x]
seeds
  where
    -- weak and equiv need every set of pairwise result-sets to match
    -- some predicate.
    go1 :: (Set (Maybe Condition, o) -> Set (Maybe Condition, o) -> Bool)
-> [x] -> IO (Maybe ([String] -> FailedProperty o x))
go1 Set (Maybe Condition, o) -> Set (Maybe Condition, o) -> Bool
f (x
x:[x]
xs) = do
      Set (Maybe Condition, o)
lrs <- Sig s1 o x -> x -> IO (Set (Maybe Condition, o))
forall o s x.
Ord o =>
Sig s o x -> x -> IO (Set (Maybe Condition, o))
evalSigWithSeed Sig s1 o x
l x
x
      Set (Maybe Condition, o)
rrs <- Sig s2 o x -> x -> IO (Set (Maybe Condition, o))
forall o s x.
Ord o =>
Sig s o x -> x -> IO (Set (Maybe Condition, o))
evalSigWithSeed Sig s2 o x
r x
x
      if Set (Maybe Condition, o)
lrs Set (Maybe Condition, o) -> Set (Maybe Condition, o) -> Bool
`f` Set (Maybe Condition, o)
rrs
        then (Set (Maybe Condition, o) -> Set (Maybe Condition, o) -> Bool)
-> [x] -> IO (Maybe ([String] -> FailedProperty o x))
go1 Set (Maybe Condition, o) -> Set (Maybe Condition, o) -> Bool
f [x]
xs
        else Maybe ([String] -> FailedProperty o x)
-> IO (Maybe ([String] -> FailedProperty o x))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (([String] -> FailedProperty o x)
-> Maybe ([String] -> FailedProperty o x)
forall a. a -> Maybe a
Just (([String] -> FailedProperty o x)
 -> Maybe ([String] -> FailedProperty o x))
-> ([String] -> FailedProperty o x)
-> Maybe ([String] -> FailedProperty o x)
forall a b. (a -> b) -> a -> b
$ x
-> Set (Maybe Condition, o)
-> Set (Maybe Condition, o)
-> [String]
-> FailedProperty o x
forall {x} {o}.
x
-> Set (Maybe Condition, o)
-> Set (Maybe Condition, o)
-> [String]
-> FailedProperty o x
toCE x
x Set (Maybe Condition, o)
lrs Set (Maybe Condition, o)
rrs)
    go1 Set (Maybe Condition, o) -> Set (Maybe Condition, o) -> Bool
_ [] = Maybe ([String] -> FailedProperty o x)
-> IO (Maybe ([String] -> FailedProperty o x))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ([String] -> FailedProperty o x)
forall a. Maybe a
Nothing

    -- strict fails if (a) any left result-set is not a subset of the
    -- corresponding right result-set, or (b) every left result-set is
    -- equal to the corresponding right result-set
    go2 :: F ([String] -> FailedProperty o x)
-> [x] -> IO (Maybe ([String] -> FailedProperty o x))
go2 F ([String] -> FailedProperty o x)
eq (x
x:[x]
xs) = do
      Set (Maybe Condition, o)
lrs <- Sig s1 o x -> x -> IO (Set (Maybe Condition, o))
forall o s x.
Ord o =>
Sig s o x -> x -> IO (Set (Maybe Condition, o))
evalSigWithSeed Sig s1 o x
l x
x
      Set (Maybe Condition, o)
rrs <- Sig s2 o x -> x -> IO (Set (Maybe Condition, o))
forall o s x.
Ord o =>
Sig s o x -> x -> IO (Set (Maybe Condition, o))
evalSigWithSeed Sig s2 o x
r x
x
      let ce :: [String] -> FailedProperty o x
ce = x
-> Set (Maybe Condition, o)
-> Set (Maybe Condition, o)
-> [String]
-> FailedProperty o x
forall {x} {o}.
x
-> Set (Maybe Condition, o)
-> Set (Maybe Condition, o)
-> [String]
-> FailedProperty o x
toCE x
x Set (Maybe Condition, o)
lrs Set (Maybe Condition, o)
rrs
      if | Set (Maybe Condition, o)
lrs Set (Maybe Condition, o) -> Set (Maybe Condition, o) -> Bool
forall a. Eq a => a -> a -> Bool
== Set (Maybe Condition, o)
rrs             -> F ([String] -> FailedProperty o x)
-> [x] -> IO (Maybe ([String] -> FailedProperty o x))
go2 (case F ([String] -> FailedProperty o x)
eq of F ([String] -> FailedProperty o x)
Unknown -> ([String] -> FailedProperty o x)
-> F ([String] -> FailedProperty o x)
forall x. x -> F x
Failing [String] -> FailedProperty o x
ce; F ([String] -> FailedProperty o x)
_ -> F ([String] -> FailedProperty o x)
eq) [x]
xs
         | Set (Maybe Condition, o)
lrs Set (Maybe Condition, o) -> Set (Maybe Condition, o) -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` Set (Maybe Condition, o)
rrs -> F ([String] -> FailedProperty o x)
-> [x] -> IO (Maybe ([String] -> FailedProperty o x))
go2 F ([String] -> FailedProperty o x)
forall x. F x
Refuted [x]
xs
         | Bool
otherwise              -> Maybe ([String] -> FailedProperty o x)
-> IO (Maybe ([String] -> FailedProperty o x))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (([String] -> FailedProperty o x)
-> Maybe ([String] -> FailedProperty o x)
forall a. a -> Maybe a
Just [String] -> FailedProperty o x
ce)
    go2 (Failing [String] -> FailedProperty o x
cf) [] = Maybe ([String] -> FailedProperty o x)
-> IO (Maybe ([String] -> FailedProperty o x))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (([String] -> FailedProperty o x)
-> Maybe ([String] -> FailedProperty o x)
forall a. a -> Maybe a
Just [String] -> FailedProperty o x
cf)
    go2 F ([String] -> FailedProperty o x)
_ [] = Maybe ([String] -> FailedProperty o x)
-> IO (Maybe ([String] -> FailedProperty o x))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ([String] -> FailedProperty o x)
forall a. Maybe a
Nothing

    toCE :: x
-> Set (Maybe Condition, o)
-> Set (Maybe Condition, o)
-> [String]
-> FailedProperty o x
toCE x
x Set (Maybe Condition, o)
lrs Set (Maybe Condition, o)
rrs [String]
args = CounterExample
      { failingSeed :: x
failingSeed  = x
x
      , failingArgs :: [String]
failingArgs  = [String]
args
      , leftResults :: Set (Maybe Condition, o)
leftResults  = Set (Maybe Condition, o)
lrs
      , rightResults :: Set (Maybe Condition, o)
rightResults = Set (Maybe Condition, o)
rrs
      }
checkWithSeeds [x]
seeds (Neg RefinementProperty o x
rp) = do
  Maybe ([String] -> FailedProperty o x)
r <- [x]
-> RefinementProperty o x
-> IO (Maybe ([String] -> FailedProperty o x))
forall x o.
[x]
-> RefinementProperty o x
-> IO (Maybe ([String] -> FailedProperty o x))
checkWithSeeds [x]
seeds RefinementProperty o x
rp
  Maybe ([String] -> FailedProperty o x)
-> IO (Maybe ([String] -> FailedProperty o x))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe ([String] -> FailedProperty o x)
 -> IO (Maybe ([String] -> FailedProperty o x)))
-> Maybe ([String] -> FailedProperty o x)
-> IO (Maybe ([String] -> FailedProperty o x))
forall a b. (a -> b) -> a -> b
$ case Maybe ([String] -> FailedProperty o x)
r of
    Just [String] -> FailedProperty o x
_ -> Maybe ([String] -> FailedProperty o x)
forall a. Maybe a
Nothing
    Maybe ([String] -> FailedProperty o x)
Nothing -> ([String] -> FailedProperty o x)
-> Maybe ([String] -> FailedProperty o x)
forall a. a -> Maybe a
Just (FailedProperty o x -> [String] -> FailedProperty o x
forall a b. a -> b -> a
const FailedProperty o x
forall o x. FailedProperty o x
NoExpectedFailure)

-- | Evaluate a signature with a given seed value
evalSigWithSeed :: Ord o
  => Sig s o x
  -> x
  -> IO (Set (Maybe Condition, o))
evalSigWithSeed :: forall o s x.
Ord o =>
Sig s o x -> x -> IO (Set (Maybe Condition, o))
evalSigWithSeed Sig s o x
sig x
x = do
  [(Either Condition (Maybe Condition, o), Trace)]
results <- Way
-> MemType
-> Program (WithSetupAndTeardown s ()) IO (Maybe Condition, o)
-> IO [(Either Condition (Maybe Condition, o), Trace)]
forall (n :: * -> *) pty a.
MonadDejaFu n =>
Way
-> MemType -> Program pty n a -> n [(Either Condition a, Trace)]
runSCT Way
defaultWay MemType
defaultMemType (Program (WithSetupAndTeardown s ()) IO (Maybe Condition, o)
 -> IO [(Either Condition (Maybe Condition, o), Trace)])
-> Program (WithSetupAndTeardown s ()) IO (Maybe Condition, o)
-> IO [(Either Condition (Maybe Condition, o), Trace)]
forall a b. (a -> b) -> a -> b
$
    Program Basic IO s
-> (s
    -> Either Condition () -> Program Basic IO (Maybe Condition, o))
-> (s -> ConcIO ())
-> Program (WithSetupAndTeardown s ()) IO (Maybe Condition, o)
forall (n :: * -> *) x y a.
Program Basic n x
-> (x -> Either Condition y -> Program Basic n a)
-> (x -> Program Basic n y)
-> Program (WithSetupAndTeardown x y) n a
withSetupAndTeardown
      (Sig s o x -> x -> Program Basic IO s
forall s o x. Sig s o x -> x -> ConcIO s
initialise Sig s o x
sig x
x)
      (\s
s Either Condition ()
r -> do
          o
o <- Sig s o x -> s -> x -> ConcIO o
forall s o x. Sig s o x -> s -> x -> ConcIO o
observe Sig s o x
sig s
s x
x
          (Maybe Condition, o) -> Program Basic IO (Maybe Condition, o)
forall a. a -> Program Basic IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Condition -> Maybe Condition)
-> (() -> Maybe Condition)
-> Either Condition ()
-> Maybe Condition
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Condition -> Maybe Condition
forall a. a -> Maybe a
Just (Maybe Condition -> () -> Maybe Condition
forall a b. a -> b -> a
const Maybe Condition
forall a. Maybe a
Nothing) Either Condition ()
r, o
o))
      (\s
s -> do
          ThreadId
_ <- ConcIO () -> Program Basic IO (ThreadId (Program Basic IO))
forall (m :: * -> *). MonadConc m => m () -> m (ThreadId m)
fork (Sig s o x -> s -> x -> ConcIO ()
forall s o x. Sig s o x -> s -> x -> ConcIO ()
interfere Sig s o x
sig s
s x
x)
          ()
_ <- Sig s o x -> s -> ConcIO ()
forall s o x. Sig s o x -> s -> ConcIO ()
expression Sig s o x
sig s
s
          () -> ConcIO ()
forall a. a -> Program Basic IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
  Set (Maybe Condition, o) -> IO (Set (Maybe Condition, o))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set (Maybe Condition, o) -> IO (Set (Maybe Condition, o)))
-> ([(Maybe Condition, o)] -> Set (Maybe Condition, o))
-> [(Maybe Condition, o)]
-> IO (Set (Maybe Condition, o))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Maybe Condition, o)] -> Set (Maybe Condition, o)
forall a. Ord a => [a] -> Set a
S.fromList ([(Maybe Condition, o)] -> IO (Set (Maybe Condition, o)))
-> [(Maybe Condition, o)] -> IO (Set (Maybe Condition, o))
forall a b. (a -> b) -> a -> b
$ ((Either Condition (Maybe Condition, o), Trace)
 -> (Maybe Condition, o))
-> [(Either Condition (Maybe Condition, o), Trace)]
-> [(Maybe Condition, o)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Right (Maybe Condition, o)
a, Trace
_) -> (Maybe Condition, o)
a) [(Either Condition (Maybe Condition, o), Trace)]
results