{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoStarIsType #-}
module Predicate.Util_TH (
refinedTH
, refinedTHIO
, refined2TH
, refined2THIO
, refined3TH
, refined3THIO
, refined5TH
, refined5THIO
) where
import Predicate.Util
import Predicate.Misc
import Predicate.Core
import Predicate.Refined
import Predicate.Refined2
import Predicate.Refined3
import Predicate.Refined5
import qualified Language.Haskell.TH.Syntax as TH
refinedTH :: forall opts p i
. (TH.Lift i, RefinedC opts p i)
=> i
-> TH.Q (TH.TExp (Refined opts p i))
refinedTH :: i -> Q (TExp (Refined opts p i))
refinedTH i
i =
let msg0 :: String
msg0 = String
"refinedTH"
in case i -> Either Msg0 (Refined opts p i)
forall k (opts :: Opt) (p :: k) a.
RefinedC opts p a =>
a -> Either Msg0 (Refined opts p a)
newRefined @opts @p i
i of
Left Msg0
m -> String -> Q (TExp (Refined opts p i))
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Q (TExp (Refined opts p i)))
-> String -> Q (TExp (Refined opts p i))
forall a b. (a -> b) -> a -> b
$ String -> Msg0 -> String
forall (opts :: Opt). OptC opts => String -> Msg0 -> String
refinedFailMsg @opts String
msg0 Msg0
m
Right Refined opts p i
r -> [||r||]
refinedTHIO :: forall opts p i
. (TH.Lift i, RefinedC opts p i)
=> i
-> TH.Q (TH.TExp (Refined opts p i))
refinedTHIO :: i -> Q (TExp (Refined opts p i))
refinedTHIO i
i = do
let msg0 :: String
msg0 = String
"refinedTHIO"
Either Msg0 (Refined opts p i)
lr <- IO (Either Msg0 (Refined opts p i))
-> Q (Either Msg0 (Refined opts p i))
forall a. IO a -> Q a
TH.runIO (i -> IO (Either Msg0 (Refined opts p i))
forall k (opts :: Opt) (p :: k) a (m :: Type -> Type).
(MonadEval m, RefinedC opts p a) =>
a -> m (Either Msg0 (Refined opts p a))
newRefined' i
i)
case Either Msg0 (Refined opts p i)
lr of
Left Msg0
m -> String -> Q (TExp (Refined opts p i))
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Q (TExp (Refined opts p i)))
-> String -> Q (TExp (Refined opts p i))
forall a b. (a -> b) -> a -> b
$ String -> Msg0 -> String
forall (opts :: Opt). OptC opts => String -> Msg0 -> String
refinedFailMsg @opts String
msg0 Msg0
m
Right Refined opts p i
r -> [||r||]
refinedFailMsg :: forall opts . OptC opts => String -> Msg0 -> String
refinedFailMsg :: String -> Msg0 -> String
refinedFailMsg String
msg Msg0
m =
let msg1 :: String
msg1 | POpts -> Bool
hasNoTree (OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts) Bool -> Bool -> Bool
|| String -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null (Msg0 -> String
m0Long Msg0
m) = String
""
| Bool
otherwise = String -> String -> String
nullIf String
"\n" (Msg0 -> String
m0Long Msg0
m)
in String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": predicate failed with " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Msg0 -> String
m0ValBoolColor Msg0
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Msg0 -> String
m0Short Msg0
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg1
refined2TH :: forall opts ip op i
. ( Refined2C opts ip op i
, TH.Lift i
, TH.Lift (PP ip i)
, Show (PP ip i)
)
=> i
-> TH.Q (TH.TExp (Refined2 opts ip op i))
refined2TH :: i -> Q (TExp (Refined2 opts ip op i))
refined2TH i
i =
case i -> Either Msg2 (Refined2 opts ip op i)
forall k1 k2 (opts :: Opt) (ip :: k1) (op :: k2) i.
(Refined2C opts ip op i, Show (PP ip i)) =>
i -> Either Msg2 (Refined2 opts ip op i)
newRefined2 i
i of
Left Msg2
e -> String -> Q (TExp (Refined2 opts ip op i))
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Q (TExp (Refined2 opts ip op i)))
-> String -> Q (TExp (Refined2 opts ip op i))
forall a b. (a -> b) -> a -> b
$ Msg2 -> String
forall a. Show a => a -> String
show Msg2
e
Right Refined2 opts ip op i
r -> [||r||]
refined2THIO :: forall opts ip op i
. ( TH.Lift i
, TH.Lift (PP ip i)
, Refined2C opts ip op i
, Show (PP ip i)
)
=> i
-> TH.Q (TH.TExp (Refined2 opts ip op i))
refined2THIO :: i -> Q (TExp (Refined2 opts ip op i))
refined2THIO i
i = do
Either Msg2 (Refined2 opts ip op i)
x <- IO (Either Msg2 (Refined2 opts ip op i))
-> Q (Either Msg2 (Refined2 opts ip op i))
forall a. IO a -> Q a
TH.runIO (i -> IO (Either Msg2 (Refined2 opts ip op i))
forall k1 k2 (opts :: Opt) (ip :: k1) (op :: k2) i
(m :: Type -> Type).
(MonadEval m, Refined2C opts ip op i, Show (PP ip i)) =>
i -> m (Either Msg2 (Refined2 opts ip op i))
newRefined2' i
i)
case Either Msg2 (Refined2 opts ip op i)
x of
Left Msg2
e -> String -> Q (TExp (Refined2 opts ip op i))
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Q (TExp (Refined2 opts ip op i)))
-> String -> Q (TExp (Refined2 opts ip op i))
forall a b. (a -> b) -> a -> b
$ Msg2 -> String
forall a. Show a => a -> String
show Msg2
e
Right Refined2 opts ip op i
r -> [||r||]
refined3TH :: forall opts ip op fmt i
. ( Refined3C opts ip op fmt i
, TH.Lift i
, TH.Lift (PP ip i)
, Show (PP ip i)
)
=> i
-> TH.Q (TH.TExp (Refined3 opts ip op fmt i))
refined3TH :: i -> Q (TExp (Refined3 opts ip op fmt i))
refined3TH i
i =
case i -> Either Msg3 (Refined3 opts ip op fmt i)
forall k1 k2 k3 (opts :: Opt) (ip :: k1) (op :: k2) (fmt :: k3) i.
(Refined3C opts ip op fmt i, Show (PP ip i)) =>
i -> Either Msg3 (Refined3 opts ip op fmt i)
newRefined3 i
i of
Left Msg3
e -> String -> Q (TExp (Refined3 opts ip op fmt i))
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Q (TExp (Refined3 opts ip op fmt i)))
-> String -> Q (TExp (Refined3 opts ip op fmt i))
forall a b. (a -> b) -> a -> b
$ Msg3 -> String
forall a. Show a => a -> String
show Msg3
e
Right Refined3 opts ip op fmt i
r -> [||r||]
refined3THIO :: forall opts ip op fmt i
. ( TH.Lift i
, TH.Lift (PP ip i)
, Refined3C opts ip op fmt i
, Show (PP ip i)
)
=> i
-> TH.Q (TH.TExp (Refined3 opts ip op fmt i))
refined3THIO :: i -> Q (TExp (Refined3 opts ip op fmt i))
refined3THIO i
i = do
Either Msg3 (Refined3 opts ip op fmt i)
x <- IO (Either Msg3 (Refined3 opts ip op fmt i))
-> Q (Either Msg3 (Refined3 opts ip op fmt i))
forall a. IO a -> Q a
TH.runIO (i -> IO (Either Msg3 (Refined3 opts ip op fmt i))
forall k1 k2 k3 (opts :: Opt) (ip :: k1) (op :: k2) (fmt :: k3) i
(m :: Type -> Type).
(MonadEval m, Refined3C opts ip op fmt i, Show (PP ip i)) =>
i -> m (Either Msg3 (Refined3 opts ip op fmt i))
newRefined3' i
i)
case Either Msg3 (Refined3 opts ip op fmt i)
x of
Left Msg3
e -> String -> Q (TExp (Refined3 opts ip op fmt i))
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Q (TExp (Refined3 opts ip op fmt i)))
-> String -> Q (TExp (Refined3 opts ip op fmt i))
forall a b. (a -> b) -> a -> b
$ Msg3 -> String
forall a. Show a => a -> String
show Msg3
e
Right Refined3 opts ip op fmt i
r -> [||r||]
refined5TH :: forall opts ip op i
. ( Refined2C opts ip op i
, TH.Lift (PP ip i)
, Show (PP ip i)
)
=> i
-> TH.Q (TH.TExp (Refined5 opts ip op i))
refined5TH :: i -> Q (TExp (Refined5 opts ip op i))
refined5TH i
i =
case i -> Either Msg2 (Refined5 opts ip op i)
forall k1 k2 (opts :: Opt) (ip :: k1) (op :: k2) i.
(Refined2C opts ip op i, Show (PP ip i)) =>
i -> Either Msg2 (Refined5 opts ip op i)
newRefined5 i
i of
Left Msg2
e -> String -> Q (TExp (Refined5 opts ip op i))
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Q (TExp (Refined5 opts ip op i)))
-> String -> Q (TExp (Refined5 opts ip op i))
forall a b. (a -> b) -> a -> b
$ Msg2 -> String
forall a. Show a => a -> String
show Msg2
e
Right Refined5 opts ip op i
r -> [||r||]
refined5THIO :: forall opts ip op i
. ( TH.Lift (PP ip i)
, Refined2C opts ip op i
, Show (PP ip i)
)
=> i
-> TH.Q (TH.TExp (Refined5 opts ip op i))
refined5THIO :: i -> Q (TExp (Refined5 opts ip op i))
refined5THIO i
i = do
Either Msg2 (Refined5 opts ip op i)
x <- IO (Either Msg2 (Refined5 opts ip op i))
-> Q (Either Msg2 (Refined5 opts ip op i))
forall a. IO a -> Q a
TH.runIO (i -> IO (Either Msg2 (Refined5 opts ip op i))
forall k1 k2 (opts :: Opt) (ip :: k1) (op :: k2) i
(m :: Type -> Type).
(MonadEval m, Refined2C opts ip op i, Show (PP ip i)) =>
i -> m (Either Msg2 (Refined5 opts ip op i))
newRefined5' i
i)
case Either Msg2 (Refined5 opts ip op i)
x of
Left Msg2
e -> String -> Q (TExp (Refined5 opts ip op i))
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Q (TExp (Refined5 opts ip op i)))
-> String -> Q (TExp (Refined5 opts ip op i))
forall a b. (a -> b) -> a -> b
$ Msg2 -> String
forall a. Show a => a -> String
show Msg2
e
Right Refined5 opts ip op i
r -> [||r||]