Struct WKVar 

pub struct WKVar {
    pub wkvid: WKVid,
    pub self_args: usize,
    pub args: List<Expr>,
}

A weak kvar is like a kvar with the exception that it infers the weakest condition necessary instead of the strongest condition. Due to the way we generate these kvars (on fn_sigs, rather than during constraint generation), they also in theory are global.

Fields

wkvid: WKVid

self_args: usize

Analagous to KVar self arguments except we require that instantiations use at least one of the self_args (unless there are none, in which case there is no such requirement).

This is mostly relevant for weak kvars corresponding to function outputs. Consider the signature

foo: fn(x: usize) -> bool{b: $wk1(b, x)}
       requires $wk0(x)

In this case self_args would be 1 (corresponding to the bool b). Consider now the snippet

let b = foo(x);
assert(x > 0);

Suppose the assertion fails. Without the self_args requirement, we could validly instantiate

$wk1(b, x) := x > 0

But this is somewhat nonsensical because only in exceptional cases does it make sense for foo to somehow “add” information to its argument (x).

By checking for the presence of at least one self arg, we ensure that the self argument is “used”; fixpoint does a similar check.

This is a syntactic underapproximation and doesn’t preclude things like

$wk1(b, x) := (b => true) && (x > 0)

But we could conceive of a more sophisticated check using the self_args.

args: List<Expr>

All arguments with self arguments at the beginning.

Implementations

impl WKVar

fn self_args(&self) -> &[Expr]

fn scope(&self) -> &[Expr]

Trait Implementations

impl Clone for WKVar

fn clone(&self) -> WKVar

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for WKVar

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

Formats the value using the given formatter.

impl<'tcx, __D: TyDecoder<'tcx>> Decodable<__D> for WKVar

fn decode(__decoder: &mut __D) -> Self

impl<'tcx, __E: TyEncoder<'tcx>> Encodable<__E> for WKVar

fn encode(&self, __encoder: &mut __E)

impl Hash for WKVar

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for WKVar

fn eq(&self, other: &WKVar) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Pretty for WKVar

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

fn default_cx(tcx: TyCtxt<'_>) -> PrettyCx<'_, '_>

impl TypeFoldable for WKVar

fn try_fold_with<__F: FallibleTypeFolder>( &self, __folder: &mut __F, ) -> Result<Self, __F::Error>

fn fold_with<F: TypeFolder>(&self, folder: &mut F) -> Self

fn normalize(&self, genv: GlobalEnv<'_, '_>) -> Self

Normalize expressions by applying beta reductions for tuples and lambda abstractions.

fn replace_holes( &self, f: impl FnMut(&[BoundVariableKinds], HoleKind) -> Expr, ) -> Self

Replaces all holes with the result of calling a closure. The closure takes a list with all the layers of bound variables at the point the hole was found. Each layer corresponds to the list of bound variables at that level. The list is ordered from outermost to innermost binder, i.e., the last element is the binder closest to the hole.

fn with_holes(&self) -> Self

Remove all refinements and turn each underlying BaseTy into a TyKind::Exists with a TyKind::Constr and a hole. For example, Vec<{v. i32[v] | v > 0}>[n] becomes {n. Vec<{v. i32[v] | *}>[n] | *}.

fn replace_evars( &self, f: &mut impl FnMut(EVid) -> Option<Expr>, ) -> Result<Self, EVid>

fn shift_horizontally(&self, amount: usize) -> Self

Shift the BoundVar of all the the variables at index INNERMOST “horizontally” to the right by the specified amount.

fn shift_in_escaping(&self, amount: u32) -> Self

fn shift_out_escaping(&self, amount: u32) -> Self

fn erase_regions(&self) -> Self

impl TypeVisitable for WKVar

fn visit_with<__V: TypeVisitor>( &self, __visitor: &mut __V, ) -> ControlFlow<__V::BreakTy>

fn has_escaping_bvars(&self) -> bool

fn has_escaping_bvars_at_or_above(&self, binder: DebruijnIndex) -> bool

Returns true if self has any late-bound vars that are either bound by binder or bound by some binder outside of binder. If binder is ty::INNERMOST, this indicates whether there are any late-bound vars that appear free.

fn fvars(&self) -> FxHashSet<Name>

Returns the set of all free variables. For example, Vec<i32[n]>{v : v > m} returns {n, m}.

fn early_params(&self) -> FxHashSet<EarlyReftParam>

fn redundant_bvars(&self) -> UnordSet<BoundVar>

Gives the indices of the provided bvars which:

impl Eq for WKVar

impl StructuralPartialEq for WKVar