Collatz.idr

module Delay
%default total


codata Partial : Type -> Type where
  Now   : a -> Partial a
  Later : Partial a -> Partial a


Functor Partial where
  map f (Now x)   = Now (f x)
  map f (Later x) = Later (map f x)

Applicative Partial where
  pure    = Now

  (Now f) <*> (Now x) = Now (f x)
  (Later f) <*> x     = Later (f <*> x)
  f <*> (Later x)     = Later (f <*> x)

Monad Partial where
  (Now x) >>= f   = f x
  (Later x) >>= f = Later (x >>= f)


never : Partial a
never = Later never

runForSteps : Partial a -> Nat -> Partial a
runForSteps (Now x) k       = Now x
runForSteps (Later x) Z     = Later x
runForSteps (Later x) (S k) = runForSteps x k

runForSteps' : Partial a -> Nat -> List (Partial a)
runForSteps' (Now x) k       = [Now x]
runForSteps' (Later x) Z     = [Later x]
runForSteps' (Later x) (S k) = (Later x) :: (runForSteps' x k)


isEven : Nat -> Bool
isEven Z         = True
isEven (S Z)     = False
isEven (S (S n)) = isEven n

collatzStep : Nat -> Nat
collatzStep n with (isEven n)
  | True  = divNatNZ n 2 (absurd . sym)
  | False = (3 * n) + 1

collatz : Nat -> Partial Nat
collatz n = if n <= 1 then (Now n)
                      else (Later (collatz (collatzStep n)))