From dbf0463bb6bd91a9d665c74619218863a6aeb71a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=81ukasz=20Czajka?=
 <62751+lukaszcz@users.noreply.github.com>
Date: Fri, 11 Oct 2024 10:53:34 +0200
Subject: [PATCH] Merge the containers library (#125)

* Depends on https://github.com/anoma/juvix/pull/3087
---
 Stdlib/Cairo/Pedersen.juvix     |   3 +-
 Stdlib/Data/BinaryTree.juvix    |  20 +++
 Stdlib/Data/Map.juvix           |  72 +++++++++
 Stdlib/Data/Maybe/Base.juvix    |   5 +
 Stdlib/Data/Queue.juvix         |   3 +
 Stdlib/Data/Queue/Base.juvix    |  81 ++++++++++
 Stdlib/Data/Result.juvix        |  10 ++
 Stdlib/Data/Set.juvix           |  11 ++
 Stdlib/Data/Set/AVL.juvix       | 263 ++++++++++++++++++++++++++++++++
 Stdlib/Data/Tree.juvix          |  31 ++++
 Stdlib/Data/UnbalancedSet.juvix |  46 ++++++
 test/Package.juvix              |   5 +-
 test/Test.juvix                 |  98 ++++++------
 test/Test/AVL.juvix             |  96 ++++++++++++
 test/Test/Map.juvix             |  56 +++++++
 test/Test/Queue.juvix           |  44 ++++++
 test/Test/StdlibTestExtra.juvix |  11 --
 test/Test/UnbalancedSet.juvix   |  32 ++++
 test/juvix.lock.yaml            |  14 +-
 19 files changed, 841 insertions(+), 60 deletions(-)
 create mode 100644 Stdlib/Data/BinaryTree.juvix
 create mode 100644 Stdlib/Data/Map.juvix
 create mode 100644 Stdlib/Data/Queue.juvix
 create mode 100644 Stdlib/Data/Queue/Base.juvix
 create mode 100644 Stdlib/Data/Set.juvix
 create mode 100644 Stdlib/Data/Set/AVL.juvix
 create mode 100644 Stdlib/Data/Tree.juvix
 create mode 100644 Stdlib/Data/UnbalancedSet.juvix
 create mode 100644 test/Test/AVL.juvix
 create mode 100644 test/Test/Map.juvix
 create mode 100644 test/Test/Queue.juvix
 delete mode 100644 test/Test/StdlibTestExtra.juvix
 create mode 100644 test/Test/UnbalancedSet.juvix

diff --git a/Stdlib/Cairo/Pedersen.juvix b/Stdlib/Cairo/Pedersen.juvix
index 55ccf585..47479986 100644
--- a/Stdlib/Cairo/Pedersen.juvix
+++ b/Stdlib/Cairo/Pedersen.juvix
@@ -1,8 +1,7 @@
 module Stdlib.Cairo.Pedersen;
 
 import Stdlib.Data.Field open using {Field};
-import
-Stdlib.Cairo.Ec as Ec;
+import Stdlib.Cairo.Ec as Ec;
 
 module ConstantPoints;
   P0 : Ec.Point :=
diff --git a/Stdlib/Data/BinaryTree.juvix b/Stdlib/Data/BinaryTree.juvix
new file mode 100644
index 00000000..e5876a06
--- /dev/null
+++ b/Stdlib/Data/BinaryTree.juvix
@@ -0,0 +1,20 @@
+module Stdlib.Data.BinaryTree;
+
+import Stdlib.Data.Nat open;
+import Stdlib.Data.List open;
+
+type BinaryTree (A : Type) :=
+  | leaf : BinaryTree A
+  | node : BinaryTree A -> A -> BinaryTree A -> BinaryTree A;
+
+--- fold a tree in depth first order
+fold {A B} (f : A -> B -> B -> B) (acc : B) : BinaryTree A -> B :=
+  let
+    go (acc : B) : BinaryTree A -> B
+      | leaf := acc
+      | (node l a r) := f a (go acc l) (go acc r);
+  in go acc;
+
+length : {A : Type} -> BinaryTree A -> Nat := fold λ {_ l r := 1 + l + r} 0;
+
+to-list : {A : Type} -> BinaryTree A -> List A := fold λ {e ls rs := e :: ls ++ rs} nil;
diff --git a/Stdlib/Data/Map.juvix b/Stdlib/Data/Map.juvix
new file mode 100644
index 00000000..eb3995e3
--- /dev/null
+++ b/Stdlib/Data/Map.juvix
@@ -0,0 +1,72 @@
+module Stdlib.Data.Map;
+
+import Stdlib.Data.Pair open;
+import Stdlib.Data.Maybe open;
+import Stdlib.Data.List open;
+import Stdlib.Data.Nat open;
+
+import Stdlib.Trait.Functor open;
+import Stdlib.Trait.Foldable open;
+import Stdlib.Trait.Ord open;
+
+import Stdlib.Function open;
+
+import Stdlib.Data.Set as Set;
+open Set using {Set};
+
+import Stdlib.Data.Set.AVL as AVL;
+open AVL using {AVLTree};
+
+import Stdlib.Data.BinaryTree as Tree;
+
+type Binding A B := binding A B;
+
+key {A B} : Binding A B -> A
+  | (binding a _) := a;
+
+value {A B} : Binding A B -> B
+  | (binding _ b) := b;
+
+toPair {A B} : Binding A B -> Pair A B
+  | (binding a b) := a, b;
+
+instance
+bindingKeyOrdering {A B} {{Ord A}} : Ord (Binding A B) :=
+  mkOrd λ {b1 b2 := Ord.cmp (key b1) (key b2)};
+
+type Map A B := mkMap (AVLTree (Binding A B));
+
+empty {A B} : Map A B := mkMap AVL.empty;
+
+{-# specialize: [1, f] #-}
+insertWith {A B} {{Ord A}} (f : B -> B -> B) (k : A) (v : B) : Map A B -> Map A B
+  | (mkMap s) :=
+    let
+      f' : Binding A B -> Binding A B -> Binding A B
+        | (binding a b1) (binding _ b2) := binding a (f b1 b2);
+    in mkMap (Set.insertWith f' (binding k v) s);
+
+insert {A B : Type} {{Ord A}} : A -> B -> Map A B -> Map A B := insertWith λ {old new := new};
+
+{-# specialize: [1] #-}
+lookup {A B} {{Ord A}} (k : A) : Map A B -> Maybe B
+  | (mkMap s) := map value (Set.lookupWith key k s);
+
+{-# specialize: [1, f] #-}
+fromListWith {A B} {{Ord A}} (f : B -> B -> B) (xs : List (Pair A B)) : Map A B :=
+  for (acc := empty) (k, v in xs)
+    insertWith f k v acc;
+
+fromList {A B} {{Ord A}} : List (Pair A B) -> Map A B := fromListWith λ {old new := new};
+
+toList {A B} : Map A B -> List (Pair A B)
+  | (mkMap s) := map (x in Set.toList s) toPair x;
+
+size {A B} : Map A B -> Nat
+  | (mkMap s) := Set.size s;
+
+delete {A B} {{Ord A}} (k : A) : Map A B -> Map A B
+  | m@(mkMap s) := Set.deleteWith key k s |> mkMap;
+
+instance
+eqMapI {A B} {{Eq A}} {{Eq B}} : Eq (Map A B) := mkEq (Eq.eq on toList);
diff --git a/Stdlib/Data/Maybe/Base.juvix b/Stdlib/Data/Maybe/Base.juvix
index aca04467..390226d3 100644
--- a/Stdlib/Data/Maybe/Base.juvix
+++ b/Stdlib/Data/Maybe/Base.juvix
@@ -1,6 +1,7 @@
 module Stdlib.Data.Maybe.Base;
 
 import Juvix.Builtin.V1.Maybe open public;
+import Juvix.Builtin.V1.Bool open;
 
 --- Extracts the value from a ;Maybe; if present, else returns the given value.
 {-# inline: true #-}
@@ -14,3 +15,7 @@ fromMaybe {A} (a : A) : Maybe A → A
 maybe {A B} (b : B) (f : A → B) : Maybe A → B
   | nothing := b
   | (just a) := f a;
+
+isJust {A} : Maybe A -> Bool
+  | nothing := false
+  | (just _) := true;
diff --git a/Stdlib/Data/Queue.juvix b/Stdlib/Data/Queue.juvix
new file mode 100644
index 00000000..c75a4209
--- /dev/null
+++ b/Stdlib/Data/Queue.juvix
@@ -0,0 +1,3 @@
+module Stdlib.Data.Queue;
+
+import Stdlib.Data.Queue.Base open public;
diff --git a/Stdlib/Data/Queue/Base.juvix b/Stdlib/Data/Queue/Base.juvix
new file mode 100644
index 00000000..1b715f38
--- /dev/null
+++ b/Stdlib/Data/Queue/Base.juvix
@@ -0,0 +1,81 @@
+--- This module provides an implementation of a First-In, First-Out (FIFO)
+--- queue based on Okasaki's "Purely Functional Data Structures." Ch.3.
+---
+--- This Okasaki Queue version data structure ensures amortized constant-time
+--- performance for basic operations such as push, pop, and front.
+---
+--- The Okasaki Queue consists of two lists (front and back) to separate
+--- the concerns of adding and removing elements for ensuring efficient
+--- performance.
+module Stdlib.Data.Queue.Base;
+
+import Stdlib.Data.List open;
+import Stdlib.Data.Bool open;
+import Stdlib.Data.Maybe open;
+import Stdlib.Data.Pair open;
+import Stdlib.Data.Nat open;
+import Stdlib.Function open;
+import Stdlib.Trait.Foldable open;
+
+--- A first-in-first-out data structure
+type Queue (A : Type) := queue (List A) (List A);
+
+--- 𝒪(1). The empty ;Queue;.
+empty {A} : Queue A := queue nil nil;
+
+--- 𝒪(1). Returns ;true; when the ;Queue; has no elements.
+isEmpty {A} : Queue A -> Bool
+  | (queue nil nil) := true
+  | _ := false;
+
+--- 𝒪(1). Returns first element of the ;Queue;, if any.
+head {A} : Queue A -> Maybe A
+  | (queue nil _) := nothing
+  | (queue (x :: _) _) := just x;
+
+--- 𝒪(1). Removes the first element from the ;Queue;. If the ;Queue; is empty
+--  then returns ;nothing;.
+tail {A} : Queue A -> Maybe (Queue A)
+  | (queue nil _) := nothing
+  | (queue (_ :: front) back) := just (queue front back);
+
+--- 𝒪(n) worst-case, but 𝒪(1) amortized
+{-# inline: true #-}
+check {A} : Queue A -> Queue A
+  | (queue nil back) := queue (reverse back) nil
+  | q := q;
+
+--- 𝒪(n) worst-case, but 𝒪(1) amortized. Returns the first element and the
+--  rest of the ;Queue;. If the ;Queue; is empty then returns ;nothing;.
+pop {A} : Queue A -> Maybe (Pair A (Queue A))
+  | (queue nil _) := nothing
+  | (queue (x :: front) back) := just (x, check (queue front back));
+
+--- 𝒪(1). Adds an element to the end of the ;Queue;.
+push {A} (x : A) : Queue A -> Queue A
+  | (queue front back) := check (queue front (x :: back));
+
+--- 𝒪(n). Adds a list of elements to the end of the ;Queue;.
+pushMany {A} (xs : List A) (q : Queue A) : Queue A := for (acc := q) (x in xs) push x acc;
+
+--- 𝒪(n). Build a ;Queue; from a ;List;.
+fromList {A} (xs : List A) : Queue A := pushMany xs empty;
+
+--- toList: O(n). Returns a ;List; of the elements in the ;Queue;.
+--- The elements are in the same order as they appear in the ;Queue;
+--- (i.e. the first element of the ;Queue; is the first element of the ;List;).
+toList {A} : Queue A -> List A
+  | (queue front back) := front ++ reverse back;
+
+--- 𝒪(n). Returns the number of elements in the ;Queue;.
+size {A} : Queue A -> Nat
+  | (queue front back) := length front + length back;
+
+instance
+eqQueueI {A} {{Eq A}} : Eq (Queue A) := mkEq ((==) on toList);
+
+instance
+showQueueI {A} {{Show A}} : Show (Queue A) := mkShow (toList >> Show.show);
+
+instance
+ordQueueI {A} {{Ord A}} : Ord (Queue A) := mkOrd (Ord.cmp on toList);
diff --git a/Stdlib/Data/Result.juvix b/Stdlib/Data/Result.juvix
index a46bb681..98b301f6 100644
--- a/Stdlib/Data/Result.juvix
+++ b/Stdlib/Data/Result.juvix
@@ -2,9 +2,11 @@ module Stdlib.Data.Result;
 
 import Stdlib.Data.Result.Base open public;
 import Stdlib.Data.Bool.Base open;
+import Stdlib.Data.String.Base open;
 
 import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
+import Stdlib.Trait.Show open;
 import Stdlib.Trait open;
 
 {-# specialize: true, inline: case #-}
@@ -28,6 +30,14 @@ eqResultI {A B} {{Eq A}} {{Eq B}} : Eq (Result A B) :=
       | _ _ := false
   };
 
+instance
+showResultI {A B} {{Show A}} {{Show B}} : Show (Result A B) :=
+  mkShow@{
+    show : Result A B -> String
+      | (error x) := "Error (" ++str Show.show x ++str ")"
+      | (ok x) := "Ok (" ++str Show.show x ++str ")"
+  };
+
 {-# specialize: true, inline: case #-}
 instance
 functorResultI {err} : Functor (Result err) :=
diff --git a/Stdlib/Data/Set.juvix b/Stdlib/Data/Set.juvix
new file mode 100644
index 00000000..fca6d9d6
--- /dev/null
+++ b/Stdlib/Data/Set.juvix
@@ -0,0 +1,11 @@
+module Stdlib.Data.Set;
+
+import Stdlib.Data.Set.AVL open public;
+import Stdlib.Trait.Eq as Eq open using {Eq};
+import Stdlib.Trait.Ord as Ord open using {Ord};
+
+syntax alias Set := AVLTree;
+
+eqSetI {A} {{Eq A}} : Eq (Set A) := eqAVLTreeI;
+
+ordSetI {A} {{Ord A}} : Ord (Set A) := ordAVLTreeI;
diff --git a/Stdlib/Data/Set/AVL.juvix b/Stdlib/Data/Set/AVL.juvix
new file mode 100644
index 00000000..988bd507
--- /dev/null
+++ b/Stdlib/Data/Set/AVL.juvix
@@ -0,0 +1,263 @@
+--- AVL trees are a type of self-balancing binary search tree, where the heights
+--- of the left and right subtrees of every node differ by at most 1. This
+--- ensures that the height of the tree is logarithmic in the number of nodes,
+--- which guarantees efficient insertion, deletion, and search operations (all
+--- are guaranteed to run in 𝒪(log 𝓃) time).
+---
+--- This module defines an AVL tree data type and provides functions for
+--- constructing, modifying, and querying AVL trees.
+module Stdlib.Data.Set.AVL;
+
+import Stdlib.Data.Tree as Tree open using {Tree; Forest};
+import Stdlib.Data.Maybe open;
+import Stdlib.Data.Nat open;
+import Stdlib.Data.Int open;
+import Stdlib.Data.Bool open;
+import Stdlib.Data.Pair open;
+import Stdlib.Data.List open;
+import Stdlib.Data.String open;
+import Stdlib.Trait.Foldable open;
+import Stdlib.Function open;
+
+--- A self-balancing binary search tree.
+type AVLTree (A : Type) :=
+  | --- An empty AVL tree.
+    empty
+  | --- A node of an AVL tree.
+    node A Nat (AVLTree A) (AVLTree A);
+
+--- 𝒪(1) Retrieves the height of an ;AVLTree;. The height is the distance from
+--- the root to the deepest child.
+height {A} : AVLTree A -> Nat
+  | empty := 0
+  | (node _ h _ _) := h;
+
+type BalanceFactor :=
+  | --- Left children is higher.
+    LeanLeft
+  | --- Equal heights of children.
+    LeanNone
+  | --- Right children is higher.
+    LeanRight;
+
+{-# inline: true #-}
+diffFactor {A} : AVLTree A -> Int
+  | empty := 0
+  | (node _ _ left right) := intSubNat (height right) (height left);
+
+--- 𝒪(1). Computes the balance factor, i.e., the height of the right subtree
+--- minus the height of the left subtree.
+{-# inline: true #-}
+balanceFactor {A} (t : AVLTree A) : BalanceFactor :=
+  let
+    diff : Int := diffFactor t;
+  in if
+    | 0 < diff := LeanRight
+    | diff < 0 := LeanLeft
+    | else := LeanNone;
+
+--- 𝒪(1). Helper function for creating a node.
+mknode {A} (val : A) (l : AVLTree A) (r : AVLTree A) : AVLTree A :=
+  node val (1 + max (height l) (height r)) l r;
+
+--- 𝒪(1). Left rotation.
+rotateLeft {A} : AVLTree A -> AVLTree A
+  | (node x _ a (node z _ b c)) := mknode z (mknode x a b) c
+  | n := n;
+
+--- 𝒪(1). Right rotation.
+rotateRight {A} : AVLTree A -> AVLTree A
+  | (node z _ (node y _ x t3) t4) := mknode y x (mknode z t3 t4)
+  | n := n;
+
+--- 𝒪(1). Applies local rotations if needed.
+balance : {A : Type} -> AVLTree A -> AVLTree A
+  | empty := empty
+  | n@(node x h l r) :=
+    let
+      factor : BalanceFactor := balanceFactor n;
+    in case factor of
+         | LeanRight :=
+           case balanceFactor r of {
+             | LeanLeft := rotateLeft (mknode x l (rotateRight r))
+             | _ := rotateLeft n
+           }
+         | LeanLeft :=
+           case balanceFactor l of {
+             | LeanRight := rotateRight (mknode x (rotateLeft l) r)
+             | _ := rotateRight n
+           }
+         | LeanNone := n;
+
+--- 𝒪(log 𝓃). Lookup a member from the ;AVLTree; using a projection function.
+--- Ord A, Ord K and f must be compatible. i.e cmp_k (f a1) (f a2) == cmp_a a1 a2
+lookupWith {A K} {{o : Ord K}} (f : A -> K) (x : K) : AVLTree A -> Maybe A :=
+  let
+    {-# specialize-by: [o, f] #-}
+    go : AVLTree A -> Maybe A
+      | empty := nothing
+      | m@(node y h l r) :=
+        case Ord.cmp x (f y) of
+          | LT := go l
+          | GT := go r
+          | EQ := just y;
+  in go;
+
+--- 𝒪(log 𝓃). Queries whether an element is in an ;AVLTree;.
+{-# specialize: [1] #-}
+member? {A} {{Ord A}} (x : A) : AVLTree A -> Bool := lookupWith id x >> isJust;
+
+--- 𝒪(log 𝓃). Inserts an element into and ;AVLTree; using a function to
+--- deduplicate entries.
+---
+--- Assumption: Given a1 == a2 then f a1 a2 == a1 == a2
+--- where == comes from Ord a.
+insertWith {A} {{o : Ord A}} (f : A -> A -> A) (x : A) : AVLTree A -> AVLTree A :=
+  let
+    {-# specialize-by: [o, f] #-}
+    go : AVLTree A -> AVLTree A
+      | empty := mknode x empty empty
+      | m@(node y h l r) :=
+        case Ord.cmp x y of
+          | LT := balance (mknode y (go l) r)
+          | GT := balance (mknode y l (go r))
+          | EQ := node (f y x) h l r;
+  in go;
+
+--- 𝒪(log 𝓃). Inserts an element into and ;AVLTree;.
+insert {A} {{Ord A}} : A -> AVLTree A -> AVLTree A := insertWith (flip const);
+
+--- 𝒪(log 𝓃). Removes an element from an ;AVLTree; based on a projected comparison value.
+---
+--- Assumption Ord A and Ord B are compatible: Given a1 a2, A then (p a1 == p a2) == (a1 == a2)
+deleteWith {A B} {{o : Ord A}} {{po : Ord B}} (p : A -> B) (x : B) : AVLTree A -> AVLTree A :=
+  let
+    {-# specialize-by: [o, po, p] #-}
+    deleteMin : AVLTree A -> Maybe (Pair A (AVLTree A))
+      | empty := nothing
+      | (node v _ l r) :=
+        case deleteMin l of
+          | nothing := just (v, r)
+          | just (m, l') := just (m, mknode v l' r);
+    {-# specialize-by: [o, po, p] #-}
+    go : AVLTree A -> AVLTree A
+      | empty := empty
+      | (node y h l r) :=
+        case Ord.cmp x (p y) of
+          | LT := balance (mknode y (go l) r)
+          | GT := balance (mknode y l (go r))
+          | EQ :=
+            case l of
+              | empty := r
+              | _ :=
+                case deleteMin r of
+                  | nothing := l
+                  | just (minRight, r') := balance (mknode minRight l r');
+  in go;
+
+--- 𝒪(log 𝓃). Removes an element from an ;AVLTree;.
+delete {A} {{o : Ord A}} : A -> AVLTree A -> AVLTree A := deleteWith id;
+
+--- 𝒪(log 𝓃). Returns the minimum element of the ;AVLTree;.
+lookupMin {A} : AVLTree A -> Maybe A
+  | empty := nothing
+  | (node y _ empty empty) := just y
+  | (node _ _ empty r) := lookupMin r
+  | (node _ _ l _) := lookupMin l;
+
+--- 𝒪(log 𝓃). Returns the maximum element of the ;AVLTree;.
+lookupMax {A} : AVLTree A -> Maybe A
+  | empty := nothing
+  | (node y _ empty empty) := just y
+  | (node _ _ l empty) := lookupMax l
+  | (node _ _ _ r) := lookupMax r;
+
+--- 𝒪(𝒹 log 𝓃). Deletes d elements from an ;AVLTree;.
+{-# specialize: [1] #-}
+deleteMany {A} {{Ord A}} : List A -> AVLTree A -> AVLTree A := deleteManyWith id;
+
+--- 𝒪(𝒹 log 𝓃). Deletes d elements from an ;AVLTree; based on a projected comparison value.
+---
+--- Assumption Ord A and Ord B are compatible: Given a1 a2, A then (p a1 == p a2) == (a1 == a2)
+{-# specialize: [2] #-}
+deleteManyWith {A B} {{Ord A}} {{Ord B}} (p : A -> B) (d : List B) (t : AVLTree A) : AVLTree A :=
+  for (acc := t) (x in d)
+    deleteWith p x acc;
+
+--- 𝒪(𝓃). Checks the ;AVLTree; height invariant. I.e. that
+--- every two children do not differ on height by more than 1.
+isBalanced {A} : AVLTree A -> Bool
+  | empty := true
+  | n@(node _ _ l r) := isBalanced l && isBalanced r && abs (diffFactor n) <= 1;
+
+--- 𝒪(𝓃 log 𝓃). Create an ;AVLTree; from an unsorted ;List;.
+{-# specialize: [1] #-}
+fromList {A} {{Ord A}} (l : List A) : AVLTree A := for (acc := empty) (x in l) insert x acc;
+
+--- 𝒪(𝓃). Returns the number of elements of an ;AVLTree;.
+size {A} : AVLTree A -> Nat
+  | empty := 0
+  | (node _ _ l r) := 1 + size l + size r;
+
+--- 𝒪(𝓃). Returns the elements of an ;AVLTree; in ascending order.
+toList {A} : AVLTree A -> List A
+  | empty := nil
+  | (node x _ l r) := toList l ++ (x :: nil) ++ toList r;
+
+--- 𝒪(𝓃). Returns an ;AVLTree; containing elements that are members of both ;AVLTree;s.
+intersection {A} {{Ord A}} (s1 s2 : AVLTree A) : AVLTree A :=
+  toList s1 |> filter \ {x := member? x s2} |> fromList;
+
+--- 𝒪(𝓃). Returns an ;AVLTree; containing elements that are members of the first but not the second ;AVLTree;.
+difference {A} {{Ord A}} (s1 s2 : AVLTree A) : AVLTree A :=
+  toList s1 |> filter \ {x := not (member? x s2)} |> fromList;
+
+--- 𝒪(𝓃). Returns an ;AVLTree; containing elements that are members of either the first or second ;AVLTree;.
+union {A} {{Ord A}} (s1 s2 : AVLTree A) : AVLTree A := fromList (toList s1 ++ toList s2);
+
+--- 𝒪(𝓃). Formats the tree in a debug friendly format.
+prettyDebug {A} {{Show A}} : AVLTree A -> String :=
+  let
+    go : AVLTree A -> String
+      | empty := "_"
+      | n@(node v h l r) :=
+        "("
+          ++str go l
+          ++str " h"
+          ++str Show.show (diffFactor n)
+          ++str " "
+          ++str Show.show v
+          ++str " "
+          ++str go r
+          ++str ")";
+  in go;
+
+--- 𝒪(𝓃).
+toTree {A} : AVLTree A -> Maybe (Tree A)
+  | empty := nothing
+  | (node v _ l r) := just (Tree.node v (catMaybes (toTree l :: toTree r :: nil)));
+
+--- Returns the textual representation of an ;AVLTree;.
+pretty {A} {{Show A}} : AVLTree A -> String := toTree >> maybe "empty" Tree.treeToString;
+
+-- TODO: remove toList
+instance
+eqAVLTreeI {A} {{Eq A}} : Eq (AVLTree A) := mkEq ((==) on toList);
+
+-- TODO: remove toList
+instance
+ordAVLTreeI {A} {{Ord A}} : Ord (AVLTree A) := mkOrd (Ord.cmp on toList);
+
+{-# specialize: true, inline: case #-}
+instance
+polymorphicFoldableAVLTreeI : Polymorphic.Foldable AVLTree :=
+  Polymorphic.mkFoldable@{
+    for {A B} (f : B -> A -> B) (acc : B) : AVLTree A -> B :=
+      toList >> Polymorphic.Foldable.for f acc;
+    rfor {A B} (f : B → A → B) (acc : B) : AVLTree A -> B :=
+      toList >> Polymorphic.Foldable.rfor f acc
+  };
+
+{-# specialize: true, inline: true #-}
+instance
+foldableVLTreeI {A} : Foldable (AVLTree A) A := fromPolymorphicFoldable;
diff --git a/Stdlib/Data/Tree.juvix b/Stdlib/Data/Tree.juvix
new file mode 100644
index 00000000..c5e943f5
--- /dev/null
+++ b/Stdlib/Data/Tree.juvix
@@ -0,0 +1,31 @@
+--- N-Ary trees with pretty printing.
+module Stdlib.Data.Tree;
+
+import Stdlib.Data.List open;
+import Stdlib.Data.String open;
+import Stdlib.Trait.Show open;
+import Stdlib.Function open;
+
+--- A ;List; of trees.
+Forest (A : Type) : Type := List (Tree A);
+
+--- N-Ary tree.
+positive
+type Tree (A : Type) := node A (List (Tree A));
+
+shift (first other : String) (xs : List String) : List String :=
+  zipWith (++str) (first :: replicate (length xs) other) xs;
+
+terminating
+draw {A} {{Show A}} : Tree A -> List String
+  | (node v cs) := Show.show v :: drawForest cs;
+
+terminating
+drawForest {A} {{Show A}} : Forest A -> List String
+  | [] := []
+  | [h] := "|" :: shift "`- " "   " (draw h)
+  | (h :: hs) := "|" :: shift "+- " "|  " (draw h) ++ drawForest hs;
+
+treeToString {A} {{Show A}} : Tree A -> String := draw >> unlines;
+
+forestToString {A} {{Show A}} : Forest A -> String := drawForest >> unlines;
diff --git a/Stdlib/Data/UnbalancedSet.juvix b/Stdlib/Data/UnbalancedSet.juvix
new file mode 100644
index 00000000..db420594
--- /dev/null
+++ b/Stdlib/Data/UnbalancedSet.juvix
@@ -0,0 +1,46 @@
+module Stdlib.Data.UnbalancedSet;
+
+import Stdlib.Prelude open;
+
+import Stdlib.Trait.Ord as Ord open using {Ord; mkOrd; module Ord};
+
+import Stdlib.Data.BinaryTree as Tree;
+open Tree using {BinaryTree; leaf; node};
+
+type UnbalancedSet (A : Type) := unbalancedSet : Ord A -> BinaryTree A -> UnbalancedSet A;
+
+empty {A} {{o : Ord A}} : UnbalancedSet A := unbalancedSet o leaf;
+
+member? {A} (x : A) : UnbalancedSet A -> Bool
+  | (unbalancedSet o@(mkOrd cmp) t) :=
+    let
+      go : BinaryTree A -> Bool
+        | leaf := false
+        | (node l y r) :=
+          case cmp x y of
+            | Ord.LT := go l
+            | Ord.GT := go r
+            | Ord.EQ := true;
+    in go t;
+
+insert {A} (x : A) : UnbalancedSet A -> UnbalancedSet A
+  | (unbalancedSet o@(mkOrd cmp) t) :=
+    let
+      go : BinaryTree A -> BinaryTree A
+        | leaf := node leaf x leaf
+        | n@(node l y r) :=
+          case cmp x y of
+            | Ord.LT := node (go l) y r
+            | Ord.EQ := n
+            | Ord.GT := node l y (go r);
+    in unbalancedSet o (go t);
+
+length {A} : UnbalancedSet A -> Nat
+  | (unbalancedSet _ t) := Tree.length t;
+
+to-list {A} : UnbalancedSet A -> List A
+  | (unbalancedSet _ t) := Tree.to-list t;
+
+instance
+set-ordering {A} {{Ord A}} : Ord (UnbalancedSet A) :=
+  mkOrd λ {s1 s2 := Ord.cmp (to-list s1) (to-list s2)};
diff --git a/test/Package.juvix b/test/Package.juvix
index 8ce4b428..8b63758a 100644
--- a/test/Package.juvix
+++ b/test/Package.juvix
@@ -6,5 +6,8 @@ package : Package :=
   defaultPackage@?{
     name := "stdlib-test";
     dependencies :=
-      [path "../"; github "anoma" "juvix-quickcheck" "b398d3cd58f0a7fb9be24d57fc5b3d82f31de555"]
+      [ path "../"
+      ; github "anoma" "juvix-quickcheck" "b398d3cd58f0a7fb9be24d57fc5b3d82f31de555"
+      ; github "anoma" "juvix-test" "3103c41e055eb9018a851fd3688cd608cad8f55d"
+      ]
   };
diff --git a/test/Test.juvix b/test/Test.juvix
index 1fa4403f..49f8281c 100644
--- a/test/Test.juvix
+++ b/test/Test.juvix
@@ -9,7 +9,13 @@ import Data.String open;
 
 import Test.QuickCheckTest as QC;
 import Test.Arb as QC;
-import Test.StdlibTestExtra;
+
+import Test.JuvixUnit open;
+import Stdlib.System.IO open;
+import Test.AVL open using {suite as avlSuite};
+import Test.Map open using {suite as mapSuite};
+import Test.Queue open using {suite as queueSuite};
+import Test.UnbalancedSet open using {suite as unbalancedSetSuite};
 
 prop-reverseDoesNotChangeLength : List Int -> Bool
   | xs := length (reverse xs) == length xs;
@@ -282,46 +288,50 @@ resultMapOk : QC.Test := QC.mkTest "result: mapOk" prop-resultMapOk;
 
 main : IO :=
   readLn
-    \ {seed :=
-      let
-        seedNat := stringToNat seed;
-      in QC.runTestsIO
-          100
-          seedNat
-          [ partitionTest
-          ; reverseLengthTest
-          ; reverseReverseIdTest
-          ; splitAtRecombineTest
-          ; splitAtLengthTest
-          ; mergeSumLengthsTest
-          ; tailLengthOneLessTest
-          ; equalCompareToEqTest
-          ; zipTest
-          ; zipWithTest
-          ; snocTest
-          ; dropTest
-          ; sortTest "mergeSort" mergeSort
-          ; sortTest "quickSort" quickSort
-          ; transposeMatrixIdTest
-          ; transposeMatrixDimentionsTest
-          ; findFoundElementSatisfiesPredicate
-          ; findNonExistenceImpliesPredicateFalseForAll
-          ; findConsistentWithSplitAt
-          ; findOnEmptyListIsNothing
-          ; findWithAlwaysTrueIsJust
-          ; findWithAlwaysFalseIsNothing
-          ]
-        >>> QC.runTestsIO
-          100
-          seedNat
-          [ resultResultErrorApplication
-          ; resultResultOkApplication
-          ; resultIsError
-          ; resultIsOk
-          ; resultFromError
-          ; resultFromOk
-          ; resultResultToMaybe
-          ; resultMaybeToResult
-          ; resultMapError
-          ; resultMapOk
-          ]};
+      \ {seed :=
+        let
+          seedNat := stringToNat seed;
+        in QC.runTestsIO
+            100
+            seedNat
+            [ partitionTest
+            ; reverseLengthTest
+            ; reverseReverseIdTest
+            ; splitAtRecombineTest
+            ; splitAtLengthTest
+            ; mergeSumLengthsTest
+            ; tailLengthOneLessTest
+            ; equalCompareToEqTest
+            ; zipTest
+            ; zipWithTest
+            ; snocTest
+            ; dropTest
+            ; sortTest "mergeSort" mergeSort
+            ; sortTest "quickSort" quickSort
+            ; transposeMatrixIdTest
+            ; transposeMatrixDimentionsTest
+            ; findFoundElementSatisfiesPredicate
+            ; findNonExistenceImpliesPredicateFalseForAll
+            ; findConsistentWithSplitAt
+            ; findOnEmptyListIsNothing
+            ; findWithAlwaysTrueIsJust
+            ; findWithAlwaysFalseIsNothing
+            ]
+          >>> QC.runTestsIO
+            100
+            seedNat
+            [ resultResultErrorApplication
+            ; resultResultOkApplication
+            ; resultIsError
+            ; resultIsOk
+            ; resultFromError
+            ; resultFromOk
+            ; resultResultToMaybe
+            ; resultMaybeToResult
+            ; resultMapError
+            ; resultMapOk
+            ]}
+    >>> runTestSuite avlSuite
+    >>> runTestSuite mapSuite
+    >>> runTestSuite queueSuite
+    >>> runTestSuite unbalancedSetSuite;
diff --git a/test/Test/AVL.juvix b/test/Test/AVL.juvix
new file mode 100644
index 00000000..37c924b9
--- /dev/null
+++ b/test/Test/AVL.juvix
@@ -0,0 +1,96 @@
+module Test.AVL;
+
+import Test.JuvixUnit open;
+import Stdlib.Prelude open;
+
+import Stdlib.Data.Set.AVL open;
+
+type Box := mkBox {b : Nat};
+
+instance
+BoxOrdI : Ord Box := mkOrd (Ord.cmp on Box.b);
+
+--- Test for size and balance.
+mkTests {A} : TestDescr A -> List Test
+  | mkTestDescr@{testTitle; testLen; testSet} :=
+    let
+      mkTitle : String -> String
+        | m := testTitle ++str " " ++str m;
+      sizeMsg : String := "sizes do not match";
+      balanceMsg : String := "not balanced";
+    in [ testCase (mkTitle "size") (assertEqual sizeMsg (size testSet) testLen)
+       ; testCase (mkTitle "balanced") (assertTrue balanceMsg (isBalanced testSet))
+       ];
+
+type TestDescr (A : Type) :=
+  mkTestDescr {
+    testTitle : String;
+    testLen : Nat;
+    testSet : AVLTree A
+  };
+
+s1-tree : AVLTree Nat := fromList [1; 2; 8; 3; 3; 2; 9];
+
+s2-tree : AVLTree Nat := fromList [1; 3; 0; 4; 4; 8; 2];
+
+s1 : TestDescr Nat := mkTestDescr "s1" 5 s1-tree;
+
+s2 : TestDescr Nat := mkTestDescr "s2" 6 s2-tree;
+
+s2-delete : TestDescr Nat :=
+  mkTestDescr@{
+    testTitle := TestDescr.testTitle s2 ++str "-delete";
+    testLen := sub (TestDescr.testLen s2) 2;
+    testSet := deleteMany [1; 8] (TestDescr.testSet s2)
+  };
+
+s2-delete-with : TestDescr Box :=
+  mkTestDescr@{
+    testTitle := TestDescr.testTitle s2 ++str "-delete-with";
+    testLen := sub (TestDescr.testLen s2) 2;
+    testSet := deleteManyWith Box.b [1; 8] (TestDescr.testSet s2 |> toList |> map mkBox |> fromList)
+  };
+
+s3 : TestDescr Nat :=
+  mkTestDescr@{
+    testTitle := "s3";
+    testLen := 6;
+    testSet := fromList [5; 4; 3; 2; 1; 0]
+  };
+
+s4 : TestDescr Nat :=
+  mkTestDescr@{
+    testTitle := "s4";
+    testLen := 5;
+    testSet := fromList [1; 2; 3; 4; 5]
+  };
+
+tests : List Test :=
+  [ testCase "s1-member" (assertTrue "member? 3 s1" (member? 3 s1-tree))
+  ; testCase
+    "s1-s2-intersection"
+    (assertEqual
+      "intersection s1-tree s2-tree"
+      (intersection s1-tree s2-tree)
+      (fromList [1; 2; 3; 8]))
+  ; testCase
+    "s1-s2-difference"
+    (assertEqual "difference s1-tree s2-tree" (difference s1-tree s2-tree) (fromList [9]))
+  ; testCase
+    "s1-s2-union"
+    (assertEqual "union s1-tree s2-tree" (union s1-tree s2-tree) (fromList [0; 1; 2; 3; 4; 8; 9]))
+  ; testCase "for ascending iteration"
+    <| assertEqual "for iterates in ascending order" [1; 2; 3; 4]
+    <| for (acc := []) (k in fromList [3; 2; 4; 1])
+         snoc acc k
+  ; testCase "rfor ascending iteration"
+    <| assertEqual "rfor iterates in descending order" [4; 3; 2; 1]
+    <| rfor (acc := []) (k in fromList [3; 2; 4; 1])
+         snoc acc k
+  ]
+    ++ concatMap mkTests [s1; s2; s3; s4; s2-delete];
+
+suite : TestSuite := testSuite "AVL Set" tests;
+
+main : IO :=
+  printStringLn (pretty s1-tree) >>> printStringLn (prettyDebug s1-tree) >>> runTestSuite suite;
diff --git a/test/Test/Map.juvix b/test/Test/Map.juvix
new file mode 100644
index 00000000..ce4e134c
--- /dev/null
+++ b/test/Test/Map.juvix
@@ -0,0 +1,56 @@
+module Test.Map;
+
+import Juvix.Builtin.V1 open;
+import Stdlib.System.IO open;
+import Stdlib.Data.Pair open;
+import Stdlib.Data.List open;
+import Stdlib.Function open;
+import Test.JuvixUnit open;
+
+import Stdlib.Data.Map as Map;
+open Map using {Map};
+
+tests : List Test :=
+  let
+    m : Map Nat String := Map.insert 2 "two" (Map.insert 1 "one" Map.empty);
+    m2 : Map Nat Nat := Map.insert 3 4 (Map.insert 1 2 Map.empty);
+    assertEqListPair : List (Pair Nat Nat) -> List (Pair Nat Nat) -> Assertion
+      | actual expected := assertEqual "lists are not equal" (quickSort actual) expected;
+  in [ testCase
+       "Map.lookup missing key"
+       (assertNothing (const "found a key expected to be missing") (Map.lookup 10 m))
+     ; testCase
+       "Map.lookup available key"
+       (assertJust "could not find expected key" (Map.lookup 2 m))
+     ; testCase
+       "Map.delete exiting key"
+       (assertNothing (const "expected deleted key to be missing") (Map.delete 2 m |> Map.lookup 2))
+     ; testCase
+       "Map.delete missing key"
+       (assertEqual "expected maps to be equal" m (Map.delete 100 m))
+     ; testCase
+       "Map.length computes the number of keys in the map"
+       (assertEqual "expected length 2" (Map.size m) 2)
+     ; testCase
+       "Map.toList computes the expected members"
+       (assertEqListPair (Map.toList m2) [1, 2; 3, 4])
+     ; testCase
+       "Map.insert-with replaces duplicates using merge function"
+       (assertEqListPair (Map.toList (Map.insertWith (+) 1 3 m2)) [1, 5; 3, 4])
+     ; testCase
+       "Map.fromListWith de-duplicates using merge function"
+       (assertEqListPair (Map.toList (Map.fromListWith (+) [1, 1; 1, 2])) [1, 3])
+     ; testCase
+       "Map.fromList can be used to create the empty Map"
+       (assertEqListPair (Map.toList (Map.fromList nil)) (nil))
+     ; testCase
+       "Map.fromList overwrites duplicates"
+       (assertEqListPair (Map.toList (Map.fromList [1, 1; 1, 2])) [1, 2])
+     ; testCase
+       "Map.fromList distinct keys"
+       (assertEqListPair (Map.toList (Map.fromList [1, 1; 2, 2])) [1, 1; 2, 2])
+     ];
+
+suite : TestSuite := testSuite "Map" tests;
+
+main : IO := runTestSuite suite;
diff --git a/test/Test/Queue.juvix b/test/Test/Queue.juvix
new file mode 100644
index 00000000..c85de1e0
--- /dev/null
+++ b/test/Test/Queue.juvix
@@ -0,0 +1,44 @@
+module Test.Queue;
+
+import Juvix.Builtin.V1 open;
+import Stdlib.System.IO.Base open;
+import Stdlib.Function open;
+import Stdlib.Data.Pair open;
+import Test.JuvixUnit open;
+
+import Stdlib.Data.Queue open;
+
+q : Queue Nat := empty;
+
+q1 : Queue Nat := push 1 q;
+
+q2 : Queue Nat := push 2 q1;
+
+q3 : Queue Nat := push 3 q2;
+
+q4 : Queue Nat := push 4 q3;
+
+tests : List Test :=
+  let
+    checkWithList : Queue Nat -> List Nat -> Assertion
+      | q q' := assertEqual "Queue should be equal" q (fromList q');
+  in [ testCase "Queue.empty should be empty" (checkWithList q [])
+     ; testCase "Queue.push should add an element" (checkWithList q1 [1])
+     ; testCase "Queue.push first element should be first pushed" (checkWithList q2 [1; 2])
+     ; testCase
+       "Queue.head should return first element"
+       (assertEqual "head of queue q3" (head q3) (just 1))
+     ; testCase
+       "Queue.fromList composes with toList should be the identity"
+       (assertEqual "fromList . toList should be the identity" (toList >> fromList <| q3) q3)
+     ; testCase
+       "Queue.pop should remove first element"
+       (assertEqual "pop of queue q3" (pop q3) (just (1, fromList [2; 3])))
+     ; testCase
+       "Queue.tail should return queue without first element"
+       (assertEqual "tail of queue q3" (tail q3) ((fromList >> just) [2; 3]))
+     ];
+
+suite : TestSuite := testSuite "Queue" tests;
+
+main : IO := runTestSuite suite;
diff --git a/test/Test/StdlibTestExtra.juvix b/test/Test/StdlibTestExtra.juvix
deleted file mode 100644
index 5f251ae2..00000000
--- a/test/Test/StdlibTestExtra.juvix
+++ /dev/null
@@ -1,11 +0,0 @@
-module Test.StdlibTestExtra;
-
-import Stdlib.Prelude open;
-
-instance
-eitherShow {A B} {{Show A}} {{Show B}} : Show (Result A B) :=
-  mkShow@{
-    show : Result A B -> String
-      | (error x) := "Error (" ++str Show.show x ++str ")"
-      | (ok x) := "Ok (" ++str Show.show x ++str ")"
-  };
diff --git a/test/Test/UnbalancedSet.juvix b/test/Test/UnbalancedSet.juvix
new file mode 100644
index 00000000..53c62cfe
--- /dev/null
+++ b/test/Test/UnbalancedSet.juvix
@@ -0,0 +1,32 @@
+module Test.UnbalancedSet;
+
+import Juvix.Builtin.V1 open;
+import Stdlib.Data.List open using {quickSort};
+import Stdlib.System.IO.Base open;
+import Test.JuvixUnit open;
+
+import Stdlib.Data.UnbalancedSet as Set;
+open Set using {UnbalancedSet};
+
+tests : List Test :=
+  let
+    s : UnbalancedSet Nat := Set.insert 1 (Set.insert 3 (Set.insert 2 (Set.insert 1 Set.empty)));
+    setInSet : UnbalancedSet (UnbalancedSet Nat) := Set.insert s Set.empty;
+  in [ testCase
+       "Set.length computes the expected size"
+       (assertEqual "unexpected size" (Set.length s) 3)
+     ; testCase
+       "Set.to-list computes the expected members"
+       (assertEqual "unexpected memebrs" (quickSort (Set.to-list s)) [1; 2; 3])
+     ; testCase
+       "Set.member? computes true for expected member"
+       (assertTrue "expected member is not present" (Set.member? 1 s))
+     ; testCase
+       "Set.member? computes false for unexpected member"
+       (assertFalse "unexpected member is present" (Set.member? 0 s))
+     ; testCase "setInSet has length 1" (assertEqual "unexpected size" (Set.length setInSet) 1)
+     ];
+
+suite : TestSuite := testSuite "UnbalancedSet" tests;
+
+main : IO := runTestSuite suite;
diff --git a/test/juvix.lock.yaml b/test/juvix.lock.yaml
index 886cfe41..b565a8e3 100644
--- a/test/juvix.lock.yaml
+++ b/test/juvix.lock.yaml
@@ -1,8 +1,8 @@
-# This file was autogenerated by Juvix version 0.6.5.
+# This file was autogenerated by Juvix version 0.6.6.
 # Do not edit this file manually.
 
 version: 2
-checksum: d7a0456ff0284c1898071b9775fbcf63ba5d9d7257e9583b9573581c16f0ec89
+checksum: 05003064be8ff630775c22735af69a82ddd4ac04fdd3ad6aa0c3f01867777225
 dependencies:
 - path: ../
   dependencies: []
@@ -16,3 +16,13 @@ dependencies:
       ref: af72f25057217619a03b7a5114000d02d0abed31
       url: https://github.com/anoma/juvix-stdlib
     dependencies: []
+- git:
+    name: anoma_juvix-test
+    ref: 3103c41e055eb9018a851fd3688cd608cad8f55d
+    url: https://github.com/anoma/juvix-test
+  dependencies:
+  - git:
+      name: anoma_juvix-stdlib
+      ref: 615a02c8107076ca9661c5234d41792be91a5104
+      url: https://github.com/anoma/juvix-stdlib
+    dependencies: []