From 3fdc516f31e87ed6d39330b13be4a32281c198d7 Mon Sep 17 00:00:00 2001
From: Masahiro Honma <hira.tara+git@gmail.com>
Date: Sat, 16 Sep 2023 08:00:41 +0900
Subject: [PATCH] fix: keep free variables from conflicting bound variables

---
 src/term.rs | 42 ++++++++++++++++++++++++++++++++++++------
 1 file changed, 36 insertions(+), 6 deletions(-)

diff --git a/src/term.rs b/src/term.rs
index 798f8ba..3739aec 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -450,11 +450,16 @@ pub fn app(lhs: Term, rhs: Term) -> Term {
 
 impl fmt::Display for Term {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
-        write!(f, "{}", show_precedence_cla(self, 0, 0))
+        write!(f, "{}", show_precedence_cla(self, 0, self.max_depth(), 0))
     }
 }
 
-fn show_precedence_cla(term: &Term, context_precedence: usize, depth: u32) -> String {
+fn show_precedence_cla(
+    term: &Term,
+    context_precedence: usize,
+    max_depth: u32,
+    depth: u32,
+) -> String {
     match term {
         Var(0) => "undefined".to_owned(),
         Var(i) => {
@@ -463,7 +468,8 @@ fn show_precedence_cla(term: &Term, context_precedence: usize, depth: u32) -> St
                     .expect("error while printing term")
                     .to_string()
             } else {
-                from_u32(96 + *i as u32)
+                // use a different name than bound variables
+                from_u32(max_depth + 96 + *i as u32 - depth)
                     .expect("error while printing term")
                     .to_string()
             }
@@ -474,7 +480,7 @@ fn show_precedence_cla(term: &Term, context_precedence: usize, depth: u32) -> St
                     "{}{}.{}",
                     LAMBDA,
                     from_u32(depth + 97).expect("error while printing term"),
-                    show_precedence_cla(t, 0, depth + 1)
+                    show_precedence_cla(t, 0, max_depth, depth + 1)
                 )
             };
             parenthesize_if(&ret, context_precedence > 1).into()
@@ -483,8 +489,8 @@ fn show_precedence_cla(term: &Term, context_precedence: usize, depth: u32) -> St
             let (ref t1, ref t2) = **boxed;
             let ret = format!(
                 "{} {}",
-                show_precedence_cla(t1, 2, depth),
-                show_precedence_cla(t2, 3, depth)
+                show_precedence_cla(t1, 2, max_depth, depth),
+                show_precedence_cla(t2, 3, max_depth, depth)
             );
             parenthesize_if(&ret, context_precedence == 3).into()
         }
@@ -598,6 +604,30 @@ mod tests {
         assert_eq!(&abs(Var(3)).to_string(), "λa.c");
         assert_eq!(&abs!(2, Var(3)).to_string(), "λa.λb.c");
         assert_eq!(&abs!(2, Var(4)).to_string(), "λa.λb.d");
+        assert_eq!(
+            app!(
+                Var(3),
+                Var(4),
+                abs(app(Var(4), Var(5))),
+                abs!(2, app(Var(5), Var(6)))
+            )
+            .to_string(),
+            "e f (λa.e f) (λa.λb.e f)"
+        );
+        assert_eq!(
+            app!(
+                abs!(2, app(Var(3), Var(4))),
+                Var(1),
+                Var(2),
+                abs(app(Var(2), Var(3)))
+            )
+            .to_string(),
+            "(λa.λb.c d) c d (λa.c d)"
+        );
+        assert_eq!(
+            &app(abs(Var(1)), app(abs(app(Var(10), Var(1))), Var(10))).to_string(),
+            "(λa.a) ((λa.j a) k)"
+        );
     }
 
     #[test]