{-# 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 indexing functions

module Predicate.Data.Index (
    Ix
  , Ix'
  , IxL
  , type (!!)
  , type (!!?)
  , Lookup
  , LookupDef
  , LookupDef'
  , LookupFail
  , LookupFail'
 ) where
import Predicate.Core
import Predicate.Misc
import Predicate.Util
import Predicate.Data.Maybe (JustDef, JustFail)
import Control.Lens
import GHC.TypeLits (Nat, KnownNat)
import Data.Proxy (Proxy(..))

-- $setup

-- >>> :set -XDataKinds

-- >>> :set -XTypeApplications

-- >>> :set -XTypeOperators

-- >>> :set -XOverloadedStrings

-- >>> import qualified Data.Map.Strict as M

-- >>> import qualified Data.Set as Set

-- >>> import qualified Data.Text as T

-- >>> import Predicate

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


-- | index a value in an 'Ixed' container and if not found return the given default value

--

-- >>> pl @(LookupDef' Snd Fst (C "xx") Id) (['a'..'e'],2)

-- Present 'c' (JustDef Just)

-- Val 'c'

--

-- >>> pl @(LookupDef' Snd Fst (C "xx") Id) (['a'..'e'],999)

-- Present 'x' (JustDef Nothing)

-- Val 'x'

--

-- >>> pl @(LookupDef' Snd Fst (C "xx") Id) ([],2)

-- Present 'x' (JustDef Nothing)

-- Val 'x'

--

-- >>> pl @(LookupDef' Snd Fst (C "xx") Snd) ('w',([],2))

-- Present 'x' (JustDef Nothing)

-- Val 'x'

--

-- >>> pl @(LookupDef' Snd Fst Fst Snd) ('x',(['a'..'e'],2))

-- Present 'c' (JustDef Just)

-- Val 'c'

--

-- >>> pl @(LookupDef' Snd Fst (MEmptyT _) Snd) ('x',(map SG.Min [10..15::Int], 3))

-- Present Min {getMin = 13} (JustDef Just)

-- Val (Min {getMin = 13})

--

data LookupDef' v w p q deriving Int -> LookupDef' v w p q -> ShowS
[LookupDef' v w p q] -> ShowS
LookupDef' v w p q -> String
(Int -> LookupDef' v w p q -> ShowS)
-> (LookupDef' v w p q -> String)
-> ([LookupDef' v w p q] -> ShowS)
-> Show (LookupDef' v w p q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (v :: k) k (w :: k) k (p :: k) k (q :: k).
Int -> LookupDef' v w p q -> ShowS
forall k (v :: k) k (w :: k) k (p :: k) k (q :: k).
[LookupDef' v w p q] -> ShowS
forall k (v :: k) k (w :: k) k (p :: k) k (q :: k).
LookupDef' v w p q -> String
showList :: [LookupDef' v w p q] -> ShowS
$cshowList :: forall k (v :: k) k (w :: k) k (p :: k) k (q :: k).
[LookupDef' v w p q] -> ShowS
show :: LookupDef' v w p q -> String
$cshow :: forall k (v :: k) k (w :: k) k (p :: k) k (q :: k).
LookupDef' v w p q -> String
showsPrec :: Int -> LookupDef' v w p q -> ShowS
$cshowsPrec :: forall k (v :: k) k (w :: k) k (p :: k) k (q :: k).
Int -> LookupDef' v w p q -> ShowS
Show
type LookupDefT' v w p q = JustDef p (q >> Lookup v w)

instance P (LookupDefT' v w p q) x => P (LookupDef' v w p q) x where
  type PP (LookupDef' v w p q) x = PP (LookupDefT' v w p q) x
  eval :: proxy (LookupDef' v w p q)
-> POpts -> x -> m (TT (PP (LookupDef' v w p q) x))
eval proxy (LookupDef' v w p q)
_ = Proxy (LookupDefT' v w p q)
-> POpts -> x -> m (TT (PP (LookupDefT' v w 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 (LookupDefT' v w p q)
forall k (t :: k). Proxy t
Proxy @(LookupDefT' v w p q))

-- | index a value in an 'Ixed' container and if not found return the given default value

--

-- >>> pl @(LookupDef 4 '[1,2,3,4,5,6] Id) 23

-- Present 5 (JustDef Just)

-- Val 5

--

-- >>> pl @(LookupDef 4 '[1,2,3,4,5,6] Fst) (23,'x')

-- Present 5 (JustDef Just)

-- Val 5

--

-- >>> pl @(LookupDef 99 '[1,2,3,4,5,6] Id) 23

-- Present 23 (JustDef Nothing)

-- Val 23

--

-- >>> pl @(LookupDef 4 Fst (MEmptyT _)) (map SG.Min [1::Int .. 10],'x')

-- Present Min {getMin = 5} (JustDef Just)

-- Val (Min {getMin = 5})

--

-- >>> pl @(LookupDef 999 Fst (MEmptyT _)) (map SG.Min [1::Int .. 10],'x')

-- Present Min {getMin = 9223372036854775807} (JustDef Nothing)

-- Val (Min {getMin = 9223372036854775807})

--

data LookupDef v w p deriving Int -> LookupDef v w p -> ShowS
[LookupDef v w p] -> ShowS
LookupDef v w p -> String
(Int -> LookupDef v w p -> ShowS)
-> (LookupDef v w p -> String)
-> ([LookupDef v w p] -> ShowS)
-> Show (LookupDef v w p)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (v :: k) k (w :: k) k (p :: k).
Int -> LookupDef v w p -> ShowS
forall k (v :: k) k (w :: k) k (p :: k). [LookupDef v w p] -> ShowS
forall k (v :: k) k (w :: k) k (p :: k). LookupDef v w p -> String
showList :: [LookupDef v w p] -> ShowS
$cshowList :: forall k (v :: k) k (w :: k) k (p :: k). [LookupDef v w p] -> ShowS
show :: LookupDef v w p -> String
$cshow :: forall k (v :: k) k (w :: k) k (p :: k). LookupDef v w p -> String
showsPrec :: Int -> LookupDef v w p -> ShowS
$cshowsPrec :: forall k (v :: k) k (w :: k) k (p :: k).
Int -> LookupDef v w p -> ShowS
Show
type LookupDefT v w p = LookupDef' v w p Id

instance P (LookupDefT v w p) x => P (LookupDef v w p) x where
  type PP (LookupDef v w p) x = PP (LookupDefT v w p) x
  eval :: proxy (LookupDef v w p)
-> POpts -> x -> m (TT (PP (LookupDef v w p) x))
eval proxy (LookupDef v w p)
_ = Proxy (LookupDefT v w p)
-> POpts -> x -> m (TT (PP (LookupDefT v w 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 (LookupDefT v w p)
forall k (t :: k). Proxy t
Proxy @(LookupDefT v w p))

-- | index a value in an 'Ixed' container and if not found fail with the given message

data LookupFail' msg v w q deriving Int -> LookupFail' msg v w q -> ShowS
[LookupFail' msg v w q] -> ShowS
LookupFail' msg v w q -> String
(Int -> LookupFail' msg v w q -> ShowS)
-> (LookupFail' msg v w q -> String)
-> ([LookupFail' msg v w q] -> ShowS)
-> Show (LookupFail' msg v w q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (msg :: k) k (v :: k) k (w :: k) k (q :: k).
Int -> LookupFail' msg v w q -> ShowS
forall k (msg :: k) k (v :: k) k (w :: k) k (q :: k).
[LookupFail' msg v w q] -> ShowS
forall k (msg :: k) k (v :: k) k (w :: k) k (q :: k).
LookupFail' msg v w q -> String
showList :: [LookupFail' msg v w q] -> ShowS
$cshowList :: forall k (msg :: k) k (v :: k) k (w :: k) k (q :: k).
[LookupFail' msg v w q] -> ShowS
show :: LookupFail' msg v w q -> String
$cshow :: forall k (msg :: k) k (v :: k) k (w :: k) k (q :: k).
LookupFail' msg v w q -> String
showsPrec :: Int -> LookupFail' msg v w q -> ShowS
$cshowsPrec :: forall k (msg :: k) k (v :: k) k (w :: k) k (q :: k).
Int -> LookupFail' msg v w q -> ShowS
Show
type LookupFailT' msg v w q = JustFail msg (q >> Lookup v w)

instance P (LookupFailT' msg v w q) x => P (LookupFail' msg v w q) x where
  type PP (LookupFail' msg v w q) x = PP (LookupFailT' msg v w q) x
  eval :: proxy (LookupFail' msg v w q)
-> POpts -> x -> m (TT (PP (LookupFail' msg v w q) x))
eval proxy (LookupFail' msg v w q)
_ = Proxy (LookupFailT' msg v w q)
-> POpts -> x -> m (TT (PP (LookupFailT' msg v w 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 (LookupFailT' msg v w q)
forall k (t :: k). Proxy t
Proxy @(LookupFailT' msg v w q))

-- | index a value in an 'Ixed' container and if not found fail with the given message

--

-- >>> pl @(LookupFail "someval" 999 Fst) (map SG.Min [1::Int .. 10],'x')

-- Error someval (JustFail Nothing)

-- Fail "someval"

--

-- >>> pl @(LookupFail (PrintF "char=%c" Snd) 49 Fst) (map SG.Min [1::Int ..10],'x')

-- Error char=x (JustFail Nothing)

-- Fail "char=x"

--

data LookupFail msg v w deriving Int -> LookupFail msg v w -> ShowS
[LookupFail msg v w] -> ShowS
LookupFail msg v w -> String
(Int -> LookupFail msg v w -> ShowS)
-> (LookupFail msg v w -> String)
-> ([LookupFail msg v w] -> ShowS)
-> Show (LookupFail msg v w)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (msg :: k) k (v :: k) k (w :: k).
Int -> LookupFail msg v w -> ShowS
forall k (msg :: k) k (v :: k) k (w :: k).
[LookupFail msg v w] -> ShowS
forall k (msg :: k) k (v :: k) k (w :: k).
LookupFail msg v w -> String
showList :: [LookupFail msg v w] -> ShowS
$cshowList :: forall k (msg :: k) k (v :: k) k (w :: k).
[LookupFail msg v w] -> ShowS
show :: LookupFail msg v w -> String
$cshow :: forall k (msg :: k) k (v :: k) k (w :: k).
LookupFail msg v w -> String
showsPrec :: Int -> LookupFail msg v w -> ShowS
$cshowsPrec :: forall k (msg :: k) k (v :: k) k (w :: k).
Int -> LookupFail msg v w -> ShowS
Show
type LookupFailT msg v w = LookupFail' msg v w Id

instance P (LookupFailT msg v w) x => P (LookupFail msg v w) x where
  type PP (LookupFail msg v w) x = PP (LookupFailT msg v w) x
  eval :: proxy (LookupFail msg v w)
-> POpts -> x -> m (TT (PP (LookupFail msg v w) x))
eval proxy (LookupFail msg v w)
_ = Proxy (LookupFailT msg v w)
-> POpts -> x -> m (TT (PP (LookupFailT msg v w) 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 (LookupFailT msg v w)
forall k (t :: k). Proxy t
Proxy @(LookupFailT msg v w))

-- | similar to 'Data.List.!!' for lists

--

-- >>> pz @(Ix 4 "not found") ["abc","D","eF","","G"]

-- Val "G"

--

-- >>> pz @(Ix 40 "not found") ["abc","D","eF","","G"]

-- Val "not found"

--

-- >>> pl @(Fst >> Dup >> (Ix 1 (FailP "failed5") *** Ix 3 (FailP "failed5")) >> Id) ([10,12,3,5],"ss")

-- Present (12,5) ((>>) (12,5) | {Id (12,5)})

-- Val (12,5)

--

-- >>> pl @(Fst >> Dup >> (Ix 1 (FailP "failed5") *** Ix 3 (FailP "failed5")) >> Fst < Snd) ([10,12,3,5],"ss")

-- False ((>>) False | {12 < 5})

-- Val False

--

-- >>> pl @(Fst >> Dup >> (Ix 1 (FailP "failed5") *** Ix 3 (FailP "failed5")) >> Fst > Snd) ([10,12,3,5],"ss")

-- True ((>>) True | {12 > 5})

-- Val True

--

-- >>> pl @(Snd >> Len &&& Ix 3 (FailP "someval1") >> Fst == Snd) ('x',[1..5])

-- False ((>>) False | {5 == 4})

-- Val False

--

-- >>> pl @(Snd >> Len &&& Ix 3 (FailP "someval2") >> Fst < Snd) ('x',[1..5])

-- False ((>>) False | {5 < 4})

-- Val False

--

-- >>> pl @(Snd >> Len &&& Ix 3 (FailP "someval3") >> Fst > Snd) ('x',[1..5])

-- True ((>>) True | {5 > 4})

-- Val True

--

-- >>> pl @(Map Len >> Ix 3 (FailP "lhs") &&& Ix 0 5 >> Fst == Snd) [[1..4],[4..5]]

-- Error lhs (Ix(3) not found | '(,))

-- Fail "lhs"

--

-- >>> pl @(Map Len >> Ix 0 (FailP "lhs") &&& Ix 1 5 >> Fst == Snd) [[1..4],[4..5]]

-- False ((>>) False | {4 == 2})

-- Val False

--

-- >>> pl @(Map Len >> Ix 1 (FailP "lhs") &&& Ix 3 (FailP "rhs") >> Fst == Snd) [[1..4],[4..5]]

-- Error rhs (Ix(3) not found | '(,))

-- Fail "rhs"

--

-- >>> pl @(Map Len >> Ix 10 (FailP "lhs") &&& Ix 1 (FailP "rhs") >> Fst == Snd) [[1..4],[4..5]]

-- Error lhs (Ix(10) not found | '(,))

-- Fail "lhs"

--

-- >>> pl @(Map Len >> Ix 0 (FailP "lhs") &&& Ix 10 (FailP "rhs") >> Fst == Snd) [[1..4],[4..5]]

-- Error rhs (Ix(10) not found | '(,))

-- Fail "rhs"

--

-- >>> pl @(Map Len >> Ix 10 3 &&& Ix 1 (FailP "rhs") >> Fst == Snd) [[1..4],[4..5]]

-- False ((>>) False | {3 == 2})

-- Val False

--

-- >>> pl @(Map Len >> Ix 3 3 &&& Ix 1 4 >> Fst == Snd) [[1..4],[4..5]]

-- False ((>>) False | {3 == 2})

-- Val False

--

-- >>> pl @(Map Len >> Ix 10 3 &&& Ix 1 4 >> Fst == Snd) [[1..4],[4..5]]

-- False ((>>) False | {3 == 2})

-- Val False

--

-- >>> pl @(Map Len >> Ix 10 5 &&& Ix 1 4 >> Fst == Snd) [[1..4],[4..5]]

-- False ((>>) False | {5 == 2})

-- Val False

--

-- >>> pl @(Map Len >> Ix 10 2 &&& Ix 1 4 >> Fst == Snd) [[1..4],[4..5]]

-- True ((>>) True | {2 == 2})

-- Val True

--

data Ix (n :: Nat) def deriving Int -> Ix n def -> ShowS
[Ix n def] -> ShowS
Ix n def -> String
(Int -> Ix n def -> ShowS)
-> (Ix n def -> String) -> ([Ix n def] -> ShowS) -> Show (Ix n def)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: Nat) k (def :: k). Int -> Ix n def -> ShowS
forall (n :: Nat) k (def :: k). [Ix n def] -> ShowS
forall (n :: Nat) k (def :: k). Ix n def -> String
showList :: [Ix n def] -> ShowS
$cshowList :: forall (n :: Nat) k (def :: k). [Ix n def] -> ShowS
show :: Ix n def -> String
$cshow :: forall (n :: Nat) k (def :: k). Ix n def -> String
showsPrec :: Int -> Ix n def -> ShowS
$cshowsPrec :: forall (n :: Nat) k (def :: k). Int -> Ix n def -> ShowS
Show

instance ( P def (Proxy a)
         , PP def (Proxy a) ~ a
         , KnownNat n
         , Show a
         , [a] ~ x
         ) => P (Ix n def) x where
  type PP (Ix n def) x = ExtractAFromTA x
  eval :: proxy (Ix n def) -> POpts -> x -> m (TT (PP (Ix n def) x))
eval proxy (Ix n def)
_ POpts
opts x
as = do
    let n :: Int
n = forall a. (KnownNat n, Num a) => a
forall (n :: Nat) a. (KnownNat n, Num a) => a
nat @n
        msg0 :: String
msg0 = String
"Ix(" 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
")"
    case x
as x -> Getting (First a) x a -> Maybe a
forall s a. s -> Getting (First a) s a -> Maybe a
^? Index x -> Traversal' x (IxValue x)
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Int
Index x
n of
         Maybe a
Nothing -> do
           let msg1 :: String
msg1 = String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" not found"
           TT a
pp <- Proxy def -> POpts -> Proxy a -> m (TT (PP def (Proxy 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 def
forall k (t :: k). Proxy t
Proxy @def) POpts
opts (Proxy a
forall k (t :: k). Proxy t
Proxy @a)
           TT a -> m (TT a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT a -> m (TT a)) -> TT a -> m (TT a)
forall a b. (a -> b) -> a -> b
$ case Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT a) a
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
Inline POpts
opts String
msg1 TT a
pp [] of
             Left TT a
e -> TT a
e
             Right a
_ -> POpts -> TT a -> String -> [Tree PE] -> TT a
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT a
pp String
msg1 []
         Just a
a -> TT a -> m (TT a)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT a -> m (TT a)) -> TT a -> m (TT a)
forall a b. (a -> b) -> a -> b
$ POpts -> Val a -> String -> [Tree PE] -> TT a
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (a -> Val a
forall a. a -> Val a
Val a
a) (String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> a -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts a
a) []

-- | similar to 'Data.List.!!' for lists with a default error message on failure

data Ix' (n :: Nat) deriving Int -> Ix' n -> ShowS
[Ix' n] -> ShowS
Ix' n -> String
(Int -> Ix' n -> ShowS)
-> (Ix' n -> String) -> ([Ix' n] -> ShowS) -> Show (Ix' n)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: Nat). Int -> Ix' n -> ShowS
forall (n :: Nat). [Ix' n] -> ShowS
forall (n :: Nat). Ix' n -> String
showList :: [Ix' n] -> ShowS
$cshowList :: forall (n :: Nat). [Ix' n] -> ShowS
show :: Ix' n -> String
$cshow :: forall (n :: Nat). Ix' n -> String
showsPrec :: Int -> Ix' n -> ShowS
$cshowsPrec :: forall (n :: Nat). Int -> Ix' n -> ShowS
Show
type IxT' (n :: Nat) = Ix n (FailP "Ix index not found")

instance P (IxT' n) x => P (Ix' n) x where
  type PP (Ix' n) x = PP (IxT' n) x
  eval :: proxy (Ix' n) -> POpts -> x -> m (TT (PP (Ix' n) x))
eval proxy (Ix' n)
_ = Proxy (IxT' n) -> POpts -> x -> m (TT (PP (IxT' n) 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 (IxT' n)
forall k (t :: k). Proxy t
Proxy @(IxT' n))

-- | similar to 'Data.List.!!' leveraging 'Ixed'

--

-- >>> pz @(IxL Id 2 "notfound") ["abc","D","eF","","G"]

-- Val "eF"

--

-- >>> pz @(IxL Id 20 "notfound") ["abc","D","eF","","G"]

-- Val "notfound"

--

-- >>> pl @(IxL Id 1 (C "x")) ("123" :: T.Text)

-- Present '2' (IxL(1) '2' | p="123" | q=1)

-- Val '2'

--

-- >>> pl @(IxL Id 15 (C "x")) ("123" :: T.Text)

-- Present 'x' (IxL(15) index not found)

-- Val 'x'

--

data IxL p q def deriving Int -> IxL p q def -> ShowS
[IxL p q def] -> ShowS
IxL p q def -> String
(Int -> IxL p q def -> ShowS)
-> (IxL p q def -> String)
-> ([IxL p q def] -> ShowS)
-> Show (IxL p q def)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k) k (def :: k).
Int -> IxL p q def -> ShowS
forall k (p :: k) k (q :: k) k (def :: k). [IxL p q def] -> ShowS
forall k (p :: k) k (q :: k) k (def :: k). IxL p q def -> String
showList :: [IxL p q def] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k) k (def :: k). [IxL p q def] -> ShowS
show :: IxL p q def -> String
$cshow :: forall k (p :: k) k (q :: k) k (def :: k). IxL p q def -> String
showsPrec :: Int -> IxL p q def -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k) k (def :: k).
Int -> IxL p q def -> ShowS
Show
-- p is the big value and q is the index and def is the default


instance ( P q a
         , P p a
         , Show (PP p a)
         , Ixed (PP p a)
         , PP q a ~ Index (PP p a)
         , Show (Index (PP p a))
         , Show (IxValue (PP p a))
         , P r (Proxy (IxValue (PP p a)))
         , PP r (Proxy (IxValue (PP p a))) ~ IxValue (PP p a)
         )
   => P (IxL p q r) a where
  type PP (IxL p q r) a = IxValue (PP p a)
  eval :: proxy (IxL p q r) -> POpts -> a -> m (TT (PP (IxL p q r) a))
eval proxy (IxL p q r)
_ POpts
opts a
a = do
    let msg0 :: String
msg0 = String
"IxL"
    Either
  (TT (IxValue (PP p a)))
  (PP p a, Index (PP p a), TT (PP p a), TT (Index (PP p a)))
lr <- Inline
-> String
-> Proxy p
-> Proxy q
-> POpts
-> a
-> [Tree PE]
-> m (Either
        (TT (IxValue (PP p a))) (PP p a, PP q a, TT (PP p a), TT (PP q a)))
forall k1 k2 (p :: k1) a (q :: k2) (m :: Type -> Type)
       (proxy1 :: k1 -> Type) (proxy2 :: k2 -> Type) x.
(P p a, P q a, MonadEval m) =>
Inline
-> String
-> proxy1 p
-> proxy2 q
-> POpts
-> a
-> [Tree PE]
-> m (Either (TT x) (PP p a, PP q a, TT (PP p a), TT (PP q a)))
runPQ Inline
NoInline String
msg0 (Proxy p
forall k (t :: k). Proxy t
Proxy @p) (Proxy q
forall k (t :: k). Proxy t
Proxy @q) POpts
opts a
a []
    case Either
  (TT (IxValue (PP p a)))
  (PP p a, Index (PP p a), TT (PP p a), TT (Index (PP p a)))
lr of
      Left TT (IxValue (PP p a))
e -> TT (IxValue (PP p a)) -> m (TT (IxValue (PP p a)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TT (IxValue (PP p a))
e
      Right (PP p a
p,Index (PP p a)
q,TT (PP p a)
pp,TT (Index (PP p a))
qq) ->
        let msg1 :: String
msg1 = String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Index (PP p a) -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts Index (PP p a)
q String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
        in case PP p a
p PP p a
-> Getting (First (IxValue (PP p a))) (PP p a) (IxValue (PP p a))
-> Maybe (IxValue (PP p a))
forall s a. s -> Getting (First a) s a -> Maybe a
^? Index (PP p a) -> Traversal' (PP p a) (IxValue (PP p a))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index (PP p a)
q of
             Maybe (IxValue (PP p a))
Nothing -> do
                TT (IxValue (PP p a))
rr <- Proxy r
-> POpts
-> Proxy (IxValue (PP p a))
-> m (TT (PP r (Proxy (IxValue (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 r
forall k (t :: k). Proxy t
Proxy @r) POpts
opts (Proxy (IxValue (PP p a))
forall k (t :: k). Proxy t
Proxy @(IxValue (PP p a)))
                TT (IxValue (PP p a)) -> m (TT (IxValue (PP p a)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (IxValue (PP p a)) -> m (TT (IxValue (PP p a))))
-> TT (IxValue (PP p a)) -> m (TT (IxValue (PP p a)))
forall a b. (a -> b) -> a -> b
$ case Inline
-> POpts
-> String
-> TT (IxValue (PP p a))
-> [Tree PE]
-> Either (TT (IxValue (PP p a))) (IxValue (PP p a))
forall a x.
Inline -> POpts -> String -> TT a -> [Tree PE] -> Either (TT x) a
getValueLR Inline
Inline POpts
opts String
msg1 TT (IxValue (PP p a))
rr [TT (PP p a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p a)
pp, TT (Index (PP p a)) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Index (PP p a))
qq] of
                  Left TT (IxValue (PP p a))
e -> TT (IxValue (PP p a))
e
                  Right IxValue (PP p a)
_ -> POpts
-> TT (IxValue (PP p a))
-> String
-> [Tree PE]
-> TT (IxValue (PP p a))
forall a. POpts -> TT a -> String -> [Tree PE] -> TT a
mkNodeCopy POpts
opts TT (IxValue (PP p a))
rr (String
msg1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" index not found") [TT (PP p a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p a)
pp, TT (Index (PP p a)) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Index (PP p a))
qq]
             Just IxValue (PP p a)
ret -> TT (IxValue (PP p a)) -> m (TT (IxValue (PP p a)))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (IxValue (PP p a)) -> m (TT (IxValue (PP p a))))
-> TT (IxValue (PP p a)) -> m (TT (IxValue (PP p a)))
forall a b. (a -> b) -> a -> b
$ POpts
-> Val (IxValue (PP p a))
-> String
-> [Tree PE]
-> TT (IxValue (PP p a))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (IxValue (PP p a) -> Val (IxValue (PP p a))
forall a. a -> Val a
Val IxValue (PP p a)
ret) (POpts -> String -> IxValue (PP p a) -> String -> PP p a -> String
forall a1 a2.
(Show a1, Show a2) =>
POpts -> String -> a1 -> String -> a2 -> String
show3' POpts
opts String
msg1 IxValue (PP p a)
ret String
"p=" PP p a
p String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> String -> Index (PP p a) -> String
forall a. Show a => POpts -> String -> a -> String
showVerbose POpts
opts String
" | q=" Index (PP p a)
q) [TT (PP p a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP p a)
pp, TT (Index (PP p a)) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Index (PP p a))
qq]

-- | similar to 'Data.List.!!' leveraging 'Ixed'

--

-- >>> pz @(Id !! 2) ["abc","D","eF","","G"]

-- Val "eF"

--

-- >>> pz @(Id !! 20) ["abc","D","eF","","G"]

-- Fail "(!!) index not found"

--

-- >>> pz @(Id !! "eF") (M.fromList (flip zip [0..] ["abc","D","eF","","G"]))

-- Val 2

--

-- >>> pl @(Id !! 3) ("asfd" :: T.Text)

-- Present 'd' (IxL(3) 'd' | p="asfd" | q=3)

-- Val 'd'

--

-- >>> pl @(Id !! 4) ("asfd" :: T.Text)

-- Error (!!) index not found (IxL(4))

-- Fail "(!!) index not found"

--

-- >>> pl @(Id !! MEmptyT _) (Just "a")

-- Present "a" (IxL(()) "a" | p=Just "a" | q=())

-- Val "a"

--

-- >>> pl @(Id !! MEmptyT _) (Nothing @()) -- had to add @() to keep this happy: ghci is fine

-- Error (!!) index not found (IxL(()))

-- Fail "(!!) index not found"

--

-- >>> pl @(Id !! 0) ('a','b','c')

-- Present 'a' (IxL(0) 'a' | p=('a','b','c') | q=0)

-- Val 'a'

--

-- >>> pl @(Id !! FailT _ "err") ('a','b','c')

-- Error err (IxL)

-- Fail "err"

--

-- >>> pl @(Id !! "d") (M.fromList $ zip (map (:[]) "abcd") [0 ..])

-- Present 3 (IxL("d") 3 | p=fromList [("a",0),("b",1),("c",2),("d",3)] | q="d")

-- Val 3

--

-- >>> pl @(Id !! C "d") (M.fromList $ zip "abcd" [0 ..])

-- Present 3 (IxL('d') 3 | p=fromList [('a',0),('b',1),('c',2),('d',3)] | q='d')

-- Val 3

--

-- >>> pl @(Id !! C "d") (Set.fromList "abcd")

-- Present () (IxL('d') () | p=fromList "abcd" | q='d')

-- Val ()

--

-- >>> pl @(Id !! HeadFail "failedn" "e") (Set.fromList "abcd")

-- Error (!!) index not found (IxL('e'))

-- Fail "(!!) index not found"

--

-- >>> pl @(Id !! C "d") (M.fromList $ zip "abcd" [0 ..])

-- Present 3 (IxL('d') 3 | p=fromList [('a',0),('b',1),('c',2),('d',3)] | q='d')

-- Val 3

--

-- >>> pl @(Id !! MEmptyT _) (Just 10)

-- Present 10 (IxL(()) 10 | p=Just 10 | q=())

-- Val 10

--

-- >>> pl @(Id !! MEmptyT _) (Nothing @())

-- Error (!!) index not found (IxL(()))

-- Fail "(!!) index not found"

--

-- >>> pl @(Id !! 6) ['a'..'z']

-- Present 'g' (IxL(6) 'g' | p="abcdefghijklmnopqrstuvwxyz" | q=6)

-- Val 'g'

--

-- >>> pl @(Snd !! Fst) (3,"abcde")

-- Present 'd' (IxL(3) 'd' | p="abcde" | q=3)

-- Val 'd'

--

-- >>> pl @(Snd !! Fst) (4,[9,8])

-- Error (!!) index not found (IxL(4))

-- Fail "(!!) index not found"

--

-- >>> pl @(2 &&& Id >> Snd !! Fst) "abcdef"

-- Present 'c' ((>>) 'c' | {IxL(2) 'c' | p="abcdef" | q=2})

-- Val 'c'

--

-- >>> pl @((Len >> Pred) &&& Id >> Snd !! Fst) "abcdef"

-- Present 'f' ((>>) 'f' | {IxL(5) 'f' | p="abcdef" | q=5})

-- Val 'f'

--

-- >>> pl @(Id !! 3) ('a','b','c','d','e')

-- Present 'd' (IxL(3) 'd' | p=('a','b','c','d','e') | q=3)

-- Val 'd'

--

-- >>> pl @(Id !! "s") $ M.fromList [("t",1), ("s", 20), ("s", 99)]

-- Present 99 (IxL("s") 99 | p=fromList [("s",99),("t",1)] | q="s")

-- Val 99

--

-- >>> pl @(Id !! C "d") (M.fromList $ zip "abcd" [0 ..])

-- Present 3 (IxL('d') 3 | p=fromList [('a',0),('b',1),('c',2),('d',3)] | q='d')

-- Val 3

--

-- >>> pl @(Id !! FromString _ "d" &&& (Map' (Snd >> Gt 3 >> Coerce SG.Any) (IToList _) >> MConcat)) (M.fromList $ zip (map T.singleton "abcdefgh") [0 ..])

-- Present (3,Any {getAny = True}) ('(3,Any {getAny = True}))

-- Val (3,Any {getAny = True})

--

-- >>> pl @(Id !! FromString _ "d" &&& (Map' (Snd >> Gt 3 >> Wrap SG.Any Id) (IToList _) >> MConcat >> Unwrap)) (M.fromList $ zip (map T.singleton "abcdefgh") [0 ..])

-- Present (3,True) ('(3,True))

-- Val (3,True)

--

-- >>> pl @(Id !! FromString _ "d") (M.fromList $ zip (map T.singleton "abcd") [0 ..])

-- Present 3 (IxL("d") 3 | p=fromList [("a",0),("b",1),("c",2),("d",3)] | q="d")

-- Val 3

--

-- >>> pl @(Id !! FromString _ "d") (M.fromList $ zip (map T.singleton "abcd") [0 ..])

-- Present 3 (IxL("d") 3 | p=fromList [("a",0),("b",1),("c",2),("d",3)] | q="d")

-- Val 3

--

-- >>> pl @(Id !! 2 !! 0) [[1..5],[10..14],[100..110]]

-- Present 100 (IxL(0) 100 | p=[100,101,102,103,104,105,106,107,108,109,110] | q=0)

-- Val 100

--

-- >>> pl @(Id !! 1 !! 7) [[1..5],[10..14],[100..110]]

-- Error (!!) index not found (IxL(7))

-- Fail "(!!) index not found"

--

-- >>> pl @(Id !! 1) [('x',14),('y',3),('z',5)]

-- Present ('y',3) (IxL(1) ('y',3) | p=[('x',14),('y',3),('z',5)] | q=1)

-- Val ('y',3)

--

-- >>> pl @(Id !! 14) [('x',14),('y',3),('z',5)]

-- Error (!!) index not found (IxL(14))

-- Fail "(!!) index not found"

--

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 BangBangT p q = IxL p q (FailP "(!!) index not found")

instance P (BangBangT p q) a => P (p !! q) a where
  type PP (p !! q) a = PP (BangBangT p q) a
  eval :: proxy (p !! q) -> POpts -> a -> m (TT (PP (p !! q) a))
eval proxy (p !! q)
_ = Proxy (BangBangT p q)
-> POpts -> a -> m (TT (PP (BangBangT p 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 (BangBangT p q)
forall k (t :: k). Proxy t
Proxy @(BangBangT p q))

-- | 'lookup' leveraging 'Ixed': see '!!?'

--

-- >>> pz @(Lookup 2 Id) ["abc","D","eF","","G"]

-- Val (Just "eF")

--

-- >>> pz @(Lookup 20 Id) ["abc","D","eF","","G"]

-- Val Nothing

--

-- >>> pl @(FromList (M.Map _ _) >> Lookup (C "y") Id) [('x',True),('y',False)]

-- Present Just False ((>>) Just False | {Lookup('y') False | q=fromList [('x',True),('y',False)] | p='y'})

-- Val (Just False)

--

-- >>> pl @(FromList (M.Map _ _) >> Lookup (C "z") Id) [('x',True),('y',False)]

-- Present Nothing ((>>) Nothing | {Lookup('z') not found})

-- Val Nothing

--

-- >>> pl @(Lookup 1 Id) [('x',14),('y',3),('z',5)]

-- Present Just ('y',3) (Lookup(1) ('y',3) | q=[('x',14),('y',3),('z',5)] | p=1)

-- Val (Just ('y',3))

--

-- >>> pl @(Lookup 14 Id) [('x',14),('y',3),('z',5)]

-- Present Nothing (Lookup(14) not found)

-- Val Nothing

--

-- >>> pl @(Lookup 3 "abcdef") ()

-- Present Just 'd' (Lookup(3) 'd' | q="abcdef" | p=3)

-- Val (Just 'd')

--

-- >>> pl @(Lookup 4 '[1,2,3,4,5,6]) ()

-- Present Just 5 (Lookup(4) 5 | q=[1,2,3,4,5,6] | p=4)

-- Val (Just 5)

--

data Lookup p q deriving Int -> Lookup p q -> ShowS
[Lookup p q] -> ShowS
Lookup p q -> String
(Int -> Lookup p q -> ShowS)
-> (Lookup p q -> String)
-> ([Lookup p q] -> ShowS)
-> Show (Lookup p q)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (q :: k). Int -> Lookup p q -> ShowS
forall k (p :: k) k (q :: k). [Lookup p q] -> ShowS
forall k (p :: k) k (q :: k). Lookup p q -> String
showList :: [Lookup p q] -> ShowS
$cshowList :: forall k (p :: k) k (q :: k). [Lookup p q] -> ShowS
show :: Lookup p q -> String
$cshow :: forall k (p :: k) k (q :: k). Lookup p q -> String
showsPrec :: Int -> Lookup p q -> ShowS
$cshowsPrec :: forall k (p :: k) k (q :: k). Int -> Lookup p q -> ShowS
Show

instance ( P p a
         , P q a
         , Show (PP q a)
         , Ixed (PP q a)
         , PP p a ~ Index (PP q a)
         , Show (Index (PP q a))
         , Show (IxValue (PP q a))
         )
   => P (Lookup p q) a where
  type PP (Lookup p q) a = Maybe (IxValue (PP q a))
  eval :: proxy (Lookup p q) -> POpts -> a -> m (TT (PP (Lookup p q) a))
eval proxy (Lookup p q)
_ POpts
opts a
a = do
    let msg0 :: String
msg0 = String
"Lookup"
    Either
  (TT (Maybe (IxValue (PP q a))))
  (Index (PP q a), PP q a, TT (Index (PP q a)), TT (PP q a))
lr <- Inline
-> String
-> Proxy p
-> Proxy q
-> POpts
-> a
-> [Tree PE]
-> m (Either
        (TT (Maybe (IxValue (PP q a))))
        (PP p a, PP q a, TT (PP p a), TT (PP q a)))
forall k1 k2 (p :: k1) a (q :: k2) (m :: Type -> Type)
       (proxy1 :: k1 -> Type) (proxy2 :: k2 -> Type) x.
(P p a, P q a, MonadEval m) =>
Inline
-> String
-> proxy1 p
-> proxy2 q
-> POpts
-> a
-> [Tree PE]
-> m (Either (TT x) (PP p a, PP q a, TT (PP p a), TT (PP q a)))
runPQ Inline
NoInline String
msg0 (Proxy p
forall k (t :: k). Proxy t
Proxy @p) (Proxy q
forall k (t :: k). Proxy t
Proxy @q) POpts
opts a
a []
    TT (Maybe (IxValue (PP q a))) -> m (TT (Maybe (IxValue (PP q a))))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TT (Maybe (IxValue (PP q a)))
 -> m (TT (Maybe (IxValue (PP q a)))))
-> TT (Maybe (IxValue (PP q a)))
-> m (TT (Maybe (IxValue (PP q a))))
forall a b. (a -> b) -> a -> b
$ case Either
  (TT (Maybe (IxValue (PP q a))))
  (Index (PP q a), PP q a, TT (Index (PP q a)), TT (PP q a))
lr of
      Left TT (Maybe (IxValue (PP q a)))
e -> TT (Maybe (IxValue (PP q a)))
e
      Right (Index (PP q a)
p,PP q a
q,TT (Index (PP q a))
pp,TT (PP q a)
qq) ->
        let msg1 :: String
msg1 = String
msg0 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> Index (PP q a) -> String
forall a. Show a => POpts -> a -> String
showL POpts
opts Index (PP q a)
p String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
            hhs :: [Tree PE]
hhs = [TT (Index (PP q a)) -> Tree PE
forall a. TT a -> Tree PE
hh TT (Index (PP q a))
pp, TT (PP q a) -> Tree PE
forall a. TT a -> Tree PE
hh TT (PP q a)
qq]
        in case PP q a
q PP q a
-> Getting (First (IxValue (PP q a))) (PP q a) (IxValue (PP q a))
-> Maybe (IxValue (PP q a))
forall s a. s -> Getting (First a) s a -> Maybe a
^? Index (PP q a) -> Traversal' (PP q a) (IxValue (PP q a))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index (PP q a)
p of
             Maybe (IxValue (PP q a))
Nothing -> POpts
-> Val (Maybe (IxValue (PP q a)))
-> String
-> [Tree PE]
-> TT (Maybe (IxValue (PP q a)))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (Maybe (IxValue (PP q a)) -> Val (Maybe (IxValue (PP q a)))
forall a. a -> Val a
Val Maybe (IxValue (PP q a))
forall a. Maybe a
Nothing) (String
msg1 String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" not found") [Tree PE]
hhs
             Just IxValue (PP q a)
ret -> POpts
-> Val (Maybe (IxValue (PP q a)))
-> String
-> [Tree PE]
-> TT (Maybe (IxValue (PP q a)))
forall a. POpts -> Val a -> String -> [Tree PE] -> TT a
mkNode POpts
opts (Maybe (IxValue (PP q a)) -> Val (Maybe (IxValue (PP q a)))
forall a. a -> Val a
Val (IxValue (PP q a) -> Maybe (IxValue (PP q a))
forall a. a -> Maybe a
Just IxValue (PP q a)
ret)) (POpts -> String -> IxValue (PP q a) -> String -> PP q a -> String
forall a1 a2.
(Show a1, Show a2) =>
POpts -> String -> a1 -> String -> a2 -> String
show3' POpts
opts String
msg1 IxValue (PP q a)
ret String
"q=" PP q a
q String -> ShowS
forall a. Semigroup a => a -> a -> a
<> POpts -> String -> Index (PP q a) -> String
forall a. Show a => POpts -> String -> a -> String
showVerbose POpts
opts String
" | p=" Index (PP q a)
p) [Tree PE]
hhs

-- | type operator version of 'Lookup'

--

-- >>> pl @((Id !!? C "d") > MkJust 99 || Length Id <= 3) (M.fromList $ zip "abcd" [1..])

-- False (False || False | (Just 4 > Just 99) || (4 <= 3))

-- Val False

--

-- >>> pz @((Id !!? C "d") > MkJust 2 || Length Id <= 3) (M.fromList $ zip "abcd" [1..])

-- Val True

--

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 BangBangQT p q = Lookup q p

instance P (BangBangQT p q) a => P (p !!? q) a where
  type PP (p !!? q) a = PP (BangBangQT p q) a
  eval :: proxy (p !!? q) -> POpts -> a -> m (TT (PP (p !!? q) a))
eval proxy (p !!? q)
_ = Proxy (BangBangQT p q)
-> POpts -> a -> m (TT (PP (BangBangQT p 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 (BangBangQT p q)
forall k (t :: k). Proxy t
Proxy @(BangBangQT p q))