normalize_languages/
lean.rs

1//! Lean language support.
2
3use crate::{ContainerBody, Import, Language, LanguageSymbols, Visibility};
4use tree_sitter::Node;
5
6/// Lean language support.
7pub struct Lean;
8
9impl Language for Lean {
10    fn name(&self) -> &'static str {
11        "Lean"
12    }
13    fn extensions(&self) -> &'static [&'static str] {
14        &["lean"]
15    }
16    fn grammar_name(&self) -> &'static str {
17        "lean"
18    }
19
20    fn as_symbols(&self) -> Option<&dyn LanguageSymbols> {
21        Some(self)
22    }
23
24    fn extract_imports(&self, node: &Node, content: &str) -> Vec<Import> {
25        if node.kind() != "import" {
26            return Vec::new();
27        }
28
29        let text = &content[node.byte_range()];
30        vec![Import {
31            module: text.trim().to_string(),
32            names: Vec::new(),
33            alias: None,
34            is_wildcard: false,
35            is_relative: false,
36            line: node.start_position().row + 1,
37        }]
38    }
39
40    fn format_import(&self, import: &Import, names: Option<&[&str]>) -> String {
41        // Lean: import Module or open Module (a, b, c)
42        let names_to_use: Vec<&str> = names
43            .map(|n| n.to_vec())
44            .unwrap_or_else(|| import.names.iter().map(|s| s.as_str()).collect());
45        if names_to_use.is_empty() {
46            format!("import {}", import.module)
47        } else {
48            format!("open {} ({})", import.module, names_to_use.join(", "))
49        }
50    }
51
52    fn get_visibility(&self, node: &Node, content: &str) -> Visibility {
53        let text = &content[node.byte_range()];
54        if text.contains("private") {
55            Visibility::Private
56        } else if text.contains("protected") {
57            Visibility::Protected
58        } else {
59            Visibility::Public
60        }
61    }
62
63    fn is_test_symbol(&self, symbol: &crate::Symbol) -> bool {
64        let name = symbol.name.as_str();
65        match symbol.kind {
66            crate::SymbolKind::Function | crate::SymbolKind::Method => name.starts_with("test_"),
67            crate::SymbolKind::Module => name == "tests" || name == "test",
68            _ => false,
69        }
70    }
71
72    fn container_body<'a>(&self, node: &'a Node<'a>) -> Option<Node<'a>> {
73        node.child_by_field_name("body")
74    }
75
76    fn analyze_container_body(
77        &self,
78        body_node: &Node,
79        content: &str,
80        inner_indent: &str,
81    ) -> Option<ContainerBody> {
82        crate::body::analyze_end_body(body_node, content, inner_indent)
83    }
84}
85
86impl LanguageSymbols for Lean {}
87
88#[cfg(test)]
89mod tests {
90    use super::*;
91    use crate::validate_unused_kinds_audit;
92
93    #[test]
94    fn unused_node_kinds_audit() {
95        #[rustfmt::skip]
96        let documented_unused: &[&str] = &[
97            // Expression nodes (not declarations)
98            "for_in", "binary_expression", "unary_expression",
99            "type_ascription", "forall", "subtype", "structure_instance",
100            "anonymous_constructor", "lift_method",
101            // Parts of declarations
102            "constructor", "declaration", "identifier",
103            // Module system
104            "module", "export",
105            // Control flow
106            "do_return",
107            // control flow — not extracted as symbols
108            "if_then_else",
109            "match_alt",
110            "match",
111            "import",
112        ];
113        validate_unused_kinds_audit(&Lean, documented_unused)
114            .expect("Lean unused node kinds audit failed");
115    }
116}
normalize_languages/lean.rs

normalize_languages/
lean.rs
