1use 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
25pub 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}