From 0095dffdbace1008176237e7b865efd4e61505fd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Sun, 29 Sep 2024 23:21:55 +0200
Subject: [PATCH 01/22] Add dictionary example

---
 example/dictionary.sw | 75 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 75 insertions(+)
 create mode 100644 example/dictionary.sw

diff --git a/example/dictionary.sw b/example/dictionary.sw
new file mode 100644
index 000000000..d3bb4f692
--- /dev/null
+++ b/example/dictionary.sw
@@ -0,0 +1,75 @@
+tydef Dict k v = rec b. Unit + (k * v * b * b) end
+
+def emptyD : Dict k v = inl () end
+
+def isEmptyD : Dict k v -> Bool = \d. case d (\_. true) (\_. false) end
+
+def containsD : k -> Dict k v -> Bool = \x.\d.
+  case d (\_. false) (\n.
+    let k = fst n in
+    if (x == k) { true } {
+        let vbb = snd n in
+        let v = fst vbb in
+        let bb = snd vbb in
+        if (x < k) {
+            containsD x (fst bb)
+        } {
+            containsD x (snd bb)
+        }
+    }
+  )
+end
+
+def insertD : k -> v -> Dict k v -> Dict k v = \x.\y.\d.
+  case d (\_. inr (x,y,inl (), inl ())) (\n.
+    let k = fst n in
+    let vbb = snd n in
+    let v = fst vbb in
+    let bb = snd vbb in
+    if (x == k) { inr (x,y,bb) } {
+        if (x < k) {
+            inr (k, v, insertD x y (fst bb), snd bb)
+        } {
+            inr (k, v, fst bb, insertD x y (snd bb))
+        }
+    }
+  )
+end
+
+// helper function to remove the leftmost element from right subtree
+def pullLeft: k * v * (Dict k v) * (Dict k v) -> ((k * v) * (Dict k v)) = \n.
+  let k = fst n in
+  let vbb = snd n in
+  let v = fst vbb in
+  let bb = snd vbb in
+  case (fst bb) (\_. ((k,v),snd bb)) (\lt. 
+    let res = pullLeft lt in
+    let rkv = fst res in
+    let rd = snd res in
+    (rkv, inr (k,v,rd, snd bb))
+  )
+end
+
+def deleteD : k -> Dict k v -> Dict k v = \x.\d.
+  case d (\_. inl ()) (\n.
+    let k = fst n in
+    let vbb = snd n in
+    let v = fst vbb in
+    let bb = snd vbb in
+    if (x == k) {
+        case (fst bb) (\_. snd bb) (\lt.
+            case (snd bb) (\_. fst bb) (\rt.
+                let r_kvd = pullLeft rt in
+                let r_kv = fst r_kvd in
+                inr (fst r_kv, snd r_kv, inr lt, snd r_kvd)
+            )
+        )
+    } {
+        if (x < k) {
+            inr (k, v, deleteD x (fst bb), snd bb)
+        } {
+            inr (k, v, fst bb, deleteD x (snd bb))
+        }
+    }
+  )
+end

From 05d22a98038dd92ee5cd2a21995ff584d6e5dbee Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Sun, 29 Sep 2024 23:44:23 +0200
Subject: [PATCH 02/22] Rewrite dictionary map with records

---
 example/dictionary.sw | 60 +++++++++++++++----------------------------
 1 file changed, 21 insertions(+), 39 deletions(-)

diff --git a/example/dictionary.sw b/example/dictionary.sw
index d3bb4f692..c6b939e01 100644
--- a/example/dictionary.sw
+++ b/example/dictionary.sw
@@ -1,74 +1,56 @@
-tydef Dict k v = rec b. Unit + (k * v * b * b) end
+tydef Dict k v = rec b. Unit + [k: k, v: v, l: b, r: b] end
 
 def emptyD : Dict k v = inl () end
 
-def isEmptyD : Dict k v -> Bool = \d. case d (\_. true) (\_. false) end
+def isEmptyD : Dict k v -> Bool = \d. d == emptyD end
 
 def containsD : k -> Dict k v -> Bool = \x.\d.
   case d (\_. false) (\n.
-    let k = fst n in
-    if (x == k) { true } {
-        let vbb = snd n in
-        let v = fst vbb in
-        let bb = snd vbb in
-        if (x < k) {
-            containsD x (fst bb)
+    if (x == n.k) { true } {
+        if (x < n.k) {
+            containsD x n.l
         } {
-            containsD x (snd bb)
+            containsD x n.r
         }
     }
   )
 end
 
 def insertD : k -> v -> Dict k v -> Dict k v = \x.\y.\d.
-  case d (\_. inr (x,y,inl (), inl ())) (\n.
-    let k = fst n in
-    let vbb = snd n in
-    let v = fst vbb in
-    let bb = snd vbb in
-    if (x == k) { inr (x,y,bb) } {
-        if (x < k) {
-            inr (k, v, insertD x y (fst bb), snd bb)
+  case d (\_. inr [k=x, v=y, l=inl (), r=inl ()]) (\n.
+    if (x == n.k) { inr [k=x, v=y, l=n.l, r=n.r] } {
+        if (x < n.k) {
+            inr [k=n.k, v=n.v, l=insertD x y n.l, r=n.r]
         } {
-            inr (k, v, fst bb, insertD x y (snd bb))
+            inr [k=n.k, v=n.v, l=n.l, r=insertD x y n.r]
         }
     }
   )
 end
 
 // helper function to remove the leftmost element from right subtree
-def pullLeft: k * v * (Dict k v) * (Dict k v) -> ((k * v) * (Dict k v)) = \n.
-  let k = fst n in
-  let vbb = snd n in
-  let v = fst vbb in
-  let bb = snd vbb in
-  case (fst bb) (\_. ((k,v),snd bb)) (\lt. 
+def pullLeft: [k: k, v: v, l: Dict k v, r: Dict k v] -> ((k * v) * (Dict k v)) = \n.
+  case (n.l) (\_. ((n.k,n.v),n.r)) (\lt. 
     let res = pullLeft lt in
-    let rkv = fst res in
-    let rd = snd res in
-    (rkv, inr (k,v,rd, snd bb))
+    (fst res, inr [k=n.k, v=n.v, l=snd res, r=n.r])
   )
 end
 
 def deleteD : k -> Dict k v -> Dict k v = \x.\d.
   case d (\_. inl ()) (\n.
-    let k = fst n in
-    let vbb = snd n in
-    let v = fst vbb in
-    let bb = snd vbb in
-    if (x == k) {
-        case (fst bb) (\_. snd bb) (\lt.
-            case (snd bb) (\_. fst bb) (\rt.
+    if (x == n.k) {
+        case (n.l) (\_. n.r) (\lt.
+            case (n.r) (\_. inl ()) (\rt.
                 let r_kvd = pullLeft rt in
                 let r_kv = fst r_kvd in
-                inr (fst r_kv, snd r_kv, inr lt, snd r_kvd)
+                inr [k=fst r_kv, v=snd r_kv, l=inr lt, r=snd r_kvd]
             )
         )
     } {
-        if (x < k) {
-            inr (k, v, deleteD x (fst bb), snd bb)
+        if (x < n.k) {
+            inr [k=n.k, v=n.v, l=deleteD x n.l, r=n.r]
         } {
-            inr (k, v, fst bb, deleteD x (snd bb))
+            inr [k=n.k, v=n.v, l=n.l, r=deleteD x n.r]
         }
     }
   )

From 8af0a0f6ce324dff568a6c55204a4a3a98db839f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Sat, 12 Oct 2024 20:06:53 +0200
Subject: [PATCH 03/22] wip

---
 example/dictionary.sw | 108 ++++++++++++++++++++++++++++++++++++------
 1 file changed, 93 insertions(+), 15 deletions(-)

diff --git a/example/dictionary.sw b/example/dictionary.sw
index c6b939e01..bcacd4819 100644
--- a/example/dictionary.sw
+++ b/example/dictionary.sw
@@ -1,42 +1,119 @@
-tydef Dict k v = rec b. Unit + [k: k, v: v, l: b, r: b] end
+tydef Color = Bool end
+def black = false end
+def red = true end
+// TODO: s/\((.*\.c) == red\)/$1.red/g
 
-def emptyD : Dict k v = inl () end
+tydef RBTree k v = rec b. Unit + [c: Color, k: k, v: v, l: b, r: b] end
+tydef RBNode k v = rec n. [c: Color, k: k, v: v, l: Unit + n, r: Unit + n] end
 
-def isEmptyD : Dict k v -> Bool = \d. d == emptyD end
+def emptyT : RBTree k v = inl () end
 
-def containsD : k -> Dict k v -> Bool = \x.\d.
-  case d (\_. false) (\n.
-    if (x == n.k) { true } {
+def isEmptyT : RBTree k v -> Bool = \d. d == emptyT end
+
+def getT : k -> RBTree k v -> Unit + v = \x.\t.
+  case t (\_. inl ()) (\n.
+    if (x == n.k) { inr n.v } {
         if (x < n.k) {
-            containsD x n.l
+            getT x n.l
         } {
-            containsD x n.r
+            getT x n.r
         }
     }
   )
 end
 
-def insertD : k -> v -> Dict k v -> Dict k v = \x.\y.\d.
-  case d (\_. inr [k=x, v=y, l=inl (), r=inl ()]) (\n.
-    if (x == n.k) { inr [k=x, v=y, l=n.l, r=n.r] } {
+def containsT : k -> RBTree k v -> Bool = \x.\t. case (getT x t) (\_. false) (\_. true) end
+
+/*
+balance B (T R (T R a x0 b) x1 c) x2 d = T R (T B a x0 b) x1 (T B c x2 d) -- case 1
+balance B (T R a x0 (T R b x1 c)) x2 d = T R (T B a x0 b) x1 (T B c x2 d) -- case 2
+balance B a x0 (T R (T R b x1 c) x2 d) = T R (T B a x0 b) x1 (T B c x2 d) -- case 3
+balance B a x0 (T R b x1 (T R c x2 d)) = T R (T B a x0 b) x1 (T B c x2 d) -- case 4
+balance color a x b = T color a x b -- case 5
+*/
+def balanceT : Color -> k -> v -> RBTree k v -> RBTree k v -> RBTree k v = \c.\x.\y.\l.\r.
+  let balanced : k->v->RBTree k v->RBTree k v  ->  k->v  ->  k->v->RBTree k v ->RBTree k v  ->  RBTree k v
+    = \x0.\y0.\a.\b. \x1.\y1. \x2.\y2.\c.\d.
+    inr [c=red, k=x1, v=y1, l=inr [c=black, k=x0, v=y0, l=a, r=b], r=inr [c=black, k=x2, v=y2, l=c, r=d]]
+  in
+  let case5 =
+    inr [c=c, k=x, v=y, l=l, r=r]
+  in
+  let balanceRR : RBNode k v -> RBTree k v = \rn.
+    undefined
+  in
+  let balanceRL : RBNode k v -> RBTree k v = \rn.
+    undefined
+  in
+  let balanceR : RBTree k v =
+    undefined
+  in
+  let balanceLR : RBNode k v -> RBTree k v = \ln.
+    case ln.r (\_. balanceR) (\lrn.
+      if (lrn.c == red) {
+        balanced lln.k lln.v lln.l lln.r  ln.k ln.v  ln.r n.x n.r
+      } {
+        balanceR
+      }
+    )  in
+  let balanceLL : RBNode k v -> RBTree k v = \ln.
+    case ln.l (\_. balanceLR ln) (\lln.
+      if (lln.c == red) {
+        balanced lln.k lln.v lln.l lln.r  ln.k ln.v  ln.r n.x n.r
+      } {
+        balanceLR ln
+      }
+    )
+  in
+  let balanceL : RBTree k v =
+    case l (\_.
+      balanceR
+    ) (\ln.
+      if (ln.c == red) {
+        balanceLL ln
+      } {
+        balanceR
+      }
+    ) 
+  in
+  if (c == red) {
+    case5
+  } {
+    balanceL
+  }
+end
+
+def insertT : k -> v -> RBTree k v -> RBTree k v = \x.\y.\t.
+  let ins : k -> v -> RBTree k v -> RBTree k v  = \x.\y.\t. case t
+    (\_.
+      inr [c=red, k=x, v=y, l=inl (), r=inl ()]
+    ) (\n.
+      if (x == n.k) { inr [c=n.c, k=x, v=y, l=n.l, r=n.r] } {
         if (x < n.k) {
-            inr [k=n.k, v=n.v, l=insertD x y n.l, r=n.r]
+            inr [c=n.c, k=n.k, v=n.v, l=insertD x y n.l, r=n.r]
         } {
-            inr [k=n.k, v=n.v, l=n.l, r=insertD x y n.r]
+            inr [c=n.c,k=n.k, v=n.v, l=n.l, r=insertD x y n.r]
         }
     }
   )
+  in let makeBlack : RBTree k v -> RBTree k v = \t. case t (\_.
+        fail "makeBlack must always be called on nonempty"
+      ) (\n.
+        inr [c=black, k=n.k, v=n.v, l=n.l, r=n.r]
+      )
+  in makeBlack $ ins x y t
 end
 
+/*
 // helper function to remove the leftmost element from right subtree
-def pullLeft: [k: k, v: v, l: Dict k v, r: Dict k v] -> ((k * v) * (Dict k v)) = \n.
+def pullLeft: [k: k, v: v, l: RBTree k v, r: RBTree k v] -> ((k * v) * (RBTree k v)) = \n.
   case (n.l) (\_. ((n.k,n.v),n.r)) (\lt. 
     let res = pullLeft lt in
     (fst res, inr [k=n.k, v=n.v, l=snd res, r=n.r])
   )
 end
 
-def deleteD : k -> Dict k v -> Dict k v = \x.\d.
+def deleteD : k -> RBTree k v -> RBTree k v = \x.\d.
   case d (\_. inl ()) (\n.
     if (x == n.k) {
         case (n.l) (\_. n.r) (\lt.
@@ -55,3 +132,4 @@ def deleteD : k -> Dict k v -> Dict k v = \x.\d.
     }
   )
 end
+*/
\ No newline at end of file

From 892c238eeffee207c76d7dde51522536cb0169cf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Sun, 13 Oct 2024 12:16:21 +0200
Subject: [PATCH 04/22] finish balance function

---
 example/dictionary.sw | 161 ++++++++++++++++++++++++++++++------------
 1 file changed, 115 insertions(+), 46 deletions(-)

diff --git a/example/dictionary.sw b/example/dictionary.sw
index bcacd4819..b473e5ba7 100644
--- a/example/dictionary.sw
+++ b/example/dictionary.sw
@@ -22,64 +22,80 @@ def getT : k -> RBTree k v -> Unit + v = \x.\t.
   )
 end
 
-def containsT : k -> RBTree k v -> Bool = \x.\t. case (getT x t) (\_. false) (\_. true) end
+def containsT : k -> RBTree k v -> Bool = \x.\t. getT x t != inl () end
 
 /*
-balance B (T R (T R a x0 b) x1 c) x2 d = T R (T B a x0 b) x1 (T B c x2 d) -- case 1
-balance B (T R a x0 (T R b x1 c)) x2 d = T R (T B a x0 b) x1 (T B c x2 d) -- case 2
-balance B a x0 (T R (T R b x1 c) x2 d) = T R (T B a x0 b) x1 (T B c x2 d) -- case 3
-balance B a x0 (T R b x1 (T R c x2 d)) = T R (T B a x0 b) x1 (T B c x2 d) -- case 4
+balance B (T R (T R a x0 b) x1 c) x2 d = T R (T B a x0 b) x1 (T B c x2 d) -- case 1: LL red
+balance B (T R a x0 (T R b x1 c)) x2 d = T R (T B a x0 b) x1 (T B c x2 d) -- case 2: LR red
+balance B a x0 (T R (T R b x1 c) x2 d) = T R (T B a x0 b) x1 (T B c x2 d) -- case 3: RL red
+balance B a x0 (T R b x1 (T R c x2 d)) = T R (T B a x0 b) x1 (T B c x2 d) -- case 4: RR red
 balance color a x b = T color a x b -- case 5
 */
-def balanceT : Color -> k -> v -> RBTree k v -> RBTree k v -> RBTree k v = \c.\x.\y.\l.\r.
-  let balanced : k->v->RBTree k v->RBTree k v  ->  k->v  ->  k->v->RBTree k v ->RBTree k v  ->  RBTree k v
+def balanceT : RBNode k v -> RBTree k v = \t.
+  let balanced : k -> v -> RBTree k v -> RBTree k v
+              -> k -> v
+              -> k -> v -> RBTree k v -> RBTree k v
+              -> RBTree k v
     = \x0.\y0.\a.\b. \x1.\y1. \x2.\y2.\c.\d.
     inr [c=red, k=x1, v=y1, l=inr [c=black, k=x0, v=y0, l=a, r=b], r=inr [c=black, k=x2, v=y2, l=c, r=d]]
-  in
-  let case5 =
-    inr [c=c, k=x, v=y, l=l, r=r]
-  in
-  let balanceRR : RBNode k v -> RBTree k v = \rn.
-    undefined
-  in
-  let balanceRL : RBNode k v -> RBTree k v = \rn.
-    undefined
-  in
-  let balanceR : RBTree k v =
-    undefined
-  in
-  let balanceLR : RBNode k v -> RBTree k v = \ln.
-    case ln.r (\_. balanceR) (\lrn.
+  in let case5 : RBNode k v -> RBTree k v =
+    inr  // just id - TODO: inline?
+  in let balanceRR : RBNode k v -> RBNode k v -> RBTree k v = \t.\rn.
+    case rn.r (\_. case5 t) (\rrn.
+      if (rrn.c == red) {
+        balanced t.k t.v t.l rn.l  rn.k rn.v  rrn.k rrn.v rrn.l rrn.r
+      } {
+        case5 t
+      }
+    )
+  in let balanceRL : RBNode k v -> RBNode k v -> RBTree k v = \t.\rn.
+    case rn.l (\_. balanceRR t rn) (\rln.
+      if (rln.c == red) {
+        balanced t.k t.v t.l rln.r  rln.k rln.v  rn.k rn.v rln.r rn.r
+      } {
+        balanceRR t rn
+      }
+    )
+  in let balanceR : RBNode k v -> RBTree k v = \t.
+    case t.r (\_.
+      case5 t
+    ) (\lr.
+      if (lr.c == red) {
+        balanceRL t lr
+      } {
+        case5 t
+      }
+    )
+  in let balanceLR : RBNode k v -> RBNode k v -> RBTree k v = \t.\ln.
+    case ln.r (\_. balanceR t) (\lrn.
       if (lrn.c == red) {
-        balanced lln.k lln.v lln.l lln.r  ln.k ln.v  ln.r n.x n.r
+        balanced ln.k ln.v ln.l lrn.l  lrn.k lrn.v  t.k t.v lrn.l t.r
       } {
-        balanceR
+        balanceR t
       }
-    )  in
-  let balanceLL : RBNode k v -> RBTree k v = \ln.
-    case ln.l (\_. balanceLR ln) (\lln.
+    )
+  in let balanceLL : RBNode k v -> RBNode k v -> RBTree k v = \t.\ln.
+    case ln.l (\_. balanceLR t ln) (\lln.
       if (lln.c == red) {
-        balanced lln.k lln.v lln.l lln.r  ln.k ln.v  ln.r n.x n.r
+        balanced lln.k lln.v lln.l lln.r  ln.k ln.v  t.k t.v ln.r t.r
       } {
-        balanceLR ln
+        balanceLR t ln
       }
     )
-  in
-  let balanceL : RBTree k v =
-    case l (\_.
-      balanceR
+  in let balanceL : RBNode k v -> RBTree k v = \t.
+    case t.l (\_.
+      balanceR t
     ) (\ln.
       if (ln.c == red) {
-        balanceLL ln
+        balanceLL t ln
       } {
-        balanceR
+        balanceR t
       }
-    ) 
-  in
-  if (c == red) {
-    case5
+    )
+  in if (t.c == red) {
+    case5 t
   } {
-    balanceL
+    balanceL t
   }
 end
 
@@ -90,14 +106,14 @@ def insertT : k -> v -> RBTree k v -> RBTree k v = \x.\y.\t.
     ) (\n.
       if (x == n.k) { inr [c=n.c, k=x, v=y, l=n.l, r=n.r] } {
         if (x < n.k) {
-            inr [c=n.c, k=n.k, v=n.v, l=insertD x y n.l, r=n.r]
+            balanceT [c=n.c, k=n.k, v=n.v, l=ins x y n.l, r=n.r]
         } {
-            inr [c=n.c,k=n.k, v=n.v, l=n.l, r=insertD x y n.r]
+            balanceT [c=n.c,k=n.k, v=n.v, l=n.l, r=ins x y n.r]
         }
-    }
-  )
+      }
+    )
   in let makeBlack : RBTree k v -> RBTree k v = \t. case t (\_.
-        fail "makeBlack must always be called on nonempty"
+        fail "makeBlack will always be called on nonempty"
       ) (\n.
         inr [c=black, k=n.k, v=n.v, l=n.l, r=n.r]
       )
@@ -132,4 +148,57 @@ def deleteD : k -> RBTree k v -> RBTree k v = \x.\d.
     }
   )
 end
-*/
\ No newline at end of file
+*/
+
+/*******************************************************************/
+/*                           UNIT TESTS                            */
+/*******************************************************************/
+def indent = \i. if (i <= 0) {""} {"  " ++ indent (i - 1)} end
+
+def assert = \i. \b. \m. if b {log $ indent i ++ "OK: " ++ m} {log "FAIL:"; fail m} end
+
+def assert_eq 
+  = \i. \exp. \act. \m.
+  if (exp == act) {log $ indent i ++ "OK: " ++ m} {
+    log (indent i ++ "FAIL: expected " ++ format exp ++ " actual " ++ format act);
+    fail m
+  }
+end
+
+def group = \i. \m. \tests.
+  log $ indent i ++ "START " ++ m ++ ":";
+  tests $ i + 1;
+  log $ indent i ++ "END " ++ m ++ ":";
+end
+
+def test_empty: Int -> Cmd Unit = \i.
+  group i "EMPTY TESTS" (\i.
+    assert i (isEmptyT emptyT) "empty tree should be empty";
+    assert_eq i (inl ()) (getT 0 $ emptyT) "no element should be present in an empty tree";
+    assert i (not $ containsT 0 $ emptyT) "empty tree should not contain any elements";
+  )
+end
+
+def test_insert: Int -> Cmd Unit = \i.
+  group i "INSERT TESTS" (\i.
+    group i "test {0: 1}" (\i.
+      let tree0 = insertT 0 1 emptyT in
+      assert i (not $ isEmptyT tree0) "nonempty tree should not be empty";
+      assert_eq i (inr 1) (getT 0 $ tree0) "one element should be present in a one element tree";
+      assert i (containsT 0 $ tree0) "one element tree should contain that elements";
+      assert i (not $ containsT 1 $ tree0) "one element tree should contain only that elements";
+    );
+    group i "test {0: 1, 2: 3}" (\i.
+      let tree02 = insertT 2 3 $ insertT 0 1 emptyT in
+      assert_eq i (inr 1) (getT 0 $ tree02) "get 0 {0: 1, 2: 3} == 1";
+      assert_eq i (inr 3) (getT 2 $ tree02) "get 2 {0: 1, 2: 3} == 3";
+    );
+  );
+end
+
+def test_tree: Cmd Unit =
+  group 0 "TREE TESTS" (\i.
+    test_empty i;
+    test_insert i;
+  )
+end
\ No newline at end of file

From 47c9995f034495eceea7d89cc71f52e3ef2d77c3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Sun, 13 Oct 2024 12:44:56 +0200
Subject: [PATCH 05/22] add inorder

---
 example/dictionary.sw | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/example/dictionary.sw b/example/dictionary.sw
index b473e5ba7..03ee169e7 100644
--- a/example/dictionary.sw
+++ b/example/dictionary.sw
@@ -24,6 +24,27 @@ end
 
 def containsT : k -> RBTree k v -> Bool = \x.\t. getT x t != inl () end
 
+tydef List a = rec l. Unit + (a * l) end
+
+def emptyL : List a = inl () end
+def insertL : a -> List a -> List a = \a.\l. inr (a, l) end
+def pureL : a -> List a = \a. insertL a emptyL end
+
+def appendL : List a -> List a -> List a = \l.\r.
+  case l (\_. r) (\ln. inr (fst ln, appendL (snd ln) r))
+end 
+
+def formatL : List a -> Text = \l.
+ let f : List a -> Text = \l. case l (\_. "]") (\n. ", " ++ format (fst n) ++ f (snd n))
+ in case l (\_. "[]") (\n. "[" ++ format (fst n) ++ f (snd n))
+end
+
+def inorder : RBTree k v -> List (k * v) = \t.
+  case t (\_. inl ()) (\n.
+    appendL (inorder n.l) (appendL (pureL (n.k, n.v)) $ inorder n.r)
+  )
+end
+
 /*
 balance B (T R (T R a x0 b) x1 c) x2 d = T R (T B a x0 b) x1 (T B c x2 d) -- case 1: LL red
 balance B (T R a x0 (T R b x1 c)) x2 d = T R (T B a x0 b) x1 (T B c x2 d) -- case 2: LR red

From 81e5d4f84db770e79193f6ef8e24fd92247059cc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Sun, 13 Oct 2024 13:17:17 +0200
Subject: [PATCH 06/22] use projection to get Set and Dict

---
 example/dictionary.sw | 124 +++++++++++++++++++++++++-----------------
 1 file changed, 74 insertions(+), 50 deletions(-)

diff --git a/example/dictionary.sw b/example/dictionary.sw
index 03ee169e7..7e8fdf530 100644
--- a/example/dictionary.sw
+++ b/example/dictionary.sw
@@ -3,26 +3,29 @@ def black = false end
 def red = true end
 // TODO: s/\((.*\.c) == red\)/$1.red/g
 
-tydef RBTree k v = rec b. Unit + [c: Color, k: k, v: v, l: b, r: b] end
-tydef RBNode k v = rec n. [c: Color, k: k, v: v, l: Unit + n, r: Unit + n] end
+tydef Maybe a = Unit + a end
+def mmap : (a -> b) -> Maybe a -> Maybe b = \f.\m. case m (\_. inl ()) (\a. inr (f a)) end
 
-def emptyT : RBTree k v = inl () end
+tydef RBTree k = rec b. Unit + [c: Color, k: k, l: b, r: b] end
+tydef RBNode k = rec n. [c: Color, k: k, l: Unit + n, r: Unit + n] end
 
-def isEmptyT : RBTree k v -> Bool = \d. d == emptyT end
+def emptyT : RBTree k = inl () end
 
-def getT : k -> RBTree k v -> Unit + v = \x.\t.
+def isEmptyT : RBTree k -> Bool = \d. d == emptyT end
+
+def getT : (k -> a) -> a -> RBTree k -> Unit + k = \p.\x.\t.
   case t (\_. inl ()) (\n.
-    if (x == n.k) { inr n.v } {
-        if (x < n.k) {
-            getT x n.l
+    if (x == p n.k) { inr n.k } {
+        if (x < p n.k) {
+            getT p x n.l
         } {
-            getT x n.r
+            getT p x n.r
         }
     }
   )
 end
 
-def containsT : k -> RBTree k v -> Bool = \x.\t. getT x t != inl () end
+def containsT : (k -> a) -> a -> RBTree k -> Bool = \p.\x.\t. getT p x t != inl () end
 
 tydef List a = rec l. Unit + (a * l) end
 
@@ -39,9 +42,9 @@ def formatL : List a -> Text = \l.
  in case l (\_. "[]") (\n. "[" ++ format (fst n) ++ f (snd n))
 end
 
-def inorder : RBTree k v -> List (k * v) = \t.
+def inorder : RBTree k -> List k = \t.
   case t (\_. inl ()) (\n.
-    appendL (inorder n.l) (appendL (pureL (n.k, n.v)) $ inorder n.r)
+    appendL (inorder n.l) (appendL (pureL n.k) $ inorder n.r)
   )
 end
 
@@ -52,32 +55,29 @@ balance B a x0 (T R (T R b x1 c) x2 d) = T R (T B a x0 b) x1 (T B c x2 d) -- cas
 balance B a x0 (T R b x1 (T R c x2 d)) = T R (T B a x0 b) x1 (T B c x2 d) -- case 4: RR red
 balance color a x b = T color a x b -- case 5
 */
-def balanceT : RBNode k v -> RBTree k v = \t.
-  let balanced : k -> v -> RBTree k v -> RBTree k v
-              -> k -> v
-              -> k -> v -> RBTree k v -> RBTree k v
-              -> RBTree k v
-    = \x0.\y0.\a.\b. \x1.\y1. \x2.\y2.\c.\d.
-    inr [c=red, k=x1, v=y1, l=inr [c=black, k=x0, v=y0, l=a, r=b], r=inr [c=black, k=x2, v=y2, l=c, r=d]]
-  in let case5 : RBNode k v -> RBTree k v =
+def balanceT : RBNode k -> RBTree k = \t.
+  let balanced : [ a: RBTree k, x0: k, b: RBTree k,   x1: k,   c: RBTree k, x2: k, d: RBTree k] -> RBTree k
+    = \v.
+    inr [c=red, l=inr [c=black, l=v.a, k=v.x0, r=v.b], k=v.x1, r=inr [c=black, l=v.c, k=v.x2, r=v.d]]
+  in let case5 : RBNode k -> RBTree k =
     inr  // just id - TODO: inline?
-  in let balanceRR : RBNode k v -> RBNode k v -> RBTree k v = \t.\rn.
+  in let balanceRR : RBNode k -> RBNode k -> RBTree k = \t.\rn.
     case rn.r (\_. case5 t) (\rrn.
       if (rrn.c == red) {
-        balanced t.k t.v t.l rn.l  rn.k rn.v  rrn.k rrn.v rrn.l rrn.r
+        balanced [a=t.l, x0=t.k, b=rn.l, x1=rn.k, c=rrn.l, x2=rrn.k, d=rrn.r]
       } {
         case5 t
       }
     )
-  in let balanceRL : RBNode k v -> RBNode k v -> RBTree k v = \t.\rn.
+  in let balanceRL : RBNode k -> RBNode k -> RBTree k = \t.\rn.
     case rn.l (\_. balanceRR t rn) (\rln.
       if (rln.c == red) {
-        balanced t.k t.v t.l rln.r  rln.k rln.v  rn.k rn.v rln.r rn.r
+        balanced [a=t.l, x0=t.k, b=rln.r, x1=rln.k, c=rln.r, x2=rn.k, d=rn.r]
       } {
         balanceRR t rn
       }
     )
-  in let balanceR : RBNode k v -> RBTree k v = \t.
+  in let balanceR : RBNode k -> RBTree k = \t.
     case t.r (\_.
       case5 t
     ) (\lr.
@@ -87,23 +87,23 @@ def balanceT : RBNode k v -> RBTree k v = \t.
         case5 t
       }
     )
-  in let balanceLR : RBNode k v -> RBNode k v -> RBTree k v = \t.\ln.
+  in let balanceLR : RBNode k -> RBNode k -> RBTree k = \t.\ln.
     case ln.r (\_. balanceR t) (\lrn.
       if (lrn.c == red) {
-        balanced ln.k ln.v ln.l lrn.l  lrn.k lrn.v  t.k t.v lrn.l t.r
+        balanced [a=ln.l, x0=ln.k, b=lrn.l, x1=lrn.k, c=lrn.l, x2=t.k, d=t.r]
       } {
         balanceR t
       }
     )
-  in let balanceLL : RBNode k v -> RBNode k v -> RBTree k v = \t.\ln.
+  in let balanceLL : RBNode k -> RBNode k -> RBTree k = \t.\ln.
     case ln.l (\_. balanceLR t ln) (\lln.
       if (lln.c == red) {
-        balanced lln.k lln.v lln.l lln.r  ln.k ln.v  t.k t.v ln.r t.r
+        balanced [a=lln.l, x0=lln.k, b=lln.r, x1=ln.k, c=ln.r, x2=t.k, d=t.r]
       } {
         balanceLR t ln
       }
     )
-  in let balanceL : RBNode k v -> RBTree k v = \t.
+  in let balanceL : RBNode k -> RBTree k = \t.
     case t.l (\_.
       balanceR t
     ) (\ln.
@@ -120,25 +120,25 @@ def balanceT : RBNode k v -> RBTree k v = \t.
   }
 end
 
-def insertT : k -> v -> RBTree k v -> RBTree k v = \x.\y.\t.
-  let ins : k -> v -> RBTree k v -> RBTree k v  = \x.\y.\t. case t
+def insertT : (k -> a) -> k -> RBTree k -> RBTree k = \p.\x.\t.
+  let ins : (k -> a) -> k -> RBTree k -> RBTree k =\p.\x.\t. case t
     (\_.
-      inr [c=red, k=x, v=y, l=inl (), r=inl ()]
+      inr [c=red, k=x, l=inl (), r=inl ()]
     ) (\n.
-      if (x == n.k) { inr [c=n.c, k=x, v=y, l=n.l, r=n.r] } {
+      if (p x == p n.k) { inr [c=n.c, k=x, l=n.l, r=n.r] } {
         if (x < n.k) {
-            balanceT [c=n.c, k=n.k, v=n.v, l=ins x y n.l, r=n.r]
+            balanceT [c=n.c, k=n.k, l=ins p x n.l, r=n.r]
         } {
-            balanceT [c=n.c,k=n.k, v=n.v, l=n.l, r=ins x y n.r]
+            balanceT [c=n.c,k=n.k, l=n.l, r=ins p x n.r]
         }
       }
     )
-  in let makeBlack : RBTree k v -> RBTree k v = \t. case t (\_.
+  in let makeBlack : RBTree k -> RBTree k = \t. case t (\_.
         fail "makeBlack will always be called on nonempty"
       ) (\n.
-        inr [c=black, k=n.k, v=n.v, l=n.l, r=n.r]
+        inr [c=black, k=n.k, l=n.l, r=n.r]
       )
-  in makeBlack $ ins x y t
+  in makeBlack $ ins p x t
 end
 
 /*
@@ -171,9 +171,33 @@ def deleteD : k -> RBTree k v -> RBTree k v = \x.\d.
 end
 */
 
+/*******************************************************************/
+/*                           DICTIONARY                            */
+/*******************************************************************/
+
+tydef Dict k v = RBTree (k * v) end
+
+def emptyD : Dict k v = emptyT end
+def isEmptyD : Dict k v -> Bool = isEmptyT end
+def getD : k -> Dict k v -> Unit + v = \k.\d. mmap snd (getT fst k d) end 
+def containsD : k -> Dict k v -> Bool = containsT fst end
+def insertD : k -> v -> Dict k v -> Dict k v = \k.\v. insertT fst (k, v) end
+
+/*******************************************************************/
+/*                              SET                                */
+/*******************************************************************/
+
+tydef Set k = RBTree k end
+
+def emptyS : Set k = emptyT end
+def isEmptyS : Set k -> Bool = isEmptyT end
+def containsS : k -> Set k -> Bool = containsT (\x.x) end
+def insertS : k -> Set k -> Set k = insertT (\x.x) end
+
 /*******************************************************************/
 /*                           UNIT TESTS                            */
 /*******************************************************************/
+
 def indent = \i. if (i <= 0) {""} {"  " ++ indent (i - 1)} end
 
 def assert = \i. \b. \m. if b {log $ indent i ++ "OK: " ++ m} {log "FAIL:"; fail m} end
@@ -194,25 +218,25 @@ end
 
 def test_empty: Int -> Cmd Unit = \i.
   group i "EMPTY TESTS" (\i.
-    assert i (isEmptyT emptyT) "empty tree should be empty";
-    assert_eq i (inl ()) (getT 0 $ emptyT) "no element should be present in an empty tree";
-    assert i (not $ containsT 0 $ emptyT) "empty tree should not contain any elements";
+    assert i (isEmptyD emptyD) "empty tree should be empty";
+    assert_eq i (inl ()) (getD 0 $ emptyD) "no element should be present in an empty tree";
+    assert i (not $ containsD 0 $ emptyD) "empty tree should not contain any elements";
   )
 end
 
 def test_insert: Int -> Cmd Unit = \i.
   group i "INSERT TESTS" (\i.
     group i "test {0: 1}" (\i.
-      let tree0 = insertT 0 1 emptyT in
-      assert i (not $ isEmptyT tree0) "nonempty tree should not be empty";
-      assert_eq i (inr 1) (getT 0 $ tree0) "one element should be present in a one element tree";
-      assert i (containsT 0 $ tree0) "one element tree should contain that elements";
-      assert i (not $ containsT 1 $ tree0) "one element tree should contain only that elements";
+      let tree0 = insertD 0 1 emptyD in
+      assert i (not $ isEmptyD tree0) "nonempty tree should not be empty";
+      assert_eq i (inr 1) (getD 0 $ tree0) "one element should be present in a one element tree";
+      assert i (containsD 0 $ tree0) "one element tree should contain that elements";
+      assert i (not $ containsD 1 $ tree0) "one element tree should contain only that elements";
     );
     group i "test {0: 1, 2: 3}" (\i.
-      let tree02 = insertT 2 3 $ insertT 0 1 emptyT in
-      assert_eq i (inr 1) (getT 0 $ tree02) "get 0 {0: 1, 2: 3} == 1";
-      assert_eq i (inr 3) (getT 2 $ tree02) "get 2 {0: 1, 2: 3} == 3";
+      let tree02 = insertD 2 3 $ insertD 0 1 emptyD in
+      assert_eq i (inr 1) (getD 0 $ tree02) "get 0 {0: 1, 2: 3} == 1";
+      assert_eq i (inr 3) (getD 2 $ tree02) "get 2 {0: 1, 2: 3} == 3";
     );
   );
 end

From 677b05604336d89135123a0b07a0358cb9a26a61 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Sun, 13 Oct 2024 23:16:20 +0200
Subject: [PATCH 07/22] Add delete

---
 example/dictionary.sw | 249 +++++++++++++++++++++++++++++++++++++-----
 1 file changed, 220 insertions(+), 29 deletions(-)

diff --git a/example/dictionary.sw b/example/dictionary.sw
index 7e8fdf530..59ca6078d 100644
--- a/example/dictionary.sw
+++ b/example/dictionary.sw
@@ -35,8 +35,20 @@ def pureL : a -> List a = \a. insertL a emptyL end
 
 def appendL : List a -> List a -> List a = \l.\r.
   case l (\_. r) (\ln. inr (fst ln, appendL (snd ln) r))
+end
+
+def lengthL : List a -> Int =
+  let len: Int -> List a -> Int = \a.\l. case l (\_. a) (\ln. len (a + 1) (snd ln)) in len 0
+end 
+
+def safeGetL : Int -> List a -> Unit + a = \i.\l.
+  case l (\_. inl ()) (\n. if (i <= 0) {inr $ fst n} {safeGetL (i - 1) (snd n)})
 end 
 
+def getL : Int -> List a -> a = \i.\l.
+  case (safeGetL i l) (\_. fail "GET_L OUT OF BOUNDS!") (\a. a)
+end
+
 def formatL : List a -> Text = \l.
  let f : List a -> Text = \l. case l (\_. "]") (\n. ", " ++ format (fst n) ++ f (snd n))
  in case l (\_. "[]") (\n. "[" ++ format (fst n) ++ f (snd n))
@@ -141,35 +153,158 @@ def insertT : (k -> a) -> k -> RBTree k -> RBTree k = \p.\x.\t.
   in makeBlack $ ins p x t
 end
 
-/*
-// helper function to remove the leftmost element from right subtree
-def pullLeft: [k: k, v: v, l: RBTree k v, r: RBTree k v] -> ((k * v) * (RBTree k v)) = \n.
-  case (n.l) (\_. ((n.k,n.v),n.r)) (\lt. 
-    let res = pullLeft lt in
-    (fst res, inr [k=n.k, v=n.v, l=snd res, r=n.r])
-  )
-end
-
-def deleteD : k -> RBTree k v -> RBTree k v = \x.\d.
-  case d (\_. inl ()) (\n.
-    if (x == n.k) {
-        case (n.l) (\_. n.r) (\lt.
-            case (n.r) (\_. inl ()) (\rt.
-                let r_kvd = pullLeft rt in
-                let r_kv = fst r_kvd in
-                inr [k=fst r_kv, v=snd r_kv, l=inr lt, r=snd r_kvd]
-            )
-        )
-    } {
-        if (x < n.k) {
-            inr [k=n.k, v=n.v, l=deleteD x n.l, r=n.r]
+def deleteT : (k -> a) -> a -> RBTree k -> RBTree k = \p.\x.\t.
+  // ------------------------------------------------------------------------------------------------------------
+  tydef Del k a = (k -> a) -> a -> RBTree k -> RBTree k end
+  // ------------------------------------------------------------------------------------------------------------
+  let makeBlack : RBTree k -> RBTree k = \t.
+    case t (\_. t) (\n. inr [c=black, k=n.k, l=n.l, r=n.r])
+  in let makeRed : RBNode k -> RBTree k = \n.
+    inr [c=red, k=n.k, l=n.l, r=n.r]
+  // ------------------------------------------------------------------------------------------------------------
+  /*
+  balL (T B (T R t1 x t2) y t3) = T R (T B t1 x t2) y t3
+  balL (T B t1 y (T B t2 z t3)) = balance' (T B t1 y (T R t2 z t3))
+  balL (T B t1 y (T R (T B t2 u t3) z t4@(T B l value r)))
+    = T R
+      (T B t1 y t2)
+      u
+      (balance' (T B t3 z
+        (T R l value r)))
+  */
+  in let balL : RBNode k -> RBTree k = \n.
+    let balL2 : RBNode k -> RBNode k -> RBTree k = \n.\rn.
+      case rn.l (\_. inr n) (\rln.
+        if (rln.c == red) {inr n} {
+          case rn.r (\_. inr n) (\rrn.
+            if (rrn.c == red) {inr n} {
+              inr [c=red,
+                   l=inr [c=black, l=n.l, k=n.k, r=rln.l],
+                   k=rln.k,
+                   r=balanceT [c=black, l=rln.r, k=rn.k, r=inr [c=red, l=rrn.l, k=rrn.k, r=rrn.r]]]
+            }
+          )
+        }
+      )
+    in let balL1 : RBNode k -> RBTree k = \n.
+      case n.r (\_. inr n) (\rn. 
+        if (rn.c == red) {balL2 n rn} {balanceT [c=black, k=n.k, l=n.l, r=makeRed rn]}
+      )
+    in case n.l (\_. balL1 n) (\ln. if (ln.c == red) {inr [c=red, k=n.k, l=makeBlack n.l, r=n.r]} {balL1 n})
+  // ------------------------------------------------------------------------------------------------------------
+  /*
+  balR (T B t1 y (T R t2 x t3)) = T R t1 y (T B t2 x t3)
+  balR (T B (T B t1 z t2) y t3) = balance' (T B (T R t1 z t2) y t3)
+  balR (T B
+    ln@(T R
+      lln@(T B lll llk llr)
+      lk
+      lrn@(T B lrl lrk lrr))
+    k
+    rn)
+    =
+    T R
+      (balance' (T B (T R lll llk llr) lk lrl))
+      lrk
+      (T B lrr k rn)
+  */
+  in let balR : RBNode k -> RBTree k = \n.
+    let balR2 : RBNode k -> RBNode k -> RBTree k = \n.\ln.
+      case ln.l (\_. inr n) (\lln.
+        if (lln.c == red) {inr n} {
+          case ln.r (\_. inr n) (\lrn.
+            if (lrn.c == red) {inr n} {
+              inr [c=red,
+                   l=balanceT [c=black, l=inr [c=red, l=lln.l, k=lln.k, r=lln.r], k=ln.k, r=lrn.l],
+                   k=lrn.k,
+                   r=inr [c=black, l=lrn.r, k=n.k, r=n.r]]
+            }
+          )
+        }
+      )
+    in let balR1 : RBNode k -> RBTree k = \n.
+      case n.l (\_. inr n) (\ln. 
+        if (ln.c == red) {balR2 n ln} {balanceT [c=black, k=n.k, l=makeRed ln, r=n.r]}
+      )
+    in case n.r (\_. balR1 n) (\rn. if (rn.c == red) {inr [c=red, k=n.k, l=n.l, r=makeBlack n.r]} {balR1 n})
+  // ------------------------------------------------------------------------------------------------------------
+  in let delL : Del k a -> (k -> a) -> a -> RBNode k -> RBTree k = \del.\p.\x.\n.
+    let dl = [c=n.c, k=n.k, l=del p x n.l, r=n.r] in
+    if (n.c == red) { inr dl } { balL dl }
+  // ------------------------------------------------------------------------------------------------------------
+  in let delR : Del k a -> (k -> a) -> a -> RBNode k -> RBTree k = \del.\p.\x.\n.
+    let dr = [c=n.c, k=n.k, l=n.l, r=del p x n.r] in
+    if (n.c == red) { inr dr } { balR dr }
+  // ------------------------------------------------------------------------------------------------------------
+  /*
+  fuse :: Tree a -> Tree a -> Tree a
+  fuse E t = t
+  fuse t E = t
+  fuse t1@(T B _ _ _) (T R t3 y t4) = T R (fuse t1 t3) y t4
+  fuse (T R t1 x t2) t3@(T B _ _ _) = T R t1 x (fuse t2 t3)
+  fuse (T R t1 x t2) (T R t3 y t4)  =
+    let s = fuse t2 t3
+    in case s of
+        (T R s1 z s2) -> (T R (T R t1 x s1) z (T R s2 y t4))
+        (T B _ _ _)   -> (T R t1 x (T R s y t4))
+  fuse (T B t1 x t2) (T B t3 y t4)  =
+    let s = fuse t2 t3
+    in case s of
+        (T R s1 z s2) -> (T R (T B t1 x s1) z (T B s2 y t4))
+        (T B s1 z s2) -> balL (T B t1 x (T B s y t4))
+  */
+  in let fuse: RBTree k -> RBTree k -> RBTree k = \l.\r.
+    /* TODO: when both are missing just pull one up as black parent of red leaf - let's see what that does */
+    case l (\_. r) (\ln. case r (\_. l) (\rn.
+      if (ln.c == red) {
+        if (rn.c == red) {
+          /* RED RED */
+          let s = fuse ln.r rn.l in
+          let b_case = {inr [c=red, l=ln.l, k=ln.k, r=inr [c=red, l=s, k=rn.k, r=rn.r]]} in
+          case s (\_. force b_case) (\sn.
+            if (sn.c == red) {
+              inr [c=red, l=inr [c=red, l=ln.l, k=ln.k, r=sn.l], k=sn.k, r=inr [c=red, l=sn.r, k=rn.k, r=rn.r]]
+            } {
+              force b_case
+            }
+          ) 
         } {
-            inr [k=n.k, v=n.v, l=n.l, r=deleteD x n.r]
+          /* RED BLACK */
+          inr [c=red, l=ln.l, k=ln.k, r=fuse ln.r (inr rn)]
         }
-    }
-  )
+      } {
+        if (rn.c == red) {
+          /* BLACK RED */
+          inr [c=red, l=fuse (inr ln) rn.l, k=rn.k, r=rn.r]
+        } {
+          /* BLACK BLACK */
+          let s = fuse ln.r rn.l in
+          let b_case = {balL [c=black, l=ln.l, k=ln.k, r=inr [c=black, l=s, k=rn.k, r=rn.r]]} in
+          case s (\_. force b_case) (\sn.
+            if (sn.c == red) {
+              inr [c=red, l=inr [c=black, l=ln.l, k=ln.k, r=sn.l], k=sn.k, r=inr [c=black, l=sn.r, k=rn.k, r=rn.r]]
+            } {
+              force b_case
+            }
+          )
+        }
+      }
+    ))
+  // ------------------------------------------------------------------------------------------------------------
+  in let del : (k -> a) -> a -> RBTree k -> RBTree k = \p.\x.\t.
+    case t (\_.t) (\n. 
+      if (p n.k == x) {fuse n.l n.r} {
+        if (x < p n.k) {delL del p x n} {delR del p x n}
+      }
+    )
+  // ------------------------------------------------------------------------------------------------------------
+  in makeBlack $ del p x t
 end
-*/
+
+// delete 8
+def problem = inr [c = false, k = 8,
+  l = inr [c = false, k = 6, l = inl (), r = inl ()],
+  r = inr [c = false, k = 80, l = inl (), r = inl ()]] end
 
 /*******************************************************************/
 /*                           DICTIONARY                            */
@@ -182,6 +317,13 @@ def isEmptyD : Dict k v -> Bool = isEmptyT end
 def getD : k -> Dict k v -> Unit + v = \k.\d. mmap snd (getT fst k d) end 
 def containsD : k -> Dict k v -> Bool = containsT fst end
 def insertD : k -> v -> Dict k v -> Dict k v = \k.\v. insertT fst (k, v) end
+def deleteD : k -> Dict k v -> Dict k v = \k. deleteT fst k end
+
+def formatD : Dict k v -> Text = \d.
+ let p : (k * v) -> Text = \kv. format (fst kv) ++ ": " ++ format (snd kv) in 
+ let f : List (k * v) -> Text = \l. case l (\_. "}") (\n. ", " ++ p (fst n) ++ f (snd n))
+ in case (inorder d) (\_. "{}") (\n. "{" ++ p (fst n) ++ f (snd n))
+end
 
 /*******************************************************************/
 /*                              SET                                */
@@ -193,12 +335,14 @@ def emptyS : Set k = emptyT end
 def isEmptyS : Set k -> Bool = isEmptyT end
 def containsS : k -> Set k -> Bool = containsT (\x.x) end
 def insertS : k -> Set k -> Set k = insertT (\x.x) end
+def deleteS : k -> Set k -> Set k = \k. deleteT (\x.x) k end
+def formatS : Set k -> Text = \s. formatL $ inorder s end
 
 /*******************************************************************/
 /*                           UNIT TESTS                            */
 /*******************************************************************/
 
-def indent = \i. if (i <= 0) {""} {"  " ++ indent (i - 1)} end
+def indent = \i. if (i <= 0) {" "} {"--" ++ indent (i - 1)} end
 
 def assert = \i. \b. \m. if b {log $ indent i ++ "OK: " ++ m} {log "FAIL:"; fail m} end
 
@@ -213,7 +357,7 @@ end
 def group = \i. \m. \tests.
   log $ indent i ++ "START " ++ m ++ ":";
   tests $ i + 1;
-  log $ indent i ++ "END " ++ m ++ ":";
+  return ()
 end
 
 def test_empty: Int -> Cmd Unit = \i.
@@ -241,9 +385,56 @@ def test_insert: Int -> Cmd Unit = \i.
   );
 end
 
+def randomTestS = \i.\s.\test.
+  if (i <= 0) {return s} {
+    x <- random 100;
+    let ns = insertS x s in
+    test ns;
+    randomTestS (i - 1) ns test
+  }
+end
+
+def delete_insert_prop = \i.\t.
+  x <- random 100;
+  let i_t = inorder t in
+  let f_t = formatS t in
+  if (not $ containsS x t) {
+    log $ format x;
+    assert_eq i
+      (formatL i_t)
+      (formatS $ deleteS x $ insertS x t)
+      (f_t ++ " == delete " ++ format x ++ " $ insert " ++ format x ++ " " ++ f_t)
+  } { delete_insert_prop i t /* reroll */}
+end
+
+def delete_delete_prop = \i.\t.
+  let i_t = inorder t in
+  i <- random (lengthL i_t);
+  let x = getL i i_t in
+  let ds = deleteS x t in
+  let dds = deleteS x ds in
+  let f_t = formatS t in
+  let f_dx = "delete " ++ format x in
+  assert_eq i (formatS ds) (formatS dds)
+    (f_dx ++ f_t ++ " == " ++ f_dx ++ " $ " ++ f_dx ++ " " ++ f_t)
+end
+
+def test_delete: Int -> Cmd Unit = \i.
+  group i "DELETE TESTS" (\i.
+    randomTestS 10 emptyS (\s.
+      group i (formatS s) (\i.
+        delete_insert_prop i s;
+        delete_delete_prop i s;
+      )
+    )
+  )
+end
+
 def test_tree: Cmd Unit =
   group 0 "TREE TESTS" (\i.
     test_empty i;
     test_insert i;
-  )
+    test_delete i;
+  );
+  log "ALL TREE TESTS PASSED!"
 end
\ No newline at end of file

From 99a75b7aaff986c3ecb41a36004c8ff9d5a00da9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Mon, 14 Oct 2024 22:48:16 +0200
Subject: [PATCH 08/22] add printf debug

---
 example/dictionary.sw | 21 +++++++++++++++++++--
 1 file changed, 19 insertions(+), 2 deletions(-)

diff --git a/example/dictionary.sw b/example/dictionary.sw
index 59ca6078d..5ced65c71 100644
--- a/example/dictionary.sw
+++ b/example/dictionary.sw
@@ -60,6 +60,25 @@ def inorder : RBTree k -> List k = \t.
   )
 end
 
+def formatT : RBTree k -> Text = \t.
+  case t (\_. "N") (\n.
+    "(T "
+    ++ if (n.c == red) {"R "} {"B "}
+    ++ formatT n.l ++ " " ++ format n.k ++ " " ++ formatT n.r ++ ")"
+  ) 
+end
+
+def indent_ = \c.\i. if (i <= 0) {" "} {c ++ indent_ c (i - 1)} end
+def indent = indent_ " " end
+
+def debugT : RBTree k -> Cmd Unit =
+  let d : Text -> Text -> Text -> RBTree k -> Cmd Unit = \i.\li.\ri.\t. case t (\_. log $ i ++ "+ N") (\n.
+    d (i ++ li) "  " "| " n.l;
+    log $ i ++ "+ " ++ if (n.c == red) {"R "} {"B "} ++ format n.k;
+    d (i ++ ri) "| " "  " n.r;
+  ) in d "" "" ""
+end
+
 /*
 balance B (T R (T R a x0 b) x1 c) x2 d = T R (T B a x0 b) x1 (T B c x2 d) -- case 1: LL red
 balance B (T R a x0 (T R b x1 c)) x2 d = T R (T B a x0 b) x1 (T B c x2 d) -- case 2: LR red
@@ -342,8 +361,6 @@ def formatS : Set k -> Text = \s. formatL $ inorder s end
 /*                           UNIT TESTS                            */
 /*******************************************************************/
 
-def indent = \i. if (i <= 0) {" "} {"--" ++ indent (i - 1)} end
-
 def assert = \i. \b. \m. if b {log $ indent i ++ "OK: " ++ m} {log "FAIL:"; fail m} end
 
 def assert_eq 

From 1618ea38cacb577cbd932efa1d9b015f9226f46c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Tue, 15 Oct 2024 11:02:51 +0200
Subject: [PATCH 09/22] fix L/R typo

---
 example/dictionary.sw | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/example/dictionary.sw b/example/dictionary.sw
index 5ced65c71..003ee582b 100644
--- a/example/dictionary.sw
+++ b/example/dictionary.sw
@@ -103,7 +103,7 @@ def balanceT : RBNode k -> RBTree k = \t.
   in let balanceRL : RBNode k -> RBNode k -> RBTree k = \t.\rn.
     case rn.l (\_. balanceRR t rn) (\rln.
       if (rln.c == red) {
-        balanced [a=t.l, x0=t.k, b=rln.r, x1=rln.k, c=rln.r, x2=rn.k, d=rn.r]
+        balanced [a=t.l, x0=t.k, b=rln.l, x1=rln.k, c=rln.r, x2=rn.k, d=rn.r]
       } {
         balanceRR t rn
       }

From ae8388e536e543772ec094fb1550001eb19867bb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Tue, 15 Oct 2024 11:02:59 +0200
Subject: [PATCH 10/22] cleanup

---
 example/dictionary.sw | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/example/dictionary.sw b/example/dictionary.sw
index 003ee582b..fa630caa2 100644
--- a/example/dictionary.sw
+++ b/example/dictionary.sw
@@ -160,7 +160,7 @@ def insertT : (k -> a) -> k -> RBTree k -> RBTree k = \p.\x.\t.
         if (x < n.k) {
             balanceT [c=n.c, k=n.k, l=ins p x n.l, r=n.r]
         } {
-            balanceT [c=n.c,k=n.k, l=n.l, r=ins p x n.r]
+            balanceT [c=n.c, k=n.k, l=n.l, r=ins p x n.r]
         }
       }
     )
@@ -256,7 +256,6 @@ def deleteT : (k -> a) -> a -> RBTree k -> RBTree k = \p.\x.\t.
     if (n.c == red) { inr dr } { balR dr }
   // ------------------------------------------------------------------------------------------------------------
   /*
-  fuse :: Tree a -> Tree a -> Tree a
   fuse E t = t
   fuse t E = t
   fuse t1@(T B _ _ _) (T R t3 y t4) = T R (fuse t1 t3) y t4
@@ -273,7 +272,6 @@ def deleteT : (k -> a) -> a -> RBTree k -> RBTree k = \p.\x.\t.
         (T B s1 z s2) -> balL (T B t1 x (T B s y t4))
   */
   in let fuse: RBTree k -> RBTree k -> RBTree k = \l.\r.
-    /* TODO: when both are missing just pull one up as black parent of red leaf - let's see what that does */
     case l (\_. r) (\ln. case r (\_. l) (\rn.
       if (ln.c == red) {
         if (rn.c == red) {
@@ -320,11 +318,6 @@ def deleteT : (k -> a) -> a -> RBTree k -> RBTree k = \p.\x.\t.
   in makeBlack $ del p x t
 end
 
-// delete 8
-def problem = inr [c = false, k = 8,
-  l = inr [c = false, k = 6, l = inl (), r = inl ()],
-  r = inr [c = false, k = 80, l = inl (), r = inl ()]] end
-
 /*******************************************************************/
 /*                           DICTIONARY                            */
 /*******************************************************************/

From eb85829f077d65307523e59427c100381340612a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Tue, 15 Oct 2024 14:28:15 +0200
Subject: [PATCH 11/22] fix other typo

---
 example/dictionary.sw | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/example/dictionary.sw b/example/dictionary.sw
index fa630caa2..9d9331e70 100644
--- a/example/dictionary.sw
+++ b/example/dictionary.sw
@@ -121,7 +121,7 @@ def balanceT : RBNode k -> RBTree k = \t.
   in let balanceLR : RBNode k -> RBNode k -> RBTree k = \t.\ln.
     case ln.r (\_. balanceR t) (\lrn.
       if (lrn.c == red) {
-        balanced [a=ln.l, x0=ln.k, b=lrn.l, x1=lrn.k, c=lrn.l, x2=t.k, d=t.r]
+        balanced [a=ln.l, x0=ln.k, b=lrn.l, x1=lrn.k, c=lrn.r, x2=t.k, d=t.r]
       } {
         balanceR t
       }
@@ -397,7 +397,7 @@ end
 
 def randomTestS = \i.\s.\test.
   if (i <= 0) {return s} {
-    x <- random 100;
+    x <- random 20;
     let ns = insertS x s in
     test ns;
     randomTestS (i - 1) ns test
@@ -405,7 +405,7 @@ def randomTestS = \i.\s.\test.
 end
 
 def delete_insert_prop = \i.\t.
-  x <- random 100;
+  x <- random 20;
   let i_t = inorder t in
   let f_t = formatS t in
   if (not $ containsS x t) {
@@ -431,7 +431,7 @@ end
 
 def test_delete: Int -> Cmd Unit = \i.
   group i "DELETE TESTS" (\i.
-    randomTestS 10 emptyS (\s.
+    randomTestS 15 emptyS (\s.
       group i (formatS s) (\i.
         delete_insert_prop i s;
         delete_delete_prop i s;

From 7ca0ddf306468d45ebd77a86d15daf5b505cbe97 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Tue, 15 Oct 2024 14:57:05 +0200
Subject: [PATCH 12/22] Add docs

---
 example/dictionary.sw | 164 +++++++++++++++++++++++-------------------
 1 file changed, 90 insertions(+), 74 deletions(-)

diff --git a/example/dictionary.sw b/example/dictionary.sw
index 9d9331e70..4707a9f32 100644
--- a/example/dictionary.sw
+++ b/example/dictionary.sw
@@ -1,33 +1,22 @@
-tydef Color = Bool end
-def black = false end
-def red = true end
-// TODO: s/\((.*\.c) == red\)/$1.red/g
+/*******************************************************************/
+/*                           CONTAINERS                            */
+/*******************************************************************/
+// This file has an example implementation of lists, sets and maps
+// (a.k.a dictionaries) using recursive types.
+//
+// The implementation uses a Red-Black tree balanced binary tree
+// with projection (k -> a) to get sets and dictionaries (compare
+// only first element of tuple). It is based on Haskell code in:
+// https://abhiroop.github.io/Haskell-Red-Black-Tree/
 
 tydef Maybe a = Unit + a end
 def mmap : (a -> b) -> Maybe a -> Maybe b = \f.\m. case m (\_. inl ()) (\a. inr (f a)) end
 
-tydef RBTree k = rec b. Unit + [c: Color, k: k, l: b, r: b] end
-tydef RBNode k = rec n. [c: Color, k: k, l: Unit + n, r: Unit + n] end
-
-def emptyT : RBTree k = inl () end
-
-def isEmptyT : RBTree k -> Bool = \d. d == emptyT end
-
-def getT : (k -> a) -> a -> RBTree k -> Unit + k = \p.\x.\t.
-  case t (\_. inl ()) (\n.
-    if (x == p n.k) { inr n.k } {
-        if (x < p n.k) {
-            getT p x n.l
-        } {
-            getT p x n.r
-        }
-    }
-  )
-end
-
-def containsT : (k -> a) -> a -> RBTree k -> Bool = \p.\x.\t. getT p x t != inl () end
+/*******************************************************************/
+/*                              LISTS                              */
+/*******************************************************************/
 
-tydef List a = rec l. Unit + (a * l) end
+tydef List a = rec l. Maybe (a * l) end
 
 def emptyL : List a = inl () end
 def insertL : a -> List a -> List a = \a.\l. inr (a, l) end
@@ -41,12 +30,12 @@ def lengthL : List a -> Int =
   let len: Int -> List a -> Int = \a.\l. case l (\_. a) (\ln. len (a + 1) (snd ln)) in len 0
 end 
 
-def safeGetL : Int -> List a -> Unit + a = \i.\l.
+def safeGetL : Int -> List a -> Maybe a = \i.\l.
   case l (\_. inl ()) (\n. if (i <= 0) {inr $ fst n} {safeGetL (i - 1) (snd n)})
 end 
 
 def getL : Int -> List a -> a = \i.\l.
-  case (safeGetL i l) (\_. fail "GET_L OUT OF BOUNDS!") (\a. a)
+  case (safeGetL i l) (\_. fail $ "INDEX " ++ format i ++ " OUT OF BOUNDS!") (\a. a)
 end
 
 def formatL : List a -> Text = \l.
@@ -54,6 +43,33 @@ def formatL : List a -> Text = \l.
  in case l (\_. "[]") (\n. "[" ++ format (fst n) ++ f (snd n))
 end
 
+/*******************************************************************/
+/*                         RED BLACK TREE                          */
+/*******************************************************************/
+
+tydef RBTree k = rec b. Maybe [red: Bool, k: k, l: b, r: b] end
+
+// equirecursive types allow us to get the node type without mutual recursion
+tydef RBNode k = rec n. [red: Bool, k: k, l: Maybe n, r: Maybe n] end
+
+def emptyT : RBTree k = inl () end
+
+def isEmptyT : RBTree k -> Bool = \d. d == emptyT end
+
+def getT : (k -> a) -> a -> RBTree k -> Maybe k = \p.\x.\t.
+  case t (\_. inl ()) (\n.
+    if (x == p n.k) { inr n.k } {
+        if (x < p n.k) {
+            getT p x n.l
+        } {
+            getT p x n.r
+        }
+    }
+  )
+end
+
+def containsT : (k -> a) -> a -> RBTree k -> Bool = \p.\x.\t. getT p x t != inl () end
+
 def inorder : RBTree k -> List k = \t.
   case t (\_. inl ()) (\n.
     appendL (inorder n.l) (appendL (pureL n.k) $ inorder n.r)
@@ -63,7 +79,7 @@ end
 def formatT : RBTree k -> Text = \t.
   case t (\_. "N") (\n.
     "(T "
-    ++ if (n.c == red) {"R "} {"B "}
+    ++ if n.red {"R "} {"B "}
     ++ formatT n.l ++ " " ++ format n.k ++ " " ++ formatT n.r ++ ")"
   ) 
 end
@@ -74,7 +90,7 @@ def indent = indent_ " " end
 def debugT : RBTree k -> Cmd Unit =
   let d : Text -> Text -> Text -> RBTree k -> Cmd Unit = \i.\li.\ri.\t. case t (\_. log $ i ++ "+ N") (\n.
     d (i ++ li) "  " "| " n.l;
-    log $ i ++ "+ " ++ if (n.c == red) {"R "} {"B "} ++ format n.k;
+    log $ i ++ "+ " ++ if n.red {"R "} {"B "} ++ format n.k;
     d (i ++ ri) "| " "  " n.r;
   ) in d "" "" ""
 end
@@ -89,12 +105,12 @@ balance color a x b = T color a x b -- case 5
 def balanceT : RBNode k -> RBTree k = \t.
   let balanced : [ a: RBTree k, x0: k, b: RBTree k,   x1: k,   c: RBTree k, x2: k, d: RBTree k] -> RBTree k
     = \v.
-    inr [c=red, l=inr [c=black, l=v.a, k=v.x0, r=v.b], k=v.x1, r=inr [c=black, l=v.c, k=v.x2, r=v.d]]
+    inr [red=true, l=inr [red=false, l=v.a, k=v.x0, r=v.b], k=v.x1, r=inr [red=false, l=v.c, k=v.x2, r=v.d]]
   in let case5 : RBNode k -> RBTree k =
     inr  // just id - TODO: inline?
   in let balanceRR : RBNode k -> RBNode k -> RBTree k = \t.\rn.
     case rn.r (\_. case5 t) (\rrn.
-      if (rrn.c == red) {
+      if rrn.red {
         balanced [a=t.l, x0=t.k, b=rn.l, x1=rn.k, c=rrn.l, x2=rrn.k, d=rrn.r]
       } {
         case5 t
@@ -102,7 +118,7 @@ def balanceT : RBNode k -> RBTree k = \t.
     )
   in let balanceRL : RBNode k -> RBNode k -> RBTree k = \t.\rn.
     case rn.l (\_. balanceRR t rn) (\rln.
-      if (rln.c == red) {
+      if rln.red {
         balanced [a=t.l, x0=t.k, b=rln.l, x1=rln.k, c=rln.r, x2=rn.k, d=rn.r]
       } {
         balanceRR t rn
@@ -112,7 +128,7 @@ def balanceT : RBNode k -> RBTree k = \t.
     case t.r (\_.
       case5 t
     ) (\lr.
-      if (lr.c == red) {
+      if lr.red {
         balanceRL t lr
       } {
         case5 t
@@ -120,7 +136,7 @@ def balanceT : RBNode k -> RBTree k = \t.
     )
   in let balanceLR : RBNode k -> RBNode k -> RBTree k = \t.\ln.
     case ln.r (\_. balanceR t) (\lrn.
-      if (lrn.c == red) {
+      if lrn.red {
         balanced [a=ln.l, x0=ln.k, b=lrn.l, x1=lrn.k, c=lrn.r, x2=t.k, d=t.r]
       } {
         balanceR t
@@ -128,7 +144,7 @@ def balanceT : RBNode k -> RBTree k = \t.
     )
   in let balanceLL : RBNode k -> RBNode k -> RBTree k = \t.\ln.
     case ln.l (\_. balanceLR t ln) (\lln.
-      if (lln.c == red) {
+      if lln.red {
         balanced [a=lln.l, x0=lln.k, b=lln.r, x1=ln.k, c=ln.r, x2=t.k, d=t.r]
       } {
         balanceLR t ln
@@ -138,13 +154,13 @@ def balanceT : RBNode k -> RBTree k = \t.
     case t.l (\_.
       balanceR t
     ) (\ln.
-      if (ln.c == red) {
+      if ln.red {
         balanceLL t ln
       } {
         balanceR t
       }
     )
-  in if (t.c == red) {
+  in if t.red {
     case5 t
   } {
     balanceL t
@@ -154,20 +170,20 @@ end
 def insertT : (k -> a) -> k -> RBTree k -> RBTree k = \p.\x.\t.
   let ins : (k -> a) -> k -> RBTree k -> RBTree k =\p.\x.\t. case t
     (\_.
-      inr [c=red, k=x, l=inl (), r=inl ()]
+      inr [red=true, k=x, l=inl (), r=inl ()]
     ) (\n.
-      if (p x == p n.k) { inr [c=n.c, k=x, l=n.l, r=n.r] } {
+      if (p x == p n.k) { inr [red=n.red, k=x, l=n.l, r=n.r] } {
         if (x < n.k) {
-            balanceT [c=n.c, k=n.k, l=ins p x n.l, r=n.r]
+            balanceT [red=n.red, k=n.k, l=ins p x n.l, r=n.r]
         } {
-            balanceT [c=n.c, k=n.k, l=n.l, r=ins p x n.r]
+            balanceT [red=n.red, k=n.k, l=n.l, r=ins p x n.r]
         }
       }
     )
   in let makeBlack : RBTree k -> RBTree k = \t. case t (\_.
         fail "makeBlack will always be called on nonempty"
       ) (\n.
-        inr [c=black, k=n.k, l=n.l, r=n.r]
+        inr [red=false, k=n.k, l=n.l, r=n.r]
       )
   in makeBlack $ ins p x t
 end
@@ -177,9 +193,9 @@ def deleteT : (k -> a) -> a -> RBTree k -> RBTree k = \p.\x.\t.
   tydef Del k a = (k -> a) -> a -> RBTree k -> RBTree k end
   // ------------------------------------------------------------------------------------------------------------
   let makeBlack : RBTree k -> RBTree k = \t.
-    case t (\_. t) (\n. inr [c=black, k=n.k, l=n.l, r=n.r])
+    case t (\_. t) (\n. inr [red=false, k=n.k, l=n.l, r=n.r])
   in let makeRed : RBNode k -> RBTree k = \n.
-    inr [c=red, k=n.k, l=n.l, r=n.r]
+    inr [red=true, k=n.k, l=n.l, r=n.r]
   // ------------------------------------------------------------------------------------------------------------
   /*
   balL (T B (T R t1 x t2) y t3) = T R (T B t1 x t2) y t3
@@ -194,22 +210,22 @@ def deleteT : (k -> a) -> a -> RBTree k -> RBTree k = \p.\x.\t.
   in let balL : RBNode k -> RBTree k = \n.
     let balL2 : RBNode k -> RBNode k -> RBTree k = \n.\rn.
       case rn.l (\_. inr n) (\rln.
-        if (rln.c == red) {inr n} {
+        if rln.red {inr n} {
           case rn.r (\_. inr n) (\rrn.
-            if (rrn.c == red) {inr n} {
-              inr [c=red,
-                   l=inr [c=black, l=n.l, k=n.k, r=rln.l],
+            if rrn.red {inr n} {
+              inr [red=true,
+                   l=inr [red=false, l=n.l, k=n.k, r=rln.l],
                    k=rln.k,
-                   r=balanceT [c=black, l=rln.r, k=rn.k, r=inr [c=red, l=rrn.l, k=rrn.k, r=rrn.r]]]
+                   r=balanceT [red=false, l=rln.r, k=rn.k, r=inr [red=true, l=rrn.l, k=rrn.k, r=rrn.r]]]
             }
           )
         }
       )
     in let balL1 : RBNode k -> RBTree k = \n.
       case n.r (\_. inr n) (\rn. 
-        if (rn.c == red) {balL2 n rn} {balanceT [c=black, k=n.k, l=n.l, r=makeRed rn]}
+        if rn.red {balL2 n rn} {balanceT [red=false, k=n.k, l=n.l, r=makeRed rn]}
       )
-    in case n.l (\_. balL1 n) (\ln. if (ln.c == red) {inr [c=red, k=n.k, l=makeBlack n.l, r=n.r]} {balL1 n})
+    in case n.l (\_. balL1 n) (\ln. if ln.red {inr [red=true, k=n.k, l=makeBlack n.l, r=n.r]} {balL1 n})
   // ------------------------------------------------------------------------------------------------------------
   /*
   balR (T B t1 y (T R t2 x t3)) = T R t1 y (T B t2 x t3)
@@ -230,30 +246,30 @@ def deleteT : (k -> a) -> a -> RBTree k -> RBTree k = \p.\x.\t.
   in let balR : RBNode k -> RBTree k = \n.
     let balR2 : RBNode k -> RBNode k -> RBTree k = \n.\ln.
       case ln.l (\_. inr n) (\lln.
-        if (lln.c == red) {inr n} {
+        if lln.red {inr n} {
           case ln.r (\_. inr n) (\lrn.
-            if (lrn.c == red) {inr n} {
-              inr [c=red,
-                   l=balanceT [c=black, l=inr [c=red, l=lln.l, k=lln.k, r=lln.r], k=ln.k, r=lrn.l],
+            if lrn.red {inr n} {
+              inr [red=true,
+                   l=balanceT [red=false, l=inr [red=true, l=lln.l, k=lln.k, r=lln.r], k=ln.k, r=lrn.l],
                    k=lrn.k,
-                   r=inr [c=black, l=lrn.r, k=n.k, r=n.r]]
+                   r=inr [red=false, l=lrn.r, k=n.k, r=n.r]]
             }
           )
         }
       )
     in let balR1 : RBNode k -> RBTree k = \n.
       case n.l (\_. inr n) (\ln. 
-        if (ln.c == red) {balR2 n ln} {balanceT [c=black, k=n.k, l=makeRed ln, r=n.r]}
+        if ln.red {balR2 n ln} {balanceT [red=false, k=n.k, l=makeRed ln, r=n.r]}
       )
-    in case n.r (\_. balR1 n) (\rn. if (rn.c == red) {inr [c=red, k=n.k, l=n.l, r=makeBlack n.r]} {balR1 n})
+    in case n.r (\_. balR1 n) (\rn. if rn.red {inr [red=true, k=n.k, l=n.l, r=makeBlack n.r]} {balR1 n})
   // ------------------------------------------------------------------------------------------------------------
   in let delL : Del k a -> (k -> a) -> a -> RBNode k -> RBTree k = \del.\p.\x.\n.
-    let dl = [c=n.c, k=n.k, l=del p x n.l, r=n.r] in
-    if (n.c == red) { inr dl } { balL dl }
+    let dl = [red=n.red, k=n.k, l=del p x n.l, r=n.r] in
+    if n.red { inr dl } { balL dl }
   // ------------------------------------------------------------------------------------------------------------
   in let delR : Del k a -> (k -> a) -> a -> RBNode k -> RBTree k = \del.\p.\x.\n.
-    let dr = [c=n.c, k=n.k, l=n.l, r=del p x n.r] in
-    if (n.c == red) { inr dr } { balR dr }
+    let dr = [red=n.red, k=n.k, l=n.l, r=del p x n.r] in
+    if n.red { inr dr } { balR dr }
   // ------------------------------------------------------------------------------------------------------------
   /*
   fuse E t = t
@@ -273,33 +289,33 @@ def deleteT : (k -> a) -> a -> RBTree k -> RBTree k = \p.\x.\t.
   */
   in let fuse: RBTree k -> RBTree k -> RBTree k = \l.\r.
     case l (\_. r) (\ln. case r (\_. l) (\rn.
-      if (ln.c == red) {
-        if (rn.c == red) {
+      if ln.red {
+        if rn.red {
           /* RED RED */
           let s = fuse ln.r rn.l in
-          let b_case = {inr [c=red, l=ln.l, k=ln.k, r=inr [c=red, l=s, k=rn.k, r=rn.r]]} in
+          let b_case = {inr [red=true, l=ln.l, k=ln.k, r=inr [red=true, l=s, k=rn.k, r=rn.r]]} in
           case s (\_. force b_case) (\sn.
-            if (sn.c == red) {
-              inr [c=red, l=inr [c=red, l=ln.l, k=ln.k, r=sn.l], k=sn.k, r=inr [c=red, l=sn.r, k=rn.k, r=rn.r]]
+            if sn.red {
+              inr [red=true, l=inr [red=true, l=ln.l, k=ln.k, r=sn.l], k=sn.k, r=inr [red=true, l=sn.r, k=rn.k, r=rn.r]]
             } {
               force b_case
             }
           ) 
         } {
           /* RED BLACK */
-          inr [c=red, l=ln.l, k=ln.k, r=fuse ln.r (inr rn)]
+          inr [red=true, l=ln.l, k=ln.k, r=fuse ln.r (inr rn)]
         }
       } {
-        if (rn.c == red) {
+        if rn.red {
           /* BLACK RED */
-          inr [c=red, l=fuse (inr ln) rn.l, k=rn.k, r=rn.r]
+          inr [red=true, l=fuse (inr ln) rn.l, k=rn.k, r=rn.r]
         } {
           /* BLACK BLACK */
           let s = fuse ln.r rn.l in
-          let b_case = {balL [c=black, l=ln.l, k=ln.k, r=inr [c=black, l=s, k=rn.k, r=rn.r]]} in
+          let b_case = {balL [red=false, l=ln.l, k=ln.k, r=inr [red=false, l=s, k=rn.k, r=rn.r]]} in
           case s (\_. force b_case) (\sn.
-            if (sn.c == red) {
-              inr [c=red, l=inr [c=black, l=ln.l, k=ln.k, r=sn.l], k=sn.k, r=inr [c=black, l=sn.r, k=rn.k, r=rn.r]]
+            if sn.red {
+              inr [red=true, l=inr [red=false, l=ln.l, k=ln.k, r=sn.l], k=sn.k, r=inr [red=false, l=sn.r, k=rn.k, r=rn.r]]
             } {
               force b_case
             }
@@ -326,7 +342,7 @@ tydef Dict k v = RBTree (k * v) end
 
 def emptyD : Dict k v = emptyT end
 def isEmptyD : Dict k v -> Bool = isEmptyT end
-def getD : k -> Dict k v -> Unit + v = \k.\d. mmap snd (getT fst k d) end 
+def getD : k -> Dict k v -> Maybe v = \k.\d. mmap snd (getT fst k d) end 
 def containsD : k -> Dict k v -> Bool = containsT fst end
 def insertD : k -> v -> Dict k v -> Dict k v = \k.\v. insertT fst (k, v) end
 def deleteD : k -> Dict k v -> Dict k v = \k. deleteT fst k end

From 75ee8b83d0cf86880d6b165c1b1bd68973405b70 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Tue, 15 Oct 2024 15:23:23 +0200
Subject: [PATCH 13/22] Add flat map/set like interface to list

---
 example/dictionary.sw | 47 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)

diff --git a/example/dictionary.sw b/example/dictionary.sw
index 4707a9f32..4fd562524 100644
--- a/example/dictionary.sw
+++ b/example/dictionary.sw
@@ -38,6 +38,43 @@ def getL : Int -> List a -> a = \i.\l.
   case (safeGetL i l) (\_. fail $ "INDEX " ++ format i ++ " OUT OF BOUNDS!") (\a. a)
 end
 
+// get from ordered list
+def getKeyL : (a -> k) -> k -> List a -> Maybe a = \p.\x.\l.
+  case l (\_. inl ()) (\n.
+    let nx = p (fst n) in
+    if (nx == x) {
+      inr $ fst n
+    } {
+      if (nx < x) {
+        inl ()
+      } {
+        getKeyL p x $ snd n
+      }
+    }
+  )
+end
+
+def containsKeyL : (a -> k) -> k -> List a -> Bool = \p.\x.\l.
+  case (getKeyL p x l) (\_. true) (\_. false)
+end
+
+// insert into ordered list - replaces elements, like set
+def insertKeyL : (a -> k) -> a -> List a -> List a = \p.\y.\l.
+  case l (\_. pureL y) (\n.
+    let nx = p (fst n) in
+    let x = p y in
+    if (nx == x) {
+      inr (y, snd n)
+    } {
+      if (nx > x) {
+        insertL y l
+      } {
+        inr (fst n, insertKeyL p y $ snd n)
+      }
+    }
+  )
+end
+
 def formatL : List a -> Text = \l.
  let f : List a -> Text = \l. case l (\_. "]") (\n. ", " ++ format (fst n) ++ f (snd n))
  in case l (\_. "[]") (\n. "[" ++ format (fst n) ++ f (snd n))
@@ -394,6 +431,15 @@ def test_empty: Int -> Cmd Unit = \i.
   )
 end
 
+def test_ordered_list : Int -> Cmd Unit = \i.
+  let s = [insert=insertKeyL (\x.x), contains=containsKeyL (\x.x)] in
+  group i "ORDERED LIST TESTS" (\i.
+    let expected = insertL 1 $ insertL 2 $ insertL 3 emptyL in
+    let actual = s.insert 2 $ s.insert 1 $ s.insert 3 emptyL in
+    assert_eq i (formatL expected) (formatL actual) "insertKeyL should insert in order";
+  )
+end
+
 def test_insert: Int -> Cmd Unit = \i.
   group i "INSERT TESTS" (\i.
     group i "test {0: 1}" (\i.
@@ -459,6 +505,7 @@ end
 def test_tree: Cmd Unit =
   group 0 "TREE TESTS" (\i.
     test_empty i;
+    test_ordered_list i;
     test_insert i;
     test_delete i;
   );

From eed6e477463b68deee7028a9b60053be77d7b3d8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Tue, 15 Oct 2024 15:27:00 +0200
Subject: [PATCH 14/22] rename

---
 example/dictionary.sw | 513 ------------------------------------------
 1 file changed, 513 deletions(-)
 delete mode 100644 example/dictionary.sw

diff --git a/example/dictionary.sw b/example/dictionary.sw
deleted file mode 100644
index 4fd562524..000000000
--- a/example/dictionary.sw
+++ /dev/null
@@ -1,513 +0,0 @@
-/*******************************************************************/
-/*                           CONTAINERS                            */
-/*******************************************************************/
-// This file has an example implementation of lists, sets and maps
-// (a.k.a dictionaries) using recursive types.
-//
-// The implementation uses a Red-Black tree balanced binary tree
-// with projection (k -> a) to get sets and dictionaries (compare
-// only first element of tuple). It is based on Haskell code in:
-// https://abhiroop.github.io/Haskell-Red-Black-Tree/
-
-tydef Maybe a = Unit + a end
-def mmap : (a -> b) -> Maybe a -> Maybe b = \f.\m. case m (\_. inl ()) (\a. inr (f a)) end
-
-/*******************************************************************/
-/*                              LISTS                              */
-/*******************************************************************/
-
-tydef List a = rec l. Maybe (a * l) end
-
-def emptyL : List a = inl () end
-def insertL : a -> List a -> List a = \a.\l. inr (a, l) end
-def pureL : a -> List a = \a. insertL a emptyL end
-
-def appendL : List a -> List a -> List a = \l.\r.
-  case l (\_. r) (\ln. inr (fst ln, appendL (snd ln) r))
-end
-
-def lengthL : List a -> Int =
-  let len: Int -> List a -> Int = \a.\l. case l (\_. a) (\ln. len (a + 1) (snd ln)) in len 0
-end 
-
-def safeGetL : Int -> List a -> Maybe a = \i.\l.
-  case l (\_. inl ()) (\n. if (i <= 0) {inr $ fst n} {safeGetL (i - 1) (snd n)})
-end 
-
-def getL : Int -> List a -> a = \i.\l.
-  case (safeGetL i l) (\_. fail $ "INDEX " ++ format i ++ " OUT OF BOUNDS!") (\a. a)
-end
-
-// get from ordered list
-def getKeyL : (a -> k) -> k -> List a -> Maybe a = \p.\x.\l.
-  case l (\_. inl ()) (\n.
-    let nx = p (fst n) in
-    if (nx == x) {
-      inr $ fst n
-    } {
-      if (nx < x) {
-        inl ()
-      } {
-        getKeyL p x $ snd n
-      }
-    }
-  )
-end
-
-def containsKeyL : (a -> k) -> k -> List a -> Bool = \p.\x.\l.
-  case (getKeyL p x l) (\_. true) (\_. false)
-end
-
-// insert into ordered list - replaces elements, like set
-def insertKeyL : (a -> k) -> a -> List a -> List a = \p.\y.\l.
-  case l (\_. pureL y) (\n.
-    let nx = p (fst n) in
-    let x = p y in
-    if (nx == x) {
-      inr (y, snd n)
-    } {
-      if (nx > x) {
-        insertL y l
-      } {
-        inr (fst n, insertKeyL p y $ snd n)
-      }
-    }
-  )
-end
-
-def formatL : List a -> Text = \l.
- let f : List a -> Text = \l. case l (\_. "]") (\n. ", " ++ format (fst n) ++ f (snd n))
- in case l (\_. "[]") (\n. "[" ++ format (fst n) ++ f (snd n))
-end
-
-/*******************************************************************/
-/*                         RED BLACK TREE                          */
-/*******************************************************************/
-
-tydef RBTree k = rec b. Maybe [red: Bool, k: k, l: b, r: b] end
-
-// equirecursive types allow us to get the node type without mutual recursion
-tydef RBNode k = rec n. [red: Bool, k: k, l: Maybe n, r: Maybe n] end
-
-def emptyT : RBTree k = inl () end
-
-def isEmptyT : RBTree k -> Bool = \d. d == emptyT end
-
-def getT : (k -> a) -> a -> RBTree k -> Maybe k = \p.\x.\t.
-  case t (\_. inl ()) (\n.
-    if (x == p n.k) { inr n.k } {
-        if (x < p n.k) {
-            getT p x n.l
-        } {
-            getT p x n.r
-        }
-    }
-  )
-end
-
-def containsT : (k -> a) -> a -> RBTree k -> Bool = \p.\x.\t. getT p x t != inl () end
-
-def inorder : RBTree k -> List k = \t.
-  case t (\_. inl ()) (\n.
-    appendL (inorder n.l) (appendL (pureL n.k) $ inorder n.r)
-  )
-end
-
-def formatT : RBTree k -> Text = \t.
-  case t (\_. "N") (\n.
-    "(T "
-    ++ if n.red {"R "} {"B "}
-    ++ formatT n.l ++ " " ++ format n.k ++ " " ++ formatT n.r ++ ")"
-  ) 
-end
-
-def indent_ = \c.\i. if (i <= 0) {" "} {c ++ indent_ c (i - 1)} end
-def indent = indent_ " " end
-
-def debugT : RBTree k -> Cmd Unit =
-  let d : Text -> Text -> Text -> RBTree k -> Cmd Unit = \i.\li.\ri.\t. case t (\_. log $ i ++ "+ N") (\n.
-    d (i ++ li) "  " "| " n.l;
-    log $ i ++ "+ " ++ if n.red {"R "} {"B "} ++ format n.k;
-    d (i ++ ri) "| " "  " n.r;
-  ) in d "" "" ""
-end
-
-/*
-balance B (T R (T R a x0 b) x1 c) x2 d = T R (T B a x0 b) x1 (T B c x2 d) -- case 1: LL red
-balance B (T R a x0 (T R b x1 c)) x2 d = T R (T B a x0 b) x1 (T B c x2 d) -- case 2: LR red
-balance B a x0 (T R (T R b x1 c) x2 d) = T R (T B a x0 b) x1 (T B c x2 d) -- case 3: RL red
-balance B a x0 (T R b x1 (T R c x2 d)) = T R (T B a x0 b) x1 (T B c x2 d) -- case 4: RR red
-balance color a x b = T color a x b -- case 5
-*/
-def balanceT : RBNode k -> RBTree k = \t.
-  let balanced : [ a: RBTree k, x0: k, b: RBTree k,   x1: k,   c: RBTree k, x2: k, d: RBTree k] -> RBTree k
-    = \v.
-    inr [red=true, l=inr [red=false, l=v.a, k=v.x0, r=v.b], k=v.x1, r=inr [red=false, l=v.c, k=v.x2, r=v.d]]
-  in let case5 : RBNode k -> RBTree k =
-    inr  // just id - TODO: inline?
-  in let balanceRR : RBNode k -> RBNode k -> RBTree k = \t.\rn.
-    case rn.r (\_. case5 t) (\rrn.
-      if rrn.red {
-        balanced [a=t.l, x0=t.k, b=rn.l, x1=rn.k, c=rrn.l, x2=rrn.k, d=rrn.r]
-      } {
-        case5 t
-      }
-    )
-  in let balanceRL : RBNode k -> RBNode k -> RBTree k = \t.\rn.
-    case rn.l (\_. balanceRR t rn) (\rln.
-      if rln.red {
-        balanced [a=t.l, x0=t.k, b=rln.l, x1=rln.k, c=rln.r, x2=rn.k, d=rn.r]
-      } {
-        balanceRR t rn
-      }
-    )
-  in let balanceR : RBNode k -> RBTree k = \t.
-    case t.r (\_.
-      case5 t
-    ) (\lr.
-      if lr.red {
-        balanceRL t lr
-      } {
-        case5 t
-      }
-    )
-  in let balanceLR : RBNode k -> RBNode k -> RBTree k = \t.\ln.
-    case ln.r (\_. balanceR t) (\lrn.
-      if lrn.red {
-        balanced [a=ln.l, x0=ln.k, b=lrn.l, x1=lrn.k, c=lrn.r, x2=t.k, d=t.r]
-      } {
-        balanceR t
-      }
-    )
-  in let balanceLL : RBNode k -> RBNode k -> RBTree k = \t.\ln.
-    case ln.l (\_. balanceLR t ln) (\lln.
-      if lln.red {
-        balanced [a=lln.l, x0=lln.k, b=lln.r, x1=ln.k, c=ln.r, x2=t.k, d=t.r]
-      } {
-        balanceLR t ln
-      }
-    )
-  in let balanceL : RBNode k -> RBTree k = \t.
-    case t.l (\_.
-      balanceR t
-    ) (\ln.
-      if ln.red {
-        balanceLL t ln
-      } {
-        balanceR t
-      }
-    )
-  in if t.red {
-    case5 t
-  } {
-    balanceL t
-  }
-end
-
-def insertT : (k -> a) -> k -> RBTree k -> RBTree k = \p.\x.\t.
-  let ins : (k -> a) -> k -> RBTree k -> RBTree k =\p.\x.\t. case t
-    (\_.
-      inr [red=true, k=x, l=inl (), r=inl ()]
-    ) (\n.
-      if (p x == p n.k) { inr [red=n.red, k=x, l=n.l, r=n.r] } {
-        if (x < n.k) {
-            balanceT [red=n.red, k=n.k, l=ins p x n.l, r=n.r]
-        } {
-            balanceT [red=n.red, k=n.k, l=n.l, r=ins p x n.r]
-        }
-      }
-    )
-  in let makeBlack : RBTree k -> RBTree k = \t. case t (\_.
-        fail "makeBlack will always be called on nonempty"
-      ) (\n.
-        inr [red=false, k=n.k, l=n.l, r=n.r]
-      )
-  in makeBlack $ ins p x t
-end
-
-def deleteT : (k -> a) -> a -> RBTree k -> RBTree k = \p.\x.\t.
-  // ------------------------------------------------------------------------------------------------------------
-  tydef Del k a = (k -> a) -> a -> RBTree k -> RBTree k end
-  // ------------------------------------------------------------------------------------------------------------
-  let makeBlack : RBTree k -> RBTree k = \t.
-    case t (\_. t) (\n. inr [red=false, k=n.k, l=n.l, r=n.r])
-  in let makeRed : RBNode k -> RBTree k = \n.
-    inr [red=true, k=n.k, l=n.l, r=n.r]
-  // ------------------------------------------------------------------------------------------------------------
-  /*
-  balL (T B (T R t1 x t2) y t3) = T R (T B t1 x t2) y t3
-  balL (T B t1 y (T B t2 z t3)) = balance' (T B t1 y (T R t2 z t3))
-  balL (T B t1 y (T R (T B t2 u t3) z t4@(T B l value r)))
-    = T R
-      (T B t1 y t2)
-      u
-      (balance' (T B t3 z
-        (T R l value r)))
-  */
-  in let balL : RBNode k -> RBTree k = \n.
-    let balL2 : RBNode k -> RBNode k -> RBTree k = \n.\rn.
-      case rn.l (\_. inr n) (\rln.
-        if rln.red {inr n} {
-          case rn.r (\_. inr n) (\rrn.
-            if rrn.red {inr n} {
-              inr [red=true,
-                   l=inr [red=false, l=n.l, k=n.k, r=rln.l],
-                   k=rln.k,
-                   r=balanceT [red=false, l=rln.r, k=rn.k, r=inr [red=true, l=rrn.l, k=rrn.k, r=rrn.r]]]
-            }
-          )
-        }
-      )
-    in let balL1 : RBNode k -> RBTree k = \n.
-      case n.r (\_. inr n) (\rn. 
-        if rn.red {balL2 n rn} {balanceT [red=false, k=n.k, l=n.l, r=makeRed rn]}
-      )
-    in case n.l (\_. balL1 n) (\ln. if ln.red {inr [red=true, k=n.k, l=makeBlack n.l, r=n.r]} {balL1 n})
-  // ------------------------------------------------------------------------------------------------------------
-  /*
-  balR (T B t1 y (T R t2 x t3)) = T R t1 y (T B t2 x t3)
-  balR (T B (T B t1 z t2) y t3) = balance' (T B (T R t1 z t2) y t3)
-  balR (T B
-    ln@(T R
-      lln@(T B lll llk llr)
-      lk
-      lrn@(T B lrl lrk lrr))
-    k
-    rn)
-    =
-    T R
-      (balance' (T B (T R lll llk llr) lk lrl))
-      lrk
-      (T B lrr k rn)
-  */
-  in let balR : RBNode k -> RBTree k = \n.
-    let balR2 : RBNode k -> RBNode k -> RBTree k = \n.\ln.
-      case ln.l (\_. inr n) (\lln.
-        if lln.red {inr n} {
-          case ln.r (\_. inr n) (\lrn.
-            if lrn.red {inr n} {
-              inr [red=true,
-                   l=balanceT [red=false, l=inr [red=true, l=lln.l, k=lln.k, r=lln.r], k=ln.k, r=lrn.l],
-                   k=lrn.k,
-                   r=inr [red=false, l=lrn.r, k=n.k, r=n.r]]
-            }
-          )
-        }
-      )
-    in let balR1 : RBNode k -> RBTree k = \n.
-      case n.l (\_. inr n) (\ln. 
-        if ln.red {balR2 n ln} {balanceT [red=false, k=n.k, l=makeRed ln, r=n.r]}
-      )
-    in case n.r (\_. balR1 n) (\rn. if rn.red {inr [red=true, k=n.k, l=n.l, r=makeBlack n.r]} {balR1 n})
-  // ------------------------------------------------------------------------------------------------------------
-  in let delL : Del k a -> (k -> a) -> a -> RBNode k -> RBTree k = \del.\p.\x.\n.
-    let dl = [red=n.red, k=n.k, l=del p x n.l, r=n.r] in
-    if n.red { inr dl } { balL dl }
-  // ------------------------------------------------------------------------------------------------------------
-  in let delR : Del k a -> (k -> a) -> a -> RBNode k -> RBTree k = \del.\p.\x.\n.
-    let dr = [red=n.red, k=n.k, l=n.l, r=del p x n.r] in
-    if n.red { inr dr } { balR dr }
-  // ------------------------------------------------------------------------------------------------------------
-  /*
-  fuse E t = t
-  fuse t E = t
-  fuse t1@(T B _ _ _) (T R t3 y t4) = T R (fuse t1 t3) y t4
-  fuse (T R t1 x t2) t3@(T B _ _ _) = T R t1 x (fuse t2 t3)
-  fuse (T R t1 x t2) (T R t3 y t4)  =
-    let s = fuse t2 t3
-    in case s of
-        (T R s1 z s2) -> (T R (T R t1 x s1) z (T R s2 y t4))
-        (T B _ _ _)   -> (T R t1 x (T R s y t4))
-  fuse (T B t1 x t2) (T B t3 y t4)  =
-    let s = fuse t2 t3
-    in case s of
-        (T R s1 z s2) -> (T R (T B t1 x s1) z (T B s2 y t4))
-        (T B s1 z s2) -> balL (T B t1 x (T B s y t4))
-  */
-  in let fuse: RBTree k -> RBTree k -> RBTree k = \l.\r.
-    case l (\_. r) (\ln. case r (\_. l) (\rn.
-      if ln.red {
-        if rn.red {
-          /* RED RED */
-          let s = fuse ln.r rn.l in
-          let b_case = {inr [red=true, l=ln.l, k=ln.k, r=inr [red=true, l=s, k=rn.k, r=rn.r]]} in
-          case s (\_. force b_case) (\sn.
-            if sn.red {
-              inr [red=true, l=inr [red=true, l=ln.l, k=ln.k, r=sn.l], k=sn.k, r=inr [red=true, l=sn.r, k=rn.k, r=rn.r]]
-            } {
-              force b_case
-            }
-          ) 
-        } {
-          /* RED BLACK */
-          inr [red=true, l=ln.l, k=ln.k, r=fuse ln.r (inr rn)]
-        }
-      } {
-        if rn.red {
-          /* BLACK RED */
-          inr [red=true, l=fuse (inr ln) rn.l, k=rn.k, r=rn.r]
-        } {
-          /* BLACK BLACK */
-          let s = fuse ln.r rn.l in
-          let b_case = {balL [red=false, l=ln.l, k=ln.k, r=inr [red=false, l=s, k=rn.k, r=rn.r]]} in
-          case s (\_. force b_case) (\sn.
-            if sn.red {
-              inr [red=true, l=inr [red=false, l=ln.l, k=ln.k, r=sn.l], k=sn.k, r=inr [red=false, l=sn.r, k=rn.k, r=rn.r]]
-            } {
-              force b_case
-            }
-          )
-        }
-      }
-    ))
-  // ------------------------------------------------------------------------------------------------------------
-  in let del : (k -> a) -> a -> RBTree k -> RBTree k = \p.\x.\t.
-    case t (\_.t) (\n. 
-      if (p n.k == x) {fuse n.l n.r} {
-        if (x < p n.k) {delL del p x n} {delR del p x n}
-      }
-    )
-  // ------------------------------------------------------------------------------------------------------------
-  in makeBlack $ del p x t
-end
-
-/*******************************************************************/
-/*                           DICTIONARY                            */
-/*******************************************************************/
-
-tydef Dict k v = RBTree (k * v) end
-
-def emptyD : Dict k v = emptyT end
-def isEmptyD : Dict k v -> Bool = isEmptyT end
-def getD : k -> Dict k v -> Maybe v = \k.\d. mmap snd (getT fst k d) end 
-def containsD : k -> Dict k v -> Bool = containsT fst end
-def insertD : k -> v -> Dict k v -> Dict k v = \k.\v. insertT fst (k, v) end
-def deleteD : k -> Dict k v -> Dict k v = \k. deleteT fst k end
-
-def formatD : Dict k v -> Text = \d.
- let p : (k * v) -> Text = \kv. format (fst kv) ++ ": " ++ format (snd kv) in 
- let f : List (k * v) -> Text = \l. case l (\_. "}") (\n. ", " ++ p (fst n) ++ f (snd n))
- in case (inorder d) (\_. "{}") (\n. "{" ++ p (fst n) ++ f (snd n))
-end
-
-/*******************************************************************/
-/*                              SET                                */
-/*******************************************************************/
-
-tydef Set k = RBTree k end
-
-def emptyS : Set k = emptyT end
-def isEmptyS : Set k -> Bool = isEmptyT end
-def containsS : k -> Set k -> Bool = containsT (\x.x) end
-def insertS : k -> Set k -> Set k = insertT (\x.x) end
-def deleteS : k -> Set k -> Set k = \k. deleteT (\x.x) k end
-def formatS : Set k -> Text = \s. formatL $ inorder s end
-
-/*******************************************************************/
-/*                           UNIT TESTS                            */
-/*******************************************************************/
-
-def assert = \i. \b. \m. if b {log $ indent i ++ "OK: " ++ m} {log "FAIL:"; fail m} end
-
-def assert_eq 
-  = \i. \exp. \act. \m.
-  if (exp == act) {log $ indent i ++ "OK: " ++ m} {
-    log (indent i ++ "FAIL: expected " ++ format exp ++ " actual " ++ format act);
-    fail m
-  }
-end
-
-def group = \i. \m. \tests.
-  log $ indent i ++ "START " ++ m ++ ":";
-  tests $ i + 1;
-  return ()
-end
-
-def test_empty: Int -> Cmd Unit = \i.
-  group i "EMPTY TESTS" (\i.
-    assert i (isEmptyD emptyD) "empty tree should be empty";
-    assert_eq i (inl ()) (getD 0 $ emptyD) "no element should be present in an empty tree";
-    assert i (not $ containsD 0 $ emptyD) "empty tree should not contain any elements";
-  )
-end
-
-def test_ordered_list : Int -> Cmd Unit = \i.
-  let s = [insert=insertKeyL (\x.x), contains=containsKeyL (\x.x)] in
-  group i "ORDERED LIST TESTS" (\i.
-    let expected = insertL 1 $ insertL 2 $ insertL 3 emptyL in
-    let actual = s.insert 2 $ s.insert 1 $ s.insert 3 emptyL in
-    assert_eq i (formatL expected) (formatL actual) "insertKeyL should insert in order";
-  )
-end
-
-def test_insert: Int -> Cmd Unit = \i.
-  group i "INSERT TESTS" (\i.
-    group i "test {0: 1}" (\i.
-      let tree0 = insertD 0 1 emptyD in
-      assert i (not $ isEmptyD tree0) "nonempty tree should not be empty";
-      assert_eq i (inr 1) (getD 0 $ tree0) "one element should be present in a one element tree";
-      assert i (containsD 0 $ tree0) "one element tree should contain that elements";
-      assert i (not $ containsD 1 $ tree0) "one element tree should contain only that elements";
-    );
-    group i "test {0: 1, 2: 3}" (\i.
-      let tree02 = insertD 2 3 $ insertD 0 1 emptyD in
-      assert_eq i (inr 1) (getD 0 $ tree02) "get 0 {0: 1, 2: 3} == 1";
-      assert_eq i (inr 3) (getD 2 $ tree02) "get 2 {0: 1, 2: 3} == 3";
-    );
-  );
-end
-
-def randomTestS = \i.\s.\test.
-  if (i <= 0) {return s} {
-    x <- random 20;
-    let ns = insertS x s in
-    test ns;
-    randomTestS (i - 1) ns test
-  }
-end
-
-def delete_insert_prop = \i.\t.
-  x <- random 20;
-  let i_t = inorder t in
-  let f_t = formatS t in
-  if (not $ containsS x t) {
-    log $ format x;
-    assert_eq i
-      (formatL i_t)
-      (formatS $ deleteS x $ insertS x t)
-      (f_t ++ " == delete " ++ format x ++ " $ insert " ++ format x ++ " " ++ f_t)
-  } { delete_insert_prop i t /* reroll */}
-end
-
-def delete_delete_prop = \i.\t.
-  let i_t = inorder t in
-  i <- random (lengthL i_t);
-  let x = getL i i_t in
-  let ds = deleteS x t in
-  let dds = deleteS x ds in
-  let f_t = formatS t in
-  let f_dx = "delete " ++ format x in
-  assert_eq i (formatS ds) (formatS dds)
-    (f_dx ++ f_t ++ " == " ++ f_dx ++ " $ " ++ f_dx ++ " " ++ f_t)
-end
-
-def test_delete: Int -> Cmd Unit = \i.
-  group i "DELETE TESTS" (\i.
-    randomTestS 15 emptyS (\s.
-      group i (formatS s) (\i.
-        delete_insert_prop i s;
-        delete_delete_prop i s;
-      )
-    )
-  )
-end
-
-def test_tree: Cmd Unit =
-  group 0 "TREE TESTS" (\i.
-    test_empty i;
-    test_ordered_list i;
-    test_insert i;
-    test_delete i;
-  );
-  log "ALL TREE TESTS PASSED!"
-end
\ No newline at end of file

From e2d846163f784ddf31c2ca3e572eda60a22ab288 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Sat, 19 Oct 2024 16:15:20 +0200
Subject: [PATCH 15/22] wip

---
 example/recursive-containers.sw | 203 +++++++++++++++++++++++++++++---
 1 file changed, 189 insertions(+), 14 deletions(-)

diff --git a/example/recursive-containers.sw b/example/recursive-containers.sw
index 4fd562524..2d28ac490 100644
--- a/example/recursive-containers.sw
+++ b/example/recursive-containers.sw
@@ -19,16 +19,30 @@ def mmap : (a -> b) -> Maybe a -> Maybe b = \f.\m. case m (\_. inl ()) (\a. inr
 tydef List a = rec l. Maybe (a * l) end
 
 def emptyL : List a = inl () end
-def insertL : a -> List a -> List a = \a.\l. inr (a, l) end
-def pureL : a -> List a = \a. insertL a emptyL end
+def cons : a -> List a -> List a = \a.\l. inr (a, l) end
+def pureL : a -> List a = \a. cons a emptyL end
 
-def appendL : List a -> List a -> List a = \l.\r.
-  case l (\_. r) (\ln. inr (fst ln, appendL (snd ln) r))
+def foldr : (a -> b -> b) -> b -> List a -> b = \f. \z. \xs.
+  case xs
+    (\_. z)
+    (\c. f (fst c) (foldr f z (snd c)))
 end
 
-def lengthL : List a -> Int =
-  let len: Int -> List a -> Int = \a.\l. case l (\_. a) (\ln. len (a + 1) (snd ln)) in len 0
-end 
+def foldl : (b -> a -> b) -> b -> List a -> b = \f. \z. \xs.
+  case xs
+    (\_. z)
+    (\c. (foldl f (f z $ fst c) (snd c)))
+end
+
+def map : (a -> b) -> List a -> List b = \f.
+  foldr (\y. cons (f y)) emptyL
+end
+
+def appendL : List a -> List a -> List a = \xs. \ys.
+  foldr cons ys xs
+end
+
+def lengthL : List a -> Int = foldl (\acc.\_. acc + 1) 0 end 
 
 def safeGetL : Int -> List a -> Maybe a = \i.\l.
   case l (\_. inl ()) (\n. if (i <= 0) {inr $ fst n} {safeGetL (i - 1) (snd n)})
@@ -38,6 +52,11 @@ def getL : Int -> List a -> a = \i.\l.
   case (safeGetL i l) (\_. fail $ "INDEX " ++ format i ++ " OUT OF BOUNDS!") (\a. a)
 end
 
+def formatL : List a -> Text = \l.
+ let f : List a -> Text = \l. case l (\_. "]") (\n. ", " ++ format (fst n) ++ f (snd n))
+ in case l (\_. "[]") (\n. "[" ++ format (fst n) ++ f (snd n))
+end
+
 // get from ordered list
 def getKeyL : (a -> k) -> k -> List a -> Maybe a = \p.\x.\l.
   case l (\_. inl ()) (\n.
@@ -67,17 +86,60 @@ def insertKeyL : (a -> k) -> a -> List a -> List a = \p.\y.\l.
       inr (y, snd n)
     } {
       if (nx > x) {
-        insertL y l
+        cons y l
       } {
-        inr (fst n, insertKeyL p y $ snd n)
+        cons (fst n) (insertKeyL p y $ snd n)
       }
     }
   )
 end
 
-def formatL : List a -> Text = \l.
- let f : List a -> Text = \l. case l (\_. "]") (\n. ", " ++ format (fst n) ++ f (snd n))
- in case l (\_. "[]") (\n. "[" ++ format (fst n) ++ f (snd n))
+// delete in ordered list
+def deleteKeyL : (a -> k) -> k -> List a -> List a = \p.\x.\l.
+  case l (\_. emptyL) (\n.
+    let nx = p (fst n) in
+    if (nx == x) {
+      snd n
+    } {
+      if (nx > x) {
+        l
+      } {
+        cons (fst n) (deleteKeyL p x $ snd n)
+      }
+    }
+  )
+end
+
+tydef FlatSet a = List a end
+
+def flat_set :
+  [ empty: FlatSet a
+  , insert: a -> FlatSet a -> FlatSet a 
+  , delete: a -> FlatSet a -> FlatSet a 
+  , contains: a -> FlatSet a -> Bool
+  ] =
+  [ empty=emptyL
+  , insert=insertKeyL (\x.x)
+  , delete=deleteKeyL (\x.x)
+  , contains=containsKeyL (\x.x)
+  ]
+end
+
+tydef FlatDict k v = List (k * v) end
+
+def flat_dict :
+  [ empty: FlatDict k v
+  , insert: k -> v -> FlatDict k v -> FlatDict k v
+  , delete: k -> FlatDict k v -> FlatDict k v
+  , get: k -> FlatDict k v -> Maybe v
+  , contains: k -> FlatDict k v -> Bool
+  ] =
+  [ empty=emptyL
+  , insert=\k.\v. insertKeyL fst (k,v)
+  , delete=deleteKeyL fst
+  , get=\k.\d. mmap snd (getKeyL fst k d)
+  , contains=containsKeyL fst
+  ]
 end
 
 /*******************************************************************/
@@ -403,6 +465,19 @@ def insertS : k -> Set k -> Set k = insertT (\x.x) end
 def deleteS : k -> Set k -> Set k = \k. deleteT (\x.x) k end
 def formatS : Set k -> Text = \s. formatL $ inorder s end
 
+def tree_set :
+  [ empty: Set a
+  , insert: a -> Set a -> Set a 
+  , delete: a -> Set a -> Set a 
+  , contains: a -> Set a -> Bool
+  ] =
+  [ empty=emptyT
+  , insert=insertT (\x.x)
+  , delete=deleteT (\x.x)
+  , contains=containsT (\x.x)
+  ]
+end
+
 /*******************************************************************/
 /*                           UNIT TESTS                            */
 /*******************************************************************/
@@ -434,7 +509,7 @@ end
 def test_ordered_list : Int -> Cmd Unit = \i.
   let s = [insert=insertKeyL (\x.x), contains=containsKeyL (\x.x)] in
   group i "ORDERED LIST TESTS" (\i.
-    let expected = insertL 1 $ insertL 2 $ insertL 3 emptyL in
+    let expected = cons 1 $ cons 2 $ cons 3 emptyL in
     let actual = s.insert 2 $ s.insert 1 $ s.insert 3 emptyL in
     assert_eq i (formatL expected) (formatL actual) "insertKeyL should insert in order";
   )
@@ -510,4 +585,104 @@ def test_tree: Cmd Unit =
     test_delete i;
   );
   log "ALL TREE TESTS PASSED!"
-end
\ No newline at end of file
+end
+
+/*******************************************************************/
+/*                           BENCHMARKS                            */
+/*******************************************************************/
+
+def benchmark: Int -> s -> (s -> s) -> Cmd (Int * (Int * Int)) = \times.\s.\act.
+  let min = \x.\y. if (x > y) {y} {x} in
+  let max = \x.\y. if (x > y) {x} {y} in
+  let runM = \acc.\s.\n.
+    if (n <= 0) {
+      log "return";
+      return acc
+    } {
+      t0 <- time;
+      log $ "START " ++ format t0;
+      let ns = act s in
+      t1 <- time;
+      log $ "END " ++ format t1;
+      log "what?";
+      log $ format t1;
+      //log $ format t0;
+      //log $ format $ t1 - t0;
+      let t = t1 in
+      log "end 2";
+      let lim = case (snd acc) (\_. (t, t)) (\l. (min t $ fst l, max t $ snd l)) in
+      log "end 3";
+      runM ((fst acc + t), lim) ns (n - 1)
+    } in
+  log "start run";
+  res <- runM (0, inl ()) s times;
+  log "end run";
+  let avg = fst res / times in
+  let lim = case (snd res) (\_. fail "BENCHMARK NOT RUN") (\l.l) in
+  return (avg, lim)
+end
+
+def cmp_bench = \i.\base_name.\base_res.\new_name.\new_res.
+  let formatLim = \l. format ("min " ++ format (fst l), "max " ++ format (snd l)) in
+  log $ indent i ++ "* " ++ base_name ++ ": "
+    ++ format (fst base_res) ++ " ticks " ++ formatLim (snd base_res);
+
+  let d = (fst new_res * 100) / fst base_res in
+  let cmp = if (d > 100) {
+     format (d - 100) ++ "% slower"
+    } {
+      format (100 - d) ++ "% faster"
+    } in
+     
+  log $ indent i ++ "* " ++ new_name ++ ": "
+    ++ format (fst new_res) ++ " ticks " ++ formatLim (snd new_res)
+    ++ " <- " ++ cmp;
+end
+
+def gen_random_list = 
+  let gen = \acc.\n.\rlim.
+    if (n <= 0) { return acc } {
+      x <- random rlim;
+      gen (cons x acc) (n - 1) rlim
+    }
+  in gen emptyL
+end
+
+def gen_random_lists = \m.\n.\rlim.
+  let gen = \acc.\m.
+    if (m <= 0) { return acc } {
+      l <- gen_random_list n rlim;
+      gen (cons l acc) (m - 1)
+    }
+  in gen emptyL m
+end
+
+def set_from_first_list : forall a s. s -> (a -> s -> s) -> List (List a) -> List (List a) =\e.\ins.\lls.
+  case lls (\_. lls) (\ls_nlls.
+    let ls = fst ls_nlls in
+    let ns = foldl (\s.\a.ins a s) e ls in
+    let nlls = snd ls_nlls in
+    nlls
+  )
+end
+
+def bench_insert = \i.
+  group i "INSERT BENCHMARK" (\i.
+    group i "INSERT 2" (\i.
+      let n = 2 in
+      let m = 2 in
+      lls10 <- gen_random_lists m n (3 * n);
+      flat_res <- benchmark m lls10 (set_from_first_list flat_set.empty flat_set.insert);
+      tree_res <- benchmark m lls10 (set_from_first_list tree_set.empty tree_set.insert);
+      cmp_bench i "flat set" flat_res "tree set" tree_res
+    );
+    group i "INSERT 5" (\i.
+      let n = 5 in
+      let m = 2 in
+      lls10 <- gen_random_lists m n (3 * n);
+      flat_res <- benchmark m lls10 (set_from_first_list flat_set.empty flat_set.insert);
+      tree_res <- benchmark m lls10 (set_from_first_list tree_set.empty tree_set.insert);
+      cmp_bench i "flat set" flat_res "tree set" tree_res
+    )
+  )
+end

From 53cbc54236c830a82b2ccab24488748bbd9d7b82 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Sat, 19 Oct 2024 16:15:35 +0200
Subject: [PATCH 16/22] remove min/max statistics to debug

---
 example/recursive-containers.sw | 27 ++++++++++-----------------
 1 file changed, 10 insertions(+), 17 deletions(-)

diff --git a/example/recursive-containers.sw b/example/recursive-containers.sw
index 2d28ac490..7de22a2df 100644
--- a/example/recursive-containers.sw
+++ b/example/recursive-containers.sw
@@ -591,12 +591,11 @@ end
 /*                           BENCHMARKS                            */
 /*******************************************************************/
 
-def benchmark: Int -> s -> (s -> s) -> Cmd (Int * (Int * Int)) = \times.\s.\act.
+def benchmark: Int -> s -> (s -> s) -> Cmd (Int ) = \times.\s.\act. /* * (Int * Int) */
   let min = \x.\y. if (x > y) {y} {x} in
   let max = \x.\y. if (x > y) {x} {y} in
   let runM = \acc.\s.\n.
     if (n <= 0) {
-      log "return";
       return acc
     } {
       t0 <- time;
@@ -604,30 +603,24 @@ def benchmark: Int -> s -> (s -> s) -> Cmd (Int * (Int * Int)) = \times.\s.\act.
       let ns = act s in
       t1 <- time;
       log $ "END " ++ format t1;
-      log "what?";
-      log $ format t1;
-      //log $ format t0;
-      //log $ format $ t1 - t0;
-      let t = t1 in
-      log "end 2";
-      let lim = case (snd acc) (\_. (t, t)) (\l. (min t $ fst l, max t $ snd l)) in
-      log "end 3";
-      runM ((fst acc + t), lim) ns (n - 1)
+      let t = t1 - t0 in
+      //let lim = case (snd acc) (\_. (t, t)) (\l. (min t $ fst l, max t $ snd l)) in
+      runM ((fst acc + t) /*, lim */) ns (n - 1)
     } in
   log "start run";
   res <- runM (0, inl ()) s times;
   log "end run";
   let avg = fst res / times in
-  let lim = case (snd res) (\_. fail "BENCHMARK NOT RUN") (\l.l) in
-  return (avg, lim)
+  // let lim = case (snd res) (\_. fail "BENCHMARK NOT RUN") (\l.l) in
+  return avg // (avg, lim)
 end
 
 def cmp_bench = \i.\base_name.\base_res.\new_name.\new_res.
-  let formatLim = \l. format ("min " ++ format (fst l), "max " ++ format (snd l)) in
+  //let formatLim = \l. format ("min " ++ format (fst l), "max " ++ format (snd l)) in
   log $ indent i ++ "* " ++ base_name ++ ": "
-    ++ format (fst base_res) ++ " ticks " ++ formatLim (snd base_res);
+    ++ format (base_res) ++ " ticks "; //++ formatLim (snd base_res);
 
-  let d = (fst new_res * 100) / fst base_res in
+  let d = (new_res * 100) / base_res in
   let cmp = if (d > 100) {
      format (d - 100) ++ "% slower"
     } {
@@ -635,7 +628,7 @@ def cmp_bench = \i.\base_name.\base_res.\new_name.\new_res.
     } in
      
   log $ indent i ++ "* " ++ new_name ++ ": "
-    ++ format (fst new_res) ++ " ticks " ++ formatLim (snd new_res)
+    ++ format (new_res) ++ " ticks "// ++ formatLim (snd new_res)
     ++ " <- " ++ cmp;
 end
 

From 59c1a4e6784f39e729a9b1d5866e37dfc18e4d15 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Sat, 19 Oct 2024 17:19:40 +0200
Subject: [PATCH 17/22] comment out last parts of min max statistic

---
 example/recursive-containers.sw | 32 ++++++++++++++++----------------
 1 file changed, 16 insertions(+), 16 deletions(-)

diff --git a/example/recursive-containers.sw b/example/recursive-containers.sw
index 7de22a2df..fe9a06cbc 100644
--- a/example/recursive-containers.sw
+++ b/example/recursive-containers.sw
@@ -599,18 +599,18 @@ def benchmark: Int -> s -> (s -> s) -> Cmd (Int ) = \times.\s.\act. /* * (Int *
       return acc
     } {
       t0 <- time;
-      log $ "START " ++ format t0;
+      //log $ "START " ++ format t0;
       let ns = act s in
       t1 <- time;
-      log $ "END " ++ format t1;
+      //log $ "END " ++ format t1;
       let t = t1 - t0 in
       //let lim = case (snd acc) (\_. (t, t)) (\l. (min t $ fst l, max t $ snd l)) in
-      runM ((fst acc + t) /*, lim */) ns (n - 1)
+      runM ((acc + t) /*, lim */) ns (n - 1)
     } in
-  log "start run";
-  res <- runM (0, inl ()) s times;
-  log "end run";
-  let avg = fst res / times in
+  //log "start run";
+  res <- runM 0 s times;
+  //log "end run";
+  let avg = res / times in
   // let lim = case (snd res) (\_. fail "BENCHMARK NOT RUN") (\l.l) in
   return avg // (avg, lim)
 end
@@ -661,20 +661,20 @@ end
 
 def bench_insert = \i.
   group i "INSERT BENCHMARK" (\i.
-    group i "INSERT 2" (\i.
-      let n = 2 in
-      let m = 2 in
+    group i "INSERT 10" (\i.
+      let n = 10 in
+      let m = 5 in
       lls10 <- gen_random_lists m n (3 * n);
       flat_res <- benchmark m lls10 (set_from_first_list flat_set.empty flat_set.insert);
       tree_res <- benchmark m lls10 (set_from_first_list tree_set.empty tree_set.insert);
       cmp_bench i "flat set" flat_res "tree set" tree_res
     );
-    group i "INSERT 5" (\i.
-      let n = 5 in
-      let m = 2 in
-      lls10 <- gen_random_lists m n (3 * n);
-      flat_res <- benchmark m lls10 (set_from_first_list flat_set.empty flat_set.insert);
-      tree_res <- benchmark m lls10 (set_from_first_list tree_set.empty tree_set.insert);
+    group i "INSERT 100" (\i.
+      let n = 100 in
+      let m = 3 in
+      lls100 <- gen_random_lists m n (3 * n);
+      flat_res <- benchmark m lls100 (set_from_first_list flat_set.empty flat_set.insert);
+      tree_res <- benchmark m lls100 (set_from_first_list tree_set.empty tree_set.insert);
       cmp_bench i "flat set" flat_res "tree set" tree_res
     )
   )

From a8874783e5b5bd5fc5fefa08325d5702c608dc70 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Sat, 19 Oct 2024 23:42:22 +0200
Subject: [PATCH 18/22] add back limits and new contains benchmark

---
 example/recursive-containers.sw | 114 +++++++++++++++++++++++---------
 1 file changed, 82 insertions(+), 32 deletions(-)

diff --git a/example/recursive-containers.sw b/example/recursive-containers.sw
index fe9a06cbc..0908c0b8e 100644
--- a/example/recursive-containers.sw
+++ b/example/recursive-containers.sw
@@ -34,6 +34,8 @@ def foldl : (b -> a -> b) -> b -> List a -> b = \f. \z. \xs.
     (\c. (foldl f (f z $ fst c) (snd c)))
 end
 
+def flip : (a -> b -> c) -> (b -> a -> c) = \f. (\b.\a.f a b) end
+
 def map : (a -> b) -> List a -> List b = \f.
   foldr (\y. cons (f y)) emptyL
 end
@@ -57,6 +59,10 @@ def formatL : List a -> Text = \l.
  in case l (\_. "[]") (\n. "[" ++ format (fst n) ++ f (snd n))
 end
 
+/*******************************************************************/
+/*                          ORDERED LISTS                          */
+/*******************************************************************/
+
 // get from ordered list
 def getKeyL : (a -> k) -> k -> List a -> Maybe a = \p.\x.\l.
   case l (\_. inl ()) (\n.
@@ -117,11 +123,13 @@ def flat_set :
   , insert: a -> FlatSet a -> FlatSet a 
   , delete: a -> FlatSet a -> FlatSet a 
   , contains: a -> FlatSet a -> Bool
+  , from_list: List a -> FlatSet a
   ] =
   [ empty=emptyL
   , insert=insertKeyL (\x.x)
   , delete=deleteKeyL (\x.x)
   , contains=containsKeyL (\x.x)
+  , from_list=foldl (flip $ insertKeyL (\x.x)) emptyL
   ]
 end
 
@@ -470,11 +478,13 @@ def tree_set :
   , insert: a -> Set a -> Set a 
   , delete: a -> Set a -> Set a 
   , contains: a -> Set a -> Bool
+  , from_list: List a -> Set a
   ] =
   [ empty=emptyT
   , insert=insertT (\x.x)
   , delete=deleteT (\x.x)
   , contains=containsT (\x.x)
+  , from_list=foldl (flip $ insertT (\x.x)) emptyT
   ]
 end
 
@@ -532,7 +542,7 @@ def test_insert: Int -> Cmd Unit = \i.
   );
 end
 
-def randomTestS = \i.\s.\test.
+def randomTestS: Int -> Set Int -> (Set Int -> Cmd a) -> Cmd (Set Int) = \i.\s.\test.
   if (i <= 0) {return s} {
     x <- random 20;
     let ns = insertS x s in
@@ -541,7 +551,7 @@ def randomTestS = \i.\s.\test.
   }
 end
 
-def delete_insert_prop = \i.\t.
+def delete_insert_prop: Int -> Set Int -> Cmd Unit = \i.\t.
   x <- random 20;
   let i_t = inorder t in
   let f_t = formatS t in
@@ -554,10 +564,10 @@ def delete_insert_prop = \i.\t.
   } { delete_insert_prop i t /* reroll */}
 end
 
-def delete_delete_prop = \i.\t.
+def delete_delete_prop: Int -> Set a -> Cmd Unit = \i.\t.
   let i_t = inorder t in
-  i <- random (lengthL i_t);
-  let x = getL i i_t in
+  ix <- random (lengthL i_t);
+  let x = getL ix i_t in
   let ds = deleteS x t in
   let dds = deleteS x ds in
   let f_t = formatS t in
@@ -591,10 +601,10 @@ end
 /*                           BENCHMARKS                            */
 /*******************************************************************/
 
-def benchmark: Int -> s -> (s -> s) -> Cmd (Int ) = \times.\s.\act. /* * (Int * Int) */
+def benchmark: Int -> s -> (s -> s) -> Cmd (Int * (Int * Int)) = \times.\s.\act.
   let min = \x.\y. if (x > y) {y} {x} in
   let max = \x.\y. if (x > y) {x} {y} in
-  let runM = \acc.\s.\n.
+  let runM: (Int * Maybe (Int * Int)) -> s -> Int -> Cmd (Int * Maybe (Int * Int)) = \acc.\s.\n.
     if (n <= 0) {
       return acc
     } {
@@ -604,23 +614,25 @@ def benchmark: Int -> s -> (s -> s) -> Cmd (Int ) = \times.\s.\act. /* * (Int *
       t1 <- time;
       //log $ "END " ++ format t1;
       let t = t1 - t0 in
-      //let lim = case (snd acc) (\_. (t, t)) (\l. (min t $ fst l, max t $ snd l)) in
-      runM ((acc + t) /*, lim */) ns (n - 1)
+      log $ format s ++ " " ++ format t ++ " ticks";
+      let lim = case (snd acc) (\_. (t, t)) (\l. (min t $ fst l, max t $ snd l)) in
+      runM ((fst acc + t), inr lim) ns (n - 1)
     } in
   //log "start run";
-  res <- runM 0 s times;
+  res <- runM (0, inl ()) s times;
   //log "end run";
-  let avg = res / times in
-  // let lim = case (snd res) (\_. fail "BENCHMARK NOT RUN") (\l.l) in
-  return avg // (avg, lim)
+  let avg = fst res / times in
+  let lim = case (snd res) (\_. fail "BENCHMARK NOT RUN") (\l.l) in
+  return (avg, lim)
 end
 
-def cmp_bench = \i.\base_name.\base_res.\new_name.\new_res.
-  //let formatLim = \l. format ("min " ++ format (fst l), "max " ++ format (snd l)) in
+def cmp_bench : Int -> Text -> (Int * (Int * Int)) -> Text -> (Int * (Int * Int)) -> Cmd Unit
+ = \i.\base_name.\base_res.\new_name.\new_res.
+  let formatLim = \l. "(min " ++ format (fst l) ++ ", max " ++ format (snd l) ++ ")" in
   log $ indent i ++ "* " ++ base_name ++ ": "
-    ++ format (base_res) ++ " ticks "; //++ formatLim (snd base_res);
+    ++ format (fst base_res) ++ " ticks " ++ formatLim (snd base_res);
 
-  let d = (new_res * 100) / base_res in
+  let d = (fst new_res * 100) / fst base_res in
   let cmp = if (d > 100) {
      format (d - 100) ++ "% slower"
     } {
@@ -628,11 +640,12 @@ def cmp_bench = \i.\base_name.\base_res.\new_name.\new_res.
     } in
      
   log $ indent i ++ "* " ++ new_name ++ ": "
-    ++ format (new_res) ++ " ticks "// ++ formatLim (snd new_res)
+    ++ format (fst new_res) ++ " ticks " ++ formatLim (snd new_res)
     ++ " <- " ++ cmp;
 end
 
-def gen_random_list = 
+// Get a list of random integers of given length and maximum element number
+def gen_random_list: Int -> Int -> Cmd (List Int) = 
   let gen = \acc.\n.\rlim.
     if (n <= 0) { return acc } {
       x <- random rlim;
@@ -641,7 +654,8 @@ def gen_random_list =
   in gen emptyL
 end
 
-def gen_random_lists = \m.\n.\rlim.
+// Get a number of lists of random integers of given length and maximum element number
+def gen_random_lists: Int -> Int -> Int -> Cmd (List (List Int)) = \m.\n.\rlim.
   let gen = \acc.\m.
     if (m <= 0) { return acc } {
       l <- gen_random_list n rlim;
@@ -650,32 +664,68 @@ def gen_random_lists = \m.\n.\rlim.
   in gen emptyL m
 end
 
-def set_from_first_list : forall a s. s -> (a -> s -> s) -> List (List a) -> List (List a) =\e.\ins.\lls.
-  case lls (\_. lls) (\ls_nlls.
-    let ls = fst ls_nlls in
-    let ns = foldl (\s.\a.ins a s) e ls in
-    let nlls = snd ls_nlls in
-    nlls
-  )
-end
 
 def bench_insert = \i.
+  // Use the given function to construct (Flat)Set from the head of provided list of lists and return the tail
+  let set_from_first_list : (List a -> s) -> List (List a) -> List (List a) =\from_list.\lls.
+    case lls (\_. lls) (\ls_nlls.
+      let ns = from_list (fst ls_nlls) in
+      snd ls_nlls
+    )
+  in
+
   group i "INSERT BENCHMARK" (\i.
     group i "INSERT 10" (\i.
       let n = 10 in
       let m = 5 in
       lls10 <- gen_random_lists m n (3 * n);
-      flat_res <- benchmark m lls10 (set_from_first_list flat_set.empty flat_set.insert);
-      tree_res <- benchmark m lls10 (set_from_first_list tree_set.empty tree_set.insert);
+      flat_res <- benchmark m lls10 (set_from_first_list flat_set.from_list);
+      tree_res <- benchmark m lls10 (set_from_first_list tree_set.from_list);
       cmp_bench i "flat set" flat_res "tree set" tree_res
     );
     group i "INSERT 100" (\i.
       let n = 100 in
       let m = 3 in
       lls100 <- gen_random_lists m n (3 * n);
-      flat_res <- benchmark m lls100 (set_from_first_list flat_set.empty flat_set.insert);
-      tree_res <- benchmark m lls100 (set_from_first_list tree_set.empty tree_set.insert);
+      flat_res <- benchmark m lls100 (set_from_first_list flat_set.from_list);
+      tree_res <- benchmark m lls100 (set_from_first_list tree_set.from_list);
       cmp_bench i "flat set" flat_res "tree set" tree_res
     )
   )
 end
+
+def bench_contains = \i.
+  let contains_int : s -> (Int -> s -> Bool) -> Int -> Int = \s.\contains.\n.
+    let _ = contains n s in n + 1
+  in
+  group i "CONTAINS BENCHMARK" (\i.
+    group i "CONTAINS 10" (\i.
+      let n = 10 in
+      let m = 3 * n in
+      ls10 <- gen_random_list n m;
+      let fls = flat_set.from_list ls10 in
+      flat_res <- benchmark m 0 (contains_int fls flat_set.contains);
+      let tls = tree_set.from_list ls10 in
+      tree_res <- benchmark m 0 (contains_int tls tree_set.contains);
+      cmp_bench i "flat set" flat_res "tree set" tree_res
+    );
+    group i "CONTAINS 100" (\i.
+      let n = 100 in
+      let m = 3 * n in
+      ls100 <- gen_random_list n m;
+      let fls = flat_set.from_list ls100 in
+      flat_res <- benchmark m 0 (contains_int fls flat_set.contains);
+      let tls = tree_set.from_list ls100 in
+      tree_res <- benchmark m 0 (contains_int tls tree_set.contains);
+      cmp_bench i "flat set" flat_res "tree set" tree_res
+    )
+  )
+end
+
+def benchmark_tree: Cmd Unit =
+  group 0 "TREE BENCHMARKS" (\i.
+    bench_insert i;
+    bench_contains i;
+  );
+  log "ALL BENCHMARKS DONE!"
+end
\ No newline at end of file

From 448c49684601b7083eaaac71b9338538b05daaee Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Sun, 20 Oct 2024 11:40:33 +0200
Subject: [PATCH 19/22] fix contains and add more tests

---
 example/recursive-containers.sw | 56 ++++++++++++++++++++++++---------
 1 file changed, 41 insertions(+), 15 deletions(-)

diff --git a/example/recursive-containers.sw b/example/recursive-containers.sw
index 0908c0b8e..4fd626594 100644
--- a/example/recursive-containers.sw
+++ b/example/recursive-containers.sw
@@ -67,20 +67,20 @@ end
 def getKeyL : (a -> k) -> k -> List a -> Maybe a = \p.\x.\l.
   case l (\_. inl ()) (\n.
     let nx = p (fst n) in
-    if (nx == x) {
-      inr $ fst n
+    if (nx < x) {
+      getKeyL p x $ snd n
     } {
-      if (nx < x) {
+      if (nx > x) {
         inl ()
       } {
-        getKeyL p x $ snd n
+        inr $ fst n
       }
     }
   )
 end
 
 def containsKeyL : (a -> k) -> k -> List a -> Bool = \p.\x.\l.
-  case (getKeyL p x l) (\_. true) (\_. false)
+  case (getKeyL p x l) (\_. false) (\_. true)
 end
 
 // insert into ordered list - replaces elements, like set
@@ -165,12 +165,15 @@ def isEmptyT : RBTree k -> Bool = \d. d == emptyT end
 
 def getT : (k -> a) -> a -> RBTree k -> Maybe k = \p.\x.\t.
   case t (\_. inl ()) (\n.
-    if (x == p n.k) { inr n.k } {
-        if (x < p n.k) {
-            getT p x n.l
-        } {
-            getT p x n.r
-        }
+    let nx = p n.k in
+    if (x < nx) {
+        getT p x n.l
+    } {
+      if (x > nx) {
+          getT p x n.r
+      } {
+        inr n.k
+      }
     }
   )
 end
@@ -517,11 +520,18 @@ def test_empty: Int -> Cmd Unit = \i.
 end
 
 def test_ordered_list : Int -> Cmd Unit = \i.
-  let s = [insert=insertKeyL (\x.x), contains=containsKeyL (\x.x)] in
+  let s = flat_set in
   group i "ORDERED LIST TESTS" (\i.
-    let expected = cons 1 $ cons 2 $ cons 3 emptyL in
-    let actual = s.insert 2 $ s.insert 1 $ s.insert 3 emptyL in
+    let expected = cons 1 $ cons 2 $ cons 3 $ cons 5 emptyL in
+    let actual = s.insert 2 $ s.insert 5 $ s.insert 1 $ s.insert 3 s.empty in
     assert_eq i (formatL expected) (formatL actual) "insertKeyL should insert in order";
+    assert i (not $ s.contains 0 actual) "not contains 0 [1,2,3,5]";
+    assert i (s.contains 1 actual) "contains 1 [1,2,3,5]";
+    assert i (s.contains 2 actual) "contains 2 [1,2,3,5]";
+    assert i (s.contains 3 actual) "contains 3 [1,2,3,5]";
+    assert i (not $ s.contains 4 actual) "not contains 4 [1,2,3,5]";
+    assert i (s.contains 5 actual) "contains 5 [1,2,3,5]";
+    assert i (not $ s.contains 6 actual) "not contains 6 [1,2,3,5]";
   )
 end
 
@@ -539,6 +549,19 @@ def test_insert: Int -> Cmd Unit = \i.
       assert_eq i (inr 1) (getD 0 $ tree02) "get 0 {0: 1, 2: 3} == 1";
       assert_eq i (inr 3) (getD 2 $ tree02) "get 2 {0: 1, 2: 3} == 3";
     );
+    let s = tree_set in
+    group i "test {1,2,3,5}" (\i.
+      let expected = cons 1 $ cons 2 $ cons 3 $ cons 5 emptyL in
+      let actual = s.insert 2 $ s.insert 5 $ s.insert 1 $ s.insert 3 s.empty in
+      assert_eq i (formatL expected) (formatS actual) "set should be in order";
+      assert i (not $ s.contains 0 actual) "not contains 0 [1,2,3,5]";
+      assert i (s.contains 1 actual) "contains 1 [1,2,3,5]";
+      assert i (s.contains 2 actual) "contains 2 [1,2,3,5]";
+      assert i (s.contains 3 actual) "contains 3 [1,2,3,5]";
+      assert i (not $ s.contains 4 actual) "not contains 4 [1,2,3,5]";
+      assert i (s.contains 5 actual) "contains 5 [1,2,3,5]";
+      assert i (not $ s.contains 6 actual) "not contains 6 [1,2,3,5]";
+    )
   );
 end
 
@@ -614,7 +637,7 @@ def benchmark: Int -> s -> (s -> s) -> Cmd (Int * (Int * Int)) = \times.\s.\act.
       t1 <- time;
       //log $ "END " ++ format t1;
       let t = t1 - t0 in
-      log $ format s ++ " " ++ format t ++ " ticks";
+      //log $ format s ++ " " ++ format t ++ " ticks";
       let lim = case (snd acc) (\_. (t, t)) (\l. (min t $ fst l, max t $ snd l)) in
       runM ((fst acc + t), inr lim) ns (n - 1)
     } in
@@ -713,9 +736,12 @@ def bench_contains = \i.
       let n = 100 in
       let m = 3 * n in
       ls100 <- gen_random_list n m;
+      //log $ formatL ls100;
       let fls = flat_set.from_list ls100 in
+      //log $ formatL fls;
       flat_res <- benchmark m 0 (contains_int fls flat_set.contains);
       let tls = tree_set.from_list ls100 in
+      //log $ formatS tls;
       tree_res <- benchmark m 0 (contains_int tls tree_set.contains);
       cmp_bench i "flat set" flat_res "tree set" tree_res
     )

From 11ca2e0b576d8c063b66cd2ff7be622dcb2f4fb1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Sun, 20 Oct 2024 11:41:38 +0200
Subject: [PATCH 20/22] cooment out delete debug log

---
 example/recursive-containers.sw | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/example/recursive-containers.sw b/example/recursive-containers.sw
index 4fd626594..e05dee4eb 100644
--- a/example/recursive-containers.sw
+++ b/example/recursive-containers.sw
@@ -579,7 +579,7 @@ def delete_insert_prop: Int -> Set Int -> Cmd Unit = \i.\t.
   let i_t = inorder t in
   let f_t = formatS t in
   if (not $ containsS x t) {
-    log $ format x;
+    // log $ format x;
     assert_eq i
       (formatL i_t)
       (formatS $ deleteS x $ insertS x t)

From 5430d88c6785e2dffa1632efaddc65f42572e57b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Sun, 20 Oct 2024 20:28:25 +0200
Subject: [PATCH 21/22] Use interfaces and declarations

---
 example/recursive-containers.sw | 164 +++++++++++++++++++-------------
 1 file changed, 97 insertions(+), 67 deletions(-)

diff --git a/example/recursive-containers.sw b/example/recursive-containers.sw
index e05dee4eb..2f2877bd5 100644
--- a/example/recursive-containers.sw
+++ b/example/recursive-containers.sw
@@ -9,15 +9,67 @@
 // only first element of tuple). It is based on Haskell code in:
 // https://abhiroop.github.io/Haskell-Red-Black-Tree/
 
+/*******************************************************************/
+/*                    (TYPE) DECLARATIONS                          */
+/*******************************************************************/
+
 tydef Maybe a = Unit + a end
+
+tydef List a = rec l. Maybe (a * l) end
+
+tydef RBTree k = rec b. Maybe [red: Bool, k: k, l: b, r: b] end
+
+tydef ISet s a = 
+  [ empty: s
+  , insert: a -> s -> s 
+  , delete: a -> s -> s
+  , contains: a -> s -> Bool
+  , from_list: List a -> s
+  , pretty: s -> Text
+  ]
+end
+
+def undefined_set : any -> ISet any s =\empty.
+    [empty=empty, insert=\x.undefined, delete=\x.undefined, contains=\x.undefined, from_list=\x.undefined, pretty=\x.undefined]
+end
+
+tydef IDict d k v =
+  [ empty: d
+  , insert: k -> v -> d -> d
+  , delete: k -> d -> d
+  , get: k -> d -> Maybe v
+  , contains: k -> d -> Bool
+  , pretty: d -> Text
+  ]
+end
+
+def undefined_dict : any -> IDict any k v =\empty.
+    [empty=empty, insert=\x.undefined, delete=\x.undefined, get=\x.undefined, contains=\x.undefined, pretty=\x.undefined]
+end
+
+tydef FlatSet a = List a end
+def flat_set : ISet (FlatSet a) a = undefined_set (inl ()) end
+
+tydef FlatDict k v = List (k * v) end
+def flat_dict : IDict (FlatDict k v) k v = undefined_dict (inl ()) end
+
+tydef Set k = RBTree k end
+def tree_set : ISet (Set a) a = undefined_set (inl ()) end
+
+tydef Dict k v = RBTree (k * v) end
+def tree_dict : IDict (Dict k v) k v = undefined_dict (inl ()) end
+
+/*******************************************************************/
+/*                              MAYBE                              */
+/*******************************************************************/
+
 def mmap : (a -> b) -> Maybe a -> Maybe b = \f.\m. case m (\_. inl ()) (\a. inr (f a)) end
 
+
 /*******************************************************************/
 /*                              LISTS                              */
 /*******************************************************************/
 
-tydef List a = rec l. Maybe (a * l) end
-
 def emptyL : List a = inl () end
 def cons : a -> List a -> List a = \a.\l. inr (a, l) end
 def pureL : a -> List a = \a. cons a emptyL end
@@ -118,35 +170,28 @@ end
 
 tydef FlatSet a = List a end
 
-def flat_set :
-  [ empty: FlatSet a
-  , insert: a -> FlatSet a -> FlatSet a 
-  , delete: a -> FlatSet a -> FlatSet a 
-  , contains: a -> FlatSet a -> Bool
-  , from_list: List a -> FlatSet a
-  ] =
+def flat_set : ISet (FlatSet a) a =
   [ empty=emptyL
   , insert=insertKeyL (\x.x)
   , delete=deleteKeyL (\x.x)
   , contains=containsKeyL (\x.x)
   , from_list=foldl (flip $ insertKeyL (\x.x)) emptyL
+  , pretty=formatL
   ]
 end
 
 tydef FlatDict k v = List (k * v) end
 
-def flat_dict :
-  [ empty: FlatDict k v
-  , insert: k -> v -> FlatDict k v -> FlatDict k v
-  , delete: k -> FlatDict k v -> FlatDict k v
-  , get: k -> FlatDict k v -> Maybe v
-  , contains: k -> FlatDict k v -> Bool
-  ] =
+def flat_dict : IDict (FlatDict k v) k v =
   [ empty=emptyL
   , insert=\k.\v. insertKeyL fst (k,v)
   , delete=deleteKeyL fst
   , get=\k.\d. mmap snd (getKeyL fst k d)
   , contains=containsKeyL fst
+  , pretty=\d.
+    let p : (k * v) -> Text = \kv. format (fst kv) ++ ": " ++ format (snd kv) in 
+    let f : List (k * v) -> Text = \l. case l (\_. "}") (\n. ", " ++ p (fst n) ++ f (snd n))
+    in case d (\_. "{}") (\n. "{" ++ p (fst n) ++ f (snd n))
   ]
 end
 
@@ -154,15 +199,12 @@ end
 /*                         RED BLACK TREE                          */
 /*******************************************************************/
 
-tydef RBTree k = rec b. Maybe [red: Bool, k: k, l: b, r: b] end
 
 // equirecursive types allow us to get the node type without mutual recursion
 tydef RBNode k = rec n. [red: Bool, k: k, l: Maybe n, r: Maybe n] end
 
 def emptyT : RBTree k = inl () end
 
-def isEmptyT : RBTree k -> Bool = \d. d == emptyT end
-
 def getT : (k -> a) -> a -> RBTree k -> Maybe k = \p.\x.\t.
   case t (\_. inl ()) (\n.
     let nx = p n.k in
@@ -450,17 +492,14 @@ end
 
 tydef Dict k v = RBTree (k * v) end
 
-def emptyD : Dict k v = emptyT end
-def isEmptyD : Dict k v -> Bool = isEmptyT end
-def getD : k -> Dict k v -> Maybe v = \k.\d. mmap snd (getT fst k d) end 
-def containsD : k -> Dict k v -> Bool = containsT fst end
-def insertD : k -> v -> Dict k v -> Dict k v = \k.\v. insertT fst (k, v) end
-def deleteD : k -> Dict k v -> Dict k v = \k. deleteT fst k end
-
-def formatD : Dict k v -> Text = \d.
- let p : (k * v) -> Text = \kv. format (fst kv) ++ ": " ++ format (snd kv) in 
- let f : List (k * v) -> Text = \l. case l (\_. "}") (\n. ", " ++ p (fst n) ++ f (snd n))
- in case (inorder d) (\_. "{}") (\n. "{" ++ p (fst n) ++ f (snd n))
+def tree_dict : IDict (Dict k v) k v =
+ [ empty = emptyT
+ , get  = \k.\d. mmap snd (getT fst k d)  
+ , contains = containsT fst 
+ , insert = \k.\v. insertT fst (k, v) 
+ , delete = \k. deleteT fst k 
+ , pretty = \d. flat_dict.pretty (inorder d)
+ ]
 end
 
 /*******************************************************************/
@@ -469,25 +508,13 @@ end
 
 tydef Set k = RBTree k end
 
-def emptyS : Set k = emptyT end
-def isEmptyS : Set k -> Bool = isEmptyT end
-def containsS : k -> Set k -> Bool = containsT (\x.x) end
-def insertS : k -> Set k -> Set k = insertT (\x.x) end
-def deleteS : k -> Set k -> Set k = \k. deleteT (\x.x) k end
-def formatS : Set k -> Text = \s. formatL $ inorder s end
-
-def tree_set :
-  [ empty: Set a
-  , insert: a -> Set a -> Set a 
-  , delete: a -> Set a -> Set a 
-  , contains: a -> Set a -> Bool
-  , from_list: List a -> Set a
-  ] =
+def tree_set : ISet (Set a) a =
   [ empty=emptyT
   , insert=insertT (\x.x)
   , delete=deleteT (\x.x)
   , contains=containsT (\x.x)
   , from_list=foldl (flip $ insertT (\x.x)) emptyT
+  , pretty=\s. formatL $ inorder s
   ]
 end
 
@@ -512,10 +539,10 @@ def group = \i. \m. \tests.
 end
 
 def test_empty: Int -> Cmd Unit = \i.
+  let d = tree_dict in
   group i "EMPTY TESTS" (\i.
-    assert i (isEmptyD emptyD) "empty tree should be empty";
-    assert_eq i (inl ()) (getD 0 $ emptyD) "no element should be present in an empty tree";
-    assert i (not $ containsD 0 $ emptyD) "empty tree should not contain any elements";
+    assert_eq i (inl ()) (d.get 0 $ d.empty) "no element should be present in an empty tree";
+    assert i (not $ d.contains 0 $ d.empty) "empty tree should not contain any elements";
   )
 end
 
@@ -536,24 +563,25 @@ def test_ordered_list : Int -> Cmd Unit = \i.
 end
 
 def test_insert: Int -> Cmd Unit = \i.
+  let d = tree_dict in
+  let s = tree_set in
   group i "INSERT TESTS" (\i.
     group i "test {0: 1}" (\i.
-      let tree0 = insertD 0 1 emptyD in
-      assert i (not $ isEmptyD tree0) "nonempty tree should not be empty";
-      assert_eq i (inr 1) (getD 0 $ tree0) "one element should be present in a one element tree";
-      assert i (containsD 0 $ tree0) "one element tree should contain that elements";
-      assert i (not $ containsD 1 $ tree0) "one element tree should contain only that elements";
+      let tree0 = d.insert 0 1 d.empty in
+      assert i (d.empty != tree0) "nonempty tree should not be empty";
+      assert_eq i (inr 1) (d.get 0 $ tree0) "one element should be present in a one element tree";
+      assert i (d.contains 0 $ tree0) "one element tree should contain that elements";
+      assert i (not $ d.contains 1 $ tree0) "one element tree should contain only that elements";
     );
     group i "test {0: 1, 2: 3}" (\i.
-      let tree02 = insertD 2 3 $ insertD 0 1 emptyD in
-      assert_eq i (inr 1) (getD 0 $ tree02) "get 0 {0: 1, 2: 3} == 1";
-      assert_eq i (inr 3) (getD 2 $ tree02) "get 2 {0: 1, 2: 3} == 3";
+      let tree02 = d.insert 2 3 $ d.insert 0 1 d.empty in
+      assert_eq i (inr 1) (d.get 0 $ tree02) "get 0 {0: 1, 2: 3} == 1";
+      assert_eq i (inr 3) (d.get 2 $ tree02) "get 2 {0: 1, 2: 3} == 3";
     );
-    let s = tree_set in
     group i "test {1,2,3,5}" (\i.
       let expected = cons 1 $ cons 2 $ cons 3 $ cons 5 emptyL in
       let actual = s.insert 2 $ s.insert 5 $ s.insert 1 $ s.insert 3 s.empty in
-      assert_eq i (formatL expected) (formatS actual) "set should be in order";
+      assert_eq i (formatL expected) (s.pretty actual) "set should be in order";
       assert i (not $ s.contains 0 actual) "not contains 0 [1,2,3,5]";
       assert i (s.contains 1 actual) "contains 1 [1,2,3,5]";
       assert i (s.contains 2 actual) "contains 2 [1,2,3,5]";
@@ -568,41 +596,43 @@ end
 def randomTestS: Int -> Set Int -> (Set Int -> Cmd a) -> Cmd (Set Int) = \i.\s.\test.
   if (i <= 0) {return s} {
     x <- random 20;
-    let ns = insertS x s in
+    let ns = tree_set.insert x s in
     test ns;
     randomTestS (i - 1) ns test
   }
 end
 
 def delete_insert_prop: Int -> Set Int -> Cmd Unit = \i.\t.
+  let s = tree_set in
   x <- random 20;
   let i_t = inorder t in
-  let f_t = formatS t in
-  if (not $ containsS x t) {
+  let f_t = s.pretty t in
+  if (not $ s.contains x t) {
     // log $ format x;
     assert_eq i
       (formatL i_t)
-      (formatS $ deleteS x $ insertS x t)
+      (s.pretty $ s.delete x $ s.insert x t)
       (f_t ++ " == delete " ++ format x ++ " $ insert " ++ format x ++ " " ++ f_t)
   } { delete_insert_prop i t /* reroll */}
 end
 
 def delete_delete_prop: Int -> Set a -> Cmd Unit = \i.\t.
+  let s = tree_set in
   let i_t = inorder t in
   ix <- random (lengthL i_t);
   let x = getL ix i_t in
-  let ds = deleteS x t in
-  let dds = deleteS x ds in
-  let f_t = formatS t in
+  let ds = s.delete x t in
+  let dds = s.delete x ds in
+  let f_t = s.pretty t in
   let f_dx = "delete " ++ format x in
-  assert_eq i (formatS ds) (formatS dds)
+  assert_eq i (s.pretty ds) (s.pretty dds)
     (f_dx ++ f_t ++ " == " ++ f_dx ++ " $ " ++ f_dx ++ " " ++ f_t)
 end
 
 def test_delete: Int -> Cmd Unit = \i.
   group i "DELETE TESTS" (\i.
-    randomTestS 15 emptyS (\s.
-      group i (formatS s) (\i.
+    randomTestS 15 tree_set.empty (\s.
+      group i (tree_set.pretty s) (\i.
         delete_insert_prop i s;
         delete_delete_prop i s;
       )

From ad4ba8fe4d083a53b626dc9750d72a4a91f0a106 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= <ondras98@icloud.com>
Date: Sun, 20 Oct 2024 20:40:54 +0200
Subject: [PATCH 22/22] Test insert interface

---
 example/recursive-containers.sw | 23 +++++++----------------
 1 file changed, 7 insertions(+), 16 deletions(-)

diff --git a/example/recursive-containers.sw b/example/recursive-containers.sw
index 2f2877bd5..697cccd21 100644
--- a/example/recursive-containers.sw
+++ b/example/recursive-containers.sw
@@ -546,9 +546,7 @@ def test_empty: Int -> Cmd Unit = \i.
   )
 end
 
-def test_ordered_list : Int -> Cmd Unit = \i.
-  let s = flat_set in
-  group i "ORDERED LIST TESTS" (\i.
+def test_insert_1235: ISet s Int -> Int -> Cmd Unit =\s.\i.
     let expected = cons 1 $ cons 2 $ cons 3 $ cons 5 emptyL in
     let actual = s.insert 2 $ s.insert 5 $ s.insert 1 $ s.insert 3 s.empty in
     assert_eq i (formatL expected) (formatL actual) "insertKeyL should insert in order";
@@ -559,7 +557,11 @@ def test_ordered_list : Int -> Cmd Unit = \i.
     assert i (not $ s.contains 4 actual) "not contains 4 [1,2,3,5]";
     assert i (s.contains 5 actual) "contains 5 [1,2,3,5]";
     assert i (not $ s.contains 6 actual) "not contains 6 [1,2,3,5]";
-  )
+end
+
+def test_ordered_list : Int -> Cmd Unit = \i.
+  let s = flat_set in
+  group i "ORDERED LIST TESTS" (test_insert_1235 flat_set)
 end
 
 def test_insert: Int -> Cmd Unit = \i.
@@ -578,18 +580,7 @@ def test_insert: Int -> Cmd Unit = \i.
       assert_eq i (inr 1) (d.get 0 $ tree02) "get 0 {0: 1, 2: 3} == 1";
       assert_eq i (inr 3) (d.get 2 $ tree02) "get 2 {0: 1, 2: 3} == 3";
     );
-    group i "test {1,2,3,5}" (\i.
-      let expected = cons 1 $ cons 2 $ cons 3 $ cons 5 emptyL in
-      let actual = s.insert 2 $ s.insert 5 $ s.insert 1 $ s.insert 3 s.empty in
-      assert_eq i (formatL expected) (s.pretty actual) "set should be in order";
-      assert i (not $ s.contains 0 actual) "not contains 0 [1,2,3,5]";
-      assert i (s.contains 1 actual) "contains 1 [1,2,3,5]";
-      assert i (s.contains 2 actual) "contains 2 [1,2,3,5]";
-      assert i (s.contains 3 actual) "contains 3 [1,2,3,5]";
-      assert i (not $ s.contains 4 actual) "not contains 4 [1,2,3,5]";
-      assert i (s.contains 5 actual) "contains 5 [1,2,3,5]";
-      assert i (not $ s.contains 6 actual) "not contains 6 [1,2,3,5]";
-    )
+    group i "test {1,2,3,5}" (test_insert_1235 tree_set)
   );
 end