Struct InferCtxt

pub struct InferCtxt<'infcx, 'genv, 'tcx> {
    pub genv: GlobalEnv<'genv, 'tcx>,
    pub region_infcx: &'infcx InferCtxt<'tcx>,
    pub def_id: DefId,
    pub check_overflow: bool,
    cursor: Cursor<'infcx>,
    inner: &'infcx RefCell<InferCtxtInner>,
}

Fields

genv: GlobalEnv<'genv, 'tcx>

region_infcx: &'infcx InferCtxt<'tcx>

def_id: DefId

check_overflow: bool

cursor: Cursor<'infcx>

inner: &'infcx RefCell<InferCtxtInner>

Implementations

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

pub fn at(&mut self, span: Span) -> InferCtxtAt<'_, 'infcx, 'genv, 'tcx>

pub fn instantiate_refine_args( &mut self, callee_def_id: DefId, args: &[GenericArg], ) -> InferResult<List<Expr>>

pub fn instantiate_generic_args( &mut self, args: &[GenericArg], ) -> Vec<GenericArg>

pub fn fresh_infer_var(&self, sort: &Sort, mode: InferMode) -> Expr

pub fn fresh_infer_var_for_hole( &mut self, binders: &[BoundVariableKinds], kind: HoleKind, ) -> Expr

pub fn fresh_kvar( &self, binders: &[BoundVariableKinds], encoding: KVarEncoding, ) -> Expr

Generate a fresh kvar in the current scope. See KVarGen::fresh.

fn fresh_evar(&self) -> Expr

pub fn unify_exprs(&self, a: &Expr, b: &Expr)

fn enter_exists<T, U>( &mut self, t: &Binder<T>, f: impl FnOnce(&mut InferCtxt<'_, 'genv, 'tcx>, T) -> U, ) -> U

where T: TypeFoldable,

pub fn push_evar_scope(&mut self)

Used in conjunction with InferCtxt::pop_evar_scope to ensure evars are solved at the end of some scope, for example, to ensure all evars generated during a function call are solved after checking argument subtyping. These functions can be used in a stack-like fashion to create nested scopes.

pub fn pop_evar_scope(&mut self) -> InferResult

Pop a scope and check all evars have been solved. This only check evars generated from the last call to InferCtxt::push_evar_scope.

pub fn ensure_resolved_evars<R>( &mut self, f: impl FnOnce(&mut Self) -> InferResult<R>, ) -> InferResult<R>

Convenience method pairing InferCtxt::push_evar_scope and InferCtxt::pop_evar_scope.

pub fn fully_resolve_evars<T: TypeFoldable>(&self, t: &T) -> T

pub fn tcx(&self) -> TyCtxt<'tcx>

pub fn cursor(&self) -> &Cursor<'infcx>

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

Methods that interact with the underlying Cursor

pub fn change_item<'a>( &'a mut self, def_id: LocalDefId, region_infcx: &'a InferCtxt<'tcx>, ) -> InferCtxt<'a, 'genv, 'tcx>

pub fn move_to( &mut self, marker: &Marker, clear_children: bool, ) -> InferCtxt<'_, 'genv, 'tcx>

pub fn branch(&mut self) -> InferCtxt<'_, 'genv, 'tcx>

pub fn define_var(&mut self, sort: &Sort) -> Name

pub fn check_pred(&mut self, pred: impl Into<Expr>, tag: Tag)

pub fn assume_pred(&mut self, pred: impl Into<Expr>)

pub fn unpack(&mut self, ty: &Ty) -> Ty

pub fn marker(&self) -> Marker

pub fn hoister( &mut self, assume_invariants: bool, ) -> Hoister<Unpacker<'_, 'infcx>>

pub fn assume_invariants(&mut self, ty: &Ty)

fn check_impl( &mut self, pred1: impl Into<Expr>, pred2: impl Into<Expr>, tag: Tag, )

Trait Implementations

impl Debug for InferCtxt<'_, '_, '_>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.