logicaffeine_language/
symbol_dict.rs

1//! Symbol Dictionary Extraction
2//!
3//! Extracts logical symbols from FOL strings for display in a symbol dictionary.
4//! Groups symbols by kind and provides descriptions.
5
6use std::collections::HashSet;
7
8/// Categories of logical symbols
9#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
10pub enum SymbolKind {
11    Quantifier,
12    Connective,
13    Variable,
14    Predicate,
15    Constant,
16    Modal,
17    Identity,
18    Punctuation,
19    Temporal,
20}
21
22impl SymbolKind {
23    pub fn label(&self) -> &'static str {
24        match self {
25            SymbolKind::Quantifier => "Quantifier",
26            SymbolKind::Connective => "Connective",
27            SymbolKind::Variable => "Variable",
28            SymbolKind::Predicate => "Predicate",
29            SymbolKind::Constant => "Constant",
30            SymbolKind::Modal => "Modal",
31            SymbolKind::Identity => "Identity",
32            SymbolKind::Punctuation => "Punctuation",
33            SymbolKind::Temporal => "Temporal",
34        }
35    }
36}
37
38/// A single symbol entry in the dictionary
39#[derive(Debug, Clone, PartialEq, Eq, Hash)]
40pub struct SymbolEntry {
41    pub symbol: String,
42    pub kind: SymbolKind,
43    pub description: String,
44}
45
46/// Extract symbols from a FOL logic string
47pub fn extract_symbols(logic: &str) -> Vec<SymbolEntry> {
48    let mut entries = Vec::new();
49    let mut seen: HashSet<String> = HashSet::new();
50
51    // Quantifiers
52    if logic.contains("∀") && seen.insert("∀".to_string()) {
53        entries.push(SymbolEntry {
54            symbol: "∀".to_string(),
55            kind: SymbolKind::Quantifier,
56            description: "Universal quantifier: \"for all\"".to_string(),
57        });
58    }
59    if logic.contains("∃") && seen.insert("∃".to_string()) {
60        entries.push(SymbolEntry {
61            symbol: "∃".to_string(),
62            kind: SymbolKind::Quantifier,
63            description: "Existential quantifier: \"there exists\"".to_string(),
64        });
65    }
66    if logic.contains("∃!") && seen.insert("∃!".to_string()) {
67        entries.push(SymbolEntry {
68            symbol: "∃!".to_string(),
69            kind: SymbolKind::Quantifier,
70            description: "Unique existence: \"there exists exactly one\"".to_string(),
71        });
72    }
73    if logic.contains("MOST") && seen.insert("MOST".to_string()) {
74        entries.push(SymbolEntry {
75            symbol: "MOST".to_string(),
76            kind: SymbolKind::Quantifier,
77            description: "Generalized quantifier: \"most\"".to_string(),
78        });
79    }
80    if logic.contains("FEW") && seen.insert("FEW".to_string()) {
81        entries.push(SymbolEntry {
82            symbol: "FEW".to_string(),
83            kind: SymbolKind::Quantifier,
84            description: "Generalized quantifier: \"few\"".to_string(),
85        });
86    }
87
88    // Connectives
89    if logic.contains("∧") && seen.insert("∧".to_string()) {
90        entries.push(SymbolEntry {
91            symbol: "∧".to_string(),
92            kind: SymbolKind::Connective,
93            description: "Conjunction: \"and\"".to_string(),
94        });
95    }
96    if logic.contains("∨") && seen.insert("∨".to_string()) {
97        entries.push(SymbolEntry {
98            symbol: "∨".to_string(),
99            kind: SymbolKind::Connective,
100            description: "Disjunction: \"or\"".to_string(),
101        });
102    }
103    if logic.contains("→") && seen.insert("→".to_string()) {
104        entries.push(SymbolEntry {
105            symbol: "→".to_string(),
106            kind: SymbolKind::Connective,
107            description: "Implication: \"if...then\"".to_string(),
108        });
109    }
110    if logic.contains("↔") && seen.insert("↔".to_string()) {
111        entries.push(SymbolEntry {
112            symbol: "↔".to_string(),
113            kind: SymbolKind::Connective,
114            description: "Biconditional: \"if and only if\"".to_string(),
115        });
116    }
117    if logic.contains("¬") && seen.insert("¬".to_string()) {
118        entries.push(SymbolEntry {
119            symbol: "¬".to_string(),
120            kind: SymbolKind::Connective,
121            description: "Negation: \"not\"".to_string(),
122        });
123    }
124
125    // Modal operators
126    if logic.contains("□") && seen.insert("□".to_string()) {
127        entries.push(SymbolEntry {
128            symbol: "□".to_string(),
129            kind: SymbolKind::Modal,
130            description: "Necessity: \"it is necessary that\"".to_string(),
131        });
132    }
133    if logic.contains("◇") && seen.insert("◇".to_string()) {
134        entries.push(SymbolEntry {
135            symbol: "◇".to_string(),
136            kind: SymbolKind::Modal,
137            description: "Possibility: \"it is possible that\"".to_string(),
138        });
139    }
140    if logic.contains("O_") && seen.insert("O".to_string()) {
141        entries.push(SymbolEntry {
142            symbol: "O".to_string(),
143            kind: SymbolKind::Modal,
144            description: "Deontic obligation: \"it ought to be that\"".to_string(),
145        });
146    }
147
148    // Identity
149    if logic.contains(" = ") && seen.insert("=".to_string()) {
150        entries.push(SymbolEntry {
151            symbol: "=".to_string(),
152            kind: SymbolKind::Identity,
153            description: "Identity: \"is identical to\"".to_string(),
154        });
155    }
156
157    // Extract predicates (uppercase letters followed by parenthesis)
158    extract_predicates(logic, &mut entries, &mut seen);
159
160    // Extract variables (lowercase x, y, z, etc.)
161    extract_variables(logic, &mut entries, &mut seen);
162
163    // Extract constants (uppercase single letters not followed by parenthesis)
164    extract_constants(logic, &mut entries, &mut seen);
165
166    entries
167}
168
169fn extract_predicates(logic: &str, entries: &mut Vec<SymbolEntry>, seen: &mut HashSet<String>) {
170    // Match patterns like "Dog(", "Mortal(", "Loves("
171    let chars: Vec<char> = logic.chars().collect();
172    let mut i = 0;
173
174    while i < chars.len() {
175        if chars[i].is_ascii_uppercase() {
176            let start = i;
177            while i < chars.len() && (chars[i].is_ascii_alphanumeric() || chars[i] == '_') {
178                i += 1;
179            }
180            if i < chars.len() && chars[i] == '(' {
181                let predicate: String = chars[start..i].iter().collect();
182                if seen.insert(format!("pred_{}", predicate)) {
183                    entries.push(SymbolEntry {
184                        symbol: predicate.clone(),
185                        kind: SymbolKind::Predicate,
186                        description: format!("Predicate: {}", predicate),
187                    });
188                }
189            }
190        }
191        i += 1;
192    }
193}
194
195fn extract_variables(logic: &str, entries: &mut Vec<SymbolEntry>, seen: &mut HashSet<String>) {
196    // Variables are lowercase letters typically x, y, z, w
197    for var in ['x', 'y', 'z', 'w', 'e'] {
198        let var_str = var.to_string();
199        // Check if variable appears in context (not as part of a word)
200        if logic.contains(&format!("({})", var))
201            || logic.contains(&format!("({},", var))
202            || logic.contains(&format!(", {})", var))
203            || logic.contains(&format!("{}.", var))
204            || logic.contains(&format!(" {}", var))
205        {
206            if seen.insert(format!("var_{}", var)) {
207                entries.push(SymbolEntry {
208                    symbol: var_str,
209                    kind: SymbolKind::Variable,
210                    description: "Bound variable".to_string(),
211                });
212            }
213        }
214    }
215}
216
217fn extract_constants(logic: &str, entries: &mut Vec<SymbolEntry>, seen: &mut HashSet<String>) {
218    // Constants are uppercase letters like J (John), M (Mary), etc.
219    // But not predicates (followed by parenthesis)
220    let chars: Vec<char> = logic.chars().collect();
221    let mut i = 0;
222
223    while i < chars.len() {
224        if chars[i].is_ascii_uppercase() {
225            let start = i;
226            // Collect the full name (may have numbers like J2)
227            while i < chars.len() && (chars[i].is_ascii_alphanumeric()) {
228                i += 1;
229            }
230            // Check if NOT followed by parenthesis (would be predicate)
231            if i >= chars.len() || chars[i] != '(' {
232                let constant: String = chars[start..i].iter().collect();
233                // Skip very long names (likely predicates) and known quantifiers
234                if constant.len() <= 3
235                    && !["MOST", "FEW", "ALL", "THE"].contains(&constant.as_str())
236                    && seen.insert(format!("const_{}", constant))
237                {
238                    entries.push(SymbolEntry {
239                        symbol: constant.clone(),
240                        kind: SymbolKind::Constant,
241                        description: format!("Constant: {}", constant),
242                    });
243                }
244            }
245        }
246        i += 1;
247    }
248}
249
250/// Get symbols grouped by kind for display
251pub fn group_symbols_by_kind(entries: &[SymbolEntry]) -> Vec<(SymbolKind, Vec<&SymbolEntry>)> {
252    let kinds = [
253        SymbolKind::Quantifier,
254        SymbolKind::Connective,
255        SymbolKind::Modal,
256        SymbolKind::Identity,
257        SymbolKind::Predicate,
258        SymbolKind::Variable,
259        SymbolKind::Constant,
260    ];
261
262    kinds
263        .iter()
264        .filter_map(|&kind| {
265            let matching: Vec<_> = entries.iter().filter(|e| e.kind == kind).collect();
266            if matching.is_empty() {
267                None
268            } else {
269                Some((kind, matching))
270            }
271        })
272        .collect()
273}
274
275#[cfg(test)]
276mod tests {
277    use super::*;
278
279    #[test]
280    fn test_extract_quantifier_symbols() {
281        let logic = "∀x(Dog(x) → Mortal(x))";
282        let symbols = extract_symbols(logic);
283
284        let quantifiers: Vec<_> = symbols.iter().filter(|s| s.kind == SymbolKind::Quantifier).collect();
285        assert!(quantifiers.iter().any(|s| s.symbol == "∀"), "Should find universal quantifier");
286    }
287
288    #[test]
289    fn test_extract_existential() {
290        let logic = "∃x(Cat(x) ∧ Black(x))";
291        let symbols = extract_symbols(logic);
292
293        assert!(symbols.iter().any(|s| s.symbol == "∃"), "Should find existential quantifier");
294    }
295
296    #[test]
297    fn test_extract_connective_symbols() {
298        let logic = "∀x(Dog(x) → (Loyal(x) ∧ Friendly(x)))";
299        let symbols = extract_symbols(logic);
300
301        let connectives: Vec<_> = symbols.iter().filter(|s| s.kind == SymbolKind::Connective).collect();
302        assert!(connectives.iter().any(|s| s.symbol == "∧"), "Should find conjunction");
303        assert!(connectives.iter().any(|s| s.symbol == "→"), "Should find implication");
304    }
305
306    #[test]
307    fn test_extract_predicate_names() {
308        let logic = "∀x(Dog(x) → Mammal(x))";
309        let symbols = extract_symbols(logic);
310
311        let predicates: Vec<_> = symbols.iter().filter(|s| s.kind == SymbolKind::Predicate).collect();
312        assert!(predicates.iter().any(|s| s.symbol == "Dog"), "Should find Dog predicate");
313        assert!(predicates.iter().any(|s| s.symbol == "Mammal"), "Should find Mammal predicate");
314    }
315
316    #[test]
317    fn test_extract_variable_names() {
318        let logic = "∀x∃y(Loves(x, y))";
319        let symbols = extract_symbols(logic);
320
321        let variables: Vec<_> = symbols.iter().filter(|s| s.kind == SymbolKind::Variable).collect();
322        assert!(variables.iter().any(|s| s.symbol == "x"), "Should find variable x");
323        assert!(variables.iter().any(|s| s.symbol == "y"), "Should find variable y");
324    }
325
326    #[test]
327    fn test_no_duplicate_symbols() {
328        let logic = "∀x(Dog(x) → Dog(x))";
329        let symbols = extract_symbols(logic);
330
331        let dog_count = symbols.iter().filter(|s| s.symbol == "Dog").count();
332        assert_eq!(dog_count, 1, "Should not have duplicate predicates");
333    }
334
335    #[test]
336    fn test_symbol_has_description() {
337        let logic = "∀x(P(x))";
338        let symbols = extract_symbols(logic);
339
340        for symbol in &symbols {
341            assert!(!symbol.description.is_empty(), "Every symbol should have a description");
342        }
343    }
344
345    #[test]
346    fn test_modal_symbols() {
347        let logic = "□(P(x)) ∧ ◇(Q(y))";
348        let symbols = extract_symbols(logic);
349
350        assert!(symbols.iter().any(|s| s.symbol == "□"), "Should find necessity operator");
351        assert!(symbols.iter().any(|s| s.symbol == "◇"), "Should find possibility operator");
352    }
353
354    #[test]
355    fn test_group_symbols_by_kind() {
356        let logic = "∀x(Dog(x) → ∃y(Loves(x, y)))";
357        let symbols = extract_symbols(logic);
358        let grouped = group_symbols_by_kind(&symbols);
359
360        // Should have multiple groups
361        assert!(!grouped.is_empty(), "Should have grouped symbols");
362
363        // Check quantifiers group exists
364        assert!(grouped.iter().any(|(k, _)| *k == SymbolKind::Quantifier), "Should have quantifier group");
365    }
366}
logicaffeine_language/symbol_dict.rs

logicaffeine_language/
symbol_dict.rs
