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}
>>>
:m + Data.Ratio
>>>
newRefined2 @OZ @(ReadP Rational Id) @'True "13 % 3"
Right (Refined2 (13 % 3) "13 % 3")
>>>
newRefined2 @OZ @(ReadP Rational Id) @'True "13x % 3"
Left Step 1. Failed Initial Conversion(ip) | ReadP Ratio Integer (13x % 3)
>>>
newRefined2 @OZ @(ReadP Rational Id) @(3 % 1 <..> 5 % 1) "13 % 3"
Right (Refined2 (13 % 3) "13 % 3")
>>>
newRefined2 @OZ @(ReadP Rational Id) @(11 -% 2 <..> 3 -% 1) "-13 % 3"
Right (Refined2 ((-13) % 3) "-13 % 3")
>>>
newRefined2 @OZ @(ReadP Rational Id) @(Id > (15 % 1)) "13 % 3"
Left Step 2. False Boolean Check(op) | FalseP
>>>
newRefined2 @OL @(ReadP Rational Id) @(Msg (PrintF "invalid=%3.2f" (FromRational Double)) (Id > (15 % 1))) "13 % 3"
Left Step 2. False Boolean Check(op) | {invalid=4.33 13 % 3 > 15 % 1}
>>>
newRefined2 @OZ @(ReadP Rational Id) @(Id > (11 % 1)) "13 % 3"
Left Step 2. False Boolean Check(op) | FalseP
>>>
newRefined2 @OZ @(ReadP UTCTime Id) @'True "2018-10-19 14:53:11.5121359 UTC"
Right (Refined2 2018-10-19 14:53:11.5121359 UTC "2018-10-19 14:53:11.5121359 UTC")
>>>
:m + Data.Aeson
>>>
newRefined2 @OZ @(ReadP Value Id) @'True "String \"jsonstring\""
Right (Refined2 (String "jsonstring") "String \"jsonstring\"")
>>>
newRefined2 @OZ @(ReadP Value Id) @'True "Number 123.4"
Right (Refined2 (Number 123.4) "Number 123.4")
>>>
:m + Text.Show.Functions
>>>
newRefined2 @OU @(Id $$ 13) @(Id > 100) (\x -> x * 14) ^? _Right . to r2Out
Just <function>
>>>
newRefined2 @OU @(Id $$ 13) @(Id > 100) (\x -> x * 14) ^? _Right . to r2In
Just 182
>>>
newRefined2 @OU @(Id $$ 13) @(Id > 100) (\x -> x * 14) ^? _Right . to (($ 13) . r2Out)
Just 182
>>>
newRefined2 @OZ @(Pop0 Fst Id) @(Len > 1) (Proxy @Snd,"Abcdef") ^? _Right . to r2In
Just "Abcdef"
>>>
newRefined2 @OZ @(Pop0 Fst Id >> Len) @(Id > 1) (Proxy @Snd,"Abcdef") ^? _Right . to r2In
Just 6
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.5-JjMXzrXEzX77YMQbrq7lii" 'True) (C1 ('MetaCons "Refined2Exception" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) |