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
202                    | TemporalOperator::BoundedEventually(_) => "F",
203                    TemporalOperator::Next => "X",
204                };
205                write!(f, "{}({})", op, body.with(interner))
206            }
207            LogicExpr::Aspectual { operator, body } => {
208                let op = match operator {
209                    AspectOperator::Progressive => "PROG",
210                    AspectOperator::Perfect => "PERF",
211                    AspectOperator::Habitual => "HAB",
212                    AspectOperator::Iterative => "ITER",
213                };
214                write!(f, "{}({})", op, body.with(interner))
215            }
216            LogicExpr::Voice { operator, body } => {
217                let op = match operator {
218                    VoiceOperator::Passive => "PASS",
219                };
220                write!(f, "{}({})", op, body.with(interner))
221            }
222            LogicExpr::BinaryOp { left, op, right } => {
223                let sym = match op {
224                    TokenType::And => "∧",
225                    TokenType::Or => "∨",
226                    TokenType::If => "→",
227                    TokenType::Iff => "↔",
228                    _ => "?",
229                };
230                write!(f, "({} {} {})", left.with(interner), sym, right.with(interner))
231            }
232            LogicExpr::UnaryOp { op, operand } => {
233                let sym = match op {
234                    TokenType::Not => "¬",
235                    _ => "?",
236                };
237                write!(f, "{}({})", sym, operand.with(interner))
238            }
239            LogicExpr::Question { wh_variable, body } => {
240                write!(f, "?{}.{}", interner.resolve(*wh_variable), body.with(interner))
241            }
242            LogicExpr::YesNoQuestion { body } => {
243                write!(f, "?{}", body.with(interner))
244            }
245            LogicExpr::Atom(s) => write!(f, "{}", interner.resolve(*s)),
246            LogicExpr::Lambda { variable, body } => {
247                write!(f, "λ{}.{}", interner.resolve(*variable), body.with(interner))
248            }
249            LogicExpr::App { function, argument } => {
250                write!(f, "({})({})", function.with(interner), argument.with(interner))
251            }
252            LogicExpr::Intensional { operator, content } => {
253                write!(f, "{}({})", interner.resolve(*operator), content.with(interner))
254            }
255            LogicExpr::Event { predicate, adverbs } => {
256                predicate.fmt_with(interner, f)?;
257                for adv in *adverbs {
258                    write!(f, "[{}]", interner.resolve(*adv))?;
259                }
260                Ok(())
261            }
262            LogicExpr::NeoEvent(data) => {
263                write!(f, "∃{}({}({})", interner.resolve(data.event_var), interner.resolve(data.verb), interner.resolve(data.event_var))?;
264                for (role, term) in data.roles.iter() {
265                    write!(f, " ∧ {:?}({}, {})", role, interner.resolve(data.event_var), term.with(interner))?;
266                }
267                for mod_sym in data.modifiers.iter() {
268                    write!(f, " ∧ {}({})", interner.resolve(*mod_sym), interner.resolve(data.event_var))?;
269                }
270                write!(f, ")")
271            }
272            LogicExpr::Imperative { action } => {
273                write!(f, "!({})", action.with(interner))
274            }
275            LogicExpr::SpeechAct { performer, act_type, content } => {
276                write!(f, "{}:{}({})", interner.resolve(*performer), interner.resolve(*act_type), content.with(interner))
277            }
278            LogicExpr::Counterfactual { antecedent, consequent } => {
279                write!(f, "({} □→ {})", antecedent.with(interner), consequent.with(interner))
280            }
281            LogicExpr::Causal { effect, cause } => {
282                write!(f, "Cause({}, {})", cause.with(interner), effect.with(interner))
283            }
284            LogicExpr::Comparative { adjective, subject, object, difference } => {
285                if let Some(diff) = difference {
286                    write!(f, "{}({}, {}, by: {})", interner.resolve(*adjective), subject.with(interner), object.with(interner), diff.with(interner))
287                } else {
288                    write!(f, "{}({}, {})", interner.resolve(*adjective), subject.with(interner), object.with(interner))
289                }
290            }
291            LogicExpr::Superlative { adjective, subject, domain } => {
292                write!(f, "MOST-{}({}, {})", interner.resolve(*adjective), subject.with(interner), interner.resolve(*domain))
293            }
294            LogicExpr::Scopal { operator, body } => {
295                write!(f, "{}({})", interner.resolve(*operator), body.with(interner))
296            }
297            LogicExpr::Control { verb, subject, object, infinitive } => {
298                write!(f, "{}(", interner.resolve(*verb))?;
299                subject.fmt_with(interner, f)?;
300                if let Some(obj) = object {
301                    write!(f, ", ")?;
302                    obj.fmt_with(interner, f)?;
303                }
304                write!(f, ", {})", infinitive.with(interner))
305            }
306            LogicExpr::Presupposition { assertion, presupposition } => {
307                write!(f, "[{} | {}]", assertion.with(interner), presupposition.with(interner))
308            }
309            LogicExpr::Focus { kind, focused, scope } => {
310                let k = match kind {
311                    crate::token::FocusKind::Only => "ONLY",
312                    crate::token::FocusKind::Even => "EVEN",
313                    crate::token::FocusKind::Just => "JUST",
314                };
315                write!(f, "{}[", k)?;
316                focused.fmt_with(interner, f)?;
317                write!(f, "]({})", scope.with(interner))
318            }
319            LogicExpr::TemporalAnchor { anchor, body } => {
320                write!(f, "@{}({})", interner.resolve(*anchor), body.with(interner))
321            }
322            LogicExpr::Distributive { predicate } => {
323                write!(f, "*")?;
324                predicate.fmt_with(interner, f)
325            }
326            LogicExpr::GroupQuantifier { group_var, count, member_var, restriction, body } => {
327                write!(
328                    f,
329                    "∃{}(Group({}) ∧ Count({}, {}) ∧ ∀{}(Member({}, {}) → ",
330                    interner.resolve(*group_var),
331                    interner.resolve(*group_var),
332                    interner.resolve(*group_var),
333                    count,
334                    interner.resolve(*member_var),
335                    interner.resolve(*member_var),
336                    interner.resolve(*group_var)
337                )?;
338                restriction.fmt_with(interner, f)?;
339                write!(f, ") ∧ ")?;
340                body.fmt_with(interner, f)?;
341                write!(f, ")")
342            }
343            LogicExpr::TemporalBinary { operator, left, right } => {
344                let op = match operator {
345                    BinaryTemporalOp::Until => "U",
346                    BinaryTemporalOp::Release => "R",
347                    BinaryTemporalOp::WeakUntil => "W",
348                };
349                write!(f, "({} {} {})", left.with(interner), op, right.with(interner))
350            }
351        }
352    }
353}
354
355#[cfg(test)]
356mod tests {
357    use super::*;
358    use logicaffeine_base::Arena;
359
360    #[test]
361    fn symbol_display_with_interner() {
362        let mut interner = Interner::new();
363        let sym = interner.intern("Socrates");
364        assert_eq!(sym.with(&interner).to_string(), "Socrates");
365    }
366
367    #[test]
368    fn symbol_empty_displays_empty() {
369        let interner = Interner::new();
370        assert_eq!(Symbol::EMPTY.with(&interner).to_string(), "");
371    }
372
373    #[test]
374    fn term_constant_display() {
375        let mut interner = Interner::new();
376        let sym = interner.intern("John");
377        let term = Term::Constant(sym);
378        assert_eq!(term.with(&interner).to_string(), "John");
379    }
380
381    #[test]
382    fn term_variable_display() {
383        let mut interner = Interner::new();
384        let x = interner.intern("x");
385        let term = Term::Variable(x);
386        assert_eq!(term.with(&interner).to_string(), "x");
387    }
388
389    #[test]
390    fn term_function_display() {
391        let mut interner = Interner::new();
392        let term_arena: Arena<Term> = Arena::new();
393        let f = interner.intern("father");
394        let j = interner.intern("John");
395        let term = Term::Function(f, term_arena.alloc_slice([Term::Constant(j)]));
396        assert_eq!(term.with(&interner).to_string(), "father(John)");
397    }
398
399    #[test]
400    fn term_group_display() {
401        let mut interner = Interner::new();
402        let term_arena: Arena<Term> = Arena::new();
403        let j = interner.intern("John");
404        let m = interner.intern("Mary");
405        let term = Term::Group(term_arena.alloc_slice([Term::Constant(j), Term::Constant(m)]));
406        assert_eq!(term.with(&interner).to_string(), "[John ⊕ Mary]");
407    }
408
409    #[test]
410    fn term_possessed_display() {
411        let mut interner = Interner::new();
412        let term_arena: Arena<Term> = Arena::new();
413        let j = interner.intern("John");
414        let dog = interner.intern("dog");
415        let term = Term::Possessed {
416            possessor: term_arena.alloc(Term::Constant(j)),
417            possessed: dog,
418        };
419        assert_eq!(term.with(&interner).to_string(), "John.dog");
420    }
421
422    #[test]
423    fn expr_predicate_display() {
424        let mut interner = Interner::new();
425        let term_arena: Arena<Term> = Arena::new();
426        let mortal = interner.intern("Mortal");
427        let x = interner.intern("x");
428        let expr = LogicExpr::Predicate {
429            name: mortal,
430            args: term_arena.alloc_slice([Term::Variable(x)]),
431            world: None,
432        };
433        assert_eq!(expr.with(&interner).to_string(), "Mortal(x)");
434    }
435
436    #[test]
437    fn expr_quantifier_display() {
438        let mut interner = Interner::new();
439        let expr_arena: Arena<LogicExpr> = Arena::new();
440        let term_arena: Arena<Term> = Arena::new();
441        let x = interner.intern("x");
442        let mortal = interner.intern("Mortal");
443        let body = expr_arena.alloc(LogicExpr::Predicate {
444            name: mortal,
445            args: term_arena.alloc_slice([Term::Variable(x)]),
446            world: None,
447        });
448        let expr = LogicExpr::Quantifier {
449            kind: QuantifierKind::Universal,
450            variable: x,
451            body,
452            island_id: 0,
453        };
454        assert_eq!(expr.with(&interner).to_string(), "∀x.Mortal(x)");
455    }
456
457    #[test]
458    fn expr_atom_display() {
459        let mut interner = Interner::new();
460        let p = interner.intern("P");
461        let expr = LogicExpr::Atom(p);
462        assert_eq!(expr.with(&interner).to_string(), "P");
463    }
464
465    #[test]
466    fn expr_binary_op_display() {
467        let mut interner = Interner::new();
468        let expr_arena: Arena<LogicExpr> = Arena::new();
469        let p = interner.intern("P");
470        let q = interner.intern("Q");
471        let expr = LogicExpr::BinaryOp {
472            left: expr_arena.alloc(LogicExpr::Atom(p)),
473            op: TokenType::And,
474            right: expr_arena.alloc(LogicExpr::Atom(q)),
475        };
476        assert_eq!(expr.with(&interner).to_string(), "(P ∧ Q)");
477    }
478
479    #[test]
480    fn expr_lambda_display() {
481        let mut interner = Interner::new();
482        let expr_arena: Arena<LogicExpr> = Arena::new();
483        let x = interner.intern("x");
484        let p = interner.intern("P");
485        let expr = LogicExpr::Lambda {
486            variable: x,
487            body: expr_arena.alloc(LogicExpr::Atom(p)),
488        };
489        assert_eq!(expr.with(&interner).to_string(), "λx.P");
490    }
491
492    #[test]
493    fn debug_world_works_with_dbg_pattern() {
494        let mut interner = Interner::new();
495        let sym = interner.intern("test");
496        let term = Term::Constant(sym);
497        let debug_str = format!("{:?}", DebugWorld { target: &term, interner: &interner });
498        assert!(debug_str.contains("test"));
499    }
500
501    #[test]
502    fn expr_temporal_display() {
503        let mut interner = Interner::new();
504        let expr_arena: Arena<LogicExpr> = Arena::new();
505        let p = interner.intern("Run");
506        let expr = LogicExpr::Temporal {
507            operator: TemporalOperator::Past,
508            body: expr_arena.alloc(LogicExpr::Atom(p)),
509        };
510        assert_eq!(expr.with(&interner).to_string(), "P(Run)");
511    }
512
513    #[test]
514    fn expr_modal_display() {
515        let mut interner = Interner::new();
516        let expr_arena: Arena<LogicExpr> = Arena::new();
517        let p = interner.intern("Rain");
518        let expr = LogicExpr::Modal {
519            vector: crate::ast::ModalVector {
520                domain: crate::ast::ModalDomain::Alethic,
521                force: 1.0,
522                flavor: crate::ast::ModalFlavor::Root,
523            },
524            operand: expr_arena.alloc(LogicExpr::Atom(p)),
525        };
526        assert_eq!(expr.with(&interner).to_string(), "□(Rain)");
527    }
528}
logicaffeine_language/debug.rs

logicaffeine_language/
debug.rs
