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#[derive(Clone, PartialEq, Eq, Hash, Debug)]
13pub enum Term {
14 Lit(Literal),
15 Var(String),
16 App(String, Vec<TermId>),
17}
18
19#[derive(Clone, PartialEq, Eq, Debug, Default)]
21pub struct TermDag {
22 nodes: IndexSet<Term>,
24}
25
26#[derive(Copy, Clone)]
31pub struct OrdTerm<'a> {
32 termdag: &'a TermDag,
33 id: TermId,
34}
35
36impl OrdTerm<'_> {
37 pub fn id(&self) -> TermId {
39 self.id
40 }
41}
42
43impl PartialEq for OrdTerm<'_> {
44 fn eq(&self, other: &Self) -> bool {
45 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
100struct TermRenderContext<'a> {
102 fresh: &'a mut SymbolGen,
104 ref_counts: &'a HashMap<TermId, usize>,
107 sizes: &'a HashMap<TermId, usize>,
110 bindings: HashMap<TermId, String>,
113 buf: &'a mut String,
115 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 pub fn size(&self) -> usize {
148 self.nodes.len()
149 }
150
151 pub fn lookup(&self, node: &Term) -> TermId {
155 self.nodes.get_index_of(node).unwrap()
156 }
157
158 pub fn get(&self, id: TermId) -> &Term {
162 self.nodes.get_index(id).unwrap()
163 }
164
165 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 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 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 pub fn sort_terms_by_ast(&self, terms: &mut [TermId]) {
215 terms.sort_by(|a, b| self.ast_cmp(*a, *b));
216 }
217
218 pub fn ord_term(&self, id: TermId) -> OrdTerm<'_> {
221 OrdTerm { termdag: self, id }
222 }
223
224 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 pub fn lit(&mut self, lit: Literal) -> TermId {
237 let node = Term::Lit(lit);
238
239 self.add_node(&node)
240 }
241
242 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 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 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 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 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 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 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 pub fn to_string(&self, term: TermId) -> String {
506 let mut result = String::new();
507 let mut ranges = HashMap::<TermId, (usize, usize)>::default();
509 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 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 assert_eq!(td.ast_cmp(i1, i2), Ordering::Less);
583 assert_eq!(td.ast_cmp(f_i1, f_i2), Ordering::Less);
585 assert_eq!(td.ast_cmp(f_i1, g_i1), Ordering::Less);
587 assert_eq!(td.ast_cmp(f_i1, f_i1_i1), Ordering::Less);
589 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 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 let e2 = td.term_to_expr(&t, span!());
617 assert_eq!(format!("{e}"), format!("{e2}")); }
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 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 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}