-- (c) MP-I and CP (1998/99-2011/12)

module List  where

import Cp
import Nat

-- (1) Datatype definition -----------------------------------------------------

--- Haskell lists are already defined, so the following is a dummy, informal declaration:
--- data [a] = [] | (a : [a])

inl = either (const []) (uncurry (:))

out []    = i1 ()
out (a:x) = i2(a,x)

-- (2) Ana + cata + hylo -------------------------------------------------------

cata h   = h . rec (cata h) . out   

rec f    = id -|- id >< f

ana g    = inl . (rec (ana g) ) . g

hylo g h = cata g . ana h

-- (3) Map ---------------------------------------------------------------------
-- instance Functor []
--          where fmap f = cata ( inl . (id -|- f >< id ))
-- NB: already in the Haskell Prelude

-- (4) Examples ----------------------------------------------------------------

-- (4.1) inversion -------------------------------------------------------------

invl = cata (either nil snoc)
       where nil = const []
	     snoc(a,l) = l ++ [a]

-- alternatively: snoc = conc . swap . (singl >< id)
--                       where singl a = [a]
--                             conc = uncurry (++)

-- (4.2) Look-up function ------------------------------------------------------

look :: Eq a => a -> [(a,b)] -> Maybe b
look k = cata (either nothing aux)
	 where nothing = const Nothing
               aux((a,b),r)
                      | a == k    = Just b
                      | otherwise = r

-- (4.3) Insertion sort --------------------------------------------------------

iSort :: Ord a => [a] -> [a]
iSort =  cata (either nil insert)
         where nil = const []
               insert(x,[])              = [x]
               insert(x,a:l) | x < a     = [x,a]++l
                             | otherwise = a:(insert(x,l))

-- also iSort = hylo (either (const []) insert) out

-- (4.4) take (cf GHC.List.take) -----------------------------------------------

take' = curry (ana aux)
         where aux(0,_) = i1()
               aux(_,[]) = i1()
        ---    aux(n+1,x:xs) = i2(x,(n,xs))
               aux(n,x:xs) = i2(x,(n-1,xs))

-- pointwise version:
-- take 0 _ = []
-- take _ [] = []
-- take (n+1) (x:xs) = x : take n xs

-- (4.5) Factorial--------------------------------------------------------------

fac = hylo multiplyall nats

-- where

multiplyall = either (const 1) mul
mul = uncurry (*)

nats = (id -|- (split succ id)) . outNat

-- (4.5.1) Factorial (alternative) ---------------------------------------------

fac' = hylo (either (const 1) (mul . (succ >< id)))
                 ((id -|- (split id id)) . outNat)

{-- cf:

fac' = hylo (either (const 1) g) nats'
       where g(n,m) = (n+1) * m
             nats' 0 = i1 ()
             nats' (n+1) = i2 (n,n)
--}

-- (4.6) Square function -------------------------------------------------------

{-- pointwise:
sq 0 = 0
sq (n+1) = 2*n+1 + sq n

cf. Newton's binomial: (n+1)^2 = n^2 + 2n + 1
--}

sq = hylo summing odds

summing = either (const 0) (uncurry (+))

odds = (id -|- (split impar id)) . outNat
       where impar n = 2*n+1

{-- odds pointwise:
odds 0 = i1 ()
odds (n+1) = i2 (2*n+1,n)
--}

-- (4.6.1) Square function reusing ana of factorial ----------------------------

sq' = (cata summing) . fmap (\n->2*n-1) . (ana nats)

-- (4.7) Prefixes and suffixes -------------------------------------------------

prefixes :: Eq a => [a] -> [[a]]
prefixes = cata (either (const [[]]) scan)
           where scan(a,l) = [[]] ++ (map (a:) l)

suffixes = ana g
           where g []   = i1 []
                 g(h:t) = i2(h:t,t)

--------------------------------------------------------------------------------