summaryrefslogtreecommitdiff
path: root/rust/src/lambda.rs
diff options
context:
space:
mode:
Diffstat (limited to 'rust/src/lambda.rs')
-rw-r--r--rust/src/lambda.rs292
1 files changed, 0 insertions, 292 deletions
diff --git a/rust/src/lambda.rs b/rust/src/lambda.rs
deleted file mode 100644
index a73ca34..0000000
--- a/rust/src/lambda.rs
+++ /dev/null
@@ -1,292 +0,0 @@
-use proptest::{
- arbitrary::any,
- prelude::*,
- strategy::{Strategy, ValueTree},
- test_runner::TestRunner,
-};
-use rand::Rng;
-use std::collections::HashMap;
-
-use crate::ast::*;
-
-#[derive(Debug, PartialEq)]
-pub struct Environment<'a> {
- parent: Box<Option<&'a Environment<'a>>>,
- bindings: HashMap<String, Value>,
-}
-
-impl<'a> Environment<'a> {
- pub fn new() -> Self {
- Environment {
- parent: Box::new(None),
- bindings: HashMap::new(),
- }
- }
-
- fn bind(&mut self, var: &str, value: &Value) {
- self.bindings.insert(var.to_string(), value.clone());
- }
-
- fn extends(&'a self) -> Self {
- Environment {
- parent: Box::new(Some(self)),
- bindings: HashMap::new(),
- }
- }
-
- fn lookup(&self, var: &str) -> Option<&Value> {
- self.bindings.get(var).or_else(|| match *self.parent {
- Some(parent) => parent.lookup(var),
- None => None,
- })
- }
-}
-
-impl<'a> Default for Environment<'a> {
- fn default() -> Self {
- Self::new()
- }
-}
-
-pub fn eval_all(values: &[Value]) -> Vec<Value> {
- let mut env = Environment::new();
- values.iter().map(|v| eval_whnf(v, &mut env)).collect()
-}
-
-/// 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) // TODO: return a more meaningful value?
- }
- Value::Let(var, value, expr) => {
- let mut newenv = env.extends();
- newenv.bind(var, value);
- eval_whnf(expr, &mut newenv)
- }
- 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_whnf(&Value::App(Box::new(val.clone()), r.clone()), env),
- None => arg.clone(),
- },
- other => Value::App(Box::new(other), r.clone()),
- },
- Value::Sym(var) => env.lookup(var).unwrap_or(arg).clone(),
- other => other.clone(),
- }
-}
-
-fn subst(var: &str, body: &Value, e: &Value) -> Value {
- match body {
- Value::Sym(x) if x == var => e.clone(),
- Value::Lam(x, b) if x == var => {
- let y = gensym();
- let bd = subst(x, b, &Value::Sym(y.clone()));
- Value::Lam(y, Box::new(bd))
- }
- 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(),
- }
-}
-
-pub fn gensym() -> String {
- let mut rng = rand::thread_rng();
-
- let n1: u8 = rng.gen();
- format!("x_{}", n1)
-}
-
-pub fn generate_expr(size: u32, runner: &mut TestRunner) -> Value {
- match size {
- 0 | 1 => {
- let n = any::<u16>().new_tree(runner).unwrap().current();
- Value::Num(n.into())
- }
- 2 => Value::Sym(ascii_identifier().new_tree(runner).unwrap().current()),
- 3 => any_sym().new_tree(runner).unwrap().current(),
- 4 => simple_app().new_tree(runner).unwrap().current(),
- 5 => nested_simple_app().new_tree(runner).unwrap().current(),
- 6 => simple_lambda().new_tree(runner).unwrap().current(),
- 7 => app_to_lambda().new_tree(runner).unwrap().current(),
- 8 => multi_app().new_tree(runner).unwrap().current(),
- _ => any::<u32>()
- .prop_flat_map(gen_terms)
- .new_tree(runner)
- .unwrap()
- .current(),
- }
-}
-
-pub fn generate_exprs(size: u32, runner: &mut TestRunner) -> Vec<Value> {
- let sz = (0..size).new_tree(runner).unwrap().current();
- (0..sz)
- .collect::<Vec<_>>()
- .into_iter()
- .map(|_| generate_expr(size, runner))
- .collect()
-}
-
-fn simple_app() -> impl Strategy<Value = Value> {
- let leaf = prop_oneof![any_num(), any_sym()];
- (leaf.clone(), leaf.clone()).prop_map(|(l, r)| Value::App(Box::new(l), Box::new(r)))
-}
-
-fn multi_app() -> impl Strategy<Value = Value> {
- let leaf = prop_oneof![any_num(), any_sym()];
- (leaf.clone(), leaf.clone()).prop_map(|(l, r)| Value::App(Box::new(l), Box::new(r)))
-}
-
-fn any_num() -> impl Strategy<Value = Value> {
- any::<i32>().prop_map(Value::Num)
-}
-
-fn nested_simple_app() -> impl Strategy<Value = Value> {
- let leaf = prop_oneof![any_num(), ascii_identifier().prop_map(Value::Sym)];
- leaf.prop_recursive(4, 128, 5, move |inner| {
- (inner.clone(), inner.clone()).prop_map(|(l, r)| Value::App(Box::new(l), Box::new(r)))
- })
-}
-
-fn any_sym() -> impl Strategy<Value = Value> {
- identifier().prop_map(Value::Sym)
-}
-
-fn simple_lambda() -> impl Strategy<Value = Value> {
- // TODO: there's nothing to guarantee the variable appears in the body
- (ascii_identifier(), nested_simple_app()).prop_map(|(v, b)| Value::Lam(v, Box::new(b)))
-}
-
-fn app_to_lambda() -> impl Strategy<Value = Value> {
- let lam = simple_lambda();
- let arg = prop_oneof![any_num(), any_sym(), nested_simple_app()];
- (lam, arg).prop_map(|(l, a)| Value::App(Box::new(l), Box::new(a)))
-}
-
-/// Cantor pairing function
-/// See https://en.wikipedia.org/wiki/Pairing_function
-fn pairing(k: u32) -> (u32, u32) {
- let a = ((((8 * (k as u64) + 1) as f64).sqrt() - 1.0) / 2.0).floor();
- let b = (a * (a + 1.0)) / 2.0;
- let n = (k as f64) - b;
- (n as u32, (a - n) as u32)
-}
-
-fn gen_terms(u: u32) -> impl Strategy<Value = Value> {
- if u % 2 != 0 {
- let j = (u - 1) / 2;
- if j % 2 == 0 {
- let k = j / 2;
- let (n, m) = pairing(k);
- let r = (gen_terms(n), gen_terms(m))
- .prop_map(move |(l, r)| Value::App(Box::new(l), Box::new(r)));
- r.boxed()
- } else {
- let k = (j - 1) / 2;
- let (n, m) = pairing(k);
- let r = gen_terms(m).prop_map(move |v| Value::Lam(format!("x_{}", n), Box::new(v)));
- r.boxed()
- }
- } else {
- let j = u / 2;
- Just(Value::Sym(format!("x_{}", j))).boxed()
- }
-}
-
-#[cfg(test)]
-mod lambda_test {
- use crate::parser::parse;
-
- use super::{eval_all, eval_whnf, Environment, Value};
-
- fn parse1(string: &str) -> Value {
- parse(string).pop().unwrap()
- }
-
- fn eval1(value: &Value) -> Value {
- eval_whnf(value, &mut Environment::new())
- }
-
- #[test]
- fn evaluating_a_non_reducible_value_yields_itself() {
- let value = parse1("(foo 12)");
- assert_eq!(value, eval1(&value));
- }
-
- #[test]
- fn evaluating_application_on_an_abstraction_reduces_it() {
- let value = parse1("((lam x x) 12)");
- assert_eq!(Value::Num(12), eval1(&value));
- }
-
- #[test]
- fn substitution_occurs_within_abstraction_body() {
- let value = parse1("(((lam x (lam y x)) 13) 12)");
- assert_eq!(Value::Num(13), eval1(&value));
- }
-
- #[test]
- fn substitution_occurs_within_application_body() {
- let value = parse1("(((lam x (lam y (y x))) 13) 12)");
- assert_eq!(
- Value::App(Box::new(Value::Num(12)), Box::new(Value::Num(13))),
- eval1(&value)
- );
- }
-
- #[test]
- fn substitution_does_not_capture_free_variables() {
- let value = parse1("(((lam x (lam x x)) 13) 12)");
- assert_eq!(Value::Num(12), eval1(&value));
- }
-
- #[test]
- fn interpretation_applies_to_both_sides_of_application() {
- let value = parse1("((lam x x) ((lam x x) 12))");
- assert_eq!(Value::Num(12), eval1(&value));
- }
-
- #[test]
- fn reduction_is_applied_until_normal_form_is_reached() {
- let value = parse1("((((lam y (lam x (lam y (x y)))) 13) (lam x x)) 11)");
- assert_eq!(Value::Num(11), eval1(&value));
- }
-
- #[test]
- fn reduction_always_select_leftmost_outermost_redex() {
- // this should not terminate if we evaluate the rightmost redex first, eg.
- // applicative order reduction
- let value = parse1("((lam x 1) ((lam x (x x)) (lam x (x x))))");
- assert_eq!(Value::Num(1), eval1(&value));
- }
-
- #[test]
- fn defined_symbols_are_evaluated_to_their_definition() {
- let values = parse("(def foo 12) foo");
- assert_eq!(vec![Value::Bool(true), Value::Num(12)], eval_all(&values));
- }
-
- #[test]
- fn let_expressions_bind_symbol_to_expression_in_environment() {
- let values = parse("(let (foo (lam x x)) (foo 12))");
- assert_eq!(vec![Value::Num(12)], eval_all(&values));
- }
-
- #[test]
- fn let_expressions_introduce_new_scope_for_bindings() {
- let values = parse("(let (foo (lam x x)) ((let (foo foo) foo) 13))");
- assert_eq!(vec![Value::Num(13)], eval_all(&values));
- }
-
- #[test]
- fn bound_symbol_in_higher_scope_are_resolved() {
- let values = parse("(let (id (lam x x)) (let (foo 12) (id foo)))");
- assert_eq!(vec![Value::Num(12)], eval_all(&values));
- }
-}
generated by cgit v1.2.3 (git 2.39.1) at 2026-02-06 03:08:29 +0000