Skip to main content

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