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

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

```