{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}

module Polysemy.State.Law where

import Polysemy
import Polysemy.Law
import Polysemy.State
import Control.Applicative
import Control.Arrow


------------------------------------------------------------------------------
-- | A collection of laws that show a `State` interpreter is correct.
prop_lawfulState
    :: forall r s
     . (Eq s, Show s, Arbitrary s, MakeLaw (State s) r)
    => InterpreterFor (State s) r
    -> Property
prop_lawfulState :: InterpreterFor (State s) r -> Property
prop_lawfulState InterpreterFor (State s) r
i12n = [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
  [ InterpreterFor (State s) r -> Law (State s) r -> Property
forall (e :: Effect) (r :: [Effect]).
InterpreterFor e r -> Law e r -> Property
runLaw InterpreterFor (State s) r
i12n Law (State s) r
forall s (r :: [Effect]).
(Eq s, Arbitrary s, Show s, MakeLaw (State s) r) =>
Law (State s) r
law_putTwice
  , InterpreterFor (State s) r -> Law (State s) r -> Property
forall (e :: Effect) (r :: [Effect]).
InterpreterFor e r -> Law e r -> Property
runLaw InterpreterFor (State s) r
i12n Law (State s) r
forall s (r :: [Effect]).
(Eq s, Arbitrary s, Show s, MakeLaw (State s) r) =>
Law (State s) r
law_getTwice
  , InterpreterFor (State s) r -> Law (State s) r -> Property
forall (e :: Effect) (r :: [Effect]).
InterpreterFor e r -> Law e r -> Property
runLaw InterpreterFor (State s) r
i12n Law (State s) r
forall s (r :: [Effect]).
(Eq s, Arbitrary s, Show s, MakeLaw (State s) r) =>
Law (State s) r
law_getPutGet
  ]


law_putTwice
    :: forall s r
     . (Eq s, Arbitrary s, Show s, MakeLaw (State s) r)
    => Law (State s) r
law_putTwice :: Law (State s) r
law_putTwice =
  String
-> (s -> s -> Sem (State s : r) s)
-> String
-> (s -> s -> Sem (State s : r) s)
-> Law (State s) r
forall (e :: Effect) (r :: [Effect]) a res.
(MakeLaw e r, Eq a, Show a, Citizen res (Sem (e : r) a)) =>
String -> res -> String -> res -> Law e r
mkLaw
    String
"put %1 >> put %2 >> get"
    (\s
s s
s' -> s -> Sem (State s : r) ()
forall s (r :: [Effect]).
MemberWithError (State s) r =>
s -> Sem r ()
put @s s
s Sem (State s : r) ()
-> Sem (State s : r) () -> Sem (State s : r) ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> s -> Sem (State s : r) ()
forall s (r :: [Effect]).
MemberWithError (State s) r =>
s -> Sem r ()
put @s s
s' Sem (State s : r) () -> Sem (State s : r) s -> Sem (State s : r) s
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (r :: [Effect]). MemberWithError (State s) r => Sem r s
forall s (r :: [Effect]). MemberWithError (State s) r => Sem r s
get @s)
    String
"put %2 >> get"
    (\s
_ s
s' ->             s -> Sem (State s : r) ()
forall s (r :: [Effect]).
MemberWithError (State s) r =>
s -> Sem r ()
put @s s
s' Sem (State s : r) () -> Sem (State s : r) s -> Sem (State s : r) s
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (r :: [Effect]). MemberWithError (State s) r => Sem r s
forall s (r :: [Effect]). MemberWithError (State s) r => Sem r s
get @s)

law_getTwice
    :: forall s r
     . (Eq s, Arbitrary s, Show s, MakeLaw (State s) r)
    => Law (State s) r
law_getTwice :: Law (State s) r
law_getTwice =
  String
-> Sem (State s : r) (s, s)
-> String
-> Sem (State s : r) (s, s)
-> Law (State s) r
forall (e :: Effect) (r :: [Effect]) a res.
(MakeLaw e r, Eq a, Show a, Citizen res (Sem (e : r) a)) =>
String -> res -> String -> res -> Law e r
mkLaw
    String
"liftA2 (,) get get"
    ((s -> s -> (s, s))
-> Sem (State s : r) s
-> Sem (State s : r) s
-> Sem (State s : r) (s, s)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,) (forall (r :: [Effect]). MemberWithError (State s) r => Sem r s
forall s (r :: [Effect]). MemberWithError (State s) r => Sem r s
get @s) (forall (r :: [Effect]). MemberWithError (State s) r => Sem r s
forall s (r :: [Effect]). MemberWithError (State s) r => Sem r s
get @s))
    String
"(id &&& id) <$> get"
    ((s -> s
forall a. a -> a
id (s -> s) -> (s -> s) -> s -> (s, s)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& s -> s
forall a. a -> a
id) (s -> (s, s)) -> Sem (State s : r) s -> Sem (State s : r) (s, s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: [Effect]). MemberWithError (State s) r => Sem r s
forall s (r :: [Effect]). MemberWithError (State s) r => Sem r s
get @s)

law_getPutGet
    :: forall s r
     . (Eq s, Arbitrary s, Show s, MakeLaw (State s) r)
    => Law (State s) r
law_getPutGet :: Law (State s) r
law_getPutGet =
  String
-> Sem (State s : r) s
-> String
-> Sem (State s : r) s
-> Law (State s) r
forall (e :: Effect) (r :: [Effect]) a res.
(MakeLaw e r, Eq a, Show a, Citizen res (Sem (e : r) a)) =>
String -> res -> String -> res -> Law e r
mkLaw
    String
"get >>= put >> get"
    (forall (r :: [Effect]). MemberWithError (State s) r => Sem r s
forall s (r :: [Effect]). MemberWithError (State s) r => Sem r s
get @s Sem (State s : r) s
-> (s -> Sem (State s : r) ()) -> Sem (State s : r) ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (r :: [Effect]).
MemberWithError (State s) r =>
s -> Sem r ()
forall s (r :: [Effect]).
MemberWithError (State s) r =>
s -> Sem r ()
put @s Sem (State s : r) () -> Sem (State s : r) s -> Sem (State s : r) s
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (r :: [Effect]). MemberWithError (State s) r => Sem r s
forall s (r :: [Effect]). MemberWithError (State s) r => Sem r s
get @s)
    String
"get"
    (forall (r :: [Effect]). MemberWithError (State s) r => Sem r s
forall s (r :: [Effect]). MemberWithError (State s) r => Sem r s
get @s)