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