Struct mm0b_parser::Type

#[repr(C)]
pub struct Type(_);

An argument binder in a term/def or axiom/theorem.

• Bit 63 (the high bit of the high byte) is 1 if this is a bound variable.
• Bits 56-62 (the low 7 bits of the high byte) give the sort of the variable.
• Bits 0-55 (the low 7 bytes) are a bitset giving the set of bound variables earlier in the list that this variable is allowed to depend on.

Implementations

impl Type

pub fn into_inner(self) -> u64

Get the u64 comprising a type

#[must_use]

pub fn new_of_sort(sort_num: u8) -> Self

Make a new Type of sort sort_num

#[must_use]

pub fn new(bound: bool) -> Self

A brand new Type; bool indicates whether it’s bound.

pub fn add_sort(&mut self, sort_id: SortId)

Annotate a Type with a sort.

Since types are often built incrementally, you may have built a “blank” type that you knew was bound, but you’ll only know it’s sort later. This is how you add the sort. If the Type already had a sort, it’s overwritten by sort_id.

pub fn add_dep(&mut self, bv_idx: u64)

Add a dependency on bv_idx

#[must_use]

pub fn depends_on(self, bv_idx: u64) -> bool

Does this type depend on the bth bound variable?

This is 0 indexed.

#[must_use]

pub fn bound(self) -> bool

True if this argument is a bound variable.

#[must_use]

pub fn sort(self) -> SortId

The sort of this variable.

#[must_use]

pub fn bound_digit(self) -> Option<u64>

If this is the type of a bound variable, return a u64 whose only activated bit is the bit indicating which bv it is.

#[must_use]

pub fn bound_pos(self) -> Option<u64>

The POSITION (1 - 55) of this bound variable, NOT the literal u64.

#[must_use]

pub fn has_deps(self) -> bool

Does this Type have dependencies?

#[must_use]

pub fn deps(self) -> Option<u64>

If this is a regular/not-bound variable, return a u64 whose only activated bits are the ones marking the bvs on which it depends.

#[must_use]

pub fn deps_unchecked(self) -> u64

Assuming this is a regular/not-bound variable, return a u64 whose only activated bits are the ones marking the bvs on which it depends.

#[must_use]

pub fn high_bit(self) -> Self

Get the high bit only, which holds the boundedness and the sort.

#[must_use]

pub fn disjoint(self, other: Self) -> bool

Are these two types totally bitwise-disjoint

Trait Implementations

impl BitAnd<Type> for Type

type Output = Self

The resulting type after applying the & operator.

fn bitand(self, rhs: Self) -> Self::Output

Performs the & operation.

impl BitAndAssign<Type> for Type

fn bitand_assign(&mut self, other: Self)

Performs the &= operation.

impl BitOr<Type> for Type

type Output = Self

The resulting type after applying the | operator.

fn bitor(self, rhs: Self) -> Self::Output

Performs the | operation.

impl BitOrAssign<Type> for Type

fn bitor_assign(&mut self, other: Self)

Performs the |= operation.

impl Clone for Type

fn clone(&self) -> Type

Returns a copy of the value.

pub fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Copy for Type

impl Debug for Type

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

Formats the value using the given formatter.

impl Default for Type

fn default() -> Self

Returns the “default value” for a type.

impl Eq for Type

impl From<u64> for Type

fn from(n: u64) -> Type

Performs the conversion.

impl FromBytes for Type

fn only_derive_is_allowed_to_implement_this_trait() where
    Self: Sized, 

impl Hash for Type

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

Feeds this value into the given Hasher.

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

Feeds a slice of this type into the given Hasher.

impl Not for Type

type Output = Type

The resulting type after applying the ! operator.

fn not(self) -> Self::Output

Performs the unary ! operation.

impl PartialEq<Type> for Type

fn eq(&self, other: &Type) -> bool

This method tests for self and other values to be equal, and is used by ==.

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

This method tests for !=.

impl StructuralEq for Type

impl StructuralPartialEq for Type

impl Unaligned for Type

fn only_derive_is_allowed_to_implement_this_trait() where
    Self: Sized,