Move λ-calcul workshop code to subdirectory

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