Function build_hashmap_from_pairs

crates/ffi/src/ix/env.rs:27–66

Build a Lean HashMap from pre-built key-value pairs. Lean's Std.HashMap structure (with unboxing): - HashMap α β unboxes through DHashMap to Raw - Raw = { size : Nat, buckets : Array (AssocList α β) } - Field 0 = size (Nat), Field 1 = buckets (Array) AssocList α β = nil | cons (key : α) (value : β) (tail : AssocList α β)

(
  pairs: Vec<(LeanOwned, LeanOwned, u64)>, // (key_obj, val_obj, hash)
)

///
/// AssocList α β = nil | cons (key : α) (value : β) (tail : AssocList α β)
pub fn build_hashmap_from_pairs(
  pairs: Vec<(LeanOwned, LeanOwned, u64)>, // (key_obj, val_obj, hash)
) -> LeanOwned {
  let size = pairs.len();
  let bucket_count = (size * 4 / 3 + 1).next_power_of_two().max(8);

  // Create array of AssocLists (initially all nil = boxed 0)
  let buckets = LeanArray::alloc(bucket_count);
  let nil = LeanOwned::box_usize(0);
  for i in 0..bucket_count {
    buckets.set(i, nil.clone()); // nil
  }

  // Insert entries
  for (key_obj, val_obj, hash) in pairs {
    let bucket_idx =
      usize::try_from(hash).expect("hash overflows usize") % bucket_count;

    // Get current bucket (AssocList)
    let current_tail = buckets.get(bucket_idx).to_owned_ref();

    // cons (key : α) (value : β) (tail : AssocList α β) -- tag 1
    let cons = LeanCtor::alloc(1, 3, 0);
    cons.set(0, key_obj);
    cons.set(1, val_obj);
    cons.set(2, current_tail);

    buckets.set(bucket_idx, cons);
  }

  // Build Raw { size : Nat, buckets : Array }
  // Due to unboxing, this IS the HashMap directly
  // Field 0 = size, Field 1 = buckets (2 object fields, no scalars)
  let size_obj = LeanOwned::box_usize(size);

  let raw = LeanCtor::alloc(0, 2, 0);
  raw.set(0, size_obj);
  raw.set(1, buckets);
  raw.into()
}

// =============================================================================
// Environment Building / Decoding