use rand::Rng;
use std::fs::read_to_string;

mod ast;
use ast::*;

mod parser;
use parser::*;

pub fn run(arg: &str) -> String {
    let content = read_to_string(arg).unwrap();
    let value = parse(&content.to_string());
    let result = eval(&value);

    result.to_string()
}

fn eval(arg: &Value) -> Value {
    match arg {
        Value::App(l, r) => {
            let result = apply(&eval(l), r);
            if is_reducible(&result) {
                eval(&result)
            } else {
                result
            }
        }
        other => other.clone(),
    }
}

fn is_reducible(result: &Value) -> bool {
    match result {
        Value::App(l, r) => match **l {
            Value::Lam(_, _) => true,
            _ => is_reducible(l) || is_reducible(r),
        },
        Value::Lam(_, _) => false,
        _ => false,
    }
}

fn apply(l: &Value, r: &Value) -> Value {
    if let Value::Lam(v, body) = l {
        subst(v, body, r)
    } else {
        Value::App(Box::new(l.clone()), Box::new(r.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)
}

#[cfg(test)]
mod lambda_test {
    use crate::{eval, parse, Value};

    #[test]
    fn evaluating_a_non_reducible_value_yields_itself() {
        let value = parse("(foo 12)");
        assert_eq!(value, eval(&value));
    }

    #[test]
    fn evaluating_application_on_an_abstraction_reduces_it() {
        let value = parse("((lam x x) 12)");
        assert_eq!(Value::Num(12), eval(&value));
    }

    #[test]
    fn substitution_occurs_within_abstraction_body() {
        let value = parse("(((lam x (lam y x)) 13) 12)");
        assert_eq!(Value::Num(13), eval(&value));
    }

    #[test]
    fn substitution_occurs_within_application_body() {
        let value = parse("(((lam x (lam y (y x))) 13) 12)");
        assert_eq!(
            Value::App(Box::new(Value::Num(12)), Box::new(Value::Num(13))),
            eval(&value)
        );
    }

    #[test]
    fn substitution_does_not_capture_free_variables() {
        let value = parse("(((lam x (lam x x)) 13) 12)");
        assert_eq!(Value::Num(12), eval(&value));
    }

    #[test]
    fn interpretation_applies_to_both_sides_of_application() {
        let value = parse("((lam x x) ((lam x x) 12))");
        assert_eq!(Value::Num(12), eval(&value));
    }

    #[test]
    fn reduction_is_applied_until_normal_form_is_reached() {
        let value = parse("((((lam y (lam x (lam y (x y)))) 13) (lam x x)) 11)");
        assert_eq!(Value::Num(11), eval(&value));
    }

    #[test]
    fn reduction_always_select_leftmost_outermost_redex() {
        // this should not terminate if we evaluate the rightmost redex first
        let value = parse("((lam x 1) ((lam x (x x)) (lam x (x x))))");
        assert_eq!(Value::Num(1), eval(&value));
    }
}