From 9707be6edd696718997e000bbc414007338481d7 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 15 Aug 2024 10:47:59 +0100 Subject: [PATCH 1/3] Update dependencies and remove ContaintersPrelude --- ContainersPrelude.juvix | 18 ------------------ Data/BinaryTree.juvix | 2 +- Data/Map.juvix | 2 +- Data/Queue/Base.juvix | 2 +- Data/Set.juvix | 2 ++ Data/Set/AVL.juvix | 2 +- Data/Tmp.juvix | 2 +- Data/Tree.juvix | 2 +- Data/UnbalancedSet.juvix | 2 +- Package.juvix | 4 ++-- juvix.lock.yaml | 6 +++--- test/Package.juvix | 2 +- test/juvix.lock.yaml | 12 ++++++------ 13 files changed, 21 insertions(+), 37 deletions(-) delete mode 100644 ContainersPrelude.juvix diff --git a/ContainersPrelude.juvix b/ContainersPrelude.juvix deleted file mode 100644 index e409c58..0000000 --- a/ContainersPrelude.juvix +++ /dev/null @@ -1,18 +0,0 @@ -module ContainersPrelude; - -import Juvix.Builtin.V1 open public; -import Stdlib.Data.String.Base open public; -import Stdlib.Data.Pair open public; -import Stdlib.Data.List.Base open public; -import Stdlib.System.IO.Base open public; -import Stdlib.System.IO.String open public; -import Stdlib.System.IO.Nat open public; -import Stdlib.Function open public; -import Stdlib.Trait.Show open public; -import Stdlib.Data.Bool.Base open public; -import Stdlib.Data.Maybe open public; -import Stdlib.Trait.Eq open public; -import Stdlib.Trait.Ord open public; -import Stdlib.Trait.Show open public; -import Stdlib.Data.List open public; -import Stdlib.Data.Int open public; diff --git a/Data/BinaryTree.juvix b/Data/BinaryTree.juvix index 8df8474..f65a516 100644 --- a/Data/BinaryTree.juvix +++ b/Data/BinaryTree.juvix @@ -1,6 +1,6 @@ module Data.BinaryTree; -import ContainersPrelude open; +import Stdlib.Prelude open; type BinaryTree (A : Type) := | leaf : BinaryTree A diff --git a/Data/Map.juvix b/Data/Map.juvix index c9ab610..e9e4dad 100644 --- a/Data/Map.juvix +++ b/Data/Map.juvix @@ -1,6 +1,6 @@ module Data.Map; -import ContainersPrelude open; +import Stdlib.Prelude open; import Data.Set as Set; open Set using {Set}; diff --git a/Data/Queue/Base.juvix b/Data/Queue/Base.juvix index 039abd9..9e101c4 100644 --- a/Data/Queue/Base.juvix +++ b/Data/Queue/Base.juvix @@ -9,7 +9,7 @@ --- performance. module Data.Queue.Base; -import ContainersPrelude open; +import Stdlib.Prelude open; --- A first-in-first-out data structure type Queue (A : Type) := queue (List A) (List A); diff --git a/Data/Set.juvix b/Data/Set.juvix index 185d1b9..06c9ca9 100644 --- a/Data/Set.juvix +++ b/Data/Set.juvix @@ -10,3 +10,5 @@ syntax alias Set := AVLTree; eqSetI {A} {{Eq A}} : Eq (Set A) := eqAVLTreeI; ordSetI {A} {{Ord A}} : Ord (Set A) := ordAVLTreeI; + +import Stdlib.Data.List open; diff --git a/Data/Set/AVL.juvix b/Data/Set/AVL.juvix index aba3603..87f82f5 100644 --- a/Data/Set/AVL.juvix +++ b/Data/Set/AVL.juvix @@ -8,7 +8,7 @@ --- constructing, modifying, and querying AVL trees. module Data.Set.AVL; -import ContainersPrelude open; +import Stdlib.Prelude open; import Data.Tmp open; import Data.Tree as Tree open using {Tree; Forest}; diff --git a/Data/Tmp.juvix b/Data/Tmp.juvix index 0c7835f..f877b59 100644 --- a/Data/Tmp.juvix +++ b/Data/Tmp.juvix @@ -1,7 +1,7 @@ --- the functions here should be eventually put in the stdlib module Data.Tmp; -import ContainersPrelude open; +import Stdlib.Prelude open; import Stdlib.Trait open; printNatListLn : List Nat → IO diff --git a/Data/Tree.juvix b/Data/Tree.juvix index 3895384..283c1f1 100644 --- a/Data/Tree.juvix +++ b/Data/Tree.juvix @@ -1,7 +1,7 @@ --- N-Ary trees with pretty printing. module Data.Tree; -import ContainersPrelude open; +import Stdlib.Prelude open; --- A ;List; of trees. Forest (A : Type) : Type := List (Tree A); diff --git a/Data/UnbalancedSet.juvix b/Data/UnbalancedSet.juvix index 89e6bb9..29e9666 100644 --- a/Data/UnbalancedSet.juvix +++ b/Data/UnbalancedSet.juvix @@ -1,6 +1,6 @@ module Data.UnbalancedSet; -import ContainersPrelude open; +import Stdlib.Prelude open; import Stdlib.Trait.Ord as Ord open using {Ord; mkOrd; module Ord}; diff --git a/Package.juvix b/Package.juvix index 4223e5e..84d563e 100644 --- a/Package.juvix +++ b/Package.juvix @@ -5,6 +5,6 @@ import PackageDescription.V2 open; package : Package := defaultPackage@?{ name := "containers"; - version := mkVersion 0 13 0; - dependencies := [github "anoma" "juvix-stdlib" "v0.5.0"] + version := mkVersion 0 14 0; + dependencies := [github "anoma" "juvix-stdlib" "v0.6.0"] }; diff --git a/juvix.lock.yaml b/juvix.lock.yaml index 93355c9..7de8dd7 100644 --- a/juvix.lock.yaml +++ b/juvix.lock.yaml @@ -1,11 +1,11 @@ -# This file was autogenerated by Juvix version 0.6.4. +# This file was autogenerated by Juvix version 0.6.5. # Do not edit this file manually. version: 2 -checksum: 64d7d399b724977d770547857b6f074a7a8c5fd4d82b5fec029a307c1ff286b9 +checksum: 84b86822b505189000d4de6ff4193143f40a64cd5a7a59c7ab8bf26c89f1891f dependencies: - git: name: anoma_juvix-stdlib - ref: 16211500dc59a944f851fbaeeef703fdd09163fa + ref: 17a82dd466010b51924677b16a3f09a6c4c86a80 url: https://github.com/anoma/juvix-stdlib dependencies: [] diff --git a/test/Package.juvix b/test/Package.juvix index 12baabd..7a5128b 100644 --- a/test/Package.juvix +++ b/test/Package.juvix @@ -7,5 +7,5 @@ package : Package := name := "containers-tests"; main := just "Main.juvix"; dependencies := - [github "anoma" "juvix-stdlib" "v0.5.0"; github "anoma" "juvix-test" "v0.12.0"; path "../"] + [github "anoma" "juvix-stdlib" "v0.6.0"; github "anoma" "juvix-test" "v0.13.0"; path "../"] }; diff --git a/test/juvix.lock.yaml b/test/juvix.lock.yaml index 774bd03..fd9ea17 100644 --- a/test/juvix.lock.yaml +++ b/test/juvix.lock.yaml @@ -1,28 +1,28 @@ -# This file was autogenerated by Juvix version 0.6.4. +# This file was autogenerated by Juvix version 0.6.5. # Do not edit this file manually. version: 2 -checksum: 13869df5ec05e9541007e466b9ccb3cb9dfab76e0a1387a2d79b58c33f959725 +checksum: f08d729e734185158847c6199dcf859238b1edc267f35f56d33eae0a195f1da5 dependencies: - git: name: anoma_juvix-stdlib - ref: 16211500dc59a944f851fbaeeef703fdd09163fa + ref: 17a82dd466010b51924677b16a3f09a6c4c86a80 url: https://github.com/anoma/juvix-stdlib dependencies: [] - git: name: anoma_juvix-test - ref: f7e822969fa82c510f38d6569a9b5ac7f1180221 + ref: 12b72c6f91126f08e19ef183cc377bb86e629de9 url: https://github.com/anoma/juvix-test dependencies: - git: name: anoma_juvix-stdlib - ref: 16211500dc59a944f851fbaeeef703fdd09163fa + ref: 17a82dd466010b51924677b16a3f09a6c4c86a80 url: https://github.com/anoma/juvix-stdlib dependencies: [] - path: ../ dependencies: - git: name: anoma_juvix-stdlib - ref: 16211500dc59a944f851fbaeeef703fdd09163fa + ref: 17a82dd466010b51924677b16a3f09a6c4c86a80 url: https://github.com/anoma/juvix-stdlib dependencies: [] From b233bb895cc002c665d1fbef5b2b244623d1fbdb Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 15 Aug 2024 10:52:21 +0100 Subject: [PATCH 2/3] Use Maybe functor from stdlib --- Data/Map.juvix | 2 +- Data/Tmp.juvix | 4 ---- 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/Data/Map.juvix b/Data/Map.juvix index e9e4dad..007103e 100644 --- a/Data/Map.juvix +++ b/Data/Map.juvix @@ -42,7 +42,7 @@ insert {A B : Type} {{Ord A}} : A -> B -> Map A B -> Map A B := insertWith λ {o {-# specialize: [1] #-} lookup {A B} {{Ord A}} (k : A) : Map A B -> Maybe B - | (mkMap s) := mapMaybe value (Set.lookupWith key k s); + | (mkMap s) := map value (Set.lookupWith key k s); {-# specialize: [1, f] #-} fromListWith {A B} {{Ord A}} (f : B -> B -> B) (xs : List (Pair A B)) : Map A B := diff --git a/Data/Tmp.juvix b/Data/Tmp.juvix index f877b59..228edea 100644 --- a/Data/Tmp.juvix +++ b/Data/Tmp.juvix @@ -8,10 +8,6 @@ printNatListLn : List Nat → IO | nil := printStringLn "nil" | (x :: xs) := printNat x >>> printString " :: " >>> printNatListLn xs; -mapMaybe {A B} (f : A -> B) : Maybe A -> Maybe B - | nothing := nothing - | (just a) := just (f a); - isJust {A} : Maybe A -> Bool | nothing := false | (just _) := true; From ba533aff6d36f4a584e322659f22d02772ad8c81 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Thu, 15 Aug 2024 11:54:06 +0100 Subject: [PATCH 3/3] Add Set.{deleteWith; intersection; difference}, Map.delete Refactors tests --- Data/Map.juvix | 3 ++ Data/Set/AVL.juvix | 31 +++++++++++++---- test/Test/AVL.juvix | 83 +++++++++++++++++++++++++++++++++------------ test/Test/Map.juvix | 6 ++++ 4 files changed, 95 insertions(+), 28 deletions(-) diff --git a/Data/Map.juvix b/Data/Map.juvix index 007103e..b885b77 100644 --- a/Data/Map.juvix +++ b/Data/Map.juvix @@ -57,5 +57,8 @@ toList {A B} : Map A B -> List (Pair A B) size {A B} : Map A B -> Nat | (mkMap s) := Set.size s; +delete {A B} {{Ord A}} (k : A) : Map A B -> Map A B + | m@(mkMap s) := Set.deleteWith key k s |> mkMap; + instance eqMapI {A B} {{Eq A}} {{Eq B}} : Eq (Map A B) := mkEq (Eq.eq on toList); diff --git a/Data/Set/AVL.juvix b/Data/Set/AVL.juvix index 87f82f5..a8e32dc 100644 --- a/Data/Set/AVL.juvix +++ b/Data/Set/AVL.juvix @@ -117,21 +117,23 @@ insertWith {A} {{o : Ord A}} (f : A -> A -> A) (x : A) : AVLTree A -> AVLTree A --- 𝒪(log 𝓃). Inserts an element into and ;AVLTree;. insert {A} {{Ord A}} : A -> AVLTree A -> AVLTree A := insertWith (flip const); ---- 𝒪(log 𝓃). Removes an element from an ;AVLTree;. -delete {A} {{o : Ord A}} (x : A) : AVLTree A -> AVLTree A := +--- 𝒪(log 𝓃). Removes an element from an ;AVLTree; based on a projected comparison value. +--- +--- Assumption Ord A and Ord B are compatible: Given a1 a2, A then (p a1 == p a2) == (a1 == a2) +deleteWith {A B} {{o : Ord A}} {{po : Ord B}} (p : A -> B) (x : B) : AVLTree A -> AVLTree A := let - {-# specialize-by: [o] #-} + {-# specialize-by: [o, po, p] #-} deleteMin : AVLTree A -> Maybe (Pair A (AVLTree A)) | empty := nothing | (node v _ l r) := case deleteMin l of | nothing := just (v, r) | just (m, l') := just (m, mknode v l' r); - {-# specialize-by: [o] #-} + {-# specialize-by: [o, po, p] #-} go : AVLTree A -> AVLTree A | empty := empty | (node y h l r) := - case Ord.cmp x y of + case Ord.cmp x (p y) of | LT := balance (mknode y (go l) r) | GT := balance (mknode y l (go r)) | EQ := @@ -143,6 +145,9 @@ delete {A} {{o : Ord A}} (x : A) : AVLTree A -> AVLTree A := | just (minRight, r') := balance (mknode minRight l r'); in go; +--- 𝒪(log 𝓃). Removes an element from an ;AVLTree;. +delete {A} {{o : Ord A}} : A -> AVLTree A -> AVLTree A := deleteWith id; + --- 𝒪(log 𝓃). Returns the minimum element of the ;AVLTree;. lookupMin {A} : AVLTree A -> Maybe A | empty := nothing @@ -159,9 +164,15 @@ lookupMax {A} : AVLTree A -> Maybe A --- 𝒪(𝒹 log 𝓃). Deletes d elements from an ;AVLTree;. {-# specialize: [1] #-} -deleteMany {A} {{Ord A}} (d : List A) (t : AVLTree A) : AVLTree A := +deleteMany {A} {{Ord A}} : List A -> AVLTree A -> AVLTree A := deleteManyWith id; + +--- 𝒪(𝒹 log 𝓃). Deletes d elements from an ;AVLTree; based on a projected comparison value. +--- +--- Assumption Ord A and Ord B are compatible: Given a1 a2, A then (p a1 == p a2) == (a1 == a2) +{-# specialize: [2] #-} +deleteManyWith {A B} {{Ord A}} {{Ord B}} (p : A -> B) (d : List B) (t : AVLTree A) : AVLTree A := for (acc := t) (x in d) - delete x acc; + deleteWith p x acc; --- 𝒪(𝓃). Checks the ;AVLTree; height invariant. I.e. that --- every two children do not differ on height by more than 1. @@ -213,3 +224,9 @@ eqAVLTreeI {A} {{Eq A}} : Eq (AVLTree A) := mkEq ((==) on toList); instance ordAVLTreeI {A} {{Ord A}} : Ord (AVLTree A) := mkOrd (Ord.cmp on toList); + +intersection {A} {{Ord A}} (s1 s2 : AVLTree A) : AVLTree A := + toList s1 |> filter \ {x := member? x s2} |> fromList; + +difference {A} {{Ord A}} (s1 s2 : AVLTree A) : AVLTree A := + toList s1 |> filter \ {x := not (member? x s2)} |> fromList; diff --git a/test/Test/AVL.juvix b/test/Test/AVL.juvix index be4c6d9..a375bd4 100644 --- a/test/Test/AVL.juvix +++ b/test/Test/AVL.juvix @@ -1,45 +1,86 @@ module Test.AVL; import Test.JuvixUnit open; -import Juvix.Builtin.V1 open; -import Stdlib.System.IO.Base open; -import Stdlib.System.IO.String open; -import Stdlib.Data.Pair open; -import Stdlib.Data.List.Base open; +import Stdlib.Prelude open; -import Data.Set.AVL open; +import +Data.Set.AVL open; + +type Box := mkBox {b : Nat}; + +instance +BoxOrdI : Ord Box := mkOrd (Ord.cmp on Box.b); --- Test for size and balance. -mkTests : Pair String (Pair Nat (AVLTree Nat)) -> List Test - | (title, len, s) := +mkTests {A} : TestDescr A -> List Test + | mkTestDescr@{testTitle; testLen; testSet} := let mkTitle : String -> String - | m := title ++str " " ++str m; + | m := testTitle ++str " " ++str m; sizeMsg : String := "sizes do not match"; balanceMsg : String := "not balanced"; - in [ testCase (mkTitle "size") (assertEqual sizeMsg (size s) len) - ; testCase (mkTitle "balanced") (assertTrue balanceMsg (isBalanced s)) + in [ testCase (mkTitle "size") (assertEqual sizeMsg (size testSet) testLen) + ; testCase (mkTitle "balanced") (assertTrue balanceMsg (isBalanced testSet)) ]; -TestDescr : Type := Pair String (Pair Nat (AVLTree Nat)); +type TestDescr (A : Type) := + mkTestDescr { + testTitle : String; + testLen : Nat; + testSet : AVLTree A + }; + +s1-tree : AVLTree Nat := fromList [1; 2; 8; 3; 3; 2; 9]; + +s2-tree : AVLTree Nat := fromList [1; 3; 0; 4; 4; 8; 2]; + +s1 : TestDescr Nat := mkTestDescr "s1" 5 s1-tree; -s1 : TestDescr := "s1", 5, fromList [1; 2; 8; 3; 3; 2; 9]; +s2 : TestDescr Nat := mkTestDescr "s2" 6 s2-tree; -s2 : TestDescr := "s2", 6, fromList [1; 3; 0; 4; 4; 8; 2]; +s2-delete : TestDescr Nat := + mkTestDescr@{ + testTitle := TestDescr.testTitle s2 ++str "-delete"; + testLen := sub (TestDescr.testLen s2) 2; + testSet := deleteMany [1; 8] (TestDescr.testSet s2) + }; -s2-delete : TestDescr := case s2 of t, l, s := t ++str "-delete", sub l 2, deleteMany [1; 8] s; +s2-delete-with : TestDescr Box := + mkTestDescr@{ + testTitle := TestDescr.testTitle s2 ++str "-delete-with"; + testLen := sub (TestDescr.testLen s2) 2; + testSet := deleteManyWith Box.b [1; 8] (TestDescr.testSet s2 |> toList |> map mkBox |> fromList) + }; -s3 : TestDescr := "s3", 6, fromList [5; 4; 3; 2; 1; 0]; +s3 : TestDescr Nat := + mkTestDescr@{ + testTitle := "s3"; + testLen := 6; + testSet := fromList [5; 4; 3; 2; 1; 0] + }; -s4 : TestDescr := "s4", 5, fromList [1; 2; 3; 4; 5]; +s4 : TestDescr Nat := + mkTestDescr@{ + testTitle := "s4"; + testLen := 5; + testSet := fromList [1; 2; 3; 4; 5] + }; tests : List Test := - [testCase "s1-member" (assertTrue "member? 3 s1" (member? 3 (snd (snd s1))))] + [ testCase "s1-member" (assertTrue "member? 3 s1" (member? 3 s1-tree)) + ; testCase + "s1-s2-intersection" + (assertEqual + "intersection s1-tree s2-tree" + (intersection s1-tree s2-tree) + (fromList [1; 2; 3; 8])) + ; testCase + "s1-s2-difference" + (assertEqual "difference s1-tree s2-tree" (difference s1-tree s2-tree) (fromList [9])) + ] ++ concatMap mkTests [s1; s2; s3; s4; s2-delete]; suite : TestSuite := testSuite "AVL Set" tests; main : IO := - printStringLn (pretty (snd (snd s1))) - >>> printStringLn (prettyDebug (snd (snd s1))) - >>> runTestSuite suite; + printStringLn (pretty s1-tree) >>> printStringLn (prettyDebug s1-tree) >>> runTestSuite suite; diff --git a/test/Test/Map.juvix b/test/Test/Map.juvix index 6b7376b..adb5245 100644 --- a/test/Test/Map.juvix +++ b/test/Test/Map.juvix @@ -22,6 +22,12 @@ tests : List Test := ; testCase "Map.lookup available key" (assertJust "could not find expected key" (Map.lookup 2 m)) + ; testCase + "Map.delete exiting key" + (assertNothing (const "expected deleted key to be missing") (Map.delete 2 m |> Map.lookup 2)) + ; testCase + "Map.delete missing key" + (assertEqual "expected maps to be equal" m (Map.delete 100 m)) ; testCase "Map.length computes the number of keys in the map" (assertEqual "expected length 2" (Map.size m) 2)