Enum SpecExpr 

pub enum SpecExpr {
    ConstInt {
        val: i128,
        pos: Pos,
    },
    ConstBitVec {
        val: u128,
        width: usize,
        pos: Pos,
    },
    ConstBool {
        val: bool,
        pos: Pos,
    },
    Var {
        var: Ident,
        pos: Pos,
    },
    As {
        x: Box<SpecExpr>,
        ty: ModelType,
        pos: Pos,
    },
    Field {
        field: Ident,
        x: Box<SpecExpr>,
        pos: Pos,
    },
    Discriminator {
        variant: Ident,
        x: Box<SpecExpr>,
        pos: Pos,
    },
    Op {
        op: SpecOp,
        args: Vec<SpecExpr>,
        pos: Pos,
    },
    Match {
        x: Box<SpecExpr>,
        arms: Vec<Arm>,
        pos: Pos,
    },
    Let {
        defs: Vec<(Ident, SpecExpr)>,
        body: Box<SpecExpr>,
        pos: Pos,
    },
    With {
        decls: Vec<Ident>,
        body: Box<SpecExpr>,
        pos: Pos,
    },
    Macro {
        params: Vec<Ident>,
        body: Box<SpecExpr>,
        pos: Pos,
    },
    Expand {
        name: Ident,
        args: Vec<SpecExpr>,
        pos: Pos,
    },
    Pair {
        l: Box<SpecExpr>,
        r: Box<SpecExpr>,
        pos: Pos,
    },
    Enum {
        name: Ident,
        variant: Ident,
        args: Vec<SpecExpr>,
        pos: Pos,
    },
    Struct {
        fields: Vec<FieldInit>,
        pos: Pos,
    },
}

An expression used to specify term semantics, similar to SMT-LIB syntax.

Variants

ConstInt

An operator that matches a constant integer value.

Fields

val: i128

pos: Pos

ConstBitVec

An operator that matches a constant bitvector value.

Fields

val: u128

width: usize

pos: Pos

ConstBool

An operator that matches a constant boolean value.

Fields

val: bool

pos: Pos

Var

Fields

var: Ident

pos: Pos

As

Fields

x: Box<SpecExpr>

ty: ModelType

pos: Pos

Field

Struct field access.

Fields

field: Ident

x: Box<SpecExpr>

pos: Pos

Discriminator

Discriminator is a predicate that tests the variant of an enum value.

Fields

variant: Ident

x: Box<SpecExpr>

pos: Pos

Op

An application of a type variant or term.

Fields

op: SpecOp

args: Vec<SpecExpr>

pos: Pos

Match

Enum pattern matching.

Fields

x: Box<SpecExpr>

arms: Vec<Arm>

pos: Pos

Let

Let bindings.

Fields

defs: Vec<(Ident, SpecExpr)>

body: Box<SpecExpr>

pos: Pos

With

Introduce new uninitialized variables.

Fields

decls: Vec<Ident>

body: Box<SpecExpr>

pos: Pos

Macro

Inline macro definition, or lambda.

Fields

params: Vec<Ident>

Parameter names.

body: Box<SpecExpr>

Macro expansion.

pos: Pos

Expand

Macro expansion.

Fields

name: Ident

args: Vec<SpecExpr>

pos: Pos

Pair

Pairs, currently used for switch statements.

Fields

l: Box<SpecExpr>

r: Box<SpecExpr>

pos: Pos

Enum

Construct enum variant.

Fields

name: Ident

variant: Ident

args: Vec<SpecExpr>

pos: Pos

Struct

Construct struct value.

Fields

fields: Vec<FieldInit>

pos: Pos

Implementations

impl SpecExpr

pub fn pos(&self) -> Pos

Trait Implementations

impl Clone for SpecExpr

fn clone(&self) -> SpecExpr

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SpecExpr

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

Formats the value using the given formatter.

impl Eq for SpecExpr

impl PartialEq for SpecExpr

fn eq(&self, other: &SpecExpr) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for SpecExpr

impl ToSExpr for SpecExpr

fn to_sexpr(&self) -> SExpr

Convert the given value to an S-expression.