use proptest::{
    prelude::*,
    string::{string_regex, RegexGeneratorStrategy},
};
use serde::{Deserialize, Serialize};
use std::fmt::{self, Display};

#[derive(Debug, PartialEq, Clone, Serialize, Deserialize)]
pub enum Type {
    Num,
    Bool,
    Arr(Box<Type>, Box<Type>),
}

impl Display for Type {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Type::Num => write!(f, "Num"),
            Type::Bool => write!(f, "Bool"),
            Type::Arr(l, r) => write!(f, "({} -> {})", l, r),
        }
    }
}

#[derive(Debug, PartialEq, Clone, Serialize, Deserialize)]
pub enum TypeError {
    UnknownType(Value),
    UnboundVariable(String),
}

#[derive(Debug, PartialEq, Clone, Serialize, Deserialize)]
pub enum Value {
    Num(i32),
    Bool(bool),
    Sym(String),
    App(Box<Value>, Box<Value>),
    Lam(String, Box<Value>),
    Def(String, Box<Value>),
    Let(String, Box<Value>, Box<Value>),
    // typed abstraction
    TLam(String, Type, Box<Value>),
    // reified type
    // this is unsound as we are not in a dependently typed language
    // but useful to unify external representation (AST). In theory,
    // we should separate AST from Terms
    Type(Type),
}

use Value::*;

impl Value {
    /// Return the spine of an application
    fn spine(&self) -> Vec<Value> {
        match self {
            App(l, r) => {
                let mut spine = l.spine();
                spine.push(*r.clone());
                spine
            }
            _ => vec![self.clone()],
        }
    }
}

impl Display for Value {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Value::Num(i) => write!(f, "{}", i),
            Value::Bool(b) => write!(f, "{}", b),
            Value::Sym(s) => write!(f, "{}", s),
            Value::App(_, _) => {
                let app = self
                    .spine()
                    .iter()
                    .map(|v| v.to_string())
                    .collect::<Vec<String>>()
                    .join(" ");
                write!(f, "({})", app)
            }
            Value::Lam(var, body) => write!(f, "(lam {} {})", var, body),
            Value::Def(var, value) => write!(f, "(def {} {})", var, value),
            Value::Let(var, value, body) => write!(f, "(let ({} {}) {})", var, value, body),
            Value::TLam(var, typ, body) => write!(f, "(tlam ({} {}) {})", var, typ, body),
            Value::Type(typ) => write!(f, ":{}", typ),
        }
    }
}

pub const IDENTIFIER: &str = "\\pL(\\pL|\\pN)*";

pub fn identifier() -> RegexGeneratorStrategy<String> {
    string_regex(IDENTIFIER).unwrap()
}

pub fn ascii_identifier() -> RegexGeneratorStrategy<String> {
    string_regex("[a-zA-Z][a-zA-Z0-9]*").unwrap()
}

impl Arbitrary for Value {
    type Parameters = ();
    type Strategy = BoxedStrategy<Self>;

    fn arbitrary_with(_args: ()) -> Self::Strategy {
        let any_num = any::<i32>().prop_map(Num);
        let any_bool = any::<bool>().prop_map(Bool);
        let leaf = prop_oneof![
            any_num,
            any_bool,
            // see https://unicode.org/reports/tr18/#General_Category_Property for one letter unicode categories
            identifier().prop_map(Sym),
        ];
        let expr = leaf.prop_recursive(4, 128, 5, move |inner| {
            prop_oneof![
                (inner.clone(), inner.clone()).prop_map(|(l, r)| App(Box::new(l), Box::new(r))),
                (identifier(), inner.clone()).prop_map(|(var, body)| Lam(var, Box::new(body))),
                (identifier(), inner.clone(), inner.clone()).prop_map(|(var, body, expr)| {
                    Value::Let(var, Box::new(body), Box::new(expr))
                }),
            ]
        });
        prop_oneof![
            expr.clone(),
            (identifier(), expr).prop_map(|(var, body)| Def(var, Box::new(body)))
        ]
        .boxed()
    }
}

#[cfg(test)]
mod ast_tests {

    use super::Value::{self, *};
    use proptest::collection::vec;
    use proptest::prelude::*;

    proptest! {
       #[test]
        fn display_multiple_applications_as_a_sequence(atoms in vec("[a-z]".prop_map(Sym), 2..10)) {
            let init  = atoms.first().unwrap().clone();
            let value = atoms.iter().skip(1).fold(init, |acc, expr| {
              Value::App(Box::new(acc.clone()), Box::new(expr.clone()))
            });
            assert_eq!(value.to_string(),
                       format!("({})",
                               atoms.iter().map(|v| v.to_string()).collect::<Vec<String>>().join(" ")));
        }

        #[test]
        fn can_serialize_and_deserialize(value in any::<Value>()) {
            let serialized = serde_json::to_string(&value).unwrap();
            let deserialized: Value = serde_json::from_str(&serialized).unwrap();
            assert_eq!(value, deserialized);
        }
    }

    #[test]
    fn can_represent_let_expression_in_json() {
        let let_expr = Let(
            "x".to_string(),
            Box::new(Num(42)),
            Box::new(Sym("x".to_string())),
        );
        let serialized = serde_json::to_string(&let_expr).unwrap();
        let expected = r#"{"Let":["x",{"Num":42},{"Sym":"x"}]}"#;
        assert_eq!(serialized, expected);
    }
}