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;