Struct EffectRowChecker 

pub struct EffectRowChecker {
    pub declared_row: EffRow,
    pub violations: Vec<String>,
}

A simple static effect row checker that verifies that performed effects are within the declared effect row.

Fields

declared_row: EffRow

The declared (allowed) effect row.

violations: Vec<String>

Violations found during checking: effect names that were used but not declared.

Implementations

impl EffectRowChecker

pub fn new(declared_row: EffRow) -> Self

Create a new checker for a given declared effect row.

pub fn check_effect(&mut self, effect: &str) -> bool

Check if the given effect is within the declared row.

pub fn check_all(&mut self, used_effects: &[&str]) -> bool

Check all effects used in a list of operations.

pub fn has_violations(&self) -> bool

Return whether any violations were found.

pub fn violation_summary(&self) -> String

Return a summary of violations.

pub fn reset(&mut self)

Reset violations (allow re-checking).

pub fn is_sound_annotation(&self) -> bool

The declared effect row is a sound over-approximation of used effects.