Predicate.Refined3

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

similar to Refined2 but also provides:
* quickCheck methods
* ability to combine refinement types
* a canonical output value using the 'fmt' parameter

Refined3

data Refined3 ip op fmt i

Refinement type that differentiates the input from output

• i is the input type
• ip converts i to PP ip i which is the internal type and stored in r3In
• op validates that internal type using PP op (PP ip i) ~ Bool
• fmt outputs the internal type PP fmt (PP ip i) ~ i and stored in r3Out
• 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 in r3Out

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)

Defined in Predicate.Refined3

Methods

(==) :: Refined3 ip op fmt i -> Refined3 ip op fmt i -> Bool

(/=) :: Refined3 ip op fmt i -> Refined3 ip op fmt i -> Bool

(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)

Read instance for Refined3

>>> reads @(Refined3 (ReadBase Int 16 Id) (Between 0 255 Id) (ShowBase 16 Id) String) "Refined3 {r3In = 254, r3Out = \"fe\"}"
[(Refined3 {r3In = 254, r3Out = "fe"},"")]

>>> reads @(Refined3 (ReadBase Int 16 Id) (Between 0 255 Id) (ShowBase 16 Id) String) "Refined3 {r3In = 300, r3Out = \"12c\"}"
[]

>>> reads @(Refined3 (ReadBase Int 16 Id) (Id < 0) (ShowBase 16 Id) String) "Refined3 {r3In = -1234, r3Out = \"-4d2\"}"
[(Refined3 {r3In = -1234, r3Out = "-4d2"},"")]

>>> reads @(Refined3 (Map (ReadP Int Id) (Resplit "\\." Id)) (Guard "len/=4" (Len == 4) >> 'True) (PrintL 4 "%d.%d.%d.%d" Id) String) "Refined3 {r3In = [192,168,0,1], r3Out = \"192.168.0.1\"}"
[(Refined3 {r3In = [192,168,0,1], r3Out = "192.168.0.1"},"")]

Defined in Predicate.Refined3

Methods

readsPrec :: Int -> ReadS (Refined3 ip op fmt i)

readList :: ReadS [Refined3 ip op fmt i]

readPrec :: ReadPrec (Refined3 ip op fmt i)

readListPrec :: ReadPrec [Refined3 ip op fmt i]

(Show i, Show (PP ip i), Show (PP fmt (PP ip i))) => Show (Refined3 ip op fmt i)

Defined in Predicate.Refined3

Methods

showsPrec :: Int -> Refined3 ip op fmt i -> ShowS

show :: Refined3 ip op fmt i -> String

showList :: [Refined3 ip op fmt i] -> ShowS

(Refined3C ip op fmt String, Show (PP ip String)) => IsString (Refined3 ip op fmt String)

Defined in Predicate.Refined3

Methods

fromString :: String -> Refined3 ip op fmt String

(Lift (PP ip i), Lift (PP fmt (PP ip i))) => Lift (Refined3 ip op fmt i)

Defined in Predicate.Refined3

Methods

lift :: Refined3 ip op fmt i -> Q Exp

(Refined3C ip op fmt i, Hashable (PP ip i)) => Hashable (Refined3 ip op fmt i)

Hashable instance for Refined3

Defined in Predicate.Refined3

Methods

hashWithSalt :: Int -> Refined3 ip op fmt i -> Int

hash :: Refined3 ip op fmt i -> Int

ToJSON (PP fmt (PP ip i)) => ToJSON (Refined3 ip op fmt i)

ToJSON instance for Refined3

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

>>> A.encode (unsafeRefined3 @Id @'True @Id 123 123)
"123"

Defined in Predicate.Refined3

Methods

toJSON :: Refined3 ip op fmt i -> Value

toEncoding :: Refined3 ip op fmt i -> Encoding

toJSONList :: [Refined3 ip op fmt i] -> Value

toEncodingList :: [Refined3 ip op fmt i] -> Encoding

(Show (PP fmt (PP ip i)), Show (PP ip i), Refined3C ip op fmt i, FromJSON i) => FromJSON (Refined3 ip op fmt i)

FromJSON instance for Refined3

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

>>> removeAnsi $ A.eitherDecode' @(Refined3 (ReadBase Int 16 Id) (Id > 10 && Id < 256) (ShowBase 16 Id) String) "\"00fe443a\""
Error in $: Refined3: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.Refined3

Methods

parseJSON :: Value -> Parser (Refined3 ip op fmt i)

parseJSONList :: Value -> Parser [Refined3 ip op fmt i]

(Show (PP fmt (PP ip i)), Show (PP ip i), Refined3C ip op fmt i, Binary i) => Binary (Refined3 ip op fmt i)

Binary instance for Refined3

>>> import Control.Arrow ((+++))
>>> import Control.Lens
>>> import Data.Time
>>> type K1 = MakeR3 '(ReadP Day Id, 'True, ShowP Id, String)
>>> type K2 = MakeR3 '(ReadP Day Id, Between (ReadP Day "2019-05-30") (ReadP Day "2019-06-01") Id, ShowP Id, String)
>>> r = unsafeRefined3' oz "2019-04-23" :: K1
>>> removeAnsi $ (view _3 +++ view _3) $ B.decodeOrFail @K1 (B.encode r)
Refined3 {r3In = 2019-04-23, r3Out = "2019-04-23"}

>>> removeAnsi $ (view _3 +++ view _3) $ B.decodeOrFail @K2 (B.encode r)
Refined3: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.Refined3

Methods

put :: Refined3 ip op fmt i -> Put

get :: Get (Refined3 ip op fmt i)

putList :: [Refined3 ip op fmt i] -> Put

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)

Provides the constraints on Refined3

display results

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)

same as prtEval3P but skips the proxy and allows you to set each parameter individually using type application

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)

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

same as prtEval3P but runs in IO

prt3IO :: (Show a, Show b) => POpts -> (RResults3 a b, Maybe r) -> IO (Either String r)

prt3 :: (Show a, Show b) => POpts -> (RResults3 a b, Maybe r) -> Either Msg3 r

prt3Impl :: (Show a, Show b) => POpts -> RResults3 a b -> Msg3

data Msg3

Constructors

Msg3

Fields

• m3Desc :: !String
• m3Short :: !String
• m3Long :: !String

Instances

Eq Msg3

Defined in Predicate.Refined3

Methods

(==) :: Msg3 -> Msg3 -> Bool

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

Show Msg3

Defined in Predicate.Refined3

Methods

showsPrec :: Int -> Msg3 -> ShowS

show :: Msg3 -> String

showList :: [Msg3] -> ShowS

data RResults3 a b

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

Constructors

RF String (Tree PE)

RTF a (Tree PE) String (Tree PE)

RTFalse a (Tree PE) (Tree PE)

RTTrueF a (Tree PE) (Tree PE) String (Tree PE)

RTTrueT a (Tree PE) (Tree PE) b (Tree PE)

Instances

(Show a, Show b) => Show (RResults3 a b)

Defined in Predicate.Refined3

Methods

showsPrec :: Int -> RResults3 a b -> ShowS

show :: RResults3 a b -> String

showList :: [RResults3 a b] -> ShowS

evaluation methods

eval3 :: forall ip op fmt i. Refined3C ip op fmt i => POpts -> i -> (RResults3 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined3 ip op fmt i))

same as eval3P but can pass the parameters individually using type application

eval3P :: forall ip op fmt i proxy. Refined3C ip op fmt i => proxy '(ip, op, fmt, i) -> POpts -> i -> (RResults3 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined3 ip op fmt i))

create a Refined3 value using a 4-tuple proxy (see mkProxy3)

use mkProxy3 to package all the types together as a 4-tuple

create a wrapped Refined3 value

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)

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)

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

create a Refined3 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
>>> b16 = Proxy @'(ReadBase Int 16 Id, Between 100 200 Id, 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}]

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

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

proxy methods

mkProxy3 :: forall z ip op fmt i. z ~ '(ip, op, fmt, i) => Proxy '(ip, op, fmt, i)

creates a 4-tuple proxy (see withRefined3TP newRefined3TP eval3P prtEval3P)

use type application to set the 4-tuple or 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)

same as mkProxy3 but checks to make sure the proxy is consistent with the Refined3C constraint

type family MakeR3 p where ...

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

Equations

MakeR3 '(ip, op, fmt, i) = Refined3 ip op fmt i

unsafe methods for creating Refined3

unsafeRefined3 :: forall ip op fmt i. PP ip i -> PP fmt (PP ip i) -> Refined3 ip op fmt i

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

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

combine Refined3 values

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)

attempts to cast a wrapped Refined3 to another Refined3 with different predicates

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)

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)

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)

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)

uses arbitrary to generate the internal r3In and then uses 'fmt' to fill in the r3Out value

emulate Refined3 using Refined

type RefinedEmulate p a = Refined3 Id p Id a

emulates Refined using Refined3 by setting the input conversion and output formatting as noops

eval3PX :: forall ip op fmt i proxy. Refined3C ip op fmt i => proxy '(ip, op, fmt, i) -> POpts -> i -> (RResults3 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined op (PP ip i), PP fmt (PP ip i)))

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 RResults3

eval3X :: forall ip op fmt i. Refined3C ip op fmt i => POpts -> i -> (RResults3 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined op (PP ip i), PP fmt (PP ip i)))

same as eval3PX but allows you to set the parameters individually using type application

extract from 4-tuple

type family T4_1 x where ...

used by Refined3 to extract 'ip' from a promoted 4-tuple

>>> pl @(T4_1 Predicate.Examples.Refined3.Ip4) "1.2.3.4"
Present [1,2,3,4] (Map [1,2,3,4] | ["1","2","3","4"])
PresentT [1,2,3,4]

Equations

T4_1 '(a, b, c, d) = a

type family T4_2 x where ...

used by Refined3 for extracting the boolean predicate 'op' from a promoted 4-tuple

>>> pl @(T4_2 Predicate.Examples.Refined3.Ip4) [141,213,308,4]
Error octet 2 out of range 0-255 found 308
FailT "octet 2 out of range 0-255 found 308"

>>> pl @(T4_2 Predicate.Examples.Refined3.Ip4) [141,213,308,4,8]
Error Guards:invalid length(5) expected 4
FailT "Guards:invalid length(5) expected 4"

Equations

T4_2 '(a, b, c, d) = b

type family T4_3 x where ...

used by Refined3 for extracting 'fmt' from a promoted 4-tuple

>>> pl @(T4_3 Predicate.Examples.Refined3.Ip4) [141,513,9,4]
Present "141.513.009.004" (PrintL(4) [141.513.009.004] | s=%03d.%03d.%03d.%03d)
PresentT "141.513.009.004"

Equations

T4_3 '(a, b, c, d) = c

type family T4_4 x where ...

used by Refined3 for extracting the input type 'i' from a promoted 4-tuple

Equations

T4_4 '(a, b, c, d) = d