Function decode_hashmap

crates/ffi/src/ix/env.rs:108–129

Decode a Lean HashMap into a Vec of key-value pairs. HashMap structure (after unboxing): Raw { size : Nat, buckets : Array (AssocList α β) } Due to single-field struct unboxing: - HashMap { inner : DHashMap } unboxes to DHashMap - DHashMap { inner : Raw, wf : Prop } unboxes to Raw (Prop is erased) - Raw { size : Nat, buckets : Array } - field 0 = size, field 1 = buckets

(
  obj: LeanBorrowed<'_>,
  decode_key: FK,
  decode_val: FV,
)

/// - DHashMap { inner : Raw, wf : Prop } unboxes to Raw (Prop is erased)
/// - Raw { size : Nat, buckets : Array } - field 0 = size, field 1 = buckets
fn decode_hashmap<K, V, FK, FV>(
  obj: LeanBorrowed<'_>,
  decode_key: FK,
  decode_val: FV,
) -> Vec<(K, V)>
where
  FK: Fn(LeanBorrowed<'_>) -> K + Copy,
  FV: Fn(LeanBorrowed<'_>) -> V + Copy,
{
  let ctor = obj.as_ctor();
  // Raw layout: field 0 = size (Nat), field 1 = buckets (Array)
  let _size = ctor.get(0); // unused but needed for layout
  let buckets = ctor.get(1).as_array();

  let mut pairs = Vec::new();
  for bucket in buckets.iter() {
    let bucket_pairs = decode_assoc_list(bucket, decode_key, decode_val);
    pairs.extend(bucket_pairs);
  }

  pairs
}

impl LeanIxRawEnvironment<LeanOwned> {
  /// Build a Ix.RawEnvironment from collected caches.