Safe Haskell | None |
---|---|
Language | Haskell2010 |
Refinement type allowing the external type to differ from the internal type
like Refined2
but also supports a canonical output value using the 'fmt' parameter
Synopsis
- data Refined3 (opts :: Opt) 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)
- data Msg3 = Msg3 {}
- data RResults3 a
- 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))
- 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)
- 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))
- 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)
- 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))
- mkProxy3 :: forall z opts ip op fmt i. z ~ '(opts, ip, op, fmt, i) => Proxy '(opts, ip, op, fmt, i)
- 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)
- type family MakeR3 p where ...
- unsafeRefined3 :: forall opts ip op fmt i. Refined3C opts ip op fmt i => PP ip i -> i -> Refined3 opts ip op fmt i
- 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
- 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)
- 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)
- newtype Refined3Exception = Refined3Exception String
Refined3
data Refined3 (opts :: Opt) ip op fmt i Source #
Like Refined2
but additionally reconstructs the output value to a standardized format
opts
are the display optionsip
convertsi
toPP ip i
which is the internal type and stored inr3In
op
validates that internal type usingPP op (PP ip i) ~ Bool
fmt
outputs the internal typePP fmt (PP ip i) ~ i
and stored inr3Out
i
is the input typePP 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 inr3Out
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) Source # | |
(Refined3C opts ip op fmt i, Eq (PP ip i), Eq i) => Eq (Refined3 opts ip op fmt i) Source # | |
(Refined3C opts ip op fmt i, Ord (PP ip i), Ord i) => Ord (Refined3 opts ip op fmt i) Source # | |
Defined in Predicate.Refined3 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) Source # |
|
(Refined3C opts ip op fmt i, Show (PP ip i), Show i) => Show (Refined3 opts ip op fmt i) Source # | |
(Refined3C opts ip op fmt String, Show (PP ip String)) => IsString (Refined3 opts ip op fmt String) Source # |
|
Defined in Predicate.Refined3 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) Source # |
|
(Refined3C opts ip op fmt i, Hashable (PP ip i)) => Hashable (Refined3 opts ip op fmt i) Source # | |
Defined in Predicate.Refined3 | |
(Refined3C opts ip op fmt i, ToJSON i) => ToJSON (Refined3 opts ip op fmt i) Source # |
|
Defined in Predicate.Refined3 | |
(Refined3C opts ip op fmt i, Show (PP ip i), FromJSON i) => FromJSON (Refined3 opts ip op fmt i) Source # |
|
(Refined3C opts ip op fmt i, Show (PP ip i), Binary i) => Binary (Refined3 opts ip op fmt i) Source # |
|
(Refined3C opts ip op fmt i, NFData i, NFData (PP ip i)) => NFData (Refined3 opts ip op fmt i) Source # | |
Defined in Predicate.Refined3 |
r3In :: Refined3 opts ip op fmt i -> PP ip i Source #
field accessor for the converted input value in Refined3
r3Out :: Refined3 opts ip op fmt i -> i Source #
field accessor for the converted output value in Refined3
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) Source #
Provides the constraints on Refined3
display results
holds the results of creating a Refined3
value for display
An ADT that summarises the results of evaluating Refined3 representing all possible states
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)) Source #
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)) Source #
workhorse for creating Refined3
values
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) Source #
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 "%#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)) Source #
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) Source #
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)) Source #
same as newRefined3P
but runs in any MonadEval instance
proxy methods
mkProxy3 :: forall z opts ip op fmt i. z ~ '(opts, ip, op, fmt, i) => Proxy '(opts, ip, op, fmt, i) Source #
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) Source #
type family MakeR3 p where ... Source #
type family for converting from a 5-tuple '(opts,ip,op,fmt,i) to a Refined3
type
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 Source #
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 Source #
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) Source #
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) Source #
create a Refined3
generator using a proxy
exception
newtype Refined3Exception Source #
refinement exception
Instances
Show Refined3Exception Source # | |
Defined in Predicate.Refined3 showsPrec :: Int -> Refined3Exception -> ShowS # show :: Refined3Exception -> String # showList :: [Refined3Exception] -> ShowS # | |
Generic Refined3Exception Source # | |
Defined in Predicate.Refined3 type Rep Refined3Exception :: Type -> Type # from :: Refined3Exception -> Rep Refined3Exception x # to :: Rep Refined3Exception x -> Refined3Exception # | |
Exception Refined3Exception Source # | |
Defined in Predicate.Refined3 | |
type Rep Refined3Exception Source # | |
Defined in Predicate.Refined3 type Rep Refined3Exception = D1 ('MetaData "Refined3Exception" "Predicate.Refined3" "predicate-typed-0.7.4.5-JjMXzrXEzX77YMQbrq7lii" 'True) (C1 ('MetaCons "Refined3Exception" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) |