use rand::Rng;
use std::{
    collections::HashMap,
    fs::read_to_string,
    io::{BufRead, BufReader, Read, Write},
};

mod ast;
use ast::*;

mod parser;
use parser::*;

#[derive(Debug, PartialEq)]
struct Environment<'a> {
    parent: Box<Option<&'a Environment<'a>>>,
    bindings: HashMap<String, Value>,
}

impl<'a> Environment<'a> {
    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,
        })
    }

    fn binds(&self, s: &str) -> bool {
        self.bindings.contains_key(s)
            || match *self.parent {
                Some(parent) => parent.binds(s),
                None => false,
            }
    }
}

pub fn eval_file(file_name: &str) -> String {
    let content = read_to_string(file_name).unwrap();
    let values = parse(&content.to_string());
    eval_all(&values)
        .iter()
        .map(|v| v.to_string())
        .collect::<Vec<String>>()
        .join(" ")
}

pub fn repl<I: Read, O: Write>(inp: &mut I, outp: &mut O) {
    let mut env = Environment::new();
    let mut reader = BufReader::new(inp);
    loop {
        let mut input = String::new();
        write!(outp, "> ").unwrap();
        outp.flush().unwrap();
        match reader.read_line(&mut input) {
            Ok(0) => break,
            Ok(_) => (),
            Err(e) => {
                writeln!(outp, "{}", e).unwrap();
                break;
            }
        }
        let values = parse(&input);
        let results = values
            .iter()
            .map(|v| eval(v, &mut env))
            .collect::<Vec<Value>>();
        for result in results {
            writeln!(outp, "{}", result).unwrap();
            outp.flush().unwrap();
        }
    }
}

fn eval_all(values: &[Value]) -> Vec<Value> {
    let mut env = Environment::new();
    values.iter().map(|v| eval(v, &mut env)).collect()
}

fn eval(arg: &Value, env: &mut Environment) -> Value {
    match arg {
        Value::Def(var, value) => {
            env.bind(var, value);
            Value::Bool(true)
        }
        Value::Let(var, value, expr) => {
            let mut newenv = env.extends();
            newenv.bind(var, value);
            eval(expr, &mut newenv)
        }
        Value::App(l, r) => {
            let result = apply(&eval(l, env), r);
            if is_reducible(&result, env) {
                eval(&result, env)
            } else {
                result
            }
        }
        Value::Sym(var) => env.lookup(var).unwrap_or(arg).clone(),
        other => other.clone(),
    }
}

fn is_reducible(result: &Value, env: &Environment) -> bool {
    match result {
        Value::App(l, r) => match **l {
            Value::Lam(_, _) => true,
            _ => is_reducible(l, env) || is_reducible(r, env),
        },
        Value::Let(_, _, _) => true,
        Value::Sym(s) => env.binds(s),
        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, eval_all, parse, Environment, Value};

    fn parse1(string: &str) -> Value {
        parse(string).pop().unwrap()
    }

    fn eval1(value: &Value) -> Value {
        eval(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
        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));
    }
}