Predicate.Refined1

Refinement type allowing the external type to differ from the internal type doesnt store the output value but runs on demand but has calculate each time and could fail later see Refined1

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

Refined1

data Refined1 (opts :: OptT) ip op fmt i

Refinement type that differentiates the input from output: similar to Refined3 but only creates the output value as needed.

• opts are the display options
• ip converts i to PP ip i which is the internal type and stored in unRefined1
• op validates that internal type using PP op (PP ip i) ~ Bool
• fmt outputs the internal type PP fmt (PP ip i) ~ i (not stored anywhere but created on demand)
• i is the input type
• PP fmt (PP ip i) should be valid as input for Refined1

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 unRefined1
• validate unRefined1 using the predicate op
• show unRefined1 using fmt (does not store the formatted result unlike Refined3)

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

>>> newRefined1 @OZ @(ReadBase Int 16 Id) @(Lt 255) @(PrintF "%x" Id) "00fe"
Right (Refined1 254)

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

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

>>> newRefined1 @OL @(Map (ReadP Int Id) (Resplit "\\." Id)) @(Msg "length invalid:" (Len == 4)) @(PrintL 4 "%03d.%03d.%03d.%03d" Id) "198.162.3.1.5"
Left "Step 2. False Boolean Check(op) | {length invalid:5 == 4}"

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

>>> newRefined1 @OZ @(Map (ReadP Int Id) (Resplit "\\." Id)) @(Guard (PrintF "found length=%d" Len) (Len == 4) >> 'True) @(PrintL 4 "%03d.%03d.%03d.%03d" Id) "198.162.3.1"
Right (Refined1 [198,162,3,1])

>>> :m + Data.Time.Calendar.WeekDate
>>> newRefined1 @OZ @(MkDayExtra Id >> 'Just Id) @(Guard "expected a Sunday" (Thd Id == 7) >> 'True) @(UnMkDay (Fst Id)) (2019,10,13)
Right (Refined1 (2019-10-13,41,7))

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

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

>>> type T4 k = '( OZ, MkDayExtra Id >> 'Just Id, Guard "expected a Sunday" (Thd Id == 7) >> 'True, UnMkDay (Fst Id), k)
>>> newRefined1P (Proxy @(T4 _)) (2019,10,12)
Left "Step 2. Failed Boolean Check(op) | expected a Sunday"

>>> newRefined1P (Proxy @(T4 _)) (2019,10,13)
Right (Refined1 (2019-10-13,41,7))

Instances

(Eq i, Eq (PP ip i), Eq (PP fmt (PP ip i))) => Eq (Refined1 opts ip op fmt i)

Defined in Predicate.Refined1

Methods

(==) :: Refined1 opts ip op fmt i -> Refined1 opts ip op fmt i -> Bool

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

(Eq i, Show i, Eq (PP ip i), Show (PP ip i), Refined1C opts ip op fmt i, Read (PP ip i), Read (PP fmt (PP ip i))) => Read (Refined1 opts ip op fmt i)

Read instance for Refined1

>>> reads @(Refined1 OZ (ReadBase Int 16 Id) (Between 0 255 Id) (ShowBase 16 Id) String) "Refined1 254"
[(Refined1 254,"")]

>>> reads @(Refined1 OZ (ReadBase Int 16 Id) (Between 0 255 Id) (ShowBase 16 Id) String) "Refined1 300"
[]

>>> reads @(Refined1 OZ (ReadBase Int 16 Id) (Id < 0) (ShowBase 16 Id) String) "Refined1 (-1234)"
[(Refined1 (-1234),"")]

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

>>> reads @(Refined1 OZ Id 'True Id Int) "Refined1 (-123)xyz"
[(Refined1 (-123),"xyz")]

Defined in Predicate.Refined1

Methods

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

readList :: ReadS [Refined1 opts ip op fmt i]

readPrec :: ReadPrec (Refined1 opts ip op fmt i)

readListPrec :: ReadPrec [Refined1 opts ip op fmt i]

(Show i, Show (PP ip i), Show (PP fmt (PP ip i))) => Show (Refined1 opts ip op fmt i)

Defined in Predicate.Refined1

Methods

showsPrec :: Int -> Refined1 opts ip op fmt i -> ShowS

show :: Refined1 opts ip op fmt i -> String

showList :: [Refined1 opts ip op fmt i] -> ShowS

(Refined1C opts ip op fmt String, Show (PP ip String)) => IsString (Refined1 opts ip op fmt String)

IsString instance for Refined1

>>> pureTryTest $ fromString @(Refined1 OL (ReadP Int Id) (Id > 12) (ShowP Id) String) "523"
Right (Refined1 523)

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

Defined in Predicate.Refined1

Methods

fromString :: String -> Refined1 opts ip op fmt String

(Lift (PP ip i), Lift (PP fmt (PP ip i))) => Lift (Refined1 opts ip op fmt i)

Defined in Predicate.Refined1

Methods

lift :: Refined1 opts ip op fmt i -> Q Exp

(Arbitrary (PP ip i), Refined1C opts ip op fmt i) => Arbitrary (Refined1 opts ip op fmt i)

Arbitrary instance for Refined1

>>> xs <- generate (vectorOf 10 (arbitrary @(Refined1 OU (ReadP Int Id) (1 <..> 120 && Even) (ShowP Id) String)))
>>> all ((/=0) . unRefined1) xs
True

>>> xs <- generate (vectorOf 10 (arbitrary @(Refined1 OU Id (Prime Id) Id Int)))
>>> all (isPrime . unRefined1) xs
True

Defined in Predicate.Refined1

Methods

arbitrary :: Gen (Refined1 opts ip op fmt i)

shrink :: Refined1 opts ip op fmt i -> [Refined1 opts ip op fmt i]

(Refined1C opts ip op fmt i, Hashable (PP ip i)) => Hashable (Refined1 opts ip op fmt i)

Hashable instance for Refined1

Defined in Predicate.Refined1

Methods

hashWithSalt :: Int -> Refined1 opts ip op fmt i -> Int

hash :: Refined1 opts ip op fmt i -> Int

(OptTC opts, Show (PP fmt (PP ip i)), ToJSON (PP fmt (PP ip i)), P fmt (PP ip i)) => ToJSON (Refined1 opts ip op fmt i)

ToJSON instance for Refined1

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

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

Defined in Predicate.Refined1

Methods

toJSON :: Refined1 opts ip op fmt i -> Value

toEncoding :: Refined1 opts ip op fmt i -> Encoding

toJSONList :: [Refined1 opts ip op fmt i] -> Value

toEncodingList :: [Refined1 opts ip op fmt i] -> Encoding

(Show (PP fmt (PP ip i)), Show (PP ip i), Refined1C opts ip op fmt i, FromJSON i) => FromJSON (Refined1 opts ip op fmt i)

FromJSON instance for Refined1

>>> import qualified Data.Aeson as A
>>> A.eitherDecode' @(Refined1 OZ (ReadBase Int 16 Id) (Id > 10 && Id < 256) (ShowBase 16 Id) String) "\"00fe\""
Right (Refined1 254)

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

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

P ReadBase(Int,16) 16663610
|
`- 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.Refined1

Methods

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

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

(Show (PP fmt (PP ip i)), Show (PP ip i), Refined1C opts ip op fmt i, Binary i) => Binary (Refined1 opts ip op fmt i)

Binary instance for Refined1

>>> import Control.Arrow ((+++))
>>> import Control.Lens
>>> import Data.Time
>>> type K1 = MakeR1 '( OAN, ReadP Day Id, 'True, ShowP Id, String)
>>> type K2 = MakeR1 '( OAN, ReadP Day Id, Between (ReadP Day "2019-05-30") (ReadP Day "2019-06-01") Id, ShowP Id, String)
>>> r = unsafeRefined1' "2019-04-23" :: K1
>>> removeAnsi $ (view _3 +++ view _3) $ B.decodeOrFail @K1 (B.encode r)
Refined1 2019-04-23

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

Methods

put :: Refined1 opts ip op fmt i -> Put

get :: Get (Refined1 opts ip op fmt i)

putList :: [Refined1 opts ip op fmt i] -> Put

unRefined1 :: forall (opts :: OptT) ip op fmt i. Refined1 opts ip op fmt i -> PP ip i

type Refined1C opts ip op fmt i = (OptTC opts, 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 Refined1

display results

prtEval1 :: forall opts ip op fmt i. (Refined1C opts ip op fmt i, Show (PP ip i), Show i) => i -> Either Msg1 (Refined1 opts ip op fmt i)

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

prtEval1P :: forall opts ip op fmt i proxy. (Refined1C opts ip op fmt i, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> i -> Either Msg1 (Refined1 opts ip op fmt i)

create a Refined1 using a 5-tuple proxy and aggregate the results on failure

prtEval1IO :: forall opts ip op fmt i. (Refined1C opts ip op fmt i, Show (PP ip i), Show i) => i -> IO (Either String (Refined1 opts ip op fmt i))

same as prtEval1PIO but passes in the proxy

prtEval1PIO :: forall opts ip op fmt i proxy. (Refined1C opts ip op fmt i, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> i -> IO (Either String (Refined1 opts ip op fmt i))

same as prtEval1P but runs in IO

prt1IO :: forall opts a b r. (OptTC opts, Show a, Show b) => (RResults1 a b, Maybe r) -> IO (Either String r)

prt1Impl :: forall a b. (Show a, Show b) => POpts -> RResults1 a b -> Msg1

data Msg1

Constructors

Msg1

Fields

• m1Desc :: !String
• m1Short :: !String
• m1Long :: !String

Instances

Eq Msg1

Defined in Predicate.Refined1

Methods

(==) :: Msg1 -> Msg1 -> Bool

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

Show Msg1

Defined in Predicate.Refined1

Methods

showsPrec :: Int -> Msg1 -> ShowS

show :: Msg1 -> String

showList :: [Msg1] -> ShowS

data RResults1 a b

An ADT that summarises the results of evaluating Refined1 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 (RResults1 a b)

Defined in Predicate.Refined1

Methods

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

show :: RResults1 a b -> String

showList :: [RResults1 a b] -> ShowS

evaluation methods

eval1 :: forall opts ip op fmt i. Refined1C opts ip op fmt i => i -> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 opts ip op fmt i))

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

eval1P :: forall opts ip op fmt i proxy. Refined1C opts ip op fmt i => proxy '(opts, ip, op, fmt, i) -> i -> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 opts ip op fmt i))

create a Refined1 value using a 5-tuple proxy (see mkProxy1)

use mkProxy1 to package all the types together as a 5-tuple

eval1M :: forall m opts ip op fmt i. (MonadEval m, Refined1C opts ip op fmt i) => i -> m (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 opts ip op fmt i))

newRefined1 :: forall opts ip op fmt i. (Refined1C opts ip op fmt i, Show (PP ip i), Show i) => i -> Either String (Refined1 opts ip op fmt i)

pure version for extracting Refined1

>>> newRefined1 @OL @(ParseTimeP TimeOfDay "%-H:%-M:%-S" Id) @'True @(FormatTimeP "%H:%M:%S" Id) "1:15:7"
Right (Refined1 01:15:07)

>>> newRefined1 @OL @(ParseTimeP TimeOfDay "%-H:%-M:%-S" Id) @'True @(FormatTimeP "%H:%M:%S" Id) "1:2:x"
Left "Step 1. Initial Conversion(ip) Failed | ParseTimeP TimeOfDay (%-H:%-M:%-S) failed to parse"

>>> newRefined1 @OL @(Rescan "^(\\d{1,2}):(\\d{1,2}):(\\d{1,2})$" Id >> Snd (Head Id) >> Map (ReadP Int Id) Id) @(All (0 <..> 59) Id && Len == 3) @(PrintL 3 "%02d:%02d:%02d" Id) "1:2:3"
Right (Refined1 [1,2,3])

newRefined1P :: forall opts ip op fmt i proxy. (Refined1C opts ip op fmt i, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> i -> Either String (Refined1 opts ip op fmt i)

create a wrapped Refined1 value

newRefined1T :: forall m opts ip op fmt i. (Refined1C opts ip op fmt i, Monad m, Show (PP ip i), Show i) => i -> RefinedT m (Refined1 opts ip op fmt i)

newRefined1TP :: forall m opts ip op fmt i proxy. (Refined1C opts ip op fmt i, Monad m, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> i -> RefinedT m (Refined1 opts ip op fmt i)

create a wrapped Refined1 type

>>> prtRefinedTIO $ newRefined1TP (Proxy @'( OZ, MkDayExtra Id >> Just Id, GuardSimple (Thd Id == 5) >> 'True, UnMkDay (Fst Id), (Int,Int,Int))) (2019,11,1)
Refined1 (2019-11-01,44,5)

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

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

newRefined1TPIO :: forall m opts ip op fmt i proxy. (Refined1C opts ip op fmt i, MonadIO m, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> i -> RefinedT m (Refined1 opts ip op fmt i)

withRefined1T :: forall opts ip op fmt i m b. (Monad m, Refined1C opts ip op fmt i, Show (PP ip i), Show i) => i -> (Refined1 opts ip op fmt i -> RefinedT m b) -> RefinedT m b

create a Refined1 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
>>> :set -XRankNTypes
>>> b16 :: forall opts . Proxy '( opts, ReadBase Int 16 Id, Between 100 200 Id, ShowBase 16 Id, String); b16 = Proxy
>>> b2 :: forall opts . Proxy '( opts, ReadBase Int 2 Id, 'True, ShowBase 2 Id, String); b2 = Proxy
>>> prtRefinedTIO $ withRefined1TP (b16 @OZ) "a3" $ \x -> withRefined1TP (b2 @OZ) "1001110111" $ \y -> pure (unRefined1 x + unRefined1 y)
794

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

>>> prtRefinedTIO $ withRefined1TP (b16 @OAN) "a388" $ \x -> withRefined1TP (b2 @OAN) "1001110111" $ \y -> pure (x,y)

*** Step 1. Success Initial Conversion(ip) (41864) ***

P ReadBase(Int,16) 41864
|
`- 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}]

withRefined1TIO :: forall opts ip op fmt i m b. (MonadIO m, Refined1C opts ip op fmt i, Show (PP ip i), Show i) => i -> (Refined1 opts ip op fmt i -> RefinedT m b) -> RefinedT m b

withRefined1TP :: forall m opts ip op fmt i b proxy. (Monad m, Refined1C opts ip op fmt i, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> i -> (Refined1 opts ip op fmt i -> RefinedT m b) -> RefinedT m b

proxy methods

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

creates a 5-tuple proxy (see withRefined1TP newRefined1TP eval1P prtEval1P)

use type application to set the 5-tuple or set the individual parameters directly

set the 5-tuple directly

>>> eg1 = mkProxy1 @'( OL, ReadP Int Id, Gt 10, ShowP Id, String)
>>> newRefined1P eg1 "24"
Right (Refined1 24)

skip the 5-tuple and set each parameter individually using type application

>>> eg2 = mkProxy1 @_ @OL @(ReadP Int Id) @(Gt 10) @(ShowP Id)
>>> newRefined1P eg2 "24"
Right (Refined1 24)

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

same as mkProxy1 but checks to make sure the proxy is consistent with the Refined1C constraint

type family MakeR1 p where ...

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

Equations

MakeR1 '(opts, ip, op, fmt, i) = Refined1 opts ip op fmt i

unsafe methods for creating Refined1

unsafeRefined1 :: forall opts ip op fmt i. PP ip i -> Refined1 opts ip op fmt i

directly load values into Refined1 without any checking

unsafeRefined1' :: forall opts ip op fmt i. (HasCallStack, Show i, Show (PP ip i), Refined1C opts ip op fmt i) => i -> Refined1 opts ip op fmt i

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

combine Refined1 values

convertRefined1TP :: forall m opts ip op fmt i ip1 op1 fmt1 i1. (Refined1C opts ip1 op1 fmt1 i1, Monad m, Show (PP ip i), PP ip i ~ PP ip1 i1, Show i1) => Proxy '(opts, ip, op, fmt, i) -> Proxy '(opts, ip1, op1, fmt1, i1) -> RefinedT m (Refined1 opts ip op fmt i) -> RefinedT m (Refined1 opts ip1 op1 fmt1 i1)

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

rapply1 :: forall m opts ip op fmt i. (Refined1C opts ip op fmt i, Monad m, Show (PP ip i), Show i) => (PP ip i -> PP ip i -> PP ip i) -> RefinedT m (Refined1 opts ip op fmt i) -> RefinedT m (Refined1 opts ip op fmt i) -> RefinedT m (Refined1 opts ip op fmt i)

applies a binary operation to two wrapped Refined1 parameters

rapply1P :: forall m opts ip op fmt i proxy. (Refined1C opts ip op fmt i, Monad m, Show (PP ip i), Show i) => proxy '(opts, ip, op, fmt, i) -> (PP ip i -> PP ip i -> PP ip i) -> RefinedT m (Refined1 opts ip op fmt i) -> RefinedT m (Refined1 opts ip op fmt i) -> RefinedT m (Refined1 opts ip op fmt i)

same as rapply1 but uses a 5-tuple proxy instead

QuickCheck methods

genRefined1 :: forall opts ip op fmt i. Refined1C opts ip op fmt i => Gen (PP ip i) -> Gen (Refined1 opts ip op fmt i)

create a Refined1 generator

>>> g = genRefined1 @OU @(ReadP Int Id) @(Between 10 100 Id && Even) @(ShowP Id) (choose (10,100))
>>> xs <- generate (vectorOf 10 g)
>>> all (\x -> let y = unRefined1 x in y >= 0 && y <= 100 && even y) xs
True

genRefined1P :: forall opts ip op fmt i. Refined1C opts ip op fmt i => Proxy '(opts, ip, op, fmt, i) -> Gen (PP ip i) -> Gen (Refined1 opts ip op fmt i)

create a Refined1 generator with a Proxy

emulate Refined1 using Refined

type RefinedEmulate (opts :: OptT) p a = Refined1 opts Id p Id a

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

eval1PX :: forall opts ip op fmt i proxy. Refined1C opts ip op fmt i => proxy '(opts, ip, op, fmt, i) -> i -> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined opts op (PP ip i), PP fmt (PP ip i)))

similar to eval1P but it emulates Refined1 but using Refined

takes a 5-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 RResults1

eval1X :: forall opts ip op fmt i. Refined1C opts ip op fmt i => i -> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined opts op (PP ip i), PP fmt (PP ip i)))

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

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

replace the opts type

Equations

ReplaceOptT1 o (Refined1 _ ip op fmt i) = Refined1 o ip op fmt i

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

change the opts type

Equations

AppendOptT1 o (Refined1 o' ip op fmt i) = Refined1 (o' :# o) ip op fmt i