Safe Haskell | None |
---|---|
Language | Haskell2010 |
a refinement type allowing the external type to differ from the internal type
Synopsis
- data Refined2 (opts :: Opt) 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)
- data Msg2 = Msg2 {}
- data RResults2 a
- prt2Impl :: forall a. Show a => POpts -> RResults2 a -> Msg2
- 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)
- 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))
- type family MakeR2 p where ...
- mkProxy2 :: forall z opts ip op i. z ~ '(opts, ip, op, i) => Proxy '(opts, ip, op, i)
- mkProxy2' :: forall z opts ip op i. (z ~ '(ip, op, i), Refined2C opts ip op i) => Proxy '(opts, ip, op, i)
- genRefined2 :: forall opts ip op i. (Refined2C opts ip op i, HasCallStack, Show (PP ip i)) => Gen i -> Gen (Refined2 opts ip op i)
- 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)
- unsafeRefined2 :: forall opts ip op i. Refined2C opts ip op i => PP ip i -> i -> Refined2 opts ip op i
- unsafeRefined2' :: forall opts ip op i. (Show (PP ip i), Refined2C opts ip op i, HasCallStack) => i -> Refined2 opts ip op i
- newtype Refined2Exception = Refined2Exception String
Refined2
data Refined2 (opts :: Opt) ip op i Source #
Refinement type for specifying an input type that is different from the output type
opts
are the display optionsip
convertsi
toPP ip i
which is the internal type inr2In
op
validates that internal type usingPP op (PP ip i) ~ Bool
i
is the input type which is stored inr2Out
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) Source # | |
(Refined2C opts ip op i, Eq i, Eq (PP ip i)) => Eq (Refined2 opts ip op i) Source # | |
(Refined2C opts ip op i, Ord i, Ord (PP ip i)) => Ord (Refined2 opts ip op i) Source # | |
Defined in Predicate.Refined2 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) Source # |
|
(Refined2C opts ip op i, Show i, Show (PP ip i)) => Show (Refined2 opts ip op i) Source # | |
(i ~ String, Refined2C opts ip op i, Show (PP ip i)) => IsString (Refined2 opts ip op i) Source # |
|
Defined in Predicate.Refined2 fromString :: String -> Refined2 opts ip op i # | |
(Arbitrary i, Refined2C opts ip op i, Show (PP ip i)) => Arbitrary (Refined2 opts ip op i) Source # |
|
(Refined2C opts ip op i, Hashable i) => Hashable (Refined2 opts ip op i) Source # | |
Defined in Predicate.Refined2 | |
(Refined2C opts ip op i, ToJSON i) => ToJSON (Refined2 opts ip op i) Source # |
|
Defined in Predicate.Refined2 | |
(Refined2C opts ip op i, Show (PP ip i), FromJSON i) => FromJSON (Refined2 opts ip op i) Source # |
|
(Refined2C opts ip op i, Show (PP ip i), Binary i) => Binary (Refined2 opts ip op i) Source # |
|
(Refined2C opts ip op i, NFData i, NFData (PP ip i)) => NFData (Refined2 opts ip op i) Source # | |
Defined in Predicate.Refined2 |
r2In :: Refined2 (opts :: Opt) ip op i -> PP ip i Source #
field accessor for the converted input value in Refined2
r2Out :: Refined2 (opts :: Opt) ip op i -> i Source #
field accessor for the original input value in Refined2
type Refined2C opts ip op i = (OptC opts, P ip i, P op (PP ip i), PP op (PP ip i) ~ Bool) Source #
Provides the constraints on Refined2
display results
holds the results of creating a Refined2
value for display
An ADT that summarises the results of evaluating Refined2 representing all possible states
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)) Source #
create a Refined2 value using a 4-tuple proxy (see mkProxy2
)
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)) Source #
workhorse for creating Refined2
values
newRefined2 :: forall opts ip op i. (Refined2C opts ip op i, Show (PP ip i)) => i -> Either Msg2 (Refined2 opts ip op i) Source #
pure version for creating a Refined2
value
>>>
newRefined2 @OZ @(ReadBase Int 16) @(Lt 255) "00fe"
Right (Refined2 254 "00fe")
>>>
newRefined2 @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
>>>
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)) Source #
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) Source #
create a Refined2 using a 4-tuple proxy and aggregate the results on failure
>>>
type T4 k = '(OZ, MkDayExtra Id >> 'Just Id, GuardBool "expected a Sunday" (Thd == 7), k)
>>>
newRefined2P (Proxy @(T4 _)) (2019,10,12)
Left Step 2. Failed Boolean Check(op) | expected a Sunday
>>>
newRefined2P (Proxy @(T4 _)) (2019,10,13)
Right (Refined2 (2019-10-13,41,7) (2019,10,13))
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)) Source #
same as newRefined2P
but runs for any MonadEval instance
proxy methods
type family MakeR2 p where ... Source #
type family for converting from a 4-tuple '(opts,ip,op,i) to a Refined2
type
mkProxy2 :: forall z opts ip op i. z ~ '(opts, ip, op, i) => Proxy '(opts, ip, op, i) Source #
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) Source #
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) Source #
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) Source #
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 Source #
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 Source #
directly load values into Refined2
. It still checks to see that those values are valid
exception
newtype Refined2Exception Source #
refinement exception
Instances
Show Refined2Exception Source # | |
Defined in Predicate.Refined2 showsPrec :: Int -> Refined2Exception -> ShowS # show :: Refined2Exception -> String # showList :: [Refined2Exception] -> ShowS # | |
Generic Refined2Exception Source # | |
Defined in Predicate.Refined2 type Rep Refined2Exception :: Type -> Type # from :: Refined2Exception -> Rep Refined2Exception x # to :: Rep Refined2Exception x -> Refined2Exception # | |
Exception Refined2Exception Source # | |
Defined in Predicate.Refined2 | |
type Rep Refined2Exception Source # | |
Defined in Predicate.Refined2 type Rep Refined2Exception = D1 ('MetaData "Refined2Exception" "Predicate.Refined2" "predicate-typed-0.7.4.4-1vpy5lu48CkBuwvIfscZLd" 'True) (C1 ('MetaCons "Refined2Exception" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) |