{-# 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 #-}
-- | promoted functions for proxies

module Predicate.Data.Proxy (
  -- ** create a proxy from a type

    ProxyT
  , Proxy1T
  , Proxy2T
  , Proxify
  -- ** simple proxy application

  , Pop0
  -- ** needs kind signatures on @p@

  , Pop1
  , Pop2
  , Pop1'
  , Pop2'
  , PApp
  , PApp2

 -- ** type families

  , 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
-- $setup

-- >>> :set -XDataKinds

-- >>> :set -XTypeApplications

-- >>> :set -XTypeOperators

-- >>> import Predicate

-- >>> import Control.Lens

-- >>> import Control.Lens.Action

-- >>> import qualified Data.Semigroup as SG

-- >>> :m + Text.Show.Functions

-- >>> :m + Data.Ratio

-- >>> :m + Data.Typeable


-- | makes a proxy from a simple type: similar to the P instance for 'Proxy but requires a show instance

--

-- >>> pz @(Pop1' (Proxy FromInteger) ProxyT 123) (4 % 0)

-- Val (123 % 1)

--

-- >>> pz @(Pop1' (Proxy MEmptyT) ProxyT ()) (SG.Product 4)

-- Val (Product {getProduct = 1})

--

-- >>> pz @((Id $$ 44) >> Pop1' (Proxy MEmptyT) ProxyT ())  SG.Product

-- Val (Product {getProduct = 1})

--

-- >>> pz @((ProxyT << Fst) >> FMap Head) ([True],13) ^!? acts . _Val . to typeRep -- Proxify is easier

-- Just Bool

--

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) []

-- | makes a proxy from a one parameter container

--

-- >>> pz @(Pop2' (Proxy EmptyT) Proxy1T (Proxy Int) 123) Nothing

-- Val Nothing

--

-- >>> pz @(Pop2' (Proxy EmptyT) Proxy1T (Proxy Int) 123) (Just 10)

-- Val Nothing

--

-- >>> pz @((Id $$ ()) >> Pop2' (Proxy EmptyT) Proxy1T (Proxy Int) 123) Just

-- Val Nothing

--

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" []

-- | makes a proxy from a two parameter container

--

-- >>> pz @(Pop2' (Proxy EmptyT) Proxy2T (Proxy Int) 123) (Left "ASf")

-- Val (Left "")

--

-- >>> pz @(Pop2' (Proxy EmptyT) Proxy2T (Proxy Int) 123) (Right 1)

-- Val (Left "")

--

-- >>> pz @((Id $$ "asdf") >> Pop2' (Proxy EmptyT) Proxy2T (Proxy Int) 123) Left

-- Val (Left "")

--

-- >>> pz @((Id $$ "asdf") >> Pop2' (Proxy EmptyT) Proxy2T (Proxy Int) 123) Right

-- Val (Left "")

--

-- >>> pz @(Pop2' (Proxy EmptyT) ((Id $$ "ss") >> Proxy2T) (Proxy Int) 123) Right

-- Val (Left "")

--

-- >>> pz @(Pop2' (Proxy EmptyT) ((Id $$ "ss") >> Proxy2T) (Proxy Int) 123) Left

-- Val (Left "")

--

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" []

-- | calculate the resulting type for 'Proxy2T'

type family Proxy2TT (x :: Type) :: (Type -> Type) where
  Proxy2TT (t a _) = t a

-- | run the proxy @p@ in the environment pointed to by @q@

--

-- >>> pl @(Pop0 (Proxy '(Head,Len)) "abcdef") ()

-- Present ('a',6) (Pop0 | '('a',6))

-- Val ('a',6)

--

-- >>> pz @(Pop0 Id "abcdef") (Proxy @'(Head,Len))

-- Val ('a',6)

--

-- >>> pl @(Pop0 Fst Snd) (Proxy @Snd,("dd","ee"))

-- Present "ee" (Pop0 | Snd "ee" | ("dd","ee"))

-- Val "ee"

--

-- >>> pz @(Pop0 Fst L22) (Proxy @(Fst <> Snd),(True,("dd","ee")))

-- Val "ddee"

--

-- >>> pz @(Pop0 Id () <> "def") (Proxy @"abc") -- Proxy works for any kind!

-- Val "abcdef"

--

-- >>> pz @(Pop0 Id () <> "def") (Nothing @(W "abc")) -- Proxy works for any kind!

-- Val "abcdef"

--

-- >>> pz @(Pop0 Id (C "A")) (Proxy @Succ)

-- Val 'B'

--

-- >>> pz @(Pop0 Fst Snd) (Proxy @(All1 Even),[1,5,2,3,4])

-- Val False

--

-- >>> pz @(Pop0 Fst Snd) (Proxy @(Partition Even Snd),(True,[8,1,5,2,3,4,6]))

-- Val ([8,2,4,6],[1,5,3])

--

-- >>> pl @(Proxy Snd >> Pop0 Id '( 'True,2)) ()

-- Present 2 ((>>) 2 | {Pop0 | Snd 2 | (True,2)})

-- Val 2

--

-- >>> pl @(Proxy (Fst <> Snd) >> Pop0 Id '("aa","bb")) ()

-- Present "aabb" ((>>) "aabb" | {Pop0 | "aa" <> "bb" = "aabb"})

-- Val "aabb"

--

-- >>> pz @(Pop0 Fst Snd) (Proxy @Succ,EQ)

-- Val GT

--

-- >>> pz @(Pop0 Fst Snd) (Proxy @(FMap Succ),Just 23)

-- Val (Just 24)

--

-- >>> pz @(Pop0 Id (1 ... 12)) (Proxy @(FMap Succ))

-- Val [2,3,4,5,6,7,8,9,10,11,12,13]

--

-- >>> pz @(Pop0 Id '( 'True, MkJust 12)) (Proxy @(FMap $ FMap Succ))

-- Val (True,Just 13)

--

-- >>> pz @('(Id, PApp (Proxy '(,)) (Proxy 4)) >> Second (PApp Id (Proxy Fst)) >> Pop0 Snd Fst) ("abc",True)

-- Val (4,"abc")

--

-- >>> pz @(Pop1 (Proxy Proxy) "abc" () >> Pop0 Id ()) ()

-- Val "abc"

--

-- >>> pz @(Proxy (Proxy (Proxy "asdff")) >> Pop0 Id () >> Pop0 Id () >> Pop0 Id ()) ()

-- Val "asdff"

--

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]

-- the key is to pass all the vars into the type family so ghc can figure stuff out

-- | calculate the resulting type for 'Pop0'

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
   )

-- | applies Proxy @p@ to @q@ in the environment pointed to by @r@ : needs kind signatures on @p@

--

-- >>> pz @(Pop1 Fst L22 Snd) (Proxy @Length,(False,('x',"abcdef")))

-- Val 6

--

-- >>> pz @(Proxy Length >> Pop1 IdT Snd '(1,'[1,2,3,4])) ()

-- Val 4

--

-- >>> pz @(LiftA2 (Pop1 Fst Snd Id) (MkJust (Proxy (Lift Succ))) (MkJust 1)) ()

-- Val (Just 2)

--

-- >>> pz @(LiftA2 (Pop1 Fst Snd Id) (MkJust (Proxy ((*) 4))) (MkJust 3)) ()

-- Val (Just 12)

--

-- >>> pz @(Pop1 Fst Snd Id <$> MkJust (Proxy ((*) 4)) <:> MkJust 3) ()

-- Val (Just 12)

--

-- >>> pz @(Pop1 Fst Snd Id <$> Fst <:> Snd) (Just (Proxy @((*) 4)), Just 3)

-- Val (Just 12)

--

-- >>> pz @(Proxy (Lift "asdf") >> Pop1 Id 123 Id) ()

-- Val "asdf"

--

-- >>> pz @(Pop1 Id "abc" ()) (Proxy @(K 99))

-- Val 99

--

-- >>> pz @(Pop1 Id "abc" ()) (Proxy @(Flip K 99))

-- Val "abc"

--

-- >>> pz @(Pop1 (Proxy ('(,) 'True)) Len "abc") ()

-- Val (True,3)

--

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
--        zz <- eval (Proxy @(Pop1T (PP p x) q)) opts r

        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]

-- | calculate the resulting type for 'Pop1'

type family Pop1T (p :: Type) (q :: k) (r :: Type) :: Type where
  Pop1T (Proxy z) q r = PP (z q) r
--  Pop1T (Proxy (z :: k -> k1)) (q :: k) r = PP (z q :: k1) 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
    )

-- | apply Proxy @p@ to Proxy @q@ and run in the environment pointed to by @r@ : needs kind signatures on @p@

--

-- >>> pz @(Pop1' (Proxy ((<>) Snd)) (Proxy Fst) Id) ("abc","def")

-- Val "defabc"

--

-- >>> pz @(Pop1' (Proxy ((>>) Snd)) (Proxy (Resplit "\\." >> Map (ReadP Int Id))) Id) (1,"123.33.5")

-- Val [123,33,5]

--

-- >>> pz @(Pop1' (Proxy (Lift Snd)) (Proxy Fst) Id) ((True,2),("abc",1 % 4))

-- Val 2

--

-- >>> pz @(Pop1' Fst Snd Thd) (Proxy @(Lift Snd), Proxy @Fst,((True,2),("abc",1 % 4)))

-- Val 2

--

-- >>> pz @(Pop1' Fst Snd '( '( 'True,2),'("abc",1 % 4))) (Proxy @(Lift Snd), Proxy @Fst)

-- Val 2

--

-- >>> pz @(Pop1' (Proxy MEmptyT) (Proxy (SG.Sum _)) ()) ()

-- Val (Sum {getSum = 0})

--

-- >>> pz @(Pop1' (Proxy MEmptyT) (PApp (Proxy SG.Sum) (Proxy Float)) ()) ()

-- Val (Sum {getSum = 0.0})

--

-- >>> pz @(Pop1' (Proxy Proxy) (Proxy Fst) () >> Pop0 Id '("abc",1234)) ()

-- Val "abc"

--

-- >>> pz @(Pop1' (Proxy ToEnum) 'Proxy 100) 'a'

-- Val 'd'

--

-- >>> pz @(Pop1' (Proxy ToEnum) 'Proxy 120) (undefined :: Char)

-- Val 'x'

--

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]

-- | calculate the resulting type for 'Pop1''

type family Pop1T' (p :: Type) (q :: Type) (r :: Type) :: Type where
  Pop1T' (Proxy z) (Proxy w) r = PP (z w) r
--  Pop1T' (Proxy (z :: k -> k1)) (Proxy (w :: k)) r = PP (z w :: k1) 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
    )

-- | apply Proxy @p@ to @q@ and @r@ then run in the environment pointed to by @s@ : needs kind signatures on @p@

--

-- >>> pz @(Pop2 (Proxy '(,)) Fst 14 Id) ([1..4],'True)

-- Val ([1,2,3,4],14)

--

-- >>> pz @(Pop2' (Proxy Pure) (Proxy SG.Sum) (Proxy Id) Id) 123

-- Val (Sum {getSum = 123})

--

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]

-- pass all the arguments in!!! else ghc gets confused

-- | calculate the resulting type for 'Pop2'

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 (Proxy (z :: k -> k1 -> k2)) (q :: k) (r :: k1) s = PP (z q r :: k2) 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
    )

-- | Applies Proxy @p@ to Proxy @q@ and Proxy @r@ and runs in the environment pointed to by @s@ : needs kind signatures on @p@

--

-- >>> pz @(Pop2' (Proxy '(,)) (Proxy 1) (Proxy "sss") ()) ()

-- Val (1,"sss")

--

-- >>> pz @(Pop2' (Proxy '(,)) (Proxy L31) (Proxy (Fst % Snd)) '(11,99,'("ss",3))) ()

-- Val ("ss",1 % 9)

--

-- >>> pz @(Pop2' Fst Snd Thd (L4 Id)) (Proxy @'(,), Proxy @L31, Proxy @(Fst % Snd), (11,99,("ss",3)))

-- Val ("ss",1 % 9)

--

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]

-- pass in all the arguments otherwise ghc gets confused

-- | calculate the resulting type for 'Pop2''

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' (Proxy (z :: k -> k1 -> k2)) (Proxy (w :: k)) (Proxy (v :: k1)) s = PP (z w v :: k2) 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
    )

-- | applies Proxy @p@ to Proxy @q@ and returns a Proxy: needs kind signatures on @p@

--

-- >>> pz @(PApp Fst Snd >> Pop0 Id '("abcdef",99)) (Proxy @('(,) (Fst >> Len)), Proxy @16)

-- Val (6,16)

--

-- >>> pz @('(Id,PApp (Proxy ('(,) (Fst >> Len))) (Proxy 16)) >> Pop0 Snd Fst) ("abcdefg",101)

-- Val (7,16)

--

-- >>> pz @('(Id,PApp (Proxy '(,)) (Proxy (Fst >> Len))) >> Second (PApp Id (Proxy 16)) >> Pop0 Snd Fst) ("abcdefg",101) -- or can call PApp2

-- Val (7,16)

--

-- >>> pz @(PApp (PApp (Proxy ('(,) :: GL.Nat -> GL.Symbol -> (GL.Nat,GL.Symbol))) (Proxy 1)) (Proxy "abc")) () ^!? acts . _Val . to typeRep

-- Just ('(,) Nat Symbol 1 "abc")

--

-- >>> pz @(PApp (Proxy '(,)) (Proxy 4) >> PApp Id (Proxy Fst) >> Pop0 Id (W '(1,2))) ()

-- Val (4,1)

--

-- >>> pz @(PApp (Proxy '(,)) (Proxy 4) >> PApp Id (Proxy Fst) >> Pop0 Id '( 'True,"hello")) ()

-- Val (4,True)

--

-- >>> pan @(PApp (Proxy (MsgI "hello ")) Fst >> Pop0 Id '(1,2,3)) (Proxy @"there",())

-- P (>>) "there"

-- |

-- +- P PApp

-- |

-- `- P Pop0 | hello '"there"

--    |

--    +- P '(,,)

--    |  |

--    |  +- P '1

--    |  |

--    |  +- P '2

--    |  |

--    |  `- P '3

--    |

--    `- P hello '"there"

-- Val "there"

--

-- >>> pz @(PApp (Proxy Proxy) (Proxy "abc") >> Pop0 Id () >> Pop0 Id ()) ()

-- Val "abc"

--

-- >>> pz @(PApp (Proxy '(,,)) (Proxy 10) >> PApp Id (Proxy "ss") >> PApp Id (Proxy Fst) >> Pop0 Id '(13 % 44,C "x")) ()

-- Val (10,"ss",13 % 44)

--

-- >>> pz @('(Id,PApp (Proxy '(,,)) (Proxy 10) >> PApp Id (Proxy "ss") >> PApp Id (Proxy Fst)) >> Pop0 Snd Fst) (13 % 44,'x')

-- Val (10,"ss",13 % 44)

--

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" []

-- | calculate the resulting type for 'PApp'

type family PAppT (p :: Type) (q :: Type) :: Type where
  PAppT (Proxy z) (Proxy w) = Proxy (z w)
--  PAppT (Proxy (z :: k -> k1)) (Proxy (w :: k)) = Proxy (z w :: k1)

  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
    )

-- | applies Proxy @p@ to Proxy @q@ and Proxy @r@ and returns a Proxy: needs kind signatures on @p@

--

-- >>> pz @(PApp2 (Proxy '(,)) (Proxy 2) (Proxy 'True) >> Pop0 Id ()) ()

-- Val (2,True)

--

-- >>> pz @('(Snd, PApp2 (Proxy (+)) L11 L12) >> Pop0 Snd Fst) ((Proxy @Fst,Proxy @(Length Snd)),(5,"abcdef"))

-- Val 11

--

-- >>> pz @(PApp2 (Proxy (+)) Fst Snd >> Pop0 Id ()) (Proxy @(W 3),Proxy @(W 7))

-- Val 10

--

-- >>> pz @(PApp2 Fst Snd Thd >> Pop0 Id ()) (Proxy @(&&&), Proxy @(W "abc"), Proxy @(W 13))

-- Val ("abc",13)

--

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" []

-- | calculate the resulting type for 'PApp2'

type family PApp2T (p :: Type) (q :: Type) (r :: Type) :: Type where
  PApp2T (Proxy z) (Proxy w) (Proxy v) = Proxy (z w v)
  --PApp2T (Proxy (z :: k -> k1 -> k2)) (Proxy (w :: k)) (Proxy (v :: k1)) = Proxy (z w v :: k2)

  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
   )

-- | create a Proxy z from proxy z where z is the expression pointed to by @p@ : Proxify alway returns Val (Proxy @z)

--

-- >>> pz @(Proxify Fst) ([True],13) ^!? acts . _Val . only (Proxy @Bool)

-- Just ()

--

-- >>> pz @(Proxify (MkJust 1)) () ^!? acts . _Val . to typeRep

-- Just Int

--

-- >>> pz @(Proxify (FailT [Double] "abc")) () ^!? acts . _Val . to typeRep

-- Just Double

--

-- >>> pz @(Proxify "abc") () ^!? acts . _Val . to typeRep

-- Just Char

--

-- >>> eval (Proxy @(Proxify Id)) defOpts ([] @Double) ^!? acts . ttVal . _Val . to typeRep

-- Just Double

--

-- >>> eval (Proxy @(Proxify Id)) defOpts ([] @Int) ^? _Id . ttVal . _Val == Just (Proxy @Int)

-- True

--

-- >>> eval (Proxy @(Proxify Id)) defOpts ([] @Int) ^? _Wrapped @(Identity _) . ttVal . _Val == Just (Proxy @Int)

-- True

--

-- >>> eval (Proxy @(Proxify Id)) defOpts ([] @Int) ^? folded @Identity . ttVal . _Val == Just (Proxy @Int)

-- True

--

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" []

-- | calculate the resulting type for '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
      )