Struct RefinedBy

pub struct RefinedBy<'fhir> {
    pub sort_params: FxIndexSet<DefId>,
    pub fields: FxIndexMap<Symbol, Sort<'fhir>>,
}

Information about the refinement parameters associated with an adt (struct/enum).

Fields

sort_params: FxIndexSet<DefId>

When a #[flux::refined_by(..)] annotation mentions generic type parameters we implicitly generate a polymorphic data sort.

For example, if we have:

#[refined_by(keys: Set<K>)]
RMap<K, V> { ... }

we implicitly create a data sort of the form forall #0. { keys: Set<#0> }, where #0 is a sort variable.

The FxIndexSet is used to track a mapping between sort varriables and their corresponding type parameter. The DefId is the id of the type parameter and its index in the set is the position of the sort variable.

fields: FxIndexMap<Symbol, Sort<'fhir>>

Fields indexed by their name and in the same order they appear in the definition.

Implementations

impl<'fhir> RefinedBy<'fhir>

pub fn new( fields: FxIndexMap<Symbol, Sort<'fhir>>, sort_params: FxIndexSet<DefId>, ) -> Self

pub fn trivial() -> Self

Trait Implementations

impl<'fhir> Clone for RefinedBy<'fhir>

fn clone(&self) -> RefinedBy<'fhir>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<'fhir> Debug for RefinedBy<'fhir>

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

Formats the value using the given formatter.