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

      All Methods Instance Methods Abstract Methods 
      Modifier and Type Method Description
      void push​(int index)
      Pushes the specified token from the source to the target.
    • Method Detail

      • push

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