{-# 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.Proxy (
ProxyT
, Proxy1T
, Proxy2T
, Proxify
, Pop0
, Pop1
, Pop2
, Pop1'
, Pop2'
, PApp
, PApp2
, Proxy2TT
, Pop0T
, Pop1T
, Pop1T'
, Pop2T
, Pop2T'
, PAppT
, PApp2T
, ProxifyT
) where
import Predicate.Core
import Predicate.Misc
import Predicate.Util
import qualified GHC.TypeLits as GL
import Data.Kind (Type)
import Data.Typeable (Proxy(..))
import Control.Lens
data ProxyT deriving Int -> ProxyT -> ShowS
[ProxyT] -> ShowS
ProxyT -> String
(Int -> ProxyT -> ShowS)
-> (ProxyT -> String) -> ([ProxyT] -> ShowS) -> Show ProxyT
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProxyT] -> ShowS
$cshowList :: [ProxyT] -> ShowS
show :: ProxyT -> String
$cshow :: ProxyT -> String
showsPrec :: Int -> ProxyT -> ShowS
$cshowsPrec :: Int -> ProxyT -> ShowS
Show
instance Show x => P ProxyT x where
type PP ProxyT x = Proxy x
eval :: proxy ProxyT -> POpts -> x -> m (TT (PP ProxyT x))
eval proxy ProxyT
_ POpts
opts x
x =
let b :: Proxy x
b = Proxy x
forall k (t :: k). Proxy t
Proxy @x
in TT (Proxy x) -> m (TT (Proxy x))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (Proxy x) -> m (TT (Proxy x)))
-> TT (Proxy x) -> m (TT (Proxy x))
forall a b. (a -> b) -> a -> b
$ POpts -> Val (Proxy x) -> String -> [Tree PE] -> TT (Proxy x)
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (Proxy x -> Val (Proxy x)
forall a. a -> Val a
Val Proxy x
b) (String
"ProxyT" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> String -> x -> String
forall a. Show a => POpts -> String -> a -> String
showVerbose POpts
opts String
" | " x
x) []
data Proxy1T deriving Int -> Proxy1T -> ShowS
[Proxy1T] -> ShowS
Proxy1T -> String
(Int -> Proxy1T -> ShowS)
-> (Proxy1T -> String) -> ([Proxy1T] -> ShowS) -> Show Proxy1T
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Proxy1T] -> ShowS
$cshowList :: [Proxy1T] -> ShowS
show :: Proxy1T -> String
$cshow :: Proxy1T -> String
showsPrec :: Int -> Proxy1T -> ShowS
$cshowsPrec :: Int -> Proxy1T -> ShowS
Show
instance P Proxy1T x where
type PP Proxy1T x = Proxy (ExtractTFromTA x)
eval :: proxy Proxy1T -> POpts -> x -> m (TT (PP Proxy1T x))
eval proxy Proxy1T
_ POpts
opts x
_ =
let b :: Proxy (ExtractTFromTA x)
b = Proxy (ExtractTFromTA x)
forall k (t :: k). Proxy t
Proxy @(ExtractTFromTA x)
in TT (Proxy (ExtractTFromTA x)) -> m (TT (Proxy (ExtractTFromTA x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (Proxy (ExtractTFromTA x))
-> m (TT (Proxy (ExtractTFromTA x))))
-> TT (Proxy (ExtractTFromTA x))
-> m (TT (Proxy (ExtractTFromTA x)))
forall a b. (a -> b) -> a -> b
$ POpts
-> Val (Proxy (ExtractTFromTA x))
-> String
-> [Tree PE]
-> TT (Proxy (ExtractTFromTA x))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (Proxy (ExtractTFromTA x) -> Val (Proxy (ExtractTFromTA x))
forall a. a -> Val a
Val Proxy (ExtractTFromTA x)
b) String
"Proxy1T" []
data Proxy2T deriving Int -> Proxy2T -> ShowS
[Proxy2T] -> ShowS
Proxy2T -> String
(Int -> Proxy2T -> ShowS)
-> (Proxy2T -> String) -> ([Proxy2T] -> ShowS) -> Show Proxy2T
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Proxy2T] -> ShowS
$cshowList :: [Proxy2T] -> ShowS
show :: Proxy2T -> String
$cshow :: Proxy2T -> String
showsPrec :: Int -> Proxy2T -> ShowS
$cshowsPrec :: Int -> Proxy2T -> ShowS
Show
instance P Proxy2T x where
type PP Proxy2T x = Proxy (Proxy2TT x)
eval :: proxy Proxy2T -> POpts -> x -> m (TT (PP Proxy2T x))
eval proxy Proxy2T
_ POpts
opts x
_ =
let b :: Proxy (Proxy2TT x)
b = Proxy (Proxy2TT x)
forall k (t :: k). Proxy t
Proxy @(Proxy2TT x)
in TT (Proxy (Proxy2TT x)) -> m (TT (Proxy (Proxy2TT x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (Proxy (Proxy2TT x)) -> m (TT (Proxy (Proxy2TT x))))
-> TT (Proxy (Proxy2TT x)) -> m (TT (Proxy (Proxy2TT x)))
forall a b. (a -> b) -> a -> b
$ POpts
-> Val (Proxy (Proxy2TT x))
-> String
-> [Tree PE]
-> TT (Proxy (Proxy2TT x))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (Proxy (Proxy2TT x) -> Val (Proxy (Proxy2TT x))
forall a. a -> Val a
Val Proxy (Proxy2TT x)
b) String
"Proxy2T" []
type family Proxy2TT (x :: Type) :: (Type -> Type) where
Proxy2TT (t a _) = t a
data Pop0 p q deriving Int -> Pop0 p q -> ShowS
[Pop0 p q] -> ShowS
Pop0 p q -> String
(Int -> Pop0 p q -> ShowS)
-> (Pop0 p q -> String) -> ([Pop0 p q] -> ShowS) -> Show (Pop0 p q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k). Int -> Pop0 p q -> ShowS
forall k (p :: k) k (q :: k). [Pop0 p q] -> ShowS
forall k (p :: k) k (q :: k). Pop0 p q -> String
showList :: [Pop0 p q] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k). [Pop0 p q] -> ShowS
show :: Pop0 p q -> String
$cshow :: forall k (p :: k) k (q :: k). Pop0 p q -> String
showsPrec :: Int -> Pop0 p q -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k). Int -> Pop0 p q -> ShowS
Show
instance ( P q x
, PP p x ~ proxy z
, P z (PP q x)
) => P (Pop0 p q) x where
type PP (Pop0 p q) x = Pop0T (PP p x) (PP q x)
eval :: proxy (Pop0 p q) -> POpts -> x -> m (TT (PP (Pop0 p q) x))
eval proxy (Pop0 p q)
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"Pop0"
TT (PP q x)
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 (PP q x)
-> [Tree PE]
-> Either (TT (PP z (PP q x))) (PP q x)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (PP q x)
qq [] of
Left TT (PP z (PP q x))
e -> TT (PP z (PP q x)) -> m (TT (PP z (PP q x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (PP z (PP q x))
e
Right PP q x
q -> do
TT (PP z (PP q x))
zz <- Proxy z -> POpts -> PP q x -> m (TT (PP z (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 z
forall k (t :: k). Proxy t
Proxy @z) POpts
opts PP q x
q
TT (PP z (PP q x)) -> m (TT (PP z (PP q x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP z (PP q x)) -> m (TT (PP z (PP q x))))
-> TT (PP z (PP q x)) -> m (TT (PP z (PP q x)))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP z (PP q x))
-> [Tree PE]
-> Either (TT (PP z (PP q x))) (PP z (PP q x))
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (PP z (PP q x))
zz [TT (PP q x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP q x)
qq] of
Left TT (PP z (PP q x))
e -> TT (PP z (PP q x))
e
Right PP z (PP q x)
_z -> POpts
-> TT (PP z (PP q x)) -> String -> [Tree PE] -> TT (PP z (PP q x))
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT (PP z (PP q x))
zz (String -> ShowS
joinStrings String
msg0 (TT (PP z (PP q x))
zz TT (PP z (PP q x))
-> Getting String (TT (PP z (PP q x))) String -> String
forall s a. s -> Getting a s a -> a
^. Getting String (TT (PP z (PP q x))) String
forall a. Lens' (TT a) String
ttString)) [TT (PP q x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP q x)
qq]
type family Pop0T (p :: Type) (q :: Type) :: Type where
Pop0T (Proxy z) q = PP z q
Pop0T (_proxy z) q = PP z q
Pop0T p q = GL.TypeError (
'GL.Text "Pop0T: requires 'Proxy z' and 'q' get applied to each other"
'GL.:$$: 'GL.Text " p = " 'GL.:<>: 'GL.ShowType p
'GL.:$$: 'GL.Text " q = " 'GL.:<>: 'GL.ShowType q
)
data Pop1 p q r deriving Int -> Pop1 p q r -> ShowS
[Pop1 p q r] -> ShowS
Pop1 p q r -> String
(Int -> Pop1 p q r -> ShowS)
-> (Pop1 p q r -> String)
-> ([Pop1 p q r] -> ShowS)
-> Show (Pop1 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 -> Pop1 p q r -> ShowS
forall k (p :: k) k (q :: k) k (r :: k). [Pop1 p q r] -> ShowS
forall k (p :: k) k (q :: k) k (r :: k). Pop1 p q r -> String
showList :: [Pop1 p q r] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k) k (r :: k). [Pop1 p q r] -> ShowS
show :: Pop1 p q r -> String
$cshow :: forall k (p :: k) k (q :: k) k (r :: k). Pop1 p q r -> String
showsPrec :: Int -> Pop1 p q r -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k) k (r :: k). Int -> Pop1 p q r -> ShowS
Show
instance ( P r x
, PP p x ~ Proxy (z :: k -> k1)
, P (z q) (PP r x)
) => P (Pop1 p q r) x where
type PP (Pop1 p q r) x = Pop1T (PP p x) q (PP r x)
eval :: proxy (Pop1 p q r) -> POpts -> x -> m (TT (PP (Pop1 p q r) x))
eval proxy (Pop1 p q r)
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"Pop1"
TT (PP r x)
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 (PP r x)
-> [Tree PE]
-> Either (TT (PP (z q) (PP r x))) (PP r x)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (PP r x)
rr [] of
Left TT (PP (z q) (PP r x))
e -> TT (PP (z q) (PP r x)) -> m (TT (PP (z q) (PP r x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (PP (z q) (PP r x))
e
Right PP r x
r -> do
TT (PP (z q) (PP r x))
zz <- Proxy (z q) -> POpts -> PP r x -> m (TT (PP (z q) (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 (z q)
forall k (t :: k). Proxy t
Proxy @(z q)) POpts
opts PP r x
r
TT (PP (z q) (PP r x)) -> m (TT (PP (z q) (PP r x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP (z q) (PP r x)) -> m (TT (PP (z q) (PP r x))))
-> TT (PP (z q) (PP r x)) -> m (TT (PP (z q) (PP r x)))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP (z q) (PP r x))
-> [Tree PE]
-> Either (TT (PP (z q) (PP r x))) (PP (z q) (PP r x))
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (PP (z q) (PP r x))
zz [TT (PP r x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP r x)
rr] of
Left TT (PP (z q) (PP r x))
e -> TT (PP (z q) (PP r x))
e
Right PP (z q) (PP r x)
_z -> POpts
-> TT (PP (z q) (PP r x))
-> String
-> [Tree PE]
-> TT (PP (z q) (PP r x))
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT (PP (z q) (PP r x))
zz (String -> ShowS
joinStrings String
msg0 (TT (PP (z q) (PP r x))
zz TT (PP (z q) (PP r x))
-> Getting String (TT (PP (z q) (PP r x))) String -> String
forall s a. s -> Getting a s a -> a
^. Getting String (TT (PP (z q) (PP r x))) String
forall a. Lens' (TT a) String
ttString)) [TT (PP r x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP r x)
rr]
type family Pop1T (p :: Type) (q :: k) (r :: Type) :: Type where
Pop1T (Proxy z) q r = PP (z q) r
Pop1T p q r =
GL.TypeError (
'GL.Text "Pop1T: requires 'Proxy z' and z must be a function requiring one parameter!!"
'GL.:$$: 'GL.Text " p = " 'GL.:<>: 'GL.ShowType p
'GL.:$$: 'GL.Text " q = " 'GL.:<>: 'GL.ShowType q
'GL.:$$: 'GL.Text " r = " 'GL.:<>: 'GL.ShowType r
)
data Pop1' p q r deriving Int -> Pop1' p q r -> ShowS
[Pop1' p q r] -> ShowS
Pop1' p q r -> String
(Int -> Pop1' p q r -> ShowS)
-> (Pop1' p q r -> String)
-> ([Pop1' p q r] -> ShowS)
-> Show (Pop1' 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 -> Pop1' p q r -> ShowS
forall k (p :: k) k (q :: k) k (r :: k). [Pop1' p q r] -> ShowS
forall k (p :: k) k (q :: k) k (r :: k). Pop1' p q r -> String
showList :: [Pop1' p q r] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k) k (r :: k). [Pop1' p q r] -> ShowS
show :: Pop1' p q r -> String
$cshow :: forall k (p :: k) k (q :: k) k (r :: k). Pop1' p q r -> String
showsPrec :: Int -> Pop1' p q r -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k) k (r :: k).
Int -> Pop1' p q r -> ShowS
Show
instance ( P r x
, PP p x ~ Proxy (z :: k -> k1)
, PP q x ~ Proxy (w :: k)
, P (z w) (PP r x)
) => P (Pop1' p q r) x where
type PP (Pop1' p q r) x = Pop1T' (PP p x) (PP q x) (PP r x)
eval :: proxy (Pop1' p q r) -> POpts -> x -> m (TT (PP (Pop1' p q r) x))
eval proxy (Pop1' p q r)
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"Pop1'"
TT (PP r x)
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 (PP r x)
-> [Tree PE]
-> Either (TT (PP (z w) (PP r x))) (PP r x)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (PP r x)
rr [] of
Left TT (PP (z w) (PP r x))
e -> TT (PP (z w) (PP r x)) -> m (TT (PP (z w) (PP r x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (PP (z w) (PP r x))
e
Right PP r x
r -> do
TT (PP (z w) (PP r x))
zz <- Proxy (z w) -> POpts -> PP r x -> m (TT (PP (z w) (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 (z w)
forall k (t :: k). Proxy t
Proxy @(z w)) POpts
opts PP r x
r
TT (PP (z w) (PP r x)) -> m (TT (PP (z w) (PP r x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP (z w) (PP r x)) -> m (TT (PP (z w) (PP r x))))
-> TT (PP (z w) (PP r x)) -> m (TT (PP (z w) (PP r x)))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP (z w) (PP r x))
-> [Tree PE]
-> Either (TT (PP (z w) (PP r x))) (PP (z w) (PP r x))
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (PP (z w) (PP r x))
zz [TT (PP r x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP r x)
rr] of
Left TT (PP (z w) (PP r x))
e -> TT (PP (z w) (PP r x))
e
Right PP (z w) (PP r x)
_z -> POpts
-> TT (PP (z w) (PP r x))
-> String
-> [Tree PE]
-> TT (PP (z w) (PP r x))
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT (PP (z w) (PP r x))
zz (String -> ShowS
joinStrings String
msg0 (TT (PP (z w) (PP r x))
zz TT (PP (z w) (PP r x))
-> Getting String (TT (PP (z w) (PP r x))) String -> String
forall s a. s -> Getting a s a -> a
^. Getting String (TT (PP (z w) (PP r x))) String
forall a. Lens' (TT a) String
ttString)) [TT (PP r x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP r x)
rr]
type family Pop1T' (p :: Type) (q :: Type) (r :: Type) :: Type where
Pop1T' (Proxy z) (Proxy w) r = PP (z w) r
Pop1T' p q r =
GL.TypeError (
'GL.Text "Pop1T': requires 'Proxy z' and z must be a function requiring one parameter!!"
'GL.:$$: 'GL.Text " p = " 'GL.:<>: 'GL.ShowType p
'GL.:$$: 'GL.Text " q = " 'GL.:<>: 'GL.ShowType q
'GL.:$$: 'GL.Text " r = " 'GL.:<>: 'GL.ShowType r
)
data Pop2 p q r s deriving Int -> Pop2 p q r s -> ShowS
[Pop2 p q r s] -> ShowS
Pop2 p q r s -> String
(Int -> Pop2 p q r s -> ShowS)
-> (Pop2 p q r s -> String)
-> ([Pop2 p q r s] -> ShowS)
-> Show (Pop2 p q r s)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k) k (r :: k) k (s :: k).
Int -> Pop2 p q r s -> ShowS
forall k (p :: k) k (q :: k) k (r :: k) k (s :: k).
[Pop2 p q r s] -> ShowS
forall k (p :: k) k (q :: k) k (r :: k) k (s :: k).
Pop2 p q r s -> String
showList :: [Pop2 p q r s] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k) k (r :: k) k (s :: k).
[Pop2 p q r s] -> ShowS
show :: Pop2 p q r s -> String
$cshow :: forall k (p :: k) k (q :: k) k (r :: k) k (s :: k).
Pop2 p q r s -> String
showsPrec :: Int -> Pop2 p q r s -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k) k (r :: k) k (s :: k).
Int -> Pop2 p q r s -> ShowS
Show
instance ( P s x
, PP p x ~ Proxy (z :: k -> k1 -> k2)
, P (z q r) (PP s x)
) => P (Pop2 p q r s) x where
type PP (Pop2 p q r s) x = Pop2T (PP p x) q r (PP s x)
eval :: proxy (Pop2 p q r s) -> POpts -> x -> m (TT (PP (Pop2 p q r s) x))
eval proxy (Pop2 p q r s)
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"Pop2"
TT (PP s x)
ss <- Proxy s -> POpts -> x -> m (TT (PP s 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 s
forall k (t :: k). Proxy t
Proxy @s) POpts
opts x
x
case Inline
-> POpts
-> String
-> TT (PP s x)
-> [Tree PE]
-> Either (TT (PP (z q r) (PP s x))) (PP s x)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (PP s x)
ss [] of
Left TT (PP (z q r) (PP s x))
e -> TT (PP (z q r) (PP s x)) -> m (TT (PP (z q r) (PP s x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (PP (z q r) (PP s x))
e
Right PP s x
s -> do
TT (PP (z q r) (PP s x))
zz <- Proxy (z q r) -> POpts -> PP s x -> m (TT (PP (z q r) (PP s 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 (z q r)
forall k (t :: k). Proxy t
Proxy @(z q r)) POpts
opts PP s x
s
TT (PP (z q r) (PP s x)) -> m (TT (PP (z q r) (PP s x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP (z q r) (PP s x)) -> m (TT (PP (z q r) (PP s x))))
-> TT (PP (z q r) (PP s x)) -> m (TT (PP (z q r) (PP s x)))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP (z q r) (PP s x))
-> [Tree PE]
-> Either (TT (PP (z q r) (PP s x))) (PP (z q r) (PP s x))
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (PP (z q r) (PP s x))
zz [TT (PP s x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP s x)
ss] of
Left TT (PP (z q r) (PP s x))
e -> TT (PP (z q r) (PP s x))
e
Right PP (z q r) (PP s x)
_z -> POpts
-> TT (PP (z q r) (PP s x))
-> String
-> [Tree PE]
-> TT (PP (z q r) (PP s x))
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT (PP (z q r) (PP s x))
zz (String -> ShowS
joinStrings String
msg0 (TT (PP (z q r) (PP s x))
zz TT (PP (z q r) (PP s x))
-> Getting String (TT (PP (z q r) (PP s x))) String -> String
forall s a. s -> Getting a s a -> a
^. Getting String (TT (PP (z q r) (PP s x))) String
forall a. Lens' (TT a) String
ttString)) [TT (PP s x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP s x)
ss]
type family Pop2T (p :: Type) (q :: k) (r :: k1) (s :: Type) :: Type where
Pop2T (Proxy z) q r s = PP (z q r) s
Pop2T p q r s =
GL.TypeError (
'GL.Text "Pop2T: requires 'Proxy z' and z must be a function requiring one parameter!!"
'GL.:$$: 'GL.Text " p = " 'GL.:<>: 'GL.ShowType p
'GL.:$$: 'GL.Text " q = " 'GL.:<>: 'GL.ShowType q
'GL.:$$: 'GL.Text " r = " 'GL.:<>: 'GL.ShowType r
'GL.:$$: 'GL.Text " s = " 'GL.:<>: 'GL.ShowType s
)
data Pop2' p q r s deriving Int -> Pop2' p q r s -> ShowS
[Pop2' p q r s] -> ShowS
Pop2' p q r s -> String
(Int -> Pop2' p q r s -> ShowS)
-> (Pop2' p q r s -> String)
-> ([Pop2' p q r s] -> ShowS)
-> Show (Pop2' p q r s)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k) k (r :: k) k (s :: k).
Int -> Pop2' p q r s -> ShowS
forall k (p :: k) k (q :: k) k (r :: k) k (s :: k).
[Pop2' p q r s] -> ShowS
forall k (p :: k) k (q :: k) k (r :: k) k (s :: k).
Pop2' p q r s -> String
showList :: [Pop2' p q r s] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k) k (r :: k) k (s :: k).
[Pop2' p q r s] -> ShowS
show :: Pop2' p q r s -> String
$cshow :: forall k (p :: k) k (q :: k) k (r :: k) k (s :: k).
Pop2' p q r s -> String
showsPrec :: Int -> Pop2' p q r s -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k) k (r :: k) k (s :: k).
Int -> Pop2' p q r s -> ShowS
Show
instance ( P s x
, PP p x ~ Proxy (z :: k -> k1 -> k2)
, PP q x ~ Proxy (w :: k)
, PP r x ~ Proxy (v :: k1)
, P (z w v) (PP s x)
) => P (Pop2' p q r s) x where
type PP (Pop2' p q r s) x = Pop2T' (PP p x) (PP q x) (PP r x) (PP s x)
eval :: proxy (Pop2' p q r s)
-> POpts -> x -> m (TT (PP (Pop2' p q r s) x))
eval proxy (Pop2' p q r s)
_ POpts
opts x
x = do
let msg0 :: String
msg0 = String
"Pop2'"
TT (PP s x)
ss <- Proxy s -> POpts -> x -> m (TT (PP s 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 s
forall k (t :: k). Proxy t
Proxy @s) POpts
opts x
x
case Inline
-> POpts
-> String
-> TT (PP s x)
-> [Tree PE]
-> Either (TT (PP (z w v) (PP s x))) (PP s x)
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (PP s x)
ss [] of
Left TT (PP (z w v) (PP s x))
e -> TT (PP (z w v) (PP s x)) -> m (TT (PP (z w v) (PP s x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (PP (z w v) (PP s x))
e
Right PP s x
s -> do
TT (PP (z w v) (PP s x))
zz <- Proxy (z w v) -> POpts -> PP s x -> m (TT (PP (z w v) (PP s 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 (z w v)
forall k (t :: k). Proxy t
Proxy @(z w v)) POpts
opts PP s x
s
TT (PP (z w v) (PP s x)) -> m (TT (PP (z w v) (PP s x)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (PP (z w v) (PP s x)) -> m (TT (PP (z w v) (PP s x))))
-> TT (PP (z w v) (PP s x)) -> m (TT (PP (z w v) (PP s x)))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (PP (z w v) (PP s x))
-> [Tree PE]
-> Either (TT (PP (z w v) (PP s x))) (PP (z w v) (PP s x))
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
NoInline POpts
opts String
msg0 TT (PP (z w v) (PP s x))
zz [TT (PP s x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP s x)
ss] of
Left TT (PP (z w v) (PP s x))
e -> TT (PP (z w v) (PP s x))
e
Right PP (z w v) (PP s x)
_z -> POpts
-> TT (PP (z w v) (PP s x))
-> String
-> [Tree PE]
-> TT (PP (z w v) (PP s x))
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT (PP (z w v) (PP s x))
zz (String -> ShowS
joinStrings String
msg0 (TT (PP (z w v) (PP s x))
zz TT (PP (z w v) (PP s x))
-> Getting String (TT (PP (z w v) (PP s x))) String -> String
forall s a. s -> Getting a s a -> a
^. Getting String (TT (PP (z w v) (PP s x))) String
forall a. Lens' (TT a) String
ttString)) [TT (PP s x) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP s x)
ss]
type family Pop2T' (p :: Type) (q :: Type) (r :: Type) (s :: Type) :: Type where
Pop2T' (Proxy z) (Proxy w) (Proxy v) s = PP (z w v) s
Pop2T' p q r s =
GL.TypeError (
'GL.Text "Pop2T': requires 'Proxy z' and z must be a function requiring one parameter!!"
'GL.:$$: 'GL.Text " p = " 'GL.:<>: 'GL.ShowType p
'GL.:$$: 'GL.Text " q = " 'GL.:<>: 'GL.ShowType q
'GL.:$$: 'GL.Text " r = " 'GL.:<>: 'GL.ShowType r
'GL.:$$: 'GL.Text " s = " 'GL.:<>: 'GL.ShowType s
)
data PApp p q deriving Int -> PApp p q -> ShowS
[PApp p q] -> ShowS
PApp p q -> String
(Int -> PApp p q -> ShowS)
-> (PApp p q -> String) -> ([PApp p q] -> ShowS) -> Show (PApp p q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k). Int -> PApp p q -> ShowS
forall k (p :: k) k (q :: k). [PApp p q] -> ShowS
forall k (p :: k) k (q :: k). PApp p q -> String
showList :: [PApp p q] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k). [PApp p q] -> ShowS
show :: PApp p q -> String
$cshow :: forall k (p :: k) k (q :: k). PApp p q -> String
showsPrec :: Int -> PApp p q -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k). Int -> PApp p q -> ShowS
Show
instance ( PP p x ~ Proxy (z :: k -> k1)
, PP q x ~ Proxy (w :: k)
) => P (PApp p q) x where
type PP (PApp p q) x = PAppT (PP p x) (PP q x)
eval :: proxy (PApp p q) -> POpts -> x -> m (TT (PP (PApp p q) x))
eval proxy (PApp p q)
_ POpts
opts x
_ =
TT (Proxy (z w)) -> m (TT (Proxy (z w)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (Proxy (z w)) -> m (TT (Proxy (z w))))
-> TT (Proxy (z w)) -> m (TT (Proxy (z w)))
forall a b. (a -> b) -> a -> b
$ POpts
-> Val (Proxy (z w)) -> String -> [Tree PE] -> TT (Proxy (z w))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (Proxy (z w) -> Val (Proxy (z w))
forall a. a -> Val a
Val Proxy (z w)
forall k (t :: k). Proxy t
Proxy) String
"PApp" []
type family PAppT (p :: Type) (q :: Type) :: Type where
PAppT (Proxy z) (Proxy w) = Proxy (z w)
PAppT p q =
GL.TypeError (
'GL.Text "PAppT: requires 'Proxy z' and 'Proxy w' get applied to each other"
'GL.:$$: 'GL.Text " p = " 'GL.:<>: 'GL.ShowType p
'GL.:$$: 'GL.Text " q = " 'GL.:<>: 'GL.ShowType q
)
data PApp2 p q r deriving Int -> PApp2 p q r -> ShowS
[PApp2 p q r] -> ShowS
PApp2 p q r -> String
(Int -> PApp2 p q r -> ShowS)
-> (PApp2 p q r -> String)
-> ([PApp2 p q r] -> ShowS)
-> Show (PApp2 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 -> PApp2 p q r -> ShowS
forall k (p :: k) k (q :: k) k (r :: k). [PApp2 p q r] -> ShowS
forall k (p :: k) k (q :: k) k (r :: k). PApp2 p q r -> String
showList :: [PApp2 p q r] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k) k (r :: k). [PApp2 p q r] -> ShowS
show :: PApp2 p q r -> String
$cshow :: forall k (p :: k) k (q :: k) k (r :: k). PApp2 p q r -> String
showsPrec :: Int -> PApp2 p q r -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k) k (r :: k).
Int -> PApp2 p q r -> ShowS
Show
instance ( PP p x ~ Proxy (z :: k -> k1 -> k2)
, PP q x ~ Proxy (w :: k)
, PP r x ~ Proxy (v :: k1)
) => P (PApp2 p q r) x where
type PP (PApp2 p q r) x = PApp2T (PP p x) (PP q x) (PP r x)
eval :: proxy (PApp2 p q r) -> POpts -> x -> m (TT (PP (PApp2 p q r) x))
eval proxy (PApp2 p q r)
_ POpts
opts x
_ =
TT (Proxy (z w v)) -> m (TT (Proxy (z w v)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (Proxy (z w v)) -> m (TT (Proxy (z w v))))
-> TT (Proxy (z w v)) -> m (TT (Proxy (z w v)))
forall a b. (a -> b) -> a -> b
$ POpts
-> Val (Proxy (z w v)) -> String -> [Tree PE] -> TT (Proxy (z w v))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (Proxy (z w v) -> Val (Proxy (z w v))
forall a. a -> Val a
Val Proxy (z w v)
forall k (t :: k). Proxy t
Proxy) String
"PApp2" []
type family PApp2T (p :: Type) (q :: Type) (r :: Type) :: Type where
PApp2T (Proxy z) (Proxy w) (Proxy v) = Proxy (z w v)
PApp2T p q r =
GL.TypeError (
'GL.Text "PApp2T: requires 'Proxy z', 'Proxy w' and 'Proxy v': z is applied to w and v"
'GL.:$$: 'GL.Text " p = " 'GL.:<>: 'GL.ShowType p
'GL.:$$: 'GL.Text " q = " 'GL.:<>: 'GL.ShowType q
'GL.:$$: 'GL.Text " r = " 'GL.:<>: 'GL.ShowType r
)
data Proxify p deriving Int -> Proxify p -> ShowS
[Proxify p] -> ShowS
Proxify p -> String
(Int -> Proxify p -> ShowS)
-> (Proxify p -> String)
-> ([Proxify p] -> ShowS)
-> Show (Proxify p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k). Int -> Proxify p -> ShowS
forall k (p :: k). [Proxify p] -> ShowS
forall k (p :: k). Proxify p -> String
showList :: [Proxify p] -> ShowS
$cshowList :: forall k (p :: k). [Proxify p] -> ShowS
show :: Proxify p -> String
$cshow :: forall k (p :: k). Proxify p -> String
showsPrec :: Int -> Proxify p -> ShowS
$cshowsPrec :: forall k (p :: k). Int -> Proxify p -> ShowS
Show
instance PP p x ~ proxy (z :: k)
=> P (Proxify p) x where
type PP (Proxify p) x = ProxifyT (PP p x)
eval :: proxy (Proxify p) -> POpts -> x -> m (TT (PP (Proxify p) x))
eval proxy (Proxify p)
_ POpts
opts x
_ =
TT (Proxy z) -> m (TT (Proxy z))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (Proxy z) -> m (TT (Proxy z)))
-> TT (Proxy z) -> m (TT (Proxy z))
forall a b. (a -> b) -> a -> b
$ POpts -> Val (Proxy z) -> String -> [Tree PE] -> TT (Proxy z)
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (Proxy z -> Val (Proxy z)
forall a. a -> Val a
Val Proxy z
forall k (t :: k). Proxy t
Proxy) String
"Proxify" []
type family ProxifyT p where
ProxifyT (_proxy z) = Proxy z
ProxifyT p = GL.TypeError (
'GL.Text "ProxifyT: requires any 'proxy z'"
'GL.:$$: 'GL.Text " p = " 'GL.:<>: 'GL.ShowType p
)