module Rerefined.Refine.TH
  ( refineTH
  , refine1TH
  ) where

import Rerefined.Refine
import Rerefined.Predicate
import Rerefined.Refined
import Rerefined.Refined1
import Language.Haskell.TH.Syntax qualified as TH

-- | Refine @a@ with predicate @p@ at compile time via Template Haskell.
refineTH
    :: forall p a m
    .  (Refine p a, TH.Lift a, TH.Quote m, MonadFail m)
    => a
    -> TH.Code m (Refined p a)
refineTH :: forall {k} (p :: k) a (m :: Type -> Type).
(Refine p a, Lift a, Quote m, MonadFail m) =>
a -> Code m (Refined p a)
refineTH = (RefineFailure String -> Code m (Refined p a))
-> (Refined p a -> Code m (Refined p a))
-> Either (RefineFailure String) (Refined p a)
-> Code m (Refined p a)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either RefineFailure String -> Code m (Refined p a)
forall a (m :: Type -> Type).
MonadFail m =>
RefineFailure String -> Code m a
refineTHFail Refined p a -> Code m (Refined p a)
forall t (m :: Type -> Type). (Lift t, Quote m) => t -> Code m t
forall (m :: Type -> Type).
Quote m =>
Refined p a -> Code m (Refined p a)
TH.liftTyped (Either (RefineFailure String) (Refined p a)
 -> Code m (Refined p a))
-> (a -> Either (RefineFailure String) (Refined p a))
-> a
-> Code m (Refined p a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: k) a.
Refine p a =>
a -> Either (RefineFailure String) (Refined p a)
forall {k} (p :: k) a.
Refine p a =>
a -> Either (RefineFailure String) (Refined p a)
refine @p @a

-- | Refine @f a@ with functor predicate @p@ at compile time via Template
--   Haskell.
refine1TH
    :: forall p f a m
    .  (Refine1 p f, TH.Lift (f a), TH.Quote m, MonadFail m)
    => f a
    -> TH.Code m (Refined1 p f a)
refine1TH :: forall {k} {k1} (p :: k) (f :: k1 -> Type) (a :: k1)
       (m :: Type -> Type).
(Refine1 p f, Lift (f a), Quote m, MonadFail m) =>
f a -> Code m (Refined1 p f a)
refine1TH = (RefineFailure String -> Code m (Refined1 p f a))
-> (Refined1 p f a -> Code m (Refined1 p f a))
-> Either (RefineFailure String) (Refined1 p f a)
-> Code m (Refined1 p f a)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either RefineFailure String -> Code m (Refined1 p f a)
forall a (m :: Type -> Type).
MonadFail m =>
RefineFailure String -> Code m a
refineTHFail Refined1 p f a -> Code m (Refined1 p f a)
forall t (m :: Type -> Type). (Lift t, Quote m) => t -> Code m t
forall (m :: Type -> Type).
Quote m =>
Refined1 p f a -> Code m (Refined1 p f a)
TH.liftTyped (Either (RefineFailure String) (Refined1 p f a)
 -> Code m (Refined1 p f a))
-> (f a -> Either (RefineFailure String) (Refined1 p f a))
-> f a
-> Code m (Refined1 p f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: k) (f :: k1 -> Type) (a :: k1).
Refine1 p f =>
f a -> Either (RefineFailure String) (Refined1 p f a)
forall {k} {k1} (p :: k) (f :: k1 -> Type) (a :: k1).
Refine1 p f =>
f a -> Either (RefineFailure String) (Refined1 p f a)
refine1 @p @f

-- | Template Haskell refinement failure helper.
refineTHFail :: forall a m. MonadFail m => RefineFailure String -> TH.Code m a
refineTHFail :: forall a (m :: Type -> Type).
MonadFail m =>
RefineFailure String -> Code m a
refineTHFail = m (TExp a) -> Code m a
forall a (m :: Type -> Type). m (TExp a) -> Code m a
TH.liftCode (m (TExp a) -> Code m a)
-> (RefineFailure String -> m (TExp a))
-> RefineFailure String
-> Code m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m (TExp a)
forall a. String -> m a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> m (TExp a))
-> (RefineFailure String -> String)
-> RefineFailure String
-> m (TExp a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RefineFailure String -> String
forall a. (Semigroup a, IsString a) => RefineFailure a -> a
prettyRefineFailure