Enum ExprKind

pub enum ExprKind {
    Var(Var),
    Local(Local),
    Constant(Constant),
    ConstDefId(DefId),
    BinaryOp(BinOp, Expr, Expr),
    GlobalFunc(Symbol, SpecFuncKind),
    UnaryOp(UnOp, Expr),
    FieldProj(Expr, FieldProj),
    Aggregate(AggregateKind, List<Expr>),
    PathProj(Expr, FieldIdx),
    IfThenElse(Expr, Expr, Expr),
    KVar(KVar),
    Alias(AliasReft, List<Expr>),
    App(Expr, List<Expr>),
    Abs(Lambda),
    Hole(HoleKind),
    ForAll(Binder<Expr>),
}

Variants

Var(Var)

Local(Local)

Constant(Constant)

ConstDefId(DefId)

BinaryOp(BinOp, Expr, Expr)

GlobalFunc(Symbol, SpecFuncKind)

UnaryOp(UnOp, Expr)

FieldProj(Expr, FieldProj)

Aggregate(AggregateKind, List<Expr>)

PathProj(Expr, FieldIdx)

IfThenElse(Expr, Expr, Expr)

KVar(KVar)

Alias(AliasReft, List<Expr>)

App(Expr, List<Expr>)

Function application. The syntax allows arbitrary expressions in function position, but in practice we are restricted by what’s possible to encode in fixpoint. In a nutshell, we need to make sure that expressions that can’t be encoded are eliminated before we generate the fixpoint constraint. Most notably, lambda abstractions have to be fully applied before encoding into fixpoint (except when they appear as an index at the top-level).

Abs(Lambda)

Lambda abstractions. They are purely syntactic and we don’t encode them in the logic. As such, they have some syntactic restrictions that we must carefully maintain:

1. They can appear as an index at the top level.
2. We can only substitute an abstraction for a variable in function position (or as an index). More generally, we need to partially evaluate expressions such that all abstractions in non-index position are eliminated before encoding into fixpoint. Right now, the implementation only evaluates abstractions that are immediately applied to arguments, thus the restriction.

Hole(HoleKind)

A hole is an expression that must be inferred either semantically by generating a kvar or syntactically by generating an evar. Whether a hole can be inferred semantically or syntactically depends on the position it appears: only holes appearing in predicate position can be inferred with a kvar (provided it satisfies the fixpoint horn constraints) and only holes used as an index (a position that fully determines their value) can be inferred with an evar.

Holes are implicitly defined in a scope, i.e., their solution could mention free and bound variables in this scope. This must be considered when generating an inference variables for them (either evar or kvar). In fact, the main reason we have holes is that we want to decouple the places where we generate holes (where we don’t want to worry about the scope), and the places where we generate inference variable for them (where we do need to worry about the scope).

ForAll(Binder<Expr>)

Implementations

impl ExprKind

fn intern(self) -> Expr

Trait Implementations

impl Clone for ExprKind

fn clone(&self) -> ExprKind

Returns a copy of the value.

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

Performs copy-assignment from source.

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

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

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

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

impl Hash for ExprKind

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 Internable for ExprKind

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

impl PartialEq for ExprKind

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

impl StructuralPartialEq for ExprKind