-- arbitrary and hash use the internal value!

-- binary and json use the external value

{-# 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 #-}
-- |

-- Refinement type allowing the external type to differ from the internal type

--

-- @

-- like 'Predicate.Refined2.Refined2' but also supports a canonical output value using the \'fmt\' parameter

-- @

--

module Predicate.Refined3 (

  -- ** Refined3

    Refined3
  , r3In
  , r3Out
  , Refined3C

 -- ** display results

  , Msg3 (..)
  , RResults3 (..)

  -- ** evaluation methods

  , eval3P
  , eval3M
  , newRefined3
  , newRefined3'
  , newRefined3P
  , newRefined3P'

  -- ** proxy methods

  , mkProxy3
  , mkProxy3'
  , MakeR3

  -- ** unsafe methods for creating Refined3

  , unsafeRefined3
  , unsafeRefined3'

  -- ** QuickCheck methods

  , genRefined3
  , genRefined3P

 -- ** exception

  , Refined3Exception(..)

 ) where
import Predicate.Core
import Predicate.Misc
import Predicate.Util
import Data.Functor.Identity (Identity(..))
import Data.Tree (Tree(..))
import Data.Proxy (Proxy(..))
import Data.Aeson (ToJSON(..), FromJSON(..))
import qualified Language.Haskell.TH.Syntax as TH
import Test.QuickCheck
import qualified GHC.Read as GR
import qualified Text.ParserCombinators.ReadPrec as PCR
import qualified Text.Read.Lex as RL
import qualified Data.Binary as B
import Data.Binary (Binary)
import Control.Lens ((^.))
import Data.Tree.Lens (root)
import Data.Char (isSpace)
import Data.String (IsString(..))
import Data.Hashable (Hashable(..))
import GHC.Stack (HasCallStack)
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

-- >>> :m + Data.Time


-- | Like 'Predicate.Refined2' but additionally reconstructs the output value to a standardized format

--

--   * @opts@ are the display options

--   * @ip@ converts @i@ to @PP ip i@ which is the internal type and stored in 'r3In'

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

--   * @fmt@ outputs the internal type @PP fmt (PP ip i) ~ i@ and stored in 'r3Out'

--   * @i@ is the input type

--

--   * @PP fmt (PP ip i)@ should be valid as input for Refined3

--

-- Setting @ip@ to @Id@ and @fmt@ to @Id@ is equivalent to 'Refined.Refined'

--

-- Setting the input type @i@ to 'GHC.Base.String' resembles the corresponding Read/Show instances but with an additional predicate on the read value

--

--   * __read__ a string using /ip/ into an internal type and store in 'r3In'

--   * __validate__ 'r3In' using the predicate /op/

--   * __show__ 'r3In' using /fmt/ and store that formatted result in 'r3Out'

--

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

--

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

type role Refined3 phantom nominal nominal nominal nominal

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

r3In :: Refined3 opts ip op fmt i -> PP ip i
r3In :: Refined3 opts ip op fmt i -> PP ip i
r3In (Refined3 PP ip i
ppi i
_) = PP ip i
ppi

-- | field accessor for the converted output value in 'Refined3'

r3Out :: Refined3 opts ip op fmt i -> i
r3Out :: Refined3 opts ip op fmt i -> i
r3Out (Refined3 PP ip i
_ i
i) = i
i


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

unsafeRefined3' :: forall opts ip op fmt i
                . ( HasCallStack
                  , Show (PP ip i)
                  , Refined3C opts ip op fmt i
                ) => i
                  -> Refined3 opts ip op fmt i
unsafeRefined3' :: i -> Refined3 opts ip op fmt i
unsafeRefined3' = (Msg3 -> Refined3 opts ip op fmt i)
-> (Refined3 opts ip op fmt i -> Refined3 opts ip op fmt i)
-> Either Msg3 (Refined3 opts ip op fmt i)
-> Refined3 opts ip op fmt i
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Refined3Exception -> Refined3 opts ip op fmt i
forall a e. Exception e => e -> a
E.throw (Refined3Exception -> Refined3 opts ip op fmt i)
-> (Msg3 -> Refined3Exception) -> Msg3 -> Refined3 opts ip op fmt i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Refined3Exception
Refined3Exception (String -> Refined3Exception)
-> (Msg3 -> String) -> Msg3 -> Refined3Exception
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Msg3 -> String
forall a. Show a => a -> String
show) Refined3 opts ip op fmt i -> Refined3 opts ip op fmt i
forall a. a -> a
id (Either Msg3 (Refined3 opts ip op fmt i)
 -> Refined3 opts ip op fmt i)
-> (i -> Either Msg3 (Refined3 opts ip op fmt i))
-> i
-> Refined3 opts ip op fmt i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. i -> Either Msg3 (Refined3 opts ip op fmt i)
forall k k k (opts :: Opt) (ip :: k) (op :: k) (fmt :: k) i.
(Refined3C opts ip op fmt i, Show (PP ip i)) =>
i -> Either Msg3 (Refined3 opts ip op fmt i)
newRefined3

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

unsafeRefined3 ::
    forall opts ip op fmt i
  .  Refined3C opts ip op fmt i
  => PP ip i
  -> i
  -> Refined3 opts ip op fmt i
unsafeRefined3 :: PP ip i -> i -> Refined3 opts ip op fmt i
unsafeRefined3 = PP ip i -> i -> Refined3 opts ip op fmt i
forall k k k (opts :: Opt) (ip :: k) (op :: k) (fmt :: k) i.
PP ip i -> i -> Refined3 opts ip op fmt i
Refined3


-- | Provides the constraints on Refined3

type Refined3C opts ip op fmt 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

       , P fmt (PP ip i)
       , PP fmt (PP ip i) ~ i  -- the output type must match the original input type

       )

deriving stock instance
  ( Refined3C opts ip op fmt i
  , Show (PP ip i)
  , Show i
  ) => Show (Refined3 opts ip op fmt i)

deriving stock instance
  ( Refined3C opts ip op fmt i
  , Eq (PP ip i)
  , Eq i
  ) => Eq (Refined3 opts ip op fmt i)

deriving stock instance
  ( Refined3C opts ip op fmt i
  , Ord (PP ip i)
  , Ord i
  ) => Ord (Refined3 opts ip op fmt i)

deriving stock instance
  ( Refined3C opts ip op fmt i
  , TH.Lift (PP ip i)
  , TH.Lift i
  ) => TH.Lift (Refined3 opts ip op fmt i)

instance ( Refined3C opts ip op fmt i
         , NFData i
         , NFData (PP ip i)
         ) => NFData (Refined3 opts ip op fmt i) where
  rnf :: Refined3 opts ip op fmt i -> ()
rnf (Refined3 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 Refined3

--

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

-- Right (Refined3 523 "523")

--

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

-- Left ()

--

instance ( Refined3C opts ip op fmt String
         , Show (PP ip String)
         ) => IsString (Refined3 opts ip op fmt String) where
  fromString :: String -> Refined3 opts ip op fmt String
fromString String
s =
    case String -> Either Msg3 (Refined3 opts ip op fmt String)
forall k k k (opts :: Opt) (ip :: k) (op :: k) (fmt :: k) i.
(Refined3C opts ip op fmt i, Show (PP ip i)) =>
i -> Either Msg3 (Refined3 opts ip op fmt i)
newRefined3 String
s of
      Left Msg3
e -> Refined3Exception -> Refined3 opts ip op fmt String
forall a e. Exception e => e -> a
E.throw (Refined3Exception -> Refined3 opts ip op fmt String)
-> Refined3Exception -> Refined3 opts ip op fmt String
forall a b. (a -> b) -> a -> b
$ String -> Refined3Exception
Refined3Exception (String -> Refined3Exception) -> String -> Refined3Exception
forall a b. (a -> b) -> a -> b
$ String
"IsString:fromString:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg3 -> String
forall a. Show a => a -> String
show Msg3
e
      Right Refined3 opts ip op fmt String
r -> Refined3 opts ip op fmt String
r

-- read instance from -ddump-deriv

-- | 'Read' instance for 'Refined3'

--

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

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

--

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

-- []

--

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

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

--

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

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

--

instance ( Eq i
         , Refined3C opts ip op fmt i
         , Read (PP ip i)
         , Read i
         ) => Read (Refined3 opts ip op fmt i) where
    readPrec :: ReadPrec (Refined3 opts ip op fmt i)
readPrec
      = ReadPrec (Refined3 opts ip op fmt i)
-> ReadPrec (Refined3 opts ip op fmt i)
forall a. ReadPrec a -> ReadPrec a
GR.parens
          (Int
-> ReadPrec (Refined3 opts ip op fmt i)
-> ReadPrec (Refined3 opts ip op fmt i)
forall a. Int -> ReadPrec a -> ReadPrec a
PCR.prec
             Int
10
             (do Lexeme -> ReadPrec ()
GR.expectP (String -> Lexeme
RL.Ident String
"Refined3")
                 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 (RResults3 (PP ip i)
_ret,Maybe (Refined3 opts ip op fmt i)
mr) = Identity (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
-> (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
forall a. Identity a -> a
runIdentity (Identity (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
 -> (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i)))
-> Identity
     (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
-> (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
forall a b. (a -> b) -> a -> b
$ PP ip i
-> Identity
     (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
forall k k k (opts :: Opt) (ip :: k) (op :: k) (fmt :: k) i
       (m :: Type -> Type).
(MonadEval m, Refined3C opts ip op fmt i) =>
PP ip i
-> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
eval3MSkip @opts @ip @op @fmt PP ip i
fld1
                 case Maybe (Refined3 opts ip op fmt i)
mr of
                   Maybe (Refined3 opts ip op fmt i)
Nothing -> String -> ReadPrec (Refined3 opts ip op fmt i)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
""
                   Just (Refined3 PP ip i
_r1 i
r2)
                     | i
r2 i -> i -> Bool
forall a. Eq a => a -> a -> Bool
== i
fld2 -> Refined3 opts ip op fmt i -> ReadPrec (Refined3 opts ip op fmt i)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PP ip i -> i -> Refined3 opts ip op fmt i
forall k k k (opts :: Opt) (ip :: k) (op :: k) (fmt :: k) i.
PP ip i -> i -> Refined3 opts ip op fmt i
Refined3 PP ip i
fld1 i
fld2)
                     | Bool
otherwise -> String -> ReadPrec (Refined3 opts ip op fmt i)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"" -- cant display a decent failure message

             )
           )
    readList :: ReadS [Refined3 opts ip op fmt i]
readList = ReadS [Refined3 opts ip op fmt i]
forall a. Read a => ReadS [a]
GR.readListDefault
    readListPrec :: ReadPrec [Refined3 opts ip op fmt i]
readListPrec = ReadPrec [Refined3 opts ip op fmt i]
forall a. Read a => ReadPrec [a]
GR.readListPrecDefault

-- | 'ToJSON' instance for 'Refined3'

--

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

-- >>> A.encode (unsafeRefined3' @OZ @(ReadBase Int 16) @(0 <..> 0xff) @(ShowBase 16) "fe")

-- "\"fe\""

--

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

-- "123"

--

instance ( Refined3C opts ip op fmt i
         , ToJSON i
         ) => ToJSON (Refined3 opts ip op fmt i) where
  toJSON :: Refined3 opts ip op fmt i -> Value
toJSON = i -> Value
forall a. ToJSON a => a -> Value
toJSON (i -> Value)
-> (Refined3 opts ip op fmt i -> i)
-> Refined3 opts ip op fmt i
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined3 opts ip op fmt i -> i
forall k k k (opts :: Opt) (ip :: k) (op :: k) (fmt :: k) i.
Refined3 opts ip op fmt i -> i
r3Out


-- | 'FromJSON' instance for 'Refined3'

--

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

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

-- Right (Refined3 254 "fe")

--

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

-- Error in $: Refined3(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 ( Refined3C opts ip op fmt i
         , Show (PP ip i)
         , FromJSON i
         ) => FromJSON (Refined3 opts ip op fmt i) where
  parseJSON :: Value -> Parser (Refined3 opts ip op fmt i)
parseJSON Value
z = do
                  i
i <- Value -> Parser i
forall a. FromJSON a => Value -> Parser a
parseJSON @i Value
z
                  case i -> Either Msg3 (Refined3 opts ip op fmt i)
forall k k k (opts :: Opt) (ip :: k) (op :: k) (fmt :: k) i.
(Refined3C opts ip op fmt i, Show (PP ip i)) =>
i -> Either Msg3 (Refined3 opts ip op fmt i)
newRefined3 i
i of
                    Left Msg3
e -> String -> Parser (Refined3 opts ip op fmt i)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Parser (Refined3 opts ip op fmt i))
-> String -> Parser (Refined3 opts ip op fmt i)
forall a b. (a -> b) -> a -> b
$ String
"Refined3(FromJSON:parseJSON):" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg3 -> String
forall a. Show a => a -> String
show Msg3
e
                    Right Refined3 opts ip op fmt i
r -> Refined3 opts ip op fmt i -> Parser (Refined3 opts ip op fmt i)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Refined3 opts ip op fmt i
r

-- | 'Arbitrary' instance for 'Refined3'

--

-- >>> xs <- generate (vectorOf 10 (arbitrary @(Refined3 OAN (ReadP Int Id) (1 <..> 120 && Even) (ShowP Id) String)))

-- >>> all (\x -> let y = r3In x in y /= 0 && r3Out x == show y) xs

-- True

--

instance ( Arbitrary (PP ip i)
         , Refined3C opts ip op fmt i
         ) => Arbitrary (Refined3 opts ip op fmt i) where
  arbitrary :: Gen (Refined3 opts ip op fmt i)
arbitrary = Gen (PP ip i) -> Gen (Refined3 opts ip op fmt i)
forall k k k (opts :: Opt) (ip :: k) (op :: k) (fmt :: k) i.
(Refined3C opts ip op fmt i, HasCallStack) =>
Gen (PP ip i) -> Gen (Refined3 opts ip op fmt i)
genRefined3 Gen (PP ip i)
forall a. Arbitrary a => Gen a
arbitrary

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

--

-- >>> g = genRefined3 @OAN @(ReadP Int Id) @(Between 10 100 Id && Even) @(ShowP Id) (choose (10,100))

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

-- >>> all (\x -> let y = r3In x in y >= 0 && y <= 100 && even y) xs

-- True

--

genRefined3 ::
    forall opts ip op fmt i
  . ( Refined3C opts ip op fmt i
    , HasCallStack
    )
  => Gen (PP ip i)
  -> Gen (Refined3 opts ip op fmt i)
genRefined3 :: Gen (PP ip i) -> Gen (Refined3 opts ip op fmt i)
genRefined3 = Proxy '(opts, ip, op, fmt, i)
-> Gen (PP ip i) -> Gen (Refined3 opts ip op fmt i)
forall k k k (opts :: Opt) (ip :: k) (op :: k) (fmt :: k) i.
(Refined3C opts ip op fmt i, HasCallStack) =>
Proxy '(opts, ip, op, fmt, i)
-> Gen (PP ip i) -> Gen (Refined3 opts ip op fmt i)
genRefined3P Proxy '(opts, ip, op, fmt, i)
forall k (t :: k). Proxy t
Proxy

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

genRefined3P ::
    forall opts ip op fmt i
  . ( Refined3C opts ip op fmt i
    , HasCallStack
    )
  => Proxy '(opts,ip,op,fmt,i)
  -> Gen (PP ip i)
  -> Gen (Refined3 opts ip op fmt i)
genRefined3P :: Proxy '(opts, ip, op, fmt, i)
-> Gen (PP ip i) -> Gen (Refined3 opts ip op fmt i)
genRefined3P Proxy '(opts, ip, op, fmt, 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 (Refined3 opts ip op fmt i)
f !Int
cnt = do
        Maybe (PP ip i)
mppi <- 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 ((PP ip i -> Bool) -> Gen (Maybe (PP ip i)))
-> (PP ip i -> Bool) -> Gen (Maybe (PP ip i))
forall a b. (a -> b) -> a -> b
$ \PP ip i
a -> 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
a Either String Bool -> Either String Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Either String Bool
forall a b. b -> Either a b
Right Bool
True
        case Maybe (PP ip i)
mppi of
          Maybe (PP ip i)
Nothing | Int
cnt Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
r -> Refined3Exception -> Gen (Refined3 opts ip op fmt i)
forall a e. Exception e => e -> a
E.throw (Refined3Exception -> Gen (Refined3 opts ip op fmt i))
-> Refined3Exception -> Gen (Refined3 opts ip op fmt i)
forall a b. (a -> b) -> a -> b
$ String -> Refined3Exception
Refined3Exception (String -> Refined3Exception) -> String -> Refined3Exception
forall a b. (a -> b) -> a -> b
$ POpts -> ShowS
setOtherEffects POpts
o (String
"genRefined3P 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 (Refined3 opts ip op fmt i)
f (Int
cntInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
          Just PP ip i
ppi ->
             case PP ip i -> Either String (PP fmt (PP ip i))
forall k (opts :: Opt) (p :: k) i.
(OptC opts, P p i) =>
i -> Either String (PP p i)
evalQuick @opts @fmt PP ip i
ppi of
               Left String
e -> Refined3Exception -> Gen (Refined3 opts ip op fmt i)
forall a e. Exception e => e -> a
E.throw (Refined3Exception -> Gen (Refined3 opts ip op fmt i))
-> Refined3Exception -> Gen (Refined3 opts ip op fmt i)
forall a b. (a -> b) -> a -> b
$ String -> Refined3Exception
Refined3Exception (String -> Refined3Exception) -> String -> Refined3Exception
forall a b. (a -> b) -> a -> b
$ String
"genRefined3P: formatting failed!! " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
e
               Right PP fmt (PP ip i)
ret -> Refined3 opts ip op fmt i -> Gen (Refined3 opts ip op fmt i)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Refined3 opts ip op fmt i -> Gen (Refined3 opts ip op fmt i))
-> Refined3 opts ip op fmt i -> Gen (Refined3 opts ip op fmt i)
forall a b. (a -> b) -> a -> b
$ PP ip i -> i -> Refined3 opts ip op fmt i
forall k k k (opts :: Opt) (ip :: k) (op :: k) (fmt :: k) i.
Refined3C opts ip op fmt i =>
PP ip i -> i -> Refined3 opts ip op fmt i
unsafeRefined3 PP ip i
ppi i
PP fmt (PP ip i)
ret
  in Int -> Gen (Refined3 opts ip op fmt i)
f Int
0

-- | 'Binary' instance for 'Refined3'

--

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

-- >>> import Control.Lens

-- >>> import Data.Time

-- >>> type K1 = MakeR3 '(OAN, ReadP Day Id, 'True, ShowP Id, String)

-- >>> type K2 = MakeR3 '(OAN, ReadP Day Id, Between (ReadP Day "2019-05-30") (ReadP Day "2019-06-01") Id, ShowP Id, String)

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

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

-- Refined3 2019-04-23 "2019-04-23"

--

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

-- Refined3(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 ( Refined3C opts ip op fmt i
         , Show (PP ip i)
         , Binary i
         ) => Binary (Refined3 opts ip op fmt i) where
  get :: Get (Refined3 opts ip op fmt i)
get = do
          i
i <- Binary i => Get i
forall t. Binary t => Get t
B.get @i
          case i -> Either Msg3 (Refined3 opts ip op fmt i)
forall k k k (opts :: Opt) (ip :: k) (op :: k) (fmt :: k) i.
(Refined3C opts ip op fmt i, Show (PP ip i)) =>
i -> Either Msg3 (Refined3 opts ip op fmt i)
newRefined3 i
i of
            Left Msg3
e -> String -> Get (Refined3 opts ip op fmt i)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Get (Refined3 opts ip op fmt i))
-> String -> Get (Refined3 opts ip op fmt i)
forall a b. (a -> b) -> a -> b
$ String
"Refined3(Binary:get):" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg3 -> String
forall a. Show a => a -> String
show Msg3
e
            Right Refined3 opts ip op fmt i
r -> Refined3 opts ip op fmt i -> Get (Refined3 opts ip op fmt i)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Refined3 opts ip op fmt i
r
  put :: Refined3 opts ip op fmt i -> Put
put (Refined3 PP ip i
_ i
r) = i -> Put
forall t. Binary t => t -> Put
B.put @i i
r

-- | 'Hashable' instance for 'Refined3'

instance ( Refined3C opts ip op fmt i
         , Hashable (PP ip i)
         ) => Hashable (Refined3 opts ip op fmt i) where
  hashWithSalt :: Int -> Refined3 opts ip op fmt i -> Int
hashWithSalt Int
s (Refined3 PP ip i
a i
_) = 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
a

-- | creates a 5-tuple proxy (see 'eval3P' 'newRefined3P')

--

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

--

-- set the 5-tuple directly

--

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

-- >>> newRefined3P eg1 "24"

-- Right (Refined3 24 "24")

--

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

--

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

-- >>> newRefined3P eg2 "24"

-- Right (Refined3 24 "24")

--

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

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

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

-- | type family for converting from a 5-tuple '(opts,ip,op,fmt,i) to a 'Refined3' type

type family MakeR3 p where
  MakeR3 '(opts,ip,op,fmt,i) = Refined3 opts ip op fmt i

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

data RResults3 a =
       RF !String !(Tree PE)        -- Left e

     | RTF !a !(Tree PE) !String !(Tree PE)    -- Right a + Left e

     | RTFalse !a !(Tree PE) !(Tree PE)        -- Right a + Right False

     | RTTrueF !a !(Tree PE) !(Tree PE) !String !(Tree PE) -- Right a + Right True + Left e

     | RTTrueT !a !(Tree PE) !(Tree PE) !(Tree PE)      -- Right a + Right True + Right b

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

-- | same as 'newRefined3P'' but passes in the proxy

newRefined3' :: forall opts ip op fmt i m
  . ( MonadEval m
    , Refined3C opts ip op fmt i
    , Show (PP ip i)
    )
  => i
  -> m (Either Msg3 (Refined3 opts ip op fmt i))
newRefined3' :: i -> m (Either Msg3 (Refined3 opts ip op fmt i))
newRefined3' = Proxy '(opts, ip, op, fmt, i)
-> i -> m (Either Msg3 (Refined3 opts ip op fmt i))
forall k k k (opts :: Opt) (ip :: k) (op :: k) (fmt :: k) i
       (proxy :: (Opt, k, k, k, Type) -> Type) (m :: Type -> Type).
(MonadEval m, Refined3C opts ip op fmt i, Show (PP ip i)) =>
proxy '(opts, ip, op, fmt, i)
-> i -> m (Either Msg3 (Refined3 opts ip op fmt i))
newRefined3P' Proxy '(opts, ip, op, fmt, i)
forall k (t :: k). Proxy t
Proxy

-- | same as 'newRefined3P' but runs in any MonadEval instance

newRefined3P' :: forall opts ip op fmt i proxy m
  . ( MonadEval m
    , Refined3C opts ip op fmt i
    , Show (PP ip i)
    )
  => proxy '(opts,ip,op,fmt,i)
  -> i
  -> m (Either Msg3 (Refined3 opts ip op fmt i))
newRefined3P' :: proxy '(opts, ip, op, fmt, i)
-> i -> m (Either Msg3 (Refined3 opts ip op fmt i))
newRefined3P' proxy '(opts, ip, op, fmt, i)
_ i
i = do
  (RResults3 (PP ip i)
ret,Maybe (Refined3 opts ip op fmt i)
mr) <- i -> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
forall k k k (opts :: Opt) (ip :: k) (op :: k) (fmt :: k) i
       (m :: Type -> Type).
(MonadEval m, Refined3C opts ip op fmt i) =>
i -> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
eval3M i
i
  Either Msg3 (Refined3 opts ip op fmt i)
-> m (Either Msg3 (Refined3 opts ip op fmt i))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Either Msg3 (Refined3 opts ip op fmt i)
 -> m (Either Msg3 (Refined3 opts ip op fmt i)))
-> Either Msg3 (Refined3 opts ip op fmt i)
-> m (Either Msg3 (Refined3 opts ip op fmt i))
forall a b. (a -> b) -> a -> b
$ Either Msg3 (Refined3 opts ip op fmt i)
-> (Refined3 opts ip op fmt i
    -> Either Msg3 (Refined3 opts ip op fmt i))
-> Maybe (Refined3 opts ip op fmt i)
-> Either Msg3 (Refined3 opts ip op fmt i)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Msg3 -> Either Msg3 (Refined3 opts ip op fmt i)
forall a b. a -> Either a b
Left (Msg3 -> Either Msg3 (Refined3 opts ip op fmt i))
-> Msg3 -> Either Msg3 (Refined3 opts ip op fmt i)
forall a b. (a -> b) -> a -> b
$ POpts -> RResults3 (PP ip i) -> Msg3
forall a. Show a => POpts -> RResults3 a -> Msg3
prt3Impl (OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts) RResults3 (PP ip i)
ret) Refined3 opts ip op fmt i
-> Either Msg3 (Refined3 opts ip op fmt i)
forall a b. b -> Either a b
Right Maybe (Refined3 opts ip op fmt i)
mr

-- | same as 'newRefined3P' but skips the proxy and allows you to set each parameter individually using type application

--

-- >>> newRefined3 @OZ @(ReadBase Int 16) @(Lt 255) @(PrintF "%x" Id) "00fe"

-- Right (Refined3 254 "fe")

--

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

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

--

-- >>> newRefined3 @OZ @(ReadBase Int 16) @(Lt 255) @(PrintF "%x" Id) "00fg"

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

--

-- >>> newRefined3 @OL @(Map' (ReadP Int Id) (Resplit "\\.")) @(Msg "length invalid:" (Len == 4)) @(PrintL 4 "%03d.%03d.%03d.%03d" Id) "198.162.3.1.5"

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

--

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

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

--

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

-- Right (Refined3 [198,162,3,1] "198.162.003.001")

--

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

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

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

--

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

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

--

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

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

--

-- >>> newRefined3 @OL @(ParseTimeP TimeOfDay "%-H:%-M:%-S") @'True @(FormatTimeP "%H:%M:%S") "1:15:7"

-- Right (Refined3 01:15:07 "01:15:07")

--

-- >>> newRefined3 @OL @(ParseTimeP TimeOfDay "%-H:%-M:%-S") @'True @(FormatTimeP "%H:%M:%S") "1:2:x"

-- Left Step 1. Failed Initial Conversion(ip) | ParseTimeP TimeOfDay (%-H:%-M:%-S) failed to parse

--

-- >>> newRefined3 @OL @(Rescan "^(\\d{1,2}):(\\d{1,2}):(\\d{1,2})$" >> L2 Head >> Map (ReadP Int Id)) @(All (0 <..> 59) && Len == 3) @(PrintL 3 "%02d:%02d:%02d" Id) "1:2:3"

-- Right (Refined3 [1,2,3] "01:02:03")

--

-- >>> newRefined3 @OL @(Resplit "\\." >> Map (ReadP Int Id)) @(BoolsN "oops" 4 (Between 0 255 Id)) @(PrintL 4 "%03d.%03d.%03d.%03d" Id) "13.2.1.251"

-- Right (Refined3 [13,2,1,251] "013.002.001.251")

--

-- >>> newRefined3 @OZ @(Resplit "\\." >> Map (ReadP Int Id)) @(BoolsN "oops" 4 (Between 0 255 Id)) @(PrintL 4 "%03d.%03d.%03d.%03d" Id) "13.2.1.259"

-- Left Step 2. Failed Boolean Check(op) | Bool(3) [oops]

--

-- >>> newRefined3 @OZ @(Resplit "\\." >> Map (ReadP Int Id)) @(BoolsN "oops" 4 (Between 0 255 Id)) @(PrintL 4 "%03d.%03d.%03d.%03d" Id) "13.2.1.253.1"

-- Left Step 2. Failed Boolean Check(op) | Bools:invalid length(5) expected 4

--

newRefined3 :: forall opts ip op fmt i
  . ( Refined3C opts ip op fmt i
    , Show (PP ip i)
    )
  => i
  -> Either Msg3 (Refined3 opts ip op fmt i)
newRefined3 :: i -> Either Msg3 (Refined3 opts ip op fmt i)
newRefined3 = Identity (Either Msg3 (Refined3 opts ip op fmt i))
-> Either Msg3 (Refined3 opts ip op fmt i)
forall a. Identity a -> a
runIdentity (Identity (Either Msg3 (Refined3 opts ip op fmt i))
 -> Either Msg3 (Refined3 opts ip op fmt i))
-> (i -> Identity (Either Msg3 (Refined3 opts ip op fmt i)))
-> i
-> Either Msg3 (Refined3 opts ip op fmt i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. i -> Identity (Either Msg3 (Refined3 opts ip op fmt i))
forall k k k (opts :: Opt) (ip :: k) (op :: k) (fmt :: k) i
       (m :: Type -> Type).
(MonadEval m, Refined3C opts ip op fmt i, Show (PP ip i)) =>
i -> m (Either Msg3 (Refined3 opts ip op fmt i))
newRefined3'

-- | create a Refined3 using a 5-tuple proxy and aggregate the results on failure

--

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

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

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

--

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

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

--

newRefined3P :: forall opts ip op fmt i proxy
  . ( Refined3C opts ip op fmt i
    , Show (PP ip i)
    )
  => proxy '(opts,ip,op,fmt,i)
  -> i
  -> Either Msg3 (Refined3 opts ip op fmt i)
newRefined3P :: proxy '(opts, ip, op, fmt, i)
-> i -> Either Msg3 (Refined3 opts ip op fmt i)
newRefined3P proxy '(opts, ip, op, fmt, i)
p = Identity (Either Msg3 (Refined3 opts ip op fmt i))
-> Either Msg3 (Refined3 opts ip op fmt i)
forall a. Identity a -> a
runIdentity (Identity (Either Msg3 (Refined3 opts ip op fmt i))
 -> Either Msg3 (Refined3 opts ip op fmt i))
-> (i -> Identity (Either Msg3 (Refined3 opts ip op fmt i)))
-> i
-> Either Msg3 (Refined3 opts ip op fmt i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy '(opts, ip, op, fmt, i)
-> i -> Identity (Either Msg3 (Refined3 opts ip op fmt i))
forall k k k (opts :: Opt) (ip :: k) (op :: k) (fmt :: k) i
       (proxy :: (Opt, k, k, k, Type) -> Type) (m :: Type -> Type).
(MonadEval m, Refined3C opts ip op fmt i, Show (PP ip i)) =>
proxy '(opts, ip, op, fmt, i)
-> i -> m (Either Msg3 (Refined3 opts ip op fmt i))
newRefined3P' proxy '(opts, ip, op, fmt, i)
p

-- | create a Refined3 value using a 5-tuple proxy (see 'mkProxy3')

--

-- use 'mkProxy3' to package all the types together as a 5-tuple

--

eval3P :: forall opts ip op fmt i m proxy
  . ( MonadEval m
    , Refined3C opts ip op fmt i
    )
  => proxy '(opts,ip,op,fmt,i)
  -> i
  -> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
eval3P :: proxy '(opts, ip, op, fmt, i)
-> i -> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
eval3P proxy '(opts, ip, op, fmt, i)
_ = i -> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
forall k k k (opts :: Opt) (ip :: k) (op :: k) (fmt :: k) i
       (m :: Type -> Type).
(MonadEval m, Refined3C opts ip op fmt i) =>
i -> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
eval3M

-- | workhorse for creating 'Refined3' values

eval3M :: forall opts ip op fmt i m
  . ( MonadEval m
    , Refined3C opts ip op fmt i
    )
  => i
  -> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
eval3M :: i -> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
eval3M 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
     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) -> do
        TT i
ss <- Proxy fmt -> POpts -> PP ip i -> m (TT (PP fmt (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 fmt
forall k (t :: k). Proxy t
Proxy @fmt) POpts
o PP ip i
a
        (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
-> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
 -> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i)))
-> (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
-> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
forall a b. (a -> b) -> a -> b
$ case TT i -> (Either String i, Tree PE)
forall a. TT a -> (Either String a, Tree PE)
getValAndPE TT i
ss of
         (Right i
b,Tree PE
t3) -> (PP ip i -> Tree PE -> Tree PE -> Tree PE -> RResults3 (PP ip i)
forall a. a -> Tree PE -> Tree PE -> Tree PE -> RResults3 a
RTTrueT PP ip i
a Tree PE
t1 Tree PE
t2 Tree PE
t3, Refined3 opts ip op fmt i -> Maybe (Refined3 opts ip op fmt i)
forall a. a -> Maybe a
Just (PP ip i -> i -> Refined3 opts ip op fmt i
forall k k k (opts :: Opt) (ip :: k) (op :: k) (fmt :: k) i.
PP ip i -> i -> Refined3 opts ip op fmt i
Refined3 PP ip i
a i
b))
         (Left String
e,Tree PE
t3) -> (PP ip i
-> Tree PE -> Tree PE -> String -> Tree PE -> RResults3 (PP ip i)
forall a.
a -> Tree PE -> Tree PE -> String -> Tree PE -> RResults3 a
RTTrueF PP ip i
a Tree PE
t1 Tree PE
t2 String
e Tree PE
t3, Maybe (Refined3 opts ip op fmt i)
forall a. Maybe a
Nothing)
      (Right Bool
False,Tree PE
t2) -> (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
-> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PP ip i -> Tree PE -> Tree PE -> RResults3 (PP ip i)
forall a. a -> Tree PE -> Tree PE -> RResults3 a
RTFalse PP ip i
a Tree PE
t1 Tree PE
t2, Maybe (Refined3 opts ip op fmt i)
forall a. Maybe a
Nothing)
      (Left String
e,Tree PE
t2) -> (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
-> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PP ip i -> Tree PE -> String -> Tree PE -> RResults3 (PP ip i)
forall a. a -> Tree PE -> String -> Tree PE -> RResults3 a
RTF PP ip i
a Tree PE
t1 String
e Tree PE
t2, Maybe (Refined3 opts ip op fmt i)
forall a. Maybe a
Nothing)
   (Left String
e,Tree PE
t1) -> (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
-> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (String -> Tree PE -> RResults3 (PP ip i)
forall a. String -> Tree PE -> RResults3 a
RF String
e Tree PE
t1, Maybe (Refined3 opts ip op fmt i)
forall a. Maybe a
Nothing)

-- | creates a 'Refined3' value but skips the initial conversion

eval3MSkip :: forall opts ip op fmt i m
  . ( MonadEval m
    , Refined3C opts ip op fmt i
    )
   => PP ip i
   -> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
eval3MSkip :: PP ip i
-> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
eval3MSkip PP ip i
a = do
   let o :: POpts
o = OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts
   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
   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) -> do
      TT i
ss <- Proxy fmt -> POpts -> PP ip i -> m (TT (PP fmt (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 fmt
forall k (t :: k). Proxy t
Proxy @fmt) POpts
o PP ip i
a
      (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
-> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
 -> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i)))
-> (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
-> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
forall a b. (a -> b) -> a -> b
$ case TT i -> (Either String i, Tree PE)
forall a. TT a -> (Either String a, Tree PE)
getValAndPE TT i
ss of
       (Right i
b,Tree PE
t3) -> (PP ip i -> Tree PE -> Tree PE -> Tree PE -> RResults3 (PP ip i)
forall a. a -> Tree PE -> Tree PE -> Tree PE -> RResults3 a
RTTrueT PP ip i
a Tree PE
mkNodeSkipP Tree PE
t2 Tree PE
t3, Refined3 opts ip op fmt i -> Maybe (Refined3 opts ip op fmt i)
forall a. a -> Maybe a
Just (PP ip i -> i -> Refined3 opts ip op fmt i
forall k k k (opts :: Opt) (ip :: k) (op :: k) (fmt :: k) i.
PP ip i -> i -> Refined3 opts ip op fmt i
Refined3 PP ip i
a i
b))
       (Left String
e,Tree PE
t3) -> (PP ip i
-> Tree PE -> Tree PE -> String -> Tree PE -> RResults3 (PP ip i)
forall a.
a -> Tree PE -> Tree PE -> String -> Tree PE -> RResults3 a
RTTrueF PP ip i
a Tree PE
mkNodeSkipP Tree PE
t2 String
e Tree PE
t3, Maybe (Refined3 opts ip op fmt i)
forall a. Maybe a
Nothing)
    (Right Bool
False,Tree PE
t2) -> (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
-> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PP ip i -> Tree PE -> Tree PE -> RResults3 (PP ip i)
forall a. a -> Tree PE -> Tree PE -> RResults3 a
RTFalse PP ip i
a Tree PE
mkNodeSkipP Tree PE
t2, Maybe (Refined3 opts ip op fmt i)
forall a. Maybe a
Nothing)
    (Left String
e,Tree PE
t2) -> (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
-> m (RResults3 (PP ip i), Maybe (Refined3 opts ip op fmt i))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PP ip i -> Tree PE -> String -> Tree PE -> RResults3 (PP ip i)
forall a. a -> Tree PE -> String -> Tree PE -> RResults3 a
RTF PP ip i
a Tree PE
mkNodeSkipP String
e Tree PE
t2, Maybe (Refined3 opts ip op fmt i)
forall a. Maybe a
Nothing)

mkNodeSkipP :: Tree PE
mkNodeSkipP :: Tree PE
mkNodeSkipP = PE -> Forest PE -> Tree PE
forall a. a -> Forest a -> Tree a
Node (ValP -> String -> PE
PE ValP
TrueP String
"skipped PP ip i = Id") []

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

data Msg3 = Msg3 { Msg3 -> String
m3Desc :: !String
                 , Msg3 -> String
m3Short :: !String
                 , Msg3 -> String
m3Long :: !String
                 , Msg3 -> ValP
m3ValP :: !ValP
                 } deriving stock Msg3 -> Msg3 -> Bool
(Msg3 -> Msg3 -> Bool) -> (Msg3 -> Msg3 -> Bool) -> Eq Msg3
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Msg3 -> Msg3 -> Bool
$c/= :: Msg3 -> Msg3 -> Bool
== :: Msg3 -> Msg3 -> Bool
$c== :: Msg3 -> Msg3 -> Bool
Eq

instance Show Msg3 where
  show :: Msg3 -> String
show (Msg3 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

prt3Impl :: forall a . Show a
  => POpts
  -> RResults3 a
  -> Msg3
prt3Impl :: POpts -> RResults3 a -> Msg3
prt3Impl POpts
opts RResults3 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
")")
      mkMsg3 :: String -> String -> String -> ValP -> Msg3
mkMsg3 String
m String
n String
r ValP
bp | POpts -> Bool
hasNoTree POpts
opts = String -> String -> String -> ValP -> Msg3
Msg3 String
m String
n String
"" ValP
bp
                     | Bool
otherwise = String -> String -> String -> ValP -> Msg3
Msg3 String
m String
n String
r ValP
bp
  in case RResults3 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 -> Msg3
mkMsg3 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 -> Msg3
mkMsg3 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 -> Msg3
mkMsg3 String
m String
n String
r ValP
FalseP
       RTTrueF a
a Tree PE
t1 Tree PE
t2 String
e Tree PE
t3 ->
         let (String
m,String
n) = (String
"Step 3. " 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
" Output Conversion(fmt)", 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
"Step 2. Success Boolean Check(op)"
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> String
prtTreePure POpts
opts Tree PE
t2
              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
t3
         in String -> String -> String -> ValP -> Msg3
mkMsg3 String
m String
n String
r (Tree PE
t3 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)
       RTTrueT a
a Tree PE
t1 Tree PE
t2 Tree PE
t3 ->
         let (String
m,String
n) = (String
"Step 3. Success Output Conversion(fmt)", 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
"Step 2. Success Boolean Check(op)"
              String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> String
prtTreePure POpts
opts Tree PE
t2
              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
t3
         in String -> String -> String -> ValP -> Msg3
mkMsg3 String
m String
n String
r (Tree PE
t3 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)

-- | refinement exception

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

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

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