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')