Struct flux_middle::rty::Expr

pub struct Expr {
    kind: Interned<ExprKind>,
    espan: Option<ESpan>,
}

Fields

kind: Interned<ExprKind>

espan: Option<ESpan>

Implementations

impl Expr

pub fn at_opt(self, espan: Option<ESpan>) -> Expr

pub fn at(self, espan: ESpan) -> Expr

pub fn at_base(self, base: ESpan) -> Expr

pub fn span(&self) -> Option<ESpan>

pub fn tt() -> Expr

pub fn ff() -> Expr

pub fn and_from_iter(exprs: impl IntoIterator<Item = Expr>) -> Expr

pub fn or_from_iter(exprs: impl IntoIterator<Item = Expr>) -> Expr

pub fn and(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr

pub fn or(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr

pub fn zero() -> Expr

pub fn int_max(int_ty: IntTy) -> Expr

pub fn int_min(int_ty: IntTy) -> Expr

pub fn uint_max(uint_ty: UintTy) -> Expr

pub fn nu() -> Expr

pub fn is_nu(&self) -> bool

pub fn expect_adt(&self) -> (DefId, List<Expr>)

pub fn unit() -> Expr

pub fn var(var: Var) -> Expr

pub fn fvar(name: Name) -> Expr

pub fn evar(evar: EVar) -> Expr

pub fn bvar(debruijn: DebruijnIndex, var: BoundVar, kind: BoundReftKind) -> Expr

pub fn early_param(index: u32, name: Symbol) -> Expr

pub fn local(local: Local) -> Expr

pub fn constant(c: Constant) -> Expr

pub fn const_def_id(c: DefId) -> Expr

pub fn const_generic(param: ParamConst) -> Expr

pub fn aggregate(kind: AggregateKind, flds: List<Expr>) -> Expr

pub fn tuple(flds: List<Expr>) -> Expr

pub fn adt(def_id: DefId, flds: List<Expr>) -> Expr

pub fn from_bits(bty: &BaseTy, bits: u128) -> Expr

pub fn ite(p: impl Into<Expr>, e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr

pub fn abs(lam: Lambda) -> Expr

pub fn hole(kind: HoleKind) -> Expr

pub fn kvar(kvar: KVar) -> Expr

pub fn alias(alias: AliasReft, args: List<Expr>) -> Expr

pub fn forall(expr: Binder<Expr>) -> Expr

pub fn binary_op(op: BinOp, e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr

pub fn unit_adt(def_id: DefId) -> Expr

pub fn app(func: impl Into<Expr>, args: List<Expr>) -> Expr

pub fn global_func(func: Symbol, kind: SpecFuncKind) -> Expr

pub fn eq(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr

pub fn unary_op(op: UnOp, e: impl Into<Expr>) -> Expr

pub fn ne(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr

pub fn ge(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr

pub fn gt(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr

pub fn lt(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr

pub fn le(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr

pub fn implies(e1: impl Into<Expr>, e2: impl Into<Expr>) -> Expr

pub fn field_proj(e: impl Into<Expr>, proj: FieldProj) -> Expr

pub fn field_projs(e: impl Into<Expr>, projs: &[FieldProj]) -> Expr

pub fn path_proj(base: Expr, field: FieldIdx) -> Expr

pub fn not(&self) -> Expr

pub fn neg(&self) -> Expr

pub fn kind(&self) -> &ExprKind

pub fn is_atom(&self) -> bool

An expression is an atom if it is “self-delimiting”, i.e., it has a clear boundary when printed. This is used to avoid unnecessary parenthesis when pretty printing.

pub fn is_trivially_true(&self) -> bool

Simple syntactic check to see if the expression is a trivially true predicate. This is used mostly for filtering predicates when pretty printing but also to simplify types in general.

pub fn is_trivially_false(&self) -> bool

Simple syntactic check to see if the expression is a trivially false predicate.

fn is_true(&self) -> bool

Whether the expression is literally the constant true.

fn is_false(&self) -> bool

Whether the expression is literally the constant false.

pub fn from_const(tcx: TyCtxt<'_>, c: &Const) -> Expr

pub fn is_binary_op(&self) -> bool

fn const_op(op: &BinOp, c1: &Constant, c2: &Constant) -> Option<Constant>

pub fn simplify(&self) -> Expr

Simplify the expression by removing double negations, short-circuiting boolean connectives and doing constant folding. Note that we also have TypeFoldable::normalize which applies beta reductions for tuples and abstractions.

pub fn to_loc(&self) -> Option<Loc>

pub fn to_path(&self) -> Option<Path>

pub fn is_abs(&self) -> bool

pub fn is_unit(&self) -> bool

Whether this is an aggregate expression with no fields.

pub fn eta_expand_abs( &self, inputs: &BoundVariableKinds, output: Sort, ) -> Lambda

pub fn fold_sort(sort: &Sort, f: impl FnMut(&Sort) -> Expr) -> Expr

pub fn proj_and_reduce(&self, proj: FieldProj) -> Expr

Applies a field projection to an expression and optimistically try to beta reduce it

pub fn flatten_conjs(&self) -> Vec<&Expr>

Trait Implementations

impl<Rhs> Add<Rhs> for &Expr

where Rhs: Into<Expr>,

type Output = Expr

The resulting type after applying the + operator.

fn add(self, rhs: Rhs) -> Self::Output

Performs the + operation.

impl<Rhs> Add<Rhs> for Expr

where Rhs: Into<Expr>,

type Output = Expr

The resulting type after applying the + operator.

fn add(self, rhs: Rhs) -> Self::Output

Performs the + operation.

impl Clone for Expr

fn clone(&self) -> Expr

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Expr

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

Formats the value using the given formatter.

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

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

impl<Rhs> Div<Rhs> for &Expr

where Rhs: Into<Expr>,

type Output = Expr

The resulting type after applying the / operator.

fn div(self, rhs: Rhs) -> Self::Output

Performs the / operation.

impl<Rhs> Div<Rhs> for Expr

where Rhs: Into<Expr>,

type Output = Expr

The resulting type after applying the / operator.

fn div(self, rhs: Rhs) -> Self::Output

Performs the / operation.

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

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

impl From<&Expr> for Expr

fn from(e: &Expr) -> Self

Converts to this type from the input type.

impl From<Name> for Expr

fn from(name: Name) -> Self

Converts to this type from the input type.

impl From<Path> for Expr

fn from(path: Path) -> Self

Converts to this type from the input type.

impl From<Var> for Expr

fn from(var: Var) -> Self

Converts to this type from the input type.

impl From<i32> for Expr

fn from(value: i32) -> Self

Converts to this type from the input type.

impl Hash for Expr

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<Rhs> Mul<Rhs> for &Expr

where Rhs: Into<Expr>,

type Output = Expr

The resulting type after applying the * operator.

fn mul(self, rhs: Rhs) -> Self::Output

Performs the * operation.

impl<Rhs> Mul<Rhs> for Expr

where Rhs: Into<Expr>,

type Output = Expr

The resulting type after applying the * operator.

fn mul(self, rhs: Rhs) -> Self::Output

Performs the * operation.

impl PartialEq for Expr

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

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

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

impl SliceInternable for Expr

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

impl<Rhs> Sub<Rhs> for &Expr

where Rhs: Into<Expr>,

type Output = Expr

The resulting type after applying the - operator.

fn sub(self, rhs: Rhs) -> Self::Output

Performs the - operation.

impl<Rhs> Sub<Rhs> for Expr

where Rhs: Into<Expr>,

type Output = Expr

The resulting type after applying the - operator.

fn sub(self, rhs: Rhs) -> Self::Output

Performs the - operation.

impl TypeFoldable for Expr

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 Expr

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 Expr

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

impl TypeVisitable for Expr

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 Expr

impl StructuralPartialEq for Expr