Predicate.Refined3

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

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
• 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 into an internal type and store in r3In
• validate r3In using the predicate op
• show r3In and store that formatted result in r3Out

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

>>> prtEval3 @(ReadBase Int 16) @(Lt 255) @(Printf "%x" Id) ol "00fe"
Right (Refined3 {r3In = 254, r3Out = "fe"})

>>> prtEval3 @(ReadBase Int 16) @(Lt 253) @(Printf "%x" Id) ol "00fe"
Left Step 2. False Boolean Check(op) | FalseP

>>> prtEval3 @(ReadBase Int 16) @(Lt 255) @(Printf "%x" Id) ol "00fg"
Left Step 1. Initial Conversion(ip) Failed | invalid base 16

>>> prtEval3 @(Map (ReadP Int) (Resplit "\\." Id)) @(Guard (Printf "found length=%d" Len) (Len >> Id == 4) >> 'True) @(Printfnt 4 "%03d.%03d.%03d.%03d") ol "198.162.3.1.5"
Left Step 2. Failed Boolean Check(op) | found length=5

>>> prtEval3 @(Map (ReadP Int) (Resplit "\\." Id)) @(Guard (Printf "found length=%d" Len) (Len >> Id == 4) >> 'True) @(Printfnt 4 "%03d.%03d.%03d.%03d") ol "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)) ol (2019,10,13)
Right (Refined3 {r3In = (2019-10-13,41,7), r3Out = (2019,10,13)})

>>> prtEval3 @(MkDay' (Fst Id) (Snd Id) (Thd Id) >> 'Just Id) @(Guard "expected a Sunday" (Thd Id == 7) >> 'True) @(UnMkDay (Fst Id)) ol (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 _)) ol (2019,10,12)
Left Step 2. Failed Boolean Check(op) | expected a Sunday

>>> prtEval3P (Proxy @(T4 _)) ol (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) (Between 0 255) (ShowBase 16) String) "Refined3 {r3In = 254, r3Out = \"fe\"}"
[(Refined3 {r3In = 254, r3Out = "fe"},"")]

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

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

>>> reads @(Refined3 (Map (ReadP Int) (Resplit "\\." Id)) (Guard "len/=4" (Len == 4) >> 'True) (Printfnt 4 "%d.%d.%d.%d") 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

(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

(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, 'True, ShowP Id, String)
>>> type K2 = MakeR3 '(ReadP Day, Between (ReadP' Day "2019-03-30") (ReadP' Day "2019-06-01"), ShowP Id, String)
>>> type K3 = MakeR3 '(ReadP Day, Between (ReadP' Day "2019-05-30") (ReadP' Day "2019-06-01"), ShowP Id, String)
>>> r = unsafeRefined3' ol "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 {r3In = 2019-04-23, r3Out = "2019-04-23"}

>>> removeAnsi $ (view _3 +++ view _3) $ B.decodeOrFail @K3 (B.encode r)
Refined3:Step 2. False Boolean Check(op) | FalseP

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

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

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

False False && True
|
+- False 2019-04-23 >= 2019-05-30
|  |
|  +- P I
|  |
|  `- P ReadP Day (2019-05-30) 2019-05-30 | 2019-05-30
|     |
|     `- P '2019-05-30
|
`- True  2019-04-23 <= 2019-06-01
   |
   +- P I
   |
   `- P ReadP Day (2019-06-01) 2019-06-01 | 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

(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

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

>>> removeAnsi $ eitherDecode' @(Refined3 (ReadBase Int 16) (Id > 10 && Id < 256) (ShowBase 16) String) "\"00fe443a\""
Error in $: Refined3:Step 2. False Boolean Check(op) | FalseP

*** 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
|
+- 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]

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

ToJSON instance for Refined3

>>> encode (unsafeRefined3 @(ReadBase Int 16) @(Between 0 255) @(ShowBase 16) 254 "fe")
"\"fe\""

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

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

type RefinedEmulate p a = Refined3 Id p Id a

emulates Refined using Refined3 ie the input conversion and output formatting are noops

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)

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

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 Results a b

Constructors

XF String

XTF a String

XTFalse a

XTTrueF a String

XTTrueT a b

Instances

(Eq a, Eq b) => Eq (Results a b)

Defined in Predicate.Refined3

Methods

(==) :: Results a b -> Results a b -> Bool

(/=) :: Results a b -> Results a b -> Bool

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

Defined in Predicate.Refined3

Methods

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

show :: Results a b -> String

showList :: [Results a b] -> ShowS

data RResults a b

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 (RResults a b)

Defined in Predicate.Refined3

Methods

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

show :: RResults a b -> String

showList :: [RResults a b] -> ShowS

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

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

eval3M :: forall m ip op fmt i. (MonadEval m, Refined3C ip op fmt i) => POpts -> i -> m (RResults (PP ip i) (PP fmt (PP ip i)), Maybe (Refined3 ip op fmt i))

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

emulates Refined3 but uses Refined reuses the mkProxy3 but returns Refined vs Refined3 using plain Refined to emulate Refined3 sort of we just output fmt instead of embedding it in Refined3 so 'ip' predicate gets us started: we store that 'PP ip i' in Refined then we run the boolean predicate 'op' which is successful if true then we run 'fmt' against 'PP ip i' and output both the Refined (PP p i) and the PP fmt (PP (ip i)) ie 'fmt' run against PP ip i if any of the three steps fails the process stops immediately and dumps out RResults

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

proxy methods

mkProxy3 :: forall ip op fmt i. Proxy '(ip, op, fmt, i)

wraps the parameters for Refined3 in a 4-tuple

useful for methods such as withRefined3TP and newRefined3TP

mkProxy3' :: forall 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

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

use type application to set the parameters which then will be wrapped into a 4-tuple

useful for passing into eval3P / prtEval3P

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

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

type family MkProxy3T p where ...

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

Equations

MkProxy3T '(ip, op, fmt, i) = Proxy '(ip, op, fmt, i)

type family MakeR3 p where ...

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

Equations

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

create or combine Refined3 values

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

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
>>> type Base n p = '(ReadBase Int n, p, ShowBase 16, String)
>>> base16 = Proxy @(Base 16 (Between 100 200))
>>> base2 = Proxy @(Base 2 'True)
>>> prtRefinedTIO $ withRefined3TP base16 ol "a3" $ \x -> withRefined3TP base2 ol "1001110111" $ \y -> pure (r3In x + r3In y)
794

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

>>> prtRefinedTIO $ withRefined3TP base16 o0 "a388" $ \x -> withRefined3TP base2 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 True && False
|
+- True  41864 >= 100
|  |
|  +- P I
|  |
|  `- P '100
|
`- False 41864 <= 200
   |
   +- P I
   |
   `- P '200

failure msg[Step 2. False Boolean Check(op) | FalseP]

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)

create a wrapped Refined3 type

>>> prtRefinedTIO $ newRefined3TP (Proxy @'(MkDay >> JustFail "asfd" Id, GuardSimple (Thd Id == 5) >> 'True, UnMkDay (Fst Id), (Int,Int,Int))) ol (2019,11,1)
Refined3 {r3In = (2019-11-01,44,5), r3Out = (2019,11,1)}

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)

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) -> POpts -> 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) -> POpts -> (PP ip i -> PP ip i) -> Gen (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