Struct Wf

struct Wf<'a, 'genv, 'tcx> {
    infcx: &'a mut InferCtxt<'genv, 'tcx>,
    errors: Errors<'genv>,
    next_type_index: u32,
    next_region_index: u32,
    next_const_index: u32,
}

Fields

infcx: &'a mut InferCtxt<'genv, 'tcx>

errors: Errors<'genv>

next_type_index: u32

next_region_index: u32

next_const_index: u32

Implementations

impl<'a, 'genv, 'tcx> Wf<'a, 'genv, 'tcx>

fn new(infcx: &'a mut InferCtxt<'genv, 'tcx>) -> Self

fn check_node(&mut self, node: &OwnerNode<'genv>)

fn insert_params( &mut self, params: &[RefineParam<'_>], ) -> Result<(), ErrorGuaranteed>

Push a layer of binders. We assume all names are fresh so we don’t care about shadowing

fn insert_params_for_node( &mut self, node: &OwnerNode<'_>, ) -> Result<(), ErrorGuaranteed>

Initializes the inference context with all refinement parameters in node

fn init_infcx(&mut self, node: &OwnerNode<'genv>) -> QueryResult

To check for well-formedness we need to know the sort of base types. For example, to check if the type i32[e] is well formed, we need to know that the sort of i32 is int so we can check the expression e against it. Computing the sort from a base type is subtle and hard to do in fhir so we must do it in rty. However, to convert from fhir to rty we need elaborated information from sort checking which we do in fhir.

To break this circularity, we do conversion in two phases. In the first phase, we do conversion without elaborated information. This results in types in rty with incorrect refinements but with the right shape to compute their sorts. We use these sorts for sort checking and then do conversion again with the elaborated information.

This function initializes the inference context by running the first phase of conversion and collecting the sort of all base types.

fn check_output_locs(&mut self, fn_decl: &FnDecl<'_>)

Trait Implementations

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

const EXPAND_TYPE_ALIASES: bool = false

We don’t expand type aliases before sort checking because we need every base type in fhir to match a type in rty.

const HAS_ELABORATED_INFORMATION: bool = false

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

type Results = InferCtxt<'genv, 'tcx>

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.

fn into_conv_ctxt(self) -> ConvCtxt<Self>

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

impl<'genv> Visitor<'genv> for Wf<'_, 'genv, '_>

fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)

fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)

fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)

fn visit_fn_decl(&mut self, decl: &FnDecl<'genv>)

fn visit_requires(&mut self, requires: &Requires<'genv>)

fn visit_ensures(&mut self, ensures: &Ensures<'genv>)

fn visit_ty(&mut self, ty: &Ty<'genv>)

fn visit_path(&mut self, path: &Path<'genv>)

fn visit_node(&mut self, node: &OwnerNode<'v>)

fn visit_item(&mut self, item: &Item<'v>)

fn visit_trait_item(&mut self, trait_item: &TraitItem<'v>)

fn visit_impl_item(&mut self, impl_item: &ImplItem<'v>)

fn visit_generics(&mut self, generics: &Generics<'v>)

fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'v>)

fn visit_impl(&mut self, impl_: &Impl<'v>)

fn visit_struct_def(&mut self, struct_def: &StructDef<'v>)

fn visit_enum_def(&mut self, enum_def: &EnumDef<'v>)

fn visit_variant(&mut self, variant: &VariantDef<'v>)

fn visit_field_def(&mut self, field: &FieldDef<'v>)

fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'v>)

fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'v>)

fn visit_generic_bound(&mut self, bound: &GenericBound<'v>)

fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'v>)

fn visit_fn_sig(&mut self, sig: &FnSig<'v>)

fn visit_refine_param(&mut self, param: &RefineParam<'v>)

fn visit_fn_output(&mut self, output: &FnOutput<'v>)

fn visit_generic_arg(&mut self, arg: &GenericArg<'v>)

fn visit_lifetime(&mut self, _lft: &Lifetime)

fn visit_bty(&mut self, bty: &BaseTy<'v>)

fn visit_qpath(&mut self, qpath: &QPath<'v>)

fn visit_path_segment(&mut self, segment: &PathSegment<'v>)

fn visit_assoc_item_constraint(&mut self, constraint: &AssocItemConstraint<'v>)

fn visit_sort(&mut self, sort: &Sort<'v>)

fn visit_sort_path(&mut self, path: &SortPath<'v>)

fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'v>)

fn visit_func_sort(&mut self, func: &FuncSort<'v>)

fn visit_expr(&mut self, expr: &Expr<'v>)

fn visit_field_expr(&mut self, expr: &FieldExpr<'v>)

fn visit_alias_reft(&mut self, alias_reft: &AliasReft<'v>)

fn visit_literal(&mut self, _lit: &Lit)

fn visit_path_expr(&mut self, _path: &PathExpr<'v>)