{-# 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.Tuple (
Dup
, First
, Second
, type (&&&)
, type (***)
, Both
, On
, Tuple
, Tuple'
, Pairs
, AndA
, type (&*)
, OrA
, type (|+)
, EachITuple
, ToITuple
, ReverseITuple
, ToITupleList
) where
import Predicate.Core
import Predicate.Misc
import Predicate.Util
import Data.Proxy (Proxy(Proxy))
import GHC.TypeNats (Nat, KnownNat)
import qualified GHC.TypeLits as GL
import Control.Lens
import Data.Kind (Type)
data Dup deriving Int -> Dup -> ShowS
[Dup] -> ShowS
Dup -> String
(Int -> Dup -> ShowS)
-> (Dup -> String) -> ([Dup] -> ShowS) -> Show Dup
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Dup] -> ShowS
$cshowList :: [Dup] -> ShowS
show :: Dup -> String
$cshow :: Dup -> String
showsPrec :: Int -> Dup -> ShowS
$cshowsPrec :: Int -> Dup -> ShowS
Show
type DupT = W '(Id, Id)
instance Show x => P Dup x where
type PP Dup x = PP DupT x
eval :: proxy Dup -> POpts -> x -> m (TT (PP Dup x))
eval proxy Dup
_ = Proxy DupT -> POpts -> x -> m (TT (PP DupT 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 DupT
forall k (t :: k). Proxy t
Proxy @DupT)
data Pairs deriving Int -> Pairs -> ShowS
[Pairs] -> ShowS
Pairs -> String
(Int -> Pairs -> ShowS)
-> (Pairs -> String) -> ([Pairs] -> ShowS) -> Show Pairs
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Pairs] -> ShowS
$cshowList :: [Pairs] -> ShowS
show :: Pairs -> String
$cshow :: Pairs -> String
showsPrec :: Int -> Pairs -> ShowS
$cshowsPrec :: Int -> Pairs -> ShowS
Show
instance ([a] ~ x, Show a) => P Pairs x where
type PP Pairs x = [(ExtractAFromTA x,ExtractAFromTA x)]
eval :: proxy Pairs -> POpts -> x -> m (TT (PP Pairs x))
eval proxy Pairs
_ POpts
opts x
as =
let zs :: [(a, a)]
zs = case x
as of
[] -> []
_:bs -> [a] -> [a] -> [(a, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip x
[a]
as [a]
bs
in TT [(a, a)] -> m (TT [(a, a)])
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT [(a, a)] -> m (TT [(a, a)])) -> TT [(a, a)] -> m (TT [(a, a)])
forall a b. (a -> b) -> a -> b
$ POpts -> Val [(a, a)] -> String -> [Tree PE] -> TT [(a, a)]
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts ([(a, a)] -> Val [(a, a)]
forall a. a -> Val a
Val [(a, a)]
zs) (POpts -> String -> [(a, a)] -> x -> String
forall a1 a2.
(Show a1, Show a2) =>
POpts -> String -> a1 -> a2 -> String
show3 POpts
opts String
"Pairs" [(a, a)]
zs x
as) []
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 3 &&&
type WAmpT p q = W '(p, q)
instance P (WAmpT p q) x => P (p &&& q) x where
type PP (p &&& q) x = PP (WAmpT p q) x
eval :: proxy (p &&& q) -> POpts -> x -> m (TT (PP (p &&& q) x))
eval proxy (p &&& q)
_ = Proxy (WAmpT p q) -> POpts -> x -> m (TT (PP (WAmpT p 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 (WAmpT p q)
forall k (t :: k). Proxy t
Proxy @(WAmpT p q))
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 3 ***
instance ( Show (PP p a)
, Show (PP q b)
, P p a
, P q b
, Show a
, Show b
) => P (p *** q) (a,b) where
type PP (p *** q) (a,b) = (PP p a, PP q b)
eval :: proxy (p *** q) -> POpts -> (a, b) -> m (TT (PP (p *** q) (a, b)))
eval proxy (p *** q)
_ POpts
opts (a
a,b
b) = do
let msg0 :: String
msg0 = String
"(***)"
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
case Inline
-> POpts
-> String
-> TT (PP p a)
-> [Tree PE]
-> Either (TT (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 (PP p a, PP q b)
e -> TT (PP p a, PP q b) -> m (TT (PP p a, PP q b))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (PP p a, PP q b)
e
Right PP p a
a1 -> 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
b
TT (PP p a, PP q b) -> m (TT (PP p a, PP q b))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP p a, PP q b) -> m (TT (PP p a, PP q b)))
-> TT (PP p a, PP q b) -> m (TT (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 (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 [TT (PP p a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p a)
pp] of
Left TT (PP p a, PP q b)
e -> TT (PP p a, PP q b)
e
Right PP q b
b1 -> POpts
-> Val (PP p a, PP q b)
-> String
-> [Tree PE]
-> TT (PP p a, PP q b)
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts ((PP p a, PP q b) -> Val (PP p a, PP q b)
forall a. a -> Val a
Val (PP p a
a1,PP q b
b1)) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> (PP p a, PP q b) -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts (PP p a
a1,PP q b
b1) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> String -> (a, b) -> String
forall a. Show a => POpts -> String -> a -> String
showVerbose POpts
opts String
" | " (a
a,b
b)) [TT (PP p a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p a)
pp, TT (PP q b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP q b)
qq]
data First p deriving Int -> First p -> ShowS
[First p] -> ShowS
First p -> String
(Int -> First p -> ShowS)
-> (First p -> String) -> ([First p] -> ShowS) -> Show (First p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k). Int -> First p -> ShowS
forall k (p :: k). [First p] -> ShowS
forall k (p :: k). First p -> String
showList :: [First p] -> ShowS
$cshowList :: forall k (p :: k). [First p] -> ShowS
show :: First p -> String
$cshow :: forall k (p :: k). First p -> String
showsPrec :: Int -> First p -> ShowS
$cshowsPrec :: forall k (p :: k). Int -> First p -> ShowS
Show
type FirstT p = p *** Id
instance P (FirstT p) x => P (First p) x where
type PP (First p) x = PP (FirstT p) x
eval :: proxy (First p) -> POpts -> x -> m (TT (PP (First p) x))
eval proxy (First p)
_ = Proxy (FirstT p) -> POpts -> x -> m (TT (PP (FirstT 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 (FirstT p)
forall k (t :: k). Proxy t
Proxy @(FirstT p))
data Second q deriving Int -> Second q -> ShowS
[Second q] -> ShowS
Second q -> String
(Int -> Second q -> ShowS)
-> (Second q -> String) -> ([Second q] -> ShowS) -> Show (Second q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (q :: k). Int -> Second q -> ShowS
forall k (q :: k). [Second q] -> ShowS
forall k (q :: k). Second q -> String
showList :: [Second q] -> ShowS
$cshowList :: forall k (q :: k). [Second q] -> ShowS
show :: Second q -> String
$cshow :: forall k (q :: k). Second q -> String
showsPrec :: Int -> Second q -> ShowS
$cshowsPrec :: forall k (q :: k). Int -> Second q -> ShowS
Show
type SecondT q = Id *** q
instance P (SecondT q) x => P (Second q) x where
type PP (Second q) x = PP (SecondT q) x
eval :: proxy (Second q) -> POpts -> x -> m (TT (PP (Second q) x))
eval proxy (Second q)
_ = Proxy (SecondT q) -> POpts -> x -> m (TT (PP (SecondT 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 (SecondT q)
forall k (t :: k). Proxy t
Proxy @(SecondT q))
data AndA p q r deriving Int -> AndA p q r -> ShowS
[AndA p q r] -> ShowS
AndA p q r -> String
(Int -> AndA p q r -> ShowS)
-> (AndA p q r -> String)
-> ([AndA p q r] -> ShowS)
-> Show (AndA 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 -> AndA p q r -> ShowS
forall k (p :: k) k (q :: k) k (r :: k). [AndA p q r] -> ShowS
forall k (p :: k) k (q :: k) k (r :: k). AndA p q r -> String
showList :: [AndA p q r] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k) k (r :: k). [AndA p q r] -> ShowS
show :: AndA p q r -> String
$cshow :: forall k (p :: k) k (q :: k) k (r :: k). AndA p q r -> String
showsPrec :: Int -> AndA p q r -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k) k (r :: k). Int -> AndA p q r -> ShowS
Show
instance ( PP r x ~ (a,b)
, PP p a ~ Bool
, PP q b ~ Bool
, P p a
, P q b
, P r x
) => P (AndA p q r) x where
type PP (AndA p q r) x = Bool
eval :: proxy (AndA p q r) -> POpts -> x -> m (TT (PP (AndA p q r) x))
eval proxy (AndA p q r)
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"(&*)"
TT (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 (a, b)
-> [Tree PE]
-> Either (TT Bool) (a, b)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (a, b)
rr [] of
Left TT Bool
e -> TT Bool -> m (TT Bool)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT Bool
e
Right (a
r1,b
r2) -> do
TT Bool
pp <- Proxy p -> POpts -> a -> m (TT (PP p a))
forall k (m :: Type -> Type) (p :: k) a (proxy :: k -> Type).
(MonadEval m, P p a, PP p a ~ Bool) =>
proxy p -> POpts -> a -> m (TT (PP p a))
evalBool (Proxy p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts a
r1
case Inline
-> POpts -> String -> TT Bool -> [Tree PE] -> Either (TT Bool) Bool
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT Bool
pp [TT (a, b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (a, b)
rr] of
Left TT Bool
e -> TT Bool -> m (TT Bool)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT Bool
e
Right Bool
p -> do
TT Bool
qq <- Proxy q -> POpts -> b -> m (TT (PP q b))
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 q
forall k (t :: k). Proxy t
Proxy @q) POpts
opts b
r2
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
$ case Inline
-> POpts -> String -> TT Bool -> [Tree PE] -> Either (TT Bool) Bool
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT Bool
qq [TT (a, b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (a, b)
rr, TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp] of
Left TT Bool
e -> TT Bool
e
Right Bool
q ->
let zz :: String
zz = case (Bool
p,Bool
q) of
(Bool
True, Bool
True) -> String
""
(Bool
False, Bool
True) -> TT Bool -> String
forall a. TT a -> String
topMessage TT Bool
pp
(Bool
True, Bool
False) -> TT Bool -> String
forall a. TT a -> String
topMessage TT Bool
qq
(Bool
False, Bool
False) -> TT Bool -> String
forall a. TT a -> String
topMessage TT Bool
pp String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> TT Bool -> String
forall a. TT a -> String
topMessage TT Bool
qq
in POpts -> Bool -> String -> [Tree PE] -> TT Bool
mkNodeB POpts
opts (Bool
pBool -> Bool -> Bool
&&Bool
q) (POpts -> Bool -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts Bool
p String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Bool -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts Bool
q String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String -> ShowS
nullIf String
" | " String
zz) [TT (a, b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (a, b)
rr, TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp, TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
qq]
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
type AndAT p q = AndA p q Id
infixr 3 &*
instance P (AndAT p q) x => P (p &* q) x where
type PP (p &* q) x = PP (AndAT p q) x
eval :: proxy (p &* q) -> POpts -> x -> m (TT (PP (p &* q) x))
eval proxy (p &* q)
_ = Proxy (AndAT p q) -> POpts -> x -> m (TT (PP (AndAT p q) x))
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 (AndAT p q)
forall k (t :: k). Proxy t
Proxy @(AndAT p q))
data OrA p q r deriving Int -> OrA p q r -> ShowS
[OrA p q r] -> ShowS
OrA p q r -> String
(Int -> OrA p q r -> ShowS)
-> (OrA p q r -> String)
-> ([OrA p q r] -> ShowS)
-> Show (OrA 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 -> OrA p q r -> ShowS
forall k (p :: k) k (q :: k) k (r :: k). [OrA p q r] -> ShowS
forall k (p :: k) k (q :: k) k (r :: k). OrA p q r -> String
showList :: [OrA p q r] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k) k (r :: k). [OrA p q r] -> ShowS
show :: OrA p q r -> String
$cshow :: forall k (p :: k) k (q :: k) k (r :: k). OrA p q r -> String
showsPrec :: Int -> OrA p q r -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k) k (r :: k). Int -> OrA p q r -> ShowS
Show
instance ( PP r x ~ (a,b)
, PP p a ~ Bool
, PP q b ~ Bool
, P p a
, P q b
, P r x
) => P (OrA p q r) x where
type PP (OrA p q r) x = Bool
eval :: proxy (OrA p q r) -> POpts -> x -> m (TT (PP (OrA p q r) x))
eval proxy (OrA p q r)
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"(|+)"
TT (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 (a, b)
-> [Tree PE]
-> Either (TT Bool) (a, b)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (a, b)
rr [] of
Left TT Bool
e -> TT Bool -> m (TT Bool)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT Bool
e
Right (a
r1,b
r2) -> do
TT Bool
pp <- Proxy p -> POpts -> a -> m (TT (PP p a))
forall k (m :: Type -> Type) (p :: k) a (proxy :: k -> Type).
(MonadEval m, P p a, PP p a ~ Bool) =>
proxy p -> POpts -> a -> m (TT (PP p a))
evalBool (Proxy p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts a
r1
case Inline
-> POpts -> String -> TT Bool -> [Tree PE] -> Either (TT Bool) Bool
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT Bool
pp [TT (a, b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (a, b)
rr] of
Left TT Bool
e -> TT Bool -> m (TT Bool)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT Bool
e
Right Bool
p -> do
TT Bool
qq <- Proxy q -> POpts -> b -> m (TT (PP q b))
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 q
forall k (t :: k). Proxy t
Proxy @q) POpts
opts b
r2
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
$ case Inline
-> POpts -> String -> TT Bool -> [Tree PE] -> Either (TT Bool) Bool
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT Bool
qq [TT (a, b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (a, b)
rr, TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp] of
Left TT Bool
e -> TT Bool
e
Right Bool
q ->
let zz :: String
zz = case (Bool
p,Bool
q) of
(Bool
False,Bool
False) -> TT Bool -> String
forall a. TT a -> String
topMessage TT Bool
pp String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> TT Bool -> String
forall a. TT a -> String
topMessage TT Bool
qq
(Bool, Bool)
_ -> String
""
in POpts -> Bool -> String -> [Tree PE] -> TT Bool
mkNodeB POpts
opts (Bool
pBool -> Bool -> Bool
||Bool
q) (POpts -> Bool -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts Bool
p String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Bool -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts Bool
q String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String -> ShowS
nullIf String
" | " String
zz) [TT (a, b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (a, b)
rr, TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
pp, TT Bool -> Tree PE
forall a. TT a -> Tree PE
hh TT Bool
qq]
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
type OrAT p q = OrA p q Id
infixr 3 |+
instance P (OrAT p q) x => P (p |+ q) x where
type PP (p |+ q) x = PP (OrAT p q) x
eval :: proxy (p |+ q) -> POpts -> x -> m (TT (PP (p |+ q) x))
eval proxy (p |+ q)
_ = Proxy (OrAT p q) -> POpts -> x -> m (TT (PP (OrAT p q) x))
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 (OrAT p q)
forall k (t :: k). Proxy t
Proxy @(OrAT p q))
data Both p deriving Int -> Both p -> ShowS
[Both p] -> ShowS
Both p -> String
(Int -> Both p -> ShowS)
-> (Both p -> String) -> ([Both p] -> ShowS) -> Show (Both p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k). Int -> Both p -> ShowS
forall k (p :: k). [Both p] -> ShowS
forall k (p :: k). Both p -> String
showList :: [Both p] -> ShowS
$cshowList :: forall k (p :: k). [Both p] -> ShowS
show :: Both p -> String
$cshow :: forall k (p :: k). Both p -> String
showsPrec :: Int -> Both p -> ShowS
$cshowsPrec :: forall k (p :: k). Int -> Both p -> ShowS
Show
instance ( P p a
, P p a'
) => P (Both p) (a,a') where
type PP (Both p) (a,a') = (PP p a, PP p a')
eval :: proxy (Both p) -> POpts -> (a, a') -> m (TT (PP (Both p) (a, a')))
eval proxy (Both p)
_ POpts
opts (a
a,a'
a') = do
let msg0 :: String
msg0 = String
"Both"
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
case Inline
-> POpts
-> String
-> TT (PP p a)
-> [Tree PE]
-> Either (TT (PP p a, PP p 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 TT (PP p a)
pp [] of
Left TT (PP p a, PP p a')
e -> TT (PP p a, PP p a') -> m (TT (PP p a, PP p a'))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (PP p a, PP p a')
e
Right PP p a
b -> 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 (PP p a, PP p a') -> m (TT (PP p a, PP p a'))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP p a, PP p a') -> m (TT (PP p a, PP p a')))
-> TT (PP p a, PP p a') -> m (TT (PP p a, PP p a'))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP p a')
-> [Tree PE]
-> Either (TT (PP p a, PP p 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 TT (PP p a')
pp' [TT (PP p a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p a)
pp] of
Left TT (PP p a, PP p a')
e -> TT (PP p a, PP p a')
e
Right PP p a'
b' ->
POpts
-> Val (PP p a, PP p a')
-> String
-> [Tree PE]
-> TT (PP p a, PP p a')
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts ((PP p a, PP p a') -> Val (PP p a, PP p a')
forall a. a -> Val a
Val (PP p a
b,PP p a'
b')) String
msg0 [TT (PP p a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p a)
pp, TT (PP p a') -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p a')
pp']
data On (p :: Type -> Type -> k2) q deriving Int -> On p q -> ShowS
[On p q] -> ShowS
On p q -> String
(Int -> On p q -> ShowS)
-> (On p q -> String) -> ([On p q] -> ShowS) -> Show (On p q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k2 (p :: Type -> Type -> k2) k (q :: k).
Int -> On p q -> ShowS
forall k2 (p :: Type -> Type -> k2) k (q :: k). [On p q] -> ShowS
forall k2 (p :: Type -> Type -> k2) k (q :: k). On p q -> String
showList :: [On p q] -> ShowS
$cshowList :: forall k2 (p :: Type -> Type -> k2) k (q :: k). [On p q] -> ShowS
show :: On p q -> String
$cshow :: forall k2 (p :: Type -> Type -> k2) k (q :: k). On p q -> String
showsPrec :: Int -> On p q -> ShowS
$cshowsPrec :: forall k2 (p :: Type -> Type -> k2) k (q :: k).
Int -> On p q -> ShowS
Show
instance ( P q a
, P q a'
, P (p Fst Snd) (PP q a, PP q a')
) => P (On p q) (a,a') where
type PP (On p q) (a,a') = PP (p Fst Snd) (PP q a, PP q a')
eval :: proxy (On p q) -> POpts -> (a, a') -> m (TT (PP (On p q) (a, a')))
eval proxy (On p q)
_ POpts
opts (a
a,a'
a') = do
let msg0 :: String
msg0 = String
"On"
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
a
case Inline
-> POpts
-> String
-> TT (PP q a)
-> [Tree PE]
-> Either (TT (PP (p Fst Snd) (PP q 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 TT (PP q a)
qq [] of
Left TT (PP (p Fst Snd) (PP q a, PP q a'))
e -> TT (PP (p Fst Snd) (PP q a, PP q a'))
-> m (TT (PP (p Fst Snd) (PP q a, PP q a')))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (PP (p Fst Snd) (PP q a, PP q a'))
e
Right PP q a
b -> 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'
a'
case Inline
-> POpts
-> String
-> TT (PP q a')
-> [Tree PE]
-> Either (TT (PP (p Fst Snd) (PP q 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 TT (PP q a')
qq' [TT (PP q a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP q a)
qq] of
Left TT (PP (p Fst Snd) (PP q a, PP q a'))
e -> TT (PP (p Fst Snd) (PP q a, PP q a'))
-> m (TT (PP (p Fst Snd) (PP q a, PP q a')))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (PP (p Fst Snd) (PP q a, PP q a'))
e
Right PP q a'
b' -> do
TT (PP (p Fst Snd) (PP q a, PP q a'))
pp <- Proxy (p Fst Snd)
-> POpts
-> (PP q a, PP q a')
-> m (TT (PP (p Fst Snd) (PP q a, 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 (p Fst Snd)
forall k (t :: k). Proxy t
Proxy @(p Fst Snd)) POpts
opts (PP q a
b,PP q a'
b')
TT (PP (p Fst Snd) (PP q a, PP q a'))
-> m (TT (PP (p Fst Snd) (PP q a, PP q a')))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP (p Fst Snd) (PP q a, PP q a'))
-> m (TT (PP (p Fst Snd) (PP q a, PP q a'))))
-> TT (PP (p Fst Snd) (PP q a, PP q a'))
-> m (TT (PP (p Fst Snd) (PP q a, PP q a')))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP (p Fst Snd) (PP q a, PP q a'))
-> [Tree PE]
-> Either
(TT (PP (p Fst Snd) (PP q a, PP q a')))
(PP (p Fst Snd) (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 TT (PP (p Fst Snd) (PP q a, PP q a'))
pp [TT (PP q a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP q a)
qq, TT (PP q a') -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP q a')
qq'] of
Left TT (PP (p Fst Snd) (PP q a, PP q a'))
e -> TT (PP (p Fst Snd) (PP q a, PP q a'))
e
Right PP (p Fst Snd) (PP q a, PP q a')
p -> POpts
-> Val (PP (p Fst Snd) (PP q a, PP q a'))
-> String
-> [Tree PE]
-> TT (PP (p Fst Snd) (PP q a, PP q a'))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (PP (p Fst Snd) (PP q a, PP q a')
-> Val (PP (p Fst Snd) (PP q a, PP q a'))
forall a. a -> Val a
Val PP (p Fst Snd) (PP q a, PP q a')
p) String
msg0 [TT (PP q a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP q a)
qq, TT (PP q a') -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP q a')
qq', TT (PP (p Fst Snd) (PP q a, PP q a')) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP (p Fst Snd) (PP q a, PP q a'))
pp]
data Tuple (n :: Nat) deriving Int -> Tuple n -> ShowS
[Tuple n] -> ShowS
Tuple n -> String
(Int -> Tuple n -> ShowS)
-> (Tuple n -> String) -> ([Tuple n] -> ShowS) -> Show (Tuple n)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: Nat). Int -> Tuple n -> ShowS
forall (n :: Nat). [Tuple n] -> ShowS
forall (n :: Nat). Tuple n -> String
showList :: [Tuple n] -> ShowS
$cshowList :: forall (n :: Nat). [Tuple n] -> ShowS
show :: Tuple n -> String
$cshow :: forall (n :: Nat). Tuple n -> String
showsPrec :: Int -> Tuple n -> ShowS
$cshowsPrec :: forall (n :: Nat). Int -> Tuple n -> ShowS
Show
instance ( KnownNat n
, FailWhenT (n GL.<=? 1)
('GL.Text "Tuple:n cannot be less than two but found n="
'GL.:<>: 'GL.ShowType n)
, TupleC n a
, x ~ [a]
, Show a
) => P (Tuple n) x where
type PP (Tuple n) x = TupleT n (ExtractAFromList x)
eval :: proxy (Tuple n) -> POpts -> x -> m (TT (PP (Tuple n) x))
eval proxy (Tuple n)
_ POpts
opts x
as =
let msg0 :: String
msg0 = String
"Tuple(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
n :: Int
n = (KnownNat n, Num Int) => Int
forall (n :: Nat) a. (KnownNat n, Num a) => a
nat @n @Int
in TT (TupleT n a) -> m (TT (TupleT n a))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (TupleT n a) -> m (TT (TupleT n a)))
-> TT (TupleT n a) -> m (TT (TupleT n a))
forall a b. (a -> b) -> a -> b
$ case [a] -> Either [a] (TupleT n a)
forall (n :: Nat) a. TupleC n a => [a] -> Either [a] (TupleT n a)
getTupleC @n x
[a]
as of
Left [a]
es -> POpts -> Val (TupleT n a) -> String -> [Tree PE] -> TT (TupleT n a)
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (String -> Val (TupleT n a)
forall a. String -> Val a
Fail (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" not enough elements(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show ([a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length x
[a]
as) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")")) (POpts -> String -> [a] -> String
forall a. Show a => POpts -> String -> a -> String
showVerbose POpts
opts String
" | " [a]
es) []
Right TupleT n a
r -> POpts -> Val (TupleT n a) -> String -> [Tree PE] -> TT (TupleT n a)
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (TupleT n a -> Val (TupleT n a)
forall a. a -> Val a
Val TupleT n a
r) String
msg0 []
data Tuple' (n :: Nat) deriving Int -> Tuple' n -> ShowS
[Tuple' n] -> ShowS
Tuple' n -> String
(Int -> Tuple' n -> ShowS)
-> (Tuple' n -> String) -> ([Tuple' n] -> ShowS) -> Show (Tuple' n)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: Nat). Int -> Tuple' n -> ShowS
forall (n :: Nat). [Tuple' n] -> ShowS
forall (n :: Nat). Tuple' n -> String
showList :: [Tuple' n] -> ShowS
$cshowList :: forall (n :: Nat). [Tuple' n] -> ShowS
show :: Tuple' n -> String
$cshow :: forall (n :: Nat). Tuple' n -> String
showsPrec :: Int -> Tuple' n -> ShowS
$cshowsPrec :: forall (n :: Nat). Int -> Tuple' n -> ShowS
Show
instance ( KnownNat n
, FailWhenT (n GL.<=? 1)
('GL.Text "Tuple':n cannot be less than two but found n="
'GL.:<>: 'GL.ShowType n)
, TupleC n a
, x ~ [a]
) => P (Tuple' n) x where
type PP (Tuple' n) x = Either x (TupleT n (ExtractAFromList x))
eval :: proxy (Tuple' n) -> POpts -> x -> m (TT (PP (Tuple' n) x))
eval proxy (Tuple' n)
_ POpts
opts x
as =
let msg0 :: String
msg0 = String
"Tuple'(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
n :: Int
n = (KnownNat n, Num Int) => Int
forall (n :: Nat) a. (KnownNat n, Num a) => a
nat @n @Int
lr :: Either [a] (TupleT n a)
lr = [a] -> Either [a] (TupleT n a)
forall (n :: Nat) a. TupleC n a => [a] -> Either [a] (TupleT n a)
getTupleC @n x
[a]
as
in TT (Either [a] (TupleT n a)) -> m (TT (Either [a] (TupleT n a)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (Either [a] (TupleT n a)) -> m (TT (Either [a] (TupleT n a))))
-> TT (Either [a] (TupleT n a)) -> m (TT (Either [a] (TupleT n a)))
forall a b. (a -> b) -> a -> b
$ case Either [a] (TupleT n a)
lr of
Left [a]
e -> POpts
-> Val (Either [a] (TupleT n a))
-> String
-> [Tree PE]
-> TT (Either [a] (TupleT n a))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (Either [a] (TupleT n a) -> Val (Either [a] (TupleT n a))
forall a. a -> Val a
Val ([a] -> Either [a] (TupleT n a)
forall a b. a -> Either a b
Left [a]
e)) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" not enough elements(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show ([a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length x
[a]
as) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")") []
Right TupleT n a
ret -> POpts
-> Val (Either [a] (TupleT n a))
-> String
-> [Tree PE]
-> TT (Either [a] (TupleT n a))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (Either [a] (TupleT n a) -> Val (Either [a] (TupleT n a))
forall a. a -> Val a
Val (TupleT n a -> Either [a] (TupleT n a)
forall a b. b -> Either a b
Right TupleT n a
ret)) String
msg0 []
data EachITuple p deriving Int -> EachITuple p -> ShowS
[EachITuple p] -> ShowS
EachITuple p -> String
(Int -> EachITuple p -> ShowS)
-> (EachITuple p -> String)
-> ([EachITuple p] -> ShowS)
-> Show (EachITuple p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k). Int -> EachITuple p -> ShowS
forall k (p :: k). [EachITuple p] -> ShowS
forall k (p :: k). EachITuple p -> String
showList :: [EachITuple p] -> ShowS
$cshowList :: forall k (p :: k). [EachITuple p] -> ShowS
show :: EachITuple p -> String
$cshow :: forall k (p :: k). EachITuple p -> String
showsPrec :: Int -> EachITuple p -> ShowS
$cshowsPrec :: forall k (p :: k). Int -> EachITuple p -> ShowS
Show
instance ( P p b
, P (EachITuple p) bs
) => P (EachITuple p) (b,bs) where
type PP (EachITuple p) (b,bs) = (PP p b, PP (EachITuple p) bs)
eval :: proxy (EachITuple p)
-> POpts -> (b, bs) -> m (TT (PP (EachITuple p) (b, bs)))
eval proxy (EachITuple p)
_ POpts
opts (b
b,bs
bs) = do
let msg0 :: String
msg0 = String
"EachITuple"
TT (PP p b)
pp <- Proxy p -> POpts -> b -> m (TT (PP p 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 p
forall k (t :: k). Proxy t
Proxy @p) POpts
opts b
b
case Inline
-> POpts
-> String
-> TT (PP p b)
-> [Tree PE]
-> Either (TT (PP p b, PP (EachITuple p) bs)) (PP p b)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (PP p b)
pp [] of
Left TT (PP p b, PP (EachITuple p) bs)
e -> TT (PP p b, PP (EachITuple p) bs)
-> m (TT (PP p b, PP (EachITuple p) bs))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (PP p b, PP (EachITuple p) bs)
e
Right PP p b
p -> do
TT (PP (EachITuple p) bs)
qq <- Proxy (EachITuple p)
-> POpts -> bs -> m (TT (PP (EachITuple p) bs))
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 (EachITuple p)
forall k (t :: k). Proxy t
Proxy @(EachITuple p)) POpts
opts bs
bs
TT (PP p b, PP (EachITuple p) bs)
-> m (TT (PP p b, PP (EachITuple p) bs))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP p b, PP (EachITuple p) bs)
-> m (TT (PP p b, PP (EachITuple p) bs)))
-> TT (PP p b, PP (EachITuple p) bs)
-> m (TT (PP p b, PP (EachITuple p) bs))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP (EachITuple p) bs)
-> [Tree PE]
-> Either
(TT (PP p b, PP (EachITuple p) bs)) (PP (EachITuple p) bs)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (PP (EachITuple p) bs)
qq [] of
Left TT (PP p b, PP (EachITuple p) bs)
e -> TT (PP p b, PP (EachITuple p) bs)
e
Right PP (EachITuple p) bs
q ->
TT (PP (EachITuple p) bs)
qq TT (PP (EachITuple p) bs)
-> (TT (PP (EachITuple p) bs) -> TT (PP p b, PP (EachITuple p) bs))
-> TT (PP p b, PP (EachITuple p) bs)
forall a b. a -> (a -> b) -> b
& (Val (PP (EachITuple p) bs)
-> Identity (Val (PP p b, PP (EachITuple p) bs)))
-> TT (PP (EachITuple p) bs)
-> Identity (TT (PP p b, PP (EachITuple p) bs))
forall a b. Lens (TT a) (TT b) (Val a) (Val b)
ttVal ((Val (PP (EachITuple p) bs)
-> Identity (Val (PP p b, PP (EachITuple p) bs)))
-> TT (PP (EachITuple p) bs)
-> Identity (TT (PP p b, PP (EachITuple p) bs)))
-> Val (PP p b, PP (EachITuple p) bs)
-> TT (PP (EachITuple p) bs)
-> TT (PP p b, PP (EachITuple p) bs)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ (PP p b, PP (EachITuple p) bs)
-> Val (PP p b, PP (EachITuple p) bs)
forall a. a -> Val a
Val (PP p b
p,PP (EachITuple p) bs
q)
TT (PP p b, PP (EachITuple p) bs)
-> (TT (PP p b, PP (EachITuple p) bs)
-> TT (PP p b, PP (EachITuple p) bs))
-> TT (PP p b, PP (EachITuple p) bs)
forall a b. a -> (a -> b) -> b
& ([Tree PE] -> Identity [Tree PE])
-> TT (PP p b, PP (EachITuple p) bs)
-> Identity (TT (PP p b, PP (EachITuple p) bs))
forall a. Lens' (TT a) [Tree PE]
ttForest (([Tree PE] -> Identity [Tree PE])
-> TT (PP p b, PP (EachITuple p) bs)
-> Identity (TT (PP p b, PP (EachITuple p) bs)))
-> ([Tree PE] -> [Tree PE])
-> TT (PP p b, PP (EachITuple p) bs)
-> TT (PP p b, PP (EachITuple p) bs)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (TT (PP p b) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p b)
ppTree PE -> [Tree PE] -> [Tree PE]
forall a. a -> [a] -> [a]
:)
instance P (EachITuple p) () where
type PP (EachITuple p) () = ()
eval :: proxy (EachITuple p)
-> POpts -> () -> m (TT (PP (EachITuple p) ()))
eval proxy (EachITuple p)
_ POpts
opts () = do
let msg0 :: String
msg0 = String
"EachITuple"
TT () -> m (TT ())
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT () -> m (TT ())) -> TT () -> m (TT ())
forall a b. (a -> b) -> a -> b
$ POpts -> Val () -> String -> [Tree PE] -> TT ()
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (() -> Val ()
forall a. a -> Val a
Val ()) String
msg0 []
data ToITuple deriving Int -> ToITuple -> ShowS
[ToITuple] -> ShowS
ToITuple -> String
(Int -> ToITuple -> ShowS)
-> (ToITuple -> String) -> ([ToITuple] -> ShowS) -> Show ToITuple
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ToITuple] -> ShowS
$cshowList :: [ToITuple] -> ShowS
show :: ToITuple -> String
$cshow :: ToITuple -> String
showsPrec :: Int -> ToITuple -> ShowS
$cshowsPrec :: Int -> ToITuple -> ShowS
Show
instance ToITupleC x => P ToITuple x where
type PP ToITuple x = ToITupleP x
eval :: proxy ToITuple -> POpts -> x -> m (TT (PP ToITuple x))
eval proxy ToITuple
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"ToITuple"
TT (ToITupleP x) -> m (TT (ToITupleP x))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (ToITupleP x) -> m (TT (ToITupleP x)))
-> TT (ToITupleP x) -> m (TT (ToITupleP x))
forall a b. (a -> b) -> a -> b
$ POpts
-> Val (ToITupleP x) -> String -> [Tree PE] -> TT (ToITupleP x)
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (ToITupleP x -> Val (ToITupleP x)
forall a. a -> Val a
Val (x -> ToITupleP x
forall x. ToITupleC x => x -> ToITupleP x
toITupleC x
x)) String
msg0 []
data ReverseITuple deriving Int -> ReverseITuple -> ShowS
[ReverseITuple] -> ShowS
ReverseITuple -> String
(Int -> ReverseITuple -> ShowS)
-> (ReverseITuple -> String)
-> ([ReverseITuple] -> ShowS)
-> Show ReverseITuple
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ReverseITuple] -> ShowS
$cshowList :: [ReverseITuple] -> ShowS
show :: ReverseITuple -> String
$cshow :: ReverseITuple -> String
showsPrec :: Int -> ReverseITuple -> ShowS
$cshowsPrec :: Int -> ReverseITuple -> ShowS
Show
instance P ReverseITuple () where
type PP ReverseITuple () = ()
eval :: proxy ReverseITuple -> POpts -> () -> m (TT (PP ReverseITuple ()))
eval proxy ReverseITuple
_ POpts
opts () = do
let msg0 :: String
msg0 = String
"ReverseITuple"
TT () -> m (TT ())
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT () -> m (TT ())) -> TT () -> m (TT ())
forall a b. (a -> b) -> a -> b
$ POpts -> Val () -> String -> [Tree PE] -> TT ()
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (() -> Val ()
forall a. a -> Val a
Val ()) String
msg0 []
instance ReverseITupleC x xs () => P ReverseITuple (x,xs) where
type PP ReverseITuple (x,xs) = ReverseITupleT x xs ()
eval :: proxy ReverseITuple
-> POpts -> (x, xs) -> m (TT (PP ReverseITuple (x, xs)))
eval proxy ReverseITuple
_ POpts
opts (x
x,xs
xs) = do
let msg0 :: String
msg0 = String
"ReverseITuple"
TT (ReverseITupleT x xs ()) -> m (TT (ReverseITupleT x xs ()))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (ReverseITupleT x xs ()) -> m (TT (ReverseITupleT x xs ())))
-> TT (ReverseITupleT x xs ()) -> m (TT (ReverseITupleT x xs ()))
forall a b. (a -> b) -> a -> b
$ POpts
-> Val (ReverseITupleT x xs ())
-> String
-> [Tree PE]
-> TT (ReverseITupleT x xs ())
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (ReverseITupleT x xs () -> Val (ReverseITupleT x xs ())
forall a. a -> Val a
Val (x -> xs -> () -> ReverseITupleT x xs ()
forall x xs ys.
ReverseITupleC x xs ys =>
x -> xs -> ys -> ReverseITupleT x xs ys
reverseITupleC x
x xs
xs ())) String
msg0 []
data ToITupleList (n :: Nat) deriving Int -> ToITupleList n -> ShowS
[ToITupleList n] -> ShowS
ToITupleList n -> String
(Int -> ToITupleList n -> ShowS)
-> (ToITupleList n -> String)
-> ([ToITupleList n] -> ShowS)
-> Show (ToITupleList n)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: Nat). Int -> ToITupleList n -> ShowS
forall (n :: Nat). [ToITupleList n] -> ShowS
forall (n :: Nat). ToITupleList n -> String
showList :: [ToITupleList n] -> ShowS
$cshowList :: forall (n :: Nat). [ToITupleList n] -> ShowS
show :: ToITupleList n -> String
$cshow :: forall (n :: Nat). ToITupleList n -> String
showsPrec :: Int -> ToITupleList n -> ShowS
$cshowsPrec :: forall (n :: Nat). Int -> ToITupleList n -> ShowS
Show
instance ( KnownNat n
, FailWhenT (n GL.<=? 0)
('GL.Text "ToITupleList:n cannot be 0")
, ToITupleListC n a
, xs ~ [a]
) => P (ToITupleList n) xs where
type PP (ToITupleList n) xs = ToITupleListP n (ExtractAFromTA xs)
eval :: proxy (ToITupleList n)
-> POpts -> xs -> m (TT (PP (ToITupleList n) xs))
eval proxy (ToITupleList n)
_ POpts
opts xs
xs =
let msg0 :: String
msg0 = String
"ToITupleList(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
n :: Int
n = (KnownNat n, Num Int) => Int
forall (n :: Nat) a. (KnownNat n, Num a) => a
nat @n @Int
in TT (ToITupleListP n a) -> m (TT (ToITupleListP n a))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (ToITupleListP n a) -> m (TT (ToITupleListP n a)))
-> TT (ToITupleListP n a) -> m (TT (ToITupleListP n a))
forall a b. (a -> b) -> a -> b
$ case [a] -> Either String (ToITupleListP n a)
forall (n :: Nat) a.
ToITupleListC n a =>
[a] -> Either String (ToITupleListP n a)
toITupleListC @n @a xs
[a]
xs of
Left String
e -> POpts
-> Val (ToITupleListP n a)
-> String
-> [Tree PE]
-> TT (ToITupleListP n a)
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (String -> Val (ToITupleListP n a)
forall a. String -> Val a
Fail String
e) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" instead found " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show ([a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length xs
[a]
xs)) []
Right ToITupleListP n a
d -> POpts
-> Val (ToITupleListP n a)
-> String
-> [Tree PE]
-> TT (ToITupleListP n a)
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (ToITupleListP n a -> Val (ToITupleListP n a)
forall a. a -> Val a
Val ToITupleListP n a
d) String
msg0 []