module Plutarch.Internal.ListLike (
  PIsListLike,
  PListLike,
  PElemConstraint,
  pelimList,
  pcons,
  pnil,
  phead,
  ptail,
  pnull,
  pconvertLists,
  precList,
  psingleton,
  plength,
  ptryIndex,
  pdrop,
  pfoldl',
  pfoldl,
  pfoldr',
  pfoldr,
  pfoldrLazy,
  pall,
  pany,
  pmap,
  pfilter,
  pconcat,
  pzipWith,
  pzipWith',
) where

import Data.Kind (Constraint, Type)

import Plutarch.Builtin.Bool (
  PBool,
  pfalse,
  pif,
  ptrue,
  (#&&),
  (#||),
 )
import Plutarch.Builtin.Data (
  PBuiltinList (PCons, PNil),
  pheadBuiltin,
  pnullBuiltin,
  ptailBuiltin,
 )
import Plutarch.Builtin.Integer (
  PInteger,
  paddInteger,
  pconstantInteger,
 )

import Plutarch.Internal.Fix (pfix)
import {-# SOURCE #-} Plutarch.Internal.Lift (PlutusRepr)
import Plutarch.Internal.PLam (PLamN (plam))
import Plutarch.Internal.PlutusType (pcon, pmatch)
import Plutarch.Internal.Term (
  PDelayed,
  S,
  Term,
  pdelay,
  perror,
  phoistAcyclic,
  plet,
  (#),
  (#$),
  type (:-->),
 )

import Numeric.Natural (Natural)
import PlutusCore qualified as PLC

-- | '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)
_ -> Term s PBool
forall (s :: S). Term s PBool
pfalse) Term s PBool
forall (s :: S). Term s PBool
ptrue

instance PListLike PBuiltinList where
  type PElemConstraint PBuiltinList a = (PLC.Contains PLC.DefaultUni (PlutusRepr a))

  pelimList :: forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint PBuiltinList a =>
(Term s a -> Term s (PBuiltinList a) -> Term s r)
-> Term s r -> Term s (PBuiltinList a) -> Term s r
pelimList Term s a -> Term s (PBuiltinList a) -> Term s r
match_cons Term s r
match_nil Term s (PBuiltinList a)
ls = Term s (PBuiltinList a)
-> (PBuiltinList 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 (PBuiltinList a)
ls ((PBuiltinList a s -> Term s r) -> Term s r)
-> (PBuiltinList a s -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ \case
    PCons Term s a
x Term s (PBuiltinList a)
xs -> Term s a -> Term s (PBuiltinList a) -> Term s r
match_cons Term s a
x Term s (PBuiltinList a)
xs
    PBuiltinList a s
PNil -> Term s r
match_nil

  pcons :: forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
pcons = (Term s a -> Term s (PBuiltinList a) -> Term s (PBuiltinList a))
-> Term s (a :--> (PBuiltinList a :--> PBuiltinList 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 (PBuiltinList a) -> Term s (PBuiltinList a))
-> Term s (c :--> (PBuiltinList a :--> PBuiltinList a))
plam ((Term s a -> Term s (PBuiltinList a) -> Term s (PBuiltinList a))
 -> Term s (a :--> (PBuiltinList a :--> PBuiltinList a)))
-> (Term s a -> Term s (PBuiltinList a) -> Term s (PBuiltinList a))
-> Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s (PBuiltinList a)
xs -> PBuiltinList a s -> Term s (PBuiltinList a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (Term s a -> Term s (PBuiltinList a) -> PBuiltinList a s
forall (a :: S -> Type) (s :: S).
Term s a -> Term s (PBuiltinList a) -> PBuiltinList a s
PCons Term s a
x Term s (PBuiltinList a)
xs)
  pnil :: forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a)
pnil = PBuiltinList a s -> Term s (PBuiltinList a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PBuiltinList a s
forall (a :: S -> Type) (s :: S). PBuiltinList a s
PNil
  phead :: forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> a)
phead = Term s (PBuiltinList a :--> a)
forall (s :: S) (a :: S -> Type). Term s (PBuiltinList a :--> a)
pheadBuiltin
  ptail :: forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> PBuiltinList a)
ptail = Term s (PBuiltinList a :--> PBuiltinList a)
forall (s :: S) (a :: S -> Type).
Term s (PBuiltinList a :--> PBuiltinList a)
ptailBuiltin
  pnull :: forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> PBool)
pnull = Term s (PBuiltinList a :--> PBool)
forall (s :: S) (a :: S -> Type).
Term s (PBuiltinList a :--> PBool)
pnullBuiltin

-- | / 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

-- | 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) /. 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 :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
paddInteger Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> 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 :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
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
# Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
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
forall (s :: S). Term s PBool
ptrue)

-- | / 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
forall (s :: S). Term s PBool
pfalse)

-- | / 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