Enum InferMode 

pub enum InferMode {
    EVar,
    KVar,
}

Inference mode for a parameter.

Variants

EVar

Generate a fresh evar for the parameter and solve it via syntactic unification. The parameter must appear at least once as an index for unification to succeed, but otherwise it can appear (mostly) freely.

KVar

Generate a fresh kvar and let fixpoint infer it. This mode can only be used with abstract refinement predicates. If the parameter is marked as kvar then it can only appear in positions that will result in a horn constraint as required by fixpoint.

Implementations

impl InferMode

pub fn from_param_kind(kind: ParamKind) -> InferMode

pub fn prefix_str(self) -> &'static str

Trait Implementations

impl Clone for InferMode

fn clone(&self) -> InferMode

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for InferMode

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

Formats the value using the given formatter.

impl<__D: SpanDecoder> Decodable<__D> for InferMode

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

impl<__E: SpanEncoder> Encodable<__E> for InferMode

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

impl Hash for InferMode

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 InferMode

fn eq(&self, other: &InferMode) -> 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 SliceInternable for InferMode

fn storage() -> &'static InternStorage<[Self]>

impl TypeFoldable for InferMode

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

fn fold_with<F: TypeFolder>(&self, _: &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 InferMode

fn visit_with<V: TypeVisitor>(&self, _: &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) -> FxHashSet<BoundVar>

Gives the indices of the provided bvars which:

impl Copy for InferMode

impl Eq for InferMode

impl StructuralPartialEq for InferMode