mcrl2::aterm::term

Struct ATermRef

Source
pub struct ATermRef<'a> { /* private fields */ }
Expand description

This represents a lifetime bound reference to an existing ATerm that is protected somewhere statically.

Can be ’static if the term is protected in a container or ATerm. That means we either return &’a ATermRef<’static> or with a concrete lifetime ATermRef<’a>. However, this means that the functions for ATermRef cannot use the associated lifetime for the results parameters, as that would allow us to acquire the ’static lifetime. This occasionally gives rise to issues where we look at the argument of a term and want to return it’s name, but this is not allowed since the temporary returned by the argument is dropped.

Implementations§

Source§

impl<'a> ATermRef<'a>

Source

pub fn protect(&self) -> ATerm

Protects the reference on the thread local protection pool.

Source

pub fn protect_global(&self) -> ATermGlobal

Protects the reference on the global protection pool.

Source

pub fn upgrade<'b: 'a>(&'a self, parent: &ATermRef<'b>) -> ATermRef<'b>

This allows us to extend our borrowed lifetime from ’a to ’b based on existing parent term which has lifetime ’b.

The main usecase is to establish transitive lifetimes. For example given a term t from which we borrow u = t.arg(0) then we cannot have u.arg(0) live as long as t since the intermediate temporary u is dropped. However, since we know that u.arg(0) is a subterm of t we can upgrade its lifetime to the lifetime of t using this function.

§Safety

This function might only be used if witness is a parent term of the current term.

Source§

impl ATermRef<'_>

Source

pub fn arg(&self, index: usize) -> ATermRef<'_>

Returns the indexed argument of the term

Source

pub fn arguments(&self) -> ATermArgs<'_>

Returns the list of arguments as a collection

Source

pub fn copy(&self) -> ATermRef<'_>

Makes a copy of the term with the same lifetime as itself.

Source

pub fn is_default(&self) -> bool

Returns whether the term is the default term (not initialised)

Source

pub fn is_list(&self) -> bool

Returns true iff this is an aterm_list

Source

pub fn is_empty_list(&self) -> bool

Returns true iff this is the empty aterm_list

Source

pub fn is_int(&self) -> bool

Returns true iff this is a aterm_int

Source

pub fn get_head_symbol(&self) -> SymbolRef<'_>

Returns the head function symbol of the term.

Source

pub fn iter(&self) -> TermIterator<'_>

Returns an iterator over all arguments of the term that runs in pre order traversal of the term trees.

Source

pub fn require_valid(&self)

Panics if the term is default

Trait Implementations§

Source§

impl<'a> Borrow<ATermRef<'a>> for ATerm

Source§

fn borrow(&self) -> &ATermRef<'a>

Immutably borrows from an owned value. Read more
Source§

impl<'a> Borrow<ATermRef<'a>> for BasicSortRef<'a>

Source§

fn borrow(&self) -> &ATermRef<'a>

Immutably borrows from an owned value. Read more
Source§

impl<'a> Borrow<ATermRef<'a>> for BoolSortRef<'a>

Source§

fn borrow(&self) -> &ATermRef<'a>

Immutably borrows from an owned value. Read more
Source§

impl<'a> Borrow<ATermRef<'a>> for DataApplicationRef<'a>

Source§

fn borrow(&self) -> &ATermRef<'a>

Immutably borrows from an owned value. Read more
Source§

impl<'a> Borrow<ATermRef<'a>> for DataExpressionRef<'a>

Source§

fn borrow(&self) -> &ATermRef<'a>

Immutably borrows from an owned value. Read more
Source§

impl<'a> Borrow<ATermRef<'a>> for DataFunctionSymbolRef<'a>

Source§

fn borrow(&self) -> &ATermRef<'a>

Immutably borrows from an owned value. Read more
Source§

impl<'a> Borrow<ATermRef<'a>> for DataVariableRef<'a>

Source§

fn borrow(&self) -> &ATermRef<'a>

Immutably borrows from an owned value. Read more
Source§

impl<'a> Borrow<ATermRef<'a>> for FunctionSortRef<'a>

Source§

fn borrow(&self) -> &ATermRef<'a>

Immutably borrows from an owned value. Read more
Source§

impl<'a> Borrow<ATermRef<'a>> for MachineNumberRef<'a>

Source§

fn borrow(&self) -> &ATermRef<'a>

Immutably borrows from an owned value. Read more
Source§

impl<'a> Borrow<ATermRef<'a>> for SortExpressionRef<'a>

Source§

fn borrow(&self) -> &ATermRef<'a>

Immutably borrows from an owned value. Read more
Source§

impl Borrow<ATermRef<'static>> for BasicSort

Source§

fn borrow(&self) -> &ATermRef<'static>

Immutably borrows from an owned value. Read more
Source§

impl Borrow<ATermRef<'static>> for BoolSort

Source§

fn borrow(&self) -> &ATermRef<'static>

Immutably borrows from an owned value. Read more
Source§

impl Borrow<ATermRef<'static>> for DataApplication

Source§

fn borrow(&self) -> &ATermRef<'static>

Immutably borrows from an owned value. Read more
Source§

impl Borrow<ATermRef<'static>> for DataExpression

Source§

fn borrow(&self) -> &ATermRef<'static>

Immutably borrows from an owned value. Read more
Source§

impl Borrow<ATermRef<'static>> for DataFunctionSymbol

Source§

fn borrow(&self) -> &ATermRef<'static>

Immutably borrows from an owned value. Read more
Source§

impl Borrow<ATermRef<'static>> for DataVariable

Source§

fn borrow(&self) -> &ATermRef<'static>

Immutably borrows from an owned value. Read more
Source§

impl Borrow<ATermRef<'static>> for FunctionSort

Source§

fn borrow(&self) -> &ATermRef<'static>

Immutably borrows from an owned value. Read more
Source§

impl Borrow<ATermRef<'static>> for SortExpression

Source§

fn borrow(&self) -> &ATermRef<'static>

Immutably borrows from an owned value. Read more
Source§

impl Debug for ATermRef<'_>

Source§

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter. Read more
Source§

impl Default for ATermRef<'_>

Source§

fn default() -> Self

Returns the “default value” for a type. Read more
Source§

impl Display for ATermRef<'_>

Source§

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter. Read more
Source§

impl<'a, T> From<ATermRef<'a>> for ATermList<T>

Source§

fn from(value: ATermRef<'a>) -> Self

Converts to this type from the input type.
Source§

impl<'a> From<ATermRef<'a>> for BasicSortRef<'a>

Source§

fn from(term: ATermRef<'a>) -> BasicSortRef<'a>

Converts to this type from the input type.
Source§

impl<'a> From<ATermRef<'a>> for BoolSortRef<'a>

Source§

fn from(term: ATermRef<'a>) -> BoolSortRef<'a>

Converts to this type from the input type.
Source§

impl<'a> From<ATermRef<'a>> for DataApplicationRef<'a>

Source§

fn from(term: ATermRef<'a>) -> DataApplicationRef<'a>

Converts to this type from the input type.
Source§

impl<'a> From<ATermRef<'a>> for DataExpressionRef<'a>

Source§

fn from(term: ATermRef<'a>) -> DataExpressionRef<'a>

Converts to this type from the input type.
Source§

impl<'a> From<ATermRef<'a>> for DataFunctionSymbolRef<'a>

Source§

fn from(term: ATermRef<'a>) -> DataFunctionSymbolRef<'a>

Converts to this type from the input type.
Source§

impl<'a> From<ATermRef<'a>> for DataVariableRef<'a>

Source§

fn from(term: ATermRef<'a>) -> DataVariableRef<'a>

Converts to this type from the input type.
Source§

impl<'a> From<ATermRef<'a>> for FunctionSortRef<'a>

Source§

fn from(term: ATermRef<'a>) -> FunctionSortRef<'a>

Converts to this type from the input type.
Source§

impl<'a> From<ATermRef<'a>> for MachineNumberRef<'a>

Source§

fn from(term: ATermRef<'a>) -> MachineNumberRef<'a>

Converts to this type from the input type.
Source§

impl<'a> From<ATermRef<'a>> for SortExpressionRef<'a>

Source§

fn from(term: ATermRef<'a>) -> SortExpressionRef<'a>

Converts to this type from the input type.
Source§

impl<'a> Hash for ATermRef<'a>

Source§

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher. Read more
1.3.0 · Source§

fn hash_slice<H>(data: &[Self], state: &mut H)
where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher. Read more
Source§

impl<'a> Into<ATermRef<'a>> for BasicSortRef<'a>

Source§

fn into(self) -> ATermRef<'a>

Converts this type into the (usually inferred) input type.
Source§

impl<'a> Into<ATermRef<'a>> for BoolSortRef<'a>

Source§

fn into(self) -> ATermRef<'a>

Converts this type into the (usually inferred) input type.
Source§

impl<'a> Into<ATermRef<'a>> for DataApplicationRef<'a>

Source§

fn into(self) -> ATermRef<'a>

Converts this type into the (usually inferred) input type.
Source§

impl<'a> Into<ATermRef<'a>> for DataExpressionRef<'a>

Source§

fn into(self) -> ATermRef<'a>

Converts this type into the (usually inferred) input type.
Source§

impl<'a> Into<ATermRef<'a>> for DataFunctionSymbolRef<'a>

Source§

fn into(self) -> ATermRef<'a>

Converts this type into the (usually inferred) input type.
Source§

impl<'a> Into<ATermRef<'a>> for DataVariableRef<'a>

Source§

fn into(self) -> ATermRef<'a>

Converts this type into the (usually inferred) input type.
Source§

impl<'a> Into<ATermRef<'a>> for FunctionSortRef<'a>

Source§

fn into(self) -> ATermRef<'a>

Converts this type into the (usually inferred) input type.
Source§

impl<'a> Into<ATermRef<'a>> for MachineNumberRef<'a>

Source§

fn into(self) -> ATermRef<'a>

Converts this type into the (usually inferred) input type.
Source§

impl<'a> Into<ATermRef<'a>> for SortExpressionRef<'a>

Source§

fn into(self) -> ATermRef<'a>

Converts this type into the (usually inferred) input type.
Source§

impl Markable for ATermRef<'_>

Source§

fn mark(&self, todo: Pin<&mut term_mark_stack>)

Marks all the ATermRefs to prevent them from being garbage collected.
Source§

fn contains_term(&self, term: &ATermRef<'_>) -> bool

Should return true iff the given term is contained in the object. Used for runtime checks.
Source§

fn len(&self) -> usize

Returns the number of terms in the instance, used to delay garbage collection.
Source§

fn is_empty(&self) -> bool

Returns true iff the container is empty.
Source§

impl<'a> Ord for ATermRef<'a>

Source§

fn cmp(&self, other: &ATermRef<'a>) -> Ordering

This method returns an Ordering between self and other. Read more
1.21.0 · Source§

fn max(self, other: Self) -> Self
where Self: Sized,

Compares and returns the maximum of two values. Read more
1.21.0 · Source§

fn min(self, other: Self) -> Self
where Self: Sized,

Compares and returns the minimum of two values. Read more
1.50.0 · Source§

fn clamp(self, min: Self, max: Self) -> Self
where Self: Sized,

Restrict a value to a certain interval. Read more
Source§

impl<'a> PartialEq for ATermRef<'a>

Source§

fn eq(&self, other: &ATermRef<'a>) -> bool

Tests for self and other values to be equal, and is used by ==.
1.0.0 · Source§

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.
Source§

impl<'a> PartialOrd for ATermRef<'a>

Source§

fn partial_cmp(&self, other: &ATermRef<'a>) -> Option<Ordering>

This method returns an ordering between self and other values if one exists. Read more
1.0.0 · Source§

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator. Read more
1.0.0 · Source§

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator. Read more
1.0.0 · Source§

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator. Read more
1.0.0 · Source§

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator. Read more
Source§

impl<'a> Eq for ATermRef<'a>

Source§

impl Send for ATermRef<'_>

These are safe because terms are never modified. Garbage collection is always performed with exclusive access and uses relaxed atomics to perform some interior mutability.

Source§

impl<'a> StructuralPartialEq for ATermRef<'a>

Source§

impl Sync for ATermRef<'_>

Auto Trait Implementations§

§

impl<'a> Freeze for ATermRef<'a>

§

impl<'a> RefUnwindSafe for ATermRef<'a>

§

impl<'a> Unpin for ATermRef<'a>

§

impl<'a> UnwindSafe for ATermRef<'a>

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source§

impl<T> ToString for T
where T: Display + ?Sized,

Source§

default fn to_string(&self) -> String

Converts the given value to a String. Read more
Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<V, T> VZip<V> for T
where V: MultiLane<T>,

§

fn vzip(self) -> V