Skip to content

Commit

Permalink
Add tests for Either
Browse files Browse the repository at this point in the history
  • Loading branch information
paulcadman committed Jul 9, 2024
1 parent c62c15e commit 7056dfc
Show file tree
Hide file tree
Showing 4 changed files with 167 additions and 51 deletions.
2 changes: 1 addition & 1 deletion test/Package.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -9,5 +9,5 @@ package : Package :=
; github
"anoma"
"juvix-quickcheck"
"97e39ade9a20580d68d9cfe8f74d2d38773962ba"
"714f0b9ff786f1582a92157da967d216e454c6a8"
]};
198 changes: 151 additions & 47 deletions test/Test.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
]};
12 changes: 12 additions & 0 deletions test/Test/StdlibTestExtra.juvix
Original file line number Diff line number Diff line change
@@ -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 ")"
};
6 changes: 3 additions & 3 deletions test/juvix.lock.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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: []

0 comments on commit 7056dfc

Please sign in to comment.