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

module Nat  where

import Cp

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

-- "data Nat = 0 | succ Nat"   -- in fact: Haskell Integer is used as carrier type

inNat = either (const 0) succ

outNat 0 = i1 ()
--outNat (n+1) = i2 n
outNat n = i2(n-1)

-- NB: inNat and outNat are isomorphisms only if restricted to non-negative integers

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

cataNat g   = g . recNat (cataNat g) . outNat

recNat f    = id -|- f

anaNat h    = inNat . (recNat (anaNat h) ) . h

hyloNat g h = cataNat g . anaNat h

-- paraNat g   = g . recNat (split id (paraNat g)) . outNat

-- (3) Map ---------------------------------------------------------------------

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

for :: (Integral b) => (a -> a) -> a -> b -> a
-- for is the "fold" of natural numbers
for b i = cataNat (either (const i) b)

somar a = cataNat (either (const a) succ)

multip a = cataNat (either (const 0) (a+))

exp a = cataNat (either (const 1) (a*))

sq 0 = 0
--sq (n+1) = oddn n + sq n where oddn n = 2*n+1
sq n = oddn(n-1) + sq(n-1) where oddn n = 2*n+1
-- sq = paraNat (either (const 0) g)i

sq' = p1 . aux
       -- this is the outcome of calculating sq as a for loop using the
       -- mutual recursion law
      where aux = cataNat (either (split (const 0)(const 1)) (split (uncurry (+))((2+).p2)))

sq'' n  = -- the same as a for loop (putting variables in)
       p1 (for body (0,1) n)
       where body(s,o) = (s+o,2+o)

-- factorial = paraNat (either (const 1) g)
--         where g(n,r) = (n+1) * r

-- Integer division as a hylomorphism ------------------------------------

idiv :: Integer -> Integer -> Integer
{-- pointwise
x `wdivx`y  |   x <  y    = 0
            |   x >= y    = (x - y) `wdiv` y + 1
--}

idiv = flip aux

aux y = hyloNat conquer divide where 
       divide x | x <  y  = i1 ()
                | x >= y  = i2(x - y)
       conquer = inNat