module Polysemy.State.Keyed.Law where

import Data.Constraint.Extras
import Data.GADT.Compare
import Data.GADT.Show
import Data.Some
import Data.Type.Equality
import Polysemy
import Polysemy.Law
import Polysemy.State.Keyed

prop_lawfulKeyedState ::
  forall k r.
  MakeLaw (KeyedState k) r =>
  (forall a. Eq a => Eq (k a), GEq k, GShow k) =>
  (Has Show k, Has Eq k, Has Arbitrary k, Arbitrary (Some k)) =>
  InterpreterFor (KeyedState k) r -> Property
prop_lawfulKeyedState :: InterpreterFor (KeyedState k) r -> Property
prop_lawfulKeyedState InterpreterFor (KeyedState k) r
f = InterpreterFor (KeyedState k) r -> Law (KeyedState k) r -> Property
forall (e :: Effect) (r :: [Effect]).
InterpreterFor e r -> Law e r -> Property
runLaw InterpreterFor (KeyedState k) r
f Law (KeyedState k) r
forall (k :: * -> *) (r :: [Effect]).
(MakeLaw (KeyedState k) r, forall a. Eq a => Eq (k a), GEq k,
 GShow k, Has Show k, Has Eq k, Has Arbitrary k,
 Arbitrary (Some k)) =>
Law (KeyedState k) r
law_consistency

newtype KeyValuePair k a = KeyValuePair (k a, a)

instance GEq k => GEq (KeyValuePair k) where
  geq :: KeyValuePair k a -> KeyValuePair k b -> Maybe (a :~: b)
geq (KeyValuePair (k a
x,a
_)) (KeyValuePair (k b
y,b
_)) = k a -> k b -> Maybe (a :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq k a
x k b
y

instance (Has Arbitrary k, Arbitrary (Some k)) => Arbitrary (Some (KeyValuePair k)) where
  arbitrary :: Gen (Some (KeyValuePair k))
arbitrary =
    Gen (Some k)
-> (forall a. k a -> Gen (Some (KeyValuePair k)))
-> Gen (Some (KeyValuePair k))
forall k (m :: * -> *) (tag :: k -> *) r.
Monad m =>
m (Some tag) -> (forall (a :: k). tag a -> m r) -> m r
withSomeM Gen (Some k)
forall a. Arbitrary a => Gen a
arbitrary ((forall a. k a -> Gen (Some (KeyValuePair k)))
 -> Gen (Some (KeyValuePair k)))
-> (forall a. k a -> Gen (Some (KeyValuePair k)))
-> Gen (Some (KeyValuePair k))
forall a b. (a -> b) -> a -> b
$ \(k :: k a) ->
      k a
-> (Arbitrary a => Gen (Some (KeyValuePair k)))
-> Gen (Some (KeyValuePair k))
forall k (c :: k -> Constraint) (f :: k -> *) (a :: k) r.
Has c f =>
f a -> (c a => r) -> r
has @Arbitrary k a
k ((Arbitrary a => Gen (Some (KeyValuePair k)))
 -> Gen (Some (KeyValuePair k)))
-> (Arbitrary a => Gen (Some (KeyValuePair k)))
-> Gen (Some (KeyValuePair k))
forall a b. (a -> b) -> a -> b
$ KeyValuePair k a -> Some (KeyValuePair k)
forall k (tag :: k -> *) (a :: k). tag a -> Some tag
Some (KeyValuePair k a -> Some (KeyValuePair k))
-> (a -> KeyValuePair k a) -> a -> Some (KeyValuePair k)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (k a, a) -> KeyValuePair k a
forall (k :: * -> *) a. (k a, a) -> KeyValuePair k a
KeyValuePair ((k a, a) -> KeyValuePair k a)
-> (a -> (k a, a)) -> a -> KeyValuePair k a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (k a
k,) (a -> Some (KeyValuePair k))
-> Gen a -> Gen (Some (KeyValuePair k))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen a
forall a. Arbitrary a => Gen a
arbitrary

instance (Has Show k, GShow k) => GShow (KeyValuePair k) where
  gshowsPrec :: Int -> KeyValuePair k a -> ShowS
gshowsPrec Int
i (KeyValuePair (k a
k, a
x)) String
s =
    k a -> (Show a => String) -> String
forall k (c :: k -> Constraint) (f :: k -> *) (a :: k) r.
Has c f =>
f a -> (c a => r) -> r
has @Show k a
k ((Show a => String) -> String) -> (Show a => String) -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"(", Int -> k a -> ShowS
forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
gshowsPrec Int
i k a
k String
"", String
", ", Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
i a
x String
"", String
")", String
s]

law_consistency ::
  forall k r.
  MakeLaw (KeyedState k) r =>
  (forall a. Eq a => Eq (k a), GEq k, GShow k) =>
  (Has Show k, Has Eq k, Has Arbitrary k, Arbitrary (Some k)) =>
  Law (KeyedState k) r
law_consistency :: Law (KeyedState k) r
law_consistency =
  String
-> (Some (KeyValuePair k)
    -> Some k -> Sem (KeyedState k : r) (Some (KeyValuePair k)))
-> String
-> (Some (KeyValuePair k)
    -> Some k -> Sem (KeyedState k : r) (Some (KeyValuePair k)))
-> Law (KeyedState k) 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 @_ @_ @_ @(_ -> _ -> Sem _ (Some (KeyValuePair k)))
    String
"uncurry putAt %1 *> getAt %2"
    (\(Some (KeyValuePair (k, x))) (Some k') ->
      k a -> a -> Sem (KeyedState k : r) ()
forall (k :: * -> *) (r :: [Effect]) a.
MemberWithError (KeyedState k) r =>
k a -> a -> Sem r ()
putAt k a
k a
x Sem (KeyedState k : r) ()
-> Sem (KeyedState k : r) (Some (KeyValuePair k))
-> Sem (KeyedState k : r) (Some (KeyValuePair k))
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (KeyValuePair k a -> Some (KeyValuePair k)
forall k (tag :: k -> *) (a :: k). tag a -> Some tag
Some (KeyValuePair k a -> Some (KeyValuePair k))
-> (a -> KeyValuePair k a) -> a -> Some (KeyValuePair k)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (k a, a) -> KeyValuePair k a
forall (k :: * -> *) a. (k a, a) -> KeyValuePair k a
KeyValuePair ((k a, a) -> KeyValuePair k a)
-> (a -> (k a, a)) -> a -> KeyValuePair k a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (k a
k',) (a -> Some (KeyValuePair k))
-> Sem (KeyedState k : r) a
-> Sem (KeyedState k : r) (Some (KeyValuePair k))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> k a -> Sem (KeyedState k : r) a
forall (k :: * -> *) (r :: [Effect]) a.
MemberWithError (KeyedState k) r =>
k a -> Sem r a
getAt k a
k'))
    String
"if fst %1 == %2 then pure (snd %1) else getAt %2"
    (\(Some (KeyValuePair (k, x))) (Some k') ->
      case k a -> k a -> Maybe (a :~: a)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq k a
k k a
k' of
        Just a :~: a
Refl | k a -> (Eq a => Bool) -> Bool
forall k (c :: k -> Constraint) (f :: k -> *) (a :: k) r.
Has c f =>
f a -> (c a => r) -> r
has @Eq k a
k ((Eq a => Bool) -> Bool) -> (Eq a => Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ k a
k k a -> k a -> Bool
forall a. Eq a => a -> a -> Bool
== k a
k a
k' -> Some (KeyValuePair k)
-> Sem (KeyedState k : r) (Some (KeyValuePair k))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Some (KeyValuePair k)
 -> Sem (KeyedState k : r) (Some (KeyValuePair k)))
-> Some (KeyValuePair k)
-> Sem (KeyedState k : r) (Some (KeyValuePair k))
forall a b. (a -> b) -> a -> b
$ KeyValuePair k a -> Some (KeyValuePair k)
forall k (tag :: k -> *) (a :: k). tag a -> Some tag
Some (KeyValuePair k a -> Some (KeyValuePair k))
-> KeyValuePair k a -> Some (KeyValuePair k)
forall a b. (a -> b) -> a -> b
$ (k a, a) -> KeyValuePair k a
forall (k :: * -> *) a. (k a, a) -> KeyValuePair k a
KeyValuePair (k a
k, a
x)
        Maybe (a :~: a)
_ -> KeyValuePair k a -> Some (KeyValuePair k)
forall k (tag :: k -> *) (a :: k). tag a -> Some tag
Some (KeyValuePair k a -> Some (KeyValuePair k))
-> (a -> KeyValuePair k a) -> a -> Some (KeyValuePair k)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (k a, a) -> KeyValuePair k a
forall (k :: * -> *) a. (k a, a) -> KeyValuePair k a
KeyValuePair ((k a, a) -> KeyValuePair k a)
-> (a -> (k a, a)) -> a -> KeyValuePair k a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (k a
k',) (a -> Some (KeyValuePair k))
-> Sem (KeyedState k : r) a
-> Sem (KeyedState k : r) (Some (KeyValuePair k))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> k a -> Sem (KeyedState k : r) a
forall (k :: * -> *) (r :: [Effect]) a.
MemberWithError (KeyedState k) r =>
k a -> Sem r a
getAt k a
k')