{-# 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 NoStarIsType #-}
{-# LANGUAGE EmptyDataDeriving #-}
module Predicate.Data.Either (
IsLeft
, IsRight
, MkLeft
, MkLeft'
, MkRight
, MkRight'
, Left'
, Right'
, LeftDef
, LeftFail
, RightDef
, RightFail
, EitherBool
, PartitionEithers
, type (|||)
, type (+++)
, EitherX
) where
import Predicate.Core
import Predicate.Misc
import Predicate.Util
import GHC.TypeLits (ErrorMessage((:$$:),(:<>:)))
import qualified GHC.TypeLits as GL
import Data.Proxy (Proxy(Proxy))
import Data.Kind (Type)
import Data.Either (isLeft, isRight, partitionEithers)
data Left' deriving Int -> Left' -> ShowS
[Left'] -> ShowS
Left' -> String
(Int -> Left' -> ShowS)
-> (Left' -> String) -> ([Left'] -> ShowS) -> Show Left'
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Left'] -> ShowS
$cshowList :: [Left'] -> ShowS
show :: Left' -> String
$cshow :: Left' -> String
showsPrec :: Int -> Left' -> ShowS
$cshowsPrec :: Int -> Left' -> ShowS
Show
instance Show a => P Left' (Either a x) where
type PP Left' (Either a x) = a
eval :: proxy Left'
-> POpts -> Either a x -> m (TT (PP Left' (Either a x)))
eval proxy Left'
_ POpts
opts Either a x
lr =
let msg0 :: String
msg0 = String
"Left'"
in TT a -> m (TT a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT a -> m (TT a)) -> TT a -> m (TT a)
forall a b. (a -> b) -> a -> b
$ case Either a x
lr of
Right x
_ -> POpts -> Val a -> String -> [Tree PE] -> TT a
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (String -> Val a
forall a. String -> Val a
Fail (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" found Right")) String
"" []
Left a
a -> POpts -> Val a -> String -> [Tree PE] -> TT a
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (a -> Val a
forall a. a -> Val a
Val a
a) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> a -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts a
a) []
data Right' deriving Int -> Right' -> ShowS
[Right'] -> ShowS
Right' -> String
(Int -> Right' -> ShowS)
-> (Right' -> String) -> ([Right'] -> ShowS) -> Show Right'
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Right'] -> ShowS
$cshowList :: [Right'] -> ShowS
show :: Right' -> String
$cshow :: Right' -> String
showsPrec :: Int -> Right' -> ShowS
$cshowsPrec :: Int -> Right' -> ShowS
Show
instance Show a => P Right' (Either x a) where
type PP Right' (Either x a) = a
eval :: proxy Right'
-> POpts -> Either x a -> m (TT (PP Right' (Either x a)))
eval proxy Right'
_ POpts
opts Either x a
lr =
let msg0 :: String
msg0 = String
"Right'"
in TT a -> m (TT a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT a -> m (TT a)) -> TT a -> m (TT a)
forall a b. (a -> b) -> a -> b
$ case Either x a
lr of
Left x
_ -> POpts -> Val a -> String -> [Tree PE] -> TT a
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (String -> Val a
forall a. String -> Val a
Fail (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" found Left")) String
"" []
Right a
a -> POpts -> Val a -> String -> [Tree PE] -> TT a
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (a -> Val a
forall a. a -> Val a
Val a
a) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> a -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts a
a) []
data p ||| q deriving Int -> (p ||| q) -> ShowS
[p ||| q] -> ShowS
(p ||| q) -> String
(Int -> (p ||| q) -> ShowS)
-> ((p ||| q) -> String) -> ([p ||| q] -> ShowS) -> Show (p ||| q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k). Int -> (p ||| q) -> ShowS
forall k (p :: k) k (q :: k). [p ||| q] -> ShowS
forall k (p :: k) k (q :: k). (p ||| q) -> String
showList :: [p ||| q] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k). [p ||| q] -> ShowS
show :: (p ||| q) -> String
$cshow :: forall k (p :: k) k (q :: k). (p ||| q) -> String
showsPrec :: Int -> (p ||| q) -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k). Int -> (p ||| q) -> ShowS
Show
infixr 2 |||
instance ( Show (PP p a)
, P p a
, P q b
, PP p a ~ PP q b
, Show a
, Show b
) => P (p ||| q) (Either a b) where
type PP (p ||| q) (Either a b) = PP p a
eval :: proxy (p ||| q)
-> POpts -> Either a b -> m (TT (PP (p ||| q) (Either a b)))
eval proxy (p ||| q)
_ POpts
opts Either a b
lr = do
let msg0 :: String
msg0 = String
"(|||)"
case Either a b
lr of
Left a
a -> do
TT (PP q b)
pp <- Proxy p -> POpts -> a -> m (TT (PP p a))
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 p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts a
a
TT (PP q b) -> m (TT (PP q b))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP q b) -> m (TT (PP q b))) -> TT (PP q b) -> m (TT (PP q b))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP q b)
-> [Tree PE]
-> Either (TT (PP q b)) (PP q b)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (PP q b)
pp [] of
Left TT (PP q b)
e -> TT (PP q b)
e
Right PP q b
a1 -> let msg1 :: String
msg1 = String
msg0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" Left"
in POpts -> TT (PP q b) -> String -> [Tree PE] -> TT (PP q b)
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT (PP q b)
pp (POpts -> String -> PP q b -> a -> String
forall a1 a2.
(Show a1, Show a2) =>
POpts -> String -> a1 -> a2 -> String
show3 POpts
opts String
msg1 PP q b
a1 a
a) [TT (PP q b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP q b)
pp]
Right b
a -> do
TT (PP q b)
qq <- Proxy q -> POpts -> b -> m (TT (PP q b))
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 q
forall k (t :: k). Proxy t
Proxy @q) POpts
opts b
a
TT (PP q b) -> m (TT (PP q b))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP q b) -> m (TT (PP q b))) -> TT (PP q b) -> m (TT (PP q b))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP q b)
-> [Tree PE]
-> Either (TT (PP q b)) (PP q b)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (PP q b)
qq [] of
Left TT (PP q b)
e -> TT (PP q b)
e
Right PP q b
a1 ->
let msg1 :: String
msg1 = String
msg0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" Right"
in POpts -> TT (PP q b) -> String -> [Tree PE] -> TT (PP q b)
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT (PP q b)
qq (POpts -> String -> PP q b -> b -> String
forall a1 a2.
(Show a1, Show a2) =>
POpts -> String -> a1 -> a2 -> String
show3 POpts
opts String
msg1 PP q b
a1 b
a) [TT (PP q b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP q b)
qq]
data IsLeft deriving Int -> IsLeft -> ShowS
[IsLeft] -> ShowS
IsLeft -> String
(Int -> IsLeft -> ShowS)
-> (IsLeft -> String) -> ([IsLeft] -> ShowS) -> Show IsLeft
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IsLeft] -> ShowS
$cshowList :: [IsLeft] -> ShowS
show :: IsLeft -> String
$cshow :: IsLeft -> String
showsPrec :: Int -> IsLeft -> ShowS
$cshowsPrec :: Int -> IsLeft -> ShowS
Show
instance x ~ Either a b
=> P IsLeft x where
type PP IsLeft x = Bool
eval :: proxy IsLeft -> POpts -> x -> m (TT (PP IsLeft x))
eval proxy IsLeft
_ POpts
opts x
x = TT Bool -> m (TT Bool)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT Bool -> m (TT Bool)) -> TT Bool -> m (TT Bool)
forall a b. (a -> b) -> a -> b
$ POpts -> Bool -> String -> [Tree PE] -> TT Bool
mkNodeB POpts
opts (Either a b -> Bool
forall a b. Either a b -> Bool
isLeft x
Either a b
x) String
"IsLeft" []
data IsRight deriving Int -> IsRight -> ShowS
[IsRight] -> ShowS
IsRight -> String
(Int -> IsRight -> ShowS)
-> (IsRight -> String) -> ([IsRight] -> ShowS) -> Show IsRight
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IsRight] -> ShowS
$cshowList :: [IsRight] -> ShowS
show :: IsRight -> String
$cshow :: IsRight -> String
showsPrec :: Int -> IsRight -> ShowS
$cshowsPrec :: Int -> IsRight -> ShowS
Show
instance x ~ Either a b
=> P IsRight x where
type PP IsRight x = Bool
eval :: proxy IsRight -> POpts -> x -> m (TT (PP IsRight x))
eval proxy IsRight
_ POpts
opts x
x = TT Bool -> m (TT Bool)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT Bool -> m (TT Bool)) -> TT Bool -> m (TT Bool)
forall a b. (a -> b) -> a -> b
$ POpts -> Bool -> String -> [Tree PE] -> TT Bool
mkNodeB POpts
opts (Either a b -> Bool
forall a b. Either a b -> Bool
isRight x
Either a b
x) String
"IsRight" []
data p +++ q deriving Int -> (p +++ q) -> ShowS
[p +++ q] -> ShowS
(p +++ q) -> String
(Int -> (p +++ q) -> ShowS)
-> ((p +++ q) -> String) -> ([p +++ q] -> ShowS) -> Show (p +++ q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k). Int -> (p +++ q) -> ShowS
forall k (p :: k) k (q :: k). [p +++ q] -> ShowS
forall k (p :: k) k (q :: k). (p +++ q) -> String
showList :: [p +++ q] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k). [p +++ q] -> ShowS
show :: (p +++ q) -> String
$cshow :: forall k (p :: k) k (q :: k). (p +++ q) -> String
showsPrec :: Int -> (p +++ q) -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k). Int -> (p +++ q) -> ShowS
Show
infixr 2 +++
instance ( Show (PP p a)
, Show (PP q b)
, P p a
, P q b
, Show a
, Show b
) => P (p +++ q) (Either a b) where
type PP (p +++ q) (Either a b) = Either (PP p a) (PP q b)
eval :: proxy (p +++ q)
-> POpts -> Either a b -> m (TT (PP (p +++ q) (Either a b)))
eval proxy (p +++ q)
_ POpts
opts Either a b
lr = do
let msg0 :: String
msg0 = String
"(+++)"
case Either a b
lr of
Left a
a -> do
TT (PP p a)
pp <- Proxy p -> POpts -> a -> m (TT (PP p a))
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 p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts a
a
TT (Either (PP p a) (PP q b)) -> m (TT (Either (PP p a) (PP q b)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (Either (PP p a) (PP q b))
-> m (TT (Either (PP p a) (PP q b))))
-> TT (Either (PP p a) (PP q b))
-> m (TT (Either (PP p a) (PP q b)))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP p a)
-> [Tree PE]
-> Either (TT (Either (PP p a) (PP q b))) (PP p a)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (PP p a)
pp [] of
Left TT (Either (PP p a) (PP q b))
e -> TT (Either (PP p a) (PP q b))
e
Right PP p a
a1 ->
let msg1 :: String
msg1 = String
msg0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" Left"
in POpts
-> Val (Either (PP p a) (PP q b))
-> String
-> [Tree PE]
-> TT (Either (PP p a) (PP q b))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (Either (PP p a) (PP q b) -> Val (Either (PP p a) (PP q b))
forall a. a -> Val a
Val (PP p a -> Either (PP p a) (PP q b)
forall a b. a -> Either a b
Left PP p a
a1)) (String
msg1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> PP p a -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts PP p a
a1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> String -> a -> String
forall a. Show a => POpts -> String -> a -> String
showVerbose POpts
opts String
" | " a
a) [TT (PP p a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p a)
pp]
Right b
a -> do
TT (PP q b)
qq <- Proxy q -> POpts -> b -> m (TT (PP q b))
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 q
forall k (t :: k). Proxy t
Proxy @q) POpts
opts b
a
TT (Either (PP p a) (PP q b)) -> m (TT (Either (PP p a) (PP q b)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (Either (PP p a) (PP q b))
-> m (TT (Either (PP p a) (PP q b))))
-> TT (Either (PP p a) (PP q b))
-> m (TT (Either (PP p a) (PP q b)))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP q b)
-> [Tree PE]
-> Either (TT (Either (PP p a) (PP q b))) (PP q b)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (PP q b)
qq [] of
Left TT (Either (PP p a) (PP q b))
e -> TT (Either (PP p a) (PP q b))
e
Right PP q b
a1 ->
let msg1 :: String
msg1 = String
msg0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" Right"
in POpts
-> Val (Either (PP p a) (PP q b))
-> String
-> [Tree PE]
-> TT (Either (PP p a) (PP q b))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (Either (PP p a) (PP q b) -> Val (Either (PP p a) (PP q b))
forall a. a -> Val a
Val (PP q b -> Either (PP p a) (PP q b)
forall a b. b -> Either a b
Right PP q b
a1)) (String
msg1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> PP q b -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts PP q b
a1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> String -> b -> String
forall a. Show a => POpts -> String -> a -> String
showVerbose POpts
opts String
" | " b
a) [TT (PP q b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP q b)
qq]
data PartitionEithers deriving Int -> PartitionEithers -> ShowS
[PartitionEithers] -> ShowS
PartitionEithers -> String
(Int -> PartitionEithers -> ShowS)
-> (PartitionEithers -> String)
-> ([PartitionEithers] -> ShowS)
-> Show PartitionEithers
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PartitionEithers] -> ShowS
$cshowList :: [PartitionEithers] -> ShowS
show :: PartitionEithers -> String
$cshow :: PartitionEithers -> String
showsPrec :: Int -> PartitionEithers -> ShowS
$cshowsPrec :: Int -> PartitionEithers -> ShowS
Show
instance ( Show a
, Show b
) => P PartitionEithers [Either a b] where
type PP PartitionEithers [Either a b] = ([a], [b])
eval :: proxy PartitionEithers
-> POpts
-> [Either a b]
-> m (TT (PP PartitionEithers [Either a b]))
eval proxy PartitionEithers
_ POpts
opts [Either a b]
as =
let msg0 :: String
msg0 = String
"PartitionEithers"
b :: ([a], [b])
b = [Either a b] -> ([a], [b])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either a b]
as
in TT ([a], [b]) -> m (TT ([a], [b]))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT ([a], [b]) -> m (TT ([a], [b])))
-> TT ([a], [b]) -> m (TT ([a], [b]))
forall a b. (a -> b) -> a -> b
$ POpts -> Val ([a], [b]) -> String -> [Tree PE] -> TT ([a], [b])
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (([a], [b]) -> Val ([a], [b])
forall a. a -> Val a
Val ([a], [b])
b) (POpts -> String -> ([a], [b]) -> [Either a b] -> String
forall a1 a2.
(Show a1, Show a2) =>
POpts -> String -> a1 -> a2 -> String
show3 POpts
opts String
msg0 ([a], [b])
b [Either a b]
as) []
data EitherBool b p q deriving Int -> EitherBool b p q -> ShowS
[EitherBool b p q] -> ShowS
EitherBool b p q -> String
(Int -> EitherBool b p q -> ShowS)
-> (EitherBool b p q -> String)
-> ([EitherBool b p q] -> ShowS)
-> Show (EitherBool b p q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (b :: k) k (p :: k) k (q :: k).
Int -> EitherBool b p q -> ShowS
forall k (b :: k) k (p :: k) k (q :: k).
[EitherBool b p q] -> ShowS
forall k (b :: k) k (p :: k) k (q :: k). EitherBool b p q -> String
showList :: [EitherBool b p q] -> ShowS
$cshowList :: forall k (b :: k) k (p :: k) k (q :: k).
[EitherBool b p q] -> ShowS
show :: EitherBool b p q -> String
$cshow :: forall k (b :: k) k (p :: k) k (q :: k). EitherBool b p q -> String
showsPrec :: Int -> EitherBool b p q -> ShowS
$cshowsPrec :: forall k (b :: k) k (p :: k) k (q :: k).
Int -> EitherBool b p q -> ShowS
Show
instance ( Show (PP p a)
, P p a
, Show (PP q a)
, P q a
, P b a
, PP b a ~ Bool
) => P (EitherBool b p q) a where
type PP (EitherBool b p q) a = Either (PP p a) (PP q a)
eval :: proxy (EitherBool b p q)
-> POpts -> a -> m (TT (PP (EitherBool b p q) a))
eval proxy (EitherBool b p q)
_ POpts
opts a
z = do
let msg0 :: String
msg0 = String
"EitherBool"
TT Bool
bb <- Proxy b -> POpts -> a -> m (TT (PP b 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 b
forall k (t :: k). Proxy t
Proxy @b) POpts
opts a
z
case Inline
-> POpts
-> String
-> TT Bool
-> [Tree PE]
-> Either (TT (Either (PP p a) (PP q a))) Bool
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" b failed") TT Bool
bb [] of
Left TT (Either (PP p a) (PP q a))
e -> TT (Either (PP p a) (PP q a)) -> m (TT (Either (PP p a) (PP q a)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (Either (PP p a) (PP q a))
e
Right Bool
False -> do
TT (PP p a)
pp <- Proxy p -> POpts -> a -> m (TT (PP p a))
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 p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts a
z
TT (Either (PP p a) (PP q a)) -> m (TT (Either (PP p a) (PP q a)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (Either (PP p a) (PP q a))
-> m (TT (Either (PP p a) (PP q a))))
-> TT (Either (PP p a) (PP q a))
-> m (TT (Either (PP p a) (PP q a)))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP p a)
-> [Tree PE]
-> Either (TT (Either (PP p a) (PP q a))) (PP p a)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" p failed") TT (PP p a)
pp [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
bb] of
Left TT (Either (PP p a) (PP q a))
e -> TT (Either (PP p a) (PP q a))
e
Right PP p a
p -> POpts
-> Val (Either (PP p a) (PP q a))
-> String
-> [Tree PE]
-> TT (Either (PP p a) (PP q a))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (Either (PP p a) (PP q a) -> Val (Either (PP p a) (PP q a))
forall a. a -> Val a
Val (PP p a -> Either (PP p a) (PP q a)
forall a b. a -> Either a b
Left PP p a
p)) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(False) Left " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> PP p a -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts PP p a
p) [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
bb, TT (PP p a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p a)
pp]
Right Bool
True -> do
TT (PP q a)
qq <- Proxy q -> POpts -> a -> m (TT (PP q a))
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 q
forall k (t :: k). Proxy t
Proxy @q) POpts
opts a
z
TT (Either (PP p a) (PP q a)) -> m (TT (Either (PP p a) (PP q a)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (Either (PP p a) (PP q a))
-> m (TT (Either (PP p a) (PP q a))))
-> TT (Either (PP p a) (PP q a))
-> m (TT (Either (PP p a) (PP q a)))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP q a)
-> [Tree PE]
-> Either (TT (Either (PP p a) (PP q a))) (PP q a)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" q failed") TT (PP q a)
qq [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
bb] of
Left TT (Either (PP p a) (PP q a))
e -> TT (Either (PP p a) (PP q a))
e
Right PP q a
q -> POpts
-> Val (Either (PP p a) (PP q a))
-> String
-> [Tree PE]
-> TT (Either (PP p a) (PP q a))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (Either (PP p a) (PP q a) -> Val (Either (PP p a) (PP q a))
forall a. a -> Val a
Val (PP q a -> Either (PP p a) (PP q a)
forall a b. b -> Either a b
Right PP q a
q)) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(True) Right " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> PP q a -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts PP q a
q) [TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
bb, TT (PP q a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP q a)
qq]
data EitherX p q r deriving Int -> EitherX p q r -> ShowS
[EitherX p q r] -> ShowS
EitherX p q r -> String
(Int -> EitherX p q r -> ShowS)
-> (EitherX p q r -> String)
-> ([EitherX p q r] -> ShowS)
-> Show (EitherX p q r)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k) k (r :: k).
Int -> EitherX p q r -> ShowS
forall k (p :: k) k (q :: k) k (r :: k). [EitherX p q r] -> ShowS
forall k (p :: k) k (q :: k) k (r :: k). EitherX p q r -> String
showList :: [EitherX p q r] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k) k (r :: k). [EitherX p q r] -> ShowS
show :: EitherX p q r -> String
$cshow :: forall k (p :: k) k (q :: k) k (r :: k). EitherX p q r -> String
showsPrec :: Int -> EitherX p q r -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k) k (r :: k).
Int -> EitherX p q r -> ShowS
Show
instance ( P r x
, P p (x,a)
, P q (x,b)
, PP r x ~ Either a b
, PP p (x,a) ~ c
, PP q (x,b) ~ c
) => P (EitherX p q r) x where
type PP (EitherX p q r) x = EitherXT (PP r x) x p
eval :: proxy (EitherX p q r)
-> POpts -> x -> m (TT (PP (EitherX p q r) x))
eval proxy (EitherX p q r)
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"EitherX"
TT (Either a b)
rr <- Proxy r -> POpts -> x -> m (TT (PP r x))
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 r
forall k (t :: k). Proxy t
Proxy @r) POpts
opts x
x
case Inline
-> POpts
-> String
-> TT (Either a b)
-> [Tree PE]
-> Either (TT c) (Either a b)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (Either a b)
rr [] of
Left TT c
e -> TT c -> m (TT c)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT c
e
Right (Left a
a) -> do
let msg1 :: String
msg1 = String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(Left)"
TT c
pp <- Proxy p -> POpts -> (x, a) -> m (TT (PP p (x, a)))
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 p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts (x
x,a
a)
TT c -> m (TT c)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT c -> m (TT c)) -> TT c -> m (TT c)
forall a b. (a -> b) -> a -> b
$ case Inline -> POpts -> String -> TT c -> [Tree PE] -> Either (TT c) c
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg1 TT c
pp [TT (Either a b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Either a b)
rr] of
Left TT c
e -> TT c
e
Right c
_ -> POpts -> TT c -> String -> [Tree PE] -> TT c
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT c
pp String
msg1 [TT (Either a b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Either a b)
rr, TT c -> Tree PE
forall a. TT a -> Tree PE
hh TT c
pp]
Right (Right b
b) -> do
let msg1 :: String
msg1 = String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(Right)"
TT c
qq <- Proxy q -> POpts -> (x, b) -> m (TT (PP q (x, b)))
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 q
forall k (t :: k). Proxy t
Proxy @q) POpts
opts (x
x,b
b)
TT c -> m (TT c)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT c -> m (TT c)) -> TT c -> m (TT c)
forall a b. (a -> b) -> a -> b
$ case Inline -> POpts -> String -> TT c -> [Tree PE] -> Either (TT c) c
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg1 TT c
qq [TT (Either a b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Either a b)
rr] of
Left TT c
e -> TT c
e
Right c
_ -> POpts -> TT c -> String -> [Tree PE] -> TT c
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT c
qq String
msg1 [TT (Either a b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Either a b)
rr, TT c -> Tree PE
forall a. TT a -> Tree PE
hh TT c
qq]
type family EitherXT lr x p where
EitherXT (Either a _b) x p = PP p (x,a)
EitherXT o _ _ = GL.TypeError (
'GL.Text "EitherXT: expected 'Either a b' "
':$$: 'GL.Text "o = "
':<>: 'GL.ShowType o)
data MkLeft' t p deriving Int -> MkLeft' t p -> ShowS
[MkLeft' t p] -> ShowS
MkLeft' t p -> String
(Int -> MkLeft' t p -> ShowS)
-> (MkLeft' t p -> String)
-> ([MkLeft' t p] -> ShowS)
-> Show (MkLeft' t p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (t :: k) k (p :: k). Int -> MkLeft' t p -> ShowS
forall k (t :: k) k (p :: k). [MkLeft' t p] -> ShowS
forall k (t :: k) k (p :: k). MkLeft' t p -> String
showList :: [MkLeft' t p] -> ShowS
$cshowList :: forall k (t :: k) k (p :: k). [MkLeft' t p] -> ShowS
show :: MkLeft' t p -> String
$cshow :: forall k (t :: k) k (p :: k). MkLeft' t p -> String
showsPrec :: Int -> MkLeft' t p -> ShowS
$cshowsPrec :: forall k (t :: k) k (p :: k). Int -> MkLeft' t p -> ShowS
Show
instance ( Show (PP p x)
, P p x
) => P (MkLeft' t p) x where
type PP (MkLeft' t p) x = Either (PP p x) (PP t x)
eval :: proxy (MkLeft' t p) -> POpts -> x -> m (TT (PP (MkLeft' t p) x))
eval proxy (MkLeft' t p)
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"MkLeft"
TT (PP p x)
pp <- Proxy p -> POpts -> x -> m (TT (PP p x))
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 p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts x
x
TT (Either (PP p x) (PP t x)) -> m (TT (Either (PP p x) (PP t x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (Either (PP p x) (PP t x))
-> m (TT (Either (PP p x) (PP t x))))
-> TT (Either (PP p x) (PP t x))
-> m (TT (Either (PP p x) (PP t x)))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP p x)
-> [Tree PE]
-> Either (TT (Either (PP p x) (PP t x))) (PP p x)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (PP p x)
pp [] of
Left TT (Either (PP p x) (PP t x))
e -> TT (Either (PP p x) (PP t x))
e
Right PP p x
p ->
let d :: Either (PP p x) (PP t x)
d = PP p x -> Either (PP p x) (PP t x)
forall a b. a -> Either a b
Left PP p x
p
in POpts
-> Val (Either (PP p x) (PP t x))
-> String
-> [Tree PE]
-> TT (Either (PP p x) (PP t x))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (Either (PP p x) (PP t x) -> Val (Either (PP p x) (PP t x))
forall a. a -> Val a
Val Either (PP p x) (PP t x)
d) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Left " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> PP p x -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts PP p x
p) [TT (PP p x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p x)
pp]
data MkLeft (t :: Type) p deriving Int -> MkLeft t p -> ShowS
[MkLeft t p] -> ShowS
MkLeft t p -> String
(Int -> MkLeft t p -> ShowS)
-> (MkLeft t p -> String)
-> ([MkLeft t p] -> ShowS)
-> Show (MkLeft t p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall t k (p :: k). Int -> MkLeft t p -> ShowS
forall t k (p :: k). [MkLeft t p] -> ShowS
forall t k (p :: k). MkLeft t p -> String
showList :: [MkLeft t p] -> ShowS
$cshowList :: forall t k (p :: k). [MkLeft t p] -> ShowS
show :: MkLeft t p -> String
$cshow :: forall t k (p :: k). MkLeft t p -> String
showsPrec :: Int -> MkLeft t p -> ShowS
$cshowsPrec :: forall t k (p :: k). Int -> MkLeft t p -> ShowS
Show
type MkLeftT (t :: Type) p = MkLeft' (Hole t) p
instance P (MkLeftT t p) x => P (MkLeft t p) x where
type PP (MkLeft t p) x = PP (MkLeftT t p) x
eval :: proxy (MkLeft t p) -> POpts -> x -> m (TT (PP (MkLeft t p) x))
eval proxy (MkLeft t p)
_ = Proxy (MkLeftT t p) -> POpts -> x -> m (TT (PP (MkLeftT t p) x))
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 (MkLeftT t p)
forall k (t :: k). Proxy t
Proxy @(MkLeftT t p))
data MkRight' t p deriving Int -> MkRight' t p -> ShowS
[MkRight' t p] -> ShowS
MkRight' t p -> String
(Int -> MkRight' t p -> ShowS)
-> (MkRight' t p -> String)
-> ([MkRight' t p] -> ShowS)
-> Show (MkRight' t p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (t :: k) k (p :: k). Int -> MkRight' t p -> ShowS
forall k (t :: k) k (p :: k). [MkRight' t p] -> ShowS
forall k (t :: k) k (p :: k). MkRight' t p -> String
showList :: [MkRight' t p] -> ShowS
$cshowList :: forall k (t :: k) k (p :: k). [MkRight' t p] -> ShowS
show :: MkRight' t p -> String
$cshow :: forall k (t :: k) k (p :: k). MkRight' t p -> String
showsPrec :: Int -> MkRight' t p -> ShowS
$cshowsPrec :: forall k (t :: k) k (p :: k). Int -> MkRight' t p -> ShowS
Show
instance ( Show (PP p x)
, P p x
) => P (MkRight' t p) x where
type PP (MkRight' t p) x = Either (PP t x) (PP p x)
eval :: proxy (MkRight' t p) -> POpts -> x -> m (TT (PP (MkRight' t p) x))
eval proxy (MkRight' t p)
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"MkRight"
TT (PP p x)
pp <- Proxy p -> POpts -> x -> m (TT (PP p x))
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 p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts x
x
TT (Either (PP t x) (PP p x)) -> m (TT (Either (PP t x) (PP p x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (Either (PP t x) (PP p x))
-> m (TT (Either (PP t x) (PP p x))))
-> TT (Either (PP t x) (PP p x))
-> m (TT (Either (PP t x) (PP p x)))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP p x)
-> [Tree PE]
-> Either (TT (Either (PP t x) (PP p x))) (PP p x)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (PP p x)
pp [] of
Left TT (Either (PP t x) (PP p x))
e -> TT (Either (PP t x) (PP p x))
e
Right PP p x
p ->
let d :: Either (PP t x) (PP p x)
d = PP p x -> Either (PP t x) (PP p x)
forall a b. b -> Either a b
Right PP p x
p
in POpts
-> Val (Either (PP t x) (PP p x))
-> String
-> [Tree PE]
-> TT (Either (PP t x) (PP p x))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (Either (PP t x) (PP p x) -> Val (Either (PP t x) (PP p x))
forall a. a -> Val a
Val Either (PP t x) (PP p x)
d) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Right " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> PP p x -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts PP p x
p) [TT (PP p x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p x)
pp]
data MkRight (t :: Type) p deriving Int -> MkRight t p -> ShowS
[MkRight t p] -> ShowS
MkRight t p -> String
(Int -> MkRight t p -> ShowS)
-> (MkRight t p -> String)
-> ([MkRight t p] -> ShowS)
-> Show (MkRight t p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall t k (p :: k). Int -> MkRight t p -> ShowS
forall t k (p :: k). [MkRight t p] -> ShowS
forall t k (p :: k). MkRight t p -> String
showList :: [MkRight t p] -> ShowS
$cshowList :: forall t k (p :: k). [MkRight t p] -> ShowS
show :: MkRight t p -> String
$cshow :: forall t k (p :: k). MkRight t p -> String
showsPrec :: Int -> MkRight t p -> ShowS
$cshowsPrec :: forall t k (p :: k). Int -> MkRight t p -> ShowS
Show
type MkRightT (t :: Type) p = MkRight' (Hole t) p
instance P (MkRightT t p) x => P (MkRight t p) x where
type PP (MkRight t p) x = PP (MkRightT t p) x
eval :: proxy (MkRight t p) -> POpts -> x -> m (TT (PP (MkRight t p) x))
eval proxy (MkRight t p)
_ = Proxy (MkRightT t p) -> POpts -> x -> m (TT (PP (MkRightT t p) x))
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 (MkRightT t p)
forall k (t :: k). Proxy t
Proxy @(MkRightT t p))
data LeftDef p q deriving Int -> LeftDef p q -> ShowS
[LeftDef p q] -> ShowS
LeftDef p q -> String
(Int -> LeftDef p q -> ShowS)
-> (LeftDef p q -> String)
-> ([LeftDef p q] -> ShowS)
-> Show (LeftDef p q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k). Int -> LeftDef p q -> ShowS
forall k (p :: k) k (q :: k). [LeftDef p q] -> ShowS
forall k (p :: k) k (q :: k). LeftDef p q -> String
showList :: [LeftDef p q] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k). [LeftDef p q] -> ShowS
show :: LeftDef p q -> String
$cshow :: forall k (p :: k) k (q :: k). LeftDef p q -> String
showsPrec :: Int -> LeftDef p q -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k). Int -> LeftDef p q -> ShowS
Show
instance ( PP q x ~ Either a b
, PP p (b,x) ~ a
, P q x
, P p (b,x)
) => P (LeftDef p q) x where
type PP (LeftDef p q) x = LeftT (PP q x)
eval :: proxy (LeftDef p q) -> POpts -> x -> m (TT (PP (LeftDef p q) x))
eval proxy (LeftDef p q)
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"LeftDef"
TT (Either a b)
qq <- Proxy q -> POpts -> x -> m (TT (PP q x))
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 q
forall k (t :: k). Proxy t
Proxy @q) POpts
opts x
x
case Inline
-> POpts
-> String
-> TT (Either a b)
-> [Tree PE]
-> Either (TT a) (Either a b)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (Either a b)
qq [] of
Left TT a
e -> TT a -> m (TT a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT a
e
Right Either a b
q ->
case Either a b
q of
Left a
a -> TT a -> m (TT a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT a -> m (TT a)) -> TT a -> m (TT a)
forall a b. (a -> b) -> a -> b
$ POpts -> Val a -> String -> [Tree PE] -> TT a
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (a -> Val a
forall a. a -> Val a
Val a
a) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Left") [TT (Either a b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Either a b)
qq]
Right b
b -> do
TT a
pp <- Proxy p -> POpts -> (b, x) -> m (TT (PP p (b, x)))
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 p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts (b
b,x
x)
TT a -> m (TT a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT a -> m (TT a)) -> TT a -> m (TT a)
forall a b. (a -> b) -> a -> b
$ case Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT a) a
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT a
pp [TT (Either a b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Either a b)
qq] of
Left TT a
e -> TT a
e
Right a
p -> POpts -> Val a -> String -> [Tree PE] -> TT a
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (a -> Val a
forall a. a -> Val a
Val a
p) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Right") [TT (Either a b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Either a b)
qq, TT a -> Tree PE
forall a. TT a -> Tree PE
hh TT a
pp]
data RightDef p q deriving Int -> RightDef p q -> ShowS
[RightDef p q] -> ShowS
RightDef p q -> String
(Int -> RightDef p q -> ShowS)
-> (RightDef p q -> String)
-> ([RightDef p q] -> ShowS)
-> Show (RightDef p q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k). Int -> RightDef p q -> ShowS
forall k (p :: k) k (q :: k). [RightDef p q] -> ShowS
forall k (p :: k) k (q :: k). RightDef p q -> String
showList :: [RightDef p q] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k). [RightDef p q] -> ShowS
show :: RightDef p q -> String
$cshow :: forall k (p :: k) k (q :: k). RightDef p q -> String
showsPrec :: Int -> RightDef p q -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k). Int -> RightDef p q -> ShowS
Show
instance ( PP q x ~ Either a b
, PP p (a,x) ~ b
, P q x
, P p (a,x)
) => P (RightDef p q) x where
type PP (RightDef p q) x = RightT (PP q x)
eval :: proxy (RightDef p q) -> POpts -> x -> m (TT (PP (RightDef p q) x))
eval proxy (RightDef p q)
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"RightDef"
TT (Either a b)
qq <- Proxy q -> POpts -> x -> m (TT (PP q x))
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 q
forall k (t :: k). Proxy t
Proxy @q) POpts
opts x
x
case Inline
-> POpts
-> String
-> TT (Either a b)
-> [Tree PE]
-> Either (TT b) (Either a b)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (Either a b)
qq [] of
Left TT b
e -> TT b -> m (TT b)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT b
e
Right Either a b
q ->
case Either a b
q of
Right b
b -> TT b -> m (TT b)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT b -> m (TT b)) -> TT b -> m (TT b)
forall a b. (a -> b) -> a -> b
$ POpts -> Val b -> String -> [Tree PE] -> TT b
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (b -> Val b
forall a. a -> Val a
Val b
b) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Right") [TT (Either a b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Either a b)
qq]
Left a
a -> do
TT b
pp <- Proxy p -> POpts -> (a, x) -> m (TT (PP p (a, x)))
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 p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts (a
a,x
x)
TT b -> m (TT b)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT b -> m (TT b)) -> TT b -> m (TT b)
forall a b. (a -> b) -> a -> b
$ case Inline -> POpts -> String -> TT b -> [Tree PE] -> Either (TT b) b
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT b
pp [TT (Either a b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Either a b)
qq] of
Left TT b
e -> TT b
e
Right b
p -> POpts -> Val b -> String -> [Tree PE] -> TT b
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (b -> Val b
forall a. a -> Val a
Val b
p) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Left") [TT (Either a b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Either a b)
qq, TT b -> Tree PE
forall a. TT a -> Tree PE
hh TT b
pp]
data LeftFail p q deriving Int -> LeftFail p q -> ShowS
[LeftFail p q] -> ShowS
LeftFail p q -> String
(Int -> LeftFail p q -> ShowS)
-> (LeftFail p q -> String)
-> ([LeftFail p q] -> ShowS)
-> Show (LeftFail p q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k). Int -> LeftFail p q -> ShowS
forall k (p :: k) k (q :: k). [LeftFail p q] -> ShowS
forall k (p :: k) k (q :: k). LeftFail p q -> String
showList :: [LeftFail p q] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k). [LeftFail p q] -> ShowS
show :: LeftFail p q -> String
$cshow :: forall k (p :: k) k (q :: k). LeftFail p q -> String
showsPrec :: Int -> LeftFail p q -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k). Int -> LeftFail p q -> ShowS
Show
instance ( PP p (b,x) ~ String
, PP q x ~ Either a b
, P p (b,x)
, P q x
)
=> P (LeftFail p q) x where
type PP (LeftFail p q) x = LeftT (PP q x)
eval :: proxy (LeftFail p q) -> POpts -> x -> m (TT (PP (LeftFail p q) x))
eval proxy (LeftFail p q)
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"LeftFail"
TT (Either a b)
qq <- Proxy q -> POpts -> x -> m (TT (PP q x))
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 q
forall k (t :: k). Proxy t
Proxy @q) POpts
opts x
x
case Inline
-> POpts
-> String
-> TT (Either a b)
-> [Tree PE]
-> Either (TT a) (Either a b)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (Either a b)
qq [] of
Left TT a
e -> TT a -> m (TT a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT a
e
Right Either a b
q ->
case Either a b
q of
Left a
a -> TT a -> m (TT a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT a -> m (TT a)) -> TT a -> m (TT a)
forall a b. (a -> b) -> a -> b
$ POpts -> Val a -> String -> [Tree PE] -> TT a
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (a -> Val a
forall a. a -> Val a
Val a
a) String
"Left" [TT (Either a b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Either a b)
qq]
Right b
b -> do
TT String
pp <- Proxy p -> POpts -> (b, x) -> m (TT (PP p (b, x)))
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 p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts (b
b,x
x)
TT a -> m (TT a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT a -> m (TT a)) -> TT a -> m (TT a)
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT String
-> [Tree PE]
-> Either (TT a) String
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT String
pp [TT (Either a b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Either a b)
qq] of
Left TT a
e -> TT a
e
Right String
p -> POpts -> Val a -> String -> [Tree PE] -> TT a
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (String -> Val a
forall a. String -> Val a
Fail String
p) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Right") [TT (Either a b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Either a b)
qq, TT String -> Tree PE
forall a. TT a -> Tree PE
hh TT String
pp]
data RightFail p q deriving Int -> RightFail p q -> ShowS
[RightFail p q] -> ShowS
RightFail p q -> String
(Int -> RightFail p q -> ShowS)
-> (RightFail p q -> String)
-> ([RightFail p q] -> ShowS)
-> Show (RightFail p q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k). Int -> RightFail p q -> ShowS
forall k (p :: k) k (q :: k). [RightFail p q] -> ShowS
forall k (p :: k) k (q :: k). RightFail p q -> String
showList :: [RightFail p q] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k). [RightFail p q] -> ShowS
show :: RightFail p q -> String
$cshow :: forall k (p :: k) k (q :: k). RightFail p q -> String
showsPrec :: Int -> RightFail p q -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k). Int -> RightFail p q -> ShowS
Show
instance ( PP p (a,x) ~ String
, PP q x ~ Either a b
, P p (a,x)
, P q x
)
=> P (RightFail p q) x where
type PP (RightFail p q) x = RightT (PP q x)
eval :: proxy (RightFail p q)
-> POpts -> x -> m (TT (PP (RightFail p q) x))
eval proxy (RightFail p q)
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"RightFail"
TT (Either a b)
qq <- Proxy q -> POpts -> x -> m (TT (PP q x))
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 q
forall k (t :: k). Proxy t
Proxy @q) POpts
opts x
x
case Inline
-> POpts
-> String
-> TT (Either a b)
-> [Tree PE]
-> Either (TT b) (Either a b)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (Either a b)
qq [] of
Left TT b
e -> TT b -> m (TT b)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT b
e
Right Either a b
q ->
case Either a b
q of
Right b
b -> TT b -> m (TT b)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT b -> m (TT b)) -> TT b -> m (TT b)
forall a b. (a -> b) -> a -> b
$ POpts -> Val b -> String -> [Tree PE] -> TT b
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (b -> Val b
forall a. a -> Val a
Val b
b) String
"Right" [TT (Either a b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Either a b)
qq]
Left a
a -> do
TT String
pp <- Proxy p -> POpts -> (a, x) -> m (TT (PP p (a, x)))
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 p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts (a
a,x
x)
TT b -> m (TT b)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT b -> m (TT b)) -> TT b -> m (TT b)
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT String
-> [Tree PE]
-> Either (TT b) String
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT String
pp [TT (Either a b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Either a b)
qq] of
Left TT b
e -> TT b
e
Right String
p -> POpts -> Val b -> String -> [Tree PE] -> TT b
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (String -> Val b
forall a. String -> Val a
Fail String
p) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Left") [TT (Either a b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Either a b)
qq, TT String -> Tree PE
forall a. TT a -> Tree PE
hh TT String
pp]