Enum flux_middle::rty::Sort

pub enum Sort {
    Int,
    Bool,
    Real,
    BitVec(BvSize),
    Str,
    Char,
    Loc,
    Param(ParamTy),
    Tuple(List<Sort>),
    Alias(AliasKind, AliasTy),
    Func(PolyFuncSort),
    App(SortCtor, List<Sort>),
    Var(ParamSort),
    Infer(SortInfer),
    Err,
}

Variants

Int

Bool

Real

BitVec(BvSize)

Str

Char

Loc

Param(ParamTy)

Tuple(List<Sort>)

Alias(AliasKind, AliasTy)

Func(PolyFuncSort)

App(SortCtor, List<Sort>)

Var(ParamSort)

Infer(SortInfer)

Err

Implementations

impl Sort

pub fn tuple(sorts: impl Into<List<Sort>>) -> Self

pub fn app(ctor: SortCtor, sorts: List<Sort>) -> Self

pub fn unit() -> Self

pub fn expect_func(&self) -> &PolyFuncSort

pub fn is_loc(&self) -> bool

pub fn is_unit(&self) -> bool

pub fn is_unit_adt(&self) -> Option<DefId>

pub fn is_pred(&self) -> bool

Whether the sort is a function with return sort bool

pub fn is_bool(&self) -> bool

Returns true if the sort is Bool.

pub fn is_numeric(&self) -> bool

pub fn walk(&self, f: impl FnMut(&Sort, &[FieldProj]))

Trait Implementations

impl Clone for Sort

fn clone(&self) -> Sort

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Sort

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

Formats the value using the given formatter.

impl<__D: TyDecoder> Decodable<__D> for Sort

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

impl<__E: TyEncoder> Encodable<__E> for Sort

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

impl From<Sort> for BoundVariableKind

fn from(sort: Sort) -> Self

Converts to this type from the input type.

impl Hash for Sort

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 IntoDiagArg for Sort

fn into_diag_arg(self) -> DiagArgValue

impl PartialEq for Sort

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

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

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

impl SliceInternable for Sort

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

impl TypeFoldable for Sort

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_projections<'tcx>( &self, genv: GlobalEnv<'_, 'tcx>, infcx: &InferCtxt<'tcx>, callsite_def_id: DefId, ) -> QueryResult<Self>

fn normalize(&self, defns: &SpecFuncDefns) -> 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, evars: &EVarSol) -> Self

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

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

fn erase_regions(&self) -> Self

impl TypeSuperFoldable for Sort

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

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

impl TypeSuperVisitable for Sort

fn super_visit_with<V: TypeVisitor>( &self, visitor: &mut V, ) -> ControlFlow<V::BreakTy>

impl TypeVisitable for Sort

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}.

impl Eq for Sort

impl EqUnifyValue for Sort

impl StructuralPartialEq for Sort