Safe Haskell	None
Language	Haskell2010

PlutusCore.StdLib.Meta.Data.Tuple

Description

tuple s of various sizes and related functions.

Synopsis

data Tuple term uni ann where
- Tuple :: TermLike term TyName Name uni fun => {..} -> Tuple term uni 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 fun 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 where Source #

A Plutus Core (Scott-encoded) tuple.

Constructors

Tuple
Fields :: TermLike term TyName Name uni fun => { _tupleElementTypes :: [ Type TyName uni ann] The types of elements of a tuple. , _tupleTerm :: term ann A term representation of the tuple. } -> Tuple term uni ann

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 fun 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 Term s to a PLC Tuple .

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