{- |
Description : Successor Functor
Copyright   : © Joachim Breitner, 2017
License     : MIT
Maintainer  : mail@joachim-breitner.de

A value of type @'Succs' a@ represents a step in a graph with nodes of type @a@, or in other words, a node plus the list of its successors.

The 'Applicative' instance for @'Succs' a@ is such that the node represented by @a '<*>' b@ is the application of the node of @a@ applied to the node of @b@, and (more importantly) the successors modeled by @a '<*>' b@ are the node of @a@ applied to the succesors of @b@ in addition to the succesors of @a@ applied to the node of @b@. This way, at most one step is taken.

>>> (++) <$> Succs "0" ["1","2"] <*> Succs "A" ["B","C"]
Succs "0A" ["1A","2A","0B", "0C"]

>>> skip x = Succs [x] [[]]
>>> getSuccs $ (concat <$> traverse skip "Hello")
["ello","Hllo","Helo","Helo","Hell"]

This applicative functor can be useful to define shrink functions for QuickCheck, using the helper

> shrinkSuccs x = Succs x (shrink x)

as explained in a <http://stackoverflow.com/a/41944525/946226 StackExchange answer.>

-}
module Control.Applicative.Successors where

data Succs a = Succs a [a] deriving (Show, Eq)

instance Functor Succs where
    fmap f (Succs o s) = Succs (f o) (map f s)

instance Applicative Succs where
    pure x = Succs x []
    Succs f fs <*> Succs x xs = Succs (f x) (map ($x) fs ++ map f xs)


instance Monad Succs where
    Succs x xs >>= f = Succs y (map (getCurrent . f) xs ++ ys)
      where Succs y ys = f x

-- | Returns the represented node
--
-- Properties:
--
-- prop> getCurrent (pure x)  == x
-- prop> getCurrent (f <*> x) == (getCurrent f) (getCurrent x)
-- prop> getCurrent (x >>= k) == getCurrent (k (getCurrent x))
getCurrent :: Succs t -> t
getCurrent (Succs x _) = x

-- | Returns the represented successors
--
-- prop> getSuccs (pure x)  == []
-- prop> getSuccs (f <*> x) == map ($ getCurrent x) (getSuccs f) ++ map (getCurrent f) (getSuccs x)
-- prop> getSuccs (x >>= k) == map (getCurrent . k) (getSuccs x) ++ getSuccs k (getCurrent x)
getSuccs :: Succs t -> [t]
getSuccs (Succs _ xs) = xs

{-

The Applicative laws:

  pure id <*> Succs x xs
= Succs id [] <*> Succs x xs
= Succs (id x) (map ($x) [] ++ map id xs)
= Succs x xs

  pure (.) <*> Succs u us <*> Succs v vs <*> Succs w ws
= Succs (.) [] <*> Succs u us <*> Succs v vs <*> Succs w ws
= Succs (u .) (map (.) us) <*> Succs v vs <*> Succs w ws
= Succs (u . v) (map ($v) (map (.) us) ++ map (u .) vs) <*> Succs w ws
= Succs (u . v) (map (($v).(.)) us ++ map (u .) vs) <*> Succs w ws
= Succs ((u . v) w) (map ($w) (map (($v).(.)) us ++ map (u .) vs) ++ map (u.v) ws)
= Succs ((u . v) w) (map (($w).($v).(.)) us ++ map (($w).(u.)) vs ++ map (u.v) ws)
= Succs (u (v w)) (map (\u -> u (v w)) us ++ map (\v -> u (v w)) vs ++ map (\w -> u (v w)) ws)
= Succs (u (v w)) (map ($(v w)) us ++ map u (map ($w) vs ++ map v ws))
= Succs u us <*> Succs (v w) (map ($w) vs ++ map v ws)
= Succs u us <*> (Succs v vs <*> Succs w ws)

  pure f <*> pure x
= Succs f [] <*> Succs x []
= Succs (f x) []
= pure (f x)

  Succs u us <*> pure y
= Succs u us <*> Succs y []
= Succs (u y) (map ($y) us)
= Succs (($y) u) (map ($y) us)
= Succs ($y) [] <*> Succs u us
= pure ($ y) <*> u

The Monad laws:
  return a >>= k
= Succs a [] >>= k
= let Succs y ys = k a in Succs y (map (getCurrent . k) [] ++ ys)
= let Succs y ys = k a in Succs y ys
= k a

  Succs x xs >>= return
= let Succs y ys = return x in Succs y (map (getCurrent . return) xs ++ ys)
= let Succs y ys = Succs x [] in Succs y (map (getCurrent . return) xs ++ ys)
= Succs x (map (getCurrent . return) xs ++ [])
= Succs x xs

Lemma: getCurrent (s >>= k) = getCurrent (k (getCurrent s))
Proof:
  getCurrent (Succs x xs >>= k)
= getCurrent (let Succs y ys = k x in Succs y …)
= let Succs y ys = k x in y
= getCurrent (k x)
= getCurrent (k (getCurrent (Succs x xs)))

  Succs x xs >>= (\x -> k x >>= h)
= let Succs z zs = (\x -> k x >>= h) x in Succs z (map (getCurrent . (\x -> k x >>= h)) xs ++ zs)
= let Succs z zs = k x >>= h in Succs z (map (getCurrent . (\x -> k x >>= h)) xs ++ zs)
= let Succs z zs = k x >>= h in Succs z (map (getCurrent . (\x -> k x >>= h)) xs ++ zs)
= let Succs z zs = k x >>= h in Succs z (map (getCurrent . (\x -> k x >>= h)) xs ++ zs)
= let Succs z zs = (let Succs y ys = k x in Succs y ys >>= h) in Succs z (map (getCurrent . (\x -> k x >>= h)) xs ++ zs)
= let Succs z zs = (let Succs y ys = k x in let Succs z zs = h y in Succs z (map (getCurrent . h) ys ++ zs)) in Succs z (map (getCurrent . (\x -> k x >>= h)) xs ++ zs)
= let Succs y ys = k x in let Succs z zs = h y in let Succs z zs = Succs z (map (getCurrent . h) ys ++ zs) in Succs z (map (getCurrent . (\x -> k x >>= h)) xs ++ zs)
= let Succs y ys = k x in let Succs z zs = h y in Succs z (map (getCurrent . (\x -> k x >>= h)) xs ++ map (getCurrent . h) ys ++ zs)
= let Succs y ys = k x in let Succs z zs = h y in Succs z (map (\x -> getCurrent (k x >>= h)) xs ++ map (getCurrent . h) ys ++ zs)
= let Succs y ys = k x in let Succs z zs = h y in Succs z (map (\x -> getCurrent (h (getCurrent (k x)))) xs ++ map (getCurrent . h) ys ++ zs)
= let Succs y ys = k x in let Succs z zs = h y in Succs z (map (getCurrent . h . getCurrent . k) xs ++ map (getCurrent . h) ys ++ zs)
= let Succs y ys = k x in let Succs z zs = h y in Succs z (map (getCurrent . h) (map (getCurrent . k) xs ++ ys) ++ zs)
= let Succs y ys = k x in Succs y (map (getCurrent . k) xs ++ ys) >>= h
= (let Succs y ys = k x in Succs y (map (getCurrent . k) xs ++ ys)) >>= h
= (Succs x xs >>= k) >>= h

Lemma: (<*>) = ap
Proof:
  Succs f fs <*> Succs x xs
= Succs (f x) (map ($x) fs ++ map f xs)
= let Succs y ys = Succs (f x) (map f xs) in Succs y (map ($x) fs ++ ys)
= let Succs y ys = Succs (f x) (map (\x -> f x) xs) in Succs y (map ($x) fs ++ ys)
= let Succs y ys = Succs (f x) (map (getCurrent . (\x -> pure (f x)) xs)) in Succs y (map ($x) fs ++ ys)
= let Succs y ys = let Succs z zs = pure (f x) in Succs z (map (getCurrent . (\x -> pure (f x)) xs ++ zs)) in Succs y (map ($x) fs ++ ys)
= let Succs y ys = Succs x xs >>= \x -> pure (f x) in Succs y (map ($x) fs ++ ys)
= let Succs y ys = Succs x xs >>= \x -> pure (f x) in Succs y (map (\f -> getCurrent ((\x -> pure (f x)) (getCurrent (Succs x xs)))) fs ++ ys)
= let Succs y ys = Succs x xs >>= \x -> pure (f x) in Succs y (map (\f -> getCurrent (Succs x xs >>= (\x -> pure (f x)))) fs ++ ys)
= let Succs y ys = Succs x xs >>= \x -> pure (f x) in Succs y (map (getCurrent . (\f -> Succs x xs >>= (\x -> pure (f x)))) fs ++ ys)
= Succs f fs >>= (\f -> Succs x xs >>= (\x -> pure (f x)))
= Succs f fs `ap` Succs x xs

-}