module Collatz;

import Stdlib.Prelude open;

collatzNext (n : Nat) : Nat := if (mod n 2 == 0) (div n 2) (3 * n + 1);

collatz : Nat → Nat
  | zero := zero
  | (suc zero) := suc zero
  | n := collatzNext n;

terminating
run (f : Nat → Nat) : Nat → IO
  | (suc zero) := printNatLn 1 >> printStringLn "Finished!"
  | n := printNatLn n >> run f (f n);

welcome : String :=
  "Collatz calculator\n------------------\n\nType a number then ENTER";

resultHeading : String := "Collatz sequence:";

main : IO :=
  printStringLn welcome
    >> readLn
      λ {s := printStringLn resultHeading >> run collatz (stringToNat s)};