module Collatz;
  open import Stdlib.Prelude;

  mapMaybe : {A : Type} → {B : Type} → (A → B) → Maybe
    A → Maybe B;
  mapMaybe _ nothing := nothing;
  mapMaybe f (just x) := just (f x);

  div2 : Nat → Maybe Nat;
  div2 zero := just zero;
  div2 (suc (suc n)) := mapMaybe suc (div2 n);
  div2 _ := nothing;

  collatzNext : Nat → Nat;
  collatzNext n := fromMaybe (suc (3 * n)) (div2 n);

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

  --- -----------------------------------------------------------------------------

  --- -----------------------------------------------------------------------------
  axiom readline : String;

  compile readline {
    c ↦ "readline()";
  };

  axiom parsePositiveInt : String → Nat;

  compile parsePositiveInt {
    c ↦ "parsePositiveInt";
  };

  getInitial : Nat;
  getInitial := parsePositiveInt (readline);

  output : Nat → Nat × IO;
  output n := n , putStrLn (natToStr n);

  terminating
  run : (Nat → Nat) → Nat → IO;
  run _ (suc zero) := putStrLn "Finished!";
  run f n := run f (fst (output (f n)));

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

  main : IO;
  main := putStrLn welcome >> run collatz getInitial;
end;