Demo

examples/demo/Demo.juvix

@@ -0,0 +1,56 @@
+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);
+
+end;