Function compute_base_size

crates/ixon/src/sharing.rs:150–190

Compute the base size of a node (Tag4 header size) for Ixon serialization.

(expr: &Expr)

/// Compute the base size of a node (Tag4 header size) for Ixon serialization.
fn compute_base_size(expr: &Expr) -> usize {
  match expr {
    Expr::Sort(univ_idx) => {
      Tag4::new(Expr::FLAG_SORT, *univ_idx).encoded_size()
    },
    Expr::Var(idx) => Tag4::new(Expr::FLAG_VAR, *idx).encoded_size(),
    Expr::Ref(ref_idx, univ_indices) => {
      // tag + ref_idx + N univ indices
      Tag4::new(Expr::FLAG_REF, univ_indices.len() as u64).encoded_size()
        + Tag0::new(*ref_idx).encoded_size()
        + univ_indices
          .iter()
          .map(|i| Tag0::new(*i).encoded_size())
          .sum::<usize>()
    },
    Expr::Rec(rec_idx, univ_indices) => {
      // tag + rec_idx + N univ indices
      Tag4::new(Expr::FLAG_REC, univ_indices.len() as u64).encoded_size()
        + Tag0::new(*rec_idx).encoded_size()
        + univ_indices
          .iter()
          .map(|i| Tag0::new(*i).encoded_size())
          .sum::<usize>()
    },
    Expr::Prj(type_ref_idx, field_idx, _) => {
      // Tag (field_idx in payload) + type_ref_idx (variable length, estimate 2 bytes)
      Tag4::new(Expr::FLAG_PRJ, *field_idx).encoded_size()
        + Tag0::new(*type_ref_idx).encoded_size()
    },
    Expr::Str(ref_idx) => Tag4::new(Expr::FLAG_STR, *ref_idx).encoded_size(),
    Expr::Nat(ref_idx) => Tag4::new(Expr::FLAG_NAT, *ref_idx).encoded_size(),
    Expr::App(..) => Tag4::new(Expr::FLAG_APP, 1).encoded_size(), // telescope count >= 1
    Expr::Lam(..) => Tag4::new(Expr::FLAG_LAM, 1).encoded_size(),
    Expr::All(..) => Tag4::new(Expr::FLAG_ALL, 1).encoded_size(),
    Expr::Let(non_dep, ..) => {
      // size=0 for dep, size=1 for non_dep
      Tag4::new(Expr::FLAG_LET, if *non_dep { 1 } else { 0 }).encoded_size()
    },
    Expr::Share(idx) => Tag4::new(Expr::FLAG_SHARE, *idx).encoded_size(),
  }
}

/// Get child expressions for traversal.
fn get_children(expr: &Expr) -> Vec<&Arc<Expr>> {
  match expr {