refined 0.4.1 → 0.4.2
raw patch · 18 files changed
+1866/−1388 lines, 18 filesdep +doctestdep +refineddep −thesedep ~aesondep ~basedep ~deepseq
Dependencies added: doctest, refined
Dependencies removed: these
Dependency ranges changed: aeson, base, deepseq, exceptions, mtl, prettyprinter, template-haskell, transformers
Files
- LICENSE +1/−1
- library/Refined.hs +0/−139
- library/Refined/Internal.hs +0/−909
- library/Refined/Orphan.hs +0/−44
- library/Refined/Orphan/Aeson.hs +0/−56
- library/Refined/Orphan/QuickCheck.hs +0/−54
- library/Refined/Unsafe.hs +0/−122
- library/Refined/Unsafe/Type.hs +0/−45
- refined.cabal +27/−18
- src/Refined.hs +139/−0
- src/Refined/Internal.hs +1090/−0
- src/Refined/Orphan.hs +44/−0
- src/Refined/Orphan/Aeson.hs +56/−0
- src/Refined/Orphan/QuickCheck.hs +54/−0
- src/Refined/These.hs +265/−0
- src/Refined/Unsafe.hs +122/−0
- src/Refined/Unsafe/Type.hs +45/−0
- test/Doctests.hs +23/−0
LICENSE view
@@ -1,6 +1,6 @@ Copyright © 2015 Nikita Volkov Copyright © 2018 Remy Goldschmidt-Copyright © 2018 Daniel Cartwright+Copyright © 2019 chessai Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation
− library/Refined.hs
@@ -1,139 +0,0 @@------------------------------------------------------------------------------------- Copyright © 2015 Nikita Volkov--- Copyright © 2018 Remy Goldschmidt--- Copyright © 2018 Daniel Cartwright------ 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- , refineThrow- , refineFail- , refineError- , refineTH-- -- ** Consumption- , unrefine-- -- * 'Predicate'- , Predicate (validate)-- -- * Logical predicates- , Not- , And- , type (&&)- , Or- , type (||)-- -- * Identity predicate- , IdPred-- -- * Numeric predicates- , LessThan- , GreaterThan- , From- , To- , FromTo- , EqualTo- , NotEqualTo - , Positive- , NonPositive- , Negative- , NonNegative- , ZeroToOne- , NonZero-- -- * Foldable predicates- , SizeLessThan- , SizeGreaterThan- , SizeEqualTo- , NonEmpty-- -- * IsList predicates- , Ascending- , Descending-- -- * Weakening- , Weaken (weaken)- , andLeft- , andRight- , leftOr- , rightOr-- -- * Error handling-- -- ** 'RefineException'- , RefineException- ( RefineNotException- , RefineAndException- , RefineOrException- , RefineOtherException- )- , displayRefineException-- -- ** 'RefineT' and 'RefineM'- , RefineT, runRefineT, mapRefineT- , RefineM, refineM, runRefineM- , throwRefine, catchRefine- , throwRefineOtherException-- -- * Re-Exports- , pretty- ) where------------------------------------------------------------------------------------import Refined.Internal---------------------------------------------------------------------------------
− library/Refined/Internal.hs
@@ -1,909 +0,0 @@------------------------------------------------------------------------------------- Copyright © 2015 Nikita Volkov--- Copyright © 2018 Remy Goldschmidt--- Copyright © 2018 Daniel Cartwright------ 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 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 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- , refineThrow- , refineFail- , refineError- , refineTH-- -- ** Consumption- , unrefine-- -- * 'Predicate'- , Predicate (validate)-- -- * Logical predicates- , Not- , And- , type (&&)- , Or- , type (||)-- -- * Identity predicate- , IdPred-- -- * Numeric predicates- , LessThan- , GreaterThan- , From- , To- , FromTo- , EqualTo- , NotEqualTo - , Positive- , NonPositive- , Negative- , NonNegative- , ZeroToOne- , NonZero- , NegativeFromTo-- -- * Foldable predicates- , SizeLessThan- , SizeGreaterThan- , SizeEqualTo- , NonEmpty-- -- * IsList predicates- , Ascending- , Descending-- -- * Weakening- , Weaken (weaken)- , andLeft- , andRight- , leftOr- , rightOr-- -- * Error handling-- -- ** 'RefineException'- , RefineException- ( RefineNotException- , RefineAndException- , RefineOrException- , RefineOtherException- )- , displayRefineException-- -- ** 'RefineT' and 'RefineM'- , RefineT, runRefineT, 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 Data.These (These(This,That,These))--import qualified Data.Text.Prettyprint.Doc as PP-import qualified Language.Haskell.TH.Syntax as TH------------------------------------------------------------------------------------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 #-}---- | 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-------------------------------------------------------------------------------------- | 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 ()-------------------------------------------------------------------------------------- | A predicate which is satisfied for all types.-data IdPred- deriving (Generic)--instance Predicate IdPred x where- validate _ _ = pure ()- {-# INLINE validate #-}-------------------------------------------------------------------------------------- | The negation of a predicate.-data Not p- 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.-data And l r- 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.-data Or l r- 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.-data SizeLessThan (n :: Nat)- 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.-data SizeGreaterThan (n :: Nat)- 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.-data SizeEqualTo (n :: Nat)- 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.-data 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.-data 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.-data LessThan (n :: Nat)- 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.-data GreaterThan (n :: Nat)- 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.-data From (n :: Nat)- 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.-data To (n :: Nat)- 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.-data FromTo (mn :: Nat) (mx :: Nat)- 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@.-data EqualTo (n :: Nat)- 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@.-data NotEqualTo (n :: Nat)- 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@.-data NegativeFromTo (n :: Nat) (m :: Nat)- deriving (Generic)--instance (Ord x, Num x, KnownNat n, KnownNat m, n <= 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 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-------------------------------------------------------------------------------------- | 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-------------------------------------------------------------------------------------- | 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----------------------------------------------------------------------------------
− library/Refined/Orphan.hs
@@ -1,44 +0,0 @@------------------------------------------------------------------------------------- Copyright © 2015 Nikita Volkov--- Copyright © 2018 Remy Goldschmidt--- Copyright © 2018 Daniel Cartwright------ 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 ()-----------------------------------------------------------------------------------
− library/Refined/Orphan/Aeson.hs
@@ -1,56 +0,0 @@------------------------------------------------------------------------------------- Copyright © 2015 Nikita Volkov--- Copyright © 2018 Remy Goldschmidt--- Copyright © 2018 Daniel Cartwright------ 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
− library/Refined/Orphan/QuickCheck.hs
@@ -1,54 +0,0 @@------------------------------------------------------------------------------------- Copyright © 2015 Nikita Volkov--- Copyright © 2018 Remy Goldschmidt--- Copyright © 2018 Daniel Cartwright------ Permission is hereby granted, free of charge, to any person--- obtaining a copy of this software and associated documentation--- files (the "Software"), to deal in the Software without--- restriction, including without limitation the rights to use,--- copy, modify, merge, publish, distribute, sublicense, and/or sell--- copies of the Software, and to permit persons to whom the--- Software is furnished to do so, subject to the following--- conditions:------ The above copyright notice and this permission notice shall be--- included in all copies or substantial portions of the Software.------ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,--- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES--- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND--- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT--- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,--- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING--- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR--- OTHER DEALINGS IN THE SOFTWARE.------------------------------------------------------------------------------------{-# LANGUAGE CPP #-}-{-# LANGUAGE ScopedTypeVariables #-}-------------------------------------------------------------------------------------- | 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(Refined), RefineException, Predicate, refine)-import Test.QuickCheck (Arbitrary(arbitrary), suchThat, Gen)------------------------------------------------------------------------------------instance forall p a. (Arbitrary a, Predicate p a) => Arbitrary (Refined p a) where- arbitrary = Refined <$> suchThat (arbitrary :: Gen a) (isRight . (refine :: a -> Either RefineException (Refined p a)))------------------------------------------------------------------------------------#endif
− library/Refined/Unsafe.hs
@@ -1,122 +0,0 @@------------------------------------------------------------------------------------- Copyright © 2015 Nikita Volkov--- Copyright © 2018 Remy Goldschmidt--- Copyright © 2018 Daniel Cartwright------ 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 #-}-#if __GLASGOW_HASKELL__ >= 805-{-# LANGUAGE QuantifiedConstraints #-}-{-# LANGUAGE RankNTypes #-}-#endif-{-# OPTIONS_GHC -Wall #-}-------------------------------------------------------------------------------------- | This module exposes /unsafe/ refinements. An /unsafe/ refinement--- is one which either does not make the guarantee of totality in construction--- of the 'Refined' value or does not perform a check of the refinement--- predicate. It is recommended only to use this when you can manually prove--- that the refinement predicate holds.-module Refined.Unsafe- ( -- * 'Refined'- Refined-- -- ** Creation- , reallyUnsafeRefine - , unsafeRefine-- -- ** Coercion- , reallyUnsafeUnderlyingRefined-#if __GLASGOW_HASKELL__ >= 805- , reallyUnsafeAllUnderlyingRefined-#endif- , reallyUnsafePredEquiv- ) where------------------------------------------------------------------------------------import Control.Exception (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 Data.Type.Coercion (Coercion (..))-#if __GLASGOW_HASKELL__ >= 805-import Data.Coerce (Coercible)-#endif-------------------------------------------------------------------------------------- | Constructs a 'Refined' value at run-time,--- calling 'Prelude.error' if the value--- does not satisfy the predicate.------ WARNING: this function is not total!-unsafeRefine :: (Predicate p x) => x -> Refined p x-unsafeRefine = refine .> either (displayException .> error) id-{-# INLINABLE unsafeRefine #-}---- | Constructs a 'Refined' value, completely--- ignoring any refinements! Use this only--- when you can manually prove that the refinement--- holds.-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.-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.-reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x)-reallyUnsafePredEquiv = Coercion--- Note: reallyUnsafePredEquiv =--- sym 'reallyUnsafeUnderlyingRefined' `trans` 'reallyUnsafeUnderlyingRefined'--#if __GLASGOW_HASKELL__ >= 805--- | Reveal that @x@ and @'Refined' p x@ are 'Coercible' for--- /all/ @x@ and @p@ simultaneously.------ === Example------ @--- reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x)--- reallyUnsafePredEquiv = reallyUnsafeAllUnderlyingRefined Coercion--- @-reallyUnsafeAllUnderlyingRefined- :: ((forall x y p. (Coercible x y => Coercible y (Refined p x))) => r) -> r--- Why is this constraint so convoluted? Because otherwise the constraint--- solver doesn't handle transitivity properly. See "Safe Zero-cost Coercions--- for Haskell" by Breitner et al.-reallyUnsafeAllUnderlyingRefined r = r-#endif
− library/Refined/Unsafe/Type.hs
@@ -1,45 +0,0 @@------------------------------------------------------------------------------------- Copyright © 2015 Nikita Volkov--- Copyright © 2018 Remy Goldschmidt--- Copyright © 2018 Daniel Cartwright------ 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 #-}-------------------------------------------------------------------------------------- | This module exports the 'Refined' type with its--- constructor. This is very risky! In particular, the 'Coercible'--- instances will be visible throughout the importing module.--- It is usually better to build the necessary coercions locally--- using the utilities in "Refined.Unsafe", but in some cases--- it may be more convenient to write a separate module that--- imports this one and exports some large coercion.-module Refined.Unsafe.Type- ( Refined(Refined)- ) where--import Refined.Internal (Refined(Refined))
refined.cabal view
@@ -3,27 +3,26 @@ name: refined version:- 0.4.1+ 0.4.2 synopsis: Refinement types with static and runtime checking description:- For an extensive introduction to the library please follow to + For an extensive introduction to the library please follow to <http://nikita-volkov.github.io/refined this blog-post>. category: Data homepage: https://github.com/nikita-volkov/refined bug-reports:- https://github.com/nikita-volkov/refined/issues + https://github.com/nikita-volkov/refined/issues author: Nikita Volkov <nikita.y.volkov@mail.ru> maintainer:- chessai <chessai1996@gmail.com> + chessai <chessai1996@gmail.com> copyright: Copyright © 2015, Nikita Volkov Copyright © 2018, Remy Goldschmidt- Copyright © 2018, Daniel Cartwright- + Copyright © 2019, chessai license: MIT license-file:@@ -34,7 +33,7 @@ GHC == 8.0.2 , GHC == 8.2.2 , GHC == 8.4.4- , GHC == 8.6.4+ , GHC == 8.6.5 flag aeson description:@@ -60,29 +59,39 @@ library hs-source-dirs:- library+ src exposed-modules: Refined Refined.Internal Refined.Orphan Refined.Orphan.Aeson Refined.Orphan.QuickCheck- Refined.Unsafe + Refined.These+ Refined.Unsafe Refined.Unsafe.Type default-language: Haskell2010 build-depends:- base >= 4.9.1.0 && < 4.13.0.0- , deepseq >= 1.4.0.0 && < 1.5.0.0- , exceptions >= 0.8.0.0 && < 0.11.0- , mtl >= 2.2.1.0 && < 3.0.0.0- , prettyprinter >= 1.1.0.1 && < 1.3.0.0- , template-haskell >= 2.9.0.0 && < 2.15.0.0- , these >= 0.7.0.0 && < 0.8.0.0- , transformers >= 0.5.0.0 && < 0.6.0.0+ 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.15+ , transformers >= 0.5 && < 0.6 if flag(aeson)- build-depends: aeson >= 0.9 && < 1.5.0.0+ build-depends: aeson >= 0.9 && < 1.5 cpp-options: -DHAVE_AESON if flag(QuickCheck) build-depends: QuickCheck >= 2.1 && < 2.13 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
+ src/Refined.hs view
@@ -0,0 +1,139 @@+--------------------------------------------------------------------------------++-- 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+ , refineThrow+ , refineFail+ , refineError+ , refineTH++ -- ** Consumption+ , unrefine++ -- * 'Predicate'+ , Predicate (validate)++ -- * Logical predicates+ , Not+ , And+ , type (&&)+ , Or+ , type (||)++ -- * Identity predicate+ , IdPred++ -- * Numeric predicates+ , LessThan+ , GreaterThan+ , From+ , To+ , FromTo+ , EqualTo+ , NotEqualTo+ , Positive+ , NonPositive+ , Negative+ , NonNegative+ , ZeroToOne+ , NonZero++ -- * Foldable predicates+ , SizeLessThan+ , SizeGreaterThan+ , SizeEqualTo+ , NonEmpty++ -- * IsList predicates+ , Ascending+ , Descending++ -- * Weakening+ , Weaken (weaken)+ , andLeft+ , andRight+ , leftOr+ , rightOr++ -- * Error handling++ -- ** 'RefineException'+ , RefineException+ ( RefineNotException+ , RefineAndException+ , RefineOrException+ , RefineOtherException+ )+ , displayRefineException++ -- ** 'RefineT' and 'RefineM'+ , RefineT, runRefineT, mapRefineT+ , RefineM, refineM, runRefineM+ , throwRefine, catchRefine+ , throwRefineOtherException++ -- * Re-Exports+ , pretty+ ) where++--------------------------------------------------------------------------------++import Refined.Internal++-------------------------------------------------------------------------------
+ src/Refined/Internal.hs view
@@ -0,0 +1,1090 @@+--------------------------------------------------------------------------------++-- 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 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 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+ , refineThrow+ , refineFail+ , refineError+ , refineTH++ -- ** Consumption+ , unrefine++ -- * 'Predicate'+ , Predicate (validate)++ -- * 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++ -- * Error handling++ -- ** 'RefineException'+ , RefineException+ ( RefineNotException+ , RefineAndException+ , RefineOrException+ , RefineOtherException+ )+ , displayRefineException++ -- ** 'RefineT' and 'RefineM'+ , RefineT, runRefineT, 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 #-}++-- | 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++--------------------------------------------------------------------------------++-- | 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 ()++--------------------------------------------------------------------------------++-- | A predicate which is satisfied for all types.+-- The value is not evaluated by 'validate'.+--+-- >>> 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@.+-- That is to say, @m `mod` 'natVal' ('Proxy' @n) '==' 0@+--+-- >>> 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++--------------------------------------------------------------------------------++-- | 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++--------------------------------------------------------------------------------++-- | 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 view
@@ -0,0 +1,44 @@+--------------------------------------------------------------------------------++-- 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 view
@@ -0,0 +1,56 @@+--------------------------------------------------------------------------------++-- 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 view
@@ -0,0 +1,54 @@+--------------------------------------------------------------------------------++-- 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 #-}+{-# LANGUAGE ScopedTypeVariables #-}++--------------------------------------------------------------------------------++-- | 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(Refined), RefineException, Predicate, refine)+import Test.QuickCheck (Arbitrary(arbitrary), suchThat, Gen)++--------------------------------------------------------------------------------++instance forall p a. (Arbitrary a, Predicate p a) => Arbitrary (Refined p a) where+ arbitrary = Refined <$> suchThat (arbitrary :: Gen a) (isRight . (refine :: a -> Either RefineException (Refined p a)))++--------------------------------------------------------------------------------++#endif
+ src/Refined/These.hs view
@@ -0,0 +1,265 @@+--------------------------------------------------------------------------------++-- 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
@@ -0,0 +1,122 @@+--------------------------------------------------------------------------------++-- 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 #-}+#if __GLASGOW_HASKELL__ >= 805+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes #-}+#endif+{-# OPTIONS_GHC -Wall #-}++--------------------------------------------------------------------------------++-- | This module exposes /unsafe/ refinements. An /unsafe/ refinement+-- is one which either does not make the guarantee of totality in construction+-- of the 'Refined' value or does not perform a check of the refinement+-- predicate. It is recommended only to use this when you can manually prove+-- that the refinement predicate holds.+module Refined.Unsafe+ ( -- * 'Refined'+ Refined++ -- ** Creation+ , reallyUnsafeRefine+ , unsafeRefine++ -- ** Coercion+ , reallyUnsafeUnderlyingRefined+#if __GLASGOW_HASKELL__ >= 805+ , reallyUnsafeAllUnderlyingRefined+#endif+ , reallyUnsafePredEquiv+ ) where++--------------------------------------------------------------------------------++import Control.Exception (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 Data.Type.Coercion (Coercion (..))+#if __GLASGOW_HASKELL__ >= 805+import Data.Coerce (Coercible)+#endif++--------------------------------------------------------------------------------++-- | Constructs a 'Refined' value at run-time,+-- calling 'Prelude.error' if the value+-- does not satisfy the predicate.+--+-- WARNING: this function is not total!+unsafeRefine :: (Predicate p x) => x -> Refined p x+unsafeRefine = refine .> either (displayException .> error) id+{-# INLINABLE unsafeRefine #-}++-- | Constructs a 'Refined' value, completely+-- ignoring any refinements! Use this only+-- when you can manually prove that the refinement+-- holds.+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.+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.+reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x)+reallyUnsafePredEquiv = Coercion+-- Note: reallyUnsafePredEquiv =+-- sym 'reallyUnsafeUnderlyingRefined' `trans` 'reallyUnsafeUnderlyingRefined'++#if __GLASGOW_HASKELL__ >= 805+-- | Reveal that @x@ and @'Refined' p x@ are 'Coercible' for+-- /all/ @x@ and @p@ simultaneously.+--+-- === Example+--+-- @+-- reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x)+-- reallyUnsafePredEquiv = reallyUnsafeAllUnderlyingRefined Coercion+-- @+reallyUnsafeAllUnderlyingRefined+ :: ((forall x y p. (Coercible x y => Coercible y (Refined p x))) => r) -> r+-- Why is this constraint so convoluted? Because otherwise the constraint+-- solver doesn't handle transitivity properly. See "Safe Zero-cost Coercions+-- for Haskell" by Breitner et al.+reallyUnsafeAllUnderlyingRefined r = r+#endif
+ src/Refined/Unsafe/Type.hs view
@@ -0,0 +1,45 @@+--------------------------------------------------------------------------------++-- 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 #-}++--------------------------------------------------------------------------------++-- | This module exports the 'Refined' type with its+-- constructor. This is very risky! In particular, the 'Coercible'+-- instances will be visible throughout the importing module.+-- It is usually better to build the necessary coercions locally+-- using the utilities in "Refined.Unsafe", but in some cases+-- it may be more convenient to write a separate module that+-- imports this one and exports some large coercion.+module Refined.Unsafe.Type+ ( Refined(Refined)+ ) where++import Refined.Internal (Refined(Refined))
+ test/Doctests.hs view
@@ -0,0 +1,23 @@+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"+ ]