From 5430d88c6785e2dffa1632efaddc65f42572e57b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= Date: Sun, 20 Oct 2024 20:28:25 +0200 Subject: [PATCH] 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; )