Predicate.Refined2

a refinement type allowing the external type to differ from the internal type

Refined2

data Refined2 (opts :: Opt) ip op i

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

Instances

(Refined2C opts ip op i, Lift (PP ip i), Lift i) => Lift (Refined2 opts ip op i :: Type)

Defined in Predicate.Refined2

Methods

lift :: Refined2 opts ip op i -> Q Exp

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

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

Defined in Predicate.Refined2

Methods

(==) :: Refined2 opts ip op i -> Refined2 opts ip op i -> Bool

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

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

Defined in Predicate.Refined2

Methods

compare :: Refined2 opts ip op i -> Refined2 opts ip op i -> Ordering

(<) :: Refined2 opts ip op i -> Refined2 opts ip op i -> Bool

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

(>) :: Refined2 opts ip op i -> Refined2 opts ip op i -> Bool

(>=) :: Refined2 opts ip op i -> Refined2 opts ip op i -> Bool

max :: Refined2 opts ip op i -> Refined2 opts ip op i -> Refined2 opts ip op i

min :: Refined2 opts ip op i -> Refined2 opts ip op i -> Refined2 opts ip op i

(Refined2C opts ip op i, Read (PP ip i), Read i) => Read (Refined2 opts ip op i)

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

Defined in Predicate.Refined2

Methods

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

readList :: ReadS [Refined2 opts ip op i]

readPrec :: ReadPrec (Refined2 opts ip op i)

readListPrec :: ReadPrec [Refined2 opts ip op i]

(Refined2C opts ip op i, Show i, Show (PP ip i)) => Show (Refined2 opts ip op i)

Defined in Predicate.Refined2

Methods

showsPrec :: Int -> Refined2 opts ip op i -> ShowS

show :: Refined2 opts ip op i -> String

showList :: [Refined2 opts ip op i] -> ShowS

(i ~ String, Refined2C opts ip op i, Show (PP ip i)) => IsString (Refined2 opts ip op i)

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

Defined in Predicate.Refined2

Methods

fromString :: String -> Refined2 opts ip op i

(Arbitrary i, Refined2C opts ip op i, Show (PP ip i)) => Arbitrary (Refined2 opts ip op i)

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

Defined in Predicate.Refined2

Methods

arbitrary :: Gen (Refined2 opts ip op i)

shrink :: Refined2 opts ip op i -> [Refined2 opts ip op i]

(Refined2C opts ip op i, Hashable i) => Hashable (Refined2 opts ip op i)

Hashable instance for Refined2

Defined in Predicate.Refined2

Methods

hashWithSalt :: Int -> Refined2 opts ip op i -> Int

hash :: Refined2 opts ip op i -> Int

(Refined2C opts ip op i, ToJSON i) => ToJSON (Refined2 opts ip op i)

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"

Defined in Predicate.Refined2

Methods

toJSON :: Refined2 opts ip op i -> Value

toEncoding :: Refined2 opts ip op i -> Encoding

toJSONList :: [Refined2 opts ip op i] -> Value

toEncodingList :: [Refined2 opts ip op i] -> Encoding

(Refined2C opts ip op i, Show (PP ip i), FromJSON i) => FromJSON (Refined2 opts ip op i)

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

Methods

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

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

(Refined2C opts ip op i, Show (PP ip i), Binary i) => Binary (Refined2 opts ip op i)

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

Methods

put :: Refined2 opts ip op i -> Put

get :: Get (Refined2 opts ip op i)

putList :: [Refined2 opts ip op i] -> Put

(Refined2C opts ip op i, NFData i, NFData (PP ip i)) => NFData (Refined2 opts ip op i)

Defined in Predicate.Refined2

Methods

rnf :: Refined2 opts ip op i -> ()

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

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

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

Provides the constraints on Refined2

display results

data Msg2

Constructors

Msg2

Fields

• m2Desc :: !String
• m2Short :: !String
• m2Long :: !String
• m2ValP :: !ValP

Instances

Eq Msg2

Defined in Predicate.Refined2

Methods

(==) :: Msg2 -> Msg2 -> Bool

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

Show Msg2

Defined in Predicate.Refined2

Methods

showsPrec :: Int -> Msg2 -> ShowS

show :: Msg2 -> String

showList :: [Msg2] -> ShowS

data RResults2 a

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

Constructors

RF !String !(Tree PE)

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

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

RTTrue !a !(Tree PE) !(Tree PE)

Instances

Show a => Show (RResults2 a)

Defined in Predicate.Refined2

Methods

showsPrec :: Int -> RResults2 a -> ShowS

show :: RResults2 a -> String

showList :: [RResults2 a] -> ShowS

prt2Impl :: forall a. Show a => POpts -> RResults2 a -> Msg2

evaluation methods

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

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

newRefined2 :: forall opts ip op i. (Refined2C opts ip op i, Show (PP ip i)) => i -> Either Msg2 (Refined2 opts ip op i)

pure version for extracting Refined2

>>> newRefined2 @OZ @(ReadBase Int 16) @(Lt 255) "00fe"
Right (Refined2 254 "00fe")

>>> newRefined2 @OZ @(ReadBase Int 16) @(GuardBool (PrintF "0x%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 m. (MonadEval m, Refined2C opts ip op i, Show (PP ip i)) => i -> m (Either Msg2 (Refined2 opts ip op i))

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

same as newRefined2P but runs in IO

proxy methods

type family MakeR2 p where ...

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

Equations

MakeR2 '(opts, ip, op, i) = Refined2 opts ip op i

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

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

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

QuickCheck methods

genRefined2 :: forall opts ip op i. (Refined2C opts ip op i, HasCallStack, Show (PP ip i)) => Gen i -> Gen (Refined2 opts ip op i)

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

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)

create a Refined2 generator using a proxy

unsafe methods for creating Refined2

unsafeRefined2 :: forall opts ip op i. Refined2C opts ip op i => PP ip i -> i -> Refined2 opts ip op i

directly load values into Refined2 without any checking

unsafeRefined2' :: forall opts ip op i. (Show (PP ip i), Refined2C opts ip op i, HasCallStack) => i -> Refined2 opts ip op i

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