```module Number.Peano.Inf.Functions
( minimum
, maximum
, length
, nodeRank
) 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)

{- |
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 @dependence n == []@ then @nodeRank n == infinity@, because @n@ is not accessable.

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

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

If there is an inevitable cycle in the graph, the rank is @infinity@.
One can observe these cases, due to the observable infinity value.
-}
nodeRank
:: Ord n
=> (n -> [[n]])         -- ^ dependence function
-> n                    -- ^ node
-> Nat                  -- ^ rank of the node
nodeRank dependence node = rank Set.empty node  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')

```