From 216cb609cbe5aec9badea858f151a5ea400f2e66 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Wed, 10 Jul 2024 16:32:49 +0100 Subject: [PATCH] Add `Stdlib.Data.Result` and `find` in `Stdlib.Data.List` (#106) This PR adds implementations of the following, with corresponding tests: * An `Result` type with associated functions to the standard library. * A `find` function to `Stdlib.Data.List` Requirements for both arose when writing Anoma applications. NB: Adding the `{-# specialize: [1] #-}` pragma to `find` causes the compiler to go into an infinite loop when compiling a `find` call with predicate `const false`, e.g ``` find {Nat} (const false) [1;2;3] ``` So I've omitted that for now and ~~I'll raise a separate bug~~, I suspect I was using the `specialize` pragma incorrectly. --- Stdlib/Data/List/Base.juvix | 9 ++ Stdlib/Data/Result.juvix | 26 ++++ Stdlib/Data/Result/Base.juvix | 60 +++++++++ Stdlib/Prelude.juvix | 1 + test/Package.juvix | 2 +- test/Test.juvix | 216 +++++++++++++++++++++++++++++--- test/Test/StdlibTestExtra.juvix | 12 ++ test/juvix.lock.yaml | 8 +- 8 files changed, 309 insertions(+), 25 deletions(-) create mode 100644 Stdlib/Data/Result.juvix create mode 100644 Stdlib/Data/Result/Base.juvix create mode 100644 test/Test/StdlibTestExtra.juvix diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index 258fb67b..956b5279 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/Stdlib/Data/List/Base.juvix @@ -16,6 +16,15 @@ elem {A} (eq : A → A → Bool) (s : A) : List A → Bool | nil := false | (x :: xs) := eq s x || elem eq s xs; +--- 𝒪(𝓃). Returns the leftmost element of the list satisfying the predicate or +--- nothing if there's no such element. +find {A} (predicate : A → Bool) : List A → Maybe A + | nil := nothing + | (x :: xs) := + if + | predicate x := just x + | else := find predicate xs; + --- Right-associative fold. {-# specialize: [1] #-} foldr {A B} (f : A → B → B) (z : B) : List A → B diff --git a/Stdlib/Data/Result.juvix b/Stdlib/Data/Result.juvix new file mode 100644 index 00000000..248aad16 --- /dev/null +++ b/Stdlib/Data/Result.juvix @@ -0,0 +1,26 @@ +module Stdlib.Data.Result; + +import Stdlib.Data.Result.Base open public; +import Stdlib.Data.Bool.Base open; + +import Stdlib.Trait.Eq open; +import Stdlib.Trait.Ord open; + +instance +ordResultI {A B} {{Ord A}} {{Ord B}} : Ord (Result A B) := + mkOrd@{ + cmp : Result A B -> Result A B -> Ordering + | (error a1) (error a2) := Ord.cmp a1 a2 + | (ok b1) (ok b2) := Ord.cmp b1 b2 + | (error _) (ok _) := LT + | (ok _) (error _) := GT + }; + +instance +eqResultI {A B} {{Eq A}} {{Eq B}} : Eq (Result A B) := + mkEq@{ + eq : Result A B -> Result A B -> Bool + | (error a1) (error a2) := a1 == a2 + | (ok b1) (ok b2) := b1 == b2 + | _ _ := false + }; diff --git a/Stdlib/Data/Result/Base.juvix b/Stdlib/Data/Result/Base.juvix new file mode 100644 index 00000000..7c1239ca --- /dev/null +++ b/Stdlib/Data/Result/Base.juvix @@ -0,0 +1,60 @@ +module Stdlib.Data.Result.Base; + +import Stdlib.Data.Bool.Base open; +import Stdlib.Data.Maybe.Base open; +import Stdlib.Function open; + +--- The Result type represents either a success with a value of `ok` or an error +--- with value `error`. +type Result E A := + | error E + | ok A; + +--- Apply the onError function if the value is ;error; or apply the +--- onOk function if the value is ;ok;. +handleResult + {E A B} + (onError : E -> B) + (onOk : A -> B) + : Result E A -> B + | (error a) := onError a + | (ok a) := onOk a; + +--- Apply a function to the ;error; value of a Result. +mapError + {A E1 E2} (f : E1 -> E2) : Result E1 A -> Result E2 A := + handleResult (f >> error) ok; + +--- Apply a function to the ;ok; value of a Result. +mapOk {E A C} (f : A -> C) : Result E A -> Result E C := + handleResult error (f >> ok); + +--- Return ;true; if the value is an ;error;, otherwise ;false;. +isError {E A} : Result E A -> Bool + | (error _) := true + | (ok _) := false; + +--- Return ;true; if the value is ;ok;, otherwise ;false;. +isOk {E A} : Result E A -> Bool + | (error _) := false + | (ok _) := true; + +--- Return the contents of an ;error; value, otherwise return a default. +fromError {E A} (default : E) : Result E A -> E + | (error a) := a + | (ok _) := default; + +--- Return the contents of an ;ok; value, otherwise return a default. +fromOk {E A} (default : A) : Result E A -> A + | (error _) := default + | (ok b) := b; + +--- Convert a Result to a Maybe. An ;error; value becomes `nothing`. +resultToMaybe {E A} : Result E A -> Maybe A := + handleResult (const nothing) just; + +--- Convert a Maybe to a Result. A ;nothing; value becomes `error defaultError`. +maybeToResult + {E A} (defaultError : E) : Maybe A -> Result E A + | nothing := error defaultError + | (just x) := ok x; diff --git a/Stdlib/Prelude.juvix b/Stdlib/Prelude.juvix index 225942ab..5e4a817f 100644 --- a/Stdlib/Prelude.juvix +++ b/Stdlib/Prelude.juvix @@ -12,6 +12,7 @@ import Stdlib.Data.Int open public; import Stdlib.Data.Field open public; import Stdlib.Data.Pair open public; import Stdlib.Data.String open public; +import Stdlib.Data.Result open public; import Stdlib.Function open public; import Stdlib.System.IO open public; diff --git a/test/Package.juvix b/test/Package.juvix index b8c2c39d..3bb3adf2 100644 --- a/test/Package.juvix +++ b/test/Package.juvix @@ -9,5 +9,5 @@ package : Package := ; github "anoma" "juvix-quickcheck" - "8068d58360d2adecba3674a31e031e7ad992e0e1" + "8e5d49682fb0b861fc0a1aed95cfebab03231d85" ]}; diff --git a/test/Test.juvix b/test/Test.juvix index a5e25788..1571528e 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; @@ -125,6 +126,89 @@ prop-transposeMatrixDimensions : List (List Int) -> Bool | _ := null xs; in checkTxsRowXsCol && checkXsRowTxsCol; +prop-foundElementSatisfiesPredicate + (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 := + case find p xs of + | 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 + | 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-findWithAlwaysTrueIsJust (xs : List Int) : Bool := + if + | 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-resultErrorApplication + (f : Int -> Int) (g : Int -> Int) (x : Int) : Bool := + handleResult f g (error x) == f x; + +prop-resultOkApplication + (f : Int -> Int) (g : Int -> Int) (x : Int) : Bool := + handleResult f g (ok x) == g x; + +prop-resultIsError : Result Int Bool -> Bool + | x@(error _) := isError x + | x@(ok _) := not (isError x); + +prop-resultIsOk : Result Int Bool -> Bool + | x@(error _) := not (isOk x) + | x@(ok _) := isOk x; + +prop-resultFromErrorDefault + (defaultError : Int) : Result Int Bool -> Bool + | e@(error x) := fromError defaultError e == x + | e@(ok _) := fromError defaultError e == defaultError; + +prop-resultFromOkDefault + (defaultOk : Bool) : Result Int Bool -> Bool + | e@(error _) := fromOk defaultOk e == defaultOk + | e@(ok x) := fromOk defaultOk e == x; + +prop-resultToMaybe : Result Int Bool -> Bool + | e@(error _) := resultToMaybe e == nothing + | e@(ok x) := resultToMaybe e == just x; + +prop-maybeToResult (def : Int) : Maybe Bool -> Bool + | m@(just x) := maybeToResult def m == ok x + | m@nothing := maybeToResult def m == error def; + +prop-resultMapError + (f : Int -> Int) : Result Int Int -> Bool + | e@(error x) := mapError f e == error (f x) + | e@(ok _) := mapError f e == e; + +prop-resultMapOk (f : Int -> Int) : Result Int Int -> Bool + | e@(error _) := mapOk f e == e + | e@(ok x) := mapOk f e == ok (f x); + sortTest : String -> (List Int -> List Int) -> QC.Test | sortName sort := QC.mkTest @@ -200,26 +284,118 @@ transposeMatrixDimentionsTest : QC.Test := "transpose: transpose swaps dimensions" prop-transposeMatrixDimensions; +findFoundElementSatisfiesPredicate : QC.Test := + QC.mkTest + "find: found element satisfies predicate" + prop-foundElementSatisfiesPredicate; + +findNonExistenceImpliesPredicateFalseForAll : QC.Test := + QC.mkTest + "find: non existence implies predicate false for all" + prop-nonExistenceImpliesPredicateFalseForAll; + +findConsistentWithSplitAt : QC.Test := + QC.mkTest + "find: consistent with splitAt" + prop-findConsistentWithSplitAt; + +findOnEmptyListIsNothing : QC.Test := + QC.mkTest + "find: called with empty list is nothing" + prop-findWithEmptyList; + +findWithAlwaysTrueIsJust : QC.Test := + QC.mkTest + "find: always true predicate returns just" + prop-findWithAlwaysTrueIsJust; + +findWithAlwaysFalseIsNothing : QC.Test := + QC.mkTest + "find: always false predicate returns nothing" + prop-findWithAlwaysFalseIsNothing; + +resultResultErrorApplication : QC.Test := + QC.mkTest + "result: result error application" + prop-resultErrorApplication; + +resultResultOkApplication : QC.Test := + QC.mkTest + "result: result ok application" + prop-resultOkApplication; + +resultIsError : QC.Test := + QC.mkTest + "result: isError detects error" + prop-resultIsError; + +resultIsOk : QC.Test := + QC.mkTest "result: isOk detects ok" prop-resultIsOk; + +resultFromError : QC.Test := + QC.mkTest + "result: fromError uses default" + prop-resultFromErrorDefault; + +resultFromOk : QC.Test := + QC.mkTest + "result: fromOk uses default" + prop-resultFromOkDefault; + +resultResultToMaybe : QC.Test := + QC.mkTest "result: resultToMaybe" prop-resultToMaybe; + +resultMaybeToResult : QC.Test := + QC.mkTest "result: maybeToResult" prop-maybeToResult; + +resultMapError : QC.Test := + QC.mkTest "result: mapError" prop-resultMapError; + +resultMapOk : QC.Test := + QC.mkTest "result: mapOk" prop-resultMapOk; + 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 - ]}; + 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 + [ resultResultErrorApplication + ; resultResultOkApplication + ; resultIsError + ; resultIsOk + ; resultFromError + ; resultFromOk + ; resultResultToMaybe + ; resultMaybeToResult + ; resultMapError + ; resultMapOk + ]}; diff --git a/test/Test/StdlibTestExtra.juvix b/test/Test/StdlibTestExtra.juvix new file mode 100644 index 00000000..b658101a --- /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 (Result A B) := + mkShow@{ + show : Result A B -> String + | (error x) := "Error (" ++str Show.show x ++str ")" + | (ok x) := "Ok (" ++str Show.show x ++str ")" + }; diff --git a/test/juvix.lock.yaml b/test/juvix.lock.yaml index cff529ff..fb83cc54 100644 --- a/test/juvix.lock.yaml +++ b/test/juvix.lock.yaml @@ -1,18 +1,18 @@ -# This file was autogenerated by Juvix version 0.6.2. +# This file was autogenerated by Juvix version 0.6.3. # Do not edit this file manually. version: 2 -checksum: 5de68b52002fccbfacd5df82593d631368f3303203d03dc72f126e74a5997283 +checksum: 8013d01c2b6d46596d97438913b23987618efe1f7a6e54e7abd22dd5e0ae7f43 dependencies: - path: ../ dependencies: [] - git: name: anoma_juvix-quickcheck - ref: 8068d58360d2adecba3674a31e031e7ad992e0e1 + ref: 8e5d49682fb0b861fc0a1aed95cfebab03231d85 url: https://github.com/anoma/juvix-quickcheck dependencies: - git: name: anoma_juvix-stdlib - ref: 290f67fc85b637ce4df886fc3cd1a5289b38db95 + ref: 95f93e60e1033046d950414a805f7a4bc75adb62 url: https://github.com/anoma/juvix-stdlib dependencies: []