bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/internal/elaboration/subsumption2/SubSolver2.java

   1 package org.simantics.scl.compiler.internal.elaboration.subsumption2;
   2
   3 import java.util.ArrayDeque;
   4 import java.util.ArrayList;
   5 import java.util.Arrays;
   6
   7 import org.simantics.scl.compiler.errors.ErrorLog;
   8 import org.simantics.scl.compiler.internal.elaboration.subsumption.Subsumption;
   9 import org.simantics.scl.compiler.internal.elaboration.subsumption2.SubsumptionGraph.LowerBoundSource;
  10 import org.simantics.scl.compiler.internal.elaboration.subsumption2.SubsumptionGraph.Node;
  11 import org.simantics.scl.compiler.internal.elaboration.subsumption2.SubsumptionGraph.PartOfUnion;
  12 import org.simantics.scl.compiler.internal.elaboration.subsumption2.SubsumptionGraph.Sub;
  13 import org.simantics.scl.compiler.internal.elaboration.subsumption2.SubsumptionGraph.UnionNode;
  14 import org.simantics.scl.compiler.internal.elaboration.subsumption2.SubsumptionGraph.VarNode;
  15 import org.simantics.scl.compiler.internal.types.effects.EffectIdMap;
  16 import org.simantics.scl.compiler.types.TMetaVar;
  17 import org.simantics.scl.compiler.types.util.Polarity;
  18
  19 import gnu.trove.map.hash.THashMap;
  20 import gnu.trove.map.hash.TIntIntHashMap;
  21 import gnu.trove.set.hash.THashSet;
  22
  23 public class SubSolver2 {
  24     public static final boolean DEBUG = false;
  25
  26     // Input
  27     private final ErrorLog errorLog;
  28     private final ArrayList<Subsumption> subsumptions;
  29
  30     //
  31     private final EffectIdMap effectIds = new EffectIdMap();
  32     private final THashMap<TMetaVar, VarNode> varNodeMap = new THashMap<TMetaVar, VarNode>();
  33     private final ArrayList<UnionNode> unionNodes = new ArrayList<UnionNode>();
  34
  35     private static TIntIntHashMap STATISTICS = new TIntIntHashMap();
  36
  37     private SubSolver2(ErrorLog errorLog, ArrayList<Subsumption> subsumptions) {
  38         this.errorLog = errorLog;
  39         this.subsumptions = subsumptions;
  40         /*if(subsumptions.size() == 1) {
  41             TypeUnparsingContext tuc = new TypeUnparsingContext();
  42             Subsumption sub = subsumptions.get(0);
  43             if(sub.a instanceof TCon && sub.b instanceof TCon)
  44                 System.out.println("caseCC");
  45             else if(sub.a instanceof TMetaVar && sub.b instanceof TCon)
  46                 System.out.println("caseMC");
  47             else if(sub.a instanceof TVar && sub.b instanceof TCon)
  48                 System.out.println("caseVC");
  49             System.out.println("    " + sub.a.toString(tuc) + " < " + sub.b.toString(tuc));
  50         }
  51         synchronized(STATISTICS) {
  52             STATISTICS.adjustOrPutValue(subsumptions.size(), 1, 1);
  53             showStatistics();
  54         }*/
  55     }
  56
  57     public static void showStatistics() {
  58         System.out.println("---");
  59         int[] keys = STATISTICS.keys();
  60         Arrays.sort(keys);
  61         int sum = 0;
  62         for(int key : keys)
  63             sum += STATISTICS.get(key);
  64         for(int key : keys) {
  65             int value = STATISTICS.get(key);
  66             System.out.println(key + ": " + value + " (" + (value*100.0/sum) + "%)");
  67         }
  68     }
  69
  70     private static boolean subsumes(int a, int b) {
  71         return (a&b) == a;
  72     }
  73
  74     private void processSubsumptions() {
  75         ArrayList<TMetaVar> aVars = new ArrayList<TMetaVar>(2);
  76         ArrayList<TMetaVar> bVars = new ArrayList<TMetaVar>(2);
  77         for(Subsumption subsumption : subsumptions) {
  78             int aCons = effectIds.toId(subsumption.a, aVars);
  79             int bCons = effectIds.toId(subsumption.b, bVars);
  80
  81             if(bVars.isEmpty()) {
  82                 if(!subsumes(aCons, bCons)) {
  83                     reportSubsumptionFailure(subsumption.loc, aCons, bCons);
  84                     continue;
  85                 }
  86                 for(TMetaVar aVar : aVars)
  87                     getOrCreateNode(aVar).upperBound &= bCons;
  88             }
  89             else {
  90                 Node bNode;
  91                 if(bVars.size() == 1 && bCons == 0)
  92                     bNode = getOrCreateNode(bVars.get(0));
  93                 else
  94                     bNode = createUnion(subsumption.loc, bCons, bVars);
  95                 if(aCons != 0)
  96                     setLowerBound(subsumption.loc, aCons, bNode);
  97                 for(TMetaVar aVar : aVars)
  98                     new Sub(getOrCreateNode(aVar), bNode);
  99                 bVars.clear();
 100             }
 101             aVars.clear();
 102         }
 103     }
 104
 105     private void setLowerBound(long location, int lower, Node node) {
 106         node.lowerBound |= lower;
 107         node.addLowerBoundSource(location, lower);
 108     }
 109
 110     private UnionNode createUnion(long location, int cons, ArrayList<TMetaVar> vars) {
 111         UnionNode node = new UnionNode(location, cons);
 112         for(TMetaVar var : vars)
 113             new PartOfUnion(getOrCreateNode(var), node);
 114         unionNodes.add(node);
 115         return node;
 116     }
 117
 118     private VarNode getOrCreateNode(TMetaVar var) {
 119         VarNode node = varNodeMap.get(var);
 120         if(node == null) {
 121             node = new VarNode(var);
 122             varNodeMap.put(var, node);
 123         }
 124         return node;
 125     }
 126
 127     public boolean solve() {
 128         //System.out.println("------------------------------------------------------");
 129         int errorCount = errorLog.getErrorCount();
 130
 131         // Check errors
 132         processSubsumptions();
 133         propagateUpperBounds();
 134         checkLowerBounds();
 135
 136         if(DEBUG)
 137             print();
 138
 139         if(errorLog.getErrorCount() != errorCount)
 140             return false;
 141
 142         // Simplify constraints
 143         stronglyConnectedComponents();
 144         propagateLowerBounds();
 145         simplify();
 146
 147         if(DEBUG)
 148             print();
 149
 150         return true;
 151     }
 152
 153     private void touchNeighborhood(VarNode node) {
 154         for(Sub cur=node.lower;cur!=null;cur=cur.bNext)
 155             touch(cur.a);
 156         for(Sub cur=node.upper;cur!=null;cur=cur.aNext)
 157             touch(cur.b);
 158         for(PartOfUnion cur=node.partOf;cur!=null;cur=cur.aNext)
 159             touch(cur.b);
 160     }
 161
 162     private void touchNeighborhood(UnionNode node) {
 163         for(Sub cur=node.lower;cur!=null;cur=cur.bNext)
 164             touch(cur.a);
 165         for(PartOfUnion cur=node.parts;cur!=null;cur=cur.bNext)
 166             touch(cur.a);
 167     }
 168
 169     THashSet<Node> set = new THashSet<Node>();
 170     private void simplify() {
 171         for(VarNode node : sortedNodes) {
 172             if(node.index == SubsumptionGraph.REMOVED)
 173                 continue;
 174             activeSet.add(node);
 175             queue.addLast(node);
 176         }
 177         for(UnionNode node : unionNodes) {
 178             if(node.constPart == SubsumptionGraph.REMOVED)
 179                 continue;
 180             activeSet.add(node);
 181             queue.addLast(node);
 182         }
 183
 184         while(!queue.isEmpty()) {
 185             Node node_ = queue.removeFirst();
 186             activeSet.remove(node_);
 187             if(node_ instanceof VarNode) {
 188                 VarNode node = (VarNode)node_;
 189                 if(node.index == SubsumptionGraph.REMOVED)
 190                     continue;
 191                 if(node.lowerBound == node.upperBound) {
 192                     if(DEBUG)
 193                         System.out.println("replace " + toName(node) + " by " + effectIds.toType(node.lowerBound) + ", node.lowerBound == node.upperBound");
 194                     touchNeighborhood(node);
 195                     node.removeConstantNode(effectIds, node.lowerBound);
 196                     continue;
 197                 }
 198                 for(Sub cur=node.upper;cur!=null;cur=cur.aNext)
 199                     if(cur.b == node)
 200                         cur.remove();
 201                 if(node.upper != null && node.upper.aNext != null) {
 202                     for(Sub cur=node.upper;cur!=null;cur=cur.aNext)
 203                         if(!set.add(cur.b) || subsumes(node.upperBound, cur.a.lowerBound)) {
 204                             touch(cur.b);
 205                             cur.remove();
 206                         }
 207                     set.clear();
 208                 }
 209                 if(node.lower != null && node.lower.bNext != null) {
 210                     for(Sub cur=node.lower;cur!=null;cur=cur.bNext)
 211                         if(!set.add(cur.a) || subsumes(cur.a.upperBound, node.lowerBound)) {
 212                             touch(cur.a);
 213                             cur.remove();
 214                         }
 215                     set.clear();
 216                 }
 217                 Polarity polarity = node.getPolarity();
 218                 if(!polarity.isNegative()) {
 219                     if(node.partOf == null) {
 220                         if(node.lower == null) {
 221                             // No low nodes
 222                             if(DEBUG)
 223                                 System.out.println("replace " + toName(node) + " by " + effectIds.toType(node.lowerBound) + ", polarity=" + polarity + ", no low nodes");
 224                             touchNeighborhood(node);
 225                             node.removeConstantNode(effectIds, node.lowerBound);
 226                             continue;
 227                         }
 228                         else if(node.lower.bNext == null) {
 229                             // Exactly one low node
 230                             VarNode low = node.lower.a;
 231
 232                             if(low.lowerBound == node.lowerBound) {
 233                                 node.lower.remove();
 234                                 if(DEBUG)
 235                                     System.out.println("replace " + toName(node) + " by " + toName(low) + ", polarity=" + polarity + ", just one low node");
 236                                 touchNeighborhood(node);
 237                                 node.replaceBy(low);
 238                                 continue;
 239                             }
 240                         }
 241                     }
 242                 }
 243                 else if(polarity == Polarity.NEGATIVE) {
 244                     if(node.upper != null && node.upper.aNext == null) {
 245                         Node high = node.upper.b;
 246                         if(node.upperBound == high.upperBound && high instanceof VarNode) {
 247                             VarNode varHigh = (VarNode)high;
 248
 249                             node.upper.remove();
 250                             if(DEBUG)
 251                                 System.out.println("replace " + toName(node) + " by " + toName(varHigh) + ", polarity=" + polarity + ", just one high node");
 252                             touchNeighborhood(node);
 253                             node.replaceBy(varHigh);
 254                             continue;
 255                         }
 256                     }
 257                 }
 258             }
 259             else {
 260                 UnionNode union = (UnionNode)node_;
 261                 if(union.constPart == SubsumptionGraph.REMOVED)
 262                     continue;
 263                 if(union.lower == null) {
 264                     int low = union.constPart;
 265                     for(PartOfUnion partOf=union.parts;partOf!=null;partOf=partOf.bNext)
 266                         low |= partOf.a.lowerBound;
 267
 268                     if(subsumes(union.lowerBound, low)) {
 269                         if(DEBUG) {
 270                             System.out.print("remove union, " + constToString(union.lowerBound) + " < " + constToString(low));
 271                             printUnion(union);
 272                         }
 273                         touchNeighborhood(union);
 274                         union.remove();
 275                         continue;
 276                     }
 277                 }
 278                 else {
 279                     for(Sub cur=union.lower;cur!=null;cur=cur.bNext) {
 280                         VarNode lowNode = union.lower.a;
 281                         for(PartOfUnion partOf=union.parts;partOf!=null;partOf=partOf.bNext)
 282                             if(partOf.a == lowNode) {
 283                                 cur.remove();
 284                                 touch(union);
 285                                 break;
 286                             }
 287                     }
 288                 }
 289             }
 290         }
 291     }
 292
 293     private void checkLowerBounds() {
 294         for(VarNode node : varNodeMap.values())
 295             checkLowerBound(node);
 296         for(UnionNode node : unionNodes)
 297             checkLowerBound(node);
 298     }
 299
 300     private void checkLowerBound(Node node) {
 301         int upperBound = node.upperBound;
 302         if(!subsumes(node.lowerBound, upperBound))
 303             for(LowerBoundSource source=node.lowerBoundSource;source!=null;source=source.next)
 304                 if(!subsumes(source.lower, upperBound))
 305                     reportSubsumptionFailure(source.location, source.lower, upperBound);
 306         node.lowerBoundSource = null;
 307     }
 308
 309     private void propagateLowerBounds() {
 310         for(VarNode node : sortedNodes) {
 311             for(Sub cur=node.lower;cur!=null;cur=cur.bNext)
 312                 node.lowerBound |= cur.a.lowerBound;
 313         }
 314         if(!unionNodes.isEmpty()) {
 315             for(UnionNode node : unionNodes) {
 316                 if(node.parts != null && node.parts.bNext != null) {
 317                     // Remove duplicate parts of the union, might be there because of merging of strongly connected components
 318                     THashSet<VarNode> varSet = new THashSet<VarNode>();
 319                     for(PartOfUnion cur=node.parts;cur!=null;cur=cur.bNext)
 320                         if(!varSet.add(cur.a))
 321                             cur.remove();
 322                 }
 323
 324                 for(Sub cur=node.lower;cur!=null;cur=cur.bNext)
 325                     node.lowerBound |= cur.a.lowerBound;
 326
 327                 activeSet.add(node);
 328                 queue.addLast(node);
 329             }
 330             while(!queue.isEmpty()) {
 331                 Node node = queue.removeFirst();
 332                 activeSet.remove(node);
 333                 int lowerBound = node.lowerBound;
 334
 335                 if(node instanceof VarNode) {
 336                     VarNode var = (VarNode)node;
 337                     for(Sub cur=var.upper;cur!=null;cur=cur.aNext) {
 338                         Node highNode = cur.b;
 339                         int newLowerBound = highNode.lowerBound & lowerBound;
 340                         if(newLowerBound != highNode.lowerBound) {
 341                             highNode.lowerBound = newLowerBound;
 342                             touch(highNode);
 343                         }
 344                     }
 345                 }
 346                 else {
 347                     UnionNode union = (UnionNode)node;
 348                     for(PartOfUnion cur=union.parts;cur!=null;cur=cur.bNext) {
 349                         int residual = lowerBound & (~union.constPart);
 350                         for(PartOfUnion cur2=union.parts;cur2!=null;cur2=cur2.bNext)
 351                             if(cur2 != cur)
 352                                 residual = lowerBound & (~cur2.a.upperBound);
 353                         VarNode partNode = cur.a;
 354                         int newLowerBound = partNode.lowerBound | residual;
 355                         if(newLowerBound != partNode.lowerBound) {
 356                             partNode.lowerBound = newLowerBound;
 357                             touch(partNode);
 358                         }
 359                     }
 360                 }
 361             }
 362         }
 363     }
 364
 365     private void reportSubsumptionFailure(long location, int lowerBound, int upperBound) {
 366         errorLog.log(location, "Side-effect " + effectIds.toType(lowerBound & (~upperBound)) + " is forbidden here.");
 367     }
 368
 369     private final THashSet<Node> activeSet = new THashSet<>();
 370     private final ArrayDeque<Node> queue = new ArrayDeque<>();
 371
 372     private void touch(Node node) {
 373         if(activeSet.add(node))
 374             queue.addLast(node);
 375     }
 376
 377     private void propagateUpperBounds() {
 378         for(VarNode node : varNodeMap.values())
 379             if(node.upperBound != EffectIdMap.MAX) {
 380                 activeSet.add(node);
 381                 queue.addLast(node);
 382             }
 383
 384         while(!queue.isEmpty()) {
 385             Node node = queue.removeFirst();
 386             activeSet.remove(node);
 387             int upperBound = node.upperBound;
 388
 389             if(node instanceof VarNode) {
 390                 // Upper bounds for unions are not calculated immediately
 391                 for(PartOfUnion cur=((VarNode)node).partOf;cur!=null;cur=cur.aNext) {
 392                     UnionNode union = cur.b;
 393                     touch(union);
 394                 }
 395             }
 396             else {
 397                 // New upper bound for union is calculated here
 398                 UnionNode union = (UnionNode)node;
 399                 int newUpperBound = union.constPart;
 400                 for(PartOfUnion cur=union.parts;cur!=null;cur=cur.bNext)
 401                     newUpperBound |= cur.a.upperBound;
 402                 if(newUpperBound != upperBound)
 403                     node.upperBound = upperBound = newUpperBound;
 404                 else
 405                     continue; // No changes in upper bound, no need to propagate
 406             }
 407
 408             // Propagate upper bound to smaller variables
 409             for(Sub cur=node.lower;cur!=null;cur=cur.bNext) {
 410                 VarNode lowNode = cur.a;
 411                 int newUpperBound = lowNode.upperBound & upperBound;
 412                 if(newUpperBound != lowNode.upperBound) {
 413                     lowNode.upperBound = newUpperBound;
 414                     touch(lowNode);
 415                 }
 416             }
 417         }
 418     }
 419
 420     int curIndex;
 421     private void stronglyConnectedComponents() {
 422         sortedNodes = new ArrayList<VarNode>(varNodeMap.size());
 423         for(VarNode node : varNodeMap.values())
 424             node.index = -1;
 425         for(VarNode node : varNodeMap.values())
 426             if(node.index == -1) {
 427                 curIndex = 0;
 428                 stronglyConnectedComponents(node);
 429             }
 430     }
 431
 432     ArrayList<VarNode> sortedNodes;
 433     ArrayList<VarNode> stack = new ArrayList<VarNode>();
 434     private int stronglyConnectedComponents(VarNode node) {
 435         int lowindex = node.index = curIndex++;
 436         stack.add(node);
 437         for(Sub sub=node.lower;sub != null;sub=sub.bNext) {
 438             VarNode child = sub.a;
 439             int childIndex = child.index;
 440             if(childIndex == -1)
 441                 childIndex = stronglyConnectedComponents(child);
 442             lowindex = Math.min(lowindex, childIndex);
 443         }
 444         if(node.index == lowindex) {
 445             // root of strongly connected component
 446             VarNode stackNode = stack.remove(stack.size()-1);
 447             if(stackNode != node) {
 448                 ArrayList<VarNode> otherInComponent = new ArrayList<VarNode>(4);
 449                 while(stackNode != node) {
 450                     otherInComponent.add(stackNode);
 451                     stackNode = stack.remove(stack.size()-1);
 452                 }
 453                 mergeComponent(node, otherInComponent);
 454             }
 455             node.index = Integer.MAX_VALUE;
 456             sortedNodes.add(node);
 457         }
 458         return lowindex;
 459     }
 460
 461     private void mergeComponent(VarNode root, ArrayList<VarNode> otherInComponent) {
 462         // There is no need to merge upper bounds, because they have been propagated
 463         int lowerBound = root.lowerBound;
 464         for(VarNode node : otherInComponent)
 465             lowerBound |= node.lowerBound;
 466         root.lowerBound = lowerBound;
 467
 468         for(VarNode node : otherInComponent) {
 469             if(DEBUG)
 470                 System.out.println("replace " + toName(node) + " by " + toName(root));
 471             node.replaceBy(root);
 472         }
 473     }
 474
 475     // Dummy debugging functions
 476     private String toName(Node node) {
 477         return "";
 478     }
 479     private void printUnion(UnionNode union) {
 480     }
 481     private void print() {
 482     }
 483     private String constToString(int cons) {
 484         return "";
 485     }
 486     /*
 487     private TypeUnparsingContext tuc = new TypeUnparsingContext();
 488     private THashMap<Node, String> nameMap = new THashMap<Node, String>();
 489     private char nextChar = 'a';
 490
 491     private String toName(Node node) {
 492         String name = nameMap.get(node);
 493         if(name == null) {
 494             name = new String(new char[] {'?', nextChar++});
 495             nameMap.put(node, name);
 496         }
 497         return name;
 498     }
 499
 500     private String constToString(int cons) {
 501         return effectIds.toType(cons).toString(tuc);
 502     }
 503
 504     private boolean hasContent() {
 505         for(VarNode node : varNodeMap.values())
 506             if(node.index != SubsumptionGraph.REMOVED)
 507 //                if(node.lower != null)
 508                 return true;
 509         for(UnionNode node : unionNodes)
 510             if(node.constPart != SubsumptionGraph.REMOVED)
 511                 return true;
 512         return false;
 513     }
 514
 515     private void print() {
 516         if(!hasContent())
 517             return;
 518         System.out.println("vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv");
 519         TypeUnparsingContext tuc = new TypeUnparsingContext();
 520         for(VarNode node : varNodeMap.values()) {
 521             if(node.index == SubsumptionGraph.REMOVED) {
 522                 //System.out.println(toName(node) + " removed");
 523                 continue;
 524             }
 525             System.out.print(toName(node));
 526             if(node.lowerBound != EffectIdMap.MIN || node.upperBound != EffectIdMap.MAX) {
 527                 System.out.print(" in [");
 528                 if(node.lowerBound != EffectIdMap.MIN)
 529                     System.out.print(constToString(node.lowerBound));
 530                 System.out.print("..");
 531                 if(node.upperBound != EffectIdMap.MAX) {
 532                     if(node.upperBound == 0)
 533                         System.out.print("Pure");
 534                     else
 535                         System.out.print(constToString(node.upperBound));
 536                 }
 537                 System.out.print("]");
 538             }
 539             System.out.println(" (" + node.getPolarity() + ")");
 540
 541             for(Sub cur=node.upper;cur!=null;cur=cur.aNext) {
 542                 System.out.print("    < ");
 543                 Node highNode = cur.b;
 544                 if(highNode instanceof VarNode) {
 545                     System.out.println(toName(highNode));
 546                 }
 547                 else
 548                     printUnion((UnionNode)highNode);
 549             }
 550         }
 551         for(UnionNode node : unionNodes) {
 552             if(node.lower != null)
 553                 continue;
 554             System.out.print(constToString(node.lowerBound) + " < ");
 555             printUnion(node);
 556         }
 557         System.out.println("^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^");
 558     }
 559
 560     private void printUnion(UnionNode union) {
 561         System.out.print("union(");
 562         boolean first = true;
 563         if(union.constPart != EffectIdMap.MIN) {
 564             System.out.print(constToString(union.constPart));
 565             first = false;
 566         }
 567         for(PartOfUnion part=union.parts;part!=null;part=part.bNext) {
 568             if(first)
 569                 first = false;
 570             else
 571                 System.out.print(", ");
 572             System.out.print(toName(part.a));
 573         }
 574         System.out.println(")");
 575     }
 576     */
 577
 578     public static void solve(ErrorLog errorLog, ArrayList<Subsumption> subsumptions) {
 579         new SubSolver2(errorLog, subsumptions).solve();
 580     }
 581 }