Safe Haskell | None |
---|---|
Language | Haskell2010 |
Refinement type allowing the external type to differ from the internal type
see Refined2
Synopsis
- data Refined2 ip op i
- type Refined2C ip op i = (P ip i, P op (PP ip i), PP op (PP ip i) ~ Bool)
- prtEval2 :: forall ip op i. (Refined2C ip op i, Show (PP ip i)) => POpts -> i -> Either Msg2 (Refined2 ip op i)
- prtEval2P :: forall ip op i. (Refined2C ip op i, Show (PP ip i)) => Proxy '(ip, op, i) -> POpts -> i -> Either Msg2 (Refined2 ip op i)
- prtEval2PIO :: forall ip op i proxy. (Refined2C ip op i, Show (PP ip i)) => proxy '(ip, op, i) -> POpts -> i -> IO (Either String (Refined2 ip op i))
- prt2IO :: Show a => POpts -> (RResults2 a, Maybe r) -> IO (Either String r)
- prt2 :: Show a => POpts -> (RResults2 a, Maybe r) -> Either Msg2 r
- prt2Impl :: Show a => POpts -> RResults2 a -> Msg2
- data Msg2 = Msg2 {}
- data Results2 a
- data RResults2 a
- eval2 :: forall ip op i. Refined2C ip op i => POpts -> i -> (RResults2 (PP ip i), Maybe (Refined2 ip op i))
- eval2P :: forall ip op i. Refined2C ip op i => Proxy '(ip, op, i) -> POpts -> i -> (RResults2 (PP ip i), Maybe (Refined2 ip op i))
- newRefined2T :: forall m ip op i. (Refined2C ip op i, Monad m, Show (PP ip i)) => POpts -> i -> RefinedT m (Refined2 ip op i)
- newRefined2TP :: forall m ip op i proxy. (Refined2C ip op i, Monad m, Show (PP ip i)) => proxy '(ip, op, i) -> POpts -> i -> RefinedT m (Refined2 ip op i)
- newRefined2TIO :: forall m ip op i. (Refined2C ip op i, MonadIO m, Show (PP ip i)) => POpts -> i -> RefinedT m (Refined2 ip op i)
- withRefined2T :: forall ip op i m b. (Monad m, Refined2C ip op i, Show (PP ip i)) => POpts -> i -> (Refined2 ip op i -> RefinedT m b) -> RefinedT m b
- withRefined2TP :: forall m ip op i b proxy. (Monad m, Refined2C ip op i, Show (PP ip i), Show i) => proxy '(ip, op, i) -> POpts -> i -> (Refined2 ip op i -> RefinedT m b) -> RefinedT m b
- withRefined2TIO :: forall ip op i m b. (MonadIO m, Refined2C ip op i, Show (PP ip i)) => POpts -> i -> (Refined2 ip op i -> RefinedT m b) -> RefinedT m b
- type family MakeR2 p where ...
- mkProxy2 :: forall z ip op i. z ~ '(ip, op, i) => Proxy '(ip, op, i)
- mkProxy2' :: forall z ip op i. (z ~ '(ip, op, i), Refined2C ip op i) => Proxy '(ip, op, i)
- unsafeRefined2 :: forall ip op i. PP ip i -> i -> Refined2 ip op i
- unsafeRefined2' :: forall ip op i. (Show (PP ip i), Refined2C ip op i) => POpts -> i -> Refined2 ip op i
- type family T3_1 x where ...
- type family T3_2 x where ...
- type family T3_3 x where ...
Refined2
data Refined2 ip op i Source #
Refinement type that allows the input and output types to vary.
i
is the input type which is stored inr2Out
ip
convertsi
toPP ip i
which is the internal type inr2In
op
validates that internal type usingPP op (PP ip i) ~ Bool
Although a common scenario is String as input, you are free to choose any input type you like
>>>
prtEval2 @(ReadBase Int 16 Id) @(Lt 255) oz "00fe"
Right (Refined2 {r2In = 254, r2Out = "00fe"})
>>>
prtEval2 @(ReadBase Int 16 Id) @(Lt 253) oz "00fe"
Left Step 2. False Boolean Check(op) | FalseP
>>>
prtEval2 @(ReadBase Int 16 Id) @(Lt 255) oz "00fg"
Left Step 1. Initial Conversion(ip) Failed | invalid base 16
>>>
prtEval2 @(Map (ReadP Int Id) (Resplit "\\." Id)) @(Msg "length invalid:" (Len == 4)) ol "198.162.3.1.5"
Left Step 2. False Boolean Check(op) | {length invalid:5 == 4}
>>>
prtEval2 @(Map (ReadP Int Id) (Resplit "\\." Id)) @(Guard (PrintF "found length=%d" Len) (Len == 4) >> 'True) oz "198.162.3.1.5"
Left Step 2. Failed Boolean Check(op) | found length=5
>>>
prtEval2 @(Map (ReadP Int Id) (Resplit "\\." Id)) @(Guard (PrintF "found length=%d" Len) (Len == 4) >> 'True) oz "198.162.3.1"
Right (Refined2 {r2In = [198,162,3,1], r2Out = "198.162.3.1"})
>>>
:m + Data.Time.Calendar.WeekDate
>>>
prtEval2 @(MkDay >> 'Just Id) @(Guard "expected a Sunday" (Thd Id == 7) >> 'True) oz (2019,10,13)
Right (Refined2 {r2In = (2019-10-13,41,7), r2Out = (2019,10,13)})
>>>
prtEval2 @(MkDay >> 'Just Id) @(Msg "expected a Sunday:" (Thd Id == 7)) ol (2019,10,12)
Left Step 2. False Boolean Check(op) | {expected a Sunday:6 == 7}
>>>
prtEval2 @(MkDay' (Fst Id) (Snd Id) (Thd Id) >> 'Just Id) @(Guard "expected a Sunday" (Thd Id == 7) >> 'True) oz (2019,10,12)
Left Step 2. Failed Boolean Check(op) | expected a Sunday
Instances
(Eq i, Eq (PP ip i)) => Eq (Refined2 ip op i) Source # | |
(Eq i, Show i, Show (PP ip i), Refined2C ip op i, Read (PP ip i), Read i) => Read (Refined2 ip op i) Source # |
|
(Show i, Show (PP ip i)) => Show (Refined2 ip op i) Source # | |
(Refined2C ip op String, Show (PP ip String)) => IsString (Refined2 ip op String) Source # | |
Defined in Predicate.Refined2 fromString :: String -> Refined2 ip op String # | |
(Lift (PP ip i), Lift i) => Lift (Refined2 ip op i) Source # | |
ToJSON i => ToJSON (Refined2 ip op i) Source # |
|
Defined in Predicate.Refined2 | |
(Show i, Show (PP ip i), Refined2C ip op i, FromJSON i) => FromJSON (Refined2 ip op i) Source # |
|
(Show i, Show (PP ip i), Refined2C ip op i, Binary i) => Binary (Refined2 ip op i) Source # |
|
type Refined2C ip op i = (P ip i, P op (PP ip i), PP op (PP ip i) ~ Bool) Source #
Provides the constraints on Refined2
display results
prtEval2 :: forall ip op i. (Refined2C ip op i, Show (PP ip i)) => POpts -> i -> Either Msg2 (Refined2 ip op i) Source #
prtEval2P :: forall ip op i. (Refined2C ip op i, Show (PP ip i)) => Proxy '(ip, op, i) -> POpts -> i -> Either Msg2 (Refined2 ip op i) Source #
prtEval2PIO :: forall ip op i proxy. (Refined2C ip op i, Show (PP ip i)) => proxy '(ip, op, i) -> POpts -> i -> IO (Either String (Refined2 ip op i)) Source #
same as prtEval2P
but runs in IO
An ADT that summarises the results of evaluating Refined2 representing all possible states
evaluation methods
eval2 :: forall ip op i. Refined2C ip op i => POpts -> i -> (RResults2 (PP ip i), Maybe (Refined2 ip op i)) Source #
eval2P :: forall ip op i. Refined2C ip op i => Proxy '(ip, op, i) -> POpts -> i -> (RResults2 (PP ip i), Maybe (Refined2 ip op i)) Source #
create a wrapped Refined2 value
newRefined2T :: forall m ip op i. (Refined2C ip op i, Monad m, Show (PP ip i)) => POpts -> i -> RefinedT m (Refined2 ip op i) Source #
create a wrapped Refined2
type
>>>
prtRefinedTIO $ newRefined2T @_ @(MkDay >> Just Id) @(Thd Id == 5) ol (2019,11,1)
Refined2 {r2In = (2019-11-01,44,5), r2Out = (2019,11,1)}
>>>
prtRefinedTIO $ newRefined2T @_ @(MkDay >> Just Id) @(Thd Id == 5) ol (2019,11,2)
failure msg[Step 2. False Boolean Check(op) | {6 == 5}]
>>>
prtRefinedTIO $ newRefined2T @_ @(MkDay >> Just Id) @(Msg "wrong day:" (Thd Id == 5)) ol (2019,11,2)
failure msg[Step 2. False Boolean Check(op) | {wrong day:6 == 5}]
newRefined2TP :: forall m ip op i proxy. (Refined2C ip op i, Monad m, Show (PP ip i)) => proxy '(ip, op, i) -> POpts -> i -> RefinedT m (Refined2 ip op i) Source #
newRefined2TIO :: forall m ip op i. (Refined2C ip op i, MonadIO m, Show (PP ip i)) => POpts -> i -> RefinedT m (Refined2 ip op i) Source #
withRefined2T :: forall ip op i m b. (Monad m, Refined2C ip op i, Show (PP ip i)) => POpts -> i -> (Refined2 ip op i -> RefinedT m b) -> RefinedT m b Source #
create a Refined2
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
>>>
prtRefinedTIO $ withRefined2T @(ReadBase Int 16 Id) @(Between 100 200 Id) oz "a3" $ \x -> withRefined2T @(ReadBase Int 2 Id) @'True oz "1001110111" $ \y -> pure (r2In x + r2In y)
794
this example fails as the the hex value is out of range
>>>
prtRefinedTIO $ withRefined2T @(ReadBase Int 16 Id) @(Between 100 200 Id) o0 "a388" $ \x -> withRefined2T @(ReadBase Int 2 Id) @'True 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}]
withRefined2TP :: forall m ip op i b proxy. (Monad m, Refined2C ip op i, Show (PP ip i), Show i) => proxy '(ip, op, i) -> POpts -> i -> (Refined2 ip op i -> RefinedT m b) -> RefinedT m b Source #
withRefined2TIO :: forall ip op i m b. (MonadIO m, Refined2C ip op i, Show (PP ip i)) => POpts -> i -> (Refined2 ip op i -> RefinedT m b) -> RefinedT m b Source #
proxy methods
type family MakeR2 p where ... Source #
type family for converting from a 3-tuple '(ip,op,i) to a Refined2
type
mkProxy2 :: forall z ip op i. z ~ '(ip, op, i) => Proxy '(ip, op, i) Source #
creates a 3-tuple proxy (see withRefined2TP
newRefined2TP
eval2P
prtEval2P
)
use type application to set the 4-tuple or set the individual parameters directly
set the 3-tuple directly
>>>
eg1 = mkProxy2 @'(ReadP Int Id, Gt 10, String)
>>>
prtEval2P eg1 ol "24"
Right (Refined2 {r2In = 24, r2Out = "24"})
skip the 4-tuple and set each parameter individually using type application
>>>
eg2 = mkProxy2 @_ @(ReadP Int Id) @(Gt 10)
>>>
prtEval2P eg2 ol "24"
Right (Refined2 {r2In = 24, r2Out = "24"})
unsafe methods for creating Refined2
unsafeRefined2 :: forall ip op i. PP ip i -> i -> Refined2 ip op i Source #
directly load values into Refined2
without any checking
unsafeRefined2' :: forall ip op i. (Show (PP ip i), Refined2C ip op i) => POpts -> i -> Refined2 ip op i Source #
directly load values into Refined2
. It still checks to see that those values are valid
extract from 3-tuple
type family T3_1 x where ... Source #
used by Refined2
to extract 'ip' from a promoted 3-tuple
T3_1 '(a, b, c) = a |