egglog/
termdag.rs

1use crate::util::{FreshGen, HashMap, HashSet, SymbolGen};
2use crate::*;
3use std::fmt::Write;
4
5pub type TermId = usize;
6
7#[allow(rustdoc::private_intra_doc_links)]
8/// Like [`Expr`]s but with sharing and deduplication.
9///
10/// Terms refer to their children indirectly via opaque [TermId]s (internally
11/// these are just `usize`s) that map into an ambient [`TermDag`].
12#[derive(Clone, PartialEq, Eq, Hash, Debug)]
13pub enum Term {
14    Lit(Literal),
15    Var(String),
16    App(String, Vec<TermId>),
17}
18
19/// A hashconsing arena for [`Term`]s.
20#[derive(Clone, PartialEq, Eq, Debug, Default)]
21pub struct TermDag {
22    /// A bidirectional map between deduplicated `Term`s and indices.
23    nodes: IndexSet<Term>,
24}
25
26/// A [`TermId`] paired with its [`TermDag`] so it can be ordered by
27/// [`TermDag::ast_cmp`], for use in ordered collections like
28/// `BTreeMap`/`BTreeSet` (see [`TermDag::ord_term`]). Only compare wrappers
29/// from the same [`TermDag`].
30#[derive(Copy, Clone)]
31pub struct OrdTerm<'a> {
32    termdag: &'a TermDag,
33    id: TermId,
34}
35
36impl OrdTerm<'_> {
37    /// The wrapped [`TermId`].
38    pub fn id(&self) -> TermId {
39        self.id
40    }
41}
42
43impl PartialEq for OrdTerm<'_> {
44    fn eq(&self, other: &Self) -> bool {
45        // Terms are hashconsed, so id equality is structural equality.
46        self.id == other.id
47    }
48}
49
50impl Eq for OrdTerm<'_> {}
51
52impl PartialOrd for OrdTerm<'_> {
53    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
54        Some(self.cmp(other))
55    }
56}
57
58impl Ord for OrdTerm<'_> {
59    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
60        self.termdag.ast_cmp(self.id, other.id)
61    }
62}
63
64const MAX_PRETTY_LINE_WIDTH: usize = 80;
65const PRETTY_INDENT_STEP: usize = 2;
66const MIN_SHARED_TERM_SIZE: usize = 4;
67
68#[macro_export]
69macro_rules! match_term_app {
70    ($e:expr; $body:tt) => {
71        match $e {
72            Term::App(head, args) => {
73                match (head.as_str(), args.as_slice())
74                    $body
75            }
76            _ => panic!("not an app")
77        }
78    }
79}
80
81#[derive(Clone)]
82struct RenderedTerm {
83    inline: String,
84    pretty: String,
85}
86
87impl RenderedTerm {
88    fn from_symbol(symbol: String) -> Self {
89        Self {
90            inline: symbol.clone(),
91            pretty: symbol,
92        }
93    }
94
95    fn is_multiline(&self) -> bool {
96        self.pretty.contains('\n')
97    }
98}
99
100/// Context used during term rendering with let-binding support.
101struct TermRenderContext<'a> {
102    /// Generator for fresh variable names used in let bindings.
103    fresh: &'a mut SymbolGen,
104    /// Maps each term ID to the number of times it is referenced in the DAG.
105    /// Terms referenced multiple times are candidates for let-binding.
106    ref_counts: &'a HashMap<TermId, usize>,
107    /// Maps each term ID to its size (number of nodes in the subtree).
108    /// Used to decide whether a term is large enough to warrant let-binding.
109    sizes: &'a HashMap<TermId, usize>,
110    /// Maps term IDs to the variable names they've been bound to.
111    /// Once a term is let-bound, subsequent references use this name.
112    bindings: HashMap<TermId, String>,
113    /// Buffer where let bindings are accumulated as they are created.
114    buf: &'a mut String,
115    /// Function that takes a constructor name and returns the name hint to use
116    name_hint_fn: Box<dyn Fn(&str) -> String + 'a>,
117}
118
119impl<'a> TermRenderContext<'a> {
120    fn new<F>(
121        fresh: &'a mut SymbolGen,
122        ref_counts: &'a HashMap<TermId, usize>,
123        sizes: &'a HashMap<TermId, usize>,
124        buf: &'a mut String,
125        name_hint_fn: F,
126    ) -> Self
127    where
128        F: Fn(&str) -> String + 'a,
129    {
130        Self {
131            fresh,
132            ref_counts,
133            sizes,
134            bindings: HashMap::default(),
135            buf,
136            name_hint_fn: Box::new(name_hint_fn),
137        }
138    }
139
140    fn get_name_hint(&self, constructor_name: &str) -> String {
141        (self.name_hint_fn)(constructor_name)
142    }
143}
144
145impl TermDag {
146    /// Returns the number of nodes in this DAG.
147    pub fn size(&self) -> usize {
148        self.nodes.len()
149    }
150
151    /// Convert the given term to its id.
152    ///
153    /// Panics if the term does not already exist in this [TermDag].
154    pub fn lookup(&self, node: &Term) -> TermId {
155        self.nodes.get_index_of(node).unwrap()
156    }
157
158    /// Convert the given id to the corresponding term.
159    ///
160    /// Panics if the id is not valid.
161    pub fn get(&self, id: TermId) -> &Term {
162        self.nodes.get_index(id).unwrap()
163    }
164
165    /// A deterministic total order on terms by their AST *structure*, rather
166    /// than by insertion order (which is what comparing raw [`TermId`]s would
167    /// give). Literals order among themselves by value, variables by name, and
168    /// applications by head symbol, then arity, then children left-to-right;
169    /// across kinds, `Lit < Var < App`.
170    ///
171    /// Useful for canonicalizing the elements of an unordered structure (e.g. a
172    /// set or multiset) into a stable, reproducible term order.
173    ///
174    /// `App` children are compared structurally, not by raw [`TermId`] order,
175    /// so [`Term`] does not derive `Ord` and the leaf arms are written out
176    /// rather than calling `l.cmp(r)`. Uses an explicit worklist because terms
177    /// can be deeply nested.
178    pub fn ast_cmp(&self, a: TermId, b: TermId) -> std::cmp::Ordering {
179        use std::cmp::Ordering;
180        let mut worklist = vec![(a, b)];
181        while let Some((a, b)) = worklist.pop() {
182            if a == b {
183                // Hashconsed: identical ids are structurally equal.
184                continue;
185            }
186            let ord = match (self.get(a), self.get(b)) {
187                (Term::Lit(x), Term::Lit(y)) => x.cmp(y),
188                (Term::Lit(_), _) => Ordering::Less,
189                (_, Term::Lit(_)) => Ordering::Greater,
190                (Term::Var(x), Term::Var(y)) => x.cmp(y),
191                (Term::Var(_), _) => Ordering::Less,
192                (_, Term::Var(_)) => Ordering::Greater,
193                (Term::App(hx, ax), Term::App(hy, ay)) => {
194                    match hx.cmp(hy).then_with(|| ax.len().cmp(&ay.len())) {
195                        Ordering::Equal => {
196                            // Children compare left to right: push reversed so
197                            // the leftmost pair pops first.
198                            worklist.extend(ax.iter().copied().zip(ay.iter().copied()).rev());
199                            continue;
200                        }
201                        ord => ord,
202                    }
203                }
204            };
205            if ord.is_ne() {
206                return ord;
207            }
208        }
209        Ordering::Equal
210    }
211
212    /// Sort child terms in place by [`ast_cmp`](Self::ast_cmp). A reusable
213    /// building block for canonicalizing container elements.
214    pub fn sort_terms_by_ast(&self, terms: &mut [TermId]) {
215        terms.sort_by(|a, b| self.ast_cmp(*a, *b));
216    }
217
218    /// Wrap `id` so it is ordered by [`ast_cmp`](Self::ast_cmp), e.g. as a key
219    /// in a `BTreeMap`/`BTreeSet` when canonicalizing container terms.
220    pub fn ord_term(&self, id: TermId) -> OrdTerm<'_> {
221        OrdTerm { termdag: self, id }
222    }
223
224    /// Make and return a [`Term::App`] with the given head symbol and children,
225    /// and insert into the DAG if it is not already present.
226    ///
227    /// Panics if any of the children are not already in the DAG.
228    pub fn app(&mut self, sym: String, children: Vec<TermId>) -> TermId {
229        let node = Term::App(sym, children);
230
231        self.add_node(&node)
232    }
233
234    /// Make a [`Term::Lit`] with the given literal and return its [`TermId`],
235    /// inserting it into the DAG if it is not already present.
236    pub fn lit(&mut self, lit: Literal) -> TermId {
237        let node = Term::Lit(lit);
238
239        self.add_node(&node)
240    }
241
242    /// Make and return a [`Term::Var`] with the given symbol, and insert into
243    /// the DAG if it is not already present.
244    pub fn var(&mut self, sym: String) -> TermId {
245        let node = Term::Var(sym);
246
247        self.add_node(&node)
248    }
249
250    fn add_node(&mut self, node: &Term) -> TermId {
251        self.nodes.get_index_of(node).unwrap_or_else(|| {
252            let id = self.nodes.len();
253            self.nodes.insert(node.clone());
254            id
255        })
256    }
257
258    /// Recursively converts the given expression to a term.
259    ///
260    /// This involves inserting every subexpression into this DAG. Because
261    /// TermDags are hashconsed, the resulting term is guaranteed to maximally
262    /// share subterms.
263    pub fn expr_to_term(&mut self, expr: &GenericExpr<String, String>) -> TermId {
264        let res = match expr {
265            GenericExpr::Lit(_, lit) => Term::Lit(lit.clone()),
266            GenericExpr::Var(_, v) => Term::Var(v.to_owned()),
267            GenericExpr::Call(_, op, args) => {
268                let args = args.iter().map(|a| self.expr_to_term(a)).collect();
269                Term::App(op.clone(), args)
270            }
271        };
272        self.add_node(&res)
273    }
274
275    /// Recursively converts the given term to an expression.
276    ///
277    /// Panics if the term contains subterms that are not in the DAG.
278    pub fn term_to_expr(&self, term: &TermId, span: Span) -> Expr {
279        let term = self.get(*term);
280        match term {
281            Term::Lit(lit) => Expr::Lit(span, lit.clone()),
282            Term::Var(v) => Expr::Var(span, v.clone()),
283            Term::App(op, args) => {
284                let args: Vec<_> = args
285                    .iter()
286                    .map(|a| self.term_to_expr(a, span.clone()))
287                    .collect();
288                Expr::Call(span, op.clone(), args)
289            }
290        }
291    }
292
293    /// Prints a term to a string, putting let bindings for shared subterms.
294    pub fn to_string_with_let(&self, fresh: &mut SymbolGen, term_id: TermId) -> String {
295        self.to_string_with_let_and_hint(fresh, term_id, "t")
296    }
297
298    /// Prints a term to a string, putting let bindings for shared subterms.
299    /// Uses the given name hint for generated variable names.
300    pub fn to_string_with_let_and_hint(
301        &self,
302        fresh: &mut SymbolGen,
303        term_id: TermId,
304        name_hint: &str,
305    ) -> String {
306        let mut buf = String::new();
307        let hint = name_hint.to_string();
308        let final_str =
309            self.to_string_with_let_internal(fresh, term_id, &mut buf, move |_| hint.clone());
310        format!("{buf}\n{final_str}")
311    }
312
313    /// Prints a term to a string, putting let bindings for shared subterms in `buf`.
314    /// Returns the final string representation of the term.
315    /// The `name_hint_fn` takes a constructor name and returns the hint to use for that term.
316    pub(crate) fn to_string_with_let_internal<'a, F>(
317        &self,
318        fresh: &'a mut SymbolGen,
319        term_id: TermId,
320        buf: &'a mut String,
321        name_hint_fn: F,
322    ) -> String
323    where
324        F: Fn(&str) -> String + 'a,
325    {
326        let (ref_counts, sizes) = self.collect_term_stats(term_id);
327        let mut ctx = TermRenderContext::new(fresh, &ref_counts, &sizes, buf, name_hint_fn);
328        let rendered = self.render_term(term_id, &mut ctx, false, 0);
329        rendered.pretty
330    }
331
332    fn render_term(
333        &self,
334        term_id: TermId,
335        ctx: &mut TermRenderContext,
336        allow_binding: bool,
337        indent: usize,
338    ) -> RenderedTerm {
339        if let Some(existing) = ctx.bindings.get(&term_id) {
340            return RenderedTerm::from_symbol(existing.clone());
341        }
342
343        // Get the constructor name for the hint function (if it's an App)
344        let constructor_name = match self.get(term_id) {
345            Term::App(name, _) => Some(name.clone()),
346            _ => None,
347        };
348
349        let rendered = match self.get(term_id) {
350            Term::App(name, children) => {
351                let mut child_renderings = Vec::with_capacity(children.len());
352                for child_id in children {
353                    let rendered_child =
354                        self.render_term(*child_id, ctx, true, indent + PRETTY_INDENT_STEP);
355                    child_renderings.push(rendered_child);
356                }
357
358                let mut inline = format!("({name}");
359                for child in &child_renderings {
360                    inline.push(' ');
361                    inline.push_str(&child.inline);
362                }
363                inline.push(')');
364
365                let inline_len = inline.chars().count();
366                let exceeds_width = indent + inline_len > MAX_PRETTY_LINE_WIDTH;
367                let child_multiline = child_renderings.iter().any(|c| c.is_multiline());
368
369                let pretty = if exceeds_width || child_multiline {
370                    if child_renderings.is_empty() {
371                        format!("({name})")
372                    } else {
373                        let mut s = format!("({name}");
374                        for (idx, child) in child_renderings.iter().enumerate() {
375                            s.push('\n');
376                            s.push_str(&" ".repeat(indent + PRETTY_INDENT_STEP));
377                            s.push_str(&child.pretty);
378                            if idx + 1 == child_renderings.len() {
379                                s.push(')');
380                            }
381                        }
382                        s
383                    }
384                } else {
385                    inline.clone()
386                };
387
388                RenderedTerm { inline, pretty }
389            }
390            Term::Lit(lit) => {
391                let repr = format!("{lit}");
392                RenderedTerm {
393                    inline: repr.clone(),
394                    pretty: repr,
395                }
396            }
397            Term::Var(v) => RenderedTerm {
398                inline: v.clone(),
399                pretty: v.clone(),
400            },
401        };
402
403        let term_size = *ctx.sizes.get(&term_id).unwrap_or(&1);
404        let repeat_count = ctx.ref_counts.get(&term_id).copied().unwrap_or(1);
405        let should_bind = allow_binding && repeat_count > 1 && term_size >= MIN_SHARED_TERM_SIZE;
406
407        if should_bind {
408            let hint = ctx.get_name_hint(constructor_name.as_deref().unwrap_or("t"));
409            let let_name = ctx.fresh.fresh(&hint);
410            self.push_binding(ctx.buf, &let_name, &rendered.pretty);
411            ctx.bindings.insert(term_id, let_name.clone());
412            RenderedTerm::from_symbol(let_name)
413        } else {
414            rendered
415        }
416    }
417
418    fn push_binding(&self, buf: &mut String, name: &str, body: &str) {
419        let trimmed = body.trim_end();
420        if trimmed.is_empty() {
421            buf.push_str("(let ");
422            buf.push_str(name);
423            buf.push_str(")\n");
424            return;
425        }
426
427        if trimmed.contains('\n') {
428            buf.push_str("(let ");
429            buf.push_str(name);
430            buf.push('\n');
431            let lines: Vec<&str> = trimmed.lines().collect();
432            for (idx, line) in lines.iter().enumerate() {
433                buf.push_str(&" ".repeat(PRETTY_INDENT_STEP));
434                buf.push_str(line);
435                if idx + 1 < lines.len() {
436                    buf.push('\n');
437                } else {
438                    buf.push(')');
439                    buf.push('\n');
440                }
441            }
442        } else {
443            buf.push_str("(let ");
444            buf.push_str(name);
445            buf.push(' ');
446            buf.push_str(trimmed);
447            buf.push_str(")\n");
448        }
449    }
450
451    fn collect_term_stats(
452        &self,
453        term_id: TermId,
454    ) -> (HashMap<TermId, usize>, HashMap<TermId, usize>) {
455        let mut counts = HashMap::default();
456        let mut visited = HashSet::default();
457        self.collect_term_ref_counts_inner(term_id, &mut counts, &mut visited);
458
459        let mut sizes = HashMap::default();
460        self.compute_term_size(term_id, &mut sizes);
461
462        (counts, sizes)
463    }
464
465    fn compute_term_size(&self, term_id: TermId, sizes: &mut HashMap<TermId, usize>) -> usize {
466        if let Some(size) = sizes.get(&term_id) {
467            return *size;
468        }
469
470        let size = match self.get(term_id) {
471            Term::App(_, children) => {
472                1 + children
473                    .iter()
474                    .map(|child| self.compute_term_size(*child, sizes))
475                    .sum::<usize>()
476            }
477            Term::Lit(_) | Term::Var(_) => 1,
478        };
479
480        sizes.insert(term_id, size);
481        size
482    }
483
484    fn collect_term_ref_counts_inner(
485        &self,
486        term_id: TermId,
487        counts: &mut HashMap<TermId, usize>,
488        visited: &mut HashSet<TermId>,
489    ) {
490        *counts.entry(term_id).or_insert(0) += 1;
491        if !visited.insert(term_id) {
492            return;
493        }
494
495        if let Term::App(_, children) = self.get(term_id) {
496            for child in children {
497                self.collect_term_ref_counts_inner(*child, counts, visited);
498            }
499        }
500    }
501
502    /// Converts the given term to a string.
503    ///
504    /// Panics if the term or any of its subterms are not in the DAG.
505    pub fn to_string(&self, term: TermId) -> String {
506        let mut result = String::new();
507        // subranges of the `result` string containing already stringified subterms
508        let mut ranges = HashMap::<TermId, (usize, usize)>::default();
509        // use a stack to avoid stack overflow
510
511        let mut stack = vec![(term, false, None)];
512        while let Some((id, space_before, mut start_index)) = stack.pop() {
513            if space_before {
514                result.push(' ');
515            }
516
517            if let Some((start, end)) = ranges.get(&id) {
518                result.extend_from_within(*start..*end);
519                continue;
520            }
521
522            match self.nodes[id].clone() {
523                Term::App(name, children) => {
524                    if start_index.is_some() {
525                        result.push(')');
526                    } else {
527                        stack.push((id, false, Some(result.len())));
528                        write!(&mut result, "({name}").unwrap();
529                        for c in children.iter().rev() {
530                            stack.push((*c, true, None));
531                        }
532                    }
533                }
534                Term::Lit(lit) => {
535                    start_index = Some(result.len());
536                    write!(&mut result, "{lit}").unwrap();
537                }
538                Term::Var(v) => {
539                    start_index = Some(result.len());
540                    write!(&mut result, "{v}").unwrap();
541                }
542            }
543
544            if let Some(start_index) = start_index {
545                ranges.insert(id, (start_index, result.len()));
546            }
547        }
548
549        result
550    }
551}
552
553#[cfg(test)]
554mod tests {
555    use super::*;
556    use crate::{ast::*, span, util::SymbolGen};
557
558    fn parse_term(s: &str) -> (TermDag, TermId) {
559        let e = Parser::default().get_expr_from_string(None, s).unwrap();
560        let mut td = TermDag::default();
561        let t = td.expr_to_term(&e);
562        (td, t)
563    }
564
565    #[test]
566    fn test_ast_cmp() {
567        use std::cmp::Ordering;
568        let mut td = TermDag::default();
569        let i1 = td.lit(Literal::Int(1));
570        let i2 = td.lit(Literal::Int(2));
571        let vx = td.var("x".into());
572        let f_i1 = td.app("f".into(), vec![i1]);
573        let f_i2 = td.app("f".into(), vec![i2]);
574        let g_i1 = td.app("g".into(), vec![i1]);
575        let f_i1_i1 = td.app("f".into(), vec![i1, i1]);
576
577        // Cross-kind: Lit < Var < App.
578        assert_eq!(td.ast_cmp(i1, vx), Ordering::Less);
579        assert_eq!(td.ast_cmp(vx, f_i1), Ordering::Less);
580        assert_eq!(td.ast_cmp(i1, f_i1), Ordering::Less);
581        // Literals by value.
582        assert_eq!(td.ast_cmp(i1, i2), Ordering::Less);
583        // Apps: same head, compare children.
584        assert_eq!(td.ast_cmp(f_i1, f_i2), Ordering::Less);
585        // Apps: by head symbol first.
586        assert_eq!(td.ast_cmp(f_i1, g_i1), Ordering::Less);
587        // Apps: by arity when head equal and shorter is a prefix.
588        assert_eq!(td.ast_cmp(f_i1, f_i1_i1), Ordering::Less);
589        // Reflexive / total.
590        assert_eq!(td.ast_cmp(f_i1, f_i1), Ordering::Equal);
591        assert_eq!(td.ast_cmp(f_i2, f_i1), Ordering::Greater);
592    }
593
594    #[test]
595    fn test_to_from_expr() {
596        let s = r#"(f (g x y) x y (g x y))"#;
597        let e = Parser::default().get_expr_from_string(None, s).unwrap();
598        let mut td = TermDag::default();
599        assert_eq!(td.size(), 0);
600        let t = td.expr_to_term(&e);
601        assert_eq!(td.size(), 4);
602        // the expression above has 4 distinct subterms.
603        // in left-to-right, depth-first order, they are:
604        //     x, y, (g x y), and the root call to f
605        // so we can compute expected answer by hand:
606        assert_eq!(
607            td.nodes.as_slice().iter().cloned().collect::<Vec<_>>(),
608            vec![
609                Term::Var("x".into()),
610                Term::Var("y".into()),
611                Term::App("g".into(), vec![0, 1]),
612                Term::App("f".into(), vec![2, 0, 1, 2]),
613            ]
614        );
615        // This is tested using string equality because e1 and e2 have different
616        let e2 = td.term_to_expr(&t, span!());
617        // annotations. A better way to test this would be to implement a map_ann
618        // function for GenericExpr.
619        assert_eq!(format!("{e}"), format!("{e2}")); // roundtrip
620    }
621
622    #[test]
623    fn test_match_term_app() {
624        let s = r#"(f (g x y) x y (g x y))"#;
625        let (td, t) = parse_term(s);
626        let term = td.get(t);
627        match_term_app!(term; {
628            ("f", [_, x, _, _]) => {
629                let span = span!();
630                assert_eq!(
631                    td.term_to_expr(x, span.clone()),
632                    crate::ast::GenericExpr::Var(span, "x".to_owned())
633                )
634            }
635            (head, _) => panic!("unexpected head {}, in {}:{}:{}", head, file!(), line!(), column!())
636        })
637    }
638
639    #[test]
640    fn test_to_string() {
641        let s = r#"(f (g x y) x y (g x y))"#;
642        let (td, t) = parse_term(s);
643        assert_eq!(td.to_string(t), s);
644    }
645
646    #[test]
647    fn test_lookup() {
648        let s = r#"(f (g x y) x y (g x y))"#;
649        let (td, t) = parse_term(s);
650        assert_eq!(t, td.size() - 1);
651    }
652
653    #[test]
654    fn test_app_var_lit() {
655        let s = r#"(f (g x y) x 7 (g x y))"#;
656        let (mut td, t) = parse_term(s);
657        let x = td.var("x".into());
658        let y = td.var("y".into());
659        let seven = td.lit(7.into());
660        let g = td.app("g".into(), vec![x, y]);
661        let t2 = td.app("f".into(), vec![g, x, seven, g]);
662        assert_eq!(t, t2);
663    }
664
665    #[test]
666    fn test_to_string_with_let_inlines_small_terms() {
667        let s = r#"(f (g x) (g x) (g x))"#;
668        let (td, t) = parse_term(s);
669        let mut sym = SymbolGen::new(String::new());
670        let result = td.to_string_with_let(&mut sym, t);
671        // No let bindings means result is just newline + repr
672        assert_eq!(result.trim(), s);
673    }
674
675    #[test]
676    fn test_to_string_with_let_shares_large_terms() {
677        let g_segment = ["(g a b)"; 8].join(" ");
678        let s = format!("(f (h {g_segment}) (h {g_segment}))");
679        let (td, t) = parse_term(&s);
680        let mut buf = String::new();
681        let mut sym = SymbolGen::new(String::new());
682        let repr = td.to_string_with_let_internal(&mut sym, t, &mut buf, |_| "t".to_string());
683        let first_line = buf.lines().next().expect("expected let binding");
684        assert!(first_line.starts_with("(let t"));
685        assert!(buf.contains("(h"));
686        let has_lonely_paren = buf.lines().any(|line| line.trim() == ")");
687        assert!(
688            !has_lonely_paren,
689            "unexpected standalone closing paren in\n{buf}"
690        );
691        assert!(buf.trim_end().ends_with(')'));
692        assert_eq!(repr, "(f t t)");
693    }
694
695    #[test]
696    fn test_to_string_with_let_wraps_long_lines() {
697        let s = r#"(verylongfunctionnamewithmanysegments alpha_argument beta_argument gamma_argument delta_argument epsilon_argument zeta_argument)"#;
698        let (td, t) = parse_term(s);
699        let mut sym = SymbolGen::new(String::new());
700        let result = td.to_string_with_let(&mut sym, t);
701        // No let bindings, so result is just newline + repr
702        let repr = result.trim();
703        assert!(repr.contains('\n'));
704        assert!(repr.contains("\n  "));
705        assert!(repr.starts_with("(verylongfunctionnamewithmanysegments"));
706    }
707
708    #[test]
709    fn test_multiline_parentheses_share_final_line() {
710        let expr = "(Trans (Add 3 2) (start) (Rule (Add 3 2) (Add 2 3) (name rw1) (premises t1) (substitution (a 2) (b 3))) t)";
711        let (td, t) = parse_term(expr);
712        let mut buf = String::new();
713        let mut sym = SymbolGen::new(String::new());
714        let repr = td.to_string_with_let_internal(&mut sym, t, &mut buf, |_| "t".to_string());
715        assert!(repr.contains('\n'), "expected multiline output, got {repr}");
716        let has_lonely_paren = repr.lines().any(|line| line.trim() == ")");
717        assert!(
718            !has_lonely_paren,
719            "found standalone closing paren line in {repr}"
720        );
721        if let Some(last_line) = repr.lines().last() {
722            assert!(
723                last_line.ends_with(')'),
724                "last line should end with closing paren: {last_line}"
725            );
726        }
727        let buf_has_lonely = buf.lines().any(|line| line.trim() == ")");
728        assert!(
729            !buf_has_lonely,
730            "bindings contain standalone closing paren in\n{buf}"
731        );
732    }
733}