From c8d3bbbda767b3cbe92159e7b0096a9d7224b931 Mon Sep 17 00:00:00 2001 From: Masahiro Honma Date: Sat, 16 Sep 2023 18:56:20 +0900 Subject: [PATCH 1/4] feat: introduce max_depth() method --- src/term.rs | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/src/term.rs b/src/term.rs index 3526558..798f8ba 100644 --- a/src/term.rs +++ b/src/term.rs @@ -397,6 +397,30 @@ impl Term { } true } + + /// Returns the max number of depth of lambda abstractions + /// + /// # Example + /// ``` + /// use lambda_calculus::*; + /// + /// assert_eq!(abs(Var(1)).max_depth(), 1); + /// ``` + pub fn max_depth(&self) -> u32 { + match self { + Var(_) => 0, + Abs(t) => t.max_depth() + 1, + App(boxed) => { + let d0 = boxed.0.max_depth(); + let d1 = boxed.1.max_depth(); + if d0 < d1 { + d1 + } else { + d0 + } + } + } + } } /// Wraps a `Term` in an `Abs`traction. Consumes its argument. @@ -615,4 +639,15 @@ mod tests { assert!(!abs!(10, Var(11)).is_supercombinator()); assert!(!abs!(10, app(Var(10), Var(11))).is_supercombinator()); } + + #[test] + fn max_depth() { + assert_eq!(Var(1).max_depth(), 0); + assert_eq!(abs(Var(1)).max_depth(), 1); + assert_eq!(abs!(10, Var(5)).max_depth(), 10); + assert_eq!( + app!(abs!(5, Var(2)), abs!(9, Var(4)), abs!(7, Var(6))).max_depth(), + 9 + ); + } } From 3fdc516f31e87ed6d39330b13be4a32281c198d7 Mon Sep 17 00:00:00 2001 From: Masahiro Honma Date: Sat, 16 Sep 2023 08:00:41 +0900 Subject: [PATCH 2/4] 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] From 7e46add3c54562e6b7bbed71e34dc740521df25d Mon Sep 17 00:00:00 2001 From: ljedrz Date: Wed, 20 Sep 2023 15:03:13 +0200 Subject: [PATCH 3/4] refactor: simplify Term::max_depth Signed-off-by: ljedrz --- src/term.rs | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/term.rs b/src/term.rs index 3739aec..c9304c3 100644 --- a/src/term.rs +++ b/src/term.rs @@ -398,7 +398,8 @@ impl Term { true } - /// Returns the max number of depth of lambda abstractions + /// Returns the maximum depth of lambda abstractions + /// in the given `Term`. /// /// # Example /// ``` @@ -413,11 +414,7 @@ impl Term { App(boxed) => { let d0 = boxed.0.max_depth(); let d1 = boxed.1.max_depth(); - if d0 < d1 { - d1 - } else { - d0 - } + d0.max(d1) } } } From 5505945c8e77173a6005725c5901a0ea4215579f Mon Sep 17 00:00:00 2001 From: ljedrz Date: Wed, 20 Sep 2023 15:07:11 +0200 Subject: [PATCH 4/4] drive-by: a small clippy fix in a test Signed-off-by: ljedrz --- src/parser.rs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/parser.rs b/src/parser.rs index aa2f98f..d72866d 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -381,10 +381,7 @@ mod tests { #[test] fn alternative_lambda_parsing() { - assert_eq!( - parse(r#"\\\2(321)"#, DeBruijn), - parse("λλλ2(321)", DeBruijn) - ) + assert_eq!(parse(r"\\\2(321)", DeBruijn), parse("λλλ2(321)", DeBruijn)) } #[test]