diff --git a/Data/Map.juvix b/Data/Map.juvix index 1e64b1c..0cac752 100644 --- a/Data/Map.juvix +++ b/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) diff --git a/Data/Set/AVL.juvix b/Data/Set/AVL.juvix index ec92081..8fe7bde 100644 --- a/Data/Set/AVL.juvix +++ b/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,8 +137,9 @@ 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) := @@ -150,6 +147,7 @@ delete {A} {{Ord A}} (x : A) : AVLTree A -> AVLTree A := | 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; diff --git a/Data/String.juvix b/Data/String.juvix deleted file mode 100644 index db6c806..0000000 --- a/Data/String.juvix +++ /dev/null @@ -1,6 +0,0 @@ -module Data.String; - -import Stdlib.Prelude open; -import Stdlib.Data.String.Ord open; - -null? (s : String) : Bool := s == ""; diff --git a/Makefile b/Makefile index 220f8a3..14dbb09 100644 --- a/Makefile +++ b/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 diff --git a/Package.juvix b/Package.juvix new file mode 100644 index 0000000..93faeac --- /dev/null +++ b/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" + ]}; diff --git a/Test/AVL.juvix b/Test/AVL.juvix index a5174cd..d7e4ca6 100644 --- a/Test/AVL.juvix +++ b/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 := diff --git a/Test/Map.juvix b/Test/Map.juvix index 46143cb..df66c5b 100644 --- a/Test/Map.juvix +++ b/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); diff --git a/Test/Queue.juvix b/Test/Queue.juvix index ceb2500..4d4ff6d 100644 --- a/Test/Queue.juvix +++ b/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; diff --git a/Test/UnbalancedSet.juvix b/Test/UnbalancedSet.juvix index 82df585..9c40026 100644 --- a/Test/UnbalancedSet.juvix +++ b/Test/UnbalancedSet.juvix @@ -11,28 +11,31 @@ tests : List Test := s : UnbalancedSet Nat := Set.insert 1 - (Set.insert - 3 - (Set.insert 2 (Set.insert 1 Set.empty))); + (Set.insert 3 (Set.insert 2 (Set.insert 1 Set.empty))); setInSet : UnbalancedSet (UnbalancedSet Nat) := Set.insert s Set.empty; - in [testCase - "Set.length computes the expected size" - (assertEqual "unexpected size" (Set.length s) 3); testCase - "Set.to-list computes the expected members" - (assertEqual - "unexpected memebrs" - (quickSort ordNatI (Set.to-list s)) - [1; 2; 3]); testCase - "Set.member? computes true for expected member" - (assertTrue - "expected member is not present" - (Set.member? 1 s)); testCase - "Set.member? computes false for unexpected member" - (assertFalse - "unexpected member is present" - (Set.member? 0 s)); testCase - "setInSet has length 1" - (assertEqual "unexpected size" (Set.length setInSet) 1)]; + in [ testCase + "Set.length computes the expected size" + (assertEqual "unexpected size" (Set.length s) 3) + ; testCase + "Set.to-list computes the expected members" + (assertEqual + "unexpected memebrs" + (quickSort (Set.to-list s)) + [1; 2; 3]) + ; testCase + "Set.member? computes true for expected member" + (assertTrue + "expected member is not present" + (Set.member? 1 s)) + ; testCase + "Set.member? computes false for unexpected member" + (assertFalse + "unexpected member is present" + (Set.member? 0 s)) + ; testCase + "setInSet has length 1" + (assertEqual "unexpected size" (Set.length setInSet) 1) + ]; main : IO := runTestSuite (testSuite "Set" tests); diff --git a/juvix.lock.yaml b/juvix.lock.yaml new file mode 100644 index 0000000..535157d --- /dev/null +++ b/juvix.lock.yaml @@ -0,0 +1,19 @@ +# This file was autogenerated by Juvix version 0.5.4. +# Do not edit this file manually. + +dependencies: +- git: + name: anoma_juvix-stdlib + ref: f68b0614ad695eaa13ead42f3466e0a78219f826 + url: https://github.com/anoma/juvix-stdlib + dependencies: [] +- git: + name: anoma_juvix-test + ref: 3ed8a393b45c75af2c2f4bc0b5262ce9f1115a05 + url: https://github.com/anoma/juvix-test + dependencies: + - git: + name: anoma_juvix-stdlib + ref: f68b0614ad695eaa13ead42f3466e0a78219f826 + url: https://github.com/anoma/juvix-stdlib + dependencies: [] diff --git a/juvix.yaml b/juvix.yaml deleted file mode 100644 index e83646c..0000000 --- a/juvix.yaml +++ /dev/null @@ -1,11 +0,0 @@ -name: containers -version: 0.7.0 -dependencies: - - git: - url: https://github.com/anoma/juvix-stdlib - ref: 4facf14d9b2d06b81ce1be1882aa9050f768cb45 - name: stdlib - - git: - url: https://github.com/anoma/juvix-test - ref: v0.6.1 - name: test