{-# 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