-- tojson binary hash arbitrary all use i not PP ip i

-- all instances work with the original input [ie not the internal values]

--   we have no way to get back to i from PP ip i (unlike Refined3)

{-# OPTIONS -Wno-redundant-constraints #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# 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 #-}
-- | a refinement type allowing the external type to differ from the internal type

module Predicate.Refined2 (

  -- ** Refined2

    Refined2
  , r2In
  , r2Out
  , Refined2C

 -- ** display results

  , Msg2 (..)
  , RResults2 (..)
  , prt2Impl

  -- ** evaluation methods

  , eval2P
  , eval2M
  , newRefined2
  , newRefined2'
  , newRefined2P
  , newRefined2P'

  -- ** proxy methods

  , MakeR2
  , mkProxy2
  , mkProxy2'

  -- ** QuickCheck methods

  , genRefined2
  , genRefined2P

  -- ** unsafe methods for creating Refined2

  , unsafeRefined2
  , unsafeRefined2'

 ) where
import Predicate.Core
import Predicate.Misc
import Predicate.Util
import Data.Tree (Tree)
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 Data.Maybe (isJust)
import Control.Lens
import Data.Tree.Lens (root)
import Data.Char (isSpace)
import Data.String (IsString(..))
import Data.Hashable (Hashable(..))
import GHC.Stack (HasCallStack)
import Test.QuickCheck
import Control.DeepSeq (rnf, rnf2, NFData)
-- $setup

-- >>> :set -XDataKinds

-- >>> :set -XTypeApplications

-- >>> :set -XTypeOperators

-- >>> :set -XOverloadedStrings

-- >>> :m + Predicate.Prelude

-- >>> :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 the internal type in 'r2In'

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

--   * @i@ is the input type which is stored in 'r2Out'

--

-- Although a common scenario is String as input, you are free to choose any input type you like

--

data Refined2 (opts :: Opt) ip op i = Refined2 !(PP ip i) !i

-- | field accessor for the converted input value in 'Refined2'

r2In :: Refined2 (opts :: Opt) ip op i -> PP ip i
r2In :: Refined2 opts ip op i -> PP ip i
r2In (Refined2 PP ip i
ppi i
_) = PP ip i
ppi

-- | field accessor for the original input value in 'Refined2'

r2Out :: Refined2 (opts :: Opt) ip op i -> i
r2Out :: Refined2 opts ip op i -> i
r2Out (Refined2 PP ip i
_ i
i) = i
i

type role Refined2 phantom nominal nominal nominal

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

unsafeRefined2' :: forall opts ip op i
                . ( Show (PP ip i)
                  , Refined2C opts ip op i
                  , HasCallStack
                  )
                => i
                -> Refined2 opts ip op i
unsafeRefined2' :: i -> Refined2 opts ip op i
unsafeRefined2' = (Msg2 -> Refined2 opts ip op i)
-> (Refined2 opts ip op i -> Refined2 opts ip op i)
-> Either Msg2 (Refined2 opts ip op i)
-> Refined2 opts ip op i
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ([Char] -> Refined2 opts ip op i
forall a. HasCallStack => [Char] -> a
error ([Char] -> Refined2 opts ip op i)
-> (Msg2 -> [Char]) -> Msg2 -> Refined2 opts ip op i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Msg2 -> [Char]
forall a. Show a => a -> [Char]
show) Refined2 opts ip op i -> Refined2 opts ip op i
forall a. a -> a
id (Either Msg2 (Refined2 opts ip op i) -> Refined2 opts ip op i)
-> (i -> Either Msg2 (Refined2 opts ip op i))
-> i
-> Refined2 opts ip op i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. i -> Either Msg2 (Refined2 opts ip op i)
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
(Refined2C opts ip op i, Show (PP ip i)) =>
i -> Either Msg2 (Refined2 opts ip op i)
newRefined2

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

unsafeRefined2 :: forall opts ip op i
   . Refined2C opts ip op i
   => PP ip i
  -> i
  -> Refined2 opts ip op i
unsafeRefined2 :: PP ip i -> i -> Refined2 opts ip op i
unsafeRefined2 = PP ip i -> i -> Refined2 opts ip op i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
PP ip i -> i -> Refined2 opts ip op i
Refined2

-- | Provides the constraints on Refined2

type Refined2C opts ip op i =
       ( OptC opts
       , P ip i
       , P op (PP ip i)
       , PP op (PP ip i) ~ Bool   -- the internal value needs to pass the predicate check

       )

deriving instance ( Refined2C opts ip op i
                  , Show i
                  , Show (PP ip i)
                  ) => Show (Refined2 opts ip op i)
deriving instance ( Refined2C opts ip op i
                  , Eq i
                  , Eq (PP ip i)
                  ) => Eq (Refined2 opts ip op i)
deriving instance ( Refined2C opts ip op i
                  , Ord i
                  , Ord (PP ip i)
                  ) => Ord (Refined2 opts ip op i)
deriving instance ( Refined2C opts ip op i
                  , TH.Lift (PP ip i)
                  , TH.Lift i
                  ) => TH.Lift (Refined2 opts ip op i)

instance ( Refined2C opts ip op i
         , NFData i
         , NFData (PP ip i)
         ) => NFData (Refined2 opts ip op i) where
  rnf :: Refined2 opts ip op i -> ()
rnf (Refined2 PP ip i
a i
b) = (PP ip i, i) -> ()
forall (p :: Type -> Type -> Type) a b.
(NFData2 p, NFData a, NFData b) =>
p a b -> ()
rnf2 (PP ip i
a,i
b)

-- | 'IsString' instance for Refined2

--

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

-- Right (Refined2 523 "523")

--

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

-- Left ()

--

instance ( i ~ String
         , Refined2C opts ip op i
         , Show (PP ip i)
         ) => IsString (Refined2 opts ip op i) where
  fromString :: [Char] -> Refined2 opts ip op i
fromString [Char]
i =
    case [Char] -> Either Msg2 (Refined2 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 (Refined2 opts ip op i)
newRefined2 [Char]
i of
      Left Msg2
e -> [Char] -> Refined2 opts ip op i
forall a. HasCallStack => [Char] -> a
error ([Char] -> Refined2 opts ip op i)
-> [Char] -> Refined2 opts ip op i
forall a b. (a -> b) -> a -> b
$ [Char]
"Refined2(IsString:fromString):" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg2 -> [Char]
forall a. Show a => a -> [Char]
show Msg2
e
      Right Refined2 opts ip op [Char]
r -> Refined2 opts ip op i
Refined2 opts ip op [Char]
r

-- read instance from -ddump-deriv

-- | 'Read' instance for 'Refined2'

--

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

-- [(Refined2 254 "fe","")]

--

-- >>> reads @(Refined2 OZ (ReadBase Int 16) (0 <..> 0xff) String) "Refined2 300 \"12c\""

-- []

--

-- >>> reads @(Refined2 OZ (ReadBase Int 16) (Id < 0) String) "Refined2 (-1234) \"-4d2\""

-- [(Refined2 (-1234) "-4d2","")]

--

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

-- [(Refined2 [192,168,0,1] "192.168.0.1","")]

--

instance ( Refined2C opts ip op i
         , Read (PP ip i)
         , Read i
         ) => Read (Refined2 opts ip op i) where
    readPrec :: ReadPrec (Refined2 opts ip op i)
readPrec
      = ReadPrec (Refined2 opts ip op i)
-> ReadPrec (Refined2 opts ip op i)
forall a. ReadPrec a -> ReadPrec a
GR.parens
          (Int
-> ReadPrec (Refined2 opts ip op i)
-> ReadPrec (Refined2 opts ip op i)
forall a. Int -> ReadPrec a -> ReadPrec a
PCR.prec
             Int
10
             (do Lexeme -> ReadPrec ()
GR.expectP ([Char] -> Lexeme
RL.Ident [Char]
"Refined2")
                 PP ip i
fld1 <- ReadPrec (PP ip i) -> ReadPrec (PP ip i)
forall a. ReadPrec a -> ReadPrec a
PCR.step ReadPrec (PP ip i)
forall a. Read a => ReadPrec a
GR.readPrec
                 i
fld2 <- ReadPrec i -> ReadPrec i
forall a. ReadPrec a -> ReadPrec a
PCR.step ReadPrec i
forall a. Read a => ReadPrec a
GR.readPrec
                 let lr :: Either [Char] (PP op (PP ip i))
lr = 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
fld1

                 case Either [Char] (PP op (PP ip i))
lr of
                   Left {} -> [Char] -> ReadPrec (Refined2 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
""
                   Right PP op (PP ip i)
True -> Refined2 opts ip op i -> ReadPrec (Refined2 opts ip op i)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PP ip i -> i -> Refined2 opts ip op i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
PP ip i -> i -> Refined2 opts ip op i
Refined2 PP ip i
fld1 i
fld2)
                   Right PP op (PP ip i)
False -> [Char] -> ReadPrec (Refined2 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
""
             )
           )
    readList :: ReadS [Refined2 opts ip op i]
readList = ReadS [Refined2 opts ip op i]
forall a. Read a => ReadS [a]
GR.readListDefault
    readListPrec :: ReadPrec [Refined2 opts ip op i]
readListPrec = ReadPrec [Refined2 opts ip op i]
forall a. Read a => ReadPrec [a]
GR.readListPrecDefault

-- | 'ToJSON' instance for 'Refined2'

--

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

-- >>> A.encode (unsafeRefined2 @OZ @(ReadBase Int 16) @(0 <..> 0xff) 254 "fe")

-- "\"fe\""

--

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

-- "123"

--

instance ( Refined2C opts ip op i
         , ToJSON i
         ) => ToJSON (Refined2 opts ip op i) where
  toJSON :: Refined2 opts ip op i -> Value
toJSON = i -> Value
forall a. ToJSON a => a -> Value
toJSON (i -> Value)
-> (Refined2 opts ip op i -> i) -> Refined2 opts ip op i -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined2 opts ip op i -> i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
Refined2 opts ip op i -> i
r2Out


-- | 'FromJSON' instance for 'Refined2'

--

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

-- >>> A.eitherDecode' @(Refined2 OZ (ReadBase Int 16) (Id > 10 && Id < 256) String) "\"00fe\""

-- Right (Refined2 254 "00fe")

--

-- >>> removeAnsi $ A.eitherDecode' @(Refined2 OAN (ReadBase Int 16) (Id > 10 && Id < 256) String) "\"00fe443a\""

-- Error in $: Refined2(FromJSON:parseJSON):Step 2. False Boolean Check(op) | {True && False | (16663610 < 256)}

-- *** Step 1. Success Initial Conversion(ip) (16663610) ***

-- P ReadBase(Int,16) 16663610

-- |

-- `- P Id "00fe443a"

-- *** Step 2. False Boolean Check(op) ***

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

-- |

-- +- True 16663610 > 10

-- |  |

-- |  +- P Id 16663610

-- |  |

-- |  `- P '10

-- |

-- `- False 16663610 < 256

--    |

--    +- P Id 16663610

--    |

--    `- P '256

--

instance ( Refined2C opts ip op i
         , Show (PP ip i)
         , FromJSON i
         ) => FromJSON (Refined2 opts ip op i) where
  parseJSON :: Value -> Parser (Refined2 opts ip op i)
parseJSON Value
z = do
                  i
i <- Value -> Parser i
forall a. FromJSON a => Value -> Parser a
parseJSON @i Value
z
                  case i -> Either Msg2 (Refined2 opts ip op i)
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
(Refined2C opts ip op i, Show (PP ip i)) =>
i -> Either Msg2 (Refined2 opts ip op i)
newRefined2 i
i of
                    Left Msg2
e -> [Char] -> Parser (Refined2 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> Parser (Refined2 opts ip op i))
-> [Char] -> Parser (Refined2 opts ip op i)
forall a b. (a -> b) -> a -> b
$ [Char]
"Refined2(FromJSON:parseJSON):" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg2 -> [Char]
forall a. Show a => a -> [Char]
show Msg2
e
                    Right Refined2 opts ip op i
r -> Refined2 opts ip op i -> Parser (Refined2 opts ip op i)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Refined2 opts ip op i
r

-- | 'Arbitrary' instance for 'Refined2'

--

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

-- >>> xs <- generate (vectorOf 10 (arbitrary @(Refined2 OAN (ToEnum Day) (L2 (ToWeekDate Id) == "Tuesday") Int)))

-- >>> all (\x -> let y = toEnum @Day (r2Out x) in view _3 (toWeekDate y) == 2 && r2In x == y) xs

-- True

--

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

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

--

-- >>> g = genRefined2 @OAN @(ToEnum Day) @(UnMkDay Id >> Snd == 10) arbitrary

-- >>> xs <- generate (vectorOf 10 g)

-- >>> all (\x -> let y = toEnum @Day (fromIntegral (r2Out x)) in view _2 (toGregorian y) == 10 && y == r2In x) xs

-- True

--

genRefined2 ::
    forall opts ip op i
  . ( Refined2C opts ip op i
    , HasCallStack
    , Show (PP ip i)
    )
  => Gen i
  -> Gen (Refined2 opts ip op i)
genRefined2 :: Gen i -> Gen (Refined2 opts ip op i)
genRefined2 = Proxy '(opts, ip, op, i) -> Gen i -> Gen (Refined2 opts ip op i)
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
(Refined2C opts ip op i, HasCallStack, Show (PP ip i)) =>
Proxy '(opts, ip, op, i) -> Gen i -> Gen (Refined2 opts ip op i)
genRefined2P 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 'Refined2' generator using a proxy

genRefined2P ::
    forall opts ip op i
  . ( Refined2C opts ip op i
    , HasCallStack
    , Show (PP ip i)
    )
  => Proxy '(opts,ip,op,i)
  -> Gen i
  -> Gen (Refined2 opts ip op i)
genRefined2P :: Proxy '(opts, ip, op, i) -> Gen i -> Gen (Refined2 opts ip op i)
genRefined2P Proxy '(opts, ip, op, i)
_ Gen i
g =
  let o :: POpts
o = OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts
      f :: Int -> Gen (Refined2 opts ip op i)
f !Int
cnt = do
        Maybe i
mi <- Gen i -> (i -> Bool) -> Gen (Maybe i)
forall a. Gen a -> (a -> Bool) -> Gen (Maybe a)
suchThatMaybe Gen i
g (Maybe (Refined2 opts ip op i) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Refined2 opts ip op i) -> Bool)
-> (i -> Maybe (Refined2 opts ip op i)) -> i -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
-> Maybe (Refined2 opts ip op i)
forall a b. (a, b) -> b
snd ((RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
 -> Maybe (Refined2 opts ip op i))
-> (i -> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i)))
-> i
-> Maybe (Refined2 opts ip op i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
-> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
forall a. Identity a -> a
runIdentity (Identity (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
 -> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i)))
-> (i
    -> Identity (RResults2 (PP ip i), Maybe (Refined2 opts ip op i)))
-> i
-> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (Refined2 opts ip op i))
forall i (m :: Type -> Type).
(MonadEval m, Refined2C opts ip op i) =>
i -> m (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
eval2M @opts @ip @op)
        case Maybe i
mi of
          Maybe i
Nothing ->
             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 (Refined2 opts ip op i)
forall a. HasCallStack => [Char] -> a
error ([Char] -> Gen (Refined2 opts ip op i))
-> [Char] -> Gen (Refined2 opts ip op i)
forall a b. (a -> b) -> a -> b
$ POpts -> ShowS
setOtherEffects POpts
o ([Char]
"genRefined2P 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 (Refined2 opts ip op i)
f (Int
cntInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
          Just i
i ->
             case i -> Either Msg2 (Refined2 opts ip op i)
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
(Refined2C opts ip op i, Show (PP ip i)) =>
i -> Either Msg2 (Refined2 opts ip op i)
newRefined2 i
i of
               Left Msg2
e -> [Char] -> Gen (Refined2 opts ip op i)
forall x. HasCallStack => [Char] -> x
errorInProgram ([Char] -> Gen (Refined2 opts ip op i))
-> [Char] -> Gen (Refined2 opts ip op i)
forall a b. (a -> b) -> a -> b
$ [Char]
"conversion failed:" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg2 -> [Char]
forall a. Show a => a -> [Char]
show Msg2
e
               Right Refined2 opts ip op i
r -> Refined2 opts ip op i -> Gen (Refined2 opts ip op i)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Refined2 opts ip op i
r
  in Int -> Gen (Refined2 opts ip op i)
f Int
0

-- | 'Binary' instance for 'Refined2'

--

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

-- >>> import Data.Time

-- >>> type K1 = Refined2 OAN (ReadP Day Id) 'True String

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

-- >>> r = unsafeRefined2' "2019-04-23" :: K1

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

-- Refined2 2019-04-23 "2019-04-23"

--

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

-- Refined2(Binary:get):Step 2. False Boolean Check(op) | {2019-05-30 <= 2019-04-23}

-- *** Step 1. Success Initial Conversion(ip) (2019-04-23) ***

-- P ReadP Day 2019-04-23

-- |

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

-- *** Step 2. False Boolean Check(op) ***

-- False 2019-05-30 <= 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 ( Refined2C opts ip op i
         , Show (PP ip i)
         , Binary i
         ) => Binary (Refined2 opts ip op i) where
  get :: Get (Refined2 opts ip op i)
get = do
          i
i <- Binary i => Get i
forall t. Binary t => Get t
B.get @i
          case i -> Either Msg2 (Refined2 opts ip op i)
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
(Refined2C opts ip op i, Show (PP ip i)) =>
i -> Either Msg2 (Refined2 opts ip op i)
newRefined2 i
i of
            Left Msg2
e -> [Char] -> Get (Refined2 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> Get (Refined2 opts ip op i))
-> [Char] -> Get (Refined2 opts ip op i)
forall a b. (a -> b) -> a -> b
$ [Char]
"Refined2(Binary:get):" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg2 -> [Char]
forall a. Show a => a -> [Char]
show Msg2
e
            Right Refined2 opts ip op i
r -> Refined2 opts ip op i -> Get (Refined2 opts ip op i)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Refined2 opts ip op i
r
  put :: Refined2 opts ip op i -> Put
put (Refined2 PP ip i
_ i
r) = i -> Put
forall t. Binary t => t -> Put
B.put @i i
r

-- | 'Hashable' instance for 'Refined2'

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

-- | An ADT that summarises the results of evaluating Refined2 representing all possible states

data RResults2 a =
       RF !String !(Tree PE)        -- fails initial conversion

     | RTF !a !(Tree PE) !String !(Tree PE)    -- op fails

     | RTFalse !a !(Tree PE) !(Tree PE)        -- op false

     | RTTrue !a !(Tree PE) !(Tree PE) -- op true

     deriving Int -> RResults2 a -> ShowS
[RResults2 a] -> ShowS
RResults2 a -> [Char]
(Int -> RResults2 a -> ShowS)
-> (RResults2 a -> [Char])
-> ([RResults2 a] -> ShowS)
-> Show (RResults2 a)
forall a. Show a => Int -> RResults2 a -> ShowS
forall a. Show a => [RResults2 a] -> ShowS
forall a. Show a => RResults2 a -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [RResults2 a] -> ShowS
$cshowList :: forall a. Show a => [RResults2 a] -> ShowS
show :: RResults2 a -> [Char]
$cshow :: forall a. Show a => RResults2 a -> [Char]
showsPrec :: Int -> RResults2 a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> RResults2 a -> ShowS
Show

-- | version for creating a 'Refined2' value that works for any 'MonadEval' instance

newRefined2' :: forall opts ip op i m
  . ( MonadEval m
    , Refined2C opts ip op i
    , Show (PP ip i)
    )
  => i
  -> m (Either Msg2 (Refined2 opts ip op i))
newRefined2' :: i -> m (Either Msg2 (Refined2 opts ip op i))
newRefined2' = Proxy '(opts, ip, op, i)
-> i -> m (Either Msg2 (Refined2 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 (Refined2 opts ip op i))
newRefined2P' Proxy '(opts, ip, op, i)
forall k (t :: k). Proxy t
Proxy

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

newRefined2P' :: 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 (Refined2 opts ip op i))
newRefined2P' :: proxy '(opts, ip, op, i)
-> i -> m (Either Msg2 (Refined2 opts ip op i))
newRefined2P' proxy '(opts, ip, op, i)
_ i
i = do
  (RResults2 (PP ip i)
ret,Maybe (Refined2 opts ip op i)
mr) <- i -> m (RResults2 (PP ip i), Maybe (Refined2 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 (Refined2 opts ip op i))
eval2M i
i
  Either Msg2 (Refined2 opts ip op i)
-> m (Either Msg2 (Refined2 opts ip op i))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Either Msg2 (Refined2 opts ip op i)
 -> m (Either Msg2 (Refined2 opts ip op i)))
-> Either Msg2 (Refined2 opts ip op i)
-> m (Either Msg2 (Refined2 opts ip op i))
forall a b. (a -> b) -> a -> b
$ Either Msg2 (Refined2 opts ip op i)
-> (Refined2 opts ip op i -> Either Msg2 (Refined2 opts ip op i))
-> Maybe (Refined2 opts ip op i)
-> Either Msg2 (Refined2 opts ip op i)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Msg2 -> Either Msg2 (Refined2 opts ip op i)
forall a b. a -> Either a b
Left (Msg2 -> Either Msg2 (Refined2 opts ip op i))
-> Msg2 -> Either Msg2 (Refined2 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) Refined2 opts ip op i -> Either Msg2 (Refined2 opts ip op i)
forall a b. b -> Either a b
Right Maybe (Refined2 opts ip op i)
mr

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

--

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

-- Right (Refined2 254 "00fe")

--

-- >>> newRefined2 @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

--

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

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

--

-- >>> newRefined2 @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}

--

-- >>> newRefined2 @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

--

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

-- Right (Refined2 [198,162,3,1] "198.162.3.1")

--

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

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

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

--

-- >>> newRefined2 @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}

--

-- >>> newRefined2 @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

--

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

-- Right (Refined2 22 22)

--

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

-- Right (Refined2 2020-05-04 12:13:14 UTC "2020-05-04 12:13:14Z")

--

-- >>> newRefined2 @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}

--

newRefined2 :: forall opts ip op i
  . ( Refined2C opts ip op i
    , Show (PP ip i)
  ) => i
    -> Either Msg2 (Refined2 opts ip op i)
newRefined2 :: i -> Either Msg2 (Refined2 opts ip op i)
newRefined2 = Proxy '(opts, ip, op, i)
-> i -> Either Msg2 (Refined2 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 (Refined2 opts ip op i)
newRefined2P Proxy '(opts, ip, op, i)
forall k (t :: k). Proxy t
Proxy

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

--

-- >>> type T4 k = '(OZ, MkDayExtra Id >> 'Just Id, GuardBool "expected a Sunday" (Thd == 7), k)

-- >>> newRefined2P (Proxy @(T4 _)) (2019,10,12)

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

--

-- >>> newRefined2P (Proxy @(T4 _)) (2019,10,13)

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

--

newRefined2P :: forall opts ip op i
  . ( Refined2C opts ip op i
    , Show (PP ip i)
  ) => Proxy '(opts,ip,op,i)
    -> i
    -> Either Msg2 (Refined2 opts ip op i)
newRefined2P :: Proxy '(opts, ip, op, i)
-> i -> Either Msg2 (Refined2 opts ip op i)
newRefined2P Proxy '(opts, ip, op, i)
_ i
i =
  let (RResults2 (PP ip i)
ret,Maybe (Refined2 opts ip op i)
mr) = Identity (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
-> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
forall a. Identity a -> a
runIdentity (Identity (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
 -> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i)))
-> Identity (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
-> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
forall a b. (a -> b) -> a -> b
$ i -> Identity (RResults2 (PP ip i), Maybe (Refined2 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 (Refined2 opts ip op i))
eval2M i
i
  in Either Msg2 (Refined2 opts ip op i)
-> (Refined2 opts ip op i -> Either Msg2 (Refined2 opts ip op i))
-> Maybe (Refined2 opts ip op i)
-> Either Msg2 (Refined2 opts ip op i)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Msg2 -> Either Msg2 (Refined2 opts ip op i)
forall a b. a -> Either a b
Left (Msg2 -> Either Msg2 (Refined2 opts ip op i))
-> Msg2 -> Either Msg2 (Refined2 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) Refined2 opts ip op i -> Either Msg2 (Refined2 opts ip op i)
forall a b. b -> Either a b
Right Maybe (Refined2 opts ip op i)
mr

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

eval2P :: 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 (Refined2 opts ip op i))
eval2P :: Proxy '(opts, ip, op, i)
-> i -> m (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
eval2P Proxy '(opts, ip, op, i)
_ = i -> m (RResults2 (PP ip i), Maybe (Refined2 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 (Refined2 opts ip op i))
eval2M

-- | workhorse for creating 'Refined2' values

eval2M :: forall opts ip op i m
  . ( MonadEval m
    , Refined2C opts ip op i
    )
  => i
  -> m (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
eval2M :: i -> m (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
eval2M 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 (Refined2 opts ip op i))
-> m (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
 -> m (RResults2 (PP ip i), Maybe (Refined2 opts ip op i)))
-> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
-> m (RResults2 (PP ip i), Maybe (Refined2 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, Refined2 opts ip op i -> Maybe (Refined2 opts ip op i)
forall a. a -> Maybe a
Just (PP ip i -> i -> Refined2 opts ip op i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
PP ip i -> i -> Refined2 opts ip op i
Refined2 PP ip i
a i
i))
      (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 (Refined2 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 (Refined2 opts ip op i)
forall a. Maybe a
Nothing)
   (Left [Char]
e,Tree PE
t1) -> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
-> m (RResults2 (PP ip i), Maybe (Refined2 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 (Refined2 opts ip op i)
forall a. Maybe a
Nothing)

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

data Msg2 = Msg2 { Msg2 -> [Char]
m2Desc :: !String
                 , Msg2 -> [Char]
m2Short :: !String
                 , Msg2 -> [Char]
m2Long :: !String
                 , Msg2 -> ValP
m2ValP :: !ValP
                 } deriving Msg2 -> Msg2 -> Bool
(Msg2 -> Msg2 -> Bool) -> (Msg2 -> Msg2 -> Bool) -> Eq Msg2
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Msg2 -> Msg2 -> Bool
$c/= :: Msg2 -> Msg2 -> Bool
== :: Msg2 -> Msg2 -> Bool
$c== :: Msg2 -> Msg2 -> Bool
Eq

instance Show Msg2 where
  show :: Msg2 -> [Char]
show (Msg2 [Char]
a [Char]
b [Char]
c ValP
_d) = [Char]
a [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char] -> ShowS
nullIf [Char]
" | " [Char]
b [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char] -> ShowS
nullIf [Char]
"\n" [Char]
c

-- | format the output from creating a 'Refined2' value into 'Msg2'

prt2Impl :: forall a . Show a
  => POpts
  -> RResults2 a
  -> Msg2
prt2Impl :: POpts -> RResults2 a -> Msg2
prt2Impl POpts
opts RResults2 a
v =
  let outmsg :: ShowS
outmsg [Char]
msg = [Char]
"*** " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> ShowS
formatOMsg POpts
opts [Char]
" " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
msg [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" ***\n"
      msg1 :: a -> [Char]
msg1 a
a = ShowS
outmsg ([Char]
"Step 1. Success Initial Conversion(ip) (" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ POpts -> a -> [Char]
forall a. Show a => POpts -> a -> [Char]
showL POpts
opts a
a [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")")
      mkMsg2 :: [Char] -> [Char] -> [Char] -> ValP -> Msg2
mkMsg2 [Char]
m [Char]
n [Char]
r ValP
bp | POpts -> Bool
hasNoTree POpts
opts = [Char] -> [Char] -> [Char] -> ValP -> Msg2
Msg2 [Char]
m [Char]
n [Char]
"" ValP
bp
                      | Bool
otherwise = [Char] -> [Char] -> [Char] -> ValP -> Msg2
Msg2 [Char]
m [Char]
n [Char]
r ValP
bp
  in case RResults2 a
v of
       RF [Char]
e Tree PE
t1 ->
         let ([Char]
m,[Char]
n) = ([Char]
"Step 1. " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Long -> POpts -> ValP -> [Char]
colorValP Long
Short POpts
opts ([Char] -> ValP
FailP [Char]
e) [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" Initial Conversion(ip)", [Char]
e)
             r :: [Char]
r = ShowS
outmsg [Char]
m
              [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> [Char]
prtTreePure POpts
opts Tree PE
t1
         in [Char] -> [Char] -> [Char] -> ValP -> Msg2
mkMsg2 [Char]
m [Char]
n [Char]
r (Tree PE
t1 Tree PE -> Getting ValP (Tree PE) ValP -> ValP
forall s a. s -> Getting a s a -> a
^. (PE -> Const ValP PE) -> Tree PE -> Const ValP (Tree PE)
forall a. Lens' (Tree a) a
root ((PE -> Const ValP PE) -> Tree PE -> Const ValP (Tree PE))
-> ((ValP -> Const ValP ValP) -> PE -> Const ValP PE)
-> Getting ValP (Tree PE) ValP
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ValP -> Const ValP ValP) -> PE -> Const ValP PE
Lens' PE ValP
peValP)
       RTF a
a Tree PE
t1 [Char]
e Tree PE
t2 ->
         let ([Char]
m,[Char]
n) = ([Char]
"Step 2. " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Long -> POpts -> ValP -> [Char]
colorValP Long
Short POpts
opts ([Char] -> ValP
FailP [Char]
e) [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" Boolean Check(op)", [Char]
e)
             r :: [Char]
r = a -> [Char]
msg1 a
a
              [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> [Char]
prtTreePure POpts
opts Tree PE
t1
              [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"\n"
              [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> ShowS
outmsg [Char]
m
              [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> [Char]
prtTreePure POpts
opts Tree PE
t2
         in [Char] -> [Char] -> [Char] -> ValP -> Msg2
mkMsg2 [Char]
m [Char]
n [Char]
r (Tree PE
t2 Tree PE -> Getting ValP (Tree PE) ValP -> ValP
forall s a. s -> Getting a s a -> a
^. (PE -> Const ValP PE) -> Tree PE -> Const ValP (Tree PE)
forall a. Lens' (Tree a) a
root ((PE -> Const ValP PE) -> Tree PE -> Const ValP (Tree PE))
-> ((ValP -> Const ValP ValP) -> PE -> Const ValP PE)
-> Getting ValP (Tree PE) ValP
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ValP -> Const ValP ValP) -> PE -> Const ValP PE
Lens' PE ValP
peValP)
       RTFalse a
a Tree PE
t1 Tree PE
t2 ->
         let ([Char]
m,[Char]
n) = ([Char]
"Step 2. " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Long -> POpts -> ValP -> [Char]
colorValP Long
Short POpts
opts ValP
FalseP [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" Boolean Check(op)", [Char]
z)
             z :: [Char]
z = let w :: [Char]
w = Tree PE
t2 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]
w then [Char]
"FalseP" else [Char]
"{" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
w [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"}"
             r :: [Char]
r = a -> [Char]
msg1 a
a
              [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> [Char]
prtTreePure POpts
opts Tree PE
t1
              [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"\n"
              [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> ShowS
outmsg [Char]
m
              [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> [Char]
prtTreePure POpts
opts Tree PE
t2
         in [Char] -> [Char] -> [Char] -> ValP -> Msg2
mkMsg2 [Char]
m [Char]
n [Char]
r ValP
FalseP
       RTTrue a
a Tree PE
t1 Tree PE
t2 ->
         let ([Char]
m,[Char]
n) = ([Char]
"Step 2. True Boolean Check(op)", [Char]
"")
             r :: [Char]
r = a -> [Char]
msg1 a
a
              [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> [Char]
prtTreePure POpts
opts Tree PE
t1
              [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"\n"
              [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> ShowS
outmsg [Char]
m
              [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> [Char]
prtTreePure POpts
opts Tree PE
t2
         in [Char] -> [Char] -> [Char] -> ValP -> Msg2
mkMsg2 [Char]
m [Char]
n [Char]
r (Tree PE
t2 Tree PE -> Getting ValP (Tree PE) ValP -> ValP
forall s a. s -> Getting a s a -> a
^. (PE -> Const ValP PE) -> Tree PE -> Const ValP (Tree PE)
forall a. Lens' (Tree a) a
root ((PE -> Const ValP PE) -> Tree PE -> Const ValP (Tree PE))
-> ((ValP -> Const ValP ValP) -> PE -> Const ValP PE)
-> Getting ValP (Tree PE) ValP
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ValP -> Const ValP ValP) -> PE -> Const ValP PE
Lens' PE ValP
peValP)

-- | creates a 4-tuple proxy (see 'eval2P' 'newRefined2P')

--

-- 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)

-- >>> newRefined2P eg1 "24"

-- Right (Refined2 24 "24")

--

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

--

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

-- >>> newRefined2P eg2 "24"

-- Right (Refined2 24 "24")

--

mkProxy2 :: forall z opts ip op i
  . z ~ '(opts,ip,op,i)
    => Proxy '(opts,ip,op,i)
mkProxy2 :: Proxy '(opts, ip, op, i)
mkProxy2 = Proxy '(opts, ip, op, i)
forall k (t :: k). Proxy t
Proxy

-- | same as 'mkProxy2' but checks to make sure the proxy is consistent with the 'Refined2C' constraint

mkProxy2' :: forall z opts ip op i
  . ( z ~ '(ip,op,i)
    , Refined2C opts ip op i
    ) => Proxy '(opts,ip,op,i)
mkProxy2' :: Proxy '(opts, ip, op, i)
mkProxy2' = Proxy '(opts, ip, op, i)
forall k (t :: k). Proxy t
Proxy

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

type family MakeR2 p where
  MakeR2 '(opts,ip,op,i) = Refined2 opts ip op i