//! Parser for the verification DSL.
//!
//! Parses specification files and Solidity-style annotations.

use crate::ast::*;
use crate::error::{VerifierError, VerifierResult};
use crate::{FunctionSig, Mutability, VarType, VerificationContext, Visibility};
use std::collections::HashMap;

/// Specification parser.
pub struct SpecParser;

impl SpecParser {
    /// Parses a contract from source code with embedded specifications.
    pub fn parse_contract(source: &str) -> VerifierResult<VerificationContext> {
        let mut ctx = VerificationContext {
            contract_name: String::new(),
            source: source.to_string(),
            specs: Vec::new(),
            state_vars: HashMap::new(),
            functions: HashMap::new(),
        };

        let lines: Vec<&str> = source.lines().collect();
        let mut i = 0;

        while i < lines.len() {
            let line = lines[i].trim();

            // Parse contract declaration
            if line.starts_with("contract ") || line.starts_with("contract\t") {
                ctx.contract_name = Self::parse_contract_name(line)?;
            }

            // Parse specification comments
            if line.starts_with("/// @") || line.starts_with("// @") {
                let spec = Self::parse_spec_comment(line, &lines, &mut i)?;
                ctx.specs.push(spec);
            }

            // Parse state variable
            if Self::is_state_var_line(line) {
                let (name, var_type) = Self::parse_state_var(line)?;
                ctx.state_vars.insert(name, var_type);
            }

            // Parse function
            if line.starts_with("function ") {
                let func = Self::parse_function_sig(line)?;
                ctx.functions.insert(func.name.clone(), func);
            }

            i += 1;
        }

        Ok(ctx)
    }

    /// Parses contract name from declaration line.
    fn parse_contract_name(line: &str) -> VerifierResult<String> {
        let parts: Vec<&str> = line.split_whitespace().collect();
        if parts.len() >= 2 {
            Ok(parts[1].trim_end_matches('{').to_string())
        } else {
            Err(VerifierError::ParseError {
                line: 0,
                message: "Invalid contract declaration".to_string(),
            })
        }
    }

    /// Parses a specification comment.
    fn parse_spec_comment(
        line: &str,
        _lines: &[&str],
        _i: &mut usize,
    ) -> VerifierResult<Specification> {
        let content = line
            .trim_start_matches("///")
            .trim_start_matches("//")
            .trim();

        if content.starts_with("@invariant") {
            Self::parse_invariant(content)
        } else if content.starts_with("@property") {
            Self::parse_property(content)
        } else if content.starts_with("@requires") || content.starts_with("@ensures") {
            Self::parse_annotation(content)
        } else {
            Err(VerifierError::ParseError {
                line: 0,
                message: format!("Unknown specification: {}", content),
            })
        }
    }

    /// Parses an invariant specification.
    fn parse_invariant(content: &str) -> VerifierResult<Specification> {
        let parts: Vec<&str> = content.splitn(2, ' ').collect();
        let expr_str = if parts.len() > 1 { parts[1] } else { "true" };

        // Extract name if provided: @invariant name: expr
        let (name, expr_str) = if let Some(idx) = expr_str.find(':') {
            let name = expr_str[..idx].trim().to_string();
            let expr = expr_str[idx + 1..].trim();
            (name, expr)
        } else {
            ("unnamed".to_string(), expr_str)
        };

        let expr = Self::parse_expression(expr_str)?;

        Ok(Specification::Invariant(Invariant {
            name,
            expr,
            description: None,
        }))
    }

    /// Parses a property specification.
    fn parse_property(content: &str) -> VerifierResult<Specification> {
        let parts: Vec<&str> = content.splitn(2, ' ').collect();
        let expr_str = if parts.len() > 1 { parts[1] } else { "true" };

        let (name, kind, expr_str) = Self::parse_property_header(expr_str)?;
        let expr = Self::parse_expression(expr_str)?;

        Ok(Specification::Property(Property {
            name,
            kind,
            expr,
            description: None,
        }))
    }

    /// Parses property header to extract name and kind.
    fn parse_property_header(s: &str) -> VerifierResult<(String, PropertyKind, &str)> {
        // Format: [safety|liveness] name: expr
        let kind = if s.starts_with("safety") {
            PropertyKind::Safety
        } else if s.starts_with("liveness") {
            PropertyKind::Liveness
        } else if s.starts_with("reachability") {
            PropertyKind::Reachability
        } else {
            PropertyKind::Custom
        };

        // Skip kind keyword
        let s = s
            .trim_start_matches("safety")
            .trim_start_matches("liveness")
            .trim_start_matches("reachability")
            .trim();

        // Extract name
        if let Some(idx) = s.find(':') {
            let name = s[..idx].trim().to_string();
            let expr = s[idx + 1..].trim();
            Ok((name, kind, expr))
        } else {
            Ok(("unnamed".to_string(), kind, s))
        }
    }

    /// Parses a function annotation.
    fn parse_annotation(content: &str) -> VerifierResult<Specification> {
        let (kind, rest) = if content.starts_with("@requires") {
            ("requires", content.trim_start_matches("@requires").trim())
        } else {
            ("ensures", content.trim_start_matches("@ensures").trim())
        };

        let expr = Self::parse_expression(rest)?;

        let annotation = Annotation {
            function: String::new(), // Will be filled in by context
            requires: if kind == "requires" {
                vec![expr.clone()]
            } else {
                vec![]
            },
            ensures: if kind == "ensures" {
                vec![expr]
            } else {
                vec![]
            },
            modifies: vec![],
        };

        Ok(Specification::Annotation(annotation))
    }

    /// Parses an expression from string.
    pub fn parse_expression(s: &str) -> VerifierResult<Expression> {
        let s = s.trim();

        // Handle parentheses
        if s.starts_with('(') && s.ends_with(')') {
            return Self::parse_expression(&s[1..s.len() - 1]);
        }

        // Handle quantifiers
        if s.starts_with("forall") || s.starts_with("exists") {
            return Self::parse_quantifier(s);
        }

        // Handle old()
        if s.starts_with("old(") && s.ends_with(')') {
            let inner = &s[4..s.len() - 1];
            return Ok(Expression::Old(Box::new(Self::parse_expression(inner)?)));
        }

        // Handle binary operators (lowest precedence first)
        for (op_str, op) in [
            ("==>", BinaryOperator::Implies),
            ("<==>", BinaryOperator::Iff),
            ("||", BinaryOperator::Or),
            ("&&", BinaryOperator::And),
            ("==", BinaryOperator::Eq),
            ("!=", BinaryOperator::Ne),
            ("<=", BinaryOperator::Le),
            (">=", BinaryOperator::Ge),
            ("<", BinaryOperator::Lt),
            (">", BinaryOperator::Gt),
            ("+", BinaryOperator::Add),
            ("-", BinaryOperator::Sub),
            ("*", BinaryOperator::Mul),
            ("/", BinaryOperator::Div),
            ("%", BinaryOperator::Mod),
        ] {
            if let Some(idx) = Self::find_operator(s, op_str) {
                let left = Self::parse_expression(&s[..idx])?;
                let right = Self::parse_expression(&s[idx + op_str.len()..])?;
                return Ok(Expression::BinaryOp {
                    left: Box::new(left),
                    op,
                    right: Box::new(right),
                });
            }
        }

        // Handle unary operators
        if s.starts_with('!') {
            let operand = Self::parse_expression(&s[1..])?;
            return Ok(Expression::UnaryOp {
                op: UnaryOperator::Not,
                operand: Box::new(operand),
            });
        }

        // Handle literals
        if s == "true" {
            return Ok(Expression::Literal(Literal::Bool(true)));
        }
        if s == "false" {
            return Ok(Expression::Literal(Literal::Bool(false)));
        }
        if let Ok(n) = s.parse::<u128>() {
            return Ok(Expression::Literal(Literal::Uint(n)));
        }

        // Handle special keywords
        if s == "result" {
            return Ok(Expression::Result);
        }

        // Handle member access
        if let Some(idx) = s.rfind('.') {
            let object = Self::parse_expression(&s[..idx])?;
            let member = s[idx + 1..].to_string();
            return Ok(Expression::MemberAccess {
                object: Box::new(object),
                member,
            });
        }

        // Handle array index
        if s.ends_with(']') {
            if let Some(idx) = s.rfind('[') {
                let array = Self::parse_expression(&s[..idx])?;
                let index = Self::parse_expression(&s[idx + 1..s.len() - 1])?;
                return Ok(Expression::Index {
                    array: Box::new(array),
                    index: Box::new(index),
                });
            }
        }

        // Handle function calls
        if s.ends_with(')') {
            if let Some(idx) = s.find('(') {
                let function = s[..idx].to_string();
                let args_str = &s[idx + 1..s.len() - 1];
                let args = Self::parse_args(args_str)?;
                return Ok(Expression::FunctionCall { function, args });
            }
        }

        // Default: variable reference
        Ok(Expression::Variable(s.to_string()))
    }

    /// Finds an operator in string, respecting parentheses.
    fn find_operator(s: &str, op: &str) -> Option<usize> {
        let mut depth = 0;
        let chars: Vec<char> = s.chars().collect();
        let op_chars: Vec<char> = op.chars().collect();

        for i in 0..chars.len() {
            match chars[i] {
                '(' | '[' => depth += 1,
                ')' | ']' => depth -= 1,
                _ => {}
            }

            if depth == 0 && i + op_chars.len() <= chars.len() {
                let slice: String = chars[i..i + op_chars.len()].iter().collect();
                if slice == op {
                    return Some(i);
                }
            }
        }

        None
    }

    /// Parses a quantifier expression.
    fn parse_quantifier(s: &str) -> VerifierResult<Expression> {
        let kind = if s.starts_with("forall") {
            QuantifierKind::ForAll
        } else {
            QuantifierKind::Exists
        };

        // Format: forall x: uint256 :: expr
        let rest = s
            .trim_start_matches("forall")
            .trim_start_matches("exists")
            .trim();

        // Find variable and type
        let parts: Vec<&str> = rest.splitn(2, "::").collect();
        if parts.len() != 2 {
            return Err(VerifierError::ParseError {
                line: 0,
                message: "Invalid quantifier syntax".to_string(),
            });
        }

        let var_part = parts[0].trim();
        let body_str = parts[1].trim();

        let (var, var_type) = Self::parse_typed_var(var_part)?;
        let body = Self::parse_expression(body_str)?;

        Ok(Expression::Quantifier {
            kind,
            var,
            var_type,
            body: Box::new(body),
        })
    }

    /// Parses a typed variable declaration.
    fn parse_typed_var(s: &str) -> VerifierResult<(String, VarType)> {
        let parts: Vec<&str> = s.split(':').collect();
        if parts.len() != 2 {
            return Err(VerifierError::ParseError {
                line: 0,
                message: "Invalid typed variable".to_string(),
            });
        }

        let var = parts[0].trim().to_string();
        let type_str = parts[1].trim();
        let var_type = Self::parse_type(type_str)?;

        Ok((var, var_type))
    }

    /// Parses a type string.
    pub fn parse_type(s: &str) -> VerifierResult<VarType> {
        let s = s.trim();

        if s.starts_with("uint") {
            let bits: u16 = s[4..].parse().unwrap_or(256);
            return Ok(VarType::Uint(bits));
        }
        if s.starts_with("int") {
            let bits: u16 = s[3..].parse().unwrap_or(256);
            return Ok(VarType::Int(bits));
        }
        if s == "bool" {
            return Ok(VarType::Bool);
        }
        if s == "address" {
            return Ok(VarType::Address);
        }
        if s.starts_with("bytes") && s.len() > 5 {
            let n: u16 = s[5..].parse().unwrap_or(32);
            return Ok(VarType::Bytes(n));
        }
        if s == "bytes" {
            return Ok(VarType::DynBytes);
        }
        if s == "string" {
            return Ok(VarType::String);
        }

        // Array type
        if s.ends_with("[]") {
            let inner = Self::parse_type(&s[..s.len() - 2])?;
            return Ok(VarType::Array(Box::new(inner)));
        }

        // Mapping type
        if s.starts_with("mapping(") && s.ends_with(')') {
            let inner = &s[8..s.len() - 1];
            if let Some(idx) = inner.find("=>") {
                let key = Self::parse_type(&inner[..idx].trim())?;
                let value = Self::parse_type(&inner[idx + 2..].trim())?;
                return Ok(VarType::Mapping(Box::new(key), Box::new(value)));
            }
        }

        Err(VerifierError::ParseError {
            line: 0,
            message: format!("Unknown type: {}", s),
        })
    }

    /// Parses function arguments.
    fn parse_args(s: &str) -> VerifierResult<Vec<Expression>> {
        if s.trim().is_empty() {
            return Ok(vec![]);
        }

        let mut args = Vec::new();
        let mut current = String::new();
        let mut depth = 0;

        for c in s.chars() {
            match c {
                '(' | '[' => {
                    depth += 1;
                    current.push(c);
                }
                ')' | ']' => {
                    depth -= 1;
                    current.push(c);
                }
                ',' if depth == 0 => {
                    args.push(Self::parse_expression(current.trim())?);
                    current.clear();
                }
                _ => current.push(c),
            }
        }

        if !current.trim().is_empty() {
            args.push(Self::parse_expression(current.trim())?);
        }

        Ok(args)
    }

    /// Checks if a line declares a state variable.
    fn is_state_var_line(line: &str) -> bool {
        // Simple heuristic: type followed by visibility/name
        let keywords = ["uint", "int", "bool", "address", "bytes", "string", "mapping"];
        keywords.iter().any(|k| line.starts_with(k))
    }

    /// Parses a state variable declaration.
    fn parse_state_var(line: &str) -> VerifierResult<(String, VarType)> {
        let parts: Vec<&str> = line.split_whitespace().collect();
        if parts.len() < 2 {
            return Err(VerifierError::ParseError {
                line: 0,
                message: "Invalid state variable".to_string(),
            });
        }

        let var_type = Self::parse_type(parts[0])?;
        let name = parts
            .last()
            .unwrap()
            .trim_end_matches(';')
            .trim_end_matches('=')
            .to_string();

        Ok((name, var_type))
    }

    /// Parses a function signature.
    fn parse_function_sig(line: &str) -> VerifierResult<FunctionSig> {
        let line = line.trim_start_matches("function").trim();

        // Extract function name
        let name_end = line.find('(').unwrap_or(line.len());
        let name = line[..name_end].trim().to_string();

        // Extract parameters
        let params_start = line.find('(').unwrap_or(0);
        let params_end = line.find(')').unwrap_or(line.len());
        let params_str = &line[params_start + 1..params_end];
        let params = Self::parse_params(params_str)?;

        // Extract return type
        let returns = if let Some(idx) = line.find("returns") {
            let ret_start = line[idx..].find('(').map(|i| idx + i + 1);
            let ret_end = line[idx..].find(')').map(|i| idx + i);
            if let (Some(start), Some(end)) = (ret_start, ret_end) {
                Some(Self::parse_type(&line[start..end])?)
            } else {
                None
            }
        } else {
            None
        };

        // Extract visibility and mutability
        let visibility = if line.contains("external") {
            Visibility::External
        } else if line.contains("internal") {
            Visibility::Internal
        } else if line.contains("private") {
            Visibility::Private
        } else {
            Visibility::Public
        };

        let mutability = if line.contains("pure") {
            Mutability::Pure
        } else if line.contains("view") {
            Mutability::View
        } else if line.contains("payable") {
            Mutability::Payable
        } else {
            Mutability::Nonpayable
        };

        Ok(FunctionSig {
            name,
            params,
            returns,
            visibility,
            mutability,
            preconditions: vec![],
            postconditions: vec![],
        })
    }

    /// Parses function parameters.
    fn parse_params(s: &str) -> VerifierResult<Vec<(String, VarType)>> {
        if s.trim().is_empty() {
            return Ok(vec![]);
        }

        let mut params = Vec::new();
        for param in s.split(',') {
            let parts: Vec<&str> = param.split_whitespace().collect();
            if parts.len() >= 2 {
                let var_type = Self::parse_type(parts[0])?;
                let name = parts.last().unwrap().to_string();
                params.push((name, var_type));
            }
        }

        Ok(params)
    }
}

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

    #[test]
    fn test_parse_type() {
        assert_eq!(SpecParser::parse_type("uint256").unwrap(), VarType::Uint(256));
        assert_eq!(SpecParser::parse_type("int128").unwrap(), VarType::Int(128));
        assert_eq!(SpecParser::parse_type("bool").unwrap(), VarType::Bool);
        assert_eq!(SpecParser::parse_type("address").unwrap(), VarType::Address);
    }

    #[test]
    fn test_parse_expression() {
        let expr = SpecParser::parse_expression("x + 1").unwrap();
        if let Expression::BinaryOp { op, .. } = expr {
            assert_eq!(op, BinaryOperator::Add);
        } else {
            panic!("Expected BinaryOp");
        }
    }

    #[test]
    fn test_parse_comparison() {
        let expr = SpecParser::parse_expression("balance >= 0").unwrap();
        if let Expression::BinaryOp { op, .. } = expr {
            assert_eq!(op, BinaryOperator::Ge);
        } else {
            panic!("Expected BinaryOp");
        }
    }

    #[test]
    fn test_parse_invariant() {
        let spec = SpecParser::parse_invariant("@invariant positive: balance >= 0").unwrap();
        if let Specification::Invariant(inv) = spec {
            assert_eq!(inv.name, "positive");
        } else {
            panic!("Expected Invariant");
        }
    }
}