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

import Rerefined.Refine
import Rerefined.Predicate
import Language.Haskell.TH.Syntax qualified as TH
import Data.Text qualified as Text

-- | Refine @a@ with predicate @p@ at compile time via Template Haskell.
--
-- Use like @$$('refineTH' \@p a)@.
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 -> Code m (Refined p a))
-> (Refined p a -> Code m (Refined p a))
-> Either RefineFailure (Refined p a)
-> Code m (Refined p a)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either RefineFailure -> Code m (Refined p a)
forall a (m :: Type -> Type).
MonadFail m =>
RefineFailure -> 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 (Refined p a) -> Code m (Refined p a))
-> (a -> Either RefineFailure (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 (Refined p a)
forall {k} (p :: k) a.
Refine p a =>
a -> Either RefineFailure (Refined p a)
refine @p @a

-- | Refine @f a@ with functor predicate @p@ at compile time via Template
--   Haskell.
--
-- Use like @$$('refine1TH' \@p a)@.
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 -> Code m (Refined1 p f a))
-> (Refined1 p f a -> Code m (Refined1 p f a))
-> Either RefineFailure (Refined1 p f a)
-> Code m (Refined1 p f a)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either RefineFailure -> Code m (Refined1 p f a)
forall a (m :: Type -> Type).
MonadFail m =>
RefineFailure -> 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 (Refined1 p f a) -> Code m (Refined1 p f a))
-> (f a -> Either RefineFailure (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 (Refined1 p f a)
forall {k1} {k2} (p :: k1) (f :: k2 -> Type) (a :: k2).
Refine1 p f =>
f a -> Either RefineFailure (Refined1 p f a)
refine1 @p @f

-- | Template Haskell refinement failure helper.
refineTHFail
    :: forall a m. MonadFail m => RefineFailure -> TH.Code m a
refineTHFail :: forall a (m :: Type -> Type).
MonadFail m =>
RefineFailure -> 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 -> m (TExp a)) -> RefineFailure -> 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) -> RefineFailure -> m (TExp a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
Text.unpack (Text -> String)
-> (RefineFailure -> Text) -> RefineFailure -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RefineFailure -> Text
prettyRefineFailure