Safe Haskell | None |
---|---|
Language | Haskell2010 |
Refinement type allowing the external type to differ from the internal type
doesnt store the output value but runs on demand but has calculate each time and could fail later
see Refined1
similar to Refined2
but also provides:
* quickCheck methods
* ability to combine refinement types
* a canonical output value using the 'fmt' parameter
Synopsis
- data Refined1 (opts :: OptT) ip op fmt i
- unRefined1 :: forall (opts :: OptT) ip op fmt i. Refined1 opts ip op fmt i -> PP ip i
- type Refined1C opts ip op fmt i = (OptTC 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)
- prtEval1 :: forall opts ip op fmt i. (Refined1C opts ip op fmt i, Show (PP ip i), Show i) => i -> Either Msg1 (Refined1 opts ip op fmt i)
- prtEval1P :: forall opts ip op fmt i proxy. (Refined1C opts ip op fmt i, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> i -> Either Msg1 (Refined1 opts ip op fmt i)
- prtEval1IO :: forall opts ip op fmt i. (Refined1C opts ip op fmt i, Show (PP ip i), Show i) => i -> IO (Either String (Refined1 opts ip op fmt i))
- prtEval1PIO :: forall opts ip op fmt i proxy. (Refined1C opts ip op fmt i, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> i -> IO (Either String (Refined1 opts ip op fmt i))
- prt1IO :: forall opts a b r. (OptTC opts, Show a, Show b) => (RResults1 a b, Maybe r) -> IO (Either String r)
- prt1Impl :: forall a b. (Show a, Show b) => POpts -> RResults1 a b -> Msg1
- data Msg1 = Msg1 {}
- data RResults1 a b
- eval1 :: forall opts ip op fmt i. Refined1C opts ip op fmt i => i -> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 opts ip op fmt i))
- eval1P :: forall opts ip op fmt i proxy. Refined1C opts ip op fmt i => proxy '(opts, ip, op, fmt, i) -> i -> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 opts ip op fmt i))
- eval1M :: forall opts ip op fmt i m. (MonadEval m, Refined1C opts ip op fmt i) => i -> m (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 opts ip op fmt i))
- newRefined1 :: forall opts ip op fmt i. (Refined1C opts ip op fmt i, Show (PP ip i), Show i) => i -> Either String (Refined1 opts ip op fmt i)
- newRefined1P :: forall opts ip op fmt i proxy. (Refined1C opts ip op fmt i, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> i -> Either String (Refined1 opts ip op fmt i)
- newRefined1T :: forall opts ip op fmt i m. (Refined1C opts ip op fmt i, Monad m, Show (PP ip i), Show i) => i -> RefinedT m (Refined1 opts ip op fmt i)
- newRefined1TP :: forall opts ip op fmt i proxy m. (Refined1C opts ip op fmt i, Monad m, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> i -> RefinedT m (Refined1 opts ip op fmt i)
- newRefined1TPIO :: forall opts ip op fmt i proxy m. (Refined1C opts ip op fmt i, MonadIO m, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> i -> RefinedT m (Refined1 opts ip op fmt i)
- withRefined1T :: forall opts ip op fmt i m b. (Monad m, Refined1C opts ip op fmt i, Show (PP ip i), Show i) => i -> (Refined1 opts ip op fmt i -> RefinedT m b) -> RefinedT m b
- withRefined1TIO :: forall opts ip op fmt i m b. (MonadIO m, Refined1C opts ip op fmt i, Show (PP ip i), Show i) => i -> (Refined1 opts ip op fmt i -> RefinedT m b) -> RefinedT m b
- withRefined1TP :: forall opts ip op fmt i b proxy m. (Monad m, Refined1C opts ip op fmt i, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> i -> (Refined1 opts ip op fmt i -> RefinedT m b) -> RefinedT m b
- mkProxy1 :: forall z opts ip op fmt i. z ~ '(opts, ip, op, fmt, i) => Proxy '(opts, ip, op, fmt, i)
- mkProxy1' :: forall z opts ip op fmt i. (z ~ '(opts, ip, op, fmt, i), Refined1C opts ip op fmt i) => Proxy '(opts, ip, op, fmt, i)
- type family MakeR1 p where ...
- unsafeRefined1 :: forall opts ip op fmt i. PP ip i -> Refined1 opts ip op fmt i
- unsafeRefined1' :: forall opts ip op fmt i. (HasCallStack, Show i, Show (PP ip i), Refined1C opts ip op fmt i) => i -> Refined1 opts ip op fmt i
- convertRefined1TP :: forall opts ip op fmt i ip1 op1 fmt1 i1 m. (Refined1C opts ip1 op1 fmt1 i1, Monad m, Show (PP ip i), PP ip i ~ PP ip1 i1, Show i1) => Proxy '(opts, ip, op, fmt, i) -> Proxy '(opts, ip1, op1, fmt1, i1) -> RefinedT m (Refined1 opts ip op fmt i) -> RefinedT m (Refined1 opts ip1 op1 fmt1 i1)
- rapply1 :: forall opts ip op fmt i m. (Refined1C opts ip op fmt i, Monad m, Show (PP ip i), Show i) => (PP ip i -> PP ip i -> PP ip i) -> RefinedT m (Refined1 opts ip op fmt i) -> RefinedT m (Refined1 opts ip op fmt i) -> RefinedT m (Refined1 opts ip op fmt i)
- rapply1P :: forall opts ip op fmt i proxy m. (Refined1C opts ip op fmt i, Monad m, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> (PP ip i -> PP ip i -> PP ip i) -> RefinedT m (Refined1 opts ip op fmt i) -> RefinedT m (Refined1 opts ip op fmt i) -> RefinedT m (Refined1 opts ip op fmt i)
- genRefined1 :: forall opts ip op fmt i. Refined1C opts ip op fmt i => Gen (PP ip i) -> Gen (Refined1 opts ip op fmt i)
- genRefined1P :: forall opts ip op fmt i. Refined1C opts ip op fmt i => Proxy '(opts, ip, op, fmt, i) -> Gen (PP ip i) -> Gen (Refined1 opts ip op fmt i)
- type RefinedEmulate (opts :: OptT) p a = Refined1 opts Id p Id a
- eval1PX :: forall opts ip op fmt i proxy. Refined1C opts ip op fmt i => proxy '(opts, ip, op, fmt, i) -> i -> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined opts op (PP ip i), PP fmt (PP ip i)))
- eval1X :: forall opts ip op fmt i. Refined1C opts ip op fmt i => i -> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined opts op (PP ip i), PP fmt (PP ip i)))
- type family ReplaceOptT1 (o :: OptT) t where ...
- type family AppendOptT1 (o :: OptT) t where ...
Refined1
data Refined1 (opts :: OptT) ip op fmt i Source #
Refinement type that differentiates the input from output: similar to Refined3
but only creates the output value as needed.
opts
are the display optionsip
convertsi
toPP ip i
which is the internal type and stored inunRefined1
op
validates that internal type usingPP op (PP ip i) ~ Bool
fmt
outputs the internal typePP fmt (PP ip i) ~ i
(not stored anywhere but created on demand)i
is the input typePP fmt (PP ip i)
should be valid as input for Refined1
Setting ip
to Id
and fmt
to Id
makes it equivalent to Refined
: see RefinedEmulate
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
unRefined1
- validate
unRefined1
using the predicate op - show
unRefined1
using fmt (does not store the formatted result unlikeRefined3
)
Although a common scenario is String as input, you are free to choose any input type you like
>>>
newRefined1 @OZ @(ReadBase Int 16 Id) @(Lt 255) @(PrintF "%x" Id) "00fe"
Right (Refined1 254)
>>>
newRefined1 @OZ @(ReadBase Int 16 Id) @(Lt 253) @(PrintF "%x" Id) "00fe"
Left "Step 2. False Boolean Check(op) | FalseP"
>>>
newRefined1 @OZ @(ReadBase Int 16 Id) @(Lt 255) @(PrintF "%x" Id) "00fg"
Left "Step 1. Initial Conversion(ip) Failed | invalid base 16"
>>>
newRefined1 @OL @(Map (ReadP Int Id) (Resplit "\\." Id)) @(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}"
>>>
newRefined1 @OZ @(Map (ReadP Int Id) (Resplit "\\." Id)) @(Guard (PrintF "found length=%d" Len) (Len == 4) >> 'True) @(PrintL 4 "%03d.%03d.%03d.%03d" Id) "198.162.3.1.5"
Left "Step 2. Failed Boolean Check(op) | found length=5"
>>>
newRefined1 @OZ @(Map (ReadP Int Id) (Resplit "\\." Id)) @(Guard (PrintF "found length=%d" Len) (Len == 4) >> 'True) @(PrintL 4 "%03d.%03d.%03d.%03d" Id) "198.162.3.1"
Right (Refined1 [198,162,3,1])
>>>
:m + Data.Time.Calendar.WeekDate
>>>
newRefined1 @OZ @(MkDayExtra Id >> 'Just Id) @(Guard "expected a Sunday" (Thd Id == 7) >> 'True) @(UnMkDay (Fst Id)) (2019,10,13)
Right (Refined1 (2019-10-13,41,7))
>>>
newRefined1 @OL @(MkDayExtra Id >> 'Just Id) @(Msg "expected a Sunday:" (Thd Id == 7)) @(UnMkDay (Fst Id)) (2019,10,12)
Left "Step 2. False Boolean Check(op) | {expected a Sunday: 6 == 7}"
>>>
newRefined1 @OZ @(MkDayExtra' (Fst Id) (Snd Id) (Thd Id) >> 'Just Id) @(Guard "expected a Sunday" (Thd Id == 7) >> 'True) @(UnMkDay (Fst Id)) (2019,10,12)
Left "Step 2. Failed Boolean Check(op) | expected a Sunday"
>>>
type T4 k = '( OZ, MkDayExtra Id >> 'Just Id, Guard "expected a Sunday" (Thd Id == 7) >> 'True, UnMkDay (Fst Id), k)
>>>
newRefined1P (Proxy @(T4 _)) (2019,10,12)
Left "Step 2. Failed Boolean Check(op) | expected a Sunday"
>>>
newRefined1P (Proxy @(T4 _)) (2019,10,13)
Right (Refined1 (2019-10-13,41,7))
Instances
(Eq i, Eq (PP ip i), Eq (PP fmt (PP ip i))) => Eq (Refined1 opts ip op fmt i) Source # | |
(Eq i, Show i, Eq (PP ip i), Show (PP ip i), Refined1C opts ip op fmt i, Read (PP ip i), Read (PP fmt (PP ip i))) => Read (Refined1 opts ip op fmt i) Source # |
|
(Show i, Show (PP ip i), Show (PP fmt (PP ip i))) => Show (Refined1 opts ip op fmt i) Source # | |
(Refined1C opts ip op fmt String, Show (PP ip String)) => IsString (Refined1 opts ip op fmt String) Source # |
|
Defined in Predicate.Refined1 fromString :: String -> Refined1 opts ip op fmt String # | |
(Lift (PP ip i), Lift (PP fmt (PP ip i))) => Lift (Refined1 opts ip op fmt i) Source # | |
(Arbitrary (PP ip i), Refined1C opts ip op fmt i) => Arbitrary (Refined1 opts ip op fmt i) Source # |
|
(Refined1C opts ip op fmt i, Hashable (PP ip i)) => Hashable (Refined1 opts ip op fmt i) Source # | |
Defined in Predicate.Refined1 | |
(OptTC opts, Show (PP fmt (PP ip i)), ToJSON (PP fmt (PP ip i)), P fmt (PP ip i)) => ToJSON (Refined1 opts ip op fmt i) Source # |
|
Defined in Predicate.Refined1 | |
(Show (PP fmt (PP ip i)), Show (PP ip i), Refined1C opts ip op fmt i, FromJSON i) => FromJSON (Refined1 opts ip op fmt i) Source # |
|
(Show (PP fmt (PP ip i)), Show (PP ip i), Refined1C opts ip op fmt i, Binary i) => Binary (Refined1 opts ip op fmt i) Source # |
|
type Refined1C opts ip op fmt i = (OptTC 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 Refined1
display results
prtEval1 :: forall opts ip op fmt i. (Refined1C opts ip op fmt i, Show (PP ip i), Show i) => i -> Either Msg1 (Refined1 opts ip op fmt i) Source #
same as prtEval1P
but skips the proxy and allows you to set each parameter individually using type application
prtEval1P :: forall opts ip op fmt i proxy. (Refined1C opts ip op fmt i, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> i -> Either Msg1 (Refined1 opts ip op fmt i) Source #
create a Refined1 using a 5-tuple proxy and aggregate the results on failure
prtEval1IO :: forall opts ip op fmt i. (Refined1C opts ip op fmt i, Show (PP ip i), Show i) => i -> IO (Either String (Refined1 opts ip op fmt i)) Source #
same as prtEval1PIO
but passes in the proxy
prtEval1PIO :: forall opts ip op fmt i proxy. (Refined1C opts ip op fmt i, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> i -> IO (Either String (Refined1 opts ip op fmt i)) Source #
same as prtEval1P
but runs in IO
prt1IO :: forall opts a b r. (OptTC opts, Show a, Show b) => (RResults1 a b, Maybe r) -> IO (Either String r) Source #
An ADT that summarises the results of evaluating Refined1 representing all possible states
evaluation methods
eval1 :: forall opts ip op fmt i. Refined1C opts ip op fmt i => i -> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 opts ip op fmt i)) Source #
same as eval1P
but can pass the parameters individually using type application
eval1P :: forall opts ip op fmt i proxy. Refined1C opts ip op fmt i => proxy '(opts, ip, op, fmt, i) -> i -> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 opts ip op fmt i)) Source #
eval1M :: forall opts ip op fmt i m. (MonadEval m, Refined1C opts ip op fmt i) => i -> m (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 opts ip op fmt i)) Source #
newRefined1 :: forall opts ip op fmt i. (Refined1C opts ip op fmt i, Show (PP ip i), Show i) => i -> Either String (Refined1 opts ip op fmt i) Source #
pure version for extracting Refined1
>>>
newRefined1 @OL @(ParseTimeP TimeOfDay "%-H:%-M:%-S" Id) @'True @(FormatTimeP "%H:%M:%S" Id) "1:15:7"
Right (Refined1 01:15:07)
>>>
newRefined1 @OL @(ParseTimeP TimeOfDay "%-H:%-M:%-S" Id) @'True @(FormatTimeP "%H:%M:%S" Id) "1:2:x"
Left "Step 1. Initial Conversion(ip) Failed | ParseTimeP TimeOfDay (%-H:%-M:%-S) failed to parse"
>>>
newRefined1 @OL @(Rescan "^(\\d{1,2}):(\\d{1,2}):(\\d{1,2})$" Id >> Snd (Head Id) >> Map (ReadP Int Id) Id) @(All (0 <..> 59) Id && Len == 3) @(PrintL 3 "%02d:%02d:%02d" Id) "1:2:3"
Right (Refined1 [1,2,3])
newRefined1P :: forall opts ip op fmt i proxy. (Refined1C opts ip op fmt i, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> i -> Either String (Refined1 opts ip op fmt i) Source #
create a wrapped Refined1 value
newRefined1T :: forall opts ip op fmt i m. (Refined1C opts ip op fmt i, Monad m, Show (PP ip i), Show i) => i -> RefinedT m (Refined1 opts ip op fmt i) Source #
newRefined1TP :: forall opts ip op fmt i proxy m. (Refined1C opts ip op fmt i, Monad m, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> i -> RefinedT m (Refined1 opts ip op fmt i) Source #
create a wrapped Refined1
type
>>>
prtRefinedTIO $ newRefined1TP (Proxy @'( OZ, MkDayExtra Id >> 'Just Id, GuardSimple (Thd Id == 5) >> 'True, UnMkDay (Fst Id), (Int,Int,Int))) (2019,11,1)
Refined1 (2019-11-01,44,5)
>>>
prtRefinedTIO $ newRefined1TP (Proxy @'( OL, MkDayExtra Id >> 'Just Id, Thd Id == 5, UnMkDay (Fst Id), (Int,Int,Int))) (2019,11,2)
failure msg[Step 2. False Boolean Check(op) | {6 == 5}]
>>>
prtRefinedTIO $ newRefined1TP (Proxy @'( OL, MkDayExtra Id >> 'Just Id, Msg "wrong day:" (Thd Id == 5), UnMkDay (Fst Id), (Int,Int,Int))) (2019,11,2)
failure msg[Step 2. False Boolean Check(op) | {wrong day: 6 == 5}]
newRefined1TPIO :: forall opts ip op fmt i proxy m. (Refined1C opts ip op fmt i, MonadIO m, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> i -> RefinedT m (Refined1 opts ip op fmt i) Source #
withRefined1T :: forall opts ip op fmt i m b. (Monad m, Refined1C opts ip op fmt i, Show (PP ip i), Show i) => i -> (Refined1 opts ip op fmt i -> RefinedT m b) -> RefinedT m b Source #
create a Refined1
value using a continuation
This first example reads a hex string and makes sure it is between 100 and 200 and then reads a binary string and adds the values together
>>>
:set -XPolyKinds
>>>
:set -XRankNTypes
>>>
b16 :: forall opts . Proxy '( opts, ReadBase Int 16 Id, Between 100 200 Id, ShowBase 16 Id, String); b16 = Proxy
>>>
b2 :: forall opts . Proxy '( opts, ReadBase Int 2 Id, 'True, ShowBase 2 Id, String); b2 = Proxy
>>>
prtRefinedTIO $ withRefined1TP (b16 @OZ) "a3" $ \x -> withRefined1TP (b2 @OZ) "1001110111" $ \y -> pure (unRefined1 x + unRefined1 y)
794
this example fails as the the hex value is out of range
>>>
prtRefinedTIO $ withRefined1TP (b16 @OAN) "a388" $ \x -> withRefined1TP (b2 @OAN) "1001110111" $ \y -> pure (x,y)
*** Step 1. Success Initial Conversion(ip) (41864) *** P ReadBase(Int,16) 41864 | `- P Id "a388" *** Step 2. False Boolean Check(op) *** False 41864 <= 200 | +- P Id 41864 | +- P '100 | `- P '200 failure msg[Step 2. False Boolean Check(op) | {41864 <= 200}]
withRefined1TIO :: forall opts ip op fmt i m b. (MonadIO m, Refined1C opts ip op fmt i, Show (PP ip i), Show i) => i -> (Refined1 opts ip op fmt i -> RefinedT m b) -> RefinedT m b Source #
withRefined1TP :: forall opts ip op fmt i b proxy m. (Monad m, Refined1C opts ip op fmt i, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> i -> (Refined1 opts ip op fmt i -> RefinedT m b) -> RefinedT m b Source #
proxy methods
mkProxy1 :: 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 withRefined1TP
newRefined1TP
eval1P
prtEval1P
)
use type application to set the 5-tuple or set the individual parameters directly
set the 5-tuple directly
>>>
eg1 = mkProxy1 @'( OL, ReadP Int Id, Gt 10, ShowP Id, String)
>>>
newRefined1P eg1 "24"
Right (Refined1 24)
skip the 5-tuple and set each parameter individually using type application
>>>
eg2 = mkProxy1 @_ @OL @(ReadP Int Id) @(Gt 10) @(ShowP Id)
>>>
newRefined1P eg2 "24"
Right (Refined1 24)
mkProxy1' :: forall z opts ip op fmt i. (z ~ '(opts, ip, op, fmt, i), Refined1C opts ip op fmt i) => Proxy '(opts, ip, op, fmt, i) Source #
type family MakeR1 p where ... Source #
type family for converting from a 5-tuple '(ip,op,fmt,i) to a Refined1
type
unsafe methods for creating Refined1
unsafeRefined1 :: forall opts ip op fmt i. PP ip i -> Refined1 opts ip op fmt i Source #
directly load values into Refined1
without any checking
unsafeRefined1' :: forall opts ip op fmt i. (HasCallStack, Show i, Show (PP ip i), Refined1C opts ip op fmt i) => i -> Refined1 opts ip op fmt i Source #
directly load values into Refined1
. It still checks to see that those values are valid
combine Refined1 values
convertRefined1TP :: forall opts ip op fmt i ip1 op1 fmt1 i1 m. (Refined1C opts ip1 op1 fmt1 i1, Monad m, Show (PP ip i), PP ip i ~ PP ip1 i1, Show i1) => Proxy '(opts, ip, op, fmt, i) -> Proxy '(opts, ip1, op1, fmt1, i1) -> RefinedT m (Refined1 opts ip op fmt i) -> RefinedT m (Refined1 opts ip1 op1 fmt1 i1) Source #
rapply1 :: forall opts ip op fmt i m. (Refined1C opts ip op fmt i, Monad m, Show (PP ip i), Show i) => (PP ip i -> PP ip i -> PP ip i) -> RefinedT m (Refined1 opts ip op fmt i) -> RefinedT m (Refined1 opts ip op fmt i) -> RefinedT m (Refined1 opts ip op fmt i) Source #
applies a binary operation to two wrapped Refined1
parameters
rapply1P :: forall opts ip op fmt i proxy m. (Refined1C opts ip op fmt i, Monad m, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> (PP ip i -> PP ip i -> PP ip i) -> RefinedT m (Refined1 opts ip op fmt i) -> RefinedT m (Refined1 opts ip op fmt i) -> RefinedT m (Refined1 opts ip op fmt i) Source #
same as rapply1
but uses a 5-tuple proxy instead
QuickCheck methods
genRefined1 :: forall opts ip op fmt i. Refined1C opts ip op fmt i => Gen (PP ip i) -> Gen (Refined1 opts ip op fmt i) Source #
create a Refined1
generator
>>>
g = genRefined1 @OU @(ReadP Int Id) @(Between 10 100 Id && Even) @(ShowP Id) (choose (10,100))
>>>
xs <- generate (vectorOf 10 g)
>>>
all (\x -> let y = unRefined1 x in y >= 0 && y <= 100 && even y) xs
True
genRefined1P :: forall opts ip op fmt i. Refined1C opts ip op fmt i => Proxy '(opts, ip, op, fmt, i) -> Gen (PP ip i) -> Gen (Refined1 opts ip op fmt i) Source #
create a Refined1
generator with a Proxy
emulate Refined1 using Refined
eval1PX :: forall opts ip op fmt i proxy. Refined1C opts ip op fmt i => proxy '(opts, ip, op, fmt, i) -> i -> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined opts op (PP ip i), PP fmt (PP ip i))) Source #
similar to eval1P
but it emulates Refined1
but using Refined
takes a 5-tuple proxy as input but outputs the Refined value and the result separately
- initial conversion using 'ip' and stores that in
Refined
- runs the boolean predicate 'op' to make sure to validate the converted value from 1.
- runs 'fmt' against the converted value from 1.
- returns both the
Refined
and the output from 3. - if any of the above steps fail the process stops it and dumps out
RResults1
eval1X :: forall opts ip op fmt i. Refined1C opts ip op fmt i => i -> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined opts op (PP ip i), PP fmt (PP ip i))) Source #
same as eval1PX
but allows you to set the parameters individually using type application
type family ReplaceOptT1 (o :: OptT) t where ... Source #
replace the opts type
ReplaceOptT1 o (Refined1 _ ip op fmt i) = Refined1 o ip op fmt i |
type family AppendOptT1 (o :: OptT) t where ... Source #
change the opts type
AppendOptT1 o (Refined1 o' ip op fmt i) = Refined1 (o' :# o) ip op fmt i |