diff --git a/test/Package.juvix b/test/Package.juvix index f1818403..e8de4c9c 100644 --- a/test/Package.juvix +++ b/test/Package.juvix @@ -9,5 +9,5 @@ package : Package := ; github "anoma" "juvix-quickcheck" - "97e39ade9a20580d68d9cfe8f74d2d38773962ba" + "714f0b9ff786f1582a92157da967d216e454c6a8" ]}; diff --git a/test/Test.juvix b/test/Test.juvix index 69ab320f..0e2c509c 100644 --- a/test/Test.juvix +++ b/test/Test.juvix @@ -9,6 +9,7 @@ import Data.String open; import Test.QuickCheckTest as QC; import Test.Arb as QC; +import Test.StdlibTestExtra; prop-reverseDoesNotChangeLength : List Int -> Bool | xs := length (reverse xs) == length xs; @@ -126,48 +127,87 @@ prop-transposeMatrixDimensions : List (List Int) -> Bool in checkTxsRowXsCol && checkXsRowTxsCol; prop-foundElementSatisfiesPredicate - (p : Int -> Bool) - (xs : List Int) : Bool := + (p : Int -> Bool) (xs : List Int) : Bool := case find p xs of | just x := p x | nothing := true; prop-nonExistenceImpliesPredicateFalseForAll - (p : Int -> Bool) - (xs : List Int) : Bool := + (p : Int -> Bool) (xs : List Int) : Bool := case find p xs of - | (just _) := true + | just _ := true | nothing := all (x in xs) not (p x); prop-findConsistentWithSplitAt - (n : Nat) - (p : Int -> Bool) - (xs : List Int) : Bool := - let ys×zs := splitAt n xs; - ys := fst ys×zs; - zs := snd ys×zs - in - case find p xs of - | (just x) := if + (n : Nat) (p : Int -> Bool) (xs : List Int) : Bool := + let + ys×zs := splitAt n xs; + ys := fst ys×zs; + zs := snd ys×zs; + in case find p xs of + | just x := + if | elem (==) x ys := find p ys == just x | elem (==) x zs := find p zs == just x | else := false | nothing := true; -prop-findWithEmptyList - (p : Int -> Bool) : Bool := find p [] == nothing; +prop-findWithEmptyList (p : Int -> Bool) : Bool := + find p [] == nothing; prop-findWithAlwaysTrueIsJust (xs : List Int) : Bool := if - | null xs := true - | else := - case find (const true) xs of - | (just _) := true - | nothing := false; + | null xs := true + | else := + case find (const true) xs of + | just _ := true + | nothing := false; prop-findWithAlwaysFalseIsNothing (xs : List Int) : Bool := find (const false) xs == nothing; +prop-eitherLeftApplication + (f : Int -> Int) (g : Int -> Int) (x : Int) : Bool := + either f g (left x) == f x; + +prop-eitherRightApplication + (f : Int -> Int) (g : Int -> Int) (x : Int) : Bool := + either f g (right x) == g x; + +prop-eitherIsLeft : Either Int Bool -> Bool + | x@(left _) := isLeft x + | x@(right _) := not (isLeft x); + +prop-eitherIsRight : Either Int Bool -> Bool + | x@(left _) := not (isRight x) + | x@(right _) := isRight x; + +prop-eitherFromLeftDefault + (defaultLeft : Int) : Either Int Bool -> Bool + | e@(left x) := fromLeft defaultLeft e == x + | e@(right _) := fromLeft defaultLeft e == defaultLeft; + +prop-eitherFromRightDefault + (defaultRight : Bool) : Either Int Bool -> Bool + | e@(left _) := fromRight defaultRight e == defaultRight + | e@(right x) := fromRight defaultRight e == x; + +prop-eitherToMaybe : Either Int Bool -> Bool + | e@(left _) := eitherToMaybe e == nothing + | e@(right x) := eitherToMaybe e == just x; + +prop-maybeToEither (def : Int) : Maybe Bool -> Bool + | m@(just x) := maybeToEither def m == right x + | m@nothing := maybeToEither def m == left def; + +prop-eitherMapLeft (f : Int -> Int) : Either Int Int -> Bool + | e@(left x) := mapLeft f e == left (f x) + | e@(right _) := mapLeft f e == e; + +prop-eitherMapRight (f : Int -> Int) : Either Int Int -> Bool + | e@(left _) := mapRight f e == e + | e@(right x) := mapRight f e == right (f x); + sortTest : String -> (List Int -> List Int) -> QC.Test | sortName sort := QC.mkTest @@ -273,32 +313,96 @@ findWithAlwaysFalseIsNothing : QC.Test := "find: always false predicate returns nothing" prop-findWithAlwaysFalseIsNothing; +eitherEitherLeftApplication : QC.Test := + QC.mkTest + "either: either left application" + prop-eitherLeftApplication; + +eitherEitherRightApplication : QC.Test := + QC.mkTest + "either: either right application" + prop-eitherRightApplication; + +eitherIsLeft : QC.Test := + QC.mkTest "either: isLeft detects left" prop-eitherIsLeft; + +eitherIsRight : QC.Test := + QC.mkTest + "either: isRight detects right" + prop-eitherIsRight; + +eitherFromLeft : QC.Test := + QC.mkTest + "either: fromLeft uses default" + prop-eitherFromLeftDefault; + +eitherFromRight : QC.Test := + QC.mkTest + "either: fromRight uses default" + prop-eitherFromRightDefault; + +eitherEitherToMaybe : QC.Test := + QC.mkTest + "either: eitherToMaybe" + prop-eitherToMaybe; + +eitherMaybeToEither : QC.Test := + QC.mkTest + "either: maybeToEither" + prop-maybeToEither; + +eitherMapLeft : QC.Test := + QC.mkTest + "either: mapLeft" + prop-eitherMapLeft; + +eitherMapRight : QC.Test := + QC.mkTest + "either: mapRight" + prop-eitherMapRight; + main : IO := readLn \ {seed := - QC.runTestsIO - 100 - (stringToNat seed) - [ partitionTest - ; reverseLengthTest - ; reverseReverseIdTest - ; splitAtRecombineTest - ; splitAtLengthTest - ; mergeSumLengthsTest - ; tailLengthOneLessTest - ; equalCompareToEqTest - ; zipTest - ; zipWithTest - ; snocTest - ; dropTest - ; sortTest "mergeSort" mergeSort - ; sortTest "quickSort" quickSort - ; transposeMatrixIdTest - ; transposeMatrixDimentionsTest - ; findFoundElementSatisfiesPredicate - ; findNonExistenceImpliesPredicateFalseForAll - ; findConsistentWithSplitAt - ; findOnEmptyListIsNothing - ; findWithAlwaysTrueIsJust - ; findWithAlwaysFalseIsNothing - ]}; + let + seedNat := stringToNat seed; + in QC.runTestsIO + 100 + seedNat + [ partitionTest + ; reverseLengthTest + ; reverseReverseIdTest + ; splitAtRecombineTest + ; splitAtLengthTest + ; mergeSumLengthsTest + ; tailLengthOneLessTest + ; equalCompareToEqTest + ; zipTest + ; zipWithTest + ; snocTest + ; dropTest + ; sortTest "mergeSort" mergeSort + ; sortTest "quickSort" quickSort + ; transposeMatrixIdTest + ; transposeMatrixDimentionsTest + ; findFoundElementSatisfiesPredicate + ; findNonExistenceImpliesPredicateFalseForAll + ; findConsistentWithSplitAt + ; findOnEmptyListIsNothing + ; findWithAlwaysTrueIsJust + ; findWithAlwaysFalseIsNothing + ] + >>> QC.runTestsIO + 100 + seedNat + [ eitherEitherLeftApplication + ; eitherEitherRightApplication + ; eitherIsLeft + ; eitherIsRight + ; eitherFromLeft + ; eitherFromRight + ; eitherEitherToMaybe + ; eitherMaybeToEither + ; eitherMapLeft + ; eitherMapRight + ]}; diff --git a/test/Test/StdlibTestExtra.juvix b/test/Test/StdlibTestExtra.juvix new file mode 100644 index 00000000..0b3e6f3a --- /dev/null +++ b/test/Test/StdlibTestExtra.juvix @@ -0,0 +1,12 @@ +module Test.StdlibTestExtra; + +import Stdlib.Prelude open; + +instance +eitherShow + {A B} {{Show A}} {{Show B}} : Show (Either A B) := + mkShow@{ + show : Either A B -> String + | (left x) := "Left (" ++str Show.show x ++str ")" + | (right x) := "Right (" ++str Show.show x ++str ")" + }; diff --git a/test/juvix.lock.yaml b/test/juvix.lock.yaml index 4c239945..e1765e8a 100644 --- a/test/juvix.lock.yaml +++ b/test/juvix.lock.yaml @@ -2,17 +2,17 @@ # Do not edit this file manually. version: 2 -checksum: 35ab63e68bf138cd895e3af709ef02d8fc1253c4a0069d0475de3899b93cc6ff +checksum: 37861064a35c2935c03f50213a4437637d1a404f67b63533b7e8d3c46b436bda dependencies: - path: ../ dependencies: [] - git: name: anoma_juvix-quickcheck - ref: 97e39ade9a20580d68d9cfe8f74d2d38773962ba + ref: 714f0b9ff786f1582a92157da967d216e454c6a8 url: https://github.com/anoma/juvix-quickcheck dependencies: - git: name: anoma_juvix-stdlib - ref: 9d5b726e1dd885cd7784ec0bfabb448de0ac79dc + ref: c62c15e8538f5c8ac69aa270a46c0aeb8c185fa4 url: https://github.com/anoma/juvix-stdlib dependencies: []