logicaffeine_language/
debug.rs

1//! Debug display utilities for AST types with interner access.
2//!
3//! This module provides the [`DisplayWith`] trait for formatting AST types that
4//! contain interned symbols. Since symbols are just integer IDs, displaying them
5//! requires access to the interner to resolve the actual strings.
6//!
7//! Use the `.with(interner)` method to create a displayable wrapper:
8//!
9//! ```ignore
10//! use logicaffeine_language::debug::DisplayWith;
11//!
12//! let expr: LogicExpr = ...;
13//! println!("{}", expr.with(&interner));
14//! ```
15
16use std::fmt;
17
18use crate::ast::{
19    AspectOperator, LogicExpr, NounPhrase, QuantifierKind, TemporalOperator, VoiceOperator, Term,
20};
21use logicaffeine_base::{Interner, Symbol};
22use crate::token::TokenType;
23
24/// Trait for formatting types that require an interner for symbol resolution.
25pub trait DisplayWith {
26    fn fmt_with(&self, interner: &Interner, f: &mut fmt::Formatter<'_>) -> fmt::Result;
27
28    fn with<'a>(&'a self, interner: &'a Interner) -> WithInterner<'a, Self> {
29        WithInterner {
30            target: self,
31            interner,
32        }
33    }
34}
35
36pub struct WithInterner<'a, T: ?Sized> {
37    pub target: &'a T,
38    pub interner: &'a Interner,
39}
40
41impl<'a, T: DisplayWith> fmt::Display for WithInterner<'a, T> {
42    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
43        self.target.fmt_with(self.interner, f)
44    }
45}
46
47pub struct DebugWorld<'a, T: ?Sized> {
48    pub target: &'a T,
49    pub interner: &'a Interner,
50}
51
52impl<'a, T: DisplayWith> fmt::Debug for DebugWorld<'a, T> {
53    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
54        self.target.fmt_with(self.interner, f)
55    }
56}
57
58impl DisplayWith for Symbol {
59    fn fmt_with(&self, interner: &Interner, f: &mut fmt::Formatter<'_>) -> fmt::Result {
60        write!(f, "{}", interner.resolve(*self))
61    }
62}
63
64impl<'a> DisplayWith for Term<'a> {
65    fn fmt_with(&self, interner: &Interner, f: &mut fmt::Formatter<'_>) -> fmt::Result {
66        match self {
67            Term::Constant(s) => write!(f, "{}", interner.resolve(*s)),
68            Term::Variable(s) => write!(f, "{}", interner.resolve(*s)),
69            Term::Function(name, args) => {
70                write!(f, "{}(", interner.resolve(*name))?;
71                for (i, arg) in args.iter().enumerate() {
72                    if i > 0 {
73                        write!(f, ", ")?;
74                    }
75                    arg.fmt_with(interner, f)?;
76                }
77                write!(f, ")")
78            }
79            Term::Group(members) => {
80                write!(f, "[")?;
81                for (i, m) in members.iter().enumerate() {
82                    if i > 0 {
83                        write!(f, " ⊕ ")?;
84                    }
85                    m.fmt_with(interner, f)?;
86                }
87                write!(f, "]")
88            }
89            Term::Possessed { possessor, possessed } => {
90                possessor.fmt_with(interner, f)?;
91                write!(f, ".{}", interner.resolve(*possessed))
92            }
93            Term::Sigma(predicate) => {
94                write!(f, "σx.{}(x)", interner.resolve(*predicate))
95            }
96            Term::Intension(predicate) => {
97                write!(f, "^{}", interner.resolve(*predicate))
98            }
99            Term::Proposition(expr) => {
100                write!(f, "[{:?}]", expr)
101            }
102            Term::Value { kind, unit, dimension } => {
103                use crate::ast::NumberKind;
104                match kind {
105                    NumberKind::Real(r) => write!(f, "{}", r)?,
106                    NumberKind::Integer(i) => write!(f, "{}", i)?,
107                    NumberKind::Symbolic(s) => write!(f, "{}", interner.resolve(*s))?,
108                }
109                if let Some(u) = unit {
110                    write!(f, " {}", interner.resolve(*u))?;
111                }
112                if let Some(d) = dimension {
113                    write!(f, " [{:?}]", d)?;
114                }
115                Ok(())
116            }
117        }
118    }
119}
120
121impl<'a> DisplayWith for NounPhrase<'a> {
122    fn fmt_with(&self, interner: &Interner, f: &mut fmt::Formatter<'_>) -> fmt::Result {
123        if let Some(def) = &self.definiteness {
124            write!(f, "{:?} ", def)?;
125        }
126        for adj in self.adjectives {
127            write!(f, "{} ", interner.resolve(*adj))?;
128        }
129        write!(f, "{}", interner.resolve(self.noun))
130    }
131}
132
133impl<'a> DisplayWith for LogicExpr<'a> {
134    fn fmt_with(&self, interner: &Interner, f: &mut fmt::Formatter<'_>) -> fmt::Result {
135        match self {
136            LogicExpr::Predicate { name, args, .. } => {
137                write!(f, "{}(", interner.resolve(*name))?;
138                for (i, arg) in args.iter().enumerate() {
139                    if i > 0 {
140                        write!(f, ", ")?;
141                    }
142                    arg.fmt_with(interner, f)?;
143                }
144                write!(f, ")")
145            }
146            LogicExpr::Identity { left, right } => {
147                left.fmt_with(interner, f)?;
148                write!(f, " = ")?;
149                right.fmt_with(interner, f)
150            }
151            LogicExpr::Metaphor { tenor, vehicle } => {
152                write!(f, "Metaphor(")?;
153                tenor.fmt_with(interner, f)?;
154                write!(f, ", ")?;
155                vehicle.fmt_with(interner, f)?;
156                write!(f, ")")
157            }
158            LogicExpr::Quantifier { kind, variable, body, .. } => {
159                let q = match kind {
160                    QuantifierKind::Universal => "∀",
161                    QuantifierKind::Existential => "∃",
162                    QuantifierKind::Most => "MOST",
163                    QuantifierKind::Few => "FEW",
164                    QuantifierKind::Many => "MANY",
165                    QuantifierKind::Generic => "Gen",
166                    QuantifierKind::Cardinal(n) => return write!(f, "∃={}{}.{}", n, interner.resolve(*variable), body.with(interner)),
167                    QuantifierKind::AtLeast(n) => return write!(f, "∃≥{}{}.{}", n, interner.resolve(*variable), body.with(interner)),
168                    QuantifierKind::AtMost(n) => return write!(f, "∃≤{}{}.{}", n, interner.resolve(*variable), body.with(interner)),
169                };
170                write!(f, "{}{}.{}", q, interner.resolve(*variable), body.with(interner))
171            }
172            LogicExpr::Categorical(data) => {
173                let q = match &data.quantifier {
174                    TokenType::All => "All",
175                    TokenType::Some => "Some",
176                    TokenType::No => "No",
177                    _ => "?",
178                };
179                let cop = if data.copula_negative { "are not" } else { "are" };
180                write!(f, "{} {} {} {}", q, data.subject.with(interner), cop, data.predicate.with(interner))
181            }
182            LogicExpr::Relation(data) => {
183                write!(f, "{}({}, {})", interner.resolve(data.verb), data.subject.with(interner), data.object.with(interner))
184            }
185            LogicExpr::Modal { vector, operand } => {
186                let op = match (vector.domain, vector.force >= 0.5) {
187                    (crate::ast::ModalDomain::Alethic, true) => "□",
188                    (crate::ast::ModalDomain::Alethic, false) => "◇",
189                    (crate::ast::ModalDomain::Deontic, true) => "O",
190                    (crate::ast::ModalDomain::Deontic, false) => "P",
191                };
192                write!(f, "{}({})", op, operand.with(interner))
193            }
194            LogicExpr::Temporal { operator, body } => {
195                let op = match operator {
196                    TemporalOperator::Past => "P",
197                    TemporalOperator::Future => "F",
198                };
199                write!(f, "{}({})", op, body.with(interner))
200            }
201            LogicExpr::Aspectual { operator, body } => {
202                let op = match operator {
203                    AspectOperator::Progressive => "PROG",
204                    AspectOperator::Perfect => "PERF",
205                    AspectOperator::Habitual => "HAB",
206                    AspectOperator::Iterative => "ITER",
207                };
208                write!(f, "{}({})", op, body.with(interner))
209            }
210            LogicExpr::Voice { operator, body } => {
211                let op = match operator {
212                    VoiceOperator::Passive => "PASS",
213                };
214                write!(f, "{}({})", op, body.with(interner))
215            }
216            LogicExpr::BinaryOp { left, op, right } => {
217                let sym = match op {
218                    TokenType::And => "∧",
219                    TokenType::Or => "∨",
220                    TokenType::If => "→",
221                    TokenType::Iff => "↔",
222                    _ => "?",
223                };
224                write!(f, "({} {} {})", left.with(interner), sym, right.with(interner))
225            }
226            LogicExpr::UnaryOp { op, operand } => {
227                let sym = match op {
228                    TokenType::Not => "¬",
229                    _ => "?",
230                };
231                write!(f, "{}({})", sym, operand.with(interner))
232            }
233            LogicExpr::Question { wh_variable, body } => {
234                write!(f, "?{}.{}", interner.resolve(*wh_variable), body.with(interner))
235            }
236            LogicExpr::YesNoQuestion { body } => {
237                write!(f, "?{}", body.with(interner))
238            }
239            LogicExpr::Atom(s) => write!(f, "{}", interner.resolve(*s)),
240            LogicExpr::Lambda { variable, body } => {
241                write!(f, "λ{}.{}", interner.resolve(*variable), body.with(interner))
242            }
243            LogicExpr::App { function, argument } => {
244                write!(f, "({})({})", function.with(interner), argument.with(interner))
245            }
246            LogicExpr::Intensional { operator, content } => {
247                write!(f, "{}({})", interner.resolve(*operator), content.with(interner))
248            }
249            LogicExpr::Event { predicate, adverbs } => {
250                predicate.fmt_with(interner, f)?;
251                for adv in *adverbs {
252                    write!(f, "[{}]", interner.resolve(*adv))?;
253                }
254                Ok(())
255            }
256            LogicExpr::NeoEvent(data) => {
257                write!(f, "∃{}({}({})", interner.resolve(data.event_var), interner.resolve(data.verb), interner.resolve(data.event_var))?;
258                for (role, term) in data.roles.iter() {
259                    write!(f, " ∧ {:?}({}, {})", role, interner.resolve(data.event_var), term.with(interner))?;
260                }
261                for mod_sym in data.modifiers.iter() {
262                    write!(f, " ∧ {}({})", interner.resolve(*mod_sym), interner.resolve(data.event_var))?;
263                }
264                write!(f, ")")
265            }
266            LogicExpr::Imperative { action } => {
267                write!(f, "!({})", action.with(interner))
268            }
269            LogicExpr::SpeechAct { performer, act_type, content } => {
270                write!(f, "{}:{}({})", interner.resolve(*performer), interner.resolve(*act_type), content.with(interner))
271            }
272            LogicExpr::Counterfactual { antecedent, consequent } => {
273                write!(f, "({} □→ {})", antecedent.with(interner), consequent.with(interner))
274            }
275            LogicExpr::Causal { effect, cause } => {
276                write!(f, "Cause({}, {})", cause.with(interner), effect.with(interner))
277            }
278            LogicExpr::Comparative { adjective, subject, object, difference } => {
279                if let Some(diff) = difference {
280                    write!(f, "{}({}, {}, by: {})", interner.resolve(*adjective), subject.with(interner), object.with(interner), diff.with(interner))
281                } else {
282                    write!(f, "{}({}, {})", interner.resolve(*adjective), subject.with(interner), object.with(interner))
283                }
284            }
285            LogicExpr::Superlative { adjective, subject, domain } => {
286                write!(f, "MOST-{}({}, {})", interner.resolve(*adjective), subject.with(interner), interner.resolve(*domain))
287            }
288            LogicExpr::Scopal { operator, body } => {
289                write!(f, "{}({})", interner.resolve(*operator), body.with(interner))
290            }
291            LogicExpr::Control { verb, subject, object, infinitive } => {
292                write!(f, "{}(", interner.resolve(*verb))?;
293                subject.fmt_with(interner, f)?;
294                if let Some(obj) = object {
295                    write!(f, ", ")?;
296                    obj.fmt_with(interner, f)?;
297                }
298                write!(f, ", {})", infinitive.with(interner))
299            }
300            LogicExpr::Presupposition { assertion, presupposition } => {
301                write!(f, "[{} | {}]", assertion.with(interner), presupposition.with(interner))
302            }
303            LogicExpr::Focus { kind, focused, scope } => {
304                let k = match kind {
305                    crate::token::FocusKind::Only => "ONLY",
306                    crate::token::FocusKind::Even => "EVEN",
307                    crate::token::FocusKind::Just => "JUST",
308                };
309                write!(f, "{}[", k)?;
310                focused.fmt_with(interner, f)?;
311                write!(f, "]({})", scope.with(interner))
312            }
313            LogicExpr::TemporalAnchor { anchor, body } => {
314                write!(f, "@{}({})", interner.resolve(*anchor), body.with(interner))
315            }
316            LogicExpr::Distributive { predicate } => {
317                write!(f, "*")?;
318                predicate.fmt_with(interner, f)
319            }
320            LogicExpr::GroupQuantifier { group_var, count, member_var, restriction, body } => {
321                write!(
322                    f,
323                    "∃{}(Group({}) ∧ Count({}, {}) ∧ ∀{}(Member({}, {}) → ",
324                    interner.resolve(*group_var),
325                    interner.resolve(*group_var),
326                    interner.resolve(*group_var),
327                    count,
328                    interner.resolve(*member_var),
329                    interner.resolve(*member_var),
330                    interner.resolve(*group_var)
331                )?;
332                restriction.fmt_with(interner, f)?;
333                write!(f, ") ∧ ")?;
334                body.fmt_with(interner, f)?;
335                write!(f, ")")
336            }
337        }
338    }
339}
340
341#[cfg(test)]
342mod tests {
343    use super::*;
344    use logicaffeine_base::Arena;
345
346    #[test]
347    fn symbol_display_with_interner() {
348        let mut interner = Interner::new();
349        let sym = interner.intern("Socrates");
350        assert_eq!(sym.with(&interner).to_string(), "Socrates");
351    }
352
353    #[test]
354    fn symbol_empty_displays_empty() {
355        let interner = Interner::new();
356        assert_eq!(Symbol::EMPTY.with(&interner).to_string(), "");
357    }
358
359    #[test]
360    fn term_constant_display() {
361        let mut interner = Interner::new();
362        let sym = interner.intern("John");
363        let term = Term::Constant(sym);
364        assert_eq!(term.with(&interner).to_string(), "John");
365    }
366
367    #[test]
368    fn term_variable_display() {
369        let mut interner = Interner::new();
370        let x = interner.intern("x");
371        let term = Term::Variable(x);
372        assert_eq!(term.with(&interner).to_string(), "x");
373    }
374
375    #[test]
376    fn term_function_display() {
377        let mut interner = Interner::new();
378        let term_arena: Arena<Term> = Arena::new();
379        let f = interner.intern("father");
380        let j = interner.intern("John");
381        let term = Term::Function(f, term_arena.alloc_slice([Term::Constant(j)]));
382        assert_eq!(term.with(&interner).to_string(), "father(John)");
383    }
384
385    #[test]
386    fn term_group_display() {
387        let mut interner = Interner::new();
388        let term_arena: Arena<Term> = Arena::new();
389        let j = interner.intern("John");
390        let m = interner.intern("Mary");
391        let term = Term::Group(term_arena.alloc_slice([Term::Constant(j), Term::Constant(m)]));
392        assert_eq!(term.with(&interner).to_string(), "[John ⊕ Mary]");
393    }
394
395    #[test]
396    fn term_possessed_display() {
397        let mut interner = Interner::new();
398        let term_arena: Arena<Term> = Arena::new();
399        let j = interner.intern("John");
400        let dog = interner.intern("dog");
401        let term = Term::Possessed {
402            possessor: term_arena.alloc(Term::Constant(j)),
403            possessed: dog,
404        };
405        assert_eq!(term.with(&interner).to_string(), "John.dog");
406    }
407
408    #[test]
409    fn expr_predicate_display() {
410        let mut interner = Interner::new();
411        let term_arena: Arena<Term> = Arena::new();
412        let mortal = interner.intern("Mortal");
413        let x = interner.intern("x");
414        let expr = LogicExpr::Predicate {
415            name: mortal,
416            args: term_arena.alloc_slice([Term::Variable(x)]),
417            world: None,
418        };
419        assert_eq!(expr.with(&interner).to_string(), "Mortal(x)");
420    }
421
422    #[test]
423    fn expr_quantifier_display() {
424        let mut interner = Interner::new();
425        let expr_arena: Arena<LogicExpr> = Arena::new();
426        let term_arena: Arena<Term> = Arena::new();
427        let x = interner.intern("x");
428        let mortal = interner.intern("Mortal");
429        let body = expr_arena.alloc(LogicExpr::Predicate {
430            name: mortal,
431            args: term_arena.alloc_slice([Term::Variable(x)]),
432            world: None,
433        });
434        let expr = LogicExpr::Quantifier {
435            kind: QuantifierKind::Universal,
436            variable: x,
437            body,
438            island_id: 0,
439        };
440        assert_eq!(expr.with(&interner).to_string(), "∀x.Mortal(x)");
441    }
442
443    #[test]
444    fn expr_atom_display() {
445        let mut interner = Interner::new();
446        let p = interner.intern("P");
447        let expr = LogicExpr::Atom(p);
448        assert_eq!(expr.with(&interner).to_string(), "P");
449    }
450
451    #[test]
452    fn expr_binary_op_display() {
453        let mut interner = Interner::new();
454        let expr_arena: Arena<LogicExpr> = Arena::new();
455        let p = interner.intern("P");
456        let q = interner.intern("Q");
457        let expr = LogicExpr::BinaryOp {
458            left: expr_arena.alloc(LogicExpr::Atom(p)),
459            op: TokenType::And,
460            right: expr_arena.alloc(LogicExpr::Atom(q)),
461        };
462        assert_eq!(expr.with(&interner).to_string(), "(P ∧ Q)");
463    }
464
465    #[test]
466    fn expr_lambda_display() {
467        let mut interner = Interner::new();
468        let expr_arena: Arena<LogicExpr> = Arena::new();
469        let x = interner.intern("x");
470        let p = interner.intern("P");
471        let expr = LogicExpr::Lambda {
472            variable: x,
473            body: expr_arena.alloc(LogicExpr::Atom(p)),
474        };
475        assert_eq!(expr.with(&interner).to_string(), "λx.P");
476    }
477
478    #[test]
479    fn debug_world_works_with_dbg_pattern() {
480        let mut interner = Interner::new();
481        let sym = interner.intern("test");
482        let term = Term::Constant(sym);
483        let debug_str = format!("{:?}", DebugWorld { target: &term, interner: &interner });
484        assert!(debug_str.contains("test"));
485    }
486
487    #[test]
488    fn expr_temporal_display() {
489        let mut interner = Interner::new();
490        let expr_arena: Arena<LogicExpr> = Arena::new();
491        let p = interner.intern("Run");
492        let expr = LogicExpr::Temporal {
493            operator: TemporalOperator::Past,
494            body: expr_arena.alloc(LogicExpr::Atom(p)),
495        };
496        assert_eq!(expr.with(&interner).to_string(), "P(Run)");
497    }
498
499    #[test]
500    fn expr_modal_display() {
501        let mut interner = Interner::new();
502        let expr_arena: Arena<LogicExpr> = Arena::new();
503        let p = interner.intern("Rain");
504        let expr = LogicExpr::Modal {
505            vector: crate::ast::ModalVector {
506                domain: crate::ast::ModalDomain::Alethic,
507                force: 1.0,
508                flavor: crate::ast::ModalFlavor::Root,
509            },
510            operand: expr_arena.alloc(LogicExpr::Atom(p)),
511        };
512        assert_eq!(expr.with(&interner).to_string(), "□(Rain)");
513    }
514}