refined 0.8.1 → 0.8.2
raw patch · 9 files changed
+2465/−2484 lines, 9 filesdep ~base
Dependency ranges changed: base
Files
- LICENSE +24/−24
- README.md +13/−13
- changelog.md +207/−207
- refined.cabal +109/−128
- src/Refined.hs +1778/−1778
- src/Refined/Unsafe.hs +132/−132
- src/Refined/Unsafe/Type.hs +81/−81
- test/Compiles.hs +58/−58
- test/QuickCheck.hs +63/−63
LICENSE view
@@ -1,24 +1,24 @@-Copyright © 2015 Nikita Volkov -Copyright © 2018 Remy Goldschmidt -Copyright © 2020 chessai - -Permission is hereby granted, free of charge, to any person -obtaining a copy of this software and associated documentation -files (the "Software"), to deal in the Software without -restriction, including without limitation the rights to use, -copy, modify, merge, publish, distribute, sublicense, and/or sell -copies of the Software, and to permit persons to whom the -Software is furnished to do so, subject to the following -conditions: - -The above copyright notice and this permission notice shall be -included in all copies or substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, -EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES -OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT -HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, -WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING -FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR -OTHER DEALINGS IN THE SOFTWARE. +Copyright © 2015 Nikita Volkov+Copyright © 2018 Remy Goldschmidt+Copyright © 2020 chessai++Permission is hereby granted, free of charge, to any person+obtaining a copy of this software and associated documentation+files (the "Software"), to deal in the Software without+restriction, including without limitation the rights to use,+copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the+Software is furnished to do so, subject to the following+conditions:++The above copyright notice and this permission notice shall be+included in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES+OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT+HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,+WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING+FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR+OTHER DEALINGS IN THE SOFTWARE.
README.md view
@@ -1,13 +1,13 @@-# refined - -[](https://travis-ci.org/nikita-volkov/refined) - -In type theory, a refinement type is a type endowed -with a predicate which is assumed to hold for any element -of the refined type. - -This library allows one to capture the idea of a refinement type -using the `Refined` type. A `Refined` `p` `x` wraps a value -of type `x`, ensuring that it satisfies a type-level predicate `p`. - -A simple introduction to this library can be found here: http://nikita-volkov.github.io/refined/ +# refined++[](https://travis-ci.org/nikita-volkov/refined)++In type theory, a refinement type is a type endowed+with a predicate which is assumed to hold for any element+of the refined type.++This library allows one to capture the idea of a refinement type+using the `Refined` type. A `Refined` `p` `x` wraps a value+of type `x`, ensuring that it satisfies a type-level predicate `p`.++A simple introduction to this library can be found here: http://nikita-volkov.github.io/refined/
changelog.md view
@@ -1,207 +1,207 @@-# Changelog -All notable changes to this project will be documented in this file. - -The format is based on [Keep a Changelog](http://keepachangelog.com/en/1.0.0/) -and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). - -## [0.8.1] - 2023-04-05 -### Added -- `Weaken` instances for `SizeGreaterThan`, `SizeLessThan`. -- `weakenAndLeft`, `weakenAndRight`, `weakenOrLeft`, `weakenOrRight` - type inference helper functions. - -### Changed -- bump `base`: "< 4.18" -> "< 4.19" -- bump `mtl`: "< 2.3" -> "< 2.4" -- bump `template-haskell`: "< 2.20" -> "< 2.21" - -## [0.8] - 2022-10-09 -### Changed -- on GHC >=9, make `refineTH` and `refineTH_` work in any monad - `(Quote m, MonadFail m)`. -- bump `base`: "< 4.17" -> "< 4.18" -- bump `template-haskell`: "< 2.19" -> "< 2.20" -- bump `aeson`: "< 2.1" -> "< 2.2" - -## [0.7] - 2022-07-01 -### Changed -- make `Refined` predicate type `p` kind polymorphic (`p :: Type` -> `p :: k`) - -## [0.6.3] - 2022-01-14 -### Added -- `Hashable` instance for `Refined` -- `FromJSONKey` instance for `Refined` -- `ToJSONKey` instance for `Refined` -- `shrink` for `Refined`'s `Arbitrary` instance. -- `refineEither` function - -### Changed -- improved efficiency of `strengthen` -- bump multiple dependency upper bounds - -## [0.6.2] - 2021-01-31 -### Changed -- `strengthen` no longer returns an `Either`, since the proof - that it should always succeed is in its constraints. -- correct `success` documentation - -## [0.6.1] - 2020-08-02 -### Changed -- upper bound on QuickCheck: <2.14 -> <2.15 - -## [0.6] - 2020-07-21 -### Changed -- `validate` now takes a `Proxy` as its first argument. -- All uses of prettyprinter are now just `Text` - -### Removed -- Refined.These module -- Dependency on `prettyprinter` - -### Fixed -- bug in `sized` internal helper that caused formatting issues - in sized predicate errors - -## [0.5.1] - 2020-07-14 -### Changed -- `refineTH_` is now implemented in terms of `refineTH` -- Fix pretty-printing of `RefineException`s during compile-time - -## [0.5] - 2020-07-11 -### Added -- sized Predicate instances for `Text` -- sized Predicate instances for strict and lazy `ByteString` -- INLINABLE pragmas on `refine_` `reifyPredicate` -- `NFData` instance for `Refined` -- RefineSomeException constructor. Enables recovering - specific validation exceptions. - Thanks to @haroldcarr for adding this. -- RefineXorException constructor. -- `Empty` and `NotEmpty` predicates. -- `NaN` and `Infinite` predicates for floating-point numbers. -- @since pragmas to EVERYTHING. - -### Changed -- lower bound on mtl to 2.2.2 due to use of liftEither. - Thanks to @k0ral for reporting this -- Generalize sized predicates -- Allow newer template-haskell (< 0.16 ==> < 0.17) -- Allow newer aeson (< 1.5 ==> < 1.6) - Thanks to @locallycompact for this change. - -### Removed -- `Refined.Internal` module - Thanks to @nikita-volkov for pushing me to do this. -- Orphan modules - Thanks to @symbiont-sam-halliday for pointing out the - silliness of these modules. -- `RefineT`. It was a needless abstraction that just made the - library harder to learn and use, providing little benefit - over `Maybe RefineException`. - Thanks to @nikita-volkov for helping me see the light. - -### Deprecated -- Refined.These module in favour of Data.These from these-skinny - -## [0.4.4] - 2019-10-18 -### Added -- `refine_` -- `refineTH_` -- test suite: unit tests for compiling. -### Changed -- Allow newer `template-haskell` and `QuickCheck`. - -## [0.4.2.3] - 2019-09-17 -### Added -- `reifyPredicate` -### Fixed -- `Arbitrary` instance for `Refined` should now always terminate. - Thanks to @symbiont-joseph-kachmar for reporting this. - -## [0.4.2.2] - 2019-07-19 -### Added -- `exceptRefine`, `strengthen`, and `strengthenM` - -## [0.4.2.1] - 2019-05-31 -### Fixed -- Documentation fix for `DivisibleBy` -### Changed -- Re-export `DivisibleBy`, `Even`, and `Odd` from module `Refined`. -- Re-export all constructors from module `Refined`. - -## [0.4.2] - 2019-05-30 -### Removed -- Re-removed dependency of `these` package. -### Added -- `Even`, `Odd`, and `DivisibleBy` predicates. -- doctests for all predicates. -### Changed -- Make all predicates unary data constructors, instead of nullary, - and export those newly added constructors. - -## [0.4.1] - 2019-04-15 -### Fixed -- Serious regression where `Not p` ~ `p`. Thanks to @k0ral who reported this. - -## [0.4] - 2019-03-18 -### Added -- 'NegativeFromTo', a Predicate that ensures a numeric value is within a range [a,b], - where a < 0 and b >= a. - Thanks to github.com/futtetennista for this change. -### Changed -- `RefinedNotException` now has a child (it should have had one in v2. This was an oversight.) -- `displayRefineException` no longer uses tabs, instead 2 spaces. -- make implementation of `displayRefineException` more clear via formatting. - -## [0.3.0.0] - 2018-09-26 -### Added -- Internal module, and Unsafe modules, making sure to take care w.r.t. - the scope of coercions related to the use of the 'Refined' constructor. -- 'IdPred' predicate, predicate that never fails. -- Generic instances for all predicates. -- `reallyUnsafeRefine`, `reallyUnsafeUnderlyingRefined`, `reallyUnsafeAllUnderlyingRefined`, - functions that allow one to use 'Coercion's to manually prove things about 'Refined' - values. -### Changed -- Type role of Refined from 'phantom Representational' to 'nominal nominal'. - With the old type role, one can use `coerce` to prove `Q x` given any `P x`. - The second parameter should also be nominal because of interactions with something - like `GreaterThan` and `Data.Ord.Down`. - Thanks to David Feuer for pointing this out. -- Change docs to point users to 'Refined.Unsafe' module instead of recommending - 'Unsafe.Coerce.unsafeCoerce'. -- 'Ascending' and 'Descending' predicates now use 'Foldable' instead of 'IsList'. -- Lowered the lower bound on 'exceptions'; it was too strict for the support window. -### Removed -- Dependency of the 'these' package. It brings in some very - heavy transitive dependencies, even though the datatype - in `refined` is used to the most minimal extent. - This is a breaking change because - this change is exposed to the end user via 'RefineAndException'. - It is exported from a module called 'Refined.These'. Users - wishing to interact with such exceptions can either just - use the datatype constituting a minimal API there, or depend - on the 'these' package. - -## [0.2.3.0] - 2018-06-01 -### Added -- back in the 'Foldable' instance for 'Refined'. It is safe. - -## [0.2.2.0] - 2018-05-31 -### Removed -- Unsafe typeclass instances that could break the 'Refined' invariant. - These should not have been added. - -## [0.2.1.0] - 2018-05-31 -### Removed -- Unsafe typeclass instances that could break the 'Refined' invariant. - These should not have been added. - -## [0.2.0.0] - 2018-05-30 -### Changed -- Radical rewrite of the library, centred around 'RefineException' - and the 'RefineT' monad transformer. - 'validate' now has the type signature - validate :: (Predicate p x, Monad m) => p -> x -> RefineT m () -### Added -- More predicates +# Changelog+All notable changes to this project will be documented in this file.++The format is based on [Keep a Changelog](http://keepachangelog.com/en/1.0.0/)+and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/).++## [0.8.1] - 2023-04-05+### Added+- `Weaken` instances for `SizeGreaterThan`, `SizeLessThan`.+- `weakenAndLeft`, `weakenAndRight`, `weakenOrLeft`, `weakenOrRight`+ type inference helper functions.++### Changed+- bump `base`: "< 4.18" -> "< 4.19"+- bump `mtl`: "< 2.3" -> "< 2.4"+- bump `template-haskell`: "< 2.20" -> "< 2.21"++## [0.8] - 2022-10-09+### Changed+- on GHC >=9, make `refineTH` and `refineTH_` work in any monad+ `(Quote m, MonadFail m)`.+- bump `base`: "< 4.17" -> "< 4.18"+- bump `template-haskell`: "< 2.19" -> "< 2.20"+- bump `aeson`: "< 2.1" -> "< 2.2"++## [0.7] - 2022-07-01+### Changed+- make `Refined` predicate type `p` kind polymorphic (`p :: Type` -> `p :: k`)++## [0.6.3] - 2022-01-14+### Added+- `Hashable` instance for `Refined`+- `FromJSONKey` instance for `Refined`+- `ToJSONKey` instance for `Refined`+- `shrink` for `Refined`'s `Arbitrary` instance.+- `refineEither` function++### Changed+- improved efficiency of `strengthen`+- bump multiple dependency upper bounds++## [0.6.2] - 2021-01-31+### Changed+- `strengthen` no longer returns an `Either`, since the proof+ that it should always succeed is in its constraints.+- correct `success` documentation++## [0.6.1] - 2020-08-02+### Changed+- upper bound on QuickCheck: <2.14 -> <2.15++## [0.6] - 2020-07-21+### Changed+- `validate` now takes a `Proxy` as its first argument.+- All uses of prettyprinter are now just `Text`++### Removed+- Refined.These module+- Dependency on `prettyprinter`++### Fixed+- bug in `sized` internal helper that caused formatting issues+ in sized predicate errors++## [0.5.1] - 2020-07-14+### Changed+- `refineTH_` is now implemented in terms of `refineTH`+- Fix pretty-printing of `RefineException`s during compile-time++## [0.5] - 2020-07-11+### Added+- sized Predicate instances for `Text`+- sized Predicate instances for strict and lazy `ByteString`+- INLINABLE pragmas on `refine_` `reifyPredicate`+- `NFData` instance for `Refined`+- RefineSomeException constructor. Enables recovering+ specific validation exceptions.+ Thanks to @haroldcarr for adding this.+- RefineXorException constructor.+- `Empty` and `NotEmpty` predicates.+- `NaN` and `Infinite` predicates for floating-point numbers.+- @since pragmas to EVERYTHING.++### Changed+- lower bound on mtl to 2.2.2 due to use of liftEither.+ Thanks to @k0ral for reporting this+- Generalize sized predicates+- Allow newer template-haskell (< 0.16 ==> < 0.17)+- Allow newer aeson (< 1.5 ==> < 1.6)+ Thanks to @locallycompact for this change.++### Removed+- `Refined.Internal` module+ Thanks to @nikita-volkov for pushing me to do this.+- Orphan modules+ Thanks to @symbiont-sam-halliday for pointing out the+ silliness of these modules.+- `RefineT`. It was a needless abstraction that just made the+ library harder to learn and use, providing little benefit+ over `Maybe RefineException`.+ Thanks to @nikita-volkov for helping me see the light.++### Deprecated+- Refined.These module in favour of Data.These from these-skinny++## [0.4.4] - 2019-10-18+### Added+- `refine_`+- `refineTH_`+- test suite: unit tests for compiling.+### Changed+- Allow newer `template-haskell` and `QuickCheck`.++## [0.4.2.3] - 2019-09-17+### Added+- `reifyPredicate`+### Fixed+- `Arbitrary` instance for `Refined` should now always terminate.+ Thanks to @symbiont-joseph-kachmar for reporting this.++## [0.4.2.2] - 2019-07-19+### Added+- `exceptRefine`, `strengthen`, and `strengthenM`++## [0.4.2.1] - 2019-05-31+### Fixed+- Documentation fix for `DivisibleBy`+### Changed+- Re-export `DivisibleBy`, `Even`, and `Odd` from module `Refined`.+- Re-export all constructors from module `Refined`.++## [0.4.2] - 2019-05-30+### Removed+- Re-removed dependency of `these` package.+### Added+- `Even`, `Odd`, and `DivisibleBy` predicates.+- doctests for all predicates.+### Changed+- Make all predicates unary data constructors, instead of nullary,+ and export those newly added constructors.++## [0.4.1] - 2019-04-15+### Fixed+- Serious regression where `Not p` ~ `p`. Thanks to @k0ral who reported this.++## [0.4] - 2019-03-18+### Added+- 'NegativeFromTo', a Predicate that ensures a numeric value is within a range [a,b],+ where a < 0 and b >= a.+ Thanks to github.com/futtetennista for this change.+### Changed+- `RefinedNotException` now has a child (it should have had one in v2. This was an oversight.)+- `displayRefineException` no longer uses tabs, instead 2 spaces.+- make implementation of `displayRefineException` more clear via formatting.++## [0.3.0.0] - 2018-09-26+### Added+- Internal module, and Unsafe modules, making sure to take care w.r.t.+ the scope of coercions related to the use of the 'Refined' constructor.+- 'IdPred' predicate, predicate that never fails.+- Generic instances for all predicates.+- `reallyUnsafeRefine`, `reallyUnsafeUnderlyingRefined`, `reallyUnsafeAllUnderlyingRefined`,+ functions that allow one to use 'Coercion's to manually prove things about 'Refined'+ values.+### Changed+- Type role of Refined from 'phantom Representational' to 'nominal nominal'.+ With the old type role, one can use `coerce` to prove `Q x` given any `P x`.+ The second parameter should also be nominal because of interactions with something+ like `GreaterThan` and `Data.Ord.Down`.+ Thanks to David Feuer for pointing this out.+- Change docs to point users to 'Refined.Unsafe' module instead of recommending+ 'Unsafe.Coerce.unsafeCoerce'.+- 'Ascending' and 'Descending' predicates now use 'Foldable' instead of 'IsList'.+- Lowered the lower bound on 'exceptions'; it was too strict for the support window.+### Removed+- Dependency of the 'these' package. It brings in some very+ heavy transitive dependencies, even though the datatype+ in `refined` is used to the most minimal extent.+ This is a breaking change because+ this change is exposed to the end user via 'RefineAndException'.+ It is exported from a module called 'Refined.These'. Users+ wishing to interact with such exceptions can either just+ use the datatype constituting a minimal API there, or depend+ on the 'these' package.++## [0.2.3.0] - 2018-06-01+### Added+- back in the 'Foldable' instance for 'Refined'. It is safe.++## [0.2.2.0] - 2018-05-31+### Removed+- Unsafe typeclass instances that could break the 'Refined' invariant.+ These should not have been added.++## [0.2.1.0] - 2018-05-31+### Removed+- Unsafe typeclass instances that could break the 'Refined' invariant.+ These should not have been added.++## [0.2.0.0] - 2018-05-30+### Changed+- Radical rewrite of the library, centred around 'RefineException'+ and the 'RefineT' monad transformer.+ 'validate' now has the type signature+ validate :: (Predicate p x, Monad m) => p -> x -> RefineT m ()+### Added+- More predicates
refined.cabal view
@@ -1,128 +1,109 @@-cabal-version: 2.0 -name: - refined -version: - 0.8.1 -synopsis: - Refinement types with static and runtime checking -description: - For an extensive introduction to the library please follow to - <http://nikita-volkov.github.io/refined this blog-post>. -category: - Data -homepage: - https://github.com/nikita-volkov/refined -bug-reports: - https://github.com/nikita-volkov/refined/issues -author: - Nikita Volkov <nikita.y.volkov@mail.ru> -maintainer: - chessai <chessai1996@gmail.com> -copyright: - Copyright © 2015, Nikita Volkov - Copyright © 2018, Remy Goldschmidt - Copyright © 2020, chessai -license: - MIT -license-file: - LICENSE -build-type: - Simple -tested-with: - GHC == 8.4.4 - , GHC == 8.6.5 - , GHC == 8.8.5 - , GHC == 8.10.7 - , GHC == 9.0.2 - , GHC == 9.2.4 - , GHC == 9.4.2 - , GHC == 9.6.1 -extra-source-files: - README.md - , changelog.md - -flag aeson - description: - You can disable the use of the `aeson` package using `-f-aeson`. - . - This may be useful for accelerating builds in sandboxes for expert users. - default: True - manual: True - -flag QuickCheck - description: - You can disable the use of the `QuickCheck` package using `-f-QuickCheck`. - . - This may be useful for accelerating builds in sandboxes for expert users. - default: True - manual: True - -source-repository head - type: - git - location: - git://github.com/nikita-volkov/refined.git - -library - hs-source-dirs: - src - exposed-modules: - Refined - Refined.Unsafe - Refined.Unsafe.Type - default-language: - Haskell2010 - build-depends: - base >= 4.11 && < 4.19 - , bytestring >= 0.10 && < 0.12 - , deepseq >= 1.4 && < 1.5 - , exceptions >= 0.8 && < 0.11 - , hashable >= 1.0 && < 1.5 - , mtl >= 2.2.2 && < 2.4 - , template-haskell >= 2.9 && < 2.21 - , text >= 1.2 && < 2.1 - , these-skinny >= 0.7.5 && < 0.8 - if flag(aeson) - build-depends: aeson >= 0.9 && < 2.2 - cpp-options: -DHAVE_AESON - if flag(QuickCheck) - build-depends: QuickCheck >= 2.1 && < 2.15 - cpp-options: -DHAVE_QUICKCHECK - ---test-suite doctest --- type: exitcode-stdio-1.0 --- hs-source-dirs: test --- main-is: Doctests.hs --- build-depends: --- base --- , refined --- , doctest >= 0.10 --- default-language: Haskell2010 - -test-suite arbitrary - type: exitcode-stdio-1.0 - hs-source-dirs: test - main-is: QuickCheck.hs - build-depends: - base - , refined - , QuickCheck - default-language: Haskell2010 - -test-suite compiles - type: exitcode-stdio-1.0 - hs-source-dirs: test - main-is: Compiles.hs - build-depends: - base - , refined - default-language: Haskell2010 - ---test-suite doesnt-compile --- type: exitcode-stdio-1.0 --- hs-source-dirs: test --- main-is: DoesntCompile.hs --- build-depends: --- base --- , refined --- default-language: Haskell2010 +cabal-version: 3.0+name:+ refined+version:+ 0.8.2+synopsis:+ Refinement types with static and runtime checking+description:+ For an extensive introduction to the library please follow to+ <http://nikita-volkov.github.io/refined this blog-post>.+category:+ Data+homepage:+ https://github.com/nikita-volkov/refined+bug-reports:+ https://github.com/nikita-volkov/refined/issues+author:+ Nikita Volkov <nikita.y.volkov@mail.ru>+maintainer:+ chessai <chessai1996@gmail.com>+copyright:+ Copyright © 2015, Nikita Volkov+ Copyright © 2018, Remy Goldschmidt+ Copyright © 2020, chessai+license:+ MIT+license-file:+ LICENSE+build-type:+ Simple+tested-with:+ GHC == 8.4.4+ , GHC == 8.6.5+ , GHC == 8.8.5+ , GHC == 8.10.7+ , GHC == 9.0.2+ , GHC == 9.2.4+ , GHC == 9.4.2+ , GHC == 9.6.1+extra-source-files:+ README.md+ , changelog.md++flag aeson+ description:+ You can disable the use of the `aeson` package using `-f-aeson`.+ .+ This may be useful for accelerating builds in sandboxes for expert users.+ default: True+ manual: True++flag QuickCheck+ description:+ You can disable the use of the `QuickCheck` package using `-f-QuickCheck`.+ .+ This may be useful for accelerating builds in sandboxes for expert users.+ default: True+ manual: True++source-repository head+ type:+ git+ location:+ git://github.com/nikita-volkov/refined.git++library+ hs-source-dirs:+ src+ exposed-modules:+ Refined+ Refined.Unsafe+ Refined.Unsafe.Type+ default-language:+ Haskell2010+ build-depends:+ , base >= 4.11 && < 5+ , bytestring >= 0.10+ , deepseq >= 1.4+ , exceptions >= 0.8+ , hashable >= 1.0+ , mtl >= 2.2.2+ , template-haskell >= 2.9+ , text >= 1.2+ , these-skinny >= 0.7.5+ if flag(aeson)+ build-depends: aeson >= 0.9+ cpp-options: -DHAVE_AESON+ if flag(QuickCheck)+ build-depends: QuickCheck >= 2.1+ cpp-options: -DHAVE_QUICKCHECK++test-suite arbitrary+ type: exitcode-stdio-1.0+ hs-source-dirs: test+ main-is: QuickCheck.hs+ build-depends:+ base+ , refined+ , QuickCheck+ default-language: Haskell2010++test-suite compiles+ type: exitcode-stdio-1.0+ hs-source-dirs: test+ main-is: Compiles.hs+ build-depends:+ base+ , refined+ default-language: Haskell2010
src/Refined.hs view
@@ -1,1778 +1,1778 @@--------------------------------------------------------------------------------- - --- Copyright © 2015 Nikita Volkov --- Copyright © 2018 Remy Goldschmidt --- Copyright © 2020 chessai --- --- Permission is hereby granted, free of charge, to any person --- obtaining a copy of this software and associated documentation --- files (the "Software"), to deal in the Software without --- restriction, including without limitation the rights to use, --- copy, modify, merge, publish, distribute, sublicense, and/or sell --- copies of the Software, and to permit persons to whom the --- Software is furnished to do so, subject to the following --- conditions: --- --- The above copyright notice and this permission notice shall be --- included in all copies or substantial portions of the Software. --- --- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, --- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES --- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND --- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT --- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, --- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING --- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR --- OTHER DEALINGS IN THE SOFTWARE. - --------------------------------------------------------------------------------- - -{-# OPTIONS_GHC -Wall #-} -{-# OPTIONS_GHC -fno-warn-orphans #-} -{-# OPTIONS_GHC -funbox-strict-fields #-} - --------------------------------------------------------------------------------- - -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE CPP #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE MagicHash #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE PackageImports #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RoleAnnotations #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TemplateHaskellQuotes #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} - --------------------------------------------------------------------------------- - --- | In type theory, a refinement type is a type endowed --- with a predicate which is assumed to hold for any element --- of the refined type. --- --- This library allows one to capture the idea of a refinement type --- using the 'Refined' type. A 'Refined' @p@ @x@ wraps a value --- of type @x@, ensuring that it satisfies a type-level predicate @p@. --- --- A simple introduction to this library can be found here: http://nikita-volkov.github.io/refined/ --- -module Refined - ( -- * 'Refined' type - Refined - - -- ** Creation - , refine - , refine_ - , refineThrow - , refineFail - , refineError - , refineEither - , refineTH - , refineTH_ - - -- ** Consumption - , unrefine - - -- * 'Predicate' - , Predicate (validate) - , reifyPredicate - - -- * Logical predicates - , Not(..) - , And(..) - , type (&&) - , Or(..) - , type (||) - , Xor(..) - - -- * Identity predicate - , IdPred(..) - - -- * Numeric predicates - , LessThan(..) - , GreaterThan(..) - , From(..) - , To(..) - , FromTo(..) - , NegativeFromTo(..) - , EqualTo(..) - , NotEqualTo(..) - , Odd(..) - , Even(..) - , DivisibleBy(..) - , NaN(..) - , Infinite(..) - , Positive - , NonPositive - , Negative - , NonNegative - , ZeroToOne - , NonZero - - -- * Foldable predicates - -- ** Size predicates - , SizeLessThan(..) - , SizeGreaterThan(..) - , SizeEqualTo(..) - , Empty - , NonEmpty - -- ** Ordering predicates - , Ascending(..) - , Descending(..) - - -- * Weakening - , Weaken (weaken) - , andLeft - , andRight - , leftOr - , rightOr - , weakenAndLeft - , weakenAndRight - , weakenOrLeft - , weakenOrRight - - -- * Strengthening - , strengthen - - -- * Error handling - - -- ** 'RefineException' - , RefineException - ( RefineNotException - , RefineAndException - , RefineOrException - , RefineXorException - , RefineOtherException - , RefineSomeException - ) - , displayRefineException - - -- ** 'validate' helpers - , throwRefineOtherException - , throwRefineSomeException - , success - ) where - --------------------------------------------------------------------------------- - -import Control.Exception (Exception (displayException)) -import Data.Coerce (coerce) -import Data.Either (isRight, rights) -import Data.Foldable (foldl') -import Data.Functor.Contravariant ((>$<)) -import Data.Proxy (Proxy(Proxy)) -import Data.Text (Text) -import qualified Data.Text as Text -import qualified Data.Text.Lazy as TextLazy -import qualified Data.Text.Lazy.Builder as TextBuilder -import qualified Data.Text.Lazy.Builder.Int as TextBuilder -import qualified Data.ByteString as BS -import qualified Data.ByteString.Lazy as BL -import Data.Typeable (TypeRep, Typeable, typeRep) - -import Control.Monad.Catch (MonadThrow, SomeException) -import qualified Control.Monad.Catch as MonadThrow -import Control.Monad.Error.Class (MonadError) -import qualified Control.Monad.Error.Class as MonadError -#if !MIN_VERSION_base(4,13,0) -import Control.Monad.Fail (MonadFail, fail) -import Prelude hiding (fail) -#endif - -import GHC.Exts (Proxy#, proxy#) -import GHC.Generics (Generic, Generic1) -import GHC.TypeLits (type (<=), KnownNat, Nat, natVal') - -import Refined.Unsafe.Type (Refined(Refined)) - -import qualified Language.Haskell.TH.Syntax as TH - -#if HAVE_AESON -import Control.Monad ((<=<)) -import Data.Aeson (FromJSON, FromJSONKey, ToJSON, ToJSONKey) -import qualified Data.Aeson as Aeson -#endif - -#if HAVE_QUICKCHECK -import Test.QuickCheck (Arbitrary, Gen) -import qualified Test.QuickCheck as QC -import Data.Typeable (showsTypeRep) -#endif - -import "these-skinny" Data.These (These(This,That,These)) - --------------------------------------------------------------------------------- - --- $setup --- --- Doctest imports --- --- >>> :set -XDataKinds --- >>> :set -XOverloadedStrings --- >>> :set -XTypeApplications --- >>> import Data.Int --- >>> import Data.Either (isLeft) --- - --------------------------------------------------------------------------------- - -infixl 0 |> -infixl 9 .> - --- | Helper function, stolen from the flow package. -(|>) :: a -> (a -> b) -> b -x |> f = apply x f -{-# INLINE (|>) #-} - --- | Helper function, stolen from the flow package. -(.>) :: (a -> b) -> (b -> c) -> a -> c -f .> g = compose f g -{-# INLINE (.>) #-} - --- | Helper function, stolen from the flow package. -apply :: a -> (a -> b) -> b -apply x f = f x - --- | Helper function, stolen from the flow package. -compose :: (a -> b) -> (b -> c) -> (a -> c) -compose f g x = g (f x) - --- | FIXME: doc -data Ordered a = Empty | Decreasing a | Increasing a - --- | FIXME: doc -inc :: Ordered a -> Bool -inc (Decreasing _) = False -inc _ = True -{-# INLINE inc #-} - --- | FIXME: doc -dec :: Ordered a -> Bool -dec (Increasing _) = False -dec _ = True -{-# INLINE dec #-} - -increasing :: (Foldable t, Ord a) => t a -> Bool -increasing = inc . foldl' go Empty where - go Empty y = Increasing y - go (Decreasing x) _ = Decreasing x - go (Increasing x) y - | x <= y = Increasing y - | otherwise = Decreasing y -{-# INLINABLE increasing #-} - -decreasing :: (Foldable t, Ord a) => t a -> Bool -decreasing = dec . foldl' go Empty where - go Empty y = Decreasing y - go (Increasing x) _ = Increasing x - go (Decreasing x) y - | x >= y = Decreasing y - | otherwise = Increasing y -{-# INLINABLE decreasing #-} - --------------------------------------------------------------------------------- - --- | This instance makes sure to check the refinement. --- --- @since 0.1.0.0 -instance (Read x, Predicate p x) => Read (Refined p x) where - readsPrec d = readParen (d > 10) $ \r1 -> do - ("Refined", r2) <- lex r1 - (raw, r3) <- readsPrec 11 r2 - case refine raw of - Right val -> [(val, r3)] - Left _ -> [] - -#if HAVE_AESON --- | @since 0.4 -instance (FromJSON a, Predicate p a) => FromJSON (Refined p a) where - parseJSON = refineFail <=< Aeson.parseJSON - -instance (FromJSONKey a, Predicate p a) => FromJSONKey (Refined p a) where - fromJSONKey = case Aeson.fromJSONKey @a of - Aeson.FromJSONKeyCoerce -> Aeson.FromJSONKeyTextParser $ refineFail . coerce - Aeson.FromJSONKeyText f -> Aeson.FromJSONKeyTextParser $ refineFail . f - Aeson.FromJSONKeyTextParser f -> Aeson.FromJSONKeyTextParser $ refineFail <=< f - Aeson.FromJSONKeyValue f -> Aeson.FromJSONKeyValue $ refineFail <=< f - - fromJSONKeyList = case Aeson.fromJSONKeyList @a of - Aeson.FromJSONKeyText f -> Aeson.FromJSONKeyTextParser $ traverse refineFail . f - Aeson.FromJSONKeyTextParser f -> Aeson.FromJSONKeyTextParser $ traverse refineFail <=< f - Aeson.FromJSONKeyValue f -> Aeson.FromJSONKeyValue $ traverse refineFail <=< f - --- | @since 0.4 -instance (ToJSON a, Predicate p a) => ToJSON (Refined p a) where - toJSON = Aeson.toJSON . unrefine - --- | @since 0.6.3 -instance (ToJSONKey a, Predicate p a) => ToJSONKey (Refined p a) where - toJSONKey = unrefine >$< Aeson.toJSONKey - toJSONKeyList = map unrefine >$< Aeson.toJSONKeyList -#endif /* HAVE_AESON */ - -#if HAVE_QUICKCHECK --- | @since 0.4 -instance forall p a. (Arbitrary a, Typeable a, Typeable p, Predicate p a) => Arbitrary (Refined p a) where - arbitrary = loop 0 QC.arbitrary - where - loop :: Int -> Gen a -> Gen (Refined p a) - loop !runs gen - | runs < 100 = do - m <- suchThatRefined gen - case m of - Just x -> do - pure x - Nothing -> do - loop (runs + 1) gen - | otherwise = error (refinedGenError (Proxy @p) (Proxy @a)) - shrink = rights . map refine . QC.shrink . unrefine - -refinedGenError :: (Typeable p, Typeable a) - => Proxy p -> Proxy a -> String -refinedGenError p a = "arbitrary :: Refined (" - ++ typeName p - ++ ") (" - ++ typeName a - ++ "): Failed to generate a value that satisfied" - ++ " the predicate after 100 tries." - -suchThatRefined :: forall p a. (Predicate p a) - => Gen a -> Gen (Maybe (Refined p a)) -suchThatRefined gen = do - m <- QC.suchThatMaybe gen (reifyPredicate @p @a) - case m of - Nothing -> pure Nothing - Just x -> pure (Just (Refined x)) - -typeName :: Typeable a => Proxy a -> String -typeName = flip showsTypeRep "" . typeRep -#endif /* HAVE_QUICKCHECK */ - --------------------------------------------------------------------------------- - --- | A smart constructor of a 'Refined' value. --- Checks the input value at runtime. --- --- @since 0.1.0.0 -refine :: forall p x. (Predicate p x) => x -> Either RefineException (Refined p x) -refine x = maybe (Right (Refined x)) Left (validate (Proxy @p) x) -{-# INLINABLE refine #-} - --- | Like 'refine', but discards the refinement. --- This _can_ be useful when you only need to validate --- that some value at runtime satisfies some predicate. --- See also 'reifyPredicate'. --- --- @since 0.4.4 -refine_ :: forall p x. (Predicate p x) => x -> Either RefineException x -refine_ = refine @p @x .> coerce -{-# INLINABLE refine_ #-} - --- | Constructs a 'Refined' value at run-time, --- calling 'Control.Monad.Catch.throwM' if the value --- does not satisfy the predicate. --- --- @since 0.2.0.0 -refineThrow :: (Predicate p x, MonadThrow m) => x -> m (Refined p x) -refineThrow = refine .> either MonadThrow.throwM pure -{-# INLINABLE refineThrow #-} - --- | Constructs a 'Refined' value at run-time, --- calling 'Control.Monad.Fail.fail' if the value --- does not satisfy the predicate. --- --- @since 0.2.0.0 -refineFail :: (Predicate p x, MonadFail m) => x -> m (Refined p x) -refineFail = refine .> either (displayException .> fail) pure -{-# INLINABLE refineFail #-} - --- | Constructs a 'Refined' value at run-time, --- calling 'Control.Monad.Error.throwError' if the value --- does not satisfy the predicate. --- --- @since 0.2.0.0 -refineError :: (Predicate p x, MonadError RefineException m) - => x -> m (Refined p x) -refineError = refine .> either MonadError.throwError pure -{-# INLINABLE refineError #-} - --- | Like 'refine', but, when the value doesn't satisfy the predicate, returns --- a 'Refined' value with the predicate negated, instead of returning --- 'RefineException'. --- --- >>> isRight (refineEither @Even @Int 42) --- True --- --- >>> isLeft (refineEither @Even @Int 43) --- True --- -refineEither :: forall p x. (Predicate p x) => x -> Either (Refined (Not p) x) (Refined p x) -refineEither x = - case validate (Proxy @p) x of - Nothing -> Right $ Refined x - Just _ -> Left $ Refined x -{-# INLINABLE refineEither #-} - --------------------------------------------------------------------------------- - --- | Constructs a 'Refined' value at compile-time using @-XTemplateHaskell@. --- --- For example: --- --- > $$(refineTH 23) :: Refined Positive Int --- > Refined 23 --- --- Here's an example of an invalid value: --- --- > $$(refineTH 0) :: Refined Positive Int --- > <interactive>:6:4: --- > Value is not greater than 0 --- > In the Template Haskell splice $$(refineTH 0) --- > In the expression: $$(refineTH 0) :: Refined Positive Int --- > In an equation for ‘it’: --- > it = $$(refineTH 0) :: Refined Positive Int --- --- The example above indicates a compile-time failure, --- which means that the checking was done at compile-time, --- thus introducing a zero-runtime overhead compared to --- a plain value construction. --- --- /Note/: It may be useful to use this function with the --- <https://hackage.haskell.org/package/th-lift-instances/ th-lift-instances package>. --- --- @since 0.1.0.0 -#if MIN_VERSION_template_haskell(2,17,0) -refineTH :: forall p x m. (Predicate p x, TH.Lift x, TH.Quote m, MonadFail m) - => x - -> TH.Code m (Refined p x) -refineTH = - let showException = refineExceptionToTree - .> showTree True - .> fail - .> TH.liftCode - in refine @p @x - .> either showException TH.liftTyped -#else -refineTH :: forall p x. (Predicate p x, TH.Lift x) - => x - -> TH.Q (TH.TExp (Refined p x)) -refineTH = - let showException = refineExceptionToTree - .> showTree True - .> fail - in refine @p @x - .> either showException TH.lift - .> fmap TH.TExp -#endif - --- | Like 'refineTH', but immediately unrefines the value. --- This is useful when some value need only be refined --- at compile-time. --- --- @since 0.4.4 -#if MIN_VERSION_template_haskell(2,17,0) -refineTH_ :: forall p x m. (Predicate p x, TH.Lift x, TH.Quote m, MonadFail m) - => x - -> TH.Code m x -refineTH_ = - refineTH @p @x - .> TH.examineCode - .> fmap unsafeUnrefineTExp - .> TH.liftCode -#else -refineTH_ :: forall p x. (Predicate p x, TH.Lift x) - => x - -> TH.Q (TH.TExp x) -refineTH_ = refineTH @p @x .> fmap unsafeUnrefineTExp -#endif - -unsafeUnrefineTExp :: TH.TExp (Refined p x) -> TH.TExp x -unsafeUnrefineTExp (TH.TExp e) = TH.TExp - (TH.VarE 'unrefine `TH.AppE` e) - --------------------------------------------------------------------------------- - --- | Extracts the refined value. --- --- @since 0.1.0.0 -unrefine :: Refined p x -> x -unrefine = coerce -{-# INLINE unrefine #-} - --------------------------------------------------------------------------------- - --- | A typeclass which defines a runtime interpretation of --- a type-level predicate @p@ for type @x@. --- --- @since 0.1.0.0 -class (Typeable p) => Predicate p x where - {-# MINIMAL validate #-} - -- | Check the value @x@ according to the predicate @p@, - -- producing an error 'RefineException' if the value - -- does not satisfy. - -- - -- /Note/: 'validate' is not intended to be used - -- directly; instead, it is intended to provide the minimal - -- means necessary for other utilities to be derived. As - -- such, the 'Maybe' here should be interpreted to mean - -- the presence or absence of a 'RefineException', and - -- nothing else. - validate :: Proxy p -> x -> Maybe RefineException - --------------------------------------------------------------------------------- - --- | Reify a 'Predicate' by turning it into a value-level predicate. --- --- @since 0.4.2.3 -reifyPredicate :: forall p a. Predicate p a => a -> Bool -reifyPredicate = refine @p @a .> isRight -{-# INLINABLE reifyPredicate #-} - --------------------------------------------------------------------------------- - --- | A predicate which is satisfied for all types. --- Arguments passed to @'validate'@ in @'validate' 'IdPred' x@ --- are not evaluated. --- --- >>> isRight (refine @IdPred @Int undefined) --- True --- --- >>> isLeft (refine @IdPred @Int undefined) --- False --- --- @since 0.3.0.0 -data IdPred - = IdPred -- ^ @since 0.4.2 - deriving - ( Generic -- ^ @since 0.3.0.0 - ) - --- | @since 0.3.0.0 -instance Predicate IdPred x where - validate _ _ = Nothing - {-# INLINE validate #-} - --------------------------------------------------------------------------------- - --- | The negation of a predicate. --- --- >>> isRight (refine @(Not NonEmpty) @[Int] []) --- True --- --- >>> isLeft (refine @(Not NonEmpty) @[Int] [1,2]) --- True --- --- @since 0.1.0.0 -data Not p - = Not -- ^ @since 0.4.2 - deriving - ( Generic -- ^ @since 0.3.0.0 - , Generic1 -- ^ @since 0.3.0.0 - ) - --- | @since 0.1.0.0 -instance (Predicate (p :: k) x, Typeable p, Typeable k) => Predicate (Not p) x where - validate p x = do - maybe (Just (RefineNotException (typeRep p))) - (const Nothing) - (validate @p undefined x) - --------------------------------------------------------------------------------- - --- | The conjunction of two predicates. --- --- >>> isLeft (refine @(And Positive Negative) @Int 3) --- True --- --- >>> isRight (refine @(And Positive Odd) @Int 203) --- True --- --- @since 0.1.0.0 -data And l r - = And -- ^ @since 0.4.2 - deriving - ( Generic -- ^ @since 0.3.0.0 - , Generic1 -- ^ @since 0.3.0.0 - ) - -infixr 3 && --- | The conjunction of two predicates. --- --- @since 0.2.0.0 -type (&&) = And - --- | @since 0.1.0.0 -instance ( Predicate (l :: k) x, Predicate (r :: k) x, Typeable l, Typeable r, Typeable k - ) => Predicate (And l r) x where - validate p x = do - let a = validate @l undefined x - let b = validate @r undefined x - let throw err = Just (RefineAndException (typeRep p) err) - case (a, b) of - (Just e, Just e1) -> throw (These e e1) - (Just e, _) -> throw (This e) - (Nothing, Just e) -> throw (That e) - (Nothing, Nothing) -> Nothing - --------------------------------------------------------------------------------- - --- | The disjunction of two predicates. --- --- >>> isRight (refine @(Or Even Odd) @Int 3) --- True --- --- >>> isRight (refine @(Or (LessThan 3) (GreaterThan 3)) @Int 2) --- True --- --- >>> isRight (refine @(Or Even Even) @Int 4) --- True --- --- @since 0.1.0.0 -data Or l r - = Or -- ^ @since 0.4.2 - deriving - ( Generic -- ^ @since 0.3.0.0 - , Generic1 -- ^ @since 0.3.0.0 - ) - -infixr 2 || --- | The disjunction of two predicates. --- --- @since 0.2.0.0 -type (||) = Or - --- | @since 0.2.0.0 -instance ( Predicate (l :: k) x, Predicate (r :: k) x, Typeable l, Typeable r, Typeable k - ) => Predicate (Or l r) x where - validate p x = do - let left = validate @l undefined x - let right = validate @r undefined x - case (left, right) of - (Just l, Just r) -> Just (RefineOrException (typeRep p) l r) - _ -> Nothing - --------------------------------------------------------------------------------- - --- | The exclusive disjunction of two predicates. --- --- --- >>> isRight (refine @(Xor Even Odd) @Int 3) --- True --- --- >>> isLeft (refine @(Xor (LessThan 3) (EqualTo 2)) @Int 2) --- True --- --- >>> isLeft (refine @(Xor Even Even) @Int 2) --- True --- --- @since 0.5 -data Xor l r - = Xor -- ^ @since 0.5 - deriving - ( Generic -- ^ @since 0.5 - , Generic1 -- ^ @since 0.5 - ) - --- not provided because it clashes with GHC.TypeLits.^ --- infixr 8 ^ --- The exclusive disjunction of two predicates. --- type (^) = Xor - --- | @since 0.5 -instance ( Predicate (l :: k) x, Predicate (r :: k) x, Typeable l, Typeable r, Typeable k - ) => Predicate (Xor l r) x where - validate p x = do - let left = validate @l undefined x - let right = validate @r undefined x - case (left, right) of - (Nothing, Nothing) -> Just (RefineXorException (typeRep p) Nothing) - (Just l, Just r) -> Just (RefineXorException (typeRep p) (Just (l, r))) - _ -> Nothing - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value has a length --- which is less than the specified type-level number. --- --- >>> isRight (refine @(SizeLessThan 4) @[Int] [1,2,3]) --- True --- --- >>> isLeft (refine @(SizeLessThan 5) @[Int] [1,2,3,4,5]) --- True --- --- >>> isRight (refine @(SizeLessThan 4) @Text "Hi") --- True --- --- >>> isLeft (refine @(SizeLessThan 4) @Text "Hello") --- True --- --- @since 0.2.0.0 -data SizeLessThan (n :: Nat) - = SizeLessThan -- ^ @since 0.4.2 - deriving - ( Generic -- ^ @since 0.3.0.0 - ) - --- | @since 0.2.0.0 -instance (Foldable t, KnownNat n) => Predicate (SizeLessThan n) (t a) where - validate p x = sized p (x, "Foldable") length ((<), "less than") --- | @since 0.5 -instance (KnownNat n) => Predicate (SizeLessThan n) Text where - validate p x = sized p (x, "Text") Text.length ((<), "less than") - --- | @since 0.5 -instance (KnownNat n) => Predicate (SizeLessThan n) BS.ByteString where - validate p x = sized p (x, "ByteString") BS.length ((<), "less than") - --- | @since 0.5 -instance (KnownNat n) => Predicate (SizeLessThan n) BL.ByteString where - validate p x = sized p (x, "ByteString") (fromIntegral . BL.length) ((<), "less than") - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value has a length --- which is greater than the specified type-level number. --- --- >>> isLeft (refine @(SizeGreaterThan 3) @[Int] [1,2,3]) --- True --- --- >>> isRight (refine @(SizeGreaterThan 3) @[Int] [1,2,3,4,5]) --- True --- --- >>> isLeft (refine @(SizeGreaterThan 4) @Text "Hi") --- True --- --- >>> isRight (refine @(SizeGreaterThan 4) @Text "Hello") --- True --- --- @since 0.2.0.0 -data SizeGreaterThan (n :: Nat) - = SizeGreaterThan -- ^ @since 0.4.2 - deriving - ( Generic -- ^ @since 0.3.0.0 - ) - --- | @since 0.2.0.0 -instance (Foldable t, KnownNat n) => Predicate (SizeGreaterThan n) (t a) where - validate p x = sized p (x, "Foldable") length ((>), "greater than") - --- | @since 0.5 -instance (KnownNat n) => Predicate (SizeGreaterThan n) Text where - validate p x = sized p (x, "Text") Text.length ((>), "greater than") - --- | @since 0.5 -instance (KnownNat n) => Predicate (SizeGreaterThan n) BS.ByteString where - validate p x = sized p (x, "ByteString") BS.length ((>), "greater than") - --- | @since 0.5 -instance (KnownNat n) => Predicate (SizeGreaterThan n) BL.ByteString where - validate p x = sized p (x, "ByteString") (fromIntegral . BL.length) ((>), "greater than") - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value has a length --- which is equal to the specified type-level number. --- --- >>> isRight (refine @(SizeEqualTo 4) @[Int] [1,2,3,4]) --- True --- --- >>> isLeft (refine @(SizeEqualTo 35) @[Int] [1,2,3,4]) --- True --- --- >>> isRight (refine @(SizeEqualTo 4) @Text "four") --- True --- --- >>> isLeft (refine @(SizeEqualTo 35) @Text "four") --- True --- --- @since 0.2.0.0 -data SizeEqualTo (n :: Nat) - = SizeEqualTo -- ^ @since 0.4.2 - deriving - ( Generic -- ^ @since 0.3.0.0 - ) - --- | @since 0.2.0.0 -instance (Foldable t, KnownNat n) => Predicate (SizeEqualTo n) (t a) where - validate p x = sized p (x, "Foldable") length ((==), "equal to") - --- | @since 0.5 -instance (KnownNat n) => Predicate (SizeEqualTo n) Text where - validate p x = sized p (x, "Text") Text.length ((==), "equal to") - --- | @since 0.5 -instance (KnownNat n) => Predicate (SizeEqualTo n) BS.ByteString where - validate p x = sized p (x, "ByteString") BS.length ((==), "equal to") - --- | @since 0.5 -instance (KnownNat n) => Predicate (SizeEqualTo n) BL.ByteString where - validate p x = sized p (x, "ByteString") (fromIntegral . BL.length) ((==), "equal to") - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the 'Foldable' contains elements --- in a strictly ascending order. --- --- >>> isRight (refine @Ascending @[Int] [5, 8, 13, 21, 34]) --- True --- --- >>> isLeft (refine @Ascending @[Int] [34, 21, 13, 8, 5]) --- True --- --- @since 0.2.0.0 -data Ascending - = Ascending -- ^ @since 0.4.2 - deriving - ( Generic -- ^ @since 0.3.0.0 - ) - --- | @since 0.2.0.0 -instance (Foldable t, Ord a) => Predicate Ascending (t a) where - validate p x = do - if increasing x - then Nothing - else throwRefineOtherException - (typeRep p) - "Foldable is not in ascending order." - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the 'Foldable' contains elements --- in a strictly descending order. --- --- >>> isRight (refine @Descending @[Int] [34, 21, 13, 8, 5]) --- True --- --- >>> isLeft (refine @Descending @[Int] [5, 8, 13, 21, 34]) --- True --- --- @since 0.2.0.0 -data Descending - = Descending -- ^ @since 0.4.2 - deriving - ( Generic -- ^ @since 0.3.0.0 - ) - --- | @since 0.2.0.0 -instance (Foldable t, Ord a) => Predicate Descending (t a) where - validate p x = do - if decreasing x - then Nothing - else throwRefineOtherException - (typeRep p) - "Foldable is not in descending order." - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is less than the --- specified type-level number. --- --- >>> isRight (refine @(LessThan 12) @Int 11) --- True --- --- >>> isLeft (refine @(LessThan 12) @Int 12) --- True --- --- @since 0.1.0.0 -data LessThan (n :: Nat) - = LessThan -- ^ @since 0.4.2 - deriving - ( Generic -- ^ @since 0.3.0.0 - ) - --- | @since 0.1.0.0 -instance (Ord x, Num x, KnownNat n) => Predicate (LessThan n) x where - validate p x = do - let n = nv @n - let x' = fromIntegral n - if x < x' - then Nothing - else throwRefineOtherException - (typeRep p) - ("Value is not less than " <> i2text n) - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is greater than the --- specified type-level number. --- --- >>> isRight (refine @(GreaterThan 65) @Int 67) --- True --- --- >>> isLeft (refine @(GreaterThan 65) @Int 65) --- True --- --- @since 0.1.0.0 -data GreaterThan (n :: Nat) - = GreaterThan -- ^ @since 0.4.2 - deriving - ( Generic -- ^ @since 0.3.0.0 - ) - --- | @since 0.1.0.0 -instance (Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x where - validate p x = do - let n = nv @n - let x' = fromIntegral n - if x > x' - then Nothing - else throwRefineOtherException - (typeRep p) - ("Value is not greater than " <> i2text n) - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is greater than or equal to the --- specified type-level number. --- --- >>> isRight (refine @(From 9) @Int 10) --- True --- --- >>> isRight (refine @(From 10) @Int 10) --- True --- --- >>> isLeft (refine @(From 11) @Int 10) --- True --- --- @since 0.1.2 -data From (n :: Nat) - = From -- ^ @since 0.4.2 - deriving - ( Generic -- ^ @since 0.3.0.0 - ) - --- | @since 0.1.2 -instance (Ord x, Num x, KnownNat n) => Predicate (From n) x where - validate p x = do - let n = nv @n - let x' = fromIntegral n - if x >= x' - then Nothing - else throwRefineOtherException - (typeRep p) - ("Value is less than " <> i2text n) - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is less than or equal to the --- specified type-level number. --- --- >>> isRight (refine @(To 23) @Int 17) --- True --- --- >>> isLeft (refine @(To 17) @Int 23) --- True --- --- @since 0.1.2 -data To (n :: Nat) - = To -- ^ @since 0.4.2 - deriving - ( Generic -- ^ @since 0.3.0.0 - ) - --- | @since 0.1.2 -instance (Ord x, Num x, KnownNat n) => Predicate (To n) x where - validate p x = do - let n = nv @n - let x' = fromIntegral n - if x <= x' - then Nothing - else throwRefineOtherException - (typeRep p) - ("Value is greater than " <> i2text n) - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is within an inclusive range. --- --- >>> isRight (refine @(FromTo 0 16) @Int 13) --- True --- --- >>> isRight (refine @(FromTo 13 15) @Int 13) --- True --- --- >>> isRight (refine @(FromTo 13 15) @Int 15) --- True --- --- >>> isLeft (refine @(FromTo 13 15) @Int 12) --- True --- --- @since 0.1.2 -data FromTo (mn :: Nat) (mx :: Nat) - = FromTo -- ^ @since 0.4.2 - deriving - ( Generic-- ^ @since 0.3.0.0 - ) - --- | @since 0.1.2 -instance ( Ord x, Num x, KnownNat mn, KnownNat mx, mn <= mx - ) => Predicate (FromTo mn mx) x where - validate p x = do - let mn' = nv @mn - let mx' = nv @mx - if x >= fromIntegral mn' && x <= fromIntegral mx' - then Nothing - else - let msg = [ "Value is out of range (minimum: " - , i2text mn' - , ", maximum: " - , i2text mx' - , ")" - ] |> mconcat - in throwRefineOtherException (typeRep p) msg - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is equal to the specified --- type-level number @n@. --- --- >>> isRight (refine @(EqualTo 5) @Int 5) --- True --- --- >>> isLeft (refine @(EqualTo 6) @Int 5) --- True --- --- @since 0.1.0.0 -data EqualTo (n :: Nat) - = EqualTo -- ^ @since 0.4.2 - deriving - ( Generic -- ^ @since 0.3.0.0 - ) - --- | @since 0.1.0.0 -instance (Eq x, Num x, KnownNat n) => Predicate (EqualTo n) x where - validate p x = do - let n = nv @n - let x' = fromIntegral n - if x == x' - then Nothing - else throwRefineOtherException - (typeRep p) - ("Value does not equal " <> i2text n) - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is not equal to the specified --- type-level number @n@. --- --- >>> isRight (refine @(NotEqualTo 6) @Int 5) --- True --- --- >>> isLeft (refine @(NotEqualTo 5) @Int 5) --- True --- --- @since 0.2.0.0 -data NotEqualTo (n :: Nat) - = NotEqualTo -- ^ @since 0.4.2 - deriving - ( Generic -- ^ @since 0.3.0.0 - ) - --- | @since 0.2.0.0 -instance (Eq x, Num x, KnownNat n) => Predicate (NotEqualTo n) x where - validate p x = do - let n = nv @n - let x' = fromIntegral n - if x /= x' - then Nothing - else throwRefineOtherException - (typeRep p) - ("Value does equal " <> i2text n) - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is greater or equal than a negative --- number specified as a type-level (positive) number @n@ and less than a --- type-level (positive) number @m@. --- --- >>> isRight (refine @(NegativeFromTo 5 12) @Int (-3)) --- True --- --- >>> isLeft (refine @(NegativeFromTo 4 3) @Int (-5)) --- True --- --- @since 0.4 -data NegativeFromTo (n :: Nat) (m :: Nat) - = NegativeFromTo -- ^ @since 0.4.2 - deriving - ( Generic -- ^ @since 0.3.0.0 - ) - --- | @since 0.4 -instance (Ord x, Num x, KnownNat n, KnownNat m) => Predicate (NegativeFromTo n m) x where - validate p x = do - let n' = nv @n - let m' = nv @m - if x >= fromIntegral (negate n') && x <= fromIntegral m' - then Nothing - else - let msg = [ "Value is out of range (minimum: " - , i2text (negate n') - , ", maximum: " - , i2text m' - , ")" - ] |> mconcat - in throwRefineOtherException (typeRep p) msg - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is divisible by @n@. --- --- >>> isRight (refine @(DivisibleBy 3) @Int 12) --- True --- --- >>> isLeft (refine @(DivisibleBy 2) @Int 37) --- True --- --- @since 0.4.2 -data DivisibleBy (n :: Nat) - = DivisibleBy -- ^ @since 0.4.2 - deriving - ( Generic -- ^ @since 0.3.0.0 - ) - --- | @since 0.4.2 -instance (Integral x, KnownNat n) => Predicate (DivisibleBy n) x where - validate p x = do - let n = nv @n - let x' = fromIntegral n - if x `mod` x' == 0 - then Nothing - else throwRefineOtherException - (typeRep p) - ("Value is not divisible by " <> i2text n) - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is odd. --- --- >>> isRight (refine @Odd @Int 33) --- True --- --- >>> isLeft (refine @Odd @Int 32) --- True --- --- @since 0.4.2 -data Odd - = Odd -- ^ @since 0.4.2 - deriving - ( Generic -- ^ @since 0.3.0.0 - ) - --- | @since 0.4.2 -instance (Integral x) => Predicate Odd x where - validate p x = do - if odd x - then Nothing - else throwRefineOtherException - (typeRep p) - "Value is not odd." - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is IEEE "not-a-number" (NaN). --- --- >>> isRight (refine @NaN @Double (0/0)) --- True --- --- >>> isLeft (refine @NaN @Double 13.9) --- True --- --- @since 0.5 -data NaN - = NaN -- ^ @since 0.5 - deriving - ( Generic -- ^ @since 0.5 - ) - --- | @since 0.5 -instance (RealFloat x) => Predicate NaN x where - validate p x = do - if isNaN x - then Nothing - else throwRefineOtherException - (typeRep p) - "Value is not IEEE \"not-a-number\" (NaN)." - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is IEEE infinity or negative infinity. --- --- >>> isRight (refine @Infinite @Double (1/0)) --- True --- --- >>> isRight (refine @Infinite @Double (-1/0)) --- True --- --- >>> isLeft (refine @Infinite @Double 13.20) --- True --- --- @since 0.5 -data Infinite - = Infinite -- ^ @since 0.5 - deriving - ( Generic -- ^ @since 0.5 - ) - --- | @since 0.5 -instance (RealFloat x) => Predicate Infinite x where - validate p x = do - if isInfinite x - then Nothing - else throwRefineOtherException - (typeRep p) - "Value is not IEEE infinity or negative infinity." - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is even. --- --- >>> isRight (refine @Even @Int 32) --- True --- --- >>> isLeft (refine @Even @Int 33) --- True --- --- @since 0.4.2 -data Even - = Even -- ^ @since 0.4.2 - deriving - ( Generic -- ^ @since 0.4.2 - ) - --- | @since 0.4.2 -instance (Integral x) => Predicate Even x where - validate p x = do - if even x - then Nothing - else throwRefineOtherException - (typeRep p) - "Value is not even." - --------------------------------------------------------------------------------- - --- | A 'Predicate' ensuring that the value is greater than zero. --- --- @since 0.1.0.0 -type Positive = GreaterThan 0 - --- | A 'Predicate' ensuring that the value is less than or equal to zero. --- --- @since 0.1.2 -type NonPositive = To 0 - --- | A 'Predicate' ensuring that the value is less than zero. --- --- @since 0.1.0.0 -type Negative = LessThan 0 - --- | A 'Predicate' ensuring that the value is greater than or equal to zero. --- --- @since 0.1.2 -type NonNegative = From 0 - --- | An inclusive range of values from zero to one. --- --- @since 0.1.0.0 -type ZeroToOne = FromTo 0 1 - --- | A 'Predicate' ensuring that the value is not equal to zero. --- --- @since 0.2.0.0 -type NonZero = NotEqualTo 0 - --- | A 'Predicate' ensuring that the type is empty. --- --- @since 0.5 -type Empty = SizeEqualTo 0 - --- | A 'Predicate' ensuring that the type is non-empty. --- --- @since 0.2.0.0 -type NonEmpty = SizeGreaterThan 0 - --------------------------------------------------------------------------------- - --- | A typeclass containing "safe" conversions between refined --- predicates where the target is /weaker/ than the source: --- that is, all values that satisfy the first predicate will --- be guaranteed to satisfy the second. --- --- Take care: writing an instance declaration for your custom --- predicates is the same as an assertion that 'weaken' is --- safe to use: --- --- @ --- instance 'Weaken' Pred1 Pred2 --- @ --- --- For most of the instances, explicit type annotations for --- the result value's type might be required. --- --- @since 0.2.0.0 -class Weaken from to where - -- | @since 0.2.0.0 - weaken :: Refined from x -> Refined to x - weaken = coerce - --- | @since 0.2.0.0 -instance (n <= m) => Weaken (LessThan n) (LessThan m) --- | @since 0.2.0.0 -instance (n <= m) => Weaken (LessThan n) (To m) --- | @since 0.2.0.0 -instance (n <= m) => Weaken (To n) (To m) --- | @since 0.2.0.0 -instance (m <= n) => Weaken (GreaterThan n) (GreaterThan m) --- | @since 0.2.0.0 -instance (m <= n) => Weaken (GreaterThan n) (From m) --- | @since 0.2.0.0 -instance (m <= n) => Weaken (From n) (From m) --- | @since 0.2.0.0 -instance (p <= n, m <= q) => Weaken (FromTo n m) (FromTo p q) --- | @since 0.2.0.0 -instance (p <= n) => Weaken (FromTo n m) (From p) --- | @since 0.2.0.0 -instance (m <= q) => Weaken (FromTo n m) (To q) --- | @since 0.8.1 -instance (n <= m) => Weaken (SizeLessThan n) (SizeLessThan m) --- | @since 0.8.1 -instance (m <= n) => Weaken (SizeGreaterThan n) (SizeGreaterThan m) - --- | This function helps type inference. --- It is equivalent to the following: --- --- @ --- instance Weaken (And l r) l --- @ --- --- @since 0.2.0.0 -andLeft :: Refined (And l r) x -> Refined l x -andLeft = coerce - --- | This function helps type inference. --- It is equivalent to the following: --- --- @ --- instance Weaken (And l r) r --- @ --- --- @since 0.2.0.0 -andRight :: Refined (And l r) x -> Refined r x -andRight = coerce - --- | This function helps type inference. --- It is equivalent to the following: --- --- @ --- instance Weaken l (Or l r) --- @ --- --- @since 0.2.0.0 -leftOr :: Refined l x -> Refined (Or l r) x -leftOr = coerce - --- | This function helps type inference. --- It is equivalent to the following: --- --- @ --- instance Weaken r (Or l r) --- @ --- --- @since 0.2.0.0 -rightOr :: Refined r x -> Refined (Or l r) x -rightOr = coerce - --- | This function helps type inference. --- It is equivalent to the following: --- --- @ --- instance Weaken from to => Weaken (And from x) (And to x) --- @ --- --- @since 0.8.1.0 -weakenAndLeft :: Weaken from to => Refined (And from x) a -> Refined (And to x) a -weakenAndLeft = coerce - --- | This function helps type inference. --- It is equivalent to the following: --- --- @ --- instance Weaken from to => Weaken (And x from) (And x to) --- @ --- --- @since 0.8.1.0 -weakenAndRight :: Weaken from to => Refined (And x from) a -> Refined (And x to) a -weakenAndRight = coerce - --- | This function helps type inference. --- It is equivalent to the following: --- --- @ --- instance Weaken from to => Weaken (Or from x) (Or to x) --- @ --- --- @since 0.8.1.0 -weakenOrLeft :: Weaken from to => Refined (And from x) a -> Refined (And to x) a -weakenOrLeft = coerce - --- | This function helps type inference. --- It is equivalent to the following: --- --- @ --- instance Weaken from to => Weaken (Or x from) (Or x to) --- @ --- --- @since 0.8.1.0 -weakenOrRight :: Weaken from to => Refined (And x from) a -> Refined (And x to) a -weakenOrRight = coerce - --- | Strengthen a refinement by composing it with another. --- --- @since 0.4.2.2 -strengthen :: forall p p' x. (Predicate p x, Predicate p' x) - => Refined p x - -> Either RefineException (Refined (p && p') x) -strengthen r = do - Refined x <- refine @p' @x (unrefine r) - pure (Refined x) -{-# inlineable strengthen #-} - --------------------------------------------------------------------------------- - --- | An exception encoding the way in which a 'Predicate' failed. --- --- @since 0.2.0.0 -data RefineException - = -- | A 'RefineException' for failures involving the 'Not' predicate. - -- - -- @since 0.2.0.0 - RefineNotException - { _RefineException_typeRep :: !TypeRep - -- ^ The 'TypeRep' of the @'Not' p@ type. - } - - | -- | A 'RefineException' for failures involving the 'And' predicate. - -- - -- @since 0.2.0.0 - RefineAndException - { _RefineException_typeRep :: !TypeRep - -- ^ The 'TypeRep' of the @'And' l r@ type. - , _RefineException_andChild :: !(These RefineException RefineException) - -- ^ A 'These' encoding which branch(es) of the 'And' failed: - -- if the 'RefineException' came from the @l@ predicate, then - -- this will be 'This', if it came from the @r@ predicate, this - -- will be 'That', and if it came from both @l@ and @r@, this - -- will be 'These'. - - -- note to self: what am I, Dr. Seuss? - } - - | -- | A 'RefineException' for failures involving the 'Or' predicate. - -- - -- @since 0.2.0.0 - RefineOrException - { _RefineException_typeRep :: !TypeRep - -- ^ The 'TypeRep' of the @'Or' l r@ type. - , _RefineException_orLChild :: !RefineException - -- ^ The 'RefineException' for the @l@ failure. - , _RefineException_orRChild :: !RefineException - -- ^ The 'RefineException' for the @l@ failure. - } - - | -- | A 'RefineException' for failures involving the 'Xor' predicate. - -- - -- @since 0.5 - RefineXorException - { _RefineException_typeRep :: !TypeRep - , _RefineException_children :: !(Maybe (RefineException, RefineException)) - } - - | -- | A 'RefineException' for failures involving all other predicates with custom exception. - -- - -- @since 0.5 - RefineSomeException - { _RefineException_typeRep :: !TypeRep - -- ^ The 'TypeRep' of the predicate that failed. - , _RefineException_Exception :: !SomeException - -- ^ A custom exception. - } - - | -- | A 'RefineException' for failures involving all other predicates. - -- - -- @since 0.2.0.0 - RefineOtherException - { _RefineException_typeRep :: !TypeRep - -- ^ The 'TypeRep' of the predicate that failed. - , _RefineException_message :: !Text - -- ^ A custom message to display. - } - deriving - ( Generic -- ^ @since 0.3.0.0 - ) - --- | /Note/: Equivalent to @'displayRefineException'@. --- --- @since 0.2.0.0 -instance Show RefineException where - show = displayRefineException - --- | A Tree which is a bit easier to pretty-print --- TODO: get rid of this -data ExceptionTree a - = NodeNone - | NodeSome !TypeRep SomeException - | NodeOther !TypeRep !Text - | NodeNot !TypeRep - | NodeOr !TypeRep [ExceptionTree a] - | NodeAnd !TypeRep [ExceptionTree a] - | NodeXor !TypeRep [ExceptionTree a] - --- | pretty-print an 'ExceptionTree', contains a hack to --- work differently whether or not you are "inGhc", i.e. --- inside of refineTH/refineTH_ (because GHC messes with --- the indentation) -showTree :: Bool -> ExceptionTree RefineException -> String -showTree inGhc - | inGhc = showOne "" "" "" - .> mapOnTail (indent 6) - .> unlines - | otherwise = showOne " " "" "" .> unlines - where - mapOnTail :: (a -> a) -> [a] -> [a] - mapOnTail f = \case - [] -> [] - (a : as) -> a : map f as - - indent :: Int -> String -> String - indent n s = replicate n ' ' ++ s - - showOne :: String -> String -> String -> ExceptionTree RefineException -> [String] - showOne leader tie arm = \case - NodeNone -> - [ - ] - NodeSome tr e -> - [ leader - <> arm - <> tie - <> "The predicate (" - <> show tr - <> ") failed with the exception: " - <> displayException e - ] - NodeOther tr p -> - [ leader - <> arm - <> tie - <> "The predicate (" - <> show tr - <> ") failed with the message: " - <> Text.unpack p - ] - NodeNot tr -> - [ leader - <> arm - <> tie - <> "The predicate (" - <> show tr - <> ") does not hold" - ] - NodeOr tr rest -> nodeRep tr : showChildren rest (leader <> extension) - NodeAnd tr rest -> nodeRep tr : showChildren rest (leader <> extension) - -- can be empty since both can be satisfied - NodeXor tr [] -> - [ leader - <> arm - <> tie - <> "The predicate (" - <> show tr - <> ") does not hold, because both predicates were satisfied" - ] - NodeXor tr rest -> nodeRep tr : showChildren rest (leader <> extension) - where - nodeRep :: TypeRep -> String - -- TODO: make tr bold - nodeRep tr = leader <> arm <> tie <> show tr - - extension :: String - extension = case arm of - "" -> "" - "└" -> " " - _ -> "│ " - - showChildren :: [ExceptionTree RefineException] -> String -> [String] - showChildren children leader = - let arms = replicate (length children - 1) "├" <> ["└"] - in concat (zipWith (showOne leader "── ") arms children) - -refineExceptionToTree :: RefineException -> ExceptionTree RefineException -refineExceptionToTree = go - where - go = \case - RefineSomeException tr e -> NodeSome tr e - RefineOtherException tr p -> NodeOther tr p - RefineNotException tr -> NodeNot tr - RefineOrException tr l r -> NodeOr tr [go l, go r] - RefineAndException tr (This l) -> NodeAnd tr [go l] - RefineAndException tr (That r) -> NodeAnd tr [go r] - RefineAndException tr (These l r) -> NodeAnd tr [go l, go r] - RefineXorException tr Nothing -> NodeXor tr [] - RefineXorException tr (Just (l, r)) -> NodeXor tr [go l, go r] - --- | Display a 'RefineException' as @'String'@ --- --- This function can be extremely useful for debugging --- @'RefineException's@, especially deeply nested ones. --- --- Consider: --- --- @ --- myRefinement = refine --- \@(And --- (Not (LessThan 5)) --- (Xor --- (DivisibleBy 10) --- (And --- (EqualTo 4) --- (EqualTo 3) --- ) --- ) --- ) --- \@Int --- 3 --- @ --- --- This function will show the following tree structure, recursively breaking down --- every issue: --- --- @ --- And (Not (LessThan 5)) (Xor (EqualTo 4) (And (EqualTo 4) (EqualTo 3))) --- ├── The predicate (Not (LessThan 5)) does not hold. --- └── Xor (DivisibleBy 10) (And (EqualTo 4) (EqualTo 3)) --- ├── The predicate (DivisibleBy 10) failed with the message: Value is not divisible by 10 --- └── And (EqualTo 4) (EqualTo 3) --- └── The predicate (EqualTo 4) failed with the message: Value does not equal 4 --- @ --- --- /Note/: Equivalent to @'show' \@'RefineException'@ --- --- @since 0.2.0.0 -displayRefineException :: RefineException -> String -displayRefineException = refineExceptionToTree .> showTree False - --- | Encode a 'RefineException' for use with \Control.Exception\. --- --- /Note/: Equivalent to @'displayRefineException'@. --- --- @since 0.2.0.0 -instance Exception RefineException where - displayException = show - --------------------------------------------------------------------------------- - --- | A handler for a @'RefineException'@. --- --- 'throwRefineOtherException' is useful for defining what --- behaviour 'validate' should have in the event of a predicate failure. --- --- Typically the first argument passed to this function --- will be the result of applying 'typeRep' to the first --- argument of 'validate'. --- --- @since 0.2.0.0 -throwRefineOtherException - :: TypeRep - -- ^ The 'TypeRep' of the 'Predicate'. This can usually be given by using 'typeRep'. - -> Text - -- ^ A 'PP.Doc' 'Void' encoding a custom error message to be pretty-printed. - -> Maybe RefineException -throwRefineOtherException rep - = RefineOtherException rep .> Just - --- | A handler for a @'RefineException'@. --- --- 'throwRefineSomeException' is useful for defining what --- behaviour 'validate' should have in the event of a predicate failure --- with a specific exception. --- --- @since 0.5 -throwRefineSomeException - :: TypeRep - -- ^ The 'TypeRep' of the 'Predicate'. This can usually be given by using 'typeRep'. - -> SomeException - -- ^ A custom exception. - -> Maybe RefineException -throwRefineSomeException rep - = RefineSomeException rep .> Just - --- | An implementation of 'validate' that always succeeds. --- --- ==== __Examples__ --- --- @ --- data ContainsLetterE = ContainsLetterE --- --- instance Predicate ContainsLetterE 'Text' where --- validate p t --- | 'Data.Text.any' (== \'e\') t = 'success' --- | otherwise = Just $ 'throwRefineException' (typeRep p) "Text doesn't contain letter \'e\'". --- @ --- --- @since 0.5 -success - :: Maybe RefineException -success - = Nothing - --------------------------------------------------------------------------------- - --- | Helper function for sized predicates. -sized :: forall p n a. (Typeable (p n), KnownNat n) - => Proxy (p n) - -- ^ predicate - -> (a, Text) - -- ^ (value, type) - -> (a -> Int) - -- ^ length of value - -> (Int -> Int -> Bool, Text) - -- ^ (compare :: Length -> KnownNat -> Bool, comparison string) - -> Maybe RefineException -sized p (x, typ) lenF (cmp, cmpDesc) = do - let x' = fromIntegral (nv @n) - let sz = lenF x - if cmp sz x' - then Nothing - else - let msg = - [ "Size of ", typ, " is not ", cmpDesc, " " - , i2text x' - , ". " - , "Size is: " - , i2text sz - ] |> mconcat - in throwRefineOtherException (typeRep p) msg - --- helper function to make sure natVal calls are --- zero runtime overhead -nv :: forall n. KnownNat n => Integer -nv = natVal' (proxy# :: Proxy# n) - --- convert an Integral number to Text --- --- todo: use toLazyTextWith, providing a tiny buffer size -i2text :: Integral a => a -> Text -i2text = TextBuilder.decimal - .> TextBuilder.toLazyText - .> TextLazy.toStrict -{-# SPECIALISE i2text :: Int -> Text #-} -{-# SPECIALISE i2text :: Integer -> Text #-} +--------------------------------------------------------------------------------++-- Copyright © 2015 Nikita Volkov+-- Copyright © 2018 Remy Goldschmidt+-- Copyright © 2020 chessai+--+-- Permission is hereby granted, free of charge, to any person+-- obtaining a copy of this software and associated documentation+-- files (the "Software"), to deal in the Software without+-- restriction, including without limitation the rights to use,+-- copy, modify, merge, publish, distribute, sublicense, and/or sell+-- copies of the Software, and to permit persons to whom the+-- Software is furnished to do so, subject to the following+-- conditions:+--+-- The above copyright notice and this permission notice shall be+-- included in all copies or substantial portions of the Software.+--+-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES+-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND+-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT+-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,+-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING+-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR+-- OTHER DEALINGS IN THE SOFTWARE.++--------------------------------------------------------------------------------++{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# OPTIONS_GHC -funbox-strict-fields #-}++--------------------------------------------------------------------------------++{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PackageImports #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskellQuotes #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++--------------------------------------------------------------------------------++-- | In type theory, a refinement type is a type endowed+-- with a predicate which is assumed to hold for any element+-- of the refined type.+--+-- This library allows one to capture the idea of a refinement type+-- using the 'Refined' type. A 'Refined' @p@ @x@ wraps a value+-- of type @x@, ensuring that it satisfies a type-level predicate @p@.+--+-- A simple introduction to this library can be found here: http://nikita-volkov.github.io/refined/+--+module Refined+ ( -- * 'Refined' type+ Refined++ -- ** Creation+ , refine+ , refine_+ , refineThrow+ , refineFail+ , refineError+ , refineEither+ , refineTH+ , refineTH_++ -- ** Consumption+ , unrefine++ -- * 'Predicate'+ , Predicate (validate)+ , reifyPredicate++ -- * Logical predicates+ , Not(..)+ , And(..)+ , type (&&)+ , Or(..)+ , type (||)+ , Xor(..)++ -- * Identity predicate+ , IdPred(..)++ -- * Numeric predicates+ , LessThan(..)+ , GreaterThan(..)+ , From(..)+ , To(..)+ , FromTo(..)+ , NegativeFromTo(..)+ , EqualTo(..)+ , NotEqualTo(..)+ , Odd(..)+ , Even(..)+ , DivisibleBy(..)+ , NaN(..)+ , Infinite(..)+ , Positive+ , NonPositive+ , Negative+ , NonNegative+ , ZeroToOne+ , NonZero++ -- * Foldable predicates+ -- ** Size predicates+ , SizeLessThan(..)+ , SizeGreaterThan(..)+ , SizeEqualTo(..)+ , Empty+ , NonEmpty+ -- ** Ordering predicates+ , Ascending(..)+ , Descending(..)++ -- * Weakening+ , Weaken (weaken)+ , andLeft+ , andRight+ , leftOr+ , rightOr+ , weakenAndLeft+ , weakenAndRight+ , weakenOrLeft+ , weakenOrRight++ -- * Strengthening+ , strengthen++ -- * Error handling++ -- ** 'RefineException'+ , RefineException+ ( RefineNotException+ , RefineAndException+ , RefineOrException+ , RefineXorException+ , RefineOtherException+ , RefineSomeException+ )+ , displayRefineException++ -- ** 'validate' helpers+ , throwRefineOtherException+ , throwRefineSomeException+ , success+ ) where++--------------------------------------------------------------------------------++import Control.Exception (Exception (displayException))+import Data.Coerce (coerce)+import Data.Either (isRight, rights)+import Data.Foldable (foldl')+import Data.Functor.Contravariant ((>$<))+import Data.Proxy (Proxy(Proxy))+import Data.Text (Text)+import qualified Data.Text as Text+import qualified Data.Text.Lazy as TextLazy+import qualified Data.Text.Lazy.Builder as TextBuilder+import qualified Data.Text.Lazy.Builder.Int as TextBuilder+import qualified Data.ByteString as BS+import qualified Data.ByteString.Lazy as BL+import Data.Typeable (TypeRep, Typeable, typeRep)++import Control.Monad.Catch (MonadThrow, SomeException)+import qualified Control.Monad.Catch as MonadThrow+import Control.Monad.Error.Class (MonadError)+import qualified Control.Monad.Error.Class as MonadError+#if !MIN_VERSION_base(4,13,0)+import Control.Monad.Fail (MonadFail, fail)+import Prelude hiding (fail)+#endif++import GHC.Exts (Proxy#, proxy#)+import GHC.Generics (Generic, Generic1)+import GHC.TypeLits (type (<=), KnownNat, Nat, natVal')++import Refined.Unsafe.Type (Refined(Refined))++import qualified Language.Haskell.TH.Syntax as TH++#if HAVE_AESON+import Control.Monad ((<=<))+import Data.Aeson (FromJSON, FromJSONKey, ToJSON, ToJSONKey)+import qualified Data.Aeson as Aeson+#endif++#if HAVE_QUICKCHECK+import Test.QuickCheck (Arbitrary, Gen)+import qualified Test.QuickCheck as QC+import Data.Typeable (showsTypeRep)+#endif++import "these-skinny" Data.These (These(This,That,These))++--------------------------------------------------------------------------------++-- $setup+--+-- Doctest imports+--+-- >>> :set -XDataKinds+-- >>> :set -XOverloadedStrings+-- >>> :set -XTypeApplications+-- >>> import Data.Int+-- >>> import Data.Either (isLeft)+--++--------------------------------------------------------------------------------++infixl 0 |>+infixl 9 .>++-- | Helper function, stolen from the flow package.+(|>) :: a -> (a -> b) -> b+x |> f = apply x f+{-# INLINE (|>) #-}++-- | Helper function, stolen from the flow package.+(.>) :: (a -> b) -> (b -> c) -> a -> c+f .> g = compose f g+{-# INLINE (.>) #-}++-- | Helper function, stolen from the flow package.+apply :: a -> (a -> b) -> b+apply x f = f x++-- | Helper function, stolen from the flow package.+compose :: (a -> b) -> (b -> c) -> (a -> c)+compose f g x = g (f x)++-- | FIXME: doc+data Ordered a = Empty | Decreasing a | Increasing a++-- | FIXME: doc+inc :: Ordered a -> Bool+inc (Decreasing _) = False+inc _ = True+{-# INLINE inc #-}++-- | FIXME: doc+dec :: Ordered a -> Bool+dec (Increasing _) = False+dec _ = True+{-# INLINE dec #-}++increasing :: (Foldable t, Ord a) => t a -> Bool+increasing = inc . foldl' go Empty where+ go Empty y = Increasing y+ go (Decreasing x) _ = Decreasing x+ go (Increasing x) y+ | x <= y = Increasing y+ | otherwise = Decreasing y+{-# INLINABLE increasing #-}++decreasing :: (Foldable t, Ord a) => t a -> Bool+decreasing = dec . foldl' go Empty where+ go Empty y = Decreasing y+ go (Increasing x) _ = Increasing x+ go (Decreasing x) y+ | x >= y = Decreasing y+ | otherwise = Increasing y+{-# INLINABLE decreasing #-}++--------------------------------------------------------------------------------++-- | This instance makes sure to check the refinement.+--+-- @since 0.1.0.0+instance (Read x, Predicate p x) => Read (Refined p x) where+ readsPrec d = readParen (d > 10) $ \r1 -> do+ ("Refined", r2) <- lex r1+ (raw, r3) <- readsPrec 11 r2+ case refine raw of+ Right val -> [(val, r3)]+ Left _ -> []++#if HAVE_AESON+-- | @since 0.4+instance (FromJSON a, Predicate p a) => FromJSON (Refined p a) where+ parseJSON = refineFail <=< Aeson.parseJSON++instance (FromJSONKey a, Predicate p a) => FromJSONKey (Refined p a) where+ fromJSONKey = case Aeson.fromJSONKey @a of+ Aeson.FromJSONKeyCoerce -> Aeson.FromJSONKeyTextParser $ refineFail . coerce+ Aeson.FromJSONKeyText f -> Aeson.FromJSONKeyTextParser $ refineFail . f+ Aeson.FromJSONKeyTextParser f -> Aeson.FromJSONKeyTextParser $ refineFail <=< f+ Aeson.FromJSONKeyValue f -> Aeson.FromJSONKeyValue $ refineFail <=< f++ fromJSONKeyList = case Aeson.fromJSONKeyList @a of+ Aeson.FromJSONKeyText f -> Aeson.FromJSONKeyTextParser $ traverse refineFail . f+ Aeson.FromJSONKeyTextParser f -> Aeson.FromJSONKeyTextParser $ traverse refineFail <=< f+ Aeson.FromJSONKeyValue f -> Aeson.FromJSONKeyValue $ traverse refineFail <=< f++-- | @since 0.4+instance (ToJSON a, Predicate p a) => ToJSON (Refined p a) where+ toJSON = Aeson.toJSON . unrefine++-- | @since 0.6.3+instance (ToJSONKey a, Predicate p a) => ToJSONKey (Refined p a) where+ toJSONKey = unrefine >$< Aeson.toJSONKey+ toJSONKeyList = map unrefine >$< Aeson.toJSONKeyList+#endif /* HAVE_AESON */++#if HAVE_QUICKCHECK+-- | @since 0.4+instance forall p a. (Arbitrary a, Typeable a, Typeable p, Predicate p a) => Arbitrary (Refined p a) where+ arbitrary = loop 0 QC.arbitrary+ where+ loop :: Int -> Gen a -> Gen (Refined p a)+ loop !runs gen+ | runs < 100 = do+ m <- suchThatRefined gen+ case m of+ Just x -> do+ pure x+ Nothing -> do+ loop (runs + 1) gen+ | otherwise = error (refinedGenError (Proxy @p) (Proxy @a))+ shrink = rights . map refine . QC.shrink . unrefine++refinedGenError :: (Typeable p, Typeable a)+ => Proxy p -> Proxy a -> String+refinedGenError p a = "arbitrary :: Refined ("+ ++ typeName p+ ++ ") ("+ ++ typeName a+ ++ "): Failed to generate a value that satisfied"+ ++ " the predicate after 100 tries."++suchThatRefined :: forall p a. (Predicate p a)+ => Gen a -> Gen (Maybe (Refined p a))+suchThatRefined gen = do+ m <- QC.suchThatMaybe gen (reifyPredicate @p @a)+ case m of+ Nothing -> pure Nothing+ Just x -> pure (Just (Refined x))++typeName :: Typeable a => Proxy a -> String+typeName = flip showsTypeRep "" . typeRep+#endif /* HAVE_QUICKCHECK */++--------------------------------------------------------------------------------++-- | A smart constructor of a 'Refined' value.+-- Checks the input value at runtime.+--+-- @since 0.1.0.0+refine :: forall p x. (Predicate p x) => x -> Either RefineException (Refined p x)+refine x = maybe (Right (Refined x)) Left (validate (Proxy @p) x)+{-# INLINABLE refine #-}++-- | Like 'refine', but discards the refinement.+-- This _can_ be useful when you only need to validate+-- that some value at runtime satisfies some predicate.+-- See also 'reifyPredicate'.+--+-- @since 0.4.4+refine_ :: forall p x. (Predicate p x) => x -> Either RefineException x+refine_ = refine @p @x .> coerce+{-# INLINABLE refine_ #-}++-- | Constructs a 'Refined' value at run-time,+-- calling 'Control.Monad.Catch.throwM' if the value+-- does not satisfy the predicate.+--+-- @since 0.2.0.0+refineThrow :: (Predicate p x, MonadThrow m) => x -> m (Refined p x)+refineThrow = refine .> either MonadThrow.throwM pure+{-# INLINABLE refineThrow #-}++-- | Constructs a 'Refined' value at run-time,+-- calling 'Control.Monad.Fail.fail' if the value+-- does not satisfy the predicate.+--+-- @since 0.2.0.0+refineFail :: (Predicate p x, MonadFail m) => x -> m (Refined p x)+refineFail = refine .> either (displayException .> fail) pure+{-# INLINABLE refineFail #-}++-- | Constructs a 'Refined' value at run-time,+-- calling 'Control.Monad.Error.throwError' if the value+-- does not satisfy the predicate.+--+-- @since 0.2.0.0+refineError :: (Predicate p x, MonadError RefineException m)+ => x -> m (Refined p x)+refineError = refine .> either MonadError.throwError pure+{-# INLINABLE refineError #-}++-- | Like 'refine', but, when the value doesn't satisfy the predicate, returns+-- a 'Refined' value with the predicate negated, instead of returning+-- 'RefineException'.+--+-- >>> isRight (refineEither @Even @Int 42)+-- True+--+-- >>> isLeft (refineEither @Even @Int 43)+-- True+--+refineEither :: forall p x. (Predicate p x) => x -> Either (Refined (Not p) x) (Refined p x)+refineEither x =+ case validate (Proxy @p) x of+ Nothing -> Right $ Refined x+ Just _ -> Left $ Refined x+{-# INLINABLE refineEither #-}++--------------------------------------------------------------------------------++-- | Constructs a 'Refined' value at compile-time using @-XTemplateHaskell@.+--+-- For example:+--+-- > $$(refineTH 23) :: Refined Positive Int+-- > Refined 23+--+-- Here's an example of an invalid value:+--+-- > $$(refineTH 0) :: Refined Positive Int+-- > <interactive>:6:4:+-- > Value is not greater than 0+-- > In the Template Haskell splice $$(refineTH 0)+-- > In the expression: $$(refineTH 0) :: Refined Positive Int+-- > In an equation for ‘it’:+-- > it = $$(refineTH 0) :: Refined Positive Int+--+-- The example above indicates a compile-time failure,+-- which means that the checking was done at compile-time,+-- thus introducing a zero-runtime overhead compared to+-- a plain value construction.+--+-- /Note/: It may be useful to use this function with the+-- <https://hackage.haskell.org/package/th-lift-instances/ th-lift-instances package>.+--+-- @since 0.1.0.0+#if MIN_VERSION_template_haskell(2,17,0)+refineTH :: forall p x m. (Predicate p x, TH.Lift x, TH.Quote m, MonadFail m)+ => x+ -> TH.Code m (Refined p x)+refineTH =+ let showException = refineExceptionToTree+ .> showTree True+ .> fail+ .> TH.liftCode+ in refine @p @x+ .> either showException TH.liftTyped+#else+refineTH :: forall p x. (Predicate p x, TH.Lift x)+ => x+ -> TH.Q (TH.TExp (Refined p x))+refineTH =+ let showException = refineExceptionToTree+ .> showTree True+ .> fail+ in refine @p @x+ .> either showException TH.lift+ .> fmap TH.TExp+#endif++-- | Like 'refineTH', but immediately unrefines the value.+-- This is useful when some value need only be refined+-- at compile-time.+--+-- @since 0.4.4+#if MIN_VERSION_template_haskell(2,17,0)+refineTH_ :: forall p x m. (Predicate p x, TH.Lift x, TH.Quote m, MonadFail m)+ => x+ -> TH.Code m x+refineTH_ =+ refineTH @p @x+ .> TH.examineCode+ .> fmap unsafeUnrefineTExp+ .> TH.liftCode+#else+refineTH_ :: forall p x. (Predicate p x, TH.Lift x)+ => x+ -> TH.Q (TH.TExp x)+refineTH_ = refineTH @p @x .> fmap unsafeUnrefineTExp+#endif++unsafeUnrefineTExp :: TH.TExp (Refined p x) -> TH.TExp x+unsafeUnrefineTExp (TH.TExp e) = TH.TExp+ (TH.VarE 'unrefine `TH.AppE` e)++--------------------------------------------------------------------------------++-- | Extracts the refined value.+--+-- @since 0.1.0.0+unrefine :: Refined p x -> x+unrefine = coerce+{-# INLINE unrefine #-}++--------------------------------------------------------------------------------++-- | A typeclass which defines a runtime interpretation of+-- a type-level predicate @p@ for type @x@.+--+-- @since 0.1.0.0+class (Typeable p) => Predicate p x where+ {-# MINIMAL validate #-}+ -- | Check the value @x@ according to the predicate @p@,+ -- producing an error 'RefineException' if the value+ -- does not satisfy.+ --+ -- /Note/: 'validate' is not intended to be used+ -- directly; instead, it is intended to provide the minimal+ -- means necessary for other utilities to be derived. As+ -- such, the 'Maybe' here should be interpreted to mean+ -- the presence or absence of a 'RefineException', and+ -- nothing else.+ validate :: Proxy p -> x -> Maybe RefineException++--------------------------------------------------------------------------------++-- | Reify a 'Predicate' by turning it into a value-level predicate.+--+-- @since 0.4.2.3+reifyPredicate :: forall p a. Predicate p a => a -> Bool+reifyPredicate = refine @p @a .> isRight+{-# INLINABLE reifyPredicate #-}++--------------------------------------------------------------------------------++-- | A predicate which is satisfied for all types.+-- Arguments passed to @'validate'@ in @'validate' 'IdPred' x@+-- are not evaluated.+--+-- >>> isRight (refine @IdPred @Int undefined)+-- True+--+-- >>> isLeft (refine @IdPred @Int undefined)+-- False+--+-- @since 0.3.0.0+data IdPred+ = IdPred -- ^ @since 0.4.2+ deriving+ ( Generic -- ^ @since 0.3.0.0+ )++-- | @since 0.3.0.0+instance Predicate IdPred x where+ validate _ _ = Nothing+ {-# INLINE validate #-}++--------------------------------------------------------------------------------++-- | The negation of a predicate.+--+-- >>> isRight (refine @(Not NonEmpty) @[Int] [])+-- True+--+-- >>> isLeft (refine @(Not NonEmpty) @[Int] [1,2])+-- True+--+-- @since 0.1.0.0+data Not p+ = Not -- ^ @since 0.4.2+ deriving+ ( Generic -- ^ @since 0.3.0.0+ , Generic1 -- ^ @since 0.3.0.0+ )++-- | @since 0.1.0.0+instance (Predicate (p :: k) x, Typeable p, Typeable k) => Predicate (Not p) x where+ validate p x = do+ maybe (Just (RefineNotException (typeRep p)))+ (const Nothing)+ (validate @p undefined x)++--------------------------------------------------------------------------------++-- | The conjunction of two predicates.+--+-- >>> isLeft (refine @(And Positive Negative) @Int 3)+-- True+--+-- >>> isRight (refine @(And Positive Odd) @Int 203)+-- True+--+-- @since 0.1.0.0+data And l r+ = And -- ^ @since 0.4.2+ deriving+ ( Generic -- ^ @since 0.3.0.0+ , Generic1 -- ^ @since 0.3.0.0+ )++infixr 3 &&+-- | The conjunction of two predicates.+--+-- @since 0.2.0.0+type (&&) = And++-- | @since 0.1.0.0+instance ( Predicate (l :: k) x, Predicate (r :: k) x, Typeable l, Typeable r, Typeable k+ ) => Predicate (And l r) x where+ validate p x = do+ let a = validate @l undefined x+ let b = validate @r undefined x+ let throw err = Just (RefineAndException (typeRep p) err)+ case (a, b) of+ (Just e, Just e1) -> throw (These e e1)+ (Just e, _) -> throw (This e)+ (Nothing, Just e) -> throw (That e)+ (Nothing, Nothing) -> Nothing++--------------------------------------------------------------------------------++-- | The disjunction of two predicates.+--+-- >>> isRight (refine @(Or Even Odd) @Int 3)+-- True+--+-- >>> isRight (refine @(Or (LessThan 3) (GreaterThan 3)) @Int 2)+-- True+--+-- >>> isRight (refine @(Or Even Even) @Int 4)+-- True+--+-- @since 0.1.0.0+data Or l r+ = Or -- ^ @since 0.4.2+ deriving+ ( Generic -- ^ @since 0.3.0.0+ , Generic1 -- ^ @since 0.3.0.0+ )++infixr 2 ||+-- | The disjunction of two predicates.+--+-- @since 0.2.0.0+type (||) = Or++-- | @since 0.2.0.0+instance ( Predicate (l :: k) x, Predicate (r :: k) x, Typeable l, Typeable r, Typeable k+ ) => Predicate (Or l r) x where+ validate p x = do+ let left = validate @l undefined x+ let right = validate @r undefined x+ case (left, right) of+ (Just l, Just r) -> Just (RefineOrException (typeRep p) l r)+ _ -> Nothing++--------------------------------------------------------------------------------++-- | The exclusive disjunction of two predicates.+--+--+-- >>> isRight (refine @(Xor Even Odd) @Int 3)+-- True+--+-- >>> isLeft (refine @(Xor (LessThan 3) (EqualTo 2)) @Int 2)+-- True+--+-- >>> isLeft (refine @(Xor Even Even) @Int 2)+-- True+--+-- @since 0.5+data Xor l r+ = Xor -- ^ @since 0.5+ deriving+ ( Generic -- ^ @since 0.5+ , Generic1 -- ^ @since 0.5+ )++-- not provided because it clashes with GHC.TypeLits.^+-- infixr 8 ^+-- The exclusive disjunction of two predicates.+-- type (^) = Xor++-- | @since 0.5+instance ( Predicate (l :: k) x, Predicate (r :: k) x, Typeable l, Typeable r, Typeable k+ ) => Predicate (Xor l r) x where+ validate p x = do+ let left = validate @l undefined x+ let right = validate @r undefined x+ case (left, right) of+ (Nothing, Nothing) -> Just (RefineXorException (typeRep p) Nothing)+ (Just l, Just r) -> Just (RefineXorException (typeRep p) (Just (l, r)))+ _ -> Nothing++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value has a length+-- which is less than the specified type-level number.+--+-- >>> isRight (refine @(SizeLessThan 4) @[Int] [1,2,3])+-- True+--+-- >>> isLeft (refine @(SizeLessThan 5) @[Int] [1,2,3,4,5])+-- True+--+-- >>> isRight (refine @(SizeLessThan 4) @Text "Hi")+-- True+--+-- >>> isLeft (refine @(SizeLessThan 4) @Text "Hello")+-- True+--+-- @since 0.2.0.0+data SizeLessThan (n :: Nat)+ = SizeLessThan -- ^ @since 0.4.2+ deriving+ ( Generic -- ^ @since 0.3.0.0+ )++-- | @since 0.2.0.0+instance (Foldable t, KnownNat n) => Predicate (SizeLessThan n) (t a) where+ validate p x = sized p (x, "Foldable") length ((<), "less than")+-- | @since 0.5+instance (KnownNat n) => Predicate (SizeLessThan n) Text where+ validate p x = sized p (x, "Text") Text.length ((<), "less than")++-- | @since 0.5+instance (KnownNat n) => Predicate (SizeLessThan n) BS.ByteString where+ validate p x = sized p (x, "ByteString") BS.length ((<), "less than")++-- | @since 0.5+instance (KnownNat n) => Predicate (SizeLessThan n) BL.ByteString where+ validate p x = sized p (x, "ByteString") (fromIntegral . BL.length) ((<), "less than")++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value has a length+-- which is greater than the specified type-level number.+--+-- >>> isLeft (refine @(SizeGreaterThan 3) @[Int] [1,2,3])+-- True+--+-- >>> isRight (refine @(SizeGreaterThan 3) @[Int] [1,2,3,4,5])+-- True+--+-- >>> isLeft (refine @(SizeGreaterThan 4) @Text "Hi")+-- True+--+-- >>> isRight (refine @(SizeGreaterThan 4) @Text "Hello")+-- True+--+-- @since 0.2.0.0+data SizeGreaterThan (n :: Nat)+ = SizeGreaterThan -- ^ @since 0.4.2+ deriving+ ( Generic -- ^ @since 0.3.0.0+ )++-- | @since 0.2.0.0+instance (Foldable t, KnownNat n) => Predicate (SizeGreaterThan n) (t a) where+ validate p x = sized p (x, "Foldable") length ((>), "greater than")++-- | @since 0.5+instance (KnownNat n) => Predicate (SizeGreaterThan n) Text where+ validate p x = sized p (x, "Text") Text.length ((>), "greater than")++-- | @since 0.5+instance (KnownNat n) => Predicate (SizeGreaterThan n) BS.ByteString where+ validate p x = sized p (x, "ByteString") BS.length ((>), "greater than")++-- | @since 0.5+instance (KnownNat n) => Predicate (SizeGreaterThan n) BL.ByteString where+ validate p x = sized p (x, "ByteString") (fromIntegral . BL.length) ((>), "greater than")++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value has a length+-- which is equal to the specified type-level number.+--+-- >>> isRight (refine @(SizeEqualTo 4) @[Int] [1,2,3,4])+-- True+--+-- >>> isLeft (refine @(SizeEqualTo 35) @[Int] [1,2,3,4])+-- True+--+-- >>> isRight (refine @(SizeEqualTo 4) @Text "four")+-- True+--+-- >>> isLeft (refine @(SizeEqualTo 35) @Text "four")+-- True+--+-- @since 0.2.0.0+data SizeEqualTo (n :: Nat)+ = SizeEqualTo -- ^ @since 0.4.2+ deriving+ ( Generic -- ^ @since 0.3.0.0+ )++-- | @since 0.2.0.0+instance (Foldable t, KnownNat n) => Predicate (SizeEqualTo n) (t a) where+ validate p x = sized p (x, "Foldable") length ((==), "equal to")++-- | @since 0.5+instance (KnownNat n) => Predicate (SizeEqualTo n) Text where+ validate p x = sized p (x, "Text") Text.length ((==), "equal to")++-- | @since 0.5+instance (KnownNat n) => Predicate (SizeEqualTo n) BS.ByteString where+ validate p x = sized p (x, "ByteString") BS.length ((==), "equal to")++-- | @since 0.5+instance (KnownNat n) => Predicate (SizeEqualTo n) BL.ByteString where+ validate p x = sized p (x, "ByteString") (fromIntegral . BL.length) ((==), "equal to")++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the 'Foldable' contains elements+-- in a strictly ascending order.+--+-- >>> isRight (refine @Ascending @[Int] [5, 8, 13, 21, 34])+-- True+--+-- >>> isLeft (refine @Ascending @[Int] [34, 21, 13, 8, 5])+-- True+--+-- @since 0.2.0.0+data Ascending+ = Ascending -- ^ @since 0.4.2+ deriving+ ( Generic -- ^ @since 0.3.0.0+ )++-- | @since 0.2.0.0+instance (Foldable t, Ord a) => Predicate Ascending (t a) where+ validate p x = do+ if increasing x+ then Nothing+ else throwRefineOtherException+ (typeRep p)+ "Foldable is not in ascending order."++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the 'Foldable' contains elements+-- in a strictly descending order.+--+-- >>> isRight (refine @Descending @[Int] [34, 21, 13, 8, 5])+-- True+--+-- >>> isLeft (refine @Descending @[Int] [5, 8, 13, 21, 34])+-- True+--+-- @since 0.2.0.0+data Descending+ = Descending -- ^ @since 0.4.2+ deriving+ ( Generic -- ^ @since 0.3.0.0+ )++-- | @since 0.2.0.0+instance (Foldable t, Ord a) => Predicate Descending (t a) where+ validate p x = do+ if decreasing x+ then Nothing+ else throwRefineOtherException+ (typeRep p)+ "Foldable is not in descending order."++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is less than the+-- specified type-level number.+--+-- >>> isRight (refine @(LessThan 12) @Int 11)+-- True+--+-- >>> isLeft (refine @(LessThan 12) @Int 12)+-- True+--+-- @since 0.1.0.0+data LessThan (n :: Nat)+ = LessThan -- ^ @since 0.4.2+ deriving+ ( Generic -- ^ @since 0.3.0.0+ )++-- | @since 0.1.0.0+instance (Ord x, Num x, KnownNat n) => Predicate (LessThan n) x where+ validate p x = do+ let n = nv @n+ let x' = fromIntegral n+ if x < x'+ then Nothing+ else throwRefineOtherException+ (typeRep p)+ ("Value is not less than " <> i2text n)++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is greater than the+-- specified type-level number.+--+-- >>> isRight (refine @(GreaterThan 65) @Int 67)+-- True+--+-- >>> isLeft (refine @(GreaterThan 65) @Int 65)+-- True+--+-- @since 0.1.0.0+data GreaterThan (n :: Nat)+ = GreaterThan -- ^ @since 0.4.2+ deriving+ ( Generic -- ^ @since 0.3.0.0+ )++-- | @since 0.1.0.0+instance (Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x where+ validate p x = do+ let n = nv @n+ let x' = fromIntegral n+ if x > x'+ then Nothing+ else throwRefineOtherException+ (typeRep p)+ ("Value is not greater than " <> i2text n)++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is greater than or equal to the+-- specified type-level number.+--+-- >>> isRight (refine @(From 9) @Int 10)+-- True+--+-- >>> isRight (refine @(From 10) @Int 10)+-- True+--+-- >>> isLeft (refine @(From 11) @Int 10)+-- True+--+-- @since 0.1.2+data From (n :: Nat)+ = From -- ^ @since 0.4.2+ deriving+ ( Generic -- ^ @since 0.3.0.0+ )++-- | @since 0.1.2+instance (Ord x, Num x, KnownNat n) => Predicate (From n) x where+ validate p x = do+ let n = nv @n+ let x' = fromIntegral n+ if x >= x'+ then Nothing+ else throwRefineOtherException+ (typeRep p)+ ("Value is less than " <> i2text n)++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is less than or equal to the+-- specified type-level number.+--+-- >>> isRight (refine @(To 23) @Int 17)+-- True+--+-- >>> isLeft (refine @(To 17) @Int 23)+-- True+--+-- @since 0.1.2+data To (n :: Nat)+ = To -- ^ @since 0.4.2+ deriving+ ( Generic -- ^ @since 0.3.0.0+ )++-- | @since 0.1.2+instance (Ord x, Num x, KnownNat n) => Predicate (To n) x where+ validate p x = do+ let n = nv @n+ let x' = fromIntegral n+ if x <= x'+ then Nothing+ else throwRefineOtherException+ (typeRep p)+ ("Value is greater than " <> i2text n)++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is within an inclusive range.+--+-- >>> isRight (refine @(FromTo 0 16) @Int 13)+-- True+--+-- >>> isRight (refine @(FromTo 13 15) @Int 13)+-- True+--+-- >>> isRight (refine @(FromTo 13 15) @Int 15)+-- True+--+-- >>> isLeft (refine @(FromTo 13 15) @Int 12)+-- True+--+-- @since 0.1.2+data FromTo (mn :: Nat) (mx :: Nat)+ = FromTo -- ^ @since 0.4.2+ deriving+ ( Generic-- ^ @since 0.3.0.0+ )++-- | @since 0.1.2+instance ( Ord x, Num x, KnownNat mn, KnownNat mx, mn <= mx+ ) => Predicate (FromTo mn mx) x where+ validate p x = do+ let mn' = nv @mn+ let mx' = nv @mx+ if x >= fromIntegral mn' && x <= fromIntegral mx'+ then Nothing+ else+ let msg = [ "Value is out of range (minimum: "+ , i2text mn'+ , ", maximum: "+ , i2text mx'+ , ")"+ ] |> mconcat+ in throwRefineOtherException (typeRep p) msg++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is equal to the specified+-- type-level number @n@.+--+-- >>> isRight (refine @(EqualTo 5) @Int 5)+-- True+--+-- >>> isLeft (refine @(EqualTo 6) @Int 5)+-- True+--+-- @since 0.1.0.0+data EqualTo (n :: Nat)+ = EqualTo -- ^ @since 0.4.2+ deriving+ ( Generic -- ^ @since 0.3.0.0+ )++-- | @since 0.1.0.0+instance (Eq x, Num x, KnownNat n) => Predicate (EqualTo n) x where+ validate p x = do+ let n = nv @n+ let x' = fromIntegral n+ if x == x'+ then Nothing+ else throwRefineOtherException+ (typeRep p)+ ("Value does not equal " <> i2text n)++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is not equal to the specified+-- type-level number @n@.+--+-- >>> isRight (refine @(NotEqualTo 6) @Int 5)+-- True+--+-- >>> isLeft (refine @(NotEqualTo 5) @Int 5)+-- True+--+-- @since 0.2.0.0+data NotEqualTo (n :: Nat)+ = NotEqualTo -- ^ @since 0.4.2+ deriving+ ( Generic -- ^ @since 0.3.0.0+ )++-- | @since 0.2.0.0+instance (Eq x, Num x, KnownNat n) => Predicate (NotEqualTo n) x where+ validate p x = do+ let n = nv @n+ let x' = fromIntegral n+ if x /= x'+ then Nothing+ else throwRefineOtherException+ (typeRep p)+ ("Value does equal " <> i2text n)++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is greater or equal than a negative+-- number specified as a type-level (positive) number @n@ and less than a+-- type-level (positive) number @m@.+--+-- >>> isRight (refine @(NegativeFromTo 5 12) @Int (-3))+-- True+--+-- >>> isLeft (refine @(NegativeFromTo 4 3) @Int (-5))+-- True+--+-- @since 0.4+data NegativeFromTo (n :: Nat) (m :: Nat)+ = NegativeFromTo -- ^ @since 0.4.2+ deriving+ ( Generic -- ^ @since 0.3.0.0+ )++-- | @since 0.4+instance (Ord x, Num x, KnownNat n, KnownNat m) => Predicate (NegativeFromTo n m) x where+ validate p x = do+ let n' = nv @n+ let m' = nv @m+ if x >= fromIntegral (negate n') && x <= fromIntegral m'+ then Nothing+ else+ let msg = [ "Value is out of range (minimum: "+ , i2text (negate n')+ , ", maximum: "+ , i2text m'+ , ")"+ ] |> mconcat+ in throwRefineOtherException (typeRep p) msg++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is divisible by @n@.+--+-- >>> isRight (refine @(DivisibleBy 3) @Int 12)+-- True+--+-- >>> isLeft (refine @(DivisibleBy 2) @Int 37)+-- True+--+-- @since 0.4.2+data DivisibleBy (n :: Nat)+ = DivisibleBy -- ^ @since 0.4.2+ deriving+ ( Generic -- ^ @since 0.3.0.0+ )++-- | @since 0.4.2+instance (Integral x, KnownNat n) => Predicate (DivisibleBy n) x where+ validate p x = do+ let n = nv @n+ let x' = fromIntegral n+ if x `mod` x' == 0+ then Nothing+ else throwRefineOtherException+ (typeRep p)+ ("Value is not divisible by " <> i2text n)++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is odd.+--+-- >>> isRight (refine @Odd @Int 33)+-- True+--+-- >>> isLeft (refine @Odd @Int 32)+-- True+--+-- @since 0.4.2+data Odd+ = Odd -- ^ @since 0.4.2+ deriving+ ( Generic -- ^ @since 0.3.0.0+ )++-- | @since 0.4.2+instance (Integral x) => Predicate Odd x where+ validate p x = do+ if odd x+ then Nothing+ else throwRefineOtherException+ (typeRep p)+ "Value is not odd."++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is IEEE "not-a-number" (NaN).+--+-- >>> isRight (refine @NaN @Double (0/0))+-- True+--+-- >>> isLeft (refine @NaN @Double 13.9)+-- True+--+-- @since 0.5+data NaN+ = NaN -- ^ @since 0.5+ deriving+ ( Generic -- ^ @since 0.5+ )++-- | @since 0.5+instance (RealFloat x) => Predicate NaN x where+ validate p x = do+ if isNaN x+ then Nothing+ else throwRefineOtherException+ (typeRep p)+ "Value is not IEEE \"not-a-number\" (NaN)."++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is IEEE infinity or negative infinity.+--+-- >>> isRight (refine @Infinite @Double (1/0))+-- True+--+-- >>> isRight (refine @Infinite @Double (-1/0))+-- True+--+-- >>> isLeft (refine @Infinite @Double 13.20)+-- True+--+-- @since 0.5+data Infinite+ = Infinite -- ^ @since 0.5+ deriving+ ( Generic -- ^ @since 0.5+ )++-- | @since 0.5+instance (RealFloat x) => Predicate Infinite x where+ validate p x = do+ if isInfinite x+ then Nothing+ else throwRefineOtherException+ (typeRep p)+ "Value is not IEEE infinity or negative infinity."++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is even.+--+-- >>> isRight (refine @Even @Int 32)+-- True+--+-- >>> isLeft (refine @Even @Int 33)+-- True+--+-- @since 0.4.2+data Even+ = Even -- ^ @since 0.4.2+ deriving+ ( Generic -- ^ @since 0.4.2+ )++-- | @since 0.4.2+instance (Integral x) => Predicate Even x where+ validate p x = do+ if even x+ then Nothing+ else throwRefineOtherException+ (typeRep p)+ "Value is not even."++--------------------------------------------------------------------------------++-- | A 'Predicate' ensuring that the value is greater than zero.+--+-- @since 0.1.0.0+type Positive = GreaterThan 0++-- | A 'Predicate' ensuring that the value is less than or equal to zero.+--+-- @since 0.1.2+type NonPositive = To 0++-- | A 'Predicate' ensuring that the value is less than zero.+--+-- @since 0.1.0.0+type Negative = LessThan 0++-- | A 'Predicate' ensuring that the value is greater than or equal to zero.+--+-- @since 0.1.2+type NonNegative = From 0++-- | An inclusive range of values from zero to one.+--+-- @since 0.1.0.0+type ZeroToOne = FromTo 0 1++-- | A 'Predicate' ensuring that the value is not equal to zero.+--+-- @since 0.2.0.0+type NonZero = NotEqualTo 0++-- | A 'Predicate' ensuring that the type is empty.+--+-- @since 0.5+type Empty = SizeEqualTo 0++-- | A 'Predicate' ensuring that the type is non-empty.+--+-- @since 0.2.0.0+type NonEmpty = SizeGreaterThan 0++--------------------------------------------------------------------------------++-- | A typeclass containing "safe" conversions between refined+-- predicates where the target is /weaker/ than the source:+-- that is, all values that satisfy the first predicate will+-- be guaranteed to satisfy the second.+--+-- Take care: writing an instance declaration for your custom+-- predicates is the same as an assertion that 'weaken' is+-- safe to use:+--+-- @+-- instance 'Weaken' Pred1 Pred2+-- @+--+-- For most of the instances, explicit type annotations for+-- the result value's type might be required.+--+-- @since 0.2.0.0+class Weaken from to where+ -- | @since 0.2.0.0+ weaken :: Refined from x -> Refined to x+ weaken = coerce++-- | @since 0.2.0.0+instance (n <= m) => Weaken (LessThan n) (LessThan m)+-- | @since 0.2.0.0+instance (n <= m) => Weaken (LessThan n) (To m)+-- | @since 0.2.0.0+instance (n <= m) => Weaken (To n) (To m)+-- | @since 0.2.0.0+instance (m <= n) => Weaken (GreaterThan n) (GreaterThan m)+-- | @since 0.2.0.0+instance (m <= n) => Weaken (GreaterThan n) (From m)+-- | @since 0.2.0.0+instance (m <= n) => Weaken (From n) (From m)+-- | @since 0.2.0.0+instance (p <= n, m <= q) => Weaken (FromTo n m) (FromTo p q)+-- | @since 0.2.0.0+instance (p <= n) => Weaken (FromTo n m) (From p)+-- | @since 0.2.0.0+instance (m <= q) => Weaken (FromTo n m) (To q)+-- | @since 0.8.1+instance (n <= m) => Weaken (SizeLessThan n) (SizeLessThan m)+-- | @since 0.8.1+instance (m <= n) => Weaken (SizeGreaterThan n) (SizeGreaterThan m)++-- | This function helps type inference.+-- It is equivalent to the following:+--+-- @+-- instance Weaken (And l r) l+-- @+--+-- @since 0.2.0.0+andLeft :: Refined (And l r) x -> Refined l x+andLeft = coerce++-- | This function helps type inference.+-- It is equivalent to the following:+--+-- @+-- instance Weaken (And l r) r+-- @+--+-- @since 0.2.0.0+andRight :: Refined (And l r) x -> Refined r x+andRight = coerce++-- | This function helps type inference.+-- It is equivalent to the following:+--+-- @+-- instance Weaken l (Or l r)+-- @+--+-- @since 0.2.0.0+leftOr :: Refined l x -> Refined (Or l r) x+leftOr = coerce++-- | This function helps type inference.+-- It is equivalent to the following:+--+-- @+-- instance Weaken r (Or l r)+-- @+--+-- @since 0.2.0.0+rightOr :: Refined r x -> Refined (Or l r) x+rightOr = coerce++-- | This function helps type inference.+-- It is equivalent to the following:+--+-- @+-- instance Weaken from to => Weaken (And from x) (And to x)+-- @+--+-- @since 0.8.1.0+weakenAndLeft :: Weaken from to => Refined (And from x) a -> Refined (And to x) a+weakenAndLeft = coerce++-- | This function helps type inference.+-- It is equivalent to the following:+--+-- @+-- instance Weaken from to => Weaken (And x from) (And x to)+-- @+--+-- @since 0.8.1.0+weakenAndRight :: Weaken from to => Refined (And x from) a -> Refined (And x to) a+weakenAndRight = coerce++-- | This function helps type inference.+-- It is equivalent to the following:+--+-- @+-- instance Weaken from to => Weaken (Or from x) (Or to x)+-- @+--+-- @since 0.8.1.0+weakenOrLeft :: Weaken from to => Refined (And from x) a -> Refined (And to x) a+weakenOrLeft = coerce++-- | This function helps type inference.+-- It is equivalent to the following:+--+-- @+-- instance Weaken from to => Weaken (Or x from) (Or x to)+-- @+--+-- @since 0.8.1.0+weakenOrRight :: Weaken from to => Refined (And x from) a -> Refined (And x to) a+weakenOrRight = coerce++-- | Strengthen a refinement by composing it with another.+--+-- @since 0.4.2.2+strengthen :: forall p p' x. (Predicate p x, Predicate p' x)+ => Refined p x+ -> Either RefineException (Refined (p && p') x)+strengthen r = do+ Refined x <- refine @p' @x (unrefine r)+ pure (Refined x)+{-# inlineable strengthen #-}++--------------------------------------------------------------------------------++-- | An exception encoding the way in which a 'Predicate' failed.+--+-- @since 0.2.0.0+data RefineException+ = -- | A 'RefineException' for failures involving the 'Not' predicate.+ --+ -- @since 0.2.0.0+ RefineNotException+ { _RefineException_typeRep :: !TypeRep+ -- ^ The 'TypeRep' of the @'Not' p@ type.+ }++ | -- | A 'RefineException' for failures involving the 'And' predicate.+ --+ -- @since 0.2.0.0+ RefineAndException+ { _RefineException_typeRep :: !TypeRep+ -- ^ The 'TypeRep' of the @'And' l r@ type.+ , _RefineException_andChild :: !(These RefineException RefineException)+ -- ^ A 'These' encoding which branch(es) of the 'And' failed:+ -- if the 'RefineException' came from the @l@ predicate, then+ -- this will be 'This', if it came from the @r@ predicate, this+ -- will be 'That', and if it came from both @l@ and @r@, this+ -- will be 'These'.++ -- note to self: what am I, Dr. Seuss?+ }++ | -- | A 'RefineException' for failures involving the 'Or' predicate.+ --+ -- @since 0.2.0.0+ RefineOrException+ { _RefineException_typeRep :: !TypeRep+ -- ^ The 'TypeRep' of the @'Or' l r@ type.+ , _RefineException_orLChild :: !RefineException+ -- ^ The 'RefineException' for the @l@ failure.+ , _RefineException_orRChild :: !RefineException+ -- ^ The 'RefineException' for the @l@ failure.+ }++ | -- | A 'RefineException' for failures involving the 'Xor' predicate.+ --+ -- @since 0.5+ RefineXorException+ { _RefineException_typeRep :: !TypeRep+ , _RefineException_children :: !(Maybe (RefineException, RefineException))+ }++ | -- | A 'RefineException' for failures involving all other predicates with custom exception.+ --+ -- @since 0.5+ RefineSomeException+ { _RefineException_typeRep :: !TypeRep+ -- ^ The 'TypeRep' of the predicate that failed.+ , _RefineException_Exception :: !SomeException+ -- ^ A custom exception.+ }++ | -- | A 'RefineException' for failures involving all other predicates.+ --+ -- @since 0.2.0.0+ RefineOtherException+ { _RefineException_typeRep :: !TypeRep+ -- ^ The 'TypeRep' of the predicate that failed.+ , _RefineException_message :: !Text+ -- ^ A custom message to display.+ }+ deriving+ ( Generic -- ^ @since 0.3.0.0+ )++-- | /Note/: Equivalent to @'displayRefineException'@.+--+-- @since 0.2.0.0+instance Show RefineException where+ show = displayRefineException++-- | A Tree which is a bit easier to pretty-print+-- TODO: get rid of this+data ExceptionTree a+ = NodeNone+ | NodeSome !TypeRep SomeException+ | NodeOther !TypeRep !Text+ | NodeNot !TypeRep+ | NodeOr !TypeRep [ExceptionTree a]+ | NodeAnd !TypeRep [ExceptionTree a]+ | NodeXor !TypeRep [ExceptionTree a]++-- | pretty-print an 'ExceptionTree', contains a hack to+-- work differently whether or not you are "inGhc", i.e.+-- inside of refineTH/refineTH_ (because GHC messes with+-- the indentation)+showTree :: Bool -> ExceptionTree RefineException -> String+showTree inGhc+ | inGhc = showOne "" "" ""+ .> mapOnTail (indent 6)+ .> unlines+ | otherwise = showOne " " "" "" .> unlines+ where+ mapOnTail :: (a -> a) -> [a] -> [a]+ mapOnTail f = \case+ [] -> []+ (a : as) -> a : map f as++ indent :: Int -> String -> String+ indent n s = replicate n ' ' ++ s++ showOne :: String -> String -> String -> ExceptionTree RefineException -> [String]+ showOne leader tie arm = \case+ NodeNone ->+ [+ ]+ NodeSome tr e ->+ [ leader+ <> arm+ <> tie+ <> "The predicate ("+ <> show tr+ <> ") failed with the exception: "+ <> displayException e+ ]+ NodeOther tr p ->+ [ leader+ <> arm+ <> tie+ <> "The predicate ("+ <> show tr+ <> ") failed with the message: "+ <> Text.unpack p+ ]+ NodeNot tr ->+ [ leader+ <> arm+ <> tie+ <> "The predicate ("+ <> show tr+ <> ") does not hold"+ ]+ NodeOr tr rest -> nodeRep tr : showChildren rest (leader <> extension)+ NodeAnd tr rest -> nodeRep tr : showChildren rest (leader <> extension)+ -- can be empty since both can be satisfied+ NodeXor tr [] ->+ [ leader+ <> arm+ <> tie+ <> "The predicate ("+ <> show tr+ <> ") does not hold, because both predicates were satisfied"+ ]+ NodeXor tr rest -> nodeRep tr : showChildren rest (leader <> extension)+ where+ nodeRep :: TypeRep -> String+ -- TODO: make tr bold+ nodeRep tr = leader <> arm <> tie <> show tr++ extension :: String+ extension = case arm of+ "" -> ""+ "└" -> " "+ _ -> "│ "++ showChildren :: [ExceptionTree RefineException] -> String -> [String]+ showChildren children leader =+ let arms = replicate (length children - 1) "├" <> ["└"]+ in concat (zipWith (showOne leader "── ") arms children)++refineExceptionToTree :: RefineException -> ExceptionTree RefineException+refineExceptionToTree = go+ where+ go = \case+ RefineSomeException tr e -> NodeSome tr e+ RefineOtherException tr p -> NodeOther tr p+ RefineNotException tr -> NodeNot tr+ RefineOrException tr l r -> NodeOr tr [go l, go r]+ RefineAndException tr (This l) -> NodeAnd tr [go l]+ RefineAndException tr (That r) -> NodeAnd tr [go r]+ RefineAndException tr (These l r) -> NodeAnd tr [go l, go r]+ RefineXorException tr Nothing -> NodeXor tr []+ RefineXorException tr (Just (l, r)) -> NodeXor tr [go l, go r]++-- | Display a 'RefineException' as @'String'@+--+-- This function can be extremely useful for debugging+-- @'RefineException's@, especially deeply nested ones.+--+-- Consider:+--+-- @+-- myRefinement = refine+-- \@(And+-- (Not (LessThan 5))+-- (Xor+-- (DivisibleBy 10)+-- (And+-- (EqualTo 4)+-- (EqualTo 3)+-- )+-- )+-- )+-- \@Int+-- 3+-- @+--+-- This function will show the following tree structure, recursively breaking down+-- every issue:+--+-- @+-- And (Not (LessThan 5)) (Xor (EqualTo 4) (And (EqualTo 4) (EqualTo 3)))+-- ├── The predicate (Not (LessThan 5)) does not hold.+-- └── Xor (DivisibleBy 10) (And (EqualTo 4) (EqualTo 3))+-- ├── The predicate (DivisibleBy 10) failed with the message: Value is not divisible by 10+-- └── And (EqualTo 4) (EqualTo 3)+-- └── The predicate (EqualTo 4) failed with the message: Value does not equal 4+-- @+--+-- /Note/: Equivalent to @'show' \@'RefineException'@+--+-- @since 0.2.0.0+displayRefineException :: RefineException -> String+displayRefineException = refineExceptionToTree .> showTree False++-- | Encode a 'RefineException' for use with \Control.Exception\.+--+-- /Note/: Equivalent to @'displayRefineException'@.+--+-- @since 0.2.0.0+instance Exception RefineException where+ displayException = show++--------------------------------------------------------------------------------++-- | A handler for a @'RefineException'@.+--+-- 'throwRefineOtherException' is useful for defining what+-- behaviour 'validate' should have in the event of a predicate failure.+--+-- Typically the first argument passed to this function+-- will be the result of applying 'typeRep' to the first+-- argument of 'validate'.+--+-- @since 0.2.0.0+throwRefineOtherException+ :: TypeRep+ -- ^ The 'TypeRep' of the 'Predicate'. This can usually be given by using 'typeRep'.+ -> Text+ -- ^ A 'PP.Doc' 'Void' encoding a custom error message to be pretty-printed.+ -> Maybe RefineException+throwRefineOtherException rep+ = RefineOtherException rep .> Just++-- | A handler for a @'RefineException'@.+--+-- 'throwRefineSomeException' is useful for defining what+-- behaviour 'validate' should have in the event of a predicate failure+-- with a specific exception.+--+-- @since 0.5+throwRefineSomeException+ :: TypeRep+ -- ^ The 'TypeRep' of the 'Predicate'. This can usually be given by using 'typeRep'.+ -> SomeException+ -- ^ A custom exception.+ -> Maybe RefineException+throwRefineSomeException rep+ = RefineSomeException rep .> Just++-- | An implementation of 'validate' that always succeeds.+--+-- ==== __Examples__+--+-- @+-- data ContainsLetterE = ContainsLetterE+--+-- instance Predicate ContainsLetterE 'Text' where+-- validate p t+-- | 'Data.Text.any' (== \'e\') t = 'success'+-- | otherwise = Just $ 'throwRefineException' (typeRep p) "Text doesn't contain letter \'e\'".+-- @+--+-- @since 0.5+success+ :: Maybe RefineException+success+ = Nothing++--------------------------------------------------------------------------------++-- | Helper function for sized predicates.+sized :: forall p n a. (Typeable (p n), KnownNat n)+ => Proxy (p n)+ -- ^ predicate+ -> (a, Text)+ -- ^ (value, type)+ -> (a -> Int)+ -- ^ length of value+ -> (Int -> Int -> Bool, Text)+ -- ^ (compare :: Length -> KnownNat -> Bool, comparison string)+ -> Maybe RefineException+sized p (x, typ) lenF (cmp, cmpDesc) = do+ let x' = fromIntegral (nv @n)+ let sz = lenF x+ if cmp sz x'+ then Nothing+ else+ let msg =+ [ "Size of ", typ, " is not ", cmpDesc, " "+ , i2text x'+ , ". "+ , "Size is: "+ , i2text sz+ ] |> mconcat+ in throwRefineOtherException (typeRep p) msg++-- helper function to make sure natVal calls are+-- zero runtime overhead+nv :: forall n. KnownNat n => Integer+nv = natVal' (proxy# :: Proxy# n)++-- convert an Integral number to Text+--+-- todo: use toLazyTextWith, providing a tiny buffer size+i2text :: Integral a => a -> Text+i2text = TextBuilder.decimal+ .> TextBuilder.toLazyText+ .> TextLazy.toStrict+{-# SPECIALISE i2text :: Int -> Text #-}+{-# SPECIALISE i2text :: Integer -> Text #-}
src/Refined/Unsafe.hs view
@@ -1,132 +1,132 @@--------------------------------------------------------------------------------- - --- Copyright © 2015 Nikita Volkov --- Copyright © 2018 Remy Goldschmidt --- Copyright © 2020 chessai --- --- Permission is hereby granted, free of charge, to any person --- obtaining a copy of this software and associated documentation --- files (the "Software"), to deal in the Software without --- restriction, including without limitation the rights to use, --- copy, modify, merge, publish, distribute, sublicense, and/or sell --- copies of the Software, and to permit persons to whom the --- Software is furnished to do so, subject to the following --- conditions: --- --- The above copyright notice and this permission notice shall be --- included in all copies or substantial portions of the Software. --- --- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, --- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES --- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND --- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT --- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, --- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING --- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR --- OTHER DEALINGS IN THE SOFTWARE. - --------------------------------------------------------------------------------- - -{-# LANGUAGE CPP #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE PolyKinds #-} -#if __GLASGOW_HASKELL__ >= 805 -{-# LANGUAGE QuantifiedConstraints #-} -{-# LANGUAGE RankNTypes #-} -#endif -{-# OPTIONS_GHC -Wall #-} - --------------------------------------------------------------------------------- - --- | This module exposes /unsafe/ refinements. An /unsafe/ refinement --- is one which either does not make the guarantee of totality in construction --- of the 'Refined' value or does not perform a check of the refinement --- predicate. It is recommended only to use this when you can manually prove --- that the refinement predicate holds. -module Refined.Unsafe - ( -- * 'Refined' - Refined - - -- ** Creation - , reallyUnsafeRefine - , unsafeRefine - - -- ** Coercion - , reallyUnsafeUnderlyingRefined -#if __GLASGOW_HASKELL__ >= 805 - , reallyUnsafeAllUnderlyingRefined -#endif - , reallyUnsafePredEquiv - ) where - --------------------------------------------------------------------------------- - -import Control.Exception (displayException) -import Data.Coerce (coerce) - -import Refined (Predicate, refine) -import Refined.Unsafe.Type (Refined(Refined)) -import Data.Type.Coercion (Coercion (..)) -#if __GLASGOW_HASKELL__ >= 805 -import Data.Coerce (Coercible) -#endif - --------------------------------------------------------------------------------- - --- | Constructs a 'Refined' value at run-time, --- calling 'Prelude.error' if the value --- does not satisfy the predicate. --- --- WARNING: this function is not total! --- --- @since 0.2.0.0 -unsafeRefine :: (Predicate p x) => x -> Refined p x -unsafeRefine = either (error . displayException) id . refine -{-# INLINABLE unsafeRefine #-} - --- | Constructs a 'Refined' value, completely --- ignoring any refinements! Use this only --- when you can manually prove that the refinement --- holds. --- --- @since 0.3.0.0 -reallyUnsafeRefine :: x -> Refined p x -reallyUnsafeRefine = coerce -{-# INLINE reallyUnsafeRefine #-} - --- | A coercion between a type and any refinement of that type. --- See "Data.Type.Coercion" for functions manipulating --- coercions. --- --- @since 0.3.0.0 -reallyUnsafeUnderlyingRefined :: Coercion x (Refined p x) -reallyUnsafeUnderlyingRefined = Coercion - --- | A coercion between two 'Refined' types, magicking up the --- claim that one predicate is entirely equivalent to another. --- --- @since 0.3.0.0 -reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x) -reallyUnsafePredEquiv = Coercion --- Note: reallyUnsafePredEquiv = --- sym 'reallyUnsafeUnderlyingRefined' `trans` 'reallyUnsafeUnderlyingRefined' - -#if __GLASGOW_HASKELL__ >= 805 --- | Reveal that @x@ and @'Refined' p x@ are 'Coercible' for --- /all/ @x@ and @p@ simultaneously. --- --- === Example --- --- @ --- reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x) --- reallyUnsafePredEquiv = reallyUnsafeAllUnderlyingRefined Coercion --- @ --- --- @since 0.3.0.0 -reallyUnsafeAllUnderlyingRefined - :: ((forall x y p. (Coercible x y => Coercible y (Refined p x))) => r) -> r --- Why is this constraint so convoluted? Because otherwise the constraint --- solver doesn't handle transitivity properly. See "Safe Zero-cost Coercions --- for Haskell" by Breitner et al. -reallyUnsafeAllUnderlyingRefined r = r -#endif +--------------------------------------------------------------------------------++-- Copyright © 2015 Nikita Volkov+-- Copyright © 2018 Remy Goldschmidt+-- Copyright © 2020 chessai+--+-- Permission is hereby granted, free of charge, to any person+-- obtaining a copy of this software and associated documentation+-- files (the "Software"), to deal in the Software without+-- restriction, including without limitation the rights to use,+-- copy, modify, merge, publish, distribute, sublicense, and/or sell+-- copies of the Software, and to permit persons to whom the+-- Software is furnished to do so, subject to the following+-- conditions:+--+-- The above copyright notice and this permission notice shall be+-- included in all copies or substantial portions of the Software.+--+-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES+-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND+-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT+-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,+-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING+-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR+-- OTHER DEALINGS IN THE SOFTWARE.++--------------------------------------------------------------------------------++{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE PolyKinds #-}+#if __GLASGOW_HASKELL__ >= 805+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes #-}+#endif+{-# OPTIONS_GHC -Wall #-}++--------------------------------------------------------------------------------++-- | This module exposes /unsafe/ refinements. An /unsafe/ refinement+-- is one which either does not make the guarantee of totality in construction+-- of the 'Refined' value or does not perform a check of the refinement+-- predicate. It is recommended only to use this when you can manually prove+-- that the refinement predicate holds.+module Refined.Unsafe+ ( -- * 'Refined'+ Refined++ -- ** Creation+ , reallyUnsafeRefine+ , unsafeRefine++ -- ** Coercion+ , reallyUnsafeUnderlyingRefined+#if __GLASGOW_HASKELL__ >= 805+ , reallyUnsafeAllUnderlyingRefined+#endif+ , reallyUnsafePredEquiv+ ) where++--------------------------------------------------------------------------------++import Control.Exception (displayException)+import Data.Coerce (coerce)++import Refined (Predicate, refine)+import Refined.Unsafe.Type (Refined(Refined))+import Data.Type.Coercion (Coercion (..))+#if __GLASGOW_HASKELL__ >= 805+import Data.Coerce (Coercible)+#endif++--------------------------------------------------------------------------------++-- | Constructs a 'Refined' value at run-time,+-- calling 'Prelude.error' if the value+-- does not satisfy the predicate.+--+-- WARNING: this function is not total!+--+-- @since 0.2.0.0+unsafeRefine :: (Predicate p x) => x -> Refined p x+unsafeRefine = either (error . displayException) id . refine+{-# INLINABLE unsafeRefine #-}++-- | Constructs a 'Refined' value, completely+-- ignoring any refinements! Use this only+-- when you can manually prove that the refinement+-- holds.+--+-- @since 0.3.0.0+reallyUnsafeRefine :: x -> Refined p x+reallyUnsafeRefine = coerce+{-# INLINE reallyUnsafeRefine #-}++-- | A coercion between a type and any refinement of that type.+-- See "Data.Type.Coercion" for functions manipulating+-- coercions.+--+-- @since 0.3.0.0+reallyUnsafeUnderlyingRefined :: Coercion x (Refined p x)+reallyUnsafeUnderlyingRefined = Coercion++-- | A coercion between two 'Refined' types, magicking up the+-- claim that one predicate is entirely equivalent to another.+--+-- @since 0.3.0.0+reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x)+reallyUnsafePredEquiv = Coercion+-- Note: reallyUnsafePredEquiv =+-- sym 'reallyUnsafeUnderlyingRefined' `trans` 'reallyUnsafeUnderlyingRefined'++#if __GLASGOW_HASKELL__ >= 805+-- | Reveal that @x@ and @'Refined' p x@ are 'Coercible' for+-- /all/ @x@ and @p@ simultaneously.+--+-- === Example+--+-- @+-- reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x)+-- reallyUnsafePredEquiv = reallyUnsafeAllUnderlyingRefined Coercion+-- @+--+-- @since 0.3.0.0+reallyUnsafeAllUnderlyingRefined+ :: ((forall x y p. (Coercible x y => Coercible y (Refined p x))) => r) -> r+-- Why is this constraint so convoluted? Because otherwise the constraint+-- solver doesn't handle transitivity properly. See "Safe Zero-cost Coercions+-- for Haskell" by Breitner et al.+reallyUnsafeAllUnderlyingRefined r = r+#endif
src/Refined/Unsafe/Type.hs view
@@ -1,81 +1,81 @@--------------------------------------------------------------------------------- - --- Copyright © 2015 Nikita Volkov --- Copyright © 2018 Remy Goldschmidt --- Copyright © 2020 chessai --- --- Permission is hereby granted, free of charge, to any person --- obtaining a copy of this software and associated documentation --- files (the "Software"), to deal in the Software without --- restriction, including without limitation the rights to use, --- copy, modify, merge, publish, distribute, sublicense, and/or sell --- copies of the Software, and to permit persons to whom the --- Software is furnished to do so, subject to the following --- conditions: --- --- The above copyright notice and this permission notice shall be --- included in all copies or substantial portions of the Software. --- --- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, --- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES --- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND --- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT --- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, --- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING --- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR --- OTHER DEALINGS IN THE SOFTWARE. - --------------------------------------------------------------------------------- - -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RoleAnnotations #-} -{-# LANGUAGE TemplateHaskell #-} - --------------------------------------------------------------------------------- - --- | This module exports the 'Refined' type with its --- constructor. This is very risky! In particular, the 'Data.Coerce.Coercible' --- instances will be visible throughout the importing module. --- It is usually better to build the necessary coercions locally --- using the utilities in "Refined.Unsafe", but in some cases --- it may be more convenient to write a separate module that --- imports this one and exports some large coercion. -module Refined.Unsafe.Type - ( Refined(Refined) - ) where - -import Control.DeepSeq (NFData) -import Data.Hashable (Hashable) -import qualified Language.Haskell.TH.Syntax as TH - --- | A refinement type, which wraps a value of type @x@. --- --- @since 0.1.0.0 -newtype Refined (p :: k) x - = Refined x -- ^ @since 0.1.0.0 - deriving newtype - ( Eq -- ^ @since 0.1.0.0 - , Ord -- ^ @since 0.1.0.0 - , Hashable -- ^ @since 0.6.3 - , NFData -- ^ @since 0.5 - ) - deriving stock - ( Show -- ^ @since 0.1.0.0 - ) - deriving stock - ( Foldable -- ^ @since 0.2 - ) - --- | @since 0.3.0.0 -type role Refined nominal nominal - --- | @since 0.1.0.0 -instance (TH.Lift x) => TH.Lift (Refined p x) where - lift (Refined a) = [|Refined a|] -#if MIN_VERSION_template_haskell(2,16,0) - liftTyped (Refined a) = [||Refined a||] -#endif +--------------------------------------------------------------------------------++-- Copyright © 2015 Nikita Volkov+-- Copyright © 2018 Remy Goldschmidt+-- Copyright © 2020 chessai+--+-- Permission is hereby granted, free of charge, to any person+-- obtaining a copy of this software and associated documentation+-- files (the "Software"), to deal in the Software without+-- restriction, including without limitation the rights to use,+-- copy, modify, merge, publish, distribute, sublicense, and/or sell+-- copies of the Software, and to permit persons to whom the+-- Software is furnished to do so, subject to the following+-- conditions:+--+-- The above copyright notice and this permission notice shall be+-- included in all copies or substantial portions of the Software.+--+-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES+-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND+-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT+-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,+-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING+-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR+-- OTHER DEALINGS IN THE SOFTWARE.++--------------------------------------------------------------------------------++{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE TemplateHaskell #-}++--------------------------------------------------------------------------------++-- | This module exports the 'Refined' type with its+-- constructor. This is very risky! In particular, the 'Data.Coerce.Coercible'+-- instances will be visible throughout the importing module.+-- It is usually better to build the necessary coercions locally+-- using the utilities in "Refined.Unsafe", but in some cases+-- it may be more convenient to write a separate module that+-- imports this one and exports some large coercion.+module Refined.Unsafe.Type+ ( Refined(Refined)+ ) where++import Control.DeepSeq (NFData)+import Data.Hashable (Hashable)+import qualified Language.Haskell.TH.Syntax as TH++-- | A refinement type, which wraps a value of type @x@.+--+-- @since 0.1.0.0+newtype Refined (p :: k) x+ = Refined x -- ^ @since 0.1.0.0+ deriving newtype+ ( Eq -- ^ @since 0.1.0.0+ , Ord -- ^ @since 0.1.0.0+ , Hashable -- ^ @since 0.6.3+ , NFData -- ^ @since 0.5+ )+ deriving stock+ ( Show -- ^ @since 0.1.0.0+ )+ deriving stock+ ( Foldable -- ^ @since 0.2+ )++-- | @since 0.3.0.0+type role Refined nominal nominal++-- | @since 0.1.0.0+instance (TH.Lift x) => TH.Lift (Refined p x) where+ lift (Refined a) = [|Refined a|]+#if MIN_VERSION_template_haskell(2,16,0)+ liftTyped (Refined a) = [||Refined a||]+#endif
test/Compiles.hs view
@@ -1,58 +1,58 @@-{-# language - AllowAmbiguousTypes - , DataKinds - , FlexibleInstances - , MultiParamTypeClasses - , OverloadedStrings - , TemplateHaskell - , TypeApplications - #-} - -module Main (main) where - -import Refined -import Data.Void (Void) - -id_ = $$(refineTH_ @IdPred @Int 3) -even_ = $$(refineTH_ @(Not Even) @Int 3) -odd_ = $$(refineTH_ @Odd @Int 3) - ---fails = --- $$(refineTH --- @( And --- NonEmpty --- ( Empty --- ) --- ) --- @[Int] --- --- [1,2,3] --- ) - - ---foo = $$(refineTH --- @( And --- Even --- ( Xor --- ( And --- (Not (DivisibleBy 3)) --- IdPred --- ) --- (DivisibleBy 2) --- ) --- ) --- @Int --- 3) ---bar = case foo of --- Left e -> e --- Right _ -> error "bad!" - -main :: IO () -main = do - putStrLn "refined/test/Compiles.hs: it compiles!" - foldMap print - [ id_ - , even_ - , odd_ - ] --- print bar +{-# language+ AllowAmbiguousTypes+ , DataKinds+ , FlexibleInstances+ , MultiParamTypeClasses+ , OverloadedStrings+ , TemplateHaskell+ , TypeApplications+ #-}++module Main (main) where++import Refined+import Data.Void (Void)++id_ = $$(refineTH_ @IdPred @Int 3)+even_ = $$(refineTH_ @(Not Even) @Int 3)+odd_ = $$(refineTH_ @Odd @Int 3)++--fails =+-- $$(refineTH+-- @( And+-- NonEmpty+-- ( Empty+-- )+-- )+-- @[Int]+--+-- [1,2,3]+-- )+++--foo = $$(refineTH+-- @( And+-- Even+-- ( Xor+-- ( And+-- (Not (DivisibleBy 3))+-- IdPred+-- )+-- (DivisibleBy 2)+-- )+-- )+-- @Int+-- 3)+--bar = case foo of+-- Left e -> e+-- Right _ -> error "bad!"++main :: IO ()+main = do+ putStrLn "refined/test/Compiles.hs: it compiles!"+ foldMap print+ [ id_+ , even_+ , odd_+ ]+-- print bar
test/QuickCheck.hs view
@@ -1,63 +1,63 @@-{-# language - DataKinds - , GeneralizedNewtypeDeriving - , ScopedTypeVariables - , TypeApplications - , TypeOperators - , ViewPatterns - #-} - -module Main (main) where - -import Test.QuickCheck -import Refined - -main :: IO () -main = mapM_ quickCheck - [ prop_lt - , prop_gt - , prop_from - , prop_to - , prop_bad - , prop_shrink_lt - , prop_shrink_gt - ] - -iddy :: (Eq a) => Refined p a -> Bool -iddy (unrefine -> r) = r == r - -prop_lt :: Property -prop_lt = property $ \(r :: Refined (LessThan 5) MyInt) -> iddy r - -prop_gt :: Property -prop_gt = property $ \(r :: Refined (GreaterThan 5) MyInt) -> iddy r - -prop_from :: Property -prop_from = property $ \(r :: Refined (From 9) MyInt) -> iddy r - -prop_to :: Property -prop_to = property $ \(r :: Refined (To 9) MyInt) -> iddy r - -prop_bad :: Property -prop_bad = expectFailure $ ioProperty $ do - -- expectFailure expects the error inside the property itself, not while - -- generating the argument to the property. So we need to hide generation from - -- it. - r :: Refined (EqualTo 2 && EqualTo 3) MyInt <- generate arbitrary - return $ iddy r - -prop_shrink_lt :: Property -prop_shrink_lt = property $ \(r :: Refined (LessThan 5) MyInt) -> - (unrefine <$> shrink r) == shrink (unrefine r) - -prop_shrink_gt :: Property -prop_shrink_gt = property $ \(r :: Refined (GreaterThan 5) MyInt) -> - (unrefine <$> shrink r) == (filter (> 5) $ shrink (unrefine r)) - -newtype MyInt = MyInt Int - deriving (Eq, Ord, Show, Num) - -instance Arbitrary MyInt where - arbitrary = MyInt <$> choose (0,100) - shrink (MyInt 0) = [] - shrink (MyInt n) = MyInt <$> [0..n-1] +{-# language+ DataKinds+ , GeneralizedNewtypeDeriving+ , ScopedTypeVariables+ , TypeApplications+ , TypeOperators+ , ViewPatterns+ #-}++module Main (main) where++import Test.QuickCheck+import Refined++main :: IO ()+main = mapM_ quickCheck+ [ prop_lt+ , prop_gt+ , prop_from+ , prop_to+ , prop_bad+ , prop_shrink_lt+ , prop_shrink_gt+ ]++iddy :: (Eq a) => Refined p a -> Bool+iddy (unrefine -> r) = r == r++prop_lt :: Property+prop_lt = property $ \(r :: Refined (LessThan 5) MyInt) -> iddy r++prop_gt :: Property+prop_gt = property $ \(r :: Refined (GreaterThan 5) MyInt) -> iddy r++prop_from :: Property+prop_from = property $ \(r :: Refined (From 9) MyInt) -> iddy r++prop_to :: Property+prop_to = property $ \(r :: Refined (To 9) MyInt) -> iddy r++prop_bad :: Property+prop_bad = expectFailure $ ioProperty $ do+ -- expectFailure expects the error inside the property itself, not while+ -- generating the argument to the property. So we need to hide generation from+ -- it.+ r :: Refined (EqualTo 2 && EqualTo 3) MyInt <- generate arbitrary+ return $ iddy r++prop_shrink_lt :: Property+prop_shrink_lt = property $ \(r :: Refined (LessThan 5) MyInt) ->+ (unrefine <$> shrink r) == shrink (unrefine r)++prop_shrink_gt :: Property+prop_shrink_gt = property $ \(r :: Refined (GreaterThan 5) MyInt) ->+ (unrefine <$> shrink r) == (filter (> 5) $ shrink (unrefine r))++newtype MyInt = MyInt Int+ deriving (Eq, Ord, Show, Num)++instance Arbitrary MyInt where+ arbitrary = MyInt <$> choose (0,100)+ shrink (MyInt 0) = []+ shrink (MyInt n) = MyInt <$> [0..n-1]