Function rs_mt_parallel_decode_exprs

crates/ffi/src/refcount.rs:324–358

(
  arr: LeanArray<LeanBorrowed<'_>>,
  n_threads: usize,
)

/// Each thread decodes all exprs and counts nodes.
#[unsafe(no_mangle)]
pub extern "C" fn rs_mt_parallel_decode_exprs(
  arr: LeanArray<LeanBorrowed<'_>>,
  n_threads: usize,
) -> LeanOwned {
  fn count_expr_nodes(expr: &LeanIxExpr<impl LeanRef>) -> u64 {
    let ctor = expr.as_ctor();
    match ctor.tag() {
      5 => {
        // app
        1 + count_expr_nodes(&LeanIxExpr(ctor.get(0)))
          + count_expr_nodes(&LeanIxExpr(ctor.get(1)))
      },
      _ => 1,
    }
  }

  let shared = LeanShared::new(arr.inner().to_owned_ref());

  let handles: Vec<_> = (0..n_threads)
    .map(|_| {
      let shared_clone = shared.clone();
      thread::spawn(move || {
        let borrowed_arr = shared_clone.borrow().as_array();
        let mut total: u64 = 0;
        for elem in borrowed_arr.iter() {
          total += count_expr_nodes(&LeanIxExpr(elem));
        }
        total
      })
    })
    .collect();

  let total: u64 = handles.into_iter().map(|h| h.join().unwrap()).sum();
  LeanNat::from_nat(&Nat::from(total)).into()
}

/// Parallel roundtrip: mark array of Names as MT, each thread decodes
/// all names and rebuilds them. Returns an array of rebuilt names from