From 4a5d3e3c19b18a329417260294ebe2d726417eeb Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Tue, 24 Sep 2024 18:11:21 +0200 Subject: Substitution occurs under application --- rust/src/lambda.rs | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/rust/src/lambda.rs b/rust/src/lambda.rs index 2ad69f7..d767003 100644 --- a/rust/src/lambda.rs +++ b/rust/src/lambda.rs @@ -29,10 +29,11 @@ fn apply(l: &Value, r: &Value) -> Value { } } -fn subst(var: &str, body: &Value, r: &Value) -> Value { +fn subst(var: &str, body: &Value, e: &Value) -> Value { match body { - Value::Sym(x) if x == var => r.clone(), - Value::Lam(x, b) => Value::Lam(x.to_string(), Box::new(subst(var, b, r))), + Value::Sym(x) if x == var => e.clone(), + Value::Lam(x, b) => Value::Lam(x.to_string(), Box::new(subst(var, b, e))), + Value::App(l, r) => Value::App(Box::new(subst(var, l, e)), Box::new(subst(var, r, e))), other => other.clone(), } } @@ -58,4 +59,13 @@ mod lambda_test { let value = parse("(((lam x (lam y x)) 13) 12)"); assert_eq!(Value::Num(13), interpret(&value)); } + + #[test] + fn substitution_occurs_within_application_body() { + let value = parse("(((lam x (lam y (y x))) 13) 12)"); + assert_eq!( + Value::App(Box::new(Value::Num(12)), Box::new(Value::Num(13))), + interpret(&value) + ); + } } -- cgit v1.2.3