module Collatz;

import Stdlib.Prelude open;

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

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

terminating
run (f : Nat -> Nat) (n : Nat) : IO :=
  case n of
    | 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)};