{-# 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 DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# 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'
, Refined2Exception(..)
) 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)
import qualified Control.Exception as E
import GHC.Generics (Generic)
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 (Refined2Exception -> Refined2 opts ip op i
forall a e. Exception e => e -> a
E.throw (Refined2Exception -> Refined2 opts ip op i)
-> (Msg2 -> Refined2Exception) -> Msg2 -> Refined2 opts ip op i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Refined2Exception
Refined2Exception (String -> Refined2Exception)
-> (Msg2 -> String) -> Msg2 -> Refined2Exception
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Msg2 -> String
forall a. Show a => a -> String
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 stock instance
( Refined2C opts ip op i
, Show i
, Show (PP ip i)
) => Show (Refined2 opts ip op i)
deriving stock instance
( Refined2C opts ip op i
, Eq i
, Eq (PP ip i)
) => Eq (Refined2 opts ip op i)
deriving stock instance
( Refined2C opts ip op i
, Ord i
, Ord (PP ip i)
) => Ord (Refined2 opts ip op i)
deriving stock 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 :: String -> Refined2 opts ip op i
fromString String
i =
case String -> Either Msg2 (Refined2 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 (Refined2 opts ip op i)
newRefined2 String
i of
Left Msg2
e -> Refined2Exception -> Refined2 opts ip op i
forall a e. Exception e => e -> a
E.throw (Refined2Exception -> Refined2 opts ip op i)
-> Refined2Exception -> Refined2 opts ip op i
forall a b. (a -> b) -> a -> b
$ String -> Refined2Exception
Refined2Exception (String -> Refined2Exception) -> String -> Refined2Exception
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 Refined2 opts ip op String
r -> Refined2 opts ip op i
Refined2 opts ip op String
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 (String -> Lexeme
RL.Ident String
"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 String (PP op (PP ip i))
lr = 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
fld1
case Either String (PP op (PP ip i))
lr of
Left {} -> String -> ReadPrec (Refined2 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
""
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 -> String -> ReadPrec (Refined2 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
""
)
)
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 -> String -> Parser (Refined2 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Parser (Refined2 opts ip op i))
-> String -> Parser (Refined2 opts ip op i)
forall a b. (a -> b) -> a -> b
$ String
"Refined2(FromJSON:parseJSON):" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg2 -> String
forall a. Show a => a -> String
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
r :: Int
r = POpts -> Int
getMaxRecursionValue POpts
o
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 | Int
cnt Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
r -> Refined2Exception -> Gen (Refined2 opts ip op i)
forall a e. Exception e => e -> a
E.throw (Refined2Exception -> Gen (Refined2 opts ip op i))
-> Refined2Exception -> Gen (Refined2 opts ip op i)
forall a b. (a -> b) -> a -> b
$ String -> Refined2Exception
Refined2Exception (String -> Refined2Exception) -> String -> Refined2Exception
forall a b. (a -> b) -> a -> b
$ POpts -> ShowS
setOtherEffects POpts
o ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"genRefined2P 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 (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 -> String -> Gen (Refined2 opts ip op i)
forall x. HasCallStack => String -> x
errorInProgram (String -> Gen (Refined2 opts ip op i))
-> String -> Gen (Refined2 opts ip op i)
forall a b. (a -> b) -> a -> b
$ String
"conversion failed:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg2 -> String
forall a. Show a => a -> String
show Msg2
e
Right Refined2 opts ip op i
ret -> 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
ret
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 -> String -> Get (Refined2 opts ip op i)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Get (Refined2 opts ip op i))
-> String -> Get (Refined2 opts ip op i)
forall a b. (a -> b) -> a -> b
$ String
"Refined2(Binary:get):" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Msg2 -> String
forall a. Show a => a -> String
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 stock Int -> RResults2 a -> ShowS
[RResults2 a] -> ShowS
RResults2 a -> String
(Int -> RResults2 a -> ShowS)
-> (RResults2 a -> String)
-> ([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 -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RResults2 a] -> ShowS
$cshowList :: forall a. Show a => [RResults2 a] -> ShowS
show :: RResults2 a -> String
$cshow :: forall a. Show a => RResults2 a -> String
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 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 (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 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, 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 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 (Refined2 opts ip op i)
forall a. Maybe a
Nothing)
(Left String
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 (String -> Tree PE -> RResults2 (PP ip i)
forall a. String -> Tree PE -> RResults2 a
RF String
e Tree PE
t1, Maybe (Refined2 opts ip op i)
forall a. Maybe a
Nothing)
data Msg2 = Msg2 { Msg2 -> String
m2Desc :: !String
, Msg2 -> String
m2Short :: !String
, Msg2 -> String
m2Long :: !String
, Msg2 -> ValP
m2ValP :: !ValP
} deriving stock 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 -> String
show (Msg2 String
a String
b String
c ValP
_d) = String -> ShowS
joinStrings String
a String
b String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String -> ShowS
nullIf String
"\n" String
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 String
msg = String
"*** " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> ShowS
formatOMsg POpts
opts String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
msg String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" ***\n"
msg1 :: a -> String
msg1 a
a = ShowS
outmsg (String
"Step 1. Success Initial Conversion(ip) (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ POpts -> a -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")")
mkMsg2 :: String -> String -> String -> ValP -> Msg2
mkMsg2 String
m String
n String
r ValP
bp | POpts -> Bool
hasNoTree POpts
opts = String -> String -> String -> ValP -> Msg2
Msg2 String
m String
n String
"" ValP
bp
| Bool
otherwise = String -> String -> String -> ValP -> Msg2
Msg2 String
m String
n String
r ValP
bp
in case RResults2 a
v of
RF String
e Tree PE
t1 ->
let (String
m,String
n) = (String
"Step 1. " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Long -> POpts -> ValP -> String
colorValP Long
Short POpts
opts (String -> ValP
FailP String
e) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Initial Conversion(ip)", String
e)
r :: String
r = ShowS
outmsg String
m
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> String
prtTreePure POpts
opts Tree PE
t1
in String -> String -> String -> ValP -> Msg2
mkMsg2 String
m String
n String
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 String
e Tree PE
t2 ->
let (String
m,String
n) = (String
"Step 2. " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Long -> POpts -> ValP -> String
colorValP Long
Short POpts
opts (String -> ValP
FailP String
e) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Boolean Check(op)", String
e)
r :: String
r = a -> String
msg1 a
a
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> String
prtTreePure POpts
opts Tree PE
t1
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\n"
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ShowS
outmsg String
m
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> String
prtTreePure POpts
opts Tree PE
t2
in String -> String -> String -> ValP -> Msg2
mkMsg2 String
m String
n String
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 (String
m,String
n) = (String
"Step 2. " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Long -> POpts -> ValP -> String
colorValP Long
Short POpts
opts ValP
FalseP String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Boolean Check(op)", String
z)
z :: String
z = let w :: String
w = Tree PE
t2 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
w then String
"FalseP" else String
"{" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
w String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"}"
r :: String
r = a -> String
msg1 a
a
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> String
prtTreePure POpts
opts Tree PE
t1
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\n"
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ShowS
outmsg String
m
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> String
prtTreePure POpts
opts Tree PE
t2
in String -> String -> String -> ValP -> Msg2
mkMsg2 String
m String
n String
r ValP
FalseP
RTTrue a
a Tree PE
t1 Tree PE
t2 ->
let (String
m,String
n) = (String
"Step 2. True Boolean Check(op)", String
"")
r :: String
r = a -> String
msg1 a
a
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> String
prtTreePure POpts
opts Tree PE
t1
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\n"
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ShowS
outmsg String
m
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Tree PE -> String
prtTreePure POpts
opts Tree PE
t2
in String -> String -> String -> ValP -> Msg2
mkMsg2 String
m String
n String
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
newtype Refined2Exception = Refined2Exception String
deriving (forall x. Refined2Exception -> Rep Refined2Exception x)
-> (forall x. Rep Refined2Exception x -> Refined2Exception)
-> Generic Refined2Exception
forall x. Rep Refined2Exception x -> Refined2Exception
forall x. Refined2Exception -> Rep Refined2Exception x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Refined2Exception x -> Refined2Exception
$cfrom :: forall x. Refined2Exception -> Rep Refined2Exception x
Generic
instance Show Refined2Exception where
show :: Refined2Exception -> String
show (Refined2Exception String
e) = String
"Refined2Exception:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
e
instance E.Exception Refined2Exception where
displayException :: Refined2Exception -> String
displayException = Refined2Exception -> String
forall a. Show a => a -> String
show