From 28ae5ded8bf38dba8b439fce58e525d092633ec3 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Tue, 24 Sep 2024 18:03:35 +0200 Subject: Fix (naive) substitution under lambda --- rust/src/lambda.rs | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) (limited to 'rust') diff --git a/rust/src/lambda.rs b/rust/src/lambda.rs index 9964021..2ad69f7 100644 --- a/rust/src/lambda.rs +++ b/rust/src/lambda.rs @@ -16,22 +16,23 @@ pub fn run(arg: &str) -> String { fn interpret(arg: &Value) -> Value { match arg { - Value::App(l, r) => apply(l, r), + Value::App(l, r) => apply(&interpret(l), r), other => other.clone(), } } fn apply(l: &Value, r: &Value) -> Value { if let Value::Lam(v, body) = l { - subst(r, v, body) + subst(v, body, r) } else { Value::App(Box::new(l.clone()), Box::new(r.clone())) } } -fn subst(r: &Value, v: &str, body: &Value) -> Value { - match r { - Value::Sym(x) if x == v => body.clone(), +fn subst(var: &str, body: &Value, r: &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))), other => other.clone(), } } @@ -51,4 +52,10 @@ mod lambda_test { let value = parse("((lam x x) 12)"); assert_eq!(Value::Num(12), interpret(&value)); } + + #[test] + fn substitution_occurs_within_abstraction_body() { + let value = parse("(((lam x (lam y x)) 13) 12)"); + assert_eq!(Value::Num(13), interpret(&value)); + } } -- cgit v1.2.3