plutus-core-1.30.0.0: Language library for Plutus Core
Safe HaskellSafe-Inferred
LanguageHaskell2010

PlutusCore.StdLib.Meta.Data.Tuple

Description

tuples of various sizes and related functions.

Synopsis

Documentation

data Tuple term uni ann Source #

A Plutus Core (Scott-encoded) tuple.

Constructors

Tuple 

Fields

getTupleTypeMonadQuote m ⇒ ann → Tuple term uni ann → m (Type TyName uni ann) Source #

Get the type of a Tuple.

getTupleType _ (Tuple [a1, ... , an] _) = all r. (a1 -> ... -> an -> r) -> r

tupleTypeTermAt ∷ (TermLike term TyName Name uni fun, MonadQuote m) ⇒ ann → IntTuple term uni ann → m (Type TyName uni ann, term ann) Source #

Get the type of the ith element of a Tuple along with the element itself.

tupleTypeTermAt _ i (Tuple [a0, ... , an] term) =
    (ai, term {ai} (\(x0 : a0) ... (xn : an) -> xi))

tupleTermAt ∷ (TermLike term TyName Name uni fun, MonadQuote m) ⇒ ann → IntTuple term uni ann → m (term ann) Source #

Get the ith element of a Tuple.

tupleDefAt ∷ (TermLike term TyName Name uni fun, MonadQuote m) ⇒ ann → IntNameTuple term uni ann → m (TermDef term TyName Name uni ann) Source #

Get the ith element of a Tuple as a TermDef.

bindTuple ∷ (TermLike term TyName Name uni fun, MonadQuote m) ⇒ ann → [Name] → Tuple term uni ann → term ann → m (term ann) Source #

Bind all elements of a Tuple inside a Term.

bindTuple _ [x_1, ... , x_n] (Tuple [a1, ... , an] term) body =
    (\(tup : all r. (a_1 -> ... -> a_n -> r) -> r) ->
      let x_1 = _1 tup
          ...
          x_n = _n tup
        in body
    ) term

prodNIntType TyName uni () Source #

Given an arity n, create the n-ary product type.

(T_1 :: *) .. (T_n :: *) . all (R :: *) . (T_1 -> .. -> T_n -> R) -> R

prodNConstructorTermLike term TyName Name uni fun ⇒ Int → term () Source #

Given an arity n, create the constructor for n-ary products.

    /(T_1 :: *) .. (T_n :: *) .
        (arg_1 : T_1) .. (arg_n : T_n) .
            /(R :: *).
                (case : T_1 -> .. -> T_n -> R) -> case arg_1 .. arg_n

prodNAccessorTermLike term TyName Name uni fun ⇒ IntInt → term () Source #

Given an arity n and an index i, create a function for accessing the i'th component of a n-tuple.

    /(T_1 :: *) .. (T_n :: *) .
        (tuple : all (R :: *) . (T_1 -> .. -> T_n -> R) -> R)) .
            tuple {T_i} ((arg_1 : T_1) .. (arg_n : T_n) . arg_i)

getSpineToTuple ∷ (TermLike term TyName Name uni fun, MonadQuote m) ⇒ ann → [(Type TyName uni ann, term ann)] → m (Tuple term uni ann) Source #

Convert a Haskell spine of Terms to a PLC Tuple.

getSpineToTuple _ [(a1, x1), ... , (an, xn)] =
    Tuple [a1, ... , an] (/\(r :: *) -> \(f :: a1 -> ... -> an -> r) -> f x1 ... xn)