Enum ExprKind 

pub enum ExprKind {
    Bool(bool),
    Int(i64),
    String(String),
    Ident(String),
    Primed(String),
    Binary {
        op: BinOp,
        left: Box<Expr>,
        right: Box<Expr>,
    },
    Unary {
        op: UnaryOp,
        operand: Box<Expr>,
    },
    Index {
        base: Box<Expr>,
        index: Box<Expr>,
    },
    Slice {
        base: Box<Expr>,
        lo: Box<Expr>,
        hi: Box<Expr>,
    },
    Field {
        base: Box<Expr>,
        field: Ident,
    },
    Call {
        func: Box<Expr>,
        args: Vec<Expr>,
    },
    SetLit(Vec<Expr>),
    SeqLit(Vec<Expr>),
    TupleLit(Vec<Expr>),
    DictLit(Vec<(Expr, Expr)>),
    FnLit {
        var: Ident,
        domain: Box<Expr>,
        body: Box<Expr>,
    },
    SetComprehension {
        element: Box<Expr>,
        var: Ident,
        domain: Box<Expr>,
        filter: Option<Box<Expr>>,
    },
    RecordUpdate {
        base: Box<Expr>,
        updates: Vec<RecordFieldUpdate>,
    },
    Quantifier {
        kind: QuantifierKind,
        bindings: Vec<Binding>,
        body: Box<Expr>,
    },
    Choose {
        var: Ident,
        domain: Box<Expr>,
        predicate: Box<Expr>,
    },
    Fix {
        var: Ident,
        predicate: Box<Expr>,
    },
    Let {
        var: Ident,
        value: Box<Expr>,
        body: Box<Expr>,
    },
    If {
        cond: Box<Expr>,
        then_branch: Box<Expr>,
        else_branch: Box<Expr>,
    },
    Require(Box<Expr>),
    Changes(Ident),
    Enabled(Ident),
    SeqHead(Box<Expr>),
    SeqTail(Box<Expr>),
    Len(Box<Expr>),
    Keys(Box<Expr>),
    Values(Box<Expr>),
    BigUnion(Box<Expr>),
    Powerset(Box<Expr>),
    Always(Box<Expr>),
    Eventually(Box<Expr>),
    LeadsTo {
        left: Box<Expr>,
        right: Box<Expr>,
    },
    Range {
        lo: Box<Expr>,
        hi: Box<Expr>,
    },
    Paren(Box<Expr>),
}

The kind of expression.

Variants

Bool(bool)

Boolean literal.

Int(i64)

Integer literal.

String(String)

String literal.

Ident(String)

Identifier.

Primed(String)

Primed identifier (next-state variable).

Binary

Binary operation.

Fields

op: BinOp

left: Box<Expr>

right: Box<Expr>

Unary

Unary operation.

Fields

op: UnaryOp

operand: Box<Expr>

Index

Function/set/sequence indexing e[i].

Fields

base: Box<Expr>

index: Box<Expr>

Slice

Sequence slicing e[lo..hi].

Fields

base: Box<Expr>

lo: Box<Expr>

hi: Box<Expr>

Field

Field access e.field.

Fields

base: Box<Expr>

field: Ident

Call

Function call f(args).

Fields

func: Box<Expr>

args: Vec<Expr>

SetLit(Vec<Expr>)

Set literal { a, b, c } or empty {}.

SeqLit(Vec<Expr>)

Sequence literal [a, b, c] or empty [].

TupleLit(Vec<Expr>)

Tuple literal (a, b, c).

DictLit(Vec<(Expr, Expr)>)

Dict literal { key: value, ... } where keys are expressions.

FnLit

Function literal fn(x in S) => e.

Fields

var: Ident

domain: Box<Expr>

body: Box<Expr>

SetComprehension

Set comprehension { e for x in S } or { x in S if P } or { e for x in S if P }.

Fields

element: Box<Expr>

var: Ident

domain: Box<Expr>

filter: Option<Box<Expr>>

RecordUpdate

Record update e with { field: value, ... }.

Fields

base: Box<Expr>

updates: Vec<RecordFieldUpdate>

Quantifier

Quantifier forall x in S: P or exists x in S: P.

Fields

kind: QuantifierKind

bindings: Vec<Binding>

body: Box<Expr>

Choose

Choose choose x in S: P.

Fields

var: Ident

domain: Box<Expr>

predicate: Box<Expr>

Fix

Fix fix x: P - picks an arbitrary value satisfying P (used for CHOOSE without domain).

Fields

var: Ident

predicate: Box<Expr>

Let

Let binding let x = e1 in e2.

Fields

var: Ident

value: Box<Expr>

body: Box<Expr>

If

Conditional if c then t else f.

Fields

cond: Box<Expr>

then_branch: Box<Expr>

else_branch: Box<Expr>

Require(Box<Expr>)

Require statement (in action body).

Changes(Ident)

Changes operator (explicit nondeterminism).

Enabled(Ident)

Enabled predicate enabled(Action).

SeqHead(Box<Expr>)

Sequence head head(seq) - get first element.

SeqTail(Box<Expr>)

Sequence tail tail(seq) - get all but first element.

Len(Box<Expr>)

Length len(x) - get length of sequence, set, or function.

Keys(Box<Expr>)

Function keys keys(f) - get domain of function as set.

Values(Box<Expr>)

Function values values(f) - get range of function as set.

BigUnion(Box<Expr>)

Distributed union union_all(S) - union of all sets in S.

Powerset(Box<Expr>)

Powerset powerset(S) - set of all subsets of S.

Always(Box<Expr>)

Temporal: always P.

Eventually(Box<Expr>)

Temporal: eventually P.

LeadsTo

Temporal: P leads_to Q.

Fields

left: Box<Expr>

right: Box<Expr>

Range

Range expression lo..hi (as value, not type).

Fields

lo: Box<Expr>

hi: Box<Expr>

Paren(Box<Expr>)

Parenthesized expression (for preserving source).

Trait Implementations

impl Clone for ExprKind

fn clone(&self) -> ExprKind

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ExprKind

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

Formats the value using the given formatter.