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