Struct Widths 

pub struct Widths { /* private fields */ }

How wide each thing in one rule is.

A rule is written at one width, the one its pattern’s opcode names, and the terms inside it may say another: (value.i64 x) under an add.i32 is a thirty two bit add of two sixty four bit registers, which is the shape every sext, zext and trunc in a lowering has. What a name stands at is fixed by the pattern, because the pattern is where a name is bound, and everywhere else reads it from here.

A bounded proof asks the same rule at a narrower width, and that scales every width in the rule by one ratio rather than flattening them all to one number. A rule that converts between widths still converts between widths when it is asked at eight bits, which it would not do if the narrow width were simply substituted everywhere.

Implementations

impl Widths

pub fn of(pattern: &Term) -> Widths

The widths one rule’s pattern fixes, at the width the rule is written in.

pub fn at(pattern: &Term, asked: u32) -> Widths

The same, scaled to a width somebody asked for. This is what a bounded proof is made of.

pub fn width(&self) -> u32

The width a term is at when nothing inside it says otherwise.

pub fn natural(&self) -> u32

The width the rule is written in, which is the one it will run at.

pub fn names(&self) -> impl Iterator<Item = (&str, u32)>

Every name the pattern binds and how wide it is, sorted.

Sorted rather than in the order the pattern binds them, because the query is something a test pins and a diff is easier to read than it is to regenerate.

pub fn with(&self, name: &str, width: u32) -> Widths

These widths and one more name, which is how the replacement’s own meaning gets a width once it has been substituted into the specification for (result).

Trait Implementations

impl Clone for Widths

fn clone(&self) -> Widths

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Widths

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

Formats the value using the given formatter.

impl Default for Widths

fn default() -> Widths

Returns the “default value” for a type.