module Collatz;

open import Stdlib.Prelude;
open import Stdlib.Data.Nat.Ord;

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

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

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

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

resultHeading : String;
resultHeading := "Collatz sequence:";

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