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;