use crate::r#type::{Type, Type::*, util::*};
use std::collections::HashMap;

impl Type {


    /// Tries to convert this type into another type.
    ///
    /// The following conversions are required:
    /// 0. self == other => self
    /// 1. (T T ... T T) -> (T ...)
    /// 2. self = concrete and other = variable type => self,
    /// 3. arrow types and lists and sums are mapped
    /// 4. makes [self] self if self == other
    pub fn convert(self, other: &Type) -> Result<Type, ()> {
	let (ty, ctx) = self.convert_ctx(other)?;
	let mut checks = HashMap::new();
	for (name, ty1) in ctx {
	    if let Some(ty2) = checks.insert(name, ty1.clone()) {
		if ty2 != ty1 {
		    return Err(());
		}
	    }
	}
	Ok(ty)
    }

    fn convert_ctx(
	self,
	other: &Type
    ) -> Result<(Type, Vec<(String, Type)>), ()> {

	let mut ctx = vec![];

	match (self, other) {

	    (a, b) if a == *b => Ok((a, ctx)),

	    (ty, VarType(name)) => if ty.is_concrete().is_ok() {
		ctx.push((name.clone(), ty.clone()));
		Ok((ty, ctx))
	    } else {
		Err(())
	    },

	    (List(v1), List(v2)) if v1.len() == v2.len() => {
		let mut res = vec![];
		for (t1, t2) in v1.into_iter().zip(v2) {
		    let (t, newctx) = t1.convert_ctx(t2)?;
		    ctx.extend(newctx);
		    res.push(t);
		}
		Ok((List(res), ctx))
	    },

	    (Arrow(a1, a2), Arrow(b1, b2)) => {
		let (t1, newctx) = a1.convert_ctx(b1)?;
		ctx.extend(newctx);
		let (t2, newctx) = a2.convert_ctx(b2)?;
		ctx.extend(newctx);
		Ok((arr(t1, t2), ctx))
	    },

	    (SumType(a1, a2), SumType(b1, b2)) => {
		let (t1, newctx) = a1.convert_ctx(b1)?;
		ctx.extend(newctx);
		let (t2, newctx) = a2.convert_ctx(b2)?;
		ctx.extend(newctx);
		Ok((sumtype(t1, t2), ctx))
	    },

	    (List(v), VecOf(ty)) => match v.get(0) {
		Some(t) => {
		    let (convt, newctx) = t.clone().convert_ctx(ty)?;
		    ctx.extend(newctx);
		    for t in v {
			let (sconvt, newctx) = t.convert_ctx(ty)?;
			if sconvt != convt {
			    return Err(());
			} else {
			    ctx.extend(newctx);
			}
		    }
		    Ok((vecof(convt), ctx))
		},
		None => Err(()), // questionable? could be useful to convert?
	    },

	    (VecOf(t1), VecOf(t2)) => {
		let (convt, ctx) = t1.convert_ctx(t2)?;
		Ok((vecof(convt), ctx))
	    },

	    // at the end, because it'd be nice to know in the
	    // guard that the conversion from v to t2 works, and
	    // if it doesn't, try something else, but now everyhting
	    // has already been tried so this is safe
	    (List(v), t2) if v.len() == 1 => v[0].clone().convert_ctx(t2),

	    _ => Err(())
	}
    }

}

#[cfg(test)]
mod tests {

    use crate::r#type::{Type::*, util::*};

    #[test]
    fn test_conversion_case0() {
	assert_eq!(Integer.convert(&Integer), Ok(Integer));
	assert_eq!(Boolean.convert(&Boolean), Ok(Boolean));
	assert_eq!(
	    List(vec![Integer, Boolean])
		.convert(&List(vec![Integer, Boolean])),
	    Ok(List(vec![Integer, Boolean]))
	);
	assert_eq!(
	    vecof(Integer).convert(&vecof(Integer)),
	    Ok(vecof(Integer))
	);
	assert_eq!(vt("T").convert(&vt("T")), Ok(vt("T")));

	assert!(Integer.convert(&Boolean).is_err());
	assert!(Boolean.convert(&Integer).is_err());
	assert!(
	    List(vec![Integer, Boolean])
		.convert(&List(vec![Integer, Integer]))
		.is_err()
	);
	assert!(
	    vecof(Integer)
		.convert(&vecof(Boolean))
		.is_err()
	);
	assert!(vt("T").convert(&vt("H")).is_err());
    }

    #[test]
    fn test_conversion_case1() {
	assert_eq!(
	    List(vec![Integer]).convert(&vecof(Integer)),
	    Ok(vecof(Integer))
	);
	assert_eq!(
	    List(vec![Integer]).convert(&vecof(vt("T"))),
	    Ok(vecof(Integer))
	);
    }

    #[test]
    fn test_conversion_case2() {
	assert_eq!(Integer.convert(&vt("T")), Ok(Integer));
	assert_eq!(Boolean.convert(&vt("T")), Ok(Boolean));
	assert_eq!(
	    List(vec![Integer, Integer])
		.convert(&List(vec![vt("T"), vt("T")])),
	    Ok(List(vec![Integer, Integer]))
	);
	assert_eq!(
	    List(vec![Integer, Boolean])
		.convert(&List(vec![vt("T"), vt("H")])),
	    Ok(List(vec![Integer, Boolean]))
	);
	assert_eq!(vecof(Integer).convert(&vecof(vt("T"))), Ok(vecof(Integer)));
	assert_eq!(
	    arr(arr(vecof(Integer), Integer), arr(vecof(Integer), Integer))
		.convert(&arr(vt("T"), vt("T"))),
	    Ok(arr(arr(vecof(Integer), Integer), arr(vecof(Integer), Integer)))
	);
	assert_eq!(
	    sumtype(sumtype(vecof(Integer), Integer), sumtype(vecof(Integer), Integer))
		.convert(&sumtype(vt("T"), vt("T"))),
	    Ok(sumtype(sumtype(vecof(Integer), Integer), sumtype(vecof(Integer), Integer)))
	);

	assert!(
	    List(vec![Integer, Boolean])
		.convert(&List(vec![vt("T"), vt("T")]))
		.is_err()
	);
	assert!(
	    arr(arr(vecof(Integer), Integer), arr(vecof(Boolean), Integer))
		.convert(&arr(vt("T"), vt("T")))
		.is_err()
	);
    }

}