use crate::r#type::{Type, TypeError, Type::*, TypeError::*, PatFail::*, util::*};
use crate::sexp::{SExp, SExp::*, SLeaf::*, util::*};
use std::collections::{HashMap, HashSet};
use std::iter;

impl SExp {

    /// Checks if this expression matches the given type,
    /// returns all variable names bound by a respective case.
    ///
    /// TODO? Nil / empty list
    pub fn matches_type(
	&self,
	ty: &Type
    ) -> Result<Vec<(String, Type)>, TypeError> {

	let mut checks = HashSet::new();

	let res = self.clone()
	    .matches_type_ctx(ty.clone(), HashMap::new())?;

	for (k, _) in res.clone() {
	    if !checks.insert(k.clone()) {
		return Err(InvalidPattern(RepeatedVariable(k, self.clone())));
	    }
	}

	Ok(res)

    }

    fn matches_type_ctx(
	self,
	ty: Type,
	ctx: HashMap<String, Type>
    ) -> Result<Vec<(String, Type)>, TypeError> {

	println!("checking if {} matches pattern {}", &ty, &self);

	match (self, ty) {

	    (a, b) if a.infer_list_type(ctx.clone()) == Ok(b.clone()) =>
		Ok(ctx.into_iter().collect()),

	    (a, b) if a.infer_type(ctx.clone()) == Ok(b.clone()) =>
		Ok(ctx.into_iter().collect()),

	    (Atom(Var(name)), t) =>
		Ok(ctx.into_iter()
		   .chain(iter::once((name, t)))
		   .collect()),

	    (exp, VecOf(ty)) => {
		let mut res: Vec<(String, Type)> =
		    ctx.clone().into_iter().collect();
		let mut exps = exp.clone().parts();
		// TODO: Nil or empty exp
		let restpat = exps.remove(exps.len() - 1);
		for exp in exps {
		    for et in exp.matches_type_ctx(*ty.clone(), ctx.clone())? {
			res.push(et);
		    }
		}
		match restpat {
		    Atom(RestPat(name)) => {
			res.push((name, vecof(ty)));
			Ok(res)
		    },
		    t => {
			for et in t.matches_type_ctx(*ty.clone(), ctx.clone())? {
			    res.push(et);
			}
			Ok(res)
		    }
		}
	    },

	    (SCons(e1, e2), List(typelist)) => {
	    	let explist = scons(e1.clone(), e2.clone()).parts();
		let mut res: Vec<(String, Type)> =
		    ctx.clone().into_iter().collect();
	    	if explist.len() == typelist.len() {
		    for (exp, ty) in explist.into_iter().zip(typelist) {
			for (e, t) in exp.matches_type_ctx(ty, ctx.clone())? {
			    res.push((e, t));
			}
		    }
		    Ok(res)
	    	} else {
		    match explist.last().cloned() {
			Some(Atom(RestPat(name))) => {
			    for (exp, ty) in explist.clone()
				.into_iter()
				.rev().skip(1).rev()
				.zip(typelist.clone())
			    {
				for (e, t) in exp.matches_type_ctx(ty, ctx.clone())? {
				    res.push((e, t));
				}
			    }
			    res.push((
				name,
				List(typelist
				     .into_iter()
				     .skip(explist.len() - 1)
				     .collect())
			    ));
			    Ok(res)
			},
			_ => Err(InvalidPattern(TypeMismatch {
			    pattern: scons(e1.clone(), e2.clone()),
			    expected: List(typelist),
			    found: scons(e1, e2).infer_list_type(ctx)?,
			})),
		    }
		}
	    },

	    (e, t) => {
		let found_ty = e.infer_list_type(ctx)?;
		Err(InvalidPattern(TypeMismatch {
		    pattern:  e,
		    expected: t,
		    found:    found_ty
		}))
	    },

	}

    }
}

#[cfg(test)]
mod tests {
    use crate::sexp::{SExp::*, SLeaf::*, util::*};
    use crate::r#type::{Type::*, util::*, TypeError::*, PatFail::*};

    #[test]
    fn test_type_atoms() {
	assert_eq!(Atom(Int(1)).matches_type(&Integer), Ok(vec![]));
	assert_eq!(Atom(True).matches_type(&Boolean), Ok(vec![]));
	assert_eq!(Atom(Ty(Integer)).matches_type(&TypeLit), Ok(vec![]));
	assert_eq!(Atom(Nil).matches_type(&NilType), Ok(vec![]));
    }

    #[test]
    fn test_vector_match() {
	assert_eq!(
	    scons(1, scons(2, Nil))
		.matches_type(&List(vec![VecType, vecof(Integer)])),
	    Ok(vec![])
	);
	assert_eq!(
	    scons(var("a"), scons(var("b"), Nil))
		.matches_type(&List(vec![VecType, vecof(Integer)])),
	    Ok(vec![
		("a".to_string(), Integer),
		("b".to_string(), Integer)
	    ])
	);
	assert_eq!(
	    scons(var("a"), scons(RestPat("b".to_string()), Nil))
		.matches_type(&List(vec![VecType, vecof(Integer)])),
	    Ok(vec![
		("a".to_string(), Integer),
		("b".to_string(), List(vec![VecType, vecof(Integer)]))
	    ])
	);
    }

    #[test]
    fn test_list_match() {
	assert_eq!(
	    scons(1, scons(2, Nil))
		.matches_type(&List(vec![QuoteTy, List(vec![Integer, Integer])])),
	    Ok(vec![])
	);
	assert_eq!(
	    scons(var("a"), scons(var("b"), Nil))
		.matches_type(&List(vec![QuoteTy, List(vec![Integer, Integer])])),
	    Ok(vec![
		("a".to_string(), Integer),
		("b".to_string(), Integer)
	    ])
	);
	assert_eq!(
	    scons(var("a"), scons(RestPat("b".to_string()), Nil))
		.matches_type(&List(vec![QuoteTy, List(vec![Integer, Integer, Integer])])),
	    Ok(vec![
		("a".to_string(), Integer),
		("b".to_string(), List(vec![QuoteTy, List(vec![Integer, Integer])]))
	    ])
	);
    }

    #[test]
    fn test_mismatch_match() {
        assert_eq!(
            scons(1, scons(2, Nil))
                .matches_type(&List(vec![QuoteTy, List(vec![Integer])])),
            Err(InvalidPattern(TypeMismatch {
                pattern: scons(1, scons(2, Nil)),
                expected: List(vec![QuoteTy, List(vec![Integer])]),
                found: List(vec![QuoteTy, List(vec![Integer, Integer])])
            }))
        );
    }

    #[test]
    fn test_simple_wildcard_match() {
        assert_eq!(
            var("x").matches_type(&List(vec![QuoteTy, List(vec![Integer, Integer])])),
            Ok(vec![("x".to_string(), List(vec![QuoteTy, List(vec![Integer, Integer])]))])
        );
    }

    #[test]
    fn test_invalid_pattern_match() {
        assert_eq!(
            scons(var("x"), scons(var("x"), Nil))
		.matches_type(&List(vec![QuoteTy, List(vec![Integer, Integer])])),
            Err(InvalidPattern(RepeatedVariable(
                "x".to_string(),
                scons(var("x"), scons(var("x"), Nil))
            )))
        );
    }

    #[test]
    fn test_nil_match() {
	assert_eq!(
	    Atom(Nil).matches_type(&List(vec![VecType, vecof(Boolean)])),
	    Ok(vec![])
	);
	assert_eq!(
	    Atom(Nil).matches_type(&List(vec![QuoteTy, List(vec![])])),
	    Ok(vec![])
	);
    }
}