use proptest::{ arbitrary::{any, any_with, arbitrary_with}, prelude::*, strategy::{Strategy, ValueTree}, test_runner::TestRunner, }; use rand::{rngs::SmallRng, Rng, RngCore, SeedableRng}; use serde::{Deserialize, Serialize}; use std::collections::HashMap; use crate::ast::*; #[derive(Debug, PartialEq)] pub struct Environment<'a> { parent: Box>>, bindings: HashMap, } 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 { 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(), } } 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::().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(), _ => todo!(), } } fn simple_app() -> impl Strategy { 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 { any::().prop_map(Value::Num) } fn nested_simple_app() -> impl Strategy { let leaf = prop_oneof![any_num(), any_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 { identifier().prop_map(Value::Sym) } #[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)); } }