-- 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 DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# 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'

 -- ** exception

  , Refined2Exception(..)

 ) 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)
import qualified Control.Exception as E
import GHC.Generics (Generic)
-- $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 (Refined2Exception -> Refined2 opts ip op i
forall a e. Exception e => e -> a
E.throw (Refined2Exception -> Refined2 opts ip op i)
-> (Msg2 -> Refined2Exception) -> Msg2 -> Refined2 opts ip op i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Refined2Exception
Refined2Exception (String -> Refined2Exception)
-> (Msg2 -> String) -> Msg2 -> Refined2Exception
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Msg2 -> String
forall a. Show a => a -> String
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 stock instance
  ( Refined2C opts ip op i
  , Show i
  , Show (PP ip i)
  ) => Show (Refined2 opts ip op i)

deriving stock instance
  ( Refined2C opts ip op i
  , Eq i
  , Eq (PP ip i)
  ) => Eq (Refined2 opts ip op i)

deriving stock instance
  ( Refined2C opts ip op i
  , Ord i
  , Ord (PP ip i)
  ) => Ord (Refined2 opts ip op i)

deriving stock 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 :: String -> Refined2 opts ip op i
fromString String
i =
    case String -> Either Msg2 (Refined2 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 (Refined2 opts ip op i)
newRefined2 String
i of
      Left Msg2
e -> Refined2Exception -> Refined2 opts ip op i
forall a e. Exception e => e -> a
E.throw (Refined2Exception -> Refined2 opts ip op i)
-> Refined2Exception -> Refined2 opts ip op i
forall a b. (a -> b) -> a -> b
$ String -> Refined2Exception
Refined2Exception  (String -> Refined2Exception) -> String -> Refined2Exception
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 Refined2 opts ip op String
r -> Refined2 opts ip op i
Refined2 opts ip op String
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 (String -> Lexeme
RL.Ident String
"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 String (PP op (PP ip i))
lr = 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
fld1

                 case Either String (PP op (PP ip i))
lr of
                   Left {} -> String -> ReadPrec (Refined2 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
""
                   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 -> String -> ReadPrec (Refined2 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
""
             )
           )
    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 -> String -> Parser (Refined2 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Parser (Refined2 opts ip op i))
-> String -> Parser (Refined2 opts ip op i)
forall a b. (a -> b) -> a -> b
$ String
"Refined2(FromJSON:parseJSON):" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg2 -> String
forall a. Show a => a -> String
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
      r :: Int
r = POpts -> Int
getMaxRecursionValue POpts
o
      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 | Int
cnt Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
r -> Refined2Exception -> Gen (Refined2 opts ip op i)
forall a e. Exception e => e -> a
E.throw (Refined2Exception -> Gen (Refined2 opts ip op i))
-> Refined2Exception -> Gen (Refined2 opts ip op i)
forall a b. (a -> b) -> a -> b
$ String -> Refined2Exception
Refined2Exception (String -> Refined2Exception) -> String -> Refined2Exception
forall a b. (a -> b) -> a -> b
$ POpts -> ShowS
setOtherEffects POpts
o ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"genRefined2P 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 (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 -> String -> Gen (Refined2 opts ip op i)
forall x. HasCallStack => String -> x
errorInProgram (String -> Gen (Refined2 opts ip op i))
-> String -> Gen (Refined2 opts ip op i)
forall a b. (a -> b) -> a -> b
$ String
"conversion failed:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg2 -> String
forall a. Show a => a -> String
show Msg2
e
               Right Refined2 opts ip op i
ret -> 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
ret
  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 -> String -> Get (Refined2 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Get (Refined2 opts ip op i))
-> String -> Get (Refined2 opts ip op i)
forall a b. (a -> b) -> a -> b
$ String
"Refined2(Binary:get):" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg2 -> String
forall a. Show a => a -> String
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 stock Int -> RResults2 a -> ShowS
[RResults2 a] -> ShowS
RResults2 a -> String
(Int -> RResults2 a -> ShowS)
-> (RResults2 a -> String)
-> ([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 -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RResults2 a] -> ShowS
$cshowList :: forall a. Show a => [RResults2 a] -> ShowS
show :: RResults2 a -> String
$cshow :: forall a. Show a => RResults2 a -> String
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 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 (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 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, 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 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 (Refined2 opts ip op i)
forall a. Maybe a
Nothing)
   (Left String
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 (String -> Tree PE -> RResults2 (PP ip i)
forall a. String -> Tree PE -> RResults2 a
RF String
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 -> String
m2Desc :: !String
                 , Msg2 -> String
m2Short :: !String
                 , Msg2 -> String
m2Long :: !String
                 , Msg2 -> ValP
m2ValP :: !ValP
                 } deriving stock 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 -> String
show (Msg2 String
a String
b String
c ValP
_d) = String -> ShowS
joinStrings String
a String
b String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String -> ShowS
nullIf String
"\n" String
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 String
msg = String
"*** " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> ShowS
formatOMsg POpts
opts String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
msg String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" ***\n"
      msg1 :: a -> String
msg1 a
a = ShowS
outmsg (String
"Step 1. Success Initial Conversion(ip) (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ POpts -> a -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")")
      mkMsg2 :: String -> String -> String -> ValP -> Msg2
mkMsg2 String
m String
n String
r ValP
bp | POpts -> Bool
hasNoTree POpts
opts = String -> String -> String -> ValP -> Msg2
Msg2 String
m String
n String
"" ValP
bp
                      | Bool
otherwise = String -> String -> String -> ValP -> Msg2
Msg2 String
m String
n String
r ValP
bp
  in case RResults2 a
v of
       RF String
e Tree PE
t1 ->
         let (String
m,String
n) = (String
"Step 1. " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Long -> POpts -> ValP -> String
colorValP Long
Short POpts
opts (String -> ValP
FailP String
e) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Initial Conversion(ip)", String
e)
             r :: String
r = ShowS
outmsg String
m
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> String
prtTreePure POpts
opts Tree PE
t1
         in String -> String -> String -> ValP -> Msg2
mkMsg2 String
m String
n String
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 String
e Tree PE
t2 ->
         let (String
m,String
n) = (String
"Step 2. " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Long -> POpts -> ValP -> String
colorValP Long
Short POpts
opts (String -> ValP
FailP String
e) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Boolean Check(op)", String
e)
             r :: String
r = a -> String
msg1 a
a
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> String
prtTreePure POpts
opts Tree PE
t1
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\n"
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ShowS
outmsg String
m
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> String
prtTreePure POpts
opts Tree PE
t2
         in String -> String -> String -> ValP -> Msg2
mkMsg2 String
m String
n String
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 (String
m,String
n) = (String
"Step 2. " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Long -> POpts -> ValP -> String
colorValP Long
Short POpts
opts ValP
FalseP String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Boolean Check(op)", String
z)
             z :: String
z = let w :: String
w = Tree PE
t2 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
w then String
"FalseP" else String
"{" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
w String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"}"
             r :: String
r = a -> String
msg1 a
a
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> String
prtTreePure POpts
opts Tree PE
t1
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\n"
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ShowS
outmsg String
m
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> String
prtTreePure POpts
opts Tree PE
t2
         in String -> String -> String -> ValP -> Msg2
mkMsg2 String
m String
n String
r ValP
FalseP
       RTTrue a
a Tree PE
t1 Tree PE
t2 ->
         let (String
m,String
n) = (String
"Step 2. True Boolean Check(op)", String
"")
             r :: String
r = a -> String
msg1 a
a
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> String
prtTreePure POpts
opts Tree PE
t1
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\n"
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ShowS
outmsg String
m
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> String
prtTreePure POpts
opts Tree PE
t2
         in String -> String -> String -> ValP -> Msg2
mkMsg2 String
m String
n String
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

-- | refinement exception

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

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

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