refined 0.4.4 → 0.8.2
raw patch · 15 files changed
Files
- LICENSE +1/−1
- README.md +13/−0
- changelog.md +207/−0
- refined.cabal +24/−40
- src/Refined.hs +1774/−146
- src/Refined/Internal.hs +0/−1150
- src/Refined/Orphan.hs +0/−44
- src/Refined/Orphan/Aeson.hs +0/−56
- src/Refined/Orphan/QuickCheck.hs +0/−91
- src/Refined/These.hs +0/−265
- src/Refined/Unsafe.hs +21/−11
- src/Refined/Unsafe/Type.hs +40/−4
- test/Compiles.hs +41/−9
- test/Doctests.hs +0/−23
- test/QuickCheck.hs +18/−2
LICENSE view
@@ -1,6 +1,6 @@ Copyright © 2015 Nikita Volkov Copyright © 2018 Remy Goldschmidt-Copyright © 2019 chessai+Copyright © 2020 chessai Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation
+ README.md view
@@ -0,0 +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/
+ changelog.md view
@@ -0,0 +1,207 @@+# Changelog+All notable changes to this project will be documented in this file.++The format is based on [Keep a Changelog](http://keepachangelog.com/en/1.0.0/)+and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/).++## [0.8.1] - 2023-04-05+### Added+- `Weaken` instances for `SizeGreaterThan`, `SizeLessThan`.+- `weakenAndLeft`, `weakenAndRight`, `weakenOrLeft`, `weakenOrRight`+ type inference helper functions.++### Changed+- bump `base`: "< 4.18" -> "< 4.19"+- bump `mtl`: "< 2.3" -> "< 2.4"+- bump `template-haskell`: "< 2.20" -> "< 2.21"++## [0.8] - 2022-10-09+### Changed+- on GHC >=9, make `refineTH` and `refineTH_` work in any monad+ `(Quote m, MonadFail m)`.+- bump `base`: "< 4.17" -> "< 4.18"+- bump `template-haskell`: "< 2.19" -> "< 2.20"+- bump `aeson`: "< 2.1" -> "< 2.2"++## [0.7] - 2022-07-01+### Changed+- make `Refined` predicate type `p` kind polymorphic (`p :: Type` -> `p :: k`)++## [0.6.3] - 2022-01-14+### Added+- `Hashable` instance for `Refined`+- `FromJSONKey` instance for `Refined`+- `ToJSONKey` instance for `Refined`+- `shrink` for `Refined`'s `Arbitrary` instance.+- `refineEither` function++### Changed+- improved efficiency of `strengthen`+- bump multiple dependency upper bounds++## [0.6.2] - 2021-01-31+### Changed+- `strengthen` no longer returns an `Either`, since the proof+ that it should always succeed is in its constraints.+- correct `success` documentation++## [0.6.1] - 2020-08-02+### Changed+- upper bound on QuickCheck: <2.14 -> <2.15++## [0.6] - 2020-07-21+### Changed+- `validate` now takes a `Proxy` as its first argument.+- All uses of prettyprinter are now just `Text`++### Removed+- Refined.These module+- Dependency on `prettyprinter`++### Fixed+- bug in `sized` internal helper that caused formatting issues+ in sized predicate errors++## [0.5.1] - 2020-07-14+### Changed+- `refineTH_` is now implemented in terms of `refineTH`+- Fix pretty-printing of `RefineException`s during compile-time++## [0.5] - 2020-07-11+### Added+- sized Predicate instances for `Text`+- sized Predicate instances for strict and lazy `ByteString`+- INLINABLE pragmas on `refine_` `reifyPredicate`+- `NFData` instance for `Refined`+- RefineSomeException constructor. Enables recovering+ specific validation exceptions.+ Thanks to @haroldcarr for adding this.+- RefineXorException constructor.+- `Empty` and `NotEmpty` predicates.+- `NaN` and `Infinite` predicates for floating-point numbers.+- @since pragmas to EVERYTHING.++### Changed+- lower bound on mtl to 2.2.2 due to use of liftEither.+ Thanks to @k0ral for reporting this+- Generalize sized predicates+- Allow newer template-haskell (< 0.16 ==> < 0.17)+- Allow newer aeson (< 1.5 ==> < 1.6)+ Thanks to @locallycompact for this change.++### Removed+- `Refined.Internal` module+ Thanks to @nikita-volkov for pushing me to do this.+- Orphan modules+ Thanks to @symbiont-sam-halliday for pointing out the+ silliness of these modules.+- `RefineT`. It was a needless abstraction that just made the+ library harder to learn and use, providing little benefit+ over `Maybe RefineException`.+ Thanks to @nikita-volkov for helping me see the light.++### Deprecated+- Refined.These module in favour of Data.These from these-skinny++## [0.4.4] - 2019-10-18+### Added+- `refine_`+- `refineTH_`+- test suite: unit tests for compiling.+### Changed+- Allow newer `template-haskell` and `QuickCheck`.++## [0.4.2.3] - 2019-09-17+### Added+- `reifyPredicate`+### Fixed+- `Arbitrary` instance for `Refined` should now always terminate.+ Thanks to @symbiont-joseph-kachmar for reporting this.++## [0.4.2.2] - 2019-07-19+### Added+- `exceptRefine`, `strengthen`, and `strengthenM`++## [0.4.2.1] - 2019-05-31+### Fixed+- Documentation fix for `DivisibleBy`+### Changed+- Re-export `DivisibleBy`, `Even`, and `Odd` from module `Refined`.+- Re-export all constructors from module `Refined`.++## [0.4.2] - 2019-05-30+### Removed+- Re-removed dependency of `these` package.+### Added+- `Even`, `Odd`, and `DivisibleBy` predicates.+- doctests for all predicates.+### Changed+- Make all predicates unary data constructors, instead of nullary,+ and export those newly added constructors.++## [0.4.1] - 2019-04-15+### Fixed+- Serious regression where `Not p` ~ `p`. Thanks to @k0ral who reported this.++## [0.4] - 2019-03-18+### Added+- 'NegativeFromTo', a Predicate that ensures a numeric value is within a range [a,b],+ where a < 0 and b >= a.+ Thanks to github.com/futtetennista for this change.+### Changed+- `RefinedNotException` now has a child (it should have had one in v2. This was an oversight.)+- `displayRefineException` no longer uses tabs, instead 2 spaces.+- make implementation of `displayRefineException` more clear via formatting.++## [0.3.0.0] - 2018-09-26+### Added+- Internal module, and Unsafe modules, making sure to take care w.r.t.+ the scope of coercions related to the use of the 'Refined' constructor.+- 'IdPred' predicate, predicate that never fails.+- Generic instances for all predicates.+- `reallyUnsafeRefine`, `reallyUnsafeUnderlyingRefined`, `reallyUnsafeAllUnderlyingRefined`,+ functions that allow one to use 'Coercion's to manually prove things about 'Refined'+ values.+### Changed+- Type role of Refined from 'phantom Representational' to 'nominal nominal'.+ With the old type role, one can use `coerce` to prove `Q x` given any `P x`.+ The second parameter should also be nominal because of interactions with something+ like `GreaterThan` and `Data.Ord.Down`.+ Thanks to David Feuer for pointing this out.+- Change docs to point users to 'Refined.Unsafe' module instead of recommending+ 'Unsafe.Coerce.unsafeCoerce'.+- 'Ascending' and 'Descending' predicates now use 'Foldable' instead of 'IsList'.+- Lowered the lower bound on 'exceptions'; it was too strict for the support window.+### Removed+- Dependency of the 'these' package. It brings in some very+ heavy transitive dependencies, even though the datatype+ in `refined` is used to the most minimal extent.+ This is a breaking change because+ this change is exposed to the end user via 'RefineAndException'.+ It is exported from a module called 'Refined.These'. Users+ wishing to interact with such exceptions can either just+ use the datatype constituting a minimal API there, or depend+ on the 'these' package.++## [0.2.3.0] - 2018-06-01+### Added+- back in the 'Foldable' instance for 'Refined'. It is safe.++## [0.2.2.0] - 2018-05-31+### Removed+- Unsafe typeclass instances that could break the 'Refined' invariant.+ These should not have been added.++## [0.2.1.0] - 2018-05-31+### Removed+- Unsafe typeclass instances that could break the 'Refined' invariant.+ These should not have been added.++## [0.2.0.0] - 2018-05-30+### Changed+- Radical rewrite of the library, centred around 'RefineException'+ and the 'RefineT' monad transformer.+ 'validate' now has the type signature+ validate :: (Predicate p x, Monad m) => p -> x -> RefineT m ()+### Added+- More predicates
refined.cabal view
@@ -1,9 +1,8 @@-cabal-version:- 2.0+cabal-version: 3.0 name: refined version:- 0.4.4+ 0.8.2 synopsis: Refinement types with static and runtime checking description:@@ -22,7 +21,7 @@ copyright: Copyright © 2015, Nikita Volkov Copyright © 2018, Remy Goldschmidt- Copyright © 2019, chessai+ Copyright © 2020, chessai license: MIT license-file:@@ -30,10 +29,17 @@ build-type: Simple tested-with:- GHC == 8.0.2- , GHC == 8.2.2- , GHC == 8.4.4+ 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:@@ -62,40 +68,27 @@ src exposed-modules: Refined- Refined.Internal- Refined.Orphan- Refined.Orphan.Aeson- Refined.Orphan.QuickCheck- Refined.These Refined.Unsafe Refined.Unsafe.Type default-language: Haskell2010 build-depends:- base >= 4.9.1 && < 4.14- , deepseq >= 1.4 && < 1.5- , exceptions >= 0.8 && < 0.11- , mtl >= 2.2.1 && < 2.3- , prettyprinter >= 1.1.0.1 && < 1.4- , template-haskell >= 2.9 && < 2.16- , transformers >= 0.5 && < 0.6+ , base >= 4.11 && < 5+ , bytestring >= 0.10+ , deepseq >= 1.4+ , exceptions >= 0.8+ , hashable >= 1.0+ , mtl >= 2.2.2+ , template-haskell >= 2.9+ , text >= 1.2+ , these-skinny >= 0.7.5 if flag(aeson)- build-depends: aeson >= 0.9 && < 1.5+ build-depends: aeson >= 0.9 cpp-options: -DHAVE_AESON if flag(QuickCheck)- build-depends: QuickCheck >= 2.1 && < 2.14+ build-depends: QuickCheck >= 2.1 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@@ -114,12 +107,3 @@ 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
@@ -2,149 +2,1777 @@ -- Copyright © 2015 Nikita Volkov -- Copyright © 2018 Remy Goldschmidt--- Copyright © 2019 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 #-}------------------------------------------------------------------------------------{-# language ExplicitNamespaces #-}-------------------------------------------------------------------------------------- | 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/------ This module only provides /safe/ constructions of 'Refined'--- values, /safe/ meaning that the refinement predicate holds,--- and the construction of the 'Refined' value is total.------ If you can manually prove that the refinement predicate holds,--- or you do not necessarily care about this definition of safety,--- use the module /Refined.Unsafe/.-module Refined- ( -- * 'Refined'- Refined-- -- ** Creation- , refine- , refine_- , refineThrow- , refineFail- , refineError- , refineTH- , refineTH_-- -- ** Consumption- , unrefine-- -- * 'Predicate'- , Predicate (validate)- , reifyPredicate-- -- * Logical predicates- , Not(..)- , And(..)- , type (&&)- , Or(..)- , type (||)-- -- * Identity predicate- , IdPred(..)-- -- * Numeric predicates- , LessThan(..)- , GreaterThan(..)- , From(..)- , To(..)- , FromTo(..)- , NegativeFromTo(..)- , EqualTo(..)- , NotEqualTo(..)- , Odd(..)- , Even(..)- , DivisibleBy(..)- , Positive- , NonPositive- , Negative- , NonNegative- , ZeroToOne- , NonZero-- -- * Foldable predicates- , SizeLessThan(..)- , SizeGreaterThan(..)- , SizeEqualTo(..)- , NonEmpty-- -- * IsList predicates- , Ascending(..)- , Descending(..)-- -- * Weakening- , Weaken (weaken)- , andLeft- , andRight- , leftOr- , rightOr-- -- * Strengthening- , strengthen- , strengthenM-- -- * Error handling-- -- ** 'RefineException'- , RefineException- ( RefineNotException- , RefineAndException- , RefineOrException- , RefineOtherException- )- , displayRefineException-- -- ** 'RefineT' and 'RefineM'- , RefineT, runRefineT, exceptRefine, mapRefineT- , RefineM, refineM, runRefineM- , throwRefine, catchRefine- , throwRefineOtherException-- -- * Re-Exports- , pretty- ) where------------------------------------------------------------------------------------import Refined.Internal---------------------------------------------------------------------------------+-- 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/Internal.hs
@@ -1,1150 +0,0 @@------------------------------------------------------------------------------------- Copyright © 2015 Nikita Volkov--- Copyright © 2018 Remy Goldschmidt--- Copyright © 2019 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 -funbox-strict-fields #-}------------------------------------------------------------------------------------{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DeriveFoldable #-}-{-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE ExplicitNamespaces #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE QuasiQuotes #-}-{-# LANGUAGE RankNTypes #-}-{-# 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.Internal- ( -- * 'Refined'- Refined(Refined)-- -- ** Creation- , refine- , refine_- , refineThrow- , refineFail- , refineError- , refineTH- , refineTH_-- -- ** Consumption- , unrefine-- -- * 'Predicate'- , Predicate (validate)- , reifyPredicate-- -- * Logical predicates- , Not(..)- , And(..)- , type (&&)- , Or(..)- , type (||)-- -- * Identity predicate- , IdPred(..)-- -- * Numeric predicates- , LessThan(..)- , GreaterThan(..)- , From(..)- , To(..)- , FromTo(..)- , NegativeFromTo(..)- , EqualTo(..)- , NotEqualTo(..)- , Odd(..)- , Even(..)- , DivisibleBy(..)- , Positive- , NonPositive- , Negative- , NonNegative- , ZeroToOne- , NonZero-- -- * Foldable predicates- , SizeLessThan(..)- , SizeGreaterThan(..)- , SizeEqualTo(..)- , NonEmpty-- -- * IsList predicates- , Ascending(..)- , Descending(..)-- -- * Weakening- , Weaken (weaken)- , andLeft- , andRight- , leftOr- , rightOr-- -- * Strengthening- , strengthen- , strengthenM-- -- * Error handling-- -- ** 'RefineException'- , RefineException- ( RefineNotException- , RefineAndException- , RefineOrException- , RefineOtherException- )- , displayRefineException-- -- ** 'RefineT' and 'RefineM'- , RefineT, runRefineT, exceptRefine, mapRefineT- , RefineM, refineM, runRefineM- , throwRefine, catchRefine- , throwRefineOtherException-- , (|>)- , (.>)-- -- * Re-Exports- , PP.pretty- ) where------------------------------------------------------------------------------------import Prelude- (Num, fromIntegral, negate, undefined)--import Control.Applicative (Applicative (pure))-import Control.Exception (Exception (displayException))-import Control.Monad (Monad, unless, when)-import Data.Bool (Bool(True,False),(&&), otherwise)-import Data.Coerce (coerce)-import Data.Either- (Either (Left, Right), either, isRight)-import Data.Eq (Eq, (==), (/=))-import Data.Foldable (Foldable(length, foldl'))-import Data.Function (const, flip, ($), (.))-import Data.Functor (Functor, fmap)-import Data.Functor.Identity (Identity (runIdentity))-import Data.Monoid (mconcat)-import Data.Ord (Ord, (<), (<=), (>), (>=))-import Data.Proxy (Proxy (Proxy))-import Data.Semigroup (Semigroup((<>)))-import Data.Typeable (TypeRep, Typeable, typeOf)-import Data.Void (Void)-import Text.Read (Read (readsPrec), lex, readParen)-import Text.Show (Show (show))--import Control.Monad.Catch (MonadThrow)-import qualified Control.Monad.Catch as MonadThrow-import Control.Monad.Error.Class (MonadError)-import qualified Control.Monad.Error.Class as MonadError-import Control.Monad.Fail (MonadFail, fail)-import Control.Monad.Fix (MonadFix, fix)-import Control.Monad.Trans.Class (MonadTrans (lift))--import Control.Monad.Trans.Except (ExceptT)-import qualified Control.Monad.Trans.Except as ExceptT--import GHC.Generics (Generic, Generic1)-import GHC.TypeLits (type (<=), KnownNat, Nat, natVal)--import GHC.Real (Integral(mod), even, odd)--import Refined.These (These(This,That,These))--import qualified Data.Text.Prettyprint.Doc as PP-import qualified Language.Haskell.TH.Syntax as TH-------------------------------------------------------------------------------------- $setup------ Doctest imports------ >>> :set -XDataKinds--- >>> :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 #-}-------------------------------------------------------------------------------------- | A refinement type, which wraps a value of type @x@,--- ensuring that it satisfies a type-level predicate @p@.-newtype Refined p x = Refined x- deriving (Eq, Foldable , Ord, Show, Typeable)--type role Refined nominal nominal---- | This instance makes sure to check the refinement.-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 _ -> []--instance (TH.Lift x) => TH.Lift (Refined p x) where- lift (Refined a) = [|Refined a|]-------------------------------------------------------------------------------------- | A smart constructor of a 'Refined' value.--- Checks the input value at runtime.-refine :: (Predicate p x) => x -> Either RefineException (Refined p x)-refine x = do- let predicateByResult :: RefineM (Refined p x) -> p- predicateByResult = const undefined- runRefineM $ fix $ \result -> do- validate (predicateByResult result) x- pure (Refined 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'.-refine_ :: forall p x. (Predicate p x) => x -> Either RefineException x-refine_ = refine @p @x .> coerce---- | Constructs a 'Refined' value at run-time,--- calling 'Control.Monad.Catch.throwM' if the value--- does not satisfy the predicate.-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.-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.-refineError :: (Predicate p x, MonadError RefineException m)- => x -> m (Refined p x)-refineError = refine .> either MonadError.throwError pure-{-# INLINABLE refineError #-}-------------------------------------------------------------------------------------- | 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------ If it's not evident, 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.------ It may be useful to use this function with the `th-lift-instances` package at https://hackage.haskell.org/package/th-lift-instances/-refineTH :: (Predicate p x, TH.Lift x) => x -> TH.Q (TH.TExp (Refined p x))-refineTH =- let refineByResult :: (Predicate p x)- => TH.Q (TH.TExp (Refined p x))- -> x- -> Either RefineException (Refined p x)- refineByResult = const refine- in fix $ \loop -> refineByResult (loop undefined)- .> either (show .> fail) TH.lift- .> fmap TH.TExp---- | Like 'refineTH', but immediately unrefines the value.--- This is useful when some value need only be refined--- at compile-time.-refineTH_ :: forall p x. (Predicate p x, TH.Lift x)- => x- -> TH.Q (TH.TExp x)-refineTH_ =- let refineByResult :: (Predicate p x)- => TH.Q (TH.TExp x)- -> x- -> Either RefineException x- refineByResult = const (refine_ @p @x)- in fix $ \loop -> refineByResult (loop undefined)- .> either (show .> fail) TH.lift- .> fmap TH.TExp-------------------------------------------------------------------------------------- | Extracts the refined value.-{-# INLINE unrefine #-}-unrefine :: Refined p x -> x-unrefine = coerce-------------------------------------------------------------------------------------- | A typeclass which defines a runtime interpretation of--- a type-level predicate @p@ for type @x@.-class (Typeable p) => Predicate p x where- {-# MINIMAL validate #-}- -- | Check the value @x@ according to the predicate @p@,- -- producing an error string if the value does not satisfy.- validate :: (Monad m) => p -> x -> RefineT m ()-------------------------------------------------------------------------------------- | Reify a 'Predicate' by turning it into a value-level predicate.-reifyPredicate :: forall p a. Predicate p a => a -> Bool-reifyPredicate = refine @p @a .> isRight-------------------------------------------------------------------------------------- | 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----data IdPred = IdPred- deriving (Generic)--instance Predicate IdPred x where- validate _ _ = pure ()- {-# INLINE validate #-}-------------------------------------------------------------------------------------- | The negation of a predicate.------ >>> isRight (refine @(Not NonEmpty) @[Int] [])--- True------ >>> isLeft (refine @(Not NonEmpty) @[Int] [1,2])--- True-data Not p = Not- deriving (Generic, Generic1)--instance (Predicate p x, Typeable p) => Predicate (Not p) x where- validate p x = do- result <- runRefineT (validate @p undefined x)- when (isRight result) $ do- throwRefine (RefineNotException (typeOf p))-------------------------------------------------------------------------------------- | The conjunction of two predicates.------ >>> isLeft (refine @(And Positive Negative) @Int 3)--- True------ >>> isRight (refine @(And Positive Odd) @Int 203)--- True-data And l r = And- deriving (Generic, Generic1)--infixr 3 &&--- | The conjunction of two predicates.-type (&&) = And--instance ( Predicate l x, Predicate r x, Typeable l, Typeable r- ) => Predicate (And l r) x where- validate p x = do- a <- lift $ runRefineT $ validate @l undefined x- b <- lift $ runRefineT $ validate @r undefined x- let throw err = throwRefine (RefineAndException (typeOf p) err)- case (a, b) of- (Left e, Left e1) -> throw (These e e1)- (Left e, _) -> throw (This e)- (Right _, Left e) -> throw (That e)- (Right _, Right _) -> pure ()-------------------------------------------------------------------------------------- | The disjunction of two predicates.------ >>> isRight (refine @(Or Even Odd) @Int 3)--- True------ >>> isRight (refine @(Or (LessThan 3) (GreaterThan 3)) @Int 2)--- True-data Or l r = Or- deriving (Generic, Generic1)--infixr 2 ||--- | The disjunction of two predicates.-type (||) = Or--instance ( Predicate l x, Predicate r x, Typeable l, Typeable r- ) => Predicate (Or l r) x where- validate p x = do- left <- lift $ runRefineT $ validate @l undefined x- right <- lift $ runRefineT $ validate @r undefined x- case (left, right) of- (Left l, Left r) -> throwRefine (RefineOrException (typeOf p) l r)- _ -> pure ()-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the 'Foldable' 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-data SizeLessThan (n :: Nat) = SizeLessThan- deriving (Generic)--instance (Foldable t, KnownNat n) => Predicate (SizeLessThan n) (t a) where- validate p x = do- let x' = natVal p- sz = length x- unless (sz < fromIntegral x') $ do- throwRefineOtherException (typeOf p)- ( [ "Size of Foldable is not less than "- , PP.pretty x'- , newline- , twoSpaces- , "Size is: "- , PP.pretty sz- ] |> mconcat- )-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the 'Foldable' 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--data SizeGreaterThan (n :: Nat) = SizeGreaterThan- deriving (Generic)--instance (Foldable t, KnownNat n) => Predicate (SizeGreaterThan n) (t a) where- validate p x = do- let x' = natVal p- sz = length x- unless (sz > fromIntegral x') $ do- throwRefineOtherException (typeOf p)- ( [ "Size of Foldable is not greater than "- , PP.pretty x'- , newline- , twoSpaces- , "Size is: "- , PP.pretty sz- ] |> mconcat- )-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the 'Foldable' 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-data SizeEqualTo (n :: Nat) = SizeEqualTo- deriving (Generic)--instance (Foldable t, KnownNat n) => Predicate (SizeEqualTo n) (t a) where- validate p x = do- let x' = natVal p- sz = length x- unless (sz == fromIntegral x') $ do- throwRefineOtherException (typeOf p)- ( [ "Size of Foldable is not equal to "- , PP.pretty x'- , newline- , twoSpaces- , "Size is: "- , PP.pretty sz- ] |> mconcat- )-------------------------------------------------------------------------------------- | 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-data Ascending = Ascending- deriving (Generic)--instance (Foldable t, Ord a) => Predicate Ascending (t a) where- validate p x = do- unless (increasing x) $ do- throwRefineOtherException (typeOf 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-data Descending = Descending- deriving (Generic)--instance (Foldable t, Ord a) => Predicate Descending (t a) where- validate p x = do- unless (decreasing x) $ do- throwRefineOtherException (typeOf 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-data LessThan (n :: Nat) = LessThan- deriving (Generic)--instance (Ord x, Num x, KnownNat n) => Predicate (LessThan n) x where- validate p x = do- let x' = natVal p- unless (x < fromIntegral x') $ do- throwRefineOtherException (typeOf p) ( "Value is not less than " <> PP.pretty x' )-------------------------------------------------------------------------------------- | 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-data GreaterThan (n :: Nat) = GreaterThan- deriving (Generic)--instance (Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x where- validate p x = do- let x' = natVal p- unless (x > fromIntegral x') $ do- throwRefineOtherException (typeOf p) ( "Value is not greater than " <> PP.pretty x' )-------------------------------------------------------------------------------------- | 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-data From (n :: Nat) = From- deriving (Generic)--instance (Ord x, Num x, KnownNat n) => Predicate (From n) x where- validate p x = do- let x' = natVal p- unless (x >= fromIntegral x') $ do- throwRefineOtherException (typeOf p) ( "Value is less than " <> PP.pretty x' )-------------------------------------------------------------------------------------- | 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-data To (n :: Nat) = To- deriving (Generic)--instance (Ord x, Num x, KnownNat n) => Predicate (To n) x where- validate p x = do- let x' = natVal p- unless (x <= fromIntegral x') $ do- throwRefineOtherException (typeOf p) ( "Value is greater than " <> PP.pretty x' )-------------------------------------------------------------------------------------- | 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-data FromTo (mn :: Nat) (mx :: Nat) = FromTo- deriving (Generic)--instance ( Ord x, Num x, KnownNat mn, KnownNat mx, mn <= mx- ) => Predicate (FromTo mn mx) x where- validate p x = do- let mn' = natVal (Proxy @mn)- let mx' = natVal (Proxy @mx)- unless ((x >= fromIntegral mn') && (x <= fromIntegral mx')) $ do- let msg = [ "Value is out of range (minimum: "- , PP.pretty mn'- , ", maximum: "- , PP.pretty mx'- , ")"- ] |> mconcat- throwRefineOtherException (typeOf 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-data EqualTo (n :: Nat) = EqualTo- deriving (Generic)--instance (Eq x, Num x, KnownNat n) => Predicate (EqualTo n) x where- validate p x = do- let x' = natVal p- unless (x == fromIntegral x') $ do- throwRefineOtherException (typeOf p) ("Value does not equal " <> PP.pretty x')-------------------------------------------------------------------------------------- | 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--data NotEqualTo (n :: Nat) = NotEqualTo- deriving (Generic)--instance (Eq x, Num x, KnownNat n) => Predicate (NotEqualTo n) x where- validate p x = do- let x' = natVal p- unless (x /= fromIntegral x') $ do- throwRefineOtherException (typeOf p) ( "Value does equal " <> PP.pretty x' )-------------------------------------------------------------------------------------- | 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-data NegativeFromTo (n :: Nat) (m :: Nat) = NegativeFromTo- deriving (Generic)--instance (Ord x, Num x, KnownNat n, KnownNat m) => Predicate (NegativeFromTo n m) x where- validate p x = do- let n' = natVal (Proxy @n)- m' = natVal (Proxy @m)- unless (x >= negate (fromIntegral n') && x <= fromIntegral m') $ do- let msg = [ "Value is out of range (minimum: "- , PP.pretty (negate n')- , ", maximum: "- , PP.pretty m'- , ")"- ] |> mconcat- throwRefineOtherException (typeOf 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-data DivisibleBy (n :: Nat) = DivisibleBy- deriving (Generic)--instance (Integral x, KnownNat n) => Predicate (DivisibleBy n) x where- validate p x = unless (x `mod` (fromIntegral $ natVal p) == 0) $ do- throwRefineOtherException (typeOf p) $ "Value is not divisible by " <> PP.pretty (natVal p)-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the value is odd.------ >>> isRight (refine @Odd @Int 33)--- True------ >>> isLeft (refine @Odd @Int 32)--- True-data Odd = Odd- deriving (Generic)--instance (Integral x) => Predicate Odd x where- validate p x = unless (odd x) $ do- throwRefineOtherException (typeOf p) $ "Value is not odd."-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the value is even.------ >>> isRight (refine @Even @Int 32)--- True------ >>> isLeft (refine @Even @Int 33)--- True-data Even = Even- deriving (Generic)--instance (Integral x) => Predicate Even x where- validate p x = unless (even x) $ do- throwRefineOtherException (typeOf p) $ "Value is not even."-------------------------------------------------------------------------------------- | A 'Predicate' ensuring that the value is greater than zero.-type Positive = GreaterThan 0---- | A 'Predicate' ensuring that the value is less than or equal to zero.-type NonPositive = To 0---- | A 'Predicate' ensuring that the value is less than zero.-type Negative = LessThan 0---- | A 'Predicate' ensuring that the value is greater than or equal to zero.-type NonNegative = From 0---- | An inclusive range of values from zero to one.-type ZeroToOne = FromTo 0 1---- | A 'Predicate' ensuring that the value is not equal to zero.-type NonZero = NotEqualTo 0---- | A 'Predicate' ensuring that the 'Foldable' is non-empty.-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 guarunteed to satisy 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.-class Weaken from to where- weaken :: Refined from x -> Refined to x- weaken = coerce--instance (n <= m) => Weaken (LessThan n) (LessThan m)-instance (n <= m) => Weaken (LessThan n) (To m)-instance (n <= m) => Weaken (To n) (To m)-instance (m <= n) => Weaken (GreaterThan n) (GreaterThan m)-instance (m <= n) => Weaken (GreaterThan n) (From m)-instance (m <= n) => Weaken (From n) (From m)-instance (p <= n, m <= q) => Weaken (FromTo n m) (FromTo p q)-instance (p <= n) => Weaken (FromTo n m) (From p)-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--- @-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--- @-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)--- @-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)--- @-rightOr :: Refined r x -> Refined (Or l r) x-rightOr = coerce---- | Strengthen a refinement by composing it with another.-strengthen :: forall p p' x. (Predicate p x, Predicate p' x)- => Refined p x- -> Either RefineException (Refined (p && p') x)-strengthen r = refine @(p && p') (unrefine r)-{-# inlineable strengthen #-}---- | Strengthen a refinement by composing it with another--- inside of the 'RefineT' monad.-strengthenM :: forall p p' x m. (Predicate p x, Predicate p' x, Monad m)- => Refined p x- -> RefineT m (Refined (p && p') x)-strengthenM r = exceptRefine (strengthen r)-------------------------------------------------------------------------------------- | An exception encoding the way in which a 'Predicate' failed.-data RefineException- = -- | A 'RefineException' for failures involving the 'Not' predicate.- RefineNotException- { _RefineException_typeRep :: !TypeRep- -- ^ The 'TypeRep' of the @'Not' p@ type.- }-- | -- | A 'RefineException' for failures involving the 'And' predicate.- 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.- 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 all other predicates.- RefineOtherException- { _RefineException_typeRep :: !TypeRep- -- ^ The 'TypeRep' of the predicate that failed.- , _RefineException_message :: !(PP.Doc Void)- -- ^ A custom message to display.- }- deriving (Generic)--instance Show RefineException where- show = PP.pretty .> show--twoSpaces, newline :: PP.Doc ann-{-# INLINE twoSpaces #-}-{-# INLINE newline #-}-twoSpaces = " "-newline = "\n"---- | Display a 'RefineException' as a @'PP.Doc' ann@-displayRefineException :: RefineException -> PP.Doc ann-displayRefineException = \case- RefineOtherException tr msg ->- [ "The predicate ("- , PP.pretty (show tr)- , ") does not hold: "- , newline- , twoSpaces- , PP.pretty (show msg)- ] |> mconcat- RefineNotException tr ->- [ "The negation of the predicate ("- , PP.pretty (show tr)- , ") does not hold:"- , newline- , twoSpaces- ] |> mconcat- RefineOrException tr orLChild orRChild ->- [ "Both subpredicates failed in: ("- , PP.pretty (show tr)- , "):"- , newline- , twoSpaces- , displayRefineException orLChild- , newline- , twoSpaces- , displayRefineException orRChild- , newline- , twoSpaces- ] |> mconcat- RefineAndException tr andChild ->- (- [ "The predicate ("- , PP.pretty (show tr)- , ") does not hold:"- , newline- , twoSpaces- ] |> mconcat- )- <> case andChild of- This a -> mconcat [ "The left subpredicate does not hold:", newline, twoSpaces, displayRefineException a, newline ]- That b -> mconcat [ "The right subpredicate does not hold:", newline, twoSpaces, displayRefineException b, newline ]- These a b -> mconcat [ twoSpaces, "Neither subpredicate holds: ", newline- , twoSpaces, displayRefineException a, newline- , twoSpaces, displayRefineException b, newline- ]---- | Pretty-print a 'RefineException'.-instance PP.Pretty RefineException where- pretty = displayRefineException---- | Encode a 'RefineException' for use with \Control.Exception\.-instance Exception RefineException where- displayException = show-------------------------------------------------------------------------------------- | A monad transformer that adds @'RefineException'@s to other monads.------ The @'pure'@ and @'Control.Monad.return'@ functions yield computations that produce--- the given value, while @'>>='@ sequences two subcomputations, exiting--- on the first @'RefineException'@.-newtype RefineT m a- = RefineT (ExceptT RefineException m a)- deriving ( Functor, Applicative, Monad, MonadFix- , MonadError RefineException, MonadTrans- , Generic, Generic1- )---- | The inverse of @'RefineT'@.-runRefineT- :: RefineT m a- -> m (Either RefineException a)-runRefineT = coerce .> ExceptT.runExceptT---- | Map the unwrapped computation using the given function.------ @'runRefineT' ('mapRefineT' f m) = f ('runRefineT' m)@-mapRefineT- :: (m (Either RefineException a) -> n (Either RefineException b))- -> RefineT m a- -> RefineT n b-mapRefineT f = coerce .> ExceptT.mapExceptT f .> coerce-------------------------------------------------------------------------------------- | @'RefineM' a@ is equivalent to @'RefineT' 'Identity' a@ for any type @a@.-type RefineM a = RefineT Identity a---- | Constructs a computation in the 'RefineM' monad. (The inverse of @'runRefineM'@).-refineM- :: Either RefineException a- -> RefineM a-refineM = ExceptT.except .> (coerce :: ExceptT RefineException Identity a -> RefineM a)---- | Run a monadic action of type @'RefineM' a@,--- yielding an @'Either' 'RefineException' a@.------ This is just defined as @'runIdentity' '.' 'runRefineT'@.-runRefineM- :: RefineM a- -> Either RefineException a-runRefineM = runRefineT .> runIdentity-------------------------------------------------------------------------------------- | Constructor for computations in the @'RefineT'@ movie.--- (The inverse of 'runRefineT').-exceptRefine- :: (Monad m)- => Either RefineException a- -> RefineT m a-exceptRefine = MonadError.liftEither---- | One can use @'throwRefine'@ inside of a monadic--- context to begin processing a @'RefineException'@.-throwRefine- :: (Monad m)- => RefineException- -> RefineT m a-throwRefine = MonadError.throwError---- | A handler function to handle previous @'RefineException'@s--- and return to normal execution. A common idiom is:------ @ do { action1; action2; action3 } `'catchRefine'` handler @------ where the action functions can call @'throwRefine'@. Note that--- handler and the do-block must have the same return type.-catchRefine- :: (Monad m)- => RefineT m a- -> (RefineException -> RefineT m a)- -> RefineT m a-catchRefine = MonadError.catchError---- | A handler for a @'RefineException'@.------ 'throwRefineOtherException' is useful for defining what--- behaviour 'validate' should have in the event of a predicate failure.-throwRefineOtherException- :: (Monad m)- => TypeRep- -- ^ The 'TypeRep' of the 'Predicate'. This can usually be given by using 'typeOf'.- -> PP.Doc Void- -- ^ A 'PP.Doc' 'Void' encoding a custom error message to be pretty-printed.- -> RefineT m a-throwRefineOtherException rep- = RefineOtherException rep .> throwRefine----------------------------------------------------------------------------------
− src/Refined/Orphan.hs
@@ -1,44 +0,0 @@------------------------------------------------------------------------------------- Copyright © 2015 Nikita Volkov--- Copyright © 2018 Remy Goldschmidt--- Copyright © 2019 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 #-}-------------------------------------------------------------------------------------- | This module exposes orphan instances for the 'Refined' type.--- This is unavoidable given the current module structure.-module Refined.Orphan () where------------------------------------------------------------------------------------import Refined.Orphan.Aeson ()-import Refined.Orphan.QuickCheck ()-----------------------------------------------------------------------------------
− src/Refined/Orphan/Aeson.hs
@@ -1,56 +0,0 @@------------------------------------------------------------------------------------- Copyright © 2015 Nikita Volkov--- Copyright © 2018 Remy Goldschmidt--- Copyright © 2019 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 #-}-------------------------------------------------------------------------------------- | This module exposes orphan instances for the 'Refined' type.--- This is unavoidable given the current module structure.-module Refined.Orphan.Aeson () where------------------------------------------------------------------------------------#if HAVE_AESON--import Control.Monad ((<=<))-import Data.Aeson (FromJSON(parseJSON), ToJSON(toJSON))-import Refined.Internal (Refined, Predicate, refineFail, unrefine)------------------------------------------------------------------------------------instance (FromJSON a, Predicate p a) => FromJSON (Refined p a) where- parseJSON = refineFail <=< parseJSON--instance (ToJSON a, Predicate p a) => ToJSON (Refined p a) where- toJSON = toJSON . unrefine------------------------------------------------------------------------------------#endif
− src/Refined/Orphan/QuickCheck.hs
@@ -1,91 +0,0 @@------------------------------------------------------------------------------------- Copyright © 2015 Nikita Volkov--- Copyright © 2018 Remy Goldschmidt--- Copyright © 2019 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 AllowAmbiguousTypes #-}-{-# LANGUAGE CPP #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}-------------------------------------------------------------------------------------- | This module exposes orphan instances for the 'Refined' type.--- This is unavoidable given the current module structure.-module Refined.Orphan.QuickCheck () where------------------------------------------------------------------------------------#if HAVE_QUICKCHECK--import Data.Either (isRight)-import Refined.Internal (Refined, RefineException, Predicate, refine, reifyPredicate)-import Refined.Unsafe (reallyUnsafeRefine)-import Test.QuickCheck (Arbitrary(arbitrary), suchThatMaybe, Gen, sized, resize)-import Data.Typeable (Typeable, showsTypeRep, typeRep)-import Data.Proxy (Proxy(Proxy))------------------------------------------------------------------------------------instance forall p a. (Arbitrary a, Typeable a, Typeable p, Predicate p a) => Arbitrary (Refined p a) where- arbitrary = loop 0 arbitrary--loop :: forall p a. (Typeable p, Typeable a, Predicate p a)- => 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))--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 <- suchThatMaybe gen (reifyPredicate @p @a)- case m of- Nothing -> pure Nothing- Just x -> pure (Just (reallyUnsafeRefine x))--typeName :: Typeable a => Proxy a -> String-typeName = flip showsTypeRep "" . typeRep------------------------------------------------------------------------------------#endif
− src/Refined/These.hs
@@ -1,265 +0,0 @@------------------------------------------------------------------------------------- Copyright © 2015 Nikita Volkov--- Copyright © 2018 Remy Goldschmidt--- Copyright © 2019 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 #-}------------------------------------------------------------------------------------{-# LANGUAGE CPP #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE InstanceSigs #-}-------------------------------------------------------------------------------------- | This module is defined internally to avoid using the 'these'--- package, which brings in a lot of very heavy and unnecessary--- transitive dependencies. We export the type and constructors--- here, in case a user should need it.--- We provide a small API for working with the 'These' type here.--- If one should need a fuller API, see https://hackage.haskell.org/package/these--- Converting to/from the two types should be trivial, as the--- data constructors are exported from both.-module Refined.These- (- -- * 'These' type- These(This, That, These)-- -- * Consumption- , these- , fromThese- , mergeThese- , mergeTheseWith-- -- * Traversals- , here, there-- -- * Case selections- , justThis- , justThat- , justThese-- , catThis- , catThat- , catThese-- , partitionThese-- -- * Case predicates- , isThis- , isThat- , isThese-- -- * Map operations- , mapThese- , mapThis- , mapThat- ) where------------------------------------------------------------------------------------import Control.DeepSeq (NFData(rnf))-#if MIN_VERSION_base(4,10,0)-import Data.Bifoldable (Bifoldable(bifold, bifoldr, bifoldl))-#endif-#if MIN_VERSION_base(4,8,0)-import Data.Bifunctor (Bifunctor(bimap, first, second))-#endif-import Data.Data (Data)-import Data.Maybe (isJust, mapMaybe)-import Data.Semigroup (Semigroup((<>)))-import Data.Typeable (Typeable)-import GHC.Generics (Generic, Generic1)---- | This is defined internally to avoid using the 'these'--- package, which brings in a lot of very heavy and unnecessary--- transitive dependencies. We export the type and constructors--- here, in case a user should need it.-data These a b = This a | That b | These a b- deriving (Eq, Ord, Read, Show, Typeable, Data, Generic, Generic1)---- | Case analysis for the 'These' type.-these :: (a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c-these l _ _ (This a) = l a-these _ r _ (That x) = r x-these _ _ lr (These a x) = lr a x---- | Takes two default values and produces a tuple.-fromThese :: a -> b -> These a b -> (a, b)-fromThese _ x (This a ) = (a, x)-fromThese a _ (That x ) = (a, x)-fromThese _ _ (These a x) = (a, x)---- | Coalesce with the provided operation.-mergeThese :: (a -> a -> a) -> These a a -> a-mergeThese = these id id---- | BiMap and coalesce results with the provided operation.-mergeTheseWith :: (a -> c) -> (b -> c) -> (c -> c -> c) -> These a b -> c-mergeTheseWith f g op t = mergeThese op $ mapThese f g t---- | A @Traversal@ of the first half of a 'These', suitable for use with @Control.Lens@.-here :: (Applicative f) => (a -> f b) -> These a t -> f (These b t)-here f (This x) = This <$> f x-here f (These x y) = flip These y <$> f x-here _ (That x) = pure (That x)---- | A @Traversal@ of the second half of a 'These', suitable for use with @Control.Lens@.-there :: (Applicative f) => (a -> f b) -> These t a -> f (These t b)-there _ (This x) = pure (This x)-there f (These x y) = These x <$> f y-there f (That x) = That <$> f x---- | @'justThis' = 'these' 'Just' (\_ -> 'Nothing') (\_ _ -> 'Nothing')@-justThis :: These a b -> Maybe a-justThis = these Just (\_ -> Nothing) (\_ _ -> Nothing)---- | @'justThat' = 'these' (\_ -> 'Nothing') 'Just' (\_ _ -> 'Nothing')@-justThat :: These a b -> Maybe b-justThat = these (\_ -> Nothing) Just (\_ _ -> Nothing)---- | @'justThese' = 'these' (\_ -> 'Nothing') (\_ -> 'Nothing') (\a b -> 'Just' (a, b))@-justThese :: These a b -> Maybe (a, b)-justThese = these (\_ -> Nothing) (\_ -> Nothing) (\a b -> Just (a, b))--isThis, isThat, isThese :: These a b -> Bool--- | @'isThis' = 'isJust' . 'justThis'@-isThis = isJust . justThis---- | @'isThat' = 'isJust' . 'justThat'@-isThat = isJust . justThat---- | @'isThese' = 'isJust' . 'justThese'@-isThese = isJust . justThese---- | 'Bifunctor' map.-mapThese :: (a -> c) -> (b -> d) -> These a b -> These c d-mapThese f _ (This a ) = This (f a)-mapThese _ g (That x) = That (g x)-mapThese f g (These a x) = These (f a) (g x)---- | @'mapThis' = over 'here'@-mapThis :: (a -> c) -> These a b -> These c b-mapThis f = mapThese f id---- | @'mapThat' = over 'there'@-mapThat :: (b -> d) -> These a b -> These a d-mapThat f = mapThese id f---- | Select all 'This' constructors from a list.-catThis :: [These a b] -> [a]-catThis = mapMaybe justThis---- | Select all 'That' constructors from a list.-catThat :: [These a b] -> [b]-catThat = mapMaybe justThat---- | Select all 'These' constructors from a list.-catThese :: [These a b] -> [(a, b)]-catThese = mapMaybe justThese---- | Select each constructor and partition them into separate lists.-partitionThese :: [These a b] -> ( [(a, b)], ([a], [b]) )-partitionThese [] = ([], ([], []))-partitionThese (These x y:xs) = first ((x, y):) $ partitionThese xs-partitionThese (This x :xs) = second (first (x:)) $ partitionThese xs-partitionThese (That y:xs) = second (second (y:)) $ partitionThese xs--instance (Semigroup a, Semigroup b) => Semigroup (These a b) where- This a <> This b = This (a <> b)- This a <> That y = These a y- This a <> These b y = These (a <> b) y- That x <> This b = These b x- That x <> That y = That (x <> y)- That x <> These b y = These b (x <> y)- These a x <> This b = These (a <> b) x- These a x <> That y = These a (x <> y)- These a x <> These b y = These (a <> b) (x <> y)--#if MIN_VERSION_base(4,8,0)-instance Bifunctor These where- bimap :: (a -> c) -> (b -> d) -> These a b -> These c d- bimap f _ (This a ) = This (f a)- bimap _ g (That b) = That (g b)- bimap f g (These a b) = These (f a) (g b)- first :: (a -> c) -> These a b -> These c b- first f = bimap f id- second :: (b -> d) -> These a b -> These a d- second f = bimap id f-#endif--instance Functor (These a) where- fmap _ (This x) = This x- fmap f (That y) = That (f y)- fmap f (These x y) = These x (f y)--instance Semigroup a => Applicative (These a) where- pure = That- This a <*> _ = This a- That _ <*> This b = This b- That f <*> That x = That (f x)- That f <*> These b x = These b (f x)- These a _ <*> This b = This (a <> b)- These a f <*> That x = These a (f x)- These a f <*> These b x = These (a <> b) (f x)--instance Semigroup a => Monad (These a) where- return = pure- This a >>= _ = This a- That x >>= k = k x- These a x >>= k = case k x of- This b -> This (a <> b)- That y -> These a y- These b y -> These (a <> b) y--instance (NFData a, NFData b) => NFData (These a b) where- rnf (This a) = rnf a- rnf (That b) = rnf b- rnf (These a b) = rnf a `seq` rnf b--instance Foldable (These a) where- foldr _ z (This _) = z- foldr f z (That x) = f x z- foldr f z (These _ x) = f x z--instance Traversable (These a) where- traverse _ (This a ) = pure $ This a- traverse f (That x) = That <$> f x- traverse f (These a x) = These a <$> f x- sequenceA (This a ) = pure $ This a- sequenceA (That x) = That <$> x- sequenceA (These a x) = These a <$> x--#if MIN_VERSION_base(4,10,0)-instance Bifoldable These where- bifold = these id id mappend- bifoldr f g z = these (`f` z) (`g` z) (\x y -> x `f` (y `g` z))- bifoldl f g z = these (z `f`) (z `g`) (\x y -> (z `f` x) `g` y)-#endif-
src/Refined/Unsafe.hs view
@@ -2,7 +2,7 @@ -- Copyright © 2015 Nikita Volkov -- Copyright © 2018 Remy Goldschmidt--- Copyright © 2019 chessai+-- Copyright © 2020 chessai -- -- Permission is hereby granted, free of charge, to any person -- obtaining a copy of this software and associated documentation@@ -28,6 +28,8 @@ -------------------------------------------------------------------------------- {-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE PolyKinds #-} #if __GLASGOW_HASKELL__ >= 805 {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-}@@ -59,14 +61,11 @@ -------------------------------------------------------------------------------- -import Control.Exception (Exception(displayException))+import Control.Exception (displayException) import Data.Coerce (coerce)-import Data.Either (either)-import Data.Function (id) -import GHC.Err (error)--import Refined.Internal (Refined(Refined), Predicate, refine, (.>))+import Refined (Predicate, refine)+import Refined.Unsafe.Type (Refined(Refined)) import Data.Type.Coercion (Coercion (..)) #if __GLASGOW_HASKELL__ >= 805 import Data.Coerce (Coercible)@@ -79,25 +78,34 @@ -- 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 = refine .> either (displayException .> error) id+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.+-- 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.+-- | 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 =@@ -113,6 +121,8 @@ -- 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
src/Refined/Unsafe/Type.hs view
@@ -2,7 +2,7 @@ -- Copyright © 2015 Nikita Volkov -- Copyright © 2018 Remy Goldschmidt--- Copyright © 2019 chessai+-- Copyright © 2020 chessai -- -- Permission is hereby granted, free of charge, to any person -- obtaining a copy of this software and associated documentation@@ -27,12 +27,18 @@ -------------------------------------------------------------------------------- -{-# OPTIONS_GHC -Wall #-}+{-# 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 'Coercible'+-- 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@@ -42,4 +48,34 @@ ( Refined(Refined) ) where -import Refined.Internal (Refined(Refined))+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,5 +1,6 @@ {-# language AllowAmbiguousTypes+ , DataKinds , FlexibleInstances , MultiParamTypeClasses , OverloadedStrings@@ -10,17 +11,48 @@ module Main (main) where import Refined-import Prelude (IO,putStrLn,Int) import Data.Void (Void) -main :: IO ()-main = do- putStrLn "refined/test/Compiles.hs: it compiles!"--id = $$(refineTH @IdPred @Int 3)-even = $$(refineTH @(Not Even) @Int 3)-odd = $$(refineTH @Odd @Int 3)- 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/Doctests.hs
@@ -1,23 +0,0 @@-module Main (main) where--import Test.DocTest--main :: IO ()-main = doctest $ srcFiles ++ compFlags--srcFiles :: [String]-srcFiles =- [ "src/Refined.hs"- , "src/Refined/Internal.hs"- , "src/Refined/Orphan/Aeson.hs"- , "src/Refined/Orphan/QuickCheck.hs"- , "src/Refined/Orphan.hs"- , "src/Refined/These.hs"- , "src/Refined/Unsafe/Type.hs"- , "src/Refined/Unsafe.hs"- ]--compFlags :: [String]-compFlags =- [ "-XScopedTypeVariables"- ]
test/QuickCheck.hs view
@@ -11,7 +11,6 @@ import Test.QuickCheck import Refined-import Refined.Orphan main :: IO () main = mapM_ quickCheck@@ -20,6 +19,8 @@ , prop_from , prop_to , prop_bad+ , prop_shrink_lt+ , prop_shrink_gt ] iddy :: (Eq a) => Refined p a -> Bool@@ -38,10 +39,25 @@ prop_to = property $ \(r :: Refined (To 9) MyInt) -> iddy r prop_bad :: Property-prop_bad = expectFailure $ \(r :: Refined (EqualTo 2 && EqualTo 3) MyInt) -> iddy r+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]