1 package org.simantics.scl.compiler.types;
3 import org.simantics.scl.compiler.environment.Environment;
4 import org.simantics.scl.compiler.internal.types.HashCodeUtils;
5 import org.simantics.scl.compiler.types.exceptions.KindUnificationException;
6 import org.simantics.scl.compiler.types.exceptions.UnificationException;
7 import org.simantics.scl.compiler.types.kinds.Kind;
8 import org.simantics.scl.compiler.types.kinds.Kinds;
10 import gnu.trove.map.hash.THashMap;
12 public class Skeletons {
14 public static Type canonicalSkeleton(Type type) {
15 while(type instanceof TMetaVar) {
16 TMetaVar metaVar = (TMetaVar)type;
17 if(metaVar.ref != null)
19 else if(metaVar.skeletonRef != null)
20 type = metaVar.skeletonRef;
27 public static Type canonicalSkeleton(THashMap<TMetaVar,Type> unifications, Type type) {
28 while(type instanceof TMetaVar) {
29 TMetaVar metaVar = (TMetaVar)type;
30 if(metaVar.ref != null)
32 else if(metaVar.skeletonRef != null)
33 type = metaVar.skeletonRef;
35 Type temp = unifications.get(metaVar);
45 public static boolean doesSkeletonContain(THashMap<TMetaVar,Type> unifications, Type type, TMetaVar metaVar) {
46 type = canonicalSkeleton(unifications, type);
49 if(type instanceof TFun) {
50 TFun fun = (TFun)type;
51 return doesSkeletonContain(unifications, fun.domain, metaVar)
52 || doesSkeletonContain(unifications, fun.range, metaVar);
54 if(type instanceof TApply) {
55 TApply apply = (TApply)type;
56 return doesSkeletonContain(unifications, apply.function, metaVar)
57 || doesSkeletonContain(unifications, apply.parameter, metaVar);
59 if(type instanceof TForAll) {
60 TForAll forAll = (TForAll)type;
61 return doesSkeletonContain(unifications, forAll.type, metaVar);
63 if(type instanceof TPred) {
64 TPred pred = (TPred)type;
65 for(Type param : pred.parameters)
66 if(doesSkeletonContain(unifications, param, metaVar))
75 * Returns true, if unification of the skeletons of the types would succeed.
77 public static boolean areSkeletonsCompatible(THashMap<TMetaVar,Type> unifications, Type a, Type b) {
78 a = canonicalSkeleton(unifications, a);
79 b = canonicalSkeleton(unifications, b);
82 Class<?> ca = a.getClass();
83 Class<?> cb = b.getClass();
85 if(ca == TMetaVar.class) {
86 TMetaVar ma = (TMetaVar)a;
87 if(doesSkeletonContain(unifications, b, ma))
89 unifications.put(ma, b);
92 if(cb == TMetaVar.class) {
93 TMetaVar mb = (TMetaVar)b;
94 if(doesSkeletonContain(unifications, a, mb))
96 unifications.put(mb, a);
101 if(ca == TFun.class) {
104 return areSkeletonsCompatible(unifications, funA.domain, funB.domain)
105 && areSkeletonsCompatible(unifications, funA.range, funB.range);
107 if(ca == TApply.class) {
108 TApply applyA = (TApply)a;
109 TApply applyB = (TApply)b;
110 return areSkeletonsCompatible(unifications, applyA.function, applyB.function)
111 && areSkeletonsCompatible(unifications, applyA.parameter, applyB.parameter);
113 if(ca == TPred.class) {
114 TPred predA = (TPred)a;
115 TPred predB = (TPred)b;
116 if(predA.typeClass != predB.typeClass)
118 for(int i=0;i<predA.parameters.length;++i)
119 if(!areSkeletonsCompatible(unifications, predA.parameters[i], predB.parameters[i]))
123 if(ca == TForAll.class) {
124 TForAll forAllA = (TForAll)a;
125 TForAll forAllB = (TForAll)b;
126 TVar temp = Types.var(forAllA.var.getKind());
127 return areSkeletonsCompatible(unifications,
128 forAllA.type.replace(forAllA.var, temp),
129 forAllB.type.replace(forAllB.var, temp));
134 public static void unifySkeletons(Type a, Type b) throws UnificationException {
135 a = canonicalSkeleton(a);
136 b = canonicalSkeleton(b);
140 if(a instanceof TMetaVar) {
141 ((TMetaVar) a).setSkeletonRef(b);
144 if(b instanceof TMetaVar) {
145 ((TMetaVar) b).setSkeletonRef(a);
149 Class<?> ca = a.getClass();
150 Class<?> cb = b.getClass();
152 throw new UnificationException(a, b);
154 if(ca == TApply.class)
155 //unifySkeletons((TApply)a, (TApply)b);
157 else if(ca == TFun.class)
158 unifySkeletons((TFun)a, (TFun)b);
159 else if(ca == TForAll.class)
160 unifySkeletons((TForAll)a, (TForAll)b);
161 else if(ca == TPred.class)
162 //unifySkeletons((TPred)a, (TPred)b);
164 else if(ca == TUnion.class)
165 unifySkeletons((TUnion)a, (TUnion)b);
166 else // ca == TCon.class || ca = TVar.class
167 throw new UnificationException(a, b);
170 public static void unifySkeletons(TFun a, TFun b) throws UnificationException {
171 unifySkeletons(a.domain, b.domain);
172 unifySkeletons(a.range, b.range);
175 public static void unifySkeletons(TApply a, TApply b) throws UnificationException {
176 unifySkeletons(a.function, b.function);
177 unifySkeletons(a.parameter, b.parameter);
180 public static void unifySkeletons(TForAll a, TForAll b) throws UnificationException {
182 Kinds.unify(a.var.getKind(), b.var.getKind());
183 } catch (KindUnificationException e) {
184 throw new UnificationException(a, b);
186 TVar newVar = Types.var(a.var.getKind());
187 unifySkeletons(a.type.replace(a.var, newVar), b.type.replace(b.var, newVar));
190 public static void unifySkeletons(TPred a, TPred b) throws UnificationException {
191 if(a.typeClass != b.typeClass
192 || a.parameters.length != b.parameters.length)
193 throw new UnificationException(a, b);
194 for(int i=0;i<a.parameters.length;++i)
195 unifySkeletons(a.parameters[i], b.parameters[i]);
198 public static void unifySkeletons(TUnion a, TUnion b) throws UnificationException {
202 public static Type commonSkeleton(Environment context, Type[] types) {
203 THashMap<Type[], TMetaVar> metaVarMap = new THashMap<Type[], TMetaVar>() {
205 protected boolean equals(Object a, Object b) {
206 return Types.equals((Type[])a, (Type[])b);
209 protected int hash(Object a) {
210 Type[] types = (Type[])a;
211 int hash = HashCodeUtils.SEED;
212 for(Type type : types)
213 hash = type.hashCode(hash);
217 return commonSkeleton(context, metaVarMap, types);
220 private static TMetaVar metaVarFor(Environment context, THashMap<Type[], TMetaVar> metaVarMap, Type[] types) {
221 TMetaVar result = metaVarMap.get(types);
224 result = Types.metaVar(types[0].inferKind(context));
225 } catch (KindUnificationException e) {
226 result = Types.metaVar(Kinds.STAR);
228 metaVarMap.put(types, result);
234 * Finds the most specific type that can be unified with the all the types
235 * given as a parameter.
237 private static Type commonSkeleton(Environment context, THashMap<Type[], TMetaVar> metaVarMap, Type[] types) {
238 for(int i=0;i<types.length;++i)
239 types[i] = canonicalSkeleton(types[i]);
241 Type first = types[0];
242 Class<?> clazz = first.getClass();
243 for(int i=1;i<types.length;++i)
244 if(types[i].getClass() != clazz)
245 return metaVarFor(context, metaVarMap, types);
247 if(clazz == TCon.class) {
248 for(int i=1;i<types.length;++i)
249 if(types[i] != first)
250 return metaVarFor(context, metaVarMap, types);
253 else if(clazz == TApply.class) {
254 Type[] functions = new Type[types.length];
255 Type[] parameters = new Type[types.length];
256 for(int i=0;i<types.length;++i) {
257 TApply apply = (TApply)types[i];
258 functions[i] = apply.function;
259 parameters[i] = apply.parameter;
262 commonSkeleton(context, metaVarMap, functions),
263 commonSkeleton(context, metaVarMap, parameters));
265 else if(clazz == TFun.class) {
266 Type[] domains = new Type[types.length];
267 Type[] effects = new Type[types.length];
268 Type[] ranges = new Type[types.length];
269 for(int i=0;i<types.length;++i) {
270 TFun fun = (TFun)types[i];
271 if(fun.domain instanceof TPred)
272 return metaVarFor(context, metaVarMap, types);
273 domains[i] = fun.domain;
274 effects[i] = fun.effect;
275 ranges[i] = fun.range;
277 return Types.functionE(
278 commonSkeleton(context, metaVarMap, domains),
279 commonEffect(effects),
280 commonSkeleton(context, metaVarMap, ranges));
283 return metaVarFor(context, metaVarMap, types);
286 private static Type commonEffect(Type[] effects) {
287 Type first = effects[0];
288 for(int i=1;i<effects.length;++i)
289 if(!Types.equals(first, effects[i]))
290 return Types.metaVar(Kinds.EFFECT);
294 public static boolean equalSkeletons(TApply a, TApply b) {
295 return equalSkeletons(a.parameter, b.parameter)
296 && equalSkeletons(a.function , b.function );
299 public static boolean equalSkeletons(TFun a, TFun b) {
300 return equalSkeletons(a.domain, b.domain)
301 && equalSkeletons(a.range, b.range);
304 public static boolean equalSkeletons(TForAll a, TForAll b) {
305 Kind aKind = a.var.getKind();
306 if(!Kinds.equalsCanonical(aKind, b.var.getKind()))
308 TVar newVar = Types.var(aKind);
309 return equalSkeletons(a.type.replace(a.var, newVar), b.type.replace(b.var, newVar));
312 public static boolean equalSkeletons(TPred a, TPred b) {
313 if(a.typeClass != b.typeClass
314 || a.parameters.length != b.parameters.length)
316 Type[] aParameters = a.parameters;
317 Type[] bParameters = b.parameters;
318 for(int i=0;i<aParameters.length;++i)
319 if(!equalSkeletons(aParameters[i], bParameters[i]))
325 * Tests equality of two types. Unbound TVars
326 * are equal only if they are the same variable.
327 * Bound TMetaVar is equal to the type it is bound to.
328 * Unbound TMetaVars are equal only if they are the same metavariable.
329 * Order of predicates and forall quantifiers matters.
331 public static boolean equalSkeletons(Type a, Type b) {
332 a = canonicalSkeleton(a);
333 b = canonicalSkeleton(b);
336 Class<?> ca = a.getClass();
337 Class<?> cb = b.getClass();
340 if(ca == TApply.class)
341 return equalSkeletons((TApply)a, (TApply)b);
342 else if(ca == TFun.class)
343 return equalSkeletons((TFun)a, (TFun)b);
344 else if(ca == TForAll.class)
345 return equalSkeletons((TForAll)a, (TForAll)b);
346 else if(ca == TPred.class)
347 return equalSkeletons((TPred)a, (TPred)b);
348 else // ca == TCon.class
349 // || (ca == TMetaVar.class && a.ref == null && b.ref == null)
350 // || ca = TVar.class
351 return false; // Equals only if a == b, that was already tested