-- | Base definitions for refinement predicates.

module Rerefined.Predicate
  ( Refine(validate)
  , Refine1(validate1)
  , RefineFailure(..)
  , Predicate(predicateName)
  ) where

import GHC.Exts ( Proxy# )
import Data.Typeable ( Typeable, typeRep )
import Data.Typeable.Typeably
import Data.Proxy ( Proxy(Proxy) )

-- | Types which define refinements on other types.
class Predicate p where
    -- | The predicate name, as a 'Show'-like (for good bracketing).
    --
    -- Non-combinator predicates may derive this via 'Typeably'. Combinator
    -- predicates must write a 'Show'-like instance manually, in order to avoid
    -- incurring insidious 'Typeable' contexts for the wrapped predicate(s).
    -- (TODO figure out some generics and/or TH to resolve that)
    predicateName :: Proxy# p -> Int -> ShowS

-- | Fill out predicate metadata using its 'Typeable' instance.
--
-- Do not use this for combinator predicates. Doing so will incur insidious
-- 'Typeable' contexts for the wrapped predicate(s).
instance Typeable a => Predicate (Typeably a) where
    predicateName :: Proxy# (Typeably a) -> Int -> ShowS
predicateName Proxy# (Typeably a)
_ Int
d = Int -> TypeRep -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d (Proxy a -> TypeRep
forall {k} (proxy :: k -> Type) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a))

-- | Refine @a@ with predicate @p@.
class Predicate p => Refine p a where
    -- | Validate predicate @p@ for the given @a@.
    --
    -- 'Nothing' indicates success. 'Just' contains a validation failure.
    validate :: Proxy# p -> a -> Maybe (RefineFailure String)

-- | Refine functor type @f@ with functor predicate @p@.
--
-- By not making the contained type accessible, we ensure refinements apply
-- @forall a. f a@. That is, refinements here apply only to the functor
-- structure, and not the stored elements.
class Predicate p => Refine1 p f where
    -- | Validate predicate @p@ for the given @f a@.
    validate1 :: Proxy# p -> f a -> Maybe (RefineFailure String)

-- | Predicate validation failure.
--
-- Polymorphic over the message type because I want to use 'Text', but want it
-- doesn't have the convenient 'Show' internals that 'String' does.
data RefineFailure a = RefineFailure
  { forall a. RefineFailure a -> a
refineFailurePredicate :: a
  -- ^ The predicate that failed.

  , forall a. RefineFailure a -> a
refineFailureDetail    :: a
  -- ^ Failure clarification.

  , forall a. RefineFailure a -> [RefineFailure a]
refineFailureInner     :: [RefineFailure a]
  -- ^ Any wrapped errors, for combinator predicates.
  --
  -- What these are, and their order, should be noted in 'refineFailureDetail'.
  }