Predicate.Refined5

refinement type allowing the external type to differ from the internal type but throws away the original value

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, Lift (PP ip i)) => Lift (Refined5 opts ip op i :: Type)

Defined in Predicate.Refined5

Methods

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

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

(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

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

(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(FromJSON:parseJSON):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(FromJSON:parseJSON):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, 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 -> ()

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

create a Refined5 value using a 4-tuple proxy (see mkProxy2)

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

workhorse for creating Refined5 values

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 creating a Refined5 value

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

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

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

creating a Refined5 value for any MonadEval

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)

create a Refined5 using a 4-tuple proxy and aggregate the results on failure

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 for any MonadEval instance

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 => 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 => 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 => PP ip i -> Refined5 opts ip op i

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

exception

newtype Refined5Exception

refinement exception

Constructors

Refined5Exception String

Instances

Show Refined5Exception

Defined in Predicate.Refined5

Methods

showsPrec :: Int -> Refined5Exception -> ShowS

show :: Refined5Exception -> String

showList :: [Refined5Exception] -> ShowS

Generic Refined5Exception

Defined in Predicate.Refined5

Associated Types

type Rep Refined5Exception :: Type -> Type

Methods

from :: Refined5Exception -> Rep Refined5Exception x

to :: Rep Refined5Exception x -> Refined5Exception

Exception Refined5Exception

Defined in Predicate.Refined5

Methods

toException :: Refined5Exception -> SomeException

fromException :: SomeException -> Maybe Refined5Exception

displayException :: Refined5Exception -> String

type Rep Refined5Exception

Defined in Predicate.Refined5

type Rep Refined5Exception = D1 ('MetaData "Refined5Exception" "Predicate.Refined5" "predicate-typed-0.7.4.5-JjMXzrXEzX77YMQbrq7lii" 'True) (C1 ('MetaCons "Refined5Exception" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))