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')