//! MCP server backend in Rust for concurrent Lean proof operations.
//! Thread-safe, async implementation with proper locking.

use std::sync::Arc;
use tokio::sync::Semaphore;
use std::time::Duration;

/// Global state for managing concurrent access
#[derive(Default)]
pub struct McpState {
    /// Build semaphore: limits concurrent lake builds to 1
    build_semaphore: Arc<Semaphore>,
    /// Git semaphore: limits concurrent git operations to 1
    git_semaphore: Arc<Semaphore>,
}

impl McpState {
    pub fn new() -> Self {
        Self {
            build_semaphore: Arc::new(Semaphore::new(1)),
            git_semaphore: Arc::new(Semaphore::new(1)),
        }
    }

    /// Acquire build semaphore
    pub async fn acquire_build(&self) -> Option<tokio::sync::OwnedSemaphorePermit> {
        match tokio::time::timeout(Duration::from_secs(5), self.build_semaphore.acquire_owned()).await {
            Ok(Ok(permit)) => Some(permit),
            _ => None,
        }
    }

    /// Acquire git semaphore
    pub async fn acquire_git(&self) -> Option<tokio::sync::OwnedSemaphorePermit> {
        match tokio::time::timeout(Duration::from_secs(5), self.git_semaphore.acquire_owned()).await {
            Ok(Ok(permit)) => Some(permit),
            _ => None,
        }
    }
}

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

    #[tokio::test]
    async fn test_concurrent_locks() {
        let state = McpState::new();
        
        // Test build lock creation
        let lock1 = state.acquire_build().await.unwrap();
        // Second lock should timeout and fail since we already have one
        let lock2 = state.acquire_build().await;
        assert!(lock2.is_none());
    }
}