minerva 0.2.0

extern crate alloc;

use alloc::collections::{BTreeMap, BTreeSet};
use alloc::vec::Vec;

use super::super::super::support::dot;
use crate::metis::{Dot, DotMap, DotSet};
use proptest::prelude::*;

proptest! {
    /// One-pass disjoint construction agrees with repeated insertion.
    #[test]
    fn prop_from_disjoint_matches_repeated_insert(
        batch in prop::collection::vec((0u8..4, (0u32..3, 1u64..6)), 0..16),
    ) {
        let mut order: Vec<u8> = Vec::new();
        let mut by_key: BTreeMap<u8, DotSet> = BTreeMap::new();
        for (key, (station, counter)) in batch {
            if !by_key.contains_key(&key) {
                order.push(key);
            }
            let _ = by_key.entry(key).or_default().insert(dot(station, counter));
        }
        let entries: Vec<(u8, DotSet)> =
            order.iter().map(|k| (*k, by_key[k].clone())).collect();

        let mut by_insert: DotMap<u8, DotSet> = DotMap::new();
        let mut insert_collided = false;
        for (key, store) in entries.clone() {
            if !by_insert.insert(key, store) {
                insert_collided = true;
                break;
            }
        }

        match DotMap::from_disjoint(entries) {
            Ok(built) => {
                prop_assert!(!insert_collided);
                prop_assert_eq!(built, by_insert);
            }
            Err(collision) => {
                prop_assert!(insert_collided);

                let mut keys_at: BTreeMap<Dot, BTreeSet<u8>> = BTreeMap::new();
                for (&key, store) in &by_key {
                    for held in store.dots() {
                        let _ = keys_at.entry(held).or_default().insert(key);
                    }
                }
                prop_assert!(keys_at.get(&collision.dot).is_some_and(|keys| keys.len() >= 2));
            }
        }
    }
}