Struct Scope

pub struct Scope<P, T> {
    pub unsafe_pattern: P,
    pub unsafe_body: T,
}

A bound scope

Fields

unsafe_pattern: P

The pattern that binds the body of the scope

You can access this directly, but only if you understand what you are doing! Prefer calling Scope::unbind instead.

unsafe_body: T

The body of the scope

You can access this directly, but only if you understand what you are doing! Prefer calling Scope::unbind instead.

Implementations

impl<P, T> Scope<P, T>

pub fn new<N>(pattern: P, body: T) -> Scope<P, T>

where N: Clone + PartialEq, P: BoundPattern<N>, T: BoundTerm<N>,

Create a new scope by binding a term with the given pattern

pub fn unbind<N>(self) -> (P, T)

where N: Clone + Eq + Hash, P: BoundPattern<N>, T: BoundTerm<N>,

Unbind a term, returning the freshened pattern and body

pub fn unbind2<N, P2, T2>(self, other: Scope<P2, T2>) -> (P, T, P2, T2)

where N: Clone + Eq + Hash, P: BoundPattern<N>, T: BoundTerm<N>, P2: BoundPattern<N>, T2: BoundTerm<N>,

Simultaneously unbind two terms

The fresh names in the first pattern with be used for the second pattern

Trait Implementations

impl<N, P, T> BoundTerm<N> for Scope<P, T>

where N: Clone + PartialEq, P: BoundPattern<N>, T: BoundTerm<N>,

fn term_eq(&self, other: &Scope<P, T>) -> bool

Alpha equivalence for terms

fn close_term(&mut self, state: ScopeState, on_free: &impl OnFreeFn<N>)

Close the term using the supplied binders

fn open_term(&mut self, state: ScopeState, on_bound: &impl OnBoundFn<N>)

Open the term using the supplied binders

fn visit_vars(&self, on_var: &mut impl FnMut(&Var<N>))

Visit each variable in the term, calling the on_var callback on each of them in turn

fn visit_mut_vars(&mut self, on_var: &mut impl FnMut(&mut Var<N>))

Visit each variable in the term, calling the on_var callback on each of them in turn

fn free_vars(&self) -> HashSet<FreeVar<N>>

where N: Eq + Hash + Clone,

Returns the set of free variables in this term

impl<P: Clone, T: Clone> Clone for Scope<P, T>

fn clone(&self) -> Scope<P, T>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<P: Debug, T: Debug> Debug for Scope<P, T>

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

Formats the value using the given formatter.

impl<P: PartialEq, T: PartialEq> PartialEq for Scope<P, T>

fn eq(&self, other: &Scope<P, T>) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<P: Eq, T: Eq> Eq for Scope<P, T>

impl<P, T> StructuralPartialEq for Scope<P, T>