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