Struct InferCtxt

pub(super) struct InferCtxt<'genv, 'tcx> {
    pub genv: GlobalEnv<'genv, 'tcx>,
    pub params: UnordMap<ParamId, (Sort, ParamKind)>,
    pub wfckresults: WfckResults,
    sort_unification_table: InPlaceUnificationTable<SortVid>,
    num_unification_table: InPlaceUnificationTable<NumVid>,
    bv_size_unification_table: InPlaceUnificationTable<BvSizeVid>,
    sort_of_bty: FxHashMap<FhirId, Sort>,
    sort_of_alias_reft: UnordMap<FhirId, FuncSort>,
}

Fields

genv: GlobalEnv<'genv, 'tcx>

params: UnordMap<ParamId, (Sort, ParamKind)>

wfckresults: WfckResults

sort_unification_table: InPlaceUnificationTable<SortVid>

num_unification_table: InPlaceUnificationTable<NumVid>

bv_size_unification_table: InPlaceUnificationTable<BvSizeVid>

sort_of_bty: FxHashMap<FhirId, Sort>

sort_of_alias_reft: UnordMap<FhirId, FuncSort>

Implementations

impl<'genv, 'tcx> InferCtxt<'genv, 'tcx>

pub(super) fn new(genv: GlobalEnv<'genv, 'tcx>, owner: FluxOwnerId) -> Self

fn check_abs( &mut self, arg: &Expr<'_>, params: &[RefineParam<'_>], body: &Expr<'_>, expected: &Sort, ) -> Result<(), ErrorGuaranteed>

fn check_field_exprs( &mut self, expr_span: Span, sort_def: &AdtSortDef, sort_args: &[Sort], field_exprs: &[FieldExpr<'_>], spread: &Option<&Spread<'_>>, expected: &Sort, ) -> Result<(), ErrorGuaranteed>

fn check_constructor( &mut self, expr: &Expr<'_>, field_exprs: &[FieldExpr<'_>], spread: &Option<&Spread<'_>>, expected: &Sort, ) -> Result<(), ErrorGuaranteed>

fn check_record( &mut self, arg: &Expr<'_>, flds: &[Expr<'_>], expected: &Sort, ) -> Result<(), ErrorGuaranteed>

pub(super) fn check_expr( &mut self, expr: &Expr<'_>, expected: &Sort, ) -> Result<(), ErrorGuaranteed>

pub(super) fn check_loc( &mut self, loc: &PathExpr<'_>, ) -> Result<(), ErrorGuaranteed>

fn synth_expr(&mut self, expr: &Expr<'_>) -> Result<Sort, ErrorGuaranteed>

fn synth_var(&mut self, path: &PathExpr<'_>) -> Sort

fn synth_binary_op( &mut self, expr: &Expr<'_>, op: BinOp, e1: &Expr<'_>, e2: &Expr<'_>, ) -> Result<Sort, ErrorGuaranteed>

fn synth_unary_op( &mut self, op: UnOp, e: &Expr<'_>, ) -> Result<Sort, ErrorGuaranteed>

fn synth_app( &mut self, func: &PathExpr<'_>, args: &[Expr<'_>], span: Span, ) -> Result<Sort, ErrorGuaranteed>

fn synth_alias_reft_app( &mut self, fhir_id: FhirId, span: Span, args: &[Expr<'_>], ) -> Result<Sort, ErrorGuaranteed>

fn synth_func( &mut self, func: &PathExpr<'_>, ) -> Result<FuncSort, ErrorGuaranteed>

fn instantiate_func_sort(&mut self, fsort: PolyFuncSort) -> FuncSort

pub(crate) fn insert_sort_for_bty(&mut self, fhir_id: FhirId, sort: Sort)

pub(crate) fn sort_of_bty(&self, fhir_id: FhirId) -> Sort

pub(crate) fn insert_sort_for_alias_reft( &mut self, fhir_id: FhirId, fsort: FuncSort, )

fn sort_of_alias_reft(&self, fhir_id: FhirId) -> FuncSort

pub(crate) fn normalize_weak_alias_sorts(&mut self) -> QueryResult

impl InferCtxt<'_, '_>

pub(super) fn insert_param(&mut self, id: ParamId, sort: Sort, kind: ParamKind)

fn is_coercible(&mut self, sort1: &Sort, sort2: &Sort, fhir_id: FhirId) -> bool

Whether a value of sort1 can be automatically coerced to a value of sort2. A value of an rty::SortCtor::Adt sort with a single field of sort s can be coerced to a value of sort s and vice versa, i.e., we can automatically project the field out of the record or inject a value into a record.

fn is_coercible_from_func( &mut self, sort: &Sort, fhir_id: FhirId, ) -> Option<PolyFuncSort>

fn is_coercible_to_func( &mut self, sort: &Sort, fhir_id: FhirId, ) -> Option<PolyFuncSort>

fn try_equate(&mut self, sort1: &Sort, sort2: &Sort) -> Option<Sort>

fn try_equate_inner(&mut self, sort1: &Sort, sort2: &Sort) -> Option<Sort>

fn try_equate_bv_sizes( &mut self, size1: BvSize, size2: BvSize, ) -> Option<BvSize>

fn equate(&mut self, sort1: &Sort, sort2: &Sort) -> Sort

pub(crate) fn next_sort_var(&mut self) -> Sort

fn next_num_var(&mut self) -> Sort

pub(crate) fn next_sort_vid(&mut self) -> SortVid

fn next_num_vid(&mut self) -> NumVid

fn next_bv_size_var(&mut self) -> BvSize

fn next_bv_size_vid(&mut self) -> BvSizeVid

pub(crate) fn resolve_param_sort( &mut self, param: &RefineParam<'_>, ) -> Result<(), ErrorGuaranteed>

fn ensure_resolved_var( &mut self, path: &PathExpr<'_>, ) -> Result<Sort, ErrorGuaranteed>

fn is_single_field_record(&mut self, sort: &Sort) -> Option<(DefId, Sort)>

pub(crate) fn into_results(self) -> WfckResults

pub(crate) fn infer_mode(&self, id: ParamId) -> InferMode

pub(crate) fn param_sort(&self, id: ParamId) -> Sort

fn shallow_resolve(&mut self, sort: &Sort) -> Sort

fn resolve_vars_if_possible(&mut self, sort: &Sort) -> Sort

pub(crate) fn fully_resolve(&mut self, sort: &Sort) -> Result<Sort, ()>

impl InferCtxt<'_, '_>

fn emit_sort_mismatch( &mut self, span: Span, expected: &Sort, found: &Sort, ) -> ErrorGuaranteed

fn emit_field_not_found(&mut self, sort: &Sort, field: Ident) -> ErrorGuaranteed

fn emit_err<'b>(&'b self, err: impl Diagnostic<'b>) -> ErrorGuaranteed

Trait Implementations

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.

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

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

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

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

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

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