-- 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 DeriveGeneric #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE NoStarIsType #-}
-- | refinement type allowing the external type to differ from the internal type but throws away the original value

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'

 -- ** exception

  , Refined5Exception(..)
 ) where
import Predicate.Refined2 (Msg2(..), RResults2(..), prt2Impl, Refined2C)
import Predicate.Refined (RefinedC)
import Predicate.Core
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 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)
import qualified Control.Exception as E
import GHC.Generics (Generic)
-- $setup

-- >>> :set -XDataKinds

-- >>> :set -XTypeApplications

-- >>> :set -XTypeOperators

-- >>> :set -XOverloadedStrings

-- >>> :m + Predicate

-- >>> :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
                  )
                => PP ip i
                -> Refined5 opts ip op i
unsafeRefined5' :: PP ip i -> Refined5 opts ip op i
unsafeRefined5' = (String -> Refined5 opts ip op i)
-> (PP ip i -> Refined5 opts ip op i)
-> Either String (PP ip i)
-> Refined5 opts ip op i
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Refined5Exception -> Refined5 opts ip op i
forall a e. Exception e => e -> a
E.throw (Refined5Exception -> Refined5 opts ip op i)
-> (String -> Refined5Exception) -> String -> Refined5 opts ip op i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Refined5Exception
Refined5Exception) 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 String (PP ip i) -> Refined5 opts ip op i)
-> (PP ip i -> Either String (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 String a
forall k (opts :: Opt) (p :: k) a.
(PP p a ~ Bool, RefinedC opts p a) =>
a -> Either String 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 :: String -> Refined5 opts ip op i
fromString String
i =
    case String -> Either Msg2 (Refined5 opts ip op String)
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 String
i of
      Left Msg2
e -> Refined5Exception -> Refined5 opts ip op i
forall a e. Exception e => e -> a
E.throw (Refined5Exception -> Refined5 opts ip op i)
-> Refined5Exception -> Refined5 opts ip op i
forall a b. (a -> b) -> a -> b
$ String -> Refined5Exception
Refined5Exception (String -> Refined5Exception) -> String -> Refined5Exception
forall a b. (a -> b) -> a -> b
$ String
"IsString:fromString:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg2 -> String
forall a. Show a => a -> String
show Msg2
e
      Right Refined5 opts ip op String
r -> Refined5 opts ip op i
Refined5 opts ip op String
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 (String -> Lexeme
RL.Ident String
"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 String (PP op (PP ip i))
forall k (opts :: Opt) (p :: k) i.
(OptC opts, P p i) =>
i -> Either String (PP p i)
evalQuick @opts @op PP ip i
fld0 of
                   Left {} -> String -> ReadPrec (Refined5 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
""
                   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 -> String -> ReadPrec (Refined5 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
""
             ))
    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 String (PP ip i)
forall k (opts :: Opt) (p :: k) a.
(PP p a ~ Bool, RefinedC opts p a) =>
a -> Either String a
evalBool5 @opts @op PP ip i
i of
                    Left String
e -> String -> Parser (Refined5 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Parser (Refined5 opts ip op i))
-> String -> Parser (Refined5 opts ip op i)
forall a b. (a -> b) -> a -> b
$ String
"Refined5(FromJSON:parseJSON):" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
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 =>
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
  => 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 =>
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
  => 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 o :: POpts
o = OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts
      r :: Int
r = POpts -> Int
getMaxRecursionValue POpts
o
      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 String (PP ip i) -> Bool
forall a b. Either a b -> Bool
isRight (Either String (PP ip i) -> Bool)
-> (PP ip i -> Either String (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 String a
forall k (opts :: Opt) (p :: k) a.
(PP p a ~ Bool, RefinedC opts p a) =>
a -> Either String a
evalBool5 @opts @op)
        case Maybe (PP ip i)
mi of
          Maybe (PP ip i)
Nothing | Int
cnt Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
r -> Refined5Exception -> Gen (Refined5 opts ip op i)
forall a e. Exception e => e -> a
E.throw (Refined5Exception -> Gen (Refined5 opts ip op i))
-> Refined5Exception -> Gen (Refined5 opts ip op i)
forall a b. (a -> b) -> a -> b
$ String -> Refined5Exception
Refined5Exception (String -> Refined5Exception) -> String -> Refined5Exception
forall a b. (a -> b) -> a -> b
$ POpts -> ShowS
setOtherEffects POpts
o (String
"genRefined5P 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
")")
                  | Bool
otherwise -> 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 String (PP ip i)
forall k (opts :: Opt) (p :: k) a.
(PP p a ~ Bool, RefinedC opts p a) =>
a -> Either String a
evalBool5 @opts @op PP ip i
i of
            Left String
e -> String -> Get (Refined5 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Get (Refined5 opts ip op i))
-> String -> Get (Refined5 opts ip op i)
forall a b. (a -> b) -> a -> b
$ String
"Refined5(Binary:get):" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
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 String (PP ip i), Tree PE)
forall a. TT a -> (Either String 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 String Bool, Tree PE)
forall a. TT a -> (Either String 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 String
e,Tree PE
t2) -> (PP ip i -> Tree PE -> String -> Tree PE -> RResults2 (PP ip i)
forall a. a -> Tree PE -> String -> Tree PE -> RResults2 a
RTF PP ip i
a Tree PE
t1 String
e Tree PE
t2, Maybe (Refined5 opts ip op i)
forall a. Maybe a
Nothing)
   (Left String
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 (String -> Tree PE -> RResults2 (PP ip i)
forall a. String -> Tree PE -> RResults2 a
RF String
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 String 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 String Bool
lr,Tree PE
p2) = TT Bool -> (Either String Bool, Tree PE)
forall a. TT a -> (Either String a, Tree PE)
getValAndPE TT Bool
pp
      z :: String
z = let zz :: String
zz = Tree PE
p2 Tree PE -> Getting String (Tree PE) String -> String
forall s a. s -> Getting a s a -> a
^. (PE -> Const String PE) -> Tree PE -> Const String (Tree PE)
forall a. Lens' (Tree a) a
root ((PE -> Const String PE) -> Tree PE -> Const String (Tree PE))
-> ((String -> Const String String) -> PE -> Const String PE)
-> Getting String (Tree PE) String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Const String String) -> PE -> Const String PE
Lens' PE String
peString
          in if (Char -> Bool) -> String -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace String
zz then String
"FalseP" else String
"{" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
zz String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"}"
      w :: Either String a
w = case Either String Bool
lr of
            Right Bool
True -> a -> Either String a
forall a b. b -> Either a b
Right a
i
            Right Bool
False -> String -> Either String a
forall a b. a -> Either a b
Left (String -> Either String a) -> String -> Either String a
forall a b. (a -> b) -> a -> b
$ String -> ShowS
joinStrings String
"false boolean check" String
z
            Left String
e -> String -> Either String a
forall a b. a -> Either a b
Left (String -> Either String a) -> String -> Either String a
forall a b. (a -> b) -> a -> b
$ String -> ShowS
joinStrings String
"failed boolean check " String
e
  in ShowS -> Either String a -> Either String a
forall (a :: Type -> Type -> Type) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left (String -> ShowS
forall a. [a] -> [a] -> [a]
++ (String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ POpts -> Tree PE -> String
prtTreePure POpts
opts Tree PE
p2)) Either String a
w

-- | refinement exception

newtype Refined5Exception = Refined5Exception String
  deriving stock (forall x. Refined5Exception -> Rep Refined5Exception x)
-> (forall x. Rep Refined5Exception x -> Refined5Exception)
-> Generic Refined5Exception
forall x. Rep Refined5Exception x -> Refined5Exception
forall x. Refined5Exception -> Rep Refined5Exception x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Refined5Exception x -> Refined5Exception
$cfrom :: forall x. Refined5Exception -> Rep Refined5Exception x
Generic

instance Show Refined5Exception where
  show :: Refined5Exception -> String
show (Refined5Exception String
e) = String
"Refined5Exception:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
e

instance E.Exception Refined5Exception where
  displayException :: Refined5Exception -> String
displayException = Refined5Exception -> String
forall a. Show a => a -> String
show