Safe Haskell | None |
---|---|
Language | Haskell2010 |
Refinement type allowing the external type to differ from the internal type
see Refined3
Synopsis
- data Refined3 ip op fmt i
- type Refined3C ip op fmt i = (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)
- prtEval3P :: forall ip op fmt i proxy. (Refined3C ip op fmt i, Show (PP ip i), Show i) => proxy '(ip, op, fmt, i) -> POpts -> i -> Either Msg3 (Refined3 ip op fmt i)
- prtEval3PIO :: forall ip op fmt i proxy. (Refined3C ip op fmt i, Show (PP ip i), Show i) => proxy '(ip, op, fmt, i) -> POpts -> i -> IO (Either String (Refined3 ip op fmt i))
- prtEval3 :: forall ip op fmt i. (Refined3C ip op fmt i, Show (PP ip i), Show i) => POpts -> i -> Either Msg3 (Refined3 ip op fmt i)
- prt3IO :: (Show a, Show b) => POpts -> (RResults a b, Maybe r) -> IO (Either String r)
- prt3 :: (Show a, Show b) => POpts -> (RResults a b, Maybe r) -> Either Msg3 r
- prt3Impl :: (Show a, Show b) => POpts -> RResults a b -> Msg3
- data Msg3 = Msg3 {}
- data Results a b
- data RResults a b
- mkProxy3 :: forall z ip op fmt i. z ~ '(ip, op, fmt, i) => Proxy '(ip, op, fmt, i)
- mkProxy3' :: forall z ip op fmt i. (z ~ '(ip, op, fmt, i), Refined3C ip op fmt i) => Proxy '(ip, op, fmt, i)
- type family MakeR3 p where ...
- eval3P :: forall ip op fmt i proxy. Refined3C ip op fmt i => proxy '(ip, op, fmt, i) -> POpts -> i -> (RResults (PP ip i) (PP fmt (PP ip i)), Maybe (Refined3 ip op fmt i))
- eval3 :: forall ip op fmt i. Refined3C ip op fmt i => POpts -> i -> (RResults (PP ip i) (PP fmt (PP ip i)), Maybe (Refined3 ip op fmt i))
- withRefined3TIO :: forall ip op fmt i m b. (MonadIO m, Refined3C ip op fmt i, Show (PP ip i), Show i) => POpts -> i -> (Refined3 ip op fmt i -> RefinedT m b) -> RefinedT m b
- withRefined3T :: forall ip op fmt i m b. (Monad m, Refined3C ip op fmt i, Show (PP ip i), Show i) => POpts -> i -> (Refined3 ip op fmt i -> RefinedT m b) -> RefinedT m b
- withRefined3TP :: forall m ip op fmt i b proxy. (Monad m, Refined3C ip op fmt i, Show (PP ip i), Show i) => proxy '(ip, op, fmt, i) -> POpts -> i -> (Refined3 ip op fmt i -> RefinedT m b) -> RefinedT m b
- newRefined3T :: forall m ip op fmt i. (Refined3C ip op fmt i, Monad m, Show (PP ip i), Show i) => POpts -> i -> RefinedT m (Refined3 ip op fmt i)
- newRefined3TP :: forall m ip op fmt i proxy. (Refined3C ip op fmt i, Monad m, Show (PP ip i), Show i) => proxy '(ip, op, fmt, i) -> POpts -> i -> RefinedT m (Refined3 ip op fmt i)
- newRefined3TPIO :: forall m ip op fmt i proxy. (Refined3C ip op fmt i, MonadIO m, Show (PP ip i), Show i) => proxy '(ip, op, fmt, i) -> POpts -> i -> RefinedT m (Refined3 ip op fmt i)
- convertRefined3TP :: forall m ip op fmt i ip1 op1 fmt1 i1. (Refined3C ip1 op1 fmt1 i1, Monad m, Show (PP ip i), PP ip i ~ PP ip1 i1, Show i1) => Proxy '(ip, op, fmt, i) -> Proxy '(ip1, op1, fmt1, i1) -> POpts -> RefinedT m (Refined3 ip op fmt i) -> RefinedT m (Refined3 ip1 op1 fmt1 i1)
- rapply3 :: forall m ip op fmt i. (Refined3C ip op fmt i, Monad m, Show (PP ip i), Show i) => POpts -> (PP ip i -> PP ip i -> PP ip i) -> RefinedT m (Refined3 ip op fmt i) -> RefinedT m (Refined3 ip op fmt i) -> RefinedT m (Refined3 ip op fmt i)
- rapply3P :: forall m ip op fmt i proxy. (Refined3C ip op fmt i, Monad m, Show (PP ip i), Show i) => proxy '(ip, op, fmt, i) -> POpts -> (PP ip i -> PP ip i -> PP ip i) -> RefinedT m (Refined3 ip op fmt i) -> RefinedT m (Refined3 ip op fmt i) -> RefinedT m (Refined3 ip op fmt i)
- arbRefined3 :: forall ip op fmt i. (Arbitrary (PP ip i), Refined3C ip op fmt i) => Proxy '(ip, op, fmt, i) -> Gen (Refined3 ip op fmt i)
- arbRefined3With :: forall ip op fmt i. (Arbitrary (PP ip i), Refined3C ip op fmt i) => Proxy '(ip, op, fmt, i) -> (PP ip i -> PP ip i) -> Gen (Refined3 ip op fmt i)
- unsafeRefined3 :: forall ip op fmt i. PP ip i -> PP fmt (PP ip i) -> Refined3 ip op fmt i
- unsafeRefined3' :: forall ip op fmt i. (Show i, Show (PP ip i), Refined3C ip op fmt i) => POpts -> i -> Refined3 ip op fmt i
- type RefinedEmulate p a = Refined3 Id p Id a
- eval3PX :: forall ip op fmt i proxy. Refined3C ip op fmt i => proxy '(ip, op, fmt, i) -> POpts -> i -> (RResults (PP ip i) (PP fmt (PP ip i)), Maybe (Refined op (PP ip i), PP fmt (PP ip i)))
- eval3X :: forall ip op fmt i. Refined3C ip op fmt i => POpts -> i -> (RResults (PP ip i) (PP fmt (PP ip i)), Maybe (Refined op (PP ip i), PP fmt (PP ip i)))
Refined3
data Refined3 ip op fmt i Source #
Refinement type that differentiates the input from output
- i is the input type
- ip converts
i
toPP ip i
which is the internal type - op validates that internal type using
PP op (PP ip i) ~ Bool
- fmt outputs the internal type
PP fmt (PP ip i) ~ i
- PP fmt (PP ip i) should be valid as input for Refined3
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
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
>>>
prtEval3 @(ReadBase Int 16 Id) @(Lt 255) @(PrintF "%x" Id) oz "00fe"
Right (Refined3 {r3In = 254, r3Out = "fe"})
>>>
prtEval3 @(ReadBase Int 16 Id) @(Lt 253) @(PrintF "%x" Id) oz "00fe"
Left Step 2. False Boolean Check(op) | FalseP
>>>
prtEval3 @(ReadBase Int 16 Id) @(Lt 255) @(PrintF "%x" Id) oz "00fg"
Left Step 1. Initial Conversion(ip) Failed | invalid base 16
>>>
prtEval3 @(Map (ReadP Int Id) (Resplit "\\." Id)) @(Msg "length invalid:" (Len == 4)) @(PrintL 4 "%03d.%03d.%03d.%03d" Id) ol "198.162.3.1.5"
Left Step 2. False Boolean Check(op) | {length invalid:5 == 4}
>>>
prtEval3 @(Map (ReadP Int Id) (Resplit "\\." Id)) @(Guard (PrintF "found length=%d" Len) (Len == 4) >> 'True) @(PrintL 4 "%03d.%03d.%03d.%03d" Id) oz "198.162.3.1.5"
Left Step 2. Failed Boolean Check(op) | found length=5
>>>
prtEval3 @(Map (ReadP Int Id) (Resplit "\\." Id)) @(Guard (PrintF "found length=%d" Len) (Len == 4) >> 'True) @(PrintL 4 "%03d.%03d.%03d.%03d" Id) oz "198.162.3.1"
Right (Refined3 {r3In = [198,162,3,1], r3Out = "198.162.003.001"})
>>>
:m + Data.Time.Calendar.WeekDate
>>>
prtEval3 @(MkDay >> 'Just Id) @(Guard "expected a Sunday" (Thd Id == 7) >> 'True) @(UnMkDay (Fst Id)) oz (2019,10,13)
Right (Refined3 {r3In = (2019-10-13,41,7), r3Out = (2019,10,13)})
>>>
prtEval3 @(MkDay >> 'Just Id) @(Msg "expected a Sunday:" (Thd Id == 7)) @(UnMkDay (Fst Id)) ol (2019,10,12)
Left Step 2. False Boolean Check(op) | {expected a Sunday:6 == 7}
>>>
prtEval3 @(MkDay' (Fst Id) (Snd Id) (Thd Id) >> 'Just Id) @(Guard "expected a Sunday" (Thd Id == 7) >> 'True) @(UnMkDay (Fst Id)) oz (2019,10,12)
Left Step 2. Failed Boolean Check(op) | expected a Sunday
>>>
type T4 k = '(MkDay >> 'Just Id, Guard "expected a Sunday" (Thd Id == 7) >> 'True, UnMkDay (Fst Id), k)
>>>
prtEval3P (Proxy @(T4 _)) oz (2019,10,12)
Left Step 2. Failed Boolean Check(op) | expected a Sunday
>>>
prtEval3P (Proxy @(T4 _)) oz (2019,10,13)
Right (Refined3 {r3In = (2019-10-13,41,7), r3Out = (2019,10,13)})
Instances
(Eq i, Eq (PP ip i), Eq (PP fmt (PP ip i))) => Eq (Refined3 ip op fmt i) Source # | |
(Eq i, Show i, Show (PP ip i), Refined3C ip op fmt i, Read (PP ip i), Read (PP fmt (PP ip i))) => Read (Refined3 ip op fmt i) Source # |
|
(Show i, Show (PP ip i), Show (PP fmt (PP ip i))) => Show (Refined3 ip op fmt i) Source # | |
(Lift (PP ip i), Lift (PP fmt (PP ip i))) => Lift (Refined3 ip op fmt i) Source # | |
ToJSON (PP fmt (PP ip i)) => ToJSON (Refined3 ip op fmt i) Source # |
|
Defined in Predicate.Refined3 | |
(Show (PP fmt (PP ip i)), Show (PP ip i), Refined3C ip op fmt i, FromJSON i) => FromJSON (Refined3 ip op fmt i) Source # |
|
(Show (PP fmt (PP ip i)), Show (PP ip i), Refined3C ip op fmt i, Binary i) => Binary (Refined3 ip op fmt i) Source # |
|
type Refined3C ip op fmt i = (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
prtEval3P :: forall ip op fmt i proxy. (Refined3C ip op fmt i, Show (PP ip i), Show i) => proxy '(ip, op, fmt, i) -> POpts -> i -> Either Msg3 (Refined3 ip op fmt i) Source #
create a Refined3 using a 4-tuple proxy and aggregate the results on failure
prtEval3PIO :: forall ip op fmt i proxy. (Refined3C ip op fmt i, Show (PP ip i), Show i) => proxy '(ip, op, fmt, i) -> POpts -> i -> IO (Either String (Refined3 ip op fmt i)) Source #
same as prtEval3P
but runs in IO
prtEval3 :: forall ip op fmt i. (Refined3C ip op fmt i, Show (PP ip i), Show i) => POpts -> i -> Either Msg3 (Refined3 ip op fmt i) Source #
same as prtEval3P
but skips the proxy and allows you to set each parameter individually using type application
An ADT that summarises the results of evaluating Refined3 representing all possible states
proxy methods
mkProxy3 :: forall z ip op fmt i. z ~ '(ip, op, fmt, i) => Proxy '(ip, op, fmt, i) Source #
creates a 4-tuple proxy (see withRefined3TP
newRefined3TP
eval3P
prtEval3P
)
use type application to set the 4-tuple or skip that and set the individual parameters directly
set the 4-tuple directly
>>>
eg1 = mkProxy3 @'(ReadP Int Id, Gt 10, ShowP Id, String)
>>>
prtEval3P eg1 ol "24"
Right (Refined3 {r3In = 24, r3Out = "24"})
skip the 4-tuple and set each parameter individually using type application
>>>
eg2 = mkProxy3 @_ @(ReadP Int Id) @(Gt 10) @(ShowP Id)
>>>
prtEval3P eg2 ol "24"
Right (Refined3 {r3In = 24, r3Out = "24"})
mkProxy3' :: forall z ip op fmt i. (z ~ '(ip, op, fmt, i), Refined3C ip op fmt i) => Proxy '(ip, op, fmt, i) Source #
type family MakeR3 p where ... Source #
convenience type family for converting from a 4-tuple '(ip,op,fmt,i) to a Refined3
signature
evaluation methods
eval3P :: forall ip op fmt i proxy. Refined3C ip op fmt i => proxy '(ip, op, fmt, i) -> POpts -> i -> (RResults (PP ip i) (PP fmt (PP ip i)), Maybe (Refined3 ip op fmt i)) Source #
eval3 :: forall ip op fmt i. Refined3C ip op fmt i => POpts -> i -> (RResults (PP ip i) (PP fmt (PP ip i)), Maybe (Refined3 ip op fmt i)) Source #
same as eval3P
but can pass the parameters individually using type application
create a wrapped Refined3 value
withRefined3TIO :: forall ip op fmt i m b. (MonadIO m, Refined3C ip op fmt i, Show (PP ip i), Show i) => POpts -> i -> (Refined3 ip op fmt i -> RefinedT m b) -> RefinedT m b Source #
withRefined3T :: forall ip op fmt i m b. (Monad m, Refined3C ip op fmt i, Show (PP ip i), Show i) => POpts -> i -> (Refined3 ip op fmt i -> RefinedT m b) -> RefinedT m b Source #
create a Refined3
value and pass it to a continuation to be processed
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
>>>
b16 = Proxy @'(ReadBase Int 16 Id, Between 100 200, ShowBase 16 Id, String)
>>>
b2 = Proxy @'(ReadBase Int 2 Id, 'True, ShowBase 2 Id, String)
>>>
prtRefinedTIO $ withRefined3TP b16 oz "a3" $ \x -> withRefined3TP b2 oz "1001110111" $ \y -> pure (r3In x + r3In y)
794
this example fails as the the hex value is out of range
>>>
prtRefinedTIO $ withRefined3TP b16 o0 "a388" $ \x -> withRefined3TP b2 o0 "1001110111" $ \y -> pure (x,y)
*** Step 1. Success Initial Conversion(ip) [41864] *** P ReadBase(Int,16) 41864 | "a388" | `- 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}]
withRefined3TP :: forall m ip op fmt i b proxy. (Monad m, Refined3C ip op fmt i, Show (PP ip i), Show i) => proxy '(ip, op, fmt, i) -> POpts -> i -> (Refined3 ip op fmt i -> RefinedT m b) -> RefinedT m b Source #
newRefined3T :: forall m ip op fmt i. (Refined3C ip op fmt i, Monad m, Show (PP ip i), Show i) => POpts -> i -> RefinedT m (Refined3 ip op fmt i) Source #
newRefined3TP :: forall m ip op fmt i proxy. (Refined3C ip op fmt i, Monad m, Show (PP ip i), Show i) => proxy '(ip, op, fmt, i) -> POpts -> i -> RefinedT m (Refined3 ip op fmt i) Source #
create a wrapped Refined3
type
>>>
prtRefinedTIO $ newRefined3TP (Proxy @'(MkDay >> Just Id, GuardSimple (Thd Id == 5) >> 'True, UnMkDay (Fst Id), (Int,Int,Int))) oz (2019,11,1)
Refined3 {r3In = (2019-11-01,44,5), r3Out = (2019,11,1)}
>>>
prtRefinedTIO $ newRefined3TP (Proxy @'(MkDay >> Just Id, Thd Id == 5, UnMkDay (Fst Id), (Int,Int,Int))) ol (2019,11,2)
failure msg[Step 2. False Boolean Check(op) | {6 == 5}]
>>>
prtRefinedTIO $ newRefined3TP (Proxy @'(MkDay >> Just Id, Msg "wrong day:" (Thd Id == 5), UnMkDay (Fst Id), (Int,Int,Int))) ol (2019,11,2)
failure msg[Step 2. False Boolean Check(op) | {wrong day:6 == 5}]
newRefined3TPIO :: forall m ip op fmt i proxy. (Refined3C ip op fmt i, MonadIO m, Show (PP ip i), Show i) => proxy '(ip, op, fmt, i) -> POpts -> i -> RefinedT m (Refined3 ip op fmt i) Source #
convertRefined3TP :: forall m ip op fmt i ip1 op1 fmt1 i1. (Refined3C ip1 op1 fmt1 i1, Monad m, Show (PP ip i), PP ip i ~ PP ip1 i1, Show i1) => Proxy '(ip, op, fmt, i) -> Proxy '(ip1, op1, fmt1, i1) -> POpts -> RefinedT m (Refined3 ip op fmt i) -> RefinedT m (Refined3 ip1 op1 fmt1 i1) Source #
rapply3 :: forall m ip op fmt i. (Refined3C ip op fmt i, Monad m, Show (PP ip i), Show i) => POpts -> (PP ip i -> PP ip i -> PP ip i) -> RefinedT m (Refined3 ip op fmt i) -> RefinedT m (Refined3 ip op fmt i) -> RefinedT m (Refined3 ip op fmt i) Source #
applies a binary operation to two wrapped Refined3
parameters
rapply3P :: forall m ip op fmt i proxy. (Refined3C ip op fmt i, Monad m, Show (PP ip i), Show i) => proxy '(ip, op, fmt, i) -> POpts -> (PP ip i -> PP ip i -> PP ip i) -> RefinedT m (Refined3 ip op fmt i) -> RefinedT m (Refined3 ip op fmt i) -> RefinedT m (Refined3 ip op fmt i) Source #
same as rapply3
but uses a 4-tuple proxy instead
QuickCheck methods
arbRefined3 :: forall ip op fmt i. (Arbitrary (PP ip i), Refined3C ip op fmt i) => Proxy '(ip, op, fmt, i) -> Gen (Refined3 ip op fmt i) Source #
arbRefined3With :: forall ip op fmt i. (Arbitrary (PP ip i), Refined3C ip op fmt i) => Proxy '(ip, op, fmt, i) -> (PP ip i -> PP ip i) -> Gen (Refined3 ip op fmt i) Source #
unsafe methods for creating Refined3
unsafeRefined3 :: forall ip op fmt i. PP ip i -> PP fmt (PP ip i) -> Refined3 ip op fmt i Source #
directly load values into Refined3
without any checking
unsafeRefined3' :: forall ip op fmt i. (Show i, Show (PP ip i), Refined3C ip op fmt i) => POpts -> i -> Refined3 ip op fmt i Source #
directly load values into Refined3
. It still checks to see that those values are valid
emulate Refined3 using Refined
eval3PX :: forall ip op fmt i proxy. Refined3C ip op fmt i => proxy '(ip, op, fmt, i) -> POpts -> i -> (RResults (PP ip i) (PP fmt (PP ip i)), Maybe (Refined op (PP ip i), PP fmt (PP ip i))) Source #
similar to eval3P
but it emulates Refined3
but using Refined
takes a 4-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
RResults