Function fmt_expr

crates/kernel/src/expr.rs:691–788

(
  e: &KExpr<M>,
  f: &mut fmt::Formatter<'_>,
  depth: usize,
)

      } else {
        write!(f, "_")?;
      }
      write!(f, " : ")?;
      fmt_expr(ty, f, depth + 1)?;
      write!(f, ") -> ")?;
      fmt_expr(body, f, depth + 1)?;
      write!(f, ")")
    },
    ExprData::Let(name, ty, val, body, _, _) => {
      write!(f, "(let ")?;
      if name.has_meta() {
        name.meta_fmt(f)?;
      } else {
        write!(f, "_")?;
      }
      write!(f, " : ")?;
      fmt_expr(ty, f, depth + 1)?;
      write!(f, " := ")?;
      fmt_expr(val, f, depth + 1)?;
      write!(f, " in ")?;
      fmt_expr(body, f, depth + 1)?;
      write!(f, ")")
    },
    ExprData::Prj(id, field, val, _) => {
      fmt_expr(val, f, depth + 1)?;
      write!(f, ".{field}@{id}")
    },
    ExprData::Nat(val, _, _) => write!(f, "{val}"),
    ExprData::Str(val, _, _) => write!(f, "{val:?}"),
  }
}

fn collect_spine<M: KernelMode>(e: &KExpr<M>) -> (KExpr<M>, Vec<KExpr<M>>) {
  let mut args = Vec::new();
  let mut cur = e.clone();
  while let ExprData::App(func, arg, _) = cur.data() {
    args.push(arg.clone());
    cur = func.clone();
  }
  args.reverse();
  (cur, args)
}

#[cfg(test)]
mod tests {
  use super::super::mode::{Anon, Meta};
  use super::*;
  use ix_common::address::Address;
  use ix_common::env::BinderInfo;

  type ME = KExpr<Meta>;
  type AE = KExpr<Anon>;
  type MU = KUniv<Meta>;
  type AU = KUniv<Anon>;

  fn mk_name(s: &str) -> Name {
    let mut name = Name::anon();
    for part in s.split('.') {
      name = Name::str(name, part.to_string());