TypeSystem.v3

// Copyright 2011 Google Inc. All rights reserved.
// See LICENSE for details of Apache 2.0 license.

// Defines operations on types for type checking.
component TypeSystem {
	// returns {true} if {t1} and {t2} are either the same type, or there is
	// some assignment to type parameters and variables where {t1} and {t2} are
	// the same type.
	def maybeEqual(t1: Type, t2: Type) -> bool {
		if (t1 == t2) return true;
		if (TypeParamType.?(t1) || TypeParamType.?(t2)) return true;
		if (TypeVarType.?(t1) || TypeVarType.?(t2)) return true;
		if (t1.typeCon == t2.typeCon) {
			return Lists.allTrue(t1.nested, t2.nested, maybeEqual);
		}
		return false;
	}
	def isSubtype(t1: Type, t2: Type) -> bool {
		if (t1 == t2) return true;
		match (t2.typeCon.kind) {
			V3Kind.VARIANT => {
				if (V3.isVariant(t1)) {
					for (ct1 = t1; ct1 != null; ct1 = V3.getSuperType(ct1)) {
						if (ct1 == t2) return true;
						if (ct1.typeCon == t2.typeCon) return false;
					}
				}
				return false;
			}
			V3Kind.CLASS => {
				// check subtyping of classes by searching up the inheritance tree.
				if (t1 == Null.TYPE) return true;
				if (V3.isClass(t1)) {
					for (ct1 = t1; ct1 != null; ct1 = V3.getSuperType(ct1)) {
						if (ct1 == t2) return true;
						if (ct1.typeCon == t2.typeCon) return false;
					}
				}
				return false;
			}
			V3Kind.ARRAY, V3Kind.RANGE => {
				// the only subtype of an array or range type is NULL.
				return t1 == Null.TYPE;
			}
			V3Kind.TUPLE => {
				// tuples are co-variantly typed.
				if (V3.isTuple(t1)) return Lists.allTrue(t1.nested, t2.nested, isSubtype);
				return false;
			}
			V3Kind.FUNCREF,
			V3Kind.CLOSURE => {
				if (t1 == Null.TYPE) return true;
				// functions are co-variant in return type and contra-variant in arguments.
				if (V3.isFunction(t1)) {
					var tl1 = t1.nested;
					var tl2 = t2.nested;
					return isSubtype(tl1.tail.head, tl2.tail.head)
						&& isSubtype(tl2.head, tl1.head);
				}
				return false;
			}
			V3Kind.REF => {
				if (t1 == Null.TYPE) return false;
				if (V3.isRef(t1)) {
					for (ct1 = t1; ct1 != null; ct1 = V3.getSuperType(ct1)) {
						if (ct1 == t2) return true;
						if (ct1.typeCon == t2.typeCon) return false;
					}
				}
				return false;
			}
		}
		return false;
	}
	def isPromotable(src: Type, dest: Type) -> bool {
		if (dest == src || isSubtype(src, dest)) return true;
		if (IntType.?(src)) {
			var st = IntType.!(src);
			if (IntType.?(dest)) {
				var dt = IntType.!(dest);
				return isIntPromotable(st, dt);
			}
		}
		var skind = src.typeCon.kind, dkind = dest.typeCon.kind;
		if (skind == V3Kind.TUPLE && dkind == V3Kind.TUPLE) {
			return Lists.allTrue(src.nested, dest.nested, isPromotable);
		}
		if (isEnumToSet(src, dest)) return true;
		if (FloatType.?(dest)) return isPromotableToFloat(src, FloatType.!(dest));
		if (dkind == V3Kind.RANGE && skind == V3Kind.ARRAY) {
			return Lists.allTrue(src.nested, dest.nested, Type.==);
		}
		return false;
	}
	def isIntPromotable(st: IntType, dt: IntType) -> bool {
		if (st == dt) return true;
		if (st.width > dt.width) return false;
		if (st.width == dt.width) return st.signed == dt.signed;
		return dt.signed || st.signed == dt.signed;
	}
	def isPromotableToFloat(src: Type, dtc: FloatType) -> bool {
		if (IntType.?(src)) {
			var st = IntType.!(src);
			if (st.signed) return st.width <= dtc.fraction_width;
			else return st.width <= 1 + dtc.fraction_width;
		}
		if (FloatType.?(src)) {
			var stc = FloatType.!(src);
			return stc.total_width <= dtc.total_width;
		}
		return false;
	}
	def isEnumToSet(ft: Type, tt: Type) -> bool {
		if (EnumType.?(ft) && EnumSetType.?(tt)) {
			return EnumType.!(ft).enumDecl == EnumSetType.!(tt).enumDecl;
		}
		return false;
	}
	def upper(t1: Type, t2: Type) -> Type {
		if (t1 == t2) {
			return t1;
		} else if (t1 == Null.TYPE && isNullable(t2)) {
			return t2;
		} else if (t2 == Null.TYPE && isNullable(t1)) {
			return t1;
		} else if (ClassType.?(t1)) {
			var crt = commonSuperClass(t1, t2);
			return if(crt.0 != null && crt.0 == crt.1, crt.0);
		} else if (V3.isFunction(t1)) {
			if (V3.isFunction(t2)) {
				return mergeLists(t1.nested, t2.nested, Function.CLOSURE, upper);
			}
			return null;
		} else if (V3.isTuple(t1) && V3.isTuple(t2)) {
			return mergeLists(t1.nested, t2.nested, Tuple.TYPECON, upper);
		} else if (V3.isRef(t1) && V3.isRef(t2)) {
			if (isSubtype(t1,t2)) return t2;
			return t1;
		}
		return null;
	}
	def widen(t1: Type, t2: Type) -> Type {
		if (t1 == t2) return t1;
		if (IntType.?(t1)) {
			var i1 = IntType.!(t1);
			if (IntType.?(t2)) {
				var i2 = IntType.!(t2);
				if (isIntPromotable(i1, i2)) return t2;
				if (isIntPromotable(i2, i1)) return t1;
			}
			if (FloatType.?(t2)) {
				if (isPromotableToFloat(t1, FloatType.!(t2))) return t2;
			}
			return null;
		}
		match (t1.typeCon.kind) {
			V3Kind.TUPLE => if(t2.typeCon.kind == V3Kind.TUPLE) return mergeLists(t1.nested, t2.nested, Tuple.TYPECON, widen);
			V3Kind.ENUM => if(isEnumToSet(t1, t2)) return t2;
			V3Kind.ENUM_SET => if (isEnumToSet(t2, t1)) return t1;
			V3Kind.FLOAT => {
				if (isPromotableToFloat(t2, FloatType.!(t1))) return t1;
				if (FloatType.?(t2) && isPromotableToFloat(t1, FloatType.!(t2))) return t2;
			}
		}
		return upper(t1, t2);
	}
	def mergeLists(tl1: List<Type>, tl2: List<Type>, tc: TypeCon, mergefun: (Type, Type) -> Type) -> Type {
		var rl: List<Type>;
		while (tl1 != null) {
			if (tl2 == null) return null;
			var rt = mergefun(tl1.head, tl2.head);
			if (rt == null) return null;
			rl = List.new(rt, rl);
			tl1 = tl1.tail;
			tl2 = tl2.tail;
		}
		if (tl2 == null) return tc.create(Lists.reverse(rl));
		return null;
	}
	def commonSuperClass(t1: Type, t2: Type) -> (Type, Type) {
		if (!ClassType.?(t1)) return (null, null);	// t1 is not a class.
		var ct1 = ClassType.!(t1);
		if (ct1.typeCon == t2.typeCon) return (ct1, t2); // common case: the same class.
		if (!ClassType.?(t2)) return (null, null);	// t2 is not a class.
		var ct2 = ClassType.!(t2);
		var d1 = ct1.getDepth(), d2 = ct2.getDepth();
		while (d1 > d2) { ct1 = ct1.getSuperType(); d1--; }	// walk up ct1 to the same depth
		while (d2 > d1) { ct2 = ct2.getSuperType(); d2--; }	// walk up ct2 to the same depth
		while (d1-- >= 0) {
			if (ct1.typeCon == ct2.typeCon) return (ct1, ct2);
			ct1 = ct1.getSuperType();
			if (ct1 == null) break;
			ct2 = ct2.getSuperType();
			if (ct2 == null) break;
		}
		return (null, null);
	}
	def isNullable(t1: Type) -> bool {
		var kind = t1.typeCon.kind;
		return kind == V3Kind.CLASS || kind == V3Kind.ARRAY || kind == V3Kind.CLOSURE ||
		       kind == V3Kind.RANGE || kind == V3Kind.REF;
	}
	def unifyWiden(t1: Type, t2: Type) {
		unify(t1, t2, true);
	}
	def unifyUpper(t1: Type, t2: Type) {
		unify(t1, t2, false);
	}
	// TODO: unify for structs
	def unify(t1: Type, t2: Type, useWiden: bool) {
		if (TypeVarType.?(t1)) {
			// solve for this type variable
			var tvar = TypeVarType.!(t1);
			if (tvar.vtype == null) {
				tvar.setType(t2);
			} else {
				var sol = if (useWiden, widen(tvar.vtype, t2), upper(tvar.vtype, t2));
				if (sol != null) tvar.setType(sol);
			}
		} else if (t1.open()) {
			// XXX: some adjustments for better inference of class types
			// may help here. For example, marking the existing solution of
			// a type variable as "do not modify" since it is already refers
			// to a nested type of an invariant type constructor

			// solve for any type variables nested in this type
			if (V3.isTuple(t1) && V3.isTuple(t2)) {
				// if both are tuple types, continue with current unification function
				if (useWiden) Lists.reduceV(t1.nested, t2.nested, unifyWiden);
				else Lists.reduceV(t1.nested, t2.nested, unifyUpper);
			} else if (t1.typeCon == t2.typeCon) {
				// if typecons match exactly, use the upper() unification function
				Lists.reduceV(t1.nested, t2.nested, unifyUpper);
			} else {
				var common = commonSuperClass(t1, t2);
				var ct1 = common.0, ct2 = common.1;
				if (ct1 != null && ct2 != null) {
					Lists.reduceV(ct1.nested, ct2.nested, unifyUpper);
				}
			}
		}
	}
	def newTypeQuery(fromType: Type, toType: Type) -> TypeQuery {
		if (fromType == Null.TYPE) return TypeQuery.FALSE;
		if (TypeParamType.?(toType)) return TypeQuery.UNKNOWN_QUERY;
		if (TypeParamType.?(fromType)) return TypeQuery.UNKNOWN_QUERY;
		if (TypeVarType.?(toType)) return TypeQuery.UNKNOWN_QUERY;
		if (TypeVarType.?(fromType)) return TypeQuery.UNKNOWN_QUERY;
		if (V3.isClass(toType)) {
			if (fromType.typeCon.kind != toType.typeCon.kind) return TypeQuery.FALSE;
			var ftc = ClassType.!(fromType), ttc = ClassType.!(toType);
			var fd = ftc.getDepth(), td = ttc.getDepth();
			var query: TypeQuery;
			if (fd < td) {  // downquery
				for (i < (td - fd)) ttc = ttc.getSuperType();
				query = if(ftc.typeCon.kind == V3Kind.CLASS, TypeQuery.CLASS_QUERY, TypeQuery.VARIANT_QUERY);
			} else {  // upquery
				for (i < (fd - td)) ftc = ftc.getSuperType();
				query = if(fromType.typeCon.kind == V3Kind.CLASS, TypeQuery.TRUE_IF_NOT_NULL, TypeQuery.TRUE);
			}
			if (ftc.typeCon == ttc.typeCon) return maybeQuery(ftc, ttc, query, TypeQuery.FALSE);
			return TypeQuery.FALSE;
		}
		if (V3.isTuple(fromType) && V3.isTuple(toType)) {
			return newTupleQuery(fromType, toType);
		}
		if (V3.isFunction(fromType) && V3.isFunction(toType)) {
			// check param and return types
			if (fromType.open() || toType.open()) return TypeQuery.UNKNOWN_QUERY;
			var fl = fromType.nested, tl = toType.nested;
			if (!TypeSystem.isSubtype(fl.tail.head, tl.tail.head)) return TypeQuery.FALSE;
			if (!TypeSystem.isSubtype(tl.head, fl.head)) return TypeQuery.FALSE;
			return TypeQuery.TRUE;
		}
		if (V3.isArray(toType)) return maybeQuery(fromType, toType, TypeQuery.TRUE_IF_NOT_NULL, TypeQuery.FALSE);
		if (fromType == toType) return TypeQuery.TRUE;
		if (IntType.?(fromType)) {
			if (FloatType.?(toType)) return TypeQuery.FLOAT_QUERY_I;
			if (IntType.?(toType)) {
				if (CLOptions.LEGACY_CAST.val) return TypeQuery.FALSE;
				var ft = IntType.!(fromType), tt = IntType.!(toType);
				return if(isIntPromotable(ft, tt), TypeQuery.TRUE, TypeQuery.INT_QUERY_I);
			}
		}
		if (FloatType.?(fromType)) {
			if (IntType.?(toType)) return TypeQuery.INT_QUERY_F;
			if (FloatType.?(toType)) {
				var ftc = FloatType.!(fromType);
				var ttc = FloatType.!(toType);
				if (ftc.total_width < ttc.total_width) return TypeQuery.TRUE;
				return TypeQuery.FLOAT_QUERY_D;
			}
		}
		return maybeQuery(fromType, toType, TypeQuery.TRUE, TypeQuery.FALSE);
	}
	def newTypeCast(fromType: Type, toType: Type) -> TypeCast {
		if (fromType == toType) return TypeCast.TRUE;
		if (toType == Void.TYPE && CLOptions.LEGACY_CAST.val) return TypeCast.VOID_CAST;
		if (TypeParamType.?(toType)) return TypeCast.UNKNOWN_CAST;
		if (TypeParamType.?(fromType)) return TypeCast.UNKNOWN_CAST;
		if (TypeVarType.?(toType)) return TypeCast.UNKNOWN_CAST;
		if (TypeVarType.?(fromType)) return TypeCast.UNKNOWN_CAST;
		if (V3.isClass(toType)) {
			if (fromType == Null.TYPE) return TypeCast.TRUE;
			if (fromType.typeCon.kind != toType.typeCon.kind) return TypeCast.THROW;
			var ftc = ClassType.!(fromType), ttc = ClassType.!(toType);
			var fd = ftc.getDepth(), td = ttc.getDepth();
			var cast: TypeCast;
			if (fd <= td) {  // downcast
				for (i < (td - fd)) ttc = ttc.getSuperType();
				cast = if(ftc.typeCon.kind == V3Kind.CLASS, TypeCast.CLASS_CAST, TypeCast.VARIANT_CAST);
			} else {  // upcast (subsumption)
				for (i < (fd - td)) ftc = ftc.getSuperType();
				cast = TypeCast.TRUE;
			}
			var not = if(fromType.typeCon.kind == V3Kind.CLASS, TypeCast.THROW_IF_NOT_NULL, TypeCast.THROW);
			if (ftc.typeCon == ttc.typeCon) return maybeCast(ftc, ttc, cast, not);
			return not;
		}
		if (V3.isTuple(fromType) && V3.isTuple(toType)) {
			return newTupleCast(fromType, toType);
		}
		if (V3.isFunction(fromType)) {
			if (fromType == Null.TYPE) return TypeCast.TRUE;
			if (V3.isFunction(toType)) {
				// check param and return types
				if (fromType.open() || toType.open()) return TypeCast.UNKNOWN_CAST;
				var fl = fromType.nested, tl = toType.nested;
				if (!TypeSystem.isSubtype(fl.tail.head, tl.tail.head)) return TypeCast.THROW;
				if (!TypeSystem.isSubtype(tl.head, fl.head)) return TypeCast.THROW;
				return TypeCast.TRUE;
			}
		}
		if (V3.isArray(toType)) {
			if (fromType == Null.TYPE) return TypeCast.TRUE;
			return maybeCast(fromType, toType, TypeCast.TRUE, TypeCast.THROW);
		}
		if (V3.isVariant(fromType)) {
			return maybeCast(fromType, toType, TypeCast.TRUE, TypeCast.THROW);
		}
		if (IntType.?(fromType)) {
			if (IntType.?(toType)) {
				if (CLOptions.LEGACY_CAST.val) return TypeCast.INT_VIEW_I;
				var ft = IntType.!(fromType), tt = IntType.!(toType);
				return if(isIntPromotable(ft, tt), TypeCast.INT_VIEW_I, TypeCast.INT_CAST_I);
			}
			if (FloatType.?(toType)) {
				return if(isPromotableToFloat(fromType,
					FloatType.!(toType)), TypeCast.FLOAT_PROMOTE_I, TypeCast.FLOAT_CAST_I);
			}
		}
		if (FloatType.?(fromType)) {
			if (IntType.?(toType)) return TypeCast.INT_CAST_F;
			var ftc = FloatType.!(fromType);
			if (FloatType.?(toType)) {
				var ttc = FloatType.!(toType);
				if (ftc.total_width < ttc.total_width) return TypeCast.FLOAT_PROMOTE_F;
				if (ftc.total_width > ttc.total_width) return TypeCast.FLOAT_CAST_D;
			}
		}
		if (isEnumToSet(fromType, toType)) return TypeCast.ENUM_TO_SET;
		if (V3.isRange(toType)) {
			if (fromType == Null.TYPE) return TypeCast.TRUE;
			if (V3.isArray(fromType)) {
				return maybeCast(fromType.nested.head, toType.nested.head, TypeCast.RANGE_PROMOTE_ARRAY, TypeCast.THROW);
			}
			return maybeCast(fromType, toType, TypeCast.TRUE, TypeCast.THROW);
		}
		if (V3.isRef(fromType)) {
			if (isSubtype(fromType, toType)) return TypeCast.TRUE;
		}
		return TypeCast.THROW;
	}
	def maybeQuery(t1: Type, t2: Type, eq: TypeQuery, neq: TypeQuery) -> TypeQuery {
		if (t1 == t2) return eq;
		if (TypeSystem.maybeEqual(t1, t2)) return TypeQuery.UNKNOWN_QUERY;
		return neq;
	}
	def maybeCast(t1: Type, t2: Type, eq: TypeCast, neq: TypeCast) -> TypeCast {
		if (t1 == t2) return eq;
		if (TypeSystem.maybeEqual(t1, t2)) return TypeCast.UNKNOWN_CAST;
		return neq;
	}
	def newTupleQuery(ff: Type, tt: Type) -> TypeQuery {
		// recursively check all nested types
		var fl = ff.nested, tl = tt.nested;
		while (fl != null) {
			if (tl == null) return TypeQuery.FALSE; // tuple size doesnt match
			var inner = TypeSystem.newTypeQuery(fl.head, tl.head);
			if (inner == TypeQuery.FALSE) return TypeQuery.FALSE;
			fl = fl.tail;
			tl = tl.tail;
		}
		if (tl != null) return TypeQuery.FALSE; // tuple size doesnt match
		return TypeQuery.TUPLE_QUERY;
	}
	def newTupleCast(ff: Type, tt: Type) -> TypeCast {
		// recursively check all nested types
		var fl = ff.nested, tl = tt.nested;
		while (fl != null) {
			if (tl == null) return TypeCast.THROW; // tuple size doesnt match
			if (TypeSystem.newTypeCast(fl.head, tl.head) == TypeCast.THROW) return TypeCast.THROW;
			fl = fl.tail;
			tl = tl.tail;
		}
		if (tl != null) return TypeCast.THROW; // tuple size doesnt match
		return TypeCast.TUPLE_CAST;
	}
	def isIntToLong(ft: IntType, tt: IntType) -> bool {
		return ft.width <= 32 && tt.width > 32;
	}
}
// enumeration of the different kinds of type casts
enum TypeCast {
	UNKNOWN_CAST,
	VOID_CAST,
	TRUE,
	SUBSUME,
	THROW_IF_NOT_NULL,
	THROW,
	INT_VIEW_I,
	INT_CAST_I,
	FLOAT_CAST_I,
	INT_CAST_F,
	FLOAT_PROMOTE_F,
	FLOAT_PROMOTE_I,
	FLOAT_CAST_D,
	CLASS_CAST,
	VARIANT_CAST,
	TUPLE_CAST,
	ENUM_TO_SET,
	RANGE_PROMOTE_ARRAY
}
// enumeration of the different kinds of type queries
enum TypeQuery {
	UNKNOWN_QUERY,
	TRUE,
	TRUE_IF_NOT_NULL,
	FALSE,
	FLOAT_QUERY_I,
	INT_QUERY_F,
	INT_QUERY_I,
	FLOAT_QUERY_D,
	CLASS_QUERY,
	VARIANT_QUERY,
	TUPLE_QUERY
}