Expand ./Prelude/Optional (#77)
This adds several new list-like utilities, such as `any`/`null`/`length`
This commit is contained in:
Gabriel Gonzalez
GitHub
parent
2b8b89e41a
commit
2d7fe03ae0
19
Prelude/Optional/all
Normal file
19
Prelude/Optional/all
Normal file
|
|
@ -0,0 +1,19 @@
|
|||
{-
|
||||
Returns `False` if the supplied function returns `False` for a present element
|
||||
and `True` otherwise:
|
||||
|
||||
Examples:
|
||||
|
||||
```
|
||||
./all Natural Natural/even ([+3] : Optional Natural) = False
|
||||
|
||||
./all Natural Natural/even ([] : Optional Natural) = True
|
||||
```
|
||||
-}
|
||||
let all : ∀(a : Type) → (a → Bool) → Optional a → Bool
|
||||
= λ(a : Type)
|
||||
→ λ(f : a → Bool)
|
||||
→ λ(xs : Optional a)
|
||||
→ Optional/fold a xs Bool f True
|
||||
|
||||
in all
|
||||
19
Prelude/Optional/any
Normal file
19
Prelude/Optional/any
Normal file
|
|
@ -0,0 +1,19 @@
|
|||
{-
|
||||
Returns `True` if the supplied function returns `True` for a present element and
|
||||
`False` otherwise
|
||||
|
||||
Examples:
|
||||
|
||||
```
|
||||
./any Natural Natural/even ([+2] : Optional Natural) = True
|
||||
|
||||
./any Natural Natural/even ([] : Optional Natural) = False
|
||||
```
|
||||
-}
|
||||
let any : ∀(a : Type) → (a → Bool) → Optional a → Bool
|
||||
= λ(a : Type)
|
||||
→ λ(f : a → Bool)
|
||||
→ λ(xs : Optional a)
|
||||
→ Optional/fold a xs Bool f False
|
||||
|
||||
in any
|
||||
31
Prelude/Optional/filter
Normal file
31
Prelude/Optional/filter
Normal file
|
|
@ -0,0 +1,31 @@
|
|||
{-
|
||||
Only keep an `Optional` element if the supplied function returns `True`
|
||||
|
||||
Examples:
|
||||
|
||||
```
|
||||
./filter Natural Natural/even ([+2] : Optional Natural)
|
||||
= [+2] : Optional Natural
|
||||
|
||||
./filter Natural Natural/odd ([+2] : Optional Natural)
|
||||
= [] : Optional Natural
|
||||
```
|
||||
-}
|
||||
let filter : ∀(a : Type) → (a → Bool) → Optional a -> Optional a
|
||||
= λ(a : Type)
|
||||
→ λ(f : a → Bool)
|
||||
→ λ(xs : Optional a)
|
||||
→ Optional/build
|
||||
a
|
||||
( λ(optional : Type)
|
||||
→ λ(just : a → optional)
|
||||
→ λ(nil : optional)
|
||||
→ Optional/fold
|
||||
a
|
||||
xs
|
||||
optional
|
||||
(λ(x : a) → if f x then just x else nil)
|
||||
nil
|
||||
)
|
||||
|
||||
in filter
|
||||
17
Prelude/Optional/length
Normal file
17
Prelude/Optional/length
Normal file
|
|
@ -0,0 +1,17 @@
|
|||
{-
|
||||
Returns `+1` if the `Optional` value is present and `+0` if the value is absent
|
||||
|
||||
Examples:
|
||||
|
||||
```
|
||||
./length Integer ([2] : Optional Integer) = +1
|
||||
|
||||
./length Integer ([] : Optional Integer) = +0
|
||||
```
|
||||
-}
|
||||
let length : ∀(a : Type) → Optional a → Natural
|
||||
= λ(a : Type)
|
||||
→ λ(xs : Optional a)
|
||||
→ Optional/fold a xs Natural (λ(_ : a) → +1) +0
|
||||
|
||||
in length
|
||||
17
Prelude/Optional/null
Normal file
17
Prelude/Optional/null
Normal file
|
|
@ -0,0 +1,17 @@
|
|||
{-
|
||||
Returns `True` if the `Optional` value is absent and `False` if present
|
||||
|
||||
Examples:
|
||||
|
||||
```
|
||||
./null Integer ([2] : Optional Integer) = False
|
||||
|
||||
./null Integer ([] : Optional Integer) = True
|
||||
```
|
||||
-}
|
||||
let null : ∀(a : Type) → Optional a → Bool
|
||||
= λ(a : Type)
|
||||
→ λ(xs : Optional a)
|
||||
→ Optional/fold a xs Bool (λ(_ : a) → False) True
|
||||
|
||||
in null
|
||||
|
|
@ -195,7 +195,15 @@ exampleTests =
|
|||
]
|
||||
]
|
||||
, Test.Tasty.testGroup "Optional"
|
||||
[ Test.Tasty.testGroup "build"
|
||||
[ Test.Tasty.testGroup "all"
|
||||
[ _Optional_all_0
|
||||
, _Optional_all_1
|
||||
]
|
||||
, Test.Tasty.testGroup "any"
|
||||
[ _Optional_any_0
|
||||
, _Optional_any_1
|
||||
]
|
||||
, Test.Tasty.testGroup "build"
|
||||
[ _Optional_build_0
|
||||
, _Optional_build_1
|
||||
]
|
||||
|
|
@ -204,6 +212,10 @@ exampleTests =
|
|||
, _Optional_concat_1
|
||||
, _Optional_concat_2
|
||||
]
|
||||
, Test.Tasty.testGroup "filter"
|
||||
[ _Optional_filter_0
|
||||
, _Optional_filter_1
|
||||
]
|
||||
, Test.Tasty.testGroup "fold"
|
||||
[ _Optional_fold_0
|
||||
, _Optional_fold_1
|
||||
|
|
@ -218,6 +230,14 @@ exampleTests =
|
|||
, _Optional_last_1
|
||||
, _Optional_last_2
|
||||
]
|
||||
, Test.Tasty.testGroup "length"
|
||||
[ _Optional_length_0
|
||||
, _Optional_length_1
|
||||
]
|
||||
, Test.Tasty.testGroup "null"
|
||||
[ _Optional_null_0
|
||||
, _Optional_null_1
|
||||
]
|
||||
, Test.Tasty.testGroup "map"
|
||||
[ _Optional_map_0
|
||||
, _Optional_map_1
|
||||
|
|
@ -973,6 +993,34 @@ _Natural_toInteger_1 = Test.Tasty.HUnit.testCase "Example #1" (do
|
|||
|]
|
||||
Util.assertNormalizesTo e "0" )
|
||||
|
||||
_Optional_all_0 :: TestTree
|
||||
_Optional_all_0 = Test.Tasty.HUnit.testCase "Example #0" (do
|
||||
e <- Util.code [NeatInterpolation.text|
|
||||
./Prelude/Optional/all Natural Natural/even ([+3] : Optional Natural)
|
||||
|]
|
||||
Util.assertNormalizesTo e "False" )
|
||||
|
||||
_Optional_all_1 :: TestTree
|
||||
_Optional_all_1 = Test.Tasty.HUnit.testCase "Example #1" (do
|
||||
e <- Util.code [NeatInterpolation.text|
|
||||
./Prelude/Optional/all Natural Natural/even ([] : Optional Natural)
|
||||
|]
|
||||
Util.assertNormalizesTo e "True" )
|
||||
|
||||
_Optional_any_0 :: TestTree
|
||||
_Optional_any_0 = Test.Tasty.HUnit.testCase "Example #0" (do
|
||||
e <- Util.code [NeatInterpolation.text|
|
||||
./Prelude/Optional/any Natural Natural/even ([+2] : Optional Natural)
|
||||
|]
|
||||
Util.assertNormalizesTo e "True" )
|
||||
|
||||
_Optional_any_1 :: TestTree
|
||||
_Optional_any_1 = Test.Tasty.HUnit.testCase "Example #1" (do
|
||||
e <- Util.code [NeatInterpolation.text|
|
||||
./Prelude/Optional/any Natural Natural/even ([] : Optional Natural)
|
||||
|]
|
||||
Util.assertNormalizesTo e "False" )
|
||||
|
||||
_Optional_build_0 :: TestTree
|
||||
_Optional_build_0 = Test.Tasty.HUnit.testCase "Example #0" (do
|
||||
e <- Util.code [NeatInterpolation.text|
|
||||
|
|
@ -1020,6 +1068,20 @@ _Optional_concat_2 = Test.Tasty.HUnit.testCase "Example #2" (do
|
|||
|]
|
||||
Util.assertNormalizesTo e "[] : Optional Integer" )
|
||||
|
||||
_Optional_filter_0 :: TestTree
|
||||
_Optional_filter_0 = Test.Tasty.HUnit.testCase "Example #0" (do
|
||||
e <- Util.code [NeatInterpolation.text|
|
||||
./Prelude/Optional/filter Natural Natural/even ([+2] : Optional Natural)
|
||||
|]
|
||||
Util.assertNormalizesTo e "[+2] : Optional Natural" )
|
||||
|
||||
_Optional_filter_1 :: TestTree
|
||||
_Optional_filter_1 = Test.Tasty.HUnit.testCase "Example #1" (do
|
||||
e <- Util.code [NeatInterpolation.text|
|
||||
./Prelude/Optional/filter Natural Natural/odd ([+2] : Optional Natural)
|
||||
|]
|
||||
Util.assertNormalizesTo e "[] : Optional Natural" )
|
||||
|
||||
_Optional_fold_0 :: TestTree
|
||||
_Optional_fold_0 = Test.Tasty.HUnit.testCase "Example #0" (do
|
||||
e <- Util.code [NeatInterpolation.text|
|
||||
|
|
@ -1095,6 +1157,20 @@ _Optional_map_0 = Test.Tasty.HUnit.testCase "Example #0" (do
|
|||
|]
|
||||
Util.assertNormalizesTo e "[False] : Optional Bool" )
|
||||
|
||||
_Optional_length_0 :: TestTree
|
||||
_Optional_length_0 = Test.Tasty.HUnit.testCase "Example #0" (do
|
||||
e <- Util.code [NeatInterpolation.text|
|
||||
./Prelude/Optional/length Integer ([2] : Optional Integer)
|
||||
|]
|
||||
Util.assertNormalizesTo e "+1" )
|
||||
|
||||
_Optional_length_1 :: TestTree
|
||||
_Optional_length_1 = Test.Tasty.HUnit.testCase "Example #1" (do
|
||||
e <- Util.code [NeatInterpolation.text|
|
||||
./Prelude/Optional/length Integer ([] : Optional Integer)
|
||||
|]
|
||||
Util.assertNormalizesTo e "+0" )
|
||||
|
||||
_Optional_map_1 :: TestTree
|
||||
_Optional_map_1 = Test.Tasty.HUnit.testCase "Example #1" (do
|
||||
e <- Util.code [NeatInterpolation.text|
|
||||
|
|
@ -1102,6 +1178,20 @@ _Optional_map_1 = Test.Tasty.HUnit.testCase "Example #1" (do
|
|||
|]
|
||||
Util.assertNormalizesTo e "[] : Optional Bool" )
|
||||
|
||||
_Optional_null_0 :: TestTree
|
||||
_Optional_null_0 = Test.Tasty.HUnit.testCase "Example #0" (do
|
||||
e <- Util.code [NeatInterpolation.text|
|
||||
./Prelude/Optional/null Integer ([2] : Optional Integer)
|
||||
|]
|
||||
Util.assertNormalizesTo e "False" )
|
||||
|
||||
_Optional_null_1 :: TestTree
|
||||
_Optional_null_1 = Test.Tasty.HUnit.testCase "Example #1" (do
|
||||
e <- Util.code [NeatInterpolation.text|
|
||||
./Prelude/Optional/null Integer ([] : Optional Integer)
|
||||
|]
|
||||
Util.assertNormalizesTo e "True" )
|
||||
|
||||
_Optional_toList_0 :: TestTree
|
||||
_Optional_toList_0 = Test.Tasty.HUnit.testCase "Example #0" (do
|
||||
e <- Util.code [NeatInterpolation.text|
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user