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 : ℕ → Maybe ℕ;
  div2 zero ≔ just zero;
  div2 (suc (suc n)) ≔ mapMaybe suc (div2 n);
  div2 _ ≔ nothing;

  collatzNext : ℕ → ℕ;
  collatzNext n ≔ fromMaybe (suc (3 * n)) (div2 n);

  collatz : ℕ → ℕ;
  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 → ℕ;

  compile parsePositiveInt {
    c ↦ "parsePositiveInt";
  };

  getInitial : ℕ;
  getInitial ≔ parsePositiveInt (readline);

  output : ℕ → ℕ × IO;
  output n ≔ n , putStrLn (natToStr n);

  terminating
  run : (ℕ → ℕ) → ℕ → 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;