-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Test monadic programs using state machine based models
--   
--   See README at
--   <a>https://github.com/advancedtelematic/quickcheck-state-machine#readme</a>
@package quickcheck-state-machine
@version 0.6.0


-- | This module defines a predicate logic-like language and its
--   counterexample semantics.
module Test.StateMachine.Logic
data Logic
Bot :: Logic
Top :: Logic
(:&&) :: Logic -> Logic -> Logic
(:||) :: Logic -> Logic -> Logic
(:=>) :: Logic -> Logic -> Logic
Not :: Logic -> Logic
Predicate :: Predicate -> Logic
Forall :: [a] -> (a -> Logic) -> Logic
Exists :: [a] -> (a -> Logic) -> Logic
Boolean :: Bool -> Logic
Annotate :: String -> Logic -> Logic
data Predicate
(:==) :: a -> a -> Predicate
(:/=) :: a -> a -> Predicate
(:<) :: a -> a -> Predicate
(:<=) :: a -> a -> Predicate
(:>) :: a -> a -> Predicate
(:>=) :: a -> a -> Predicate
Elem :: a -> [a] -> Predicate
NotElem :: a -> [a] -> Predicate
dual :: Predicate -> Predicate
strongNeg :: Logic -> Logic
data Counterexample
BotC :: Counterexample
Fst :: Counterexample -> Counterexample
Snd :: Counterexample -> Counterexample
EitherC :: Counterexample -> Counterexample -> Counterexample
ImpliesC :: Counterexample -> Counterexample
NotC :: Counterexample -> Counterexample
PredicateC :: Predicate -> Counterexample
ForallC :: a -> Counterexample -> Counterexample
ExistsC :: [a] -> [Counterexample] -> Counterexample
BooleanC :: Counterexample
AnnotateC :: String -> Counterexample -> Counterexample
data Value
VFalse :: Counterexample -> Value
VTrue :: Value
boolean :: Logic -> Bool
logic :: Logic -> Value
predicate :: Predicate -> Value
(.==) :: (Eq a, Show a) => a -> a -> Logic
infix 5 .==
(./=) :: (Eq a, Show a) => a -> a -> Logic
infix 5 ./=
(.<) :: (Ord a, Show a) => a -> a -> Logic
infix 5 .<
(.<=) :: (Ord a, Show a) => a -> a -> Logic
infix 5 .<=
(.>) :: (Ord a, Show a) => a -> a -> Logic
infix 5 .>
(.>=) :: (Ord a, Show a) => a -> a -> Logic
infix 5 .>=
elem :: (Eq a, Show a) => a -> [a] -> Logic
infix 8 `elem`
notElem :: (Eq a, Show a) => a -> [a] -> Logic
infix 8 `notElem`
(.//) :: Logic -> String -> Logic
infixl 4 .//
(.&&) :: Logic -> Logic -> Logic
infixr 3 .&&
(.||) :: Logic -> Logic -> Logic
infixr 2 .||
(.=>) :: Logic -> Logic -> Logic
infixr 1 .=>
forall :: Show a => [a] -> (a -> Logic) -> Logic
exists :: Show a => [a] -> (a -> Logic) -> Logic
instance GHC.Show.Show Test.StateMachine.Logic.Value
instance GHC.Show.Show Test.StateMachine.Logic.Predicate
instance GHC.Show.Show Test.StateMachine.Logic.Counterexample

module Test.StateMachine.Types.Rank2
class Functor (f :: (k -> Type) -> Type)
fmap :: Functor f => (forall x. p x -> q x) -> f p -> f q
gfmap :: (Generic1 f, Functor (Rep1 f)) => (forall a. p a -> q a) -> f p -> f q
(<$>) :: Functor f => (forall x. p x -> q x) -> f p -> f q
class Foldable (f :: (k -> Type) -> Type)
foldMap :: (Foldable f, Monoid m) => (forall x. p x -> m) -> f p -> m
gfoldMap :: (Generic1 f, Foldable (Rep1 f), Monoid m) => (forall a. p a -> m) -> f p -> m
class (Functor t, Foldable t) => Traversable (t :: (k -> Type) -> Type)
traverse :: (Traversable t, Applicative f) => (forall a. p a -> f (q a)) -> t p -> f (t q)
gtraverse :: (Generic1 t, Traversable (Rep1 t), Applicative f) => (forall a. p a -> f (q a)) -> t p -> f (t q)
instance Test.StateMachine.Types.Rank2.Traversable GHC.Generics.U1
instance Test.StateMachine.Types.Rank2.Traversable (GHC.Generics.K1 i c)
instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Test.StateMachine.Types.Rank2.Traversable f, Test.StateMachine.Types.Rank2.Traversable g) => Test.StateMachine.Types.Rank2.Traversable (f GHC.Generics.:+: g)
instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Test.StateMachine.Types.Rank2.Traversable f, Test.StateMachine.Types.Rank2.Traversable g) => Test.StateMachine.Types.Rank2.Traversable (f GHC.Generics.:*: g)
instance forall k (f :: * -> *) (g :: (k -> *) -> *). (Data.Traversable.Traversable f, Test.StateMachine.Types.Rank2.Traversable g) => Test.StateMachine.Types.Rank2.Traversable (f GHC.Generics.:.: g)
instance forall k (f :: (k -> *) -> *) i (c :: GHC.Generics.Meta). Test.StateMachine.Types.Rank2.Traversable f => Test.StateMachine.Types.Rank2.Traversable (GHC.Generics.M1 i c f)
instance forall k (f :: (k -> *) -> *). Test.StateMachine.Types.Rank2.Traversable f => Test.StateMachine.Types.Rank2.Traversable (GHC.Generics.Rec1 f)
instance Test.StateMachine.Types.Rank2.Foldable GHC.Generics.U1
instance Test.StateMachine.Types.Rank2.Foldable (GHC.Generics.K1 i c)
instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Test.StateMachine.Types.Rank2.Foldable f, Test.StateMachine.Types.Rank2.Foldable g) => Test.StateMachine.Types.Rank2.Foldable (f GHC.Generics.:+: g)
instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Test.StateMachine.Types.Rank2.Foldable f, Test.StateMachine.Types.Rank2.Foldable g) => Test.StateMachine.Types.Rank2.Foldable (f GHC.Generics.:*: g)
instance forall k (f :: * -> *) (g :: (k -> *) -> *). (Data.Foldable.Foldable f, Test.StateMachine.Types.Rank2.Foldable g) => Test.StateMachine.Types.Rank2.Foldable (f GHC.Generics.:.: g)
instance forall k (f :: (k -> *) -> *) i (c :: GHC.Generics.Meta). Test.StateMachine.Types.Rank2.Foldable f => Test.StateMachine.Types.Rank2.Foldable (GHC.Generics.M1 i c f)
instance forall k (f :: (k -> *) -> *). Test.StateMachine.Types.Rank2.Foldable f => Test.StateMachine.Types.Rank2.Foldable (GHC.Generics.Rec1 f)
instance Test.StateMachine.Types.Rank2.Functor GHC.Generics.U1
instance Test.StateMachine.Types.Rank2.Functor (GHC.Generics.K1 i c)
instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Test.StateMachine.Types.Rank2.Functor f, Test.StateMachine.Types.Rank2.Functor g) => Test.StateMachine.Types.Rank2.Functor (f GHC.Generics.:+: g)
instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Test.StateMachine.Types.Rank2.Functor f, Test.StateMachine.Types.Rank2.Functor g) => Test.StateMachine.Types.Rank2.Functor (f GHC.Generics.:*: g)
instance forall k (f :: * -> *) (g :: (k -> *) -> *). (GHC.Base.Functor f, Test.StateMachine.Types.Rank2.Functor g) => Test.StateMachine.Types.Rank2.Functor (f GHC.Generics.:.: g)
instance forall k (f :: (k -> *) -> *) i (c :: GHC.Generics.Meta). Test.StateMachine.Types.Rank2.Functor f => Test.StateMachine.Types.Rank2.Functor (GHC.Generics.M1 i c f)
instance forall k (f :: (k -> *) -> *). Test.StateMachine.Types.Rank2.Functor f => Test.StateMachine.Types.Rank2.Functor (GHC.Generics.Rec1 f)


-- | This module contains reference related types. It's taken almost
--   verbatim from the Hedgehog <a>library</a>.
module Test.StateMachine.Types.References
newtype Var
Var :: Int -> Var
data Symbolic a
[Symbolic] :: Typeable a => Var -> Symbolic a
data Concrete a
[Concrete] :: Typeable a => a -> Concrete a
data Reference a r
Reference :: r a -> Reference a r
reference :: Typeable a => a -> Reference a Concrete
concrete :: Reference a Concrete -> a
opaque :: Reference (Opaque a) Concrete -> a
newtype Opaque a
Opaque :: a -> Opaque a
unOpaque :: Opaque a -> a
instance GHC.Classes.Ord a => GHC.Classes.Ord (Test.StateMachine.Types.References.Opaque a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Test.StateMachine.Types.References.Opaque a)
instance GHC.Generics.Generic (Test.StateMachine.Types.References.Reference a r)
instance Data.TreeDiff.Class.ToExpr Test.StateMachine.Types.References.Var
instance GHC.Generics.Generic Test.StateMachine.Types.References.Var
instance GHC.Show.Show Test.StateMachine.Types.References.Var
instance GHC.Classes.Ord Test.StateMachine.Types.References.Var
instance GHC.Classes.Eq Test.StateMachine.Types.References.Var
instance GHC.Show.Show (Test.StateMachine.Types.References.Symbolic a)
instance GHC.Classes.Eq (Test.StateMachine.Types.References.Symbolic a)
instance GHC.Classes.Ord (Test.StateMachine.Types.References.Symbolic a)
instance GHC.Show.Show a => GHC.Show.Show (Test.StateMachine.Types.References.Concrete a)
instance GHC.Show.Show (Test.StateMachine.Types.References.Opaque a)
instance Data.TreeDiff.Class.ToExpr (Test.StateMachine.Types.References.Opaque a)
instance Data.TreeDiff.Class.ToExpr (r a) => Data.TreeDiff.Class.ToExpr (Test.StateMachine.Types.References.Reference a r)
instance Test.StateMachine.Types.Rank2.Functor (Test.StateMachine.Types.References.Reference a)
instance Test.StateMachine.Types.Rank2.Foldable (Test.StateMachine.Types.References.Reference a)
instance Test.StateMachine.Types.Rank2.Traversable (Test.StateMachine.Types.References.Reference a)
instance (GHC.Classes.Eq a, Data.Functor.Classes.Eq1 r) => GHC.Classes.Eq (Test.StateMachine.Types.References.Reference a r)
instance (GHC.Classes.Ord a, Data.Functor.Classes.Ord1 r) => GHC.Classes.Ord (Test.StateMachine.Types.References.Reference a r)
instance (Data.Functor.Classes.Show1 r, GHC.Show.Show a) => GHC.Show.Show (Test.StateMachine.Types.References.Reference a r)
instance Data.Functor.Classes.Show1 Test.StateMachine.Types.References.Concrete
instance Data.Functor.Classes.Eq1 Test.StateMachine.Types.References.Concrete
instance Data.Functor.Classes.Ord1 Test.StateMachine.Types.References.Concrete
instance Data.TreeDiff.Class.ToExpr a => Data.TreeDiff.Class.ToExpr (Test.StateMachine.Types.References.Concrete a)
instance Data.Functor.Classes.Show1 Test.StateMachine.Types.References.Symbolic
instance Data.TreeDiff.Class.ToExpr a => Data.TreeDiff.Class.ToExpr (Test.StateMachine.Types.References.Symbolic a)
instance Data.Functor.Classes.Eq1 Test.StateMachine.Types.References.Symbolic
instance Data.Functor.Classes.Ord1 Test.StateMachine.Types.References.Symbolic


-- | This module contains the notion of a history of an execution of a
--   (parallel) program.
module Test.StateMachine.Types.History
newtype History cmd resp
History :: History' cmd resp -> History cmd resp
[unHistory] :: History cmd resp -> History' cmd resp
type History' cmd resp = [(Pid, HistoryEvent cmd resp)]
newtype Pid
Pid :: Int -> Pid
[unPid] :: Pid -> Int
data HistoryEvent cmd resp
Invocation :: !cmd Concrete -> !Set Var -> HistoryEvent cmd resp
Response :: !resp Concrete -> HistoryEvent cmd resp
Exception :: !String -> HistoryEvent cmd resp

-- | An operation packs up an invocation event with its corresponding
--   response event.
data Operation cmd resp
Operation :: cmd Concrete -> resp Concrete -> Pid -> Operation cmd resp
Crash :: cmd Concrete -> String -> Pid -> Operation cmd resp
makeOperations :: History' cmd resp -> [Operation cmd resp]

-- | Given a history, return all possible interleavings of invocations and
--   corresponding response events.
interleavings :: [(Pid, HistoryEvent cmd resp)] -> Forest (Operation cmd resp)
instance GHC.Show.Show Test.StateMachine.Types.History.Pid
instance GHC.Classes.Eq Test.StateMachine.Types.History.Pid
instance (GHC.Classes.Eq (cmd Test.StateMachine.Types.References.Concrete), GHC.Classes.Eq (resp Test.StateMachine.Types.References.Concrete)) => GHC.Classes.Eq (Test.StateMachine.Types.History.History cmd resp)
instance (GHC.Show.Show (cmd Test.StateMachine.Types.References.Concrete), GHC.Show.Show (resp Test.StateMachine.Types.References.Concrete)) => GHC.Show.Show (Test.StateMachine.Types.History.History cmd resp)
instance (GHC.Classes.Eq (cmd Test.StateMachine.Types.References.Concrete), GHC.Classes.Eq (resp Test.StateMachine.Types.References.Concrete)) => GHC.Classes.Eq (Test.StateMachine.Types.History.HistoryEvent cmd resp)
instance (GHC.Show.Show (cmd Test.StateMachine.Types.References.Concrete), GHC.Show.Show (resp Test.StateMachine.Types.References.Concrete)) => GHC.Show.Show (Test.StateMachine.Types.History.HistoryEvent cmd resp)
instance (GHC.Show.Show (cmd Test.StateMachine.Types.References.Concrete), GHC.Show.Show (resp Test.StateMachine.Types.References.Concrete)) => GHC.Show.Show (Test.StateMachine.Types.History.Operation cmd resp)


module Test.StateMachine.Types.GenSym
data GenSym a
runGenSym :: GenSym a -> Counter -> (a, Counter)
genSym :: Typeable a => GenSym (Reference a Symbolic)
data Counter
newCounter :: Counter
instance GHC.Base.Monad Test.StateMachine.Types.GenSym.GenSym
instance GHC.Base.Applicative Test.StateMachine.Types.GenSym.GenSym
instance GHC.Base.Functor Test.StateMachine.Types.GenSym.GenSym


-- | This module contains environments that are used to translate between
--   symbolic and concrete references. It's taken from the Hedgehog
--   <a>library</a>.
module Test.StateMachine.Types.Environment

-- | A mapping of symbolic values to concrete values.
newtype Environment
Environment :: Map Var Dynamic -> Environment
[unEnvironment] :: Environment -> Map Var Dynamic

-- | Environment errors.
data EnvironmentError
EnvironmentValueNotFound :: !Var -> EnvironmentError
EnvironmentTypeError :: !TypeRep -> !TypeRep -> EnvironmentError

-- | Create an empty environment.
emptyEnvironment :: Environment

-- | Insert a symbolic / concrete pairing in to the environment.
insertConcrete :: Var -> Dynamic -> Environment -> Environment
insertConcretes :: [Var] -> [Dynamic] -> Environment -> Environment

-- | Cast a <a>Dynamic</a> in to a concrete value.
reifyDynamic :: forall a. Typeable a => Dynamic -> Either EnvironmentError (Concrete a)

-- | Turns an environment in to a function for looking up a concrete value
--   from a symbolic one.
reifyEnvironment :: Environment -> forall a. Symbolic a -> Either EnvironmentError (Concrete a)

-- | Convert a symbolic structure to a concrete one, using the provided
--   environment.
reify :: Traversable t => Environment -> t Symbolic -> Either EnvironmentError (t Concrete)
instance GHC.Show.Show Test.StateMachine.Types.Environment.EnvironmentError
instance GHC.Classes.Ord Test.StateMachine.Types.Environment.EnvironmentError
instance GHC.Classes.Eq Test.StateMachine.Types.Environment.EnvironmentError
instance GHC.Show.Show Test.StateMachine.Types.Environment.Environment
instance GHC.Base.Monoid Test.StateMachine.Types.Environment.Environment
instance GHC.Base.Semigroup Test.StateMachine.Types.Environment.Environment


module Test.StateMachine.Types
data StateMachine model cmd m resp
StateMachine :: (forall r. model r) -> (forall r. (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r) -> (model Symbolic -> cmd Symbolic -> Logic) -> (model Concrete -> cmd Concrete -> resp Concrete -> Logic) -> Maybe (model Concrete -> Logic) -> (model Symbolic -> Maybe (Gen (cmd Symbolic))) -> Maybe (Matrix Int) -> (model Symbolic -> cmd Symbolic -> [cmd Symbolic]) -> (cmd Concrete -> m (resp Concrete)) -> (model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)) -> StateMachine model cmd m resp
[initModel] :: StateMachine model cmd m resp -> forall r. model r
[transition] :: StateMachine model cmd m resp -> forall r. (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r
[precondition] :: StateMachine model cmd m resp -> model Symbolic -> cmd Symbolic -> Logic
[postcondition] :: StateMachine model cmd m resp -> model Concrete -> cmd Concrete -> resp Concrete -> Logic
[invariant] :: StateMachine model cmd m resp -> Maybe (model Concrete -> Logic)
[generator] :: StateMachine model cmd m resp -> model Symbolic -> Maybe (Gen (cmd Symbolic))
[distribution] :: StateMachine model cmd m resp -> Maybe (Matrix Int)
[shrinker] :: StateMachine model cmd m resp -> model Symbolic -> cmd Symbolic -> [cmd Symbolic]
[semantics] :: StateMachine model cmd m resp -> cmd Concrete -> m (resp Concrete)
[mock] :: StateMachine model cmd m resp -> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)

-- | Previously symbolically executed command
--   
--   Invariant: the variables must be the variables in the response.
data Command cmd resp
Command :: !cmd Symbolic -> !resp Symbolic -> ![Var] -> Command cmd resp
newtype Commands cmd resp
Commands :: [Command cmd resp] -> Commands cmd resp
[unCommands] :: Commands cmd resp -> [Command cmd resp]
lengthCommands :: Commands cmd resp -> Int
data ParallelCommandsF t cmd resp
ParallelCommands :: !Commands cmd resp -> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
[prefix] :: ParallelCommandsF t cmd resp -> !Commands cmd resp
[suffixes] :: ParallelCommandsF t cmd resp -> [t (Commands cmd resp)]
type ParallelCommands = ParallelCommandsF Pair
data Pair a
Pair :: !a -> !a -> Pair a
[proj1] :: Pair a -> !a
[proj2] :: Pair a -> !a
fromPair :: Pair a -> (a, a)
toPair :: (a, a) -> Pair a
data Reason
Ok :: Reason
PreconditionFailed :: String -> Reason
PostconditionFailed :: String -> Reason
InvariantBroken :: String -> Reason
ExceptionThrown :: Reason
instance Data.Traversable.Traversable Test.StateMachine.Types.Pair
instance Data.Foldable.Foldable Test.StateMachine.Types.Pair
instance GHC.Base.Functor Test.StateMachine.Types.Pair
instance GHC.Show.Show a => GHC.Show.Show (Test.StateMachine.Types.Pair a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Test.StateMachine.Types.Pair a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Test.StateMachine.Types.Pair a)
instance GHC.Show.Show Test.StateMachine.Types.Reason
instance GHC.Classes.Eq Test.StateMachine.Types.Reason
instance GHC.Base.Monoid (Test.StateMachine.Types.Commands cmd resp)
instance GHC.Base.Semigroup (Test.StateMachine.Types.Commands cmd resp)
instance (GHC.Show.Show (cmd Test.StateMachine.Types.References.Symbolic), GHC.Show.Show (resp Test.StateMachine.Types.References.Symbolic)) => GHC.Show.Show (Test.StateMachine.Types.Command cmd resp)
instance (GHC.Show.Show (cmd Test.StateMachine.Types.References.Symbolic), GHC.Show.Show (resp Test.StateMachine.Types.References.Symbolic)) => GHC.Show.Show (Test.StateMachine.Types.Commands cmd resp)
instance (GHC.Show.Show (cmd Test.StateMachine.Types.References.Symbolic), GHC.Show.Show (resp Test.StateMachine.Types.References.Symbolic), GHC.Show.Show (t (Test.StateMachine.Types.Commands cmd resp))) => GHC.Show.Show (Test.StateMachine.Types.ParallelCommandsF t cmd resp)

module Test.StateMachine.ConstructorName

-- | The names of all possible commands
--   
--   This is used for things like tagging, coverage checking, etc.
class CommandNames (cmd :: k -> Type)

-- | Name of this particular command
cmdName :: CommandNames cmd => cmd r -> String

-- | Name of all possible commands
cmdNames :: CommandNames cmd => Proxy (cmd r) -> [String]

-- | Name of this particular command
cmdName :: (CommandNames cmd, Generic1 cmd, CommandNames (Rep1 cmd)) => cmd r -> String

-- | Name of all possible commands
cmdNames :: forall r. (CommandNames cmd, CommandNames (Rep1 cmd)) => Proxy (cmd r) -> [String]

-- | Convenience wrapper for <a>Command</a>
commandName :: CommandNames cmd => Command cmd resp -> String
instance Test.StateMachine.ConstructorName.CommandNames GHC.Generics.U1
instance Test.StateMachine.ConstructorName.CommandNames (GHC.Generics.K1 i c)
instance forall k (c :: GHC.Generics.Meta) (f :: k -> *). GHC.Generics.Constructor c => Test.StateMachine.ConstructorName.CommandNames (GHC.Generics.M1 GHC.Generics.C c f)
instance forall k (f :: k -> *) (c :: GHC.Generics.Meta). Test.StateMachine.ConstructorName.CommandNames f => Test.StateMachine.ConstructorName.CommandNames (GHC.Generics.M1 GHC.Generics.D c f)
instance forall k (f :: k -> *) (c :: GHC.Generics.Meta). Test.StateMachine.ConstructorName.CommandNames f => Test.StateMachine.ConstructorName.CommandNames (GHC.Generics.M1 GHC.Generics.S c f)
instance forall k (f :: k -> *) (g :: k -> *). (Test.StateMachine.ConstructorName.CommandNames f, Test.StateMachine.ConstructorName.CommandNames g) => Test.StateMachine.ConstructorName.CommandNames (f GHC.Generics.:+: g)
instance forall k (f :: k -> *) (g :: k -> *). (Test.StateMachine.ConstructorName.CommandNames f, Test.StateMachine.ConstructorName.CommandNames g) => Test.StateMachine.ConstructorName.CommandNames (f GHC.Generics.:*: g)
instance forall k (f :: k -> *). Test.StateMachine.ConstructorName.CommandNames f => Test.StateMachine.ConstructorName.CommandNames (GHC.Generics.Rec1 f)


-- | This module contains functions for visualing a history of a parallel
--   execution.
module Test.StateMachine.BoxDrawer

-- | Event invocation or response.
data EventType
Open :: EventType
Close :: EventType
data Fork a
Fork :: a -> a -> a -> Fork a

-- | Given a history, and output from processes generate Doc with boxes
exec :: [(EventType, Pid)] -> Fork [String] -> Doc
instance GHC.Base.Functor Test.StateMachine.BoxDrawer.Fork
instance GHC.Show.Show Test.StateMachine.BoxDrawer.EventType


-- | This module exports some QuickCheck utility functions. Some of these
--   should perhaps be upstreamed.
module Test.StateMachine.Utils

-- | Lifts a plain property into a monadic property.
liftProperty :: Monad m => Property -> PropertyM m ()

-- | Lifts <a>whenFail</a> to <a>PropertyM</a>.
whenFailM :: Monad m => IO () -> Property -> PropertyM m ()

-- | A variant of <a>forAllShrink</a> with an explicit show function.
forAllShrinkShow :: Testable prop => Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property

-- | Lifts <a>any</a> to properties.
anyP :: (a -> Property) -> [a] -> Property

-- | Same above, but for homogeneous pairs.
shrinkPair :: (a -> [a]) -> (a, a) -> [(a, a)]

-- | Given shrinkers for the components of a pair we can shrink the pair.
shrinkPair' :: (a -> [a]) -> (b -> [b]) -> (a, b) -> [(a, b)]
suchThatOneOf :: [(Int, Gen a)] -> (a -> Bool) -> Gen (Maybe a)
oldCover :: Testable prop => Bool -> Int -> String -> prop -> Property

-- | More permissive notion of shrinking where a value can shrink to itself
--   
--   For example
--   
--   <pre>
--   shrink  3 == [0, 2] -- standard QuickCheck shrink
--   shrinkS 3 == [Shrunk True 0, Shrunk True 2, Shrunk False 3]
--   </pre>
--   
--   This is primarily useful when shrinking composite structures: the
--   combinators here keep track of whether something was shrunk
--   <i>somewhere</i> in the structure. For example, we have
--   
--   <pre>
--      shrinkListS (shrinkPairS shrinkS shrinkS) [(1,3),(2,4)]
--   == [ Shrunk True  []             -- removed all elements of the list
--      , Shrunk True  [(2,4)]        -- removed the first
--      , Shrunk True  [(1,3)]        -- removed the second
--      , Shrunk True  [(0,3),(2,4)]  -- shrinking the '1'
--      , Shrunk True  [(1,0),(2,4)]  -- shrinking the '3'
--      , Shrunk True  [(1,2),(2,4)]  -- ..
--      , Shrunk True  [(1,3),(0,4)]  -- shrinking the '2'
--      , Shrunk True  [(1,3),(1,4)]  -- ..
--      , Shrunk True  [(1,3),(2,0)]  -- shrinking the '4'
--      , Shrunk True  [(1,3),(2,2)]  -- ..
--      , Shrunk True  [(1,3),(2,3)]  -- ..
--      , Shrunk False [(1,3),(2,4)]  -- the original unchanged list
--      ]
--   </pre>
data Shrunk a
Shrunk :: Bool -> a -> Shrunk a
[wasShrunk] :: Shrunk a -> Bool
[shrunk] :: Shrunk a -> a
shrinkS :: Arbitrary a => a -> [Shrunk a]
shrinkListS :: forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]

-- | Shrink list without shrinking elements
shrinkListS' :: [a] -> [Shrunk [a]]
shrinkPairS :: (a -> [Shrunk a]) -> (b -> [Shrunk b]) -> (a, b) -> [Shrunk (a, b)]
shrinkPairS' :: (a -> [Shrunk a]) -> (a, a) -> [Shrunk (a, a)]
instance GHC.Base.Functor Test.StateMachine.Utils.Shrunk
instance GHC.Show.Show a => GHC.Show.Show (Test.StateMachine.Utils.Shrunk a)


-- | This module contains helpers for generating, shrinking, and checking
--   sequential programs.
module Test.StateMachine.Sequential
forAllCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => CommandNames cmd => (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> (Commands cmd resp -> prop) -> Property
generateCommands :: (Foldable resp, Show (model Symbolic)) => CommandNames cmd => StateMachine model cmd m resp -> Maybe Int -> Gen (Commands cmd resp)
generateCommandsState :: forall model cmd m resp. Foldable resp => Show (model Symbolic) => CommandNames cmd => StateMachine model cmd m resp -> Counter -> Maybe Int -> StateT (model Symbolic, Maybe (cmd Symbolic)) Gen (Commands cmd resp)
measureFrequency :: (Foldable resp, Show (model Symbolic)) => CommandNames cmd => StateMachine model cmd m resp -> Maybe Int -> Int -> IO (Map (String, Maybe String) Int)
calculateFrequency :: CommandNames cmd => Commands cmd resp -> Map (String, Maybe String) Int
getUsedVars :: Foldable f => f Symbolic -> [Var]

-- | Shrink commands in a pre-condition and scope respecting way.
shrinkCommands :: forall model cmd m resp. (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Commands cmd resp -> [Commands cmd resp]

-- | Validate list of commands, optionally shrinking one of the commands
--   
--   The input to this function is a list of commands (<a>Commands</a>),
--   for example
--   
--   <pre>
--   [A, B, C, D, E, F, G, H]
--   </pre>
--   
--   The <i>result</i> is a <i>list</i> of <a>Commands</a>, i.e. a list of
--   lists. The outermost list is used for all the shrinking possibilities.
--   For example, let's assume we haven't shrunk something yet, and
--   therefore need to shrink one of the commands. Let's further assume
--   that only commands B and E can be shrunk, to B1, B2 and E1, E2, E3
--   respectively. Then the result will look something like
--   
--   <pre>
--   [    -- outermost list recording all the shrink possibilities
--       [A', B1', C', D', E' , F', G', H']   -- B shrunk to B1
--     , [A', B1', C', D', E' , F', G', H']   -- B shrunk to B2
--     , [A', B' , C', D', E1', F', G', H']   -- E shrunk to E1
--     , [A', B' , C', D', E2', F', G', H']   -- E shrunk to E2
--     , [A', B' , C', D', E3', F', G', H']   -- E shrunk to E3
--   ]
--   </pre>
--   
--   where one of the commands has been shrunk and all commands have been
--   validated and renumbered (references updated). So, in this example,
--   the result will contain at most 5 lists; it may contain fewer, since
--   some of these lists may not be valid.
--   
--   If we _did_ already shrink something, then no commands will be shrunk,
--   and the resulting list will either be empty (if the list of commands
--   was invalid) or contain a <i>single</i> element with the validated and
--   renumbered commands.
shrinkAndValidate :: forall model cmd m resp. (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)]

-- | Environment required during <a>shrinkAndValidate</a>
data ValidateEnv model
ValidateEnv :: model Symbolic -> Map Var Var -> Counter -> ValidateEnv model

-- | The model we're starting validation from
[veModel] :: ValidateEnv model -> model Symbolic

-- | Reference renumbering
--   
--   When a command
--   
--   <pre>
--   Command .. [Var i, ..]
--   </pre>
--   
--   is changed during validation to
--   
--   <pre>
--   Command .. [Var j, ..]
--   </pre>
--   
--   then any subsequent uses of <tt>Var i</tt> should be replaced by
--   <tt>Var j</tt>. This is recorded in <a>veScope</a>. When we
--   <i>remove</i> the first command altogether (during shrinking), then
--   <tt>Var i</tt> won't appear in the <a>veScope</a> and shrank
--   candidates that contain commands referring to <tt>Var i</tt> should be
--   considered as invalid.
[veScope] :: ValidateEnv model -> Map Var Var

-- | Counter (for generating new references)
[veCounter] :: ValidateEnv model -> Counter
data ShouldShrink
MustShrink :: ShouldShrink
DontShrink :: ShouldShrink
initValidateEnv :: model Symbolic -> ValidateEnv model
runCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadIO m) => StateMachine model cmd m resp -> Commands cmd resp -> PropertyM m (History cmd resp, model Concrete, Reason)
getChanContents :: MonadIO m => TChan a -> m [a]
executeCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadIO m) => StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Bool -> Commands cmd resp -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason
prettyPrintHistory :: forall model cmd m resp. ToExpr (model Concrete) => (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> IO ()
prettyCommands :: (MonadIO m, ToExpr (model Concrete)) => (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Property -> PropertyM m ()
commandNames :: forall cmd resp. CommandNames cmd => Commands cmd resp -> [(String, Int)]
commandNamesInOrder :: forall cmd resp. CommandNames cmd => Commands cmd resp -> [String]

-- | Print distribution of commands and fail if some commands have not been
--   executed.
checkCommandNames :: forall cmd resp. CommandNames cmd => Commands cmd resp -> Property -> Property
transitionMatrix :: forall cmd. CommandNames cmd => Proxy (cmd Symbolic) -> (String -> String -> Int) -> Matrix Int


-- | This module contains helpers for generating, shrinking, and checking
--   parallel programs.
module Test.StateMachine.Parallel
forAllParallelCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => CommandNames cmd => (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> (ParallelCommands cmd resp -> prop) -> Property

-- | Generate parallel commands.
--   
--   Parallel commands are generated as follows. We begin by generating
--   sequential commands and then splitting this list in two at some index.
--   The first half will be used as the prefix.
--   
--   The second half will be used to build suffixes. For example, starting
--   from the following sequential commands:
--   
--   <pre>
--   [A, B, C, D, E, F, G, H, I]
--   </pre>
--   
--   We split it in two, giving us the prefix and the rest:
--   
--   <pre>
--   prefix: [A, B]
--   rest:   [C, D, E, F, G, H, I]
--   </pre>
--   
--   We advance the model with the prefix.
--   
--   <b>Make a suffix</b>: we take commands from <tt>rest</tt> as long as
--   these are parallel safe (see <a>parallelSafe</a>). This means that the
--   pre-conditions (using the 'advanced' model) of each of those commands
--   will hold no matter in which order they are executed.
--   
--   Say this is true for <tt>[C, D, E]</tt>, but not anymore for
--   <tt>F</tt>, maybe because <tt>F</tt> depends on one of <tt>[C, D,
--   E]</tt>. Then we divide this 'chunk' in two by splitting it in the
--   middle, obtaining <tt>[C]</tt> and <tt>[D, E]</tt>. These two halves
--   of the chunk (stored as a <a>Pair</a>) will later be executed in
--   parallel. Together they form one suffix.
--   
--   Then the model is advanced using the whole chunk <tt>[C, D, E]</tt>.
--   Think of it as a barrier after executing the two halves of the chunk
--   in parallel. Then this process of building a chunk/suffix repeats
--   itself, starting from <b>Make a suffix</b> using the 'advanced' model.
--   
--   In the end we might end up with something like this:
--   
--   <pre>
--           ┌─ [C] ──┐  ┌ [F, G] ┐
--   [A, B] ─┤        ├──┤        │
--           └ [D, E] ┘  └ [H, I] ┘
--   </pre>
generateParallelCommands :: forall model cmd m resp. (Foldable resp, Show (model Symbolic)) => CommandNames cmd => StateMachine model cmd m resp -> Gen (ParallelCommands cmd resp)

-- | Shrink a parallel program in a pre-condition and scope respecting way.
shrinkParallelCommands :: forall cmd model m resp. Traversable cmd => Foldable resp => StateMachine model cmd m resp -> ParallelCommands cmd resp -> [ParallelCommands cmd resp]
shrinkAndValidateParallel :: forall model cmd m resp. (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> ParallelCommands cmd resp -> [ParallelCommands cmd resp]
runParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadCatch m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, Logic)]
runParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadCatch m, MonadUnliftIO m) => Int -> StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, Logic)]
executeParallelCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> m (History cmd resp, Reason)

-- | Try to linearise a history of a parallel program execution using a
--   sequential model. See the *Linearizability: a correctness condition
--   for concurrent objects* paper linked to from the README for more info.
linearise :: forall model cmd m resp. (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Logic

-- | Draw an ASCII diagram of the history of a parallel program. Useful for
--   seeing how a race condition might have occured.
toBoxDrawings :: forall cmd resp. Foldable cmd => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> History cmd resp -> Doc

-- | Takes the output of parallel program runs and pretty prints a
--   counterexample if any of the runs fail.
prettyParallelCommands :: (MonadIO m, Foldable cmd) => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> [(History cmd resp, Logic)] -> PropertyM m ()

-- | Apply the transition of some commands to a model.
advanceModel :: StateMachine model cmd m resp -> model Symbolic -> Commands cmd resp -> model Symbolic


-- | The main module for state machine based testing, it contains
--   combinators that help you build sequential and parallel properties.
module Test.StateMachine
forAllCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => CommandNames cmd => (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> (Commands cmd resp -> prop) -> Property
transitionMatrix :: forall cmd. CommandNames cmd => Proxy (cmd Symbolic) -> (String -> String -> Int) -> Matrix Int
runCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadIO m) => StateMachine model cmd m resp -> Commands cmd resp -> PropertyM m (History cmd resp, model Concrete, Reason)
prettyCommands :: (MonadIO m, ToExpr (model Concrete)) => (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Property -> PropertyM m ()

-- | Print distribution of commands and fail if some commands have not been
--   executed.
checkCommandNames :: forall cmd resp. CommandNames cmd => Commands cmd resp -> Property -> Property
commandNames :: forall cmd resp. CommandNames cmd => Commands cmd resp -> [(String, Int)]
commandNamesInOrder :: forall cmd resp. CommandNames cmd => Commands cmd resp -> [String]
forAllParallelCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => CommandNames cmd => (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> (ParallelCommands cmd resp -> prop) -> Property
runParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadCatch m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, Logic)]
runParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadCatch m, MonadUnliftIO m) => Int -> StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, Logic)]

-- | Takes the output of parallel program runs and pretty prints a
--   counterexample if any of the runs fail.
prettyParallelCommands :: (MonadIO m, Foldable cmd) => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> [(History cmd resp, Logic)] -> PropertyM m ()
data StateMachine model cmd m resp
StateMachine :: (forall r. model r) -> (forall r. (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r) -> (model Symbolic -> cmd Symbolic -> Logic) -> (model Concrete -> cmd Concrete -> resp Concrete -> Logic) -> Maybe (model Concrete -> Logic) -> (model Symbolic -> Maybe (Gen (cmd Symbolic))) -> Maybe (Matrix Int) -> (model Symbolic -> cmd Symbolic -> [cmd Symbolic]) -> (cmd Concrete -> m (resp Concrete)) -> (model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)) -> StateMachine model cmd m resp
data Concrete a
data Symbolic a
data Reference a r
concrete :: Reference a Concrete -> a
reference :: Typeable a => a -> Reference a Concrete
newtype Opaque a
Opaque :: a -> Opaque a
[unOpaque] :: Opaque a -> a
opaque :: Reference (Opaque a) Concrete -> a
data Reason
Ok :: Reason
PreconditionFailed :: String -> Reason
PostconditionFailed :: String -> Reason
InvariantBroken :: String -> Reason
ExceptionThrown :: Reason
data GenSym a
genSym :: Typeable a => GenSym (Reference a Symbolic)

-- | The names of all possible commands
--   
--   This is used for things like tagging, coverage checking, etc.
class CommandNames (cmd :: k -> Type)

-- | Name of this particular command
cmdName :: CommandNames cmd => cmd r -> String

-- | Name of all possible commands
cmdNames :: CommandNames cmd => Proxy (cmd r) -> [String]

-- | Name of this particular command
cmdName :: (CommandNames cmd, Generic1 cmd, CommandNames (Rep1 cmd)) => cmd r -> String

-- | Name of all possible commands
cmdNames :: forall r. (CommandNames cmd, CommandNames (Rep1 cmd)) => Proxy (cmd r) -> [String]


-- | This module contains Z-inspried combinators for working with
--   relations. The idea is that they can be used to define concise and
--   showable models. This module is an experiment and will likely change
--   or move to its own package.
module Test.StateMachine.Z
cons :: a -> [a] -> [a]
union :: Eq a => [a] -> [a] -> [a]
infixr 6 `union`
intersect :: Eq a => [a] -> [a] -> [a]
infixr 7 `intersect`

-- | Subset.
--   
--   <pre>
--   &gt;&gt;&gt; boolean ([1, 2] `isSubsetOf` [3, 2, 1])
--   True
--   </pre>
isSubsetOf :: (Eq a, Show a) => [a] -> [a] -> Logic
infix 5 `isSubsetOf`

-- | Set equality.
--   
--   <pre>
--   &gt;&gt;&gt; boolean ([1, 1, 2] ~= [2, 1])
--   True
--   </pre>
(~=) :: (Eq a, Show a) => [a] -> [a] -> Logic
infix 5 ~=

-- | Relations.
type Rel a b = [(a, b)]

-- | (Partial) functions.
type Fun a b = Rel a b
type a :<-> b = Rel a b
infixr 1 :<->
type a :-> b = Fun a b
infixr 1 :->
type a :/-> b = Fun a b
infixr 1 :/->
empty :: Rel a b
identity :: [a] -> Rel a a
singleton :: a -> b -> Rel a b
domain :: Rel a b -> [a]
codomain :: Rel a b -> [b]
compose :: Eq b => Rel b c -> Rel a b -> Rel a c
fcompose :: Eq b => Rel a b -> Rel b c -> Rel a c
inverse :: Rel a b -> Rel b a
lookupDom :: Eq a => a -> Rel a b -> [b]
lookupCod :: Eq b => b -> Rel a b -> [a]

-- | Domain restriction.
--   
--   <pre>
--   &gt;&gt;&gt; ['a'] &lt;| [ ('a', "apa"), ('b', "bepa") ]
--   [('a',"apa")]
--   </pre>
(<|) :: Eq a => [a] -> Rel a b -> Rel a b
infixr 4 <|

-- | Codomain restriction.
--   
--   <pre>
--   &gt;&gt;&gt; [ ('a', "apa"), ('b', "bepa") ] |&gt; ["apa"]
--   [('a',"apa")]
--   </pre>
(|>) :: Eq b => Rel a b -> [b] -> Rel a b
infixl 4 |>

-- | Domain substraction.
--   
--   <pre>
--   &gt;&gt;&gt; ['a'] &lt;-| [ ('a', "apa"), ('b', "bepa") ]
--   [('b',"bepa")]
--   </pre>
(<-|) :: Eq a => [a] -> Rel a b -> Rel a b
infixr 4 <-|

-- | Codomain substraction.
--   
--   <pre>
--   &gt;&gt;&gt; [ ('a', "apa"), ('b', "bepa"), ('c', "cepa") ] |-&gt; ["apa"]
--   [('b',"bepa"),('c',"cepa")]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; [ ('a', "apa"), ('b', "bepa"), ('c', "cepa") ] |-&gt; ["apa", "cepa"]
--   [('b',"bepa")]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; [ ('a', "apa"), ('b', "bepa"), ('c', "cepa") ] |-&gt; ["apa"] |-&gt; ["cepa"]
--   [('b',"bepa")]
--   </pre>
(|->) :: Eq b => Rel a b -> [b] -> Rel a b
infixl 4 |->

-- | The image of a relation.
image :: Eq a => Rel a b -> [a] -> [b]

-- | Overriding.
--   
--   <pre>
--   &gt;&gt;&gt; [('a', "apa")] &lt;+ [('a', "bepa")]
--   [('a',"bepa")]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; [('a', "apa")] &lt;+ [('b', "bepa")]
--   [('a',"apa"),('b',"bepa")]
--   </pre>
(<+) :: (Eq a, Eq b) => Rel a b -> Rel a b -> Rel a b
infixr 4 <+

-- | Direct product.
(<**>) :: Eq a => Rel a b -> Rel a c -> Rel a (b, c)
infixl 4 <**>

-- | Parallel product.
(<||>) :: Rel a c -> Rel b d -> Rel (a, b) (c, d)
infixl 4 <||>
isTotalRel :: (Eq a, Show a) => Rel a b -> [a] -> Logic
isSurjRel :: (Eq b, Show b) => Rel a b -> [b] -> Logic
isTotalSurjRel :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> [b] -> Logic
isPartialFun :: (Eq a, Eq b, Show b) => Rel a b -> Logic
isTotalFun :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> Logic
isPartialInj :: (Eq a, Eq b, Show a, Show b) => Rel a b -> Logic
isTotalInj :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> Logic
isPartialSurj :: (Eq a, Eq b, Show b) => Rel a b -> [b] -> Logic
isTotalSurj :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> [b] -> Logic
isBijection :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> [b] -> Logic

-- | Application.
(!) :: (Eq a, Show a, Show b) => Fun a b -> a -> b
(!?) :: Eq a => Fun a b -> a -> Maybe b
(.%) :: (Eq a, Eq b, Show a, Show b) => (Fun a b, a) -> (b -> b) -> Fun a b
infixr 4 .%
(.!) :: Rel a b -> a -> (Rel a b, a)
infixr 9 .!

-- | Assignment.
--   
--   <pre>
--   &gt;&gt;&gt; singleton 'a' "apa" .! 'a' .= "bepa"
--   [('a',"bepa")]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; singleton 'a' "apa" .! 'b' .= "bepa"
--   [('a',"apa"),('b',"bepa")]
--   </pre>
(.=) :: (Eq a, Eq b) => (Rel a b, a) -> b -> Rel a b
infix 4 .=