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.

This [FxIndexSet] is used to track a mapping between sort variables 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 in the same order they appear in the #[refined_by(..)] annotation.

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 duplicate 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.