Predicate.Refined2

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

Refined2

data Refined2 ip op i

Refinement type that allows the input and output types to vary.

• i is the input type which is stored in r2Out
• 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

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)

Defined in Predicate.Refined2

Methods

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

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

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

Read instance for Refined2

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

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

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

>>> reads @(Refined2 (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 ip op i)

readList :: ReadS [Refined2 ip op i]

readPrec :: ReadPrec (Refined2 ip op i)

readListPrec :: ReadPrec [Refined2 ip op i]

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

Defined in Predicate.Refined2

Methods

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

show :: Refined2 ip op i -> String

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

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

Defined in Predicate.Refined2

Methods

fromString :: String -> Refined2 ip op String

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

Defined in Predicate.Refined2

Methods

lift :: Refined2 ip op i -> Q Exp

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

Hashable instance for Refined2

Defined in Predicate.Refined2

Methods

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

hash :: Refined2 ip op i -> Int

ToJSON i => ToJSON (Refined2 ip op i)

ToJSON instance for Refined2

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

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

Defined in Predicate.Refined2

Methods

toJSON :: Refined2 ip op i -> Value

toEncoding :: Refined2 ip op i -> Encoding

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

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

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

FromJSON instance for Refined2

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

>>> removeAnsi $ A.eitherDecode' @(Refined2 (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 ip op i)

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

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

Binary instance for Refined2

>>> import Control.Arrow ((+++))
>>> import Control.Lens
>>> import Data.Time
>>> type K1 = Refined2 (ReadP Day Id) 'True String
>>> type K2 = Refined2 (ReadP Day Id) (Between (ReadP Day "2019-05-30") (ReadP Day "2019-06-01") Id) String
>>> r = unsafeRefined2' oz "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 ip op i -> Put

get :: Get (Refined2 ip op i)

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

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

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)

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

same as prtEval2P but runs in IO

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

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

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)

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)

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

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

proxy methods

type family MakeR2 p where ...

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

Equations

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

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

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

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

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

unsafe methods for creating Refined2

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

directly load values into Refined2 without any checking

unsafeRefined2' :: forall ip op i. (Show (PP ip i), Refined2C ip op i, HasCallStack) => POpts -> i -> Refined2 ip op i

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

used by Refined2 to extract 'ip' from a promoted 3-tuple

Equations

T3_1 '(a, b, c) = a

type family T3_2 x where ...

used by Refined2 for extracting the boolean predicate 'op' from a promoted 3-tuple

Equations

T3_2 '(a, b, c) = b

type family T3_3 x where ...

used by Refined2 for extracting the input type 'i' from a promoted 3-tuple

Equations

T3_3 '(a, b, c) = c