{-# LANGUAGE AllowAmbiguousTypes #-} -- for predicate reification
{-# LANGUAGE UndecidableInstances #-} -- for KnownPredicateName in Arbitrary

module Rerefined.Refine
  (
  -- * @Refined@
    type Refined
  , refine
  , unrefine
  , reifyPredicate
  , unsafeRefine
  , unsafeRerefine

  -- * @Refined1@
  , type Refined1
  , refine1
  , unrefine1
  , reifyPredicate1
  , squashRefined1
  , unsafeRefine1
  , unsafeRerefine1

  -- * Errors
  , type RefineFailure
  , prettyRefineFailure
  , prettyRefineFailure'
  ) where

import Rerefined.Predicate
import Language.Haskell.TH.Syntax ( Lift )
import GHC.Exts ( proxy# )
import Data.Text ( Text )
import Data.Text.Builder.Linear qualified as TBL

import Test.QuickCheck ( Arbitrary(arbitrary) )
import Test.QuickCheck.Gen qualified as QC

-- | @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, Refined p a -> Refined p a -> Bool
(Refined p a -> Refined p a -> Bool)
-> (Refined p a -> Refined p a -> Bool) -> Eq (Refined p a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (p :: k) a. Eq a => Refined p a -> Refined p a -> Bool
$c== :: forall k (p :: k) a. Eq a => Refined p a -> Refined p a -> Bool
== :: Refined p a -> Refined p a -> Bool
$c/= :: forall k (p :: k) a. Eq a => Refined p a -> Refined p a -> Bool
/= :: Refined p a -> Refined p a -> Bool
Eq, Eq (Refined p a)
Eq (Refined p a) =>
(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)
-> (Refined p a -> Refined p a -> Refined p a)
-> (Refined p a -> Refined p a -> Refined p a)
-> Ord (Refined p a)
Refined p a -> Refined p a -> Bool
Refined p a -> Refined p a -> Ordering
Refined p a -> Refined p a -> Refined p a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (p :: k) a. Ord a => Eq (Refined p a)
forall k (p :: k) a. Ord a => Refined p a -> Refined p a -> Bool
forall k (p :: k) a.
Ord a =>
Refined p a -> Refined p a -> Ordering
forall k (p :: k) a.
Ord a =>
Refined p a -> Refined p a -> Refined p a
$ccompare :: forall k (p :: k) a.
Ord a =>
Refined p a -> Refined p a -> Ordering
compare :: Refined p a -> Refined p a -> Ordering
$c< :: forall k (p :: k) a. Ord a => Refined p a -> Refined p a -> Bool
< :: Refined p a -> Refined p a -> Bool
$c<= :: forall k (p :: k) a. Ord a => Refined p a -> Refined p a -> Bool
<= :: Refined p a -> Refined p a -> Bool
$c> :: forall k (p :: k) a. Ord a => Refined p a -> Refined p a -> Bool
> :: Refined p a -> Refined p a -> Bool
$c>= :: forall k (p :: k) a. Ord a => Refined p a -> Refined p a -> Bool
>= :: Refined p a -> Refined p a -> Bool
$cmax :: forall k (p :: k) a.
Ord a =>
Refined p a -> Refined p a -> Refined p a
max :: Refined p a -> Refined p a -> Refined p a
$cmin :: forall k (p :: k) a.
Ord a =>
Refined p a -> Refined p a -> Refined p a
min :: Refined p a -> Refined p a -> Refined p a
Ord, 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, 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)
-> Eq (Refined1 p f a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (p :: k) k (f :: k -> Type) (a :: k).
Eq (f a) =>
Refined1 p f a -> Refined1 p f a -> Bool
$c== :: forall k (p :: k) k (f :: k -> Type) (a :: k).
Eq (f a) =>
Refined1 p f a -> Refined1 p f a -> Bool
== :: Refined1 p f a -> Refined1 p f a -> Bool
$c/= :: forall k (p :: k) k (f :: k -> Type) (a :: k).
Eq (f a) =>
Refined1 p f a -> Refined1 p f a -> Bool
/= :: Refined1 p f a -> Refined1 p f a -> Bool
Eq, Eq (Refined1 p f a)
Eq (Refined1 p f a) =>
(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)
-> (Refined1 p f a -> Refined1 p f a -> Refined1 p f a)
-> (Refined1 p f a -> Refined1 p f a -> Refined1 p f a)
-> Ord (Refined1 p f a)
Refined1 p f a -> Refined1 p f a -> Bool
Refined1 p f a -> Refined1 p f a -> Ordering
Refined1 p f a -> Refined1 p f a -> Refined1 p f a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (p :: k) k (f :: k -> Type) (a :: k).
Ord (f a) =>
Eq (Refined1 p f a)
forall k (p :: k) k (f :: k -> Type) (a :: k).
Ord (f a) =>
Refined1 p f a -> Refined1 p f a -> Bool
forall k (p :: k) k (f :: k -> Type) (a :: k).
Ord (f a) =>
Refined1 p f a -> Refined1 p f a -> Ordering
forall k (p :: k) k (f :: k -> Type) (a :: k).
Ord (f a) =>
Refined1 p f a -> Refined1 p f a -> Refined1 p f a
$ccompare :: forall k (p :: k) k (f :: k -> Type) (a :: k).
Ord (f a) =>
Refined1 p f a -> Refined1 p f a -> Ordering
compare :: Refined1 p f a -> Refined1 p f a -> Ordering
$c< :: forall k (p :: k) k (f :: k -> Type) (a :: k).
Ord (f a) =>
Refined1 p f a -> Refined1 p f a -> Bool
< :: Refined1 p f a -> Refined1 p f a -> Bool
$c<= :: forall k (p :: k) k (f :: k -> Type) (a :: k).
Ord (f a) =>
Refined1 p f a -> Refined1 p f a -> Bool
<= :: Refined1 p f a -> Refined1 p f a -> Bool
$c> :: forall k (p :: k) k (f :: k -> Type) (a :: k).
Ord (f a) =>
Refined1 p f a -> Refined1 p f a -> Bool
> :: Refined1 p f a -> Refined1 p f a -> Bool
$c>= :: forall k (p :: k) k (f :: k -> Type) (a :: k).
Ord (f a) =>
Refined1 p f a -> Refined1 p f a -> Bool
>= :: Refined1 p f a -> Refined1 p f a -> Bool
$cmax :: forall k (p :: k) k (f :: k -> Type) (a :: k).
Ord (f a) =>
Refined1 p f a -> Refined1 p f a -> Refined1 p f a
max :: Refined1 p f a -> Refined1 p f a -> Refined1 p f a
$cmin :: forall k (p :: k) k (f :: k -> Type) (a :: k).
Ord (f a) =>
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
Ord, 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

-- | Refine @a@ with predicate @p@.
refine
    :: forall p a. Refine p a
    => a -> Either RefineFailure (Refined p a)
refine :: forall {k} (p :: k) a.
Refine p a =>
a -> Either RefineFailure (Refined p a)
refine a
a =
    case Proxy# p -> a -> Maybe RefineFailure
forall {k} (p :: k) a.
Refine p a =>
Proxy# p -> a -> Maybe RefineFailure
validate (forall (a :: k). Proxy# a
forall {k} (a :: k). Proxy# a
proxy# @p) a
a of
      Maybe RefineFailure
Nothing -> Refined p a -> Either RefineFailure (Refined p a)
forall a b. b -> Either a b
Right (a -> Refined p a
forall {k} (p :: k) a. a -> Refined p a
Refined a
a)
      Just RefineFailure
e  -> RefineFailure -> Either RefineFailure (Refined p a)
forall a b. a -> Either a b
Left RefineFailure
e

-- | Construct a 'Refined' without validating the predicate @p@.
--
-- Unsafe. Use only when you can manually prove that the predicate holds.
unsafeRefine :: a -> Refined p a
unsafeRefine :: forall {k} a (p :: k). a -> Refined p a
unsafeRefine = a -> Refined p a
forall {k} (p :: k) a. a -> Refined p a
Refined

-- | Replace a 'Refined''s predicate without validating the new predicate
--   @pNew@.
--
-- Unsafe. Use only when you can manually prove that the new predicate holds.
unsafeRerefine :: forall pNew pOld a. Refined pOld a -> Refined pNew a
unsafeRerefine :: forall {k} {k} (pNew :: k) (pOld :: k) a.
Refined pOld a -> Refined pNew a
unsafeRerefine = a -> Refined pNew a
forall {k} (p :: k) a. a -> Refined p a
Refined (a -> Refined pNew a)
-> (Refined pOld a -> a) -> Refined pOld a -> Refined pNew a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined pOld a -> a
forall {k} (p :: k) a. Refined p a -> a
unrefine

-- | Reify a predicate.
reifyPredicate :: forall p a. Refine p a => a -> Bool
reifyPredicate :: forall {k} (p :: k) a. Refine p a => a -> Bool
reifyPredicate a
a = case forall (p :: k) a.
Refine p a =>
a -> Either RefineFailure (Refined p a)
forall {k} (p :: k) a.
Refine p a =>
a -> Either RefineFailure (Refined p a)
refine @p a
a of Right{} -> Bool
True; Left{} -> Bool
False

-- | Refine @f a@ with functor predicate @p@.
refine1
    :: forall p f a. Refine1 p f
    => f a -> Either RefineFailure (Refined1 p f a)
refine1 :: forall {k} {k} (p :: k) (f :: k -> Type) (a :: k).
Refine1 p f =>
f a -> Either RefineFailure (Refined1 p f a)
refine1 f a
fa =
    case Proxy# p -> f a -> Maybe RefineFailure
forall (a :: k). Proxy# p -> f a -> Maybe RefineFailure
forall {k} {k1} (p :: k) (f :: k1 -> Type) (a :: k1).
Refine1 p f =>
Proxy# p -> f a -> Maybe RefineFailure
validate1 (forall (a :: k). Proxy# a
forall {k} (a :: k). Proxy# a
proxy# @p) f a
fa of
      Maybe RefineFailure
Nothing -> Refined1 p f a -> Either RefineFailure (Refined1 p f a)
forall a b. b -> Either a b
Right (f a -> Refined1 p f a
forall {k} {k} (p :: k) (f :: k -> Type) (a :: k).
f a -> Refined1 p f a
Refined1 f a
fa)
      Just RefineFailure
e  -> RefineFailure -> Either RefineFailure (Refined1 p f a)
forall a b. a -> Either a b
Left RefineFailure
e

-- | Construct a 'Refined1' without validating the predicate @p@.
--
-- Unsafe. Use only when you can manually prove that the predicate holds.
unsafeRefine1 :: f a -> Refined1 p f a
unsafeRefine1 :: forall {k} {k} (f :: k -> Type) (a :: k) (p :: k).
f a -> Refined1 p f a
unsafeRefine1 = f a -> Refined1 p f a
forall {k} {k} (p :: k) (f :: k -> Type) (a :: k).
f a -> Refined1 p f a
Refined1

-- | Replace a 'Refined1''s predicate without validating the new predicate
--   @pNew@.
--
-- Unsafe. Use only when you can manually prove that the new predicate holds.
unsafeRerefine1 :: forall pNew pOld f a. Refined1 pOld f a -> Refined1 pNew f a
unsafeRerefine1 :: forall {k} {k} {k} (pNew :: k) (pOld :: k) (f :: k -> Type)
       (a :: k).
Refined1 pOld f a -> Refined1 pNew f a
unsafeRerefine1 = f a -> Refined1 pNew f a
forall {k} {k} (p :: k) (f :: k -> Type) (a :: k).
f a -> Refined1 p f a
Refined1 (f a -> Refined1 pNew f a)
-> (Refined1 pOld f a -> f a)
-> Refined1 pOld f a
-> Refined1 pNew f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined1 pOld f a -> f a
forall {k} {k} (p :: k) (f :: k -> Type) (a :: k).
Refined1 p f a -> f a
unrefine1

-- | Reify a functor predicate.
reifyPredicate1 :: forall p f a. Refine1 p f => f a -> Bool
reifyPredicate1 :: forall {k} {k1} (p :: k) (f :: k1 -> Type) (a :: k1).
Refine1 p f =>
f a -> Bool
reifyPredicate1 f a
fa = case forall (p :: k) (f :: k1 -> Type) (a :: k1).
Refine1 p f =>
f a -> Either RefineFailure (Refined1 p f a)
forall {k} {k} (p :: k) (f :: k -> Type) (a :: k).
Refine1 p f =>
f a -> Either RefineFailure (Refined1 p f a)
refine1 @p f a
fa of Right{} -> Bool
True; Left{} -> Bool
False

{- TODO
* got an extra \n at start oops
* make it look better lol
* make tail-call recursive? need to ferry more indents around though
-}
prettyRefineFailure :: RefineFailure -> Text
prettyRefineFailure :: RefineFailure -> Text
prettyRefineFailure = Builder -> Text
Builder -> Text
TBL.runBuilder (Builder -> Text)
-> (RefineFailure -> Builder) -> RefineFailure -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [RefineFailure] -> Builder
go (Int
0 :: Int) ([RefineFailure] -> Builder)
-> (RefineFailure -> [RefineFailure]) -> RefineFailure -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\RefineFailure
e -> [RefineFailure
e])
  where
    go :: Int -> [RefineFailure] -> Builder
go Int
n = \case
      []     -> Builder
forall a. Monoid a => a
mempty
      (RefineFailure
e:[RefineFailure]
es) ->
        let bPred :: Builder
bPred   = Char -> Builder
TBL.fromChar Char
'\n' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
indent Int
n Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> RefineFailure -> Builder
refineFailurePredicate RefineFailure
e
            bDetail :: Builder
bDetail = Char -> Builder
TBL.fromChar Char
'\n' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
indent (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> RefineFailure -> Builder
refineFailureDetail RefineFailure
e
         in Builder
bPred Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
bDetail Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> [RefineFailure] -> Builder
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) (RefineFailure -> [RefineFailure]
refineFailureInner RefineFailure
e) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> [RefineFailure] -> Builder
go Int
n [RefineFailure]
es
    indent :: Int -> Builder
indent = \case
      Int
0 -> Builder
forall a. Monoid a => a
mempty
      Int
n -> Char -> Builder
TBL.fromChar Char
' ' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
indent (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)

-- TODO this requires switching inner errors so that last is first lol x)
-- also we only <> right. maybe that's useful for perf
-- to remove newline at start we need to start in a special mode so we know not
-- to add the first newline at bPred. but I cba it will be messier and I want to
-- replace this ASAP when someone comes up with a good pretty error format
prettyRefineFailure' :: RefineFailure -> Text
prettyRefineFailure' :: RefineFailure -> Text
prettyRefineFailure' = \RefineFailure
e -> Builder -> Text
Builder -> Text
TBL.runBuilder (Builder -> Text) -> Builder -> Text
forall a b. (a -> b) -> a -> b
$ Builder -> [(Int, RefineFailure)] -> Builder
go Builder
forall a. Monoid a => a
mempty [(Int
0 :: Int, RefineFailure
e)]
  where
    go :: Builder -> [(Int, RefineFailure)] -> Builder
go Builder
b = \case
      []            -> Builder
b
      ((Int
n, RefineFailure
e) : [(Int, RefineFailure)]
es) ->
        let bPred :: Builder
bPred   = Char -> Builder
TBL.fromChar Char
'\n' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
indent Int
n Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> RefineFailure -> Builder
refineFailurePredicate RefineFailure
e
            bDetail :: Builder
bDetail = Char -> Builder
TBL.fromChar Char
'\n' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
indent (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> RefineFailure -> Builder
refineFailureDetail RefineFailure
e
            b' :: Builder
b'      = Builder
b Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
bPred Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
bDetail
         in Builder -> [(Int, RefineFailure)] -> Builder
go Builder
b' (Int
-> [(Int, RefineFailure)]
-> [RefineFailure]
-> [(Int, RefineFailure)]
forall {a} {b}. a -> [(a, b)] -> [b] -> [(a, b)]
idk (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) [(Int, RefineFailure)]
es (RefineFailure -> [RefineFailure]
refineFailureInner RefineFailure
e))
    indent :: Int -> Builder
indent = \case
      Int
0 -> Builder
forall a. Monoid a => a
mempty
      Int
n -> Char -> Builder
TBL.fromChar Char
' ' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
indent (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
    idk :: a -> [(a, b)] -> [b] -> [(a, b)]
idk a
n [(a, b)]
rs = \case
      []   -> [(a, b)]
rs
      b
l:[b]
ls -> a -> [(a, b)] -> [b] -> [(a, b)]
idk a
n ((a
n, b
l)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[(a, b)]
rs) [b]
ls

-- | 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 (Arbitrary a, Refine p a, KnownPredicateName p)
  => Arbitrary (Refined p a) where
    arbitrary :: Gen (Refined p a)
arbitrary = Gen a -> (a -> Bool) -> Gen (Maybe a)
forall a. Gen a -> (a -> Bool) -> Gen (Maybe a)
QC.suchThatMaybe Gen a
forall a. Arbitrary a => Gen a
arbitrary (forall (p :: k) a. Refine p a => a -> Bool
forall {k} (p :: k) a. Refine p a => a -> Bool
reifyPredicate @p) Gen (Maybe a)
-> (Maybe a -> Gen (Refined p a)) -> Gen (Refined p a)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Just a
a  -> Refined p a -> Gen (Refined p a)
forall a. a -> Gen a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Refined p a -> Gen (Refined p a))
-> Refined p a -> Gen (Refined p a)
forall a b. (a -> b) -> a -> b
$ a -> Refined p a
forall {k} (p :: k) a. a -> Refined p a
Refined a
a
      Maybe a
Nothing -> String -> Gen (Refined p a)
forall a. HasCallStack => String -> a
error (String -> Gen (Refined p a)) -> String -> Gen (Refined p a)
forall a b. (a -> b) -> a -> b
$
           String
"rerefined: couldn't generate a value satisfying predicate: "
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> forall (p :: k). KnownPredicateName p => String
forall {k} (p :: k). KnownPredicateName p => String
predicateName @p

-- | 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 (Arbitrary (f a), Refine1 p f, KnownPredicateName p)
  => Arbitrary (Refined1 p f a) where
    arbitrary :: Gen (Refined1 p f a)
arbitrary = Gen (f a) -> (f a -> Bool) -> Gen (Maybe (f a))
forall a. Gen a -> (a -> Bool) -> Gen (Maybe a)
QC.suchThatMaybe Gen (f a)
forall a. Arbitrary a => Gen a
arbitrary (forall (p :: k) (f :: k -> Type) (a :: k).
Refine1 p f =>
f a -> Bool
forall {k} {k1} (p :: k) (f :: k1 -> Type) (a :: k1).
Refine1 p f =>
f a -> Bool
reifyPredicate1 @p) Gen (Maybe (f a))
-> (Maybe (f a) -> Gen (Refined1 p f a)) -> Gen (Refined1 p f a)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Just f a
fa -> Refined1 p f a -> Gen (Refined1 p f a)
forall a. a -> Gen a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Refined1 p f a -> Gen (Refined1 p f a))
-> Refined1 p f a -> Gen (Refined1 p f a)
forall a b. (a -> b) -> a -> b
$ f a -> Refined1 p f a
forall {k} {k} (p :: k) (f :: k -> Type) (a :: k).
f a -> Refined1 p f a
Refined1 f a
fa
      Maybe (f a)
Nothing -> String -> Gen (Refined1 p f a)
forall a. HasCallStack => String -> a
error (String -> Gen (Refined1 p f a)) -> String -> Gen (Refined1 p f a)
forall a b. (a -> b) -> a -> b
$
           String
"rerefined: couldn't generate a value satisfying predicate: "
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> forall (p :: k). KnownPredicateName p => String
forall {k} (p :: k). KnownPredicateName p => String
predicateName @p