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

-- 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 RoleAnnotations            #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TemplateHaskell            #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE TypeOperators              #-}

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

-- | 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
  , 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)
import           Data.Foldable                (foldl')
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(parseJSON), ToJSON(toJSON))
#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
|> :: a -> (a -> b) -> b
(|>) = ((a -> b) -> a -> b) -> a -> (a -> b) -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($)
{-# INLINE (|>) #-}

-- | Helper function, stolen from the flow package.
(.>) :: (a -> b) -> (b -> c) -> a -> c
a -> b
f .> :: (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 :: Ordered a -> Bool
inc (Decreasing a
_) = Bool
False
inc Ordered a
_              = Bool
True
{-# INLINE inc #-}

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

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

decreasing :: (Foldable t, Ord a) => t a -> Bool
decreasing :: t a -> Bool
decreasing = Ordered a -> Bool
forall a. Ordered a -> Bool
dec (Ordered a -> Bool) -> (t a -> Ordered a) -> t a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ordered a -> a -> Ordered a) -> Ordered a -> t a -> Ordered a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Ordered a -> a -> Ordered a
forall a. Ord a => Ordered a -> a -> Ordered a
go Ordered a
forall a. Ordered a
Empty where
  go :: Ordered a -> a -> Ordered a
go Ordered a
Empty a
y = a -> Ordered a
forall a. a -> Ordered a
Decreasing a
y
  go (Increasing a
x) a
_ = a -> Ordered a
forall a. a -> Ordered a
Increasing a
x
  go (Decreasing a
x) a
y
    | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
y = a -> Ordered a
forall a. a -> Ordered a
Decreasing a
y
    | Bool
otherwise = a -> Ordered a
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 = Bool -> ReadS (Refined p x) -> ReadS (Refined p x)
forall a. Bool -> ReadS a -> ReadS a
readParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ReadS (Refined p x) -> ReadS (Refined p x))
-> ReadS (Refined p x) -> ReadS (Refined p x)
forall a b. (a -> b) -> a -> b
$ \String
r1 -> do
    (String
"Refined", String
r2) <- ReadS String
lex String
r1
    (x
raw,       String
r3) <- Int -> ReadS x
forall a. Read a => Int -> ReadS a
readsPrec Int
11 String
r2
    case x -> Either RefineException (Refined p x)
forall p 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 = a -> Parser (Refined p a)
forall p x (m :: * -> *).
(Predicate p x, MonadFail m) =>
x -> m (Refined p x)
refineFail (a -> Parser (Refined p a))
-> (Value -> Parser a) -> Value -> Parser (Refined p a)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Value -> Parser a
forall a. FromJSON a => Value -> Parser a
parseJSON

-- | @since 0.4
instance (ToJSON a, Predicate p a) => ToJSON (Refined p a) where
  toJSON :: Refined p a -> Value
toJSON = a -> Value
forall a. ToJSON a => a -> Value
toJSON (a -> Value) -> (Refined p a -> a) -> Refined p a -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined p a -> a
forall p x. Refined p x -> x
unrefine
#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 Gen a
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
100 = do
            Maybe (Refined p a)
m <- Gen a -> Gen (Maybe (Refined p a))
forall p 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
                Refined p a -> Gen (Refined p a)
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Gen a
gen
        | Bool
otherwise = String -> Gen (Refined p a)
forall a. HasCallStack => String -> a
error (Proxy p -> Proxy a -> String
forall p a.
(Typeable p, Typeable a) =>
Proxy p -> Proxy a -> String
refinedGenError (Proxy p
forall k (t :: k). Proxy t
Proxy @p) (Proxy a
forall k (t :: k). Proxy t
Proxy @a))

refinedGenError :: (Typeable p, Typeable a)
  => Proxy p -> Proxy a -> String
refinedGenError :: Proxy p -> Proxy a -> String
refinedGenError Proxy p
p Proxy a
a = String
"arbitrary :: Refined ("
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Proxy p -> String
forall a. Typeable a => Proxy a -> String
typeName Proxy p
p
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") ("
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Proxy a -> String
forall a. Typeable a => Proxy a -> String
typeName Proxy a
a
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"): Failed to generate a value that satisfied"
  String -> String -> String
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 :: Gen a -> Gen (Maybe (Refined p a))
suchThatRefined Gen a
gen = do
  Maybe a
m <- Gen a -> (a -> Bool) -> Gen (Maybe a)
forall a. Gen a -> (a -> Bool) -> Gen (Maybe a)
QC.suchThatMaybe Gen a
gen (Predicate p a => a -> Bool
forall p a. Predicate p a => a -> Bool
reifyPredicate @p @a)
  case Maybe a
m of
    Maybe a
Nothing -> Maybe (Refined p a) -> Gen (Maybe (Refined p a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Refined p a)
forall a. Maybe a
Nothing
    Just a
x -> Maybe (Refined p a) -> Gen (Maybe (Refined p a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Refined p a -> Maybe (Refined p a)
forall a. a -> Maybe a
Just (a -> Refined p a
forall p x. x -> Refined p x
Refined a
x))

typeName :: Typeable a => Proxy a -> String
typeName :: Proxy a -> String
typeName = (TypeRep -> String -> String) -> String -> TypeRep -> String
forall a b c. (a -> b -> c) -> b -> a -> c
flip TypeRep -> String -> String
showsTypeRep String
"" (TypeRep -> String) -> (Proxy a -> TypeRep) -> Proxy a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy a -> TypeRep
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 :: x -> Either RefineException (Refined p x)
refine x
x = Either RefineException (Refined p x)
-> (RefineException -> Either RefineException (Refined p x))
-> Maybe RefineException
-> Either RefineException (Refined p x)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Refined p x -> Either RefineException (Refined p x)
forall a b. b -> Either a b
Right (x -> Refined p x
forall p x. x -> Refined p x
Refined x
x)) RefineException -> Either RefineException (Refined p x)
forall a b. a -> Either a b
Left (Proxy p -> x -> Maybe RefineException
forall p x. Predicate p x => Proxy p -> x -> Maybe RefineException
validate (Proxy p
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_ :: x -> Either RefineException x
refine_ = Predicate p x => x -> Either RefineException (Refined p x)
forall p x.
Predicate p x =>
x -> Either RefineException (Refined p x)
refine @p @x (x -> Either RefineException (Refined p x))
-> (Either RefineException (Refined p x)
    -> Either RefineException x)
-> x
-> Either RefineException x
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> Either RefineException (Refined p x) -> Either RefineException x
coerce
{-# INLINABLE refine_ #-}

-- | Constructs a 'Refined' value at run-time,
--   calling 'Control.Monad.Catch.throwM' if the value
--   does not satisfy the predicate.
--
--   @since 0.2.0.0
refineThrow :: (Predicate p x, MonadThrow m) => x -> m (Refined p x)
refineThrow :: x -> m (Refined p x)
refineThrow = x -> Either RefineException (Refined p x)
forall p x.
Predicate p x =>
x -> Either RefineException (Refined p x)
refine (x -> Either RefineException (Refined p x))
-> (Either RefineException (Refined p x) -> m (Refined p x))
-> x
-> m (Refined p x)
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> (RefineException -> m (Refined p x))
-> (Refined p x -> m (Refined p x))
-> Either RefineException (Refined p x)
-> m (Refined p x)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either RefineException -> m (Refined p x)
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
MonadThrow.throwM Refined p x -> m (Refined p x)
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 :: x -> m (Refined p x)
refineFail = x -> Either RefineException (Refined p x)
forall p x.
Predicate p x =>
x -> Either RefineException (Refined p x)
refine (x -> Either RefineException (Refined p x))
-> (Either RefineException (Refined p x) -> m (Refined p x))
-> x
-> m (Refined p x)
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> (RefineException -> m (Refined p x))
-> (Refined p x -> m (Refined p x))
-> Either RefineException (Refined p x)
-> m (Refined p x)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (RefineException -> String
forall e. Exception e => e -> String
displayException (RefineException -> String)
-> (String -> m (Refined p x))
-> RefineException
-> m (Refined p x)
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> String -> m (Refined p x)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail) Refined p x -> m (Refined p x)
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 :: x -> m (Refined p x)
refineError = x -> Either RefineException (Refined p x)
forall p x.
Predicate p x =>
x -> Either RefineException (Refined p x)
refine (x -> Either RefineException (Refined p x))
-> (Either RefineException (Refined p x) -> m (Refined p x))
-> x
-> m (Refined p x)
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> (RefineException -> m (Refined p x))
-> (Refined p x -> m (Refined p x))
-> Either RefineException (Refined p x)
-> m (Refined p x)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either RefineException -> m (Refined p x)
forall e (m :: * -> *) a. MonadError e m => e -> m a
MonadError.throwError Refined p x -> m (Refined p x)
forall (f :: * -> *) a. Applicative f => a -> f a
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
--
--   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
refineTH :: forall p x. (Predicate p x, TH.Lift x) => x -> TH.Q (TH.TExp (Refined p x))
refineTH :: x -> Q (TExp (Refined p x))
refineTH =
  let showException :: RefineException -> Q a
showException = RefineException -> ExceptionTree RefineException
refineExceptionToTree
        (RefineException -> ExceptionTree RefineException)
-> (ExceptionTree RefineException -> String)
-> RefineException
-> String
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> Bool -> ExceptionTree RefineException -> String
showTree Bool
True
        (RefineException -> String)
-> (String -> Q a) -> RefineException -> Q a
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail
  in Predicate p x => x -> Either RefineException (Refined p x)
forall p x.
Predicate p x =>
x -> Either RefineException (Refined p x)
refine @p @x
     (x -> Either RefineException (Refined p x))
-> (Either RefineException (Refined p x) -> Q Exp) -> x -> Q Exp
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> (RefineException -> Q Exp)
-> (Refined p x -> Q Exp)
-> Either RefineException (Refined p x)
-> Q Exp
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either RefineException -> Q Exp
forall a. RefineException -> Q a
showException Refined p x -> Q Exp
forall t. Lift t => t -> Q Exp
TH.lift
     (x -> Q Exp)
-> (Q Exp -> Q (TExp (Refined p x))) -> x -> Q (TExp (Refined p x))
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> (Exp -> TExp (Refined p x)) -> Q Exp -> Q (TExp (Refined p x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Exp -> TExp (Refined p x)
forall a. Exp -> TExp a
TH.TExp
-- | Like 'refineTH', but immediately unrefines the value.
--   This is useful when some value need only be refined
--   at compile-time.
--
--   @since 0.4.4
refineTH_ :: forall p x. (Predicate p x, TH.Lift x)
  => x
  -> TH.Q (TH.TExp x)
refineTH_ :: x -> Q (TExp x)
refineTH_ = (Predicate p x, Lift x) => x -> Q (TExp (Refined p x))
forall p x. (Predicate p x, Lift x) => x -> Q (TExp (Refined p x))
refineTH @p @x (x -> Q (TExp (Refined p x)))
-> (Q (TExp (Refined p x)) -> Q (TExp x)) -> x -> Q (TExp x)
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> (TExp (Refined p x) -> TExp x)
-> Q (TExp (Refined p x)) -> Q (TExp x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TExp (Refined p x) -> TExp x
forall p x. TExp (Refined p x) -> TExp x
unsafeUnrefineTExp

unsafeUnrefineTExp :: TH.TExp (Refined p x) -> TH.TExp x
unsafeUnrefineTExp :: TExp (Refined p x) -> TExp x
unsafeUnrefineTExp (TH.TExp Exp
e) = Exp -> TExp x
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 :: Refined p x -> x
unrefine = Refined p x -> x
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 :: a -> Bool
reifyPredicate = Predicate p a => a -> Either RefineException (Refined p a)
forall p x.
Predicate p x =>
x -> Either RefineException (Refined p x)
refine @p @a (a -> Either RefineException (Refined p a))
-> (Either RefineException (Refined p a) -> Bool) -> a -> Bool
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> Either RefineException (Refined p a) -> Bool
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
    ( 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
_ = Maybe RefineException
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
    ( Generic -- ^ @since 0.3.0.0
    , Generic1 -- ^ @since 0.3.0.0
    )

-- | @since 0.1.0.0
instance (Predicate p x, Typeable p) => Predicate (Not p) x where
  validate :: Proxy (Not p) -> x -> Maybe RefineException
validate Proxy (Not p)
p x
x = do
    Maybe RefineException
-> (RefineException -> Maybe RefineException)
-> Maybe RefineException
-> Maybe RefineException
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (RefineException -> Maybe RefineException
forall a. a -> Maybe a
Just (TypeRep -> RefineException
RefineNotException (Proxy (Not p) -> TypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (Not p)
p)))
          (Maybe RefineException -> RefineException -> Maybe RefineException
forall a b. a -> b -> a
const Maybe RefineException
forall a. Maybe a
Nothing)
          (Proxy p -> x -> Maybe RefineException
forall p x. Predicate p x => Proxy p -> x -> Maybe RefineException
validate @p Proxy 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
    ( Generic -- ^ @since 0.3.0.0
    , Generic1 -- ^ @since 0.3.0.0
    )

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

-- | @since 0.1.0.0
instance ( Predicate l x, Predicate r x, Typeable l, Typeable r
         ) => 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 = Proxy l -> x -> Maybe RefineException
forall p x. Predicate p x => Proxy p -> x -> Maybe RefineException
validate @l Proxy l
forall a. HasCallStack => a
undefined x
x
    let b :: Maybe RefineException
b = Proxy r -> x -> Maybe RefineException
forall p x. Predicate p x => Proxy p -> x -> Maybe RefineException
validate @r Proxy r
forall a. HasCallStack => a
undefined x
x
    let throw :: These RefineException RefineException -> Maybe RefineException
throw These RefineException RefineException
err = RefineException -> Maybe RefineException
forall a. a -> Maybe a
Just (TypeRep -> These RefineException RefineException -> RefineException
RefineAndException (Proxy (And l r) -> TypeRep
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 (RefineException
-> RefineException -> These RefineException RefineException
forall a b. a -> b -> These a b
These RefineException
e RefineException
e1)
      (Just  RefineException
e,       Maybe RefineException
_) -> These RefineException RefineException -> Maybe RefineException
throw (RefineException -> These RefineException RefineException
forall a b. a -> These a b
This RefineException
e)
      (Maybe RefineException
Nothing, Just  RefineException
e) -> These RefineException RefineException -> Maybe RefineException
throw (RefineException -> These RefineException RefineException
forall a b. b -> These a b
That RefineException
e)
      (Maybe RefineException
Nothing, Maybe RefineException
Nothing) -> Maybe RefineException
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
    ( Generic -- ^ @since 0.3.0.0
    , Generic1 -- ^ @since 0.3.0.0
    )

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

-- | @since 0.2.0.0
instance ( Predicate l x, Predicate r x, Typeable l, Typeable r
         ) => 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  = Proxy l -> x -> Maybe RefineException
forall p x. Predicate p x => Proxy p -> x -> Maybe RefineException
validate @l Proxy l
forall a. HasCallStack => a
undefined x
x
    let right :: Maybe RefineException
right = Proxy r -> x -> Maybe RefineException
forall p x. Predicate p x => Proxy p -> x -> Maybe RefineException
validate @r Proxy r
forall a. HasCallStack => a
undefined x
x
    case (Maybe RefineException
left, Maybe RefineException
right) of
      (Just RefineException
l, Just RefineException
r) -> RefineException -> Maybe RefineException
forall a. a -> Maybe a
Just (TypeRep -> RefineException -> RefineException -> RefineException
RefineOrException (Proxy (Or l r) -> TypeRep
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)
_                -> 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
    ( Generic -- ^ @since 0.5
    , Generic1 -- ^ @since 0.5
    )

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

-- | @since 0.5
instance ( Predicate l x, Predicate r x, Typeable l, Typeable r
         ) => 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 = Proxy l -> x -> Maybe RefineException
forall p x. Predicate p x => Proxy p -> x -> Maybe RefineException
validate @l Proxy l
forall a. HasCallStack => a
undefined x
x
    let right :: Maybe RefineException
right = Proxy r -> x -> Maybe RefineException
forall p x. Predicate p x => Proxy p -> x -> Maybe RefineException
validate @r Proxy r
forall a. HasCallStack => a
undefined x
x
    case (Maybe RefineException
left, Maybe RefineException
right) of
      (Maybe RefineException
Nothing, Maybe RefineException
Nothing) -> RefineException -> Maybe RefineException
forall a. a -> Maybe a
Just (TypeRep
-> Maybe (RefineException, RefineException) -> RefineException
RefineXorException (Proxy (Xor l r) -> TypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (Xor l r)
p) Maybe (RefineException, RefineException)
forall a. Maybe a
Nothing)
      (Just  RefineException
l, Just  RefineException
r) -> RefineException -> Maybe RefineException
forall a. a -> Maybe a
Just (TypeRep
-> Maybe (RefineException, RefineException) -> RefineException
RefineXorException (Proxy (Xor l r) -> TypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (Xor l r)
p) ((RefineException, RefineException)
-> Maybe (RefineException, RefineException)
forall a. a -> Maybe a
Just (RefineException
l, RefineException
r)))
      (Maybe RefineException, 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
    ( 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 = Proxy (SizeLessThan n)
-> (t a, Text)
-> (t a -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
forall (p :: Nat -> *) (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") t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Int -> Int -> Bool
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 = Proxy (SizeLessThan n)
-> (Text, Text)
-> (Text -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
forall (p :: Nat -> *) (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 (Int -> Int -> Bool
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 = Proxy (SizeLessThan n)
-> (ByteString, Text)
-> (ByteString -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
forall (p :: Nat -> *) (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 (Int -> Int -> Bool
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 = Proxy (SizeLessThan n)
-> (ByteString, Text)
-> (ByteString -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
forall (p :: Nat -> *) (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") (Int64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int64 -> Int) -> (ByteString -> Int64) -> ByteString -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Int64
BL.length) (Int -> Int -> Bool
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
    ( 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 = Proxy (SizeGreaterThan n)
-> (t a, Text)
-> (t a -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
forall (p :: Nat -> *) (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") t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Int -> Int -> Bool
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 = Proxy (SizeGreaterThan n)
-> (Text, Text)
-> (Text -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
forall (p :: Nat -> *) (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 (Int -> Int -> Bool
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 = Proxy (SizeGreaterThan n)
-> (ByteString, Text)
-> (ByteString -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
forall (p :: Nat -> *) (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 (Int -> Int -> Bool
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 = Proxy (SizeGreaterThan n)
-> (ByteString, Text)
-> (ByteString -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
forall (p :: Nat -> *) (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") (Int64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int64 -> Int) -> (ByteString -> Int64) -> ByteString -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Int64
BL.length) (Int -> Int -> Bool
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
    ( 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 = Proxy (SizeEqualTo n)
-> (t a, Text)
-> (t a -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
forall (p :: Nat -> *) (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") t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Int -> Int -> Bool
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 = Proxy (SizeEqualTo n)
-> (Text, Text)
-> (Text -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
forall (p :: Nat -> *) (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 (Int -> Int -> Bool
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 = Proxy (SizeEqualTo n)
-> (ByteString, Text)
-> (ByteString -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
forall (p :: Nat -> *) (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 (Int -> Int -> Bool
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 = Proxy (SizeEqualTo n)
-> (ByteString, Text)
-> (ByteString -> Int)
-> (Int -> Int -> Bool, Text)
-> Maybe RefineException
forall (p :: Nat -> *) (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") (Int64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int64 -> Int) -> (ByteString -> Int64) -> ByteString -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Int64
BL.length) (Int -> Int -> Bool
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
    ( 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 t a -> Bool
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> Bool
increasing t a
x
    then Maybe RefineException
forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (Proxy Ascending -> TypeRep
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
    ( 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 t a -> Bool
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> Bool
decreasing t a
x
    then Maybe RefineException
forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
        (Proxy Descending -> TypeRep
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
    ( 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 = KnownNat n => Integer
forall (n :: Nat). KnownNat n => Integer
nv @n
    let x' :: x
x' = Integer -> x
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n
    if x
x x -> x -> Bool
forall a. Ord a => a -> a -> Bool
< x
x'
    then Maybe RefineException
forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (Proxy (LessThan n) -> TypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (LessThan n)
p)
         (Text
"Value is not less than " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Integer -> Text
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
    ( 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 = KnownNat n => Integer
forall (n :: Nat). KnownNat n => Integer
nv @n
    let x' :: x
x' = Integer -> x
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n
    if x
x x -> x -> Bool
forall a. Ord a => a -> a -> Bool
> x
x'
    then Maybe RefineException
forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (Proxy (GreaterThan n) -> TypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (GreaterThan n)
p)
         (Text
"Value is not greater than " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Integer -> Text
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
    ( 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 = KnownNat n => Integer
forall (n :: Nat). KnownNat n => Integer
nv @n
    let x' :: x
x' = Integer -> x
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n
    if x
x x -> x -> Bool
forall a. Ord a => a -> a -> Bool
>= x
x'
    then Maybe RefineException
forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (Proxy (From n) -> TypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (From n)
p)
         (Text
"Value is less than " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Integer -> Text
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
    ( 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 = KnownNat n => Integer
forall (n :: Nat). KnownNat n => Integer
nv @n
    let x' :: x
x' = Integer -> x
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n
    if x
x x -> x -> Bool
forall a. Ord a => a -> a -> Bool
<= x
x'
    then Maybe RefineException
forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (Proxy (To n) -> TypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (To n)
p)
         (Text
"Value is greater than " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Integer -> Text
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
    ( 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' = KnownNat mn => Integer
forall (n :: Nat). KnownNat n => Integer
nv @mn
    let mx' :: Integer
mx' = KnownNat mx => Integer
forall (n :: Nat). KnownNat n => Integer
nv @mx
    if x
x x -> x -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer -> x
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
mn' Bool -> Bool -> Bool
&& x
x x -> x -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer -> x
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
mx'
    then Maybe RefineException
forall a. Maybe a
Nothing
    else
      let msg :: Text
msg = [ Text
"Value is out of range (minimum: "
                , Integer -> Text
forall a. Integral a => a -> Text
i2text Integer
mn'
                , Text
", maximum: "
                , Integer -> Text
forall a. Integral a => a -> Text
i2text Integer
mx'
                , Text
")"
                ] [Text] -> ([Text] -> Text) -> Text
forall a b. a -> (a -> b) -> b
|> [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat
      in TypeRep -> Text -> Maybe RefineException
throwRefineOtherException (Proxy (FromTo mn mx) -> TypeRep
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
    ( 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 = KnownNat n => Integer
forall (n :: Nat). KnownNat n => Integer
nv @n
    let x' :: x
x' = Integer -> x
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n
    if x
x x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== x
x'
    then Maybe RefineException
forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (Proxy (EqualTo n) -> TypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (EqualTo n)
p)
         (Text
"Value does not equal " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Integer -> Text
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
    ( 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 = KnownNat n => Integer
forall (n :: Nat). KnownNat n => Integer
nv @n
    let x' :: x
x' = Integer -> x
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n
    if x
x x -> x -> Bool
forall a. Eq a => a -> a -> Bool
/= x
x'
    then Maybe RefineException
forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (Proxy (NotEqualTo n) -> TypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (NotEqualTo n)
p)
         (Text
"Value does equal " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Integer -> Text
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
    ( 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' = KnownNat n => Integer
forall (n :: Nat). KnownNat n => Integer
nv @n
    let m' :: Integer
m' = KnownNat m => Integer
forall (n :: Nat). KnownNat n => Integer
nv @m
    if x
x x -> x -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer -> x
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Integer
forall a. Num a => a -> a
negate Integer
n') Bool -> Bool -> Bool
&& x
x x -> x -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer -> x
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
m'
    then Maybe RefineException
forall a. Maybe a
Nothing
    else
      let msg :: Text
msg = [ Text
"Value is out of range (minimum: "
                , Integer -> Text
forall a. Integral a => a -> Text
i2text (Integer -> Integer
forall a. Num a => a -> a
negate Integer
n')
                , Text
", maximum: "
                , Integer -> Text
forall a. Integral a => a -> Text
i2text Integer
m'
                , Text
")"
                ] [Text] -> ([Text] -> Text) -> Text
forall a b. a -> (a -> b) -> b
|> [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat
      in TypeRep -> Text -> Maybe RefineException
throwRefineOtherException (Proxy (NegativeFromTo n m) -> TypeRep
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
    ( 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 = KnownNat n => Integer
forall (n :: Nat). KnownNat n => Integer
nv @n
    let x' :: x
x' = Integer -> x
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n
    if x
x x -> x -> x
forall a. Integral a => a -> a -> a
`mod` x
x' x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== x
0
    then Maybe RefineException
forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (Proxy (DivisibleBy n) -> TypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (DivisibleBy n)
p)
         (Text
"Value is not divisible by " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Integer -> Text
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
    ( 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 x -> Bool
forall a. Integral a => a -> Bool
odd x
x
    then Maybe RefineException
forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (Proxy Odd -> TypeRep
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
    ( 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 x -> Bool
forall a. RealFloat a => a -> Bool
isNaN x
x
    then Maybe RefineException
forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (Proxy NaN -> TypeRep
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
    ( 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 x -> Bool
forall a. RealFloat a => a -> Bool
isInfinite x
x
    then Maybe RefineException
forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (Proxy Infinite -> TypeRep
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
    ( 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 x -> Bool
forall a. Integral a => a -> Bool
even x
x
    then Maybe RefineException
forall a. Maybe a
Nothing
    else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException
         (Proxy Even -> TypeRep
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 non-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 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.
--
-- @since 0.2.0.0
class Weaken from to where
  -- | @since 0.2.0.0
  weaken :: Refined from x -> Refined to x
  weaken = Refined from x -> Refined to x
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 :: Refined (And l r) x -> Refined l x
andLeft = Refined (And l r) x -> Refined l x
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 :: Refined (And l r) x -> Refined r x
andRight = Refined (And l r) x -> Refined r x
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 :: Refined l x -> Refined (Or l r) x
leftOr = Refined l x -> Refined (Or l r) x
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 :: Refined r x -> Refined (Or l r) x
rightOr = Refined r x -> Refined (Or l r) x
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 :: Refined p x -> Either RefineException (Refined (p && p') x)
strengthen = Refined p x -> x
forall p x. Refined p x -> x
unrefine (Refined p x -> x)
-> (x -> Either RefineException (Refined (p && p') x))
-> Refined p x
-> Either RefineException (Refined (p && p') x)
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> x -> Either RefineException (Refined (p && p') x)
forall p x.
Predicate p x =>
x -> Either RefineException (Refined p x)
refine
{-# 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
    ( 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
""
      (ExceptionTree RefineException -> [String])
-> ([String] -> [String])
-> ExceptionTree RefineException
-> [String]
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> (String -> String) -> [String] -> [String]
forall a. (a -> a) -> [a] -> [a]
mapOnTail (Int -> String -> String
indent Int
6)
      (ExceptionTree RefineException -> [String])
-> ([String] -> String) -> ExceptionTree RefineException -> String
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
"" (ExceptionTree RefineException -> [String])
-> ([String] -> String) -> ExceptionTree RefineException -> String
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> [String] -> String
unlines
  where
    mapOnTail :: (a -> a) -> [a] -> [a]
    mapOnTail :: (a -> a) -> [a] -> [a]
mapOnTail a -> a
f = \case
      [] -> []
      (a
a : [a]
as) -> a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map a -> a
f [a]
as

    indent :: Int -> String -> String
    indent :: Int -> String -> String
indent Int
n String
s = Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
n Char
' ' String -> String -> String
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
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
arm
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
tie
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"The predicate ("
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TypeRep -> String
forall a. Show a => a -> String
show TypeRep
tr
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
") failed with the exception: "
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> SomeException -> String
forall e. Exception e => e -> String
displayException SomeException
e
        ]
      NodeOther TypeRep
tr Text
p ->
        [ String
leader
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
arm
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
tie
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"The predicate ("
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TypeRep -> String
forall a. Show a => a -> String
show TypeRep
tr
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
") failed with the message: "
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Text -> String
Text.unpack Text
p
        ]
      NodeNot TypeRep
tr ->
        [ String
leader
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
arm
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
tie
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"The predicate ("
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TypeRep -> String
forall a. Show a => a -> String
show TypeRep
tr
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
") does not hold"
        ]
      NodeOr TypeRep
tr [ExceptionTree RefineException]
rest -> TypeRep -> String
nodeRep TypeRep
tr String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [ExceptionTree RefineException] -> String -> [String]
showChildren [ExceptionTree RefineException]
rest (String
leader String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
extension)
      NodeAnd TypeRep
tr [ExceptionTree RefineException]
rest -> TypeRep -> String
nodeRep TypeRep
tr String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [ExceptionTree RefineException] -> String -> [String]
showChildren [ExceptionTree RefineException]
rest (String
leader String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
extension)
      -- can be empty since both can be satisfied
      NodeXor TypeRep
tr [] ->
        [ String
leader
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
arm
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
tie
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"The predicate ("
          String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TypeRep -> String
forall a. Show a => a -> String
show TypeRep
tr
          String -> String -> String
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 String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [ExceptionTree RefineException] -> String -> [String]
showChildren [ExceptionTree RefineException]
rest (String
leader String -> String -> String
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 String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
arm String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
tie String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TypeRep -> String
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 = Int -> String -> [String]
forall a. Int -> a -> [a]
replicate ([ExceptionTree RefineException] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExceptionTree RefineException]
children Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) String
"├" [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> [String
"└"]
      in [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((String -> ExceptionTree RefineException -> [String])
-> [String] -> [ExceptionTree RefineException] -> [[String]]
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 = RefineException -> ExceptionTree RefineException
forall a. RefineException -> ExceptionTree a
go
  where
    go :: RefineException -> ExceptionTree a
go = \case
      RefineSomeException TypeRep
tr SomeException
e -> TypeRep -> SomeException -> ExceptionTree a
forall a. TypeRep -> SomeException -> ExceptionTree a
NodeSome TypeRep
tr SomeException
e
      RefineOtherException TypeRep
tr Text
p -> TypeRep -> Text -> ExceptionTree a
forall a. TypeRep -> Text -> ExceptionTree a
NodeOther TypeRep
tr Text
p
      RefineNotException TypeRep
tr -> TypeRep -> ExceptionTree a
forall a. TypeRep -> ExceptionTree a
NodeNot TypeRep
tr
      RefineOrException TypeRep
tr RefineException
l RefineException
r -> TypeRep -> [ExceptionTree a] -> ExceptionTree a
forall a. 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) -> TypeRep -> [ExceptionTree a] -> ExceptionTree a
forall a. TypeRep -> [ExceptionTree a] -> ExceptionTree a
NodeAnd TypeRep
tr [RefineException -> ExceptionTree a
go RefineException
l]
      RefineAndException TypeRep
tr (That RefineException
r) -> TypeRep -> [ExceptionTree a] -> ExceptionTree a
forall a. TypeRep -> [ExceptionTree a] -> ExceptionTree a
NodeAnd TypeRep
tr [RefineException -> ExceptionTree a
go RefineException
r]
      RefineAndException TypeRep
tr (These RefineException
l RefineException
r) -> TypeRep -> [ExceptionTree a] -> ExceptionTree a
forall a. 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 -> TypeRep -> [ExceptionTree a] -> ExceptionTree a
forall a. TypeRep -> [ExceptionTree a] -> ExceptionTree a
NodeXor TypeRep
tr []
      RefineXorException TypeRep
tr (Just (RefineException
l, RefineException
r)) -> TypeRep -> [ExceptionTree a] -> ExceptionTree a
forall a. 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 (RefineException -> ExceptionTree RefineException)
-> (ExceptionTree RefineException -> String)
-> RefineException
-> String
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 = RefineException -> String
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 (Text -> RefineException)
-> (RefineException -> Maybe RefineException)
-> Text
-> Maybe RefineException
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> RefineException -> Maybe RefineException
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 (SomeException -> RefineException)
-> (RefineException -> Maybe RefineException)
-> SomeException
-> Maybe RefineException
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> RefineException -> Maybe RefineException
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
  = Maybe RefineException
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 :: 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' = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (KnownNat n => Integer
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 Maybe RefineException
forall a. Maybe a
Nothing
  else
    let msg :: Text
msg =
          [ Text
"Size of ", Text
typ, Text
" is not ", Text
cmpDesc, Text
" "
          , Int -> Text
forall a. Integral a => a -> Text
i2text Int
x'
          , Text
". "
          , Text
"Size is: "
          , Int -> Text
forall a. Integral a => a -> Text
i2text Int
sz
          ] [Text] -> ([Text] -> Text) -> Text
forall a b. a -> (a -> b) -> b
|> [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat
    in TypeRep -> Text -> Maybe RefineException
throwRefineOtherException (Proxy (p n) -> TypeRep
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 :: Integer
nv = Proxy# n -> Integer
forall (n :: Nat). KnownNat n => Proxy# n -> Integer
natVal' (Proxy# n
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 :: a -> Text
i2text = a -> Builder
forall a. Integral a => a -> Builder
TextBuilder.decimal
  (a -> Builder) -> (Builder -> Text) -> a -> Text
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> Builder -> Text
TextBuilder.toLazyText
  (a -> Text) -> (Text -> Text) -> a -> Text
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> Text -> Text
TextLazy.toStrict
{-# SPECIALISE i2text :: Int -> Text #-}
{-# SPECIALISE i2text :: Integer -> Text #-}