//! Assembly index via DAG join count with reuse tracking.
//!
//! Corresponds to AssemblyIndex.lean.
//! Key theorem: assemblyIndex_eq_dagJoinCount

use std::collections::HashSet;
use crate::assembly_space::Obj;

/// Count DISTINCT join operations (the reuse-aware assembly index).
///
/// Lean theorem: `assemblyIndex_eq_dagJoinCount`
///   assemblyIndex o = dagJoinCount o
///
/// The assembly index equals the number of distinct intermediate products
/// needed to construct the object. Reuse of intermediates reduces complexity.
pub fn assembly_index(o: &Obj) -> u32 {
    let mut seen = HashSet::new();
    count_distinct_joins(o, &mut seen)
}

fn count_distinct_joins(o: &Obj, seen: &mut HashSet<Obj>) -> u32 {
    match o {
        Obj::Base(_) => 0,
        Obj::Join(l, r) => {
            let mut count = 0;
            if seen.insert(o.clone()) {
                count += 1;
            }
            count += count_distinct_joins(l, seen);
            count += count_distinct_joins(r, seen);
            count
        }
    }
}

/// Verify: assemblyIndex_eq_zero_iff
///   assemblyIndex o = 0 ↔ o ∈ U (primitive)
pub fn is_primitive_iff_zero_index(o: &Obj) -> bool {
    (assembly_index(o) == 0) == o.is_primitive()
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::assembly_space::Obj;

    fn base(a: u32) -> Obj { Obj::Base(a) }
    fn join(l: Obj, r: Obj) -> Obj { Obj::Join(Box::new(l), Box::new(r)) }

    #[test]
    fn primitive_index_zero() {
        // assemblyIndex_eq_zero_iff: primitives have AI = 0
        assert_eq!(assembly_index(&base(0)), 0);
    }

    #[test]
    fn single_join_index_one() {
        let o = join(base(0), base(1));
        assert_eq!(assembly_index(&o), 1);
    }

    #[test]
    fn reuse_reduces_index() {
        // join(join(a,b), join(a,b)) — reuse of join(a,b) means AI < joinCount
        let ab = join(base(0), base(1));
        let o = join(ab.clone(), ab);
        let ai = assembly_index(&o);
        let jc = o.join_count();
        assert!(ai <= jc, "AI={ai} should be ≤ joinCount={jc}");
        // Specifically: 2 distinct joins (the inner + the outer), not 3
        assert_eq!(ai, 2);
    }

    #[test]
    fn primitive_iff_zero() {
        assert!(is_primitive_iff_zero_index(&base(0)));
        assert!(is_primitive_iff_zero_index(&join(base(0), base(1))));
    }

    #[test]
    fn chain_index_equals_length() {
        // Linear chain: join(join(join(a,b),c),d) — no reuse, AI = joinCount = size-1
        let o = join(join(join(base(0), base(1)), base(2)), base(3));
        assert_eq!(assembly_index(&o), o.join_count());
        assert_eq!(assembly_index(&o), o.size() - 1);
    }
}