Struct Bind 

pub struct Bind<P, T> { /* private fields */ }

A binding construct that binds a name within a term

Implementations

impl<P, T> Bind<P, T>

pub fn new(pattern: P, body: T) -> Self

Create a new binding

Examples found in repository

examples/system_f.rs (lines 50-53)

    fn subst(&self, var: &Name<Ty>, value: &Ty) -> Self {
        match self {
            Ty::TyVar(v) if v == var => value.clone(),
            Ty::TyVar(v) => Ty::TyVar(v.clone()),
            Ty::Arr(t1, t2) => Ty::Arr(
                Box::new((**t1).subst(var, value)),
                Box::new((**t2).subst(var, value)),
            ),
            Ty::All(bnd) => {
                let vars = bnd.pattern();
                if vars.iter().any(|v| v == var) {
                    // Variable is bound, no substitution
                    self.clone()
                } else {
                    Ty::All(Bind::new(
                        vars.clone(),
                        Box::new((**bnd.body()).subst(var, value)),
                    ))
                }
            }
        }
    }
}

// Subst Tm Ty - terms don't substitute into types
impl Subst<Tm> for Ty {
    fn is_var(&self) -> Option<SubstName<Tm>> {
        None
    }

    fn subst(&self, _var: &Name<Tm>, _value: &Tm) -> Self {
        self.clone()
    }
}

impl Ty {
    fn tyvar(name: TyName) -> Ty {
        Ty::TyVar(name)
    }

    fn arr(t1: Ty, t2: Ty) -> Ty {
        Ty::Arr(Box::new(t1), Box::new(t2))
    }

    fn forall(vars: Vec<TyName>, ty: Ty) -> Ty {
        Ty::All(bind(vars, Box::new(ty)))
    }
}

impl fmt::Display for Ty {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Ty::TyVar(a) => write!(f, "{}", a),
            Ty::Arr(t1, t2) => write!(f, "({} → {})", t1, t2),
            Ty::All(bnd) => {
                let vars = bnd.pattern();
                write!(f, "∀")?;
                for (i, v) in vars.iter().enumerate() {
                    if i > 0 {
                        write!(f, " ")?;
                    }
                    write!(f, "{}", v)?;
                }
                write!(f, ". {}", bnd.body())
            }
        }
    }
}

/// Embedded type annotation
#[derive(Clone, Debug, PartialEq)]
struct Embed<T>(T);

impl<T: Alpha> Alpha for Embed<T> {
    fn aeq(&self, other: &Self) -> bool {
        self.0.aeq(&other.0)
    }

    fn aeq_in(&self, ctx: &mut AlphaCtx, other: &Self) -> bool {
        self.0.aeq_in(ctx, &other.0)
    }

    fn fv_in(&self, vars: &mut Vec<String>) {
        self.0.fv_in(vars)
    }
}

impl<T: Subst<V>, V> Subst<V> for Embed<T> {
    fn is_var(&self) -> Option<SubstName<V>> {
        None
    }

    fn subst(&self, var: &Name<V>, value: &V) -> Self {
        Embed(self.0.subst(var, value))
    }
}

/// System F terms
#[derive(Clone, Debug, Alpha)]
#[allow(dead_code)]
enum Tm {
    /// Term variables
    TmVar(TmName),
    /// Term abstraction (lambda)
    Lam(Bind<(TmName, Embed<Ty>), Box<Tm>>),
    /// Type abstraction (big lambda)
    TLam(Bind<Vec<TyName>, Box<Tm>>),
    /// Term application
    App(Box<Tm>, Box<Tm>),
    /// Type application
    TApp(Box<Tm>, Vec<Ty>),
}

// Only need to specify when it's a variable for Subst<Tm>
impl Subst<Tm> for Tm {
    fn is_var(&self) -> Option<SubstName<Tm>> {
        match self {
            Tm::TmVar(v) => Some(SubstName::Name(v.clone())),
            _ => None,
        }
    }

    fn subst(&self, var: &Name<Tm>, value: &Tm) -> Self {
        match self {
            Tm::TmVar(v) if v == var => value.clone(),
            Tm::TmVar(v) => Tm::TmVar(v.clone()),
            Tm::Lam(b) => {
                let (x, ann) = b.pattern();
                if x == var {
                    // Variable is bound, no substitution
                    self.clone()
                } else {
                    // Substitute in body
                    Tm::Lam(Bind::new(
                        (x.clone(), ann.clone()),
                        Box::new((**b.body()).subst(var, value)),
                    ))
                }
            }
            Tm::TLam(b) => {
                // Type variables can't capture term variables, so substitute in body
                Tm::TLam(Bind::new(
                    b.pattern().clone(),
                    Box::new((**b.body()).subst(var, value)),
                ))
            }
            Tm::App(e1, e2) => Tm::App(
                Box::new((**e1).subst(var, value)),
                Box::new((**e2).subst(var, value)),
            ),
            Tm::TApp(t, tys) => Tm::TApp(Box::new((**t).subst(var, value)), tys.clone()),
        }
    }
}

// Subst Ty Tm - substituting types in terms
impl Subst<Ty> for Tm {
    fn is_var(&self) -> Option<SubstName<Ty>> {
        None // Terms never contain type variables at the term level
    }

    fn subst(&self, var: &Name<Ty>, value: &Ty) -> Self {
        match self {
            Tm::TmVar(x) => Tm::TmVar(x.clone()),
            Tm::Lam(b) => {
                let (x, Embed(ty)) = b.pattern();
                Tm::Lam(Bind::new(
                    (x.clone(), Embed(ty.subst(var, value))),
                    Box::new((**b.body()).subst(var, value)),
                ))
            }
            Tm::TLam(b) => {
                let vars = b.pattern();
                if vars.iter().any(|v| v == var) {
                    // Type variable is bound, no substitution
                    self.clone()
                } else {
                    Tm::TLam(Bind::new(
                        vars.clone(),
                        Box::new((**b.body()).subst(var, value)),
                    ))
                }
            }
            Tm::App(e1, e2) => Tm::App(
                Box::new((**e1).subst(var, value)),
                Box::new((**e2).subst(var, value)),
            ),
            Tm::TApp(t, tys) => Tm::TApp(
                Box::new((**t).subst(var, value)),
                tys.iter().map(|ty| ty.subst(var, value)).collect(),
            ),
        }
    }

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

Unbind a binding, returning the pattern and body This should be used within FreshM to get fresh names

Examples found in repository

examples/system_f.rs (line 341)

fn check_type(ctx: &Context, ty: &Ty) -> Result<(), String> {
    match ty {
        Ty::TyVar(a) => {
            if ctx.lookup_type(a) {
                Ok(())
            } else {
                Err(format!("Type variable {} not in scope", a))
            }
        }
        Ty::Arr(t1, t2) => {
            check_type(ctx, t1)?;
            check_type(ctx, t2)
        }
        Ty::All(bnd) => {
            let (vars, body) = bnd.clone().unbind();
            let new_ctx = ctx.extend_type(vars);
            check_type(&new_ctx, &body)
        }
    }
}

/// Type inference for terms
fn type_infer(ctx: &Context, tm: &Tm) -> FreshM<Result<Ty, String>> {
    match tm {
        Tm::TmVar(x) => FreshM::pure(
            ctx.lookup_term(x)
                .ok_or_else(|| format!("Term variable {} not in scope", x)),
        ),
        Tm::Lam(bnd) => {
            let ((x, Embed(ty)), body) = bnd.clone().unbind();
            if let Err(e) = check_type(ctx, &ty) {
                return FreshM::pure(Err(e));
            }
            let new_ctx = ctx.extend_term(x, ty.clone());
            type_infer(&new_ctx, &body).map(|result| result.map(|body_ty| Ty::arr(ty, body_ty)))
        }
        Tm::TLam(bnd) => {
            let (vars, body) = bnd.clone().unbind();
            let new_ctx = ctx.extend_type(vars.clone());
            type_infer(&new_ctx, &body).map(|result| result.map(|ty| Ty::forall(vars, ty)))
        }
        Tm::App(t1, t2) => {
            let ctx_clone = ctx.clone();
            let t2_clone = t2.clone();
            type_infer(ctx, t1).and_then(move |ty1_result| match ty1_result {
                Ok(Ty::Arr(arg_ty, ret_ty)) => {
                    type_infer(&ctx_clone, &t2_clone).map(move |ty2_result| match ty2_result {
                        Ok(ty2) if arg_ty.aeq(&Box::new(ty2.clone())) => Ok(*ret_ty),
                        Ok(ty2) => Err(format!("Type mismatch: expected {}, got {}", arg_ty, ty2)),
                        Err(e) => Err(e),
                    })
                }
                Ok(ty) => FreshM::pure(Err(format!("Expected function type, got {}", ty))),
                Err(e) => FreshM::pure(Err(e)),
            })
        }
        Tm::TApp(t, tys) => {
            // Check all type arguments are well-formed
            for ty in tys {
                if let Err(e) = check_type(ctx, ty) {
                    return FreshM::pure(Err(e));
                }
            }

            let tys_clone = tys.clone();
            type_infer(ctx, t).map(move |ty_result| match ty_result {
                Ok(Ty::All(bnd)) => {
                    let (vars, body) = bnd.clone().unbind();
                    if vars.len() != tys_clone.len() {
                        Err(format!(
                            "Type application arity mismatch: expected {}, got {}",
                            vars.len(),
                            tys_clone.len()
                        ))
                    } else {
                        // Substitute type arguments
                        let mut result = *body;
                        for (var, ty) in vars.iter().zip(tys_clone.iter()) {
                            result = result.subst(var, ty);
                        }
                        Ok(result)
                    }
                }
                Ok(ty) => Err(format!("Expected polymorphic type, got {}", ty)),
                Err(e) => Err(e),
            })
        }
    }
}

examples/lambda.rs (line 45)

fn eval(expr: Expr) -> FreshM<Expr> {
    match expr {
        Expr::V(x) => FreshM::pure(Expr::V(x)),
        Expr::Lam(bnd) => {
            let (x, body) = bnd.unbind();
            eval(*body).map(move |evaluated_body| Expr::Lam(bind(x, Box::new(evaluated_body))))
        }
        Expr::App(e1, e2) => eval(*e1.clone()).and_then(move |v1| {
            eval(*e2.clone()).and_then(move |v2| match v1 {
                Expr::Lam(bnd) => {
                    let (x, body) = bnd.unbind();
                    let substituted = body.subst(&x, &v2);
                    eval(*substituted)
                }
                other => FreshM::pure(Expr::app(other, v2)),
            })
        }),
    }
}

pub fn pattern(&self) -> &P

Get a reference to the pattern

Examples found in repository

examples/system_f.rs (line 45)

    fn subst(&self, var: &Name<Ty>, value: &Ty) -> Self {
        match self {
            Ty::TyVar(v) if v == var => value.clone(),
            Ty::TyVar(v) => Ty::TyVar(v.clone()),
            Ty::Arr(t1, t2) => Ty::Arr(
                Box::new((**t1).subst(var, value)),
                Box::new((**t2).subst(var, value)),
            ),
            Ty::All(bnd) => {
                let vars = bnd.pattern();
                if vars.iter().any(|v| v == var) {
                    // Variable is bound, no substitution
                    self.clone()
                } else {
                    Ty::All(Bind::new(
                        vars.clone(),
                        Box::new((**bnd.body()).subst(var, value)),
                    ))
                }
            }
        }
    }
}

// Subst Tm Ty - terms don't substitute into types
impl Subst<Tm> for Ty {
    fn is_var(&self) -> Option<SubstName<Tm>> {
        None
    }

    fn subst(&self, _var: &Name<Tm>, _value: &Tm) -> Self {
        self.clone()
    }
}

impl Ty {
    fn tyvar(name: TyName) -> Ty {
        Ty::TyVar(name)
    }

    fn arr(t1: Ty, t2: Ty) -> Ty {
        Ty::Arr(Box::new(t1), Box::new(t2))
    }

    fn forall(vars: Vec<TyName>, ty: Ty) -> Ty {
        Ty::All(bind(vars, Box::new(ty)))
    }
}

impl fmt::Display for Ty {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Ty::TyVar(a) => write!(f, "{}", a),
            Ty::Arr(t1, t2) => write!(f, "({} → {})", t1, t2),
            Ty::All(bnd) => {
                let vars = bnd.pattern();
                write!(f, "∀")?;
                for (i, v) in vars.iter().enumerate() {
                    if i > 0 {
                        write!(f, " ")?;
                    }
                    write!(f, "{}", v)?;
                }
                write!(f, ". {}", bnd.body())
            }
        }
    }
}

/// Embedded type annotation
#[derive(Clone, Debug, PartialEq)]
struct Embed<T>(T);

impl<T: Alpha> Alpha for Embed<T> {
    fn aeq(&self, other: &Self) -> bool {
        self.0.aeq(&other.0)
    }

    fn aeq_in(&self, ctx: &mut AlphaCtx, other: &Self) -> bool {
        self.0.aeq_in(ctx, &other.0)
    }

    fn fv_in(&self, vars: &mut Vec<String>) {
        self.0.fv_in(vars)
    }
}

impl<T: Subst<V>, V> Subst<V> for Embed<T> {
    fn is_var(&self) -> Option<SubstName<V>> {
        None
    }

    fn subst(&self, var: &Name<V>, value: &V) -> Self {
        Embed(self.0.subst(var, value))
    }
}

/// System F terms
#[derive(Clone, Debug, Alpha)]
#[allow(dead_code)]
enum Tm {
    /// Term variables
    TmVar(TmName),
    /// Term abstraction (lambda)
    Lam(Bind<(TmName, Embed<Ty>), Box<Tm>>),
    /// Type abstraction (big lambda)
    TLam(Bind<Vec<TyName>, Box<Tm>>),
    /// Term application
    App(Box<Tm>, Box<Tm>),
    /// Type application
    TApp(Box<Tm>, Vec<Ty>),
}

// Only need to specify when it's a variable for Subst<Tm>
impl Subst<Tm> for Tm {
    fn is_var(&self) -> Option<SubstName<Tm>> {
        match self {
            Tm::TmVar(v) => Some(SubstName::Name(v.clone())),
            _ => None,
        }
    }

    fn subst(&self, var: &Name<Tm>, value: &Tm) -> Self {
        match self {
            Tm::TmVar(v) if v == var => value.clone(),
            Tm::TmVar(v) => Tm::TmVar(v.clone()),
            Tm::Lam(b) => {
                let (x, ann) = b.pattern();
                if x == var {
                    // Variable is bound, no substitution
                    self.clone()
                } else {
                    // Substitute in body
                    Tm::Lam(Bind::new(
                        (x.clone(), ann.clone()),
                        Box::new((**b.body()).subst(var, value)),
                    ))
                }
            }
            Tm::TLam(b) => {
                // Type variables can't capture term variables, so substitute in body
                Tm::TLam(Bind::new(
                    b.pattern().clone(),
                    Box::new((**b.body()).subst(var, value)),
                ))
            }
            Tm::App(e1, e2) => Tm::App(
                Box::new((**e1).subst(var, value)),
                Box::new((**e2).subst(var, value)),
            ),
            Tm::TApp(t, tys) => Tm::TApp(Box::new((**t).subst(var, value)), tys.clone()),
        }
    }
}

// Subst Ty Tm - substituting types in terms
impl Subst<Ty> for Tm {
    fn is_var(&self) -> Option<SubstName<Ty>> {
        None // Terms never contain type variables at the term level
    }

    fn subst(&self, var: &Name<Ty>, value: &Ty) -> Self {
        match self {
            Tm::TmVar(x) => Tm::TmVar(x.clone()),
            Tm::Lam(b) => {
                let (x, Embed(ty)) = b.pattern();
                Tm::Lam(Bind::new(
                    (x.clone(), Embed(ty.subst(var, value))),
                    Box::new((**b.body()).subst(var, value)),
                ))
            }
            Tm::TLam(b) => {
                let vars = b.pattern();
                if vars.iter().any(|v| v == var) {
                    // Type variable is bound, no substitution
                    self.clone()
                } else {
                    Tm::TLam(Bind::new(
                        vars.clone(),
                        Box::new((**b.body()).subst(var, value)),
                    ))
                }
            }
            Tm::App(e1, e2) => Tm::App(
                Box::new((**e1).subst(var, value)),
                Box::new((**e2).subst(var, value)),
            ),
            Tm::TApp(t, tys) => Tm::TApp(
                Box::new((**t).subst(var, value)),
                tys.iter().map(|ty| ty.subst(var, value)).collect(),
            ),
        }
    }
}

impl Tm {
    fn var(name: TmName) -> Tm {
        Tm::TmVar(name)
    }

    fn lam(var: TmName, ty: Ty, body: Tm) -> Tm {
        Tm::Lam(bind((var, Embed(ty)), Box::new(body)))
    }

    fn tlam(tyvars: Vec<TyName>, body: Tm) -> Tm {
        Tm::TLam(bind(tyvars, Box::new(body)))
    }

    #[allow(dead_code)]
    fn app(t1: Tm, t2: Tm) -> Tm {
        Tm::App(Box::new(t1), Box::new(t2))
    }

    fn tapp(t: Tm, tys: Vec<Ty>) -> Tm {
        Tm::TApp(Box::new(t), tys)
    }
}

impl fmt::Display for Tm {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Tm::TmVar(x) => write!(f, "{}", x),
            Tm::Lam(bnd) => {
                let (x, Embed(ty)) = bnd.pattern();
                write!(f, "λ{}:{}. ...", x, ty)
            }
            Tm::TLam(bnd) => {
                let vars = bnd.pattern();
                write!(f, "Λ")?;
                for (i, v) in vars.iter().enumerate() {
                    if i > 0 {
                        write!(f, " ")?;
                    }
                    write!(f, "{}", v)?;
                }
                write!(f, ". ...")
            }
            Tm::App(t1, t2) => write!(f, "({} {})", t1, t2),
            Tm::TApp(t, tys) => {
                write!(f, "({}", t)?;
                for ty in tys {
                    write!(f, " [{}]", ty)?;
                }
                write!(f, ")")
            }
        }
    }

pub fn body(&self) -> &T

Get a reference to the body

Examples found in repository

examples/system_f.rs (line 52)

    fn subst(&self, var: &Name<Ty>, value: &Ty) -> Self {
        match self {
            Ty::TyVar(v) if v == var => value.clone(),
            Ty::TyVar(v) => Ty::TyVar(v.clone()),
            Ty::Arr(t1, t2) => Ty::Arr(
                Box::new((**t1).subst(var, value)),
                Box::new((**t2).subst(var, value)),
            ),
            Ty::All(bnd) => {
                let vars = bnd.pattern();
                if vars.iter().any(|v| v == var) {
                    // Variable is bound, no substitution
                    self.clone()
                } else {
                    Ty::All(Bind::new(
                        vars.clone(),
                        Box::new((**bnd.body()).subst(var, value)),
                    ))
                }
            }
        }
    }
}

// Subst Tm Ty - terms don't substitute into types
impl Subst<Tm> for Ty {
    fn is_var(&self) -> Option<SubstName<Tm>> {
        None
    }

    fn subst(&self, _var: &Name<Tm>, _value: &Tm) -> Self {
        self.clone()
    }
}

impl Ty {
    fn tyvar(name: TyName) -> Ty {
        Ty::TyVar(name)
    }

    fn arr(t1: Ty, t2: Ty) -> Ty {
        Ty::Arr(Box::new(t1), Box::new(t2))
    }

    fn forall(vars: Vec<TyName>, ty: Ty) -> Ty {
        Ty::All(bind(vars, Box::new(ty)))
    }
}

impl fmt::Display for Ty {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Ty::TyVar(a) => write!(f, "{}", a),
            Ty::Arr(t1, t2) => write!(f, "({} → {})", t1, t2),
            Ty::All(bnd) => {
                let vars = bnd.pattern();
                write!(f, "∀")?;
                for (i, v) in vars.iter().enumerate() {
                    if i > 0 {
                        write!(f, " ")?;
                    }
                    write!(f, "{}", v)?;
                }
                write!(f, ". {}", bnd.body())
            }
        }
    }
}

/// Embedded type annotation
#[derive(Clone, Debug, PartialEq)]
struct Embed<T>(T);

impl<T: Alpha> Alpha for Embed<T> {
    fn aeq(&self, other: &Self) -> bool {
        self.0.aeq(&other.0)
    }

    fn aeq_in(&self, ctx: &mut AlphaCtx, other: &Self) -> bool {
        self.0.aeq_in(ctx, &other.0)
    }

    fn fv_in(&self, vars: &mut Vec<String>) {
        self.0.fv_in(vars)
    }
}

impl<T: Subst<V>, V> Subst<V> for Embed<T> {
    fn is_var(&self) -> Option<SubstName<V>> {
        None
    }

    fn subst(&self, var: &Name<V>, value: &V) -> Self {
        Embed(self.0.subst(var, value))
    }
}

/// System F terms
#[derive(Clone, Debug, Alpha)]
#[allow(dead_code)]
enum Tm {
    /// Term variables
    TmVar(TmName),
    /// Term abstraction (lambda)
    Lam(Bind<(TmName, Embed<Ty>), Box<Tm>>),
    /// Type abstraction (big lambda)
    TLam(Bind<Vec<TyName>, Box<Tm>>),
    /// Term application
    App(Box<Tm>, Box<Tm>),
    /// Type application
    TApp(Box<Tm>, Vec<Ty>),
}

// Only need to specify when it's a variable for Subst<Tm>
impl Subst<Tm> for Tm {
    fn is_var(&self) -> Option<SubstName<Tm>> {
        match self {
            Tm::TmVar(v) => Some(SubstName::Name(v.clone())),
            _ => None,
        }
    }

    fn subst(&self, var: &Name<Tm>, value: &Tm) -> Self {
        match self {
            Tm::TmVar(v) if v == var => value.clone(),
            Tm::TmVar(v) => Tm::TmVar(v.clone()),
            Tm::Lam(b) => {
                let (x, ann) = b.pattern();
                if x == var {
                    // Variable is bound, no substitution
                    self.clone()
                } else {
                    // Substitute in body
                    Tm::Lam(Bind::new(
                        (x.clone(), ann.clone()),
                        Box::new((**b.body()).subst(var, value)),
                    ))
                }
            }
            Tm::TLam(b) => {
                // Type variables can't capture term variables, so substitute in body
                Tm::TLam(Bind::new(
                    b.pattern().clone(),
                    Box::new((**b.body()).subst(var, value)),
                ))
            }
            Tm::App(e1, e2) => Tm::App(
                Box::new((**e1).subst(var, value)),
                Box::new((**e2).subst(var, value)),
            ),
            Tm::TApp(t, tys) => Tm::TApp(Box::new((**t).subst(var, value)), tys.clone()),
        }
    }
}

// Subst Ty Tm - substituting types in terms
impl Subst<Ty> for Tm {
    fn is_var(&self) -> Option<SubstName<Ty>> {
        None // Terms never contain type variables at the term level
    }

    fn subst(&self, var: &Name<Ty>, value: &Ty) -> Self {
        match self {
            Tm::TmVar(x) => Tm::TmVar(x.clone()),
            Tm::Lam(b) => {
                let (x, Embed(ty)) = b.pattern();
                Tm::Lam(Bind::new(
                    (x.clone(), Embed(ty.subst(var, value))),
                    Box::new((**b.body()).subst(var, value)),
                ))
            }
            Tm::TLam(b) => {
                let vars = b.pattern();
                if vars.iter().any(|v| v == var) {
                    // Type variable is bound, no substitution
                    self.clone()
                } else {
                    Tm::TLam(Bind::new(
                        vars.clone(),
                        Box::new((**b.body()).subst(var, value)),
                    ))
                }
            }
            Tm::App(e1, e2) => Tm::App(
                Box::new((**e1).subst(var, value)),
                Box::new((**e2).subst(var, value)),
            ),
            Tm::TApp(t, tys) => Tm::TApp(
                Box::new((**t).subst(var, value)),
                tys.iter().map(|ty| ty.subst(var, value)).collect(),
            ),
        }
    }

Trait Implementations

impl<T: Alpha, U: Alpha> Alpha for Bind<(Name<T>, U), Box<T>>

fn aeq(&self, other: &Self) -> bool

Check if two terms are alpha-equivalent

fn aeq_in(&self, ctx: &mut AlphaCtx, other: &Self) -> bool

Check alpha equivalence with a renaming context

fn fv_in(&self, vars: &mut Vec<String>)

Collect free variables into a vector

fn fv(&self) -> Vec<String>

Collect free variables

impl<T: Alpha> Alpha for Bind<Name<T>, Box<T>>

fn aeq(&self, other: &Self) -> bool

Check if two terms are alpha-equivalent

fn aeq_in(&self, ctx: &mut AlphaCtx, other: &Self) -> bool

Check alpha equivalence with a renaming context

fn fv_in(&self, vars: &mut Vec<String>)

Collect free variables into a vector

fn fv(&self) -> Vec<String>

Collect free variables

impl<T: Alpha, U: Alpha> Alpha for Bind<Vec<Name<T>>, Box<U>>

fn aeq(&self, other: &Self) -> bool

Check if two terms are alpha-equivalent

fn aeq_in(&self, ctx: &mut AlphaCtx, other: &Self) -> bool

Check alpha equivalence with a renaming context

fn fv_in(&self, vars: &mut Vec<String>)

Collect free variables into a vector

fn fv(&self) -> Vec<String>

Collect free variables

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

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

Returns a duplicate of the value.

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

Performs copy-assignment from source.

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

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

Formats the value using the given formatter.

impl<P: Display, T: Display> Display for Bind<P, T>

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

Formats the value using the given formatter.

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

fn eq(&self, other: &Bind<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<T: Subst<V> + Clone, U: Subst<V> + Clone, V: Clone> Subst<V> for Bind<(Name<V>, U), Box<T>>

fn is_var(&self) -> Option<SubstName<V>>

Check if this term is a variable and return its name

fn subst(&self, var: &Name<V>, value: &V) -> Self

Perform substitution of value for var in self

fn subst_all(&self, subst_map: &HashMap<Name<V>, V>) -> Self

where V: Clone, Self: Clone,

Perform substitution with a mapping

impl<T: Subst<V> + Clone, V: Clone> Subst<V> for Bind<Name<V>, Box<T>>

fn is_var(&self) -> Option<SubstName<V>>

Check if this term is a variable and return its name

fn subst(&self, var: &Name<V>, value: &V) -> Self

Perform substitution of value for var in self

fn subst_all(&self, subst_map: &HashMap<Name<V>, V>) -> Self

where V: Clone, Self: Clone,

Perform substitution with a mapping

impl<T: Subst<V> + Clone, V: Clone> Subst<V> for Bind<Vec<Name<V>>, Box<T>>

fn is_var(&self) -> Option<SubstName<V>>

Check if this term is a variable and return its name

fn subst(&self, var: &Name<V>, value: &V) -> Self

Perform substitution of value for var in self

fn subst_all(&self, subst_map: &HashMap<Name<V>, V>) -> Self

where V: Clone, Self: Clone,

Perform substitution with a mapping

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