```{-# options_ghc -XEmptyDataDecls #-}
module BasicGames where

import Data.Maybe
import Iso
import Games
import List

-- /unitGame/
unitGame :: Game ()
unitGame = Single (Iso id id)
-- /End/

-- /boolGame/
boolGame :: Game Bool
boolGame = Split boolIso unitGame unitGame
-- /End/

-- /constGame/
constGame :: t -> Game t
-- forall (k:t), Game { x | x=k }
constGame k = Single (singleIso k)
-- /End/

-- /geNatGame/
geNatGame :: Nat -> Game Nat
-- forall k:nat, Game { x | x >= k }
geNatGame k = Split (splitIso ((==) k))
(Single (singleIso k))
(geNatGame (k+1))
-- /End/

-- /unaryNatGame/
unaryNatGame :: Game Nat
unaryNatGame = Split succIso unitGame unaryNatGame
-- /End/

-- /encUnaryNat/
encUnaryNat x = case x of 0 -> I : []
n+1 -> O : encUnaryNat n
-- /End/

-- /rangeGame/
rangeGame :: Nat -> Nat -> Game Nat
-- forall m n : nat, Game { x | m <= x && x <= n }
rangeGame m n | m == n = Single (singleIso m)
rangeGame m n = Split (splitIso (\x -> x > mid))
(rangeGame (mid+1) n)
(rangeGame m mid)
where mid = (m + n) `div` 2
-- /End/

-- /binNatGame/
binNatGame :: Game Nat
binNatGame = Split succIso unitGame
(Split parityIso binNatGame binNatGame)
-- /End/

-- Flip the meaning of the bits
flipGame :: Game a -> Game a
flipGame (Split iso g1 g2) = Split (iso `seqI` swapSumI) (flipGame g2) (flipGame g1)
flipGame g = g

-- A game for sums
-- /sumGame/
sumGame :: Game t -> Game s -> Game (Either t s)
sumGame = Split idI
-- /End/

-- A game for products, based on appending
-- /prodGame/
prodGame :: Game t -> Game s -> Game (t,s)
prodGame (Single iso) g2 =
g2 +> prodI iso idI `seqI` prodLUnitI
prodGame (Split iso g1a g1b) g2 =
Split (prodI iso idI `seqI` prodLSumI)
(prodGame g1a g2)
(prodGame g1b g2)
-- /End/

-- A game for products, based on interleaving
-- /ilGame/
ilGame :: Game t -> Game s -> Game (t,s)
ilGame (Single iso) g2 =
g2 +> prodI iso idI `seqI` prodLUnitI
ilGame (Split iso g1a g1b) g2 =
Split (swapProdI `seqI` prodI idI iso `seqI` prodRSumI)
(ilGame g2 g1a)
(ilGame g2 g1b)
-- /End/

-- Dependent composition
-- /depGame/
depGame :: Game t -> (t -> Game s) -> Game (t,s)
-- Game t -> (forall x:t, Game(s x)) -> Game {x:t & s x}
depGame (Single iso) f =
f (from iso ()) +> prodI iso idI `seqI` prodLUnitI
depGame (Split iso g1a g1b) f
= Split (prodI iso idI `seqI` prodLSumI)
(depGame g1a (f . from iso . Left))
(depGame g1b (f . from iso . Right))
-- /End/

-- A game for lists, using sum-of-products
-- /listGame/
listGame :: Game t -> Game [t]
listGame g =
Split listIso unitGame (prodGame g (listGame g))
-- /End/

nonemptyIso = Iso (\(x:xs) -> (x,xs)) (\(x,xs) -> x:xs)

-- /vecGame/
vecGame :: Game t -> Nat -> Game [t]
-- Game t -> forall n:nat, Game t^n
-- /End/
vecGame g 0 = constGame []
vecGame g (n+1) = prodGame g (vecGame g n) +> nonemptyIso

-- /listGameAux/
listGame' :: Game t -> Game [t]
listGame' g = depGame binNatGame (vecGame g)
+> depListIso
-- /End/
```