diff options
| author | Arnaud Bailly <arnaud.bailly@iohk.io> | 2024-10-01 20:10:02 +0200 |
|---|---|---|
| committer | Arnaud Bailly <arnaud.bailly@iohk.io> | 2024-10-01 20:10:02 +0200 |
| commit | cd3c54945d8bff57b121a2f834d165314e0f0738 (patch) | |
| tree | b93f164a8128fc036d22789d34993aa590652c7c /rust | |
| parent | 0c2119268bc54905bec2070676468f48b3002a89 (diff) | |
| download | lambda-nantes-cd3c54945d8bff57b121a2f834d165314e0f0738.tar.gz | |
Rename eval() to be more specific
Diffstat (limited to 'rust')
| -rw-r--r-- | rust/sample/test03/input | 2 | ||||
| -rw-r--r-- | rust/sample/test03/output | 2 | ||||
| -rw-r--r-- | rust/src/io.rs | 6 | ||||
| -rw-r--r-- | rust/src/lambda.rs | 23 |
4 files changed, 19 insertions, 14 deletions
diff --git a/rust/sample/test03/input b/rust/sample/test03/input index a23f8c6..6cff466 100644 --- a/rust/sample/test03/input +++ b/rust/sample/test03/input @@ -7,6 +7,6 @@ (def four (succ three)) (def five (succ four)) -(def plus (lam (a b) (a succ b))) +(def plus (lam (a b f s) (a f (b f s)))) (plus one three) diff --git a/rust/sample/test03/output b/rust/sample/test03/output index 578d298..fd56297 100644 --- a/rust/sample/test03/output +++ b/rust/sample/test03/output @@ -6,4 +6,4 @@ true true true true -five +four diff --git a/rust/src/io.rs b/rust/src/io.rs index 435f32f..8c628ba 100644 --- a/rust/src/io.rs +++ b/rust/src/io.rs @@ -5,7 +5,7 @@ use std::{ use crate::{ ast::Value, - lambda::{eval, eval_all, Environment}, + lambda::{eval_all, eval_whnf, Environment}, parser::parse, }; @@ -36,7 +36,7 @@ pub fn batch_eval<I: Read, O: Write>(inp: &mut I, outp: &mut O) { let values = parse(&input); let results = values .iter() - .map(|v| eval(v, &mut env)) + .map(|v| eval_whnf(v, &mut env)) .collect::<Vec<Value>>(); for result in results { writeln!(outp, "{}", result).unwrap(); @@ -63,7 +63,7 @@ pub fn repl<I: Read, O: Write>(inp: &mut I, outp: &mut O) { let values = parse(&input); let results = values .iter() - .map(|v| eval(v, &mut env)) + .map(|v| eval_whnf(v, &mut env)) .collect::<Vec<Value>>(); for result in results { writeln!(outp, "{}", result).unwrap(); diff --git a/rust/src/lambda.rs b/rust/src/lambda.rs index f69fb5b..6f394d8 100644 --- a/rust/src/lambda.rs +++ b/rust/src/lambda.rs @@ -44,24 +44,29 @@ impl<'a> Default for Environment<'a> { pub fn eval_all(values: &[Value]) -> Vec<Value> { let mut env = Environment::new(); - values.iter().map(|v| eval(v, &mut env)).collect() + values.iter().map(|v| eval_whnf(v, &mut env)).collect() } -pub fn eval(arg: &Value, env: &mut Environment) -> Value { +/// Reduce the given value to weak head normal form using call-by-name +/// evaluation strategy. +/// +/// call-by-name reduces the leftmost outermost redex first, which is +/// not under a lambda abstraction. +pub fn eval_whnf(arg: &Value, env: &mut Environment) -> Value { match arg { Value::Def(var, value) => { env.bind(var, value); - Value::Bool(true) + Value::Bool(true) // TODO: return a more meaningful value? } Value::Let(var, value, expr) => { let mut newenv = env.extends(); newenv.bind(var, value); - eval(expr, &mut newenv) + eval_whnf(expr, &mut newenv) } - Value::App(l, r) => match eval(l, env) { - Value::Lam(v, body) => eval(&subst(&v, &body, r), env), + Value::App(l, r) => match eval_whnf(l, env) { + Value::Lam(v, body) => eval_whnf(&subst(&v, &body, r), env), Value::Sym(var) => match env.lookup(&var) { - Some(val) => eval(&Value::App(Box::new(val.clone()), r.clone()), env), + Some(val) => eval_whnf(&Value::App(Box::new(val.clone()), r.clone()), env), None => arg.clone(), }, other => Value::App(Box::new(other), r.clone()), @@ -96,14 +101,14 @@ fn gensym() -> String { mod lambda_test { use crate::parser::parse; - use super::{eval, eval_all, Environment, Value}; + use super::{eval_all, eval_whnf, Environment, Value}; fn parse1(string: &str) -> Value { parse(string).pop().unwrap() } fn eval1(value: &Value) -> Value { - eval(value, &mut Environment::new()) + eval_whnf(value, &mut Environment::new()) } #[test] |
