Struct RefinementResolver

pub(crate) struct RefinementResolver<'a, 'genv, 'tcx> {
    scopes: Vec<Scope>,
    sort_params: FxIndexSet<Symbol>,
    param_defs: FxIndexMap<NodeId, ParamDef>,
    resolver: &'a mut CrateResolver<'genv, 'tcx>,
    path_res_map: FxHashMap<NodeId, ExprRes<NodeId>>,
    errors: Errors<'genv>,
}

Fields

scopes: Vec<Scope>

sort_params: FxIndexSet<Symbol>

param_defs: FxIndexMap<NodeId, ParamDef>

resolver: &'a mut CrateResolver<'genv, 'tcx>

path_res_map: FxHashMap<NodeId, ExprRes<NodeId>>

errors: Errors<'genv>

Implementations

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

pub(crate) fn for_flux_item( resolver: &'a mut CrateResolver<'genv, 'tcx>, sort_params: &[Ident], ) -> Self

pub(crate) fn for_rust_item( resolver: &'a mut CrateResolver<'genv, 'tcx>, ) -> Self

pub(crate) fn resolve_qualifier( resolver: &'a mut CrateResolver<'genv, 'tcx>, qualifier: &Qualifier, ) -> Result<(), ErrorGuaranteed>

pub(crate) fn resolve_defn( resolver: &'a mut CrateResolver<'genv, 'tcx>, defn: &SpecFunc, ) -> Result<(), ErrorGuaranteed>

pub(crate) fn resolve_fn_sig( resolver: &'a mut CrateResolver<'genv, 'tcx>, fn_sig: &FnSig, ) -> Result<(), ErrorGuaranteed>

pub(crate) fn resolve_struct_def( resolver: &'a mut CrateResolver<'genv, 'tcx>, struct_def: &StructDef, ) -> Result<(), ErrorGuaranteed>

pub(crate) fn resolve_enum_def( resolver: &'a mut CrateResolver<'genv, 'tcx>, enum_def: &EnumDef, ) -> Result<(), ErrorGuaranteed>

pub(crate) fn resolve_constant( resolver: &'a mut CrateResolver<'genv, 'tcx>, constant_info: &ConstantInfo, ) -> Result<(), ErrorGuaranteed>

pub(crate) fn resolve_ty_alias( resolver: &'a mut CrateResolver<'genv, 'tcx>, ty_alias: &TyAlias, ) -> Result<(), ErrorGuaranteed>

pub(crate) fn resolve_impl( resolver: &'a mut CrateResolver<'genv, 'tcx>, impl_: &Impl, ) -> Result<(), ErrorGuaranteed>

pub(crate) fn resolve_trait( resolver: &'a mut CrateResolver<'genv, 'tcx>, trait_: &Trait, ) -> Result<(), ErrorGuaranteed>

fn new( resolver: &'a mut CrateResolver<'genv, 'tcx>, sort_params: FxIndexSet<Symbol>, ) -> Self

fn run( self, f: impl FnOnce(&mut ScopedVisitorWrapper<Self>), ) -> Result<(), ErrorGuaranteed>

fn define_param( &mut self, ident: Ident, kind: ParamKind, param_id: NodeId, scope: Option<NodeId>, )

fn find(&mut self, ident: Ident) -> Option<ParamRes>

fn try_resolve_enum_variant( &mut self, typ: Ident, variant: Ident, ) -> Option<ExprRes<NodeId>>

fn resolve_path(&mut self, path: &ExprPath)

fn resolve_ident(&mut self, ident: Ident, node_id: NodeId)

fn try_resolve_expr_with_ribs<S: Segment>( &mut self, segments: &[S], ) -> Option<ExprRes<NodeId>>

fn try_resolve_param(&mut self, ident: Ident) -> Option<ExprRes<NodeId>>

fn try_resolve_global_func(&mut self, ident: Ident) -> Option<ExprRes<NodeId>>

fn resolve_sort_path(&mut self, path: &SortPath)

fn try_resolve_sort_param(&self, path: &SortPath) -> Option<SortRes>

fn try_resolve_sort_with_ribs(&mut self, path: &SortPath) -> Option<SortRes>

fn try_resolve_user_sort(&self, path: &SortPath) -> Option<SortRes>

fn try_resolve_prim_sort(&self, path: &SortPath) -> Option<SortRes>

pub(crate) fn finish(self) -> Result<(), ErrorGuaranteed>

fn resolver_output(&self) -> &ResolverOutput

Trait Implementations

impl ScopedVisitor for RefinementResolver<'_, '_, '_>

fn is_box(&self, segment: &PathSegment) -> bool

fn enter_scope(&mut self, kind: ScopeKind) -> ControlFlow<()>

fn exit_scope(&mut self)

fn on_enum_variant(&mut self, variant: &VariantDef)

fn on_fn_sig(&mut self, fn_sig: &FnSig)

fn on_fn_output(&mut self, output: &FnOutput)

fn on_refine_param(&mut self, param: &RefineParam)

fn on_loc(&mut self, loc: Ident, node_id: NodeId)

fn on_path(&mut self, path: &ExprPath)

fn on_base_sort(&mut self, sort: &BaseSort)

fn wrap(self) -> ScopedVisitorWrapper<Self>

fn on_implicit_param( &mut self, _ident: Ident, _kind: ParamKind, _node_id: NodeId, )

fn on_generic_param(&mut self, _param: &GenericParam)