Interface TokenPusher


public interface TokenPusher
An object capable of transferring a token from a random-access source to a target. A TokenPusher only exists in the context of a source and target. The source is normally a TokenSequence, the target an output port.

Using a TokenPusher provides an efficient way for copying tokens one at a time, without requiring constant type checks. An example of this would be reading some number of tokens from an input, sorting them with a TokenSorter, and then pushing them on an output in sorted order:

    TokenArrayWriter buffer= TokenArrays.allocateWriter(input.getType(), size);
    input.transfer(buffer, size);
    int[] ordering= TokenSorter.MERGE_SORT.sort(buffer);
    TokenPusher pusher= PortTokenUtilities.constructPusher(output, buffer);
    for (int index : ordering) pusher.push(index);
 
  • Method Summary

    Modifier and Type
    Method
    Description
    void
    push(int index)
    Pushes the specified token from the source to the target.
  • Method Details

    • push

      void push(int index)
      Pushes the specified token from the source to the target.
      Parameters:
      index - the token to push