Struct LinearTypeChecker 

pub struct LinearTypeChecker;

A simple linearity checker that tracks variable usage counts. In linear typing, each variable must be used exactly once.

Implementations

impl LinearTypeChecker

pub fn new() -> Self

Create a new linearity checker.

pub fn count_uses(&self, term: &Term, depth: usize) -> UsageMap

Count free variable occurrences in term, relative to a context of depth variables. Returns a vector of length depth with usage counts for each variable.

pub fn is_linear(&self, term: &Term, depth: usize) -> bool

Check if term is linear in the context of depth variables. Returns true iff every variable in the context is used exactly once.

pub fn is_affine(&self, term: &Term, depth: usize) -> bool

Check if term is affine in the context of depth variables. Returns true iff every variable in the context is used at most once.

pub fn is_relevant(&self, term: &Term, depth: usize) -> bool

Check if term is relevant in the context of depth variables. Returns true iff every variable in the context is used at least once.

Trait Implementations

impl Default for LinearTypeChecker

fn default() -> Self

Returns the “default value” for a type.