module Refined
(
Refined,
refine,
refineTH,
unrefine,
Predicate(..),
Not,
And,
Or,
LessThan,
GreaterThan,
From,
To,
FromTo,
EqualTo,
Positive,
NonPositive,
Negative,
NonNegative,
ZeroToOne,
)
where
import BasePrelude
import GHC.TypeLits
import qualified Language.Haskell.TH.Syntax as TH
newtype Refined p x =
Refined x
deriving (Show, Eq, Ord, Typeable, Data, Generic)
instance (Read x, Predicate p x) => Read (Refined p x) where
readsPrec d =
readParen (d > 10) $ \r1 -> do
("Refined", r2) <- lex r1
(raw, r3) <- readsPrec 11 r2
case refine raw of
Right val -> [(val, r3)]
Left _ -> []
instance TH.Lift x => TH.Lift (Refined p x) where
lift (Refined a) =
[|Refined a|]
refine :: Predicate p x => x -> Either String (Refined p x)
refine x =
fix $ \result ->
maybe (Right (Refined x)) Left $
validate (predicateByResult result) x
where
predicateByResult :: Either String (Refined p x) -> p
predicateByResult =
const undefined
refineTH :: (Predicate p x, TH.Lift x) => x -> TH.Q (TH.TExp (Refined p x))
refineTH =
fix $ \loop ->
fmap TH.TExp . either fail TH.lift . refineByResult (loop undefined)
where
refineByResult :: Predicate p x => TH.Q (TH.TExp (Refined p x)) -> x -> Either String (Refined p x)
refineByResult =
const refine
unrefine :: Refined p x -> x
unrefine =
unsafeCoerce
class Predicate p x where
validate :: p -> x -> Maybe String
data Not r
instance Predicate r x => Predicate (Not r) x where
validate _ =
maybe (Just "A subpredicate didn't fail") (const Nothing) .
validate (undefined :: r)
data And l r
instance (Predicate l x, Predicate r x) => Predicate (And l r) x where
validate _ x =
fmap (showString "The left subpredicate failed with: ")
(validate (undefined :: l) x)
<|>
fmap (showString "The right subpredicate failed with: ")
(validate (undefined :: r) x)
data Or l r
instance (Predicate l x, Predicate r x) => Predicate (Or l r) x where
validate _ x =
case (validate (undefined :: l) x, validate (undefined :: r) x) of
(Just a, Just b) ->
Just $ "Both subpredicates failed. First with: " <> a <> ". Second with: " <> b <> "."
_ ->
Nothing
data LessThan (n :: Nat)
instance (Ord x, Num x, KnownNat n) => Predicate (LessThan n) x where
validate p x =
if x < fromIntegral x'
then Nothing
else Just ("Value is not less than " <> show x')
where
x' = natVal p
data GreaterThan (n :: Nat)
instance (Ord x, Num x, KnownNat n) => Predicate (GreaterThan n) x where
validate p x =
if x > fromIntegral x'
then Nothing
else Just ("Value is not greater than " <> show x')
where
x' = natVal p
data From (n :: Nat)
instance (Ord x, Num x, KnownNat n) => Predicate (From n) x where
validate p x =
if x >= fromIntegral x'
then Nothing
else Just ("Value is less than " <> show x')
where
x' = natVal p
data To (n :: Nat)
instance (Ord x, Num x, KnownNat n) => Predicate (To n) x where
validate p x =
if x <= fromIntegral x'
then Nothing
else Just ("Value is greater than " <> show x')
where
x' = natVal p
data FromTo (mn :: Nat) (mx :: Nat)
instance (Ord x, Num x, KnownNat mn, KnownNat mx, mn <= mx) => Predicate (FromTo mn mx) x where
validate p x =
if x >= fromIntegral mn' && x <= fromIntegral mx'
then Nothing
else Just ("Value is out of range (minimum: " <> show mn' <> ", maximum: " <> show mx' <> ")")
where
mn' = natVal (Proxy :: Proxy mn)
mx' = natVal (Proxy :: Proxy mx)
data EqualTo (n :: Nat)
instance (Ord x, Num x, KnownNat n) => Predicate (EqualTo n) x where
validate p x =
if x == fromIntegral x'
then Nothing
else Just ("Value does not equal " <> show x')
where
x' = natVal p
type Positive =
GreaterThan 0
type NonPositive =
To 0
type Negative =
LessThan 0
type NonNegative =
From 0
type ZeroToOne =
FromTo 0 1