--- /dev/null
+package org.simantics.scl.compiler.internal.elaboration.subsumption;\r
+\r
+import gnu.trove.map.hash.THashMap;\r
+import gnu.trove.set.hash.THashSet;\r
+\r
+import java.util.ArrayDeque;\r
+import java.util.ArrayList;\r
+\r
+import org.simantics.scl.compiler.errors.ErrorLog;\r
+import org.simantics.scl.compiler.errors.Locations;\r
+import org.simantics.scl.compiler.internal.types.effects.EffectIdMap;\r
+import org.simantics.scl.compiler.types.TMetaVar;\r
+import org.simantics.scl.compiler.types.TUnion;\r
+import org.simantics.scl.compiler.types.Type;\r
+import org.simantics.scl.compiler.types.Types;\r
+import org.simantics.scl.compiler.types.util.Polarity;\r
+import org.simantics.scl.compiler.types.util.TypeUnparsingContext;\r
+\r
+public class SubSolver {\r
+\r
+ public static final boolean DEBUG = false;\r
+ \r
+ long globalLoc;\r
+ ErrorLog errorLog;\r
+ ArrayList<Subsumption> subsumptions;\r
+ ArrayList<Type> potentialSingletonEffects;\r
+ EffectIdMap effectIds = new EffectIdMap();\r
+ THashMap<TMetaVar,Var> vars = new THashMap<TMetaVar,Var>();\r
+ ArrayDeque<Var> dirtyQueue = new ArrayDeque<Var>();\r
+ \r
+ TypeUnparsingContext tuc = new TypeUnparsingContext();\r
+ \r
+ public SubSolver(ErrorLog errorLog, ArrayList<Subsumption> subsumptions,\r
+ ArrayList<Type> potentialSingletonEffects,\r
+ long globalLoc) {\r
+ this.errorLog = errorLog;\r
+ this.subsumptions = subsumptions;\r
+ this.potentialSingletonEffects = potentialSingletonEffects;\r
+ this.globalLoc = globalLoc;\r
+ \r
+ //for(Subsumption sub : subsumptions)\r
+ // System.out.println("[" + sub.a.toString(tuc) + " < " + sub.b.toString(tuc) + "]");\r
+ } \r
+ \r
+ public void solve() {\r
+ //printSubsumptions();\r
+ createVar();\r
+ //print();\r
+ reduceChains();\r
+ propagateUpperBounds();\r
+ checkLowerBounds();\r
+ errorFromUnsolvedEquations();\r
+ //System.out.println("--");\r
+ //print();\r
+ }\r
+ \r
+ private void markAllDirty() {\r
+ for(Var v : vars.values())\r
+ v.markDirty();\r
+ }\r
+ \r
+ private Var getOrCreateVar(TMetaVar mv) {\r
+ Var var = vars.get(mv);\r
+ if(var == null) {\r
+ var = new Var(mv, mv.toString(tuc).substring(1), this);\r
+ vars.put(mv, var);\r
+ }\r
+ return var;\r
+ }\r
+\r
+ private void addVar(Type t) {\r
+ t = Types.canonical(t);\r
+ if(t instanceof TMetaVar)\r
+ getOrCreateVar((TMetaVar)t);\r
+ else if(t instanceof TUnion)\r
+ for(Type c : ((TUnion)t).effects)\r
+ addVar(c);\r
+ }\r
+\r
+ ArrayList<TMetaVar> aVars = new ArrayList<TMetaVar>();\r
+ \r
+ private void addSubsumption(long loc, Type a, Type b) {\r
+ int aCons = effectIds.toId(a, aVars);\r
+ if(!aVars.isEmpty()) {\r
+ for(TMetaVar var : aVars)\r
+ getOrCreateVar((TMetaVar)var).addUpperBound(toVUnion(b));\r
+ aVars.clear();\r
+ } \r
+ if(aCons != 0) {\r
+ VUnion u = toVUnion(b);\r
+ if(u.vars.isEmpty()) {\r
+ testSubsumption(loc, aCons, u.con);\r
+ }\r
+ else\r
+ u.makeLowerBound(aCons);\r
+ }\r
+ }\r
+\r
+ ArrayList<TMetaVar> bVars = new ArrayList<TMetaVar>();\r
+ \r
+ private VUnion toVUnion(Type a) {\r
+ int cons = effectIds.toId(a, bVars);\r
+ ArrayList<Var> vars = new ArrayList<Var>(bVars.size());\r
+ for(TMetaVar v : bVars)\r
+ vars.add(getOrCreateVar(v));\r
+ bVars.clear();\r
+ return new VUnion(cons, vars);\r
+ }\r
+\r
+ private void createVar() {\r
+ for(Subsumption sub : subsumptions)\r
+ addSubsumption(sub.loc, sub.a, sub.b);\r
+ for(Type t : potentialSingletonEffects)\r
+ addVar(t);\r
+ }\r
+ \r
+ private void reduceChains() {\r
+ markAllDirty();\r
+ while(true) {\r
+ Var v = dirtyQueue.poll();\r
+ if(v == null)\r
+ break;\r
+ \r
+ reduceChains(v);\r
+ v.dirty = false;\r
+ }\r
+ }\r
+ \r
+ private void reduceChains(Var v) {\r
+ if(v.constLowerBound == v.constUpperBound) {\r
+ v.replaceWith(v.constLowerBound);\r
+ return;\r
+ }\r
+ Polarity p = v.original.getPolarity();\r
+ if(!p.isNegative() && v.complexLowerBounds.isEmpty()) {\r
+ if(v.simpleLowerBounds.isEmpty()) {\r
+ if((v.constLowerBound&v.constUpperBound) != v.constLowerBound)\r
+ errorLog.log(globalLoc, "Subsumption failed.");\r
+ v.replaceWith(v.constLowerBound);\r
+ return;\r
+ }\r
+ else if(v.simpleLowerBounds.size() == 1 && v.constLowerBound == 0) {\r
+ v.replaceDownwards(v.simpleLowerBounds.get(0));\r
+ return;\r
+ }\r
+ }\r
+ if(p == Polarity.NEGATIVE && v.complexUpperBounds.isEmpty()) {\r
+ if(v.simpleUpperBounds.isEmpty()) {\r
+ if((v.constLowerBound&v.constUpperBound) != v.constLowerBound)\r
+ errorLog.log(globalLoc, "Subsumption failed.");\r
+ v.replaceWith(v.constUpperBound);\r
+ return;\r
+ }\r
+ else if(v.simpleUpperBounds.size() == 1 && v.constUpperBound == EffectIdMap.MAX) {\r
+ v.replaceUpwards(v.simpleUpperBounds.get(0));\r
+ return;\r
+ }\r
+ }\r
+ }\r
+ \r
+ private void propagateUpperBounds() {\r
+ markAllDirty(); \r
+ while(true) {\r
+ Var v = dirtyQueue.poll();\r
+ if(v == null)\r
+ break;\r
+ \r
+ int upperApprox = v.constUpperBound;\r
+ for(Var u : v.simpleUpperBounds)\r
+ upperApprox &= u.upperApprox;\r
+ for(VUnion u : v.complexUpperBounds)\r
+ upperApprox &= u.getUpperApprox();\r
+ \r
+ if(upperApprox != v.upperApprox) {\r
+ v.upperApprox = upperApprox;\r
+ for(Var u : v.simpleLowerBounds)\r
+ u.markDirty();\r
+ for(VUnion u : v.complexLowerBounds)\r
+ if(u.low != null)\r
+ u.low.markDirty();\r
+ } \r
+ \r
+ v.dirty = false;\r
+ }\r
+ }\r
+ \r
+ private void checkLowerBounds() {\r
+ THashSet<VUnion> lowerBounds = new THashSet<VUnion>(); \r
+ for(Var v : vars.values()) {\r
+ if((v.constLowerBound & v.upperApprox) != v.constLowerBound)\r
+ testSubsumption(globalLoc, v.constLowerBound, v.upperApprox);\r
+ for(VUnion u : v.complexLowerBounds)\r
+ if(u.low == null)\r
+ lowerBounds.add(u);\r
+ }\r
+ for(VUnion u : lowerBounds)\r
+ if(u.getUpperApprox() != EffectIdMap.MAX)\r
+ errorLog.log(globalLoc, "Subsumption failed.");\r
+ }\r
+\r
+ private void errorFromUnsolvedEquations() {\r
+ for(Var v : vars.values()) {\r
+ if(!v.isFree()) {\r
+ errorLog.log(globalLoc, "Couldn't simplify all effect subsumptions away. " +\r
+ "The current compiler cannot handle this situation. Try adding more type annotations.");\r
+ break;\r
+ }\r
+ }\r
+ }\r
+ \r
+ private void print() {\r
+ for(Var v : vars.values()) {\r
+ System.out.println(v.name + \r
+ ", " + v.original.getPolarity() + \r
+ (v.simpleLowerBounds.isEmpty() ? "" : ", simpleLowerRefs: " + v.simpleLowerBounds.size()) + \r
+ (v.complexLowerBounds.isEmpty() ? "" : ", complexLowerRefs: " + v.complexLowerBounds.size()) +\r
+ ", " + v.original.getKind());\r
+ if(v.constLowerBound != EffectIdMap.MIN)\r
+ System.out.println(" > " + v.constLowerBound);\r
+ if(v.constUpperBound != EffectIdMap.MAX)\r
+ System.out.println(" < " + v.constUpperBound);\r
+ for(Var u : v.simpleUpperBounds)\r
+ System.out.println(" < " + u.name);\r
+ for(VUnion u : v.complexUpperBounds)\r
+ System.out.println(" << " + u);\r
+ }\r
+ }\r
+ \r
+ private void printSubsumptions() {\r
+ for(Subsumption sub : subsumptions)\r
+ System.out.println("[" + sub.a.toString(tuc) + " < " + sub.b.toString(tuc) + " : " + \r
+ Locations.beginOf(sub.loc) + "," + Locations.endOf(sub.loc) + "]");\r
+ }\r
+\r
+ private void testSubsumption(long location, int a, int b) {\r
+ int extraEffects = a & (~b);\r
+ if(extraEffects != 0)\r
+ subsumptionFailed(location, extraEffects);\r
+ }\r
+ \r
+ private void subsumptionFailed(long location , int effects) {\r
+ errorLog.log(location, "Side-effect " + effectIds.toType(effects) + " is forbidden here.");\r
+ }\r
+}\r