-- refined5 doesnt care about the input as it is thrown away so we have no choice but to use PP ip i

-- like Refined2 but discards the original input value

-- all instances uses the internal values except for IsString [internal value is less likely to be a string!]

--   but json/binary/hash use internal input (ie PP ip i) as they json and binary have to roundtrip

-- tojson only has access to PP ip i! so fromjson can only use this!

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE NoStarIsType #-}
-- | refinement type allowing the external type to differ from the internal type

module Predicate.Refined5 (

  -- ** Refined5

    Refined5
  , unRefined5

  -- ** evaluation methods

  , eval5P
  , eval5M
  , newRefined5
  , newRefined5'
  , newRefined5P
  , newRefined5P'

  -- ** proxy methods

  , MakeR5

  -- ** QuickCheck methods

  , genRefined5
  , genRefined5P

  -- ** unsafe methods for creating Refined5

  , unsafeRefined5
  , unsafeRefined5'

 ) where
import Predicate.Refined2 (Msg2(..), RResults2(..), prt2Impl, Refined2C)
import Predicate.Refined (RefinedC)
import Predicate.Core
import Predicate.Misc
import Predicate.Util
import Data.Proxy (Proxy(..))
import Data.Aeson (ToJSON(..), FromJSON(..))
import qualified Language.Haskell.TH.Syntax as TH
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 Control.Lens
import Data.String (IsString(..))
import Data.Hashable (Hashable(..))
import GHC.Stack (HasCallStack)
import Test.QuickCheck
import Data.Coerce (coerce)
import Data.Either (isRight)
import Data.Char (isSpace)
import Control.Arrow (left)
import Data.Tree.Lens (root)
import Control.DeepSeq (NFData)

-- $setup

-- >>> :set -XDataKinds

-- >>> :set -XTypeApplications

-- >>> :set -XTypeOperators

-- >>> :set -XOverloadedStrings

-- >>> :m + Predicate.Prelude

-- >>> :m + Predicate.Refined2

-- >>> :m + Data.Time


-- | Refinement type for specifying an input type that is different from the output type

--

--   * @opts@ are the display options

--   * @ip@ converts @i@ to @PP ip i@ which is stored

--   * @op@ validates that internal type using @PP op (PP ip i) ~ Bool@

--   * @i@ is the input type which is discarded after converting to PP ip i

--

newtype Refined5 (opts :: Opt) ip op i = Refined5 (PP ip i)

type role Refined5 phantom nominal nominal nominal

-- | extract the value from 'Refined5'

unRefined5 :: forall k k1 (opts :: Opt) (ip :: k) (op :: k1) i
   . Refined5 opts ip op i
  -> PP ip i
unRefined5 :: Refined5 opts ip op i -> PP ip i
unRefined5 = Refined5 opts ip op i -> PP ip i
coerce

-- | directly load values into 'Refined5'. It still checks to see that those values are valid

unsafeRefined5' :: forall opts ip op i
                . ( Refined2C opts ip op i
                  , HasCallStack
                  )
                => PP ip i
                -> Refined5 opts ip op i
unsafeRefined5' :: PP ip i -> Refined5 opts ip op i
unsafeRefined5' = ([Char] -> Refined5 opts ip op i)
-> (PP ip i -> Refined5 opts ip op i)
-> Either [Char] (PP ip i)
-> Refined5 opts ip op i
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either [Char] -> Refined5 opts ip op i
forall a. HasCallStack => [Char] -> a
error PP ip i -> Refined5 opts ip op i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
PP ip i -> Refined5 opts ip op i
Refined5 (Either [Char] (PP ip i) -> Refined5 opts ip op i)
-> (PP ip i -> Either [Char] (PP ip i))
-> PP ip i
-> Refined5 opts ip op i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
(PP op a ~ Bool, RefinedC opts op a) =>
a -> Either [Char] a
forall k (opts :: Opt) (p :: k) a.
(PP p a ~ Bool, RefinedC opts p a) =>
a -> Either [Char] a
evalBool5 @opts @op

-- | directly load values into 'Refined5' without any checking

unsafeRefined5 :: forall opts ip op i
   . PP ip i
  -> Refined5 opts ip op i
unsafeRefined5 :: PP ip i -> Refined5 opts ip op i
unsafeRefined5 = PP ip i -> Refined5 opts ip op i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
PP ip i -> Refined5 opts ip op i
Refined5

deriving newtype instance ( Refined2C opts ip op i
                          , NFData (PP ip i)
                          ) => NFData (Refined5 opts ip op i)
deriving stock instance  ( Refined2C opts ip op i
                         , Show (PP ip i)
                         ) => Show (Refined5 opts ip op i)
deriving stock instance ( Refined2C opts ip op i
                        , Eq (PP ip i)
                        ) => Eq (Refined5 opts ip op i)
deriving stock instance ( Refined2C opts ip op i
                        , Ord (PP ip i)
                        ) => Ord (Refined5 opts ip op i)
deriving stock instance ( Refined2C opts ip op i
                        , TH.Lift (PP ip i)
                        ) => TH.Lift (Refined5 opts ip op i)

-- | 'IsString' instance for Refined5

--

-- >>> pureTryTest $ fromString @(Refined5 OL (ReadP Int Id) (Id > 12) String) "523"

-- Right (Refined5 523)

--

-- >>> pureTryTest $ fromString @(Refined5 OL (ReadP Int Id) (Id > 12) String) "2"

-- Left ()

--

instance ( i ~ String
         , Refined2C opts ip op i
         , Show (PP ip i)
         ) => IsString (Refined5 opts ip op i) where
  fromString :: [Char] -> Refined5 opts ip op i
fromString [Char]
i =
    case [Char] -> Either Msg2 (Refined5 opts ip op [Char])
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
(Refined2C opts ip op i, Show (PP ip i)) =>
i -> Either Msg2 (Refined5 opts ip op i)
newRefined5 [Char]
i of
      Left Msg2
e -> [Char] -> Refined5 opts ip op i
forall a. HasCallStack => [Char] -> a
error ([Char] -> Refined5 opts ip op i)
-> [Char] -> Refined5 opts ip op i
forall a b. (a -> b) -> a -> b
$ [Char]
"Refined5(IsString:fromString):" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg2 -> [Char]
forall a. Show a => a -> [Char]
show Msg2
e
      Right Refined5 opts ip op [Char]
r -> Refined5 opts ip op i
Refined5 opts ip op [Char]
r

-- read instance from -ddump-deriv

-- | 'Read' instance for 'Refined5'

--

-- >>> reads @(Refined5 OZ (ReadBase Int 16) (0 <..> 0xff) String) "Refined5 254"

-- [(Refined5 254,"")]

--

-- >>> reads @(Refined5 OZ (ReadBase Int 16) (0 <..> 0xff) String) "Refined5 300"

-- []

--

-- >>> reads @(Refined5 OZ (ReadBase Int 16) (Id < 0) String) "Refined5 -1234"

-- [(Refined5 (-1234),"")]

--

-- >>> reads @(Refined5 OZ (Map' (ReadP Int Id) (Resplit "\\.")) (GuardBool "len/=4" (Len == 4)) String) "Refined5 [192,168,0,1]"

-- [(Refined5 [192,168,0,1],"")]

--

-- >>> reads @(Refined5 OZ (ReadP Rational Id) (Id > Negate 4 % 3) String) "Refined5 (-10 % 9)"

-- [(Refined5 ((-10) % 9),"")]

--

-- >>> reads @(Refined5 OZ (ReadP Rational Id) (Id > Negate 4 % 3) String) "Refined5 (-10 % 6)"

-- []


instance ( Refined2C opts ip op i
         , Read (PP ip i)
         ) => Read (Refined5 opts ip op i) where
    readPrec :: ReadPrec (Refined5 opts ip op i)
readPrec
      = ReadPrec (Refined5 opts ip op i)
-> ReadPrec (Refined5 opts ip op i)
forall a. ReadPrec a -> ReadPrec a
GR.parens
          (Int
-> ReadPrec (Refined5 opts ip op i)
-> ReadPrec (Refined5 opts ip op i)
forall a. Int -> ReadPrec a -> ReadPrec a
PCR.prec
             Int
11
             (do Lexeme -> ReadPrec ()
GR.expectP ([Char] -> Lexeme
RL.Ident [Char]
"Refined5")
                 PP ip i
fld0 <- ReadPrec (PP ip i) -> ReadPrec (PP ip i)
forall a. ReadPrec a -> ReadPrec a
PCR.reset ReadPrec (PP ip i)
forall a. Read a => ReadPrec a
GR.readPrec
                 case PP ip i -> Either [Char] (PP op (PP ip i))
forall k (opts :: Opt) (p :: k) i.
(OptC opts, P p i) =>
i -> Either [Char] (PP p i)
evalQuick @opts @op PP ip i
fld0 of
                   Left {} -> [Char] -> ReadPrec (Refined5 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
""
                   Right PP op (PP ip i)
True -> Refined5 opts ip op i -> ReadPrec (Refined5 opts ip op i)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PP ip i -> Refined5 opts ip op i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
PP ip i -> Refined5 opts ip op i
Refined5 PP ip i
fld0)
                   Right PP op (PP ip i)
False -> [Char] -> ReadPrec (Refined5 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
""
             ))
    readList :: ReadS [Refined5 opts ip op i]
readList = ReadS [Refined5 opts ip op i]
forall a. Read a => ReadS [a]
GR.readListDefault
    readListPrec :: ReadPrec [Refined5 opts ip op i]
readListPrec = ReadPrec [Refined5 opts ip op i]
forall a. Read a => ReadPrec [a]
GR.readListPrecDefault

-- | 'ToJSON' instance for 'Refined5'

--

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

-- >>> A.encode (unsafeRefined5' @OZ @(ReadBase Int 16) @(Between 0 255 Id) 254)

-- "254"

--

-- >>> A.encode (unsafeRefined5 @OZ @Id @'True @Int 123)

-- "123"

--

instance ( Refined2C opts ip op i
         , ToJSON (PP ip i)
         ) => ToJSON (Refined5 opts ip op i) where
  toJSON :: Refined5 opts ip op i -> Value
toJSON (Refined5 PP ip i
x) = PP ip i -> Value
forall a. ToJSON a => a -> Value
toJSON PP ip i
x

-- | 'FromJSON' instance for 'Refined5'

--

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

-- >>> A.eitherDecode' @(Refined5 OZ (ReadBase Int 16) (Id > 10 && Id < 256) String) "123"

-- Right (Refined5 123)

--

-- >>> removeAnsi $ A.eitherDecode' @(Refined5 OL (ReadBase Int 16) (Id > 10 && Id < 256) String) "9"

-- Error in $: Refined5(FromJSON:parseJSON):false boolean check | {False && True | (9 > 10)}

-- False

--

-- >>> A.eitherDecode' @(Refined5 OZ (ReadBase Int 16) (Id > 10 && Id < 256) String) "254"

-- Right (Refined5 254)

--

-- >>> removeAnsi $ A.eitherDecode' @(Refined5 OAN (ReadBase Int 16) (Id > 10 && Id < 256) String) "12345"

-- Error in $: Refined5(FromJSON:parseJSON):false boolean check | {True && False | (12345 < 256)}

-- False True && False | (12345 < 256)

-- |

-- +- True 12345 > 10

-- |  |

-- |  +- P Id 12345

-- |  |

-- |  `- P '10

-- |

-- `- False 12345 < 256

--    |

--    +- P Id 12345

--    |

--    `- P '256

--

instance ( Refined2C opts ip op i
         , FromJSON (PP ip i)
         ) => FromJSON (Refined5 opts ip op i) where
  parseJSON :: Value -> Parser (Refined5 opts ip op i)
parseJSON Value
z = do
                  PP ip i
i <- Value -> Parser (PP ip i)
forall a. FromJSON a => Value -> Parser a
parseJSON @(PP ip i) Value
z
                  case PP ip i -> Either [Char] (PP ip i)
forall k (opts :: Opt) (p :: k) a.
(PP p a ~ Bool, RefinedC opts p a) =>
a -> Either [Char] a
evalBool5 @opts @op PP ip i
i of
                    Left [Char]
e -> [Char] -> Parser (Refined5 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> Parser (Refined5 opts ip op i))
-> [Char] -> Parser (Refined5 opts ip op i)
forall a b. (a -> b) -> a -> b
$ [Char]
"Refined5(FromJSON:parseJSON):" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
e
                    Right PP ip i
_ -> Refined5 opts ip op i -> Parser (Refined5 opts ip op i)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PP ip i -> Refined5 opts ip op i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
PP ip i -> Refined5 opts ip op i
Refined5 PP ip i
i)

-- | 'Arbitrary' instance for 'Refined5'

--

-- >>> :m + Data.Time.Calendar.WeekDate

-- >>> xs <- generate (vectorOf 10 (arbitrary @(Refined5 OAN (ReadP Int Id) (Negate 10 <..> 10) String)))

-- >>> all (\x -> unRefined5 x `elem` [-10 .. 10]) xs

-- True

--

instance ( Arbitrary (PP ip i)
         , Refined2C opts ip op i
         ) => Arbitrary (Refined5 opts ip op i) where
  arbitrary :: Gen (Refined5 opts ip op i)
arbitrary = Gen (PP ip i) -> Gen (Refined5 opts ip op i)
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
(Refined2C opts ip op i, HasCallStack) =>
Gen (PP ip i) -> Gen (Refined5 opts ip op i)
genRefined5 Gen (PP ip i)
forall a. Arbitrary a => Gen a
arbitrary

-- | create a 'Refined5' generator using a generator to restrict the values (so it completes)

genRefined5 ::
    forall opts ip op i
  . ( Refined2C opts ip op i
    , HasCallStack
    )
  => Gen (PP ip i)
  -> Gen (Refined5 opts ip op i)
genRefined5 :: Gen (PP ip i) -> Gen (Refined5 opts ip op i)
genRefined5 = Proxy '(opts, ip, op, i)
-> Gen (PP ip i) -> Gen (Refined5 opts ip op i)
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
(Refined2C opts ip op i, HasCallStack) =>
Proxy '(opts, ip, op, i)
-> Gen (PP ip i) -> Gen (Refined5 opts ip op i)
genRefined5P Proxy '(opts, ip, op, i)
forall k (t :: k). Proxy t
Proxy

-- generates the external value unlike Refined3 as we dont have a way to recreate the output from the internal value

-- | create a 'Refined5' generator using a proxy

genRefined5P ::
    forall opts ip op i
  . ( Refined2C opts ip op i
    , HasCallStack
    )
  => Proxy '(opts,ip,op,i)
  -> Gen (PP ip i)
  -> Gen (Refined5 opts ip op i)
genRefined5P :: Proxy '(opts, ip, op, i)
-> Gen (PP ip i) -> Gen (Refined5 opts ip op i)
genRefined5P Proxy '(opts, ip, op, i)
_ Gen (PP ip i)
g =
  let f :: Int -> Gen (Refined5 opts ip op i)
f !Int
cnt = do
        Maybe (PP ip i)
mi <- Gen (PP ip i) -> (PP ip i -> Bool) -> Gen (Maybe (PP ip i))
forall a. Gen a -> (a -> Bool) -> Gen (Maybe a)
suchThatMaybe Gen (PP ip i)
g (Either [Char] (PP ip i) -> Bool
forall a b. Either a b -> Bool
isRight (Either [Char] (PP ip i) -> Bool)
-> (PP ip i -> Either [Char] (PP ip i)) -> PP ip i -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
(PP op a ~ Bool, RefinedC opts op a) =>
a -> Either [Char] a
forall k (opts :: Opt) (p :: k) a.
(PP p a ~ Bool, RefinedC opts p a) =>
a -> Either [Char] a
evalBool5 @opts @op)
        case Maybe (PP ip i)
mi of
          Maybe (PP ip i)
Nothing ->
             let o :: POpts
o = OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts
             in if Int
cnt Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= POpts -> HKD Identity Int
forall (f :: Type -> Type). HOpts f -> HKD f Int
oRecursion POpts
o
                then [Char] -> Gen (Refined5 opts ip op i)
forall a. HasCallStack => [Char] -> a
error ([Char] -> Gen (Refined5 opts ip op i))
-> [Char] -> Gen (Refined5 opts ip op i)
forall a b. (a -> b) -> a -> b
$ POpts -> ShowS
setOtherEffects POpts
o ([Char]
"genRefined5P recursion exceeded(" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (POpts -> HKD Identity Int
forall (f :: Type -> Type). HOpts f -> HKD f Int
oRecursion POpts
o) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")")
             else Int -> Gen (Refined5 opts ip op i)
f (Int
cntInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
          Just PP ip i
i -> Refined5 opts ip op i -> Gen (Refined5 opts ip op i)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Refined5 opts ip op i -> Gen (Refined5 opts ip op i))
-> Refined5 opts ip op i -> Gen (Refined5 opts ip op i)
forall a b. (a -> b) -> a -> b
$ PP ip i -> Refined5 opts ip op i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
PP ip i -> Refined5 opts ip op i
unsafeRefined5 PP ip i
i
  in Int -> Gen (Refined5 opts ip op i)
f Int
0

-- | 'Binary' instance for 'Refined5'

--

instance ( Refined2C opts ip op i
         , Binary (PP ip i)
         ) => Binary (Refined5 opts ip op i) where
  get :: Get (Refined5 opts ip op i)
get = do
          PP ip i
i <- Binary (PP ip i) => Get (PP ip i)
forall t. Binary t => Get t
B.get @(PP ip i)
          case PP ip i -> Either [Char] (PP ip i)
forall k (opts :: Opt) (p :: k) a.
(PP p a ~ Bool, RefinedC opts p a) =>
a -> Either [Char] a
evalBool5 @opts @op PP ip i
i of
            Left [Char]
e -> [Char] -> Get (Refined5 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> Get (Refined5 opts ip op i))
-> [Char] -> Get (Refined5 opts ip op i)
forall a b. (a -> b) -> a -> b
$ [Char]
"Refined5(Binary:get):" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
e
            Right PP ip i
_ -> Refined5 opts ip op i -> Get (Refined5 opts ip op i)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Refined5 opts ip op i -> Get (Refined5 opts ip op i))
-> Refined5 opts ip op i -> Get (Refined5 opts ip op i)
forall a b. (a -> b) -> a -> b
$ PP ip i -> Refined5 opts ip op i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
PP ip i -> Refined5 opts ip op i
Refined5 PP ip i
i
  put :: Refined5 opts ip op i -> Put
put (Refined5 PP ip i
r) = PP ip i -> Put
forall t. Binary t => t -> Put
B.put @(PP ip i) PP ip i
r

-- | 'Hashable' instance for 'Refined5'

instance ( Refined2C opts ip op i
         , Hashable (PP ip i)
         ) => Hashable (Refined5 opts ip op i) where
  hashWithSalt :: Int -> Refined5 opts ip op i -> Int
hashWithSalt Int
s (Refined5 PP ip i
b) = Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ PP ip i -> Int
forall a. Hashable a => a -> Int
hash PP ip i
b

-- | creating a 'Refined5' value for any 'MonadEval'

newRefined5' :: forall opts ip op i m
  . ( MonadEval m
    , Refined2C opts ip op i
    , Show (PP ip i)
    )
  => i
  -> m (Either Msg2 (Refined5 opts ip op i))
newRefined5' :: i -> m (Either Msg2 (Refined5 opts ip op i))
newRefined5' = Proxy '(opts, ip, op, i)
-> i -> m (Either Msg2 (Refined5 opts ip op i))
forall k k (opts :: Opt) (ip :: k) (op :: k) i
       (proxy :: (Opt, k, k, Type) -> Type) (m :: Type -> Type).
(MonadEval m, Refined2C opts ip op i, Show (PP ip i)) =>
proxy '(opts, ip, op, i)
-> i -> m (Either Msg2 (Refined5 opts ip op i))
newRefined5P' Proxy '(opts, ip, op, i)
forall k (t :: k). Proxy t
Proxy

-- | same as 'newRefined5P' but runs for any MonadEval instance

newRefined5P' :: forall opts ip op i proxy m
  . ( MonadEval m
    , Refined2C opts ip op i
    , Show (PP ip i)
    )
  => proxy '(opts,ip,op,i)
  -> i
  -> m (Either Msg2 (Refined5 opts ip op i))
newRefined5P' :: proxy '(opts, ip, op, i)
-> i -> m (Either Msg2 (Refined5 opts ip op i))
newRefined5P' proxy '(opts, ip, op, i)
_ i
i = do
  (RResults2 (PP ip i)
ret,Maybe (Refined5 opts ip op i)
mr) <- i -> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
forall k k (opts :: Opt) (ip :: k) (op :: k) i (m :: Type -> Type).
(MonadEval m, Refined2C opts ip op i) =>
i -> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
eval5M i
i
  Either Msg2 (Refined5 opts ip op i)
-> m (Either Msg2 (Refined5 opts ip op i))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Either Msg2 (Refined5 opts ip op i)
 -> m (Either Msg2 (Refined5 opts ip op i)))
-> Either Msg2 (Refined5 opts ip op i)
-> m (Either Msg2 (Refined5 opts ip op i))
forall a b. (a -> b) -> a -> b
$ Either Msg2 (Refined5 opts ip op i)
-> (Refined5 opts ip op i -> Either Msg2 (Refined5 opts ip op i))
-> Maybe (Refined5 opts ip op i)
-> Either Msg2 (Refined5 opts ip op i)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Msg2 -> Either Msg2 (Refined5 opts ip op i)
forall a b. a -> Either a b
Left (Msg2 -> Either Msg2 (Refined5 opts ip op i))
-> Msg2 -> Either Msg2 (Refined5 opts ip op i)
forall a b. (a -> b) -> a -> b
$ POpts -> RResults2 (PP ip i) -> Msg2
forall a. Show a => POpts -> RResults2 a -> Msg2
prt2Impl (OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts) RResults2 (PP ip i)
ret) Refined5 opts ip op i -> Either Msg2 (Refined5 opts ip op i)
forall a b. b -> Either a b
Right Maybe (Refined5 opts ip op i)
mr

-- | pure version for creating a 'Refined5' value

--

-- >>> newRefined5 @OZ @(ReadBase Int 16) @(Lt 255) "00fe"

-- Right (Refined5 254)

--

-- >>> newRefined5 @OZ @(ReadBase Int 16) @(GuardBool (PrintF "%#x is too large" Id) (Lt 253)) "00fe"

-- Left Step 2. Failed Boolean Check(op) | 0xfe is too large

--

-- >>> newRefined5 @OZ @(ReadBase Int 16) @(Lt 255) "00fg"

-- Left Step 1. Failed Initial Conversion(ip) | invalid base 16

--

-- >>> newRefined5 @OL @(Map' (ReadP Int Id) (Resplit "\\.")) @(Msg "length invalid:" (Len == 4)) "198.162.3.1.5"

-- Left Step 2. False Boolean Check(op) | {length invalid: 5 == 4}

--

-- >>> newRefined5 @OZ @(Map' (ReadP Int Id) (Resplit "\\.")) @(GuardBool (PrintF "found length=%d" Len) (Len == 4)) "198.162.3.1.5"

-- Left Step 2. Failed Boolean Check(op) | found length=5

--

-- >>> newRefined5 @OZ @(Map' (ReadP Int Id) (Resplit "\\.")) @(GuardBool (PrintF "found length=%d" Len) (Len == 4)) "198.162.3.1"

-- Right (Refined5 [198,162,3,1])

--

-- >>> :m + Data.Time.Calendar.WeekDate

-- >>> newRefined5 @OZ @(MkDayExtra Id >> 'Just Id) @(GuardBool "expected a Sunday" (Thd == 7)) (2019,10,13)

-- Right (Refined5 (2019-10-13,41,7))

--

-- >>> newRefined5 @OL @(MkDayExtra Id >> 'Just Id) @(Msg "expected a Sunday:" (Thd == 7)) (2019,10,12)

-- Left Step 2. False Boolean Check(op) | {expected a Sunday: 6 == 7}

--

-- >>> newRefined5 @OZ @(MkDayExtra' Fst Snd Thd >> 'Just Id) @(GuardBool "expected a Sunday" (Thd == 7)) (2019,10,12)

-- Left Step 2. Failed Boolean Check(op) | expected a Sunday

--

-- >>> newRefined5 @OL @Id @'True 22

-- Right (Refined5 22)

--

-- >>> newRefined5 @OL @(ReadP UTCTime Id) @(Between (MkDay '(2020,5,2)) (MkDay '(2020,5,7)) (MkJust ToDay)) "2020-05-04 12:13:14Z"

-- Right (Refined5 2020-05-04 12:13:14 UTC)

--

-- >>> newRefined5 @OL @(ReadP UTCTime Id) @(Between (MkDay '(2020,5,2)) (MkDay '(2020,5,7)) (MkJust ToDay)) "2020-05-08 12:13:14Z"

-- Left Step 2. False Boolean Check(op) | {Just 2020-05-08 <= Just 2020-05-07}

--

newRefined5 :: forall opts ip op i
  . ( Refined2C opts ip op i
    , Show (PP ip i)
    ) => i
    -> Either Msg2 (Refined5 opts ip op i)
newRefined5 :: i -> Either Msg2 (Refined5 opts ip op i)
newRefined5 = Proxy '(opts, ip, op, i)
-> i -> Either Msg2 (Refined5 opts ip op i)
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
(Refined2C opts ip op i, Show (PP ip i)) =>
Proxy '(opts, ip, op, i)
-> i -> Either Msg2 (Refined5 opts ip op i)
newRefined5P Proxy '(opts, ip, op, i)
forall k (t :: k). Proxy t
Proxy

-- | create a Refined5 using a 4-tuple proxy and aggregate the results on failure

newRefined5P :: forall opts ip op i
  . ( Refined2C opts ip op i
    , Show (PP ip i)
    ) => Proxy '(opts,ip,op,i)
    -> i
    -> Either Msg2 (Refined5 opts ip op i)
newRefined5P :: Proxy '(opts, ip, op, i)
-> i -> Either Msg2 (Refined5 opts ip op i)
newRefined5P Proxy '(opts, ip, op, i)
_ i
i =
  let (RResults2 (PP ip i)
ret,Maybe (Refined5 opts ip op i)
mr) = Identity (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
-> (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
forall a. Identity a -> a
runIdentity (Identity (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
 -> (RResults2 (PP ip i), Maybe (Refined5 opts ip op i)))
-> Identity (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
-> (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
forall a b. (a -> b) -> a -> b
$ i -> Identity (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
forall k k (opts :: Opt) (ip :: k) (op :: k) i (m :: Type -> Type).
(MonadEval m, Refined2C opts ip op i) =>
i -> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
eval5M i
i
  in Either Msg2 (Refined5 opts ip op i)
-> (Refined5 opts ip op i -> Either Msg2 (Refined5 opts ip op i))
-> Maybe (Refined5 opts ip op i)
-> Either Msg2 (Refined5 opts ip op i)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Msg2 -> Either Msg2 (Refined5 opts ip op i)
forall a b. a -> Either a b
Left (Msg2 -> Either Msg2 (Refined5 opts ip op i))
-> Msg2 -> Either Msg2 (Refined5 opts ip op i)
forall a b. (a -> b) -> a -> b
$ POpts -> RResults2 (PP ip i) -> Msg2
forall a. Show a => POpts -> RResults2 a -> Msg2
prt2Impl (OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts) RResults2 (PP ip i)
ret) Refined5 opts ip op i -> Either Msg2 (Refined5 opts ip op i)
forall a b. b -> Either a b
Right Maybe (Refined5 opts ip op i)
mr

-- | create a 'Refined5' value using a 4-tuple proxy (see 'Predicate.Refined2.mkProxy2')

eval5P :: forall opts ip op i m
  . ( Refined2C opts ip op i
    , MonadEval m
    )
  => Proxy '(opts,ip,op,i)
  -> i
  -> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
eval5P :: Proxy '(opts, ip, op, i)
-> i -> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
eval5P Proxy '(opts, ip, op, i)
_ = i -> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
forall k k (opts :: Opt) (ip :: k) (op :: k) i (m :: Type -> Type).
(MonadEval m, Refined2C opts ip op i) =>
i -> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
eval5M

-- | workhorse for creating 'Refined5' values

eval5M :: forall opts ip op i m
  . ( MonadEval m
    , Refined2C opts ip op i
    )
  => i
  -> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
eval5M :: i -> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
eval5M i
i = do
  let o :: POpts
o = OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts
  TT (PP ip i)
ll <- Proxy ip -> POpts -> i -> m (TT (PP ip i))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy ip
forall k (t :: k). Proxy t
Proxy @ip) POpts
o i
i
  case TT (PP ip i) -> (Either [Char] (PP ip i), Tree PE)
forall a. TT a -> (Either [Char] a, Tree PE)
getValAndPE TT (PP ip i)
ll of
   (Right PP ip i
a, Tree PE
t1) -> do
     TT Bool
rr <- Proxy op -> POpts -> PP ip i -> m (TT (PP op (PP ip i)))
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 op
forall k (t :: k). Proxy t
Proxy @op) POpts
o PP ip i
a
     (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
-> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
 -> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i)))
-> (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
-> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
forall a b. (a -> b) -> a -> b
$ case TT Bool -> (Either [Char] Bool, Tree PE)
forall a. TT a -> (Either [Char] a, Tree PE)
getValAndPE TT Bool
rr of
      (Right Bool
True,Tree PE
t2) -> (PP ip i -> Tree PE -> Tree PE -> RResults2 (PP ip i)
forall a. a -> Tree PE -> Tree PE -> RResults2 a
RTTrue PP ip i
a Tree PE
t1 Tree PE
t2, Refined5 opts ip op i -> Maybe (Refined5 opts ip op i)
forall a. a -> Maybe a
Just (PP ip i -> Refined5 opts ip op i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
PP ip i -> Refined5 opts ip op i
Refined5 PP ip i
a))
      (Right Bool
False,Tree PE
t2) -> (PP ip i -> Tree PE -> Tree PE -> RResults2 (PP ip i)
forall a. a -> Tree PE -> Tree PE -> RResults2 a
RTFalse PP ip i
a Tree PE
t1 Tree PE
t2, Maybe (Refined5 opts ip op i)
forall a. Maybe a
Nothing)
      (Left [Char]
e,Tree PE
t2) -> (PP ip i -> Tree PE -> [Char] -> Tree PE -> RResults2 (PP ip i)
forall a. a -> Tree PE -> [Char] -> Tree PE -> RResults2 a
RTF PP ip i
a Tree PE
t1 [Char]
e Tree PE
t2, Maybe (Refined5 opts ip op i)
forall a. Maybe a
Nothing)
   (Left [Char]
e,Tree PE
t1) -> (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
-> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([Char] -> Tree PE -> RResults2 (PP ip i)
forall a. [Char] -> Tree PE -> RResults2 a
RF [Char]
e Tree PE
t1, Maybe (Refined5 opts ip op i)
forall a. Maybe a
Nothing)

-- | creates a 4-tuple proxy (see 'eval5P' 'newRefined5P')

--

-- use type application to set the 4-tuple or set the individual parameters directly

--

-- set the 4-tuple directly

--

-- >>> eg1 = mkProxy2 @'(OL, ReadP Int Id, Gt 10, String)

-- >>> newRefined5P eg1 "24"

-- Right (Refined5 24)

--

-- skip the 4-tuple and set each parameter individually using type application

--

-- >>> eg2 = mkProxy2 @_ @OL @(ReadP Int Id) @(Gt 10)

-- >>> newRefined5P eg2 "24"

-- Right (Refined5 24)

--


-- | type family for converting from a 4-tuple '(opts,ip,op,i) to a 'Refined5' type

type family MakeR5 p where
  MakeR5 '(opts,ip,op,i) = Refined5 opts ip op i

evalBool5 :: forall opts p a
   . (PP p a ~ Bool, RefinedC opts p a)
   => a
   -> Either String a
evalBool5 :: a -> Either [Char] a
evalBool5 a
i =
  let pp :: TT Bool
pp = 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) (OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts) a
i
      opts :: POpts
opts = OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts
      (Either [Char] Bool
lr,Tree PE
p2) = TT Bool -> (Either [Char] Bool, Tree PE)
forall a. TT a -> (Either [Char] a, Tree PE)
getValAndPE TT Bool
pp
      z :: [Char]
z = let zz :: [Char]
zz = Tree PE
p2 Tree PE -> Getting [Char] (Tree PE) [Char] -> [Char]
forall s a. s -> Getting a s a -> a
^. (PE -> Const [Char] PE) -> Tree PE -> Const [Char] (Tree PE)
forall a. Lens' (Tree a) a
root ((PE -> Const [Char] PE) -> Tree PE -> Const [Char] (Tree PE))
-> (([Char] -> Const [Char] [Char]) -> PE -> Const [Char] PE)
-> Getting [Char] (Tree PE) [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> Const [Char] [Char]) -> PE -> Const [Char] PE
Lens' PE [Char]
peString
          in if (Char -> Bool) -> [Char] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace [Char]
zz then [Char]
"FalseP" else [Char]
"{" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
zz [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"}"
      w :: Either [Char] a
w = case Either [Char] Bool
lr of
            Right Bool
True -> a -> Either [Char] a
forall a b. b -> Either a b
Right a
i
            Right Bool
False -> [Char] -> Either [Char] a
forall a b. a -> Either a b
Left ([Char] -> Either [Char] a) -> [Char] -> Either [Char] a
forall a b. (a -> b) -> a -> b
$ [Char]
"false boolean check" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char] -> ShowS
nullIf [Char]
" | " [Char]
z
            Left [Char]
e -> [Char] -> Either [Char] a
forall a b. a -> Either a b
Left ([Char] -> Either [Char] a) -> [Char] -> Either [Char] a
forall a b. (a -> b) -> a -> b
$ [Char]
"failed boolean check " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char] -> ShowS
nullIf [Char]
" | " [Char]
e
  in ShowS -> Either [Char] a -> Either [Char] a
forall (a :: Type -> Type -> Type) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left ([Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ([Char]
"\n" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ POpts -> Tree PE -> [Char]
prtTreePure POpts
opts Tree PE
p2)) Either [Char] a
w