Function decode_assoc_list

crates/ffi/src/ix/env.rs:73–99

Decode a HashMap's AssocList and collect key-value pairs using a custom decoder.

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

/// Decode a HashMap's AssocList and collect key-value pairs using a custom decoder.
fn decode_assoc_list<K, V, FK, FV>(
  obj: LeanBorrowed<'_>,
  decode_key: FK,
  decode_val: FV,
) -> Vec<(K, V)>
where
  FK: Fn(LeanBorrowed<'_>) -> K,
  FV: Fn(LeanBorrowed<'_>) -> V,
{
  let mut result = Vec::new();
  let mut current = obj;

  while !current.is_scalar() {
    let ctor = current.as_ctor();
    if ctor.tag() == 0 {
      break; // AssocList.nil
    }
    // AssocList.cons: 3 fields (key, value, tail)
    let key = ctor.get(0);
    let val = ctor.get(1);
    let next = ctor.get(2).as_raw();
    result.push((decode_key(key), decode_val(val)));
    current = unsafe { LeanBorrowed::from_raw(next) };
  }

  result
}

/// Decode a Lean HashMap into a Vec of key-value pairs.
/// HashMap structure (after unboxing): Raw { size : Nat, buckets : Array (AssocList α β) }