{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module ADD.Games.Correct where
import Data.Foldable
import qualified Data.Set as S
import Data.Set (Set)
import Data.Data
import Data.Word
import GHC.Generics
import Test.QuickCheck hiding (Result)
import Control.Monad.Writer
import Data.Tuple (swap)
import Data.List
import QuickSpec
data Event = Event Word8
deriving stock (Eq, Ord, Show, Data, Generic)
-- # ArbitraryEvent
instance Arbitrary Event where
arbitrary = Event <$> arbitrary
shrink = genericShrink
data EventFilter
= Always
| Never
| Exactly Word8 -- ! 1
deriving stock (Eq, Ord, Show, Data, Generic)
-- # ArbitraryEventFilter
instance Arbitrary EventFilter where
arbitrary = frequency
[ (3, pure Always)
, (1, pure Never)
, (5, Exactly <$> arbitrary)
]
shrink = genericShrink
always :: EventFilter
always = Always
never :: EventFilter
never = Never
sig_filters :: Sig
sig_filters = signature
[ con "always" always
, con "never" never
]
data Reward = Reward Word8
deriving stock (Eq, Ord, Show, Data, Generic)
-- # ArbitraryReward
instance Arbitrary Reward where
arbitrary = Reward <$> arbitrary
shrink = genericShrink
data Result
= Victory
| Defeat
deriving stock (Eq, Ord, Show, Data, Generic)
-- # ArbitraryResult
instance Arbitrary Result where
arbitrary = elements [ victory, defeat ]
shrink = genericShrink
victory :: Result
victory = Victory
defeat :: Result
defeat = Defeat
sig_results :: Sig
sig_results = signature
[ con "victory" victory
, con "defeat" defeat
]
------------------------------------------------------------------------------
-- constructors
------------------------------------------------------------------------------
data Game
= Win
| Lose
| RewardThen Reward Game
| Subgame Game Game Game
| EitherW Game Game
| Both Game Game
| Race Game Game
| Multigate [(EventFilter, Game)]
deriving stock (Eq, Ord, Show, Data, Generic)
-- # ArbitraryGame
instance Arbitrary Game where
arbitrary = sized $ \n ->
case n <= 1 of
True -> elements [win, lose]
False -> frequency
[ (3, pure win)
, (3, pure lose)
, (3, reward <$> arbitrary)
, (5, rewardThen <$> arbitrary
<*> decayArbitrary 2)
, (5, andThen <$> decayArbitrary 2
<*> decayArbitrary 2)
, (5, subgame <$> decayArbitrary 3
<*> decayArbitrary 3
<*> decayArbitrary 3)
, (5, both <$> decayArbitrary 2
<*> decayArbitrary 2)
, (5, eitherG <$> decayArbitrary 2
<*> decayArbitrary 2)
, (5, race <$> decayArbitrary 2
<*> decayArbitrary 2)
, (5, multigate <$> decayArbitrary 5)
, (2, comeback <$> arbitrary)
, (1, pure bottom)
, (5, gate <$> arbitrary <*> arbitrary)
]
shrink = genericShrink
-- # ObserveGame
instance
Observe [Event] (Set Reward, Maybe Result) Game
where
observe = runGame
decayArbitrary :: Arbitrary a => Int -> Gen a
decayArbitrary n = scale (`div` n) arbitrary
reward :: Reward -> Game
reward r = rewardThen r win
rewardThen :: Reward -> Game -> Game
rewardThen = RewardThen
win :: Game
win = Win
lose :: Game
lose = Lose
andThen :: Game -> Game -> Game
andThen g1 g2 = subgame g1 g2 lose
subgame :: Game -> Game -> Game -> Game
subgame (RewardThen r g) g1 g2 =
rewardThen r (subgame g g1 g2)
subgame Win g1 _ = g1
subgame Lose _ g2 = g2
subgame g g1 g2 = Subgame g g1 g2
eitherG :: Game -> Game -> Game
eitherG (RewardThen r g1) g2 =
rewardThen r (eitherG g1 g2)
eitherG g1 (RewardThen r g2) =
rewardThen r (eitherG g1 g2)
eitherG Lose Lose = lose
eitherG Win _ = win
eitherG _ Win = win
eitherG a b = EitherW a b
both :: Game -> Game -> Game
both (RewardThen r g1) g2 = rewardThen r (both g1 g2)
both g1 (RewardThen r g2) = rewardThen r (both g1 g2)
both Win Win = win
both Lose _ = lose
both _ Lose = lose
both a b = Both a b
race :: Game -> Game -> Game
race (RewardThen r g1) g2 = rewardThen r (race g1 g2)
race g1 (RewardThen r g2) = rewardThen r (race g1 g2)
race Win _ = win
race Lose _ = lose
race _ Win = win
race _ Lose = lose
race a b = Race a b
multigate :: [(EventFilter, Game)] -> Game
multigate cs = Multigate cs
sig_games_core :: Sig
sig_games_core = signature
[ con "win" win
, con "lose" lose
, con "subgame" subgame
, con "eitherG" eitherG
, con "both" both
, con "race" race
, con "multigate" multigate
, con "rewardThen" rewardThen
, con "gate" gate
]
------------------------------------------------------------------------------
-- extensions
------------------------------------------------------------------------------
comeback :: Game -> Game
comeback g = subgame g lose win
bottom :: Game
bottom = multigate []
gate :: EventFilter -> Game -> Game
gate ef g = multigate [(ef, g)]
sig_games_ext :: Sig
sig_games_ext = signature
[ con "comeback" comeback
, con "bottom" bottom
, con "andThen" andThen
, con "reward" reward
]
bingo :: [[Game]] -> Reward -> Game
bingo squares r
= let subgames = squares
++ transpose squares -- ! 1
allOf :: [Game] -> Game
allOf = foldr both win
anyOf :: [Game] -> Game
anyOf = foldr eitherG lose
in subgame (anyOf (fmap allOf subgames)) (reward r) lose
------------------------------------------------------------------------------
-- tests
------------------------------------------------------------------------------
bingo_game :: Game
bingo_game = flip bingo (Reward 100) $ do
x <- [0..2]
pure $ do
y <- [0..2]
pure $ gate (Exactly $ x * 10 + y) win
foo :: Property
foo = property $ \g g2 -> race g g2 =~= race g2 g
------------------------------------------------------------------------------
-- observations
------------------------------------------------------------------------------
runGame :: [Event] -> Game -> (Set Reward, Maybe Result)
runGame evs g =
swap $ runWriter $ fmap _toResult $ _runGame g evs
_toResult :: Game -> Maybe Result
_toResult Win = Just Victory
_toResult Lose = Just Defeat
_toResult _ = Nothing
_runGame :: Game -> [Event] -> Writer (Set Reward) Game
_runGame g (e : es) = do
g' <- _stepGame g (Just e)
_runGame g' es
_runGame g [] = do
g' <- _stepGame g Nothing
case g == g' of -- ! 1
True -> pure g'
False -> _runGame g' []
_stepGame :: Game -> Maybe Event -> Writer (Set Reward) Game
_stepGame Win _ = pure win
_stepGame Lose _ = pure lose
-- # _stepGameRewardThen
_stepGame (RewardThen r g) e =
tell (S.singleton r) >> _stepGame g e
_stepGame (Subgame g g1 g2) e = -- ! 1
subgame <$> _stepGame g e -- ! 2
<*> pure g1
<*> pure g2
_stepGame (EitherW g1 g2) e =
eitherG <$> _stepGame g1 e
<*> _stepGame g2 e
_stepGame (Both g1 g2) e =
both <$> _stepGame g1 e
<*> _stepGame g2 e
_stepGame (Race g1 g2) e =
race <$> _stepGame g1 e
<*> _stepGame g2 e
_stepGame (Multigate cs) (Just e)
| Just (_, g) <- find (\(ef, _) -> matches ef e) cs
= pure g
_stepGame x@Multigate{} _ = pure x
matches :: EventFilter -> Event -> Bool
matches Never _ = False
matches Always _ = True
matches (Exactly e) (Event ev) = e == ev
------------------------------------------------------------------------------
-- specifications
------------------------------------------------------------------------------
sig_types :: Sig
sig_types = signature
[ monoType $ Proxy @Event
, monoType $ Proxy @EventFilter
, monoType $ Proxy @Reward
, monoType $ Proxy @Result
, monoTypeObserve $ Proxy @Game
, vars ["e"] $ Proxy @Event
, vars ["ef"] $ Proxy @EventFilter
, vars ["r"] $ Proxy @Reward
, vars ["res"] $ Proxy @Result
, vars ["g"] $ Proxy @Game
]
sig_options :: Sig
sig_options = signature
[ withMaxTermSize 5
]
quickspec_laws' :: [(String, Property)]
quickspec_laws' =
[ ( "comeback bottom = bottom"
, property $ comeback bottom =~= bottom)
, ( "win = comeback lose"
, property $ win =~= comeback lose)
, ( "lose = comeback win"
, property $ lose =~= comeback win)
, ( "both g g2 = both g2 g"
, property $
\ (g :: Game) (g2 :: Game) ->
both g g2 =~= both g2 g)
, ( "both g g = g"
, property $ \ (g :: Game) -> both g g =~= g)
, ( "eitherG g g2 = eitherG g2 g"
, property $
\ (g :: Game) (g2 :: Game) ->
eitherG g g2 =~= eitherG g2 g)
, ( "eitherG g g = g"
, property $ \ (g :: Game) -> eitherG g g =~= g)
, ( "race g g = g"
, property $ \ (g :: Game) -> race g g =~= g)
, ( "andThen g win = g"
, property $ \ (g :: Game) -> andThen g win =~= g)
, ( "andThen bottom g = bottom"
, property $
\ (g :: Game) -> andThen bottom g =~= bottom)
, ( "andThen lose g = lose"
, property $
\ (g :: Game) -> andThen lose g =~= lose)
, ( "andThen win g = g"
, property $ \ (g :: Game) -> andThen win g =~= g)
, ( "both g bottom = andThen g bottom"
, property $
\ (g :: Game) -> both g bottom =~= andThen g bottom)
, ( "both g win = g"
, property $ \ (g :: Game) -> both g win =~= g)
, ( "eitherG g lose = g"
, property $ \ (g :: Game) -> eitherG g lose =~= g)
, ( "race g bottom = g"
, property $ \ (g :: Game) -> race g bottom =~= g)
, ( "race bottom g = g"
, property $ \ (g :: Game) -> race bottom g =~= g)
, ( "race lose g = both g lose"
, property $
\ (g :: Game) -> race lose g =~= both g lose)
, ( "race win g = eitherG g win"
, property $
\ (g :: Game) -> race win g =~= eitherG g win)
, ( "gate ef bottom = bottom"
, property $
\ (ef :: EventFilter) -> gate ef bottom =~= bottom)
, ( "reward r = rewardThen r win"
, property $
\ (r :: Reward) -> reward r =~= rewardThen r win)
, ( "comeback (comeback g) = g"
, property $
\ (g :: Game) -> comeback (comeback g) =~= g)
, ( "comeback (reward r) = rewardThen r lose"
, property $
\ (r :: Reward) ->
comeback (reward r) =~= rewardThen r lose)
, ( "andThen g g2 = subgame g g2 lose"
, property $
\ (g :: Game) (g2 :: Game) ->
andThen g g2 =~= subgame g g2 lose)
, ( "subgame bottom g g2 = bottom"
, property $
\ (g :: Game) (g2 :: Game) ->
subgame bottom g g2 =~= bottom)
, ( "subgame lose g g2 = g2"
, property $
\ (g :: Game) (g2 :: Game) ->
subgame lose g g2 =~= g2)
, ( "subgame win g g2 = g"
, property $
\ (g :: Game) (g2 :: Game) ->
subgame win g g2 =~= g)
, ( "comeback g = subgame g lose win"
, property $
\ (g :: Game) -> comeback g =~= subgame g lose win)
, ( "subgame g win bottom = eitherG g bottom"
, property $
\ (g :: Game) ->
subgame g win bottom =~= eitherG g bottom)
, ( "andThen (comeback g) g2 = subgame g lose g2"
, property $
\ (g :: Game) (g2 :: Game) ->
andThen (comeback g) g2 =~= subgame g lose g2)
, ( "rewardThen r g = andThen (reward r) g"
, property $
\ (g :: Game) (r :: Reward) ->
rewardThen r g =~= andThen (reward r) g)
, ( "both g (comeback g) = andThen g lose"
, property $
\ (g :: Game) ->
both g (comeback g) =~= andThen g lose)
, ( "rewardThen r g = both g (reward r)"
, property $
\ (g :: Game) (r :: Reward) ->
rewardThen r g =~= both g (reward r))
, ( "eitherG g (comeback g) = subgame g win win"
, property $
\ (g :: Game) ->
eitherG g (comeback g) =~= subgame g win win)
, ( "race g (comeback g) = g"
, property $
\ (g :: Game) -> race g (comeback g) =~= g)
, ( "race (reward r) g = eitherG g (reward r)"
, property $
\ (g :: Game) (r :: Reward) ->
race (reward r) g =~= eitherG g (reward r))
, ( "gate ef (comeback g) = comeback (gate ef g)"
, property $
\ (ef :: EventFilter) (g :: Game) ->
gate ef (comeback g) =~= comeback (gate ef g))
, ( "rewardThen r (comeback g) = comeback (rewardThen r g)"
, property $
\ (g :: Game) (r :: Reward) ->
rewardThen r (comeback g) =~= comeback (rewardThen r g))
, ( "comeback (andThen g bottom) = subgame g bottom win"
, property $
\ (g :: Game) ->
comeback (andThen g bottom) =~= subgame g bottom win)
, ( "comeback (andThen g lose) = subgame g win win"
, property $
\ (g :: Game) ->
comeback (andThen g lose) =~= subgame g win win)
, ( "comeback (both g lose) = eitherG g win"
, property $
\ (g :: Game) ->
comeback (both g lose) =~= eitherG g win)
, ( "comeback (eitherG g bottom) = subgame g lose bottom"
, property $
\ (g :: Game) ->
comeback (eitherG g bottom) =~= subgame g lose bottom)
, ( "both lose (comeback g) = both g lose"
, property $
\ (g :: Game) ->
both lose (comeback g) =~= both g lose)
, ( "both lose (multigate xs) = lose"
, property $
\ (xs :: [(EventFilter, Game)]) ->
both lose (multigate xs) =~= lose)
, ( "race (comeback g) lose = comeback (race g win)"
, property $
\ (g :: Game) ->
race (comeback g) lose =~= comeback (race g win))
, ( "race (multigate xs) lose = lose"
, property $
\ (xs :: [(EventFilter, Game)]) ->
race (multigate xs) lose =~= lose)
, ( "race (multigate xs) win = win"
, property $
\ (xs :: [(EventFilter, Game)]) ->
race (multigate xs) win =~= win)
, ( "andThen (andThen g g2) g3 = andThen g (andThen g2 g3)"
, property $
\ (g :: Game) (g2 :: Game) (g3 :: Game) ->
andThen (andThen g g2) g3 =~= andThen g (andThen g2 g3))
, ( "both (both g g2) g3 = both g (both g2 g3)"
, property $
\ (g :: Game) (g2 :: Game) (g3 :: Game) ->
both (both g g2) g3 =~= both g (both g2 g3))
, ( "eitherG g (andThen g g) = g"
, property $
\ (g :: Game) -> eitherG g (andThen g g) =~= g)
, ( "eitherG g (both g g2) = both g (eitherG g g2)"
, property $
\ (g :: Game) (g2 :: Game) ->
eitherG g (both g g2) =~= both g (eitherG g g2))
, ( "eitherG (eitherG g g2) g3 = eitherG g (eitherG g2 g3)"
, property $
\ (g :: Game) (g2 :: Game) (g3 :: Game) ->
eitherG (eitherG g g2) g3 =~= eitherG g (eitherG g2 g3))
, ( "eitherG g (rewardThen r g2) = eitherG g2 (rewardThen r g)"
, property $
\ (g :: Game) (g2 :: Game) (r :: Reward) ->
eitherG g (rewardThen r g2) =~= eitherG g2 (rewardThen r g))
, ( "race g (andThen g g2) = eitherG g (andThen g g2)"
, property $
\ (g :: Game) (g2 :: Game) ->
race g (andThen g g2) =~= eitherG g (andThen g g2))
, ( "race g (both g g2) = both g (race g g2)"
, property $
\ (g :: Game) (g2 :: Game) ->
race g (both g g2) =~= both g (race g g2))
, ( "race g (eitherG g g2) = eitherG g (race g g2)"
, property $
\ (g :: Game) (g2 :: Game) ->
race g (eitherG g g2) =~= eitherG g (race g g2))
, ( "race g (race g g2) = race g g2"
, property $
\ (g :: Game) (g2 :: Game) ->
race g (race g g2) =~= race g g2)
, ( "race g (race g2 g) = race g g2"
, property $
\ (g :: Game) (g2 :: Game) ->
race g (race g2 g) =~= race g g2)
, ( "race g (rewardThen r g) = rewardThen r g"
, property $
\ (g :: Game) (r :: Reward) ->
race g (rewardThen r g) =~= rewardThen r g)
, ( "race (both g g2) g = both g (race g2 g)"
, property $
\ (g :: Game) (g2 :: Game) ->
race (both g g2) g =~= both g (race g2 g))
, ( "race (eitherG g g2) g = eitherG g (race g2 g)"
, property $
\ (g :: Game) (g2 :: Game) ->
race (eitherG g g2) g =~= eitherG g (race g2 g))
, ( "race (race g g2) g3 = race g (race g2 g3)"
, property $
\ (g :: Game) (g2 :: Game) (g3 :: Game) ->
race (race g g2) g3 =~= race g (race g2 g3))
, ( "race (rewardThen r g) g2 = race g (rewardThen r g2)"
, property $
\ (g :: Game) (g2 :: Game) (r :: Reward) ->
race (rewardThen r g) g2 =~= race g (rewardThen r g2))
, ( "gate ef (andThen g g2) = andThen (gate ef g) g2"
, property $
\ (ef :: EventFilter) (g :: Game) (g2 :: Game) ->
gate ef (andThen g g2) =~= andThen (gate ef g) g2)
, ( "subgame (comeback g) g2 g3 = subgame g g3 g2"
, property $
\ (g :: Game) (g2 :: Game) (g3 :: Game) ->
subgame (comeback g) g2 g3 =~= subgame g g3 g2)
, ( "subgame (reward r) g g2 = rewardThen r g"
, property $
\ (g :: Game) (g2 :: Game) (r :: Reward) ->
subgame (reward r) g g2 =~= rewardThen r g)
, ( "comeback (subgame g g2 win) = andThen g (comeback g2)"
, property $
\ (g :: Game) (g2 :: Game) ->
comeback (subgame g g2 win) =~= andThen g (comeback g2))
, ( "andThen g (both g lose) = andThen g lose"
, property $
\ (g :: Game) ->
andThen g (both g lose) =~= andThen g lose)
, ( "andThen g (eitherG g2 win) = eitherG g (andThen g g2)"
, property $
\ (g :: Game) (g2 :: Game) ->
andThen g (eitherG g2 win) =~= eitherG g (andThen g g2))
, ( "andThen g (race g2 win) = race (andThen g g2) g"
, property $
\ (g :: Game) (g2 :: Game) ->
andThen g (race g2 win) =~= race (andThen g g2) g)
, ( "andThen (eitherG g bottom) g2 = subgame g g2 bottom"
, property $
\ (g :: Game) (g2 :: Game) ->
andThen (eitherG g bottom) g2 =~= subgame g g2 bottom)
, ( "andThen (eitherG g win) g = g"
, property $
\ (g :: Game) -> andThen (eitherG g win) g =~= g)
, ( "andThen (race g g2) lose = andThen (race g2 g) lose"
, property $
\ (g :: Game) (g2 :: Game) ->
andThen (race g g2) lose =~= andThen (race g2 g) lose)
, ( "andThen (race g lose) g = race g lose"
, property $
\ (g :: Game) ->
andThen (race g lose) g =~= race g lose)
, ( "andThen (race g win) g = g"
, property $
\ (g :: Game) -> andThen (race g win) g =~= g)
, ( "both g (eitherG g2 win) = andThen (eitherG g2 win) g"
, property $
\ (g :: Game) (g2 :: Game) ->
both g (eitherG g2 win) =~= andThen (eitherG g2 win) g)
, ( "both lose (eitherG g g2) = both g (both g2 lose)"
, property $
\ (g :: Game) (g2 :: Game) ->
both lose (eitherG g g2) =~= both g (both g2 lose))
, ( "both lose (race g g2) = both g (both g2 lose)"
, property $
\ (g :: Game) (g2 :: Game) ->
both lose (race g g2) =~= both g (both g2 lose))
, ( "both lose (gate ef g) = lose"
, property $
\ (ef :: EventFilter) (g :: Game) ->
both lose (gate ef g) =~= lose)
, ( "both (comeback g) (comeback g2) = comeback (eitherG g g2)"
, property $
\ (g :: Game) (g2 :: Game) ->
both (comeback g) (comeback g2) =~= comeback (eitherG g g2))
, ( "eitherG g (both g2 lose) = andThen (eitherG g2 win) g"
, property $
\ (g :: Game) (g2 :: Game) ->
eitherG g (both g2 lose) =~= andThen (eitherG g2 win) g)
, ( "race g (andThen g2 bottom) = both g (race g g2)"
, property $
\ (g :: Game) (g2 :: Game) ->
race g (andThen g2 bottom) =~= both g (race g g2))
, ( "race g (eitherG g2 bottom) = eitherG g (race g g2)"
, property $
\ (g :: Game) (g2 :: Game) ->
race g (eitherG g2 bottom) =~= eitherG g (race g g2))
, ( "race (comeback g) (comeback g2) = comeback (race g g2)"
, property $
\ (g :: Game) (g2 :: Game) ->
race (comeback g) (comeback g2) =~= comeback (race g g2))
, ( "race (andThen g g) lose = race g lose"
, property $
\ (g :: Game) ->
race (andThen g g) lose =~= race g lose)
, ( "race (andThen g g) win = race g win"
, property $
\ (g :: Game) ->
race (andThen g g) win =~= race g win)
, ( "race (andThen g bottom) g2 = both g2 (race g g2)"
, property $
\ (g :: Game) (g2 :: Game) ->
race (andThen g bottom) g2 =~= both g2 (race g g2))
, ( "race (eitherG g bottom) g2 = eitherG g2 (race g g2)"
, property $
\ (g :: Game) (g2 :: Game) ->
race (eitherG g bottom) g2 =~= eitherG g2 (race g g2))
, ( "race (gate ef g) lose = lose"
, property $
\ (ef :: EventFilter) (g :: Game) ->
race (gate ef g) lose =~= lose)
, ( "race (gate ef g) win = win"
, property $
\ (ef :: EventFilter) (g :: Game) ->
race (gate ef g) win =~= win)
, ( "gate ef (eitherG g bottom) = eitherG bottom (gate ef g)"
, property $
\ (ef :: EventFilter) (g :: Game) ->
gate ef (eitherG g bottom) =~= eitherG bottom (gate ef g))
, ( "subgame g bottom (comeback g2) = comeback (subgame g bottom g2)"
, property $
\ (g :: Game) (g2 :: Game) ->
subgame g bottom (comeback g2) =~= comeback (subgame g bottom g2))
, ( "eitherG bottom (andThen g lose) = subgame g bottom bottom"
, property $
\ (g :: Game) ->
eitherG bottom (andThen g lose) =~= subgame g bottom bottom)
]