{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE TypeOperators #-}
-- | simple refinement type with only one type and a predicate

module Predicate.Refined (
  -- ** Refined

    Refined
  , unRefined
  , Msg0(..)
  , showMsg0
  , RefinedC

  -- ** create methods

  , newRefined
  , newRefined'

  -- ** QuickCheck method

  , genRefined

  -- ** unsafe create methods

  , unsafeRefined
  , unsafeRefined'

 ) where
import Predicate.Core
import Predicate.Misc (nullIf)
import Predicate.Util
import Control.Lens
import Data.Proxy (Proxy(Proxy))
import Data.Aeson (ToJSON(..), FromJSON(..))
import qualified Language.Haskell.TH.Syntax as TH
import Test.QuickCheck
import qualified GHC.Read as GR
import qualified Text.ParserCombinators.ReadPrec as PCR
import qualified Text.Read.Lex as RL
import qualified Data.Binary as B
import Data.Binary (Binary)
import Data.String (IsString(..))
import Data.Hashable (Hashable(..))
import GHC.Stack (HasCallStack)
import Data.Coerce (coerce)
import Control.DeepSeq (NFData)
-- $setup

-- >>> :set -XDataKinds

-- >>> :set -XTypeApplications

-- >>> :set -XTypeOperators

-- >>> :set -XOverloadedStrings

-- >>> :set -XNoOverloadedLists

-- >>> :m + Predicate.Prelude

-- >>> :m + Control.Arrow

-- >>> :m + Text.Show.Functions


-- | a simple refinement type that ensures the predicate @p@ holds for the type @a@

--

newtype Refined (opts :: Opt) p a = Refined a
  deriving stock (Int -> Refined opts p a -> ShowS
[Refined opts p a] -> ShowS
Refined opts p a -> String
(Int -> Refined opts p a -> ShowS)
-> (Refined opts p a -> String)
-> ([Refined opts p a] -> ShowS)
-> Show (Refined opts p a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (opts :: Opt) k (p :: k) a.
Show a =>
Int -> Refined opts p a -> ShowS
forall (opts :: Opt) k (p :: k) a.
Show a =>
[Refined opts p a] -> ShowS
forall (opts :: Opt) k (p :: k) a.
Show a =>
Refined opts p a -> String
showList :: [Refined opts p a] -> ShowS
$cshowList :: forall (opts :: Opt) k (p :: k) a.
Show a =>
[Refined opts p a] -> ShowS
show :: Refined opts p a -> String
$cshow :: forall (opts :: Opt) k (p :: k) a.
Show a =>
Refined opts p a -> String
showsPrec :: Int -> Refined opts p a -> ShowS
$cshowsPrec :: forall (opts :: Opt) k (p :: k) a.
Show a =>
Int -> Refined opts p a -> ShowS
Show, Refined opts p a -> Q Exp
Refined opts p a -> Q (TExp (Refined opts p a))
(Refined opts p a -> Q Exp)
-> (Refined opts p a -> Q (TExp (Refined opts p a)))
-> Lift (Refined opts p a)
forall t. (t -> Q Exp) -> (t -> Q (TExp t)) -> Lift t
forall (opts :: Opt) k (p :: k) a.
Lift a =>
Refined opts p a -> Q Exp
forall (opts :: Opt) k (p :: k) a.
Lift a =>
Refined opts p a -> Q (TExp (Refined opts p a))
liftTyped :: Refined opts p a -> Q (TExp (Refined opts p a))
$cliftTyped :: forall (opts :: Opt) k (p :: k) a.
Lift a =>
Refined opts p a -> Q (TExp (Refined opts p a))
lift :: Refined opts p a -> Q Exp
$clift :: forall (opts :: Opt) k (p :: k) a.
Lift a =>
Refined opts p a -> Q Exp
TH.Lift)
  deriving newtype (Refined opts p a -> Refined opts p a -> Bool
(Refined opts p a -> Refined opts p a -> Bool)
-> (Refined opts p a -> Refined opts p a -> Bool)
-> Eq (Refined opts p a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (opts :: Opt) k (p :: k) a.
Eq a =>
Refined opts p a -> Refined opts p a -> Bool
/= :: Refined opts p a -> Refined opts p a -> Bool
$c/= :: forall (opts :: Opt) k (p :: k) a.
Eq a =>
Refined opts p a -> Refined opts p a -> Bool
== :: Refined opts p a -> Refined opts p a -> Bool
$c== :: forall (opts :: Opt) k (p :: k) a.
Eq a =>
Refined opts p a -> Refined opts p a -> Bool
Eq, Eq (Refined opts p a)
Eq (Refined opts p a)
-> (Refined opts p a -> Refined opts p a -> Ordering)
-> (Refined opts p a -> Refined opts p a -> Bool)
-> (Refined opts p a -> Refined opts p a -> Bool)
-> (Refined opts p a -> Refined opts p a -> Bool)
-> (Refined opts p a -> Refined opts p a -> Bool)
-> (Refined opts p a -> Refined opts p a -> Refined opts p a)
-> (Refined opts p a -> Refined opts p a -> Refined opts p a)
-> Ord (Refined opts p a)
Refined opts p a -> Refined opts p a -> Bool
Refined opts p a -> Refined opts p a -> Ordering
Refined opts p a -> Refined opts p a -> Refined opts p a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (opts :: Opt) k (p :: k) a. Ord a => Eq (Refined opts p a)
forall (opts :: Opt) k (p :: k) a.
Ord a =>
Refined opts p a -> Refined opts p a -> Bool
forall (opts :: Opt) k (p :: k) a.
Ord a =>
Refined opts p a -> Refined opts p a -> Ordering
forall (opts :: Opt) k (p :: k) a.
Ord a =>
Refined opts p a -> Refined opts p a -> Refined opts p a
min :: Refined opts p a -> Refined opts p a -> Refined opts p a
$cmin :: forall (opts :: Opt) k (p :: k) a.
Ord a =>
Refined opts p a -> Refined opts p a -> Refined opts p a
max :: Refined opts p a -> Refined opts p a -> Refined opts p a
$cmax :: forall (opts :: Opt) k (p :: k) a.
Ord a =>
Refined opts p a -> Refined opts p a -> Refined opts p a
>= :: Refined opts p a -> Refined opts p a -> Bool
$c>= :: forall (opts :: Opt) k (p :: k) a.
Ord a =>
Refined opts p a -> Refined opts p a -> Bool
> :: Refined opts p a -> Refined opts p a -> Bool
$c> :: forall (opts :: Opt) k (p :: k) a.
Ord a =>
Refined opts p a -> Refined opts p a -> Bool
<= :: Refined opts p a -> Refined opts p a -> Bool
$c<= :: forall (opts :: Opt) k (p :: k) a.
Ord a =>
Refined opts p a -> Refined opts p a -> Bool
< :: Refined opts p a -> Refined opts p a -> Bool
$c< :: forall (opts :: Opt) k (p :: k) a.
Ord a =>
Refined opts p a -> Refined opts p a -> Bool
compare :: Refined opts p a -> Refined opts p a -> Ordering
$ccompare :: forall (opts :: Opt) k (p :: k) a.
Ord a =>
Refined opts p a -> Refined opts p a -> Ordering
$cp1Ord :: forall (opts :: Opt) k (p :: k) a. Ord a => Eq (Refined opts p a)
Ord, Refined opts p a -> ()
(Refined opts p a -> ()) -> NFData (Refined opts p a)
forall a. (a -> ()) -> NFData a
forall (opts :: Opt) k (p :: k) a.
NFData a =>
Refined opts p a -> ()
rnf :: Refined opts p a -> ()
$crnf :: forall (opts :: Opt) k (p :: k) a.
NFData a =>
Refined opts p a -> ()
NFData)

-- | extract the value from 'Refined'

unRefined :: forall k (opts :: Opt) (p :: k) a
   . Refined opts p a
  -> a
unRefined :: Refined opts p a -> a
unRefined = Refined opts p a -> a
coerce

type role Refined phantom nominal nominal

-- | 'IsString' instance for Refined

--

-- >>> pureTryTest $ fromString @(Refined OL (ReadP Int Id >> Id > 244) String) "523"

-- Right (Refined "523")

--

-- >>> pureTryTest $ fromString @(Refined OL (ReadP Int Id >> Id > 244) String) "52"

-- Left ()

--

instance RefinedC opts p String
      => IsString (Refined opts p String) where
  fromString :: String -> Refined opts p String
fromString String
s =
    case String -> Either Msg0 (Refined opts p String)
forall k (opts :: Opt) (p :: k) a.
RefinedC opts p a =>
a -> Either Msg0 (Refined opts p a)
newRefined @opts @p String
s of
      Left Msg0
w -> String -> Refined opts p String
forall a. HasCallStack => String -> a
error (String -> Refined opts p String)
-> String -> Refined opts p String
forall a b. (a -> b) -> a -> b
$ String
"Refined(IsString:fromString):" String -> ShowS
forall a. [a] -> [a] -> [a]
++ POpts -> Msg0 -> String
errorDisplay (OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts) Msg0
w
      Right Refined opts p String
r -> Refined opts p String
r

errorDisplay :: POpts -> Msg0 -> String
errorDisplay :: POpts -> Msg0 -> String
errorDisplay POpts
o Msg0
m =
     Msg0 -> String
m0ValBoolColor Msg0
m
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> ShowS
nullIf String
" " (Msg0 -> String
m0Short Msg0
m)
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if String -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null (Msg0 -> String
m0Long Msg0
m) Bool -> Bool -> Bool
|| POpts -> Bool
hasNoTree POpts
o
      then String
""
      else String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg0 -> String
m0Long Msg0
m)

-- | 'Read' instance for 'Refined'

--

-- >>> reads @(Refined OZ (0 <..> 299) Int) "Refined 254"

-- [(Refined 254,"")]

--

-- >>> reads @(Refined OZ (0 <..> 299) Int) "Refined 300"

-- []

--

-- >>> reads @(Refined OZ 'True Int) "Refined (-123)xyz"

-- [(Refined (-123),"xyz")]

--

instance ( RefinedC opts p a
         , Read a
         ) => Read (Refined opts p a) where
  readPrec :: ReadPrec (Refined opts p a)
readPrec
    = ReadPrec (Refined opts p a) -> ReadPrec (Refined opts p a)
forall a. ReadPrec a -> ReadPrec a
GR.parens
        (Int -> ReadPrec (Refined opts p a) -> ReadPrec (Refined opts p a)
forall a. Int -> ReadPrec a -> ReadPrec a
PCR.prec
           Int
11
           (do Lexeme -> ReadPrec ()
GR.expectP (String -> Lexeme
RL.Ident String
"Refined")
               a
fld0 <- ReadPrec a -> ReadPrec a
forall a. ReadPrec a -> ReadPrec a
PCR.reset ReadPrec a
forall a. Read a => ReadPrec a
GR.readPrec
               case a -> Either Msg0 (Refined opts p a)
forall k (opts :: Opt) (p :: k) a.
RefinedC opts p a =>
a -> Either Msg0 (Refined opts p a)
newRefined @opts @p a
fld0 of -- since we cant display the failure message

                 Left Msg0
_e -> String -> ReadPrec (Refined opts p a)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
""
                 Right Refined opts p a
_r -> Refined opts p a -> ReadPrec (Refined opts p a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (a -> Refined opts p a
forall k (opts :: Opt) (p :: k) a. a -> Refined opts p a
Refined a
fld0)
           ))
  readList :: ReadS [Refined opts p a]
readList = ReadS [Refined opts p a]
forall a. Read a => ReadS [a]
GR.readListDefault
  readListPrec :: ReadPrec [Refined opts p a]
readListPrec = ReadPrec [Refined opts p a]
forall a. Read a => ReadPrec [a]
GR.readListPrecDefault

-- | the constraints that 'Refined' must adhere to

type RefinedC opts p a = (OptC opts, PP p a ~ Bool, P p a)

-- | 'ToJSON' instance for 'Refined'

instance ToJSON a => ToJSON (Refined opts p a) where
  toJSON :: Refined opts p a -> Value
toJSON = a -> Value
forall a. ToJSON a => a -> Value
toJSON (a -> Value)
-> (Refined opts p a -> a) -> Refined opts p a -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined opts p a -> a
forall k (opts :: Opt) (p :: k) a. Refined opts p a -> a
unRefined

-- | 'FromJSON' instance for 'Refined'

--

-- >>> import qualified Data.Aeson as A

-- >>> A.eitherDecode' @(Refined OZ (Between 10 14 Id) Int) "13"

-- Right (Refined 13)

--

-- >>> removeAnsi $ A.eitherDecode' @(Refined OAN (Between 10 14 Id) Int) "16"

-- Error in $: Refined(FromJSON:parseJSON):False (16 <= 14)

-- False 16 <= 14

-- |

-- +- P Id 16

-- |

-- +- P '10

-- |

-- `- P '14

--

instance ( RefinedC opts p a
         , FromJSON a
         ) => FromJSON (Refined opts p a) where
  parseJSON :: Value -> Parser (Refined opts p a)
parseJSON Value
z = do
    a
a <- Value -> Parser a
forall a. FromJSON a => Value -> Parser a
parseJSON Value
z
    case a -> Either Msg0 (Refined opts p a)
forall k (opts :: Opt) (p :: k) a.
RefinedC opts p a =>
a -> Either Msg0 (Refined opts p a)
newRefined @opts @p a
a of
      Left Msg0
w -> String -> Parser (Refined opts p a)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Parser (Refined opts p a))
-> String -> Parser (Refined opts p a)
forall a b. (a -> b) -> a -> b
$ String
"Refined(FromJSON:parseJSON):" String -> ShowS
forall a. [a] -> [a] -> [a]
++ POpts -> Msg0 -> String
errorDisplay (OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts) Msg0
w
      Right Refined opts p a
r -> Refined opts p a -> Parser (Refined opts p a)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Refined opts p a
r

-- | 'Binary' instance for 'Refined'

--

-- >>> import Data.Time

-- >>> import Control.Lens

-- >>> import Control.Arrow ((+++))

-- >>> type K1 = Refined OZ (ReadP Day Id >> 'True) String

-- >>> type K2 = Refined OAN (Between (ReadP Day "2019-05-30") (ReadP Day "2019-06-01") (ReadP Day Id)) String

-- >>> r = unsafeRefined' @OZ "2019-04-23" :: K1

-- >>> removeAnsi $ (view _3 +++ view _3) $ B.decodeOrFail @K1 (B.encode r)

-- Refined "2019-04-23"

--

-- >>> removeAnsi $ (view _3 +++ view _3) $ B.decodeOrFail @K2 (B.encode r)

-- Refined(Binary:get):False (2019-05-30 <= 2019-04-23)

-- False 2019-05-30 <= 2019-04-23

-- |

-- +- P ReadP Day 2019-04-23

-- |  |

-- |  `- P Id "2019-04-23"

-- |

-- +- P ReadP Day 2019-05-30

-- |  |

-- |  `- P '"2019-05-30"

-- |

-- `- P ReadP Day 2019-06-01

--    |

--    `- P '"2019-06-01"

--

instance ( RefinedC opts p a
         , Binary a
         ) => Binary (Refined opts p a) where
  get :: Get (Refined opts p a)
get = do
    a
fld0 <- Binary a => Get a
forall t. Binary t => Get t
B.get @a
    case a -> Either Msg0 (Refined opts p a)
forall k (opts :: Opt) (p :: k) a.
RefinedC opts p a =>
a -> Either Msg0 (Refined opts p a)
newRefined @opts @p a
fld0 of
      Left Msg0
w -> String -> Get (Refined opts p a)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Get (Refined opts p a))
-> String -> Get (Refined opts p a)
forall a b. (a -> b) -> a -> b
$ String
"Refined(Binary:get):" String -> ShowS
forall a. [a] -> [a] -> [a]
++ POpts -> Msg0 -> String
errorDisplay (OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts) Msg0
w
      Right Refined opts p a
r -> Refined opts p a -> Get (Refined opts p a)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Refined opts p a
r
  put :: Refined opts p a -> Put
put (Refined a
r) = a -> Put
forall t. Binary t => t -> Put
B.put @a a
r

-- | 'Hashable' instance for 'Refined'

instance ( RefinedC opts p a
         , Hashable a
         ) => Hashable (Refined opts p a) where
  hashWithSalt :: Int -> Refined opts p a -> Int
hashWithSalt Int
s (Refined a
a) = Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ a -> Int
forall a. Hashable a => a -> Int
hash a
a

-- | 'Arbitrary' instance for 'Refined'

--

-- >>> xs <- generate (vectorOf 10 (arbitrary @(Refined OAN (Id /= 0) Int)))

-- >>> all ((/=0) . unRefined) xs

-- True

--

-- >>> xs <- generate (vectorOf 10 (arbitrary @(Refined OAN IsPrime Int)))

-- >>> all (isPrime . unRefined) xs

-- True

--

instance ( Arbitrary a
         , RefinedC opts p a
         , Show a
         ) => Arbitrary (Refined opts p a) where
  arbitrary :: Gen (Refined opts p a)
arbitrary = Gen a -> Gen (Refined opts p a)
forall k (opts :: Opt) (p :: k) a.
(RefinedC opts p a, HasCallStack) =>
Gen a -> Gen (Refined opts p a)
genRefined Gen a
forall a. Arbitrary a => Gen a
arbitrary

-- | create 'Refined' generator using a generator to restrict the values

genRefined :: forall opts p a .
   ( RefinedC opts p a
   , HasCallStack
   )
   => Gen a
   -> Gen (Refined opts p a)
genRefined :: Gen a -> Gen (Refined opts p a)
genRefined Gen a
g =
  let f :: Int -> Gen (Refined opts p a)
f !Int
cnt = do
        Maybe a
ma <- Gen a -> (a -> Bool) -> Gen (Maybe a)
forall a. Gen a -> (a -> Bool) -> Gen (Maybe a)
suchThatMaybe Gen a
g ((a -> Bool) -> Gen (Maybe a)) -> (a -> Bool) -> Gen (Maybe a)
forall a b. (a -> b) -> a -> b
$ \a
a -> a -> Either String (PP p a)
forall k (opts :: Opt) (p :: k) i.
(OptC opts, P p i) =>
i -> Either String (PP p i)
evalQuick @opts @p a
a Either String Bool -> Either String Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Either String Bool
forall a b. b -> Either a b
Right Bool
True
        case Maybe a
ma of
          Maybe a
Nothing ->
             let o :: POpts
o = OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts
                 r :: Int
r = POpts -> Int
getMaxRecursionValue POpts
o
             in if Int
cnt Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
r
                then String -> Gen (Refined opts p a)
forall a. HasCallStack => String -> a
error (String -> Gen (Refined opts p a))
-> String -> Gen (Refined opts p a)
forall a b. (a -> b) -> a -> b
$ POpts -> ShowS
setOtherEffects POpts
o (String
"genRefined recursion exceeded(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")")
                else Int -> Gen (Refined opts p a)
f (Int
cntInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
          Just a
a -> Refined opts p a -> Gen (Refined opts p a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Refined opts p a -> Gen (Refined opts p a))
-> Refined opts p a -> Gen (Refined opts p a)
forall a b. (a -> b) -> a -> b
$ a -> Refined opts p a
forall k (opts :: Opt) (p :: k) a. a -> Refined opts p a
unsafeRefined a
a
  in Int -> Gen (Refined opts p a)
f Int
0

-- | holds the results of creating a 'Refined' value for display

data Msg0 = Msg0 { Msg0 -> Either String Bool
m0BoolE :: !(Either String Bool)
                 , Msg0 -> String
m0Short :: !String
                 , Msg0 -> String
m0Long :: !String
                 , Msg0 -> String
m0ValBoolColor :: !String
                 } deriving Msg0 -> Msg0 -> Bool
(Msg0 -> Msg0 -> Bool) -> (Msg0 -> Msg0 -> Bool) -> Eq Msg0
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Msg0 -> Msg0 -> Bool
$c/= :: Msg0 -> Msg0 -> Bool
== :: Msg0 -> Msg0 -> Bool
$c== :: Msg0 -> Msg0 -> Bool
Eq

-- | verbose display of 'Msg0'

showMsg0 :: Msg0 -> String
showMsg0 :: Msg0 -> String
showMsg0 (Msg0 Either String Bool
a String
b String
c String
d) = String
"Msg0 [" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Either String Bool -> String
forall a. Show a => a -> String
show Either String Bool
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]\nShort[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]\nLong[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]\nColor[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
d String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"

instance Show Msg0 where
  show :: Msg0 -> String
show = Msg0 -> String
m0Long

-- | returns a 'Refined' value if @a@ is valid for the predicate @p@ for any 'MonadEval' instance

newRefined' :: forall opts p a m
   . ( MonadEval m
     , RefinedC opts p a
     )
   => a
   -> m (Either Msg0 (Refined opts p a))
newRefined' :: a -> m (Either Msg0 (Refined opts p a))
newRefined' a
a = do
  let o :: POpts
o = OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts
  TT Bool
pp <- Proxy p -> POpts -> a -> m (TT (PP p a))
forall k (m :: Type -> Type) (p :: k) a (proxy :: k -> Type).
(MonadEval m, P p a, PP p a ~ Bool) =>
proxy p -> POpts -> a -> m (TT (PP p a))
evalBool (Proxy p
forall k (t :: k). Proxy t
Proxy @p) POpts
o a
a
  let r :: String
r = POpts -> Val Bool -> String
colorValBool POpts
o (TT Bool
pp TT Bool -> Getting (Val Bool) (TT Bool) (Val Bool) -> Val Bool
forall s a. s -> Getting a s a -> a
^. Getting (Val Bool) (TT Bool) (Val Bool)
forall a b. Lens (TT a) (TT b) (Val a) (Val b)
ttVal)
      s :: String
s = POpts -> TT Bool -> String
forall x. Show x => POpts -> TT x -> String
prtTree POpts
o TT Bool
pp
      msg0 :: Msg0
msg0 = Either String Bool -> String -> String -> String -> Msg0
Msg0 (TT Bool
pp TT Bool
-> Getting (Either String Bool) (TT Bool) (Either String Bool)
-> Either String Bool
forall s a. s -> Getting a s a -> a
^. (Val Bool -> Const (Either String Bool) (Val Bool))
-> TT Bool -> Const (Either String Bool) (TT Bool)
forall a b. Lens (TT a) (TT b) (Val a) (Val b)
ttVal ((Val Bool -> Const (Either String Bool) (Val Bool))
 -> TT Bool -> Const (Either String Bool) (TT Bool))
-> ((Either String Bool
     -> Const (Either String Bool) (Either String Bool))
    -> Val Bool -> Const (Either String Bool) (Val Bool))
-> Getting (Either String Bool) (TT Bool) (Either String Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either String Bool
 -> Const (Either String Bool) (Either String Bool))
-> Val Bool -> Const (Either String Bool) (Val Bool)
forall a b. Iso (Val a) (Val b) (Either String a) (Either String b)
_ValEither) (TT Bool -> String
forall a. TT a -> String
topMessage TT Bool
pp) String
s String
r
  Either Msg0 (Refined opts p a)
-> m (Either Msg0 (Refined opts p a))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Either Msg0 (Refined opts p a)
 -> m (Either Msg0 (Refined opts p a)))
-> Either Msg0 (Refined opts p a)
-> m (Either Msg0 (Refined opts p a))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts -> String -> TT Bool -> [Tree PE] -> Either (TT Any) Bool
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
o String
"" TT Bool
pp [] of
       Right Bool
True -> Refined opts p a -> Either Msg0 (Refined opts p a)
forall a b. b -> Either a b
Right (a -> Refined opts p a
forall k (opts :: Opt) (p :: k) a. a -> Refined opts p a
Refined a
a)
       Either (TT Any) Bool
_ -> Msg0 -> Either Msg0 (Refined opts p a)
forall a b. a -> Either a b
Left Msg0
msg0

-- | returns a pure 'Refined' value if @a@ is valid for the predicate @p@

--

-- >>> newRefined @OL @(ReadP Int Id > 99) "123"

-- Right (Refined "123")

--

-- >>> left m0Long $ newRefined @OL @(ReadP Int Id > 99) "12"

-- Left "False (12 > 99)"

--

-- >>> newRefined @OZ @(Between 10 14 Id) 13

-- Right (Refined 13)

--

-- >>> left m0BoolE $ newRefined @OZ @(Between 10 14 Id) 99

-- Left (Right False)

--

-- >>> newRefined @OZ @(Last >> Len == 4) ["one","two","three","four"]

-- Right (Refined ["one","two","three","four"])

--

-- >>> newRefined @OZ @(Re "^\\d{1,3}\\.\\d{1,3}\\.\\d{1,3}\\.\\d{1,3}$") "141.213.1.99"

-- Right (Refined "141.213.1.99")

--

-- >>> left m0BoolE $ newRefined @OZ @(Re "^\\d{1,3}\\.\\d{1,3}\\.\\d{1,3}\\.\\d{1,3}$") "141.213.1"

-- Left (Right False)

--

-- >>> left m0BoolE $ newRefined @OZ @(Map' (ReadP Int Id) (Resplit "\\.") >> GuardBool (PrintF "bad length: found %d" Len) (Len == 4)) "141.213.1"

-- Left (Left "bad length: found 3")

--

-- >>> left m0BoolE $ newRefined @OZ @(Map' (ReadP Int Id) (Resplit "\\.") >> GuardBool (PrintF "bad length: found %d" Len) (Len == 4) && BoolsN (PrintT "octet %d out of range %d" Id) 4 (0 <..> 0xff)) "141.213.1.444"

-- Left (Left "Bool(3) [octet 3 out of range 444]")

--

-- >>> left m0BoolE $ newRefined @OZ @(Map' (ReadP Int Id) (Resplit "\\.") >> GuardBool (PrintF "bad length: found %d" Len) (Len == 4) && BoolsN (PrintT "octet %d out of range %d" Id) 4 (0 <..> 0xff)) "141.213.1x34.444"

-- Left (Left "ReadP Int (1x34)")

--

-- >>> newRefined @OZ @(Map ('[Id] >> ReadP Int Id) >> IsLuhn) "12344"

-- Right (Refined "12344")

--

-- >>> left m0BoolE $ newRefined @OZ @(Map ('[Id] >> ReadP Int Id) >> IsLuhn) "12340"

-- Left (Right False)

--

-- >>> newRefined @OZ @(Any IsPrime) [11,13,17,18]

-- Right (Refined [11,13,17,18])

--

-- >>> left m0BoolE $ newRefined @OZ @(All IsPrime) [11,13,17,18]

-- Left (Right False)

--

-- >>> newRefined @OZ @(Snd !! Fst >> Len > 5) (2,["abc","defghij","xyzxyazsfd"])

-- Right (Refined (2,["abc","defghij","xyzxyazsfd"]))

--

-- >>> left m0BoolE $ newRefined @OZ @(Snd !! Fst >> Len > 5) (27,["abc","defghij","xyzxyazsfd"])

-- Left (Left "(!!) index not found")

--

-- >>> left m0BoolE $ newRefined @OZ @(Snd !! Fst >> Len <= 5) (2,["abc","defghij","xyzxyazsfd"])

-- Left (Right False)

--

-- >>> newRefined @OU @((Id $$ 13) > 100) (\x -> x * 14) ^? _Right . to unRefined . to ($ 99)

-- Just 1386

--

newRefined :: forall opts p a
    . RefinedC opts p a
   => a
   -> Either Msg0 (Refined opts p a)
newRefined :: a -> Either Msg0 (Refined opts p a)
newRefined = Identity (Either Msg0 (Refined opts p a))
-> Either Msg0 (Refined opts p a)
forall a. Identity a -> a
runIdentity (Identity (Either Msg0 (Refined opts p a))
 -> Either Msg0 (Refined opts p a))
-> (a -> Identity (Either Msg0 (Refined opts p a)))
-> a
-> Either Msg0 (Refined opts p a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Identity (Either Msg0 (Refined opts p a))
forall k (opts :: Opt) (p :: k) a (m :: Type -> Type).
(MonadEval m, RefinedC opts p a) =>
a -> m (Either Msg0 (Refined opts p a))
newRefined'

-- | create an unsafe 'Refined' value without running the predicate

unsafeRefined :: forall opts p a . a -> Refined opts p a
unsafeRefined :: a -> Refined opts p a
unsafeRefined = a -> Refined opts p a
forall k (opts :: Opt) (p :: k) a. a -> Refined opts p a
Refined

-- | create an unsafe 'Refined' value and also run the predicate

unsafeRefined' :: forall opts p a
  . ( RefinedC opts p a
    , HasCallStack
    ) => a -> Refined opts p a
unsafeRefined' :: a -> Refined opts p a
unsafeRefined' a
a =
  let o :: POpts
o = OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts
      tt :: TT Bool
tt = Identity (TT Bool) -> TT Bool
forall a. Identity a -> a
runIdentity (Identity (TT Bool) -> TT Bool) -> Identity (TT Bool) -> TT Bool
forall a b. (a -> b) -> a -> b
$ Proxy p -> POpts -> a -> Identity (TT (PP p a))
forall k (m :: Type -> Type) (p :: k) a (proxy :: k -> Type).
(MonadEval m, P p a, PP p a ~ Bool) =>
proxy p -> POpts -> a -> m (TT (PP p a))
evalBool (Proxy p
forall k (t :: k). Proxy t
Proxy @p) POpts
o a
a
  in case Inline
-> POpts -> String -> TT Bool -> [Tree PE] -> Either (TT Any) Bool
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
o String
"" TT Bool
tt [] of
       Right Bool
True -> a -> Refined opts p a
forall k (opts :: Opt) (p :: k) a. a -> Refined opts p a
Refined a
a
       Either (TT Any) Bool
_ -> let s :: String
s = POpts -> TT Bool -> String
forall x. Show x => POpts -> TT x -> String
prtTree POpts
o TT Bool
tt
                bp :: String
bp = POpts -> Val Bool -> String
colorValBool POpts
o (TT Bool
tt TT Bool -> Getting (Val Bool) (TT Bool) (Val Bool) -> Val Bool
forall s a. s -> Getting a s a -> a
^. Getting (Val Bool) (TT Bool) (Val Bool)
forall a b. Lens (TT a) (TT b) (Val a) (Val b)
ttVal)
            in case POpts -> HKD Identity Debug
forall (f :: Type -> Type). HOpts f -> HKD f Debug
oDebug POpts
o of
                 HKD Identity Debug
DZero -> String -> Refined opts p a
forall a. HasCallStack => String -> a
error String
bp
                 HKD Identity Debug
DLite -> String -> Refined opts p a
forall a. HasCallStack => String -> a
error (String -> Refined opts p a) -> String -> Refined opts p a
forall a b. (a -> b) -> a -> b
$ String
bp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> ShowS
nullIf String
"\n" String
s
                 HKD Identity Debug
_ -> String -> Refined opts p a
forall a. HasCallStack => String -> a
error (String -> Refined opts p a) -> String -> Refined opts p a
forall a b. (a -> b) -> a -> b
$ String
bp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> ShowS
nullIf String
"\n" String
s