-- | Scott-encoded lists and ListLike typeclass
module Plutarch.List (
  PList (..),
  PListLike (..),
  PIsListLike,
  pconvertLists,
  pshowList,

  -- * Comparison
  plistEquals,

  -- * Query
  pelem,
  plength,
  ptryIndex,
  pdrop,
  pfind,
  pelemAt,
  (#!!),

  -- * Construction
  psingleton,

  -- * Deconstruction
  puncons,
  ptryUncons,

  -- * Combine
  pconcat,
  pzipWith,
  pzipWith',
  pzip,

  -- * Traversals
  pmap,
  pfilter,

  -- * Catamorphisms
  precList,
  pfoldr,
  pfoldr',
  pfoldrLazy,
  pfoldl,
  pfoldl',

  -- * Special Folds
  pall,
  pany,

  -- * Modification
  preverse,

  -- * Predicates
  pcheckSorted,
) where

import Data.Kind (Constraint, Type)
import GHC.Generics (Generic)
import Numeric.Natural (Natural)
import Plutarch.Builtin.Bool (PBool (PFalse, PTrue), pif, (#&&), (#||))
import Plutarch.Integer (PInteger)
import Plutarch.Internal.Eq (PEq ((#==)))
import Plutarch.Internal.Lift (pconstant)
import Plutarch.Internal.Ord (POrd, (#<), (#<=))
import Plutarch.Internal.Other (pfix)
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.PlutusType (
  DerivePlutusType (DPTStrat),
  PlutusType,
  pcon,
  pmatch,
 )
import Plutarch.Internal.ScottEncoding (
  PlutusTypeScott,
 )
import Plutarch.Internal.Term (
  PDelayed,
  S,
  Term,
  pdelay,
  perror,
  phoistAcyclic,
  plet,
  (#),
  (#$),
  (:-->),
 )
import Plutarch.Maybe (PMaybe (PJust, PNothing))
import Plutarch.Pair (PPair (PPair))
import Plutarch.Show (PShow (pshow'), pshow)
import Plutarch.String (PString)
import Plutarch.Trace (ptraceInfoError)

data PList (a :: S -> Type) (s :: S)
  = PSCons (Term s a) (Term s (PList a))
  | PSNil
  deriving stock ((forall x. PList a s -> Rep (PList a s) x)
-> (forall x. Rep (PList a s) x -> PList a s)
-> Generic (PList a s)
forall x. Rep (PList a s) x -> PList a s
forall x. PList a s -> Rep (PList a s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: S -> Type) (s :: S) x. Rep (PList a s) x -> PList a s
forall (a :: S -> Type) (s :: S) x. PList a s -> Rep (PList a s) x
$cfrom :: forall (a :: S -> Type) (s :: S) x. PList a s -> Rep (PList a s) x
from :: forall x. PList a s -> Rep (PList a s) x
$cto :: forall (a :: S -> Type) (s :: S) x. Rep (PList a s) x -> PList a s
to :: forall x. Rep (PList a s) x -> PList a s
Generic)
  deriving anyclass ((forall (s :: S). PList a s -> Term s (PInner (PList a)))
-> (forall (s :: S) (b :: S -> Type).
    Term s (PInner (PList a)) -> (PList a s -> Term s b) -> Term s b)
-> PlutusType (PList a)
forall (s :: S). PList a s -> Term s (PInner (PList a))
forall (s :: S) (b :: S -> Type).
Term s (PInner (PList a)) -> (PList a s -> Term s b) -> Term s b
forall (a :: S -> Type).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: S -> Type).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
forall (a :: S -> Type) (s :: S).
PList a s -> Term s (PInner (PList a))
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
Term s (PInner (PList a)) -> (PList a s -> Term s b) -> Term s b
$cpcon' :: forall (a :: S -> Type) (s :: S).
PList a s -> Term s (PInner (PList a))
pcon' :: forall (s :: S). PList a s -> Term s (PInner (PList a))
$cpmatch' :: forall (a :: S -> Type) (s :: S) (b :: S -> Type).
Term s (PInner (PList a)) -> (PList a s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PList a)) -> (PList a s -> Term s b) -> Term s b
PlutusType)

instance DerivePlutusType (PList a) where
  type DPTStrat _ = PlutusTypeScott

instance PShow a => PShow (PList a) where
  pshow' :: forall (s :: S). Bool -> Term s (PList a) -> Term s PString
pshow' Bool
_ Term s (PList a)
x = forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PShow a, PIsListLike list a) =>
Term s (list a :--> PString)
pshowList @PList @a Term s (PList a :--> PString) -> Term s (PList a) -> Term s PString
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PList a)
x

pshowList :: forall list a s. (PShow a, PIsListLike list a) => Term s (list a :--> PString)
pshowList :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PShow a, PIsListLike list a) =>
Term s (list a :--> PString)
pshowList =
  ClosedTerm (list a :--> PString) -> Term s (list a :--> PString)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> PString) -> Term s (list a :--> PString))
-> ClosedTerm (list a :--> PString) -> Term s (list a :--> PString)
forall a b. (a -> b) -> a -> b
$
    (Term s (list a) -> Term s PString) -> Term s (list a :--> PString)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PString) -> Term s (c :--> PString)
plam ((Term s (list a) -> Term s PString)
 -> Term s (list a :--> PString))
-> (Term s (list a) -> Term s PString)
-> Term s (list a :--> PString)
forall a b. (a -> b) -> a -> b
$ \Term s (list a)
list ->
      Term s PString
"[" Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PShow a, PIsListLike list a) =>
Term s (list a :--> PString)
pshowList' @list @a Term s (list a :--> PString) -> Term s (list a) -> Term s PString
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
list Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s PString
"]"

pshowList' :: forall list a s. (PShow a, PIsListLike list a) => Term s (list a :--> PString)
pshowList' :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PShow a, PIsListLike list a) =>
Term s (list a :--> PString)
pshowList' =
  ClosedTerm (list a :--> PString) -> Term s (list a :--> PString)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> PString) -> Term s (list a :--> PString))
-> ClosedTerm (list a :--> PString) -> Term s (list a :--> PString)
forall a b. (a -> b) -> a -> b
$
    (Term s (list a :--> PString)
 -> Term s a -> Term s (list a) -> Term s PString)
-> (Term s (list a :--> PString) -> Term s PString)
-> Term s (list a :--> PString)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
PIsListLike list a =>
(Term s (list a :--> r) -> Term s a -> Term s (list a) -> Term s r)
-> (Term s (list a :--> r) -> Term s r) -> Term s (list a :--> r)
precList
      ( \Term s (list a :--> PString)
self Term s a
x Term s (list a)
xs ->
          (Term s a -> Term s (list a) -> Term s PString)
-> Term s PString -> Term s (list a) -> Term s PString
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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
_ Term s (list a)
_ -> Term s a -> Term s PString
forall (a :: S -> Type) (s :: S).
PShow a =>
Term s a -> Term s PString
pshow Term s a
x Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s PString
", " Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s (list a :--> PString)
self Term s (list a :--> PString) -> Term s (list a) -> Term s PString
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs)
            (Term s a -> Term s PString
forall (a :: S -> Type) (s :: S).
PShow a =>
Term s a -> Term s PString
pshow Term s a
x)
            Term s (list a)
xs
      )
      (Term s PString -> Term s (list a :--> PString) -> Term s PString
forall a b. a -> b -> a
const Term s PString
"")

instance PEq a => PEq (PList a) where
  #== :: forall (s :: S).
Term s (PList a) -> Term s (PList a) -> Term s PBool
(#==) Term s (PList a)
xs Term s (PList a)
ys = Term s (PList a :--> (PList a :--> PBool))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PIsListLike list a, PEq a) =>
Term s (list a :--> (list a :--> PBool))
plistEquals Term s (PList a :--> (PList a :--> PBool))
-> Term s (PList a) -> Term s (PList a :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PList a)
xs Term s (PList a :--> PBool) -> Term s (PList a) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PList a)
ys

--------------------------------------------------------------------------------

-- | 'PIsListLike list a' constraints 'list' be a 'PListLike' with valid element type, 'a'.
type PIsListLike list a = (PListLike list, PElemConstraint list a)

-- | Plutarch types that behave like lists.
class PListLike (list :: (S -> Type) -> S -> Type) where
  type PElemConstraint list (a :: S -> Type) :: Constraint

  -- | Canonical eliminator for list-likes.
  pelimList ::
    PElemConstraint list a =>
    (Term s a -> Term s (list a) -> Term s r) ->
    Term s r ->
    Term s (list a) ->
    Term s r

  -- | Cons an element onto an existing list.
  pcons :: PElemConstraint list a => Term s (a :--> list a :--> list a)

  -- | The empty list
  pnil :: PElemConstraint list a => Term s (list a)

  -- | Return the first element of a list. Partial, throws an error upon encountering an empty list.
  phead :: PElemConstraint list a => Term s (list a :--> a)
  phead = ClosedTerm (list a :--> a) -> Term s (list a :--> a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> a) -> Term s (list a :--> a))
-> ClosedTerm (list a :--> a) -> Term s (list a :--> a)
forall a b. (a -> b) -> a -> b
$ (Term s (list a) -> Term s a) -> Term s (list a :--> a)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s a) -> Term s (c :--> a)
plam ((Term s (list a) -> Term s a) -> Term s (list a :--> a))
-> (Term s (list a) -> Term s a) -> Term s (list a :--> a)
forall a b. (a -> b) -> a -> b
$ (Term s a -> Term s (list a) -> Term s a)
-> Term s a -> Term s (list a) -> Term s a
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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 -> Term s (list a) -> Term s a
forall a b. a -> b -> a
const Term s a
forall (s :: S) (a :: S -> Type). Term s a
perror

  -- | Take the tail of a list, meaning drop its head. Partial, throws an error upon encountering an empty list.
  ptail :: PElemConstraint list a => Term s (list a :--> list a)
  ptail = ClosedTerm (list a :--> list a) -> Term s (list a :--> list a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> list a) -> Term s (list a :--> list a))
-> ClosedTerm (list a :--> list a) -> Term s (list a :--> list a)
forall a b. (a -> b) -> a -> b
$ (Term s (list a) -> Term s (list a)) -> Term s (list a :--> list a)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (list a)) -> Term s (c :--> list a)
plam ((Term s (list a) -> Term s (list a))
 -> Term s (list a :--> list a))
-> (Term s (list a) -> Term s (list a))
-> Term s (list a :--> list a)
forall a b. (a -> b) -> a -> b
$ (Term s a -> Term s (list a) -> Term s (list a))
-> Term s (list a) -> Term s (list a) -> Term s (list a)
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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
_ Term s (list a)
xs -> Term s (list a)
xs) Term s (list a)
forall (s :: S) (a :: S -> Type). Term s a
perror

  -- | / O(1) /. Check if a list is empty
  pnull :: PElemConstraint list a => Term s (list a :--> PBool)
  pnull = ClosedTerm (list a :--> PBool) -> Term s (list a :--> PBool)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> PBool) -> Term s (list a :--> PBool))
-> ClosedTerm (list a :--> PBool) -> Term s (list a :--> PBool)
forall a b. (a -> b) -> a -> b
$ (Term s (list a) -> Term s PBool) -> Term s (list a :--> PBool)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PBool) -> Term s (c :--> PBool)
plam ((Term s (list a) -> Term s PBool) -> Term s (list a :--> PBool))
-> (Term s (list a) -> Term s PBool) -> Term s (list a :--> PBool)
forall a b. (a -> b) -> a -> b
$ (Term s a -> Term s (list a) -> Term s PBool)
-> Term s PBool -> Term s (list a) -> Term s PBool
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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
_ Term s (list a)
_ -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False) (Term s PBool -> Term s (list a) -> Term s PBool)
-> Term s PBool -> Term s (list a) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True

instance PListLike PList where
  type PElemConstraint PList _ = ()
  pelimList :: forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint PList a =>
(Term s a -> Term s (PList a) -> Term s r)
-> Term s r -> Term s (PList a) -> Term s r
pelimList Term s a -> Term s (PList a) -> Term s r
match_cons Term s r
match_nil Term s (PList a)
ls = Term s (PList a) -> (PList a s -> Term s r) -> Term s r
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PList a)
ls ((PList a s -> Term s r) -> Term s r)
-> (PList a s -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ \case
    PSCons Term s a
x Term s (PList a)
xs -> Term s a -> Term s (PList a) -> Term s r
match_cons Term s a
x Term s (PList a)
xs
    PList a s
PSNil -> Term s r
match_nil
  pcons :: forall (a :: S -> Type) (s :: S).
PElemConstraint PList a =>
Term s (a :--> (PList a :--> PList a))
pcons = ClosedTerm (a :--> (PList a :--> PList a))
-> Term s (a :--> (PList a :--> PList a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (a :--> (PList a :--> PList a))
 -> Term s (a :--> (PList a :--> PList a)))
-> ClosedTerm (a :--> (PList a :--> PList a))
-> Term s (a :--> (PList a :--> PList a))
forall a b. (a -> b) -> a -> b
$ (Term s a -> Term s (PList a) -> Term s (PList a))
-> Term s (a :--> (PList a :--> PList a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PList a) -> Term s (PList a))
-> Term s (c :--> (PList a :--> PList a))
plam ((Term s a -> Term s (PList a) -> Term s (PList a))
 -> Term s (a :--> (PList a :--> PList a)))
-> (Term s a -> Term s (PList a) -> Term s (PList a))
-> Term s (a :--> (PList a :--> PList a))
forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s (PList a)
xs -> PList a s -> Term s (PList a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (Term s a -> Term s (PList a) -> PList a s
forall (a :: S -> Type) (s :: S).
Term s a -> Term s (PList a) -> PList a s
PSCons Term s a
x Term s (PList a)
xs)
  pnil :: forall (a :: S -> Type) (s :: S).
PElemConstraint PList a =>
Term s (PList a)
pnil = PList a s -> Term s (PList a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PList a s
forall (a :: S -> Type) (s :: S). PList a s
PSNil

-- | / O(n) /. Convert from any ListLike to any ListLike, provided both lists' element constraints are met.
pconvertLists ::
  forall f g a s.
  (PIsListLike f a, PIsListLike g a) =>
  Term s (f a :--> g a)
pconvertLists :: forall (f :: (S -> Type) -> S -> Type)
       (g :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
(PIsListLike f a, PIsListLike g a) =>
Term s (f a :--> g a)
pconvertLists = ClosedTerm (f a :--> g a) -> Term s (f a :--> g a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (f a :--> g a) -> Term s (f a :--> g a))
-> ClosedTerm (f a :--> g a) -> Term s (f a :--> g a)
forall a b. (a -> b) -> a -> b
$
  Term s (((f a :--> g a) :--> (f a :--> g a)) :--> (f a :--> g a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term s (((f a :--> g a) :--> (f a :--> g a)) :--> (f a :--> g a))
-> Term s ((f a :--> g a) :--> (f a :--> g a))
-> Term s (f a :--> g a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s (f a :--> g a) -> Term s (f a) -> Term s (g a))
-> Term s ((f a :--> g a) :--> (f a :--> g a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (f a) -> Term s (g a))
-> Term s (c :--> (f a :--> g a))
plam ((Term s (f a :--> g a) -> Term s (f a) -> Term s (g a))
 -> Term s ((f a :--> g a) :--> (f a :--> g a)))
-> (Term s (f a :--> g a) -> Term s (f a) -> Term s (g a))
-> Term s ((f a :--> g a) :--> (f a :--> g a))
forall a b. (a -> b) -> a -> b
$ \Term s (f a :--> g a)
self ->
    (Term s a -> Term s (f a) -> Term s (g a))
-> Term s (g a) -> Term s (f a) -> Term s (g a)
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint f a =>
(Term s a -> Term s (f a) -> Term s r)
-> Term s r -> Term s (f a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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
x Term s (f a)
xs -> Term s (a :--> (g a :--> g a))
forall (a :: S -> Type) (s :: S).
PElemConstraint g a =>
Term s (a :--> (g a :--> g a))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons Term s (a :--> (g a :--> g a)) -> Term s a -> Term s (g a :--> g a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x Term s (g a :--> g a) -> Term s (g a) -> Term s (g a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (f a :--> g a)
self Term s (f a :--> g a) -> Term s (f a) -> Term s (g a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (f a)
xs)
      Term s (g a)
forall (a :: S -> Type) (s :: S).
PElemConstraint g a =>
Term s (g a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil

-- | Extract head and tail of the list, throws error if list is empty.
ptryUncons ::
  PIsListLike list a =>
  Term s (list a :--> PPair a (list a))
ptryUncons :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Term s (list a :--> PPair a (list a))
ptryUncons =
  ClosedTerm (list a :--> PPair a (list a))
-> Term s (list a :--> PPair a (list a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> PPair a (list a))
 -> Term s (list a :--> PPair a (list a)))
-> ClosedTerm (list a :--> PPair a (list a))
-> Term s (list a :--> PPair a (list a))
forall a b. (a -> b) -> a -> b
$
    (Term s (list a) -> Term s (PPair a (list a)))
-> Term s (list a :--> PPair a (list a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PPair a (list a)))
-> Term s (c :--> PPair a (list a))
plam ((Term s (list a) -> Term s (PPair a (list a)))
 -> Term s (list a :--> PPair a (list a)))
-> (Term s (list a) -> Term s (PPair a (list a)))
-> Term s (list a :--> PPair a (list a))
forall a b. (a -> b) -> a -> b
$
      (Term s a -> Term s (list a) -> Term s (PPair a (list a)))
-> Term s (PPair a (list a))
-> Term s (list a)
-> Term s (PPair a (list a))
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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
x -> PPair a (list a) s -> Term s (PPair a (list a))
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PPair a (list a) s -> Term s (PPair a (list a)))
-> (Term s (list a) -> PPair a (list a) s)
-> Term s (list a)
-> Term s (PPair a (list a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s a -> Term s (list a) -> PPair a (list a) s
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair Term s a
x) Term s (PPair a (list a))
forall (s :: S) (a :: S -> Type). Term s a
perror

-- | Extract head and tail of the list, if list is not empty.
puncons ::
  PIsListLike list a =>
  Term s (list a :--> PMaybe (PPair a (list a)))
puncons :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Term s (list a :--> PMaybe (PPair a (list a)))
puncons =
  ClosedTerm (list a :--> PMaybe (PPair a (list a)))
-> Term s (list a :--> PMaybe (PPair a (list a)))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> PMaybe (PPair a (list a)))
 -> Term s (list a :--> PMaybe (PPair a (list a))))
-> ClosedTerm (list a :--> PMaybe (PPair a (list a)))
-> Term s (list a :--> PMaybe (PPair a (list a)))
forall a b. (a -> b) -> a -> b
$
    (Term s (list a) -> Term s (PMaybe (PPair a (list a))))
-> Term s (list a :--> PMaybe (PPair a (list a)))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PMaybe (PPair a (list a))))
-> Term s (c :--> PMaybe (PPair a (list a)))
plam ((Term s (list a) -> Term s (PMaybe (PPair a (list a))))
 -> Term s (list a :--> PMaybe (PPair a (list a))))
-> (Term s (list a) -> Term s (PMaybe (PPair a (list a))))
-> Term s (list a :--> PMaybe (PPair a (list a)))
forall a b. (a -> b) -> a -> b
$
      (Term s a -> Term s (list a) -> Term s (PMaybe (PPair a (list a))))
-> Term s (PMaybe (PPair a (list a)))
-> Term s (list a)
-> Term s (PMaybe (PPair a (list a)))
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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
x -> PMaybe (PPair a (list a)) s -> Term s (PMaybe (PPair a (list a)))
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PMaybe (PPair a (list a)) s -> Term s (PMaybe (PPair a (list a))))
-> (Term s (list a) -> PMaybe (PPair a (list a)) s)
-> Term s (list a)
-> Term s (PMaybe (PPair a (list a)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PPair a (list a)) -> PMaybe (PPair a (list a)) s
forall (a :: S -> Type) (s :: S). Term s a -> PMaybe a s
PJust (Term s (PPair a (list a)) -> PMaybe (PPair a (list a)) s)
-> (Term s (list a) -> Term s (PPair a (list a)))
-> Term s (list a)
-> PMaybe (PPair a (list a)) s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PPair a (list a) s -> Term s (PPair a (list a))
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PPair a (list a) s -> Term s (PPair a (list a)))
-> (Term s (list a) -> PPair a (list a) s)
-> Term s (list a)
-> Term s (PPair a (list a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s a -> Term s (list a) -> PPair a (list a) s
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair Term s a
x) (PMaybe (PPair a (list a)) s -> Term s (PMaybe (PPair a (list a)))
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PMaybe (PPair a (list a)) s
forall (a :: S -> Type) (s :: S). PMaybe a s
PNothing)

-- | Like 'pelimList', but with a fixpoint recursion hatch.
precList ::
  PIsListLike list a =>
  (Term s (list a :--> r) -> Term s a -> Term s (list a) -> Term s r) ->
  (Term s (list a :--> r) -> Term s r) ->
  Term s (list a :--> r)
precList :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
PIsListLike list a =>
(Term s (list a :--> r) -> Term s a -> Term s (list a) -> Term s r)
-> (Term s (list a :--> r) -> Term s r) -> Term s (list a :--> r)
precList Term s (list a :--> r) -> Term s a -> Term s (list a) -> Term s r
mcons Term s (list a :--> r) -> Term s r
mnil =
  Term
  s (((list a :--> r) :--> (list a :--> r)) :--> (list a :--> r))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
  s (((list a :--> r) :--> (list a :--> r)) :--> (list a :--> r))
-> Term s ((list a :--> r) :--> (list a :--> r))
-> Term s (list a :--> r)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s (list a :--> r) -> Term s (list a) -> Term s r)
-> Term s ((list a :--> r) :--> (list a :--> r))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (list a) -> Term s r)
-> Term s (c :--> (list a :--> r))
plam ((Term s (list a :--> r) -> Term s (list a) -> Term s r)
 -> Term s ((list a :--> r) :--> (list a :--> r)))
-> (Term s (list a :--> r) -> Term s (list a) -> Term s r)
-> Term s ((list a :--> r) :--> (list a :--> r))
forall a b. (a -> b) -> a -> b
$ \Term s (list a :--> r)
self ->
    (Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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 (list a :--> r) -> Term s a -> Term s (list a) -> Term s r
mcons Term s (list a :--> r)
self)
      (Term s (list a :--> r) -> Term s r
mnil Term s (list a :--> r)
self)

--------------------------------------------------------------------------------
-- Construction

-- | / O(1) /. Create a singleton list from an element
psingleton :: PIsListLike list a => Term s (a :--> list a)
psingleton :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Term s (a :--> list a)
psingleton = ClosedTerm (a :--> list a) -> Term s (a :--> list a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (a :--> list a) -> Term s (a :--> list a))
-> ClosedTerm (a :--> list a) -> Term s (a :--> list a)
forall a b. (a -> b) -> a -> b
$ (Term s a -> Term s (list a)) -> Term s (a :--> list a)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (list a)) -> Term s (c :--> list a)
plam ((Term s a -> Term s (list a)) -> Term s (a :--> list a))
-> (Term s a -> Term s (list a)) -> Term s (a :--> list a)
forall a b. (a -> b) -> a -> b
$ \Term s a
x -> Term s (a :--> (list a :--> list a))
forall (a :: S -> Type) (s :: S).
PElemConstraint list a =>
Term s (a :--> (list a :--> list a))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons Term s (a :--> (list a :--> list a))
-> Term s a -> Term s (list a :--> list a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x Term s (list a :--> list a) -> Term s (list a) -> Term s (list a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
forall (a :: S -> Type) (s :: S).
PElemConstraint list a =>
Term s (list a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil

--------------------------------------------------------------------------------
-- Querying

-- | / O(n) /. Check if element is in the list
pelem :: (PIsListLike list a, PEq a) => Term s (a :--> list a :--> PBool)
pelem :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PIsListLike list a, PEq a) =>
Term s (a :--> (list a :--> PBool))
pelem =
  ClosedTerm (a :--> (list a :--> PBool))
-> Term s (a :--> (list a :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (a :--> (list a :--> PBool))
 -> Term s (a :--> (list a :--> PBool)))
-> ClosedTerm (a :--> (list a :--> PBool))
-> Term s (a :--> (list a :--> PBool))
forall a b. (a -> b) -> a -> b
$
    (Term s a -> Term s (list a :--> PBool))
-> Term s (a :--> (list a :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (list a :--> PBool))
-> Term s (c :--> (list a :--> PBool))
plam ((Term s a -> Term s (list a :--> PBool))
 -> Term s (a :--> (list a :--> PBool)))
-> (Term s a -> Term s (list a :--> PBool))
-> Term s (a :--> (list a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s a
needle ->
      (Term s (list a :--> PBool)
 -> Term s a -> Term s (list a) -> Term s PBool)
-> (Term s (list a :--> PBool) -> Term s PBool)
-> Term s (list a :--> PBool)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
PIsListLike list a =>
(Term s (list a :--> r) -> Term s a -> Term s (list a) -> Term s r)
-> (Term s (list a :--> r) -> Term s r) -> Term s (list a :--> r)
precList
        (\Term s (list a :--> PBool)
self Term s a
x Term s (list a)
xs -> Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s a
x Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s a
needle) (PBool s -> Term s PBool
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PTrue) (Term s (list a :--> PBool)
self Term s (list a :--> PBool) -> Term s (list a) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs))
        (\Term s (list a :--> PBool)
_self -> PBool s -> Term s PBool
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PFalse)

-- | / O(n) /. Count the number of elements in the list
plength :: PIsListLike list a => Term s (list a :--> PInteger)
plength :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Term s (list a :--> PInteger)
plength =
  ClosedTerm (list a :--> PInteger) -> Term s (list a :--> PInteger)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> PInteger)
 -> Term s (list a :--> PInteger))
-> ClosedTerm (list a :--> PInteger)
-> Term s (list a :--> PInteger)
forall a b. (a -> b) -> a -> b
$
    let go :: PIsListLike list a => Term s (PInteger :--> list a :--> PInteger)
        go :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Term s (PInteger :--> (list a :--> PInteger))
go = Term
  s
  (((PInteger :--> (list a :--> PInteger))
    :--> (PInteger :--> (list a :--> PInteger)))
   :--> (PInteger :--> (list a :--> PInteger)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
  s
  (((PInteger :--> (list a :--> PInteger))
    :--> (PInteger :--> (list a :--> PInteger)))
   :--> (PInteger :--> (list a :--> PInteger)))
-> Term
     s
     ((PInteger :--> (list a :--> PInteger))
      :--> (PInteger :--> (list a :--> PInteger)))
-> Term s (PInteger :--> (list a :--> PInteger))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s (PInteger :--> (list a :--> PInteger))
 -> Term s PInteger -> Term s (list a) -> Term s PInteger)
-> Term
     s
     ((PInteger :--> (list a :--> PInteger))
      :--> (PInteger :--> (list a :--> PInteger)))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PInteger -> Term s (list a) -> Term s PInteger)
-> Term s (c :--> (PInteger :--> (list a :--> PInteger)))
plam ((Term s (PInteger :--> (list a :--> PInteger))
  -> Term s PInteger -> Term s (list a) -> Term s PInteger)
 -> Term
      s
      ((PInteger :--> (list a :--> PInteger))
       :--> (PInteger :--> (list a :--> PInteger))))
-> (Term s (PInteger :--> (list a :--> PInteger))
    -> Term s PInteger -> Term s (list a) -> Term s PInteger)
-> Term
     s
     ((PInteger :--> (list a :--> PInteger))
      :--> (PInteger :--> (list a :--> PInteger)))
forall a b. (a -> b) -> a -> b
$ \Term s (PInteger :--> (list a :--> PInteger))
self Term s PInteger
n -> (Term s a -> Term s (list a) -> Term s PInteger)
-> Term s PInteger -> Term s (list a) -> Term s PInteger
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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
_ Term s (list a)
xs -> Term s (PInteger :--> (list a :--> PInteger))
self Term s (PInteger :--> (list a :--> PInteger))
-> Term s PInteger -> Term s (list a :--> PInteger)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PInteger
n Term s PInteger -> Term s PInteger -> Term s PInteger
forall a. Num a => a -> a -> a
+ Term s PInteger
1) Term s (list a :--> PInteger) -> Term s (list a) -> Term s PInteger
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs) Term s PInteger
n
     in Term s (PInteger :--> (list a :--> PInteger))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Term s (PInteger :--> (list a :--> PInteger))
go Term s (PInteger :--> (list a :--> PInteger))
-> Term s PInteger -> Term s (list a :--> PInteger)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
0

-- | Index a BuiltinList, throwing an error if the index is out of bounds.
ptryIndex :: PIsListLike list a => Natural -> Term s (list a) -> Term s a
ptryIndex :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Natural -> Term s (list a) -> Term s a
ptryIndex Natural
n Term s (list a)
xs = Term s (list a :--> a)
forall (a :: S -> Type) (s :: S).
PElemConstraint list a =>
Term s (list a :--> a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead Term s (list a :--> a) -> Term s (list a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Natural -> Term s (list a) -> Term s (list a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Natural -> Term s (list a) -> Term s (list a)
pdrop Natural
n Term s (list a)
xs

{- |
  Drop the first n fields of a List.

  The term will be statically generated as
  repeated applications of 'ptail', which will be more
  efficient in many circumstances.
-}
pdrop :: PIsListLike list a => Natural -> Term s (list a) -> Term s (list a)
pdrop :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Natural -> Term s (list a) -> Term s (list a)
pdrop Natural
n Term s (list a)
xs = Natural -> forall (s :: S). Term s (list a :--> list a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type).
PIsListLike list a =>
Natural -> forall (s :: S). Term s (list a :--> list a)
pdrop' Natural
n Term s (list a :--> list a) -> Term s (list a) -> Term s (list a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs
  where
    pdrop' :: PIsListLike list a => Natural -> (forall (s :: S). Term s (list a :--> list a))
    pdrop' :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type).
PIsListLike list a =>
Natural -> forall (s :: S). Term s (list a :--> list a)
pdrop' Natural
0 = (Term s (list a) -> Term s (list a)) -> Term s (list a :--> list a)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (list a)) -> Term s (c :--> list a)
plam Term s (list a) -> Term s (list a)
forall a. a -> a
id
    pdrop' Natural
1 = Term s (list a :--> list a)
forall (a :: S -> Type) (s :: S).
PElemConstraint list a =>
Term s (list a :--> list a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail
    pdrop' Natural
n' = ClosedTerm (list a :--> list a) -> Term s (list a :--> list a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> list a) -> Term s (list a :--> list a))
-> ClosedTerm (list a :--> list a) -> Term s (list a :--> list a)
forall a b. (a -> b) -> a -> b
$ (Term s (list a) -> Term s (list a)) -> Term s (list a :--> list a)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (list a)) -> Term s (c :--> list a)
plam ((Term s (list a) -> Term s (list a))
 -> Term s (list a :--> list a))
-> (Term s (list a) -> Term s (list a))
-> Term s (list a :--> list a)
forall a b. (a -> b) -> a -> b
$ \Term s (list a)
x -> Term s (list a :--> list a)
forall (a :: S -> Type) (s :: S).
PElemConstraint list a =>
Term s (list a :--> list a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail Term s (list a :--> list a) -> Term s (list a) -> Term s (list a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Natural -> ClosedTerm (list a :--> list a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type).
PIsListLike list a =>
Natural -> forall (s :: S). Term s (list a :--> list a)
pdrop' (Natural
n' Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1) Term s (list a :--> list a) -> Term s (list a) -> Term s (list a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
x

--------------------------------------------------------------------------------

-- | / O(n) /. Fold on a list left-associatively.
pfoldl :: PIsListLike list a => Term s ((b :--> a :--> b) :--> b :--> list a :--> b)
pfoldl :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (b :: S -> Type).
PIsListLike list a =>
Term s ((b :--> (a :--> b)) :--> (b :--> (list a :--> b)))
pfoldl = ClosedTerm ((b :--> (a :--> b)) :--> (b :--> (list a :--> b)))
-> Term s ((b :--> (a :--> b)) :--> (b :--> (list a :--> b)))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm ((b :--> (a :--> b)) :--> (b :--> (list a :--> b)))
 -> Term s ((b :--> (a :--> b)) :--> (b :--> (list a :--> b))))
-> ClosedTerm ((b :--> (a :--> b)) :--> (b :--> (list a :--> b)))
-> Term s ((b :--> (a :--> b)) :--> (b :--> (list a :--> b)))
forall a b. (a -> b) -> a -> b
$
  (Term s (b :--> (a :--> b)) -> Term s (b :--> (list a :--> b)))
-> Term s ((b :--> (a :--> b)) :--> (b :--> (list 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)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (b :--> (list a :--> b)))
-> Term s (c :--> (b :--> (list a :--> b)))
plam ((Term s (b :--> (a :--> b)) -> Term s (b :--> (list a :--> b)))
 -> Term s ((b :--> (a :--> b)) :--> (b :--> (list a :--> b))))
-> (Term s (b :--> (a :--> b)) -> Term s (b :--> (list a :--> b)))
-> Term s ((b :--> (a :--> b)) :--> (b :--> (list a :--> b)))
forall a b. (a -> b) -> a -> b
$ \Term s (b :--> (a :--> b))
f ->
    Term
  s
  (((b :--> (list a :--> b)) :--> (b :--> (list a :--> b)))
   :--> (b :--> (list a :--> b)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
  s
  (((b :--> (list a :--> b)) :--> (b :--> (list a :--> b)))
   :--> (b :--> (list a :--> b)))
-> Term s ((b :--> (list a :--> b)) :--> (b :--> (list a :--> b)))
-> Term s (b :--> (list a :--> b))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s (b :--> (list a :--> b))
 -> Term s b -> Term s (list a) -> Term s b)
-> Term s ((b :--> (list a :--> b)) :--> (b :--> (list 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)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s b -> Term s (list a) -> Term s b)
-> Term s (c :--> (b :--> (list a :--> b)))
plam ((Term s (b :--> (list a :--> b))
  -> Term s b -> Term s (list a) -> Term s b)
 -> Term s ((b :--> (list a :--> b)) :--> (b :--> (list a :--> b))))
-> (Term s (b :--> (list a :--> b))
    -> Term s b -> Term s (list a) -> Term s b)
-> Term s ((b :--> (list a :--> b)) :--> (b :--> (list a :--> b)))
forall a b. (a -> b) -> a -> b
$ \Term s (b :--> (list a :--> b))
self Term s b
z ->
      (Term s a -> Term s (list a) -> Term s b)
-> Term s b -> Term s (list a) -> Term s b
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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
x Term s (list a)
xs -> Term s (b :--> (list a :--> b))
self Term s (b :--> (list a :--> b))
-> Term s b -> Term s (list a :--> b)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (b :--> (a :--> b))
f Term s (b :--> (a :--> b)) -> Term s b -> Term s (a :--> b)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
z Term s (a :--> b) -> Term s a -> Term s b
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x) Term s (list a :--> b) -> Term s (list a) -> Term s b
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs)
        Term s b
z

-- | The same as 'pfoldl', but with Haskell-level reduction function.
pfoldl' :: PIsListLike list a => (forall s. Term s b -> Term s a -> Term s b) -> Term s (b :--> list a :--> b)
pfoldl' :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
PIsListLike list a =>
(forall (s :: S). Term s b -> Term s a -> Term s b)
-> Term s (b :--> (list a :--> b))
pfoldl' forall (s :: S). Term s b -> Term s a -> Term s b
f = ClosedTerm (b :--> (list a :--> b))
-> Term s (b :--> (list a :--> b))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (b :--> (list a :--> b))
 -> Term s (b :--> (list a :--> b)))
-> ClosedTerm (b :--> (list a :--> b))
-> Term s (b :--> (list a :--> b))
forall a b. (a -> b) -> a -> b
$
  Term
  s
  (((b :--> (list a :--> b)) :--> (b :--> (list a :--> b)))
   :--> (b :--> (list a :--> b)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
  s
  (((b :--> (list a :--> b)) :--> (b :--> (list a :--> b)))
   :--> (b :--> (list a :--> b)))
-> Term s ((b :--> (list a :--> b)) :--> (b :--> (list a :--> b)))
-> Term s (b :--> (list a :--> b))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s (b :--> (list a :--> b))
 -> Term s b -> Term s (list a) -> Term s b)
-> Term s ((b :--> (list a :--> b)) :--> (b :--> (list 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)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s b -> Term s (list a) -> Term s b)
-> Term s (c :--> (b :--> (list a :--> b)))
plam ((Term s (b :--> (list a :--> b))
  -> Term s b -> Term s (list a) -> Term s b)
 -> Term s ((b :--> (list a :--> b)) :--> (b :--> (list a :--> b))))
-> (Term s (b :--> (list a :--> b))
    -> Term s b -> Term s (list a) -> Term s b)
-> Term s ((b :--> (list a :--> b)) :--> (b :--> (list a :--> b)))
forall a b. (a -> b) -> a -> b
$ \Term s (b :--> (list a :--> b))
self Term s b
z ->
    (Term s a -> Term s (list a) -> Term s b)
-> Term s b -> Term s (list a) -> Term s b
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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
x Term s (list a)
xs -> Term s (b :--> (list a :--> b))
self Term s (b :--> (list a :--> b))
-> Term s b -> Term s (list a :--> b)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s b -> Term s a -> Term s b
forall (s :: S). Term s b -> Term s a -> Term s b
f Term s b
z Term s a
x Term s (list a :--> b) -> Term s (list a) -> Term s b
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs)
      Term s b
z

-- | / O(n) /. Fold on a list right-associatively.
pfoldr :: PIsListLike list a => Term s ((a :--> b :--> b) :--> b :--> list a :--> b)
pfoldr :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (b :: S -> Type).
PIsListLike list a =>
Term s ((a :--> (b :--> b)) :--> (b :--> (list a :--> b)))
pfoldr = ClosedTerm ((a :--> (b :--> b)) :--> (b :--> (list a :--> b)))
-> Term s ((a :--> (b :--> b)) :--> (b :--> (list a :--> b)))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm ((a :--> (b :--> b)) :--> (b :--> (list a :--> b)))
 -> Term s ((a :--> (b :--> b)) :--> (b :--> (list a :--> b))))
-> ClosedTerm ((a :--> (b :--> b)) :--> (b :--> (list a :--> b)))
-> Term s ((a :--> (b :--> b)) :--> (b :--> (list a :--> b)))
forall a b. (a -> b) -> a -> b
$
  (Term s (a :--> (b :--> b)) -> Term s b -> Term s (list a :--> b))
-> Term s ((a :--> (b :--> b)) :--> (b :--> (list 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)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s b -> Term s (list a :--> b))
-> Term s (c :--> (b :--> (list a :--> b)))
plam ((Term s (a :--> (b :--> b)) -> Term s b -> Term s (list a :--> b))
 -> Term s ((a :--> (b :--> b)) :--> (b :--> (list a :--> b))))
-> (Term s (a :--> (b :--> b))
    -> Term s b -> Term s (list a :--> b))
-> Term s ((a :--> (b :--> b)) :--> (b :--> (list a :--> b)))
forall a b. (a -> b) -> a -> b
$ \Term s (a :--> (b :--> b))
f Term s b
z ->
    (Term s (list a :--> b) -> Term s a -> Term s (list a) -> Term s b)
-> (Term s (list a :--> b) -> Term s b) -> Term s (list a :--> b)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
PIsListLike list a =>
(Term s (list a :--> r) -> Term s a -> Term s (list a) -> Term s r)
-> (Term s (list a :--> r) -> Term s r) -> Term s (list a :--> r)
precList
      (\Term s (list a :--> b)
self Term s a
x Term s (list a)
xs -> Term s (a :--> (b :--> b))
f Term s (a :--> (b :--> b)) -> Term s a -> Term s (b :--> b)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x Term s (b :--> b) -> Term s b -> Term s b
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (list a :--> b)
self Term s (list a :--> b) -> Term s (list a) -> Term s b
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs))
      (Term s b -> Term s (list a :--> b) -> Term s b
forall a b. a -> b -> a
const Term s b
z)

-- | The same as 'pfoldr'', but with Haskell-level reduction function.
pfoldr' :: PIsListLike list a => (forall s. Term s a -> Term s b -> Term s b) -> Term s (b :--> list a :--> b)
pfoldr' :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
PIsListLike list a =>
(forall (s :: S). Term s a -> Term s b -> Term s b)
-> Term s (b :--> (list a :--> b))
pfoldr' forall (s :: S). Term s a -> Term s b -> Term s b
f = ClosedTerm (b :--> (list a :--> b))
-> Term s (b :--> (list a :--> b))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (b :--> (list a :--> b))
 -> Term s (b :--> (list a :--> b)))
-> ClosedTerm (b :--> (list a :--> b))
-> Term s (b :--> (list a :--> b))
forall a b. (a -> b) -> a -> b
$
  (Term s b -> Term s (list a :--> b))
-> Term s (b :--> (list 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)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (list a :--> b))
-> Term s (c :--> (list a :--> b))
plam ((Term s b -> Term s (list a :--> b))
 -> Term s (b :--> (list a :--> b)))
-> (Term s b -> Term s (list a :--> b))
-> Term s (b :--> (list a :--> b))
forall a b. (a -> b) -> a -> b
$ \Term s b
z ->
    (Term s (list a :--> b) -> Term s a -> Term s (list a) -> Term s b)
-> (Term s (list a :--> b) -> Term s b) -> Term s (list a :--> b)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
PIsListLike list a =>
(Term s (list a :--> r) -> Term s a -> Term s (list a) -> Term s r)
-> (Term s (list a :--> r) -> Term s r) -> Term s (list a :--> r)
precList
      (\Term s (list a :--> b)
self Term s a
x Term s (list a)
xs -> Term s a -> Term s b -> Term s b
forall (s :: S). Term s a -> Term s b -> Term s b
f Term s a
x (Term s (list a :--> b)
self Term s (list a :--> b) -> Term s (list a) -> Term s b
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs))
      (Term s b -> Term s (list a :--> b) -> Term s b
forall a b. a -> b -> a
const Term s b
z)

{- | / O(n) /. Fold on a list right-associatively, with opportunity for short circuting.

May short circuit when given reducer function is lazy in its second argument.
-}
pfoldrLazy :: PIsListLike list a => Term s ((a :--> PDelayed b :--> b) :--> b :--> list a :--> b)
pfoldrLazy :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (b :: S -> Type).
PIsListLike list a =>
Term s ((a :--> (PDelayed b :--> b)) :--> (b :--> (list a :--> b)))
pfoldrLazy = ClosedTerm
  ((a :--> (PDelayed b :--> b)) :--> (b :--> (list a :--> b)))
-> Term
     s ((a :--> (PDelayed b :--> b)) :--> (b :--> (list a :--> b)))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm
   ((a :--> (PDelayed b :--> b)) :--> (b :--> (list a :--> b)))
 -> Term
      s ((a :--> (PDelayed b :--> b)) :--> (b :--> (list a :--> b))))
-> ClosedTerm
     ((a :--> (PDelayed b :--> b)) :--> (b :--> (list a :--> b)))
-> Term
     s ((a :--> (PDelayed b :--> b)) :--> (b :--> (list a :--> b)))
forall a b. (a -> b) -> a -> b
$
  (Term s (a :--> (PDelayed b :--> b))
 -> Term s b -> Term s (list a :--> b))
-> Term
     s ((a :--> (PDelayed b :--> b)) :--> (b :--> (list 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)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s b -> Term s (list a :--> b))
-> Term s (c :--> (b :--> (list a :--> b)))
plam ((Term s (a :--> (PDelayed b :--> b))
  -> Term s b -> Term s (list a :--> b))
 -> Term
      s ((a :--> (PDelayed b :--> b)) :--> (b :--> (list a :--> b))))
-> (Term s (a :--> (PDelayed b :--> b))
    -> Term s b -> Term s (list a :--> b))
-> Term
     s ((a :--> (PDelayed b :--> b)) :--> (b :--> (list a :--> b)))
forall a b. (a -> b) -> a -> b
$ \Term s (a :--> (PDelayed b :--> b))
f Term s b
z ->
    (Term s (list a :--> b) -> Term s a -> Term s (list a) -> Term s b)
-> (Term s (list a :--> b) -> Term s b) -> Term s (list a :--> b)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
PIsListLike list a =>
(Term s (list a :--> r) -> Term s a -> Term s (list a) -> Term s r)
-> (Term s (list a :--> r) -> Term s r) -> Term s (list a :--> r)
precList
      (\Term s (list a :--> b)
self Term s a
x Term s (list a)
xs -> Term s (a :--> (PDelayed b :--> b))
f Term s (a :--> (PDelayed b :--> b))
-> Term s a -> Term s (PDelayed b :--> b)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x Term s (PDelayed b :--> b) -> Term s (PDelayed b) -> Term s b
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s b -> Term s (PDelayed b)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PDelayed a)
pdelay (Term s (list a :--> b)
self Term s (list a :--> b) -> Term s (list a) -> Term s b
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs))
      (Term s b -> Term s (list a :--> b) -> Term s b
forall a b. a -> b -> a
const Term s b
z)

-- | / O(n) /. Check that predicate holds for all elements in a list.
pall :: PIsListLike list a => Term s ((a :--> PBool) :--> list a :--> PBool)
pall :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> PBool))
pall = ClosedTerm ((a :--> PBool) :--> (list a :--> PBool))
-> Term s ((a :--> PBool) :--> (list a :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm ((a :--> PBool) :--> (list a :--> PBool))
 -> Term s ((a :--> PBool) :--> (list a :--> PBool)))
-> ClosedTerm ((a :--> PBool) :--> (list a :--> PBool))
-> Term s ((a :--> PBool) :--> (list a :--> PBool))
forall a b. (a -> b) -> a -> b
$
  (Term s (a :--> PBool) -> Term s (list a :--> PBool))
-> Term s ((a :--> PBool) :--> (list a :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (list a :--> PBool))
-> Term s (c :--> (list a :--> PBool))
plam ((Term s (a :--> PBool) -> Term s (list a :--> PBool))
 -> Term s ((a :--> PBool) :--> (list a :--> PBool)))
-> (Term s (a :--> PBool) -> Term s (list a :--> PBool))
-> Term s ((a :--> PBool) :--> (list a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s (a :--> PBool)
predicate ->
    (Term s (list a :--> PBool)
 -> Term s a -> Term s (list a) -> Term s PBool)
-> (Term s (list a :--> PBool) -> Term s PBool)
-> Term s (list a :--> PBool)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
PIsListLike list a =>
(Term s (list a :--> r) -> Term s a -> Term s (list a) -> Term s r)
-> (Term s (list a :--> r) -> Term s r) -> Term s (list a :--> r)
precList (\Term s (list a :--> PBool)
self Term s a
x Term s (list a)
xs -> Term s (a :--> PBool)
predicate Term s (a :--> PBool) -> Term s a -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#&& Term s (list a :--> PBool)
self Term s (list a :--> PBool) -> Term s (list a) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs) (Term s PBool -> Term s (list a :--> PBool) -> Term s PBool
forall a b. a -> b -> a
const (Term s PBool -> Term s (list a :--> PBool) -> Term s PBool)
-> Term s PBool -> Term s (list a :--> PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True)

-- | / O(n) /. Check that predicate holds for any element in a list.
pany :: PIsListLike list a => Term s ((a :--> PBool) :--> list a :--> PBool)
pany :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> PBool))
pany = ClosedTerm ((a :--> PBool) :--> (list a :--> PBool))
-> Term s ((a :--> PBool) :--> (list a :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm ((a :--> PBool) :--> (list a :--> PBool))
 -> Term s ((a :--> PBool) :--> (list a :--> PBool)))
-> ClosedTerm ((a :--> PBool) :--> (list a :--> PBool))
-> Term s ((a :--> PBool) :--> (list a :--> PBool))
forall a b. (a -> b) -> a -> b
$
  (Term s (a :--> PBool) -> Term s (list a :--> PBool))
-> Term s ((a :--> PBool) :--> (list a :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (list a :--> PBool))
-> Term s (c :--> (list a :--> PBool))
plam ((Term s (a :--> PBool) -> Term s (list a :--> PBool))
 -> Term s ((a :--> PBool) :--> (list a :--> PBool)))
-> (Term s (a :--> PBool) -> Term s (list a :--> PBool))
-> Term s ((a :--> PBool) :--> (list a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s (a :--> PBool)
predicate ->
    (Term s (list a :--> PBool)
 -> Term s a -> Term s (list a) -> Term s PBool)
-> (Term s (list a :--> PBool) -> Term s PBool)
-> Term s (list a :--> PBool)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
PIsListLike list a =>
(Term s (list a :--> r) -> Term s a -> Term s (list a) -> Term s r)
-> (Term s (list a :--> r) -> Term s r) -> Term s (list a :--> r)
precList (\Term s (list a :--> PBool)
self Term s a
x Term s (list a)
xs -> Term s (a :--> PBool)
predicate Term s (a :--> PBool) -> Term s a -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| Term s (list a :--> PBool)
self Term s (list a :--> PBool) -> Term s (list a) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs) (Term s PBool -> Term s (list a :--> PBool) -> Term s PBool
forall a b. a -> b -> a
const (Term s PBool -> Term s (list a :--> PBool) -> Term s PBool)
-> Term s PBool -> Term s (list a :--> PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False)

-- | / O(n) /. Map a function over a list of elements
pmap :: (PListLike list, PElemConstraint list a, PElemConstraint list b) => Term s ((a :--> b) :--> list a :--> list b)
pmap :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b) =>
Term s ((a :--> b) :--> (list a :--> list b))
pmap = ClosedTerm ((a :--> b) :--> (list a :--> list b))
-> Term s ((a :--> b) :--> (list a :--> list b))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm ((a :--> b) :--> (list a :--> list b))
 -> Term s ((a :--> b) :--> (list a :--> list b)))
-> ClosedTerm ((a :--> b) :--> (list a :--> list b))
-> Term s ((a :--> b) :--> (list a :--> list b))
forall a b. (a -> b) -> a -> b
$
  (Term s (a :--> b) -> Term s (list a :--> list b))
-> Term s ((a :--> b) :--> (list a :--> list b))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (list a :--> list b))
-> Term s (c :--> (list a :--> list b))
plam ((Term s (a :--> b) -> Term s (list a :--> list b))
 -> Term s ((a :--> b) :--> (list a :--> list b)))
-> (Term s (a :--> b) -> Term s (list a :--> list b))
-> Term s ((a :--> b) :--> (list a :--> list b))
forall a b. (a -> b) -> a -> b
$ \Term s (a :--> b)
f ->
    (Term s (list a :--> list b)
 -> Term s a -> Term s (list a) -> Term s (list b))
-> (Term s (list a :--> list b) -> Term s (list b))
-> Term s (list a :--> list b)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
PIsListLike list a =>
(Term s (list a :--> r) -> Term s a -> Term s (list a) -> Term s r)
-> (Term s (list a :--> r) -> Term s r) -> Term s (list a :--> r)
precList (\Term s (list a :--> list b)
self Term s a
x Term s (list a)
xs -> Term s (b :--> (list b :--> list b))
forall (a :: S -> Type) (s :: S).
PElemConstraint list a =>
Term s (a :--> (list a :--> list a))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons Term s (b :--> (list b :--> list b))
-> Term s b -> Term s (list b :--> list b)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (a :--> b)
f Term s (a :--> b) -> Term s a -> Term s b
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x) Term s (list b :--> list b) -> Term s (list b) -> Term s (list b)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (list a :--> list b)
self Term s (list a :--> list b) -> Term s (list a) -> Term s (list b)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs)) (Term s (list b) -> Term s (list a :--> list b) -> Term s (list b)
forall a b. a -> b -> a
const Term s (list b)
forall (a :: S -> Type) (s :: S).
PElemConstraint list a =>
Term s (list a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil)

-- | / O(n) /. Filter elements from a list that don't match the predicate.
pfilter :: PIsListLike list a => Term s ((a :--> PBool) :--> list a :--> list a)
pfilter :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> list a))
pfilter =
  ClosedTerm ((a :--> PBool) :--> (list a :--> list a))
-> Term s ((a :--> PBool) :--> (list a :--> list a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm ((a :--> PBool) :--> (list a :--> list a))
 -> Term s ((a :--> PBool) :--> (list a :--> list a)))
-> ClosedTerm ((a :--> PBool) :--> (list a :--> list a))
-> Term s ((a :--> PBool) :--> (list a :--> list a))
forall a b. (a -> b) -> a -> b
$
    (Term s (a :--> PBool) -> Term s (list a :--> list a))
-> Term s ((a :--> PBool) :--> (list a :--> list a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (list a :--> list a))
-> Term s (c :--> (list a :--> list a))
plam ((Term s (a :--> PBool) -> Term s (list a :--> list a))
 -> Term s ((a :--> PBool) :--> (list a :--> list a)))
-> (Term s (a :--> PBool) -> Term s (list a :--> list a))
-> Term s ((a :--> PBool) :--> (list a :--> list a))
forall a b. (a -> b) -> a -> b
$ \Term s (a :--> PBool)
predicate ->
      (Term s (list a :--> list a)
 -> Term s a -> Term s (list a) -> Term s (list a))
-> (Term s (list a :--> list a) -> Term s (list a))
-> Term s (list a :--> list a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
PIsListLike list a =>
(Term s (list a :--> r) -> Term s a -> Term s (list a) -> Term s r)
-> (Term s (list a :--> r) -> Term s r) -> Term s (list a :--> r)
precList
        ( \Term s (list a :--> list a)
self Term s a
x' Term s (list a)
xs -> Term s a -> (Term s a -> Term s (list a)) -> Term s (list a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s a
x' ((Term s a -> Term s (list a)) -> Term s (list a))
-> (Term s a -> Term s (list a)) -> Term s (list a)
forall a b. (a -> b) -> a -> b
$ \Term s a
x ->
            Term s PBool
-> Term s (list a) -> Term s (list a) -> Term s (list a)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
              (Term s (a :--> PBool)
predicate Term s (a :--> PBool) -> Term s a -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x)
              (Term s (a :--> (list a :--> list a))
forall (a :: S -> Type) (s :: S).
PElemConstraint list a =>
Term s (a :--> (list a :--> list a))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons Term s (a :--> (list a :--> list a))
-> Term s a -> Term s (list a :--> list a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x Term s (list a :--> list a) -> Term s (list a) -> Term s (list a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (list a :--> list a)
self Term s (list a :--> list a) -> Term s (list a) -> Term s (list a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs))
              (Term s (list a :--> list a)
self Term s (list a :--> list a) -> Term s (list a) -> Term s (list a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs)
        )
        (Term s (list a) -> Term s (list a :--> list a) -> Term s (list a)
forall a b. a -> b -> a
const Term s (list a)
forall (a :: S -> Type) (s :: S).
PElemConstraint list a =>
Term s (list a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil)

--------------------------------------------------------------------------------

{- | / O(n) /. Concatenate two lists

 Example:
 > pconcat # psingleton x # psingleton y == plistLiteral [x, y]

 pconcat exhibits identities with empty lists such that
 > forall x. pconcat # pnil # x == x
 > forall x. pconcat # x # pnil == x
-}
pconcat :: PIsListLike list a => Term s (list a :--> list a :--> list a)
pconcat :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Term s (list a :--> (list a :--> list a))
pconcat =
  ClosedTerm (list a :--> (list a :--> list a))
-> Term s (list a :--> (list a :--> list a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> (list a :--> list a))
 -> Term s (list a :--> (list a :--> list a)))
-> ClosedTerm (list a :--> (list a :--> list a))
-> Term s (list a :--> (list a :--> list a))
forall a b. (a -> b) -> a -> b
$
    (Term s (list a) -> Term s (list a) -> Term s (list a))
-> Term s (list a :--> (list a :--> list a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (list a) -> Term s (list a))
-> Term s (c :--> (list a :--> list a))
plam ((Term s (list a) -> Term s (list a) -> Term s (list a))
 -> Term s (list a :--> (list a :--> list a)))
-> (Term s (list a) -> Term s (list a) -> Term s (list a))
-> Term s (list a :--> (list a :--> list a))
forall a b. (a -> b) -> a -> b
$ \Term s (list a)
xs Term s (list a)
ys ->
      (Term s (list a :--> list a)
 -> Term s a -> Term s (list a) -> Term s (list a))
-> (Term s (list a :--> list a) -> Term s (list a))
-> Term s (list a :--> list a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
PIsListLike list a =>
(Term s (list a :--> r) -> Term s a -> Term s (list a) -> Term s r)
-> (Term s (list a :--> r) -> Term s r) -> Term s (list a :--> r)
precList
        ( \Term s (list a :--> list a)
self Term s a
x Term s (list a)
xs ->
            Term s (a :--> (list a :--> list a))
forall (a :: S -> Type) (s :: S).
PElemConstraint list a =>
Term s (a :--> (list a :--> list a))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons Term s (a :--> (list a :--> list a))
-> Term s a -> Term s (list a :--> list a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x Term s (list a :--> list a) -> Term s (list a) -> Term s (list a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (list a :--> list a)
self Term s (list a :--> list a) -> Term s (list a) -> Term s (list a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs)
        )
        (Term s (list a) -> Term s (list a :--> list a) -> Term s (list a)
forall a b. a -> b -> a
const Term s (list a)
ys)
        # xs

{- | / O(min(n, m)) /. Zip two lists together with a passed function.

If the lists are of differing lengths, cut to the shortest.
-}
pzipWith ::
  ( PListLike list
  , PElemConstraint list a
  , PElemConstraint list b
  , PElemConstraint list c
  ) =>
  Term s ((a :--> b :--> c) :--> list a :--> list b :--> list c)
pzipWith :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (c :: S -> Type) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b,
 PElemConstraint list c) =>
Term
  s ((a :--> (b :--> c)) :--> (list a :--> (list b :--> list c)))
pzipWith =
  ClosedTerm
  ((a :--> (b :--> c)) :--> (list a :--> (list b :--> list c)))
-> Term
     s ((a :--> (b :--> c)) :--> (list a :--> (list b :--> list c)))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm
   ((a :--> (b :--> c)) :--> (list a :--> (list b :--> list c)))
 -> Term
      s ((a :--> (b :--> c)) :--> (list a :--> (list b :--> list c))))
-> ClosedTerm
     ((a :--> (b :--> c)) :--> (list a :--> (list b :--> list c)))
-> Term
     s ((a :--> (b :--> c)) :--> (list a :--> (list b :--> list c)))
forall a b. (a -> b) -> a -> b
$
    (Term s (a :--> (b :--> c))
 -> Term s (list a :--> (list b :--> list c)))
-> Term
     s ((a :--> (b :--> c)) :--> (list a :--> (list b :--> list c)))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (list a :--> (list b :--> list c)))
-> Term s (c :--> (list a :--> (list b :--> list c)))
plam ((Term s (a :--> (b :--> c))
  -> Term s (list a :--> (list b :--> list c)))
 -> Term
      s ((a :--> (b :--> c)) :--> (list a :--> (list b :--> list c))))
-> (Term s (a :--> (b :--> c))
    -> Term s (list a :--> (list b :--> list c)))
-> Term
     s ((a :--> (b :--> c)) :--> (list a :--> (list b :--> list c)))
forall a b. (a -> b) -> a -> b
$ \Term s (a :--> (b :--> c))
f ->
      Term
  s
  (((list a :--> (list b :--> list c))
    :--> (list a :--> (list b :--> list c)))
   :--> (list a :--> (list b :--> list c)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
  s
  (((list a :--> (list b :--> list c))
    :--> (list a :--> (list b :--> list c)))
   :--> (list a :--> (list b :--> list c)))
-> Term
     s
     ((list a :--> (list b :--> list c))
      :--> (list a :--> (list b :--> list c)))
-> Term s (list a :--> (list b :--> list c))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s (list a :--> (list b :--> list c))
 -> Term s (list a) -> Term s (list b) -> Term s (list c))
-> Term
     s
     ((list a :--> (list b :--> list c))
      :--> (list a :--> (list b :--> list c)))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (list a) -> Term s (list b) -> Term s (list c))
-> Term s (c :--> (list a :--> (list b :--> list c)))
plam ((Term s (list a :--> (list b :--> list c))
  -> Term s (list a) -> Term s (list b) -> Term s (list c))
 -> Term
      s
      ((list a :--> (list b :--> list c))
       :--> (list a :--> (list b :--> list c))))
-> (Term s (list a :--> (list b :--> list c))
    -> Term s (list a) -> Term s (list b) -> Term s (list c))
-> Term
     s
     ((list a :--> (list b :--> list c))
      :--> (list a :--> (list b :--> list c)))
forall a b. (a -> b) -> a -> b
$ \Term s (list a :--> (list b :--> list c))
self Term s (list a)
lx Term s (list b)
ly ->
        (Term s a -> Term s (list a) -> Term s (list c))
-> Term s (list c) -> Term s (list a) -> Term s (list c)
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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
x Term s (list a)
xs ->
              (Term s b -> Term s (list b) -> Term s (list c))
-> Term s (list c) -> Term s (list b) -> Term s (list c)
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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 b
y Term s (list b)
ys -> Term s (c :--> (list c :--> list c))
forall (a :: S -> Type) (s :: S).
PElemConstraint list a =>
Term s (a :--> (list a :--> list a))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons Term s (c :--> (list c :--> list c))
-> Term s c -> Term s (list c :--> list c)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (a :--> (b :--> c))
f Term s (a :--> (b :--> c)) -> Term s a -> Term s (b :--> c)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x Term s (b :--> c) -> Term s b -> Term s c
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
y) Term s (list c :--> list c) -> Term s (list c) -> Term s (list c)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (list a :--> (list b :--> list c))
self Term s (list a :--> (list b :--> list c))
-> Term s (list a) -> Term s (list b :--> list c)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs Term s (list b :--> list c) -> Term s (list b) -> Term s (list c)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list b)
ys))
                Term s (list c)
forall (a :: S -> Type) (s :: S).
PElemConstraint list a =>
Term s (list a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil
                Term s (list b)
ly
          )
          Term s (list c)
forall (a :: S -> Type) (s :: S).
PElemConstraint list a =>
Term s (list a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil
          Term s (list a)
lx

-- | Like 'pzipWith' but with Haskell-level merge function.
pzipWith' ::
  ( PListLike list
  , PElemConstraint list a
  , PElemConstraint list b
  , PElemConstraint list c
  ) =>
  (Term s a -> Term s b -> Term s c) ->
  Term s (list a :--> list b :--> list c)
pzipWith' :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (c :: S -> Type) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b,
 PElemConstraint list c) =>
(Term s a -> Term s b -> Term s c)
-> Term s (list a :--> (list b :--> list c))
pzipWith' Term s a -> Term s b -> Term s c
f =
  Term
  s
  (((list a :--> (list b :--> list c))
    :--> (list a :--> (list b :--> list c)))
   :--> (list a :--> (list b :--> list c)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
  s
  (((list a :--> (list b :--> list c))
    :--> (list a :--> (list b :--> list c)))
   :--> (list a :--> (list b :--> list c)))
-> Term
     s
     ((list a :--> (list b :--> list c))
      :--> (list a :--> (list b :--> list c)))
-> Term s (list a :--> (list b :--> list c))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s (list a :--> (list b :--> list c))
 -> Term s (list a) -> Term s (list b) -> Term s (list c))
-> Term
     s
     ((list a :--> (list b :--> list c))
      :--> (list a :--> (list b :--> list c)))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (list a) -> Term s (list b) -> Term s (list c))
-> Term s (c :--> (list a :--> (list b :--> list c)))
plam ((Term s (list a :--> (list b :--> list c))
  -> Term s (list a) -> Term s (list b) -> Term s (list c))
 -> Term
      s
      ((list a :--> (list b :--> list c))
       :--> (list a :--> (list b :--> list c))))
-> (Term s (list a :--> (list b :--> list c))
    -> Term s (list a) -> Term s (list b) -> Term s (list c))
-> Term
     s
     ((list a :--> (list b :--> list c))
      :--> (list a :--> (list b :--> list c)))
forall a b. (a -> b) -> a -> b
$ \Term s (list a :--> (list b :--> list c))
self Term s (list a)
lx Term s (list b)
ly ->
    (Term s a -> Term s (list a) -> Term s (list c))
-> Term s (list c) -> Term s (list a) -> Term s (list c)
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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
x Term s (list a)
xs ->
          (Term s b -> Term s (list b) -> Term s (list c))
-> Term s (list c) -> Term s (list b) -> Term s (list c)
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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 b
y Term s (list b)
ys -> Term s (c :--> (list c :--> list c))
forall (a :: S -> Type) (s :: S).
PElemConstraint list a =>
Term s (a :--> (list a :--> list a))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons Term s (c :--> (list c :--> list c))
-> Term s c -> Term s (list c :--> list c)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a -> Term s b -> Term s c
f Term s a
x Term s b
y Term s (list c :--> list c) -> Term s (list c) -> Term s (list c)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (list a :--> (list b :--> list c))
self Term s (list a :--> (list b :--> list c))
-> Term s (list a) -> Term s (list b :--> list c)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs Term s (list b :--> list c) -> Term s (list b) -> Term s (list c)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list b)
ys))
            Term s (list c)
forall (a :: S -> Type) (s :: S).
PElemConstraint list a =>
Term s (list a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil
            Term s (list b)
ly
      )
      Term s (list c)
forall (a :: S -> Type) (s :: S).
PElemConstraint list a =>
Term s (list a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil
      Term s (list a)
lx

{- | / O(min(n, m)) /. Zip two lists together, creating pairs of the elements.

If the lists are of differing lengths, cut to the shortest.
-}
pzip ::
  ( PListLike list
  , PElemConstraint list a
  , PElemConstraint list b
  , PElemConstraint list (PPair a b)
  ) =>
  Term s (list a :--> list b :--> list (PPair a b))
pzip :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b,
 PElemConstraint list (PPair a b)) =>
Term s (list a :--> (list b :--> list (PPair a b)))
pzip = ClosedTerm (list a :--> (list b :--> list (PPair a b)))
-> Term s (list a :--> (list b :--> list (PPair a b)))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> (list b :--> list (PPair a b)))
 -> Term s (list a :--> (list b :--> list (PPair a b))))
-> ClosedTerm (list a :--> (list b :--> list (PPair a b)))
-> Term s (list a :--> (list b :--> list (PPair a b)))
forall a b. (a -> b) -> a -> b
$ (Term s a -> Term s b -> Term s (PPair a b))
-> Term s (list a :--> (list b :--> list (PPair a b)))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (c :: S -> Type) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b,
 PElemConstraint list c) =>
(Term s a -> Term s b -> Term s c)
-> Term s (list a :--> (list b :--> list c))
pzipWith' ((Term s a -> Term s b -> Term s (PPair a b))
 -> Term s (list a :--> (list b :--> list (PPair a b))))
-> (Term s a -> Term s b -> Term s (PPair a b))
-> Term s (list a :--> (list b :--> list (PPair a b)))
forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s b
y -> PPair a b s -> Term s (PPair a b)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (Term s a -> Term s b -> PPair a b s
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair Term s a
x Term s b
y)

-- | / O(min(n, m)) /. Check if two lists are equal.
plistEquals :: (PIsListLike list a, PEq a) => Term s (list a :--> list a :--> PBool)
plistEquals :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PIsListLike list a, PEq a) =>
Term s (list a :--> (list a :--> PBool))
plistEquals =
  ClosedTerm (list a :--> (list a :--> PBool))
-> Term s (list a :--> (list a :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> (list a :--> PBool))
 -> Term s (list a :--> (list a :--> PBool)))
-> ClosedTerm (list a :--> (list a :--> PBool))
-> Term s (list a :--> (list a :--> PBool))
forall a b. (a -> b) -> a -> b
$
    Term
  s
  (((list a :--> (list a :--> PBool))
    :--> (list a :--> (list a :--> PBool)))
   :--> (list a :--> (list a :--> PBool)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
  s
  (((list a :--> (list a :--> PBool))
    :--> (list a :--> (list a :--> PBool)))
   :--> (list a :--> (list a :--> PBool)))
-> Term
     s
     ((list a :--> (list a :--> PBool))
      :--> (list a :--> (list a :--> PBool)))
-> Term s (list a :--> (list a :--> PBool))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s (list a :--> (list a :--> PBool))
 -> Term s (list a) -> Term s (list a) -> Term s PBool)
-> Term
     s
     ((list a :--> (list a :--> PBool))
      :--> (list a :--> (list a :--> PBool)))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (list a) -> Term s (list a) -> Term s PBool)
-> Term s (c :--> (list a :--> (list a :--> PBool)))
plam ((Term s (list a :--> (list a :--> PBool))
  -> Term s (list a) -> Term s (list a) -> Term s PBool)
 -> Term
      s
      ((list a :--> (list a :--> PBool))
       :--> (list a :--> (list a :--> PBool))))
-> (Term s (list a :--> (list a :--> PBool))
    -> Term s (list a) -> Term s (list a) -> Term s PBool)
-> Term
     s
     ((list a :--> (list a :--> PBool))
      :--> (list a :--> (list a :--> PBool)))
forall a b. (a -> b) -> a -> b
$ \Term s (list a :--> (list a :--> PBool))
self Term s (list a)
xlist Term s (list a)
ylist ->
      (Term s a -> Term s (list a) -> Term s PBool)
-> Term s PBool -> Term s (list a) -> Term s PBool
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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
x Term s (list a)
xs ->
            (Term s a -> Term s (list a) -> Term s PBool)
-> Term s PBool -> Term s (list a) -> Term s PBool
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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
y Term s (list a)
ys -> Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s a
x Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s a
y) (Term s (list a :--> (list a :--> PBool))
self Term s (list a :--> (list a :--> PBool))
-> Term s (list a) -> Term s (list a :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs Term s (list a :--> PBool) -> Term s (list a) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
ys) (AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False)) (AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False) Term s (list a)
ylist
        )
        ((Term s a -> Term s (list a) -> Term s PBool)
-> Term s PBool -> Term s (list a) -> Term s PBool
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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
_ Term s (list a)
_ -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False) (AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True) Term s (list a)
ylist)
        Term s (list a)
xlist

-- | / O(n) /. Like Haskell level `(!!)` but on the plutarch level
(#!!) :: PIsListLike l a => Term s (l a) -> Term s PInteger -> Term s a
Term s (l a)
l #!! :: forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s (l a) -> Term s PInteger -> Term s a
#!! Term s PInteger
i = Term s (PInteger :--> (l a :--> a))
forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s (PInteger :--> (l a :--> a))
pelemAt Term s (PInteger :--> (l a :--> a))
-> Term s PInteger -> Term s (l a :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
i Term s (l a :--> a) -> Term s (l a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
l

{- | / O(n) /. Like Haskell level `(!!)` but on the Plutarch level, not infix and
    with arguments reversed, errors if the specified index is greater than or equal
    to the lists length
-}
pelemAt :: PIsListLike l a => Term s (PInteger :--> l a :--> a)
pelemAt :: forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s (PInteger :--> (l a :--> a))
pelemAt = ClosedTerm (PInteger :--> (l a :--> a))
-> Term s (PInteger :--> (l a :--> a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PInteger :--> (l a :--> a))
 -> Term s (PInteger :--> (l a :--> a)))
-> ClosedTerm (PInteger :--> (l a :--> a))
-> Term s (PInteger :--> (l a :--> a))
forall a b. (a -> b) -> a -> b
$
  (Term s PInteger -> Term s (l a) -> Term s a)
-> Term s (PInteger :--> (l a :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (l a) -> Term s a)
-> Term s (c :--> (l a :--> a))
plam ((Term s PInteger -> Term s (l a) -> Term s a)
 -> Term s (PInteger :--> (l a :--> a)))
-> (Term s PInteger -> Term s (l a) -> Term s a)
-> Term s (PInteger :--> (l a :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s PInteger
n Term s (l a)
xs ->
    Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s PInteger
n Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s PInteger
0)
      (Term s PString -> Term s a
forall (a :: S -> Type) (s :: S). Term s PString -> Term s a
ptraceInfoError Term s PString
"pelemAt: negative index")
      (Term s (PInteger :--> (l a :--> a))
forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s (PInteger :--> (l a :--> a))
pelemAt' Term s (PInteger :--> (l a :--> a))
-> Term s PInteger -> Term s (l a :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
n Term s (l a :--> a) -> Term s (l a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
xs)

-- | / O(n) /. like `pelemAt` but doesn't fail on negative indexes
pelemAt' :: PIsListLike l a => Term s (PInteger :--> l a :--> a)
pelemAt' :: forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s (PInteger :--> (l a :--> a))
pelemAt' = ClosedTerm (PInteger :--> (l a :--> a))
-> Term s (PInteger :--> (l a :--> a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PInteger :--> (l a :--> a))
 -> Term s (PInteger :--> (l a :--> a)))
-> ClosedTerm (PInteger :--> (l a :--> a))
-> Term s (PInteger :--> (l a :--> a))
forall a b. (a -> b) -> a -> b
$
  Term
  s
  (((PInteger :--> (l a :--> a)) :--> (PInteger :--> (l a :--> a)))
   :--> (PInteger :--> (l a :--> a)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
  s
  (((PInteger :--> (l a :--> a)) :--> (PInteger :--> (l a :--> a)))
   :--> (PInteger :--> (l a :--> a)))
-> Term
     s ((PInteger :--> (l a :--> a)) :--> (PInteger :--> (l a :--> a)))
-> Term s (PInteger :--> (l a :--> a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s (PInteger :--> (l a :--> a))
 -> Term s PInteger -> Term s (l a) -> Term s a)
-> Term
     s ((PInteger :--> (l a :--> a)) :--> (PInteger :--> (l a :--> a)))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PInteger -> Term s (l a) -> Term s a)
-> Term s (c :--> (PInteger :--> (l a :--> a)))
plam ((Term s (PInteger :--> (l a :--> a))
  -> Term s PInteger -> Term s (l a) -> Term s a)
 -> Term
      s ((PInteger :--> (l a :--> a)) :--> (PInteger :--> (l a :--> a))))
-> (Term s (PInteger :--> (l a :--> a))
    -> Term s PInteger -> Term s (l a) -> Term s a)
-> Term
     s ((PInteger :--> (l a :--> a)) :--> (PInteger :--> (l a :--> a)))
forall a b. (a -> b) -> a -> b
$ \Term s (PInteger :--> (l a :--> a))
self Term s PInteger
n Term s (l a)
xs ->
    Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s PInteger
n Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
0)
      (Term s (l a :--> a)
forall (a :: S -> Type) (s :: S).
PElemConstraint l a =>
Term s (l a :--> a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead Term s (l a :--> a) -> Term s (l a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
xs)
      (Term s (PInteger :--> (l a :--> a))
self Term s (PInteger :--> (l a :--> a))
-> Term s PInteger -> Term s (l a :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PInteger
n Term s PInteger -> Term s PInteger -> Term s PInteger
forall a. Num a => a -> a -> a
- Term s PInteger
1) Term s (l a :--> a) -> Term s (l a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (l a :--> l a)
forall (a :: S -> Type) (s :: S).
PElemConstraint l a =>
Term s (l a :--> l a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail Term s (l a :--> l a) -> Term s (l a) -> Term s (l a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
xs)

-- | / O(n) /. like haskell level `find` but on plutarch level
pfind :: PIsListLike l a => Term s ((a :--> PBool) :--> l a :--> PMaybe a)
pfind :: forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
pfind = ClosedTerm ((a :--> PBool) :--> (l a :--> PMaybe a))
-> Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm ((a :--> PBool) :--> (l a :--> PMaybe a))
 -> Term s ((a :--> PBool) :--> (l a :--> PMaybe a)))
-> ClosedTerm ((a :--> PBool) :--> (l a :--> PMaybe a))
-> Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
forall a b. (a -> b) -> a -> b
$
  Term
  s
  ((((a :--> PBool) :--> (l a :--> PMaybe a))
    :--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
   :--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
  s
  ((((a :--> PBool) :--> (l a :--> PMaybe a))
    :--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
   :--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
-> Term
     s
     (((a :--> PBool) :--> (l a :--> PMaybe a))
      :--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
-> Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
 -> Term s (a :--> PBool) -> Term s (l a) -> Term s (PMaybe a))
-> Term
     s
     (((a :--> PBool) :--> (l a :--> PMaybe a))
      :--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c
 -> Term s (a :--> PBool) -> Term s (l a) -> Term s (PMaybe a))
-> Term s (c :--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
plam ((Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
  -> Term s (a :--> PBool) -> Term s (l a) -> Term s (PMaybe a))
 -> Term
      s
      (((a :--> PBool) :--> (l a :--> PMaybe a))
       :--> ((a :--> PBool) :--> (l a :--> PMaybe a))))
-> (Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
    -> Term s (a :--> PBool) -> Term s (l a) -> Term s (PMaybe a))
-> Term
     s
     (((a :--> PBool) :--> (l a :--> PMaybe a))
      :--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
forall a b. (a -> b) -> a -> b
$ \Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
self Term s (a :--> PBool)
f Term s (l a)
xs ->
    (Term s a -> Term s (l a) -> Term s (PMaybe a))
-> Term s (PMaybe a) -> Term s (l a) -> Term s (PMaybe a)
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint l a =>
(Term s a -> Term s (l a) -> Term s r)
-> Term s r -> Term s (l a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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
y Term s (l a)
ys ->
          Term s PBool
-> Term s (PMaybe a) -> Term s (PMaybe a) -> Term s (PMaybe a)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
            (Term s (a :--> PBool)
f Term s (a :--> PBool) -> Term s a -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
y)
            (PMaybe a s -> Term s (PMaybe a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PMaybe a s -> Term s (PMaybe a))
-> PMaybe a s -> Term s (PMaybe a)
forall a b. (a -> b) -> a -> b
$ Term s a -> PMaybe a s
forall (a :: S -> Type) (s :: S). Term s a -> PMaybe a s
PJust Term s a
y)
            (Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
self Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
-> Term s (a :--> PBool) -> Term s (l a :--> PMaybe a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (a :--> PBool)
f Term s (l a :--> PMaybe a) -> Term s (l a) -> Term s (PMaybe a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
ys)
      )
      (PMaybe a s -> Term s (PMaybe a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PMaybe a s
forall (a :: S -> Type) (s :: S). PMaybe a s
PNothing)
      Term s (l a)
xs

{- | / O(n) /. Reverse a list-like structure.

@since WIP
-}
preverse ::
  forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
  PIsListLike l a =>
  Term s (l a :--> l a)
preverse :: forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s (l a :--> l a)
preverse = ClosedTerm (l a :--> l a) -> Term s (l a :--> l a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (l a :--> l a) -> Term s (l a :--> l a))
-> ClosedTerm (l a :--> l a) -> Term s (l a :--> l a)
forall a b. (a -> b) -> a -> b
$ Term s ((l a :--> (a :--> l a)) :--> (l a :--> (l a :--> l a)))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (b :: S -> Type).
PIsListLike list a =>
Term s ((b :--> (a :--> b)) :--> (b :--> (list a :--> b)))
pfoldl Term s ((l a :--> (a :--> l a)) :--> (l a :--> (l a :--> l a)))
-> Term s (l a :--> (a :--> l a))
-> Term s (l a :--> (l a :--> l a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (l a) -> Term s a -> Term s (l a))
-> Term s (l a :--> (a :--> l a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s a -> Term s (l a))
-> Term s (c :--> (a :--> l a))
plam (\Term s (l a)
xs Term s a
x -> Term s (a :--> (l a :--> l a))
forall (a :: S -> Type) (s :: S).
PElemConstraint l a =>
Term s (a :--> (l a :--> l a))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons Term s (a :--> (l a :--> l a)) -> Term s a -> Term s (l a :--> l a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x Term s (l a :--> l a) -> Term s (l a) -> Term s (l a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
xs) Term s (l a :--> (l a :--> l a))
-> Term s (l a) -> Term s (l a :--> l a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
forall (a :: S -> Type) (s :: S).
PElemConstraint l a =>
Term s (l a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil

{- | / O(n) /. Checks if a list-list structure is sorted.

@since WIP
-}
pcheckSorted ::
  forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
  (PIsListLike l a, POrd a) =>
  Term s (l a :--> PBool)
pcheckSorted :: forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
(PIsListLike l a, POrd a) =>
Term s (l a :--> PBool)
pcheckSorted =
  Term
  s (((l a :--> PBool) :--> (l a :--> PBool)) :--> (l a :--> PBool))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
  s (((l a :--> PBool) :--> (l a :--> PBool)) :--> (l a :--> PBool))
-> Term s ((l a :--> PBool) :--> (l a :--> PBool))
-> Term s (l a :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s (l a :--> PBool) -> Term s (l a) -> Term s PBool)
-> Term s ((l a :--> PBool) :--> (l a :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (l a) -> Term s PBool)
-> Term s (c :--> (l a :--> PBool))
plam ((Term s (l a :--> PBool) -> Term s (l a) -> Term s PBool)
 -> Term s ((l a :--> PBool) :--> (l a :--> PBool)))
-> (Term s (l a :--> PBool) -> Term s (l a) -> Term s PBool)
-> Term s ((l a :--> PBool) :--> (l a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s (l a :--> PBool)
self Term s (l a)
xs ->
    (Term s a -> Term s (l a) -> Term s PBool)
-> Term s PBool -> Term s (l a) -> Term s PBool
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint l a =>
(Term s a -> Term s (l a) -> Term s r)
-> Term s r -> Term s (l a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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 ->
          (Term s a -> Term s (l a) -> Term s PBool)
-> Term s PBool -> Term s (l a) -> Term s PBool
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint l a =>
(Term s a -> Term s (l a) -> Term s r)
-> Term s r -> Term s (l a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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 Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s a
x2 Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#&& (Term s (l a :--> PBool)
self Term s (l a :--> PBool) -> Term s (l a) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
xs))
            (PBool s -> Term s PBool
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PTrue)
            Term s (l a)
xs
      )
      (PBool s -> Term s PBool
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PTrue)
      Term s (l a)
xs