path: root/lambda-calcul/rust/src/lambda.rs

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 type_of_all(values: &[Value]) -> Vec<Type> {
    let mut env = Environment::new();
    values.iter().map(|v| type_of(v, &mut env).unwrap()).collect()
}

fn type_of(v: &Value, env: &mut Environment) -> Result<Type, TypeError> {
    match v {
        Value::Num(_) => Ok(Type::Int),
        _ => Err(TypeError::UnknownType(v.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_expression_to_type(size: u32, runner: &mut TestRunner) -> Vec<Value> {
    match size {
        _ => {
            let n = any::<u16>().new_tree(runner).unwrap().current();
            vec![Value::Num(n.into())]
        }
    }
}

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::{ast::Type, parser::parse};

    use super::{Environment, Value, eval_all, eval_whnf, type_of};

    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));
    }

    #[test]
    fn type_of_a_number_is_int() {
        let value = parse1("12");
        let ty = type_of(&value, &mut Environment::new()).unwrap();
        assert_eq!(Type::Int, ty);
    }
}