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.