{-# LANGUAGE OverlappingInstances, FlexibleInstances,FlexibleContexts #-}
-- Does not yet check put/get properties!
module MonadState where

import Hip.Prelude
import Prelude (Int,Eq)

-- Poor man's equality
instance Eq b => Eq (Int -> b)


type State s a = s -> (a,s)

uncurry f (a,b) = f a b
uncurry' f t = f (fst t) (snd t)

fst (a,b) = a
snd (a,b) = b

bind_strict :: State s a -> (a -> State s b) -> State s b
(m `bind_strict` f) s = uncurry f (m s)

bind_lazy :: State s a -> (a -> State s b) -> State s b
(m `bind_lazy` f) s = uncurry' f (m s)

bind_let :: State s a -> (a -> State s b) -> State s b
(m `bind_let` f) s = let a  = fst (m s)
                         s' = snd (m s)
                     in  f a s'

bind_strict_lambda :: State s a -> (a -> State s b) -> State s b
m `bind_strict_lambda` f = \s -> uncurry f (m s)

bind_lazy_lambda :: State s a -> (a -> State s b) -> State s b
m `bind_lazy_lambda` f = \s -> uncurry' f (m s)

bind_let_lambda :: State s a -> (a -> State s b) -> State s b
m `bind_let_lambda` f = \s -> let a  = fst (m s)
                                  s' = snd (m s)
                              in  f a s'

return :: a -> State s a
return x s = (x,s)


returnl :: a -> State s a
returnl x = \s -> (x,s)

-- Bind without lambda --------------------------------------------------------

prop_return_left_strict :: (s -> (a,s)) -> Prop (s -> (a,s))
prop_return_left_strict f = (f `bind_strict` return) =:= f

prop_return_left_lazy :: (s -> (a,s)) -> Prop (s -> (a,s))
prop_return_left_lazy f = (f `bind_lazy` return) =:= f

prop_return_left_let :: (s -> (a,s)) -> Prop (s -> (a,s))
prop_return_left_let f = (f `bind_let` return) =:= f

prop_return_right_lazy :: (a -> s -> (a,s)) -> a -> Prop (s -> (a,s))
prop_return_right_lazy f a = (return a `bind_lazy` f) =:= f a

prop_return_right_strict :: (a -> s -> (a,s)) -> a -> Prop (s -> (a,s))
prop_return_right_strict f a = (return a `bind_strict` f) =:= f a

prop_return_right_let :: (a -> s -> (a,s)) -> a -> Prop (s -> (a,s))
prop_return_right_let f a = (return a `bind_let` f) =:= f a

prop_assoc_strict :: (s -> (a,s)) -> (a -> s -> (b,s)) -> (b -> s -> (c,s)) -> Prop (s -> (c,s))
prop_assoc_strict m f g = ((m `bind_strict` f) `bind_strict` g) =:= (m `bind_strict` (\x -> f x `bind_strict` g))

prop_assoc_lazy :: (s -> (a,s)) -> (a -> s -> (b,s)) -> (b -> s -> (c,s)) -> Prop (s -> (c,s))
prop_assoc_lazy m f g = ((m `bind_lazy` f) `bind_lazy` g) =:= (m `bind_lazy` (\x -> f x `bind_lazy` g))

prop_assoc_let :: (s -> (a,s)) -> (a -> s -> (b,s)) -> (b -> s -> (c,s)) -> Prop (s -> (c,s))
prop_assoc_let m f g = ((m `bind_let` f) `bind_let` g) =:= (m `bind_let` (\x -> f x `bind_let` g))

-- Lambda definition ----------------------------------------------------------

prop_return_left_strict_lambda :: (s -> (a,s)) -> Prop (s -> (a,s))
prop_return_left_strict_lambda f = (f `bind_strict_lambda` return) =:= f

prop_return_left_lazy_lambda :: (s -> (a,s)) -> Prop (s -> (a,s))
prop_return_left_lazy_lambda f = (f `bind_lazy_lambda` return) =:= f

prop_return_left_let_lambda :: (s -> (a,s)) -> Prop (s -> (a,s))
prop_return_left_let_lambda f = (f `bind_let_lambda` return) =:= f

prop_return_right_strict_lambda :: (a -> s -> (a,s)) -> a -> Prop (s -> (a,s))
prop_return_right_strict_lambda f a = (return a `bind_strict_lambda` f) =:= f a

prop_return_right_lazy_lambda :: (a -> s -> (a,s)) -> a -> Prop (s -> (a,s))
prop_return_right_lazy_lambda f a = (return a `bind_lazy_lambda` f) =:= f a

prop_return_right_let_lambda :: (a -> s -> (a,s)) -> a -> Prop (s -> (a,s))
prop_return_right_let_lambda f a = (return a `bind_let_lambda` f) =:= f a

prop_assoc_strict_lambda :: (s -> (a,s)) -> (a -> s -> (b,s)) -> (b -> s -> (c,s)) -> Prop (s -> (c,s))
prop_assoc_strict_lambda m f g = ((m `bind_strict_lambda` f) `bind_strict_lambda` g) =:= (m `bind_strict_lambda` (\x -> f x `bind_strict_lambda` g))

prop_assoc_lazy_lambda :: (s -> (a,s)) -> (a -> s -> (b,s)) -> (b -> s -> (c,s)) -> Prop (s -> (c,s))
prop_assoc_lazy_lambda m f g = ((m `bind_lazy_lambda` f) `bind_lazy_lambda` g) =:= (m `bind_lazy_lambda` (\x -> f x `bind_lazy_lambda` g))

prop_assoc_let_lambda :: (s -> (a,s)) -> (a -> s -> (b,s)) -> (b -> s -> (c,s)) -> Prop (s -> (c,s))
prop_assoc_let_lambda m f g = ((m `bind_let_lambda` f) `bind_let_lambda` g) =:= (m `bind_let_lambda` (\x -> f x `bind_let_lambda` g))

-- And the same with return as lambda -----------------------------------------



prop_return_lambda_left_strict :: (s -> (a,s)) -> Prop (s -> (a,s))
prop_return_lambda_left_strict f = (f `bind_strict` returnl) =:= f

prop_return_lambda_left_lazy :: (s -> (a,s)) -> Prop (s -> (a,s))
prop_return_lambda_left_lazy f = (f `bind_lazy` returnl) =:= f

prop_return_lambda_right_lazy :: (a -> s -> (a,s)) -> a -> Prop (s -> (a,s))
prop_return_lambda_right_lazy f a = (returnl a `bind_lazy` f) =:= f a

prop_return_lambda_right_strict :: (a -> s -> (a,s)) -> a -> Prop (s -> (a,s))
prop_return_lambda_right_strict f a = (returnl a `bind_strict` f) =:= f a

prop_return_lambda_left_let :: (s -> (a,s)) -> Prop (s -> (a,s))
prop_return_lambda_left_let f = (f `bind_let` returnl) =:= f

prop_return_lambda_right_let :: (a -> s -> (a,s)) -> a -> Prop (s -> (a,s))
prop_return_lambda_right_let f a = (returnl a `bind_let` f) =:= f a

prop_return_lambda_left_strict_lambda :: (s -> (a,s)) -> Prop (s -> (a,s))
prop_return_lambda_left_strict_lambda f = (f `bind_strict_lambda` returnl) =:= f

prop_return_lambda_left_lazy_lambda :: (s -> (a,s)) -> Prop (s -> (a,s))
prop_return_lambda_left_lazy_lambda f = (f `bind_lazy_lambda` returnl) =:= f

prop_return_lambda_left_let_lambda :: (s -> (a,s)) -> Prop (s -> (a,s))
prop_return_lambda_left_let_lambda f = (f `bind_let_lambda` returnl) =:= f

prop_return_lambda_right_strict_lambda :: (a -> s -> (a,s)) -> a -> Prop (s -> (a,s))
prop_return_lambda_right_strict_lambda f a = (returnl a `bind_strict_lambda` f) =:= f a

prop_return_lambda_right_lazy_lambda :: (a -> s -> (a,s)) -> a -> Prop (s -> (a,s))
prop_return_lambda_right_lazy_lambda f a = (returnl a `bind_lazy_lambda` f) =:= f a

prop_return_lambda_right_let_lambda :: (a -> s -> (a,s)) -> a -> Prop (s -> (a,s))
prop_return_lambda_right_let_lambda f a = (returnl a `bind_let_lambda` f) =:= f a

-- Let's also try something with kliesli-composition

(>=>) :: (a -> State s b) -> (b -> State s c) -> a -> State s c
m >=> n = \a s -> uncurry n (m a s)

prop_right_kliesli :: (a -> s -> (a,s)) -> Prop (a -> s -> (a,s))
prop_right_kliesli f = (f >=> return) =:= f

prop_left_kliesli :: (a -> s -> (a,s)) -> Prop (a -> s -> (a,s))
prop_left_kliesli f = (return >=> f) =:= f

prop_assoc_kliesli :: (a -> s -> (b,s)) -> (b -> s -> (c,s)) -> (c -> s -> (d,s)) -> Prop (a -> s -> (d,s))
prop_assoc_kliesli f g h = ((f >=> g) >=> h) =:= (f >=> (g >=> h))

(>==>) :: (a -> State s b) -> (b -> State s c) -> a -> State s c
m >==> n = \a s -> uncurry' n (m a s)

prop_right_kliesli_strict :: (a -> s -> (a,s)) -> Prop (a -> s -> (a,s))
prop_right_kliesli_strict f = (f >==> return) =:= f

prop_left_kliesli_strict :: (a -> s -> (a,s)) -> Prop (a -> s -> (a,s))
prop_left_kliesli_strict f = (return >==> f) =:= f

prop_assoc_kliesli_strict :: (a -> s -> (b,s)) -> (b -> s -> (c,s)) -> (c -> s -> (d,s)) -> Prop (a -> s -> (d,s))
prop_assoc_kliesli_strict f g h = ((f >==> g) >==> h) =:= (f >==> (g >==> h))


-- Let's join and fmap these beasts -------------------------------------------

id x = x

fmap_strict_lambda f m = m `bind_strict_lambda` (\x -> return (f x))
join_strict_lambda n = n `bind_strict_lambda` id
fmap_lazy_lambda f m = m `bind_lazy_lambda` (\x -> return (f x))
join_lazy_lambda n = n `bind_lazy_lambda` id
fmap_let_lambda f m = m `bind_let_lambda` (\x -> return (f x))
join_let_lambda n = n `bind_let_lambda` id
fmap_strict f m = m `bind_strict` (\x -> return (f x))
join_strict n = n `bind_strict` id
fmap_lazy f m = m `bind_lazy` (\x -> return (f x))
join_lazy n = n `bind_lazy` id
fmap_let f m = m `bind_let` (\x -> return (f x))
join_let n = n `bind_let` id

prop_fmap_id_strict :: Prop ((s -> (a,s)) -> (s -> (a,s)))
prop_fmap_id_strict = fmap_strict id =:= id

prop_fmap_id_lazy :: Prop ((s -> (a,s)) -> (s -> (a,s)))
prop_fmap_id_lazy = fmap_lazy id =:= id

prop_fmap_id_let :: Prop ((s -> (a,s)) -> (s -> (a,s)))
prop_fmap_id_let = fmap_let id =:= id

prop_fmap_id_strict_lambda :: Prop ((s -> (a,s)) -> (s -> (a,s)))
prop_fmap_id_strict_lambda = fmap_strict_lambda id =:= id

prop_fmap_id_lazy_lambda :: Prop ((s -> (a,s)) -> (s -> (a,s)))
prop_fmap_id_lazy_lambda = fmap_lazy_lambda id =:= id

prop_fmap_id_let_lambda :: Prop ((s -> (a,s)) -> (s -> (a,s)))
prop_fmap_id_let_lambda = fmap_let_lambda id =:= id


-- Let's just go with the non-lambda definition
(f . g) x = f (g x)

prop_fmap_comp_strict  :: (b -> c) -> (a -> b) -> Prop ((s -> (a,s)) -> s -> (c,s))
prop_fmap_comp_strict f g  = fmap_strict (f . g) =:= fmap_strict f . fmap_strict g

prop_fmap_comp_lazy  :: (b -> c) -> (a -> b) -> Prop ((s -> (a,s)) -> s -> (c,s))
prop_fmap_comp_lazy f g  = fmap_lazy (f . g) =:= fmap_lazy f . fmap_lazy g

prop_fmap_comp_let  :: (b -> c) -> (a -> b) -> Prop ((s -> (a,s)) -> s -> (c,s))
prop_fmap_comp_let f g  = fmap_let (f . g) =:= fmap_let f . fmap_let g

prop_fmap_comp_strict_lambda :: (b -> c) -> (a -> b) -> Prop ((s -> (a,s)) -> s -> (c,s))
prop_fmap_comp_strict_lambda f g = fmap_strict_lambda (f . g) =:= fmap_strict_lambda f . fmap_strict_lambda g

prop_fmap_comp_lazy_lambda :: (b -> c) -> (a -> b) -> Prop ((s -> (a,s)) -> s -> (c,s))
prop_fmap_comp_lazy_lambda f g = fmap_lazy_lambda (f . g) =:= fmap_lazy_lambda f . fmap_lazy_lambda g

prop_fmap_comp_let_lambda :: (b -> c) -> (a -> b) -> Prop ((s -> (a,s)) -> s -> (c,s))
prop_fmap_comp_let_lambda f g = fmap_let_lambda (f . g) =:= fmap_let_lambda f . fmap_let_lambda g



main = do
  quickCheck (printTestCase "prop_return_left_strict" (prop_return_left_strict :: (Int -> (Int,Int)) -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_right_strict" (prop_return_right_strict :: (Int -> Int -> (Int,Int)) -> Int -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_assoc_strict" (prop_assoc_strict :: (Int -> (Int,Int)) -> (Int -> Int -> (Int,Int)) -> (Int -> Int -> (Int,Int)) -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_left_lazy" (prop_return_left_lazy :: (Int -> (Int,Int)) -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_right_lazy" (prop_return_right_lazy :: (Int -> Int -> (Int,Int)) -> Int -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_assoc_lazy" (prop_assoc_lazy :: (Int -> (Int,Int)) -> (Int -> Int -> (Int,Int)) -> (Int -> Int -> (Int,Int)) -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_left_let" (prop_return_left_let :: (Int -> (Int,Int)) -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_right_let" (prop_return_right_let :: (Int -> Int -> (Int,Int)) -> Int -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_assoc_let" (prop_assoc_let :: (Int -> (Int,Int)) -> (Int -> Int -> (Int,Int)) -> (Int -> Int -> (Int,Int)) -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_left_strict_lambda" (prop_return_left_strict_lambda :: (Int -> (Int,Int)) -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_right_strict_lambda" (prop_return_right_strict_lambda :: (Int -> Int -> (Int,Int)) -> Int -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_assoc_strict_lambda" (prop_assoc_strict_lambda :: (Int -> (Int,Int)) -> (Int -> Int -> (Int,Int)) -> (Int -> Int -> (Int,Int)) -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_left_lazy_lambda" (prop_return_left_lazy_lambda :: (Int -> (Int,Int)) -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_right_lazy_lambda" (prop_return_right_lazy_lambda :: (Int -> Int -> (Int,Int)) -> Int -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_assoc_lazy_lambda" (prop_assoc_lazy_lambda :: (Int -> (Int,Int)) -> (Int -> Int -> (Int,Int)) -> (Int -> Int -> (Int,Int)) -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_left_let_lambda" (prop_return_left_let_lambda :: (Int -> (Int,Int)) -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_right_let_lambda" (prop_return_right_let_lambda :: (Int -> Int -> (Int,Int)) -> Int -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_assoc_let_lambda" (prop_assoc_let_lambda :: (Int -> (Int,Int)) -> (Int -> Int -> (Int,Int)) -> (Int -> Int -> (Int,Int)) -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_lambda_left_strict" (prop_return_lambda_left_strict :: (Int -> (Int,Int)) -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_lambda_right_strict" (prop_return_lambda_right_strict :: (Int -> Int -> (Int,Int)) -> Int -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_lambda_left_lazy" (prop_return_lambda_left_lazy :: (Int -> (Int,Int)) -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_lambda_right_lazy" (prop_return_lambda_right_lazy :: (Int -> Int -> (Int,Int)) -> Int -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_lambda_left_let" (prop_return_lambda_left_let :: (Int -> (Int,Int)) -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_lambda_right_let" (prop_return_lambda_right_let :: (Int -> Int -> (Int,Int)) -> Int -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_lambda_left_strict_lambda" (prop_return_lambda_left_strict_lambda :: (Int -> (Int,Int)) -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_lambda_right_strict_lambda" (prop_return_lambda_right_strict_lambda :: (Int -> Int -> (Int,Int)) -> Int -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_lambda_left_lazy_lambda" (prop_return_lambda_left_lazy_lambda :: (Int -> (Int,Int)) -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_lambda_right_lazy_lambda" (prop_return_lambda_right_lazy_lambda :: (Int -> Int -> (Int,Int)) -> Int -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_lambda_left_let_lambda" (prop_return_lambda_left_let_lambda :: (Int -> (Int,Int)) -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_return_lambda_right_let_lambda" (prop_return_lambda_right_let_lambda :: (Int -> Int -> (Int,Int)) -> Int -> Prop (Int -> (Int,Int))))
  quickCheck (printTestCase "prop_right_kliesli" (prop_right_kliesli :: (Int -> Int -> (Int,Int)) -> Prop (Int -> Int -> (Int,Int))))
  quickCheck (printTestCase "prop_left_kliesli" (prop_left_kliesli :: (Int -> Int -> (Int,Int)) -> Prop (Int -> Int -> (Int,Int))))
  quickCheck (printTestCase "prop_assoc_kliesli" (prop_assoc_kliesli :: (Int -> Int -> (Int,Int)) -> (Int -> Int -> (Int,Int)) -> (Int -> Int -> (Int,Int)) -> Prop (Int -> Int -> (Int,Int))))
  quickCheck (printTestCase "prop_fmap_id_strict_lambda" (prop_fmap_id_strict_lambda :: Prop ((Int -> (Int,Int)) -> (Int -> (Int,Int)))))
  quickCheck (printTestCase "prop_fmap_id_lazy_lambda" (prop_fmap_id_lazy_lambda :: Prop ((Int -> (Int,Int)) -> (Int -> (Int,Int)))))
  quickCheck (printTestCase "prop_fmap_id_let_lambda" (prop_fmap_id_let_lambda :: Prop ((Int -> (Int,Int)) -> (Int -> (Int,Int)))))
  quickCheck (printTestCase "prop_fmap_id_strict" (prop_fmap_id_strict :: Prop ((Int -> (Int,Int)) -> (Int -> (Int,Int)))))
  quickCheck (printTestCase "prop_fmap_id_lazy" (prop_fmap_id_lazy :: Prop ((Int -> (Int,Int)) -> (Int -> (Int,Int)))))
  quickCheck (printTestCase "prop_fmap_id_let" (prop_fmap_id_let :: Prop ((Int -> (Int,Int)) -> (Int -> (Int,Int)))))
  quickCheck (printTestCase "prop_fmap_comp_strict_lambda" (prop_fmap_comp_strict_lambda :: (Int -> Int) -> (Int -> Int) -> Prop ((Int -> (Int,Int)) -> Int -> (Int,Int))))
  quickCheck (printTestCase "prop_fmap_comp_lazy_lambda" (prop_fmap_comp_lazy_lambda :: (Int -> Int) -> (Int -> Int) -> Prop ((Int -> (Int,Int)) -> Int -> (Int,Int))))
  quickCheck (printTestCase "prop_fmap_comp_let_lambda" (prop_fmap_comp_let_lambda :: (Int -> Int) -> (Int -> Int) -> Prop ((Int -> (Int,Int)) -> Int -> (Int,Int))))
  quickCheck (printTestCase "prop_fmap_comp_strict" (prop_fmap_comp_strict :: (Int -> Int) -> (Int -> Int) -> Prop ((Int -> (Int,Int)) -> Int -> (Int,Int))))
  quickCheck (printTestCase "prop_fmap_comp_lazy" (prop_fmap_comp_lazy :: (Int -> Int) -> (Int -> Int) -> Prop ((Int -> (Int,Int)) -> Int -> (Int,Int))))
  quickCheck (printTestCase "prop_fmap_comp_let" (prop_fmap_comp_let :: (Int -> Int) -> (Int -> Int) -> Prop ((Int -> (Int,Int)) -> Int -> (Int,Int))))

{- more properties for later :)

return . f = fmap f . return

join . fmap join = join . join
join . fmap return = join . return = id
join . fmap (fmap f) = fmap f . join
-}

