//! Assembly space (Ω, U, J) — paper-faithful syntax tree model.
//!
//! Corresponds to AssemblySpace.lean and AssemblyCore.lean.

use std::hash::{Hash, Hasher};

/// Syntax tree object: either a primitive atom or a binary join.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Obj {
    Base(u32),
    Join(Box<Obj>, Box<Obj>),
}

impl Hash for Obj {
    fn hash<H: Hasher>(&self, state: &mut H) {
        match self {
            Obj::Base(a) => {
                0u8.hash(state);
                a.hash(state);
            }
            Obj::Join(l, r) => {
                1u8.hash(state);
                l.hash(state);
                r.hash(state);
            }
        }
    }
}

impl Obj {
    /// Number of primitive leaves in the tree.
    /// Lean: `Obj.size`
    pub fn size(&self) -> u32 {
        match self {
            Obj::Base(_) => 1,
            Obj::Join(l, r) => l.size() + r.size(),
        }
    }

    /// Number of join nodes in the tree (without reuse tracking).
    /// Lean: `Obj.joinCount`
    pub fn join_count(&self) -> u32 {
        match self {
            Obj::Base(_) => 0,
            Obj::Join(l, r) => 1 + l.join_count() + r.join_count(),
        }
    }

    /// Whether this object is a primitive (base atom).
    pub fn is_primitive(&self) -> bool {
        matches!(self, Obj::Base(_))
    }
}

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

    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 size_base() {
        assert_eq!(base(0).size(), 1);
    }

    #[test]
    fn size_join() {
        let o = join(base(0), base(1));
        assert_eq!(o.size(), 2);
    }

    #[test]
    fn size_eq_joincount_plus_one() {
        // Lean: size_eq_joinCount_add_one
        let o = join(join(base(0), base(1)), base(2));
        assert_eq!(o.size(), o.join_count() + 1);
    }

    #[test]
    fn size_positive() {
        // Lean: size_pos
        let o = join(base(0), join(base(1), base(2)));
        assert!(o.size() > 0);
    }

    #[test]
    fn primitive_has_zero_joins() {
        assert_eq!(base(42).join_count(), 0);
    }
}