brrr-lint 0.1.0

//! FST006: Naming convention checker for F* code.
//!
//! F* naming conventions (derived from community codebase analysis of FStar stdlib,
//! hacl-star, everparse, and other major projects):
//!
//! - Modules: CamelCase.Dot.Separated (e.g., FStar.List.Tot)
//! - Types: Must start with lowercase. Both snake_case (nat, pure_wp, int_t) and
//!   camelCase (inttype, secrecy_level) are accepted. PascalCase types are flagged
//!   because they look like constructors or module names.
//! - Functions/values: Must start with lowercase. Both snake_case (fold_left) and
//!   camelCase (loadState, createL, mapT) are widely used in the community.
//!   PascalCase (starts with uppercase) is flagged as it conflicts with
//!   constructor/module/effect conventions.
//! - Lemmas: lemma_* prefix or *_lemma suffix
//! - Effects: CamelCase starting with uppercase (e.g., Tot, GTot, Lemma, Stack)
//! - Constructors: CamelCase (Some, None, U8, Cons) - not checked here as the
//!   parser extracts type names, not constructor names.

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

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

lazy_static! {
    /// Pattern for valid F* value/type names: starts with lowercase or underscore,
    /// followed by any alphanumeric or underscore. Accepts both snake_case and
    /// camelCase since the F* community uses both freely (e.g., fold_left,
    /// loadState, createL, mapT, storeState_inner, ivTable_S).
    static ref LOWERCASE_START: Regex = Regex::new(r"^[a-z_][a-zA-Z0-9_]*$").unwrap();

    /// Pattern for CamelCase identifiers: starts with uppercase letter,
    /// followed by alphanumeric characters. Used for effects.
    static ref CAMEL_CASE: Regex = Regex::new(r"^[A-Z][a-zA-Z0-9]*$").unwrap();

    /// Pattern for PascalCase identifiers: starts with uppercase letter.
    /// Used to detect type/function names that look like constructors or modules.
    static ref STARTS_UPPERCASE: Regex = Regex::new(r"^[A-Z]").unwrap();

}

/// Check if name starts with lowercase (valid for F* types, functions, values).
/// Both snake_case and camelCase are accepted since the F* community uses both.
fn is_lowercase_start(name: &str) -> bool {
    LOWERCASE_START.is_match(name)
}

/// Check if name follows CamelCase convention (for effects).
fn is_camel_case(name: &str) -> bool {
    CAMEL_CASE.is_match(name)
}

/// Check if name starts with uppercase (looks like constructor/module/effect).
fn starts_with_uppercase(name: &str) -> bool {
    STARTS_UPPERCASE.is_match(name)
}

/// Convert a PascalCase name to snake_case for suggestion purposes.
///
/// Examples:
/// - "BadType" -> "bad_type"
/// - "FooBar" -> "foo_bar"
/// - "XMLParser" -> "xml_parser"
fn to_snake_case(name: &str) -> String {
    let mut result = String::with_capacity(name.len() + 4);
    let mut prev_was_upper = false;
    let mut prev_was_underscore = true; // Treat start as if preceded by underscore

    for (i, c) in name.chars().enumerate() {
        if c.is_uppercase() {
            // Add underscore before uppercase if:
            // - Not at start
            // - Previous char was not uppercase (to handle "HTTPServer" -> "http_server")
            // - Or next char is lowercase (to handle "XMLParser" -> "xml_parser")
            if i > 0 && !prev_was_underscore {
                let next_is_lower = name
                    .chars()
                    .nth(i + 1)
                    .map(|n| n.is_lowercase())
                    .unwrap_or(false);
                if !prev_was_upper || next_is_lower {
                    result.push('_');
                }
            }
            result.push(c.to_ascii_lowercase());
            prev_was_upper = true;
            prev_was_underscore = false;
        } else if c == '_' {
            result.push(c);
            prev_was_upper = false;
            prev_was_underscore = true;
        } else {
            result.push(c);
            prev_was_upper = false;
            prev_was_underscore = false;
        }
    }

    result
}

/// FST006: Naming convention checker rule.
pub struct NamingRule;

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

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

impl Rule for NamingRule {
    fn code(&self) -> RuleCode {
        RuleCode::FST006
    }

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

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

                // Strip trailing primes for checking (e.g., expr', pattern')
                let check_name = name.trim_end_matches('\'');
                if check_name.is_empty() {
                    continue;
                }

                match block.block_type {
                    BlockType::Type => {
                        // Types must start with lowercase in F*.
                        // Names starting with uppercase look like constructors or modules.
                        if starts_with_uppercase(check_name) {
                            let suggested = to_snake_case(check_name);
                            diagnostics.push(Diagnostic {
                                rule: RuleCode::FST006,
                                severity: DiagnosticSeverity::Info,
                                file: file.clone(),
                                range: Range::point(block.start_line, 1),
                                message: format!(
                                    "Type `{}` should start with lowercase. \
                                     PascalCase is reserved for constructors/modules. \
                                     Suggested: `{}`",
                                    name, suggested
                                ),
                                fix: None,
                            });
                        }
                    }

                    BlockType::Let
                    | BlockType::Val
                    | BlockType::UnfoldLet
                    | BlockType::InlineLet => {
                        // Functions/values must start with lowercase in F*.
                        // Both snake_case and camelCase are accepted.
                        if starts_with_uppercase(check_name) {
                            let suggested = to_snake_case(check_name);
                            diagnostics.push(Diagnostic {
                                rule: RuleCode::FST006,
                                severity: DiagnosticSeverity::Info,
                                file: file.clone(),
                                range: Range::point(block.start_line, 1),
                                message: format!(
                                    "Function/value `{}` should start with lowercase. \
                                     PascalCase is reserved for constructors/modules. \
                                     Suggested: `{}`",
                                    name, suggested
                                ),
                                fix: None,
                            });
                        }
                    }

                    BlockType::Effect => {
                        // Effects must start with uppercase (CamelCase) in F*.
                        if !starts_with_uppercase(check_name) {
                            diagnostics.push(Diagnostic {
                                rule: RuleCode::FST006,
                                severity: DiagnosticSeverity::Info,
                                file: file.clone(),
                                range: Range::point(block.start_line, 1),
                                message: format!(
                                    "Effect `{}` should use CamelCase (start with uppercase)",
                                    name
                                ),
                                fix: None,
                            });
                        }
                    }

                    // Skip other block types (Module, Open, Friend, etc.)
                    _ => {}
                }
            }
        }

        diagnostics
    }
}

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

    #[test]
    fn test_is_lowercase_start() {
        // snake_case: valid
        assert!(is_lowercase_start("foo"));
        assert!(is_lowercase_start("foo_bar"));
        assert!(is_lowercase_start("foo_bar_baz"));
        assert!(is_lowercase_start("_internal"));
        assert!(is_lowercase_start("int_t"));
        assert!(is_lowercase_start("nat"));

        // camelCase: also valid in F*
        assert!(is_lowercase_start("fooBar"));
        assert!(is_lowercase_start("loadState"));
        assert!(is_lowercase_start("createL"));
        assert!(is_lowercase_start("mapT"));
        assert!(is_lowercase_start("storeState_inner"));
        assert!(is_lowercase_start("ivTable_S"));
        assert!(is_lowercase_start("modBits_t"));

        // PascalCase: invalid for types/values
        assert!(!is_lowercase_start("Foo"));
        assert!(!is_lowercase_start("FooBar"));
        assert!(!is_lowercase_start("FOO_BAR"));
    }

    #[test]
    fn test_starts_with_uppercase() {
        assert!(starts_with_uppercase("Foo"));
        assert!(starts_with_uppercase("FooBar"));
        assert!(starts_with_uppercase("Tot"));
        assert!(starts_with_uppercase("GTot"));
        assert!(starts_with_uppercase("FOO_BAR"));

        assert!(!starts_with_uppercase("foo"));
        assert!(!starts_with_uppercase("fooBar"));
        assert!(!starts_with_uppercase("_foo"));
    }

    #[test]
    fn test_is_camel_case() {
        assert!(is_camel_case("Foo"));
        assert!(is_camel_case("FooBar"));
        assert!(is_camel_case("Tot"));
        assert!(is_camel_case("GTot"));
        assert!(is_camel_case("Lemma"));

        assert!(!is_camel_case("foo"));
        assert!(!is_camel_case("foo_bar"));
        assert!(!is_camel_case("fooBar"));
    }

    #[test]
    fn test_to_snake_case() {
        assert_eq!(to_snake_case("BadType"), "bad_type");
        assert_eq!(to_snake_case("FooBar"), "foo_bar");
        assert_eq!(to_snake_case("foo"), "foo");
        assert_eq!(to_snake_case("XMLParser"), "xml_parser");
    }

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

type BadType = int
type good_type = int
"#;
        let file = PathBuf::from("test.fst");
        let diagnostics = rule.check(&file, content);

        // Should flag BadType (PascalCase) but not good_type
        assert_eq!(diagnostics.len(), 1);
        assert!(diagnostics[0].message.contains("BadType"));
        assert!(diagnostics[0].message.contains("lowercase"));
    }

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

type inttype = int
type range_t = int
type secrecy_level = int
"#;
        let file = PathBuf::from("test.fst");
        let diagnostics = rule.check(&file, content);

        // All snake_case types are fine
        assert!(diagnostics.is_empty());
    }

    #[test]
    fn test_naming_rule_function_camelcase_accepted() {
        // camelCase function names are common in F* (loadState, createL, mapT, etc.)
        let rule = NamingRule::new();
        let content = r#"module Test

val loadState : int -> int
let loadState x = x

val createL : int -> int
let createL x = x

val storeState_inner : int -> int
let storeState_inner x = x

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

        // None should be flagged: camelCase and snake_case are both valid
        assert!(
            diagnostics.is_empty(),
            "Expected no diagnostics for camelCase functions, got: {:?}",
            diagnostics.iter().map(|d| &d.message).collect::<Vec<_>>()
        );
    }

    #[test]
    fn test_naming_rule_function_pascal_case_flagged() {
        // PascalCase (starts with uppercase) is wrong for functions
        let rule = NamingRule::new();
        let content = r#"module Test

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

        // Should flag BadFunc (PascalCase) for both val and let
        assert_eq!(diagnostics.len(), 2);
        assert!(diagnostics[0].message.contains("BadFunc"));
        assert!(diagnostics[0].message.contains("lowercase"));
    }

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

effect bad_effect = Tot
effect GoodEffect = Tot
"#;
        let file = PathBuf::from("test.fst");
        let diagnostics = rule.check(&file, content);

        // Should flag bad_effect but not GoodEffect
        assert_eq!(diagnostics.len(), 1);
        assert!(diagnostics[0].message.contains("bad_effect"));
        assert!(diagnostics[0].message.contains("CamelCase"));
    }

    #[test]
    fn test_naming_rule_underscore_prefix() {
        let rule = NamingRule::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);

        // Should not flag _internal (starts with underscore)
        assert!(diagnostics.is_empty());
    }

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

val foo' : int -> int
let foo' x = x

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

        // Primed names with valid bases should not be flagged
        assert!(
            diagnostics.is_empty(),
            "Expected no diagnostics for primed names, got: {:?}",
            diagnostics.iter().map(|d| &d.message).collect::<Vec<_>>()
        );
    }

    #[test]
    fn test_naming_rule_hacl_star_patterns() {
        // Real patterns from hacl-star that MUST NOT be flagged
        let rule = NamingRule::new();
        let content = r#"module Test

val sigmaTable : int -> int
let sigmaTable x = x

val ivTable_S : int -> int
let ivTable_S x = x

val rTable_B : int -> int
let rTable_B x = x

val msgHash2 : int -> int
let msgHash2 x = x

val modBits_t : int -> int
let modBits_t x = x

inline_for_extraction let fillT x = x

unfold let createL x = x
"#;
        let file = PathBuf::from("test.fst");
        let diagnostics = rule.check(&file, content);

        assert!(
            diagnostics.is_empty(),
            "Expected no diagnostics for hacl-star patterns, got: {:?}",
            diagnostics.iter().map(|d| &d.message).collect::<Vec<_>>()
        );
    }
}