Class RuleVector

java.lang.Object
es.ucm.maude.bindings.RuleVector
public class RuleVector extends Object
Internal Maude vector.

  • Constructor Summary

    Constructors
    Constructor
    Description
    RuleVector()
    Construct a vector.

    RuleVector(long length)
    Construct a vector.

  • Method Summary

    Modifier and Type
    Method
    Description
    void
    append(Rule value)
    Append a new element to the vector.
    long
    capacity()
    Reserved capacity of the vector.
    void
    clear()
    Set the vector length to zero.
    void
    delete()
     
    boolean
    empty()
    Is the vector empty?
    Rule
    get(long n)
    Get a vector position value.

    void
    resize(long new_size)
    Resize the vector.

    void
    set(long n, Rule value)
    Set a vector position value.

    long
    size()
    Size of the vector.
    void
    swap(RuleVector other)
    Swap this vector's contents with another.

    Methods inherited from class java.lang.Object

    equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

  • Constructor Details

    • RuleVector

      public RuleVector(long length)
      Construct a vector.

      Parameters:
      length - The initial length.

    • RuleVector

      public RuleVector()
      Construct a vector.

  • Method Details

    • delete

      public void delete()

    • empty

      public boolean empty()
      Is the vector empty?

    • size

      public long size()
      Size of the vector.

    • capacity

      public long capacity()
      Reserved capacity of the vector.

    • swap

      public void swap(RuleVector other)
      Swap this vector's contents with another.

      Parameters:
      other - The other vector.

    • get

      public Rule get(long n)
      Get a vector position value.

      Parameters:
      n - Vector position from zero.

    • set

      public void set(long n, Rule value)
      Set a vector position value.

      Parameters:
      n - Vector position from zero.
      value - Value to be set.

    • append

      public void append(Rule value)
      Append a new element to the vector.

    • clear

      public void clear()
      Set the vector length to zero.

    • resize

      public void resize(long new_size)
      Resize the vector.

      Parameters:
      new_size - New size.