Struct ItemUid

pub struct ItemUid {
    pub uid: String,
}

Each item can be marked with a unique identifier. This is useful whenever the payload of an attribute is a piece of Rust code (an expression, a path, a type…). We don’t want to retrieve those pieces of Rust code as raw token stream: we want to let Rustc give meaning to those. For instance, we want Rustc to type expressions and to resolve paths.

Thus, we expand attributes with Rust-code-payloads as top-level items marked with an ItemUid. The attributes are then replaced in place with a simple reference (the ItemUid in stake).

Morally, we expand struct Foo { #[refine(x > 3)] x: u32 } to:

1. #[uuid(A_UNIQUE_ID_123)] fn refinement(x: u32) -> hax_lib::Prop {x > 3};
2. struct Foo { #[refined_by(A_UNIQUE_ID_123)] x: u32 }.

Fields

uid: String

Currently, this is a UUID.

Implementations

impl ItemUid

pub fn fresh() -> Self

Trait Implementations

impl Clone for ItemUid

fn clone(&self) -> ItemUid

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ItemUid

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for ItemUid

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Serialize for ItemUid

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.