refined 0.8 → 0.8.1
raw patch · 9 files changed
+2484/−2413 lines, 9 filesdep ~QuickCheckdep ~aesondep ~base
Dependency ranges changed: QuickCheck, aeson, base, bytestring, deepseq, exceptions, hashable, mtl, template-haskell, text, these-skinny
Files
- LICENSE +24/−24
- README.md +13/−13
- changelog.md +207/−196
- refined.cabal +128/−128
- src/Refined.hs +1778/−1718
- 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,196 +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] - 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,128 @@-cabal-version:- 2.0-name:- refined-version:- 0.8-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-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.18- , 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.3- , template-haskell >= 2.9 && < 2.20- , 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: 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
src/Refined.hs view
@@ -1,1718 +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 TemplateHaskell #-}-{-# 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-- -- * 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-(|>) = flip ($)-{-# INLINE (|>) #-}---- | Helper function, stolen from the flow package.-(.>) :: (a -> b) -> (b -> c) -> a -> c-f .> g = \x -> g (f x)-{-# INLINE (.>) #-}---- | 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)---- | 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---- | 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]