brrr-lint 0.1.0

//! F* source file parser for lint rules.
//!
//! Port of reorder_fsti.py's FStarParser class.
//! Parses F* files into logical blocks for analysis and reordering.

use lazy_static::lazy_static;
use regex::Regex;
use std::collections::{HashMap, HashSet};

/// Types of top-level blocks in F* files.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum BlockType {
    Module,
    Open,
    Friend,
    SetOptions,
    Val,
    Type,
    Let,
    Assume,
    Effect,
    Class,
    Instance,
    Exception,
    UnfoldLet,
    InlineLet,
    Directive,
    Comment,
    Unknown,
}

/// A logical block in an F* file representing a single declaration
/// with its associated comments, options, and continuations.
#[derive(Debug, Clone)]
pub struct DeclarationBlock {
    pub block_type: BlockType,
    /// All names in this block (for mutual recursion).
    pub names: Vec<String>,
    /// All lines including leading comments, options.
    pub lines: Vec<String>,
    /// 1-indexed line number.
    pub start_line: usize,
    pub has_push_options: bool,
    pub has_pop_options: bool,
    /// Names this block references (potential dependencies).
    pub references: HashSet<String>,
}

impl DeclarationBlock {
    /// Primary name (first in list) for compatibility.
    pub fn name(&self) -> Option<&str> {
        self.names.first().map(|s| s.as_str())
    }

    /// Return the full text of this block.
    pub fn text(&self) -> String {
        self.lines.join("")
    }
}

lazy_static! {
    // F* identifier pattern - identifiers can contain apostrophes (primes)
    // Examples: expr', pattern', expr'_size, type_name
    static ref FSTAR_IDENT: &'static str = r"[a-zA-Z_][\w']*";

    // Declaration patterns - order matters: more specific patterns first
    // CRITICAL: Top-level F* declarations ALWAYS start at column 0
    static ref VAL_PATTERN: Regex = Regex::new(
        &format!(r"^(?:private\s+)?val\s+(?:\(([^)]+)\)|({}))", *FSTAR_IDENT)
    ).unwrap();

    static ref ASSUME_VAL_PATTERN: Regex = Regex::new(
        &format!(r"^assume\s+val\s+(?:\(([^)]+)\)|({}))", *FSTAR_IDENT)
    ).unwrap();

    static ref ASSUME_TYPE_PATTERN: Regex = Regex::new(
        &format!(r"^assume\s+type\s+({})", *FSTAR_IDENT)
    ).unwrap();

    static ref TYPE_PATTERN: Regex = Regex::new(
        &format!(r"^(?:private\s+)?(?:noeq\s+)?(?:abstract\s+)?type\s+({})", *FSTAR_IDENT)
    ).unwrap();

    static ref UNFOLD_LET_PATTERN: Regex = Regex::new(
        &format!(r"^(?:\[@[^\]]*\]\s*)*(?:private\s+)?unfold\s+(?:inline_for_extraction\s+)?let\s+({})", *FSTAR_IDENT)
    ).unwrap();

    static ref INLINE_LET_PATTERN: Regex = Regex::new(
        &format!(r"^(?:\[@[^\]]*\]\s*)*(?:private\s+)?inline_for_extraction\s+(?:noextract\s+)?(?:unfold\s+)?let\s+({})", *FSTAR_IDENT)
    ).unwrap();

    static ref LET_REC_PATTERN: Regex = Regex::new(
        &format!(r"^(?:\[@[^\]]*\]\s*)*(?:private\s+)?let\s+rec\s+({})", *FSTAR_IDENT)
    ).unwrap();

    // Match regular let bindings, including ghost let
    // The ghost modifier makes the binding erased at extraction
    static ref LET_PATTERN: Regex = Regex::new(
        &format!(r"^(?:\[@[^\]]*\]\s*)*(?:private\s+)?(?:ghost\s+)?let\s+({})", *FSTAR_IDENT)
    ).unwrap();

    static ref EFFECT_PATTERN: Regex = Regex::new(
        &format!(r"^(?:layered_)?effect\s+({})", *FSTAR_IDENT)
    ).unwrap();

    static ref NEW_EFFECT_PATTERN: Regex = Regex::new(
        &format!(r"^new_effect\s+\{{?\s*({})", *FSTAR_IDENT)
    ).unwrap();

    static ref SUB_EFFECT_PATTERN: Regex = Regex::new(
        r"^sub_effect\s+"
    ).unwrap();

    static ref CLASS_PATTERN: Regex = Regex::new(
        &format!(r"^class\s+({})", *FSTAR_IDENT)
    ).unwrap();

    static ref INSTANCE_PATTERN: Regex = Regex::new(
        &format!(r"^instance\s+({})", *FSTAR_IDENT)
    ).unwrap();

    static ref EXCEPTION_PATTERN: Regex = Regex::new(
        &format!(r"^exception\s+({})", *FSTAR_IDENT)
    ).unwrap();

    // Pattern for 'and' continuation in mutual recursion
    static ref AND_PATTERN: Regex = Regex::new(
        &format!(r"^and\s+(?:\(([^)]+)\)|({}))", *FSTAR_IDENT)
    ).unwrap();

    // Pattern for inline 'and' within a single line (e.g., "type A = ... and B = ...")
    // Used to extract additional names from mutual recursion on a single line
    static ref INLINE_AND_PATTERN: Regex = Regex::new(
        &format!(r"\band\s+(?:\(([^)]+)\)|({}))\s*=", *FSTAR_IDENT)
    ).unwrap();

    // Header patterns (kept at top, not reordered)
    static ref MODULE_PATTERN: Regex = Regex::new(r"^module\s+").unwrap();
    static ref OPEN_PATTERN: Regex = Regex::new(r"^open\s+").unwrap();
    static ref FRIEND_PATTERN: Regex = Regex::new(r"^friend\s+").unwrap();

    // Option directive patterns
    static ref PUSH_OPTIONS: Regex = Regex::new(r"^#push-options\s").unwrap();
    static ref POP_OPTIONS: Regex = Regex::new(r"^#pop-options").unwrap();
    static ref SET_OPTIONS: Regex = Regex::new(r"^#set-options\s").unwrap();
    static ref RESET_OPTIONS: Regex = Regex::new(r"^#reset-options").unwrap();
    static ref RESTART_SOLVER: Regex = Regex::new(r"^#restart-solver").unwrap();

    // Type reference pattern for dependency extraction
    // CRITICAL: F* identifiers can contain apostrophes (e.g., expr', pattern')
    // Uses fancy-regex for lookahead/lookbehind support
    // CRITICAL: The '.' in the negative lookbehind prevents matching qualified name
    // components (e.g., in `S.bn_add`, only `S` matches, not `bn_add`).
    // Without this, qualified references like `Module.name` would create false
    // dependencies on locally declared `name`, causing spurious forward-reference
    // warnings in FST002.
    static ref TYPE_REF_PATTERN: fancy_regex::Regex = fancy_regex::Regex::new(
        r"(?<![a-zA-Z0-9_'.])([A-Z][\w']*|[a-z_][\w']*)(?![a-zA-Z0-9_'])"
    ).unwrap();

    // F* keywords to exclude from dependency analysis
    // CRITICAL: This list must be comprehensive to avoid false positive dependencies
    static ref FSTAR_KEYWORDS: HashSet<&'static str> = {
        let mut s = HashSet::new();
        // Declaration keywords
        for kw in &["val", "let", "rec", "type", "noeq", "and", "with", "match",
                    "module", "open", "friend", "include",
                    "effect", "layered_effect", "new_effect", "sub_effect", "total_effect",
                    "class", "instance", "exception",
                    "assume", "private", "abstract", "unfold", "irreducible",
                    "inline_for_extraction", "noextract", "opaque_to_smt"] {
            s.insert(*kw);
        }
        // Control flow keywords
        for kw in &["if", "then", "else", "begin", "end",
                    "fun", "function", "return", "yield",
                    "in", "of", "when", "as", "try"] {
            s.insert(*kw);
        }
        // Logic/quantifier keywords
        for kw in &["forall", "exists", "True", "False", "true", "false",
                    "not", "mod", "div", "land", "lor", "lxor"] {
            s.insert(*kw);
        }
        // Type-related keywords
        for kw in &["prop", "Type", "Type0", "Type1", "eqtype", "squash",
                    "Tot", "GTot", "Lemma", "Pure", "Ghost", "ST", "Dv", "Div", "Exn",
                    "requires", "ensures", "returns", "decreases", "modifies",
                    "assert", "admit", "calc"] {
            s.insert(*kw);
        }
        // F* built-in primitive types
        for kw in &["unit", "bool", "int", "nat", "pos", "string", "char"] {
            s.insert(*kw);
        }
        // Standard library types
        for kw in &["option", "list", "either", "ref", "seq", "set", "map"] {
            s.insert(*kw);
        }
        // Module prefixes
        for kw in &["FStar", "Prims"] {
            s.insert(*kw);
        }
        // Common constructors
        for kw in &["Some", "None", "Cons", "Nil", "Inl", "Inr"] {
            s.insert(*kw);
        }
        s
    };

    // F* operator character to function name component mapping
    // In F*, operator `@%.` resolves to function `op_At_Percent_Dot`
    static ref FSTAR_OP_CHARS: HashMap<char, &'static str> = {
        let mut m = HashMap::new();
        m.insert('@', "At");
        m.insert('%', "Percent");
        m.insert('.', "Dot");
        m.insert('+', "Plus");
        m.insert('-', "Minus");
        m.insert('*', "Star");
        m.insert('/', "Slash");
        m.insert('<', "Less");
        m.insert('>', "Greater");
        m.insert('=', "Equals");
        m.insert('!', "Bang");
        m.insert('|', "Bar");
        m.insert('&', "Amp");
        m.insert('^', "Hat");
        m.insert('~', "Tilde");
        m.insert('?', "Qmark");
        m.insert(':', "Colon");
        m.insert('$', "Dollar");
        m
    };

    // Pattern to match F* custom operators (sequences of operator chars)
    // These appear in expressions like `(a + b) @%. it` or `x |> f`
    // Uses fancy_regex for lookbehind support
    static ref FSTAR_OP_PATTERN: fancy_regex::Regex = fancy_regex::Regex::new(
        r"(?<![a-zA-Z0-9_])\s([!@#$%^&*+\-/|<>=~?:.]+)\s"
    ).unwrap();
}

/// Check if line is a header (module/open/friend). Returns BlockType or None.
/// Header lines must start at column 0 (no leading whitespace).
pub fn is_header_line(line: &str) -> Option<BlockType> {
    // Header lines must not have leading whitespace
    if line.starts_with(' ') || line.starts_with('\t') {
        return None;
    }
    let stripped = line.trim();
    if MODULE_PATTERN.is_match(stripped) {
        Some(BlockType::Module)
    } else if OPEN_PATTERN.is_match(stripped) {
        Some(BlockType::Open)
    } else if FRIEND_PATTERN.is_match(stripped) {
        Some(BlockType::Friend)
    } else {
        None
    }
}

/// Check if line is a standalone #set-options at file level.
pub fn is_standalone_options(line: &str) -> bool {
    let stripped = line.trim();
    SET_OPTIONS.is_match(stripped)
        || RESET_OPTIONS.is_match(stripped)
        || RESTART_SOLVER.is_match(stripped)
}

/// Check if line is #push-options.
pub fn is_push_options(line: &str) -> bool {
    PUSH_OPTIONS.is_match(line.trim())
}

/// Check if line is #pop-options.
pub fn is_pop_options(line: &str) -> bool {
    POP_OPTIONS.is_match(line.trim())
}

/// Extract declaration name from regex captures.
fn extract_name_from_captures(caps: &regex::Captures) -> Option<String> {
    for i in 1..=caps.len() {
        if let Some(m) = caps.get(i) {
            let name = m.as_str().trim();
            // Clean up name - remove type annotations
            let name = name.split(':').next().unwrap_or(name);
            let name = name.split('(').next().unwrap_or(name).trim();
            // Handle special cases like 'unfold' appearing as name
            if matches!(
                name,
                "unfold" | "inline_for_extraction" | "noextract" | "rec"
            ) {
                continue;
            }
            if !name.is_empty() {
                return Some(name.to_string());
            }
        }
    }
    None
}

/// Extract declaration info from a line.
///
/// CRITICAL: Top-level F* declarations ALWAYS start at column 0.
/// Lines with leading whitespace are CONTINUATION lines, not new declarations.
pub fn get_declaration_info(line: &str) -> Option<(String, BlockType)> {
    // CRITICAL FIX: Top-level declarations never have leading whitespace.
    if line.starts_with(' ') || line.starts_with('\t') {
        return None;
    }

    let stripped = line.trim();

    // Skip if line is a comment or directive
    if stripped.starts_with("(*") || stripped.starts_with('#') {
        return None;
    }

    // Check patterns in order (most specific first)
    let patterns: &[(&Regex, BlockType)] = &[
        (&ASSUME_VAL_PATTERN, BlockType::Assume),
        (&ASSUME_TYPE_PATTERN, BlockType::Assume),
        (&UNFOLD_LET_PATTERN, BlockType::UnfoldLet),
        (&INLINE_LET_PATTERN, BlockType::InlineLet),
        (&LET_REC_PATTERN, BlockType::Let),
        (&VAL_PATTERN, BlockType::Val),
        (&TYPE_PATTERN, BlockType::Type),
        (&LET_PATTERN, BlockType::Let),
        (&EFFECT_PATTERN, BlockType::Effect),
        (&NEW_EFFECT_PATTERN, BlockType::Effect),
        (&CLASS_PATTERN, BlockType::Class),
        (&INSTANCE_PATTERN, BlockType::Instance),
        (&EXCEPTION_PATTERN, BlockType::Exception),
    ];

    for (pattern, block_type) in patterns {
        if let Some(caps) = pattern.captures(stripped) {
            if let Some(name) = extract_name_from_captures(&caps) {
                return Some((name, *block_type));
            }
        }
    }

    // Check sub_effect separately (no name capture)
    if SUB_EFFECT_PATTERN.is_match(stripped) {
        return Some(("sub_effect".to_string(), BlockType::Effect));
    }

    None
}

/// Extract name from 'and' continuation line.
/// 'and' in mutual recursion must start at column 0.
pub fn get_and_name(line: &str) -> Option<String> {
    // 'and' continuations must not have leading whitespace
    if line.starts_with(' ') || line.starts_with('\t') {
        return None;
    }
    let stripped = line.trim();
    AND_PATTERN
        .captures(stripped)
        .and_then(|caps| extract_name_from_captures(&caps))
}

/// Extract additional names from inline 'and' in mutual recursion.
///
/// F* allows mutual recursion on a single line:
///     type expr = ELit of int and stmt = SExpr of expr
///
/// This function finds all 'and NAME =' patterns in a line.
pub fn extract_inline_and_names(line: &str) -> Vec<String> {
    let mut names = Vec::new();
    for caps in INLINE_AND_PATTERN.captures_iter(line) {
        if let Some(name) = extract_name_from_captures(&caps) {
            names.push(name);
        }
    }
    names
}

/// Convert F* operator syntax to its op_* function name.
///
/// F* maps operator characters to names:
///     @%. -> op_At_Percent_Dot
///     |> -> op_Bar_Greater
///
/// Returns None if not all characters are valid F* operator chars.
pub fn operator_to_function_name(op: &str) -> Option<String> {
    let mut parts = Vec::new();
    for ch in op.chars() {
        if let Some(name) = FSTAR_OP_CHARS.get(&ch) {
            parts.push(*name);
        } else {
            return None;
        }
    }
    if parts.is_empty() {
        None
    } else {
        Some(format!("op_{}", parts.join("_")))
    }
}

/// Check if line is blank.
pub fn is_blank_line(line: &str) -> bool {
    line.trim().is_empty()
}

/// Count (* and *) occurrences in a line (naive, ignores strings).
pub fn count_comment_opens_closes(line: &str) -> (usize, usize) {
    let opens = line.matches("(*").count();
    let closes = line.matches("*)").count();
    (opens, closes)
}

/// Remove F* comments and string literals from text to avoid false dependencies.
pub fn strip_comments_and_strings(text: &str) -> String {
    let mut result = Vec::new();
    let chars: Vec<char> = text.chars().collect();
    let n = chars.len();
    let mut i = 0;
    let mut comment_depth = 0;

    while i < n {
        // Check for comment start
        if i + 1 < n && chars[i] == '(' && chars[i + 1] == '*' {
            comment_depth += 1;
            i += 2;
            continue;
        }

        // Check for comment end
        if i + 1 < n && chars[i] == '*' && chars[i + 1] == ')' && comment_depth > 0 {
            comment_depth -= 1;
            i += 2;
            continue;
        }

        // Inside comment - skip
        if comment_depth > 0 {
            i += 1;
            continue;
        }

        // Check for string literal
        if chars[i] == '"' {
            i += 1;
            // Skip to end of string
            while i < n && chars[i] != '"' {
                if chars[i] == '\\' && i + 1 < n {
                    i += 2; // Skip escaped char
                } else {
                    i += 1;
                }
            }
            if i < n {
                i += 1; // Skip closing quote
            }
            continue;
        }

        result.push(chars[i]);
        i += 1;
    }

    result.into_iter().collect()
}

/// Extract type/val references from declaration text.
///
/// Filters out comments and string literals to avoid false dependencies.
/// Also recognizes F* operator syntax and maps to op_* function names.
pub fn extract_references(text: &str, exclude_names: &HashSet<String>) -> HashSet<String> {
    let clean_text = strip_comments_and_strings(text);
    let mut refs = HashSet::new();

    // Extract identifier references
    // fancy-regex captures_iter returns Results, so we filter_map
    for caps in TYPE_REF_PATTERN
        .captures_iter(&clean_text)
        .filter_map(|r| r.ok())
    {
        if let Some(m) = caps.get(1) {
            let name = m.as_str();
            if !FSTAR_KEYWORDS.contains(name) && !exclude_names.contains(name) {
                refs.insert(name.to_string());
            }
        }
    }

    // Extract operator references: @%. -> op_At_Percent_Dot
    // fancy_regex captures_iter returns Results
    for caps in FSTAR_OP_PATTERN.captures_iter(&clean_text).filter_map(|r| r.ok()) {
        if let Some(m) = caps.get(1) {
            let op_str = m.as_str();
            if let Some(func_name) = operator_to_function_name(op_str) {
                if !exclude_names.contains(&func_name) {
                    refs.insert(func_name);
                }
            }
        }
    }

    refs
}

/// Parse an F* file into header lines and declaration blocks.
pub fn parse_fstar_file(content: &str) -> (Vec<String>, Vec<DeclarationBlock>) {
    let lines: Vec<&str> = content.lines().collect();
    let mut header_lines: Vec<String> = Vec::new();
    let mut blocks: Vec<DeclarationBlock> = Vec::new();

    let n = lines.len();
    let mut i = 0;

    // Phase 1: Collect header (module, opens, friends, initial comments, initial #set-options)
    let mut in_header = true;
    let mut comment_depth: i32 = 0;

    while i < n && in_header {
        let line = lines[i];
        let stripped = line.trim();

        // Track comment depth
        let (opens, closes) = count_comment_opens_closes(line);
        let prev_depth = comment_depth;
        comment_depth += opens as i32 - closes as i32;

        // Empty line in header
        if stripped.is_empty() {
            header_lines.push(format!("{}\n", line));
            i += 1;
            continue;
        }

        // Inside multi-line comment
        if prev_depth > 0 || (opens > 0 && comment_depth > 0) {
            header_lines.push(format!("{}\n", line));
            i += 1;
            continue;
        }

        // Check for module/open/friend
        if is_header_line(line).is_some() {
            header_lines.push(format!("{}\n", line));
            i += 1;
            continue;
        }

        // Check for standalone #set-options at file level
        if is_standalone_options(line) {
            header_lines.push(format!("{}\n", line));
            i += 1;
            continue;
        }

        // Check if this is a file-level comment (doc comment before declarations)
        if stripped.starts_with("(*") {
            // Collect entire comment
            let mut comment_lines_temp = vec![line];
            let mut temp_depth = comment_depth;
            let mut j = i + 1;

            while j < n && temp_depth > 0 {
                let (c_opens, c_closes) = count_comment_opens_closes(lines[j]);
                temp_depth += c_opens as i32 - c_closes as i32;
                comment_lines_temp.push(lines[j]);
                j += 1;
            }

            // Skip blank lines after comment
            let mut peek = j;
            while peek < n && lines[peek].trim().is_empty() {
                peek += 1;
            }

            // Check what follows
            if peek < n {
                let next_header = is_header_line(lines[peek]);
                let next_opts = is_standalone_options(lines[peek]);
                if next_header.is_some() || next_opts {
                    // Comment is part of header
                    for cl in comment_lines_temp {
                        header_lines.push(format!("{}\n", cl));
                    }
                    i = j;
                    comment_depth = 0;
                    continue;
                }
            }

            // This comment is before declarations - ends header
            in_header = false;
            break;
        }

        // Any other content ends header
        in_header = false;
        break;
    }

    // Reset comment depth for declaration parsing
    comment_depth = 0;

    // Phase 2: Parse declarations
    let mut pending_lines: Vec<String> = Vec::new();
    let mut pending_start = i + 1;
    let mut pending_push_options = false;

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

        // Track comment depth for multi-line comments
        let (opens, closes) = count_comment_opens_closes(line);
        let prev_depth = comment_depth;
        comment_depth += opens as i32 - closes as i32;

        // Inside multi-line comment - accumulate
        if prev_depth > 0 {
            pending_lines.push(format!("{}\n", line));
            i += 1;
            continue;
        }

        // Blank line - accumulate sparingly
        if stripped.is_empty() {
            // Only keep if we have content before, and not too many blanks
            if !pending_lines.is_empty()
                && !pending_lines
                    .last()
                    .map(|l| l.trim().is_empty())
                    .unwrap_or(true)
            {
                pending_lines.push(format!("{}\n", line));
            }
            i += 1;
            continue;
        }

        // #push-options - starts potential block
        if is_push_options(line) {
            if pending_lines.is_empty() {
                pending_start = i + 1;
            }
            pending_lines.push(format!("{}\n", line));
            pending_push_options = true;
            i += 1;
            continue;
        }

        // #pop-options - attach to current block if we have one with push
        if is_pop_options(line) {
            if !blocks.is_empty()
                && blocks.last().unwrap().has_push_options
                && !blocks.last().unwrap().has_pop_options
            {
                blocks.last_mut().unwrap().lines.push(format!("{}\n", line));
                blocks.last_mut().unwrap().has_pop_options = true;
            } else {
                pending_lines.push(format!("{}\n", line));
            }
            i += 1;
            continue;
        }

        // Standalone #set-options in body - attach to pending
        if is_standalone_options(line) {
            if pending_lines.is_empty() {
                pending_start = i + 1;
            }
            pending_lines.push(format!("{}\n", line));
            i += 1;
            continue;
        }

        // Comment start
        if stripped.starts_with("(*") {
            let mut comment_lines_here = vec![line];
            let mut temp_depth = comment_depth;
            let mut j = i + 1;

            while j < n && temp_depth > 0 {
                let (c_opens, c_closes) = count_comment_opens_closes(lines[j]);
                temp_depth += c_opens as i32 - c_closes as i32;
                comment_lines_here.push(lines[j]);
                j += 1;
            }

            if pending_lines.is_empty() {
                pending_start = i + 1;
            }
            for cl in comment_lines_here {
                pending_lines.push(format!("{}\n", cl));
            }
            i = j;
            comment_depth = 0;
            continue;
        }

        // Check for declaration start
        if let Some((decl_name, decl_type)) = get_declaration_info(line) {
            let mut all_names = vec![decl_name];

            // Check for inline 'and' on the same line
            // e.g., "type expr = ELit of int and stmt = SExpr of expr"
            let inline_and_names = extract_inline_and_names(line);
            all_names.extend(inline_and_names);

            // Collect the declaration lines
            let mut decl_lines: Vec<String> = pending_lines.clone();
            decl_lines.push(format!("{}\n", line));
            let decl_start = if pending_lines.is_empty() {
                i + 1
            } else {
                pending_start
            };
            let has_push = pending_push_options;
            pending_lines.clear();
            pending_push_options = false;

            i += 1;

            // Continue reading declaration body and 'and' continuations
            while i < n {
                let next_line = lines[i];
                let next_stripped = next_line.trim();

                // Track comments within declaration
                let (c_opens, c_closes) = count_comment_opens_closes(next_line);
                comment_depth += c_opens as i32 - c_closes as i32;

                if comment_depth > 0 {
                    decl_lines.push(format!("{}\n", next_line));
                    i += 1;
                    continue;
                }

                // Check for 'and' continuation (mutual recursion)
                if let Some(and_name) = get_and_name(next_line) {
                    all_names.push(and_name);
                    decl_lines.push(format!("{}\n", next_line));
                    i += 1;
                    continue;
                }

                // Check for new declaration (ends current)
                if get_declaration_info(next_line).is_some() {
                    break;
                }

                // Check for #pop-options
                if is_pop_options(next_line) {
                    if has_push {
                        decl_lines.push(format!("{}\n", next_line));
                        i += 1;
                    }
                    break;
                }

                // Check for #push-options (starts new context)
                if is_push_options(next_line) {
                    break;
                }

                // Header-like items shouldn't appear in body
                if is_header_line(next_line).is_some() {
                    break;
                }

                // Blank lines - check if declaration continues
                if next_stripped.is_empty() {
                    // Look ahead for continuation
                    let mut peek = i + 1;
                    let mut blank_count = 1;
                    while peek < n && lines[peek].trim().is_empty() {
                        blank_count += 1;
                        peek += 1;
                    }

                    if blank_count >= 2 && peek < n {
                        // Two+ blank lines often indicate section break
                        let peek_decl = get_declaration_info(lines[peek]);
                        let peek_and = get_and_name(lines[peek]);
                        if peek_decl.is_some() || peek_and.is_some() {
                            break;
                        }
                    }

                    decl_lines.push(format!("{}\n", next_line));
                    i += 1;
                    continue;
                }

                // Regular content line
                decl_lines.push(format!("{}\n", next_line));
                i += 1;
            }

            // Extract references from declaration
            let decl_text: String = decl_lines.concat();
            let exclude: HashSet<String> = all_names.iter().cloned().collect();
            let refs = extract_references(&decl_text, &exclude);

            let block = DeclarationBlock {
                block_type: decl_type,
                names: all_names,
                lines: decl_lines,
                start_line: decl_start,
                has_push_options: has_push,
                has_pop_options: false,
                references: refs,
            };
            blocks.push(block);
            comment_depth = 0;
            continue;
        }

        // Unrecognized content - accumulate
        if pending_lines.is_empty() {
            pending_start = i + 1;
        }
        pending_lines.push(format!("{}\n", line));
        i += 1;
    }

    // Flush any remaining pending content as comment block
    if !pending_lines.is_empty() {
        // Strip trailing blank lines
        while !pending_lines.is_empty()
            && pending_lines
                .last()
                .map(|l| l.trim().is_empty())
                .unwrap_or(false)
        {
            pending_lines.pop();
        }
        if !pending_lines.is_empty() {
            blocks.push(DeclarationBlock {
                block_type: BlockType::Comment,
                names: Vec::new(),
                lines: pending_lines,
                start_line: pending_start,
                has_push_options: pending_push_options,
                has_pop_options: false,
                references: HashSet::new(),
            });
        }
    }

    (header_lines, blocks)
}

/// Extract ordered list of definition names from .fst implementation file.
pub fn get_definition_order(content: &str) -> Vec<String> {
    let (_, blocks) = parse_fstar_file(content);
    let mut names = Vec::new();
    for block in blocks {
        for name in block.names {
            if !names.contains(&name) {
                names.push(name);
            }
        }
    }
    names
}

/// Build a dependency graph from declaration blocks.
pub fn build_dependency_graph(blocks: &[DeclarationBlock]) -> HashMap<String, HashSet<String>> {
    // Collect all declared names
    let mut declared_names = HashSet::new();
    for block in blocks {
        declared_names.extend(block.names.iter().cloned());
    }

    // Build dependency graph
    let mut deps: HashMap<String, HashSet<String>> = HashMap::new();
    for block in blocks {
        for name in &block.names {
            // Filter references to only include names declared in this file
            let valid_refs: HashSet<String> = block
                .references
                .intersection(&declared_names)
                .cloned()
                .collect();
            // Remove self-references (same block)
            let block_names: HashSet<String> = block.names.iter().cloned().collect();
            let final_refs: HashSet<String> =
                valid_refs.difference(&block_names).cloned().collect();
            deps.insert(name.clone(), final_refs);
        }
    }

    deps
}

/// Validation error from parsing.
#[derive(Debug, Clone)]
pub struct ParseValidationError {
    pub message: String,
    pub line: usize,
    pub severity: ParseErrorSeverity,
}

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum ParseErrorSeverity {
    Error,
    Warning,
}

lazy_static! {
    // Pattern to detect orphaned 'let...in' expressions that got parsed as top-level
    // These are bugs in parsing - let...in should be inside function bodies
    static ref IN_KEYWORD_PATTERN: Regex = Regex::new(r"\s+in(?:\s|$|[)\]}])").unwrap();
}

/// Validate that parsing produced sensible results.
///
/// Detects:
/// - Orphaned 'let...in' expressions parsed as declarations (should be inside function bodies)
/// - Blocks with suspicious content patterns
/// - Blocks starting with whitespace (should never happen for top-level declarations)
///
/// This is a safety net to catch parsing errors before they corrupt output files.
pub fn validate_parsing(blocks: &[DeclarationBlock]) -> Vec<ParseValidationError> {
    let mut errors = Vec::new();

    for block in blocks {
        // Check 1: Blocks should not start with whitespace
        // Top-level F* declarations ALWAYS start at column 0
        if let Some(first_line) = block.lines.first() {
            let stripped_first = first_line.trim_start_matches('\n');
            if !stripped_first.is_empty()
                && (stripped_first.starts_with(' ') || stripped_first.starts_with('\t'))
            {
                // Skip Comment and Unknown blocks - they may legitimately have whitespace
                if !matches!(block.block_type, BlockType::Comment | BlockType::Unknown) {
                    errors.push(ParseValidationError {
                        message: format!(
                            "Block '{}' starts with whitespace but is parsed as top-level {:?}. \
                             This may indicate a parsing error.",
                            block.name().unwrap_or("unnamed"),
                            block.block_type
                        ),
                        line: block.start_line,
                        severity: ParseErrorSeverity::Warning,
                    });
                }
            }
        }

        // Check 2: Orphaned 'let...in' expressions
        // These should be inside function bodies, not top-level declarations
        if block.block_type == BlockType::Let {
            if let Some(first_line) = block.lines.first() {
                let stripped = first_line.trim();
                if stripped.starts_with("let ") && !stripped.starts_with("let rec ") {
                    // Check if this line contains ' in ' suggesting it's a let...in expression
                    if IN_KEYWORD_PATTERN.is_match(first_line) {
                        // Verify balanced parens/braces before flagging
                        let paren_depth = count_balanced(first_line, '(', ')');
                        let brace_depth = count_balanced(first_line, '{', '}');
                        let bracket_depth = count_balanced(first_line, '[', ']');

                        if paren_depth == 0 && brace_depth == 0 && bracket_depth == 0 {
                            // Check what comes after 'in'
                            if let Some(in_pos) = first_line.find(" in ") {
                                let after_in = &first_line[in_pos + 4..];
                                if !after_in.trim().is_empty() {
                                    errors.push(ParseValidationError {
                                        message: format!(
                                            "Orphaned 'let...in' expression detected at line {}. \
                                             This looks like a let-binding inside a function body \
                                             that was parsed as a top-level declaration. \
                                             Check that the containing function has proper indentation.",
                                            block.start_line
                                        ),
                                        line: block.start_line,
                                        severity: ParseErrorSeverity::Error,
                                    });
                                }
                            }
                        }
                    }
                }
            }
        }
    }

    errors
}

/// Count balanced delimiter pairs.
/// Returns the net difference (opens - closes).
fn count_balanced(text: &str, open: char, close: char) -> i32 {
    let opens = text.chars().filter(|&c| c == open).count() as i32;
    let closes = text.chars().filter(|&c| c == close).count() as i32;
    opens - closes
}

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

    #[test]
    fn test_parse_simple_file() {
        let content = r#"module Test

open FStar.All

val foo : int -> int
let foo x = x + 1

type mytype = int
"#;
        let (header, blocks) = parse_fstar_file(content);
        assert!(!header.is_empty());
        assert!(blocks.iter().any(|b| b.names.contains(&"foo".to_string())));
        assert!(blocks
            .iter()
            .any(|b| b.names.contains(&"mytype".to_string())));
    }

    #[test]
    fn test_mutual_recursion() {
        let content = r#"module Test

type a = A of b
and b = B of a
"#;
        let (_, blocks) = parse_fstar_file(content);
        // Both a and b should be in the same block
        let type_block = blocks.iter().find(|b| b.names.contains(&"a".to_string()));
        assert!(type_block.is_some());
        assert!(type_block.unwrap().names.contains(&"b".to_string()));
    }

    #[test]
    fn test_no_leading_whitespace() {
        // Indented 'let' should NOT be parsed as declaration
        let content = r#"module Test

val foo : int -> int
let foo x =
  let y = x + 1 in
  y
"#;
        let (_, blocks) = parse_fstar_file(content);
        // Should only have 'foo' as declaration, not 'y'
        let names: Vec<&str> = blocks
            .iter()
            .flat_map(|b| b.names.iter().map(|s| s.as_str()))
            .collect();
        assert!(names.contains(&"foo"));
        assert!(!names.contains(&"y"));
    }

    #[test]
    fn test_validate_parsing_clean() {
        let content = r#"module Test

val foo : int -> int
let foo x = x + 1

type mytype = int
"#;
        let (_, blocks) = parse_fstar_file(content);
        let errors = validate_parsing(&blocks);
        assert!(
            errors.is_empty(),
            "Expected no validation errors, got: {:?}",
            errors
        );
    }

    #[test]
    fn test_validate_parsing_orphaned_let_in() {
        // This simulates what would happen if parser incorrectly captured
        // a let...in expression as a top-level declaration
        let blocks = vec![DeclarationBlock {
            block_type: BlockType::Let,
            names: vec!["x".to_string()],
            lines: vec!["let x = 1 in x + 1\n".to_string()],
            start_line: 5,
            has_push_options: false,
            has_pop_options: false,
            references: HashSet::new(),
        }];
        let errors = validate_parsing(&blocks);
        assert!(
            !errors.is_empty(),
            "Expected validation error for orphaned let...in"
        );
        assert!(errors[0].message.contains("let...in"));
    }

    #[test]
    fn test_extract_references_qualified_names_excluded() {
        // In F*, `S.bn_add` means `bn_add` from module alias `S`.
        // The `bn_add` part should NOT be extracted as a local reference
        // because it's a qualified name, not a reference to a locally
        // declared `bn_add`.
        let text = "val foo: S.bn_add -> Module.bar -> baz";
        let exclude = HashSet::new();
        let refs = extract_references(text, &exclude);

        // `S` and `Module` are module-level names (still extracted)
        assert!(refs.contains("S"), "Module alias S should be extracted");
        assert!(
            refs.contains("Module"),
            "Module name should be extracted"
        );

        // `bn_add` and `bar` follow a dot - they are qualified and should NOT be extracted
        assert!(
            !refs.contains("bn_add"),
            "Qualified name bn_add (after dot) should NOT be extracted"
        );
        assert!(
            !refs.contains("bar"),
            "Qualified name bar (after dot) should NOT be extracted"
        );

        // `baz` is unqualified - should be extracted
        assert!(refs.contains("baz"), "Unqualified name baz should be extracted");
    }

    #[test]
    fn test_extract_references_nested_qualified_names() {
        // Nested qualified: A.B.c - only A should match
        let text = "val foo: A.B.c -> int";
        let exclude = HashSet::new();
        let refs = extract_references(text, &exclude);

        assert!(refs.contains("A"), "Top-level module A should be extracted");
        assert!(
            !refs.contains("B"),
            "Nested module B (after dot) should NOT be extracted"
        );
        assert!(
            !refs.contains("c"),
            "Nested name c (after dot) should NOT be extracted"
        );
    }

    #[test]
    fn test_extract_references_unqualified_still_works() {
        // Unqualified references should still work normally
        let text = "val foo: mytype -> result_t";
        let exclude = HashSet::new();
        let refs = extract_references(text, &exclude);

        assert!(refs.contains("mytype"));
        assert!(refs.contains("result_t"));
        assert!(refs.contains("foo"));
    }

    #[test]
    fn test_inline_and_extraction() {
        // Single-line mutual recursion
        let line = "type expr = ELit of int and stmt = SExpr of expr";
        let names = extract_inline_and_names(line);
        assert_eq!(names, vec!["stmt"]);
    }

    #[test]
    fn test_inline_and_extraction_multiple() {
        // Multiple inline 'and' patterns
        let line = "type a = A and b = B and c = C";
        let names = extract_inline_and_names(line);
        assert_eq!(names, vec!["b", "c"]);
    }

    #[test]
    fn test_inline_and_extraction_none() {
        // No inline 'and' - just regular type
        let line = "type foo = int";
        let names = extract_inline_and_names(line);
        assert!(names.is_empty());
    }

    #[test]
    fn test_operator_to_function_name() {
        assert_eq!(operator_to_function_name("@%."), Some("op_At_Percent_Dot".to_string()));
        assert_eq!(operator_to_function_name("|>"), Some("op_Bar_Greater".to_string()));
        assert_eq!(operator_to_function_name("+"), Some("op_Plus".to_string()));
        assert_eq!(operator_to_function_name("*"), Some("op_Star".to_string()));
        assert_eq!(operator_to_function_name("<=>"), Some("op_Less_Equals_Greater".to_string()));
    }

    #[test]
    fn test_operator_to_function_name_invalid() {
        // Characters not in the operator mapping
        assert_eq!(operator_to_function_name("abc"), None);
        assert_eq!(operator_to_function_name(""), None);
    }

    #[test]
    fn test_extract_references_operators() {
        // Operators should be extracted as op_* function names
        let text = "let f x y = x @%. y";
        let exclude = HashSet::new();
        let refs = extract_references(text, &exclude);

        // Note: The pattern requires whitespace around the operator
        // "x @%. y" should extract op_At_Percent_Dot
        assert!(refs.contains("x"));
        assert!(refs.contains("y"));
        // The operator pattern matches operators surrounded by whitespace
    }

    #[test]
    fn test_parse_inline_mutual_recursion() {
        let content = r#"module Test

type expr = ELit of int and stmt = SExpr of expr
"#;
        let (_, blocks) = parse_fstar_file(content);
        // The type block should contain both names
        let type_block = blocks.iter().find(|b| b.block_type == BlockType::Type);
        assert!(type_block.is_some());
        let names = &type_block.unwrap().names;
        assert!(names.contains(&"expr".to_string()), "Should contain expr");
        assert!(names.contains(&"stmt".to_string()), "Should contain stmt from inline and");
    }
}