/// Provenance: Lean 4 → Safe Rust
/// Source: HeytingLean.Algebra.HomotopyTower.GroupoidBridge + InfinityGroupoidBridge
/// Theorem preserved: stabilized_fixed_point_category_has_infty_groupoid_presentation

/// A directed graph with typed vertices and edges.
#[derive(Clone, Debug)]
pub struct Quiver {
    pub num_vertices: usize,
    pub edge_src: Vec<usize>,
    pub edge_dst: Vec<usize>,
}

impl Quiver {
    pub fn num_edges(&self) -> usize {
        self.edge_src.len()
    }
}

/// Free groupoid element: a word in generators and their inverses.
#[derive(Clone, Debug, PartialEq)]
pub struct FreeGroupoidElement {
    pub edges: Vec<usize>,
    pub inverted: Vec<bool>,
}

impl FreeGroupoidElement {
    /// The identity element (empty word).
    pub fn identity() -> Self {
        FreeGroupoidElement {
            edges: vec![],
            inverted: vec![],
        }
    }

    pub fn is_identity(&self) -> bool {
        self.edges.is_empty()
    }

    pub fn len(&self) -> usize {
        self.edges.len()
    }

    /// Compose two free groupoid elements with cancellation at the junction.
    pub fn compose(&self, other: &FreeGroupoidElement) -> FreeGroupoidElement {
        let mut cancel = 0;
        while cancel < self.len() && cancel < other.len() {
            let ai = self.len() - 1 - cancel;
            if self.edges[ai] == other.edges[cancel]
                && self.inverted[ai] != other.inverted[cancel]
            {
                cancel += 1;
            } else {
                break;
            }
        }
        let mut edges = self.edges[..self.len() - cancel].to_vec();
        edges.extend_from_slice(&other.edges[cancel..]);
        let mut inverted = self.inverted[..self.len() - cancel].to_vec();
        inverted.extend_from_slice(&other.inverted[cancel..]);
        FreeGroupoidElement { edges, inverted }
    }

    /// Invert a free groupoid element.
    pub fn invert(&self) -> FreeGroupoidElement {
        FreeGroupoidElement {
            edges: self.edges.iter().rev().copied().collect(),
            inverted: self.inverted.iter().rev().map(|b| !b).collect(),
        }
    }
}

/// Stable transport quiver: quiver-valued transport surface across tower levels.
pub struct StableTransportQuiver {
    pub quivers: Vec<Quiver>,
}

impl StableTransportQuiver {
    pub fn num_levels(&self) -> usize {
        self.quivers.len()
    }
}

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

    #[test]
    fn test_identity_compose() {
        let id = FreeGroupoidElement::identity();
        let g = FreeGroupoidElement {
            edges: vec![0, 1],
            inverted: vec![false, false],
        };
        assert_eq!(id.compose(&g), g);
        assert_eq!(g.compose(&id), g);
    }

    #[test]
    fn test_inverse_cancels() {
        let g = FreeGroupoidElement {
            edges: vec![0, 1, 2],
            inverted: vec![false, true, false],
        };
        let inv = g.invert();
        let composed = g.compose(&inv);
        assert!(composed.is_identity());
    }

    #[test]
    fn test_partial_cancellation() {
        let a = FreeGroupoidElement {
            edges: vec![0, 1],
            inverted: vec![false, false],
        };
        let b = FreeGroupoidElement {
            edges: vec![1, 2],
            inverted: vec![true, false],
        };
        let c = a.compose(&b);
        assert_eq!(c.len(), 2);
        assert_eq!(c.edges, vec![0, 2]);
    }
}