{-# 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 DeriveGeneric #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE NoStarIsType #-}
module Predicate.Refined5 (
Refined5
, unRefined5
, eval5P
, eval5M
, newRefined5
, newRefined5'
, newRefined5P
, newRefined5P'
, MakeR5
, genRefined5
, genRefined5P
, unsafeRefined5
, unsafeRefined5'
, Refined5Exception(..)
) where
import Predicate.Refined2 (Msg2(..), RResults2(..), prt2Impl, Refined2C)
import Predicate.Refined (RefinedC)
import Predicate.Core
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 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)
import qualified Control.Exception as E
import GHC.Generics (Generic)
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
)
=> PP ip i
-> Refined5 opts ip op i
unsafeRefined5' :: PP ip i -> Refined5 opts ip op i
unsafeRefined5' = (String -> Refined5 opts ip op i)
-> (PP ip i -> Refined5 opts ip op i)
-> Either String (PP ip i)
-> Refined5 opts ip op i
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Refined5Exception -> Refined5 opts ip op i
forall a e. Exception e => e -> a
E.throw (Refined5Exception -> Refined5 opts ip op i)
-> (String -> Refined5Exception) -> String -> Refined5 opts ip op i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Refined5Exception
Refined5Exception) 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 String (PP ip i) -> Refined5 opts ip op i)
-> (PP ip i -> Either String (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 String a
forall k (opts :: Opt) (p :: k) a.
(PP p a ~ Bool, RefinedC opts p a) =>
a -> Either String 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 :: String -> Refined5 opts ip op i
fromString String
i =
case String -> Either Msg2 (Refined5 opts ip op String)
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 String
i of
Left Msg2
e -> Refined5Exception -> Refined5 opts ip op i
forall a e. Exception e => e -> a
E.throw (Refined5Exception -> Refined5 opts ip op i)
-> Refined5Exception -> Refined5 opts ip op i
forall a b. (a -> b) -> a -> b
$ String -> Refined5Exception
Refined5Exception (String -> Refined5Exception) -> String -> Refined5Exception
forall a b. (a -> b) -> a -> b
$ String
"IsString:fromString:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg2 -> String
forall a. Show a => a -> String
show Msg2
e
Right Refined5 opts ip op String
r -> Refined5 opts ip op i
Refined5 opts ip op String
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 (String -> Lexeme
RL.Ident String
"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 String (PP op (PP ip i))
forall k (opts :: Opt) (p :: k) i.
(OptC opts, P p i) =>
i -> Either String (PP p i)
evalQuick @opts @op PP ip i
fld0 of
Left {} -> String -> ReadPrec (Refined5 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
""
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 -> String -> ReadPrec (Refined5 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
""
))
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 String (PP ip i)
forall k (opts :: Opt) (p :: k) a.
(PP p a ~ Bool, RefinedC opts p a) =>
a -> Either String a
evalBool5 @opts @op PP ip i
i of
Left String
e -> String -> Parser (Refined5 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Parser (Refined5 opts ip op i))
-> String -> Parser (Refined5 opts ip op i)
forall a b. (a -> b) -> a -> b
$ String
"Refined5(FromJSON:parseJSON):" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
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 =>
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
=> 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 =>
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
=> 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 o :: POpts
o = OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts
r :: Int
r = POpts -> Int
getMaxRecursionValue POpts
o
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 String (PP ip i) -> Bool
forall a b. Either a b -> Bool
isRight (Either String (PP ip i) -> Bool)
-> (PP ip i -> Either String (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 String a
forall k (opts :: Opt) (p :: k) a.
(PP p a ~ Bool, RefinedC opts p a) =>
a -> Either String a
evalBool5 @opts @op)
case Maybe (PP ip i)
mi of
Maybe (PP ip i)
Nothing | Int
cnt Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
r -> Refined5Exception -> Gen (Refined5 opts ip op i)
forall a e. Exception e => e -> a
E.throw (Refined5Exception -> Gen (Refined5 opts ip op i))
-> Refined5Exception -> Gen (Refined5 opts ip op i)
forall a b. (a -> b) -> a -> b
$ String -> Refined5Exception
Refined5Exception (String -> Refined5Exception) -> String -> Refined5Exception
forall a b. (a -> b) -> a -> b
$ POpts -> ShowS
setOtherEffects POpts
o (String
"genRefined5P 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
")")
| Bool
otherwise -> 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 String (PP ip i)
forall k (opts :: Opt) (p :: k) a.
(PP p a ~ Bool, RefinedC opts p a) =>
a -> Either String a
evalBool5 @opts @op PP ip i
i of
Left String
e -> String -> Get (Refined5 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Get (Refined5 opts ip op i))
-> String -> Get (Refined5 opts ip op i)
forall a b. (a -> b) -> a -> b
$ String
"Refined5(Binary:get):" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
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 String (PP ip i), Tree PE)
forall a. TT a -> (Either String 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 String Bool, Tree PE)
forall a. TT a -> (Either String 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 String
e,Tree PE
t2) -> (PP ip i -> Tree PE -> String -> Tree PE -> RResults2 (PP ip i)
forall a. a -> Tree PE -> String -> Tree PE -> RResults2 a
RTF PP ip i
a Tree PE
t1 String
e Tree PE
t2, Maybe (Refined5 opts ip op i)
forall a. Maybe a
Nothing)
(Left String
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 (String -> Tree PE -> RResults2 (PP ip i)
forall a. String -> Tree PE -> RResults2 a
RF String
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 String 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 String Bool
lr,Tree PE
p2) = TT Bool -> (Either String Bool, Tree PE)
forall a. TT a -> (Either String a, Tree PE)
getValAndPE TT Bool
pp
z :: String
z = let zz :: String
zz = Tree PE
p2 Tree PE -> Getting String (Tree PE) String -> String
forall s a. s -> Getting a s a -> a
^. (PE -> Const String PE) -> Tree PE -> Const String (Tree PE)
forall a. Lens' (Tree a) a
root ((PE -> Const String PE) -> Tree PE -> Const String (Tree PE))
-> ((String -> Const String String) -> PE -> Const String PE)
-> Getting String (Tree PE) String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Const String String) -> PE -> Const String PE
Lens' PE String
peString
in if (Char -> Bool) -> String -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace String
zz then String
"FalseP" else String
"{" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
zz String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"}"
w :: Either String a
w = case Either String Bool
lr of
Right Bool
True -> a -> Either String a
forall a b. b -> Either a b
Right a
i
Right Bool
False -> String -> Either String a
forall a b. a -> Either a b
Left (String -> Either String a) -> String -> Either String a
forall a b. (a -> b) -> a -> b
$ String -> ShowS
joinStrings String
"false boolean check" String
z
Left String
e -> String -> Either String a
forall a b. a -> Either a b
Left (String -> Either String a) -> String -> Either String a
forall a b. (a -> b) -> a -> b
$ String -> ShowS
joinStrings String
"failed boolean check " String
e
in ShowS -> Either String a -> Either String a
forall (a :: Type -> Type -> Type) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left (String -> ShowS
forall a. [a] -> [a] -> [a]
++ (String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ POpts -> Tree PE -> String
prtTreePure POpts
opts Tree PE
p2)) Either String a
w
newtype Refined5Exception = Refined5Exception String
deriving stock (forall x. Refined5Exception -> Rep Refined5Exception x)
-> (forall x. Rep Refined5Exception x -> Refined5Exception)
-> Generic Refined5Exception
forall x. Rep Refined5Exception x -> Refined5Exception
forall x. Refined5Exception -> Rep Refined5Exception x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Refined5Exception x -> Refined5Exception
$cfrom :: forall x. Refined5Exception -> Rep Refined5Exception x
Generic
instance Show Refined5Exception where
show :: Refined5Exception -> String
show (Refined5Exception String
e) = String
"Refined5Exception:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
e
instance E.Exception Refined5Exception where
displayException :: Refined5Exception -> String
displayException = Refined5Exception -> String
forall a. Show a => a -> String
show