Predicate.Refined3

Refinement type allowing the external type to differ from the internal type see Refined3

similar to Refined2 but also provides:
* quickCheck methods
* a canonical output value using the 'fmt' parameter

Refined3

data Refined3 (opts :: Opt) ip op fmt i

Like 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

Setting the input type i to 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

Instances

(Refined3C opts ip op fmt i, Lift (PP ip i), Lift i) => Lift (Refined3 opts ip op fmt i :: Type)

Defined in Predicate.Refined3

Methods

lift :: Refined3 opts ip op fmt i -> Q Exp

liftTyped :: Refined3 opts ip op fmt i -> Q (TExp (Refined3 opts ip op fmt i))

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

Defined in Predicate.Refined3

Methods

(==) :: Refined3 opts ip op fmt i -> Refined3 opts ip op fmt i -> Bool

(/=) :: Refined3 opts ip op fmt i -> Refined3 opts ip op fmt i -> Bool

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

Defined in Predicate.Refined3

Methods

compare :: Refined3 opts ip op fmt i -> Refined3 opts ip op fmt i -> Ordering

(<) :: Refined3 opts ip op fmt i -> Refined3 opts ip op fmt i -> Bool

(<=) :: Refined3 opts ip op fmt i -> Refined3 opts ip op fmt i -> Bool

(>) :: Refined3 opts ip op fmt i -> Refined3 opts ip op fmt i -> Bool

(>=) :: Refined3 opts ip op fmt i -> Refined3 opts ip op fmt i -> Bool

max :: Refined3 opts ip op fmt i -> Refined3 opts ip op fmt i -> Refined3 opts ip op fmt i

min :: Refined3 opts ip op fmt i -> Refined3 opts ip op fmt i -> Refined3 opts ip op fmt i

(Eq i, Refined3C opts ip op fmt i, Read (PP ip i), Read i) => Read (Refined3 opts ip op fmt i)

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","")]

Defined in Predicate.Refined3

Methods

readsPrec :: Int -> ReadS (Refined3 opts ip op fmt i)

readList :: ReadS [Refined3 opts ip op fmt i]

readPrec :: ReadPrec (Refined3 opts ip op fmt i)

readListPrec :: ReadPrec [Refined3 opts ip op fmt i]

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

Defined in Predicate.Refined3

Methods

showsPrec :: Int -> Refined3 opts ip op fmt i -> ShowS

show :: Refined3 opts ip op fmt i -> String

showList :: [Refined3 opts ip op fmt i] -> ShowS

(Refined3C opts ip op fmt String, Show (PP ip String)) => IsString (Refined3 opts ip op fmt String)

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

Defined in Predicate.Refined3

Methods

fromString :: String -> Refined3 opts ip op fmt String

(Arbitrary (PP ip i), Refined3C opts ip op fmt i) => Arbitrary (Refined3 opts ip op fmt i)

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

Defined in Predicate.Refined3

Methods

arbitrary :: Gen (Refined3 opts ip op fmt i)

shrink :: Refined3 opts ip op fmt i -> [Refined3 opts ip op fmt i]

(Refined3C opts ip op fmt i, Hashable (PP ip i)) => Hashable (Refined3 opts ip op fmt i)

Hashable instance for Refined3

Defined in Predicate.Refined3

Methods

hashWithSalt :: Int -> Refined3 opts ip op fmt i -> Int

hash :: Refined3 opts ip op fmt i -> Int

(Refined3C opts ip op fmt i, ToJSON i) => ToJSON (Refined3 opts ip op fmt i)

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"

Defined in Predicate.Refined3

Methods

toJSON :: Refined3 opts ip op fmt i -> Value

toEncoding :: Refined3 opts ip op fmt i -> Encoding

toJSONList :: [Refined3 opts ip op fmt i] -> Value

toEncodingList :: [Refined3 opts ip op fmt i] -> Encoding

(Refined3C opts ip op fmt i, Show (PP ip i), FromJSON i) => FromJSON (Refined3 opts ip op fmt i)

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

Defined in Predicate.Refined3

Methods

parseJSON :: Value -> Parser (Refined3 opts ip op fmt i)

parseJSONList :: Value -> Parser [Refined3 opts ip op fmt i]

(Refined3C opts ip op fmt i, Show (PP ip i), Binary i) => Binary (Refined3 opts ip op fmt i)

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: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"

Defined in Predicate.Refined3

Methods

put :: Refined3 opts ip op fmt i -> Put

get :: Get (Refined3 opts ip op fmt i)

putList :: [Refined3 opts ip op fmt i] -> Put

(Refined3C opts ip op fmt i, NFData i, NFData (PP ip i)) => NFData (Refined3 opts ip op fmt i)

Defined in Predicate.Refined3

Methods

rnf :: Refined3 opts ip op fmt i -> ()

r3In :: Refined3 opts ip op fmt i -> PP ip i

r3Out :: Refined3 opts ip op fmt i -> i

type Refined3C opts ip op fmt i = (OptC opts, P ip i, P op (PP ip i), PP op (PP ip i) ~ Bool, P fmt (PP ip i), PP fmt (PP ip i) ~ i)

Provides the constraints on Refined3

display results

data Msg3

Constructors

Msg3

Fields

• m3Desc :: !String
• m3Short :: !String
• m3Long :: !String
• m3ValP :: !ValP

Instances

Eq Msg3

Defined in Predicate.Refined3

Methods

(==) :: Msg3 -> Msg3 -> Bool

(/=) :: Msg3 -> Msg3 -> Bool

Show Msg3

Defined in Predicate.Refined3

Methods

showsPrec :: Int -> Msg3 -> ShowS

show :: Msg3 -> String

showList :: [Msg3] -> ShowS

data RResults3 a

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

Constructors

RF !String !(Tree PE)

RTF !a !(Tree PE) !String !(Tree PE)

RTFalse !a !(Tree PE) !(Tree PE)

RTTrueF !a !(Tree PE) !(Tree PE) !String !(Tree PE)

RTTrueT !a !(Tree PE) !(Tree PE) !(Tree PE)

Instances

Show a => Show (RResults3 a)

Defined in Predicate.Refined3

Methods

showsPrec :: Int -> RResults3 a -> ShowS

show :: RResults3 a -> String

showList :: [RResults3 a] -> ShowS

evaluation methods

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

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

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

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

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)

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 "0x%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 m. (MonadEval m, Refined3C opts ip op fmt i, Show (PP ip i)) => i -> m (Either Msg3 (Refined3 opts ip op fmt i))

same as newRefined3P' but passes in the proxy

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)

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

same as newRefined3P but runs in IO

proxy methods

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

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), Refined3C opts ip op fmt i) => Proxy '(opts, ip, op, fmt, i)

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

type family MakeR3 p where ...

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

Equations

MakeR3 '(opts, ip, op, fmt, i) = Refined3 opts ip op fmt i

type family MakeR3' opts p where ...

Equations

MakeR3' opts '(ip, op, fmt, i) = Refined3 opts ip op fmt i

unsafe methods for creating Refined3

unsafeRefined3 :: forall opts ip op fmt i. Refined3C opts ip op fmt i => PP ip i -> i -> Refined3 opts ip op fmt i

directly load values into Refined3 without any checking

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

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

QuickCheck methods

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)

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

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)

create a Refined3 generator using a proxy