Predicate.Refined2

Refinement type allowing the external type to differ from the internal type see Refined2

Refined2

data Refined2 (opts :: OptT) ip op i

Refinement type for specifying an input type that is different from the output type

• opts are the display options
• ip converts i to PP ip i which is the internal type in r2In
• op validates that internal type using PP op (PP ip i) ~ Bool
• i is the input type which is stored in r2Out

Although a common scenario is String as input, you are free to choose any input type you like

>>> newRefined2 @'OZ @(ReadBase Int 16 Id) @(Lt 255) "00fe"
Right (Refined2 {r2In = 254, r2Out = "00fe"})

>>> newRefined2 @'OZ @(ReadBase Int 16 Id) @(Lt 253) "00fe"
Left "Step 2. False Boolean Check(op) | FalseP"

>>> newRefined2 @'OZ @(ReadBase Int 16 Id) @(Lt 255) "00fg"
Left "Step 1. Initial Conversion(ip) Failed | invalid base 16"

>>> newRefined2 @'OL @(Map (ReadP Int Id) (Resplit "\\." Id)) @(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 "\\." Id)) @(Guard (PrintF "found length=%d" Len) (Len == 4) >> 'True) "198.162.3.1.5"
Left "Step 2. Failed Boolean Check(op) | found length=5"

>>> newRefined2 @'OZ @(Map (ReadP Int Id) (Resplit "\\." Id)) @(Guard (PrintF "found length=%d" Len) (Len == 4) >> 'True) "198.162.3.1"
Right (Refined2 {r2In = [198,162,3,1], r2Out = "198.162.3.1"})

>>> :m + Data.Time.Calendar.WeekDate
>>> newRefined2 @'OZ @(MkDayExtra Id >> 'Just Id) @(Guard "expected a Sunday" (Thd Id == 7) >> 'True) (2019,10,13)
Right (Refined2 {r2In = (2019-10-13,41,7), r2Out = (2019,10,13)})

>>> newRefined2 @'OL @(MkDayExtra Id >> 'Just Id) @(Msg "expected a Sunday:" (Thd Id == 7)) (2019,10,12)
Left "Step 2. False Boolean Check(op) | {expected a Sunday:6 == 7}"

>>> newRefined2 @'OZ @(MkDayExtra' (Fst Id) (Snd Id) (Thd Id) >> 'Just Id) @(Guard "expected a Sunday" (Thd Id == 7) >> 'True) (2019,10,12)
Left "Step 2. Failed Boolean Check(op) | expected a Sunday"

Instances

(Eq i, Eq (PP ip i)) => Eq (Refined2 opts ip op i)

Defined in Predicate.Refined2

Methods

(==) :: Refined2 opts ip op i -> Refined2 opts ip op i -> Bool

(/=) :: Refined2 opts ip op i -> Refined2 opts ip op i -> Bool

(Eq i, Show i, Show (PP ip i), Refined2C opts ip op i, Read (PP ip i), Read i) => Read (Refined2 opts ip op i)

Read instance for Refined2

>>> reads @(Refined2 'OZ (ReadBase Int 16 Id) (Between 0 255 Id) String) "Refined2 {r2In = 254, r2Out = \"fe\"}"
[(Refined2 {r2In = 254, r2Out = "fe"},"")]

>>> reads @(Refined2 'OZ (ReadBase Int 16 Id) (Between 0 255 Id) String) "Refined2 {r2In = 300, r2Out = \"12c\"}"
[]

>>> reads @(Refined2 'OZ (ReadBase Int 16 Id) (Id < 0) String) "Refined2 {r2In = -1234, r2Out = \"-4d2\"}"
[(Refined2 {r2In = -1234, r2Out = "-4d2"},"")]

>>> reads @(Refined2 'OZ (Map (ReadP Int Id) (Resplit "\\." Id)) (Guard "len/=4" (Len == 4) >> 'True) String) "Refined2 {r2In = [192,168,0,1], r2Out = \"192.168.0.1\"}"
[(Refined2 {r2In = [192,168,0,1], r2Out = "192.168.0.1"},"")]

Defined in Predicate.Refined2

Methods

readsPrec :: Int -> ReadS (Refined2 opts ip op i)

readList :: ReadS [Refined2 opts ip op i]

readPrec :: ReadPrec (Refined2 opts ip op i)

readListPrec :: ReadPrec [Refined2 opts ip op i]

(Show i, Show (PP ip i)) => Show (Refined2 opts ip op i)

Defined in Predicate.Refined2

Methods

showsPrec :: Int -> Refined2 opts ip op i -> ShowS

show :: Refined2 opts ip op i -> String

showList :: [Refined2 opts ip op i] -> ShowS

(s ~ String, Refined2C opts ip op s, Show (PP ip s)) => IsString (Refined2 opts ip op s)

IsString instance for Refined2

>>> pureTryTest $ fromString @(Refined2 'OL (ReadP Int Id) (Id > 12) String) "523"
Right (Refined2 {r2In = 523, r2Out = "523"})

>>> pureTryTest $ fromString @(Refined2 'OL (ReadP Int Id) (Id > 12) String) "2"
Left ()

Defined in Predicate.Refined2

Methods

fromString :: String -> Refined2 opts ip op s

(Lift (PP ip i), Lift i) => Lift (Refined2 opts ip op i)

Defined in Predicate.Refined2

Methods

lift :: Refined2 opts ip op i -> Q Exp

(Arbitrary i, Refined2C opts ip op i, Show (PP ip i)) => Arbitrary (Refined2 opts ip op i)

Arbitrary instance for Refined2

>>> :m + Data.Time.Calendar.WeekDate
>>> xs <- generate (vectorOf 10 (arbitrary @(Refined2 'OU (ToEnum Day Id) (Snd (ToWeekDate Id) == "Tuesday") Int)))
>>> all (\x -> let y = toEnum @Day (r2Out x) in view _3 (toWeekDate y) == 2 && r2In x == y) xs
True

Defined in Predicate.Refined2

Methods

arbitrary :: Gen (Refined2 opts ip op i)

shrink :: Refined2 opts ip op i -> [Refined2 opts ip op i]

(Refined2C opts ip op i, Hashable i) => Hashable (Refined2 opts ip op i)

Hashable instance for Refined2

Defined in Predicate.Refined2

Methods

hashWithSalt :: Int -> Refined2 opts ip op i -> Int

hash :: Refined2 opts ip op i -> Int

ToJSON i => ToJSON (Refined2 opts ip op i)

ToJSON instance for Refined2

>>> import qualified Data.Aeson as A
>>> A.encode (unsafeRefined2 @'OZ @(ReadBase Int 16 Id) @(Between 0 255 Id) 254 "fe")
"\"fe\""

>>> A.encode (unsafeRefined2 @'OZ @Id @'True @Int 123 123)
"123"

Defined in Predicate.Refined2

Methods

toJSON :: Refined2 opts ip op i -> Value

toEncoding :: Refined2 opts ip op i -> Encoding

toJSONList :: [Refined2 opts ip op i] -> Value

toEncodingList :: [Refined2 opts ip op i] -> Encoding

(Show i, Show (PP ip i), Refined2C opts ip op i, FromJSON i) => FromJSON (Refined2 opts ip op i)

FromJSON instance for Refined2

>>> import qualified Data.Aeson as A
>>> A.eitherDecode' @(Refined2 'OZ (ReadBase Int 16 Id) (Id > 10 && Id < 256) String) "\"00fe\""
Right (Refined2 {r2In = 254, r2Out = "00fe"})

>>> removeAnsi $ A.eitherDecode' @(Refined2 'OAN (ReadBase Int 16 Id) (Id > 10 && Id < 256) String) "\"00fe443a\""
Error in $: Refined2:Step 2. False Boolean Check(op) | {True && False | (16663610 < 256)}

*** Step 1. Success Initial Conversion(ip) [16663610] ***

P ReadBase(Int,16) 16663610 | "00fe443a"
|
`- P Id "00fe443a"

*** Step 2. False Boolean Check(op) ***

False True && False | (16663610 < 256)
|
+- True 16663610 > 10
|  |
|  +- P Id 16663610
|  |
|  `- P '10
|
`- False 16663610 < 256
   |
   +- P Id 16663610
   |
   `- P '256

Defined in Predicate.Refined2

Methods

parseJSON :: Value -> Parser (Refined2 opts ip op i)

parseJSONList :: Value -> Parser [Refined2 opts ip op i]

(Show i, Show (PP ip i), Refined2C opts ip op i, Binary i) => Binary (Refined2 opts ip op i)

Binary instance for Refined2

>>> import Control.Arrow ((+++))
>>> import Data.Time
>>> type K1 = Refined2 'OAN (ReadP Day Id) 'True String
>>> type K2 = Refined2 'OAN (ReadP Day Id) (Between (ReadP Day "2019-05-30") (ReadP Day "2019-06-01") Id) String
>>> r = unsafeRefined2' "2019-04-23" :: K1
>>> removeAnsi $ (view _3 +++ view _3) $ B.decodeOrFail @K1 (B.encode r)
Refined2 {r2In = 2019-04-23, r2Out = "2019-04-23"}

>>> removeAnsi $ (view _3 +++ view _3) $ B.decodeOrFail @K2 (B.encode r)
Refined2:Step 2. False Boolean Check(op) | {2019-05-30 <= 2019-04-23}

*** Step 1. Success Initial Conversion(ip) [2019-04-23] ***

P ReadP Day 2019-04-23
|
`- P Id "2019-04-23"

*** Step 2. False Boolean Check(op) ***

False 2019-05-30 <= 2019-04-23
|
+- P Id 2019-04-23
|
+- P ReadP Day 2019-05-30
|  |
|  `- P '2019-05-30
|
`- P ReadP Day 2019-06-01
   |
   `- P '2019-06-01

Defined in Predicate.Refined2

Methods

put :: Refined2 opts ip op i -> Put

get :: Get (Refined2 opts ip op i)

putList :: [Refined2 opts ip op i] -> Put

type Refined2C opts ip op i = (OptTC opts, P ip i, P op (PP ip i), PP op (PP ip i) ~ Bool)

Provides the constraints on Refined2

display results

prtEval2 :: forall opts ip op i. (Refined2C opts ip op i, Show (PP ip i)) => i -> Either Msg2 (Refined2 opts ip op i)

prtEval2P :: 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)

prtEval2IO :: forall opts ip op i. (Refined2C opts ip op i, Show (PP ip i)) => i -> IO (Either String (Refined2 opts ip op i))

same as prtEval2PIO without a proxy for used with TypeApplications

prtEval2PIO :: forall opts ip op i proxy. (Refined2C opts ip op i, Show (PP ip i)) => proxy '(opts, ip, op, i) -> i -> IO (Either String (Refined2 opts ip op i))

same as prtEval2P but runs in IO

prt2IO :: forall opts a r. (OptTC opts, Show a) => (RResults2 a, Maybe r) -> IO (Either String r)

prt2Impl :: forall a. Show a => POpts -> RResults2 a -> Msg2

data Msg2

Constructors

Msg2

Fields

• m2Desc :: !String
• m2Short :: !String
• m2Long :: !String

Instances

Eq Msg2

Defined in Predicate.Refined2

Methods

(==) :: Msg2 -> Msg2 -> Bool

(/=) :: Msg2 -> Msg2 -> Bool

Show Msg2

Defined in Predicate.Refined2

Methods

showsPrec :: Int -> Msg2 -> ShowS

show :: Msg2 -> String

showList :: [Msg2] -> ShowS

data RResults2 a

An ADT that summarises the results of evaluating Refined2 representing all possible states

Constructors

RF !String !(Tree PE)

RTF !a !(Tree PE) !String !(Tree PE)

RTFalse !a !(Tree PE) !(Tree PE)

RTTrue !a !(Tree PE) !(Tree PE)

Instances

Show a => Show (RResults2 a)

Defined in Predicate.Refined2

Methods

showsPrec :: Int -> RResults2 a -> ShowS

show :: RResults2 a -> String

showList :: [RResults2 a] -> ShowS

evaluation methods

eval2 :: forall opts ip op i. Refined2C opts ip op i => i -> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))

eval2P :: forall opts ip op i. Refined2C opts ip op i => Proxy '(opts, ip, op, i) -> i -> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))

eval2M :: forall m opts ip op i. (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 String (Refined2 opts ip op i)

pure version for extracting Refined2

>>> newRefined2 @'OL @Id @'True 22
Right (Refined2 {r2In = 22, r2Out = 22})

>>> newRefined2 @'OL @(ReadP UTCTime Id) @(Between (MkDay '(2020,5,2)) (MkDay '(2020,5,7)) (MkJust (ToDay Id))) "2020-05-04 12:13:14Z"
Right (Refined2 {r2In = 2020-05-04 12:13:14 UTC, r2Out = "2020-05-04 12:13:14Z"})

>>> newRefined2 @'OL @(ReadP UTCTime Id) @(Between (MkDay '(2020,5,2)) (MkDay '(2020,5,7)) (MkJust (ToDay Id))) "2020-05-08 12:13:14Z"
Left "Step 2. False Boolean Check(op) | {Just 2020-05-08 <= Just 2020-05-07}"

newRefined2P :: forall opts ip op i proxy. (Refined2C opts ip op i, Show (PP ip i)) => proxy '(opts, ip, op, i) -> i -> Either String (Refined2 opts ip op i)

create a wrapped Refined2 value

newRefined2T :: forall m opts ip op i. (Refined2C opts ip op i, Monad m, Show (PP ip i)) => i -> RefinedT m (Refined2 opts ip op i)

create a wrapped Refined2 type

>>> prtRefinedTIO $ newRefined2T @_ @'OL @(MkDayExtra Id >> Just Id) @(Thd Id == 5) (2019,11,1)
Refined2 {r2In = (2019-11-01,44,5), r2Out = (2019,11,1)}

>>> prtRefinedTIO $ newRefined2T @_ @'OL @(MkDayExtra Id >> Just Id) @(Thd Id == 5) (2019,11,2)
failure msg[Step 2. False Boolean Check(op) | {6 == 5}]

>>> prtRefinedTIO $ newRefined2T @_ @'OL @(MkDayExtra Id >> Just Id) @(Msg "wrong day:" (Thd Id == 5)) (2019,11,2)
failure msg[Step 2. False Boolean Check(op) | {wrong day:6 == 5}]

newRefined2TP :: forall m opts ip op i proxy. (Refined2C opts ip op i, Monad m, Show (PP ip i)) => proxy '(opts, ip, op, i) -> i -> RefinedT m (Refined2 opts ip op i)

create a wrapped Refined2 type with an explicit proxy

newRefined2TIO :: forall m opts ip op i. (Refined2C opts ip op i, MonadIO m, Show (PP ip i)) => i -> RefinedT m (Refined2 opts ip op i)

create a wrapped Refined2 type in IO

withRefined2T :: forall opts ip op i m b. (Monad m, Refined2C opts ip op i, Show (PP ip i)) => i -> (Refined2 opts ip op i -> RefinedT m b) -> RefinedT m b

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 @'OZ @(ReadBase Int 16 Id) @(Between 100 200 Id) "a3" $ \x -> withRefined2T @'OZ @(ReadBase Int 2 Id) @'True "1001110111" $ \y -> pure (r2In x + r2In y)
794

this example fails as the the hex value is out of range

>>> prtRefinedTIO $ withRefined2T @'OAN @(ReadBase Int 16 Id) @(Between 100 200 Id) "a388" $ \x -> withRefined2T @'OAN @(ReadBase Int 2 Id) @'True "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 opts ip op i b proxy. (Monad m, Refined2C opts ip op i, Show (PP ip i)) => proxy '(opts, ip, op, i) -> i -> (Refined2 opts ip op i -> RefinedT m b) -> RefinedT m b

withRefined2TIO :: forall opts ip op i m b. (MonadIO m, Refined2C opts ip op i, Show (PP ip i)) => i -> (Refined2 opts ip op i -> RefinedT m b) -> RefinedT m b

same as withRefined2T for IO

proxy methods

type family MakeR2 p where ...

type family for converting from a 4-tuple '(opts,ip,op,i) to a Refined2 type

Equations

MakeR2 '(opts, ip, op, i) = Refined2 opts ip op i

mkProxy2 :: forall z opts ip op i. z ~ '(opts, ip, op, i) => Proxy '(opts, ip, op, i)

creates a 4-tuple proxy (see withRefined2TP newRefined2TP eval2P prtEval2P)

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 {r2In = 24, r2Out = "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 {r2In = 24, r2Out = "24"})

mkProxy2' :: forall z opts ip op i. (z ~ '(ip, op, i), Refined2C opts ip op i) => Proxy '(opts, ip, op, i)

same as mkProxy2 but checks to make sure the proxy is consistent with the Refined2C constraint

QuickCheck methods

genRefined2 :: forall opts ip op i. (Refined2C opts ip op i, Show (PP ip i)) => Gen i -> Gen (Refined2 opts ip op i)

create a Refined2 generator using a generator to restrict the values (so it completes)

>>> g = genRefined2 @'OU @(ToEnum Day Id) @(UnMkDay Id >> Snd Id == 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, Show (PP ip i)) => Proxy '(opts, ip, op, i) -> Gen i -> Gen (Refined2 opts ip op i)

create a Refined2 generator using a proxy

unsafe methods for creating Refined2

unsafeRefined2 :: forall opts ip op i. PP ip i -> i -> Refined2 opts ip op i

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

directly load values into Refined2. It still checks to see that those values are valid

type family ReplaceOptT2 (o :: OptT) t where ...

Equations

ReplaceOptT2 o (Refined2 _ ip op i) = Refined2 o ip op i

type family AppendOptT2 (o :: OptT) t where ...

Equations

AppendOptT2 o (Refined2 o' ip op i) = Refined2 (o' :# o) ip op i