Safe Haskell	Safe-Inferred
Language	Haskell2010

PlutusCore.StdLib.Meta.Data.Tuple

Description

tuples of various sizes and related functions.

Synopsis

data Tuple term uni ann = Tuple {
- _tupleElementTypes ∷ [Type TyName uni ann]
- _tupleTerm ∷ term ann
}
getTupleType ∷ MonadQuote m ⇒ ann → Tuple term uni ann → m (Type TyName uni ann)
tupleTypeTermAt ∷ (TermLike term TyName Name uni fun, MonadQuote m) ⇒ ann → Int → Tuple term uni ann → m (Type TyName uni ann, term ann)
tupleTermAt ∷ (TermLike term TyName Name uni fun, MonadQuote m) ⇒ ann → Int → Tuple term uni ann → m (term ann)
tupleDefAt ∷ (TermLike term TyName Name uni fun, MonadQuote m) ⇒ ann → Int → Name → Tuple term uni ann → m (TermDef term TyName Name uni ann)
bindTuple ∷ (TermLike term TyName Name uni fun, MonadQuote m) ⇒ ann → [Name] → Tuple term uni ann → term ann → m (term ann)
prodN ∷ Int → Type TyName uni ()
prodNConstructor ∷ TermLike term TyName Name uni fun ⇒ Int → term ()
prodNAccessor ∷ TermLike term TyName Name uni fun ⇒ Int → Int → term ()
getSpineToTuple ∷ (TermLike term TyName Name uni fun, MonadQuote m) ⇒ ann → [(Type TyName uni ann, term ann)] → m (Tuple term uni ann)

Documentation

data Tuple term uni ann Source #

A Plutus Core (Scott-encoded) tuple.

Constructors

Tuple
Fields _tupleElementTypes ∷ [Type TyName uni ann] The types of elements of a tuple. _tupleTerm ∷ term ann A term representation of the tuple.

getTupleType ∷ MonadQuote 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 → Int → Tuple 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 → Int → Tuple term uni ann → m (term ann) Source #

Get the ith element of a Tuple.

tupleDefAt ∷ (TermLike term TyName Name uni fun, MonadQuote m) ⇒ ann → Int → Name → Tuple 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

prodN ∷ Int → Type 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

prodNConstructor ∷ TermLike 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

prodNAccessor ∷ TermLike term TyName Name uni fun ⇒ Int → Int → 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)