Rerefined.Refine

Refined

data Refined p a

a refined with predicate p.

Instances

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

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)

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

Defined in Rerefined.Refine

Methods

arbitrary :: Gen (Refined p a)

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

Show a => Show (Refined p a)

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)

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)

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 p a. Refine p a => a -> Either RefineFailure (Refined p a)

Refine a with predicate p.

unrefine :: Refined p a -> a

Strip the refinement from a Refined.

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

reifyPredicate :: forall p a. Refine p a => a -> Bool

Reify a predicate.

unsafeRefine :: a -> Refined p a

Construct a Refined without validating the predicate p.

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

unsafeRerefine :: forall pNew pOld a. Refined pOld a -> Refined pNew a

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

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

Refined1

data Refined1 p f a

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

Lift (f a) => Lift (Refined1 p f a :: Type)

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)

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)

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)

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)

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

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)

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)

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)

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 p f a. Refine1 p f => f a -> Either RefineFailure (Refined1 p f a)

Refine f a with functor predicate p.

unrefine1 :: Refined1 p f a -> f a

Strip the refinement from a Refined1.

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

reifyPredicate1 :: forall p f a. Refine1 p f => f a -> Bool

Reify a functor predicate.

squashRefined1 :: Refined1 p f a -> Refined p (f a)

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

unsafeRefine1 :: f a -> Refined1 p f a

Construct a Refined1 without validating the predicate p.

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

unsafeRerefine1 :: forall pNew pOld f a. Refined1 pOld f a -> Refined1 pNew f a

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

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

Errors

data RefineFailure

Predicate validation failure.

Instances

Show RefineFailure

Defined in Rerefined.Predicate

Methods

showsPrec :: Int -> RefineFailure -> ShowS

show :: RefineFailure -> String

showList :: [RefineFailure] -> ShowS

prettyRefineFailure :: RefineFailure -> Text

prettyRefineFailure' :: RefineFailure -> Text