Add Set.{deleteWith; intersection; difference}, Map.delete (#17)

* Update dependencies and remove ContaintersPrelude

* Use Maybe functor from stdlib

* Add Set.{deleteWith; intersection; difference}, Map.delete

Refactors tests

Data/BinaryTree.juvix

@@ -1,6 +1,6 @@
 module Data.BinaryTree;
 
-import ContainersPrelude open;
+import Stdlib.Prelude open;
 
 type BinaryTree (A : Type) :=
   | leaf : BinaryTree A

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};
@@ -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 :=
@@ -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);

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);

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;

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};
@@ -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;

Data/Tmp.juvix

@@ -1,17 +1,13 @@
 --- 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
   | 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;

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);

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};
 

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"]
   };

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: []

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 "../"]
   };

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;

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)

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: []