Predicate.Refined5

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

Refined5

data Refined5 (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 stored
• op validates that internal type using PP op (PP ip i) ~ Bool
• i is the input type which is discarded after converting to PP ip i

Instances

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

Defined in Predicate.Refined5

Methods

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

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

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

Defined in Predicate.Refined5

Methods

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

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

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

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

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

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

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

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

Read instance for Refined5

>>> reads @(Refined5 OZ (ReadBase Int 16) (0 <..> 0xff) String) "Refined5 254"
[(Refined5 254,"")]

>>> reads @(Refined5 OZ (ReadBase Int 16) (0 <..> 0xff) String) "Refined5 300"
[]

>>> reads @(Refined5 OZ (ReadBase Int 16) (Id < 0) String) "Refined5 -1234"
[(Refined5 (-1234),"")]

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

>>> reads @(Refined5 OZ (ReadP Rational Id) (Id > Negate 4 % 3) String) "Refined5 (-10 % 9)"
[(Refined5 ((-10) % 9),"")]

>>> reads @(Refined5 OZ (ReadP Rational Id) (Id > Negate 4 % 3) String) "Refined5 (-10 % 6)"
[]

Defined in Predicate.Refined5

Methods

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

readList :: ReadS [Refined5 opts ip op i]

readPrec :: ReadPrec (Refined5 opts ip op i)

readListPrec :: ReadPrec [Refined5 opts ip op i]

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

Defined in Predicate.Refined5

Methods

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

show :: Refined5 opts ip op i -> String

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

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

IsString instance for Refined5

>>> pureTryTest $ fromString @(Refined5 OL (ReadP Int Id) (Id > 12) String) "523"
Right (Refined5 523)

>>> pureTryTest $ fromString @(Refined5 OL (ReadP Int Id) (Id > 12) String) "2"
Left ()

Defined in Predicate.Refined5

Methods

fromString :: String -> Refined5 opts ip op i

(Refined2C opts ip op i, Lift (PP ip i)) => Lift (Refined5 opts ip op i)

Defined in Predicate.Refined5

Methods

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

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

Arbitrary instance for Refined5

>>> :m + Data.Time.Calendar.WeekDate
>>> xs <- generate (vectorOf 10 (arbitrary @(Refined5 OAN (ReadP Int Id) (Negate 10 <..> 10) String)))
>>> all (\x -> unRefined5 x `elem` [-10 .. 10]) xs
True

Defined in Predicate.Refined5

Methods

arbitrary :: Gen (Refined5 opts ip op i)

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

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

Binary instance for Refined5

Defined in Predicate.Refined5

Methods

put :: Refined5 opts ip op i -> Put

get :: Get (Refined5 opts ip op i)

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

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

Defined in Predicate.Refined5

Methods

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

(Refined2C opts ip op i, Hashable (PP ip i)) => Hashable (Refined5 opts ip op i)

Hashable instance for Refined5

Defined in Predicate.Refined5

Methods

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

hash :: Refined5 opts ip op i -> Int

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

FromJSON instance for Refined5

>>> import qualified Data.Aeson as A
>>> A.eitherDecode' @(Refined5 OZ (ReadBase Int 16) (Id > 10 && Id < 256) String) "123"
Right (Refined5 123)

>>> removeAnsi $ A.eitherDecode' @(Refined5 OL (ReadBase Int 16) (Id > 10 && Id < 256) String) "9"
Error in $: Refined5:false boolean check | {False && True | (9 > 10)}
False

>>> A.eitherDecode' @(Refined5 OZ (ReadBase Int 16) (Id > 10 && Id < 256) String) "254"
Right (Refined5 254)

>>> removeAnsi $ A.eitherDecode' @(Refined5 OAN (ReadBase Int 16) (Id > 10 && Id < 256) String) "12345"
Error in $: Refined5:false boolean check | {True && False | (12345 < 256)}
False True && False | (12345 < 256)
|
+- True 12345 > 10
|  |
|  +- P Id 12345
|  |
|  `- P '10
|
`- False 12345 < 256
   |
   +- P Id 12345
   |
   `- P '256

Defined in Predicate.Refined5

Methods

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

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

(Refined2C opts ip op i, ToJSON (PP ip i)) => ToJSON (Refined5 opts ip op i)

ToJSON instance for Refined5

>>> import qualified Data.Aeson as A
>>> A.encode (unsafeRefined5' @OZ @(ReadBase Int 16) @(Between 0 255 Id) 254)
"254"

>>> A.encode (unsafeRefined5 @OZ @Id @'True @Int 123)
"123"

Defined in Predicate.Refined5

Methods

toJSON :: Refined5 opts ip op i -> Value

toEncoding :: Refined5 opts ip op i -> Encoding

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

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

unRefined5 :: forall k k1 (opts :: Opt) (ip :: k) (op :: k1) i. Refined5 opts ip op i -> PP ip i

extract the value from Refined5

evaluation methods

eval5P :: 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 (Refined5 opts ip op i))

eval5M :: forall opts ip op i m. (MonadEval m, Refined2C opts ip op i) => i -> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))

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

pure version for extracting Refined5

>>> newRefined5 @OZ @(ReadBase Int 16) @(Lt 255) "00fe"
Right (Refined5 254)

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

>>> newRefined5 @OZ @(ReadBase Int 16) @(Lt 255) "00fg"
Left Step 1. Failed Initial Conversion(ip) | invalid base 16

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

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

>>> newRefined5 @OZ @(Map' (ReadP Int Id) (Resplit "\\.")) @(GuardBool (PrintF "found length=%d" Len) (Len == 4)) "198.162.3.1"
Right (Refined5 [198,162,3,1])

>>> :m + Data.Time.Calendar.WeekDate
>>> newRefined5 @OZ @(MkDayExtra Id >> 'Just Id) @(GuardBool "expected a Sunday" (Thd == 7)) (2019,10,13)
Right (Refined5 (2019-10-13,41,7))

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

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

>>> newRefined5 @OL @Id @'True 22
Right (Refined5 22)

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

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

newRefined5' :: forall opts ip op i m. (MonadEval m, Refined2C opts ip op i, Show (PP ip i)) => i -> m (Either Msg2 (Refined5 opts ip op i))

newRefined5P :: forall opts ip op i. (Refined2C opts ip op i, Show (PP ip i)) => Proxy '(opts, ip, op, i) -> i -> Either Msg2 (Refined5 opts ip op i)

newRefined5P' :: 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 (Refined5 opts ip op i))

same as newRefined5P but runs in IO

proxy methods

type family MakeR5 p where ...

creates a 4-tuple proxy (see eval5P newRefined5P)

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)
>>> newRefined5P eg1 "24"
Right (Refined5 24)

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

>>> eg2 = mkProxy2 @_ @OL @(ReadP Int Id) @(Gt 10)
>>> newRefined5P eg2 "24"
Right (Refined5 24)

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

Equations

MakeR5 '(opts, ip, op, i) = Refined5 opts ip op i

QuickCheck methods

genRefined5 :: forall opts ip op i. (Refined2C opts ip op i, HasCallStack) => Gen (PP ip i) -> Gen (Refined5 opts ip op i)

create a Refined5 generator using a generator to restrict the values (so it completes)

genRefined5P :: forall opts ip op i. (Refined2C opts ip op i, HasCallStack) => Proxy '(opts, ip, op, i) -> Gen (PP ip i) -> Gen (Refined5 opts ip op i)

create a Refined5 generator using a proxy

unsafe methods for creating Refined5

unsafeRefined5 :: forall opts ip op i. PP ip i -> Refined5 opts ip op i

directly load values into Refined5 without any checking

unsafeRefined5' :: forall opts ip op i. (Refined2C opts ip op i, HasCallStack) => PP ip i -> Refined5 opts ip op i

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