Trait WfckResultsProvider

pub trait WfckResultsProvider: Sized {
    // Required methods
    fn bin_rel_sort(&self, fhir_id: FhirId) -> Sort;
    fn coercions_for(&self, fhir_id: FhirId) -> &[Coercion];
    fn field_proj(&self, fhir_id: FhirId) -> FieldProj;
    fn lambda_output(&self, fhir_id: FhirId) -> Sort;
    fn record_ctor(&self, fhir_id: FhirId) -> DefId;
    fn param_sort(&self, param: &RefineParam<'_>) -> Sort;
}

An interface to the information elaborated during sort checking. We mock these results in the first conversion phase during sort checking.

Required Methods

fn bin_rel_sort(&self, fhir_id: FhirId) -> Sort

fn coercions_for(&self, fhir_id: FhirId) -> &[Coercion]

fn field_proj(&self, fhir_id: FhirId) -> FieldProj

fn lambda_output(&self, fhir_id: FhirId) -> Sort

fn record_ctor(&self, fhir_id: FhirId) -> DefId

fn param_sort(&self, param: &RefineParam<'_>) -> Sort

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementations on Foreign Types

impl WfckResultsProvider for WfckResults

fn bin_rel_sort(&self, fhir_id: FhirId) -> Sort

fn coercions_for(&self, fhir_id: FhirId) -> &[Coercion]

fn field_proj(&self, fhir_id: FhirId) -> FieldProj

fn lambda_output(&self, fhir_id: FhirId) -> Sort

fn record_ctor(&self, fhir_id: FhirId) -> DefId

fn param_sort(&self, param: &RefineParam<'_>) -> Sort

Implementors

impl WfckResultsProvider for InferCtxt<'_, '_>

The purpose of doing conversion before sort checking is to collect the sorts of base types. Thus, what we return here mostly doesn’t matter because the refinements on a type should not affect its sort. The one exception is the sort we generate for refinement parameters.

For instance, consider the following definition where we refine a struct with a polymorphic set:

#[flux::refined_by(elems: Set<T>)]
struct RSet<T> { ... }

Now, consider the type RSet<i32{v: v >= 0}>. This type desugars to RSet<λv:σ. {i32[v] | v >= 0}> where the sort σ needs to be inferred. The type RSet<λv:σ. {i32[v] | v >= 0}> has sort RSet<σ> where RSet is the sort-level representation of the RSet type. Thus, it is important that the inference variable we generate for σ is the same we use for sort checking.