Struct WhnfDepthBudget 

pub struct WhnfDepthBudget {
    pub budget: u32,
    pub remaining: u32,
}

A step budget for WHNF reduction to prevent non-termination.

Fields

budget: u32

Total allowed steps.

remaining: u32

Remaining steps.

Implementations

impl WhnfDepthBudget

pub fn new(budget: u32) -> Self

Create a budget with the given limit.

pub fn unlimited() -> Self

Create an unlimited budget (u32::MAX).

pub fn consume(&mut self) -> bool

Consume one step. Returns true if budget still remains.

pub fn is_exhausted(&self) -> bool

Whether the budget is exhausted.

pub fn consumed(&self) -> u32

Steps consumed so far.

pub fn reset(&mut self)

Reset to full budget.

Trait Implementations

impl Clone for WhnfDepthBudget

fn clone(&self) -> WhnfDepthBudget

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for WhnfDepthBudget

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

Formats the value using the given formatter.