module Collatz;

import Stdlib.Prelude open;

collatzNext (n : Nat) : Nat := ite (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)};