module Plutarch.Extra.List (preverse, pcheckSorted) where
import Plutarch.Prelude
preverse :: (PIsListLike l a) => Term s (l a :--> l a)
preverse :: forall (l :: PType -> PType) (a :: PType) (s :: S).
PIsListLike l a =>
Term s (l a :--> l a)
preverse =
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
forall (list :: PType -> PType) (a :: PType) (s :: S) (b :: PType).
PIsListLike list a =>
Term s ((b :--> (a :--> b)) :--> (b :--> (list a :--> b)))
pfoldl forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam (\Term s (l a)
ys Term s a
y -> forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
y forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
ys) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil
pcheckSorted :: (PIsListLike l a, POrd a) => Term s (l a :--> PBool)
pcheckSorted :: forall (l :: PType -> PType) (a :: PType) (s :: S).
(PIsListLike l a, POrd a) =>
Term s (l a :--> PBool)
pcheckSorted =
forall (s :: S) (a :: PType) (b :: PType).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (l a :--> PBool)
self Term s (l a)
xs ->
forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList
( \Term s a
x1 Term s (l a)
xs ->
forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList
(\Term s a
x2 Term s (l a)
_ -> Term s a
x1 forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s a
x2 forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#&& (Term s (l a :--> PBool)
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
xs))
(forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PTrue)
Term s (l a)
xs
)
(forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PTrue)
Term s (l a)
xs