module Plutarch.Extra.Function (
pconst,
pidentity,
papply,
pon,
pbuiltinUncurry,
pflip,
(#.*),
(#.**),
(#.***),
) where
pconst ::
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s (a :--> b :--> a)
pconst :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s (a :--> (b :--> a))
pconst = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. a -> b -> a
const
pidentity ::
forall (a :: S -> Type) (s :: S).
Term s (a :--> a)
pidentity :: forall (a :: S -> Type) (s :: S). Term s (a :--> a)
pidentity = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a. a -> a
id
papply ::
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s ((a :--> b) :--> a :--> b)
papply :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s ((a :--> b) :--> (a :--> b))
papply = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> b)
f Term s a
x -> Term s (a :--> b)
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x
pon ::
forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
Term s ((b :--> b :--> c) :--> (a :--> b) :--> a :--> a :--> c)
pon :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
Term
s ((b :--> (b :--> c)) :--> ((a :--> b) :--> (a :--> (a :--> c))))
pon = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (b :--> (b :--> c))
f Term s (a :--> b)
g Term s a
x Term s a
y ->
let a :: Term s b
a = Term s (a :--> b)
g forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x
b :: Term s b
b = Term s (a :--> b)
g forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
y
in Term s (b :--> (b :--> c))
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
a forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
b
pbuiltinUncurry ::
forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
( PIsData a
, PIsData b
) =>
(Term s a -> Term s b -> Term s c) ->
Term s (PBuiltinPair (PAsData a) (PAsData b)) ->
Term s c
pbuiltinUncurry :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
(PIsData a, PIsData b) =>
(Term s a -> Term s b -> Term s c)
-> Term s (PBuiltinPair (PAsData a) (PAsData b)) -> Term s c
pbuiltinUncurry Term s a -> Term s b -> Term s c
f Term s (PBuiltinPair (PAsData a) (PAsData b))
p =
let p1 :: Term s a
p1 = forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData a) (PAsData b))
p
p2 :: Term s b
p2 = forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData a) (PAsData b))
p
in Term s a -> Term s b -> Term s c
f Term s a
p1 Term s b
p2
pflip ::
forall
(a :: S -> Type)
(b :: S -> Type)
(c :: S -> Type)
(s :: S).
Term
s
((a :--> b :--> c) :--> b :--> a :--> c)
pflip :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
Term s ((a :--> (b :--> c)) :--> (b :--> (a :--> c)))
pflip = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> (b :--> c))
f Term s b
y Term s a
x -> Term s (a :--> (b :--> c))
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
y
infixr 8 #.*
(#.*) ::
forall
(d :: S -> Type)
(c :: S -> Type)
(b :: S -> Type)
(a :: S -> Type)
(s :: S).
Term s (c :--> d) ->
Term s (a :--> b :--> c) ->
Term s (a :--> b :--> d)
#.* :: forall (d :: S -> Type) (c :: S -> Type) (b :: S -> Type)
(a :: S -> Type) (s :: S).
Term s (c :--> d)
-> Term s (a :--> (b :--> c)) -> Term s (a :--> (b :--> d))
(#.*) Term s (c :--> d)
f Term s (a :--> (b :--> c))
g = forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s b
y -> Term s (c :--> d)
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (a :--> (b :--> c))
g forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
y
infixr 8 #.**
(#.**) ::
forall
(e :: S -> Type)
(d :: S -> Type)
(c :: S -> Type)
(b :: S -> Type)
(a :: S -> Type)
(s :: S).
Term s (d :--> e) ->
Term s (a :--> b :--> c :--> d) ->
Term s (a :--> b :--> c :--> e)
#.** :: forall (e :: S -> Type) (d :: S -> Type) (c :: S -> Type)
(b :: S -> Type) (a :: S -> Type) (s :: S).
Term s (d :--> e)
-> Term s (a :--> (b :--> (c :--> d)))
-> Term s (a :--> (b :--> (c :--> e)))
(#.**) Term s (d :--> e)
f Term s (a :--> (b :--> (c :--> d)))
g = forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s b
y Term s c
z -> Term s (d :--> e)
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (a :--> (b :--> (c :--> d)))
g forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
y forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s c
z
infixr 8 #.***
(#.***) ::
forall
(f :: S -> Type)
(e :: S -> Type)
(d :: S -> Type)
(c :: S -> Type)
(b :: S -> Type)
(a :: S -> Type)
(s :: S).
Term s (e :--> f) ->
Term s (a :--> b :--> c :--> d :--> e) ->
Term s (a :--> b :--> c :--> d :--> f)
#.*** :: forall (f :: S -> Type) (e :: S -> Type) (d :: S -> Type)
(c :: S -> Type) (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s (e :--> f)
-> Term s (a :--> (b :--> (c :--> (d :--> e))))
-> Term s (a :--> (b :--> (c :--> (d :--> f))))
(#.***) Term s (e :--> f)
f Term s (a :--> (b :--> (c :--> (d :--> e))))
g = forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s b
y Term s c
z Term s d
a -> Term s (e :--> f)
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (a :--> (b :--> (c :--> (d :--> e))))
g forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
y forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s c
z forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s d
a