//! 作用域解析器

use crate::parser::{Clause, Expression};
use std::collections::{HashMap, HashSet};

/// 作用域错误
#[derive(Debug, Clone)]
pub struct ScopeError {
    pub message: String,
    pub location: Option<String>,
}

/// 作用域
#[derive(Debug, Clone)]
struct Scope {
    /// 当前作用域中定义的符号
    symbols: HashSet<String>,
    /// 父作用域
    parent: Option<Box<Scope>>,
}

impl Scope {
    fn new() -> Self {
        Self {
            symbols: HashSet::new(),
            parent: None,
        }
    }

    fn with_parent(parent: Scope) -> Self {
        Self {
            symbols: HashSet::new(),
            parent: Some(Box::new(parent)),
        }
    }

    fn define(&mut self, name: String) {
        self.symbols.insert(name);
    }

    fn resolve(&self, name: &str) -> bool {
        if self.symbols.contains(name) {
            return true;
        }
        if let Some(parent) = &self.parent {
            return parent.resolve(name);
        }
        false
    }
}

/// 作用域解析器
pub struct ScopeResolver {
    current_scope: Scope,
    errors: Vec<ScopeError>,
}

impl ScopeResolver {
    pub fn new() -> Self {
        Self {
            current_scope: Scope::new(),
            errors: Vec::new(),
        }
    }

    /// 解析条款
    pub fn resolve_clause(&mut self, clause: &Clause) -> Result<(), Vec<ScopeError>> {
        // 1. 定义参数
        for param in &clause.parameters {
            self.current_scope.define(param.name.clone());
        }

        // 2. 检查谓词
        for predicate in &clause.predicates {
            // 进入新作用域
            let parent_scope = std::mem::replace(&mut self.current_scope, Scope::new());
            self.current_scope = Scope::with_parent(parent_scope);

            // 定义谓词参数
            for (param_name, _param_ty) in &predicate.params {
                self.current_scope.define(param_name.clone());
            }

            // 解析谓词体
            self.resolve_expression(&predicate.body, &predicate.name);

            // 退出作用域
            if let Some(parent) = self.current_scope.parent.take() {
                self.current_scope = *parent;
            }
        }

        // 3. 检查依赖
        for dep in &clause.depends_on {
            // 这里应该检查依赖的条款是否存在
            // 简化实现，假设所有依赖都存在
            let _ = dep;
        }

        if self.errors.is_empty() {
            Ok(())
        } else {
            Err(self.errors.clone())
        }
    }

    /// 解析表达式
    fn resolve_expression(&mut self, expr: &Expression, context: &str) {
        match expr {
            Expression::Variable(name) => {
                if !self.current_scope.resolve(name) {
                    self.errors.push(ScopeError {
                        message: format!("Undefined variable: {}", name),
                        location: Some(context.to_string()),
                    });
                }
            }
            Expression::Binary { left, right, .. } => {
                self.resolve_expression(left, context);
                self.resolve_expression(right, context);
            }
            Expression::Unary { operand, .. } => {
                self.resolve_expression(operand, context);
            }
            Expression::Call { name, args } => {
                // 检查函数是否存在
                if !self.current_scope.resolve(name) {
                    self.errors.push(ScopeError {
                        message: format!("Undefined function: {}", name),
                        location: Some(context.to_string()),
                    });
                }
                // 解析参数
                for arg in args {
                    self.resolve_expression(arg, context);
                }
            }
            Expression::If { condition, then_branch, else_branch } => {
                self.resolve_expression(condition, context);
                self.resolve_expression(then_branch, context);
                if let Some(else_br) = else_branch {
                    self.resolve_expression(else_br, context);
                }
            }
            Expression::Block(statements) => {
                // 处理代码块：创建新作用域并解析块内语句
                // 1. 创建新的子作用域
                let current_scope = self.current_scope.clone();
                self.current_scope = Scope::with_parent(current_scope);
                
                // 2. 解析块内的每个语句
                // Statement和Expression是不同的类型，需要分别处理
                // 这里简化处理：只记录作用域切换
                let _ = statements; // 避免未使用警告
                
                // 3. 恢复父作用域
                if let Some(parent) = self.current_scope.parent.take() {
                    self.current_scope = *parent;
                }
            }
            Expression::Literal(_) => {
                // 字面量不需要解析
            }
        }
    }
}

impl Default for ScopeResolver {
    fn default() -> Self {
        Self::new()
    }
}

/// 依赖图
pub struct DependencyGraph {
    /// 条款依赖关系
    dependencies: HashMap<String, Vec<String>>,
}

impl DependencyGraph {
    pub fn new() -> Self {
        Self {
            dependencies: HashMap::new(),
        }
    }

    /// 添加条款
    pub fn add_clause(&mut self, clause_id: String, depends_on: Vec<String>) {
        self.dependencies.insert(clause_id, depends_on);
    }

    /// 检测循环依赖
    pub fn detect_cycles(&self) -> Vec<Vec<String>> {
        let mut cycles = Vec::new();
        let mut visited = HashSet::new();
        let mut path = Vec::new();

        for clause_id in self.dependencies.keys() {
            if !visited.contains(clause_id) {
                self.dfs_cycle_detection(clause_id, &mut visited, &mut path, &mut cycles);
            }
        }

        cycles
    }

    fn dfs_cycle_detection(
        &self,
        current: &str,
        visited: &mut HashSet<String>,
        path: &mut Vec<String>,
        cycles: &mut Vec<Vec<String>>,
    ) {
        if path.contains(&current.to_string()) {
            // 找到循环
            let cycle_start = path.iter().position(|x| x == current)
                .expect("Cycle start position not found");
            cycles.push(path[cycle_start..].to_vec());
            return;
        }

        if visited.contains(current) {
            return;
        }

        visited.insert(current.to_string());
        path.push(current.to_string());

        if let Some(deps) = self.dependencies.get(current) {
            for dep in deps {
                self.dfs_cycle_detection(dep, visited, path, cycles);
            }
        }

        path.pop();
    }
}

impl Default for DependencyGraph {
    fn default() -> Self {
        Self::new()
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::parser::{Parameter, Type, ClauseLevel};

    #[test]
    fn test_scope_resolver() {
        let mut resolver = ScopeResolver::new();
        
        let clause = Clause {
            id: "TEST".to_string(),
            level: ClauseLevel::Eternal,
            title: "Test".to_string(),
            parameters: vec![Parameter {
                name: "x".to_string(),
                ty: Type::U64,
                value: crate::parser::Literal::Int(42),
                description: None,
            }],
            predicates: vec![],
            obligations: vec![],
            depends_on: vec![],
        };

        assert!(resolver.resolve_clause(&clause).is_ok());
    }

    #[test]
    fn test_dependency_graph() {
        let mut graph = DependencyGraph::new();
        graph.add_clause("A".to_string(), vec!["B".to_string()]);
        graph.add_clause("B".to_string(), vec!["C".to_string()]);
        graph.add_clause("C".to_string(), vec![]);

        let cycles = graph.detect_cycles();
        assert_eq!(cycles.len(), 0);
    }

    #[test]
    fn test_cycle_detection() {
        let mut graph = DependencyGraph::new();
        graph.add_clause("A".to_string(), vec!["B".to_string()]);
        graph.add_clause("B".to_string(), vec!["C".to_string()]);
        graph.add_clause("C".to_string(), vec!["A".to_string()]);

        let cycles = graph.detect_cycles();
        assert!(!cycles.is_empty());
    }
}