{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE TypeOperators #-}
module Predicate.Refined (
Refined
, unRefined
, Msg0(..)
, showMsg0
, RefinedC
, newRefined
, newRefined'
, genRefined
, unsafeRefined
, unsafeRefined'
) where
import Predicate.Core
import Predicate.Misc (nullIf)
import Predicate.Util
import Control.Lens
import Data.Proxy (Proxy(Proxy))
import Data.Aeson (ToJSON(..), FromJSON(..))
import qualified Language.Haskell.TH.Syntax as TH
import Test.QuickCheck
import qualified GHC.Read as GR
import qualified Text.ParserCombinators.ReadPrec as PCR
import qualified Text.Read.Lex as RL
import qualified Data.Binary as B
import Data.Binary (Binary)
import Data.String (IsString(..))
import Data.Hashable (Hashable(..))
import GHC.Stack (HasCallStack)
import Data.Coerce (coerce)
import Control.DeepSeq (NFData)
newtype Refined (opts :: Opt) p a = Refined a
deriving stock (Int -> Refined opts p a -> ShowS
[Refined opts p a] -> ShowS
Refined opts p a -> String
(Int -> Refined opts p a -> ShowS)
-> (Refined opts p a -> String)
-> ([Refined opts p a] -> ShowS)
-> Show (Refined opts p a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (opts :: Opt) k (p :: k) a.
Show a =>
Int -> Refined opts p a -> ShowS
forall (opts :: Opt) k (p :: k) a.
Show a =>
[Refined opts p a] -> ShowS
forall (opts :: Opt) k (p :: k) a.
Show a =>
Refined opts p a -> String
showList :: [Refined opts p a] -> ShowS
$cshowList :: forall (opts :: Opt) k (p :: k) a.
Show a =>
[Refined opts p a] -> ShowS
show :: Refined opts p a -> String
$cshow :: forall (opts :: Opt) k (p :: k) a.
Show a =>
Refined opts p a -> String
showsPrec :: Int -> Refined opts p a -> ShowS
$cshowsPrec :: forall (opts :: Opt) k (p :: k) a.
Show a =>
Int -> Refined opts p a -> ShowS
Show, Refined opts p a -> Q Exp
Refined opts p a -> Q (TExp (Refined opts p a))
(Refined opts p a -> Q Exp)
-> (Refined opts p a -> Q (TExp (Refined opts p a)))
-> Lift (Refined opts p a)
forall t. (t -> Q Exp) -> (t -> Q (TExp t)) -> Lift t
forall (opts :: Opt) k (p :: k) a.
Lift a =>
Refined opts p a -> Q Exp
forall (opts :: Opt) k (p :: k) a.
Lift a =>
Refined opts p a -> Q (TExp (Refined opts p a))
liftTyped :: Refined opts p a -> Q (TExp (Refined opts p a))
$cliftTyped :: forall (opts :: Opt) k (p :: k) a.
Lift a =>
Refined opts p a -> Q (TExp (Refined opts p a))
lift :: Refined opts p a -> Q Exp
$clift :: forall (opts :: Opt) k (p :: k) a.
Lift a =>
Refined opts p a -> Q Exp
TH.Lift)
deriving newtype (Refined opts p a -> Refined opts p a -> Bool
(Refined opts p a -> Refined opts p a -> Bool)
-> (Refined opts p a -> Refined opts p a -> Bool)
-> Eq (Refined opts p a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (opts :: Opt) k (p :: k) a.
Eq a =>
Refined opts p a -> Refined opts p a -> Bool
/= :: Refined opts p a -> Refined opts p a -> Bool
$c/= :: forall (opts :: Opt) k (p :: k) a.
Eq a =>
Refined opts p a -> Refined opts p a -> Bool
== :: Refined opts p a -> Refined opts p a -> Bool
$c== :: forall (opts :: Opt) k (p :: k) a.
Eq a =>
Refined opts p a -> Refined opts p a -> Bool
Eq, Eq (Refined opts p a)
Eq (Refined opts p a)
-> (Refined opts p a -> Refined opts p a -> Ordering)
-> (Refined opts p a -> Refined opts p a -> Bool)
-> (Refined opts p a -> Refined opts p a -> Bool)
-> (Refined opts p a -> Refined opts p a -> Bool)
-> (Refined opts p a -> Refined opts p a -> Bool)
-> (Refined opts p a -> Refined opts p a -> Refined opts p a)
-> (Refined opts p a -> Refined opts p a -> Refined opts p a)
-> Ord (Refined opts p a)
Refined opts p a -> Refined opts p a -> Bool
Refined opts p a -> Refined opts p a -> Ordering
Refined opts p a -> Refined opts p a -> Refined opts 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 (opts :: Opt) k (p :: k) a. Ord a => Eq (Refined opts p a)
forall (opts :: Opt) k (p :: k) a.
Ord a =>
Refined opts p a -> Refined opts p a -> Bool
forall (opts :: Opt) k (p :: k) a.
Ord a =>
Refined opts p a -> Refined opts p a -> Ordering
forall (opts :: Opt) k (p :: k) a.
Ord a =>
Refined opts p a -> Refined opts p a -> Refined opts p a
min :: Refined opts p a -> Refined opts p a -> Refined opts p a
$cmin :: forall (opts :: Opt) k (p :: k) a.
Ord a =>
Refined opts p a -> Refined opts p a -> Refined opts p a
max :: Refined opts p a -> Refined opts p a -> Refined opts p a
$cmax :: forall (opts :: Opt) k (p :: k) a.
Ord a =>
Refined opts p a -> Refined opts p a -> Refined opts p a
>= :: Refined opts p a -> Refined opts p a -> Bool
$c>= :: forall (opts :: Opt) k (p :: k) a.
Ord a =>
Refined opts p a -> Refined opts p a -> Bool
> :: Refined opts p a -> Refined opts p a -> Bool
$c> :: forall (opts :: Opt) k (p :: k) a.
Ord a =>
Refined opts p a -> Refined opts p a -> Bool
<= :: Refined opts p a -> Refined opts p a -> Bool
$c<= :: forall (opts :: Opt) k (p :: k) a.
Ord a =>
Refined opts p a -> Refined opts p a -> Bool
< :: Refined opts p a -> Refined opts p a -> Bool
$c< :: forall (opts :: Opt) k (p :: k) a.
Ord a =>
Refined opts p a -> Refined opts p a -> Bool
compare :: Refined opts p a -> Refined opts p a -> Ordering
$ccompare :: forall (opts :: Opt) k (p :: k) a.
Ord a =>
Refined opts p a -> Refined opts p a -> Ordering
$cp1Ord :: forall (opts :: Opt) k (p :: k) a. Ord a => Eq (Refined opts p a)
Ord, Refined opts p a -> ()
(Refined opts p a -> ()) -> NFData (Refined opts p a)
forall a. (a -> ()) -> NFData a
forall (opts :: Opt) k (p :: k) a.
NFData a =>
Refined opts p a -> ()
rnf :: Refined opts p a -> ()
$crnf :: forall (opts :: Opt) k (p :: k) a.
NFData a =>
Refined opts p a -> ()
NFData)
unRefined :: forall k (opts :: Opt) (p :: k) a
. Refined opts p a
-> a
unRefined :: Refined opts p a -> a
unRefined = Refined opts p a -> a
coerce
type role Refined phantom nominal nominal
instance RefinedC opts p String
=> IsString (Refined opts p String) where
fromString :: String -> Refined opts p String
fromString String
s =
case String -> Either Msg0 (Refined opts p String)
forall k (opts :: Opt) (p :: k) a.
RefinedC opts p a =>
a -> Either Msg0 (Refined opts p a)
newRefined @opts @p String
s of
Left Msg0
w -> String -> Refined opts p String
forall a. HasCallStack => String -> a
error (String -> Refined opts p String)
-> String -> Refined opts p String
forall a b. (a -> b) -> a -> b
$ String
"Refined(IsString:fromString):" String -> ShowS
forall a. [a] -> [a] -> [a]
++ POpts -> Msg0 -> String
errorDisplay (OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts) Msg0
w
Right Refined opts p String
r -> Refined opts p String
r
errorDisplay :: POpts -> Msg0 -> String
errorDisplay :: POpts -> Msg0 -> String
errorDisplay POpts
o Msg0
m =
Msg0 -> String
m0ValBoolColor Msg0
m
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> ShowS
nullIf String
" " (Msg0 -> String
m0Short Msg0
m)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if String -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null (Msg0 -> String
m0Long Msg0
m) Bool -> Bool -> Bool
|| POpts -> Bool
hasNoTree POpts
o
then String
""
else String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg0 -> String
m0Long Msg0
m)
instance ( RefinedC opts p a
, Read a
) => Read (Refined opts p a) where
readPrec :: ReadPrec (Refined opts p a)
readPrec
= ReadPrec (Refined opts p a) -> ReadPrec (Refined opts p a)
forall a. ReadPrec a -> ReadPrec a
GR.parens
(Int -> ReadPrec (Refined opts p a) -> ReadPrec (Refined opts p a)
forall a. Int -> ReadPrec a -> ReadPrec a
PCR.prec
Int
11
(do Lexeme -> ReadPrec ()
GR.expectP (String -> Lexeme
RL.Ident String
"Refined")
a
fld0 <- ReadPrec a -> ReadPrec a
forall a. ReadPrec a -> ReadPrec a
PCR.reset ReadPrec a
forall a. Read a => ReadPrec a
GR.readPrec
case a -> Either Msg0 (Refined opts p a)
forall k (opts :: Opt) (p :: k) a.
RefinedC opts p a =>
a -> Either Msg0 (Refined opts p a)
newRefined @opts @p a
fld0 of
Left Msg0
_e -> String -> ReadPrec (Refined opts p a)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
""
Right Refined opts p a
_r -> Refined opts p a -> ReadPrec (Refined opts p a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (a -> Refined opts p a
forall k (opts :: Opt) (p :: k) a. a -> Refined opts p a
Refined a
fld0)
))
readList :: ReadS [Refined opts p a]
readList = ReadS [Refined opts p a]
forall a. Read a => ReadS [a]
GR.readListDefault
readListPrec :: ReadPrec [Refined opts p a]
readListPrec = ReadPrec [Refined opts p a]
forall a. Read a => ReadPrec [a]
GR.readListPrecDefault
type RefinedC opts p a = (OptC opts, PP p a ~ Bool, P p a)
instance ToJSON a => ToJSON (Refined opts p a) where
toJSON :: Refined opts p a -> Value
toJSON = a -> Value
forall a. ToJSON a => a -> Value
toJSON (a -> Value)
-> (Refined opts p a -> a) -> Refined opts p a -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined opts p a -> a
forall k (opts :: Opt) (p :: k) a. Refined opts p a -> a
unRefined
instance ( RefinedC opts p a
, FromJSON a
) => FromJSON (Refined opts p a) where
parseJSON :: Value -> Parser (Refined opts p a)
parseJSON Value
z = do
a
a <- Value -> Parser a
forall a. FromJSON a => Value -> Parser a
parseJSON Value
z
case a -> Either Msg0 (Refined opts p a)
forall k (opts :: Opt) (p :: k) a.
RefinedC opts p a =>
a -> Either Msg0 (Refined opts p a)
newRefined @opts @p a
a of
Left Msg0
w -> String -> Parser (Refined opts p a)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Parser (Refined opts p a))
-> String -> Parser (Refined opts p a)
forall a b. (a -> b) -> a -> b
$ String
"Refined(FromJSON:parseJSON):" String -> ShowS
forall a. [a] -> [a] -> [a]
++ POpts -> Msg0 -> String
errorDisplay (OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts) Msg0
w
Right Refined opts p a
r -> Refined opts p a -> Parser (Refined opts p a)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Refined opts p a
r
instance ( RefinedC opts p a
, Binary a
) => Binary (Refined opts p a) where
get :: Get (Refined opts p a)
get = do
a
fld0 <- Binary a => Get a
forall t. Binary t => Get t
B.get @a
case a -> Either Msg0 (Refined opts p a)
forall k (opts :: Opt) (p :: k) a.
RefinedC opts p a =>
a -> Either Msg0 (Refined opts p a)
newRefined @opts @p a
fld0 of
Left Msg0
w -> String -> Get (Refined opts p a)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Get (Refined opts p a))
-> String -> Get (Refined opts p a)
forall a b. (a -> b) -> a -> b
$ String
"Refined(Binary:get):" String -> ShowS
forall a. [a] -> [a] -> [a]
++ POpts -> Msg0 -> String
errorDisplay (OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts) Msg0
w
Right Refined opts p a
r -> Refined opts p a -> Get (Refined opts p a)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Refined opts p a
r
put :: Refined opts p a -> Put
put (Refined a
r) = a -> Put
forall t. Binary t => t -> Put
B.put @a a
r
instance ( RefinedC opts p a
, Hashable a
) => Hashable (Refined opts p a) where
hashWithSalt :: Int -> Refined opts p a -> Int
hashWithSalt Int
s (Refined a
a) = Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ a -> Int
forall a. Hashable a => a -> Int
hash a
a
instance ( Arbitrary a
, RefinedC opts p a
, Show a
) => Arbitrary (Refined opts p a) where
arbitrary :: Gen (Refined opts p a)
arbitrary = Gen a -> Gen (Refined opts p a)
forall k (opts :: Opt) (p :: k) a.
(RefinedC opts p a, HasCallStack) =>
Gen a -> Gen (Refined opts p a)
genRefined Gen a
forall a. Arbitrary a => Gen a
arbitrary
genRefined :: forall opts p a .
( RefinedC opts p a
, HasCallStack
)
=> Gen a
-> Gen (Refined opts p a)
genRefined :: Gen a -> Gen (Refined opts p a)
genRefined Gen a
g =
let f :: Int -> Gen (Refined opts p a)
f !Int
cnt = do
Maybe a
ma <- Gen a -> (a -> Bool) -> Gen (Maybe a)
forall a. Gen a -> (a -> Bool) -> Gen (Maybe a)
suchThatMaybe Gen a
g ((a -> Bool) -> Gen (Maybe a)) -> (a -> Bool) -> Gen (Maybe a)
forall a b. (a -> b) -> a -> b
$ \a
a -> a -> Either String (PP p a)
forall k (opts :: Opt) (p :: k) i.
(OptC opts, P p i) =>
i -> Either String (PP p i)
evalQuick @opts @p a
a Either String Bool -> Either String Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Either String Bool
forall a b. b -> Either a b
Right Bool
True
case Maybe a
ma of
Maybe a
Nothing ->
let o :: POpts
o = OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts
r :: Int
r = POpts -> Int
getMaxRecursionValue POpts
o
in if Int
cnt Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
r
then String -> Gen (Refined opts p a)
forall a. HasCallStack => String -> a
error (String -> Gen (Refined opts p a))
-> String -> Gen (Refined opts p a)
forall a b. (a -> b) -> a -> b
$ POpts -> ShowS
setOtherEffects POpts
o (String
"genRefined recursion exceeded(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")")
else Int -> Gen (Refined opts p a)
f (Int
cntInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
Just a
a -> Refined opts p a -> Gen (Refined opts p a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Refined opts p a -> Gen (Refined opts p a))
-> Refined opts p a -> Gen (Refined opts p a)
forall a b. (a -> b) -> a -> b
$ a -> Refined opts p a
forall k (opts :: Opt) (p :: k) a. a -> Refined opts p a
unsafeRefined a
a
in Int -> Gen (Refined opts p a)
f Int
0
data Msg0 = Msg0 { Msg0 -> Either String Bool
m0BoolE :: !(Either String Bool)
, Msg0 -> String
m0Short :: !String
, Msg0 -> String
m0Long :: !String
, Msg0 -> String
m0ValBoolColor :: !String
} deriving Msg0 -> Msg0 -> Bool
(Msg0 -> Msg0 -> Bool) -> (Msg0 -> Msg0 -> Bool) -> Eq Msg0
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Msg0 -> Msg0 -> Bool
$c/= :: Msg0 -> Msg0 -> Bool
== :: Msg0 -> Msg0 -> Bool
$c== :: Msg0 -> Msg0 -> Bool
Eq
showMsg0 :: Msg0 -> String
showMsg0 :: Msg0 -> String
showMsg0 (Msg0 Either String Bool
a String
b String
c String
d) = String
"Msg0 [" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Either String Bool -> String
forall a. Show a => a -> String
show Either String Bool
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]\nShort[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]\nLong[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]\nColor[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
d String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"
instance Show Msg0 where
show :: Msg0 -> String
show = Msg0 -> String
m0Long
newRefined' :: forall opts p a m
. ( MonadEval m
, RefinedC opts p a
)
=> a
-> m (Either Msg0 (Refined opts p a))
newRefined' :: a -> m (Either Msg0 (Refined opts p a))
newRefined' a
a = do
let o :: POpts
o = OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts
TT Bool
pp <- Proxy p -> POpts -> a -> m (TT (PP p a))
forall k (m :: Type -> Type) (p :: k) a (proxy :: k -> Type).
(MonadEval m, P p a, PP p a ~ Bool) =>
proxy p -> POpts -> a -> m (TT (PP p a))
evalBool (Proxy p
forall k (t :: k). Proxy t
Proxy @p) POpts
o a
a
let r :: String
r = POpts -> Val Bool -> String
colorValBool POpts
o (TT Bool
pp TT Bool -> Getting (Val Bool) (TT Bool) (Val Bool) -> Val Bool
forall s a. s -> Getting a s a -> a
^. Getting (Val Bool) (TT Bool) (Val Bool)
forall a b. Lens (TT a) (TT b) (Val a) (Val b)
ttVal)
s :: String
s = POpts -> TT Bool -> String
forall x. Show x => POpts -> TT x -> String
prtTree POpts
o TT Bool
pp
msg0 :: Msg0
msg0 = Either String Bool -> String -> String -> String -> Msg0
Msg0 (TT Bool
pp TT Bool
-> Getting (Either String Bool) (TT Bool) (Either String Bool)
-> Either String Bool
forall s a. s -> Getting a s a -> a
^. (Val Bool -> Const (Either String Bool) (Val Bool))
-> TT Bool -> Const (Either String Bool) (TT Bool)
forall a b. Lens (TT a) (TT b) (Val a) (Val b)
ttVal ((Val Bool -> Const (Either String Bool) (Val Bool))
-> TT Bool -> Const (Either String Bool) (TT Bool))
-> ((Either String Bool
-> Const (Either String Bool) (Either String Bool))
-> Val Bool -> Const (Either String Bool) (Val Bool))
-> Getting (Either String Bool) (TT Bool) (Either String Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either String Bool
-> Const (Either String Bool) (Either String Bool))
-> Val Bool -> Const (Either String Bool) (Val Bool)
forall a b. Iso (Val a) (Val b) (Either String a) (Either String b)
_ValEither) (TT Bool -> String
forall a. TT a -> String
topMessage TT Bool
pp) String
s String
r
Either Msg0 (Refined opts p a)
-> m (Either Msg0 (Refined opts p a))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Either Msg0 (Refined opts p a)
-> m (Either Msg0 (Refined opts p a)))
-> Either Msg0 (Refined opts p a)
-> m (Either Msg0 (Refined opts p a))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts -> String -> TT Bool -> [Tree PE] -> Either (TT Any) Bool
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
o String
"" TT Bool
pp [] of
Right Bool
True -> Refined opts p a -> Either Msg0 (Refined opts p a)
forall a b. b -> Either a b
Right (a -> Refined opts p a
forall k (opts :: Opt) (p :: k) a. a -> Refined opts p a
Refined a
a)
Either (TT Any) Bool
_ -> Msg0 -> Either Msg0 (Refined opts p a)
forall a b. a -> Either a b
Left Msg0
msg0
newRefined :: forall opts p a
. RefinedC opts p a
=> a
-> Either Msg0 (Refined opts p a)
newRefined :: a -> Either Msg0 (Refined opts p a)
newRefined = Identity (Either Msg0 (Refined opts p a))
-> Either Msg0 (Refined opts p a)
forall a. Identity a -> a
runIdentity (Identity (Either Msg0 (Refined opts p a))
-> Either Msg0 (Refined opts p a))
-> (a -> Identity (Either Msg0 (Refined opts p a)))
-> a
-> Either Msg0 (Refined opts p a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Identity (Either Msg0 (Refined opts p a))
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'
unsafeRefined :: forall opts p a . a -> Refined opts p a
unsafeRefined :: a -> Refined opts p a
unsafeRefined = a -> Refined opts p a
forall k (opts :: Opt) (p :: k) a. a -> Refined opts p a
Refined
unsafeRefined' :: forall opts p a
. ( RefinedC opts p a
, HasCallStack
) => a -> Refined opts p a
unsafeRefined' :: a -> Refined opts p a
unsafeRefined' a
a =
let o :: POpts
o = OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts
tt :: TT Bool
tt = Identity (TT Bool) -> TT Bool
forall a. Identity a -> a
runIdentity (Identity (TT Bool) -> TT Bool) -> Identity (TT Bool) -> TT Bool
forall a b. (a -> b) -> a -> b
$ Proxy p -> POpts -> a -> Identity (TT (PP p a))
forall k (m :: Type -> Type) (p :: k) a (proxy :: k -> Type).
(MonadEval m, P p a, PP p a ~ Bool) =>
proxy p -> POpts -> a -> m (TT (PP p a))
evalBool (Proxy p
forall k (t :: k). Proxy t
Proxy @p) POpts
o a
a
in case Inline
-> POpts -> String -> TT Bool -> [Tree PE] -> Either (TT Any) Bool
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
o String
"" TT Bool
tt [] of
Right Bool
True -> a -> Refined opts p a
forall k (opts :: Opt) (p :: k) a. a -> Refined opts p a
Refined a
a
Either (TT Any) Bool
_ -> let s :: String
s = POpts -> TT Bool -> String
forall x. Show x => POpts -> TT x -> String
prtTree POpts
o TT Bool
tt
bp :: String
bp = POpts -> Val Bool -> String
colorValBool POpts
o (TT Bool
tt TT Bool -> Getting (Val Bool) (TT Bool) (Val Bool) -> Val Bool
forall s a. s -> Getting a s a -> a
^. Getting (Val Bool) (TT Bool) (Val Bool)
forall a b. Lens (TT a) (TT b) (Val a) (Val b)
ttVal)
in case POpts -> HKD Identity Debug
forall (f :: Type -> Type). HOpts f -> HKD f Debug
oDebug POpts
o of
HKD Identity Debug
DZero -> String -> Refined opts p a
forall a. HasCallStack => String -> a
error String
bp
HKD Identity Debug
DLite -> String -> Refined opts p a
forall a. HasCallStack => String -> a
error (String -> Refined opts p a) -> String -> Refined opts p a
forall a b. (a -> b) -> a -> b
$ String
bp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> ShowS
nullIf String
"\n" String
s
HKD Identity Debug
_ -> String -> Refined opts p a
forall a. HasCallStack => String -> a
error (String -> Refined opts p a) -> String -> Refined opts p a
forall a b. (a -> b) -> a -> b
$ String
bp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> ShowS
nullIf String
"\n" String
s