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

impl Type {

    /// Checks if this type is known as the given other type,
    /// ie. checks if there exists an implicit conversion from
    /// one to the other.
    ///
    /// This is needed for list to vec conversions.
    /// ```rust
    /// use myslip::r#type::{Type::*, util::*};
    /// assert!(List(vec![Integer, Integer, Integer]).aka(&vecof(Integer)));
    /// ```
    ///
    /// Preferrably this should also work with generics:
    /// ```rust
    /// use myslip::r#type::{Type::*, util::*};
    /// assert!(List(vec![Integer, Integer, Integer]).aka(&vecof(vt("T"))));
    /// assert!(List(vec![Boolean, Boolean, Boolean]).aka(&vecof(vt("T"))));
    /// ```
    ///
    /// But of course it also should know when to fail:
    /// ```rust
    /// use myslip::r#type::{Type::*, util::*};
    /// assert!(!List(vec![Integer, Boolean]).aka(&vecof(Integer)));
    /// assert!(!List(vec![Integer, Boolean]).aka(&vecof(Boolean)));
    /// ```
    ///
    /// Generics might be dangerous:
    /// ```rust
    /// use myslip::r#type::{Type::*, util::*};
    /// assert!(arr(Boolean, Boolean).aka(&arr(vt("T"), vt("T"))));
    /// assert!(
    ///     List(vec![Integer, Integer])
    ///         .aka(&List(vec![vt("T"), vt("T")]))
    /// );
    /// assert!(
    ///     List(vec![Integer, Boolean])
    ///         .aka(&List(vec![vt("T"), vt("H")]))
    /// );
    /// assert!(
    ///     !List(vec![Integer, Boolean])
    ///         .aka(&List(vec![vt("T"), vt("T")]))
    /// );
    /// assert!(
    ///     !List(vec![Integer, Boolean])
    ///         .aka(&List(vec![vt("T"), vt("T")]))
    /// );
    /// assert!(!List(vec![Integer, Boolean, vt("X")]).aka(&vecof(vt("T"))));
    /// ```
    pub fn aka(&self, known_as: &Type) -> bool {
	self.least_general_supertype(known_as) == *known_as
    }

    pub fn least_general_supertype(&self, other: &Type) -> Type {
	let (ty, ctx) = self.lgst_ctx(other, Vec::new());
	let mut checks = HashMap::new();
	for (name, ty1) in ctx {
	    if let Some(ty2) = checks.insert(name, ty1.clone()) {
		if ty2 != ty1 {
		    return vt("?");
		}
	    }
	}
	ty
    }

    fn lgst_ctx(
	&self,
	other: &Type,
	mut ctx: Vec<(String, Type)>
    ) -> (Type, Vec<(String, Type)>) {

	match (self, other) {

	    (a, b) if a == b => (a.clone(), ctx),

	    (a, VarType(name)) => {
		ctx.push((name.clone(), a.clone()));
		(vt(name), ctx)
	    },

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

	    //(VecOf(a), VecOf(b)) => {
	    //	let (res, ctx) = a.lgst_ctx(b, ctx);
	    //	(vecof(res), ctx)
	    //},

	    (List(v1), List(v2)) if v1.len() == v2.len() => {
	    	let mut res = vec![];
	    	for (a, b) in v1.into_iter().zip(v2) {
	    	    let (ty, newctx) = a.lgst_ctx(b, ctx.clone());
	    	    res.push(ty);
		    ctx = newctx;
	    	}
	    	(List(res), ctx)
	    },

	    (List(v1), List(v2)) => match v1.get(0).or(v2.get(0)) {
	    	Some(first) => {
		    let mut res = first.clone();
		    for ty in v1.into_iter().chain(v2) {
			let (ty, newctx) = res.lgst_ctx(ty, ctx.clone());
			res = ty;
			ctx = newctx;
		    }
		    (vecof(res), ctx)
	    	},
	    	None => panic!("unreachable - types would be equal")
	    },

	    (List(v), VecOf(b)) => {
		let mut res = *b.clone();
		for ty in v {
		    let (ty, newctx) = res.lgst_ctx(ty, ctx.clone());
		    res = ty;
		    ctx = newctx;
		}
		(vecof(res), ctx)
	    },
	    (VecOf(b), List(v)) => {
		let mut res = *b.clone();
		for ty in v {
		    let (ty, newctx) = res.lgst_ctx(ty, ctx.clone());
		    res = ty;
		    ctx = newctx;
		}
		(vecof(res), ctx)
	    },

	    (List(v), b) if v.len() == 1 && *&v[0].aka(b) => (b.clone(), ctx),

	    _ => (vt("T"), ctx)

	}    

    }

    /// Tries to convert this type into a subtype of the other.
    ///
    /// Currently the most important conversion is from list to vec.
    /// ```rust
    /// use myslip::r#type::{Type::*, util::*};
    /// 
    /// assert_eq!(Integer.into_type(&Boolean), Err(()));
    /// assert_eq!(Integer.into_type(&Integer), Ok(Integer));
    /// assert_eq!(Integer.into_type(&vt("T")), Ok(Integer));
    /// assert_eq!(
    ///     List(vec![Integer, Integer]).into_type(&vecof(Integer)),
    ///     Ok(vecof(Integer))
    /// );
    /// assert_eq!(
    ///     List(vec![Integer, Integer]).into_type(&vecof(vt("T"))),
    ///     Ok(vecof(Integer))
    /// );
    /// assert_eq!(
    ///     List(vec![Integer, Boolean]).into_type(&vecof(vt("T"))),
    ///     Ok(vecof(vt("T")))
    /// );
    /// assert_eq!(List(vec![Boolean, Integer, Integer]).into_type(&List(vec![Boolean, vt("T"), vt("T")])), Ok(List(vec![Boolean, Integer, Integer])))
    /// ```
    ///
    /// Though the conversion from (a) to a is also convenient:
    /// ```rust
    /// use myslip::r#type::{Type::*, util::*};
    /// 
    /// assert_eq!(List(vec![Integer]).into_type(&Integer), Ok(Integer));
    /// ```
    ///
    /// Now this also needs to be able to hand generics:
    /// ```rust
    /// use myslip::r#type::{Type::*, util::*};
    /// assert_eq!(
    ///     arr(Boolean, Boolean)
    ///         .into_type(&arr(vt("T"), vt("T"))),
    ///     Ok(arr(Boolean, Boolean))
    /// );
    /// assert_eq!(
    ///     arr(Boolean, Integer)
    ///         .into_type(&arr(vt("T"), vt("H"))),
    ///     Ok(arr(Boolean, Integer))
    /// );
    /// assert_eq!(
    ///     arr(Boolean, Integer)
    ///         .into_type(&arr(vt("T"), vt("T"))),
    ///     Err(())
    /// );
    /// assert_eq!(
    ///     List(vec![Integer, Integer])
    ///         .into_type(&List(vec![vt("T"), vt("T")])),
    ///     Ok(List(vec![Integer, Integer]))
    /// );
    /// assert!(
    ///     List(vec![Integer, Boolean])
    ///         .into_type(&List(vec![vt("T"), vt("T")]))
    ///         .is_err()
    /// );
    /// assert!(
    ///     List(vec![Integer, Boolean, vt("X")])
    ///         .into_type(&vecof(vt("T")))
    ///         .is_err()
    /// );
    /// ```
    pub fn into_type(self, other: &Type) -> Result<Type, ()> {
	if !self.aka(other) {
	    return Err(());
	}

	match (&self, other) {

	    (a, b) if a == b => Ok(self),

	    (_, VarType(_)) => Ok(self),

	    (Arrow(a1, a2), Arrow(b1, b2)) => {
		let t1 = a1.clone().into_type(b1)?;
		let t2 = a2.clone().into_type(b2)?;
		Ok(arr(t1, t2))
	    },

	    (List(v1), List(v2)) if v1.len() == v2.len() => {
		let mut res = vec![];
		for (t1, t2) in v1.into_iter().zip(v2) {
		    res.push(t1.clone().into_type(&t2)?);
		}
		Ok(List(res))
	    }

	    (List(v), VecOf(b)) => match v.get(0) {
		Some(first) => {
		    let cand = v.into_iter()
			.fold(first.clone(), |a, b| a.least_general_supertype(b));
		    if cand.aka(b) {
			Ok(vecof(cand))
		    } else {
			Err(())
		    }
		},
		None => if NilType.aka(b) {
		    Ok(vecof(NilType))
		} else {
		    Err(())
		},
	    },

	    (List(x), b) if x.len() == 1 && *&x[0].aka(b) => Ok(x[0].clone()),
	    
	    _ => Err(())

	}
    }

}

#[cfg(test)]
mod tests {

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

    #[test]
    fn test_basic_general_supertypes() {

	assert_eq!(
	    Integer.least_general_supertype(&Integer),
	    Integer,
	    "if two types are equal, they get the same supertype"
	);
	assert_eq!(
	    Integer.least_general_supertype(&Boolean),
	    vt("T"),
	    "if two types have nothing in common, vt(\"t\") is returned"
	);

    }

    #[test]
    fn test_compound_general_supertypes() {

	assert_eq!(
	    List(vec![Integer, Integer])
		.least_general_supertype(
		    &List(vec![Integer, Integer])
		),
	    List(vec![Integer, Integer])
	);

	assert_eq!(
	    List(vec![Integer, Boolean])
		.least_general_supertype(
		    &List(vec![Integer, Integer])
		),
	    List(vec![Integer, vt("T")])
	);

	assert_eq!(
	    vecof(Integer)
		.least_general_supertype(
		    &vecof(Integer)
		),
	    vecof(Integer)
	);

	assert_eq!(
	    vecof(Integer)
		.least_general_supertype(
		    &vecof(Boolean)
		),
	    vt("T")
	);

	assert_eq!(
	    List(vec![Integer, Boolean]).least_general_supertype(
		&List(vec![Boolean, Integer])
	    ),
	    List(vec![vt("T"), vt("T")])
	);

    }

    #[test]
    fn test_conversion_in_general_supertypes() {

	assert_eq!(
	    List(vec![Integer, Integer]).least_general_supertype(
		&vecof(Integer)
	    ),
	    vecof(Integer)
	);

	assert_eq!(
	    List(vec![Integer, Integer]).least_general_supertype(
		&List(vec![Integer, Integer, Integer])
	    ),
	    vecof(Integer)
	);

	assert_eq!(
	    List(vec![Integer, Boolean]).least_general_supertype(
		&List(vec![Integer, Boolean, Integer])
	    ),
	    vecof(vt("T"))
	);

	assert_eq!(
	    List(vec![Boolean, Integer]).least_general_supertype(
		&vecof(Integer)
	    ),
	    vecof(vt("T"))
	);

    }

}