tensorlogic_ir/
pretty_print.rs

1//! Human-readable pretty printing for TLExpr.
2//!
3//! Renders logical expressions using standard mathematical notation:
4//! `forall x in Person. exists y in Person. knows(x, y) -> friends(x, y)`
5//!
6//! Supports both Unicode and ASCII symbol sets, configurable indentation,
7//! maximum line width, and optional type annotations.
8
9use std::fmt::Write;
10
11use crate::{TLExpr, Term};
12
13/// Symbol set for rendering logical connectives.
14#[derive(Debug, Clone, PartialEq, Eq)]
15pub enum SymbolSet {
16    /// Unicode mathematical symbols: `\u{2200}` `\u{2203}` `\u{2227}` `\u{2228}` `\u{00ac}` `\u{2192}` `\u{2208}`
17    Unicode,
18    /// ASCII-only symbols: `forall` `exists` `&` `|` `!` `->` `in`
19    Ascii,
20}
21
22/// Configuration for pretty printing.
23#[derive(Debug, Clone)]
24pub struct PrettyConfig {
25    /// Symbol set to use for rendering
26    pub symbols: SymbolSet,
27    /// Number of spaces per indentation level
28    pub indent_width: usize,
29    /// Maximum line width before wrapping (advisory)
30    pub max_width: usize,
31    /// Whether to show type annotations on terms
32    pub show_types: bool,
33}
34
35impl Default for PrettyConfig {
36    fn default() -> Self {
37        Self {
38            symbols: SymbolSet::Unicode,
39            indent_width: 2,
40            max_width: 80,
41            show_types: false,
42        }
43    }
44}
45
46impl PrettyConfig {
47    /// Create a Unicode-symbol configuration.
48    pub fn unicode() -> Self {
49        Self::default()
50    }
51
52    /// Create an ASCII-only configuration.
53    pub fn ascii() -> Self {
54        Self {
55            symbols: SymbolSet::Ascii,
56            ..Self::default()
57        }
58    }
59
60    /// Set the indentation width.
61    pub fn with_indent(mut self, w: usize) -> Self {
62        self.indent_width = w;
63        self
64    }
65
66    /// Set the maximum line width.
67    pub fn with_max_width(mut self, w: usize) -> Self {
68        self.max_width = w;
69        self
70    }
71
72    /// Enable or disable type annotation display.
73    pub fn with_types(mut self, v: bool) -> Self {
74        self.show_types = v;
75        self
76    }
77
78    // ---- symbol helpers ----
79
80    fn sym_and(&self) -> &str {
81        match self.symbols {
82            SymbolSet::Unicode => "\u{2227}",
83            SymbolSet::Ascii => "&",
84        }
85    }
86
87    fn sym_or(&self) -> &str {
88        match self.symbols {
89            SymbolSet::Unicode => "\u{2228}",
90            SymbolSet::Ascii => "|",
91        }
92    }
93
94    fn sym_not(&self) -> &str {
95        match self.symbols {
96            SymbolSet::Unicode => "\u{00ac}",
97            SymbolSet::Ascii => "!",
98        }
99    }
100
101    fn sym_implies(&self) -> &str {
102        match self.symbols {
103            SymbolSet::Unicode => "\u{2192}",
104            SymbolSet::Ascii => "->",
105        }
106    }
107
108    fn sym_forall(&self) -> &str {
109        match self.symbols {
110            SymbolSet::Unicode => "\u{2200}",
111            SymbolSet::Ascii => "forall",
112        }
113    }
114
115    fn sym_exists(&self) -> &str {
116        match self.symbols {
117            SymbolSet::Unicode => "\u{2203}",
118            SymbolSet::Ascii => "exists",
119        }
120    }
121
122    fn sym_in(&self) -> &str {
123        match self.symbols {
124            SymbolSet::Unicode => "\u{2208}",
125            SymbolSet::Ascii => "in",
126        }
127    }
128
129    fn sym_box(&self) -> &str {
130        match self.symbols {
131            SymbolSet::Unicode => "\u{25a1}",
132            SymbolSet::Ascii => "[]",
133        }
134    }
135
136    fn sym_diamond(&self) -> &str {
137        match self.symbols {
138            SymbolSet::Unicode => "\u{25c7}",
139            SymbolSet::Ascii => "<>",
140        }
141    }
142
143    fn sym_lambda(&self) -> &str {
144        match self.symbols {
145            SymbolSet::Unicode => "\u{03bb}",
146            SymbolSet::Ascii => "\\",
147        }
148    }
149
150    fn sym_mu(&self) -> &str {
151        match self.symbols {
152            SymbolSet::Unicode => "\u{03bc}",
153            SymbolSet::Ascii => "mu",
154        }
155    }
156
157    fn sym_nu(&self) -> &str {
158        match self.symbols {
159            SymbolSet::Unicode => "\u{03bd}",
160            SymbolSet::Ascii => "nu",
161        }
162    }
163
164    fn sym_union(&self) -> &str {
165        match self.symbols {
166            SymbolSet::Unicode => "\u{222a}",
167            SymbolSet::Ascii => "U",
168        }
169    }
170
171    fn sym_intersection(&self) -> &str {
172        match self.symbols {
173            SymbolSet::Unicode => "\u{2229}",
174            SymbolSet::Ascii => "^",
175        }
176    }
177
178    fn sym_setminus(&self) -> &str {
179        match self.symbols {
180            SymbolSet::Unicode => "\\",
181            SymbolSet::Ascii => "\\",
182        }
183    }
184
185    fn sym_emptyset(&self) -> &str {
186        match self.symbols {
187            SymbolSet::Unicode => "\u{2205}",
188            SymbolSet::Ascii => "{}",
189        }
190    }
191
192    fn sym_element_of(&self) -> &str {
193        // re-use ∈ for set membership
194        self.sym_in()
195    }
196
197    fn sym_at(&self) -> &str {
198        "@"
199    }
200
201    fn sym_sigma(&self) -> &str {
202        match self.symbols {
203            SymbolSet::Unicode => "\u{03c3}",
204            SymbolSet::Ascii => "sigma",
205        }
206    }
207}
208
209// ---------------------------------------------------------------------------
210// Public API
211// ---------------------------------------------------------------------------
212
213/// Pretty-print a [`TLExpr`] to a string with the given configuration.
214pub fn pretty_print(expr: &TLExpr, config: &PrettyConfig) -> String {
215    let mut buf = String::with_capacity(128);
216    // write_expr never actually fails on a String sink
217    let _ = write_expr(expr, config, &mut buf);
218    buf
219}
220
221/// Pretty-print a [`TLExpr`] with the default Unicode configuration.
222pub fn pretty(expr: &TLExpr) -> String {
223    pretty_print(expr, &PrettyConfig::default())
224}
225
226/// Pretty-print a [`Term`] to a string (uses Unicode config).
227pub fn pretty_term(term: &Term) -> String {
228    pretty_term_with(term, &PrettyConfig::default())
229}
230
231/// Pretty-print a [`Term`] with the given configuration.
232pub fn pretty_term_with(term: &Term, config: &PrettyConfig) -> String {
233    let mut buf = String::with_capacity(32);
234    let _ = write_term(term, config, &mut buf);
235    buf
236}
237
238// ---------------------------------------------------------------------------
239// Term rendering
240// ---------------------------------------------------------------------------
241
242fn write_term(term: &Term, config: &PrettyConfig, buf: &mut String) -> std::fmt::Result {
243    match term {
244        Term::Var(name) => write!(buf, "{name}"),
245        Term::Const(name) => write!(buf, "{name}"),
246        Term::Typed {
247            value,
248            type_annotation,
249        } => {
250            write_term(value, config, buf)?;
251            if config.show_types {
252                write!(buf, ":{}", type_annotation.type_name)?;
253            }
254            Ok(())
255        }
256    }
257}
258
259fn write_term_list(args: &[Term], config: &PrettyConfig, buf: &mut String) -> std::fmt::Result {
260    for (i, arg) in args.iter().enumerate() {
261        if i > 0 {
262            write!(buf, ", ")?;
263        }
264        write_term(arg, config, buf)?;
265    }
266    Ok(())
267}
268
269// ---------------------------------------------------------------------------
270// Expression rendering
271// ---------------------------------------------------------------------------
272
273fn write_expr(expr: &TLExpr, cfg: &PrettyConfig, buf: &mut String) -> std::fmt::Result {
274    match expr {
275        // ---- predicates ----
276        TLExpr::Pred { name, args } => {
277            write!(buf, "{name}(")?;
278            write_term_list(args, cfg, buf)?;
279            write!(buf, ")")
280        }
281
282        // ---- logical connectives ----
283        TLExpr::And(l, r) => write_binop(l, r, cfg, buf, cfg.sym_and()),
284        TLExpr::Or(l, r) => write_binop(l, r, cfg, buf, cfg.sym_or()),
285        TLExpr::Imply(l, r) => write_binop(l, r, cfg, buf, cfg.sym_implies()),
286        TLExpr::Not(e) => {
287            write!(buf, "{}", cfg.sym_not())?;
288            write_subexpr(e, cfg, buf)
289        }
290
291        // ---- quantifiers ----
292        TLExpr::Exists { var, domain, body } => {
293            write!(
294                buf,
295                "{}{} {} {}. ",
296                cfg.sym_exists(),
297                var,
298                cfg.sym_in(),
299                domain
300            )?;
301            write_expr(body, cfg, buf)
302        }
303        TLExpr::ForAll { var, domain, body } => {
304            write!(
305                buf,
306                "{}{} {} {}. ",
307                cfg.sym_forall(),
308                var,
309                cfg.sym_in(),
310                domain
311            )?;
312            write_expr(body, cfg, buf)
313        }
314
315        // ---- arithmetic ----
316        TLExpr::Add(l, r) => write_binop(l, r, cfg, buf, "+"),
317        TLExpr::Sub(l, r) => write_binop(l, r, cfg, buf, "-"),
318        TLExpr::Mul(l, r) => write_binop(l, r, cfg, buf, "*"),
319        TLExpr::Div(l, r) => write_binop(l, r, cfg, buf, "/"),
320        TLExpr::Pow(l, r) => write_binop(l, r, cfg, buf, "^"),
321        TLExpr::Mod(l, r) => write_binop(l, r, cfg, buf, "%"),
322        TLExpr::Min(l, r) => write_func2("min", l, r, cfg, buf),
323        TLExpr::Max(l, r) => write_func2("max", l, r, cfg, buf),
324
325        // ---- unary math ----
326        TLExpr::Abs(e) => write_func1("abs", e, cfg, buf),
327        TLExpr::Floor(e) => write_func1("floor", e, cfg, buf),
328        TLExpr::Ceil(e) => write_func1("ceil", e, cfg, buf),
329        TLExpr::Round(e) => write_func1("round", e, cfg, buf),
330        TLExpr::Sqrt(e) => write_func1("sqrt", e, cfg, buf),
331        TLExpr::Exp(e) => write_func1("exp", e, cfg, buf),
332        TLExpr::Log(e) => write_func1("log", e, cfg, buf),
333        TLExpr::Sin(e) => write_func1("sin", e, cfg, buf),
334        TLExpr::Cos(e) => write_func1("cos", e, cfg, buf),
335        TLExpr::Tan(e) => write_func1("tan", e, cfg, buf),
336
337        // ---- comparisons ----
338        TLExpr::Eq(l, r) => write_binop(l, r, cfg, buf, "="),
339        TLExpr::Lt(l, r) => write_binop(l, r, cfg, buf, "<"),
340        TLExpr::Gt(l, r) => write_binop(l, r, cfg, buf, ">"),
341        TLExpr::Lte(l, r) => {
342            let sym = match cfg.symbols {
343                SymbolSet::Unicode => "\u{2264}",
344                SymbolSet::Ascii => "<=",
345            };
346            write_binop(l, r, cfg, buf, sym)
347        }
348        TLExpr::Gte(l, r) => {
349            let sym = match cfg.symbols {
350                SymbolSet::Unicode => "\u{2265}",
351                SymbolSet::Ascii => ">=",
352            };
353            write_binop(l, r, cfg, buf, sym)
354        }
355
356        // ---- conditional ----
357        TLExpr::IfThenElse {
358            condition,
359            then_branch,
360            else_branch,
361        } => {
362            write!(buf, "if ")?;
363            write_expr(condition, cfg, buf)?;
364            write!(buf, " then ")?;
365            write_expr(then_branch, cfg, buf)?;
366            write!(buf, " else ")?;
367            write_expr(else_branch, cfg, buf)
368        }
369
370        // ---- constants ----
371        TLExpr::Constant(v) => {
372            // Format without trailing zeros where possible
373            if v.fract() == 0.0 && v.abs() < 1e15 {
374                write!(buf, "{}", *v as i64)
375            } else {
376                write!(buf, "{v}")
377            }
378        }
379
380        // ---- score ----
381        TLExpr::Score(e) => {
382            write!(buf, "{}(", cfg.sym_sigma())?;
383            write_expr(e, cfg, buf)?;
384            write!(buf, ")")
385        }
386
387        // ---- aggregation ----
388        TLExpr::Aggregate {
389            op,
390            var,
391            domain,
392            body,
393            group_by,
394        } => {
395            write!(buf, "{op:?}({var} {} {domain}", cfg.sym_in())?;
396            if let Some(groups) = group_by {
397                write!(buf, " group_by [{}]", groups.join(", "))?;
398            }
399            write!(buf, ". ")?;
400            write_expr(body, cfg, buf)?;
401            write!(buf, ")")
402        }
403
404        // ---- let binding ----
405        TLExpr::Let { var, value, body } => {
406            write!(buf, "let {var} = ")?;
407            write_expr(value, cfg, buf)?;
408            write!(buf, " in ")?;
409            write_expr(body, cfg, buf)
410        }
411
412        // ---- modal logic ----
413        TLExpr::Box(e) => {
414            write!(buf, "{}", cfg.sym_box())?;
415            write_subexpr(e, cfg, buf)
416        }
417        TLExpr::Diamond(e) => {
418            write!(buf, "{}", cfg.sym_diamond())?;
419            write_subexpr(e, cfg, buf)
420        }
421
422        // ---- temporal logic ----
423        TLExpr::Next(e) => {
424            write!(buf, "X ")?;
425            write_subexpr(e, cfg, buf)
426        }
427        TLExpr::Eventually(e) => {
428            write!(buf, "F ")?;
429            write_subexpr(e, cfg, buf)
430        }
431        TLExpr::Always(e) => {
432            write!(buf, "G ")?;
433            write_subexpr(e, cfg, buf)
434        }
435        TLExpr::Until { before, after } => write_binop(before, after, cfg, buf, "U"),
436        TLExpr::Release { released, releaser } => write_binop(released, releaser, cfg, buf, "R"),
437        TLExpr::WeakUntil { before, after } => write_binop(before, after, cfg, buf, "W"),
438        TLExpr::StrongRelease { released, releaser } => {
439            write_binop(released, releaser, cfg, buf, "M")
440        }
441
442        // ---- fuzzy logic ----
443        TLExpr::TNorm { kind, left, right } => {
444            write!(buf, "T_{kind:?}(")?;
445            write_expr(left, cfg, buf)?;
446            write!(buf, ", ")?;
447            write_expr(right, cfg, buf)?;
448            write!(buf, ")")
449        }
450        TLExpr::TCoNorm { kind, left, right } => {
451            write!(buf, "S_{kind:?}(")?;
452            write_expr(left, cfg, buf)?;
453            write!(buf, ", ")?;
454            write_expr(right, cfg, buf)?;
455            write!(buf, ")")
456        }
457        TLExpr::FuzzyNot { kind, expr } => {
458            write!(buf, "FN_{kind:?}(")?;
459            write_expr(expr, cfg, buf)?;
460            write!(buf, ")")
461        }
462        TLExpr::FuzzyImplication {
463            kind,
464            premise,
465            conclusion,
466        } => {
467            write!(buf, "FI_{kind:?}(")?;
468            write_expr(premise, cfg, buf)?;
469            write!(buf, ", ")?;
470            write_expr(conclusion, cfg, buf)?;
471            write!(buf, ")")
472        }
473
474        // ---- probabilistic ----
475        TLExpr::SoftExists {
476            var,
477            domain,
478            body,
479            temperature,
480        } => {
481            write!(
482                buf,
483                "soft_{}{} {} {} [t={temperature}]. ",
484                cfg.sym_exists(),
485                var,
486                cfg.sym_in(),
487                domain
488            )?;
489            write_expr(body, cfg, buf)
490        }
491        TLExpr::SoftForAll {
492            var,
493            domain,
494            body,
495            temperature,
496        } => {
497            write!(
498                buf,
499                "soft_{}{} {} {} [t={temperature}]. ",
500                cfg.sym_forall(),
501                var,
502                cfg.sym_in(),
503                domain
504            )?;
505            write_expr(body, cfg, buf)
506        }
507        TLExpr::WeightedRule { weight, rule } => {
508            write!(buf, "{weight}:: ")?;
509            write_expr(rule, cfg, buf)
510        }
511        TLExpr::ProbabilisticChoice { alternatives } => {
512            write!(buf, "choice(")?;
513            for (i, (prob, expr)) in alternatives.iter().enumerate() {
514                if i > 0 {
515                    write!(buf, "; ")?;
516                }
517                write!(buf, "{prob}: ")?;
518                write_expr(expr, cfg, buf)?;
519            }
520            write!(buf, ")")
521        }
522
523        // ---- higher-order ----
524        TLExpr::Lambda {
525            var,
526            var_type,
527            body,
528        } => {
529            write!(buf, "{}{var}", cfg.sym_lambda())?;
530            if let Some(ty) = var_type {
531                write!(buf, ":{ty}")?;
532            }
533            write!(buf, ". ")?;
534            write_expr(body, cfg, buf)
535        }
536        TLExpr::Apply { function, argument } => {
537            write_subexpr(function, cfg, buf)?;
538            write!(buf, "(")?;
539            write_expr(argument, cfg, buf)?;
540            write!(buf, ")")
541        }
542
543        // ---- set operations ----
544        TLExpr::SetMembership { element, set } => {
545            write_subexpr(element, cfg, buf)?;
546            write!(buf, " {} ", cfg.sym_element_of())?;
547            write_subexpr(set, cfg, buf)
548        }
549        TLExpr::SetUnion { left, right } => write_binop(left, right, cfg, buf, cfg.sym_union()),
550        TLExpr::SetIntersection { left, right } => {
551            write_binop(left, right, cfg, buf, cfg.sym_intersection())
552        }
553        TLExpr::SetDifference { left, right } => {
554            write_binop(left, right, cfg, buf, cfg.sym_setminus())
555        }
556        TLExpr::SetCardinality { set } => {
557            write!(buf, "|")?;
558            write_expr(set, cfg, buf)?;
559            write!(buf, "|")
560        }
561        TLExpr::EmptySet => write!(buf, "{}", cfg.sym_emptyset()),
562        TLExpr::SetComprehension {
563            var,
564            domain,
565            condition,
566        } => {
567            write!(buf, "{{ {var} : {domain} | ")?;
568            write_expr(condition, cfg, buf)?;
569            write!(buf, " }}")
570        }
571
572        // ---- counting quantifiers ----
573        TLExpr::CountingExists {
574            var,
575            domain,
576            body,
577            min_count,
578        } => {
579            let sym_e = cfg.sym_exists();
580            let sym_in = cfg.sym_in();
581            write!(buf, "{sym_e}>={min_count} {var} {sym_in} {domain}. ")?;
582            write_expr(body, cfg, buf)
583        }
584        TLExpr::CountingForAll {
585            var,
586            domain,
587            body,
588            min_count,
589        } => {
590            let sym_a = cfg.sym_forall();
591            let sym_in = cfg.sym_in();
592            write!(buf, "{sym_a}>={min_count} {var} {sym_in} {domain}. ")?;
593            write_expr(body, cfg, buf)
594        }
595        TLExpr::ExactCount {
596            var,
597            domain,
598            body,
599            count,
600        } => {
601            let sym_e = cfg.sym_exists();
602            let sym_in = cfg.sym_in();
603            write!(buf, "{sym_e}={count} {var} {sym_in} {domain}. ")?;
604            write_expr(body, cfg, buf)
605        }
606        TLExpr::Majority { var, domain, body } => {
607            let sym_in = cfg.sym_in();
608            write!(buf, "majority {var} {sym_in} {domain}. ")?;
609            write_expr(body, cfg, buf)
610        }
611
612        // ---- fixed points ----
613        TLExpr::LeastFixpoint { var, body } => {
614            write!(buf, "{}{var}. ", cfg.sym_mu())?;
615            write_expr(body, cfg, buf)
616        }
617        TLExpr::GreatestFixpoint { var, body } => {
618            write!(buf, "{}{var}. ", cfg.sym_nu())?;
619            write_expr(body, cfg, buf)
620        }
621
622        // ---- hybrid logic ----
623        TLExpr::Nominal { name } => write!(buf, "{}{name}", cfg.sym_at()),
624        TLExpr::At { nominal, formula } => {
625            write!(buf, "{}{nominal} ", cfg.sym_at())?;
626            write_subexpr(formula, cfg, buf)
627        }
628        TLExpr::Somewhere { formula } => {
629            write!(buf, "E ")?;
630            write_subexpr(formula, cfg, buf)
631        }
632        TLExpr::Everywhere { formula } => {
633            write!(buf, "A ")?;
634            write_subexpr(formula, cfg, buf)
635        }
636
637        // ---- constraint programming ----
638        TLExpr::AllDifferent { variables } => {
639            write!(buf, "all_different({})", variables.join(", "))
640        }
641        TLExpr::GlobalCardinality {
642            variables,
643            values,
644            min_occurrences,
645            max_occurrences,
646        } => {
647            write!(buf, "gcc([{}], [", variables.join(", "))?;
648            for (i, val) in values.iter().enumerate() {
649                if i > 0 {
650                    write!(buf, ", ")?;
651                }
652                write_expr(val, cfg, buf)?;
653            }
654            write!(buf, "], min={min_occurrences:?}, max={max_occurrences:?})")
655        }
656
657        // ---- abductive reasoning ----
658        TLExpr::Abducible { name, cost } => write!(buf, "abd({name}, {cost})"),
659        TLExpr::Explain { formula } => {
660            write!(buf, "explain(")?;
661            write_expr(formula, cfg, buf)?;
662            write!(buf, ")")
663        }
664
665        // ---- symbol literal ----
666        TLExpr::SymbolLiteral(s) => write!(buf, ":{s}"),
667
668        // ---- pattern matching ----
669        TLExpr::Match { scrutinee, arms } => {
670            write!(buf, "match ")?;
671            write_subexpr(scrutinee, cfg, buf)?;
672            write!(buf, " {{")?;
673            for (pat, body) in arms {
674                writeln!(buf)?;
675                for _ in 0..cfg.indent_width {
676                    write!(buf, " ")?;
677                }
678                write!(buf, "{pat} => ")?;
679                write_expr(body, cfg, buf)?;
680                write!(buf, ",")?;
681            }
682            write!(buf, "\n}}")
683        }
684    }
685}
686
687/// Write a sub-expression, wrapping in parentheses if it is compound.
688fn write_subexpr(expr: &TLExpr, cfg: &PrettyConfig, buf: &mut String) -> std::fmt::Result {
689    if needs_parens(expr) {
690        write!(buf, "(")?;
691        write_expr(expr, cfg, buf)?;
692        write!(buf, ")")
693    } else {
694        write_expr(expr, cfg, buf)
695    }
696}
697
698/// Binary operator helper: `(left op right)`.
699fn write_binop(
700    left: &TLExpr,
701    right: &TLExpr,
702    cfg: &PrettyConfig,
703    buf: &mut String,
704    op: &str,
705) -> std::fmt::Result {
706    write!(buf, "(")?;
707    write_expr(left, cfg, buf)?;
708    write!(buf, " {op} ")?;
709    write_expr(right, cfg, buf)?;
710    write!(buf, ")")
711}
712
713/// Unary function helper: `name(inner)`.
714fn write_func1(
715    name: &str,
716    inner: &TLExpr,
717    cfg: &PrettyConfig,
718    buf: &mut String,
719) -> std::fmt::Result {
720    write!(buf, "{name}(")?;
721    write_expr(inner, cfg, buf)?;
722    write!(buf, ")")
723}
724
725/// Binary function helper: `name(a, b)`.
726fn write_func2(
727    name: &str,
728    a: &TLExpr,
729    b: &TLExpr,
730    cfg: &PrettyConfig,
731    buf: &mut String,
732) -> std::fmt::Result {
733    write!(buf, "{name}(")?;
734    write_expr(a, cfg, buf)?;
735    write!(buf, ", ")?;
736    write_expr(b, cfg, buf)?;
737    write!(buf, ")")
738}
739
740/// Determine whether a sub-expression needs parenthesisation for clarity.
741fn needs_parens(expr: &TLExpr) -> bool {
742    matches!(
743        expr,
744        TLExpr::And(..)
745            | TLExpr::Or(..)
746            | TLExpr::Imply(..)
747            | TLExpr::Add(..)
748            | TLExpr::Sub(..)
749            | TLExpr::Mul(..)
750            | TLExpr::Div(..)
751            | TLExpr::Pow(..)
752            | TLExpr::Mod(..)
753            | TLExpr::Eq(..)
754            | TLExpr::Lt(..)
755            | TLExpr::Gt(..)
756            | TLExpr::Lte(..)
757            | TLExpr::Gte(..)
758            | TLExpr::Until { .. }
759            | TLExpr::Release { .. }
760            | TLExpr::WeakUntil { .. }
761            | TLExpr::StrongRelease { .. }
762            | TLExpr::SetUnion { .. }
763            | TLExpr::SetIntersection { .. }
764            | TLExpr::SetDifference { .. }
765    )
766}
767
768// ---------------------------------------------------------------------------
769// Tests
770// ---------------------------------------------------------------------------
771
772#[cfg(test)]
773mod tests {
774    use super::*;
775    use crate::{TLExpr, Term};
776
777    #[test]
778    fn test_pretty_pred() {
779        let expr = TLExpr::pred("knows", vec![Term::var("x"), Term::var("y")]);
780        assert_eq!(pretty(&expr), "knows(x, y)");
781    }
782
783    #[test]
784    fn test_pretty_and_unicode() {
785        let a = TLExpr::pred("P", vec![Term::var("x")]);
786        let b = TLExpr::pred("Q", vec![Term::var("y")]);
787        let expr = TLExpr::and(a, b);
788        let out = pretty(&expr);
789        assert!(out.contains('\u{2227}'), "expected unicode AND: {out}");
790    }
791
792    #[test]
793    fn test_pretty_and_ascii() {
794        let a = TLExpr::pred("P", vec![Term::var("x")]);
795        let b = TLExpr::pred("Q", vec![Term::var("y")]);
796        let expr = TLExpr::and(a, b);
797        let out = pretty_print(&expr, &PrettyConfig::ascii());
798        assert!(out.contains('&'), "expected & in ascii mode: {out}");
799    }
800
801    #[test]
802    fn test_pretty_or() {
803        let a = TLExpr::pred("P", vec![]);
804        let b = TLExpr::pred("Q", vec![]);
805        let expr = TLExpr::or(a, b);
806        let out = pretty(&expr);
807        assert!(out.contains('\u{2228}'), "expected unicode OR: {out}");
808    }
809
810    #[test]
811    fn test_pretty_not() {
812        let a = TLExpr::pred("P", vec![Term::var("x")]);
813        let expr = TLExpr::negate(a);
814        let out = pretty(&expr);
815        assert!(out.contains('\u{00ac}'), "expected unicode NOT: {out}");
816    }
817
818    #[test]
819    fn test_pretty_exists() {
820        let body = TLExpr::pred("P", vec![Term::var("x")]);
821        let expr = TLExpr::exists("x", "Person", body);
822        let out = pretty(&expr);
823        assert!(out.contains("\u{2203}x"), "expected exists with var: {out}");
824        assert!(out.contains("Person"), "expected domain: {out}");
825    }
826
827    #[test]
828    fn test_pretty_forall() {
829        let body = TLExpr::pred("P", vec![Term::var("x")]);
830        let expr = TLExpr::forall("x", "D", body);
831        let out = pretty(&expr);
832        assert!(out.contains("\u{2200}x"), "expected forall with var: {out}");
833    }
834
835    #[test]
836    fn test_pretty_implication() {
837        let a = TLExpr::pred("P", vec![]);
838        let b = TLExpr::pred("Q", vec![]);
839        let expr = TLExpr::imply(a, b);
840        let out = pretty(&expr);
841        assert!(out.contains('\u{2192}'), "expected unicode arrow: {out}");
842    }
843
844    #[test]
845    fn test_pretty_constant() {
846        let expr = TLExpr::Constant(0.5);
847        assert_eq!(pretty(&expr), "0.5");
848    }
849
850    #[test]
851    fn test_pretty_constant_integer() {
852        let expr = TLExpr::Constant(3.0);
853        assert_eq!(pretty(&expr), "3");
854    }
855
856    #[test]
857    fn test_pretty_add() {
858        let a = TLExpr::Constant(1.0);
859        let b = TLExpr::Constant(2.0);
860        let expr = TLExpr::add(a, b);
861        let out = pretty(&expr);
862        assert!(out.contains('+'), "expected +: {out}");
863    }
864
865    #[test]
866    fn test_pretty_nested() {
867        let p = TLExpr::pred("P", vec![]);
868        let q = TLExpr::pred("Q", vec![]);
869        let r = TLExpr::pred("R", vec![]);
870        let and_expr = TLExpr::and(p, q);
871        let or_expr = TLExpr::or(and_expr, r);
872        let out = pretty(&or_expr);
873        // The inner AND should be parenthesised inside the OR
874        assert!(out.contains('('), "expected parens in nested: {out}");
875        assert!(out.contains('\u{2227}'), "expected AND symbol: {out}");
876        assert!(out.contains('\u{2228}'), "expected OR symbol: {out}");
877    }
878
879    #[test]
880    fn test_pretty_term_var() {
881        let t = Term::var("hello");
882        assert_eq!(pretty_term(&t), "hello");
883    }
884
885    #[test]
886    fn test_pretty_term_const() {
887        let t = Term::constant("42");
888        assert_eq!(pretty_term(&t), "42");
889    }
890
891    #[test]
892    fn test_config_default_is_unicode() {
893        let cfg = PrettyConfig::default();
894        assert_eq!(cfg.symbols, SymbolSet::Unicode);
895    }
896
897    #[test]
898    fn test_config_ascii() {
899        let cfg = PrettyConfig::ascii();
900        assert_eq!(cfg.symbols, SymbolSet::Ascii);
901    }
902
903    #[test]
904    fn test_config_indent() {
905        let cfg = PrettyConfig::default().with_indent(4);
906        assert_eq!(cfg.indent_width, 4);
907    }
908
909    #[test]
910    fn test_pretty_deterministic() {
911        let expr = TLExpr::and(
912            TLExpr::pred("P", vec![Term::var("x")]),
913            TLExpr::or(TLExpr::pred("Q", vec![]), TLExpr::Constant(1.0)),
914        );
915        let a = pretty(&expr);
916        let b = pretty(&expr);
917        assert_eq!(a, b, "pretty printing must be deterministic");
918    }
919
920    #[test]
921    fn test_pretty_convenience() {
922        let expr = TLExpr::pred("P", vec![Term::var("x")]);
923        // `pretty` is just a shorthand for `pretty_print` with default config
924        let a = pretty(&expr);
925        let b = pretty_print(&expr, &PrettyConfig::default());
926        assert_eq!(a, b);
927    }
928}
tensorlogic_ir/pretty_print.rs

tensorlogic_ir/
pretty_print.rs
