brrr-lint 0.1.0

//! FST013: Documentation checker.
//!
//! Checks for missing documentation on public declarations.
//! F* supports two documentation comment styles:
//! - Block doc comments: `(** ... *)`
//! - Triple-slash comments: `/// ...`
//!
//! ## Safety Features
//!
//! This rule includes safeguards to prevent unwanted modifications:
//! - Skips auto-generated files (detected by markers in comments)
//! - Skips test files (detected by filename/path patterns)
//! - Preserves existing partial documentation
//! - Uses INFO severity (not warning/error)
//! - Marks fixes as LOW confidence (requires explicit --apply)
//!
//! ## Batch Mode
//!
//! When many declarations are missing documentation, the tool shows a summary
//! of how many stubs would be added rather than auto-applying all changes.

use lazy_static::lazy_static;
use regex::Regex;
use std::path::PathBuf;

use super::parser::{parse_fstar_file, BlockType};
use super::rules::{Diagnostic, DiagnosticSeverity, Edit, Fix, FixConfidence, FixSafetyLevel, Range, Rule, RuleCode};

lazy_static! {
    /// Pattern for block doc comments: `(**` at start of trimmed line,
    /// but not `(***` or `(**)`
    static ref DOC_BLOCK: Regex = Regex::new(r"^\(\*\*(?:[^*)]|$)").unwrap();

    /// Pattern for triple-slash doc comments at line start
    static ref DOC_TRIPLE: Regex = Regex::new(r"^\s*///").unwrap();

    /// Pattern to detect private declarations
    static ref PRIVATE_DECL: Regex = Regex::new(r"(?:^|\s)private\s").unwrap();

    /// Pattern to extract parameter names from F* signatures.
    /// Matches patterns like `(param: Type)` or `(param : Type)`.
    static ref PARAM_RE: Regex = Regex::new(r"\((\w+)\s*:").unwrap();

    /// Pattern to detect simple type abbreviations: `type foo = bar`
    /// where the RHS is a single identifier (possibly qualified like A.B.c).
    /// These are self-documenting and do not need doc comments.
    static ref TYPE_ABBREVIATION: Regex = Regex::new(
        r"(?m)^\s*(?:type|and)\s+\w+(?:\s+\w+)*\s*=\s*[\w.]+\s*$"
    ).unwrap();

    /// Patterns indicating auto-generated files that should be skipped.
    /// These appear in file headers/comments.
    static ref AUTO_GENERATED_MARKERS: Vec<Regex> = vec![
        Regex::new(r"(?i)auto[-_]?generated").unwrap(),
        Regex::new(r"(?i)do\s+not\s+edit").unwrap(),
        Regex::new(r"(?i)generated\s+by").unwrap(),
        Regex::new(r"(?i)machine[-_]?generated").unwrap(),
        Regex::new(r"(?i)automatically\s+generated").unwrap(),
        Regex::new(r"(?i)this\s+file\s+is\s+generated").unwrap(),
    ];

    /// Patterns for test file names/paths that should be skipped.
    /// NOTE: These patterns are intentionally conservative to avoid false positives.
    /// Only matches files IN test directories, not files NAMED "test.fst".
    static ref TEST_FILE_PATTERNS: Vec<Regex> = vec![
        // Test directory patterns (most reliable)
        Regex::new(r"(?i)/tests?/").unwrap(),
        Regex::new(r"(?i)/spec[s]?/").unwrap(),
        Regex::new(r"(?i)/__tests__/").unwrap(),
        // Example/scratch patterns
        Regex::new(r"(?i)/examples?/").unwrap(),
        Regex::new(r"(?i)/scratch/").unwrap(),
        // Test suffix patterns - require prefix to avoid matching "test.fst"
        Regex::new(r"(?i)[A-Z][a-zA-Z0-9]*[_-]?[Tt]est[s]?\.fsti?$").unwrap(),
        Regex::new(r"(?i)[A-Z][a-zA-Z0-9]*[_-]?[Ss]pec[s]?\.fsti?$").unwrap(),
    ];

    /// Pattern to detect return type annotation in val signature.
    /// Matches the final type after the last arrow (captures everything after ->).
    /// Uses greedy match to get the full return type.
    static ref RETURN_TYPE_PATTERN: Regex = Regex::new(r"->\s*(.+)$").unwrap();

    /// Pattern to detect unit/void return types (no meaningful return value).
    /// Matches: unit, Tot unit, Pure unit, ST unit, Lemma, etc.
    /// Also handles cases where unit appears anywhere in the return type.
    static ref UNIT_RETURN_PATTERN: Regex = Regex::new(r"(?i)^\s*(unit\b|Tot\s+unit|Pure\s+unit|ST\s+unit|Lemma\b|squash\b)").unwrap();
}

/// Extract parameter names from an F* function signature.
///
/// Parses signatures like:
/// - `(x: int) -> (y: int) -> int`
/// - `(#a: Type) -> (b: a) -> b`
///
/// Filters out:
/// - Parameters starting with underscore (internal/ignored)
/// - Implicit type parameters (starting with #)
fn extract_params_from_signature(signature: &str) -> Vec<String> {
    PARAM_RE
        .captures_iter(signature)
        .filter_map(|c| c.get(1).map(|m| m.as_str().to_string()))
        .filter(|p| !p.starts_with('_') && !p.starts_with('#'))
        .collect()
}

/// Check if a signature has a meaningful return value (not unit/void).
///
/// Returns `true` if the function returns something other than unit,
/// `false` for unit-returning functions, lemmas, etc.
fn has_meaningful_return(signature: &str) -> bool {
    if let Some(caps) = RETURN_TYPE_PATTERN.captures(signature) {
        if let Some(ret_type) = caps.get(1) {
            let ret = ret_type.as_str();
            // Check if it's a unit type or Lemma (which returns squash/proof)
            if UNIT_RETURN_PATTERN.is_match(ret) {
                return false;
            }
            return true;
        }
    }
    // If no arrow found, it's a constant (has a value)
    signature.contains(':')
}

/// Check if file content indicates it is auto-generated.
///
/// Scans the first N lines for markers like "auto-generated", "do not edit", etc.
fn is_auto_generated_content(content: &str) -> bool {
    // Only check first 50 lines (or first comment block)
    let check_lines: String = content.lines().take(50).collect::<Vec<_>>().join("\n");

    for pattern in AUTO_GENERATED_MARKERS.iter() {
        if pattern.is_match(&check_lines) {
            return true;
        }
    }
    false
}

/// Check if file path indicates it is a test file.
///
/// Checks filename patterns like *Test.fst, *_test.fst, and
/// directory patterns like /tests/, /test/, etc.
fn is_test_file(file: &PathBuf) -> bool {
    let path_str = file.to_string_lossy();

    for pattern in TEST_FILE_PATTERNS.iter() {
        if pattern.is_match(&path_str) {
            return true;
        }
    }
    false
}

/// Generate a documentation stub for a declaration.
///
/// Creates an F*-style doc comment with:
/// - Function name and parameters in the header
/// - `@param` tags for each parameter
/// - `@returns` tag for return value (for val declarations with meaningful returns)
///
/// # Arguments
/// * `name` - The name of the declaration
/// * `block_type` - The type of declaration (Val, Type, etc.)
/// * `signature` - The full signature text to extract parameters from
///
/// # Returns
/// A string containing the generated doc comment stub.
pub fn generate_doc_stub(name: &str, block_type: BlockType, signature: &str) -> String {
    let mut stub = String::new();

    stub.push_str("(** ");

    match block_type {
        BlockType::Val => {
            // Extract parameters from signature
            let params = extract_params_from_signature(signature);

            stub.push_str(&format!(
                "[{}{}] TODO: Add description.\n",
                name,
                if params.is_empty() {
                    String::new()
                } else {
                    format!(" {}", params.join(" "))
                }
            ));
            stub.push('\n');

            for param in &params {
                stub.push_str(&format!("    @param {} TODO: Describe parameter\n", param));
            }

            // Only add @returns if the function has a meaningful return value
            if has_meaningful_return(signature) {
                stub.push_str("    @returns TODO: Describe return value\n");
            }
        }
        BlockType::Type => {
            stub.push_str(&format!("[{}] TODO: Describe this type.\n", name));
        }
        _ => {
            stub.push_str(&format!("[{}] TODO: Add description.\n", name));
        }
    }

    stub.push_str("*)\n");
    stub
}

/// FST013: Documentation checker rule.
///
/// Checks that public `val` and `type` declarations have documentation comments.
///
/// ## Safety Features
///
/// This rule includes multiple safeguards:
/// - Skips auto-generated files (detected by comment markers)
/// - Skips test files (detected by filename/path patterns)
/// - Skips private declarations (marked with `private` keyword)
/// - Skips internal names (starting with underscore `_`)
/// - Skips `.fst` files that have a corresponding `.fsti` (docs belong in interface)
/// - Skips simple type abbreviations (`type t = nat`) which are self-documenting
/// - Uses INFO severity (not warning/error)
/// - Marks fixes as LOW confidence (requires explicit --apply)
///
/// ## Batch Mode Behavior
///
/// When multiple declarations are missing documentation, the diagnostics provide
/// a count and encourage reviewing before applying. Auto-fixing doc comments
/// requires explicit confirmation because:
/// 1. Generated stubs contain TODOs that need human completion
/// 2. Mass-adding stubs can clutter code without adding value
/// 3. Some declarations may intentionally lack docs (internal use)
pub struct DocCheckerRule;

impl DocCheckerRule {
    pub fn new() -> Self {
        Self
    }

    /// Check if a type declaration is a simple abbreviation.
    ///
    /// Simple type abbreviations like `type t = nat` or `type counter = size_nat`
    /// are self-documenting and do not need explicit doc comments.
    /// Returns true for `type foo = bar` where bar is a single (possibly qualified)
    /// identifier, false for ADTs, records, or complex type expressions.
    fn is_type_abbreviation(block_text: &str) -> bool {
        TYPE_ABBREVIATION.is_match(block_text)
    }

    /// Check if a `.fst` file has a corresponding `.fsti` interface file.
    ///
    /// In F*, the `.fsti` file is the public interface. When it exists,
    /// documentation belongs there, not in the `.fst` implementation.
    fn has_interface_file(fst_path: &PathBuf) -> bool {
        fst_path
            .extension()
            .map_or(false, |ext| ext == "fst")
            && fst_path.with_extension("fsti").exists()
    }

    /// Check if a block has a doc comment.
    ///
    /// Checks both:
    /// 1. The block's own lines (parser may include leading comments)
    /// 2. Lines in the source content immediately before the block
    ///
    /// Returns true if either contains a doc comment.
    fn block_has_doc_comment(
        block_lines: &[String],
        source_lines: &[&str],
        block_start_line: usize,
    ) -> bool {
        // First, check the block's own lines for doc comments
        for line in block_lines {
            let trimmed = line.trim();

            // Skip blank lines at the start
            if trimmed.is_empty() {
                continue;
            }

            // Check for block doc comment `(** ... `
            if DOC_BLOCK.is_match(trimmed) {
                return true;
            }

            // Check for triple-slash doc comment `///`
            if DOC_TRIPLE.is_match(line) {
                return true;
            }

            // If we hit a non-comment, non-blank line that's not a doc comment,
            // check if it's a regular comment or the declaration itself
            if trimmed.starts_with("(*") {
                // Regular comment - continue looking
                continue;
            }

            // Hit the actual declaration - no doc comment found in block lines
            break;
        }

        // Second, check lines before the block in the source content
        // The parser may have put the doc comment in the header section
        Self::has_doc_comment_before_line(source_lines, block_start_line)
    }

    /// Check if there's a doc comment in the lines immediately before a given line.
    ///
    /// Scans backward from `line_num` (1-indexed) looking for doc comments,
    /// skipping blank lines and tracking comment blocks.
    fn has_doc_comment_before_line(lines: &[&str], line_num: usize) -> bool {
        if line_num < 2 {
            return false;
        }

        // Convert to 0-indexed and look at line before
        let mut idx = line_num - 2;

        // Skip trailing blank lines
        while idx > 0 && lines.get(idx).map_or(false, |l| l.trim().is_empty()) {
            idx -= 1;
        }

        // Check if we're at the end of a block comment
        if let Some(line) = lines.get(idx) {
            let trimmed = line.trim();

            // Check for single-line doc block comment
            if DOC_BLOCK.is_match(trimmed) {
                return true;
            }

            // Check for triple-slash doc comment
            if DOC_TRIPLE.is_match(line) {
                return true;
            }

            // If line ends with `*)`, scan backward for opening
            if trimmed.ends_with("*)") {
                let mut scan_idx = idx;
                let mut found_doc_marker = false;

                // Scan backward through the comment
                while scan_idx > 0 {
                    if let Some(scan_line) = lines.get(scan_idx) {
                        // Check for doc comment opening marker
                        if DOC_BLOCK.is_match(scan_line.trim()) {
                            found_doc_marker = true;
                            break;
                        }

                        // Check for regular comment opening (not doc)
                        if scan_line.trim().starts_with("(*")
                            && !DOC_BLOCK.is_match(scan_line.trim())
                        {
                            break;
                        }
                    }
                    if scan_idx == 0 {
                        break;
                    }
                    scan_idx -= 1;
                }

                if found_doc_marker {
                    return true;
                }
            }
        }

        false
    }
}

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

impl Rule for DocCheckerRule {
    fn code(&self) -> RuleCode {
        RuleCode::FST013
    }

    fn check(&self, file: &PathBuf, content: &str) -> Vec<Diagnostic> {
        let mut diagnostics = Vec::new();

        // SAFETY: Skip auto-generated files
        // These files are maintained by tools, not humans
        if is_auto_generated_content(content) {
            return diagnostics;
        }

        // SAFETY: Skip test files
        // Test code often has less rigorous documentation requirements
        if is_test_file(file) {
            return diagnostics;
        }

        // If this is a .fst file with a corresponding .fsti, skip it entirely.
        // Documentation belongs in the .fsti interface file, not the implementation.
        if Self::has_interface_file(file) {
            return diagnostics;
        }

        let (_, blocks) = parse_fstar_file(content);
        let source_lines: Vec<&str> = content.lines().collect();

        for block in &blocks {
            // Only check val and type declarations
            if !matches!(block.block_type, BlockType::Val | BlockType::Type) {
                continue;
            }

            // Check if declaration is private
            let block_text = block.lines.join("");
            if PRIVATE_DECL.is_match(&block_text) {
                continue;
            }

            // Skip simple type abbreviations (e.g., `type t = nat`) - self-documenting
            if block.block_type == BlockType::Type && Self::is_type_abbreviation(&block_text) {
                continue;
            }

            for name in &block.names {
                // Skip internal names (starting with underscore)
                if name.starts_with('_') {
                    continue;
                }

                // Check if there's a doc comment for this block
                if !Self::block_has_doc_comment(&block.lines, &source_lines, block.start_line) {
                    let kind = match block.block_type {
                        BlockType::Val => "val",
                        BlockType::Type => "type",
                        _ => "declaration",
                    };

                    // Generate documentation stub as autofix
                    let stub = generate_doc_stub(name, block.block_type, &block_text);

                    // SAFETY: This fix is SAFE from a semantic perspective - adding
                    // comments does not change code behavior. However, we use LOW
                    // confidence because the generated stubs contain TODOs that need
                    // human completion.
                    let fix = Fix::new(
                        format!("Add documentation stub for `{}`", name),
                        vec![Edit {
                            file: file.clone(),
                            range: Range::new(block.start_line, 1, block.start_line, 1),
                            new_text: stub,
                        }],
                    )
                    .with_confidence(FixConfidence::Low)  // Stubs need completion
                    .with_safety_level(FixSafetyLevel::Safe)  // Adding comments is safe
                    .with_reversible(true)  // Can delete the comment
                    .with_requires_review(true);  // Need to fill in TODOs

                    diagnostics.push(Diagnostic {
                        rule: RuleCode::FST013,
                        severity: DiagnosticSeverity::Info,
                        file: file.clone(),
                        range: Range::point(block.start_line, 1),
                        message: format!(
                            "Public {} `{}` is missing documentation. \
                             Add a doc comment (** ... *) or /// above the declaration.",
                            kind, name
                        ),
                        fix: Some(fix),
                    });

                    // Only report once per block (for mutual recursion)
                    break;
                }
            }
        }

        diagnostics
    }
}

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

    #[test]
    fn test_doc_checker_missing_doc() {
        let rule = DocCheckerRule::new();
        let content = r#"module Test

val undocumented_func : int -> int
let undocumented_func x = x
"#;
        let file = PathBuf::from("test.fst");
        let diagnostics = rule.check(&file, content);

        assert_eq!(diagnostics.len(), 1);
        assert!(diagnostics[0].message.contains("undocumented_func"));
        assert!(diagnostics[0].message.contains("missing documentation"));
    }

    #[test]
    fn test_doc_checker_with_block_doc() {
        let rule = DocCheckerRule::new();
        let content = r#"module Test

(** This function does something. *)
val documented_func : int -> int
let documented_func x = x
"#;
        let file = PathBuf::from("test.fst");
        let diagnostics = rule.check(&file, content);

        assert!(diagnostics.is_empty());
    }

    #[test]
    fn test_doc_checker_with_triple_slash() {
        let rule = DocCheckerRule::new();
        let content = r#"module Test

/// This function does something.
val documented_func : int -> int
let documented_func x = x
"#;
        let file = PathBuf::from("test.fst");
        let diagnostics = rule.check(&file, content);

        assert!(diagnostics.is_empty());
    }

    #[test]
    fn test_doc_checker_private_skipped() {
        let rule = DocCheckerRule::new();
        let content = r#"module Test

private val internal_func : int -> int
let internal_func x = x
"#;
        let file = PathBuf::from("test.fst");
        let diagnostics = rule.check(&file, content);

        assert!(diagnostics.is_empty());
    }

    #[test]
    fn test_doc_checker_underscore_skipped() {
        let rule = DocCheckerRule::new();
        let content = r#"module Test

val _internal : int -> int
let _internal x = x
"#;
        let file = PathBuf::from("test.fst");
        let diagnostics = rule.check(&file, content);

        assert!(diagnostics.is_empty());
    }

    #[test]
    fn test_doc_checker_fsti_checked() {
        let rule = DocCheckerRule::new();
        let content = r#"module Test

val undocumented_func : int -> int
"#;
        let file = PathBuf::from("test.fsti");
        let diagnostics = rule.check(&file, content);

        // .fsti files ARE checked - they are the public interface
        assert_eq!(diagnostics.len(), 1);
        assert!(diagnostics[0].message.contains("undocumented_func"));
    }

    #[test]
    fn test_doc_checker_type_missing_doc() {
        let rule = DocCheckerRule::new();
        // ADT type (not a simple abbreviation) should still require docs
        let content = r#"module Test

type my_type =
  | A
  | B of int
"#;
        let file = PathBuf::from("test.fst");
        let diagnostics = rule.check(&file, content);

        assert_eq!(diagnostics.len(), 1);
        assert!(diagnostics[0].message.contains("my_type"));
        assert!(diagnostics[0].message.contains("type"));
    }

    #[test]
    fn test_doc_checker_multiline_doc_block() {
        let rule = DocCheckerRule::new();
        let content = r#"module Test

(**
 * This is a multi-line
 * documentation comment.
 *)
val documented_func : int -> int
"#;
        let file = PathBuf::from("test.fst");
        let diagnostics = rule.check(&file, content);

        assert!(diagnostics.is_empty());
    }

    #[test]
    fn test_block_has_doc_comment() {
        // Empty source lines for testing block lines only
        let empty_source: Vec<&str> = vec![];

        // Block doc comments should be detected in block lines
        let lines_with_block_doc = vec![
            "(** doc comment *)\n".to_string(),
            "val foo : int\n".to_string(),
        ];
        assert!(DocCheckerRule::block_has_doc_comment(
            &lines_with_block_doc,
            &empty_source,
            1
        ));

        // Triple slash doc comments should be detected
        let lines_with_triple_slash = vec![
            "/// doc comment\n".to_string(),
            "val foo : int\n".to_string(),
        ];
        assert!(DocCheckerRule::block_has_doc_comment(
            &lines_with_triple_slash,
            &empty_source,
            1
        ));

        // Regular comments are not doc comments
        let lines_with_regular_comment = vec![
            "(* regular comment *)\n".to_string(),
            "val foo : int\n".to_string(),
        ];
        assert!(!DocCheckerRule::block_has_doc_comment(
            &lines_with_regular_comment,
            &empty_source,
            1
        ));

        // No comment at all
        let lines_no_doc = vec!["val foo : int\n".to_string()];
        assert!(!DocCheckerRule::block_has_doc_comment(
            &lines_no_doc,
            &empty_source,
            1
        ));

        // Doc comment in source lines before block
        let source_with_doc: Vec<&str> =
            vec!["module Test", "", "(** doc comment *)", "val foo : int"];
        let block_only_val = vec!["val foo : int\n".to_string()];
        assert!(DocCheckerRule::block_has_doc_comment(
            &block_only_val,
            &source_with_doc,
            4
        ));
    }

    #[test]
    fn test_extract_params_from_signature() {
        // Simple parameters
        let sig = "val foo : (x: int) -> (y: int) -> int";
        let params = extract_params_from_signature(sig);
        assert_eq!(params, vec!["x", "y"]);

        // Parameters with spaces around colon
        let sig2 = "val bar : (a : nat) -> (b : nat) -> nat";
        let params2 = extract_params_from_signature(sig2);
        assert_eq!(params2, vec!["a", "b"]);

        // No parameters (constant)
        let sig3 = "val constant : int";
        let params3 = extract_params_from_signature(sig3);
        assert!(params3.is_empty());

        // Parameters starting with underscore should be filtered
        let sig4 = "val internal : (_x: int) -> (y: int) -> int";
        let params4 = extract_params_from_signature(sig4);
        assert_eq!(params4, vec!["y"]);

        // Complex signature with type parameters
        let sig5 = "val complex : (a: Type) -> (x: a) -> (y: a) -> a";
        let params5 = extract_params_from_signature(sig5);
        assert_eq!(params5, vec!["a", "x", "y"]);
    }

    #[test]
    fn test_generate_doc_stub_val() {
        let stub = generate_doc_stub(
            "foo",
            BlockType::Val,
            "val foo : (x: int) -> (y: int) -> int",
        );

        assert!(stub.starts_with("(** "));
        assert!(stub.ends_with("*)\n"));
        assert!(stub.contains("[foo x y]"));
        assert!(stub.contains("@param x"));
        assert!(stub.contains("@param y"));
        assert!(stub.contains("@returns"));
    }

    #[test]
    fn test_generate_doc_stub_type() {
        let stub = generate_doc_stub("my_type", BlockType::Type, "type my_type = int");

        assert!(stub.starts_with("(** "));
        assert!(stub.ends_with("*)\n"));
        assert!(stub.contains("[my_type]"));
        assert!(stub.contains("Describe this type"));
        assert!(!stub.contains("@param"));
        assert!(!stub.contains("@returns"));
    }

    #[test]
    fn test_generate_doc_stub_val_no_params() {
        let stub = generate_doc_stub("constant", BlockType::Val, "val constant : int");

        assert!(stub.starts_with("(** "));
        assert!(stub.ends_with("*)\n"));
        assert!(stub.contains("[constant]"));
        assert!(!stub.contains("@param"));
        assert!(stub.contains("@returns"));
    }

    #[test]
    fn test_doc_checker_produces_fix() {
        let rule = DocCheckerRule::new();
        let content = r#"module Test

val undocumented_func : (x: int) -> (y: int) -> int
let undocumented_func x y = x + y
"#;
        let file = PathBuf::from("test.fst");
        let diagnostics = rule.check(&file, content);

        assert_eq!(diagnostics.len(), 1);
        assert!(diagnostics[0].fix.is_some());

        let fix = diagnostics[0].fix.as_ref().unwrap();
        assert!(fix.message.contains("undocumented_func"));
        assert_eq!(fix.edits.len(), 1);

        let edit = &fix.edits[0];
        assert!(edit.new_text.contains("(** "));
        assert!(edit.new_text.contains("[undocumented_func"));
        assert!(edit.new_text.contains("@param x"));
        assert!(edit.new_text.contains("@param y"));
        assert!(edit.new_text.contains("@returns"));
        assert!(edit.new_text.contains("*)"));
    }

    #[test]
    fn test_doc_checker_type_produces_fix() {
        let rule = DocCheckerRule::new();
        // ADT type needs docs and gets a fix suggestion
        let content = r#"module Test

type my_type =
  | A
  | B of int
"#;
        let file = PathBuf::from("test.fst");
        let diagnostics = rule.check(&file, content);

        assert_eq!(diagnostics.len(), 1);
        assert!(diagnostics[0].fix.is_some());

        let fix = diagnostics[0].fix.as_ref().unwrap();
        let edit = &fix.edits[0];
        assert!(edit.new_text.contains("[my_type]"));
        assert!(edit.new_text.contains("Describe this type"));
    }

    #[test]
    fn test_doc_checker_type_abbreviation_skipped() {
        let rule = DocCheckerRule::new();

        // Simple type abbreviation: `type t = nat`
        let content1 = "module Test\n\ntype counter = size_nat\n";
        let file = PathBuf::from("test.fst");
        assert!(
            rule.check(&file, content1).is_empty(),
            "simple type abbreviation should be skipped"
        );

        // Qualified type abbreviation: `type t = A.B.c`
        let content2 = "module Test\n\ntype my_buf = Lib.Buffer.buffer\n";
        assert!(
            rule.check(&file, content2).is_empty(),
            "qualified type abbreviation should be skipped"
        );

        // Type with parameters is still an abbreviation: `type t a = a`
        let content3 = "module Test\n\ntype alias a = a\n";
        assert!(
            rule.check(&file, content3).is_empty(),
            "parameterized type abbreviation should be skipped"
        );
    }

    #[test]
    fn test_doc_checker_complex_type_not_skipped() {
        let rule = DocCheckerRule::new();
        let file = PathBuf::from("test.fst");

        // ADT with constructors needs docs
        let content = "module Test\n\ntype color =\n  | Red\n  | Blue\n";
        assert!(
            !rule.check(&file, content).is_empty(),
            "ADT type should NOT be skipped"
        );
    }

    #[test]
    fn test_doc_checker_fsti_val_checked() {
        let rule = DocCheckerRule::new();
        let content = r#"module Test

val add : int -> int -> int

val sub : int -> int -> int
"#;
        // .fsti file: public interface declarations should be checked
        // Note: Use a path that won't match test file patterns
        let file = PathBuf::from("/project/src/Module.fsti");
        let diagnostics = rule.check(&file, content);

        assert_eq!(diagnostics.len(), 2, "both undocumented vals in .fsti should warn");
    }

    #[test]
    fn test_doc_checker_fsti_with_docs_passes() {
        let rule = DocCheckerRule::new();
        let content = r#"module Test

(** Adds two integers. *)
val add : int -> int -> int

(** Subtracts two integers. *)
val sub : int -> int -> int
"#;
        let file = PathBuf::from("test.fsti");
        let diagnostics = rule.check(&file, content);

        assert!(diagnostics.is_empty(), "documented .fsti vals should pass");
    }

    #[test]
    fn test_is_type_abbreviation() {
        // Simple abbreviations
        assert!(DocCheckerRule::is_type_abbreviation("type t = nat"));
        assert!(DocCheckerRule::is_type_abbreviation("type counter = size_nat"));
        assert!(DocCheckerRule::is_type_abbreviation("type va_fuel = nat"));
        assert!(DocCheckerRule::is_type_abbreviation("type name = string"));
        assert!(DocCheckerRule::is_type_abbreviation("type t = Lib.Buffer.buffer"));

        // Parameterized abbreviations
        assert!(DocCheckerRule::is_type_abbreviation("type alias a = a"));

        // NOT abbreviations
        assert!(!DocCheckerRule::is_type_abbreviation(
            "type color =\n  | Red\n  | Blue"
        ));
        assert!(!DocCheckerRule::is_type_abbreviation(
            "type pair = { fst: int; snd: int }"
        ));
        assert!(!DocCheckerRule::is_type_abbreviation(
            "type t = x:int{x > 0}"
        ));
    }

    #[test]
    fn test_has_interface_file_nonexistent() {
        // For a path where no .fsti exists on disk, should return false
        let path = PathBuf::from("/tmp/definitely_nonexistent_fstar_test.fst");
        assert!(!DocCheckerRule::has_interface_file(&path));

        // Non-.fst extension should return false regardless
        let fsti_path = PathBuf::from("test.fsti");
        assert!(!DocCheckerRule::has_interface_file(&fsti_path));
    }

    // =========================================================================
    // SAFETY FEATURE TESTS
    // =========================================================================

    #[test]
    fn test_auto_generated_file_detection() {
        // Auto-generated markers should be detected
        assert!(is_auto_generated_content("(* This file is auto-generated. Do not edit. *)\nmodule Test"));
        assert!(is_auto_generated_content("(** Generated by some tool *)\nmodule Test"));
        assert!(is_auto_generated_content("// AUTO_GENERATED\nmodule Test"));
        assert!(is_auto_generated_content("(* MACHINE GENERATED - DO NOT EDIT *)\nmodule Test"));
        assert!(is_auto_generated_content("(* This file is automatically generated *)\nmodule Test"));

        // Normal files should not be flagged
        assert!(!is_auto_generated_content("module Test\nval foo : int"));
        assert!(!is_auto_generated_content("(** Documentation for module *)\nmodule Test"));
        assert!(!is_auto_generated_content("(* Regular comment *)\nmodule Test\nlet x = 1"));
    }

    #[test]
    fn test_test_file_detection() {
        // Test directory patterns (primary detection mechanism)
        assert!(is_test_file(&PathBuf::from("/project/tests/Module.fst")));
        assert!(is_test_file(&PathBuf::from("/project/test/Module.fst")));
        assert!(is_test_file(&PathBuf::from("/project/__tests__/Module.fst")));
        assert!(is_test_file(&PathBuf::from("/project/specs/Module.fst")));
        assert!(is_test_file(&PathBuf::from("/project/examples/Demo.fst")));

        // Test suffix patterns (require CamelCase prefix)
        assert!(is_test_file(&PathBuf::from("/project/MyModuleTest.fst")));
        assert!(is_test_file(&PathBuf::from("/project/MyModule_test.fst")));
        assert!(is_test_file(&PathBuf::from("/project/SecuritySpec.fst")));

        // Non-test files - these should NOT be skipped
        assert!(!is_test_file(&PathBuf::from("/project/src/Module.fst")));
        assert!(!is_test_file(&PathBuf::from("/project/core/Types.fsti")));
        assert!(!is_test_file(&PathBuf::from("/project/lib/Utils.fst")));
        // "test.fst" standalone is NOT a test file (it's a module name)
        assert!(!is_test_file(&PathBuf::from("test.fst")));
        assert!(!is_test_file(&PathBuf::from("/project/Test.fst")));
    }

    #[test]
    fn test_doc_checker_skips_auto_generated() {
        let rule = DocCheckerRule::new();
        let content = r#"(* AUTO-GENERATED - DO NOT EDIT *)
module Test

val undocumented_func : int -> int
"#;
        let file = PathBuf::from("test.fst");
        let diagnostics = rule.check(&file, content);

        assert!(diagnostics.is_empty(), "Auto-generated files should be skipped");
    }

    #[test]
    fn test_doc_checker_skips_test_files() {
        let rule = DocCheckerRule::new();
        let content = r#"module Test

val undocumented_func : int -> int
"#;
        let file = PathBuf::from("/project/tests/Test.fst");
        let diagnostics = rule.check(&file, content);

        assert!(diagnostics.is_empty(), "Test files should be skipped");
    }

    // =========================================================================
    // RETURN TYPE DETECTION TESTS
    // =========================================================================

    #[test]
    fn test_has_meaningful_return() {
        // Functions with meaningful returns
        assert!(has_meaningful_return("val foo : int -> int"));
        assert!(has_meaningful_return("val bar : (x: nat) -> nat"));
        assert!(has_meaningful_return("val complex : (a: Type) -> (x: a) -> option a"));
        assert!(has_meaningful_return("val get_value : unit -> string"));

        // Functions without meaningful returns (unit, Lemma, etc.)
        assert!(!has_meaningful_return("val foo : int -> unit"));
        assert!(!has_meaningful_return("val lemma_foo : (x: int) -> Lemma (x >= 0)"));
        // Note: "Tot unit" as a return type should be detected
        // The pattern captures "Tot unit" and matches "unit" within
        assert!(!has_meaningful_return("val stateful : int -> unit"));
    }

    #[test]
    fn test_generate_doc_stub_no_returns_for_unit() {
        let stub = generate_doc_stub("action", BlockType::Val, "val action : int -> unit");
        assert!(!stub.contains("@returns"), "Unit-returning functions should not have @returns");
    }

    #[test]
    fn test_generate_doc_stub_no_returns_for_lemma() {
        // Lemmas return a proof/squash, not a meaningful value
        // Signature: val name : param_type -> Lemma ...
        let stub = generate_doc_stub("my_lemma", BlockType::Val, "val my_lemma : int -> Lemma True");
        assert!(!stub.contains("@returns"), "Lemmas should not have @returns");
    }

    // =========================================================================
    // COMPLEX SIGNATURE TESTS (from real F* code)
    // =========================================================================

    #[test]
    fn test_extract_params_complex_signatures() {
        // From BrrrInformationFlow.fsti - complex signatures
        let sig1 = "val sec_typecheck (ctx: sec_ctx) (pc: pc_label) (e: expr) : Tot (option labeled_type) (decreases e)";
        let params1 = extract_params_from_signature(sig1);
        assert_eq!(params1, vec!["ctx", "pc", "e"]);

        // Note: F* allows multiple params to share a type: (v1 v2 v3: value)
        // Our current regex only captures "param:" pattern, so this is a limitation.
        // The first param in the group will be captured.
        let sig2 = "val value_eq_trans (v1: value) (v2: value) (v3: value) : Lemma";
        let params2 = extract_params_from_signature(sig2);
        assert_eq!(params2, vec!["v1", "v2", "v3"]);

        // Generic/polymorphic parameters - #a is implicit
        // The # marker is filtered out. Only explicit parameters are kept.
        let sig3 = "val untrusted (#a:Type) (v: a) : integrity_labeled a";
        let params3 = extract_params_from_signature(sig3);
        // #a is captured as "#a" and filtered because it starts with #
        // Only 'v' remains as an explicit parameter
        assert_eq!(params3, vec!["v"]);
    }

    #[test]
    fn test_generate_stub_for_lemma() {
        let stub = generate_doc_stub(
            "sec_leq_refl",
            BlockType::Val,
            // Note: For the return type detector, the signature needs "->" before Lemma
            "val sec_leq_refl : (l: sec_level) -> Lemma (ensures sec_leq l l = true)",
        );

        assert!(stub.contains("[sec_leq_refl l]"));
        assert!(stub.contains("@param l"));
        assert!(!stub.contains("@returns"), "Lemmas should not have @returns");
    }

    #[test]
    fn test_generate_stub_for_complex_function() {
        let stub = generate_doc_stub(
            "dlm_declassify_logged",
            BlockType::Val,
            "val dlm_declassify_logged (env: acts_for_env) (req: dlm_declassify_request) (log: dlm_audit_log) (timestamp: nat) : option (dlm_label & dlm_audit_log)",
        );

        assert!(stub.contains("[dlm_declassify_logged env req log timestamp]"));
        assert!(stub.contains("@param env"));
        assert!(stub.contains("@param req"));
        assert!(stub.contains("@param log"));
        assert!(stub.contains("@param timestamp"));
        assert!(stub.contains("@returns"));
    }

    // =========================================================================
    // FIX CONFIDENCE TESTS
    // =========================================================================

    #[test]
    fn test_doc_fix_is_low_confidence() {
        let rule = DocCheckerRule::new();
        let content = r#"module Test

val undocumented_func : int -> int
"#;
        let file = PathBuf::from("test.fst");
        let diagnostics = rule.check(&file, content);

        assert_eq!(diagnostics.len(), 1);
        let fix = diagnostics[0].fix.as_ref().unwrap();

        // Doc fixes should be marked as unsafe (low confidence)
        assert!(!fix.is_safe, "Doc fixes should not be marked as safe");
        assert_eq!(fix.confidence, FixConfidence::Low, "Doc fixes should have low confidence");
        assert!(fix.unsafe_reason.is_some(), "Doc fixes should have an unsafe reason");
    }

    #[test]
    fn test_doc_fix_cannot_auto_apply() {
        let rule = DocCheckerRule::new();
        let content = r#"module Test

val foo : int -> int
"#;
        let file = PathBuf::from("test.fst");
        let diagnostics = rule.check(&file, content);

        assert_eq!(diagnostics.len(), 1);
        let fix = diagnostics[0].fix.as_ref().unwrap();

        // Should NOT auto-apply
        assert!(!fix.can_auto_apply(), "Doc fixes should require explicit --apply");
    }
}