-- | @since 1.12.0
module Plutarch.Array (
  -- * Type
  PPullArray,

  -- * Functions

  -- ** Introduction
  piota,
  pgenerate,
  pfromArray,
  pfromList,

  -- ** Transformation

  -- *** Linear
  pmapArray,
  pimapArray,

  -- *** Affine
  ptakeArray,
  pdropArray,

  -- ** Combination
  pzipWithArray,
  pizipWithArray,

  -- ** Elimination

  -- *** Folds
  pfoldArray,
  prfoldArray,

  -- *** Conversions
  ppullArrayToList,
  ppullArrayToSOPList,
) where

import Data.Kind (Type)
import Plutarch.Builtin.Array (
  PArray,
  pindexArray,
  plengthOfArray,
  plistToArray,
 )
import Plutarch.Builtin.Bool (pif)
import Plutarch.Builtin.Data (PBuiltinList (PNil), pconsBuiltin)
import Plutarch.Builtin.Integer (PInteger)
import Plutarch.Internal.Eq ((#==))
import Plutarch.Internal.Fix (pfix)
import Plutarch.Internal.Numeric (
  PAdditiveSemigroup (pscalePositive, (#+)),
  PMultiplicativeSemigroup (ppowPositive, (#*)),
  PNatural,
  (#-),
 )
import Plutarch.Internal.Ord (POrd ((#<=)), pmin)
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.PlutusType (PlutusType (PInner, pcon', pmatch'), pcon, pmatch)
import Plutarch.Internal.Subtype (pupcast)
import Plutarch.Internal.Term (
  S,
  Term,
  phoistAcyclic,
  plet,
  punsafeCoerce,
  (#),
  (#$),
  (:-->),
 )
import Plutarch.List (PList (PSCons, PSNil))

{- | A pull array, represented as its Boehm-Berrarducci encoding. Put another
way, a pull array is a function which can be \'materialized\' to produce the
elements of that array, in order.

Pull arrays give efficient linear transformations, in exchange for no ability
to index them without evaluation. Pull arrays are best used when you need to
perform a lot of transformations, with a fold or materialization at the end,
as they fuse away /all/ intermediate values. We achieve this by using
Boehm-Berrarducci encodings, which means that every pull array is essentially
a lambda onchain.

@since 1.12.0
-}
newtype PPullArray (a :: S -> Type) (s :: S)
  = PPullArray (forall (r :: S -> Type). Term s ((PNatural :--> (PInteger :--> a) :--> r) :--> r))

-- | @since 1.13.0
instance PlutusType (PPullArray a) where
  type PInner (PPullArray a) = PPullArray a
  pcon' :: forall (s :: S). PPullArray a s -> Term s (PInner (PPullArray a))
pcon' (PPullArray forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
t) = Term
  s
  ((PNatural :--> ((PInteger :--> a) :--> Any @(S -> Type)))
   :--> Any @(S -> Type))
-> Term s (PInner (PPullArray a))
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term
  s
  ((PNatural :--> ((PInteger :--> a) :--> Any @(S -> Type)))
   :--> Any @(S -> Type))
forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
t
  pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PPullArray a))
-> (PPullArray a s -> Term s b) -> Term s b
pmatch' Term s (PInner (PPullArray a))
x PPullArray a s -> Term s b
f = PPullArray a s -> Term s b
f ((forall (r :: S -> Type).
 Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> PPullArray a s
forall (a :: S -> Type) (s :: S).
(forall (r :: S -> Type).
 Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> PPullArray a s
PPullArray ((forall (r :: S -> Type).
  Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
 -> PPullArray a s)
-> (forall (r :: S -> Type).
    Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> PPullArray a s
forall a b. (a -> b) -> a -> b
$ Term s (PInner (PPullArray a))
-> Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s (PInner (PPullArray a))
x)

-- | @since 1.12.0
instance PAdditiveSemigroup a => PAdditiveSemigroup (PPullArray a) where
  #+ :: forall (s :: S).
Term s (PPullArray a)
-> Term s (PPullArray a) -> Term s (PPullArray a)
(#+) = Term s (a :--> (a :--> a))
-> Term s (PPullArray a)
-> Term s (PPullArray a)
-> Term s (PPullArray a)
forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
Term s (a :--> (b :--> c))
-> Term s (PPullArray a)
-> Term s (PPullArray b)
-> Term s (PPullArray c)
pzipWithArray ((Term s a -> Term s a -> Term s a) -> Term s (a :--> (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 a) -> Term s (c :--> (a :--> a))
plam Term s a -> Term s a -> Term s a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
(#+))
  pscalePositive :: forall (s :: S).
Term s (PPullArray a) -> Term s PPositive -> Term s (PPullArray a)
pscalePositive Term s (PPullArray a)
arr Term s PPositive
p = Term s (a :--> a) -> Term s (PPullArray a) -> Term s (PPullArray a)
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s (a :--> b) -> Term s (PPullArray a) -> Term s (PPullArray b)
pmapArray ((Term s a -> Term s a) -> Term s (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 a -> Term s a) -> Term s (a :--> a))
-> (Term s a -> Term s a) -> Term s (a :--> a)
forall a b. (a -> b) -> a -> b
$ \Term s a
x -> Term s a -> Term s PPositive -> Term s a
forall (s :: S). Term s a -> Term s PPositive -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s PPositive -> Term s a
pscalePositive Term s a
x Term s PPositive
p) Term s (PPullArray a)
arr

-- | @since 1.12.0
instance PMultiplicativeSemigroup a => PMultiplicativeSemigroup (PPullArray a) where
  #* :: forall (s :: S).
Term s (PPullArray a)
-> Term s (PPullArray a) -> Term s (PPullArray a)
(#*) = Term s (a :--> (a :--> a))
-> Term s (PPullArray a)
-> Term s (PPullArray a)
-> Term s (PPullArray a)
forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
Term s (a :--> (b :--> c))
-> Term s (PPullArray a)
-> Term s (PPullArray b)
-> Term s (PPullArray c)
pzipWithArray ((Term s a -> Term s a -> Term s a) -> Term s (a :--> (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 a) -> Term s (c :--> (a :--> a))
plam Term s a -> Term s a -> Term s a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s a -> Term s a
(#*))
  ppowPositive :: forall (s :: S).
Term s (PPullArray a) -> Term s PPositive -> Term s (PPullArray a)
ppowPositive Term s (PPullArray a)
arr Term s PPositive
p = Term s (a :--> a) -> Term s (PPullArray a) -> Term s (PPullArray a)
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s (a :--> b) -> Term s (PPullArray a) -> Term s (PPullArray b)
pmapArray ((Term s a -> Term s a) -> Term s (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 a -> Term s a) -> Term s (a :--> a))
-> (Term s a -> Term s a) -> Term s (a :--> a)
forall a b. (a -> b) -> a -> b
$ \Term s a
x -> Term s a -> Term s PPositive -> Term s a
forall (s :: S). Term s a -> Term s PPositive -> Term s a
forall (a :: S -> Type) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s PPositive -> Term s a
ppowPositive Term s a
x Term s PPositive
p) Term s (PPullArray a)
arr

{- | Given a length @n@, construct the pull array equivalent of @[0, 1, ... n -
1]@.

\(Theta(1)\) space and time complexity.

@since 1.12.0
-}
piota :: forall (s :: S). Term s PNatural -> Term s (PPullArray PNatural)
piota :: forall (s :: S). Term s PNatural -> Term s (PPullArray PNatural)
piota Term s PNatural
n = PPullArray PNatural s -> Term s (PPullArray PNatural)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PPullArray PNatural s -> Term s (PPullArray PNatural))
-> PPullArray PNatural s -> Term s (PPullArray PNatural)
forall a b. (a -> b) -> a -> b
$ (forall (r :: S -> Type).
 Term s ((PNatural :--> ((PInteger :--> PNatural) :--> r)) :--> r))
-> PPullArray PNatural s
forall (a :: S -> Type) (s :: S).
(forall (r :: S -> Type).
 Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> PPullArray a s
PPullArray ((forall (r :: S -> Type).
  Term s ((PNatural :--> ((PInteger :--> PNatural) :--> r)) :--> r))
 -> PPullArray PNatural s)
-> (forall (r :: S -> Type).
    Term s ((PNatural :--> ((PInteger :--> PNatural) :--> r)) :--> r))
-> PPullArray PNatural s
forall a b. (a -> b) -> a -> b
$ (Term s (PNatural :--> ((PInteger :--> PNatural) :--> r))
 -> Term s r)
-> Term
     s ((PNatural :--> ((PInteger :--> PNatural) :--> r)) :--> 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 r) -> Term s (c :--> r)
plam ((Term s (PNatural :--> ((PInteger :--> PNatural) :--> r))
  -> Term s r)
 -> Term
      s ((PNatural :--> ((PInteger :--> PNatural) :--> r)) :--> r))
-> (Term s (PNatural :--> ((PInteger :--> PNatural) :--> r))
    -> Term s r)
-> Term
     s ((PNatural :--> ((PInteger :--> PNatural) :--> r)) :--> r)
forall a b. (a -> b) -> a -> b
$ \Term s (PNatural :--> ((PInteger :--> PNatural) :--> r))
k -> Term s (PNatural :--> ((PInteger :--> PNatural) :--> r))
k Term s (PNatural :--> ((PInteger :--> PNatural) :--> r))
-> Term s PNatural -> Term s ((PInteger :--> PNatural) :--> r)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PNatural
n Term s ((PInteger :--> PNatural) :--> r)
-> Term s (PInteger :--> PNatural) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInteger :--> PNatural)
forall (s' :: S). Term s' (PInteger :--> PNatural)
go
  where
    go :: forall (s' :: S). Term s' (PInteger :--> PNatural)
    go :: forall (s' :: S). Term s' (PInteger :--> PNatural)
go = (forall (s' :: S). Term s' (PInteger :--> PNatural))
-> Term s' (PInteger :--> PNatural)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S). Term s' (PInteger :--> PNatural))
 -> Term s' (PInteger :--> PNatural))
-> (forall (s' :: S). Term s' (PInteger :--> PNatural))
-> Term s' (PInteger :--> PNatural)
forall a b. (a -> b) -> a -> b
$ (Term s' PInteger -> Term s' PNatural)
-> Term s' (PInteger :--> PNatural)
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' PNatural) -> Term s' (c :--> PNatural)
plam ((Term s' PInteger -> Term s' PNatural)
 -> Term s' (PInteger :--> PNatural))
-> (Term s' PInteger -> Term s' PNatural)
-> Term s' (PInteger :--> PNatural)
forall a b. (a -> b) -> a -> b
$ \Term s' PInteger
x -> Term s' PInteger -> Term s' PNatural
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s' PInteger
x

{- | Given a length and a function from indexes to values, construct the pull
array of that length, each of whose indexes stores the value computed by that
function.

\(Theta(1)\) space and time complexity.

@since 1.12.0
-}
pgenerate ::
  forall (a :: S -> Type) (s :: S).
  Term s PNatural ->
  Term s (PInteger :--> a) ->
  Term s (PPullArray a)
pgenerate :: forall (a :: S -> Type) (s :: S).
Term s PNatural
-> Term s (PInteger :--> a) -> Term s (PPullArray a)
pgenerate Term s PNatural
len Term s (PInteger :--> a)
f = PPullArray a s -> Term s (PPullArray a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PPullArray a s -> Term s (PPullArray a))
-> PPullArray a s -> Term s (PPullArray a)
forall a b. (a -> b) -> a -> b
$ (forall (r :: S -> Type).
 Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> PPullArray a s
forall (a :: S -> Type) (s :: S).
(forall (r :: S -> Type).
 Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> PPullArray a s
PPullArray ((forall (r :: S -> Type).
  Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
 -> PPullArray a s)
-> (forall (r :: S -> Type).
    Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> PPullArray a s
forall a b. (a -> b) -> a -> b
$ (Term s (PNatural :--> ((PInteger :--> a) :--> r)) -> Term s r)
-> Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> 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 r) -> Term s (c :--> r)
plam ((Term s (PNatural :--> ((PInteger :--> a) :--> r)) -> Term s r)
 -> Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> (Term s (PNatural :--> ((PInteger :--> a) :--> r)) -> Term s r)
-> Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
forall a b. (a -> b) -> a -> b
$ \Term s (PNatural :--> ((PInteger :--> a) :--> r))
k -> Term s (PNatural :--> ((PInteger :--> a) :--> r))
k Term s (PNatural :--> ((PInteger :--> a) :--> r))
-> Term s PNatural -> Term s ((PInteger :--> a) :--> r)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PNatural
len Term s ((PInteger :--> a) :--> r)
-> Term s (PInteger :--> a) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInteger :--> a)
f

{- | Given a builtin array, construct the equivalent pull array.

\(\Theta(1)\) space and time complexity.

@since 1.12.0
-}
pfromArray ::
  forall (a :: S -> Type) (s :: S).
  Term s (PArray a) ->
  Term s (PPullArray a)
pfromArray :: forall (a :: S -> Type) (s :: S).
Term s (PArray a) -> Term s (PPullArray a)
pfromArray Term s (PArray a)
arr = PPullArray a s -> Term s (PPullArray a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PPullArray a s -> Term s (PPullArray a))
-> PPullArray a s -> Term s (PPullArray a)
forall a b. (a -> b) -> a -> b
$ (forall (r :: S -> Type).
 Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> PPullArray a s
forall (a :: S -> Type) (s :: S).
(forall (r :: S -> Type).
 Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> PPullArray a s
PPullArray ((forall (r :: S -> Type).
  Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
 -> PPullArray a s)
-> (forall (r :: S -> Type).
    Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> PPullArray a s
forall a b. (a -> b) -> a -> b
$ (Term s (PNatural :--> ((PInteger :--> a) :--> r)) -> Term s r)
-> Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> 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 r) -> Term s (c :--> r)
plam ((Term s (PNatural :--> ((PInteger :--> a) :--> r)) -> Term s r)
 -> Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> (Term s (PNatural :--> ((PInteger :--> a) :--> r)) -> Term s r)
-> Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
forall a b. (a -> b) -> a -> b
$ \Term s (PNatural :--> ((PInteger :--> a) :--> r))
k ->
  Term s (PNatural :--> ((PInteger :--> a) :--> r))
k Term s (PNatural :--> ((PInteger :--> a) :--> r))
-> Term s PNatural -> Term s ((PInteger :--> a) :--> r)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger -> Term s PNatural
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s (PArray a :--> PInteger)
forall (a :: S -> Type) (s :: S). Term s (PArray a :--> PInteger)
plengthOfArray Term s (PArray a :--> PInteger)
-> Term s (PArray 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 (PArray a)
arr) Term s ((PInteger :--> a) :--> r)
-> Term s (PInteger :--> a) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (PArray a :--> (PInteger :--> a))
forall (a :: S -> Type) (s :: S).
Term s (PArray a :--> (PInteger :--> a))
pindexArray Term s (PArray a :--> (PInteger :--> a))
-> Term s (PArray a) -> Term s (PInteger :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PArray a)
arr

{- | Given a builtin list, construct the equivalent pull array. Uses
'plistToArray' internally.

\(\Theta(1)\) space complexity, \(\Theta(n)\) time complexity.

@since 1.12.0
-}
pfromList ::
  forall (a :: S -> Type) (s :: S).
  Term s (PBuiltinList a) ->
  Term s (PPullArray a)
pfromList :: forall (a :: S -> Type) (s :: S).
Term s (PBuiltinList a) -> Term s (PPullArray a)
pfromList Term s (PBuiltinList a)
ell = Term s (PArray a) -> Term s (PPullArray a)
forall (a :: S -> Type) (s :: S).
Term s (PArray a) -> Term s (PPullArray a)
pfromArray (Term s (PBuiltinList a :--> PArray a)
forall (a :: S -> Type) (s :: S).
Term s (PBuiltinList a :--> PArray a)
plistToArray Term s (PBuiltinList a :--> PArray a)
-> Term s (PBuiltinList a) -> Term s (PArray a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList a)
ell)

{- | Given a \'transformation function\' and a pull array, construct a new pull
array where each element of the argument array has been transformed without
moving it.

\(\Theta(1)\) space and time complexity.

@since 1.12.0
-}
pmapArray ::
  forall (a :: S -> Type) (b :: S -> Type) (s :: S).
  Term s (a :--> b) ->
  Term s (PPullArray a) ->
  Term s (PPullArray b)
pmapArray :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s (a :--> b) -> Term s (PPullArray a) -> Term s (PPullArray b)
pmapArray Term s (a :--> b)
f Term s (PPullArray a)
arr = Term s (PPullArray a)
-> (PPullArray a s -> Term s (PPullArray b))
-> Term s (PPullArray b)
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 (PPullArray a)
arr ((PPullArray a s -> Term s (PPullArray b))
 -> Term s (PPullArray b))
-> (PPullArray a s -> Term s (PPullArray b))
-> Term s (PPullArray b)
forall a b. (a -> b) -> a -> b
$ \(PPullArray forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
g) ->
  PPullArray b s -> Term s (PPullArray b)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PPullArray b s -> Term s (PPullArray b))
-> PPullArray b s -> Term s (PPullArray b)
forall a b. (a -> b) -> a -> b
$ (forall (r :: S -> Type).
 Term s ((PNatural :--> ((PInteger :--> b) :--> r)) :--> r))
-> PPullArray b s
forall (a :: S -> Type) (s :: S).
(forall (r :: S -> Type).
 Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> PPullArray a s
PPullArray ((forall (r :: S -> Type).
  Term s ((PNatural :--> ((PInteger :--> b) :--> r)) :--> r))
 -> PPullArray b s)
-> (forall (r :: S -> Type).
    Term s ((PNatural :--> ((PInteger :--> b) :--> r)) :--> r))
-> PPullArray b s
forall a b. (a -> b) -> a -> b
$ (Term s (PNatural :--> ((PInteger :--> b) :--> r)) -> Term s r)
-> Term s ((PNatural :--> ((PInteger :--> b) :--> r)) :--> 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 r) -> Term s (c :--> r)
plam ((Term s (PNatural :--> ((PInteger :--> b) :--> r)) -> Term s r)
 -> Term s ((PNatural :--> ((PInteger :--> b) :--> r)) :--> r))
-> (Term s (PNatural :--> ((PInteger :--> b) :--> r)) -> Term s r)
-> Term s ((PNatural :--> ((PInteger :--> b) :--> r)) :--> r)
forall a b. (a -> b) -> a -> b
$ \Term s (PNatural :--> ((PInteger :--> b) :--> r))
k ->
    Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
g Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
-> Term s (PNatural :--> ((PInteger :--> a) :--> r)) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PNatural -> Term s (PInteger :--> a) -> Term s r)
-> Term s (PNatural :--> ((PInteger :--> 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 (PInteger :--> a) -> Term s r)
-> Term s (c :--> ((PInteger :--> a) :--> r))
plam (\Term s PNatural
len Term s (PInteger :--> a)
h -> Term s (PNatural :--> ((PInteger :--> b) :--> r))
k Term s (PNatural :--> ((PInteger :--> b) :--> r))
-> Term s PNatural -> Term s ((PInteger :--> b) :--> r)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PNatural
len Term s ((PInteger :--> b) :--> r)
-> Term s (PInteger :--> b) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s ((a :--> b) :--> ((PInteger :--> a) :--> (PInteger :--> b)))
forall (s' :: S).
Term
  s' ((a :--> b) :--> ((PInteger :--> a) :--> (PInteger :--> b)))
pcompose Term s ((a :--> b) :--> ((PInteger :--> a) :--> (PInteger :--> b)))
-> Term s (a :--> b)
-> Term s ((PInteger :--> a) :--> (PInteger :--> 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 ((PInteger :--> a) :--> (PInteger :--> b))
-> Term s (PInteger :--> a) -> Term s (PInteger :--> b)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInteger :--> a)
h)
  where
    pcompose :: forall (s' :: S). Term s' ((a :--> b) :--> (PInteger :--> a) :--> PInteger :--> b)
    pcompose :: forall (s' :: S).
Term
  s' ((a :--> b) :--> ((PInteger :--> a) :--> (PInteger :--> b)))
pcompose = (forall (s' :: S).
 Term
   s' ((a :--> b) :--> ((PInteger :--> a) :--> (PInteger :--> b))))
-> Term
     s' ((a :--> b) :--> ((PInteger :--> a) :--> (PInteger :--> b)))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S).
  Term
    s' ((a :--> b) :--> ((PInteger :--> a) :--> (PInteger :--> b))))
 -> Term
      s' ((a :--> b) :--> ((PInteger :--> a) :--> (PInteger :--> b))))
-> (forall (s' :: S).
    Term
      s' ((a :--> b) :--> ((PInteger :--> a) :--> (PInteger :--> b))))
-> Term
     s' ((a :--> b) :--> ((PInteger :--> a) :--> (PInteger :--> b)))
forall a b. (a -> b) -> a -> b
$ (Term s' (a :--> b)
 -> Term s' (PInteger :--> a) -> Term s' PInteger -> Term s' b)
-> Term
     s' ((a :--> b) :--> ((PInteger :--> a) :--> (PInteger :--> 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' (PInteger :--> a) -> Term s' PInteger -> Term s' b)
-> Term s' (c :--> ((PInteger :--> a) :--> (PInteger :--> b)))
plam ((Term s' (a :--> b)
  -> Term s' (PInteger :--> a) -> Term s' PInteger -> Term s' b)
 -> Term
      s' ((a :--> b) :--> ((PInteger :--> a) :--> (PInteger :--> b))))
-> (Term s' (a :--> b)
    -> Term s' (PInteger :--> a) -> Term s' PInteger -> Term s' b)
-> Term
     s' ((a :--> b) :--> ((PInteger :--> a) :--> (PInteger :--> b)))
forall a b. (a -> b) -> a -> b
$ \Term s' (a :--> b)
f1 Term s' (PInteger :--> a)
f2 Term s' PInteger
i -> Term s' (a :--> b)
f1 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' (PInteger :--> a)
f2 Term s' (PInteger :--> a) -> Term s' PInteger -> Term s' a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' PInteger
i

{- | As 'pmapArray', but with an index-aware \'transformer function\'.

@since 1.12.0
-}
pimapArray ::
  forall (a :: S -> Type) (b :: S -> Type) (s :: S).
  Term s (PInteger :--> a :--> b) ->
  Term s (PPullArray a) ->
  Term s (PPullArray b)
pimapArray :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s (PInteger :--> (a :--> b))
-> Term s (PPullArray a) -> Term s (PPullArray b)
pimapArray Term s (PInteger :--> (a :--> b))
f Term s (PPullArray a)
arr = Term s (PPullArray a)
-> (PPullArray a s -> Term s (PPullArray b))
-> Term s (PPullArray b)
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 (PPullArray a)
arr ((PPullArray a s -> Term s (PPullArray b))
 -> Term s (PPullArray b))
-> (PPullArray a s -> Term s (PPullArray b))
-> Term s (PPullArray b)
forall a b. (a -> b) -> a -> b
$ \(PPullArray forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
g) ->
  PPullArray b s -> Term s (PPullArray b)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PPullArray b s -> Term s (PPullArray b))
-> PPullArray b s -> Term s (PPullArray b)
forall a b. (a -> b) -> a -> b
$ (forall (r :: S -> Type).
 Term s ((PNatural :--> ((PInteger :--> b) :--> r)) :--> r))
-> PPullArray b s
forall (a :: S -> Type) (s :: S).
(forall (r :: S -> Type).
 Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> PPullArray a s
PPullArray ((forall (r :: S -> Type).
  Term s ((PNatural :--> ((PInteger :--> b) :--> r)) :--> r))
 -> PPullArray b s)
-> (forall (r :: S -> Type).
    Term s ((PNatural :--> ((PInteger :--> b) :--> r)) :--> r))
-> PPullArray b s
forall a b. (a -> b) -> a -> b
$ (Term s (PNatural :--> ((PInteger :--> b) :--> r)) -> Term s r)
-> Term s ((PNatural :--> ((PInteger :--> b) :--> r)) :--> 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 r) -> Term s (c :--> r)
plam ((Term s (PNatural :--> ((PInteger :--> b) :--> r)) -> Term s r)
 -> Term s ((PNatural :--> ((PInteger :--> b) :--> r)) :--> r))
-> (Term s (PNatural :--> ((PInteger :--> b) :--> r)) -> Term s r)
-> Term s ((PNatural :--> ((PInteger :--> b) :--> r)) :--> r)
forall a b. (a -> b) -> a -> b
$ \Term s (PNatural :--> ((PInteger :--> b) :--> r))
k ->
    Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
g Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
-> Term s (PNatural :--> ((PInteger :--> a) :--> r)) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PNatural -> Term s (PInteger :--> a) -> Term s r)
-> Term s (PNatural :--> ((PInteger :--> 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 (PInteger :--> a) -> Term s r)
-> Term s (c :--> ((PInteger :--> a) :--> r))
plam (\Term s PNatural
len Term s (PInteger :--> a)
h -> Term s (PNatural :--> ((PInteger :--> b) :--> r))
k Term s (PNatural :--> ((PInteger :--> b) :--> r))
-> Term s PNatural -> Term s ((PInteger :--> b) :--> r)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PNatural
len Term s ((PInteger :--> b) :--> r)
-> Term s (PInteger :--> b) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term
  s
  ((PInteger :--> (a :--> b))
   :--> ((PInteger :--> a) :--> (PInteger :--> b)))
forall (s' :: S).
Term
  s'
  ((PInteger :--> (a :--> b))
   :--> ((PInteger :--> a) :--> (PInteger :--> b)))
picompose Term
  s
  ((PInteger :--> (a :--> b))
   :--> ((PInteger :--> a) :--> (PInteger :--> b)))
-> Term s (PInteger :--> (a :--> b))
-> Term s ((PInteger :--> a) :--> (PInteger :--> b))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInteger :--> (a :--> b))
f Term s ((PInteger :--> a) :--> (PInteger :--> b))
-> Term s (PInteger :--> a) -> Term s (PInteger :--> b)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInteger :--> a)
h)
  where
    picompose :: forall (s' :: S). Term s' ((PInteger :--> a :--> b) :--> (PInteger :--> a) :--> PInteger :--> b)
    picompose :: forall (s' :: S).
Term
  s'
  ((PInteger :--> (a :--> b))
   :--> ((PInteger :--> a) :--> (PInteger :--> b)))
picompose = (forall (s' :: S).
 Term
   s'
   ((PInteger :--> (a :--> b))
    :--> ((PInteger :--> a) :--> (PInteger :--> b))))
-> Term
     s'
     ((PInteger :--> (a :--> b))
      :--> ((PInteger :--> a) :--> (PInteger :--> b)))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S).
  Term
    s'
    ((PInteger :--> (a :--> b))
     :--> ((PInteger :--> a) :--> (PInteger :--> b))))
 -> Term
      s'
      ((PInteger :--> (a :--> b))
       :--> ((PInteger :--> a) :--> (PInteger :--> b))))
-> (forall (s' :: S).
    Term
      s'
      ((PInteger :--> (a :--> b))
       :--> ((PInteger :--> a) :--> (PInteger :--> b))))
-> Term
     s'
     ((PInteger :--> (a :--> b))
      :--> ((PInteger :--> a) :--> (PInteger :--> b)))
forall a b. (a -> b) -> a -> b
$ (Term s' (PInteger :--> (a :--> b))
 -> Term s' (PInteger :--> a) -> Term s' PInteger -> Term s' b)
-> Term
     s'
     ((PInteger :--> (a :--> b))
      :--> ((PInteger :--> a) :--> (PInteger :--> 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' (PInteger :--> a) -> Term s' PInteger -> Term s' b)
-> Term s' (c :--> ((PInteger :--> a) :--> (PInteger :--> b)))
plam ((Term s' (PInteger :--> (a :--> b))
  -> Term s' (PInteger :--> a) -> Term s' PInteger -> Term s' b)
 -> Term
      s'
      ((PInteger :--> (a :--> b))
       :--> ((PInteger :--> a) :--> (PInteger :--> b))))
-> (Term s' (PInteger :--> (a :--> b))
    -> Term s' (PInteger :--> a) -> Term s' PInteger -> Term s' b)
-> Term
     s'
     ((PInteger :--> (a :--> b))
      :--> ((PInteger :--> a) :--> (PInteger :--> b)))
forall a b. (a -> b) -> a -> b
$ \Term s' (PInteger :--> (a :--> b))
f1 Term s' (PInteger :--> a)
f2 Term s' PInteger
i -> Term s' (PInteger :--> (a :--> b))
f1 Term s' (PInteger :--> (a :--> b))
-> Term s' PInteger -> 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' PInteger
i 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' (PInteger :--> a)
f2 Term s' (PInteger :--> a) -> Term s' PInteger -> Term s' a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' PInteger
i

{- | Given a size limit \(k\) and a pull array of length \(n\), construct a new
pull array that consists of the first \(\min \{k, n\}\) elements of the
argument pull array, at the same indexes.

\(\Theta(1)\) space and time complexity.

@since 1.12.0
-}
ptakeArray ::
  forall (a :: S -> Type) (s :: S).
  Term s PNatural ->
  Term s (PPullArray a) ->
  Term s (PPullArray a)
ptakeArray :: forall (a :: S -> Type) (s :: S).
Term s PNatural -> Term s (PPullArray a) -> Term s (PPullArray a)
ptakeArray Term s PNatural
lim Term s (PPullArray a)
arr = Term s (PPullArray a)
-> (PPullArray a s -> Term s (PPullArray a))
-> Term s (PPullArray a)
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 (PPullArray a)
arr ((PPullArray a s -> Term s (PPullArray a))
 -> Term s (PPullArray a))
-> (PPullArray a s -> Term s (PPullArray a))
-> Term s (PPullArray a)
forall a b. (a -> b) -> a -> b
$ \(PPullArray forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
g) ->
  PPullArray a s -> Term s (PPullArray a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PPullArray a s -> Term s (PPullArray a))
-> PPullArray a s -> Term s (PPullArray a)
forall a b. (a -> b) -> a -> b
$ (forall (r :: S -> Type).
 Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> PPullArray a s
forall (a :: S -> Type) (s :: S).
(forall (r :: S -> Type).
 Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> PPullArray a s
PPullArray ((forall (r :: S -> Type).
  Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
 -> PPullArray a s)
-> (forall (r :: S -> Type).
    Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> PPullArray a s
forall a b. (a -> b) -> a -> b
$ (Term s (PNatural :--> ((PInteger :--> a) :--> r)) -> Term s r)
-> Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> 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 r) -> Term s (c :--> r)
plam ((Term s (PNatural :--> ((PInteger :--> a) :--> r)) -> Term s r)
 -> Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> (Term s (PNatural :--> ((PInteger :--> a) :--> r)) -> Term s r)
-> Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
forall a b. (a -> b) -> a -> b
$ \Term s (PNatural :--> ((PInteger :--> a) :--> r))
k ->
    Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
g Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
-> Term s (PNatural :--> ((PInteger :--> a) :--> r)) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PNatural -> Term s (PInteger :--> a) -> Term s r)
-> Term s (PNatural :--> ((PInteger :--> 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 (PInteger :--> a) -> Term s r)
-> Term s (c :--> ((PInteger :--> a) :--> r))
plam (\Term s PNatural
len Term s (PInteger :--> a)
h -> Term s (PNatural :--> ((PInteger :--> a) :--> r))
k Term s (PNatural :--> ((PInteger :--> a) :--> r))
-> Term s PNatural -> Term s ((PInteger :--> a) :--> r)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PNatural -> Term s PNatural -> Term s PNatural
forall (s :: S).
Term s PNatural -> Term s PNatural -> Term s PNatural
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s t
pmin Term s PNatural
lim Term s PNatural
len Term s ((PInteger :--> a) :--> r)
-> Term s (PInteger :--> a) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInteger :--> a)
h)

{- | Given a desired number of discarded elements \(k\) and a pull array of length
\(n\), construct a new pull array that consists of all but the first \(min
\{k, n\}\) elements of the argument pull array, with indexes appropriately
offset.

\(\Theta(1)\) space and time complexity.

@since 1.12.0
-}
pdropArray ::
  forall (a :: S -> Type) (s :: S).
  Term s PNatural ->
  Term s (PPullArray a) ->
  Term s (PPullArray a)
pdropArray :: forall (a :: S -> Type) (s :: S).
Term s PNatural -> Term s (PPullArray a) -> Term s (PPullArray a)
pdropArray Term s PNatural
dropped Term s (PPullArray a)
arr = Term s (PPullArray a)
-> (PPullArray a s -> Term s (PPullArray a))
-> Term s (PPullArray a)
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 (PPullArray a)
arr ((PPullArray a s -> Term s (PPullArray a))
 -> Term s (PPullArray a))
-> (PPullArray a s -> Term s (PPullArray a))
-> Term s (PPullArray a)
forall a b. (a -> b) -> a -> b
$ \(PPullArray forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
g) ->
  PPullArray a s -> Term s (PPullArray a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PPullArray a s -> Term s (PPullArray a))
-> PPullArray a s -> Term s (PPullArray a)
forall a b. (a -> b) -> a -> b
$ (forall (r :: S -> Type).
 Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> PPullArray a s
forall (a :: S -> Type) (s :: S).
(forall (r :: S -> Type).
 Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> PPullArray a s
PPullArray ((forall (r :: S -> Type).
  Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
 -> PPullArray a s)
-> (forall (r :: S -> Type).
    Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> PPullArray a s
forall a b. (a -> b) -> a -> b
$ (Term s (PNatural :--> ((PInteger :--> a) :--> r)) -> Term s r)
-> Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> 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 r) -> Term s (c :--> r)
plam ((Term s (PNatural :--> ((PInteger :--> a) :--> r)) -> Term s r)
 -> Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> (Term s (PNatural :--> ((PInteger :--> a) :--> r)) -> Term s r)
-> Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
forall a b. (a -> b) -> a -> b
$ \Term s (PNatural :--> ((PInteger :--> a) :--> r))
k ->
    Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
g Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
-> Term s (PNatural :--> ((PInteger :--> a) :--> r)) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PNatural -> Term s (PInteger :--> a) -> Term s r)
-> Term s (PNatural :--> ((PInteger :--> 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 (PInteger :--> a) -> Term s r)
-> Term s (c :--> ((PInteger :--> a) :--> r))
plam (\Term s PNatural
len Term s (PInteger :--> a)
h -> Term s (PNatural :--> ((PInteger :--> a) :--> r))
k Term s (PNatural :--> ((PInteger :--> a) :--> r))
-> Term s PNatural -> Term s ((PInteger :--> a) :--> r)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PNatural -> Term s PNatural -> Term s PNatural
pdoz Term s PNatural
len Term s PNatural
dropped Term s ((PInteger :--> a) :--> r)
-> Term s (PInteger :--> a) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s ((PInteger :--> a) :--> (PNatural :--> (PInteger :--> a)))
forall (s' :: S).
Term s' ((PInteger :--> a) :--> (PNatural :--> (PInteger :--> a)))
go Term s ((PInteger :--> a) :--> (PNatural :--> (PInteger :--> a)))
-> Term s (PInteger :--> a)
-> Term s (PNatural :--> (PInteger :--> a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInteger :--> a)
h Term s (PNatural :--> (PInteger :--> a))
-> Term s PNatural -> Term s (PInteger :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PNatural
dropped)
  where
    pdoz :: Term s PNatural -> Term s PNatural -> Term s PNatural
    pdoz :: Term s PNatural -> Term s PNatural -> Term s PNatural
pdoz Term s PNatural
x Term s PNatural
y = Term s PInteger
-> (Term s PInteger -> Term s PNatural) -> Term s PNatural
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (forall (a :: S -> Type) (b :: S -> Type) (s :: S).
PSubtype a b =>
Term s b -> Term s a
pupcast @PInteger Term s PNatural
x Term s PInteger -> Term s PInteger -> Term s PInteger
forall (s :: S).
Term s PInteger -> Term s PInteger -> Term s PInteger
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s a -> Term s a -> Term s a
#- Term s PNatural -> Term s PInteger
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
PSubtype a b =>
Term s b -> Term s a
pupcast Term s PNatural
y) ((Term s PInteger -> Term s PNatural) -> Term s PNatural)
-> (Term s PInteger -> Term s PNatural) -> Term s PNatural
forall a b. (a -> b) -> a -> b
$ \Term s PInteger
result ->
      Term s PInteger -> Term s PNatural
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s PInteger -> Term s PNatural)
-> Term s PInteger -> Term s PNatural
forall a b. (a -> b) -> a -> b
$
        Term s PBool
-> Term s PInteger -> Term s PInteger -> Term s PInteger
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
          (Term s PInteger
result 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).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= (Term s PInteger
-1))
          Term s PInteger
0
          Term s PInteger
result
    go :: forall (s' :: S). Term s' ((PInteger :--> a) :--> PNatural :--> PInteger :--> a)
    go :: forall (s' :: S).
Term s' ((PInteger :--> a) :--> (PNatural :--> (PInteger :--> a)))
go = (forall (s' :: S).
 Term s' ((PInteger :--> a) :--> (PNatural :--> (PInteger :--> a))))
-> Term
     s' ((PInteger :--> a) :--> (PNatural :--> (PInteger :--> a)))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S).
  Term s' ((PInteger :--> a) :--> (PNatural :--> (PInteger :--> a))))
 -> Term
      s' ((PInteger :--> a) :--> (PNatural :--> (PInteger :--> a))))
-> (forall (s' :: S).
    Term s' ((PInteger :--> a) :--> (PNatural :--> (PInteger :--> a))))
-> Term
     s' ((PInteger :--> a) :--> (PNatural :--> (PInteger :--> a)))
forall a b. (a -> b) -> a -> b
$ (Term s' (PInteger :--> a)
 -> Term s' PNatural -> Term s' PInteger -> Term s' a)
-> Term
     s' ((PInteger :--> a) :--> (PNatural :--> (PInteger :--> 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' PNatural -> Term s' PInteger -> Term s' a)
-> Term s' (c :--> (PNatural :--> (PInteger :--> a)))
plam ((Term s' (PInteger :--> a)
  -> Term s' PNatural -> Term s' PInteger -> Term s' a)
 -> Term
      s' ((PInteger :--> a) :--> (PNatural :--> (PInteger :--> a))))
-> (Term s' (PInteger :--> a)
    -> Term s' PNatural -> Term s' PInteger -> Term s' a)
-> Term
     s' ((PInteger :--> a) :--> (PNatural :--> (PInteger :--> a)))
forall a b. (a -> b) -> a -> b
$ \Term s' (PInteger :--> a)
f Term s' PNatural
x Term s' PInteger
i -> Term s' (PInteger :--> a)
f Term s' (PInteger :--> a) -> Term s' PInteger -> Term s' 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' PInteger -> Term s' PInteger -> Term s' PInteger
forall (s :: S).
Term s PInteger -> Term s PInteger -> Term s PInteger
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
#+ forall (a :: S -> Type) (b :: S -> Type) (s :: S).
PSubtype a b =>
Term s b -> Term s a
pupcast @PInteger Term s' PNatural
x)

{- | Given a \'combining function\' and two pull arrays, produce a new pull
array whose length is the minimum of the lengths of the arguments, and whose
elements are applications of the \'combining function\' at the respective
indexes of the argument arrays.

\(\Theta(1)\) space and time complexity.

@since 1.12.0
-}
pzipWithArray ::
  forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
  Term s (a :--> b :--> c) ->
  Term s (PPullArray a) ->
  Term s (PPullArray b) ->
  Term s (PPullArray c)
pzipWithArray :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
Term s (a :--> (b :--> c))
-> Term s (PPullArray a)
-> Term s (PPullArray b)
-> Term s (PPullArray c)
pzipWithArray Term s (a :--> (b :--> c))
f Term s (PPullArray a)
arr1 Term s (PPullArray b)
arr2 = Term s (PPullArray a)
-> (PPullArray a s -> Term s (PPullArray c))
-> Term s (PPullArray c)
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 (PPullArray a)
arr1 ((PPullArray a s -> Term s (PPullArray c))
 -> Term s (PPullArray c))
-> (PPullArray a s -> Term s (PPullArray c))
-> Term s (PPullArray c)
forall a b. (a -> b) -> a -> b
$ \(PPullArray forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
k1) ->
  Term s (PPullArray b)
-> (PPullArray b s -> Term s (PPullArray c))
-> Term s (PPullArray c)
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 (PPullArray b)
arr2 ((PPullArray b s -> Term s (PPullArray c))
 -> Term s (PPullArray c))
-> (PPullArray b s -> Term s (PPullArray c))
-> Term s (PPullArray c)
forall a b. (a -> b) -> a -> b
$ \(PPullArray forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> b) :--> r)) :--> r)
k2) ->
    PPullArray c s -> Term s (PPullArray c)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PPullArray c s -> Term s (PPullArray c))
-> PPullArray c s -> Term s (PPullArray c)
forall a b. (a -> b) -> a -> b
$ (forall (r :: S -> Type).
 Term s ((PNatural :--> ((PInteger :--> c) :--> r)) :--> r))
-> PPullArray c s
forall (a :: S -> Type) (s :: S).
(forall (r :: S -> Type).
 Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> PPullArray a s
PPullArray ((forall (r :: S -> Type).
  Term s ((PNatural :--> ((PInteger :--> c) :--> r)) :--> r))
 -> PPullArray c s)
-> (forall (r :: S -> Type).
    Term s ((PNatural :--> ((PInteger :--> c) :--> r)) :--> r))
-> PPullArray c s
forall a b. (a -> b) -> a -> b
$ (Term s (PNatural :--> ((PInteger :--> c) :--> r)) -> Term s r)
-> Term s ((PNatural :--> ((PInteger :--> c) :--> r)) :--> 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 r) -> Term s (c :--> r)
plam ((Term s (PNatural :--> ((PInteger :--> c) :--> r)) -> Term s r)
 -> Term s ((PNatural :--> ((PInteger :--> c) :--> r)) :--> r))
-> (Term s (PNatural :--> ((PInteger :--> c) :--> r)) -> Term s r)
-> Term s ((PNatural :--> ((PInteger :--> c) :--> r)) :--> r)
forall a b. (a -> b) -> a -> b
$ \Term s (PNatural :--> ((PInteger :--> c) :--> r))
k ->
      Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
k1
        # plam
          ( \len1 h1 ->
              k2
                # plam
                  ( \len2 h2 ->
                      k # pmin len1 len2 #$ go # f # h1 # h2
                  )
          )
  where
    go ::
      forall (s' :: S).
      Term s' ((a :--> b :--> c) :--> (PInteger :--> a) :--> (PInteger :--> b) :--> PInteger :--> c)
    go :: forall (s' :: S).
Term
  s'
  ((a :--> (b :--> c))
   :--> ((PInteger :--> a)
         :--> ((PInteger :--> b) :--> (PInteger :--> c))))
go = (forall (s' :: S).
 Term
   s'
   ((a :--> (b :--> c))
    :--> ((PInteger :--> a)
          :--> ((PInteger :--> b) :--> (PInteger :--> c)))))
-> Term
     s'
     ((a :--> (b :--> c))
      :--> ((PInteger :--> a)
            :--> ((PInteger :--> b) :--> (PInteger :--> c))))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S).
  Term
    s'
    ((a :--> (b :--> c))
     :--> ((PInteger :--> a)
           :--> ((PInteger :--> b) :--> (PInteger :--> c)))))
 -> Term
      s'
      ((a :--> (b :--> c))
       :--> ((PInteger :--> a)
             :--> ((PInteger :--> b) :--> (PInteger :--> c)))))
-> (forall (s' :: S).
    Term
      s'
      ((a :--> (b :--> c))
       :--> ((PInteger :--> a)
             :--> ((PInteger :--> b) :--> (PInteger :--> c)))))
-> Term
     s'
     ((a :--> (b :--> c))
      :--> ((PInteger :--> a)
            :--> ((PInteger :--> b) :--> (PInteger :--> c))))
forall a b. (a -> b) -> a -> b
$ (Term s' (a :--> (b :--> c))
 -> Term s' (PInteger :--> a)
 -> Term s' (PInteger :--> b)
 -> Term s' PInteger
 -> Term s' c)
-> Term
     s'
     ((a :--> (b :--> c))
      :--> ((PInteger :--> a)
            :--> ((PInteger :--> b) :--> (PInteger :--> 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' (PInteger :--> a)
 -> Term s' (PInteger :--> b)
 -> Term s' PInteger
 -> Term s' c)
-> Term
     s'
     (c
      :--> ((PInteger :--> a)
            :--> ((PInteger :--> b) :--> (PInteger :--> c))))
plam ((Term s' (a :--> (b :--> c))
  -> Term s' (PInteger :--> a)
  -> Term s' (PInteger :--> b)
  -> Term s' PInteger
  -> Term s' c)
 -> Term
      s'
      ((a :--> (b :--> c))
       :--> ((PInteger :--> a)
             :--> ((PInteger :--> b) :--> (PInteger :--> c)))))
-> (Term s' (a :--> (b :--> c))
    -> Term s' (PInteger :--> a)
    -> Term s' (PInteger :--> b)
    -> Term s' PInteger
    -> Term s' c)
-> Term
     s'
     ((a :--> (b :--> c))
      :--> ((PInteger :--> a)
            :--> ((PInteger :--> b) :--> (PInteger :--> c))))
forall a b. (a -> b) -> a -> b
$ \Term s' (a :--> (b :--> c))
combine Term s' (PInteger :--> a)
ix1 Term s' (PInteger :--> b)
ix2 Term s' PInteger
i -> Term s' (a :--> (b :--> c))
combine 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' (PInteger :--> a)
ix1 Term s' (PInteger :--> a) -> Term s' PInteger -> Term s' 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' (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' (PInteger :--> b)
ix2 Term s' (PInteger :--> b) -> Term s' PInteger -> Term s' b
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' PInteger
i

{- | As 'pzipWithArray', but with an index-aware \'combining function\'.

@since 1.12.0
-}
pizipWithArray ::
  forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
  Term s (PInteger :--> a :--> b :--> c) ->
  Term s (PPullArray a) ->
  Term s (PPullArray b) ->
  Term s (PPullArray c)
pizipWithArray :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
Term s (PInteger :--> (a :--> (b :--> c)))
-> Term s (PPullArray a)
-> Term s (PPullArray b)
-> Term s (PPullArray c)
pizipWithArray Term s (PInteger :--> (a :--> (b :--> c)))
f Term s (PPullArray a)
arr1 Term s (PPullArray b)
arr2 = Term s (PPullArray a)
-> (PPullArray a s -> Term s (PPullArray c))
-> Term s (PPullArray c)
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 (PPullArray a)
arr1 ((PPullArray a s -> Term s (PPullArray c))
 -> Term s (PPullArray c))
-> (PPullArray a s -> Term s (PPullArray c))
-> Term s (PPullArray c)
forall a b. (a -> b) -> a -> b
$ \(PPullArray forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
k1) ->
  Term s (PPullArray b)
-> (PPullArray b s -> Term s (PPullArray c))
-> Term s (PPullArray c)
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 (PPullArray b)
arr2 ((PPullArray b s -> Term s (PPullArray c))
 -> Term s (PPullArray c))
-> (PPullArray b s -> Term s (PPullArray c))
-> Term s (PPullArray c)
forall a b. (a -> b) -> a -> b
$ \(PPullArray forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> b) :--> r)) :--> r)
k2) ->
    PPullArray c s -> Term s (PPullArray c)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PPullArray c s -> Term s (PPullArray c))
-> PPullArray c s -> Term s (PPullArray c)
forall a b. (a -> b) -> a -> b
$ (forall (r :: S -> Type).
 Term s ((PNatural :--> ((PInteger :--> c) :--> r)) :--> r))
-> PPullArray c s
forall (a :: S -> Type) (s :: S).
(forall (r :: S -> Type).
 Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r))
-> PPullArray a s
PPullArray ((forall (r :: S -> Type).
  Term s ((PNatural :--> ((PInteger :--> c) :--> r)) :--> r))
 -> PPullArray c s)
-> (forall (r :: S -> Type).
    Term s ((PNatural :--> ((PInteger :--> c) :--> r)) :--> r))
-> PPullArray c s
forall a b. (a -> b) -> a -> b
$ (Term s (PNatural :--> ((PInteger :--> c) :--> r)) -> Term s r)
-> Term s ((PNatural :--> ((PInteger :--> c) :--> r)) :--> 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 r) -> Term s (c :--> r)
plam ((Term s (PNatural :--> ((PInteger :--> c) :--> r)) -> Term s r)
 -> Term s ((PNatural :--> ((PInteger :--> c) :--> r)) :--> r))
-> (Term s (PNatural :--> ((PInteger :--> c) :--> r)) -> Term s r)
-> Term s ((PNatural :--> ((PInteger :--> c) :--> r)) :--> r)
forall a b. (a -> b) -> a -> b
$ \Term s (PNatural :--> ((PInteger :--> c) :--> r))
k ->
      Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
k1
        # plam
          ( \len1 h1 ->
              k2
                # plam
                  ( \len2 h2 ->
                      k # pmin len1 len2 #$ go # f # h1 # h2
                  )
          )
  where
    go ::
      forall (s' :: S).
      Term s' ((PInteger :--> a :--> b :--> c) :--> (PInteger :--> a) :--> (PInteger :--> b) :--> PInteger :--> c)
    go :: forall (s' :: S).
Term
  s'
  ((PInteger :--> (a :--> (b :--> c)))
   :--> ((PInteger :--> a)
         :--> ((PInteger :--> b) :--> (PInteger :--> c))))
go = (forall (s' :: S).
 Term
   s'
   ((PInteger :--> (a :--> (b :--> c)))
    :--> ((PInteger :--> a)
          :--> ((PInteger :--> b) :--> (PInteger :--> c)))))
-> Term
     s'
     ((PInteger :--> (a :--> (b :--> c)))
      :--> ((PInteger :--> a)
            :--> ((PInteger :--> b) :--> (PInteger :--> c))))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S).
  Term
    s'
    ((PInteger :--> (a :--> (b :--> c)))
     :--> ((PInteger :--> a)
           :--> ((PInteger :--> b) :--> (PInteger :--> c)))))
 -> Term
      s'
      ((PInteger :--> (a :--> (b :--> c)))
       :--> ((PInteger :--> a)
             :--> ((PInteger :--> b) :--> (PInteger :--> c)))))
-> (forall (s' :: S).
    Term
      s'
      ((PInteger :--> (a :--> (b :--> c)))
       :--> ((PInteger :--> a)
             :--> ((PInteger :--> b) :--> (PInteger :--> c)))))
-> Term
     s'
     ((PInteger :--> (a :--> (b :--> c)))
      :--> ((PInteger :--> a)
            :--> ((PInteger :--> b) :--> (PInteger :--> c))))
forall a b. (a -> b) -> a -> b
$ (Term s' (PInteger :--> (a :--> (b :--> c)))
 -> Term s' (PInteger :--> a)
 -> Term s' (PInteger :--> b)
 -> Term s' PInteger
 -> Term s' c)
-> Term
     s'
     ((PInteger :--> (a :--> (b :--> c)))
      :--> ((PInteger :--> a)
            :--> ((PInteger :--> b) :--> (PInteger :--> 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' (PInteger :--> a)
 -> Term s' (PInteger :--> b)
 -> Term s' PInteger
 -> Term s' c)
-> Term
     s'
     (c
      :--> ((PInteger :--> a)
            :--> ((PInteger :--> b) :--> (PInteger :--> c))))
plam ((Term s' (PInteger :--> (a :--> (b :--> c)))
  -> Term s' (PInteger :--> a)
  -> Term s' (PInteger :--> b)
  -> Term s' PInteger
  -> Term s' c)
 -> Term
      s'
      ((PInteger :--> (a :--> (b :--> c)))
       :--> ((PInteger :--> a)
             :--> ((PInteger :--> b) :--> (PInteger :--> c)))))
-> (Term s' (PInteger :--> (a :--> (b :--> c)))
    -> Term s' (PInteger :--> a)
    -> Term s' (PInteger :--> b)
    -> Term s' PInteger
    -> Term s' c)
-> Term
     s'
     ((PInteger :--> (a :--> (b :--> c)))
      :--> ((PInteger :--> a)
            :--> ((PInteger :--> b) :--> (PInteger :--> c))))
forall a b. (a -> b) -> a -> b
$ \Term s' (PInteger :--> (a :--> (b :--> c)))
combine Term s' (PInteger :--> a)
ix1 Term s' (PInteger :--> b)
ix2 Term s' PInteger
i -> Term s' (PInteger :--> (a :--> (b :--> c)))
combine Term s' (PInteger :--> (a :--> (b :--> c)))
-> Term s' PInteger -> Term s' (a :--> (b :--> c))
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' (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' (PInteger :--> a)
ix1 Term s' (PInteger :--> a) -> Term s' PInteger -> Term s' 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' (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' (PInteger :--> b)
ix2 Term s' (PInteger :--> b) -> Term s' PInteger -> Term s' b
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' PInteger
i

{- | Given a \'combining function\' and a starting value, reduce the argument
array by repeatedly combining elements with the starting value. This is a
left fold: thus, it will start at the lowest index and work its way upward.

Assuming \(\Theta(k)\) cost in space, and \(\Theta(\ell)\) cost in time, per
application of the \'combining function\', \(\Theta(kn)\) space complexity
and \(\Theta(k\ell)\) time complexity.

@since 1.13.0
-}
pfoldArray ::
  forall (a :: S -> Type) (b :: S -> Type) (s :: S).
  Term s (b :--> a :--> b) ->
  Term s b ->
  Term s (PPullArray a) ->
  Term s b
pfoldArray :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s (b :--> (a :--> b))
-> Term s b -> Term s (PPullArray a) -> Term s b
pfoldArray Term s (b :--> (a :--> b))
f Term s b
x Term s (PPullArray a)
arr = Term s (PPullArray a) -> (PPullArray a s -> Term s b) -> Term s b
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 (PPullArray a)
arr ((PPullArray a s -> Term s b) -> Term s b)
-> (PPullArray a s -> Term s b) -> Term s b
forall a b. (a -> b) -> a -> b
$ \(PPullArray forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
k) ->
  Term s ((PNatural :--> ((PInteger :--> a) :--> b)) :--> b)
forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
k Term s ((PNatural :--> ((PInteger :--> a) :--> b)) :--> b)
-> Term s (PNatural :--> ((PInteger :--> a) :--> 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 PNatural -> Term s (PInteger :--> a) -> Term s b)
-> Term s (PNatural :--> ((PInteger :--> 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 (PInteger :--> a) -> Term s b)
-> Term s (c :--> ((PInteger :--> a) :--> b))
plam (\Term s PNatural
len Term s (PInteger :--> a)
h -> Term
  s
  ((b :--> (a :--> b))
   :--> ((PInteger :--> a)
         :--> (PInteger :--> (b :--> (PInteger :--> b)))))
forall (s' :: S).
Term
  s'
  ((b :--> (a :--> b))
   :--> ((PInteger :--> a)
         :--> (PInteger :--> (b :--> (PInteger :--> b)))))
go Term
  s
  ((b :--> (a :--> b))
   :--> ((PInteger :--> a)
         :--> (PInteger :--> (b :--> (PInteger :--> b)))))
-> Term s (b :--> (a :--> b))
-> Term
     s
     ((PInteger :--> a) :--> (PInteger :--> (b :--> (PInteger :--> 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
  ((PInteger :--> a) :--> (PInteger :--> (b :--> (PInteger :--> b))))
-> Term s (PInteger :--> a)
-> Term s (PInteger :--> (b :--> (PInteger :--> b)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInteger :--> a)
h Term s (PInteger :--> (b :--> (PInteger :--> b)))
-> Term s PInteger -> Term s (b :--> (PInteger :--> b))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PNatural -> Term s PInteger
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
PSubtype a b =>
Term s b -> Term s a
pupcast Term s PNatural
len Term s (b :--> (PInteger :--> b))
-> Term s b -> Term s (PInteger :--> b)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
x Term s (PInteger :--> b) -> Term s PInteger -> Term s b
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
0)
  where
    go ::
      forall (s' :: S).
      Term s' ((b :--> a :--> b) :--> (PInteger :--> a) :--> PInteger :--> b :--> PInteger :--> b)
    go :: forall (s' :: S).
Term
  s'
  ((b :--> (a :--> b))
   :--> ((PInteger :--> a)
         :--> (PInteger :--> (b :--> (PInteger :--> b)))))
go = (forall (s' :: S).
 Term
   s'
   ((b :--> (a :--> b))
    :--> ((PInteger :--> a)
          :--> (PInteger :--> (b :--> (PInteger :--> b))))))
-> Term
     s'
     ((b :--> (a :--> b))
      :--> ((PInteger :--> a)
            :--> (PInteger :--> (b :--> (PInteger :--> b)))))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S).
  Term
    s'
    ((b :--> (a :--> b))
     :--> ((PInteger :--> a)
           :--> (PInteger :--> (b :--> (PInteger :--> b))))))
 -> Term
      s'
      ((b :--> (a :--> b))
       :--> ((PInteger :--> a)
             :--> (PInteger :--> (b :--> (PInteger :--> b))))))
-> (forall (s' :: S).
    Term
      s'
      ((b :--> (a :--> b))
       :--> ((PInteger :--> a)
             :--> (PInteger :--> (b :--> (PInteger :--> b))))))
-> Term
     s'
     ((b :--> (a :--> b))
      :--> ((PInteger :--> a)
            :--> (PInteger :--> (b :--> (PInteger :--> b)))))
forall a b. (a -> b) -> a -> b
$ (Term
   s'
   ((b :--> (a :--> b))
    :--> ((PInteger :--> a)
          :--> (PInteger :--> (b :--> (PInteger :--> b)))))
 -> Term
      s'
      ((b :--> (a :--> b))
       :--> ((PInteger :--> a)
             :--> (PInteger :--> (b :--> (PInteger :--> b))))))
-> Term
     s'
     ((b :--> (a :--> b))
      :--> ((PInteger :--> a)
            :--> (PInteger :--> (b :--> (PInteger :--> b)))))
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(Term s (a :--> b) -> Term s (a :--> b)) -> Term s (a :--> b)
pfix ((Term
    s'
    ((b :--> (a :--> b))
     :--> ((PInteger :--> a)
           :--> (PInteger :--> (b :--> (PInteger :--> b)))))
  -> Term
       s'
       ((b :--> (a :--> b))
        :--> ((PInteger :--> a)
              :--> (PInteger :--> (b :--> (PInteger :--> b))))))
 -> Term
      s'
      ((b :--> (a :--> b))
       :--> ((PInteger :--> a)
             :--> (PInteger :--> (b :--> (PInteger :--> b))))))
-> (Term
      s'
      ((b :--> (a :--> b))
       :--> ((PInteger :--> a)
             :--> (PInteger :--> (b :--> (PInteger :--> b)))))
    -> Term
         s'
         ((b :--> (a :--> b))
          :--> ((PInteger :--> a)
                :--> (PInteger :--> (b :--> (PInteger :--> b))))))
-> Term
     s'
     ((b :--> (a :--> b))
      :--> ((PInteger :--> a)
            :--> (PInteger :--> (b :--> (PInteger :--> b)))))
forall a b. (a -> b) -> a -> b
$ \Term
  s'
  ((b :--> (a :--> b))
   :--> ((PInteger :--> a)
         :--> (PInteger :--> (b :--> (PInteger :--> b)))))
self -> (Term s' (b :--> (a :--> b))
 -> Term s' (PInteger :--> a)
 -> Term s' PInteger
 -> Term s' b
 -> Term s' PInteger
 -> Term s' b)
-> Term
     s'
     ((b :--> (a :--> b))
      :--> ((PInteger :--> a)
            :--> (PInteger :--> (b :--> (PInteger :--> 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' (PInteger :--> a)
 -> Term s' PInteger
 -> Term s' b
 -> Term s' PInteger
 -> Term s' b)
-> Term
     s'
     (c
      :--> ((PInteger :--> a)
            :--> (PInteger :--> (b :--> (PInteger :--> b)))))
plam ((Term s' (b :--> (a :--> b))
  -> Term s' (PInteger :--> a)
  -> Term s' PInteger
  -> Term s' b
  -> Term s' PInteger
  -> Term s' b)
 -> Term
      s'
      ((b :--> (a :--> b))
       :--> ((PInteger :--> a)
             :--> (PInteger :--> (b :--> (PInteger :--> b))))))
-> (Term s' (b :--> (a :--> b))
    -> Term s' (PInteger :--> a)
    -> Term s' PInteger
    -> Term s' b
    -> Term s' PInteger
    -> Term s' b)
-> Term
     s'
     ((b :--> (a :--> b))
      :--> ((PInteger :--> a)
            :--> (PInteger :--> (b :--> (PInteger :--> b)))))
forall a b. (a -> b) -> a -> b
$ \Term s' (b :--> (a :--> b))
combine Term s' (PInteger :--> a)
get Term s' PInteger
limit Term s' b
acc Term s' PInteger
ix ->
      Term s' PBool -> Term s' b -> Term s' b -> Term s' b
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
        (Term s' PInteger
ix 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
limit)
        Term s' b
acc
        (Term
  s'
  ((b :--> (a :--> b))
   :--> ((PInteger :--> a)
         :--> (PInteger :--> (b :--> (PInteger :--> b)))))
self Term
  s'
  ((b :--> (a :--> b))
   :--> ((PInteger :--> a)
         :--> (PInteger :--> (b :--> (PInteger :--> b)))))
-> Term s' (b :--> (a :--> b))
-> Term
     s'
     ((PInteger :--> a) :--> (PInteger :--> (b :--> (PInteger :--> 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))
combine Term
  s'
  ((PInteger :--> a) :--> (PInteger :--> (b :--> (PInteger :--> b))))
-> Term s' (PInteger :--> a)
-> Term s' (PInteger :--> (b :--> (PInteger :--> b)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' (PInteger :--> a)
get Term s' (PInteger :--> (b :--> (PInteger :--> b)))
-> Term s' PInteger -> Term s' (b :--> (PInteger :--> b))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' PInteger
limit Term s' (b :--> (PInteger :--> b))
-> Term s' b -> Term s' (PInteger :--> 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))
combine 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
acc 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' (PInteger :--> a)
get Term s' (PInteger :--> a) -> Term s' PInteger -> Term s' a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' PInteger
ix) Term s' (PInteger :--> b) -> Term s' PInteger -> Term s' b
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s' PInteger
ix Term s' PInteger -> Term s' PInteger -> Term s' PInteger
forall a. Num a => a -> a -> a
+ Term s' PInteger
1))

{- | As 'pfoldArray', but from the /highest/ index working /downward/.

@since 1.13.0
-}
prfoldArray ::
  forall (a :: S -> Type) (b :: S -> Type) (s :: S).
  Term s (b :--> a :--> b) ->
  Term s b ->
  Term s (PPullArray a) ->
  Term s b
prfoldArray :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s (b :--> (a :--> b))
-> Term s b -> Term s (PPullArray a) -> Term s b
prfoldArray Term s (b :--> (a :--> b))
f Term s b
x Term s (PPullArray a)
arr = Term s (PPullArray a) -> (PPullArray a s -> Term s b) -> Term s b
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 (PPullArray a)
arr ((PPullArray a s -> Term s b) -> Term s b)
-> (PPullArray a s -> Term s b) -> Term s b
forall a b. (a -> b) -> a -> b
$ \(PPullArray forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
k) ->
  Term s ((PNatural :--> ((PInteger :--> a) :--> b)) :--> b)
forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
k Term s ((PNatural :--> ((PInteger :--> a) :--> b)) :--> b)
-> Term s (PNatural :--> ((PInteger :--> a) :--> 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 PNatural -> Term s (PInteger :--> a) -> Term s b)
-> Term s (PNatural :--> ((PInteger :--> 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 (PInteger :--> a) -> Term s b)
-> Term s (c :--> ((PInteger :--> a) :--> b))
plam (\Term s PNatural
len Term s (PInteger :--> a)
h -> Term
  s
  ((b :--> (a :--> b))
   :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b))))
forall (s' :: S).
Term
  s'
  ((b :--> (a :--> b))
   :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b))))
go Term
  s
  ((b :--> (a :--> b))
   :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b))))
-> Term s (b :--> (a :--> b))
-> Term s ((PInteger :--> a) :--> (b :--> (PInteger :--> 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 ((PInteger :--> a) :--> (b :--> (PInteger :--> b)))
-> Term s (PInteger :--> a) -> Term s (b :--> (PInteger :--> b))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInteger :--> a)
h Term s (b :--> (PInteger :--> b))
-> Term s b -> Term s (PInteger :--> b)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
x Term s (PInteger :--> b) -> Term s PInteger -> Term s b
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PNatural -> Term s PInteger
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
PSubtype a b =>
Term s b -> Term s a
pupcast Term s PNatural
len Term s PInteger -> Term s PInteger -> Term s PInteger
forall a. Num a => a -> a -> a
- Term s PInteger
1))
  where
    go ::
      forall (s' :: S).
      Term s' ((b :--> a :--> b) :--> (PInteger :--> a) :--> b :--> PInteger :--> b)
    go :: forall (s' :: S).
Term
  s'
  ((b :--> (a :--> b))
   :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b))))
go = (forall (s' :: S).
 Term
   s'
   ((b :--> (a :--> b))
    :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b)))))
-> Term
     s'
     ((b :--> (a :--> b))
      :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b))))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S).
  Term
    s'
    ((b :--> (a :--> b))
     :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b)))))
 -> Term
      s'
      ((b :--> (a :--> b))
       :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b)))))
-> (forall (s' :: S).
    Term
      s'
      ((b :--> (a :--> b))
       :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b)))))
-> Term
     s'
     ((b :--> (a :--> b))
      :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b))))
forall a b. (a -> b) -> a -> b
$ (Term
   s'
   ((b :--> (a :--> b))
    :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b))))
 -> Term
      s'
      ((b :--> (a :--> b))
       :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b)))))
-> Term
     s'
     ((b :--> (a :--> b))
      :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b))))
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(Term s (a :--> b) -> Term s (a :--> b)) -> Term s (a :--> b)
pfix ((Term
    s'
    ((b :--> (a :--> b))
     :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b))))
  -> Term
       s'
       ((b :--> (a :--> b))
        :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b)))))
 -> Term
      s'
      ((b :--> (a :--> b))
       :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b)))))
-> (Term
      s'
      ((b :--> (a :--> b))
       :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b))))
    -> Term
         s'
         ((b :--> (a :--> b))
          :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b)))))
-> Term
     s'
     ((b :--> (a :--> b))
      :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b))))
forall a b. (a -> b) -> a -> b
$ \Term
  s'
  ((b :--> (a :--> b))
   :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b))))
self -> (Term s' (b :--> (a :--> b))
 -> Term s' (PInteger :--> a)
 -> Term s' b
 -> Term s' PInteger
 -> Term s' b)
-> Term
     s'
     ((b :--> (a :--> b))
      :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> 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' (PInteger :--> a)
 -> Term s' b
 -> Term s' PInteger
 -> Term s' b)
-> Term
     s' (c :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b))))
plam ((Term s' (b :--> (a :--> b))
  -> Term s' (PInteger :--> a)
  -> Term s' b
  -> Term s' PInteger
  -> Term s' b)
 -> Term
      s'
      ((b :--> (a :--> b))
       :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b)))))
-> (Term s' (b :--> (a :--> b))
    -> Term s' (PInteger :--> a)
    -> Term s' b
    -> Term s' PInteger
    -> Term s' b)
-> Term
     s'
     ((b :--> (a :--> b))
      :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b))))
forall a b. (a -> b) -> a -> b
$ \Term s' (b :--> (a :--> b))
combine Term s' (PInteger :--> a)
get Term s' b
acc Term s' PInteger
ix ->
      Term s' PBool -> Term s' b -> Term s' b -> Term s' b
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
        (Term s' PInteger
ix 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
-1))
        Term s' b
acc
        (Term
  s'
  ((b :--> (a :--> b))
   :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b))))
self Term
  s'
  ((b :--> (a :--> b))
   :--> ((PInteger :--> a) :--> (b :--> (PInteger :--> b))))
-> Term s' (b :--> (a :--> b))
-> Term s' ((PInteger :--> a) :--> (b :--> (PInteger :--> 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))
combine Term s' ((PInteger :--> a) :--> (b :--> (PInteger :--> b)))
-> Term s' (PInteger :--> a) -> Term s' (b :--> (PInteger :--> b))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' (PInteger :--> a)
get Term s' (b :--> (PInteger :--> b))
-> Term s' b -> Term s' (PInteger :--> 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))
combine 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
acc 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' (PInteger :--> a)
get Term s' (PInteger :--> a) -> Term s' PInteger -> Term s' a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' PInteger
ix) Term s' (PInteger :--> b) -> Term s' PInteger -> Term s' b
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s' PInteger
ix Term s' PInteger -> Term s' PInteger -> Term s' PInteger
forall a. Num a => a -> a -> a
- Term s' PInteger
1))

{- | Convert a pull array to a builtin list. Prefer using this function to
either kind of fold, as it is faster.

If you want to construct a builtin /array/ instead, use this function
together with 'plistToArray'.

\(\Theta(n)\) space and time complexity.

@since 1.12.0
-}
ppullArrayToList ::
  forall (a :: S -> Type) (s :: S).
  PlutusType (PBuiltinList a) =>
  Term s (PPullArray a) ->
  Term s (PBuiltinList a)
ppullArrayToList :: forall (a :: S -> Type) (s :: S).
PlutusType (PBuiltinList a) =>
Term s (PPullArray a) -> Term s (PBuiltinList a)
ppullArrayToList Term s (PPullArray a)
arr = Term s (PPullArray a)
-> (PPullArray a s -> Term s (PBuiltinList a))
-> Term s (PBuiltinList a)
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 (PPullArray a)
arr ((PPullArray a s -> Term s (PBuiltinList a))
 -> Term s (PBuiltinList a))
-> (PPullArray a s -> Term s (PBuiltinList a))
-> Term s (PBuiltinList a)
forall a b. (a -> b) -> a -> b
$ \(PPullArray forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
k) ->
  Term
  s
  ((PNatural :--> ((PInteger :--> a) :--> PBuiltinList a))
   :--> PBuiltinList a)
forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
k Term
  s
  ((PNatural :--> ((PInteger :--> a) :--> PBuiltinList a))
   :--> PBuiltinList a)
-> Term s (PNatural :--> ((PInteger :--> a) :--> PBuiltinList a))
-> Term s (PBuiltinList a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PNatural
 -> Term s (PInteger :--> a) -> Term s (PBuiltinList a))
-> Term s (PNatural :--> ((PInteger :--> 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 (PInteger :--> a) -> Term s (PBuiltinList a))
-> Term s (c :--> ((PInteger :--> a) :--> PBuiltinList a))
plam (\Term s PNatural
len Term s (PInteger :--> a)
h -> Term
  s
  ((PInteger :--> a)
   :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a)))
forall (s' :: S).
Term
  s'
  ((PInteger :--> a)
   :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a)))
go Term
  s
  ((PInteger :--> a)
   :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a)))
-> Term s (PInteger :--> a)
-> Term s (PBuiltinList a :--> (PInteger :--> PBuiltinList a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInteger :--> a)
h Term s (PBuiltinList a :--> (PInteger :--> PBuiltinList a))
-> Term s (PBuiltinList a) -> Term s (PInteger :--> PBuiltinList a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# 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 Term s (PInteger :--> PBuiltinList a)
-> Term s PInteger -> Term s (PBuiltinList a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PNatural -> Term s PInteger
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
PSubtype a b =>
Term s b -> Term s a
pupcast Term s PNatural
len Term s PInteger -> Term s PInteger -> Term s PInteger
forall a. Num a => a -> a -> a
- Term s PInteger
1))
  where
    go ::
      forall (s' :: S).
      Term s' ((PInteger :--> a) :--> PBuiltinList a :--> PInteger :--> PBuiltinList a)
    go :: forall (s' :: S).
Term
  s'
  ((PInteger :--> a)
   :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a)))
go = (forall (s' :: S).
 Term
   s'
   ((PInteger :--> a)
    :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a))))
-> Term
     s'
     ((PInteger :--> a)
      :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a)))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S).
  Term
    s'
    ((PInteger :--> a)
     :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a))))
 -> Term
      s'
      ((PInteger :--> a)
       :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a))))
-> (forall (s' :: S).
    Term
      s'
      ((PInteger :--> a)
       :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a))))
-> Term
     s'
     ((PInteger :--> a)
      :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a)))
forall a b. (a -> b) -> a -> b
$ (Term
   s'
   ((PInteger :--> a)
    :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a)))
 -> Term
      s'
      ((PInteger :--> a)
       :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a))))
-> Term
     s'
     ((PInteger :--> a)
      :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a)))
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(Term s (a :--> b) -> Term s (a :--> b)) -> Term s (a :--> b)
pfix ((Term
    s'
    ((PInteger :--> a)
     :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a)))
  -> Term
       s'
       ((PInteger :--> a)
        :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a))))
 -> Term
      s'
      ((PInteger :--> a)
       :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a))))
-> (Term
      s'
      ((PInteger :--> a)
       :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a)))
    -> Term
         s'
         ((PInteger :--> a)
          :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a))))
-> Term
     s'
     ((PInteger :--> a)
      :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a)))
forall a b. (a -> b) -> a -> b
$ \Term
  s'
  ((PInteger :--> a)
   :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a)))
self -> (Term s' (PInteger :--> a)
 -> Term s' (PBuiltinList a)
 -> Term s' PInteger
 -> Term s' (PBuiltinList a))
-> Term
     s'
     ((PInteger :--> a)
      :--> (PBuiltinList a :--> (PInteger :--> 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' PInteger
 -> Term s' (PBuiltinList a))
-> Term
     s' (c :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a)))
plam ((Term s' (PInteger :--> a)
  -> Term s' (PBuiltinList a)
  -> Term s' PInteger
  -> Term s' (PBuiltinList a))
 -> Term
      s'
      ((PInteger :--> a)
       :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a))))
-> (Term s' (PInteger :--> a)
    -> Term s' (PBuiltinList a)
    -> Term s' PInteger
    -> Term s' (PBuiltinList a))
-> Term
     s'
     ((PInteger :--> a)
      :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a)))
forall a b. (a -> b) -> a -> b
$ \Term s' (PInteger :--> a)
get Term s' (PBuiltinList a)
acc Term s' PInteger
ix ->
      Term s' PBool
-> Term s' (PBuiltinList a)
-> Term s' (PBuiltinList a)
-> Term s' (PBuiltinList a)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
        (Term s' PInteger
ix 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
-1))
        Term s' (PBuiltinList a)
acc
        (Term
  s'
  ((PInteger :--> a)
   :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a)))
self Term
  s'
  ((PInteger :--> a)
   :--> (PBuiltinList a :--> (PInteger :--> PBuiltinList a)))
-> Term s' (PInteger :--> a)
-> Term s' (PBuiltinList a :--> (PInteger :--> PBuiltinList a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' (PInteger :--> a)
get Term s' (PBuiltinList a :--> (PInteger :--> PBuiltinList a))
-> Term s' (PBuiltinList a)
-> Term s' (PInteger :--> PBuiltinList a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s' (a :--> (PBuiltinList a :--> PBuiltinList a))
forall (s :: S) (a :: S -> Type).
Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
pconsBuiltin Term s' (a :--> (PBuiltinList a :--> PBuiltinList a))
-> Term s' a -> Term s' (PBuiltinList a :--> PBuiltinList a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s' (PInteger :--> a)
get Term s' (PInteger :--> a) -> Term s' PInteger -> Term s' a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' PInteger
ix) Term s' (PBuiltinList a :--> PBuiltinList a)
-> Term s' (PBuiltinList a) -> Term s' (PBuiltinList a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' (PBuiltinList a)
acc) Term s' (PInteger :--> PBuiltinList a)
-> Term s' PInteger -> Term s' (PBuiltinList a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s' PInteger
ix Term s' PInteger -> Term s' PInteger -> Term s' PInteger
forall a. Num a => a -> a -> a
- Term s' PInteger
1))

{- | Convert a pull array to a 'PList'. Prefer using this function to either
kind of fold, as it is faster.

\(\Theta(n)\) space and time complexity.

@since 1.12.0
-}
ppullArrayToSOPList ::
  forall (a :: S -> Type) (s :: S).
  Term s (PPullArray a) ->
  Term s (PList a)
ppullArrayToSOPList :: forall (a :: S -> Type) (s :: S).
Term s (PPullArray a) -> Term s (PList a)
ppullArrayToSOPList Term s (PPullArray a)
arr = Term s (PPullArray a)
-> (PPullArray a s -> Term s (PList a)) -> Term s (PList a)
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 (PPullArray a)
arr ((PPullArray a s -> Term s (PList a)) -> Term s (PList a))
-> (PPullArray a s -> Term s (PList a)) -> Term s (PList a)
forall a b. (a -> b) -> a -> b
$ \(PPullArray forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
k) ->
  Term
  s ((PNatural :--> ((PInteger :--> a) :--> PList a)) :--> PList a)
forall (r :: S -> Type).
Term s ((PNatural :--> ((PInteger :--> a) :--> r)) :--> r)
k Term
  s ((PNatural :--> ((PInteger :--> a) :--> PList a)) :--> PList a)
-> Term s (PNatural :--> ((PInteger :--> a) :--> PList a))
-> Term s (PList a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PNatural -> Term s (PInteger :--> a) -> Term s (PList a))
-> Term s (PNatural :--> ((PInteger :--> 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 (PInteger :--> a) -> Term s (PList a))
-> Term s (c :--> ((PInteger :--> a) :--> PList a))
plam (\Term s PNatural
len Term s (PInteger :--> a)
h -> Term
  s ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a)))
forall (s' :: S).
Term
  s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a)))
go Term
  s ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a)))
-> Term s (PInteger :--> a)
-> Term s (PList a :--> (PInteger :--> PList a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInteger :--> a)
h Term s (PList a :--> (PInteger :--> PList a))
-> Term s (PList a) -> Term s (PInteger :--> PList a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# 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 Term s (PInteger :--> PList a)
-> Term s PInteger -> Term s (PList a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PNatural -> Term s PInteger
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
PSubtype a b =>
Term s b -> Term s a
pupcast Term s PNatural
len Term s PInteger -> Term s PInteger -> Term s PInteger
forall a. Num a => a -> a -> a
- Term s PInteger
1))
  where
    go ::
      forall (s' :: S).
      Term s' ((PInteger :--> a) :--> PList a :--> PInteger :--> PList a)
    go :: forall (s' :: S).
Term
  s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a)))
go = (forall (s' :: S).
 Term
   s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a))))
-> Term
     s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a)))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S).
  Term
    s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a))))
 -> Term
      s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a))))
-> (forall (s' :: S).
    Term
      s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a))))
-> Term
     s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a)))
forall a b. (a -> b) -> a -> b
$ (Term
   s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a)))
 -> Term
      s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a))))
-> Term
     s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a)))
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(Term s (a :--> b) -> Term s (a :--> b)) -> Term s (a :--> b)
pfix ((Term
    s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a)))
  -> Term
       s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a))))
 -> Term
      s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a))))
-> (Term
      s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a)))
    -> Term
         s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a))))
-> Term
     s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a)))
forall a b. (a -> b) -> a -> b
$ \Term
  s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a)))
self -> (Term s' (PInteger :--> a)
 -> Term s' (PList a) -> Term s' PInteger -> Term s' (PList a))
-> Term
     s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> 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' PInteger -> Term s' (PList a))
-> Term s' (c :--> (PList a :--> (PInteger :--> PList a)))
plam ((Term s' (PInteger :--> a)
  -> Term s' (PList a) -> Term s' PInteger -> Term s' (PList a))
 -> Term
      s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a))))
-> (Term s' (PInteger :--> a)
    -> Term s' (PList a) -> Term s' PInteger -> Term s' (PList a))
-> Term
     s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a)))
forall a b. (a -> b) -> a -> b
$ \Term s' (PInteger :--> a)
get Term s' (PList a)
acc Term s' PInteger
ix ->
      Term s' PBool
-> Term s' (PList a) -> Term s' (PList a) -> Term s' (PList a)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
        (Term s' PInteger
ix 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
-1))
        Term s' (PList a)
acc
        (Term
  s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a)))
self Term
  s' ((PInteger :--> a) :--> (PList a :--> (PInteger :--> PList a)))
-> Term s' (PInteger :--> a)
-> Term s' (PList a :--> (PInteger :--> PList a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' (PInteger :--> a)
get Term s' (PList a :--> (PInteger :--> PList a))
-> Term s' (PList a) -> Term s' (PInteger :--> PList a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (PList a s' -> Term s' (PList a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PList a s' -> Term s' (PList a))
-> (Term s' (PList a) -> PList a s')
-> Term s' (PList a)
-> Term s' (PList a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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' (PInteger :--> a)
get Term s' (PInteger :--> a) -> Term s' PInteger -> Term s' a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' PInteger
ix) (Term s' (PList a) -> Term s' (PList a))
-> Term s' (PList a) -> Term s' (PList a)
forall a b. (a -> b) -> a -> b
$ Term s' (PList a)
acc) Term s' (PInteger :--> PList a)
-> Term s' PInteger -> Term s' (PList a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s' PInteger
ix Term s' PInteger -> Term s' PInteger -> Term s' PInteger
forall a. Num a => a -> a -> a
- Term s' PInteger
1))