{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE NoStarIsType #-}
module Predicate.Refined5 (
Refined5
, unRefined5
, eval5P
, eval5M
, newRefined5
, newRefined5'
, newRefined5P
, newRefined5P'
, MakeR5
, genRefined5
, genRefined5P
, unsafeRefined5
, unsafeRefined5'
) where
import Predicate.Refined2 (Msg2(..), RResults2(..), prt2Impl, Refined2C)
import Predicate.Refined (RefinedC)
import Predicate.Core
import Predicate.Misc
import Predicate.Util
import Data.Proxy (Proxy(..))
import Data.Aeson (ToJSON(..), FromJSON(..))
import qualified Language.Haskell.TH.Syntax as TH
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 Control.Lens
import Data.String (IsString(..))
import Data.Hashable (Hashable(..))
import GHC.Stack (HasCallStack)
import Test.QuickCheck
import Data.Coerce (coerce)
import Data.Either (isRight)
import Data.Char (isSpace)
import Control.Arrow (left)
import Data.Tree.Lens (root)
import Control.DeepSeq (NFData)
newtype Refined5 (opts :: Opt) ip op i = Refined5 (PP ip i)
type role Refined5 phantom nominal nominal nominal
unRefined5 :: forall k k1 (opts :: Opt) (ip :: k) (op :: k1) i
. Refined5 opts ip op i
-> PP ip i
unRefined5 :: Refined5 opts ip op i -> PP ip i
unRefined5 = Refined5 opts ip op i -> PP ip i
coerce
unsafeRefined5' :: forall opts ip op i
. ( Refined2C opts ip op i
, HasCallStack
)
=> PP ip i
-> Refined5 opts ip op i
unsafeRefined5' :: PP ip i -> Refined5 opts ip op i
unsafeRefined5' = ([Char] -> Refined5 opts ip op i)
-> (PP ip i -> Refined5 opts ip op i)
-> Either [Char] (PP ip i)
-> Refined5 opts ip op i
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either [Char] -> Refined5 opts ip op i
forall a. HasCallStack => [Char] -> a
error PP ip i -> Refined5 opts ip op i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
PP ip i -> Refined5 opts ip op i
Refined5 (Either [Char] (PP ip i) -> Refined5 opts ip op i)
-> (PP ip i -> Either [Char] (PP ip i))
-> PP ip i
-> Refined5 opts ip op i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
(PP op a ~ Bool, RefinedC opts op a) =>
a -> Either [Char] a
forall k (opts :: Opt) (p :: k) a.
(PP p a ~ Bool, RefinedC opts p a) =>
a -> Either [Char] a
evalBool5 @opts @op
unsafeRefined5 :: forall opts ip op i
. PP ip i
-> Refined5 opts ip op i
unsafeRefined5 :: PP ip i -> Refined5 opts ip op i
unsafeRefined5 = PP ip i -> Refined5 opts ip op i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
PP ip i -> Refined5 opts ip op i
Refined5
deriving newtype instance ( Refined2C opts ip op i
, NFData (PP ip i)
) => NFData (Refined5 opts ip op i)
deriving stock instance ( Refined2C opts ip op i
, Show (PP ip i)
) => Show (Refined5 opts ip op i)
deriving stock instance ( Refined2C opts ip op i
, Eq (PP ip i)
) => Eq (Refined5 opts ip op i)
deriving stock instance ( Refined2C opts ip op i
, Ord (PP ip i)
) => Ord (Refined5 opts ip op i)
deriving stock instance ( Refined2C opts ip op i
, TH.Lift (PP ip i)
) => TH.Lift (Refined5 opts ip op i)
instance ( i ~ String
, Refined2C opts ip op i
, Show (PP ip i)
) => IsString (Refined5 opts ip op i) where
fromString :: [Char] -> Refined5 opts ip op i
fromString [Char]
i =
case [Char] -> Either Msg2 (Refined5 opts ip op [Char])
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
(Refined2C opts ip op i, Show (PP ip i)) =>
i -> Either Msg2 (Refined5 opts ip op i)
newRefined5 [Char]
i of
Left Msg2
e -> [Char] -> Refined5 opts ip op i
forall a. HasCallStack => [Char] -> a
error ([Char] -> Refined5 opts ip op i)
-> [Char] -> Refined5 opts ip op i
forall a b. (a -> b) -> a -> b
$ [Char]
"Refined5(fromString):" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg2 -> [Char]
forall a. Show a => a -> [Char]
show Msg2
e
Right Refined5 opts ip op [Char]
r -> Refined5 opts ip op i
Refined5 opts ip op [Char]
r
instance ( Refined2C opts ip op i
, Read (PP ip i)
) => Read (Refined5 opts ip op i) where
readPrec :: ReadPrec (Refined5 opts ip op i)
readPrec
= ReadPrec (Refined5 opts ip op i)
-> ReadPrec (Refined5 opts ip op i)
forall a. ReadPrec a -> ReadPrec a
GR.parens
(Int
-> ReadPrec (Refined5 opts ip op i)
-> ReadPrec (Refined5 opts ip op i)
forall a. Int -> ReadPrec a -> ReadPrec a
PCR.prec
Int
11
(do Lexeme -> ReadPrec ()
GR.expectP ([Char] -> Lexeme
RL.Ident [Char]
"Refined5")
PP ip i
fld0 <- ReadPrec (PP ip i) -> ReadPrec (PP ip i)
forall a. ReadPrec a -> ReadPrec a
PCR.reset ReadPrec (PP ip i)
forall a. Read a => ReadPrec a
GR.readPrec
case PP ip i -> Either [Char] (PP op (PP ip i))
forall k (opts :: Opt) (p :: k) i.
(OptC opts, P p i) =>
i -> Either [Char] (PP p i)
evalQuick @opts @op PP ip i
fld0 of
Left {} -> [Char] -> ReadPrec (Refined5 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
""
Right PP op (PP ip i)
True -> Refined5 opts ip op i -> ReadPrec (Refined5 opts ip op i)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PP ip i -> Refined5 opts ip op i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
PP ip i -> Refined5 opts ip op i
Refined5 PP ip i
fld0)
Right PP op (PP ip i)
False -> [Char] -> ReadPrec (Refined5 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
""
))
readList :: ReadS [Refined5 opts ip op i]
readList = ReadS [Refined5 opts ip op i]
forall a. Read a => ReadS [a]
GR.readListDefault
readListPrec :: ReadPrec [Refined5 opts ip op i]
readListPrec = ReadPrec [Refined5 opts ip op i]
forall a. Read a => ReadPrec [a]
GR.readListPrecDefault
instance ( Refined2C opts ip op i
, ToJSON (PP ip i)
) => ToJSON (Refined5 opts ip op i) where
toJSON :: Refined5 opts ip op i -> Value
toJSON (Refined5 PP ip i
x) = PP ip i -> Value
forall a. ToJSON a => a -> Value
toJSON PP ip i
x
instance ( Refined2C opts ip op i
, FromJSON (PP ip i)
) => FromJSON (Refined5 opts ip op i) where
parseJSON :: Value -> Parser (Refined5 opts ip op i)
parseJSON Value
z = do
PP ip i
i <- Value -> Parser (PP ip i)
forall a. FromJSON a => Value -> Parser a
parseJSON @(PP ip i) Value
z
case PP ip i -> Either [Char] (PP ip i)
forall k (opts :: Opt) (p :: k) a.
(PP p a ~ Bool, RefinedC opts p a) =>
a -> Either [Char] a
evalBool5 @opts @op PP ip i
i of
Left [Char]
e -> [Char] -> Parser (Refined5 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> Parser (Refined5 opts ip op i))
-> [Char] -> Parser (Refined5 opts ip op i)
forall a b. (a -> b) -> a -> b
$ [Char]
"Refined5:" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
e
Right PP ip i
_ -> Refined5 opts ip op i -> Parser (Refined5 opts ip op i)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PP ip i -> Refined5 opts ip op i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
PP ip i -> Refined5 opts ip op i
Refined5 PP ip i
i)
instance ( Arbitrary (PP ip i)
, Refined2C opts ip op i
) => Arbitrary (Refined5 opts ip op i) where
arbitrary :: Gen (Refined5 opts ip op i)
arbitrary = Gen (PP ip i) -> Gen (Refined5 opts ip op i)
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
(Refined2C opts ip op i, HasCallStack) =>
Gen (PP ip i) -> Gen (Refined5 opts ip op i)
genRefined5 Gen (PP ip i)
forall a. Arbitrary a => Gen a
arbitrary
genRefined5 ::
forall opts ip op i
. ( Refined2C opts ip op i
, HasCallStack
)
=> Gen (PP ip i)
-> Gen (Refined5 opts ip op i)
genRefined5 :: Gen (PP ip i) -> Gen (Refined5 opts ip op i)
genRefined5 = Proxy '(opts, ip, op, i)
-> Gen (PP ip i) -> Gen (Refined5 opts ip op i)
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
(Refined2C opts ip op i, HasCallStack) =>
Proxy '(opts, ip, op, i)
-> Gen (PP ip i) -> Gen (Refined5 opts ip op i)
genRefined5P Proxy '(opts, ip, op, i)
forall k (t :: k). Proxy t
Proxy
genRefined5P ::
forall opts ip op i
. ( Refined2C opts ip op i
, HasCallStack
)
=> Proxy '(opts,ip,op,i)
-> Gen (PP ip i)
-> Gen (Refined5 opts ip op i)
genRefined5P :: Proxy '(opts, ip, op, i)
-> Gen (PP ip i) -> Gen (Refined5 opts ip op i)
genRefined5P Proxy '(opts, ip, op, i)
_ Gen (PP ip i)
g =
let f :: Int -> Gen (Refined5 opts ip op i)
f !Int
cnt = do
Maybe (PP ip i)
mi <- Gen (PP ip i) -> (PP ip i -> Bool) -> Gen (Maybe (PP ip i))
forall a. Gen a -> (a -> Bool) -> Gen (Maybe a)
suchThatMaybe Gen (PP ip i)
g (Either [Char] (PP ip i) -> Bool
forall a b. Either a b -> Bool
isRight (Either [Char] (PP ip i) -> Bool)
-> (PP ip i -> Either [Char] (PP ip i)) -> PP ip i -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
(PP op a ~ Bool, RefinedC opts op a) =>
a -> Either [Char] a
forall k (opts :: Opt) (p :: k) a.
(PP p a ~ Bool, RefinedC opts p a) =>
a -> Either [Char] a
evalBool5 @opts @op)
case Maybe (PP ip i)
mi of
Maybe (PP ip i)
Nothing ->
let o :: POpts
o = OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts
in if Int
cnt Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= POpts -> HKD Identity Int
forall (f :: Type -> Type). HOpts f -> HKD f Int
oRecursion POpts
o
then [Char] -> Gen (Refined5 opts ip op i)
forall a. HasCallStack => [Char] -> a
error ([Char] -> Gen (Refined5 opts ip op i))
-> [Char] -> Gen (Refined5 opts ip op i)
forall a b. (a -> b) -> a -> b
$ POpts -> ShowS
setOtherEffects POpts
o ([Char]
"genRefined5P recursion exceeded(" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (POpts -> HKD Identity Int
forall (f :: Type -> Type). HOpts f -> HKD f Int
oRecursion POpts
o) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")")
else Int -> Gen (Refined5 opts ip op i)
f (Int
cntInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
Just PP ip i
i -> Refined5 opts ip op i -> Gen (Refined5 opts ip op i)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Refined5 opts ip op i -> Gen (Refined5 opts ip op i))
-> Refined5 opts ip op i -> Gen (Refined5 opts ip op i)
forall a b. (a -> b) -> a -> b
$ PP ip i -> Refined5 opts ip op i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
PP ip i -> Refined5 opts ip op i
unsafeRefined5 PP ip i
i
in Int -> Gen (Refined5 opts ip op i)
f Int
0
instance ( Refined2C opts ip op i
, Binary (PP ip i)
) => Binary (Refined5 opts ip op i) where
get :: Get (Refined5 opts ip op i)
get = do
PP ip i
i <- Binary (PP ip i) => Get (PP ip i)
forall t. Binary t => Get t
B.get @(PP ip i)
case PP ip i -> Either [Char] (PP ip i)
forall k (opts :: Opt) (p :: k) a.
(PP p a ~ Bool, RefinedC opts p a) =>
a -> Either [Char] a
evalBool5 @opts @op PP ip i
i of
Left [Char]
e -> [Char] -> Get (Refined5 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> Get (Refined5 opts ip op i))
-> [Char] -> Get (Refined5 opts ip op i)
forall a b. (a -> b) -> a -> b
$ [Char]
"Refined5:Binary:" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
e
Right PP ip i
_ -> Refined5 opts ip op i -> Get (Refined5 opts ip op i)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Refined5 opts ip op i -> Get (Refined5 opts ip op i))
-> Refined5 opts ip op i -> Get (Refined5 opts ip op i)
forall a b. (a -> b) -> a -> b
$ PP ip i -> Refined5 opts ip op i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
PP ip i -> Refined5 opts ip op i
Refined5 PP ip i
i
put :: Refined5 opts ip op i -> Put
put (Refined5 PP ip i
r) = PP ip i -> Put
forall t. Binary t => t -> Put
B.put @(PP ip i) PP ip i
r
instance ( Refined2C opts ip op i
, Hashable (PP ip i)
) => Hashable (Refined5 opts ip op i) where
hashWithSalt :: Int -> Refined5 opts ip op i -> Int
hashWithSalt Int
s (Refined5 PP ip i
b) = Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ PP ip i -> Int
forall a. Hashable a => a -> Int
hash PP ip i
b
newRefined5' :: forall opts ip op i m
. ( MonadEval m
, Refined2C opts ip op i
, Show (PP ip i)
)
=> i
-> m (Either Msg2 (Refined5 opts ip op i))
newRefined5' :: i -> m (Either Msg2 (Refined5 opts ip op i))
newRefined5' = Proxy '(opts, ip, op, i)
-> i -> m (Either Msg2 (Refined5 opts ip op i))
forall k k (opts :: Opt) (ip :: k) (op :: k) i
(proxy :: (Opt, k, k, Type) -> Type) (m :: Type -> Type).
(MonadEval m, Refined2C opts ip op i, Show (PP ip i)) =>
proxy '(opts, ip, op, i)
-> i -> m (Either Msg2 (Refined5 opts ip op i))
newRefined5P' Proxy '(opts, ip, op, i)
forall k (t :: k). Proxy t
Proxy
newRefined5P' :: forall opts ip op i proxy m
. ( MonadEval m
, Refined2C opts ip op i
, Show (PP ip i)
)
=> proxy '(opts,ip,op,i)
-> i
-> m (Either Msg2 (Refined5 opts ip op i))
newRefined5P' :: proxy '(opts, ip, op, i)
-> i -> m (Either Msg2 (Refined5 opts ip op i))
newRefined5P' proxy '(opts, ip, op, i)
_ i
i = do
(RResults2 (PP ip i)
ret,Maybe (Refined5 opts ip op i)
mr) <- i -> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
forall k k (opts :: Opt) (ip :: k) (op :: k) i (m :: Type -> Type).
(MonadEval m, Refined2C opts ip op i) =>
i -> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
eval5M i
i
Either Msg2 (Refined5 opts ip op i)
-> m (Either Msg2 (Refined5 opts ip op i))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Either Msg2 (Refined5 opts ip op i)
-> m (Either Msg2 (Refined5 opts ip op i)))
-> Either Msg2 (Refined5 opts ip op i)
-> m (Either Msg2 (Refined5 opts ip op i))
forall a b. (a -> b) -> a -> b
$ Either Msg2 (Refined5 opts ip op i)
-> (Refined5 opts ip op i -> Either Msg2 (Refined5 opts ip op i))
-> Maybe (Refined5 opts ip op i)
-> Either Msg2 (Refined5 opts ip op i)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Msg2 -> Either Msg2 (Refined5 opts ip op i)
forall a b. a -> Either a b
Left (Msg2 -> Either Msg2 (Refined5 opts ip op i))
-> Msg2 -> Either Msg2 (Refined5 opts ip op i)
forall a b. (a -> b) -> a -> b
$ POpts -> RResults2 (PP ip i) -> Msg2
forall a. Show a => POpts -> RResults2 a -> Msg2
prt2Impl (OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts) RResults2 (PP ip i)
ret) Refined5 opts ip op i -> Either Msg2 (Refined5 opts ip op i)
forall a b. b -> Either a b
Right Maybe (Refined5 opts ip op i)
mr
newRefined5 :: forall opts ip op i
. ( Refined2C opts ip op i
, Show (PP ip i)
) => i
-> Either Msg2 (Refined5 opts ip op i)
newRefined5 :: i -> Either Msg2 (Refined5 opts ip op i)
newRefined5 = Proxy '(opts, ip, op, i)
-> i -> Either Msg2 (Refined5 opts ip op i)
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
(Refined2C opts ip op i, Show (PP ip i)) =>
Proxy '(opts, ip, op, i)
-> i -> Either Msg2 (Refined5 opts ip op i)
newRefined5P Proxy '(opts, ip, op, i)
forall k (t :: k). Proxy t
Proxy
newRefined5P :: forall opts ip op i
. ( Refined2C opts ip op i
, Show (PP ip i)
) => Proxy '(opts,ip,op,i)
-> i
-> Either Msg2 (Refined5 opts ip op i)
newRefined5P :: Proxy '(opts, ip, op, i)
-> i -> Either Msg2 (Refined5 opts ip op i)
newRefined5P Proxy '(opts, ip, op, i)
_ i
i =
let (RResults2 (PP ip i)
ret,Maybe (Refined5 opts ip op i)
mr) = Identity (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
-> (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
forall a. Identity a -> a
runIdentity (Identity (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
-> (RResults2 (PP ip i), Maybe (Refined5 opts ip op i)))
-> Identity (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
-> (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
forall a b. (a -> b) -> a -> b
$ i -> Identity (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
forall k k (opts :: Opt) (ip :: k) (op :: k) i (m :: Type -> Type).
(MonadEval m, Refined2C opts ip op i) =>
i -> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
eval5M i
i
in Either Msg2 (Refined5 opts ip op i)
-> (Refined5 opts ip op i -> Either Msg2 (Refined5 opts ip op i))
-> Maybe (Refined5 opts ip op i)
-> Either Msg2 (Refined5 opts ip op i)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Msg2 -> Either Msg2 (Refined5 opts ip op i)
forall a b. a -> Either a b
Left (Msg2 -> Either Msg2 (Refined5 opts ip op i))
-> Msg2 -> Either Msg2 (Refined5 opts ip op i)
forall a b. (a -> b) -> a -> b
$ POpts -> RResults2 (PP ip i) -> Msg2
forall a. Show a => POpts -> RResults2 a -> Msg2
prt2Impl (OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts) RResults2 (PP ip i)
ret) Refined5 opts ip op i -> Either Msg2 (Refined5 opts ip op i)
forall a b. b -> Either a b
Right Maybe (Refined5 opts ip op i)
mr
eval5P :: forall opts ip op i m
. ( Refined2C opts ip op i
, MonadEval m
)
=> Proxy '(opts,ip,op,i)
-> i
-> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
eval5P :: Proxy '(opts, ip, op, i)
-> i -> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
eval5P Proxy '(opts, ip, op, i)
_ = i -> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
forall k k (opts :: Opt) (ip :: k) (op :: k) i (m :: Type -> Type).
(MonadEval m, Refined2C opts ip op i) =>
i -> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
eval5M
eval5M :: forall opts ip op i m
. ( MonadEval m
, Refined2C opts ip op i
)
=> i
-> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
eval5M :: i -> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
eval5M i
i = do
let o :: POpts
o = OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts
TT (PP ip i)
ll <- Proxy ip -> POpts -> i -> m (TT (PP ip i))
forall k (p :: k) a (m :: Type -> Type) (proxy :: k -> Type).
(P p a, MonadEval m) =>
proxy p -> POpts -> a -> m (TT (PP p a))
eval (Proxy ip
forall k (t :: k). Proxy t
Proxy @ip) POpts
o i
i
case TT (PP ip i) -> (Either [Char] (PP ip i), Tree PE)
forall a. TT a -> (Either [Char] a, Tree PE)
getValAndPE TT (PP ip i)
ll of
(Right PP ip i
a, Tree PE
t1) -> do
TT Bool
rr <- Proxy op -> POpts -> PP ip i -> m (TT (PP op (PP ip i)))
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 op
forall k (t :: k). Proxy t
Proxy @op) POpts
o PP ip i
a
(RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
-> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
-> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i)))
-> (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
-> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
forall a b. (a -> b) -> a -> b
$ case TT Bool -> (Either [Char] Bool, Tree PE)
forall a. TT a -> (Either [Char] a, Tree PE)
getValAndPE TT Bool
rr of
(Right Bool
True,Tree PE
t2) -> (PP ip i -> Tree PE -> Tree PE -> RResults2 (PP ip i)
forall a. a -> Tree PE -> Tree PE -> RResults2 a
RTTrue PP ip i
a Tree PE
t1 Tree PE
t2, Refined5 opts ip op i -> Maybe (Refined5 opts ip op i)
forall a. a -> Maybe a
Just (PP ip i -> Refined5 opts ip op i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
PP ip i -> Refined5 opts ip op i
Refined5 PP ip i
a))
(Right Bool
False,Tree PE
t2) -> (PP ip i -> Tree PE -> Tree PE -> RResults2 (PP ip i)
forall a. a -> Tree PE -> Tree PE -> RResults2 a
RTFalse PP ip i
a Tree PE
t1 Tree PE
t2, Maybe (Refined5 opts ip op i)
forall a. Maybe a
Nothing)
(Left [Char]
e,Tree PE
t2) -> (PP ip i -> Tree PE -> [Char] -> Tree PE -> RResults2 (PP ip i)
forall a. a -> Tree PE -> [Char] -> Tree PE -> RResults2 a
RTF PP ip i
a Tree PE
t1 [Char]
e Tree PE
t2, Maybe (Refined5 opts ip op i)
forall a. Maybe a
Nothing)
(Left [Char]
e,Tree PE
t1) -> (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
-> m (RResults2 (PP ip i), Maybe (Refined5 opts ip op i))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([Char] -> Tree PE -> RResults2 (PP ip i)
forall a. [Char] -> Tree PE -> RResults2 a
RF [Char]
e Tree PE
t1, Maybe (Refined5 opts ip op i)
forall a. Maybe a
Nothing)
type family MakeR5 p where
MakeR5 '(opts,ip,op,i) = Refined5 opts ip op i
evalBool5 :: forall opts p a
. (PP p a ~ Bool, RefinedC opts p a)
=> a
-> Either String a
evalBool5 :: a -> Either [Char] a
evalBool5 a
i =
let pp :: TT Bool
pp = 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) (OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts) a
i
opts :: POpts
opts = OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts
(Either [Char] Bool
lr,Tree PE
p2) = TT Bool -> (Either [Char] Bool, Tree PE)
forall a. TT a -> (Either [Char] a, Tree PE)
getValAndPE TT Bool
pp
z :: [Char]
z = let zz :: [Char]
zz = Tree PE
p2 Tree PE -> Getting [Char] (Tree PE) [Char] -> [Char]
forall s a. s -> Getting a s a -> a
^. (PE -> Const [Char] PE) -> Tree PE -> Const [Char] (Tree PE)
forall a. Lens' (Tree a) a
root ((PE -> Const [Char] PE) -> Tree PE -> Const [Char] (Tree PE))
-> (([Char] -> Const [Char] [Char]) -> PE -> Const [Char] PE)
-> Getting [Char] (Tree PE) [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> Const [Char] [Char]) -> PE -> Const [Char] PE
Lens' PE [Char]
peString
in if (Char -> Bool) -> [Char] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace [Char]
zz then [Char]
"FalseP" else [Char]
"{" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
zz [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"}"
w :: Either [Char] a
w = case Either [Char] Bool
lr of
Right Bool
True -> a -> Either [Char] a
forall a b. b -> Either a b
Right a
i
Right Bool
False -> [Char] -> Either [Char] a
forall a b. a -> Either a b
Left ([Char] -> Either [Char] a) -> [Char] -> Either [Char] a
forall a b. (a -> b) -> a -> b
$ [Char]
"false boolean check" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char] -> ShowS
nullIf [Char]
" | " [Char]
z
Left [Char]
e -> [Char] -> Either [Char] a
forall a b. a -> Either a b
Left ([Char] -> Either [Char] a) -> [Char] -> Either [Char] a
forall a b. (a -> b) -> a -> b
$ [Char]
"failed boolean check " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char] -> ShowS
nullIf [Char]
" | " [Char]
e
in ShowS -> Either [Char] a -> Either [Char] a
forall (a :: Type -> Type -> Type) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left ([Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ([Char]
"\n" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ POpts -> Tree PE -> [Char]
prtTreePure POpts
opts Tree PE
p2)) Either [Char] a
w