module BasicGames where
import Data.Maybe
import Iso
import Games
import List
unitGame :: Game ()
unitGame = Single (Iso id id)
boolGame :: Game Bool
boolGame = Split boolIso unitGame unitGame
constGame :: t -> Game t
constGame k = Single (singleIso k)
geNatGame :: Nat -> Game Nat
geNatGame k = Split (splitIso ((==) k))
(Single (singleIso k))
(geNatGame (k+1))
unaryNatGame :: Game Nat
unaryNatGame = Split succIso unitGame unaryNatGame
encUnaryNat x = case x of 0 -> I : []
n+1 -> O : encUnaryNat n
rangeGame :: Nat -> Nat -> Game Nat
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
binNatGame :: Game Nat
binNatGame = Split succIso unitGame
(Split parityIso binNatGame binNatGame)
flipGame :: Game a -> Game a
flipGame (Split iso g1 g2) = Split (iso `seqI` swapSumI) (flipGame g2) (flipGame g1)
flipGame g = g
sumGame :: Game t -> Game s -> Game (Either t s)
sumGame = Split idI
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)
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)
depGame :: Game t -> (t -> Game s) -> Game (t,s)
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))
listGame :: Game t -> Game [t]
listGame g =
Split listIso unitGame (prodGame g (listGame g))
nonemptyIso = Iso (\(x:xs) -> (x,xs)) (\(x,xs) -> x:xs)
vecGame :: Game t -> Nat -> Game [t]
vecGame g 0 = constGame []
vecGame g (n+1) = prodGame g (vecGame g n) +> nonemptyIso
listGame' :: Game t -> Game [t]
listGame' g = depGame binNatGame (vecGame g)
+> depListIso