//! Property tests for Patch algebra (diff/apply roundtrips)

mod generators;

use generators::{StructureParams, check_structure_invariants, structures_equivalent};
use geolog::core::Structure;
use geolog::naming::NamingIndex;
use geolog::patch::{Patch, apply_patch, diff, to_initial_patch};
use geolog::universe::Universe;
use proptest::prelude::*;
use std::collections::HashSet;

proptest! {
    /// Empty patch is identity: apply_patch(s, empty) == s
    #[test]
    fn empty_patch_is_identity(
        (structure, mut universe) in generators::arb_structure(StructureParams {
            num_sorts: 3,
            max_elements_per_sort: 8,
        })
    ) {
        let empty_patch = Patch::new(None, structure.num_sorts(), structure.num_functions(), structure.relations.len());
        let mut naming = NamingIndex::new();

        let result = apply_patch(&structure, &empty_patch, &mut universe, &mut naming);
        prop_assert!(result.is_ok());

        let result = result.unwrap();
        prop_assert_eq!(result.len(), structure.len());
        prop_assert_eq!(result.num_sorts(), structure.num_sorts());

        // Check same UUIDs
        prop_assert!(structures_equivalent(&result, &structure, &universe, &universe));
    }

    /// diff(s, s) produces empty patch
    #[test]
    fn diff_same_is_empty(
        (structure, universe) in generators::arb_structure(StructureParams {
            num_sorts: 3,
            max_elements_per_sort: 8,
        })
    ) {
        let naming = NamingIndex::new();

        let patch = diff(&structure, &structure, &universe, &naming, &naming);

        prop_assert!(patch.is_empty());
    }

    /// to_initial_patch creates patch that builds structure from empty
    #[test]
    fn initial_patch_builds_from_empty(
        (structure, mut universe) in generators::arb_structure(StructureParams {
            num_sorts: 3,
            max_elements_per_sort: 8,
        })
    ) {
        // Build naming for structure elements
        let mut naming = NamingIndex::new();
        for &luid in &structure.luids {
            if let Some(uuid) = universe.get(luid) {
                naming.insert(uuid, vec![format!("elem_{}", luid)]);
            }
        }

        let patch = to_initial_patch(&structure, &universe, &naming);

        // Apply to empty structure
        let empty = Structure::new(structure.num_sorts());
        let mut result_naming = NamingIndex::new();
        let result = apply_patch(&empty, &patch, &mut universe, &mut result_naming);

        prop_assert!(result.is_ok());
        let result = result.unwrap();

        // Should have same number of elements
        prop_assert_eq!(result.len(), structure.len());

        // Should have same UUIDs
        prop_assert!(structures_equivalent(&result, &structure, &universe, &universe));
    }

    /// Element additions are tracked in patch
    #[test]
    fn additions_tracked(
        num_elements in 1usize..10,
    ) {
        let mut universe = Universe::new();
        let mut naming = NamingIndex::new();

        let old = Structure::new(2);
        let mut new = Structure::new(2);

        for i in 0..num_elements {
            let (_, luid) = new.add_element(&mut universe, i % 2);
            if let Some(uuid) = universe.get(luid) {
                naming.insert(uuid, vec![format!("elem_{}", i)]);
            }
        }

        let old_naming = NamingIndex::new();
        let patch = diff(&old, &new, &universe, &old_naming, &naming);

        prop_assert_eq!(patch.elements.additions.len(), num_elements);
        prop_assert!(patch.elements.deletions.is_empty());
    }

    /// Element deletions are tracked in patch
    #[test]
    fn deletions_tracked(
        num_elements in 1usize..10,
    ) {
        let mut universe = Universe::new();
        let mut old_naming = NamingIndex::new();

        let mut old = Structure::new(2);
        for i in 0..num_elements {
            let (_, luid) = old.add_element(&mut universe, i % 2);
            if let Some(uuid) = universe.get(luid) {
                old_naming.insert(uuid, vec![format!("elem_{}", i)]);
            }
        }

        let new = Structure::new(2);
        let new_naming = NamingIndex::new();

        let patch = diff(&old, &new, &universe, &old_naming, &new_naming);

        prop_assert_eq!(patch.elements.deletions.len(), num_elements);
        prop_assert!(patch.elements.additions.is_empty());
    }

    /// Element patch has disjoint additions and deletions
    #[test]
    fn element_patch_disjoint(
        (old, universe) in generators::arb_structure(StructureParams {
            num_sorts: 2,
            max_elements_per_sort: 5,
        }),
        (new, _) in generators::arb_structure(StructureParams {
            num_sorts: 2,
            max_elements_per_sort: 5,
        })
    ) {
        let old_naming = NamingIndex::new();
        let new_naming = NamingIndex::new();

        let patch = diff(&old, &new, &universe, &old_naming, &new_naming);

        // Additions and deletions should be disjoint
        let additions: HashSet<_> = patch.elements.additions.keys().collect();
        let deletions: HashSet<_> = patch.elements.deletions.iter().collect();

        let intersection: Vec<_> = additions.intersection(&deletions).collect();
        prop_assert!(intersection.is_empty());
    }

    /// NamingPatch tracks name additions for new elements
    #[test]
    fn naming_patch_additions(
        num_elements in 1usize..8,
    ) {
        let mut universe = Universe::new();
        let mut naming = NamingIndex::new();

        let old = Structure::new(2);
        let mut new = Structure::new(2);

        for i in 0..num_elements {
            let (_, luid) = new.add_element(&mut universe, 0);
            if let Some(uuid) = universe.get(luid) {
                naming.insert(uuid, vec![format!("elem_{}", i)]);
            }
        }

        let old_naming = NamingIndex::new();
        let patch = diff(&old, &new, &universe, &old_naming, &naming);

        // Naming patch should have names for new elements
        prop_assert_eq!(patch.names.additions.len(), num_elements);
    }

    /// Patch inversion swaps additions/deletions
    #[test]
    fn inversion_swaps_elements(
        (old, mut universe) in generators::arb_structure(StructureParams {
            num_sorts: 2,
            max_elements_per_sort: 4,
        })
    ) {
        // Create a new structure with some different elements
        let mut new = Structure::new(2);
        new.add_element(&mut universe, 0);
        new.add_element(&mut universe, 1);

        let old_naming = NamingIndex::new();
        let new_naming = NamingIndex::new();

        let patch = diff(&old, &new, &universe, &old_naming, &new_naming);
        let inverted = patch.invert();

        // Inverted patch swaps source/target commits
        prop_assert_eq!(inverted.source_commit, Some(patch.target_commit));

        // Additions become deletions (by key count)
        prop_assert_eq!(
            inverted.elements.deletions.len(),
            patch.elements.additions.len()
        );
    }

    /// Double inversion preserves target_commit (but creates new source)
    #[test]
    fn double_inversion_target_preserved(
        (structure, universe) in generators::arb_structure(StructureParams {
            num_sorts: 2,
            max_elements_per_sort: 3,
        })
    ) {
        let naming = NamingIndex::new();
        let patch = to_initial_patch(&structure, &universe, &naming);

        let inverted = patch.invert();
        let double_inverted = inverted.invert();

        // Original target becomes source after double inversion
        // (because each inversion swaps source ↔ target)
        prop_assert_eq!(double_inverted.source_commit, Some(inverted.target_commit));
    }

    /// Result of apply_patch maintains structure invariants
    #[test]
    fn apply_patch_maintains_invariants(
        (old, mut universe) in generators::arb_structure(StructureParams {
            num_sorts: 3,
            max_elements_per_sort: 5,
        }),
        (new, _) in generators::arb_structure(StructureParams {
            num_sorts: 3,
            max_elements_per_sort: 5,
        })
    ) {
        let old_naming = NamingIndex::new();
        let new_naming = NamingIndex::new();

        let patch = diff(&old, &new, &universe, &old_naming, &new_naming);
        let mut result_naming = NamingIndex::new();

        let result = apply_patch(&old, &patch, &mut universe, &mut result_naming);
        prop_assert!(result.is_ok());

        let result = result.unwrap();
        prop_assert!(check_structure_invariants(&result).is_ok());
    }
}

// More focused roundtrip tests

proptest! {
    #![proptest_config(ProptestConfig::with_cases(256))]

    /// THE KEY PROPERTY: diff then apply is identity
    /// diff(old, new) |> apply_patch(old, _) ≈ new
    ///
    /// We test this by starting with a structure and modifying it (adding/removing elements)
    /// to create `new`, ensuring both share the same Universe.
    #[test]
    fn diff_apply_roundtrip(
        (base, mut universe) in generators::arb_structure(StructureParams {
            num_sorts: 2,
            max_elements_per_sort: 4,
        }),
        additions in proptest::collection::vec(0usize..2, 0..4),
        deletions_count in 0usize..3,
    ) {
        // Create `old` as a clone of base
        let old = base.clone();

        // Build naming for old structure
        let mut old_naming = NamingIndex::new();
        for &luid in &old.luids {
            if let Some(uuid) = universe.get(luid) {
                old_naming.insert(uuid, vec![format!("old_elem_{}", luid)]);
            }
        }

        // Create `new` by modifying base: add some elements, potentially skip some old ones
        let mut new = Structure::new(base.num_sorts());
        let mut new_naming = NamingIndex::new();

        // Keep some elements from old (skip the first `deletions_count`)
        let keep_count = base.len().saturating_sub(deletions_count);
        for slid in 0..keep_count {
            let luid = base.luids[slid];
            let sort_id = base.sorts[slid];
            new.add_element_with_luid(luid, sort_id);

            if let Some(uuid) = universe.get(luid) {
                new_naming.insert(uuid, vec![format!("kept_elem_{}", luid)]);
            }
        }

        // Add new elements
        for sort_id in additions {
            let (_, luid) = new.add_element(&mut universe, sort_id);
            if let Some(uuid) = universe.get(luid) {
                new_naming.insert(uuid, vec![format!("new_elem_{}", luid)]);
            }
        }

        // Now diff and apply
        let patch = diff(&old, &new, &universe, &old_naming, &new_naming);
        let mut result_naming = NamingIndex::new();

        let result = apply_patch(&old, &patch, &mut universe, &mut result_naming);
        prop_assert!(result.is_ok());

        let result = result.unwrap();

        // Result should have same number of elements as new
        prop_assert_eq!(result.len(), new.len());

        // Result should have same UUIDs as new (both use the same universe)
        let result_uuids: HashSet<_> = result.luids.iter()
            .filter_map(|&luid| universe.get(luid))
            .collect();
        let new_uuids: HashSet<_> = new.luids.iter()
            .filter_map(|&luid| universe.get(luid))
            .collect();

        prop_assert_eq!(result_uuids, new_uuids);
    }
}