+
+ public static boolean equalSkeletons(TApply a, TApply b) {
+ return equalSkeletons(a.parameter, b.parameter)
+ && equalSkeletons(a.function , b.function );
+ }
+
+ public static boolean equalSkeletons(TFun a, TFun b) {
+ return equalSkeletons(a.domain, b.domain)
+ && equalSkeletons(a.range, b.range);
+ }
+
+ public static boolean equalSkeletons(TForAll a, TForAll b) {
+ Kind aKind = a.var.getKind();
+ if(!Kinds.equalsCanonical(aKind, b.var.getKind()))
+ return false;
+ TVar newVar = Types.var(aKind);
+ return equalSkeletons(a.type.replace(a.var, newVar), b.type.replace(b.var, newVar));
+ }
+
+ public static boolean equalSkeletons(TPred a, TPred b) {
+ if(a.typeClass != b.typeClass
+ || a.parameters.length != b.parameters.length)
+ return false;
+ Type[] aParameters = a.parameters;
+ Type[] bParameters = b.parameters;
+ for(int i=0;i<aParameters.length;++i)
+ if(!equalSkeletons(aParameters[i], bParameters[i]))
+ return false;
+ return true;
+ }
+
+ /**
+ * Tests equality of two types. Unbound TVars
+ * are equal only if they are the same variable.
+ * Bound TMetaVar is equal to the type it is bound to.
+ * Unbound TMetaVars are equal only if they are the same metavariable.
+ * Order of predicates and forall quantifiers matters.
+ */
+ public static boolean equalSkeletons(Type a, Type b) {
+ a = canonicalSkeleton(a);
+ b = canonicalSkeleton(b);
+ if(a == b)
+ return true;
+ Class<?> ca = a.getClass();
+ Class<?> cb = b.getClass();
+ if(ca != cb)
+ return false;
+ if(ca == TApply.class)
+ return equalSkeletons((TApply)a, (TApply)b);
+ else if(ca == TFun.class)
+ return equalSkeletons((TFun)a, (TFun)b);
+ else if(ca == TForAll.class)
+ return equalSkeletons((TForAll)a, (TForAll)b);
+ else if(ca == TPred.class)
+ return equalSkeletons((TPred)a, (TPred)b);
+ else // ca == TCon.class
+ // || (ca == TMetaVar.class && a.ref == null && b.ref == null)
+ // || ca = TVar.class
+ return false; // Equals only if a == b, that was already tested
+ }