content: {-# LANGUAGE DeriveDataTypeable    #-}
  {-# LANGUAGE DeriveGeneric         #-}
  {-# LANGUAGE FlexibleInstances     #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  
  module Workflow.WIP2 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
    ]
  
  
  main :: IO ()
  main = traverse_ (quickCheckWith stdArgs {maxSuccess=100000} . uncurry counterexample) quickspec_laws'
  
  
  
  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)
    ]
  
  