{-# options_ghc -XEmptyDataDecls -XOverlappingInstances -XScopedTypeVariables -XGADTs #-}
module PBasicGames where
import Data.Maybe
import Iso
import PGames
import List
type Nat = Int
-- Game for ()
-- /boolGame/
unitGame :: Game ()
unitGame = Single (Iso (\() -> ()) (\() -> ()))
boolIso :: ISO Bool (Either () ())
boolIso =
Iso (\b -> if b then Left() else Right())
(\x -> case x of Left() -> True; Right() -> False)
boolGame :: Game Bool
boolGame = split boolIso unitGame unitGame
-- /End/
-- /constGame/
constGame :: t -> Game t
constGame k = Single (Iso (const ()) (const k))
-- /End/
-- Games for natural numbers
parityIso :: ISO Int (Either Int Int)
parityIso = Iso
(\n -> if even n then Left (n `div` 2) else Right (n `div` 2))
(\x -> case x of Left m -> m*2; Right m -> m*2+1)
-- /geNatGame/
-- geNatGame k returns a game for { n:Nat | n >= k }
geNatGame :: Nat -> Game Nat
geNatGame k = split iso (constGame k) (geNatGame (k+1))
where iso :: ISO Nat (Either Nat Nat)
iso = Iso ask bld
-- Precondition of ask x: x >= k
ask x = if x == k then Left x else Right x
bld (Left x) = x
bld (Right x) = x
-- /End/
-- /unaryNatGame/
succIso :: ISO Nat (Either () Nat)
succIso = Iso ask bld
where ask 0 = Left ()
ask (n+1) = Right n
bld (Left ()) = 0
bld (Right n) = n+1
unaryNatGame :: Game Nat
unaryNatGame = split succIso unitGame unaryNatGame
-- /End/
-- /encUnaryNat/
encUnaryNat x = case x of 0 -> 1 : []
n+1 -> 0 : encUnaryNat n
-- /End/
-- /binNatGame/
binNatGame :: Game Nat
binNatGame = split succIso unitGame divG
where divG = split (Iso ask bld) binNatGame binNatGame
ask n | even n = Left (n `div` 2)
| otherwise = Right (n `div` 2)
bld (Left m) = 2*m
bld (Right m) = 2*m+1
-- /End/
-- /natGameFunny/
natGameFunny :: Game Nat
natGameFunny = split (Iso ask bld) (constGame 0) gfunny
where ask n = if n == 0 then Left n else Right n -- Are you 0 or not?
bld (Left n) = n
bld (Right n) = n
gfunny = split evi binNatGame (split pred_evi binNatGame voidNatGame)
evi = Iso (\n -> if even n then Left (n `div` 2) else Right n) -- Are you even or not?
(either (\n->2*n) id)
pred_evi = Iso (\(n+1) -> if even n then Left (n `div` 2) else Right (n+1)) -- Is your predecessor odd or not?
(either (\n->2*n+1) id)
voidNatGame :: Game Nat
-- In reality: Game { x: Nat | x > 0 /\ x odd /\ x-1 odd }
voidNatGame = split voidi voidNatGame voidNatGame
-- Empty set is disjoint with any set so voidi *is* an isomorphism
voidi = Iso (\x -> Right x) bld
-- /End/
binNatGameFunny :: Game Nat
binNatGameFunny = split (Iso ask bld) zOneG divG
where zOneG = split (Iso askz bldz) (constGame 0)
(constGame 1)
askz 0 = Left 0
askz 1 = Right 1
bldz (Right 1) = 1
bldz (Left 0) = 0
-- the rest as in binNatGame
-- /End/
ask 0 = Left 0
ask (n+1) = Right n
bld (Left 0) = 0
bld (Right n) = n+1
divG = split iso binNatGame binNatGame
iso = Iso ask' bld'
ask' n = if even n then Left (n `div` 2)
else Right (n `div` 2)
bld' (Left m) = 2*m
bld' (Right m) = 2*m+1
-- Flip the meaning of the bits
{-
flipGame :: Game a -> Game a
flipGame (Split iso f1 g1 f0 g0) = Split (iso `seqI` swapSumI) f0 (flipGame g0) f1 (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/
data ProdGamesResult s t where
PGR :: ISO (s,t) s' -> GamesOver s' -> ProdGamesResult s t
prodGame :: forall t s. Game t -> Game s -> Game (t,s)
prodGame (Single iso) g = g +> iso'
where iso' :: ISO (t,s) s -- assuming ISO t ()
iso' = prodI iso idI `seqI` prodLUnitI
prodGame (Split (Iso i j) gs) g =
case prodGames gs of
PGR (Iso i' j') gs' ->
Split (Iso (\(x,y) -> i' (i x, y)) (\z -> let (x,y) = j' z in (j x,y))) gs'
where
prodGames :: forall sum. GamesOver sum -> ProdGamesResult sum s
prodGames gs =
case gs of
NilGames -> PGR (Iso (\_ -> error "should not happen") (\_ -> error "should not happen")) NilGames
ConsGames w ga gsa ->
case prodGames gsa of
PGR (Iso i j) gs'' -> PGR (Iso (\(x,y) -> case x of Left xl -> Left (xl,y); Right xr -> Right (i (xr,y)))
(\x -> case x of Left (y,z) -> (Left y,z); Right z -> let (z1,z2) = j z in (Right z1,z2))) (ConsGames w (prodGame ga g) gs'')
-- /End/
-- A game for products, based on interleaving
-- /ilGame/
{-
ilGame :: forall t s. Game t -> Game s -> Game (t,s)
ilGame (Single iso) g2 = g2 +> iso'
where iso' :: ISO (t,s) s -- assuming ISO t ()
iso' = prodI iso idI `seqI` prodLUnitI
ilGame (Split (iso :: ISO t (Either ta tb)) f1a g1a f1b g1b) g2
= Split iso' f1a (ilGame g2 g1a) f1b (ilGame g2 g1b)
where iso' :: ISO (t,s) (Either (s,ta) (s,tb))
iso' = swapProdI `seqI` prodI idI iso
`seqI` prodRSumI
-}
-- /End/
-- /depGame/
depGame :: forall t s. Game t -> (t -> Game s) -> Game (t,s)
depGame (Single iso) f = f (from iso ()) +> iso'
where iso' = prodI iso idI `seqI` prodLUnitI
depGame (Split (Iso i j) gs) f =
case depGames gs (f . j) of
PGR (Iso i' j') gs' -> Split (Iso (\(x,y) -> i' (i x, y)) (\z -> let (x,y) = j' z in (j x,y))) gs'
where
depGames :: forall sum. GamesOver sum -> (sum -> Game s) -> ProdGamesResult sum s
depGames gs f =
case gs of
NilGames -> PGR (Iso (\_ -> error "should not happen") (\_ -> error "should not happen")) NilGames
ConsGames w ga gsa ->
case depGames gsa (f . Right) of
PGR (Iso i'' j'') gs'' ->
PGR (Iso (\(x,y) -> case x of Left xl -> Left (xl,y); Right xr -> Right (i'' (xr,y)))
(\x -> case x of Left (y,z) -> (Left y,z); Right z -> let (z1,z2) = j'' z in (Right z1,z2)))
(ConsGames w (depGame ga (f . Left)) gs'')
-- /End/
getRight (Right x) = x
getLeft (Left x) = x
nonemptyIso = Iso (\(x:xs) -> (x,xs)) (\(x,xs) -> x:xs)
-- /vecGame/
vecGame :: Game t -> Nat -> Game [t]
-- /End/
vecGame g 0 = constGame []
vecGame g (n+1) = prodGame g (vecGame g n) +> nonemptyIso
-- /lengthListGame/
lengthListGame :: Game t -> Game (Nat,[t])
lengthListGame g = depGame binNatGame (vecGame g)
listGame' :: forall t. Game t -> Game [t]
listGame' g = lengthListGame g +> Iso h j
where h :: [t] -> (Nat,[t])
h lst = (length lst, lst)
j :: (Nat,[t]) -> [t]
-- Precondition: n = length lst
j (n,lst) = lst
-- /End/
-- A game for lists, using sum-of-products
-- /listGame/
listIso :: ISO [t] (Either () (t,[t]))
listIso = Iso ask bld
where ask [] = Left ()
ask (x:xs) = Right (x,xs)
bld (Left ()) = []
bld (Right (x,xs)) = x:xs
listGame :: Game t -> Game [t]
listGame g =
split listIso unitGame (prodGame g (listGame g))
-- Parameterized on how much more likely a Cons is than a Nil
biasedListGame :: Int -> Game t -> Game [t]
biasedListGame n g =
split2 listIso 1 unitGame n (prodGame g (biasedListGame n g))
-- /End/
-- /rangeGame/
-- Precondition for rangeGame k1 k2: k1 <= k2
rangeGame :: Nat -> Nat -> Game Nat
rangeGame k1 k2 | k1 == k2 = constGame k1
rangeGame k1 k2 = split (Iso ask bld) g1 g2
where g1 = rangeGame (m+1) k2
g2 = rangeGame k1 m
ask x = if x > m then Left x else Right x
bld (Left x) = x
bld (Right x) = x
m = (k1 + k2) `div` 2
-- /End/
data Tree = Leaf | Node Tree Tree deriving Show
tiso = Iso ask bld
where ask (Leaf) = Left ()
ask (Node t1 t2) = Right (t1,t2)
bld (Left ()) = Leaf
bld (Right (t1,t2)) = Node t1 t2
treeGame1 = split tiso (Single idI) (prodGame treeGame1 treeGame1)
{-treeGame2 = split tiso (Single idI) (ilGame treeGame2 treeGame2)-}
ones :: [Bit]
ones = 1:ones
biasedBool = split2 boolIso 3 unitGame 1 unitGame
biasedBoolTriple = prodGame biasedBool (prodGame biasedBool biasedBool)
data Three = A | B | C
threeGame = split3 (flat3 (Iso (\x -> case x of A -> Left (); B -> Right (Left ()); C -> Right (Right ()))
(\x -> case x of Left () -> A; Right (Left ()) -> B; Right (Right ()) -> C)))
1 unitGame 1 unitGame 1 unitGame