--------------------------------------------------------------------------------

-- Copyright © 2015 Nikita Volkov
-- Copyright © 2018 Remy Goldschmidt
-- Copyright © 2020 chessai
--
-- Permission is hereby granted, free of charge, to any person
-- obtaining a copy of this software and associated documentation
-- files (the "Software"), to deal in the Software without
-- restriction, including without limitation the rights to use,
-- copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the
-- Software is furnished to do so, subject to the following
-- conditions:
--
-- The above copyright notice and this permission notice shall be
-- included in all copies or substantial portions of the Software.
--
-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-- OTHER DEALINGS IN THE SOFTWARE.

--------------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall                        #-}
{-# OPTIONS_GHC -fno-warn-orphans            #-}
{-# OPTIONS_GHC -funbox-strict-fields        #-}

--------------------------------------------------------------------------------

{-# LANGUAGE AllowAmbiguousTypes        #-}
{-# LANGUAGE BangPatterns               #-}
{-# LANGUAGE CPP                        #-}
{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE MagicHash                  #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE PackageImports             #-}
{-# LANGUAGE PolyKinds                  #-}
{-# LANGUAGE RoleAnnotations            #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TemplateHaskell            #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE TypeOperators              #-}
{-# LANGUAGE UndecidableInstances       #-}

--------------------------------------------------------------------------------

-- | In type theory, a refinement type is a type endowed
--   with a predicate which is assumed to hold for any element
--   of the refined type.
--
--   This library allows one to capture the idea of a refinement type
--   using the 'Refined' type. A 'Refined' @p@ @x@ wraps a value
--   of type @x@, ensuring that it satisfies a type-level predicate @p@.
--
--   A simple introduction to this library can be found here: http://nikita-volkov.github.io/refined/
--
module Refined
  ( -- * 'Refined' type
    Refined

    -- ** Creation
  , refine
  , refine_
  , refineThrow
  , refineFail
  , refineError
  , refineEither
  , refineTH
  , refineTH_

    -- ** Consumption
  , unrefine

    -- * 'Predicate'
  , Predicate (validate)
  , reifyPredicate

    -- * Logical predicates
  , Not(..)
  , And(..)
  , type (&&)
  , Or(..)
  , type (||)
  , Xor(..)

    -- * Identity predicate
  , IdPred(..)

    -- * Numeric predicates
  , LessThan(..)
  , GreaterThan(..)
  , From(..)
  , To(..)
  , FromTo(..)
  , NegativeFromTo(..)
  , EqualTo(..)
  , NotEqualTo(..)
  , Odd(..)
  , Even(..)
  , DivisibleBy(..)
  , NaN(..)
  , Infinite(..)
  , Positive
  , NonPositive
  , Negative
  , NonNegative
  , ZeroToOne
  , NonZero

    -- * Foldable predicates
    -- ** Size predicates
  , SizeLessThan(..)
  , SizeGreaterThan(..)
  , SizeEqualTo(..)
  , Empty
  , NonEmpty
    -- ** Ordering predicates
  , Ascending(..)
  , Descending(..)

    -- * Weakening
  , Weaken (weaken)
  , andLeft
  , andRight
  , leftOr
  , rightOr

    -- * Strengthening
  , strengthen

    -- * Error handling

    -- ** 'RefineException'
  , RefineException
    ( RefineNotException
    , RefineAndException
    , RefineOrException
    , RefineXorException
    , RefineOtherException
    , RefineSomeException
    )
  , displayRefineException

    -- ** 'validate' helpers
  , throwRefineOtherException
  , throwRefineSomeException
  , success
 ) where

--------------------------------------------------------------------------------

import           Control.Exception            (Exception (displayException))
import           Data.Coerce                  (coerce)
import           Data.Either                  (isRight, rights)
import           Data.Foldable                (foldl')
import           Data.Functor.Contravariant   ((>$<))
import           Data.Proxy                   (Proxy(Proxy))
import           Data.Text                    (Text)
import qualified Data.Text                    as Text
import qualified Data.Text.Lazy               as TextLazy
import qualified Data.Text.Lazy.Builder       as TextBuilder
import qualified Data.Text.Lazy.Builder.Int   as TextBuilder
import qualified Data.ByteString              as BS
import qualified Data.ByteString.Lazy         as BL
import           Data.Typeable                (TypeRep, Typeable, typeRep)

import           Control.Monad.Catch          (MonadThrow, SomeException)
import qualified Control.Monad.Catch          as MonadThrow
import           Control.Monad.Error.Class    (MonadError)
import qualified Control.Monad.Error.Class    as MonadError
#if !MIN_VERSION_base(4,13,0)
import           Control.Monad.Fail           (MonadFail, fail)
import           Prelude                      hiding (fail)
#endif

import           GHC.Exts                     (Proxy#, proxy#)
import           GHC.Generics                 (Generic, Generic1)
import           GHC.TypeLits                 (type (<=), KnownNat, Nat, natVal')

import           Refined.Unsafe.Type          (Refined(Refined))

import qualified Language.Haskell.TH.Syntax   as TH

#if HAVE_AESON
import           Control.Monad    ((<=<))
import           Data.Aeson       (FromJSON, FromJSONKey, ToJSON, ToJSONKey)
import qualified Data.Aeson    as Aeson
#endif

#if HAVE_QUICKCHECK
import           Test.QuickCheck  (Arbitrary, Gen)
import qualified Test.QuickCheck  as QC
import           Data.Typeable    (showsTypeRep)
#endif

import "these-skinny" Data.These                   (These(This,That,These))

--------------------------------------------------------------------------------

-- $setup
--
-- Doctest imports
--
-- >>> :set -XDataKinds
-- >>> :set -XOverloadedStrings
-- >>> :set -XTypeApplications
-- >>> import Data.Int
-- >>> import Data.Either (isLeft)
--

--------------------------------------------------------------------------------

infixl 0 |>
infixl 9 .>

-- | Helper function, stolen from the flow package.
(|>) :: a -> (a -> b) -> b
|> :: forall a b. a -> (a -> b) -> b
(|>) = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
($)
{-# INLINE (|>) #-}

-- | Helper function, stolen from the flow package.
(.>) :: (a -> b) -> (b -> c) -> a -> c
a -> b
f .> :: forall a b c. (a -> b) -> (b -> c) -> a -> c
.> b -> c
g = \a
x -> b -> c
g (a -> b
f a
x)
{-# INLINE (.>) #-}

-- | FIXME: doc
data Ordered a = Empty | Decreasing a | Increasing a

-- | FIXME: doc
inc :: Ordered a -> Bool
inc :: forall a. Ordered a -> Bool
inc (Decreasing a
_) = Bool
False
inc Ordered a
_              = Bool
True
{-# INLINE inc #-}

-- | FIXME: doc
dec :: Ordered a -> Bool
dec :: forall a. Ordered a -> Bool
dec (Increasing a
_) = Bool
False
dec Ordered a
_              = Bool
True
{-# INLINE dec #-}

increasing :: (Foldable t, Ord a) => t a -> Bool
increasing :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> Bool
increasing = forall a. Ordered a -> Bool
inc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall {a}. Ord a => Ordered a -> a -> Ordered a
go forall a. Ordered a
Empty where
  go :: Ordered a -> a -> Ordered a
go Ordered a
Empty a
y = forall a. a -> Ordered a
Increasing a
y
  go (Decreasing a
x) a
_ = forall a. a -> Ordered a
Decreasing a
x
  go (Increasing a
x) a
y
    | a
x forall a. Ord a => a -> a -> Bool
<= a
y = forall a. a -> Ordered a
Increasing a
y
    | Bool
otherwise = forall a. a -> Ordered a
Decreasing a
y
{-# INLINABLE increasing #-}

decreasing :: (Foldable t, Ord a) => t a -> Bool
decreasing :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> Bool
decreasing = forall a. Ordered a -> Bool
dec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall {a}. Ord a => Ordered a -> a -> Ordered a
go forall a. Ordered a
Empty where
  go :: Ordered a -> a -> Ordered a
go Ordered a
Empty a
y = forall a. a -> Ordered a
Decreasing a
y
  go (Increasing a
x) a
_ = forall a. a -> Ordered a
Increasing a
x
  go (Decreasing a
x) a
y
    | a
x forall a. Ord a => a -> a -> Bool
>= a
y = forall a. a -> Ordered a
Decreasing a
y
    | Bool
otherwise = forall a. a -> Ordered a
Increasing a
y
{-# INLINABLE decreasing #-}

--------------------------------------------------------------------------------

-- | This instance makes sure to check the refinement.
--
--   @since 0.1.0.0
instance (Read x, Predicate p x) => Read (Refined p x) where
  readsPrec :: Int -> ReadS (Refined p x)
readsPrec Int
d = forall a. Bool -> ReadS a -> ReadS a
readParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$ \String
r1 -> do
    (String
"Refined", String
r2) <- ReadS String
lex String
r1
    (x
raw,       String
r3) <- forall a. Read a => Int -> ReadS a
readsPrec Int
11 String
r2
    case forall {k} (p :: k) x.
Predicate p x =>
x -> Either RefineException (Refined p x)
refine x
raw of
      Right Refined p x
val -> [(Refined p x
val, String
r3)]
      Left  RefineException
_   -> []

#if HAVE_AESON
-- | @since 0.4
instance (FromJSON a, Predicate p a) => FromJSON (Refined p a) where
  parseJSON :: Value -> Parser (Refined p a)
parseJSON = forall {k} (p :: k) x (m :: * -> *).
(Predicate p x, MonadFail m) =>
x -> m (Refined p x)
refineFail forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a. FromJSON a => Value -> Parser a
Aeson.parseJSON

instance (FromJSONKey a, Predicate p a) => FromJSONKey (Refined p a) where
  fromJSONKey :: FromJSONKeyFunction (Refined p a)
fromJSONKey = case forall a. FromJSONKey a => FromJSONKeyFunction a
Aeson.fromJSONKey @a of
    FromJSONKeyFunction a
Aeson.FromJSONKeyCoerce -> forall a. (Text -> Parser a) -> FromJSONKeyFunction a
Aeson.FromJSONKeyTextParser forall a b. (a -> b) -> a -> b
$ forall {k} (p :: k) x (m :: * -> *).
(Predicate p x, MonadFail m) =>
x -> m (Refined p x)
refineFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce
    Aeson.FromJSONKeyText Text -> a
f -> forall a. (Text -> Parser a) -> FromJSONKeyFunction a
Aeson.FromJSONKeyTextParser forall a b. (a -> b) -> a -> b
$ forall {k} (p :: k) x (m :: * -> *).
(Predicate p x, MonadFail m) =>
x -> m (Refined p x)
refineFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> a
f
    Aeson.FromJSONKeyTextParser Text -> Parser a
f -> forall a. (Text -> Parser a) -> FromJSONKeyFunction a
Aeson.FromJSONKeyTextParser forall a b. (a -> b) -> a -> b
$ forall {k} (p :: k) x (m :: * -> *).
(Predicate p x, MonadFail m) =>
x -> m (Refined p x)
refineFail forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Text -> Parser a
f
    Aeson.FromJSONKeyValue Value -> Parser a
f -> forall a. (Value -> Parser a) -> FromJSONKeyFunction a
Aeson.FromJSONKeyValue forall a b. (a -> b) -> a -> b
$ forall {k} (p :: k) x (m :: * -> *).
(Predicate p x, MonadFail m) =>
x -> m (Refined p x)
refineFail forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Value -> Parser a
f

  fromJSONKeyList :: FromJSONKeyFunction [Refined p a]
fromJSONKeyList = case forall a. FromJSONKey a => FromJSONKeyFunction [a]
Aeson.fromJSONKeyList @a of
    Aeson.FromJSONKeyText Text -> [a]
f -> forall a. (Text -> Parser a) -> FromJSONKeyFunction a
Aeson.FromJSONKeyTextParser forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall {k} (p :: k) x (m :: * -> *).
(Predicate p x, MonadFail m) =>
x -> m (Refined p x)
refineFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [a]
f
    Aeson.FromJSONKeyTextParser Text -> Parser [a]
f -> forall a. (Text -> Parser a) -> FromJSONKeyFunction a
Aeson.FromJSONKeyTextParser forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall {k} (p :: k) x (m :: * -> *).
(Predicate p x, MonadFail m) =>
x -> m (Refined p x)
refineFail forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Text -> Parser [a]
f
    Aeson.FromJSONKeyValue Value -> Parser [a]
f -> forall a. (Value -> Parser a) -> FromJSONKeyFunction a
Aeson.FromJSONKeyValue forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall {k} (p :: k) x (m :: * -> *).
(Predicate p x, MonadFail m) =>
x -> m (Refined p x)
refineFail forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Value -> Parser [a]
f

-- | @since 0.4
instance (ToJSON a, Predicate p a) => ToJSON (Refined p a) where
  toJSON :: Refined p a -> Value
toJSON = forall a. ToJSON a => a -> Value
Aeson.toJSON forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (p :: k) x. Refined p x -> x
unrefine

-- | @since 0.6.3
instance (ToJSONKey a, Predicate p a) => ToJSONKey (Refined p a) where
  toJSONKey :: ToJSONKeyFunction (Refined p a)
toJSONKey = forall {k} (p :: k) x. Refined p x -> x
unrefine forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
>$< forall a. ToJSONKey a => ToJSONKeyFunction a
Aeson.toJSONKey
  toJSONKeyList :: ToJSONKeyFunction [Refined p a]
toJSONKeyList = forall a b. (a -> b) -> [a] -> [b]
map forall {k} (p :: k) x. Refined p x -> x
unrefine forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
>$< forall a. ToJSONKey a => ToJSONKeyFunction [a]
Aeson.toJSONKeyList
#endif /* HAVE_AESON */

#if HAVE_QUICKCHECK
-- | @since 0.4
instance forall p a. (Arbitrary a, Typeable a, Typeable p, Predicate p a) => Arbitrary (Refined p a) where
  arbitrary :: Gen (Refined p a)
arbitrary = Int -> Gen a -> Gen (Refined p a)
loop Int
0 forall a. Arbitrary a => Gen a
QC.arbitrary
    where
      loop :: Int -> Gen a -> Gen (Refined p a)
      loop :: Int -> Gen a -> Gen (Refined p a)
loop !Int
runs Gen a
gen
        | Int
runs forall a. Ord a => a -> a -> Bool
< Int
100 = do
            Maybe (Refined p a)
m <- forall {k} (p :: k) a.
Predicate p a =>
Gen a -> Gen (Maybe (Refined p a))
suchThatRefined Gen a
gen
            case Maybe (Refined p a)
m of
              Just Refined p a
x -> do
                forall (f :: * -> *) a. Applicative f => a -> f a
pure Refined p a
x
              Maybe (Refined p a)
Nothing -> do
                Int -> Gen a -> Gen (Refined p a)
loop (Int
runs forall a. Num a => a -> a -> a
+ Int
1) Gen a
gen
        | Bool
otherwise = forall a. HasCallStack => String -> a
error (forall {k} {k} (p :: k) (a :: k).
(Typeable p, Typeable a) =>
Proxy p -> Proxy a -> String
refinedGenError (forall {k} (t :: k). Proxy t
Proxy @p) (forall {k} (t :: k). Proxy t
Proxy @a))
  shrink :: Refined p a -> [Refined p a]
shrink = forall a b. [Either a b] -> [b]
rights forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall {k} (p :: k) x.
Predicate p x =>
x -> Either RefineException (Refined p x)
refine forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Arbitrary a => a -> [a]
QC.shrink forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (p :: k) x. Refined p x -> x
unrefine

refinedGenError :: (Typeable p, Typeable a)
  => Proxy p -> Proxy a -> String
refinedGenError :: forall {k} {k} (p :: k) (a :: k).
(Typeable p, Typeable a) =>
Proxy p -> Proxy a -> String
refinedGenError Proxy p
p Proxy a
a = String
"arbitrary :: Refined ("
  forall a. [a] -> [a] -> [a]
++ forall {k} (a :: k). Typeable a => Proxy a -> String
typeName Proxy p
p
  forall a. [a] -> [a] -> [a]
++ String
") ("
  forall a. [a] -> [a] -> [a]
++ forall {k} (a :: k). Typeable a => Proxy a -> String
typeName Proxy a
a
  forall a. [a] -> [a] -> [a]
++ String
"): Failed to generate a value that satisfied"
  forall a. [a] -> [a] -> [a]
++ String
" the predicate after 100 tries."

suchThatRefined :: forall p a. (Predicate p a)
  => Gen a -> Gen (Maybe (Refined p a))
suchThatRefined :: forall {k} (p :: k) a.
Predicate p a =>
Gen a -> Gen (Maybe (Refined p a))
suchThatRefined Gen a
gen = do
  Maybe a
m <- forall a. Gen a -> (a -> Bool) -> Gen (Maybe a)
QC.suchThatMaybe Gen a
gen (forall {k} (p :: k) a. Predicate p a => a -> Bool
reifyPredicate @p @a)
  case Maybe a
m of
    Maybe a
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
    Just a
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> Maybe a
Just (forall k (p :: k) x. x -> Refined p x
Refined a
x))

typeName :: Typeable a => Proxy a -> String
typeName :: forall {k} (a :: k). Typeable a => Proxy a -> String
typeName = forall a b c. (a -> b -> c) -> b -> a -> c
flip TypeRep -> ShowS
showsTypeRep String
"" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep
#endif /* HAVE_QUICKCHECK */

--------------------------------------------------------------------------------

-- | A smart constructor of a 'Refined' value.
--   Checks the input value at runtime.
--
--   @since 0.1.0.0
refine :: forall p x. (Predicate p x) => x -> Either RefineException (Refined p x)
refine :: forall {k} (p :: k) x.
Predicate p x =>
x -> Either RefineException (Refined p x)
refine x
x = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a b. b -> Either a b
Right (forall k (p :: k) x. x -> Refined p x
Refined x
x)) forall a b. a -> Either a b
Left (forall {k} (p :: k) x.
Predicate p x =>
Proxy p -> x -> Maybe RefineException
validate (forall {k} (t :: k). Proxy t
Proxy @p) x
x)
{-# INLINABLE refine #-}

-- | Like 'refine', but discards the refinement.
--   This _can_ be useful when you only need to validate
--   that some value at runtime satisfies some predicate.
--   See also 'reifyPredicate'.
--
--   @since 0.4.4
refine_ :: forall p x. (Predicate p x) => x -> Either RefineException x
refine_ :: forall {k} (p :: k) x.
Predicate p x =>
x -> Either RefineException x
refine_ = forall {k} (p :: k) x.
Predicate p x =>
x -> Either RefineException (Refined p x)
refine @p @x forall a b c. (a -> b) -> (b -> c) -> a -> c
.> coerce :: forall a b. Coercible a b => a -> b
coerce
{-# INLINABLE refine_ #-}

-- | Constructs a 'Refined' value at run-time,
--   calling 'Control.Monad.Catch.throwM' if the value
--   does not satisfy the predicate.
--
--   @since 0.2.0.0
refineThrow :: (Predicate p x, MonadThrow m) => x -> m (Refined p x)
refineThrow :: forall {k} (p :: k) x (m :: * -> *).
(Predicate p x, MonadThrow m) =>
x -> m (Refined p x)
refineThrow = forall {k} (p :: k) x.
Predicate p x =>
x -> Either RefineException (Refined p x)
refine forall a b c. (a -> b) -> (b -> c) -> a -> c
.> forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
MonadThrow.throwM forall (f :: * -> *) a. Applicative f => a -> f a
pure
{-# INLINABLE refineThrow #-}

-- | Constructs a 'Refined' value at run-time,
--   calling 'Control.Monad.Fail.fail' if the value
--   does not satisfy the predicate.
--
--   @since 0.2.0.0
refineFail :: (Predicate p x, MonadFail m) => x -> m (Refined p x)
refineFail :: forall {k} (p :: k) x (m :: * -> *).
(Predicate p x, MonadFail m) =>
x -> m (Refined p x)
refineFail = forall {k} (p :: k) x.
Predicate p x =>
x -> Either RefineException (Refined p x)
refine forall a b c. (a -> b) -> (b -> c) -> a -> c
.> forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall e. Exception e => e -> String
displayException forall a b c. (a -> b) -> (b -> c) -> a -> c
.> forall (m :: * -> *) a. MonadFail m => String -> m a
fail) forall (f :: * -> *) a. Applicative f => a -> f a
pure
{-# INLINABLE refineFail #-}

-- | Constructs a 'Refined' value at run-time,
--   calling 'Control.Monad.Error.throwError' if the value
--   does not satisfy the predicate.
--
--   @since 0.2.0.0
refineError :: (Predicate p x, MonadError RefineException m)
            => x -> m (Refined p x)
refineError :: forall {k} (p :: k) x (m :: * -> *).
(Predicate p x, MonadError RefineException m) =>
x -> m (Refined p x)
refineError = forall {k} (p :: k) x.
Predicate p x =>
x -> Either RefineException (Refined p x)
refine forall a b c. (a -> b) -> (b -> c) -> a -> c
.> forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall e (m :: * -> *) a. MonadError e m => e -> m a
MonadError.throwError forall (f :: * -> *) a. Applicative f => a -> f a
pure
{-# INLINABLE refineError #-}

-- | Like 'refine', but, when the value doesn't satisfy the predicate, returns
--   a 'Refined' value with the predicate negated, instead of returning
--   'RefineException'.
--
--   >>> isRight (refineEither @Even @Int 42)
--   True
--
--   >>> isLeft (refineEither @Even @Int 43)
--   True
--
refineEither :: forall p x. (Predicate p x) => x -> Either (Refined (Not p) x) (Refined p x)
refineEither :: forall {k} (p :: k) x.
Predicate p x =>
x -> Either (Refined (Not p) x) (Refined p x)
refineEither x
x =
  case forall {k} (p :: k) x.
Predicate p x =>
Proxy p -> x -> Maybe RefineException
validate (forall {k} (t :: k). Proxy t
Proxy @p) x
x of
    Maybe RefineException
Nothing -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall k (p :: k) x. x -> Refined p x
Refined x
x
    Just RefineException
_  -> forall a b. a -> Either a b
Left  forall a b. (a -> b) -> a -> b
$ forall k (p :: k) x. x -> Refined p x
Refined x
x
{-# INLINABLE refineEither #-}

--------------------------------------------------------------------------------

-- | Constructs a 'Refined' value at compile-time using @-XTemplateHaskell@.
--
--   For example:
--
--   > $$(refineTH 23) :: Refined Positive Int
--   > Refined 23
--
--   Here's an example of an invalid value:
--
--   > $$(refineTH 0) :: Refined Positive Int
--   > <interactive>:6:4:
--   >     Value is not greater than 0
--   >     In the Template Haskell splice $$(refineTH 0)
--   >     In the expression: $$(refineTH 0) :: Refined Positive Int
--   >     In an equation for ‘it’:
--   >         it = $$(refineTH 0) :: Refined Positive Int
--
--   The example above indicates a compile-time failure,
--   which means that the checking was done at compile-time,
--   thus introducing a zero-runtime overhead compared to
--   a plain value construction.
--
--   /Note/: It may be useful to use this function with the
--   <https://hackage.haskell.org/package/th-lift-instances/ th-lift-instances package>.
--
--   @since 0.1.0.0
#if MIN_VERSION_template_haskell(2,17,0)
refineTH :: forall p x m. (Predicate p x, TH.Lift x, TH.Quote m, MonadFail m)
  => x
  -> TH.Code m (Refined p x)
refineTH :: forall {k} (p :: k) x (m :: * -> *).
(Predicate p x, Lift x, Quote m, MonadFail m) =>
x -> Code m (Refined p x)
refineTH =
  let showException :: RefineException -> Code m a
showException = RefineException -> ExceptionTree RefineException
refineExceptionToTree
        forall a b c. (a -> b) -> (b -> c) -> a -> c
.> Bool -> ExceptionTree RefineException -> String
showTree Bool
True
        forall a b c. (a -> b) -> (b -> c) -> a -> c
.> forall (m :: * -> *) a. MonadFail m => String -> m a
fail
        forall a b c. (a -> b) -> (b -> c) -> a -> c
.> forall a (m :: * -> *). m (TExp a) -> Code m a
TH.liftCode
  in forall {k} (p :: k) x.
Predicate p x =>
x -> Either RefineException (Refined p x)
refine @p @x
     forall a b c. (a -> b) -> (b -> c) -> a -> c
.> forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall {a}. RefineException -> Code m a
showException forall t (m :: * -> *). (Lift t, Quote m) => t -> Code m t
TH.liftTyped
#else
refineTH :: forall p x. (Predicate p x, TH.Lift x)
  => x
  -> TH.Q (TH.TExp (Refined p x))
refineTH =
  let showException = refineExceptionToTree
        .> showTree True
        .> fail
  in refine @p @x
     .> either showException TH.lift
     .> fmap TH.TExp
#endif

-- | Like 'refineTH', but immediately unrefines the value.
--   This is useful when some value need only be refined
--   at compile-time.
--
--   @since 0.4.4
#if MIN_VERSION_template_haskell(2,17,0)
refineTH_ :: forall p x m. (Predicate p x, TH.Lift x, TH.Quote m, MonadFail m)
  => x
  -> TH.Code m x
refineTH_ :: forall {k} (p :: k) x (m :: * -> *).
(Predicate p x, Lift x, Quote m, MonadFail m) =>
x -> Code m x
refineTH_ =
  forall {k} (p :: k) x (m :: * -> *).
(Predicate p x, Lift x, Quote m, MonadFail m) =>
x -> Code m (Refined p x)
refineTH @p @x
  forall a b c. (a -> b) -> (b -> c) -> a -> c
.> forall (m :: * -> *) a. Code m a -> m (TExp a)
TH.examineCode
  forall a b c. (a -> b) -> (b -> c) -> a -> c
.> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {k} (p :: k) x. TExp (Refined p x) -> TExp x
unsafeUnrefineTExp
  forall a b c. (a -> b) -> (b -> c) -> a -> c
.> forall a (m :: * -> *). m (TExp a) -> Code m a
TH.liftCode
#else
refineTH_ :: forall p x. (Predicate p x, TH.Lift x)
  => x
  -> TH.Q (TH.TExp x)
refineTH_ = refineTH @p @x .> fmap unsafeUnrefineTExp
#endif

unsafeUnrefineTExp :: TH.TExp (Refined p x) -> TH.TExp x
unsafeUnrefineTExp :: forall {k} (p :: k) x. TExp (Refined p x) -> TExp x
unsafeUnrefineTExp (TH.TExp Exp
e) = forall a. Exp -> TExp a
TH.TExp
  (Name -> Exp
TH.VarE 'unrefine Exp -> Exp -> Exp
`TH.AppE` Exp
e)

--------------------------------------------------------------------------------

-- | Extracts the refined value.
--
--   @since 0.1.0.0
unrefine :: Refined p x -> x
unrefine :: forall {k} (p :: k) x. Refined p x -> x
unrefine = coerce :: forall a b. Coercible a b => a -> b
coerce
{-# INLINE unrefine #-}

--------------------------------------------------------------------------------

-- | A typeclass which defines a runtime interpretation of
--   a type-level predicate @p@ for type @x@.
--
--   @since 0.1.0.0
class (Typeable p) => Predicate p x where
  {-# MINIMAL validate #-}
  -- | Check the value @x@ according to the predicate @p@,
  --   producing an error 'RefineException' if the value
  --   does not satisfy.
  --
  --   /Note/: 'validate' is not intended to be used
  --   directly; instead, it is intended to provide the minimal
  --   means necessary for other utilities to be derived. As
  --   such, the 'Maybe' here should be interpreted to mean
  --   the presence or absence of a 'RefineException', and
  --   nothing else.
  validate :: Proxy p -> x -> Maybe RefineException

--------------------------------------------------------------------------------

-- | Reify a 'Predicate' by turning it into a value-level predicate.
--
--   @since 0.4.2.3
reifyPredicate :: forall p a. Predicate p a => a -> Bool
reifyPredicate :: forall {k} (p :: k) a. Predicate p a => a -> Bool
reifyPredicate = forall {k} (p :: k) x.
Predicate p x =>
x -> Either RefineException (Refined p x)
refine @p @a forall a b c. (a -> b) -> (b -> c) -> a -> c
.> forall a b. Either a b -> Bool
isRight
{-# INLINABLE reifyPredicate #-}

--------------------------------------------------------------------------------

-- | A predicate which is satisfied for all types.
--   Arguments passed to @'validate'@ in @'validate' 'IdPred' x@
--   are not evaluated.
--
--   >>> isRight (refine @IdPred @Int undefined)
--   True
--
--   >>> isLeft (refine @IdPred @Int undefined)
--   False
--
--   @since 0.3.0.0
data IdPred
  = IdPred -- ^ @since 0.4.2
  deriving
    ( forall x. Rep IdPred x -> IdPred
forall x. IdPred -> Rep IdPred x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep IdPred x -> IdPred
$cfrom :: forall x. IdPred -> Rep IdPred x
Generic -- ^ @since 0.3.0.0
    )

-- | @since 0.3.0.0
instance Predicate IdPred x where
  validate :: Proxy IdPred -> x -> Maybe RefineException
validate Proxy IdPred
_ x
_ = forall a. Maybe a
Nothing
  {-# INLINE validate #-}

--------------------------------------------------------------------------------

-- | The negation of a predicate.
--
--   >>> isRight (refine @(Not NonEmpty) @[Int] [])
--   True
--
--   >>> isLeft (refine @(Not NonEmpty) @[Int] [1,2])
--   True
--
--   @since 0.1.0.0
data Not p
  = Not -- ^ @since 0.4.2
  deriving
    ( forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (p :: k) x. Rep (Not p) x -> Not p
forall k (p :: k) x. Not p -> Rep (Not p) x
$cto :: forall k (p :: k) x. Rep (Not p) x -> Not p
$cfrom :: forall k (p :: k) x. Not p -> Rep (Not p) x
Generic -- ^ @since 0.3.0.0
    , forall k (a :: k). Rep1 Not a -> Not a
forall k (a :: k). Not a -> Rep1 Not a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cto1 :: forall k (a :: k). Rep1 Not a -> Not a
$cfrom1 :: forall k (a :: k). Not a -> Rep1 Not a
Generic1 -- ^ @since 0.3.0.0
    )

-- | @since 0.1.0.0
instance (Predicate (p :: k) x, Typeable p, Typeable k) => Predicate (Not p) x where
  validate :: Proxy (Not p) -> x -> Maybe RefineException
validate Proxy (Not p)
p x
x = do
    forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. a -> Maybe a
Just (TypeRep -> RefineException
RefineNotException (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (Not p)
p)))
          (forall a b. a -> b -> a
const forall a. Maybe a
Nothing)
          (forall {k} (p :: k) x.
Predicate p x =>
Proxy p -> x -> Maybe RefineException
validate @p forall a. HasCallStack => a
undefined x
x)

--------------------------------------------------------------------------------

-- | The conjunction of two predicates.
--
--   >>> isLeft (refine @(And Positive Negative) @Int 3)
--   True
--
--   >>> isRight (refine @(And Positive Odd) @Int 203)
--   True
--
--   @since 0.1.0.0
data And l r
  = And -- ^ @since 0.4.2
  deriving
    ( forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (l :: k) k (r :: k) x. Rep (And l r) x -> And l r
forall k (l :: k) k (r :: k) x. And l r -> Rep (And l r) x
$cto :: forall k (l :: k) k (r :: k) x. Rep (And l r) x -> And l r
$cfrom :: forall k (l :: k) k (r :: k) x. And l r -> Rep (And l r) x
Generic -- ^ @since 0.3.0.0
    , forall k k (l :: k) (a :: k). Rep1 (And l) a -> And l a
forall k k (l :: k) (a :: k). And l a -> Rep1 (And l) a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cto1 :: forall k k (l :: k) (a :: k). Rep1 (And l) a -> And l a
$cfrom1 :: forall k k (l :: k) (a :: k). And l a -> Rep1 (And l) a
Generic1 -- ^ @since 0.3.0.0
    )

infixr 3 &&
-- | The conjunction of two predicates.
--
--   @since 0.2.0.0
type (&&) = And

-- | @since 0.1.0.0
instance ( Predicate (l :: k) x, Predicate (r :: k) x, Typeable l, Typeable r, Typeable k
         ) => Predicate (And l r) x where
  validate :: Proxy (And l r) -> x -> Maybe RefineException
validate Proxy (And l r)
p x
x = do
    let a :: Maybe RefineException
a = forall {k} (p :: k) x.
Predicate p x =>
Proxy p -> x -> Maybe RefineException
validate @l forall a. HasCallStack => a
undefined x
x
    let b :: Maybe RefineException
b = forall {k} (p :: k) x.
Predicate p x =>
Proxy p -> x -> Maybe RefineException
validate @r forall a. HasCallStack => a
undefined x
x
    let throw :: These RefineException RefineException -> Maybe RefineException
throw These RefineException RefineException
err = forall a. a -> Maybe a
Just (TypeRep -> These RefineException RefineException -> RefineException
RefineAndException (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (And l r)
p) These RefineException RefineException
err)
    case (Maybe RefineException
a, Maybe RefineException
b) of
      (Just  RefineException
e, Just RefineException
e1) -> These RefineException RefineException -> Maybe RefineException
throw (forall a b. a -> b -> These a b
These RefineException
e RefineException
e1)
      (Just  RefineException
e,       Maybe RefineException
_) -> These RefineException RefineException -> Maybe RefineException
throw (forall a b. a -> These a b
This RefineException
e)
      (Maybe RefineException
Nothing, Just  RefineException
e) -> These RefineException RefineException -> Maybe RefineException
throw (forall a b. b -> These a b
That RefineException
e)
      (Maybe RefineException
Nothing, Maybe RefineException
Nothing) -> forall a. Maybe a
Nothing

--------------------------------------------------------------------------------

-- | The disjunction of two predicates.
--
--   >>> isRight (refine @(Or Even Odd) @Int 3)
--   True
--
--   >>> isRight (refine @(Or (LessThan 3) (GreaterThan 3)) @Int 2)
--   True
--
--   >>> isRight (refine @(Or Even Even) @Int 4)
--   True
--
--   @since 0.1.0.0
data Or l r
  = Or -- ^ @since 0.4.2
  deriving
    ( forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (l :: k) k (r :: k) x. Rep (Or l r) x -> Or l r
forall k (l :: k) k (r :: k) x. Or l r -> Rep (Or l r) x
$cto :: forall k (l :: k) k (r :: k) x. Rep (Or l r) x -> Or l r
$cfrom :: forall k (l :: k) k (r :: k) x. Or l r -> Rep (Or l r) x
Generic -- ^ @since 0.3.0.0
    , forall k k (l :: k) (a :: k). Rep1 (Or l) a -> Or l a
forall k k (l :: k) (a :: k). Or l a -> Rep1 (Or l) a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cto1 :: forall k k (l :: k) (a :: k). Rep1 (Or l) a -> Or l a
$cfrom1 :: forall k k (l :: k) (a :: k). Or l a -> Rep1 (Or l) a
Generic1 -- ^ @since 0.3.0.0
    )

infixr 2 ||
-- | The disjunction of two predicates.
--
--   @since 0.2.0.0
type (||) = Or

-- | @since 0.2.0.0
instance ( Predicate (l :: k) x, Predicate (r :: k) x, Typeable l, Typeable r, Typeable k
         ) => Predicate (Or l r) x where
  validate :: Proxy (Or l r) -> x -> Maybe RefineException
validate Proxy (Or l r)
p x
x = do
    let left :: Maybe RefineException
left  = forall {k} (p :: k) x.
Predicate p x =>
Proxy p -> x -> Maybe RefineException
validate @l forall a. HasCallStack => a
undefined x
x
    let right :: Maybe RefineException
right = forall {k} (p :: k) x.
Predicate p x =>
Proxy p -> x -> Maybe RefineException
validate @r forall a. HasCallStack => a
undefined x
x
    case (Maybe RefineException
left, Maybe RefineException
right) of
      (Just RefineException
l, Just RefineException
r) -> forall a. a -> Maybe a
Just (TypeRep -> RefineException -> RefineException -> RefineException
RefineOrException (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (Or l r)
p) RefineException
l RefineException
r)
      (Maybe RefineException, Maybe RefineException)
_                -> forall a. Maybe a
Nothing

--------------------------------------------------------------------------------

-- | The exclusive disjunction of two predicates.
--
--
--   >>> isRight (refine @(Xor Even Odd) @Int 3)
--   True
--
--   >>> isLeft (refine @(Xor (LessThan 3) (EqualTo 2)) @Int 2)
--   True
--
--   >>> isLeft (refine @(Xor Even Even) @Int 2)
--   True
--
--   @since 0.5
data Xor l r
  = Xor -- ^ @since 0.5
  deriving
    ( forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (l :: k) k (r :: k) x. Rep (Xor l r) x -> Xor l r
forall k (l :: k) k (r :: k) x. Xor l r -> Rep (Xor l r) x
$cto :: forall k (l :: k) k (r :: k) x. Rep (Xor l r) x -> Xor l r
$cfrom :: forall k (l :: k) k (r :: k) x. Xor l r -> Rep (Xor l r) x
Generic -- ^ @since 0.5
    , forall k k (l :: k) (a :: k). Rep1 (Xor l) a -> Xor l a
forall k k (l :: k) (a :: k). Xor l a -> Rep1 (Xor l) a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cto1 :: forall k k (l :: k) (a :: k). Rep1 (Xor l) a -> Xor l a
$cfrom1 :: forall k k (l :: k) (a :: k). Xor l a -> Rep1 (Xor l) a
Generic1 -- ^ @since 0.5
    )

-- not provided because it clashes with GHC.TypeLits.^
-- infixr 8 ^
-- The exclusive disjunction of two predicates.
-- type (^) = Xor

-- | @since 0.5
instance ( Predicate (l :: k) x, Predicate (r :: k) x, Typeable l, Typeable r, Typeable k
         ) => Predicate (Xor l r) x where
  validate :: Proxy (Xor l r) -> x -> Maybe RefineException
validate Proxy (Xor l r)
p x
x = do
    let left :: Maybe RefineException
left = forall {k} (p :: k) x.
Predicate p x =>
Proxy p -> x -> Maybe RefineException
validate @l forall a. HasCallStack => a
undefined x
x
    let right :: Maybe RefineException
right = forall {k} (p :: k) x.
Predicate p x =>
Proxy p -> x -> Maybe RefineException
validate @r forall a. HasCallStack => a
undefined x
x
    case (Maybe RefineException
left, Maybe RefineException
right) of
      (Maybe RefineException
Nothing, Maybe RefineException
Nothing) -> forall a. a -> Maybe a
Just (TypeRep
-> Maybe (RefineException, RefineException) -> RefineException
RefineXorException (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (Xor l r)
p) forall a. Maybe a
Nothing)
      (Just  RefineException
l, Just  RefineException
r) -> forall a. a -> Maybe a
Just (TypeRep
-> Maybe (RefineException, RefineException) -> RefineException
RefineXorException (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (Xor l r)
p) (forall a. a -> Maybe a
Just (RefineException
l, RefineException
r)))
      (Maybe RefineException, Maybe RefineException)
_ -> forall a. Maybe a
Nothing

--------------------------------------------------------------------------------

-- | A 'Predicate' ensuring that the value has a length
-- which is less than the specified type-level number.
--
--   >>> isRight (refine @(SizeLessThan 4) @[Int] [1,2,3])
--   True
--
--   >>> isLeft (refine @(SizeLessThan 5) @[Int] [1,2,3,4,5])
--   True
--
--   >>> isRight (refine @(SizeLessThan 4) @Text "Hi")
--   True
--
--   >>> isLeft (refine @(SizeLessThan 4) @Text "Hello")
--   True
--
--   @since 0.2.0.0
data SizeLessThan (n :: Nat)
  = SizeLessThan -- ^ @since 0.4.2
  deriving
    ( forall (n :: Nat) x. Rep (SizeLessThan n) x -> SizeLessThan n
forall (n :: Nat) x. SizeLessThan n -> Rep (SizeLessThan n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (n :: Nat) x. Rep (SizeLessThan n) x -> SizeLessThan n
$cfrom :: forall (n :: Nat) x. SizeLessThan n -> Rep (SizeLessThan n) x
Generic -- ^ @since 0.3.0.0
    )

-- | @since 0.2.0.0
instance (Foldable t, KnownNat n) => Predicate (SizeLessThan n) (t a) where
  validate :: Proxy (SizeLessThan n) -> t a -> Maybe RefineException
validate Proxy (SizeLessThan n)
p t a
x = forall {k} (p :: Nat -> k) (n :: Nat) a.
(Typeable (p n), KnownNat n) =>
Proxy (p n)
-> (a, Text)
-> (a -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
sized Proxy (SizeLessThan n)
p (t a
x, Text
"Foldable") forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Ord a => a -> a -> Bool
(<), Text
"less than")
-- | @since 0.5
instance (KnownNat n) => Predicate (SizeLessThan n) Text where
  validate :: Proxy (SizeLessThan n) -> Text -> Maybe RefineException
validate Proxy (SizeLessThan n)
p Text
x = forall {k} (p :: Nat -> k) (n :: Nat) a.
(Typeable (p n), KnownNat n) =>
Proxy (p n)
-> (a, Text)
-> (a -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
sized Proxy (SizeLessThan n)
p (Text
x, Text
"Text") Text -> Int
Text.length (forall a. Ord a => a -> a -> Bool
(<), Text
"less than")

-- | @since 0.5
instance (KnownNat n) => Predicate (SizeLessThan n) BS.ByteString where
  validate :: Proxy (SizeLessThan n) -> ByteString -> Maybe RefineException
validate Proxy (SizeLessThan n)
p ByteString
x = forall {k} (p :: Nat -> k) (n :: Nat) a.
(Typeable (p n), KnownNat n) =>
Proxy (p n)
-> (a, Text)
-> (a -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
sized Proxy (SizeLessThan n)
p (ByteString
x, Text
"ByteString") ByteString -> Int
BS.length (forall a. Ord a => a -> a -> Bool
(<), Text
"less than")

-- | @since 0.5
instance (KnownNat n) => Predicate (SizeLessThan n) BL.ByteString where
  validate :: Proxy (SizeLessThan n) -> ByteString -> Maybe RefineException
validate Proxy (SizeLessThan n)
p ByteString
x = forall {k} (p :: Nat -> k) (n :: Nat) a.
(Typeable (p n), KnownNat n) =>
Proxy (p n)
-> (a, Text)
-> (a -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
sized Proxy (SizeLessThan n)
p (ByteString
x, Text
"ByteString") (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Int64
BL.length) (forall a. Ord a => a -> a -> Bool
(<), Text
"less than")

--------------------------------------------------------------------------------

-- | A 'Predicate' ensuring that the value has a length
-- which is greater than the specified type-level number.
--
--   >>> isLeft (refine  @(SizeGreaterThan 3) @[Int] [1,2,3])
--   True
--
--   >>> isRight (refine @(SizeGreaterThan 3) @[Int] [1,2,3,4,5])
--   True
--
--   >>> isLeft (refine @(SizeGreaterThan 4) @Text "Hi")
--   True
--
--   >>> isRight (refine @(SizeGreaterThan 4) @Text "Hello")
--   True
--
--   @since 0.2.0.0
data SizeGreaterThan (n :: Nat)
  = SizeGreaterThan -- ^ @since 0.4.2
  deriving
    ( forall (n :: Nat) x. Rep (SizeGreaterThan n) x -> SizeGreaterThan n
forall (n :: Nat) x. SizeGreaterThan n -> Rep (SizeGreaterThan n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (n :: Nat) x. Rep (SizeGreaterThan n) x -> SizeGreaterThan n
$cfrom :: forall (n :: Nat) x. SizeGreaterThan n -> Rep (SizeGreaterThan n) x
Generic -- ^ @since 0.3.0.0
    )

-- | @since 0.2.0.0
instance (Foldable t, KnownNat n) => Predicate (SizeGreaterThan n) (t a) where
  validate :: Proxy (SizeGreaterThan n) -> t a -> Maybe RefineException
validate Proxy (SizeGreaterThan n)
p t a
x = forall {k} (p :: Nat -> k) (n :: Nat) a.
(Typeable (p n), KnownNat n) =>
Proxy (p n)
-> (a, Text)
-> (a -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
sized Proxy (SizeGreaterThan n)
p (t a
x, Text
"Foldable") forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Ord a => a -> a -> Bool
(>), Text
"greater than")

-- | @since 0.5
instance (KnownNat n) => Predicate (SizeGreaterThan n) Text where
  validate :: Proxy (SizeGreaterThan n) -> Text -> Maybe RefineException
validate Proxy (SizeGreaterThan n)
p Text
x = forall {k} (p :: Nat -> k) (n :: Nat) a.
(Typeable (p n), KnownNat n) =>
Proxy (p n)
-> (a, Text)
-> (a -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
sized Proxy (SizeGreaterThan n)
p (Text
x, Text
"Text") Text -> Int
Text.length (forall a. Ord a => a -> a -> Bool
(>), Text
"greater than")

-- | @since 0.5
instance (KnownNat n) => Predicate (SizeGreaterThan n) BS.ByteString where
  validate :: Proxy (SizeGreaterThan n) -> ByteString -> Maybe RefineException
validate Proxy (SizeGreaterThan n)
p ByteString
x = forall {k} (p :: Nat -> k) (n :: Nat) a.
(Typeable (p n), KnownNat n) =>
Proxy (p n)
-> (a, Text)
-> (a -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
sized Proxy (SizeGreaterThan n)
p (ByteString
x, Text
"ByteString") ByteString -> Int
BS.length (forall a. Ord a => a -> a -> Bool
(>), Text
"greater than")

-- | @since 0.5
instance (KnownNat n) => Predicate (SizeGreaterThan n) BL.ByteString where
  validate :: Proxy (SizeGreaterThan n) -> ByteString -> Maybe RefineException
validate Proxy (SizeGreaterThan n)
p ByteString
x = forall {k} (p :: Nat -> k) (n :: Nat) a.
(Typeable (p n), KnownNat n) =>
Proxy (p n)
-> (a, Text)
-> (a -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
sized Proxy (SizeGreaterThan n)
p (ByteString
x, Text
"ByteString") (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Int64
BL.length) (forall a. Ord a => a -> a -> Bool
(>), Text
"greater than")

--------------------------------------------------------------------------------

-- | A 'Predicate' ensuring that the value has a length
-- which is equal to the specified type-level number.
--
--   >>> isRight (refine @(SizeEqualTo 4) @[Int] [1,2,3,4])
--   True
--
--   >>> isLeft (refine @(SizeEqualTo 35) @[Int] [1,2,3,4])
--   True
--
--   >>> isRight (refine @(SizeEqualTo 4) @Text "four")
--   True
--
--   >>> isLeft (refine @(SizeEqualTo 35) @Text "four")
--   True
--
--   @since 0.2.0.0
data SizeEqualTo (n :: Nat)
  = SizeEqualTo -- ^ @since 0.4.2
  deriving
    ( forall (n :: Nat) x. Rep (SizeEqualTo n) x -> SizeEqualTo n
forall (n :: Nat) x. SizeEqualTo n -> Rep (SizeEqualTo n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (n :: Nat) x. Rep (SizeEqualTo n) x -> SizeEqualTo n
$cfrom :: forall (n :: Nat) x. SizeEqualTo n -> Rep (SizeEqualTo n) x
Generic -- ^ @since 0.3.0.0
    )

-- | @since 0.2.0.0
instance (Foldable t, KnownNat n) => Predicate (SizeEqualTo n) (t a) where
  validate :: Proxy (SizeEqualTo n) -> t a -> Maybe RefineException
validate Proxy (SizeEqualTo n)
p t a
x = forall {k} (p :: Nat -> k) (n :: Nat) a.
(Typeable (p n), KnownNat n) =>
Proxy (p n)
-> (a, Text)
-> (a -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
sized Proxy (SizeEqualTo n)
p (t a
x, Text
"Foldable") forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Eq a => a -> a -> Bool
(==), Text
"equal to")

-- | @since 0.5
instance (KnownNat n) => Predicate (SizeEqualTo n) Text where
  validate :: Proxy (SizeEqualTo n) -> Text -> Maybe RefineException
validate Proxy (SizeEqualTo n)
p Text
x = forall {k} (p :: Nat -> k) (n :: Nat) a.
(Typeable (p n), KnownNat n) =>
Proxy (p n)
-> (a, Text)
-> (a -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
sized Proxy (SizeEqualTo n)
p (Text
x, Text
"Text") Text -> Int
Text.length (forall a. Eq a => a -> a -> Bool
(==), Text
"equal to")

-- | @since 0.5
instance (KnownNat n) => Predicate (SizeEqualTo n) BS.ByteString where
  validate :: Proxy (SizeEqualTo n) -> ByteString -> Maybe RefineException
validate Proxy (SizeEqualTo n)
p ByteString
x = forall {k} (p :: Nat -> k) (n :: Nat) a.
(Typeable (p n), KnownNat n) =>
Proxy (p n)
-> (a, Text)
-> (a -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
sized Proxy (SizeEqualTo n)
p (ByteString
x, Text
"ByteString") ByteString -> Int
BS.length (forall a. Eq a => a -> a -> Bool
(==), Text
"equal to")

-- | @since 0.5
instance (KnownNat n) => Predicate (SizeEqualTo n) BL.ByteString where
  validate :: Proxy (SizeEqualTo n) -> ByteString -> Maybe RefineException
validate Proxy (SizeEqualTo n)
p ByteString
x = forall {k} (p :: Nat -> k) (n :: Nat) a.
(Typeable (p n), KnownNat n) =>
Proxy (p n)
-> (a, Text)
-> (a -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
sized Proxy (SizeEqualTo n)
p (ByteString
x, Text
"ByteString") (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Int64
BL.length) (forall a. Eq a => a -> a -> Bool
(==), Text
"equal to")

--------------------------------------------------------------------------------

-- | A 'Predicate' ensuring that the 'Foldable' contains elements
-- in a strictly ascending order.
--
--   >>> isRight (refine @Ascending @[Int] [5, 8, 13, 21, 34])
--   True
--
--   >>> isLeft (refine @Ascending @[Int] [34, 21, 13, 8, 5])
--   True
--
--   @since 0.2.0.0
data Ascending
  = Ascending -- ^ @since 0.4.2
  deriving
    ( forall x. Rep Ascending x -> Ascending
forall x. Ascending -> Rep Ascending x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Ascending x -> Ascending
$cfrom :: forall x. Ascending -> Rep Ascending x
Generic -- ^ @since 0.3.0.0
    )

-- | @since 0.2.0.0
instance (Foldable t, Ord a) => Predicate Ascending (t a) where
  validate :: Proxy Ascending -> t a -> Maybe RefineException
validate Proxy Ascending
p t a
x = do
    if forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> Bool
increasing t a
x
    then forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy Ascending
p)
         Text
"Foldable is not in ascending order."

--------------------------------------------------------------------------------

-- | A 'Predicate' ensuring that the 'Foldable' contains elements
-- in a strictly descending order.
--
--   >>> isRight (refine @Descending @[Int] [34, 21, 13, 8, 5])
--   True
--
--   >>> isLeft (refine @Descending @[Int] [5, 8, 13, 21, 34])
--   True
--
--   @since 0.2.0.0
data Descending
  = Descending -- ^ @since 0.4.2
  deriving
    ( forall x. Rep Descending x -> Descending
forall x. Descending -> Rep Descending x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Descending x -> Descending
$cfrom :: forall x. Descending -> Rep Descending x
Generic -- ^ @since 0.3.0.0
    )

-- | @since 0.2.0.0
instance (Foldable t, Ord a) => Predicate Descending (t a) where
  validate :: Proxy Descending -> t a -> Maybe RefineException
validate Proxy Descending
p t a
x = do
    if forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> Bool
decreasing t a
x
    then forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
        (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy Descending
p)
        Text
"Foldable is not in descending order."

--------------------------------------------------------------------------------

-- | A 'Predicate' ensuring that the value is less than the
--   specified type-level number.
--
--   >>> isRight (refine @(LessThan 12) @Int 11)
--   True
--
--   >>> isLeft (refine @(LessThan 12) @Int 12)
--   True
--
--   @since 0.1.0.0
data LessThan (n :: Nat)
  = LessThan -- ^ @since 0.4.2
  deriving
    ( forall (n :: Nat) x. Rep (LessThan n) x -> LessThan n
forall (n :: Nat) x. LessThan n -> Rep (LessThan n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (n :: Nat) x. Rep (LessThan n) x -> LessThan n
$cfrom :: forall (n :: Nat) x. LessThan n -> Rep (LessThan n) x
Generic -- ^ @since 0.3.0.0
    )

-- | @since 0.1.0.0
instance (Ord x, Num x, KnownNat n) => Predicate (LessThan n) x where
  validate :: Proxy (LessThan n) -> x -> Maybe RefineException
validate Proxy (LessThan n)
p x
x = do
    let n :: Integer
n = forall (n :: Nat). KnownNat n => Integer
nv @n
    let x' :: x
x' = forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n
    if x
x forall a. Ord a => a -> a -> Bool
< x
x'
    then forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (LessThan n)
p)
         (Text
"Value is not less than " forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Text
i2text Integer
n)

--------------------------------------------------------------------------------

-- | A 'Predicate' ensuring that the value is greater than the
--   specified type-level number.
--
--   >>> isRight (refine @(GreaterThan 65) @Int 67)
--   True
--
--   >>> isLeft (refine @(GreaterThan 65) @Int 65)
--   True
--
--   @since 0.1.0.0
data GreaterThan (n :: Nat)
  = GreaterThan -- ^ @since 0.4.2
  deriving
    ( forall (n :: Nat) x. Rep (GreaterThan n) x -> GreaterThan n
forall (n :: Nat) x. GreaterThan n -> Rep (GreaterThan n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (n :: Nat) x. Rep (GreaterThan n) x -> GreaterThan n
$cfrom :: forall (n :: Nat) x. GreaterThan n -> Rep (GreaterThan n) x
Generic -- ^ @since 0.3.0.0
    )

-- | @since 0.1.0.0
instance (Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x where
  validate :: Proxy (GreaterThan n) -> x -> Maybe RefineException
validate Proxy (GreaterThan n)
p x
x = do
    let n :: Integer
n = forall (n :: Nat). KnownNat n => Integer
nv @n
    let x' :: x
x' = forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n
    if x
x forall a. Ord a => a -> a -> Bool
> x
x'
    then forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (GreaterThan n)
p)
         (Text
"Value is not greater than " forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Text
i2text Integer
n)

--------------------------------------------------------------------------------

-- | A 'Predicate' ensuring that the value is greater than or equal to the
--   specified type-level number.
--
--   >>> isRight (refine @(From 9) @Int 10)
--   True
--
--   >>> isRight (refine @(From 10) @Int 10)
--   True
--
--   >>> isLeft (refine @(From 11) @Int 10)
--   True
--
--   @since 0.1.2
data From (n :: Nat)
  = From -- ^ @since 0.4.2
  deriving
    ( forall (n :: Nat) x. Rep (From n) x -> From n
forall (n :: Nat) x. From n -> Rep (From n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (n :: Nat) x. Rep (From n) x -> From n
$cfrom :: forall (n :: Nat) x. From n -> Rep (From n) x
Generic -- ^ @since 0.3.0.0
    )

-- | @since 0.1.2
instance (Ord x, Num x, KnownNat n) => Predicate (From n) x where
  validate :: Proxy (From n) -> x -> Maybe RefineException
validate Proxy (From n)
p x
x = do
    let n :: Integer
n = forall (n :: Nat). KnownNat n => Integer
nv @n
    let x' :: x
x' = forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n
    if x
x forall a. Ord a => a -> a -> Bool
>= x
x'
    then forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (From n)
p)
         (Text
"Value is less than " forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Text
i2text Integer
n)

--------------------------------------------------------------------------------

-- | A 'Predicate' ensuring that the value is less than or equal to the
--   specified type-level number.
--
--   >>> isRight (refine @(To 23) @Int 17)
--   True
--
--   >>> isLeft (refine @(To 17) @Int 23)
--   True
--
--   @since 0.1.2
data To (n :: Nat)
  = To -- ^ @since 0.4.2
  deriving
    ( forall (n :: Nat) x. Rep (To n) x -> To n
forall (n :: Nat) x. To n -> Rep (To n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (n :: Nat) x. Rep (To n) x -> To n
$cfrom :: forall (n :: Nat) x. To n -> Rep (To n) x
Generic -- ^ @since 0.3.0.0
    )

-- | @since 0.1.2
instance (Ord x, Num x, KnownNat n) => Predicate (To n) x where
  validate :: Proxy (To n) -> x -> Maybe RefineException
validate Proxy (To n)
p x
x = do
    let n :: Integer
n = forall (n :: Nat). KnownNat n => Integer
nv @n
    let x' :: x
x' = forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n
    if x
x forall a. Ord a => a -> a -> Bool
<= x
x'
    then forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (To n)
p)
         (Text
"Value is greater than " forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Text
i2text Integer
n)

--------------------------------------------------------------------------------

-- | A 'Predicate' ensuring that the value is within an inclusive range.
--
--   >>> isRight (refine @(FromTo 0 16) @Int 13)
--   True
--
--   >>> isRight (refine @(FromTo 13 15) @Int 13)
--   True
--
--   >>> isRight (refine @(FromTo 13 15) @Int 15)
--   True
--
--   >>> isLeft (refine @(FromTo 13 15) @Int 12)
--   True
--
--   @since 0.1.2
data FromTo (mn :: Nat) (mx :: Nat)
  = FromTo -- ^ @since 0.4.2
  deriving
    ( forall (mn :: Nat) (mx :: Nat) x.
Rep (FromTo mn mx) x -> FromTo mn mx
forall (mn :: Nat) (mx :: Nat) x.
FromTo mn mx -> Rep (FromTo mn mx) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (mn :: Nat) (mx :: Nat) x.
Rep (FromTo mn mx) x -> FromTo mn mx
$cfrom :: forall (mn :: Nat) (mx :: Nat) x.
FromTo mn mx -> Rep (FromTo mn mx) x
Generic-- ^ @since 0.3.0.0
    )

-- | @since 0.1.2
instance ( Ord x, Num x, KnownNat mn, KnownNat mx, mn <= mx
         ) => Predicate (FromTo mn mx) x where
  validate :: Proxy (FromTo mn mx) -> x -> Maybe RefineException
validate Proxy (FromTo mn mx)
p x
x = do
    let mn' :: Integer
mn' = forall (n :: Nat). KnownNat n => Integer
nv @mn
    let mx' :: Integer
mx' = forall (n :: Nat). KnownNat n => Integer
nv @mx
    if x
x forall a. Ord a => a -> a -> Bool
>= forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
mn' Bool -> Bool -> Bool
&& x
x forall a. Ord a => a -> a -> Bool
<= forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
mx'
    then forall a. Maybe a
Nothing
    else
      let msg :: Text
msg = [ Text
"Value is out of range (minimum: "
                , forall a. Integral a => a -> Text
i2text Integer
mn'
                , Text
", maximum: "
                , forall a. Integral a => a -> Text
i2text Integer
mx'
                , Text
")"
                ] forall a b. a -> (a -> b) -> b
|> forall a. Monoid a => [a] -> a
mconcat
      in TypeRep -> Text -> Maybe RefineException
throwRefineOtherException (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (FromTo mn mx)
p) Text
msg

--------------------------------------------------------------------------------

-- | A 'Predicate' ensuring that the value is equal to the specified
--   type-level number @n@.
--
--   >>> isRight (refine @(EqualTo 5) @Int 5)
--   True
--
--   >>> isLeft (refine @(EqualTo 6) @Int 5)
--   True
--
--   @since 0.1.0.0
data EqualTo (n :: Nat)
  = EqualTo -- ^ @since 0.4.2
  deriving
    ( forall (n :: Nat) x. Rep (EqualTo n) x -> EqualTo n
forall (n :: Nat) x. EqualTo n -> Rep (EqualTo n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (n :: Nat) x. Rep (EqualTo n) x -> EqualTo n
$cfrom :: forall (n :: Nat) x. EqualTo n -> Rep (EqualTo n) x
Generic -- ^ @since 0.3.0.0
    )

-- | @since 0.1.0.0
instance (Eq x, Num x, KnownNat n) => Predicate (EqualTo n) x where
  validate :: Proxy (EqualTo n) -> x -> Maybe RefineException
validate Proxy (EqualTo n)
p x
x = do
    let n :: Integer
n = forall (n :: Nat). KnownNat n => Integer
nv @n
    let x' :: x
x' = forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n
    if x
x forall a. Eq a => a -> a -> Bool
== x
x'
    then forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (EqualTo n)
p)
         (Text
"Value does not equal " forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Text
i2text Integer
n)

--------------------------------------------------------------------------------

-- | A 'Predicate' ensuring that the value is not equal to the specified
--   type-level number @n@.
--
--   >>> isRight (refine @(NotEqualTo 6) @Int 5)
--   True
--
--   >>> isLeft (refine @(NotEqualTo 5) @Int 5)
--   True
--
--   @since 0.2.0.0
data NotEqualTo (n :: Nat)
  = NotEqualTo -- ^ @since 0.4.2
  deriving
    ( forall (n :: Nat) x. Rep (NotEqualTo n) x -> NotEqualTo n
forall (n :: Nat) x. NotEqualTo n -> Rep (NotEqualTo n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (n :: Nat) x. Rep (NotEqualTo n) x -> NotEqualTo n
$cfrom :: forall (n :: Nat) x. NotEqualTo n -> Rep (NotEqualTo n) x
Generic -- ^ @since 0.3.0.0
    )

-- | @since 0.2.0.0
instance (Eq x, Num x, KnownNat n) => Predicate (NotEqualTo n) x where
  validate :: Proxy (NotEqualTo n) -> x -> Maybe RefineException
validate Proxy (NotEqualTo n)
p x
x = do
    let n :: Integer
n = forall (n :: Nat). KnownNat n => Integer
nv @n
    let x' :: x
x' = forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n
    if x
x forall a. Eq a => a -> a -> Bool
/= x
x'
    then forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (NotEqualTo n)
p)
         (Text
"Value does equal " forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Text
i2text Integer
n)

--------------------------------------------------------------------------------

-- | A 'Predicate' ensuring that the value is greater or equal than a negative
--   number specified as a type-level (positive) number @n@ and less than a
--   type-level (positive) number @m@.
--
--   >>> isRight (refine @(NegativeFromTo 5 12) @Int (-3))
--   True
--
--   >>> isLeft (refine @(NegativeFromTo 4 3) @Int (-5))
--   True
--
--   @since 0.4
data NegativeFromTo (n :: Nat) (m :: Nat)
  = NegativeFromTo -- ^ @since 0.4.2
  deriving
    ( forall (n :: Nat) (m :: Nat) x.
Rep (NegativeFromTo n m) x -> NegativeFromTo n m
forall (n :: Nat) (m :: Nat) x.
NegativeFromTo n m -> Rep (NegativeFromTo n m) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (n :: Nat) (m :: Nat) x.
Rep (NegativeFromTo n m) x -> NegativeFromTo n m
$cfrom :: forall (n :: Nat) (m :: Nat) x.
NegativeFromTo n m -> Rep (NegativeFromTo n m) x
Generic -- ^ @since 0.3.0.0
    )

-- | @since 0.4
instance (Ord x, Num x, KnownNat n, KnownNat m) => Predicate (NegativeFromTo n m) x where
  validate :: Proxy (NegativeFromTo n m) -> x -> Maybe RefineException
validate Proxy (NegativeFromTo n m)
p x
x = do
    let n' :: Integer
n' = forall (n :: Nat). KnownNat n => Integer
nv @n
    let m' :: Integer
m' = forall (n :: Nat). KnownNat n => Integer
nv @m
    if x
x forall a. Ord a => a -> a -> Bool
>= forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Num a => a -> a
negate Integer
n') Bool -> Bool -> Bool
&& x
x forall a. Ord a => a -> a -> Bool
<= forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
m'
    then forall a. Maybe a
Nothing
    else
      let msg :: Text
msg = [ Text
"Value is out of range (minimum: "
                , forall a. Integral a => a -> Text
i2text (forall a. Num a => a -> a
negate Integer
n')
                , Text
", maximum: "
                , forall a. Integral a => a -> Text
i2text Integer
m'
                , Text
")"
                ] forall a b. a -> (a -> b) -> b
|> forall a. Monoid a => [a] -> a
mconcat
      in TypeRep -> Text -> Maybe RefineException
throwRefineOtherException (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (NegativeFromTo n m)
p) Text
msg

--------------------------------------------------------------------------------

-- | A 'Predicate' ensuring that the value is divisible by @n@.
--
--   >>> isRight (refine @(DivisibleBy 3) @Int 12)
--   True
--
--   >>> isLeft (refine @(DivisibleBy 2) @Int 37)
--   True
--
--   @since 0.4.2
data DivisibleBy (n :: Nat)
  = DivisibleBy -- ^ @since 0.4.2
  deriving
    ( forall (n :: Nat) x. Rep (DivisibleBy n) x -> DivisibleBy n
forall (n :: Nat) x. DivisibleBy n -> Rep (DivisibleBy n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (n :: Nat) x. Rep (DivisibleBy n) x -> DivisibleBy n
$cfrom :: forall (n :: Nat) x. DivisibleBy n -> Rep (DivisibleBy n) x
Generic -- ^ @since 0.3.0.0
    )

-- | @since 0.4.2
instance (Integral x, KnownNat n) => Predicate (DivisibleBy n) x where
  validate :: Proxy (DivisibleBy n) -> x -> Maybe RefineException
validate Proxy (DivisibleBy n)
p x
x = do
    let n :: Integer
n = forall (n :: Nat). KnownNat n => Integer
nv @n
    let x' :: x
x' = forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n
    if x
x forall a. Integral a => a -> a -> a
`mod` x
x' forall a. Eq a => a -> a -> Bool
== x
0
    then forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (DivisibleBy n)
p)
         (Text
"Value is not divisible by " forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Text
i2text Integer
n)

--------------------------------------------------------------------------------

-- | A 'Predicate' ensuring that the value is odd.
--
--   >>> isRight (refine @Odd @Int 33)
--   True
--
--   >>> isLeft (refine @Odd @Int 32)
--   True
--
--   @since 0.4.2
data Odd
  = Odd -- ^ @since 0.4.2
  deriving
    ( forall x. Rep Odd x -> Odd
forall x. Odd -> Rep Odd x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Odd x -> Odd
$cfrom :: forall x. Odd -> Rep Odd x
Generic -- ^ @since 0.3.0.0
    )

-- | @since 0.4.2
instance (Integral x) => Predicate Odd x where
  validate :: Proxy Odd -> x -> Maybe RefineException
validate Proxy Odd
p x
x = do
    if forall a. Integral a => a -> Bool
odd x
x
    then forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy Odd
p)
         Text
"Value is not odd."

--------------------------------------------------------------------------------

-- | A 'Predicate' ensuring that the value is IEEE "not-a-number" (NaN).
--
--   >>> isRight (refine @NaN @Double (0/0))
--   True
--
--   >>> isLeft (refine @NaN @Double 13.9)
--   True
--
--   @since 0.5
data NaN
  = NaN -- ^ @since 0.5
  deriving
    ( forall x. Rep NaN x -> NaN
forall x. NaN -> Rep NaN x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep NaN x -> NaN
$cfrom :: forall x. NaN -> Rep NaN x
Generic -- ^ @since 0.5
    )

-- | @since 0.5
instance (RealFloat x) => Predicate NaN x where
  validate :: Proxy NaN -> x -> Maybe RefineException
validate Proxy NaN
p x
x = do
    if forall a. RealFloat a => a -> Bool
isNaN x
x
    then forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy NaN
p)
         Text
"Value is not IEEE \"not-a-number\" (NaN)."

--------------------------------------------------------------------------------

-- | A 'Predicate' ensuring that the value is IEEE infinity or negative infinity.
--
--   >>> isRight (refine @Infinite @Double (1/0))
--   True
--
--   >>> isRight (refine @Infinite @Double (-1/0))
--   True
--
--   >>> isLeft (refine @Infinite @Double 13.20)
--   True
--
--   @since 0.5
data Infinite
  = Infinite -- ^ @since 0.5
  deriving
    ( forall x. Rep Infinite x -> Infinite
forall x. Infinite -> Rep Infinite x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Infinite x -> Infinite
$cfrom :: forall x. Infinite -> Rep Infinite x
Generic -- ^ @since 0.5
    )

-- | @since 0.5
instance (RealFloat x) => Predicate Infinite x where
  validate :: Proxy Infinite -> x -> Maybe RefineException
validate Proxy Infinite
p x
x = do
    if forall a. RealFloat a => a -> Bool
isInfinite x
x
    then forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy Infinite
p)
         Text
"Value is not IEEE infinity or negative infinity."

--------------------------------------------------------------------------------

-- | A 'Predicate' ensuring that the value is even.
--
--   >>> isRight (refine @Even @Int 32)
--   True
--
--   >>> isLeft (refine @Even @Int 33)
--   True
--
--   @since 0.4.2
data Even
  = Even -- ^ @since 0.4.2
  deriving
    ( forall x. Rep Even x -> Even
forall x. Even -> Rep Even x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Even x -> Even
$cfrom :: forall x. Even -> Rep Even x
Generic -- ^ @since 0.4.2
    )

-- | @since 0.4.2
instance (Integral x) => Predicate Even x where
  validate :: Proxy Even -> x -> Maybe RefineException
validate Proxy Even
p x
x = do
    if forall a. Integral a => a -> Bool
even x
x
    then forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy Even
p)
         Text
"Value is not even."

--------------------------------------------------------------------------------

-- | A 'Predicate' ensuring that the value is greater than zero.
--
--   @since 0.1.0.0
type Positive = GreaterThan 0

-- | A 'Predicate' ensuring that the value is less than or equal to zero.
--
--   @since 0.1.2
type NonPositive = To 0

-- | A 'Predicate' ensuring that the value is less than zero.
--
--   @since 0.1.0.0
type Negative = LessThan 0

-- | A 'Predicate' ensuring that the value is greater than or equal to zero.
--
--   @since 0.1.2
type NonNegative = From 0

-- | An inclusive range of values from zero to one.
--
--   @since 0.1.0.0
type ZeroToOne = FromTo 0 1

-- | A 'Predicate' ensuring that the value is not equal to zero.
--
--   @since 0.2.0.0
type NonZero = NotEqualTo 0

-- | A 'Predicate' ensuring that the type is empty.
--
--   @since 0.5
type Empty = SizeEqualTo 0

-- | A 'Predicate' ensuring that the type is non-empty.
--
--   @since 0.2.0.0
type NonEmpty = SizeGreaterThan 0

--------------------------------------------------------------------------------

-- | A typeclass containing "safe" conversions between refined
--   predicates where the target is /weaker/ than the source:
--   that is, all values that satisfy the first predicate will
--   be guaranteed to satisfy the second.
--
--   Take care: writing an instance declaration for your custom
--   predicates is the same as an assertion that 'weaken' is
--   safe to use:
--
--   @
--   instance 'Weaken' Pred1 Pred2
--   @
--
--   For most of the instances, explicit type annotations for
--   the result value's type might be required.
--
-- @since 0.2.0.0
class Weaken from to where
  -- | @since 0.2.0.0
  weaken :: Refined from x -> Refined to x
  weaken = coerce :: forall a b. Coercible a b => a -> b
coerce

-- | @since 0.2.0.0
instance (n <= m)         => Weaken (LessThan n)    (LessThan m)
-- | @since 0.2.0.0
instance (n <= m)         => Weaken (LessThan n)    (To m)
-- | @since 0.2.0.0
instance (n <= m)         => Weaken (To n)          (To m)
-- | @since 0.2.0.0
instance (m <= n)         => Weaken (GreaterThan n) (GreaterThan m)
-- | @since 0.2.0.0
instance (m <= n)         => Weaken (GreaterThan n) (From m)
-- | @since 0.2.0.0
instance (m <= n)         => Weaken (From n)        (From m)
-- | @since 0.2.0.0
instance (p <= n, m <= q) => Weaken (FromTo n m)    (FromTo p q)
-- | @since 0.2.0.0
instance (p <= n)         => Weaken (FromTo n m)    (From p)
-- | @since 0.2.0.0
instance (m <= q)         => Weaken (FromTo n m)    (To q)

-- | This function helps type inference.
--   It is equivalent to the following:
--
-- @
-- instance Weaken (And l r) l
-- @
--
--   @since 0.2.0.0
andLeft :: Refined (And l r) x -> Refined l x
andLeft :: forall {k} {k} (l :: k) (r :: k) x.
Refined (And l r) x -> Refined l x
andLeft = coerce :: forall a b. Coercible a b => a -> b
coerce

-- | This function helps type inference.
--   It is equivalent to the following:
--
-- @
-- instance Weaken (And l r) r
-- @
--
--   @since 0.2.0.0
andRight :: Refined (And l r) x -> Refined r x
andRight :: forall {k} {k} (l :: k) (r :: k) x.
Refined (And l r) x -> Refined r x
andRight = coerce :: forall a b. Coercible a b => a -> b
coerce

-- | This function helps type inference.
--   It is equivalent to the following:
--
-- @
-- instance Weaken l (Or l r)
-- @
--
--   @since 0.2.0.0
leftOr :: Refined l x -> Refined (Or l r) x
leftOr :: forall {k} {k} (l :: k) x (r :: k).
Refined l x -> Refined (Or l r) x
leftOr = coerce :: forall a b. Coercible a b => a -> b
coerce

-- | This function helps type inference.
--   It is equivalent to the following:
--
-- @
-- instance Weaken r (Or l r)
-- @
--
--   @since 0.2.0.0
rightOr :: Refined r x -> Refined (Or l r) x
rightOr :: forall {k} {k} (r :: k) x (l :: k).
Refined r x -> Refined (Or l r) x
rightOr = coerce :: forall a b. Coercible a b => a -> b
coerce

-- | Strengthen a refinement by composing it with another.
--
--   @since 0.4.2.2
strengthen :: forall p p' x. (Predicate p x, Predicate p' x)
  => Refined p x
  -> Either RefineException (Refined (p && p') x)
strengthen :: forall {k} {k} (p :: k) (p' :: k) x.
(Predicate p x, Predicate p' x) =>
Refined p x -> Either RefineException (Refined (p && p') x)
strengthen Refined p x
r = do
  Refined x
x <- forall {k} (p :: k) x.
Predicate p x =>
x -> Either RefineException (Refined p x)
refine @p' @x (forall {k} (p :: k) x. Refined p x -> x
unrefine Refined p x
r)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k (p :: k) x. x -> Refined p x
Refined x
x)
{-# inlineable strengthen #-}

--------------------------------------------------------------------------------

-- | An exception encoding the way in which a 'Predicate' failed.
--
--   @since 0.2.0.0
data RefineException
  = -- | A 'RefineException' for failures involving the 'Not' predicate.
    --
    --   @since 0.2.0.0
    RefineNotException
    { RefineException -> TypeRep
_RefineException_typeRep   :: !TypeRep
      -- ^ The 'TypeRep' of the @'Not' p@ type.
    }

  | -- | A 'RefineException' for failures involving the 'And' predicate.
    --
    --   @since 0.2.0.0
    RefineAndException
    { _RefineException_typeRep   :: !TypeRep
      -- ^ The 'TypeRep' of the @'And' l r@ type.
    , RefineException -> These RefineException RefineException
_RefineException_andChild  :: !(These RefineException RefineException)
      -- ^ A 'These' encoding which branch(es) of the 'And' failed:
      --   if the 'RefineException' came from the @l@ predicate, then
      --   this will be 'This', if it came from the @r@ predicate, this
      --   will be 'That', and if it came from both @l@ and @r@, this
      --   will be 'These'.

      -- note to self: what am I, Dr. Seuss?
    }

  | -- | A 'RefineException' for failures involving the 'Or' predicate.
    --
    --   @since 0.2.0.0
    RefineOrException
    { _RefineException_typeRep   :: !TypeRep
      -- ^ The 'TypeRep' of the @'Or' l r@ type.
    , RefineException -> RefineException
_RefineException_orLChild  :: !RefineException
      -- ^ The 'RefineException' for the @l@ failure.
    , RefineException -> RefineException
_RefineException_orRChild  :: !RefineException
      -- ^ The 'RefineException' for the @l@ failure.
    }

  | -- | A 'RefineException' for failures involving the 'Xor' predicate.
    --
    --   @since 0.5
    RefineXorException
    { _RefineException_typeRep   :: !TypeRep
    , RefineException -> Maybe (RefineException, RefineException)
_RefineException_children  :: !(Maybe (RefineException, RefineException))
    }

  | -- | A 'RefineException' for failures involving all other predicates with custom exception.
    --
    --   @since 0.5
    RefineSomeException
    { _RefineException_typeRep   :: !TypeRep
      -- ^ The 'TypeRep' of the predicate that failed.
    , RefineException -> SomeException
_RefineException_Exception :: !SomeException
      -- ^ A custom exception.
    }

  | -- | A 'RefineException' for failures involving all other predicates.
    --
    --   @since 0.2.0.0
    RefineOtherException
    { _RefineException_typeRep   :: !TypeRep
      -- ^ The 'TypeRep' of the predicate that failed.
    , RefineException -> Text
_RefineException_message   :: !Text
      -- ^ A custom message to display.
    }
  deriving
    ( forall x. Rep RefineException x -> RefineException
forall x. RefineException -> Rep RefineException x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep RefineException x -> RefineException
$cfrom :: forall x. RefineException -> Rep RefineException x
Generic -- ^ @since 0.3.0.0
    )

-- | /Note/: Equivalent to @'displayRefineException'@.
--
--   @since 0.2.0.0
instance Show RefineException where
  show :: RefineException -> String
show = RefineException -> String
displayRefineException

-- | A Tree which is a bit easier to pretty-print
--   TODO: get rid of this
data ExceptionTree a
  = NodeNone
  | NodeSome !TypeRep SomeException
  | NodeOther !TypeRep !Text
  | NodeNot !TypeRep
  | NodeOr !TypeRep [ExceptionTree a]
  | NodeAnd !TypeRep [ExceptionTree a]
  | NodeXor !TypeRep [ExceptionTree a]

-- | pretty-print an 'ExceptionTree', contains a hack to
--   work differently whether or not you are "inGhc", i.e.
--   inside of refineTH/refineTH_ (because GHC messes with
--   the indentation)
showTree :: Bool -> ExceptionTree RefineException -> String
showTree :: Bool -> ExceptionTree RefineException -> String
showTree Bool
inGhc
  | Bool
inGhc = String
-> String -> String -> ExceptionTree RefineException -> [String]
showOne String
"" String
"" String
""
      forall a b c. (a -> b) -> (b -> c) -> a -> c
.> forall a. (a -> a) -> [a] -> [a]
mapOnTail (Int -> ShowS
indent Int
6)
      forall a b c. (a -> b) -> (b -> c) -> a -> c
.> [String] -> String
unlines
  | Bool
otherwise = String
-> String -> String -> ExceptionTree RefineException -> [String]
showOne String
"  " String
"" String
"" forall a b c. (a -> b) -> (b -> c) -> a -> c
.> [String] -> String
unlines
  where
    mapOnTail :: (a -> a) -> [a] -> [a]
    mapOnTail :: forall a. (a -> a) -> [a] -> [a]
mapOnTail a -> a
f = \case
      [] -> []
      (a
a : [a]
as) -> a
a forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map a -> a
f [a]
as

    indent :: Int -> String -> String
    indent :: Int -> ShowS
indent Int
n String
s = forall a. Int -> a -> [a]
replicate Int
n Char
' ' forall a. [a] -> [a] -> [a]
++ String
s

    showOne :: String -> String -> String -> ExceptionTree RefineException -> [String]
    showOne :: String
-> String -> String -> ExceptionTree RefineException -> [String]
showOne String
leader String
tie String
arm = \case
      ExceptionTree RefineException
NodeNone ->
        [
        ]
      NodeSome TypeRep
tr SomeException
e ->
        [ String
leader
          forall a. Semigroup a => a -> a -> a
<> String
arm
          forall a. Semigroup a => a -> a -> a
<> String
tie
          forall a. Semigroup a => a -> a -> a
<> String
"The predicate ("
          forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show TypeRep
tr
          forall a. Semigroup a => a -> a -> a
<> String
") failed with the exception: "
          forall a. Semigroup a => a -> a -> a
<> forall e. Exception e => e -> String
displayException SomeException
e
        ]
      NodeOther TypeRep
tr Text
p ->
        [ String
leader
          forall a. Semigroup a => a -> a -> a
<> String
arm
          forall a. Semigroup a => a -> a -> a
<> String
tie
          forall a. Semigroup a => a -> a -> a
<> String
"The predicate ("
          forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show TypeRep
tr
          forall a. Semigroup a => a -> a -> a
<> String
") failed with the message: "
          forall a. Semigroup a => a -> a -> a
<> Text -> String
Text.unpack Text
p
        ]
      NodeNot TypeRep
tr ->
        [ String
leader
          forall a. Semigroup a => a -> a -> a
<> String
arm
          forall a. Semigroup a => a -> a -> a
<> String
tie
          forall a. Semigroup a => a -> a -> a
<> String
"The predicate ("
          forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show TypeRep
tr
          forall a. Semigroup a => a -> a -> a
<> String
") does not hold"
        ]
      NodeOr TypeRep
tr [ExceptionTree RefineException]
rest -> TypeRep -> String
nodeRep TypeRep
tr forall a. a -> [a] -> [a]
: [ExceptionTree RefineException] -> String -> [String]
showChildren [ExceptionTree RefineException]
rest (String
leader forall a. Semigroup a => a -> a -> a
<> String
extension)
      NodeAnd TypeRep
tr [ExceptionTree RefineException]
rest -> TypeRep -> String
nodeRep TypeRep
tr forall a. a -> [a] -> [a]
: [ExceptionTree RefineException] -> String -> [String]
showChildren [ExceptionTree RefineException]
rest (String
leader forall a. Semigroup a => a -> a -> a
<> String
extension)
      -- can be empty since both can be satisfied
      NodeXor TypeRep
tr [] ->
        [ String
leader
          forall a. Semigroup a => a -> a -> a
<> String
arm
          forall a. Semigroup a => a -> a -> a
<> String
tie
          forall a. Semigroup a => a -> a -> a
<> String
"The predicate ("
          forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show TypeRep
tr
          forall a. Semigroup a => a -> a -> a
<> String
") does not hold, because both predicates were satisfied"
        ]
      NodeXor TypeRep
tr [ExceptionTree RefineException]
rest -> TypeRep -> String
nodeRep TypeRep
tr forall a. a -> [a] -> [a]
: [ExceptionTree RefineException] -> String -> [String]
showChildren [ExceptionTree RefineException]
rest (String
leader forall a. Semigroup a => a -> a -> a
<> String
extension)
      where
        nodeRep :: TypeRep -> String
        -- TODO: make tr bold
        nodeRep :: TypeRep -> String
nodeRep TypeRep
tr = String
leader forall a. Semigroup a => a -> a -> a
<> String
arm forall a. Semigroup a => a -> a -> a
<> String
tie forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show TypeRep
tr

        extension :: String
        extension :: String
extension = case String
arm of
          String
""  -> String
""
          String
"└" -> String
"    "
          String
_   -> String
"│   "

    showChildren :: [ExceptionTree RefineException] -> String -> [String]
    showChildren :: [ExceptionTree RefineException] -> String -> [String]
showChildren [ExceptionTree RefineException]
children String
leader =
      let arms :: [String]
arms = forall a. Int -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExceptionTree RefineException]
children forall a. Num a => a -> a -> a
- Int
1) String
"├" forall a. Semigroup a => a -> a -> a
<> [String
"└"]
      in forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (String
-> String -> String -> ExceptionTree RefineException -> [String]
showOne String
leader String
"── ") [String]
arms [ExceptionTree RefineException]
children)

refineExceptionToTree :: RefineException -> ExceptionTree RefineException
refineExceptionToTree :: RefineException -> ExceptionTree RefineException
refineExceptionToTree = forall {k} {a :: k}. RefineException -> ExceptionTree a
go
  where
    go :: RefineException -> ExceptionTree a
go = \case
      RefineSomeException TypeRep
tr SomeException
e -> forall {k} (a :: k). TypeRep -> SomeException -> ExceptionTree a
NodeSome TypeRep
tr SomeException
e
      RefineOtherException TypeRep
tr Text
p -> forall {k} (a :: k). TypeRep -> Text -> ExceptionTree a
NodeOther TypeRep
tr Text
p
      RefineNotException TypeRep
tr -> forall {k} (a :: k). TypeRep -> ExceptionTree a
NodeNot TypeRep
tr
      RefineOrException TypeRep
tr RefineException
l RefineException
r -> forall {k} (a :: k).
TypeRep -> [ExceptionTree a] -> ExceptionTree a
NodeOr TypeRep
tr [RefineException -> ExceptionTree a
go RefineException
l, RefineException -> ExceptionTree a
go RefineException
r]
      RefineAndException TypeRep
tr (This RefineException
l) -> forall {k} (a :: k).
TypeRep -> [ExceptionTree a] -> ExceptionTree a
NodeAnd TypeRep
tr [RefineException -> ExceptionTree a
go RefineException
l]
      RefineAndException TypeRep
tr (That RefineException
r) -> forall {k} (a :: k).
TypeRep -> [ExceptionTree a] -> ExceptionTree a
NodeAnd TypeRep
tr [RefineException -> ExceptionTree a
go RefineException
r]
      RefineAndException TypeRep
tr (These RefineException
l RefineException
r) -> forall {k} (a :: k).
TypeRep -> [ExceptionTree a] -> ExceptionTree a
NodeAnd TypeRep
tr [RefineException -> ExceptionTree a
go RefineException
l, RefineException -> ExceptionTree a
go RefineException
r]
      RefineXorException TypeRep
tr Maybe (RefineException, RefineException)
Nothing -> forall {k} (a :: k).
TypeRep -> [ExceptionTree a] -> ExceptionTree a
NodeXor TypeRep
tr []
      RefineXorException TypeRep
tr (Just (RefineException
l, RefineException
r)) -> forall {k} (a :: k).
TypeRep -> [ExceptionTree a] -> ExceptionTree a
NodeXor TypeRep
tr [RefineException -> ExceptionTree a
go RefineException
l, RefineException -> ExceptionTree a
go RefineException
r]

-- | Display a 'RefineException' as @'String'@
--
--   This function can be extremely useful for debugging
--   @'RefineException's@, especially deeply nested ones.
--
--   Consider:
--
--   @
--   myRefinement = refine
--     \@(And
--         (Not (LessThan 5))
--         (Xor
--           (DivisibleBy 10)
--           (And
--             (EqualTo 4)
--             (EqualTo 3)
--           )
--         )
--      )
--     \@Int
--     3
--   @
--
--   This function will show the following tree structure, recursively breaking down
--   every issue:
--
--   @
--   And (Not (LessThan 5)) (Xor (EqualTo 4) (And (EqualTo 4) (EqualTo 3)))
--   ├── The predicate (Not (LessThan 5)) does not hold.
--   └── Xor (DivisibleBy 10) (And (EqualTo 4) (EqualTo 3))
--       ├── The predicate (DivisibleBy 10) failed with the message: Value is not divisible by 10
--       └── And (EqualTo 4) (EqualTo 3)
--           └── The predicate (EqualTo 4) failed with the message: Value does not equal 4
--   @
--
--   /Note/: Equivalent to @'show' \@'RefineException'@
--
--   @since 0.2.0.0
displayRefineException :: RefineException -> String
displayRefineException :: RefineException -> String
displayRefineException = RefineException -> ExceptionTree RefineException
refineExceptionToTree forall a b c. (a -> b) -> (b -> c) -> a -> c
.> Bool -> ExceptionTree RefineException -> String
showTree Bool
False

-- | Encode a 'RefineException' for use with \Control.Exception\.
--
--   /Note/: Equivalent to @'displayRefineException'@.
--
--   @since 0.2.0.0
instance Exception RefineException where
  displayException :: RefineException -> String
displayException = forall a. Show a => a -> String
show

--------------------------------------------------------------------------------

-- | A handler for a @'RefineException'@.
--
--   'throwRefineOtherException' is useful for defining what
--   behaviour 'validate' should have in the event of a predicate failure.
--
--   Typically the first argument passed to this function
--   will be the result of applying 'typeRep' to the first
--   argument of 'validate'.
--
--   @since 0.2.0.0
throwRefineOtherException
  :: TypeRep
  -- ^ The 'TypeRep' of the 'Predicate'. This can usually be given by using 'typeRep'.
  -> Text
  -- ^ A 'PP.Doc' 'Void' encoding a custom error message to be pretty-printed.
  -> Maybe RefineException
throwRefineOtherException :: TypeRep -> Text -> Maybe RefineException
throwRefineOtherException TypeRep
rep
  = TypeRep -> Text -> RefineException
RefineOtherException TypeRep
rep forall a b c. (a -> b) -> (b -> c) -> a -> c
.> forall a. a -> Maybe a
Just

-- | A handler for a @'RefineException'@.
--
--   'throwRefineSomeException' is useful for defining what
--   behaviour 'validate' should have in the event of a predicate failure
--   with a specific exception.
--
--   @since 0.5
throwRefineSomeException
  :: TypeRep
  -- ^ The 'TypeRep' of the 'Predicate'. This can usually be given by using 'typeRep'.
  -> SomeException
  -- ^ A custom exception.
  -> Maybe RefineException
throwRefineSomeException :: TypeRep -> SomeException -> Maybe RefineException
throwRefineSomeException TypeRep
rep
  = TypeRep -> SomeException -> RefineException
RefineSomeException TypeRep
rep forall a b c. (a -> b) -> (b -> c) -> a -> c
.> forall a. a -> Maybe a
Just

-- | An implementation of 'validate' that always succeeds.
--
--   ==== __Examples__
--
--   @
--   data ContainsLetterE = ContainsLetterE
--
--   instance Predicate ContainsLetterE 'Text' where
--     validate p t
--       | 'Data.Text.any' (== \'e\') t = 'success'
--       | otherwise = Just $ 'throwRefineException' (typeRep p) "Text doesn't contain letter \'e\'".
--   @
--
--   @since 0.5
success
  :: Maybe RefineException
success :: Maybe RefineException
success
  = forall a. Maybe a
Nothing

--------------------------------------------------------------------------------

-- | Helper function for sized predicates.
sized :: forall p n a. (Typeable (p n), KnownNat n)
  => Proxy (p n)
     -- ^ predicate
  -> (a, Text)
     -- ^ (value, type)
  -> (a -> Int)
     -- ^ length of value
  -> (Int -> Int -> Bool, Text)
     -- ^ (compare :: Length -> KnownNat -> Bool, comparison string)
  -> Maybe RefineException
sized :: forall {k} (p :: Nat -> k) (n :: Nat) a.
(Typeable (p n), KnownNat n) =>
Proxy (p n)
-> (a, Text)
-> (a -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
sized Proxy (p n)
p (a
x, Text
typ) a -> Int
lenF (Int -> Int -> Bool
cmp, Text
cmpDesc) = do
  let x' :: Int
x' = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Nat). KnownNat n => Integer
nv @n)
  let sz :: Int
sz = a -> Int
lenF a
x
  if Int -> Int -> Bool
cmp Int
sz Int
x'
  then forall a. Maybe a
Nothing
  else
    let msg :: Text
msg =
          [ Text
"Size of ", Text
typ, Text
" is not ", Text
cmpDesc, Text
" "
          , forall a. Integral a => a -> Text
i2text Int
x'
          , Text
". "
          , Text
"Size is: "
          , forall a. Integral a => a -> Text
i2text Int
sz
          ] forall a b. a -> (a -> b) -> b
|> forall a. Monoid a => [a] -> a
mconcat
    in TypeRep -> Text -> Maybe RefineException
throwRefineOtherException (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (p n)
p) Text
msg

-- helper function to make sure natVal calls are
-- zero runtime overhead
nv :: forall n. KnownNat n => Integer
nv :: forall (n :: Nat). KnownNat n => Integer
nv = forall (n :: Nat). KnownNat n => Proxy# n -> Integer
natVal' (forall {k} (a :: k). Proxy# a
proxy# :: Proxy# n)

-- convert an Integral number to Text
--
-- todo: use toLazyTextWith, providing a tiny buffer size
i2text :: Integral a => a -> Text
i2text :: forall a. Integral a => a -> Text
i2text = forall a. Integral a => a -> Builder
TextBuilder.decimal
  forall a b c. (a -> b) -> (b -> c) -> a -> c
.> Builder -> Text
TextBuilder.toLazyText
  forall a b c. (a -> b) -> (b -> c) -> a -> c
.> Text -> Text
TextLazy.toStrict
{-# SPECIALISE i2text :: Int -> Text #-}
{-# SPECIALISE i2text :: Integer -> Text #-}