Enum IrExpr 

pub enum IrExpr {
    Var(String),
    Literal(IrLiteral),
    FieldAccess {
        root: Box<IrExpr>,
        field: String,
    },
    Compare {
        left: Box<IrExpr>,
        op: CmpOp,
        right: Box<IrExpr>,
    },
    Arithmetic {
        left: Box<IrExpr>,
        op: ArithOp,
        right: Box<IrExpr>,
    },
    And(Box<IrExpr>, Box<IrExpr>),
    Or(Box<IrExpr>, Box<IrExpr>),
    Not(Box<IrExpr>),
    Implies(Box<IrExpr>, Box<IrExpr>),
    Old(Box<IrExpr>),
    Forall {
        binding: String,
        ty: String,
        body: Box<IrExpr>,
    },
    Exists {
        binding: String,
        ty: String,
        body: Box<IrExpr>,
    },
    Call {
        name: String,
        args: Vec<IrExpr>,
    },
}

An IR expression — a simplified, typed expression tree.

Variants

Var(String)

Variable reference (parameter name or quantifier binding).

Literal(IrLiteral)

Literal value.

FieldAccess

Field access: obj.field

Fields

root: Box<IrExpr>

field: String

Compare

Binary comparison.

Fields

left: Box<IrExpr>

op: CmpOp

right: Box<IrExpr>

Arithmetic

Arithmetic operation.

Fields

left: Box<IrExpr>

op: ArithOp

right: Box<IrExpr>

And(Box<IrExpr>, Box<IrExpr>)

Logical AND.

Or(Box<IrExpr>, Box<IrExpr>)

Logical OR.

Not(Box<IrExpr>)

Logical NOT.

Implies(Box<IrExpr>, Box<IrExpr>)

Logical implication: a => b ≡ !a || b.

Old(Box<IrExpr>)

Pre-state reference: old(expr).

Forall

Universal quantifier: forall x: T => body.

Fields

binding: String

ty: String

body: Box<IrExpr>

Exists

Existential quantifier: exists x: T => body.

Fields

binding: String

ty: String

body: Box<IrExpr>

Call

Function call.

Fields

name: String

args: Vec<IrExpr>

Trait Implementations

impl Clone for IrExpr

fn clone(&self) -> IrExpr

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for IrExpr

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

Formats the value using the given formatter.

impl Serialize for IrExpr

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.