predicate-typed-0.7.4.0: Predicates, Refinement types and Dsl

Safe HaskellNone
LanguageHaskell2010

Predicate.Data.Proxy

Contents

Description

promoted functions for proxies

Synopsis

create a proxy from a type

data ProxyT #

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
Instances
Show ProxyT # 
Instance details

Defined in Predicate.Data.Proxy

Show x => P ProxyT x # 
Instance details

Defined in Predicate.Data.Proxy

Associated Types

type PP ProxyT x :: Type #

Methods

eval :: MonadEval m => proxy ProxyT -> POpts -> x -> m (TT (PP ProxyT x)) #

type PP ProxyT x # 
Instance details

Defined in Predicate.Data.Proxy

type PP ProxyT x = Proxy x

data Proxy1T #

makes a proxy from a one parameter container

>>> pz @(Pop1' (Proxy EmptyT) Proxy1T 123) Nothing
Val Nothing
>>> pz @(Pop1' (Proxy EmptyT) Proxy1T 123) (Just 10)
Val Nothing
>>> pz @((Id $$ ()) >> Pop1' (Proxy EmptyT) Proxy1T 123) Just
Val Nothing
Instances
Show Proxy1T # 
Instance details

Defined in Predicate.Data.Proxy

P Proxy1T x # 
Instance details

Defined in Predicate.Data.Proxy

Associated Types

type PP Proxy1T x :: Type #

Methods

eval :: MonadEval m => proxy Proxy1T -> POpts -> x -> m (TT (PP Proxy1T x)) #

type PP Proxy1T x # 
Instance details

Defined in Predicate.Data.Proxy

data Proxy2T #

makes a proxy from a two parameter container

>>> pz @(Pop1' (Proxy EmptyT) Proxy2T 123) (Left "ASf")
Val (Left "")
>>> pz @(Pop1' (Proxy EmptyT) Proxy2T 123) (Right 1)
Val (Left "")
>>> pz @((Id $$ "asdf") >> Pop1' (Proxy EmptyT) Proxy2T 123) Left
Val (Left "")
>>> pz @((Id $$ "asdf") >> Pop1' (Proxy EmptyT) Proxy2T 123) Right
Val (Left "")
>>> pz @(Pop1' (Proxy EmptyT) ((Id $$ "ss") >> Proxy2T) 123) Right
Val (Left "")
>>> pz @(Pop1' (Proxy EmptyT) ((Id $$ "ss") >> Proxy2T) 123) Left
Val (Left "")
Instances
Show Proxy2T # 
Instance details

Defined in Predicate.Data.Proxy

P Proxy2T x # 
Instance details

Defined in Predicate.Data.Proxy

Associated Types

type PP Proxy2T x :: Type #

Methods

eval :: MonadEval m => proxy Proxy2T -> POpts -> x -> m (TT (PP Proxy2T x)) #

type PP Proxy2T x # 
Instance details

Defined in Predicate.Data.Proxy

type PP Proxy2T x

data Proxify p #

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
Instances
PP p x ~ proxy z => P (Proxify p :: Type) x # 
Instance details

Defined in Predicate.Data.Proxy

Associated Types

type PP (Proxify p) x :: Type #

Methods

eval :: MonadEval m => proxy (Proxify p) -> POpts -> x -> m (TT (PP (Proxify p) x)) #

Show (Proxify p) # 
Instance details

Defined in Predicate.Data.Proxy

Methods

showsPrec :: Int -> Proxify p -> ShowS #

show :: Proxify p -> String #

showList :: [Proxify p] -> ShowS #

type PP (Proxify p :: Type) x # 
Instance details

Defined in Predicate.Data.Proxy

type PP (Proxify p :: Type) x

simple proxy application

data Pop0 p q #

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"
Instances
(P q x, PP p x ~ proxy z, P z (PP q x)) => P (Pop0 p q :: Type) x # 
Instance details

Defined in Predicate.Data.Proxy

Associated Types

type PP (Pop0 p q) x :: Type #

Methods

eval :: MonadEval m => proxy (Pop0 p q) -> POpts -> x -> m (TT (PP (Pop0 p q) x)) #

Show (Pop0 p q) # 
Instance details

Defined in Predicate.Data.Proxy

Methods

showsPrec :: Int -> Pop0 p q -> ShowS #

show :: Pop0 p q -> String #

showList :: [Pop0 p q] -> ShowS #

type PP (Pop0 p q :: Type) x # 
Instance details

Defined in Predicate.Data.Proxy

type PP (Pop0 p q :: Type) x

needs kind signatures on p

data Pop1 p q r #

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)
Instances
(P r x, PP p x ~ Proxy z, P (z q) (PP r x)) => P (Pop1 p q r :: Type) x # 
Instance details

Defined in Predicate.Data.Proxy

Associated Types

type PP (Pop1 p q r) x :: Type #

Methods

eval :: MonadEval m => proxy (Pop1 p q r) -> POpts -> x -> m (TT (PP (Pop1 p q r) x)) #

Show (Pop1 p q r) # 
Instance details

Defined in Predicate.Data.Proxy

Methods

showsPrec :: Int -> Pop1 p q r -> ShowS #

show :: Pop1 p q r -> String #

showList :: [Pop1 p q r] -> ShowS #

type PP (Pop1 p q r :: Type) x # 
Instance details

Defined in Predicate.Data.Proxy

type PP (Pop1 p q r :: Type) x

data Pop2 p q r s #

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})
Instances
(P s x, PP p x ~ Proxy z, P (z q r) (PP s x)) => P (Pop2 p q r s :: Type) x # 
Instance details

Defined in Predicate.Data.Proxy

Associated Types

type PP (Pop2 p q r s) x :: Type #

Methods

eval :: MonadEval m => proxy (Pop2 p q r s) -> POpts -> x -> m (TT (PP (Pop2 p q r s) x)) #

Show (Pop2 p q r s) # 
Instance details

Defined in Predicate.Data.Proxy

Methods

showsPrec :: Int -> Pop2 p q r s -> ShowS #

show :: Pop2 p q r s -> String #

showList :: [Pop2 p q r s] -> ShowS #

type PP (Pop2 p q r s :: Type) x # 
Instance details

Defined in Predicate.Data.Proxy

type PP (Pop2 p q r s :: Type) x

data Pop1' p q 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'
Instances
(P r x, PP p x ~ Proxy z, PP q x ~ Proxy w, P (z w) (PP r x)) => P (Pop1' p q r :: Type) x # 
Instance details

Defined in Predicate.Data.Proxy

Associated Types

type PP (Pop1' p q r) x :: Type #

Methods

eval :: MonadEval m => proxy (Pop1' p q r) -> POpts -> x -> m (TT (PP (Pop1' p q r) x)) #

Show (Pop1' p q r) # 
Instance details

Defined in Predicate.Data.Proxy

Methods

showsPrec :: Int -> Pop1' p q r -> ShowS #

show :: Pop1' p q r -> String #

showList :: [Pop1' p q r] -> ShowS #

type PP (Pop1' p q r :: Type) x # 
Instance details

Defined in Predicate.Data.Proxy

type PP (Pop1' p q r :: Type) x

data Pop2' p q r 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)
Instances
(P s x, PP p x ~ Proxy z, PP q x ~ Proxy w, PP r x ~ Proxy v, P (z w v) (PP s x)) => P (Pop2' p q r s :: Type) x # 
Instance details

Defined in Predicate.Data.Proxy

Associated Types

type PP (Pop2' p q r s) x :: Type #

Methods

eval :: MonadEval m => proxy (Pop2' p q r s) -> POpts -> x -> m (TT (PP (Pop2' p q r s) x)) #

Show (Pop2' p q r s) # 
Instance details

Defined in Predicate.Data.Proxy

Methods

showsPrec :: Int -> Pop2' p q r s -> ShowS #

show :: Pop2' p q r s -> String #

showList :: [Pop2' p q r s] -> ShowS #

type PP (Pop2' p q r s :: Type) x # 
Instance details

Defined in Predicate.Data.Proxy

type PP (Pop2' p q r s :: Type) x

data PApp p q #

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)
Instances
(PP p x ~ Proxy z, PP q x ~ Proxy w) => P (PApp p q :: Type) x # 
Instance details

Defined in Predicate.Data.Proxy

Associated Types

type PP (PApp p q) x :: Type #

Methods

eval :: MonadEval m => proxy (PApp p q) -> POpts -> x -> m (TT (PP (PApp p q) x)) #

Show (PApp p q) # 
Instance details

Defined in Predicate.Data.Proxy

Methods

showsPrec :: Int -> PApp p q -> ShowS #

show :: PApp p q -> String #

showList :: [PApp p q] -> ShowS #

type PP (PApp p q :: Type) x # 
Instance details

Defined in Predicate.Data.Proxy

type PP (PApp p q :: Type) x

data PApp2 p q r #

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)
Instances
(PP p x ~ Proxy z, PP q x ~ Proxy w, PP r x ~ Proxy v) => P (PApp2 p q r :: Type) x # 
Instance details

Defined in Predicate.Data.Proxy

Associated Types

type PP (PApp2 p q r) x :: Type #

Methods

eval :: MonadEval m => proxy (PApp2 p q r) -> POpts -> x -> m (TT (PP (PApp2 p q r) x)) #

Show (PApp2 p q r) # 
Instance details

Defined in Predicate.Data.Proxy

Methods

showsPrec :: Int -> PApp2 p q r -> ShowS #

show :: PApp2 p q r -> String #

showList :: [PApp2 p q r] -> ShowS #

type PP (PApp2 p q r :: Type) x # 
Instance details

Defined in Predicate.Data.Proxy

type PP (PApp2 p q r :: Type) x