{-# OPTIONS -Wno-redundant-constraints #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# 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.Refined2 (
Refined2
, r2In
, r2Out
, Refined2C
, Msg2 (..)
, RResults2 (..)
, prt2Impl
, eval2P
, eval2M
, newRefined2
, newRefined2'
, newRefined2P
, newRefined2P'
, MakeR2
, mkProxy2
, mkProxy2'
, genRefined2
, genRefined2P
, unsafeRefined2
, unsafeRefined2'
) where
import Predicate.Core
import Predicate.Misc
import Predicate.Util
import Data.Tree (Tree)
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 Data.Maybe (isJust)
import Control.Lens
import Data.Tree.Lens (root)
import Data.Char (isSpace)
import Data.String (IsString(..))
import Data.Hashable (Hashable(..))
import GHC.Stack (HasCallStack)
import Test.QuickCheck
import Control.DeepSeq (rnf, rnf2, NFData)
data Refined2 (opts :: Opt) ip op i = Refined2 !(PP ip i) !i
r2In :: Refined2 (opts :: Opt) ip op i -> PP ip i
r2In :: Refined2 opts ip op i -> PP ip i
r2In (Refined2 PP ip i
ppi i
_) = PP ip i
ppi
r2Out :: Refined2 (opts :: Opt) ip op i -> i
r2Out :: Refined2 opts ip op i -> i
r2Out (Refined2 PP ip i
_ i
i) = i
i
type role Refined2 phantom nominal nominal nominal
unsafeRefined2' :: forall opts ip op i
. ( Show (PP ip i)
, Refined2C opts ip op i
, HasCallStack
)
=> i
-> Refined2 opts ip op i
unsafeRefined2' :: i -> Refined2 opts ip op i
unsafeRefined2' = (Msg2 -> Refined2 opts ip op i)
-> (Refined2 opts ip op i -> Refined2 opts ip op i)
-> Either Msg2 (Refined2 opts ip op i)
-> Refined2 opts ip op i
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ([Char] -> Refined2 opts ip op i
forall a. HasCallStack => [Char] -> a
error ([Char] -> Refined2 opts ip op i)
-> (Msg2 -> [Char]) -> Msg2 -> Refined2 opts ip op i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Msg2 -> [Char]
forall a. Show a => a -> [Char]
show) Refined2 opts ip op i -> Refined2 opts ip op i
forall a. a -> a
id (Either Msg2 (Refined2 opts ip op i) -> Refined2 opts ip op i)
-> (i -> Either Msg2 (Refined2 opts ip op i))
-> i
-> Refined2 opts ip op i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. i -> Either Msg2 (Refined2 opts ip op i)
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
(Refined2C opts ip op i, Show (PP ip i)) =>
i -> Either Msg2 (Refined2 opts ip op i)
newRefined2
unsafeRefined2 :: forall opts ip op i
. Refined2C opts ip op i
=> PP ip i
-> i
-> Refined2 opts ip op i
unsafeRefined2 :: PP ip i -> i -> Refined2 opts ip op i
unsafeRefined2 = PP ip i -> i -> Refined2 opts ip op i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
PP ip i -> i -> Refined2 opts ip op i
Refined2
type Refined2C opts ip op i =
( OptC opts
, P ip i
, P op (PP ip i)
, PP op (PP ip i) ~ Bool
)
deriving instance ( Refined2C opts ip op i
, Show i
, Show (PP ip i)
) => Show (Refined2 opts ip op i)
deriving instance ( Refined2C opts ip op i
, Eq i
, Eq (PP ip i)
) => Eq (Refined2 opts ip op i)
deriving instance ( Refined2C opts ip op i
, Ord i
, Ord (PP ip i)
) => Ord (Refined2 opts ip op i)
deriving instance ( Refined2C opts ip op i
, TH.Lift (PP ip i)
, TH.Lift i
) => TH.Lift (Refined2 opts ip op i)
instance ( Refined2C opts ip op i
, NFData i
, NFData (PP ip i)
) => NFData (Refined2 opts ip op i) where
rnf :: Refined2 opts ip op i -> ()
rnf (Refined2 PP ip i
a i
b) = (PP ip i, i) -> ()
forall (p :: Type -> Type -> Type) a b.
(NFData2 p, NFData a, NFData b) =>
p a b -> ()
rnf2 (PP ip i
a,i
b)
instance ( i ~ String
, Refined2C opts ip op i
, Show (PP ip i)
) => IsString (Refined2 opts ip op i) where
fromString :: [Char] -> Refined2 opts ip op i
fromString [Char]
i =
case [Char] -> Either Msg2 (Refined2 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 (Refined2 opts ip op i)
newRefined2 [Char]
i of
Left Msg2
e -> [Char] -> Refined2 opts ip op i
forall a. HasCallStack => [Char] -> a
error ([Char] -> Refined2 opts ip op i)
-> [Char] -> Refined2 opts ip op i
forall a b. (a -> b) -> a -> b
$ [Char]
"Refined2(IsString:fromString):" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg2 -> [Char]
forall a. Show a => a -> [Char]
show Msg2
e
Right Refined2 opts ip op [Char]
r -> Refined2 opts ip op i
Refined2 opts ip op [Char]
r
instance ( Refined2C opts ip op i
, Read (PP ip i)
, Read i
) => Read (Refined2 opts ip op i) where
readPrec :: ReadPrec (Refined2 opts ip op i)
readPrec
= ReadPrec (Refined2 opts ip op i)
-> ReadPrec (Refined2 opts ip op i)
forall a. ReadPrec a -> ReadPrec a
GR.parens
(Int
-> ReadPrec (Refined2 opts ip op i)
-> ReadPrec (Refined2 opts ip op i)
forall a. Int -> ReadPrec a -> ReadPrec a
PCR.prec
Int
10
(do Lexeme -> ReadPrec ()
GR.expectP ([Char] -> Lexeme
RL.Ident [Char]
"Refined2")
PP ip i
fld1 <- ReadPrec (PP ip i) -> ReadPrec (PP ip i)
forall a. ReadPrec a -> ReadPrec a
PCR.step ReadPrec (PP ip i)
forall a. Read a => ReadPrec a
GR.readPrec
i
fld2 <- ReadPrec i -> ReadPrec i
forall a. ReadPrec a -> ReadPrec a
PCR.step ReadPrec i
forall a. Read a => ReadPrec a
GR.readPrec
let lr :: Either [Char] (PP op (PP ip i))
lr = 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
fld1
case Either [Char] (PP op (PP ip i))
lr of
Left {} -> [Char] -> ReadPrec (Refined2 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
""
Right PP op (PP ip i)
True -> Refined2 opts ip op i -> ReadPrec (Refined2 opts ip op i)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PP ip i -> i -> Refined2 opts ip op i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
PP ip i -> i -> Refined2 opts ip op i
Refined2 PP ip i
fld1 i
fld2)
Right PP op (PP ip i)
False -> [Char] -> ReadPrec (Refined2 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail [Char]
""
)
)
readList :: ReadS [Refined2 opts ip op i]
readList = ReadS [Refined2 opts ip op i]
forall a. Read a => ReadS [a]
GR.readListDefault
readListPrec :: ReadPrec [Refined2 opts ip op i]
readListPrec = ReadPrec [Refined2 opts ip op i]
forall a. Read a => ReadPrec [a]
GR.readListPrecDefault
instance ( Refined2C opts ip op i
, ToJSON i
) => ToJSON (Refined2 opts ip op i) where
toJSON :: Refined2 opts ip op i -> Value
toJSON = i -> Value
forall a. ToJSON a => a -> Value
toJSON (i -> Value)
-> (Refined2 opts ip op i -> i) -> Refined2 opts ip op i -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined2 opts ip op i -> i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
Refined2 opts ip op i -> i
r2Out
instance ( Refined2C opts ip op i
, Show (PP ip i)
, FromJSON i
) => FromJSON (Refined2 opts ip op i) where
parseJSON :: Value -> Parser (Refined2 opts ip op i)
parseJSON Value
z = do
i
i <- Value -> Parser i
forall a. FromJSON a => Value -> Parser a
parseJSON @i Value
z
case i -> Either Msg2 (Refined2 opts ip op i)
forall k k (opts :: Opt) (ip :: k) (op :: k) 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 -> [Char] -> Parser (Refined2 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> Parser (Refined2 opts ip op i))
-> [Char] -> Parser (Refined2 opts ip op i)
forall a b. (a -> b) -> a -> b
$ [Char]
"Refined2(FromJSON:parseJSON):" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg2 -> [Char]
forall a. Show a => a -> [Char]
show Msg2
e
Right Refined2 opts ip op i
r -> Refined2 opts ip op i -> Parser (Refined2 opts ip op i)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Refined2 opts ip op i
r
instance ( Arbitrary i
, Refined2C opts ip op i
, Show (PP ip i)
) => Arbitrary (Refined2 opts ip op i) where
arbitrary :: Gen (Refined2 opts ip op i)
arbitrary = Gen i -> Gen (Refined2 opts ip op i)
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
(Refined2C opts ip op i, HasCallStack, Show (PP ip i)) =>
Gen i -> Gen (Refined2 opts ip op i)
genRefined2 Gen i
forall a. Arbitrary a => Gen a
arbitrary
genRefined2 ::
forall opts ip op i
. ( Refined2C opts ip op i
, HasCallStack
, Show (PP ip i)
)
=> Gen i
-> Gen (Refined2 opts ip op i)
genRefined2 :: Gen i -> Gen (Refined2 opts ip op i)
genRefined2 = Proxy '(opts, ip, op, i) -> Gen i -> Gen (Refined2 opts ip op i)
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
(Refined2C opts ip op i, HasCallStack, Show (PP ip i)) =>
Proxy '(opts, ip, op, i) -> Gen i -> Gen (Refined2 opts ip op i)
genRefined2P Proxy '(opts, ip, op, i)
forall k (t :: k). Proxy t
Proxy
genRefined2P ::
forall opts ip op i
. ( Refined2C opts ip op i
, HasCallStack
, Show (PP ip i)
)
=> Proxy '(opts,ip,op,i)
-> Gen i
-> Gen (Refined2 opts ip op i)
genRefined2P :: Proxy '(opts, ip, op, i) -> Gen i -> Gen (Refined2 opts ip op i)
genRefined2P Proxy '(opts, ip, op, i)
_ Gen i
g =
let o :: POpts
o = OptC opts => POpts
forall (o :: Opt). OptC o => POpts
getOpt @opts
f :: Int -> Gen (Refined2 opts ip op i)
f !Int
cnt = do
Maybe i
mi <- Gen i -> (i -> Bool) -> Gen (Maybe i)
forall a. Gen a -> (a -> Bool) -> Gen (Maybe a)
suchThatMaybe Gen i
g (Maybe (Refined2 opts ip op i) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Refined2 opts ip op i) -> Bool)
-> (i -> Maybe (Refined2 opts ip op i)) -> i -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
-> Maybe (Refined2 opts ip op i)
forall a b. (a, b) -> b
snd ((RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
-> Maybe (Refined2 opts ip op i))
-> (i -> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i)))
-> i
-> Maybe (Refined2 opts ip op i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
-> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
forall a. Identity a -> a
runIdentity (Identity (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
-> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i)))
-> (i
-> Identity (RResults2 (PP ip i), Maybe (Refined2 opts ip op i)))
-> i
-> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (Refined2 opts ip op i))
forall i (m :: Type -> Type).
(MonadEval m, Refined2C opts ip op i) =>
i -> m (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
eval2M @opts @ip @op)
case Maybe i
mi of
Maybe i
Nothing ->
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 (Refined2 opts ip op i)
forall a. HasCallStack => [Char] -> a
error ([Char] -> Gen (Refined2 opts ip op i))
-> [Char] -> Gen (Refined2 opts ip op i)
forall a b. (a -> b) -> a -> b
$ POpts -> ShowS
setOtherEffects POpts
o ([Char]
"genRefined2P 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 (Refined2 opts ip op i)
f (Int
cntInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
Just i
i ->
case i -> Either Msg2 (Refined2 opts ip op i)
forall k k (opts :: Opt) (ip :: k) (op :: k) 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 -> [Char] -> Gen (Refined2 opts ip op i)
forall x. HasCallStack => [Char] -> x
errorInProgram ([Char] -> Gen (Refined2 opts ip op i))
-> [Char] -> Gen (Refined2 opts ip op i)
forall a b. (a -> b) -> a -> b
$ [Char]
"conversion failed:" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg2 -> [Char]
forall a. Show a => a -> [Char]
show Msg2
e
Right Refined2 opts ip op i
r -> Refined2 opts ip op i -> Gen (Refined2 opts ip op i)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Refined2 opts ip op i
r
in Int -> Gen (Refined2 opts ip op i)
f Int
0
instance ( Refined2C opts ip op i
, Show (PP ip i)
, Binary i
) => Binary (Refined2 opts ip op i) where
get :: Get (Refined2 opts ip op i)
get = do
i
i <- Binary i => Get i
forall t. Binary t => Get t
B.get @i
case i -> Either Msg2 (Refined2 opts ip op i)
forall k k (opts :: Opt) (ip :: k) (op :: k) 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 -> [Char] -> Get (Refined2 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> Get (Refined2 opts ip op i))
-> [Char] -> Get (Refined2 opts ip op i)
forall a b. (a -> b) -> a -> b
$ [Char]
"Refined2(Binary:get):" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg2 -> [Char]
forall a. Show a => a -> [Char]
show Msg2
e
Right Refined2 opts ip op i
r -> Refined2 opts ip op i -> Get (Refined2 opts ip op i)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Refined2 opts ip op i
r
put :: Refined2 opts ip op i -> Put
put (Refined2 PP ip i
_ i
r) = i -> Put
forall t. Binary t => t -> Put
B.put @i i
r
instance ( Refined2C opts ip op i
, Hashable i
) => Hashable (Refined2 opts ip op i) where
hashWithSalt :: Int -> Refined2 opts ip op i -> Int
hashWithSalt Int
s (Refined2 PP ip i
_ i
b) = Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ i -> Int
forall a. Hashable a => a -> Int
hash i
b
data RResults2 a =
RF !String !(Tree PE)
| RTF !a !(Tree PE) !String !(Tree PE)
| RTFalse !a !(Tree PE) !(Tree PE)
| RTTrue !a !(Tree PE) !(Tree PE)
deriving Int -> RResults2 a -> ShowS
[RResults2 a] -> ShowS
RResults2 a -> [Char]
(Int -> RResults2 a -> ShowS)
-> (RResults2 a -> [Char])
-> ([RResults2 a] -> ShowS)
-> Show (RResults2 a)
forall a. Show a => Int -> RResults2 a -> ShowS
forall a. Show a => [RResults2 a] -> ShowS
forall a. Show a => RResults2 a -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [RResults2 a] -> ShowS
$cshowList :: forall a. Show a => [RResults2 a] -> ShowS
show :: RResults2 a -> [Char]
$cshow :: forall a. Show a => RResults2 a -> [Char]
showsPrec :: Int -> RResults2 a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> RResults2 a -> ShowS
Show
newRefined2' :: forall opts ip op i m
. ( MonadEval m
, Refined2C opts ip op i
, Show (PP ip i)
)
=> i
-> m (Either Msg2 (Refined2 opts ip op i))
newRefined2' :: i -> m (Either Msg2 (Refined2 opts ip op i))
newRefined2' = Proxy '(opts, ip, op, i)
-> i -> m (Either Msg2 (Refined2 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 (Refined2 opts ip op i))
newRefined2P' Proxy '(opts, ip, op, i)
forall k (t :: k). Proxy t
Proxy
newRefined2P' :: 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 (Refined2 opts ip op i))
newRefined2P' :: proxy '(opts, ip, op, i)
-> i -> m (Either Msg2 (Refined2 opts ip op i))
newRefined2P' proxy '(opts, ip, op, i)
_ i
i = do
(RResults2 (PP ip i)
ret,Maybe (Refined2 opts ip op i)
mr) <- i -> m (RResults2 (PP ip i), Maybe (Refined2 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 (Refined2 opts ip op i))
eval2M i
i
Either Msg2 (Refined2 opts ip op i)
-> m (Either Msg2 (Refined2 opts ip op i))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Either Msg2 (Refined2 opts ip op i)
-> m (Either Msg2 (Refined2 opts ip op i)))
-> Either Msg2 (Refined2 opts ip op i)
-> m (Either Msg2 (Refined2 opts ip op i))
forall a b. (a -> b) -> a -> b
$ Either Msg2 (Refined2 opts ip op i)
-> (Refined2 opts ip op i -> Either Msg2 (Refined2 opts ip op i))
-> Maybe (Refined2 opts ip op i)
-> Either Msg2 (Refined2 opts ip op i)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Msg2 -> Either Msg2 (Refined2 opts ip op i)
forall a b. a -> Either a b
Left (Msg2 -> Either Msg2 (Refined2 opts ip op i))
-> Msg2 -> Either Msg2 (Refined2 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) Refined2 opts ip op i -> Either Msg2 (Refined2 opts ip op i)
forall a b. b -> Either a b
Right Maybe (Refined2 opts ip op i)
mr
newRefined2 :: forall opts ip op i
. ( Refined2C opts ip op i
, Show (PP ip i)
) => i
-> Either Msg2 (Refined2 opts ip op i)
newRefined2 :: i -> Either Msg2 (Refined2 opts ip op i)
newRefined2 = Proxy '(opts, ip, op, i)
-> i -> Either Msg2 (Refined2 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 (Refined2 opts ip op i)
newRefined2P Proxy '(opts, ip, op, i)
forall k (t :: k). Proxy t
Proxy
newRefined2P :: forall opts ip op i
. ( Refined2C opts ip op i
, Show (PP ip i)
) => Proxy '(opts,ip,op,i)
-> i
-> Either Msg2 (Refined2 opts ip op i)
newRefined2P :: Proxy '(opts, ip, op, i)
-> i -> Either Msg2 (Refined2 opts ip op i)
newRefined2P Proxy '(opts, ip, op, i)
_ i
i =
let (RResults2 (PP ip i)
ret,Maybe (Refined2 opts ip op i)
mr) = Identity (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
-> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
forall a. Identity a -> a
runIdentity (Identity (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
-> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i)))
-> Identity (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
-> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
forall a b. (a -> b) -> a -> b
$ i -> Identity (RResults2 (PP ip i), Maybe (Refined2 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 (Refined2 opts ip op i))
eval2M i
i
in Either Msg2 (Refined2 opts ip op i)
-> (Refined2 opts ip op i -> Either Msg2 (Refined2 opts ip op i))
-> Maybe (Refined2 opts ip op i)
-> Either Msg2 (Refined2 opts ip op i)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Msg2 -> Either Msg2 (Refined2 opts ip op i)
forall a b. a -> Either a b
Left (Msg2 -> Either Msg2 (Refined2 opts ip op i))
-> Msg2 -> Either Msg2 (Refined2 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) Refined2 opts ip op i -> Either Msg2 (Refined2 opts ip op i)
forall a b. b -> Either a b
Right Maybe (Refined2 opts ip op i)
mr
eval2P :: 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 (Refined2 opts ip op i))
eval2P :: Proxy '(opts, ip, op, i)
-> i -> m (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
eval2P Proxy '(opts, ip, op, i)
_ = i -> m (RResults2 (PP ip i), Maybe (Refined2 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 (Refined2 opts ip op i))
eval2M
eval2M :: forall opts ip op i m
. ( MonadEval m
, Refined2C opts ip op i
)
=> i
-> m (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
eval2M :: i -> m (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
eval2M 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 (Refined2 opts ip op i))
-> m (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
-> m (RResults2 (PP ip i), Maybe (Refined2 opts ip op i)))
-> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
-> m (RResults2 (PP ip i), Maybe (Refined2 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, Refined2 opts ip op i -> Maybe (Refined2 opts ip op i)
forall a. a -> Maybe a
Just (PP ip i -> i -> Refined2 opts ip op i
forall k k (opts :: Opt) (ip :: k) (op :: k) i.
PP ip i -> i -> Refined2 opts ip op i
Refined2 PP ip i
a i
i))
(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 (Refined2 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 (Refined2 opts ip op i)
forall a. Maybe a
Nothing)
(Left [Char]
e,Tree PE
t1) -> (RResults2 (PP ip i), Maybe (Refined2 opts ip op i))
-> m (RResults2 (PP ip i), Maybe (Refined2 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 (Refined2 opts ip op i)
forall a. Maybe a
Nothing)
data Msg2 = Msg2 { Msg2 -> [Char]
m2Desc :: !String
, Msg2 -> [Char]
m2Short :: !String
, Msg2 -> [Char]
m2Long :: !String
, Msg2 -> ValP
m2ValP :: !ValP
} deriving Msg2 -> Msg2 -> Bool
(Msg2 -> Msg2 -> Bool) -> (Msg2 -> Msg2 -> Bool) -> Eq Msg2
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Msg2 -> Msg2 -> Bool
$c/= :: Msg2 -> Msg2 -> Bool
== :: Msg2 -> Msg2 -> Bool
$c== :: Msg2 -> Msg2 -> Bool
Eq
instance Show Msg2 where
show :: Msg2 -> [Char]
show (Msg2 [Char]
a [Char]
b [Char]
c ValP
_d) = [Char]
a [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char] -> ShowS
nullIf [Char]
" | " [Char]
b [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char] -> ShowS
nullIf [Char]
"\n" [Char]
c
prt2Impl :: forall a . Show a
=> POpts
-> RResults2 a
-> Msg2
prt2Impl :: POpts -> RResults2 a -> Msg2
prt2Impl POpts
opts RResults2 a
v =
let outmsg :: ShowS
outmsg [Char]
msg = [Char]
"*** " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> ShowS
formatOMsg POpts
opts [Char]
" " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
msg [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" ***\n"
msg1 :: a -> [Char]
msg1 a
a = ShowS
outmsg ([Char]
"Step 1. Success Initial Conversion(ip) (" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ POpts -> a -> [Char]
forall a. Show a => POpts -> a -> [Char]
showL POpts
opts a
a [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")")
mkMsg2 :: [Char] -> [Char] -> [Char] -> ValP -> Msg2
mkMsg2 [Char]
m [Char]
n [Char]
r ValP
bp | POpts -> Bool
hasNoTree POpts
opts = [Char] -> [Char] -> [Char] -> ValP -> Msg2
Msg2 [Char]
m [Char]
n [Char]
"" ValP
bp
| Bool
otherwise = [Char] -> [Char] -> [Char] -> ValP -> Msg2
Msg2 [Char]
m [Char]
n [Char]
r ValP
bp
in case RResults2 a
v of
RF [Char]
e Tree PE
t1 ->
let ([Char]
m,[Char]
n) = ([Char]
"Step 1. " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Long -> POpts -> ValP -> [Char]
colorValP Long
Short POpts
opts ([Char] -> ValP
FailP [Char]
e) [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" Initial Conversion(ip)", [Char]
e)
r :: [Char]
r = ShowS
outmsg [Char]
m
[Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> [Char]
prtTreePure POpts
opts Tree PE
t1
in [Char] -> [Char] -> [Char] -> ValP -> Msg2
mkMsg2 [Char]
m [Char]
n [Char]
r (Tree PE
t1 Tree PE -> Getting ValP (Tree PE) ValP -> ValP
forall s a. s -> Getting a s a -> a
^. (PE -> Const ValP PE) -> Tree PE -> Const ValP (Tree PE)
forall a. Lens' (Tree a) a
root ((PE -> Const ValP PE) -> Tree PE -> Const ValP (Tree PE))
-> ((ValP -> Const ValP ValP) -> PE -> Const ValP PE)
-> Getting ValP (Tree PE) ValP
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ValP -> Const ValP ValP) -> PE -> Const ValP PE
Lens' PE ValP
peValP)
RTF a
a Tree PE
t1 [Char]
e Tree PE
t2 ->
let ([Char]
m,[Char]
n) = ([Char]
"Step 2. " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Long -> POpts -> ValP -> [Char]
colorValP Long
Short POpts
opts ([Char] -> ValP
FailP [Char]
e) [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" Boolean Check(op)", [Char]
e)
r :: [Char]
r = a -> [Char]
msg1 a
a
[Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> [Char]
prtTreePure POpts
opts Tree PE
t1
[Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"\n"
[Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> ShowS
outmsg [Char]
m
[Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> [Char]
prtTreePure POpts
opts Tree PE
t2
in [Char] -> [Char] -> [Char] -> ValP -> Msg2
mkMsg2 [Char]
m [Char]
n [Char]
r (Tree PE
t2 Tree PE -> Getting ValP (Tree PE) ValP -> ValP
forall s a. s -> Getting a s a -> a
^. (PE -> Const ValP PE) -> Tree PE -> Const ValP (Tree PE)
forall a. Lens' (Tree a) a
root ((PE -> Const ValP PE) -> Tree PE -> Const ValP (Tree PE))
-> ((ValP -> Const ValP ValP) -> PE -> Const ValP PE)
-> Getting ValP (Tree PE) ValP
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ValP -> Const ValP ValP) -> PE -> Const ValP PE
Lens' PE ValP
peValP)
RTFalse a
a Tree PE
t1 Tree PE
t2 ->
let ([Char]
m,[Char]
n) = ([Char]
"Step 2. " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Long -> POpts -> ValP -> [Char]
colorValP Long
Short POpts
opts ValP
FalseP [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" Boolean Check(op)", [Char]
z)
z :: [Char]
z = let w :: [Char]
w = Tree PE
t2 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]
w then [Char]
"FalseP" else [Char]
"{" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
w [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"}"
r :: [Char]
r = a -> [Char]
msg1 a
a
[Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> [Char]
prtTreePure POpts
opts Tree PE
t1
[Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"\n"
[Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> ShowS
outmsg [Char]
m
[Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> [Char]
prtTreePure POpts
opts Tree PE
t2
in [Char] -> [Char] -> [Char] -> ValP -> Msg2
mkMsg2 [Char]
m [Char]
n [Char]
r ValP
FalseP
RTTrue a
a Tree PE
t1 Tree PE
t2 ->
let ([Char]
m,[Char]
n) = ([Char]
"Step 2. True Boolean Check(op)", [Char]
"")
r :: [Char]
r = a -> [Char]
msg1 a
a
[Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> [Char]
prtTreePure POpts
opts Tree PE
t1
[Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"\n"
[Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> ShowS
outmsg [Char]
m
[Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> [Char]
prtTreePure POpts
opts Tree PE
t2
in [Char] -> [Char] -> [Char] -> ValP -> Msg2
mkMsg2 [Char]
m [Char]
n [Char]
r (Tree PE
t2 Tree PE -> Getting ValP (Tree PE) ValP -> ValP
forall s a. s -> Getting a s a -> a
^. (PE -> Const ValP PE) -> Tree PE -> Const ValP (Tree PE)
forall a. Lens' (Tree a) a
root ((PE -> Const ValP PE) -> Tree PE -> Const ValP (Tree PE))
-> ((ValP -> Const ValP ValP) -> PE -> Const ValP PE)
-> Getting ValP (Tree PE) ValP
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ValP -> Const ValP ValP) -> PE -> Const ValP PE
Lens' PE ValP
peValP)
mkProxy2 :: forall z opts ip op i
. z ~ '(opts,ip,op,i)
=> Proxy '(opts,ip,op,i)
mkProxy2 :: Proxy '(opts, ip, op, i)
mkProxy2 = Proxy '(opts, ip, op, i)
forall k (t :: k). Proxy t
Proxy
mkProxy2' :: forall z opts ip op i
. ( z ~ '(ip,op,i)
, Refined2C opts ip op i
) => Proxy '(opts,ip,op,i)
mkProxy2' :: Proxy '(opts, ip, op, i)
mkProxy2' = Proxy '(opts, ip, op, i)
forall k (t :: k). Proxy t
Proxy
type family MakeR2 p where
MakeR2 '(opts,ip,op,i) = Refined2 opts ip op i