normalize_languages/
agda.rs

1//! Agda language support.
2
3use crate::{ContainerBody, Import, Language, LanguageSymbols};
4use tree_sitter::Node;
5
6/// Agda language support.
7pub struct Agda;
8
9impl Language for Agda {
10    fn name(&self) -> &'static str {
11        "Agda"
12    }
13    fn extensions(&self) -> &'static [&'static str] {
14        &["agda"]
15    }
16    fn grammar_name(&self) -> &'static str {
17        "agda"
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        match node.kind() {
26            "import" | "open" => {
27                let text = &content[node.byte_range()];
28                vec![Import {
29                    module: text.trim().to_string(),
30                    names: Vec::new(),
31                    alias: None,
32                    is_wildcard: node.kind() == "open",
33                    is_relative: false,
34                    line: node.start_position().row + 1,
35                }]
36            }
37            _ => Vec::new(),
38        }
39    }
40
41    fn format_import(&self, import: &Import, names: Option<&[&str]>) -> String {
42        // Agda: open import Module or import Module using (a; b; c)
43        let names_to_use: Vec<&str> = names
44            .map(|n| n.to_vec())
45            .unwrap_or_else(|| import.names.iter().map(|s| s.as_str()).collect());
46        if names_to_use.is_empty() {
47            format!("open import {}", import.module)
48        } else {
49            format!(
50                "import {} using ({})",
51                import.module,
52                names_to_use.join("; ")
53            )
54        }
55    }
56
57    fn is_test_symbol(&self, symbol: &crate::Symbol) -> bool {
58        let name = symbol.name.as_str();
59        match symbol.kind {
60            crate::SymbolKind::Function | crate::SymbolKind::Method => name.starts_with("test_"),
61            crate::SymbolKind::Module => name == "tests" || name == "test",
62            _ => false,
63        }
64    }
65
66    fn container_body<'a>(&self, node: &'a Node<'a>) -> Option<Node<'a>> {
67        // Agda has no dedicated body field; use the container node itself
68        Some(*node)
69    }
70
71    fn analyze_container_body(
72        &self,
73        body_node: &Node,
74        content: &str,
75        inner_indent: &str,
76    ) -> Option<ContainerBody> {
77        // Agda: module/record body comes after the `where` keyword
78        let end = body_node.end_byte();
79        let bytes = content.as_bytes();
80
81        let mut content_start = body_node.start_byte();
82        let mut c = body_node.walk();
83        for child in body_node.children(&mut c) {
84            if child.kind() == "where" {
85                content_start = child.end_byte();
86                if content_start < end && bytes[content_start] == b'\n' {
87                    content_start += 1;
88                }
89                break;
90            }
91        }
92
93        let is_empty = content[content_start..end].trim().is_empty();
94        Some(ContainerBody {
95            content_start,
96            content_end: end,
97            inner_indent: inner_indent.to_string(),
98            is_empty,
99        })
100    }
101
102    fn node_name<'a>(&self, node: &Node, content: &'a str) -> Option<&'a str> {
103        if let Some(name_node) = node.child_by_field_name("name") {
104            return Some(&content[name_node.byte_range()]);
105        }
106        let mut cursor = node.walk();
107        for child in node.children(&mut cursor) {
108            if child.kind() == "id" || child.kind() == "qid" {
109                return Some(&content[child.byte_range()]);
110            }
111        }
112        None
113    }
114}
115
116impl LanguageSymbols for Agda {}
117
118#[cfg(test)]
119mod tests {
120    use super::*;
121    use crate::validate_unused_kinds_audit;
122
123    #[test]
124    fn unused_node_kinds_audit() {
125        #[rustfmt::skip]
126        let documented_unused: &[&str] = &[
127            // Function and lambda definitions
128            "catchall_pragma", "forall", "lambda",
129            "lambda_clause_absurd", "type_signature",
130            // Module-related
131            "import_directive", "module_application", "module_assignment", "module_macro",
132            // Record definitions
133            "record_constructor", "record_constructor_instance", "record_declarations_block",
134            // Bindings
135            "typed_binding", "untyped_binding", "with_expressions",
136            // control flow — not extracted as symbols
137            "lambda_clause",
138            "import",
139        ];
140        validate_unused_kinds_audit(&Agda, documented_unused)
141            .expect("Agda unused node kinds audit failed");
142    }
143}
normalize_languages/agda.rs

normalize_languages/
agda.rs
