-- | 'Refined' and 'Refined1' definitions for refined values.
--
-- Not intended for external use. For unsafe refining, use
-- 'Rerefined.Refine.Unsafe'.

module Rerefined.Refined
  (
  -- * @Refined@
    Refined(..)
  , unrefine

  -- * @Refined1@
  , Refined1(..)
  , unrefine1
  , squashRefined1
  ) where

import Language.Haskell.TH.Syntax ( Lift )

-- | @a@ refined with predicate @p@.
newtype Refined p a = Refined a
    deriving stock ((forall (m :: Type -> Type). Quote m => Refined p a -> m Exp)
-> (forall (m :: Type -> Type).
    Quote m =>
    Refined p a -> Code m (Refined p a))
-> Lift (Refined p a)
forall k (p :: k) a (m :: Type -> Type).
(Lift a, Quote m) =>
Refined p a -> m Exp
forall k (p :: k) a (m :: Type -> Type).
(Lift a, Quote m) =>
Refined p a -> Code m (Refined p a)
forall t.
(forall (m :: Type -> Type). Quote m => t -> m Exp)
-> (forall (m :: Type -> Type). Quote m => t -> Code m t) -> Lift t
forall (m :: Type -> Type). Quote m => Refined p a -> m Exp
forall (m :: Type -> Type).
Quote m =>
Refined p a -> Code m (Refined p a)
$clift :: forall k (p :: k) a (m :: Type -> Type).
(Lift a, Quote m) =>
Refined p a -> m Exp
lift :: forall (m :: Type -> Type). Quote m => Refined p a -> m Exp
$cliftTyped :: forall k (p :: k) a (m :: Type -> Type).
(Lift a, Quote m) =>
Refined p a -> Code m (Refined p a)
liftTyped :: forall (m :: Type -> Type).
Quote m =>
Refined p a -> Code m (Refined p a)
Lift, Int -> Refined p a -> ShowS
[Refined p a] -> ShowS
Refined p a -> String
(Int -> Refined p a -> ShowS)
-> (Refined p a -> String)
-> ([Refined p a] -> ShowS)
-> Show (Refined p a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) a. Show a => Int -> Refined p a -> ShowS
forall k (p :: k) a. Show a => [Refined p a] -> ShowS
forall k (p :: k) a. Show a => Refined p a -> String
$cshowsPrec :: forall k (p :: k) a. Show a => Int -> Refined p a -> ShowS
showsPrec :: Int -> Refined p a -> ShowS
$cshow :: forall k (p :: k) a. Show a => Refined p a -> String
show :: Refined p a -> String
$cshowList :: forall k (p :: k) a. Show a => [Refined p a] -> ShowS
showList :: [Refined p a] -> ShowS
Show)

-- | Strip the refinement from a 'Refined'.
--
-- This is kept as a separate function for prettier @'Show' 'Refined'@ output.
unrefine :: Refined p a -> a
unrefine :: forall {k} (p :: k) a. Refined p a -> a
unrefine (Refined a
a) = a
a

-- | @f a@ refined with predicate @p@.
--
-- We may derive legal 'Functor', 'Traversable' instances for this as
-- 'Rerefined.Predicate.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').
newtype Refined1 p f a = Refined1 (f a)
    deriving stock ((forall a b. (a -> b) -> Refined1 p f a -> Refined1 p f b)
-> (forall a b. a -> Refined1 p f b -> Refined1 p f a)
-> Functor (Refined1 p f)
forall k (p :: k) (f :: Type -> Type) a b.
Functor f =>
a -> Refined1 p f b -> Refined1 p f a
forall k (p :: k) (f :: Type -> Type) a b.
Functor f =>
(a -> b) -> Refined1 p f a -> Refined1 p f b
forall a b. a -> Refined1 p f b -> Refined1 p f a
forall a b. (a -> b) -> Refined1 p f a -> Refined1 p f b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall k (p :: k) (f :: Type -> Type) a b.
Functor f =>
(a -> b) -> Refined1 p f a -> Refined1 p f b
fmap :: forall a b. (a -> b) -> Refined1 p f a -> Refined1 p f b
$c<$ :: forall k (p :: k) (f :: Type -> Type) a b.
Functor f =>
a -> Refined1 p f b -> Refined1 p f a
<$ :: forall a b. a -> Refined1 p f b -> Refined1 p f a
Functor, (forall m. Monoid m => Refined1 p f m -> m)
-> (forall m a. Monoid m => (a -> m) -> Refined1 p f a -> m)
-> (forall m a. Monoid m => (a -> m) -> Refined1 p f a -> m)
-> (forall a b. (a -> b -> b) -> b -> Refined1 p f a -> b)
-> (forall a b. (a -> b -> b) -> b -> Refined1 p f a -> b)
-> (forall b a. (b -> a -> b) -> b -> Refined1 p f a -> b)
-> (forall b a. (b -> a -> b) -> b -> Refined1 p f a -> b)
-> (forall a. (a -> a -> a) -> Refined1 p f a -> a)
-> (forall a. (a -> a -> a) -> Refined1 p f a -> a)
-> (forall a. Refined1 p f a -> [a])
-> (forall a. Refined1 p f a -> Bool)
-> (forall a. Refined1 p f a -> Int)
-> (forall a. Eq a => a -> Refined1 p f a -> Bool)
-> (forall a. Ord a => Refined1 p f a -> a)
-> (forall a. Ord a => Refined1 p f a -> a)
-> (forall a. Num a => Refined1 p f a -> a)
-> (forall a. Num a => Refined1 p f a -> a)
-> Foldable (Refined1 p f)
forall a. Eq a => a -> Refined1 p f a -> Bool
forall a. Num a => Refined1 p f a -> a
forall a. Ord a => Refined1 p f a -> a
forall m. Monoid m => Refined1 p f m -> m
forall a. Refined1 p f a -> Bool
forall a. Refined1 p f a -> Int
forall a. Refined1 p f a -> [a]
forall a. (a -> a -> a) -> Refined1 p f a -> a
forall k (p :: k) (f :: Type -> Type) a.
(Foldable f, Eq a) =>
a -> Refined1 p f a -> Bool
forall k (p :: k) (f :: Type -> Type) a.
(Foldable f, Num a) =>
Refined1 p f a -> a
forall k (p :: k) (f :: Type -> Type) a.
(Foldable f, Ord a) =>
Refined1 p f a -> a
forall k (p :: k) (f :: Type -> Type) m.
(Foldable f, Monoid m) =>
Refined1 p f m -> m
forall k (p :: k) (f :: Type -> Type) a.
Foldable f =>
Refined1 p f a -> Bool
forall k (p :: k) (f :: Type -> Type) a.
Foldable f =>
Refined1 p f a -> Int
forall k (p :: k) (f :: Type -> Type) a.
Foldable f =>
Refined1 p f a -> [a]
forall k (p :: k) (f :: Type -> Type) a.
Foldable f =>
(a -> a -> a) -> Refined1 p f a -> a
forall k (p :: k) (f :: Type -> Type) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Refined1 p f a -> m
forall k (p :: k) (f :: Type -> Type) b a.
Foldable f =>
(b -> a -> b) -> b -> Refined1 p f a -> b
forall k (p :: k) (f :: Type -> Type) a b.
Foldable f =>
(a -> b -> b) -> b -> Refined1 p f a -> b
forall m a. Monoid m => (a -> m) -> Refined1 p f a -> m
forall b a. (b -> a -> b) -> b -> Refined1 p f a -> b
forall a b. (a -> b -> b) -> b -> Refined1 p f a -> b
forall (t :: Type -> Type).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall k (p :: k) (f :: Type -> Type) m.
(Foldable f, Monoid m) =>
Refined1 p f m -> m
fold :: forall m. Monoid m => Refined1 p f m -> m
$cfoldMap :: forall k (p :: k) (f :: Type -> Type) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Refined1 p f a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Refined1 p f a -> m
$cfoldMap' :: forall k (p :: k) (f :: Type -> Type) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Refined1 p f a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Refined1 p f a -> m
$cfoldr :: forall k (p :: k) (f :: Type -> Type) a b.
Foldable f =>
(a -> b -> b) -> b -> Refined1 p f a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Refined1 p f a -> b
$cfoldr' :: forall k (p :: k) (f :: Type -> Type) a b.
Foldable f =>
(a -> b -> b) -> b -> Refined1 p f a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Refined1 p f a -> b
$cfoldl :: forall k (p :: k) (f :: Type -> Type) b a.
Foldable f =>
(b -> a -> b) -> b -> Refined1 p f a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Refined1 p f a -> b
$cfoldl' :: forall k (p :: k) (f :: Type -> Type) b a.
Foldable f =>
(b -> a -> b) -> b -> Refined1 p f a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Refined1 p f a -> b
$cfoldr1 :: forall k (p :: k) (f :: Type -> Type) a.
Foldable f =>
(a -> a -> a) -> Refined1 p f a -> a
foldr1 :: forall a. (a -> a -> a) -> Refined1 p f a -> a
$cfoldl1 :: forall k (p :: k) (f :: Type -> Type) a.
Foldable f =>
(a -> a -> a) -> Refined1 p f a -> a
foldl1 :: forall a. (a -> a -> a) -> Refined1 p f a -> a
$ctoList :: forall k (p :: k) (f :: Type -> Type) a.
Foldable f =>
Refined1 p f a -> [a]
toList :: forall a. Refined1 p f a -> [a]
$cnull :: forall k (p :: k) (f :: Type -> Type) a.
Foldable f =>
Refined1 p f a -> Bool
null :: forall a. Refined1 p f a -> Bool
$clength :: forall k (p :: k) (f :: Type -> Type) a.
Foldable f =>
Refined1 p f a -> Int
length :: forall a. Refined1 p f a -> Int
$celem :: forall k (p :: k) (f :: Type -> Type) a.
(Foldable f, Eq a) =>
a -> Refined1 p f a -> Bool
elem :: forall a. Eq a => a -> Refined1 p f a -> Bool
$cmaximum :: forall k (p :: k) (f :: Type -> Type) a.
(Foldable f, Ord a) =>
Refined1 p f a -> a
maximum :: forall a. Ord a => Refined1 p f a -> a
$cminimum :: forall k (p :: k) (f :: Type -> Type) a.
(Foldable f, Ord a) =>
Refined1 p f a -> a
minimum :: forall a. Ord a => Refined1 p f a -> a
$csum :: forall k (p :: k) (f :: Type -> Type) a.
(Foldable f, Num a) =>
Refined1 p f a -> a
sum :: forall a. Num a => Refined1 p f a -> a
$cproduct :: forall k (p :: k) (f :: Type -> Type) a.
(Foldable f, Num a) =>
Refined1 p f a -> a
product :: forall a. Num a => Refined1 p f a -> a
Foldable, Functor (Refined1 p f)
Foldable (Refined1 p f)
(Functor (Refined1 p f), Foldable (Refined1 p f)) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> Refined1 p f a -> f (Refined1 p f b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    Refined1 p f (f a) -> f (Refined1 p f a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> Refined1 p f a -> m (Refined1 p f b))
-> (forall (m :: Type -> Type) a.
    Monad m =>
    Refined1 p f (m a) -> m (Refined1 p f a))
-> Traversable (Refined1 p f)
forall k (p :: k) (f :: Type -> Type).
Traversable f =>
Functor (Refined1 p f)
forall k (p :: k) (f :: Type -> Type).
Traversable f =>
Foldable (Refined1 p f)
forall k (p :: k) (f :: Type -> Type) (m :: Type -> Type) a.
(Traversable f, Monad m) =>
Refined1 p f (m a) -> m (Refined1 p f a)
forall k (p :: k) (f :: Type -> Type) (f :: Type -> Type) a.
(Traversable f, Applicative f) =>
Refined1 p f (f a) -> f (Refined1 p f a)
forall k (p :: k) (f :: Type -> Type) (m :: Type -> Type) a b.
(Traversable f, Monad m) =>
(a -> m b) -> Refined1 p f a -> m (Refined1 p f b)
forall k (p :: k) (f :: Type -> Type) (f :: Type -> Type) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> Refined1 p f a -> f (Refined1 p f b)
forall (t :: Type -> Type).
(Functor t, Foldable t) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    t (f a) -> f (t a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: Type -> Type) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: Type -> Type) a.
Monad m =>
Refined1 p f (m a) -> m (Refined1 p f a)
forall (f :: Type -> Type) a.
Applicative f =>
Refined1 p f (f a) -> f (Refined1 p f a)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Refined1 p f a -> m (Refined1 p f b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Refined1 p f a -> f (Refined1 p f b)
$ctraverse :: forall k (p :: k) (f :: Type -> Type) (f :: Type -> Type) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> Refined1 p f a -> f (Refined1 p f b)
traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Refined1 p f a -> f (Refined1 p f b)
$csequenceA :: forall k (p :: k) (f :: Type -> Type) (f :: Type -> Type) a.
(Traversable f, Applicative f) =>
Refined1 p f (f a) -> f (Refined1 p f a)
sequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
Refined1 p f (f a) -> f (Refined1 p f a)
$cmapM :: forall k (p :: k) (f :: Type -> Type) (m :: Type -> Type) a b.
(Traversable f, Monad m) =>
(a -> m b) -> Refined1 p f a -> m (Refined1 p f b)
mapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Refined1 p f a -> m (Refined1 p f b)
$csequence :: forall k (p :: k) (f :: Type -> Type) (m :: Type -> Type) a.
(Traversable f, Monad m) =>
Refined1 p f (m a) -> m (Refined1 p f a)
sequence :: forall (m :: Type -> Type) a.
Monad m =>
Refined1 p f (m a) -> m (Refined1 p f a)
Traversable, (forall (m :: Type -> Type). Quote m => Refined1 p f a -> m Exp)
-> (forall (m :: Type -> Type).
    Quote m =>
    Refined1 p f a -> Code m (Refined1 p f a))
-> Lift (Refined1 p f a)
forall k (p :: k) k (f :: k -> Type) (a :: k) (m :: Type -> Type).
(Lift (f a), Quote m) =>
Refined1 p f a -> m Exp
forall k (p :: k) k (f :: k -> Type) (a :: k) (m :: Type -> Type).
(Lift (f a), Quote m) =>
Refined1 p f a -> Code m (Refined1 p f a)
forall t.
(forall (m :: Type -> Type). Quote m => t -> m Exp)
-> (forall (m :: Type -> Type). Quote m => t -> Code m t) -> Lift t
forall (m :: Type -> Type). Quote m => Refined1 p f a -> m Exp
forall (m :: Type -> Type).
Quote m =>
Refined1 p f a -> Code m (Refined1 p f a)
$clift :: forall k (p :: k) k (f :: k -> Type) (a :: k) (m :: Type -> Type).
(Lift (f a), Quote m) =>
Refined1 p f a -> m Exp
lift :: forall (m :: Type -> Type). Quote m => Refined1 p f a -> m Exp
$cliftTyped :: forall k (p :: k) k (f :: k -> Type) (a :: k) (m :: Type -> Type).
(Lift (f a), Quote m) =>
Refined1 p f a -> Code m (Refined1 p f a)
liftTyped :: forall (m :: Type -> Type).
Quote m =>
Refined1 p f a -> Code m (Refined1 p f a)
Lift, Int -> Refined1 p f a -> ShowS
[Refined1 p f a] -> ShowS
Refined1 p f a -> String
(Int -> Refined1 p f a -> ShowS)
-> (Refined1 p f a -> String)
-> ([Refined1 p f a] -> ShowS)
-> Show (Refined1 p f a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (f :: k -> Type) (a :: k).
Show (f a) =>
Int -> Refined1 p f a -> ShowS
forall k (p :: k) k (f :: k -> Type) (a :: k).
Show (f a) =>
[Refined1 p f a] -> ShowS
forall k (p :: k) k (f :: k -> Type) (a :: k).
Show (f a) =>
Refined1 p f a -> String
$cshowsPrec :: forall k (p :: k) k (f :: k -> Type) (a :: k).
Show (f a) =>
Int -> Refined1 p f a -> ShowS
showsPrec :: Int -> Refined1 p f a -> ShowS
$cshow :: forall k (p :: k) k (f :: k -> Type) (a :: k).
Show (f a) =>
Refined1 p f a -> String
show :: Refined1 p f a -> String
$cshowList :: forall k (p :: k) k (f :: k -> Type) (a :: k).
Show (f a) =>
[Refined1 p f a] -> ShowS
showList :: [Refined1 p f a] -> ShowS
Show)

-- | Strip the refinement from a 'Refined1'.
--
-- This is kept as a separate function for prettier @'Show' 'Refined1'@ output.
unrefine1 :: Refined1 p f a -> f a
unrefine1 :: forall {k} {k} (p :: k) (f :: k -> Type) (a :: k).
Refined1 p f a -> f a
unrefine1 (Refined1 f a
fa) = f a
fa

-- | Squash a 'Refined1' into a 'Refined'. Essentially forget the @f@.
squashRefined1 :: Refined1 p f a -> Refined p (f a)
squashRefined1 :: forall {k} {k} (p :: k) (f :: k -> Type) (a :: k).
Refined1 p f a -> Refined p (f a)
squashRefined1 = f a -> Refined p (f a)
forall {k} (p :: k) a. a -> Refined p a
Refined (f a -> Refined p (f a))
-> (Refined1 p f a -> f a) -> Refined1 p f a -> Refined p (f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined1 p f a -> f a
forall {k} {k} (p :: k) (f :: k -> Type) (a :: k).
Refined1 p f a -> f a
unrefine1