Use interfaces and declarations

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,51 +170,41 @@ 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
 
 /*******************************************************************/
 /*                         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;
       )