```module Number.Peano.Inf.Functions
( minimum
, maximum
, length
, nodeRank
--    , nodeRankSimple
, nodeRankMemo
, nodeRankMemoIntegral
) where

import Number.Peano.Inf

import qualified Data.Set as Set

import qualified Prelude
import Prelude hiding (minimum, maximum, length)

{- |
Minimum of the list elements.
Works also for empty lists.
-}
minimum :: [Nat] -> Nat
minimum = foldr min infinity

{- |
Maximum of the list elements.
Works also for empty lists.
-}
maximum :: [Nat] -> Nat
maximum = foldr max 0

{- |
Lazyness properties of @Nat@ makes it ideal for lazy list length computation.
Examples:

> length [1..] > 100

> length undefined >= 0

> length (undefined: undefined) >= 1
-}
length :: [a] -> Nat
length [] = 0
length (_:t) = succ (length t)

nodeRankSimple
:: (n -> [[n]])
-> n
-> Nat

nodeRankSimple dependence = rank where

rank = minimum . map f . dependence

f = maximum . map (succ . rank)

{- |
Rank computation with lazy Peano numbers.

The dependence function represents a graph with multiedges (edges with multiple start nodes).
@dependence n@ is the list of the start nodes of all multiedges whose end node is @n@.

@nodeRank n@ computes the length of the shortest path to @n@. Note that if @n@ is an end point of a multiedge with no start point,
then @nodeRank n == 0@.

* If @any null (dependence n)@ then @nodeRank n == 0@.

* Otherwise @nodeRank n == 1 + minimum [maximum (map nodeRank l1), maximum (map nodeRank l2), ..] where @[l1, l2, ..] == dependence n@ if this is computable.@

* Otherwise the rank is @infinity@. (These cases are observable.)
-}
nodeRank
:: Ord n
=> (n -> [[n]])         -- ^ dependence function
-> n                    -- ^ node
-> Nat                  -- ^ rank of the node

nodeRank dependence = rank Set.empty  where

rank visited node
| Set.member node visited   = infinity
| otherwise                 = minimum \$ map f \$ dependence node
where
visited' = Set.insert node visited

f = maximum . map (succ . rank visited')

{- |
Memoising version of @nodeRank@.

The rank of inaccessable nodes are @inductive_infinity@.
These cases are observable with the predicate @(> n)@ where @n@ is an upper bound for the number of nodes in the graph.
-}
nodeRankMemo
:: (n -> [[n]])         -- ^ dependence function
-> (n -> Nat)           -- ^ memoised version of the result function
-> (n -> Nat)           -- ^ rank of a node

nodeRankMemo dependence rank' = rank  where

rank = minimum . map f . dependence

f = maximum . map (succ . rank')

{- |
@nodeRankMemo@ specialised for integral types.
-}
nodeRankMemoIntegral
:: Integral a
=> (a -> [[a]])         -- ^ dependence function
-> a                    -- ^ node number
-> Nat                  -- ^ rank of the node

nodeRankMemoIntegral dep = f where

f = nodeRankMemo dep (memoise f)

----------------- memoisation for non-negative integrals

data T x = B x (T x) (T x)

memoise :: Integral a => (a -> x) -> (a -> x)
memoise = decode . code
where
code f = B (f 0) (code (\n -> f (2*n+1)))
(code (\n -> f (2*n+2)))

decode (B x l r) n
| n == 0    = x
| odd n     = decode l (n `div` 2)
| otherwise = decode r ((n-2) `div` 2)

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

```