Function decode_source_info

crates/ffi/src/lean_env.rs:676–697

(obj: LeanBorrowed<'_>)

}

/// Decode an `@& Array Lean.Name` FFI argument into a `Vec<Name>`.
///
/// Uses a fresh `GlobalCache` to deduplicate shared sub-names within the
/// array (the cache keys by pointer identity, so repeat prefixes like
/// `Lean.Meta.Grind.Arith.Cutsat` are decoded once). Callers don't need
/// to manage the cache; it's dropped when this function returns.
///
/// Preferred over going through `String` + `parse_name` at the FFI
/// boundary: Lean's `Name.toString` adds `«»` escaping for components
/// that aren't valid identifiers, and the resulting string doesn't
/// round-trip through a naive split-on-`.` parser. By decoding the
/// structured `Lean.Name` directly we match the kernel's stored `Name`s
/// exactly (same component strings, same content hash).
pub fn decode_name_array(arr: &LeanArray<LeanBorrowed<'_>>) -> Vec<Name> {
  let global = GlobalCache::new();
  arr.map(|obj| decode_name(obj, &global))
}

fn decode_level(obj: LeanBorrowed<'_>, cache: &mut Cache<'_>) -> Level {
  let ptr = obj.as_raw();
  if let Some(cached) = cache.local.univs.get(&ptr) {
    return cached.clone();
  }
  let level = if obj.is_scalar() {
    Level::zero()