Struct TerminationChecker 

pub struct TerminationChecker { /* private fields */ }

Termination checker for recursive definitions.

Implementations

impl TerminationChecker

pub fn new() -> Self

Create a new termination checker.

pub fn register_params(&mut self, name: Name, params: Vec<ParamInfo>)

Register parameter info for a function.

pub fn add_smaller(&mut self, big: Expr, small: Expr)

Mark an expression as structurally smaller than another.

This is used when we know that small is a subterm of big, e.g., when pattern matching on an inductive type.

pub fn is_smaller(&self, big: &Expr, small: &Expr) -> bool

Check if small is known to be structurally smaller than big.

pub fn check_terminates( &mut self, name: &Name, body: &Expr, ) -> Result<(), String>

Check if a recursive definition terminates.

Returns Ok(()) if the definition is structurally decreasing, or Err with a message explaining why it might not terminate.

pub fn check_mutual_terminates( &mut self, names: &[Name], bodies: &[Expr], ) -> Result<(), String>

Check termination for mutual recursion.

pub fn get_calls(&self, name: &Name) -> Option<&Vec<RecCallInfo>>

Get the recorded calls for a function.

Trait Implementations

impl Default for TerminationChecker

fn default() -> Self

Returns the “default value” for a type.