Adapt to #2417 and update to standard library traits

Data/Map.juvix

@@ -38,6 +38,7 @@ type Map A B := mkMap (AVLTree (Binding A B));
 
 empty {A B} : Map A B := mkMap AVL.empty;
 
+{-# specialize: [1, f] #-}
 insertWith {A B} {{Ord A}} (f : B -> B -> B) (k : A) (v : B)
   : Map A B -> Map A B
   | (mkMap s) :=
@@ -50,9 +51,11 @@ insert {A B : Type} {{Ord A}}
   : A -> B -> Map A B -> Map A B :=
   insertWith λ {old new := new};
 
+{-# specialize: [1] #-}
 lookup {A B} {{Ord A}} (k : A) : Map A B -> Maybe B
   | (mkMap s) := mapMaybe value (Set.lookupWith key k s);
 
+{-# specialize: [1, f] #-}
 fromListWith {A B} {{Ord A}} (f : B -> B -> B) (xs : List
   (A × B)) : Map A B :=
   for (acc := empty) (k, v in xs)

Data/Set/AVL.juvix

@@ -16,10 +16,7 @@ import Stdlib.Data.Int.Ord as Int;
 
 import Data.Tree as Tree open using {Tree; Forest};
 
-import Stdlib.Data.Nat.Ord as Nat open;
-
 import Stdlib.Trait.Eq as Eq open using {Eq};
-
 import Stdlib.Trait.Ord as Ord open using {Ord};
 
 --- A self-balancing binary search tree.
@@ -82,26 +79,25 @@ balance : {A : Type} -> AVLTree A -> AVLTree A
     let
       factor : BalanceFactor := balanceFactor n;
     in case factor of {
-      | LeanRight :=
-        case balanceFactor r of {
-          | LeanLeft := rotateLeft (mknode x l (rotateRight r))
-          | _ := rotateLeft n
-        }
-      | LeanLeft :=
-        case balanceFactor l of {
-          | LeanRight := rotateRight (mknode x (rotateLeft l) r)
-          | _ := rotateRight n
-        }
-      | LeanNone := n
-    };
+         | LeanRight :=
+           case balanceFactor r of {
+             | LeanLeft := rotateLeft (mknode x l (rotateRight r))
+             | _ := rotateLeft n
+           }
+         | LeanLeft :=
+           case balanceFactor l of {
+             | LeanRight := rotateRight (mknode x (rotateLeft l) r)
+             | _ := rotateRight n
+           }
+         | LeanNone := n
+       };
 
 --- 𝒪(log 𝓃). Lookup a member from the ;AVLTree; using a projection function.
 --- Ord A, Ord K and f must be compatible. i.e cmp_k (f a1) (f a2) == cmp_a a1 a2
-{-# specialize: [1] #-}
-lookupWith {A K} {{Ord K}} (f : A -> K) (x : K)
+lookupWith {A K} {{o : Ord K}} (f : A -> K) (x : K)
   : AVLTree A -> Maybe A :=
   let
-    {-# specialize-by: [f] #-}
+    {-# specialize-by: [o, f] #-}
     go : AVLTree A -> Maybe A
       | empty := nothing
       | m@(node y h l r) :=
@@ -113,6 +109,7 @@ lookupWith {A K} {{Ord K}} (f : A -> K) (x : K)
   in go;
 
 --- 𝒪(log 𝓃). Queries whether an element is in an ;AVLTree;.
+{-# specialize: [1] #-}
 member? {A} {{Ord A}} (x : A) : AVLTree A -> Bool :=
   isJust ∘ lookupWith id x;
 
@@ -121,11 +118,10 @@ member? {A} {{Ord A}} (x : A) : AVLTree A -> Bool :=
 ---
 --- Assumption: Given a1 == a2 then f a1 a2 == a1 == a2
 --- where == comes from Ord a.
-{-# specialize: [1] #-}
-insertWith {A} {{Ord A}} (f : A -> A -> A) (x : A)
+insertWith {A} {{o : Ord A}} (f : A -> A -> A) (x : A)
   : AVLTree A -> AVLTree A :=
   let
-    {-# specialize-by: [f] #-}
+    {-# specialize-by: [o, f] #-}
     go : AVLTree A -> AVLTree A
       | empty := mknode x empty empty
       | m@(node y h l r) :=
@@ -141,15 +137,17 @@ insert {A} {{Ord A}} : A -> AVLTree A -> AVLTree A :=
   insertWith (flip const);
 
 --- 𝒪(log 𝓃). Removes an element from an ;AVLTree;.
-delete {A} {{Ord A}} (x : A) : AVLTree A -> AVLTree A :=
+delete {A} {{o : Ord A}} (x : A) : AVLTree A -> AVLTree A :=
   let
+    {-# specialize-by: [o] #-}
     deleteMin : AVLTree A -> Maybe (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] #-}
     go : AVLTree A -> AVLTree A
       | empty := empty
       | (node y h l r) :=
@@ -183,6 +181,7 @@ lookupMax {A} : AVLTree A -> Maybe A
   | (node _ _ _ r) := lookupMax r;
 
 --- 𝒪(𝒹 log 𝓃). Deletes d elements from an ;AVLTree;.
+{-# specialize: [1] #-}
 deleteMany {A} {{Ord A}} (d : List A) (t : AVLTree A)
   : AVLTree A := for (acc := t) (x in d) delete x acc;
 
@@ -194,6 +193,7 @@ isBalanced {A} : AVLTree A -> Bool
     isBalanced l && isBalanced r && abs (diffFactor n) <= 1;
 
 --- 𝒪(𝓃 log 𝓃). Create an ;AVLTree; from an unsorted ;List;.
+{-# specialize: [1] #-}
 fromList {A} {{Ord A}} (l : List A) : AVLTree A :=
   for (acc := empty) (x in l)
     insert x acc;

Makefile

@@ -31,10 +31,6 @@ test: build/UnbalancedSet \
 clean-build:
 	@rm -rf build/
 
-.PHONY: clean-deps
-clean-deps:
-	@rm -rf/
-
 .PHONY: clean
-clean: clean-deps clean-build
-
+clean: clean-build
+	@juvix clean

Package.juvix

@@ -0,0 +1,11 @@
+module Package;
+
+import PackageDescription.V1 open;
+
+package : Package :=
+  defaultPackage
+    {name := "containers";
+     version := mkVersion 0 8 0;
+     dependencies := [ github "anoma" "juvix-stdlib" "v0.0.1"
+                     ; github "anoma" "juvix-test" "v0.7.0"
+                     ]};

Test/AVL.juvix

@@ -12,11 +12,13 @@ mkTests : String × Nat × AVLTree Nat -> List Test
         | m := title ++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 s) len)
+       ; testCase
+         (mkTitle "balanced")
+         (assertTrue balanceMsg (isBalanced s))
+       ];
 
 TestDescr : Type := String × Nat × AVLTree Nat;
 
@@ -25,17 +27,19 @@ s1 : TestDescr := "s1", 5, fromList [1; 2; 8; 3; 3; 2; 9];
 s2 : TestDescr := "s2", 6, fromList [1; 3; 0; 4; 4; 8; 2];
 
 s2-delete : TestDescr :=
-  case s2 of {t, l, s :=
-    t ++str "-delete", sub l 2, deleteMany [1; 8] s};
+  case s2 of {
+    t, l, s := t ++str "-delete", sub l 2, deleteMany [1; 8] s
+  };
 
 s3 : TestDescr := "s3", 6, fromList [5; 4; 3; 2; 1; 0];
 
 s4 : TestDescr := "s4", 5, 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 (snd (snd s1))))
+  ]
     ++ concatMap mkTests [s1; s2; s3; s4; s2-delete];
 
 main : IO :=

Test/Map.juvix

@@ -17,40 +17,45 @@ tests : List Test :=
       | actual expected :=
         assertEqual
           "lists are not equal"
-          (quickSort ordProductI actual)
+          (quickSort actual)
           expected;
-  in [testCase
-    "Map.lookup missing key"
-    (assertNothing
-      (const "found a key expected to be missing")
-      (Map.lookup 10 m)); testCase
-    "Map.lookup available key"
-    (assertJust
-      "could not find expected key"
-      (Map.lookup 2 m)); testCase
-    "Map.length computes the number of keys in the map"
-    (assertEqual "expected length 2" (Map.size m) 2); testCase
-    "Map.toList computes the expected members"
-    (assertEqListPair (Map.toList m2) [1, 2; 3, 4]); testCase
-    "Map.insert-with replaces duplicates using merge function"
-    (assertEqListPair
-      (Map.toList (Map.insertWith (+) 1 3 m2))
-      [1, 5; 3, 4]); testCase
-    "Map.fromListWith de-duplicates using merge function"
-    (assertEqListPair
-      (Map.toList (Map.fromListWith (+) [1, 1; 1, 2]))
-      [1, 3]); testCase
-    "Map.fromList can be used to create the empty Map"
-    (assertEqListPair
-      (Map.toList (Map.fromList nil))
-      (nil)); testCase
-    "Map.fromList overwrites duplicates"
-    (assertEqListPair
-      (Map.toList (Map.fromList [1, 1; 1, 2]))
-      [1, 2]); testCase
-    "Map.fromList distinct keys"
-    (assertEqListPair
-      (Map.toList (Map.fromList [1, 1; 2, 2]))
-      [1, 1; 2, 2])];
+  in [ testCase
+       "Map.lookup missing key"
+       (assertNothing
+         (const "found a key expected to be missing")
+         (Map.lookup 10 m))
+     ; testCase
+       "Map.lookup available key"
+       (assertJust "could not find expected key" (Map.lookup 2 m))
+     ; testCase
+       "Map.length computes the number of keys in the map"
+       (assertEqual "expected length 2" (Map.size m) 2)
+     ; testCase
+       "Map.toList computes the expected members"
+       (assertEqListPair (Map.toList m2) [1, 2; 3, 4])
+     ; testCase
+       "Map.insert-with replaces duplicates using merge function"
+       (assertEqListPair
+         (Map.toList (Map.insertWith (+) 1 3 m2))
+         [1, 5; 3, 4])
+     ; testCase
+       "Map.fromListWith de-duplicates using merge function"
+       (assertEqListPair
+         (Map.toList (Map.fromListWith (+) [1, 1; 1, 2]))
+         [1, 3])
+     ; testCase
+       "Map.fromList can be used to create the empty Map"
+       (assertEqListPair (Map.toList (Map.fromList nil)) (nil))
+     ; testCase
+       "Map.fromList overwrites duplicates"
+       (assertEqListPair
+         (Map.toList (Map.fromList [1, 1; 1, 2]))
+         [1, 2])
+     ; testCase
+       "Map.fromList distinct keys"
+       (assertEqListPair
+         (Map.toList (Map.fromList [1, 1; 2, 2]))
+         [1, 1; 2, 2])
+     ];
 
 main : IO := runTestSuite (testSuite "Map" tests);

Test/Queue.juvix

@@ -21,32 +21,36 @@ tests : List Test :=
     checkWithList : Queue Nat -> List Nat -> Assertion
       | q q' :=
         assertEqual "Queue should be equal" q (fromList q');
-  in [testCase
-    "Queue.empty should be empty"
-    (checkWithList q []); testCase
-    "Queue.push should add an element"
-    (checkWithList q1 [1]); testCase
-    "Queue.push first element should be first pushed"
-    (checkWithList q2 [1; 2]); testCase
-    "Queue.head should return first element"
-    (assertEqual
-      "head of queue q3"
-      (head q3)
-      (just 1)); testCase
-    "Queue.fromList composes with toList should be the identity"
-    (assertEqual
-      "fromList . toList should be the identity"
-      (fromList ∘ toList $ q3)
-      q3); testCase
-    "Queue.pop should remove first element"
-    (assertEqual
-      "pop of queue q3"
-      (pop q3)
-      (just (1, fromList [2; 3]))); testCase
-    "Queue.tail should return queue without first element"
-    (assertEqual
-      "tail of queue q3"
-      (tail q3)
-      ((just ∘ fromList) [2; 3]))];
+  in [ testCase
+       "Queue.empty should be empty"
+       (checkWithList q [])
+     ; testCase
+       "Queue.push should add an element"
+       (checkWithList q1 [1])
+     ; testCase
+       "Queue.push first element should be first pushed"
+       (checkWithList q2 [1; 2])
+     ; testCase
+       "Queue.head should return first element"
+       (assertEqual "head of queue q3" (head q3) (just 1))
+     ; testCase
+       "Queue.fromList composes with toList should be the identity"
+       (assertEqual
+         "fromList . toList should be the identity"
+         (fromList ∘ toList $ q3)
+         q3)
+     ; testCase
+       "Queue.pop should remove first element"
+       (assertEqual
+         "pop of queue q3"
+         (pop q3)
+         (just (1, fromList [2; 3])))
+     ; testCase
+       "Queue.tail should return queue without first element"
+       (assertEqual
+         "tail of queue q3"
+         (tail q3)
+         ((just ∘ fromList) [2; 3]))
+     ];
 
 main : IO := runTestSuite $ testSuite "Queue" tests;