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.
    ///
    /// Two equal values match:
    /// ```rust
    /// use myslip::sexp::{SExp::*, SLeaf::*, util::*};
    /// use myslip::r#type::{Type::*, util::*, TypeError::*, PatFail::*};
    /// assert_eq!(
    ///     scons(1, scons(2, Nil))
    ///         .matches_type(&List(vec![Integer, Integer])),
    ///     Ok(vec![])
    /// );
    /// ```
    ///
    /// On the other hand, if values don't match, an invalid pattern
    /// error should be thrown:
    /// ```rust
    /// use myslip::sexp::{SExp::*, SLeaf::*, util::*};
    /// use myslip::r#type::{Type::*, util::*, TypeError::*, PatFail::*};
    /// assert_eq!(
    ///     scons(1, scons(2, Nil))
    ///         .matches_type(&List(vec![Integer])),
    ///     Err(InvalidPattern(TypeMismatch {
    ///         pattern: scons(1, scons(2, Nil)),
    ///         expected: List(vec![Integer]),
    ///         found: List(vec![Integer, Integer])
    ///     }))
    /// );
    /// ```
    ///
    /// A wildcard variable matches too and gets the correct type:
    /// ```rust
    /// use myslip::sexp::{SExp::*, SLeaf::*, util::*};
    /// use myslip::r#type::{Type::*, util::*, TypeError::*, PatFail::*};
    /// assert_eq!(
    ///     var("x").matches_type(&List(vec![Integer, Integer])),
    ///     Ok(vec![("x".to_string(), List(vec![Integer, Integer]))])
    /// );
    /// ```
    ///
    /// Obviously that should also work for sub-expressions:
    /// ```rust
    /// use myslip::sexp::{SExp::*, SLeaf::*, util::*};
    /// use myslip::r#type::{Type::*, util::*, TypeError::*, PatFail::*};
    /// assert_eq!(
    ///     scons(var("x"), scons(2, Nil)).matches_type(&List(vec![arr(Integer, Integer), Integer])),
    ///     Ok(vec![("x".to_string(), arr(Integer, Integer))])
    /// );
    /// ```
    ///
    /// If the wildcard variable is encountered multiple times,
    /// an invalid operator error should be returned:
    /// ```rust
    /// use myslip::sexp::{SExp::*, SLeaf::*, util::*};
    /// use myslip::r#type::{Type::*, util::*, TypeError::*, PatFail::*};
    /// assert_eq!(
    ///     scons(var("x"), scons(var("x"), Nil)).matches_type(&List(vec![Integer, Integer])),
    ///     Err(InvalidPattern(RepeatedVariable(
    ///         "x".to_string(),
    ///         scons(var("x"), scons(var("x"), Nil))
    ///     )))
    /// );
    /// ```
    ///
    /// Then there's also rest patterns which should be appropriately typed:
    /// ```rust
    /// use myslip::sexp::{SExp::*, SLeaf::*, util::*};
    /// use myslip::r#type::{Type::*, util::*, TypeError::*, PatFail::*};
    /// assert_eq!(
    ///     scons(var("h"), scons(RestPat("t".to_string()), Nil))
    ///         .matches_type(&List(vec![arr(Integer, Integer), Integer, Integer, Integer])),
    ///     Ok(vec![
    ///         ("h".to_string(), arr(Integer, Integer)),
    ///         ("t".to_string(), List(vec![Integer, Integer, Integer]))
    ///     ])
    /// );
    /// ```
    ///
    /// They should also work with vectors:
    /// ```rust
    /// use myslip::sexp::{SExp::*, SLeaf::*, util::*};
    /// use myslip::r#type::{Type::*, util::*, TypeError::*, PatFail::*};
    /// assert_eq!(
    ///     scons(var("h"), scons(RestPat("t".to_string()), Nil))
    ///         .matches_type(&vecof(Integer)),
    ///     Ok(vec![
    ///         ("h".to_string(), Integer),
    ///         ("t".to_string(), vecof(Integer))
    ///     ])
    /// );
    /// ```
    ///
    /// Vector matching should work without the rest pattern too:
    /// ```rust
    /// use myslip::sexp::{SExp::*, SLeaf::*, util::*};
    /// use myslip::r#type::{Type::*, util::*, TypeError::*, PatFail::*};
    /// assert_eq!(
    ///     scons(var("h"), scons(2, Nil)).matches_type(&vecof(Integer)),
    ///     Ok(vec![("h".to_string(), Integer)])
    /// );
    /// ```
    /// 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> {

	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
		}))
	    },

	}

    }
}