bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/internal/elaboration/subsumption/SubSolver.java

   1 package org.simantics.scl.compiler.internal.elaboration.subsumption;
   2
   3 import java.util.ArrayDeque;
   4 import java.util.ArrayList;
   5
   6 import org.simantics.scl.compiler.errors.ErrorLog;
   7 import org.simantics.scl.compiler.errors.Locations;
   8 import org.simantics.scl.compiler.internal.types.effects.EffectIdMap;
   9 import org.simantics.scl.compiler.types.TMetaVar;
  10 import org.simantics.scl.compiler.types.TUnion;
  11 import org.simantics.scl.compiler.types.Type;
  12 import org.simantics.scl.compiler.types.Types;
  13 import org.simantics.scl.compiler.types.util.Polarity;
  14 import org.simantics.scl.compiler.types.util.TypeUnparsingContext;
  15
  16 import gnu.trove.map.hash.THashMap;
  17 import gnu.trove.set.hash.THashSet;
  18
  19 public class SubSolver {
  20
  21     public static final boolean DEBUG = false;
  22
  23     long globalLoc;
  24     ErrorLog errorLog;
  25     ArrayList<Subsumption> subsumptions;
  26     ArrayList<Type> potentialSingletonEffects;
  27     EffectIdMap effectIds = new EffectIdMap();
  28     THashMap<TMetaVar,Var> vars = new THashMap<TMetaVar,Var>();
  29     ArrayDeque<Var> dirtyQueue = new ArrayDeque<Var>();
  30
  31     TypeUnparsingContext tuc = new TypeUnparsingContext();
  32
  33     public SubSolver(ErrorLog errorLog, ArrayList<Subsumption> subsumptions,
  34             ArrayList<Type> potentialSingletonEffects,
  35             long globalLoc) {
  36         this.errorLog = errorLog;
  37         this.subsumptions = subsumptions;
  38         this.potentialSingletonEffects = potentialSingletonEffects;
  39         this.globalLoc = globalLoc;
  40
  41         //for(Subsumption sub : subsumptions)
  42         //    System.out.println("[" + sub.a.toString(tuc) + " < " + sub.b.toString(tuc) + "]");
  43     }
  44
  45     public void solve() {
  46         //System.out.println("--------------------------------------------------");
  47         //printSubsumptions();
  48         createVar();
  49         //print();
  50         reduceChains();
  51         propagateUpperBounds();
  52         checkLowerBounds();
  53         //errorFromUnsolvedEquations();
  54         //print();
  55     }
  56
  57     private void markAllDirty() {
  58         for(Var v : vars.values())
  59             v.markDirty();
  60     }
  61
  62     private Var getOrCreateVar(TMetaVar mv) {
  63         Var var = vars.get(mv);
  64         if(var == null) {
  65             var = new Var(mv, mv.toString(tuc).substring(1), this);
  66             vars.put(mv, var);
  67         }
  68         return var;
  69     }
  70
  71     private void addVar(Type t) {
  72         t = Types.canonical(t);
  73         if(t instanceof TMetaVar)
  74             getOrCreateVar((TMetaVar)t);
  75         else if(t instanceof TUnion)
  76             for(Type c : ((TUnion)t).effects)
  77                 addVar(c);
  78     }
  79
  80     ArrayList<TMetaVar> aVars = new ArrayList<TMetaVar>();
  81
  82     private void addSubsumption(long loc, Type a, Type b) {
  83         int aCons = effectIds.toId(a, aVars);
  84         if(!aVars.isEmpty()) {
  85             for(TMetaVar var : aVars)
  86                 getOrCreateVar((TMetaVar)var).addUpperBound(toVUnion(b));
  87             aVars.clear();
  88         }
  89         if(aCons != 0) {
  90             VUnion u = toVUnion(b);
  91             if(u.vars.isEmpty()) {
  92                 testSubsumption(loc, aCons, u.con);
  93             }
  94             else
  95                 u.makeLowerBound(aCons);
  96         }
  97     }
  98
  99     ArrayList<TMetaVar> bVars = new ArrayList<TMetaVar>();
 100
 101     private VUnion toVUnion(Type a) {
 102         int cons = effectIds.toId(a, bVars);
 103         ArrayList<Var> vars = new ArrayList<Var>(bVars.size());
 104         for(TMetaVar v : bVars)
 105             vars.add(getOrCreateVar(v));
 106         bVars.clear();
 107         return new VUnion(cons, vars);
 108     }
 109
 110     private void createVar() {
 111         for(Subsumption sub : subsumptions)
 112             addSubsumption(sub.loc, sub.a, sub.b);
 113         // In some cases there might be types that are not part of any subsumption, for example related to typeOf
 114         for(Type t : potentialSingletonEffects)
 115             addVar(t);
 116     }
 117
 118     private void reduceChains() {
 119         markAllDirty();
 120         while(true) {
 121             Var v = dirtyQueue.poll();
 122             if(v == null)
 123                 break;
 124
 125             reduceChains(v);
 126             v.dirty = false;
 127         }
 128     }
 129
 130     private void reduceChains(Var v) {
 131         if(v.constLowerBound == v.constUpperBound) {
 132             v.replaceWith(v.constLowerBound);
 133             return;
 134         }
 135         Polarity p = v.original.getPolarity();
 136         if(!p.isNegative() && v.complexLowerBounds.isEmpty()) {
 137             if(v.simpleLowerBounds.isEmpty()) {
 138                 if((v.constLowerBound&v.constUpperBound) != v.constLowerBound)
 139                     errorLog.log(globalLoc, "Subsumption failed.");
 140                 v.replaceWith(v.constLowerBound);
 141                 return;
 142             }
 143             else if(v.simpleLowerBounds.size() == 1 && v.constLowerBound == 0) {
 144                 v.replaceDownwards(v.simpleLowerBounds.get(0));
 145                 return;
 146             }
 147         }
 148         if(p == Polarity.NEGATIVE && v.complexUpperBounds.isEmpty()) {
 149             if(v.simpleUpperBounds.isEmpty()) {
 150                 if((v.constLowerBound&v.constUpperBound) != v.constLowerBound)
 151                     errorLog.log(globalLoc, "Subsumption failed.");
 152                 v.replaceWith(v.constUpperBound);
 153                 return;
 154             }
 155             else if(v.simpleUpperBounds.size() == 1 && v.constUpperBound == EffectIdMap.MAX) {
 156                 v.replaceUpwards(v.simpleUpperBounds.get(0));
 157                 return;
 158             }
 159         }
 160     }
 161
 162     private void propagateUpperBounds() {
 163         markAllDirty();
 164         while(true) {
 165             Var v = dirtyQueue.poll();
 166             if(v == null)
 167                 break;
 168
 169             int upperApprox = v.constUpperBound;
 170             for(Var u : v.simpleUpperBounds)
 171                 upperApprox &= u.upperApprox;
 172             for(VUnion u : v.complexUpperBounds)
 173                 upperApprox &= u.getUpperApprox();
 174
 175             if(upperApprox != v.upperApprox) {
 176                 v.upperApprox = upperApprox;
 177                 for(Var u : v.simpleLowerBounds)
 178                     u.markDirty();
 179                 for(VUnion u : v.complexLowerBounds)
 180                     if(u.low != null)
 181                         u.low.markDirty();
 182             }
 183
 184             v.dirty = false;
 185         }
 186     }
 187
 188     private void checkLowerBounds() {
 189         THashSet<VUnion> lowerBounds = new THashSet<VUnion>();
 190         for(Var v : vars.values()) {
 191             if((v.constLowerBound & v.upperApprox) != v.constLowerBound)
 192                 testSubsumption(globalLoc, v.constLowerBound, v.upperApprox);
 193             for(VUnion u : v.complexLowerBounds)
 194                 if(u.low == null)
 195                     lowerBounds.add(u);
 196         }
 197         for(VUnion u : lowerBounds)
 198             if(u.getUpperApprox() != EffectIdMap.MAX)
 199                 errorLog.log(globalLoc, "Subsumption failed.");
 200     }
 201
 202     private void errorFromUnsolvedEquations() {
 203         for(Var v : vars.values()) {
 204             if(!v.isFree()) {
 205                 errorLog.log(globalLoc, "Couldn't simplify all effect subsumptions away. " +
 206                                 "The current compiler cannot handle this situation. Try adding more type annotations.");
 207                 break;
 208             }
 209         }
 210     }
 211
 212     private void print() {
 213         for(Var v : vars.values()) {
 214             System.out.println(v.name +
 215                     ", " + v.original.getPolarity() +
 216                     (v.simpleLowerBounds.isEmpty() ? "" : ", simpleLowerRefs: " + v.simpleLowerBounds.size()) +
 217                     (v.complexLowerBounds.isEmpty() ? "" : ", complexLowerRefs: " + v.complexLowerBounds.size()) +
 218                     ", " + v.original.getKind());
 219             if(v.constLowerBound != EffectIdMap.MIN)
 220                 System.out.println("    > " + v.constLowerBound);
 221             if(v.constUpperBound != EffectIdMap.MAX)
 222                 System.out.println("    < " + v.constUpperBound);
 223             for(Var u : v.simpleUpperBounds)
 224                 System.out.println("    < " + u.name);
 225             for(VUnion u : v.complexUpperBounds)
 226                 System.out.println("    << " + u);
 227         }
 228     }
 229
 230     private void printSubsumptions() {
 231         for(Subsumption sub : subsumptions)
 232             System.out.println("[" + sub.a.toString(tuc) + " < " + sub.b.toString(tuc) + " : " +
 233                     Locations.beginOf(sub.loc) + "," + Locations.endOf(sub.loc) + "]");
 234     }
 235
 236     private void testSubsumption(long location, int a, int b) {
 237         int extraEffects = a & (~b);
 238         if(extraEffects != 0)
 239             subsumptionFailed(location, extraEffects);
 240     }
 241
 242     private void subsumptionFailed(long location , int effects) {
 243         errorLog.log(location, "Side-effect " + effectIds.toType(effects) + " is forbidden here.");
 244     }
 245 }