module Demo;

-- standard library prelude
open import Stdlib.Prelude;
-- for comparisons on natural numbers
open import Stdlib.Data.Nat.Ord;
-- for Ordering
open import Stdlib.Data.Ord;

even : Nat → Bool;
even zero := true;
even (suc zero) := false;
even (suc (suc n)) := even n;

even' : Nat → Bool;
even' n := mod n 2 == 0;

-- base 2 logarithm rounded down
terminating
log2 : Nat → Nat;
log2 n := if (n <= 1) 0 (suc (log2 (div n 2)));

type Tree (A : Type) :=
  | leaf : A → Tree A
  | node : A → Tree A → Tree A → Tree A;

mirror : {A : Type} → Tree A → Tree A;
mirror t@(leaf _) := t;
mirror (node x l r) := node x (mirror r) (mirror l);

tree : Tree Nat;
tree := node 2 (node 3 (leaf 0) (leaf 1)) (leaf 7);

preorder : {A : Type} → Tree A → List A;
preorder (leaf x) := x :: nil;
preorder (node x l r) :=
  x :: nil ++ preorder l ++ preorder r;

terminating
sort : {A : Type} → (A → A → Ordering) → List A → List A;
sort _ nil := nil;
sort _ xs@(_ :: nil) := xs;
sort cmp xs :=
  uncurry
    (merge cmp)
    (both (sort cmp) (splitAt (div (length xs) 2) xs));

printNatListLn : List Nat → IO;
printNatListLn nil := printStringLn "nil";
printNatListLn (x :: xs) :=
  printNat x >> printString " :: " >> printNatListLn xs;

main : IO;
main :=
  printStringLn "Hello!"
    >> printNatListLn (preorder (mirror tree))
    >> printNatListLn (sort compare (preorder (mirror tree)))
    >> printNatLn (log2 3)
    >> printNatLn (log2 130);