{-# OPTIONS -fglasgow-exts -fallow-overlapping-instances #-}
module StateMonad.ImplementationStandardApprox where

import ChasingBottoms
import Debug.QuickCheck
import Control.Monad
import Data.Generics
import StateMonad.Basics
import Control.Arrow
import Data.List

newtype State s a = S (s -> Pair a s)
                 deriving (Data, Typeable)

get :: State s s
get = S $ \s -> Pair s s

put :: s -> State s One
put s = S $ const (Pair One s)

runState :: State s a -> s -> a
runState (S m) = fst . m
  where fst (Pair a _) = a

run :: State s a -> s -> (a, s)
run (S m) s = (a, s')
  where Pair a s' = m s

instance Monad (State s) where
    return x = S $ \s -> Pair x s
    S m >>= f = S $ \s ->
                  let Pair x s' = m s
                      S m' = f x
                  in m' s'

-- We need to restrict ourselves to Bit here to avoid trouble with
-- overlapping instances. And without the overlapping instances we
-- don't get any non-strict functions generated inside S.

instance (Arbitrary a, Data a) => Arbitrary (State Bit a) where
  arbitrary = frequency [ (20, liftM S arbitrary), (1, return bottom) ]
  coarbitrary x | isBottom x = variant 0
                | otherwise  =
    case x of
      S f -> variant 1 . coarbitrary f

instance Data a => Show (State Bit a) where
  showsPrec p s | isBottom s = showString "_|_"
  showsPrec p (S f) = showParen (p > 10) $
    showString "S " . if isBottom f then showString "_|_" else
      showString "<" .
        (foldr (.) id .
         intersperse (showString ", ") .
         map (\(x, y) -> showString "(" . x . showString ", " .
                         y . showString ")") .
         map (approxShowsPrec 8 0 &&& approxShowsPrec 8 0 . f) $
         [bottom, O, I]
        ) .
      showString ">"

(=^=) :: Data a => State Bit a -> State Bit a -> Bool
m   =^= m'  | Just eq <- m =-=-> m' = eq
S f =^= S g | Just eq <- f =-= g = eq
            | otherwise = all (\x -> f x ==! g x) [bottom, O, I]

(<^=) :: Data a => State Bit a -> State Bit a -> Bool
m   <^= m'  | Just leq <- m <-=-> m' = leq
S f <^= S g | Just leq <- f <-= g = leq
            | otherwise = all (\x -> f x <=! g x) [bottom, O, I]

(=-=->) :: (Monad m, Data a) => State Bit a -> State Bit a -> m Bool
x =-=-> y = case (isBottom' x, isBottom' y) of
  (False, False) -> fail "No bottoms"
  (True, True)   -> return True
  _              -> return False

(<-=->) :: (Monad m, Data a) => State Bit a -> State Bit a -> m Bool
x <-=-> y = case (isBottom' x, isBottom' y) of
  (False, False) -> fail "No bottoms"
  (True, False)  -> return True
  _              -> return False

isBottom' :: Data a => State Bit a -> Bool
isBottom' (S m) = isBottom m || all (isBottom . m) [bottom, O, I]

-- Failing tests:

-- M_Id2:
-- _|_ >>= return  /===  _|_

-- _|_ >>= return = S $ \s -> Pair _|_ _|_