{-# OPTIONS_GHC -fglasgow-exts #-} 
module FilterGames where 

import Iso
import Games 
import BasicGames 

import Data.Maybe 

-- /voidGame/
voidGame :: Game t -- Precondition: t is uninhabited 
voidGame = Split (Iso ask bld) voidGame voidGame
  where ask = Right 
        bld (Left x)  = x 
        bld (Right x) = x 
-- /End/ 


-- /filterGame/
filterGame :: (t -> Bool) -> Game t -> Game t 
-- forall (p : t -> Bool), Game t -> Game { x | p x } 
filterGame p g@(Single (Iso _ bld)) =
 if p (bld ()) then g else voidGame
filterGame p (Split (Iso ask bld) g1 g2)
 = Split (Iso ask bld) (filterGame (p . bld . Left)  g1)
                       (filterGame (p . bld . Right) g2)
-- /End/ 

-- /filterGameOpt/
-- (f : t -> Bool) -> Game t -> Maybe (Game {x:t | f t})
filterGameOpt :: (t -> Bool) -> Game t -> Maybe (Game t)
filterGameOpt f (Single iso)
  | f (from iso ()) = Just $ Single iso 
  | otherwise       = Nothing 
filterGameOpt f (Split (Iso ask bld) g1 g2) 
  = case filterGameOpt (f . bld . Left) g1 of 
      Nothing -> 
        case filterGameOpt (f . bld . Right) g2 of 
          Nothing  -> Nothing 
          Just g2' -> Just (g2' +> iso2)
      Just g1' -> 
        case filterGameOpt (f . bld . Right) g2 of 
          Nothing -> Just (g1' +> iso1) 
          Just g2' -> Just $ Split (Iso ask bld) g1' g2'
  where iso1 = Iso (\x -> case ask x of Left x1 -> x1) 
                   (bld . Left) 
        iso2 = Iso (\x -> case ask x of Right x2 -> x2)
                   (bld . Right) 
-- /End/

-- /filterFinGame/
filterFinGame :: (t -> Bool) -> Game t -> Maybe (Game t)
-- forall (p : t -> Bool), Game t -> option (Game { x | p x })
filterFinGame p g@(Single (Iso _ bld)) =
  if p (bld ()) then Just g else Nothing
filterFinGame p (Split iso@(Iso ask bld) g1 g2) 
  = case (filterFinGame (p . bld . Left) g1, 
            filterFinGame (p . bld . Right) g2) of 
      (Nothing, Nothing)   -> Nothing
      (Just g1', Nothing)  -> Just $ g1' +> iso1
      (Nothing, Just g2')  -> Just $ g2' +> iso2
      (Just g1', Just g2') -> Just $ Split iso g1' g2'
  where fromLeft  (Left x)  = x
        fromRight (Right x) = x
        iso1 = Iso (fromLeft  . ask) (bld . Left ) 
        iso2 = Iso (fromRight . ask) (bld . Right)
-- /End/

{- Games for infinitely inhabited (after filtering) data types -} 

pre_filterGame_inf :: Eq t => Game t -> (t -> Bool) -> Game t 
pre_filterGame_inf stack f
  = case unfoldUntil stack of 
      (x,rest) | f x ->  
                   let iso = Iso ask (either id id)
                       ask z = if x == z then Left z else Right z 
                       sing_iso = Iso (\_ -> ()) (\_ -> x)
                   in Split iso (Single sing_iso) (pre_filterGame_inf rest f)
               | otherwise -> pre_filterGame_inf rest f

filterInfGame :: forall t. Eq t => (t -> Bool) ->  Game t -> Game t 
filterInfGame f g = pre_filterGame_inf (mkStack g) f 
  where mkStack g = Split (iso :: ISO t (Either t t)) g (Single undefined) -- terminator node
        iso = Iso Left (either id id) 

-- -- unfoldUntil (stack :: Game t) returns an element z and 
-- -- Game {x : t | x <> z }
-- -- We *know* it will terminate because there are infinitely many 
-- -- elements inhabiting the datatype
unfoldUntil :: Game t -> (t, Game t) 
unfoldUntil stack = case find stack of 
                      Left (x,rest) -> (x,rest) 
                      Right unfolded -> unfoldUntil unfolded 

-- One step unfolding of a list-like game         
unfoldOne :: forall t. Game t -> Game t 
unfoldOne (Single undef) = Single undef    -- Terminator
unfoldOne (Split iso (Single siso) rest)
  = Split iso (Single siso) (unfoldOne rest)
unfoldOne (Split iso (Split iso' g1 g2) rest) 
  = shufflePartition (Split iso (Split iso' g1 g2) (unfoldOne rest))

find :: forall t. Game t -> Either (t,Game t) (Game t) 
find (Single undef) = Right (Single undef) -- Terminator: not found
find (Split (iso :: ISO t (Either t1 t2)) (Single siso) rest) 
  = let x = from iso $ Left (from siso ())
        unfolded = unfoldOne rest +> ciso
        ciso :: ISO t t2 
        ciso = Iso (\x -> case to iso x of Right x2 -> x2) (from iso . Right) 
  in Left (x,unfolded)
find (Split siso (Split siso' g1 g2) rest)
  = case find rest of 
      Left (x, unfolded) -> Left (from siso (Right x), shufflePartition (Split siso (Split siso' g1 g2) unfolded))
      Right unfolded     -> Right (shufflePartition (Split siso (Split siso' g1 g2) unfolded))

shufflePartition :: forall t. Game t -> Game t 
shufflePartition (Split (siso :: ISO t (Either t1 trest)) 
                        (Split (siso' :: ISO t1 (Either t11 t12)) g1 g2) rest)
  = Split siso1 g1 (Split siso2 g2 rest)    
  where siso2 = idI 
        siso1 = Iso ask bld 
        
        ask :: t -> Either t11 (Either t12 trest)
        ask x = case to siso x of 
                  Left x1 -> case to siso' x1 of 
                               Left x11  -> Left x11 
                               Right x12 -> Right (Left x12) 
                  Right xrest -> Right (Right xrest)

        bld (Left x11) = from siso $ Left (from siso' (Left x11)) 
        bld (Right (Left x12))    = from siso $ Left (from siso' (Right x12)) 
        bld (Right (Right xrest)) = from siso $ Right xrest 

mkOddNatGame = filterInfGame odd unaryNatGame 
test_odd0 bitstream = dec mkOddNatGame bitstream
test_odd1 num = enc mkOddNatGame num