Trait flux_fhir_analysis::conv::ConvPhase

pub trait ConvPhase<'genv, 'tcx>: Sized {
    type Results: WfckResultsProvider;

    const EXPAND_TYPE_ALIASES: bool;
    const HAS_ELABORATED_INFORMATION: bool;

    // Required methods
    fn genv(&self) -> GlobalEnv<'genv, 'tcx>;
    fn owner(&self) -> FluxOwnerId;
    fn next_sort_vid(&mut self) -> SortVid;
    fn next_type_vid(&mut self) -> TyVid;
    fn next_region_vid(&mut self) -> RegionVid;
    fn next_const_vid(&mut self) -> ConstVid;
    fn results(&self) -> &Self::Results;
    fn insert_bty_sort(&mut self, fhir_id: FhirId, sort: Sort);
    fn insert_alias_reft_sort(&mut self, fhir_id: FhirId, fsort: FuncSort);

    // Provided methods
    fn into_conv_ctxt(self) -> ConvCtxt<Self> { ... }
    fn as_conv_ctxt(&mut self) -> &mut ConvCtxt<Self> { ... }
}

We do conversion twice: once before sort checking when we don’t have elaborated information and then again after sort checking after all information has been elaborated. This is the interface to configure conversion for both phases.

Required Associated Types

type Results: WfckResultsProvider

Required Associated Constants

const EXPAND_TYPE_ALIASES: bool

Whether to expand type aliases or to generate a weak rty::AliasTy.

const HAS_ELABORATED_INFORMATION: bool

Whether we have elaborated information or not (in the first phase we will not, but in the second we will).

Required Methods

fn genv(&self) -> GlobalEnv<'genv, 'tcx>

fn owner(&self) -> FluxOwnerId

fn next_sort_vid(&mut self) -> SortVid

fn next_type_vid(&mut self) -> TyVid

fn next_region_vid(&mut self) -> RegionVid

fn next_const_vid(&mut self) -> ConstVid

fn results(&self) -> &Self::Results

fn insert_bty_sort(&mut self, fhir_id: FhirId, sort: Sort)

Called after converting an indexed type b[e] with the fhir_id and sort of b. Used during the first phase to collect the sort of base types.

fn insert_alias_reft_sort(&mut self, fhir_id: FhirId, fsort: FuncSort)

Called after converting an fhir::ExprKind::Alias with the sort of the resulting rty::AliasReft. Used during the first phase to collect the sorts of refinement aliases.

Provided Methods

fn into_conv_ctxt(self) -> ConvCtxt<Self>

fn as_conv_ctxt(&mut self) -> &mut ConvCtxt<Self>

Object Safety

This trait is not object safe.

Implementors

impl<'genv, 'tcx> ConvPhase<'genv, 'tcx> for Wf<'_, 'genv, 'tcx>

const EXPAND_TYPE_ALIASES: bool = false

const HAS_ELABORATED_INFORMATION: bool = false

type Results = InferCtxt<'genv, 'tcx>

impl<'genv, 'tcx> ConvPhase<'genv, 'tcx> for AfterSortck<'_, 'genv, 'tcx>

const EXPAND_TYPE_ALIASES: bool = true

const HAS_ELABORATED_INFORMATION: bool = true

type Results = WfckResults