Function bind 

pub fn bind<P, T>(pattern: P, body: T) -> Bind<P, T>

Helper function to bind a pattern in a body

Examples found in repository

examples/lambda.rs (line 22)

    fn lam(var: Var, body: Expr) -> Expr {
        Expr::Lam(bind(var, Box::new(body)))
    }

    fn app(e1: Expr, e2: Expr) -> Expr {
        Expr::App(Box::new(e1), Box::new(e2))
    }
}

impl std::fmt::Display for Expr {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Expr::V(x) => write!(f, "{}", x),
            Expr::Lam(bnd) => write!(f, "λ{}", bnd),
            Expr::App(e1, e2) => write!(f, "({} {})", e1, e2),
        }
    }
}

// Evaluate to normal form
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)),
            })
        }),
    }
}

examples/system_f.rs (line 81)

    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)))
    }