Safe Haskell	None
Language	GHC2021

Rerefined.Refine

Contents

Refined
Refined1
Errors

Synopsis

data Refined (p :: k) a
refine :: forall {k} (p :: k) a. Refine p a => a -> Either RefineFailure (Refined p a)
unrefine :: forall {k} (p :: k) a. Refined p a -> a
reifyPredicate :: forall {k} (p :: k) a. Refine p a => a -> Bool
unsafeRefine :: forall {k} a (p :: k). a -> Refined p a
unsafeRerefine :: forall {k1} {k2} (pNew :: k1) (pOld :: k2) a. Refined pOld a -> Refined pNew a
data Refined1 (p :: k) (f :: k1 -> Type) (a :: k1)
refine1 :: forall {k1} {k2} (p :: k1) f (a :: k2). Refine1 p f => f a -> Either RefineFailure (Refined1 p f a)
unrefine1 :: forall {k1} {k2} (p :: k1) f (a :: k2). Refined1 p f a -> f a
reifyPredicate1 :: forall {k} {k1} (p :: k) f (a :: k1). Refine1 p f => f a -> Bool
squashRefined1 :: forall {k1} {k2} (p :: k1) f (a :: k2). Refined1 p f a -> Refined p (f a)
unsafeRefine1 :: forall {k1} {k2} f (a :: k1) (p :: k2). f a -> Refined1 p f a
unsafeRerefine1 :: forall {k1} {k2} {k3} (pNew :: k1) (pOld :: k2) (f :: k3 -> Type) (a :: k3). Refined1 pOld f a -> Refined1 pNew f a
data RefineFailure
prettyRefineFailure :: RefineFailure -> Text
prettyRefineFailure' :: RefineFailure -> Text

`Refined`

data Refined (p :: k) a Source #

a refined with predicate p.

Instances

Instances details

Lift a => Lift (Refined p a :: Type) Source #
Instance details Defined in Rerefined.Refine Methods lift :: Quote m => Refined p a -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => Refined p a -> Code m (Refined p a) #
(Arbitrary a, Refine p a, KnownPredicateName p) => Arbitrary (Refined p a) Source #	Generate a refined term by generating an unrefined term and asserting the predicate. Will runtime error if it fails to find a satisfying term (based on size).
Instance details Defined in Rerefined.Refine Methods arbitrary :: Gen (Refined p a) # shrink :: Refined p a -> [Refined p a] #
Show a => Show (Refined p a) Source #
Instance details Defined in Rerefined.Refine Methods showsPrec :: Int -> Refined p a -> ShowS # show :: Refined p a -> String # showList :: [Refined p a] -> ShowS #
Eq a => Eq (Refined p a) Source #
Instance details Defined in Rerefined.Refine Methods (==) :: Refined p a -> Refined p a -> Bool # (/=) :: Refined p a -> Refined p a -> Bool #
Ord a => Ord (Refined p a) Source #
Instance details Defined in Rerefined.Refine Methods compare :: Refined p a -> Refined p a -> Ordering # (<) :: Refined p a -> Refined p a -> Bool # (<=) :: Refined p a -> Refined p a -> Bool # (>) :: Refined p a -> Refined p a -> Bool # (>=) :: Refined p a -> Refined p a -> Bool # max :: Refined p a -> Refined p a -> Refined p a # min :: Refined p a -> Refined p a -> Refined p a #

refine :: forall {k} (p :: k) a. Refine p a => a -> Either RefineFailure (Refined p a) Source #

Refine a with predicate p.

unrefine :: forall {k} (p :: k) a. Refined p a -> a Source #

Strip the refinement from a Refined.

This is kept as a separate function for prettier Show Refined output.

reifyPredicate :: forall {k} (p :: k) a. Refine p a => a -> Bool Source #

Reify a predicate.

unsafeRefine :: forall {k} a (p :: k). a -> Refined p a Source #

Construct a Refined without validating the predicate p.

Unsafe. Use only when you can manually prove that the predicate holds.

unsafeRerefine :: forall {k1} {k2} (pNew :: k1) (pOld :: k2) a. Refined pOld a -> Refined pNew a Source #

Replace a Refined's predicate without validating the new predicate pNew.

Unsafe. Use only when you can manually prove that the new predicate holds.

`Refined1`

data Refined1 (p :: k) (f :: k1 -> Type) (a :: k1) Source #

f a refined with predicate p.

We may derive legal Functor, Traversable instances for this as Refine1 guarantees that the predicate only applies to the functor structure. That is, you may alter a Refined1 without re-asserting its predicate, provided your changes are made without altering the structure/shape of f (e.g. fmap, traverse).

Instances

Instances details

Lift (f a) => Lift (Refined1 p f a :: Type) Source #
Instance details Defined in Rerefined.Refine Methods lift :: Quote m => Refined1 p f a -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => Refined1 p f a -> Code m (Refined1 p f a) #
Foldable f => Foldable (Refined1 p f) Source #
Instance details Defined in Rerefined.Refine Methods fold :: Monoid m => Refined1 p f m -> m # foldMap :: Monoid m => (a -> m) -> Refined1 p f a -> m # foldMap' :: Monoid m => (a -> m) -> Refined1 p f a -> m # foldr :: (a -> b -> b) -> b -> Refined1 p f a -> b # foldr' :: (a -> b -> b) -> b -> Refined1 p f a -> b # foldl :: (b -> a -> b) -> b -> Refined1 p f a -> b # foldl' :: (b -> a -> b) -> b -> Refined1 p f a -> b # foldr1 :: (a -> a -> a) -> Refined1 p f a -> a # foldl1 :: (a -> a -> a) -> Refined1 p f a -> a # toList :: Refined1 p f a -> [a] # null :: Refined1 p f a -> Bool # length :: Refined1 p f a -> Int # elem :: Eq a => a -> Refined1 p f a -> Bool # maximum :: Ord a => Refined1 p f a -> a # minimum :: Ord a => Refined1 p f a -> a # sum :: Num a => Refined1 p f a -> a # product :: Num a => Refined1 p f a -> a #
Traversable f => Traversable (Refined1 p f) Source #
Instance details Defined in Rerefined.Refine Methods traverse :: Applicative f0 => (a -> f0 b) -> Refined1 p f a -> f0 (Refined1 p f b) # sequenceA :: Applicative f0 => Refined1 p f (f0 a) -> f0 (Refined1 p f a) # mapM :: Monad m => (a -> m b) -> Refined1 p f a -> m (Refined1 p f b) # sequence :: Monad m => Refined1 p f (m a) -> m (Refined1 p f a) #
Functor f => Functor (Refined1 p f) Source #
Instance details Defined in Rerefined.Refine Methods fmap :: (a -> b) -> Refined1 p f a -> Refined1 p f b # (<$) :: a -> Refined1 p f b -> Refined1 p f a #
(Arbitrary (f a), Refine1 p f, KnownPredicateName p) => Arbitrary (Refined1 p f a) Source #	Generate a refined term by generating an unrefined term and asserting the functor predicate. Will runtime error if it fails to find a satisfying term (based on size).
Instance details Defined in Rerefined.Refine Methods arbitrary :: Gen (Refined1 p f a) # shrink :: Refined1 p f a -> [Refined1 p f a] #
Show (f a) => Show (Refined1 p f a) Source #
Instance details Defined in Rerefined.Refine Methods showsPrec :: Int -> Refined1 p f a -> ShowS # show :: Refined1 p f a -> String # showList :: [Refined1 p f a] -> ShowS #
Eq (f a) => Eq (Refined1 p f a) Source #
Instance details Defined in Rerefined.Refine Methods (==) :: Refined1 p f a -> Refined1 p f a -> Bool # (/=) :: Refined1 p f a -> Refined1 p f a -> Bool #
Ord (f a) => Ord (Refined1 p f a) Source #
Instance details Defined in Rerefined.Refine Methods compare :: Refined1 p f a -> Refined1 p f a -> Ordering # (<) :: Refined1 p f a -> Refined1 p f a -> Bool # (<=) :: Refined1 p f a -> Refined1 p f a -> Bool # (>) :: Refined1 p f a -> Refined1 p f a -> Bool # (>=) :: Refined1 p f a -> Refined1 p f a -> Bool # max :: Refined1 p f a -> Refined1 p f a -> Refined1 p f a # min :: Refined1 p f a -> Refined1 p f a -> Refined1 p f a #

refine1 :: forall {k1} {k2} (p :: k1) f (a :: k2). Refine1 p f => f a -> Either RefineFailure (Refined1 p f a) Source #

Refine f a with functor predicate p.

unrefine1 :: forall {k1} {k2} (p :: k1) f (a :: k2). Refined1 p f a -> f a Source #

Strip the refinement from a Refined1.

This is kept as a separate function for prettier Show Refined1 output.

reifyPredicate1 :: forall {k} {k1} (p :: k) f (a :: k1). Refine1 p f => f a -> Bool Source #

Reify a functor predicate.

squashRefined1 :: forall {k1} {k2} (p :: k1) f (a :: k2). Refined1 p f a -> Refined p (f a) Source #

Squash a Refined1 into a Refined. Essentially forget the f.

unsafeRefine1 :: forall {k1} {k2} f (a :: k1) (p :: k2). f a -> Refined1 p f a Source #

Construct a Refined1 without validating the predicate p.

Unsafe. Use only when you can manually prove that the predicate holds.

unsafeRerefine1 :: forall {k1} {k2} {k3} (pNew :: k1) (pOld :: k2) (f :: k3 -> Type) (a :: k3). Refined1 pOld f a -> Refined1 pNew f a Source #

Replace a Refined1's predicate without validating the new predicate pNew.

Unsafe. Use only when you can manually prove that the new predicate holds.

Errors

data RefineFailure Source #

Predicate validation failure.

Instances

Instances details

Show RefineFailure Source #
Instance details Defined in Rerefined.Predicate Methods showsPrec :: Int -> RefineFailure -> ShowS # show :: RefineFailure -> String # showList :: [RefineFailure] -> ShowS #

prettyRefineFailure :: RefineFailure -> Text Source #

prettyRefineFailure' :: RefineFailure -> Text Source #