normalize_languages/
tlaplus.rs

1//! TLA+ specification language support.
2
3use crate::{ContainerBody, Import, Language, LanguageSymbols};
4use tree_sitter::Node;
5
6/// TLA+ language support.
7pub struct TlaPlus;
8
9impl Language for TlaPlus {
10    fn name(&self) -> &'static str {
11        "TLA+"
12    }
13    fn extensions(&self) -> &'static [&'static str] {
14        &["tla"]
15    }
16    fn grammar_name(&self) -> &'static str {
17        "tlaplus"
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() != "extends" {
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        // TLA+: EXTENDS ModuleName
42        format!("EXTENDS {}", import.module)
43    }
44
45    fn is_test_symbol(&self, symbol: &crate::Symbol) -> bool {
46        let name = symbol.name.as_str();
47        match symbol.kind {
48            crate::SymbolKind::Function | crate::SymbolKind::Method => name.starts_with("test_"),
49            crate::SymbolKind::Module => name == "tests" || name == "test",
50            _ => false,
51        }
52    }
53
54    fn container_body<'a>(&self, node: &'a Node<'a>) -> Option<Node<'a>> {
55        // TLA+ module has no dedicated body field; use the module node itself
56        Some(*node)
57    }
58
59    fn analyze_container_body(
60        &self,
61        body_node: &Node,
62        content: &str,
63        inner_indent: &str,
64    ) -> Option<ContainerBody> {
65        // TLA+ module: ---- MODULE Foo ----\n...body...\n====
66        // Skip the first line (---- MODULE Foo ----), strip ==== from the tail.
67        let start = body_node.start_byte();
68        let end = body_node.end_byte();
69        let bytes = content.as_bytes();
70
71        let mut content_start = start;
72        while content_start < end && bytes[content_start] != b'\n' {
73            content_start += 1;
74        }
75        if content_start < end {
76            content_start += 1; // skip \n
77        }
78
79        let mut content_end = end;
80        if end >= 4 && bytes.get(end - 4..end) == Some(b"====") {
81            content_end = end - 4;
82            while content_end > content_start
83                && matches!(bytes[content_end - 1], b' ' | b'\t' | b'\n')
84            {
85                content_end -= 1;
86            }
87        }
88
89        let is_empty = content[content_start..content_end].trim().is_empty();
90        Some(ContainerBody {
91            content_start,
92            content_end,
93            inner_indent: inner_indent.to_string(),
94            is_empty,
95        })
96    }
97}
98
99impl LanguageSymbols for TlaPlus {}
100
101#[cfg(test)]
102mod tests {
103    use super::*;
104    use crate::validate_unused_kinds_audit;
105
106    #[test]
107    fn unused_node_kinds_audit() {
108        #[rustfmt::skip]
109        let documented_unused: &[&str] = &[
110            // Declarations and definitions
111            "constant_declaration", "variable_declaration", "operator_declaration",
112            "local_definition", "function_definition", "module_definition",
113            "recursive_declaration", "operator_args",
114            // Proof-related
115            "definition_proof_step", "case_proof_step", "use_body", "use_body_def",
116            "use_body_expr", "statement_level",
117            // Quantifiers
118            "forall", "quantifier_bound", "tuple_of_identifiers",
119            "unbounded_quantification", "bounded_quantification", "temporal_forall",
120            // Case expressions
121            "case_arm", "case_arrow", "case_box",
122            // Function-related
123            "function_literal", "function_evaluation", "set_of_functions",
124            // Except
125            "except", "except_update", "except_update_specifier",
126            "except_update_fn_appl", "except_update_record_field",
127            // PlusCal
128            "pcal_algorithm_body", "pcal_definitions", "pcal_if", "pcal_end_if",
129            "pcal_while", "pcal_end_while", "pcal_with", "pcal_end_with",
130            "pcal_await", "pcal_return",
131            // Identifiers and references
132            "identifier", "identifier_ref", "module_ref",
133            // Comments
134            "block_comment", "block_comment_text",
135            // Other
136            "lambda", "iff", "format", "subexpression",
137            // Control flow — not definition constructs
138            "case", "if_then_else",
139            // control flow — not extracted as symbols
140
141        ];
142        validate_unused_kinds_audit(&TlaPlus, documented_unused)
143            .expect("TLA+ unused node kinds audit failed");
144    }
145}
normalize_languages/tlaplus.rs

normalize_languages/
tlaplus.rs
