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;