{-# options_ghc -XEmptyDataDecls -XOverlappingInstances -XScopedTypeVariables #-}
module NatGames where 

import Data.Maybe
import Iso
import Games
import BasicGames

-- positive integers
type Pos = Int

-- /Elias/
power2 0 = 1
power2 (n+1) = 2 * power2 n

log2 1 = 0
log2 n = 1 + log2 (n `div` 2)

-- binaryIso :: ISO Pos (n:Nat, [0,2^n-1])
binaryIso :: ISO Pos (Nat,Pos)
binaryIso = Iso (\p -> (log2 p, p)) snd

-- Parameterized on a game for encoding the number of bits
eliasGame :: Game Nat -> Game Pos
eliasGame natGame = depGame natGame (\n -> let m = power2 n in rangeGame m (2*m - 1)) +> binaryIso

-- The Elias gamma game for positive integers: 
-- First encode the number of bits - 1 in unary, then the binary rep of the number, without the leading one
gammaGame = eliasGame unaryNatGame

isOneIso :: ISO Pos (Either () Pos)
isOneIso = Iso ask bld
  where ask 1 = Left ()
        ask n = Right n
        bld (Left ()) = 1
        bld (Right n) = n

-- The Elias omega game: 
-- Recursively apply the game to the number of bits
omegaGame = Split isOneIso unitGame (eliasGame omegaGame)
-- /End/

primes = sieve [2..]
   where
    sieve (p:xs) = p : sieve [x | x<-xs, x `mod` p /= 0]  


factIso :: [Int] -> ISO Int (Either Int Int)
factIso (p:ps) = 
  Iso (\n -> let (d,r) = divMod n p in if r==0 then Left d else Right n) 
      (\z -> case z of Left d -> d*p; Right n -> n)

factPosGame ps = Split isOneIso unitGame (factPosNotOneGame ps)
factPosNotOneGame (p:ps) = Split (factIso (p:ps)) (factPosGame (p:ps)) (factPosNotOneGame ps)

factGame :: Game Pos
factGame = factPosGame primes