diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index 4a8f069d..47acb4f2 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/Stdlib/Data/List/Base.juvix @@ -8,7 +8,6 @@ import Stdlib.Data.Nat.Base open; import Stdlib.Data.Maybe.Base open; import Stdlib.Trait.Ord open; import Stdlib.Data.Product.Base open; -import Stdlib.Trait.Ord open; syntax operator :: cons; --- Inductive list. @@ -100,14 +99,15 @@ splitAt {A} : Nat → List A → List A × List A case splitAt m xs of {l1, l2 := x :: l1, l2}; --- 𝒪(𝓃 + 𝓂). Merges two lists according the given ordering. -merge {A} : Ord A → List A → List A → List A - | o@(mkOrd cmp) (x :: xs) (y :: ys) := +terminating +merge {A} {{Ord A}} : List A → List A → List A + | xs@(x :: xs') ys@(y :: ys') := if - (isLT (cmp x y)) - (x :: merge o xs (y :: ys)) - (y :: merge o (x :: xs) ys) - | _ nil ys := ys - | _ xs nil := xs; + (isLT (Ord.cmp x y)) + (x :: merge xs' ys) + (y :: merge xs ys') + | nil ys := ys + | xs nil := xs; --- 𝒪(𝓃). Returns a tuple where the first component has the items that --- satisfy the predicate and the second component has the elements that don't. @@ -184,7 +184,7 @@ zip {A B} : List A -> List B -> List (A × B) --- 𝒪(𝓃 log 𝓃). Sorts a list of elements in ascending order using the MergeSort --- algorithm. -mergeSort {A} (o : Ord A) (l : List A) : List A := +mergeSort {A} {{Ord A}} (l : List A) : List A := let terminating go : Nat -> List A -> List A @@ -196,23 +196,22 @@ mergeSort {A} (o : Ord A) (l : List A) : List A := splitXs : List A × List A := splitAt len' xs; left : List A := fst splitXs; right : List A := snd splitXs; - in merge o (go len' left) (go (sub len len') right); + in merge (go len' left) (go (sub len len') right); in go (length l) l; --- On average 𝒪(𝓃 log 𝓃), worst case 𝒪(𝓃²). Sorts a list of elements in --- ascending order using the QuickSort algorithm. terminating -quickSort {A} : Ord A → List A → List A - | (mkOrd cmp) := - let - terminating - go : List A → List A - | nil := nil - | xs@(_ :: nil) := xs - | (x :: xs) := - case partition (isGT ∘ cmp x) xs of {l1, l2 := - go l1 ++ x :: go l2}; - in go; +quickSort {A} {{Ord A}} : List A → List A := + let + terminating + go : List A → List A + | nil := nil + | xs@(_ :: nil) := xs + | (x :: xs) := + case partition (isGT ∘ Ord.cmp x) xs of {l1, l2 := + go l1 ++ x :: go l2}; + in go; --- 𝒪(𝓃) Filters out every ;nothing; from a ;List;. catMaybes {A} : List (Maybe A) -> List A diff --git a/test/Test.juvix b/test/Test.juvix index 748a12ec..587611f3 100644 --- a/test/Test.juvix +++ b/test/Test.juvix @@ -43,8 +43,7 @@ prop-splitAtLength : Nat -> List Int -> Bool prop-mergeSumLengths : List Int -> List Int -> Bool | xs ys := - length xs Nat.+ length ys - Nat.== length (merge ordIntI xs ys); + length xs Nat.+ length ys Nat.== length (merge xs ys); prop-partition : List Int -> (Int -> Bool) -> Bool | xs p := @@ -137,109 +136,104 @@ prop-transposeMatrixDimensions : List (List Int) -> Bool sortTest : String -> (List Int -> List Int) -> QC.Test | sortName sort := QC.mkTest - (QC.testableFunction QC.argumentListInt QC.testableBool) ("sort properties: " ++str sortName) - (prop-sort sort); + (QC.mkFun (prop-sort sort)); dropTest : QC.Test := QC.mkTest - (QC.testableFunction - QC.argumentNat - (QC.testableFunction QC.argumentListInt QC.testableBool)) "drop properties" - prop-drop; + (QC.mkFun \ {a := QC.mkFun \ {b := prop-drop a b}}); snocTest : QC.Test := QC.mkTest - (QC.testableFunction - QC.argumentListInt - (QC.testableFunction QC.argumentInt QC.testableBool)) "snoc properties" - prop-snoc; + (QC.mkFun \ {a := QC.mkFun \ {b := prop-snoc a b}}); zipTest : QC.Test := QC.mkTest - QC.testableListIntListInt "zip properties" - prop-zip; + (QC.mkFun \ {a := QC.mkFun \ {b := prop-zip a b}}); zipWithTest : QC.Test := QC.mkTest - QC.testableHofIntIntListIntListInt "zipWith properties" - prop-zipWith; + (QC.mkFun + \ {a := + QC.mkFun + \ {b := + QC.mkFun + \ {c := + prop-zipWith \ {x := QC.Fun.fun (QC.Fun.fun a x)} b c}}}); equalCompareToEqTest : QC.Test := QC.mkTest - (QC.testableFunction QC.argumentNat QC.testableBool) "equal Nats compare to EQ" - prop-equal-compare-to-eq; + (QC.mkFun prop-equal-compare-to-eq); gcdNoCoprimeTest : QC.Test := QC.mkTest - QC.testableBinaryInt "no integers are coprime" - prop-gcd-bad; + (QC.mkFun \ {a := QC.mkFun \ {b := prop-gcd-bad a b}}); partitionTest : QC.Test := QC.mkTest - QC.testableListIntHofIntBool "partition: recombination of the output equals the input" - prop-partition; + (QC.mkFun + \ {a := QC.mkFun \ {b := prop-partition a (QC.Fun.fun b)}}); testDistributive : QC.Test := QC.mkTest - QC.testableIntIntHofIntInt "all functions are distributive over +" - prop-distributive; + (QC.mkFun + \ {a := + QC.mkFun + \ {b := + QC.mkFun \ {c := prop-distributive a b (QC.Fun.fun c)}}}); reverseLengthTest : QC.Test := QC.mkTest - QC.testableListInt "reverse preserves length" - prop-reverseDoesNotChangeLength; + (QC.mkFun prop-reverseDoesNotChangeLength); reverseReverseIdTest : QC.Test := QC.mkTest - QC.testableListInt "reverse of reverse is identity" - prop-reverseReverseIsIdentity; + (QC.mkFun prop-reverseReverseIsIdentity); splitAtRecombineTest : QC.Test := QC.mkTest - QC.testableNatListInt "splitAt: recombination of the output is equal to the input list" - prop-splitAtRecombine; + (QC.mkFun + \ {a := QC.mkFun \ {b := prop-splitAtRecombine a b}}); splitAtLengthTest : QC.Test := QC.mkTest - QC.testableNatListInt "splitAt: Check lengths of output if the input Nat is greater than the length of the input list" - prop-splitAtLength; + (QC.mkFun + \ {a := QC.mkFun \ {b := prop-splitAtLength a b}}); mergeSumLengthsTest : QC.Test := QC.mkTest - QC.testableListIntListInt "merge: sum of the lengths of input lists is equal to the length of output list" - prop-mergeSumLengths; + (QC.mkFun + \ {a := QC.mkFun \ {b := prop-mergeSumLengths a b}}); tailLengthOneLessTest : QC.Test := QC.mkTest - QC.testableListInt "tail: length of output is one less than input unless empty" - prop-tailLengthOneLess; + (QC.mkFun prop-tailLengthOneLess); transposeMatrixIdTest : QC.Test := QC.mkTest - (QC.testableFunction QC.argumentMatrixInt QC.testableBool) + {{QC.testableFunction {{showListI}} {{QC.arbitraryMatrix}}}} "transpose: recrangular matrix has property transpose . transpose = id" - prop-transposeMatrixId; + (QC.mkFun prop-transposeMatrixId); transposeMatrixDimentionsTest : QC.Test := QC.mkTest - (QC.testableFunction QC.argumentMatrixInt QC.testableBool) + {{QC.testableFunction {{showListI}} {{QC.arbitraryMatrix}}}} "transpose: transpose swaps dimensions" - prop-transposeMatrixDimensions; + (QC.mkFun prop-transposeMatrixDimensions); main : IO := readLn @@ -259,8 +253,8 @@ main : IO := :: zipWithTest :: snocTest :: dropTest - :: sortTest "mergeSort" (mergeSort ordIntI) - :: sortTest "quickSort" (quickSort ordIntI) + :: sortTest "mergeSort" mergeSort + :: sortTest "quickSort" quickSort :: transposeMatrixIdTest :: transposeMatrixDimentionsTest :: nil)}; diff --git a/test/Test/Arb.juvix b/test/Test/Arb.juvix index 5980356f..cf9f3966 100644 --- a/test/Test/Arb.juvix +++ b/test/Test/Arb.juvix @@ -6,11 +6,11 @@ import Test.QuickCheck.Arbitrary open; import Test.QuickCheck.Gen open; import Data.Random open; -arbitrarySizedList - : {A : Type} -> Nat -> Arbitrary A -> Arbitrary (List A) - | {A} size (arbitrary g) := - arbitrary - (gen +arbitrarySizedList {A} (size : Nat) + : Arbitrary A -> Arbitrary (List A) + | (mkArbitrary g) := + mkArbitrary + (mkGen \ {rand := let randList : StdGen -> Nat -> List A @@ -20,23 +20,19 @@ arbitrarySizedList rSplit : StdGen × StdGen := stdSplit r; r1 : StdGen := fst rSplit; r2 : StdGen := snd rSplit; - in runGen g r1 :: randList r2 n; + in Gen.run g r1 :: randList r2 n; in randList rand size}); --- Generate an arbitrary rectangular matrix -arbitraryMatrix - : {A : Type} -> Arbitrary A -> Arbitrary (List (List A)) - | {A} arbA := - arbitrary - (gen - \ {rand := - let - randSplit : StdGen × StdGen := stdSplit rand; - rand1 : StdGen := fst randSplit; - rand2 : StdGen := snd randSplit; - cols : Nat := fst (randNat rand1 1 10); - arbRow : Arbitrary (List A) := arbitrarySizedList cols arbA; - in runArb (arbitraryList arbRow) rand2}); - -argumentMatrixInt : Argument (List (List Int)) := - argument showListI (arbitraryMatrix arbitraryInt); +arbitraryMatrix {A} {{arbA : Arbitrary A}} + : Arbitrary (List (List A)) := + mkArbitrary + (mkGen + \ {rand := + let + randSplit : StdGen × StdGen := stdSplit rand; + rand1 : StdGen := fst randSplit; + rand2 : StdGen := snd randSplit; + cols : Nat := fst (randNat rand1 1 10); + arbRow : Arbitrary (List A) := arbitrarySizedList cols arbA; + in runArb {{arbitraryList {{arbRow}}}} rand2}); diff --git a/test/juvix.yaml b/test/juvix.yaml index 31618b1e..414a0c9f 100644 --- a/test/juvix.yaml +++ b/test/juvix.yaml @@ -2,7 +2,7 @@ dependencies: - ../ - git: url: https://github.com/anoma/juvix-quickcheck.git - ref: update-for-0.5.0 + ref: v0.7.1 name: quickcheck name: stdlib-test version: 0.0.0