use crate::ast::Value;
use proptest::prelude::*;
use proptest::prop_oneof;
use std::collections::BTreeMap;

type Name = String;

#[derive(Debug, Clone, PartialEq)]
enum Type {
    Int,
    Bool,
}

fn any_type() -> impl Strategy<Value = Type> {
    prop_oneof![Just(Type::Int), Just(Type::Bool),]
}

struct Context {
    context: BTreeMap<Name, Type>,
}

impl Context {
    pub fn empty() -> Self {
        Context {
            context: BTreeMap::new(),
        }
    }

    pub fn bind(&mut self, sym: Name, ty: Type) -> &mut Self {
        self.context.insert(sym, ty);
        self
    }

    pub fn type_of(&self, val: &Value) -> Option<Type> {
        use Value::*;

        match val {
            Num(_) => Some(Type::Int),
            Bool(_) => Some(Type::Bool),
            Sym(s) => self.context.get(s).cloned(),
            _ => None,
        }
    }
}

#[cfg(test)]
mod tests {

    use super::*;
    use crate::ast::Value::*;
    use proptest::prelude::*;

    proptest! {

        #[test]
        fn any_int_value_has_type_int(n in any::<i32>().prop_map(Num)) {
            let ctx = Context::empty();

            let ty = ctx.type_of(&n);

            assert_eq!(Some(Type::Int), ty);
        }

        #[test]
        fn any_bool_value_has_type_Bool(n in any::<bool>().prop_map(Bool)) {
            let ctx = Context::empty();

            let ty = ctx.type_of(&n);

            assert_eq!(Some(Type::Bool), ty);
        }

        #[test]
        fn any_bound_variable_has_bound_type(s in crate::ast::identifier(), t in any_type()) {
            let mut ctx = Context::empty();
            ctx.bind(s.clone(), t.clone());

            let ty = ctx.type_of(&Sym(s));

            assert_eq!(Some(t), ty);
        }

        #[test]
        fn any_unbound_variable_has_no_type(s in crate::ast::identifier()) {
            let mut ctx = Context::empty();

            let ty = ctx.type_of(&Sym(s));

            assert_eq!(None, ty);
        }

        #[test]
        fn def_symbol_has_type_of_its_body(s in crate::ast::identifier(), t in any_type()) {
        }

    }
}