Struct Rule 

pub struct Rule {
    pub pattern: Term,
    pub guard: Option<Term>,
    pub replacement: Term,
    pub spec: Term,
    pub bounded: Option<String>,
    pub line: u32,
    pub column: u32,
}

One rule: what it matches, what it produces, and what makes that sound.

Fields

pattern: Term

The term to match, which is IR for a rewrite and IR for a lowering.

guard: Option<Term>

A condition on the match, which is where a rule that only holds for some constants says so. It sits between the pattern and the replacement because it is part of deciding whether the rule fires, not part of what firing produces.

replacement: Term

What to put in the matched term’s place.

spec: Term

The bitvector claim relating the two, which is what rucc-verify discharges. It is not optional, because a rule set that lets one rule through without a specification is a rule set with an unverified rule in it.

bounded: Option<String>

Why a proof at narrower widths is enough for this rule, when there is a reason to think the solver will not manage the real one. A rule carrying this is not excused anything: it is still asked at its own width first, and the clause only says what a person is willing to sign for if the answer comes back as a shrug.

line: u32

The line the rule starts on.

column: u32

The column the rule starts at.

Trait Implementations

impl Clone for Rule

fn clone(&self) -> Rule

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Rule

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

Formats the value using the given formatter.

impl Display for Rule

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

Prints the rule back in the shape spec/10-backend.md writes it: one clause to a line, with the continuation lines under the pattern.

impl Eq for Rule

impl PartialEq for Rule

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for Rule