Predicate.Refined

simple refinement type with only one type and a predicate

Refined

data Refined (opts :: Opt) p a

a simple refinement type that ensures the predicate p holds for the type a

Instances

Lift a => Lift (Refined opts p a :: Type)

Defined in Predicate.Refined

Methods

lift :: Refined opts p a -> Q Exp

liftTyped :: Refined opts p a -> Q (TExp (Refined opts p a))

Eq a => Eq (Refined opts p a)

Defined in Predicate.Refined

Methods

(==) :: Refined opts p a -> Refined opts p a -> Bool

(/=) :: Refined opts p a -> Refined opts p a -> Bool

Ord a => Ord (Refined opts p a)

Defined in Predicate.Refined

Methods

compare :: Refined opts p a -> Refined opts p a -> Ordering

(<) :: Refined opts p a -> Refined opts p a -> Bool

(<=) :: Refined opts p a -> Refined opts p a -> Bool

(>) :: Refined opts p a -> Refined opts p a -> Bool

(>=) :: Refined opts p a -> Refined opts p a -> Bool

max :: Refined opts p a -> Refined opts p a -> Refined opts p a

min :: Refined opts p a -> Refined opts p a -> Refined opts p a

(RefinedC opts p a, Read a) => Read (Refined opts p a)

Read instance for Refined

>>> reads @(Refined OZ (0 <..> 299) Int) "Refined 254"
[(Refined 254,"")]

>>> reads @(Refined OZ (0 <..> 299) Int) "Refined 300"
[]

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

Defined in Predicate.Refined

Methods

readsPrec :: Int -> ReadS (Refined opts p a)

readList :: ReadS [Refined opts p a]

readPrec :: ReadPrec (Refined opts p a)

readListPrec :: ReadPrec [Refined opts p a]

Show a => Show (Refined opts p a)

Defined in Predicate.Refined

Methods

showsPrec :: Int -> Refined opts p a -> ShowS

show :: Refined opts p a -> String

showList :: [Refined opts p a] -> ShowS

RefinedC opts p String => IsString (Refined opts p String)

IsString instance for Refined

>>> pureTryTest $ fromString @(Refined OL (ReadP Int Id >> Id > 244) String) "523"
Right (Refined "523")

>>> pureTryTest $ fromString @(Refined OL (ReadP Int Id >> Id > 244) String) "52"
Left ()

Defined in Predicate.Refined

Methods

fromString :: String -> Refined opts p String

(Arbitrary a, RefinedC opts p a, Show a) => Arbitrary (Refined opts p a)

Arbitrary instance for Refined

>>> xs <- generate (vectorOf 10 (arbitrary @(Refined OAN (Id /= 0) Int)))
>>> all ((/=0) . unRefined) xs
True

>>> xs <- generate (vectorOf 10 (arbitrary @(Refined OAN IsPrime Int)))
>>> all (isPrime . unRefined) xs
True

Defined in Predicate.Refined

Methods

arbitrary :: Gen (Refined opts p a)

shrink :: Refined opts p a -> [Refined opts p a]

(RefinedC opts p a, Hashable a) => Hashable (Refined opts p a)

Hashable instance for Refined

Defined in Predicate.Refined

Methods

hashWithSalt :: Int -> Refined opts p a -> Int

hash :: Refined opts p a -> Int

ToJSON a => ToJSON (Refined opts p a)

ToJSON instance for Refined

Defined in Predicate.Refined

Methods

toJSON :: Refined opts p a -> Value

toEncoding :: Refined opts p a -> Encoding

toJSONList :: [Refined opts p a] -> Value

toEncodingList :: [Refined opts p a] -> Encoding

(RefinedC opts p a, FromJSON a) => FromJSON (Refined opts p a)

FromJSON instance for Refined

>>> import qualified Data.Aeson as A
>>> A.eitherDecode' @(Refined OZ (Between 10 14 Id) Int) "13"
Right (Refined 13)

>>> removeAnsi $ A.eitherDecode' @(Refined OAN (Between 10 14 Id) Int) "16"
Error in $: Refined(FromJSON:parseJSON):False (16 <= 14)
False 16 <= 14
|
+- P Id 16
|
+- P '10
|
`- P '14

Defined in Predicate.Refined

Methods

parseJSON :: Value -> Parser (Refined opts p a)

parseJSONList :: Value -> Parser [Refined opts p a]

(RefinedC opts p a, Binary a) => Binary (Refined opts p a)

Binary instance for Refined

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

>>> removeAnsi $ (view _3 +++ view _3) $ B.decodeOrFail @K2 (B.encode r)
Refined(Binary:get):False (2019-05-30 <= 2019-04-23)
False 2019-05-30 <= 2019-04-23
|
+- P ReadP Day 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.Refined

Methods

put :: Refined opts p a -> Put

get :: Get (Refined opts p a)

putList :: [Refined opts p a] -> Put

NFData a => NFData (Refined opts p a)

Defined in Predicate.Refined

Methods

rnf :: Refined opts p a -> ()

unRefined :: forall k (opts :: Opt) (p :: k) a. Refined opts p a -> a

extract the value from Refined

data Msg0

holds the results of creating a Refined value for display

Constructors

Msg0

Fields

• m0BoolE :: !(Either String Bool)
• m0Short :: !String
• m0Long :: !String
• m0ValBoolColor :: !String

Instances

Eq Msg0

Defined in Predicate.Refined

Methods

(==) :: Msg0 -> Msg0 -> Bool

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

Show Msg0

Defined in Predicate.Refined

Methods

showsPrec :: Int -> Msg0 -> ShowS

show :: Msg0 -> String

showList :: [Msg0] -> ShowS

showMsg0 :: Msg0 -> String

verbose display of Msg0

type RefinedC opts p a = (OptC opts, PP p a ~ Bool, P p a)

the constraints that Refined must adhere to

create methods

newRefined :: forall opts p a. RefinedC opts p a => a -> Either Msg0 (Refined opts p a)

returns a pure Refined value if a is valid for the predicate p

>>> newRefined @OL @(ReadP Int Id > 99) "123"
Right (Refined "123")

>>> left m0Long $ newRefined @OL @(ReadP Int Id > 99) "12"
Left "False (12 > 99)"

>>> newRefined @OZ @(Between 10 14 Id) 13
Right (Refined 13)

>>> left m0BoolE $ newRefined @OZ @(Between 10 14 Id) 99
Left (Right False)

>>> newRefined @OZ @(Last >> Len == 4) ["one","two","three","four"]
Right (Refined ["one","two","three","four"])

>>> newRefined @OZ @(Re "^\\d{1,3}\\.\\d{1,3}\\.\\d{1,3}\\.\\d{1,3}$") "141.213.1.99"
Right (Refined "141.213.1.99")

>>> left m0BoolE $ newRefined @OZ @(Re "^\\d{1,3}\\.\\d{1,3}\\.\\d{1,3}\\.\\d{1,3}$") "141.213.1"
Left (Right False)

>>> left m0BoolE $ newRefined @OZ @(Map' (ReadP Int Id) (Resplit "\\.") >> GuardBool (PrintF "bad length: found %d" Len) (Len == 4)) "141.213.1"
Left (Left "bad length: found 3")

>>> left m0BoolE $ newRefined @OZ @(Map' (ReadP Int Id) (Resplit "\\.") >> GuardBool (PrintF "bad length: found %d" Len) (Len == 4) && BoolsN (PrintT "octet %d out of range %d" Id) 4 (0 <..> 0xff)) "141.213.1.444"
Left (Left "Bool(3) [octet 3 out of range 444]")

>>> left m0BoolE $ newRefined @OZ @(Map' (ReadP Int Id) (Resplit "\\.") >> GuardBool (PrintF "bad length: found %d" Len) (Len == 4) && BoolsN (PrintT "octet %d out of range %d" Id) 4 (0 <..> 0xff)) "141.213.1x34.444"
Left (Left "ReadP Int (1x34)")

>>> newRefined @OZ @(Map ('[Id] >> ReadP Int Id) >> IsLuhn) "12344"
Right (Refined "12344")

>>> left m0BoolE $ newRefined @OZ @(Map ('[Id] >> ReadP Int Id) >> IsLuhn) "12340"
Left (Right False)

>>> newRefined @OZ @(Any IsPrime) [11,13,17,18]
Right (Refined [11,13,17,18])

>>> left m0BoolE $ newRefined @OZ @(All IsPrime) [11,13,17,18]
Left (Right False)

>>> newRefined @OZ @(Snd !! Fst >> Len > 5) (2,["abc","defghij","xyzxyazsfd"])
Right (Refined (2,["abc","defghij","xyzxyazsfd"]))

>>> left m0BoolE $ newRefined @OZ @(Snd !! Fst >> Len > 5) (27,["abc","defghij","xyzxyazsfd"])
Left (Left "(!!) index not found")

>>> left m0BoolE $ newRefined @OZ @(Snd !! Fst >> Len <= 5) (2,["abc","defghij","xyzxyazsfd"])
Left (Right False)

>>> newRefined @OU @((Id $$ 13) > 100) (\x -> x * 14) ^? _Right . to unRefined . to ($ 99)
Just 1386

newRefined' :: forall opts p a m. (MonadEval m, RefinedC opts p a) => a -> m (Either Msg0 (Refined opts p a))

returns a Refined value if a is valid for the predicate p for any MonadEval instance

QuickCheck method

genRefined :: forall opts p a. (RefinedC opts p a, HasCallStack) => Gen a -> Gen (Refined opts p a)

create Refined generator using a generator to restrict the values

unsafe create methods

unsafeRefined :: forall opts p a. a -> Refined opts p a

create an unsafe Refined value without running the predicate

unsafeRefined' :: forall opts p a. (RefinedC opts p a, HasCallStack) => a -> Refined opts p a

create an unsafe Refined value and also run the predicate