From a3b484b70e1d683780de9eec34fcc34aefba36db 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] 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]
         }
     }
   )