]> gerrit.simantics Code Review - simantics/platform.git/commitdiff
New solver for SCL effects inequalities 34/1734/3
authorHannu Niemistö <hannu.niemisto@semantum.fi>
Wed, 25 Apr 2018 13:57:31 +0000 (16:57 +0300)
committerHannu Niemistö <hannu.niemisto@semantum.fi>
Fri, 27 Apr 2018 13:08:04 +0000 (16:08 +0300)
In particularly, solving of cyclic inequalities.

Change-Id: I5d5734e9f029bf694221db2d7fc994d16d8d607a

bundles/org.simantics.scl.compiler/META-INF/MANIFEST.MF
bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/compilation/TypeChecking.java
bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/elaboration/contexts/TypingContext.java
bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/internal/elaboration/subsumption/SubSolver.java
bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/internal/elaboration/subsumption2/SubSolver2.java [new file with mode: 0644]
bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/internal/elaboration/subsumption2/SubsumptionGraph.java [new file with mode: 0644]
bundles/org.simantics.scl.runtime/scl/Prelude.scl
tests/org.simantics.scl.compiler.tests/src/org/simantics/scl/compiler/tests/TestRegression.java
tests/org.simantics.scl.compiler.tests/src/org/simantics/scl/compiler/tests/unit/TestSubSolver2.java [new file with mode: 0644]

index 91014207da4e9452fd154d1d64253dd327983e0e..7bfc9da61812996e1eb9eb035b1b6e74bc33c174 100644 (file)
@@ -55,6 +55,7 @@ Export-Package: org.cojen.classfile,
  org.simantics.scl.compiler.internal.codegen.writer,
  org.simantics.scl.compiler.internal.elaboration.constraints2,
  org.simantics.scl.compiler.internal.elaboration.subsumption,
+ org.simantics.scl.compiler.internal.elaboration.subsumption2,
  org.simantics.scl.compiler.internal.parsing,
  org.simantics.scl.compiler.internal.parsing.exceptions,
  org.simantics.scl.compiler.internal.parsing.parser,
index 373a9a333b4e05f2b6c9389325e657ece8a059cc..ff713b1705a85284c841e1fb2a9393aa0a3a4d19 100644 (file)
@@ -186,6 +186,7 @@ public class TypeChecking {
                                     .closure(vars));
                             value.setType(Types.forAll(vars, 
                                     Types.constrained(constraints, value.getType())));
+                            //System.out.println(value.getName() + " :: " + value.getType());
                             
                             // Add evidence parameters to recursive calls
                             for(EPlaceholder ref : recursiveReferences) {
@@ -220,6 +221,7 @@ public class TypeChecking {
                                 for(EAmbiguous overloaded : context.overloadedExpressions)
                                     overloaded.assertResolved(compilationContext.errorLog);
                                 expression.getType().addPolarity(Polarity.POSITIVE);
+                                //System.out.println("--- " + value.getName() + " -------------------------------------------------------------------------");
                                 context.solveSubsumptions(expression.getLocation());
                                 
                                 if(compilationContext.errorLog.getErrorCount() != errorCountBeforeTypeChecking) {
index f862d2128c358999edc0a79c188c008fe348c0b5..68468076d32fa155d81d3e7c82371d33162eff97 100644 (file)
@@ -20,8 +20,8 @@ import org.simantics.scl.compiler.internal.elaboration.constraints.ConstraintEnv
 import org.simantics.scl.compiler.internal.elaboration.constraints.ConstraintSolver;
 import org.simantics.scl.compiler.internal.elaboration.constraints.ExpressionAugmentation;
 import org.simantics.scl.compiler.internal.elaboration.constraints.ReducedConstraints;
-import org.simantics.scl.compiler.internal.elaboration.subsumption.SubSolver;
 import org.simantics.scl.compiler.internal.elaboration.subsumption.Subsumption;
+import org.simantics.scl.compiler.internal.elaboration.subsumption2.SubSolver2;
 import org.simantics.scl.compiler.types.Skeletons;
 import org.simantics.scl.compiler.types.TApply;
 import org.simantics.scl.compiler.types.TCon;
@@ -35,6 +35,7 @@ import org.simantics.scl.compiler.types.Type;
 import org.simantics.scl.compiler.types.Types;
 import org.simantics.scl.compiler.types.exceptions.UnificationException;
 import org.simantics.scl.compiler.types.kinds.Kinds;
+import org.simantics.scl.compiler.types.util.Polarity;
 import org.simantics.scl.compiler.types.util.TypeUnparsingContext;
 
 import gnu.trove.map.hash.THashMap;
@@ -406,8 +407,28 @@ public class TypingContext {
     }
     
     public void solveSubsumptions(long globalLoc) {
-        if(expandSubsumptions())
-            new SubSolver(compilationContext.errorLog, effectSubsumptions, potentialSingletonEffects, globalLoc).solve();
+        if(expandSubsumptions()) {
+            if(!effectSubsumptions.isEmpty())
+                SubSolver2.solve(compilationContext.errorLog, effectSubsumptions);
+            
+            if(!potentialSingletonEffects.isEmpty())
+                try {
+                    THashSet<TMetaVar> vars = new THashSet<TMetaVar>(4);
+                    for(Type type : potentialSingletonEffects)
+                        type.collectMetaVars(vars);
+                    for(TMetaVar var : vars) {
+                        if(var.getRef() == null) {
+                            Polarity polarity = var.getPolarity();
+                            if(!polarity.isNegative())
+
+                                var.setRef(Types.NO_EFFECTS);
+                        }
+                    }
+                } catch(UnificationException e) {
+                    throw new InternalCompilerError(e);
+                }
+            //new SubSolver(compilationContext.errorLog, effectSubsumptions, potentialSingletonEffects, globalLoc).solve();
+        }
     }
     
     public void declareEffect(long loc, Type effect) {
index 40f8fdf6ada254b483a05e5f82666aac2af98a6d..088cf3396cf941554cbc678fa9c511bde066e92a 100644 (file)
@@ -43,6 +43,7 @@ public class SubSolver {
     }    
     
     public void solve() {
+        //System.out.println("--------------------------------------------------");
         //printSubsumptions();
         createVar();
         //print();
@@ -50,7 +51,6 @@ public class SubSolver {
         propagateUpperBounds();
         checkLowerBounds();
         //errorFromUnsolvedEquations();
-        //System.out.println("--");
         //print();
     }
     
@@ -110,6 +110,7 @@ public class SubSolver {
     private void createVar() {
         for(Subsumption sub : subsumptions)
             addSubsumption(sub.loc, sub.a, sub.b);
+        // In some cases there might be types that are not part of any subsumption, for example related to typeOf
         for(Type t : potentialSingletonEffects)
             addVar(t);
     }
diff --git a/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/internal/elaboration/subsumption2/SubSolver2.java b/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/internal/elaboration/subsumption2/SubSolver2.java
new file mode 100644 (file)
index 0000000..3acd0ca
--- /dev/null
@@ -0,0 +1,581 @@
+package org.simantics.scl.compiler.internal.elaboration.subsumption2;
+
+import java.util.ArrayDeque;
+import java.util.ArrayList;
+import java.util.Arrays;
+
+import org.simantics.scl.compiler.errors.ErrorLog;
+import org.simantics.scl.compiler.internal.elaboration.subsumption.Subsumption;
+import org.simantics.scl.compiler.internal.elaboration.subsumption2.SubsumptionGraph.LowerBoundSource;
+import org.simantics.scl.compiler.internal.elaboration.subsumption2.SubsumptionGraph.Node;
+import org.simantics.scl.compiler.internal.elaboration.subsumption2.SubsumptionGraph.PartOfUnion;
+import org.simantics.scl.compiler.internal.elaboration.subsumption2.SubsumptionGraph.Sub;
+import org.simantics.scl.compiler.internal.elaboration.subsumption2.SubsumptionGraph.UnionNode;
+import org.simantics.scl.compiler.internal.elaboration.subsumption2.SubsumptionGraph.VarNode;
+import org.simantics.scl.compiler.internal.types.effects.EffectIdMap;
+import org.simantics.scl.compiler.types.TMetaVar;
+import org.simantics.scl.compiler.types.util.Polarity;
+
+import gnu.trove.map.hash.THashMap;
+import gnu.trove.map.hash.TIntIntHashMap;
+import gnu.trove.set.hash.THashSet;
+
+public class SubSolver2 {
+    public static final boolean DEBUG = false;
+    
+    // Input
+    private final ErrorLog errorLog;
+    private final ArrayList<Subsumption> subsumptions;
+
+    //
+    private final EffectIdMap effectIds = new EffectIdMap();
+    private final THashMap<TMetaVar, VarNode> varNodeMap = new THashMap<TMetaVar, VarNode>();
+    private final ArrayList<UnionNode> unionNodes = new ArrayList<UnionNode>(); 
+
+    private static TIntIntHashMap STATISTICS = new TIntIntHashMap();
+    
+    private SubSolver2(ErrorLog errorLog, ArrayList<Subsumption> subsumptions) {
+        this.errorLog = errorLog;
+        this.subsumptions = subsumptions;
+        /*if(subsumptions.size() == 1) {
+            TypeUnparsingContext tuc = new TypeUnparsingContext();
+            Subsumption sub = subsumptions.get(0);
+            if(sub.a instanceof TCon && sub.b instanceof TCon)
+                System.out.println("caseCC");
+            else if(sub.a instanceof TMetaVar && sub.b instanceof TCon)
+                System.out.println("caseMC");
+            else if(sub.a instanceof TVar && sub.b instanceof TCon)
+                System.out.println("caseVC");
+            System.out.println("    " + sub.a.toString(tuc) + " < " + sub.b.toString(tuc));
+        }
+        synchronized(STATISTICS) {
+            STATISTICS.adjustOrPutValue(subsumptions.size(), 1, 1);
+            showStatistics();
+        }*/
+    }
+    
+    public static void showStatistics() {
+        System.out.println("---");
+        int[] keys = STATISTICS.keys();
+        Arrays.sort(keys);
+        int sum = 0;
+        for(int key : keys)
+            sum += STATISTICS.get(key);
+        for(int key : keys) {
+            int value = STATISTICS.get(key);
+            System.out.println(key + ": " + value + " (" + (value*100.0/sum) + "%)");
+        }
+    }
+
+    private static boolean subsumes(int a, int b) {
+        return (a&b) == a;
+    }
+
+    private void processSubsumptions() {
+        ArrayList<TMetaVar> aVars = new ArrayList<TMetaVar>(2);
+        ArrayList<TMetaVar> bVars = new ArrayList<TMetaVar>(2);
+        for(Subsumption subsumption : subsumptions) {
+            int aCons = effectIds.toId(subsumption.a, aVars);
+            int bCons = effectIds.toId(subsumption.b, bVars);
+
+            if(bVars.isEmpty()) {
+                if(!subsumes(aCons, bCons)) {
+                    reportSubsumptionFailure(subsumption.loc, aCons, bCons);
+                    continue;
+                }
+                for(TMetaVar aVar : aVars)
+                    getOrCreateNode(aVar).upperBound &= bCons;
+            }
+            else {
+                Node bNode;
+                if(bVars.size() == 1 && bCons == 0)
+                    bNode = getOrCreateNode(bVars.get(0));
+                else
+                    bNode = createUnion(subsumption.loc, bCons, bVars);
+                if(aCons != 0)
+                    setLowerBound(subsumption.loc, aCons, bNode);
+                for(TMetaVar aVar : aVars)
+                    new Sub(getOrCreateNode(aVar), bNode);
+                bVars.clear();
+            }
+            aVars.clear();
+        }
+    }
+
+    private void setLowerBound(long location, int lower, Node node) {
+        node.lowerBound |= lower;
+        node.addLowerBoundSource(location, lower);
+    }
+
+    private UnionNode createUnion(long location, int cons, ArrayList<TMetaVar> vars) {
+        UnionNode node = new UnionNode(location, cons);
+        for(TMetaVar var : vars)
+            new PartOfUnion(getOrCreateNode(var), node);
+        unionNodes.add(node);
+        return node;
+    }
+
+    private VarNode getOrCreateNode(TMetaVar var) {
+        VarNode node = varNodeMap.get(var);
+        if(node == null) {
+            node = new VarNode(var);
+            varNodeMap.put(var, node);
+        }
+        return node;
+    }
+
+    public boolean solve() {
+        //System.out.println("------------------------------------------------------");
+        int errorCount = errorLog.getErrorCount();
+
+        // Check errors
+        processSubsumptions();
+        propagateUpperBounds();
+        checkLowerBounds();
+        
+        if(DEBUG)
+            print();
+
+        if(errorLog.getErrorCount() != errorCount)
+            return false;
+
+        // Simplify constraints
+        stronglyConnectedComponents();
+        propagateLowerBounds();
+        simplify();
+
+        if(DEBUG)
+            print();
+        
+        return true;
+    }
+    
+    private void touchNeighborhood(VarNode node) {
+        for(Sub cur=node.lower;cur!=null;cur=cur.bNext)
+            touch(cur.a);
+        for(Sub cur=node.upper;cur!=null;cur=cur.aNext)
+            touch(cur.b);
+        for(PartOfUnion cur=node.partOf;cur!=null;cur=cur.aNext)
+            touch(cur.b);
+    }
+    
+    private void touchNeighborhood(UnionNode node) {
+        for(Sub cur=node.lower;cur!=null;cur=cur.bNext)
+            touch(cur.a);
+        for(PartOfUnion cur=node.parts;cur!=null;cur=cur.bNext)
+            touch(cur.a);
+    }
+
+    THashSet<Node> set = new THashSet<Node>(); 
+    private void simplify() {
+        for(VarNode node : sortedNodes) {
+            if(node.index == SubsumptionGraph.REMOVED)
+                continue;
+            activeSet.add(node);
+            queue.addLast(node);
+        }
+        for(UnionNode node : unionNodes) {
+            if(node.constPart == SubsumptionGraph.REMOVED)
+                continue;
+            activeSet.add(node);
+            queue.addLast(node);
+        }
+        
+        while(!queue.isEmpty()) {
+            Node node_ = queue.removeFirst();
+            activeSet.remove(node_);
+            if(node_ instanceof VarNode) {
+                VarNode node = (VarNode)node_;
+                if(node.index == SubsumptionGraph.REMOVED)
+                    continue;
+                if(node.lowerBound == node.upperBound) {
+                    if(DEBUG)
+                        System.out.println("replace " + toName(node) + " by " + effectIds.toType(node.lowerBound) + ", node.lowerBound == node.upperBound");
+                    touchNeighborhood(node);
+                    node.removeConstantNode(effectIds, node.lowerBound);
+                    continue;
+                }
+                for(Sub cur=node.upper;cur!=null;cur=cur.aNext)
+                    if(cur.b == node)
+                        cur.remove();
+                if(node.upper != null && node.upper.aNext != null) {
+                    for(Sub cur=node.upper;cur!=null;cur=cur.aNext)
+                        if(!set.add(cur.b) || subsumes(node.upperBound, cur.a.lowerBound)) {
+                            touch(cur.b);
+                            cur.remove();
+                        }
+                    set.clear();
+                }
+                if(node.lower != null && node.lower.bNext != null) {
+                    for(Sub cur=node.lower;cur!=null;cur=cur.bNext)
+                        if(!set.add(cur.a) || subsumes(cur.a.upperBound, node.lowerBound)) {
+                            touch(cur.a);
+                            cur.remove();
+                        }
+                    set.clear();
+                }
+                Polarity polarity = node.getPolarity();
+                if(!polarity.isNegative()) { 
+                    if(node.partOf == null) {
+                        if(node.lower == null) {
+                            // No low nodes
+                            if(DEBUG)
+                                System.out.println("replace " + toName(node) + " by " + effectIds.toType(node.lowerBound) + ", polarity=" + polarity + ", no low nodes");
+                            touchNeighborhood(node);
+                            node.removeConstantNode(effectIds, node.lowerBound);
+                            continue;
+                        }
+                        else if(node.lower.bNext == null) {
+                            // Exactly one low node
+                            VarNode low = node.lower.a;
+
+                            if(low.lowerBound == node.lowerBound) {
+                                node.lower.remove();
+                                if(DEBUG)
+                                    System.out.println("replace " + toName(node) + " by " + toName(low) + ", polarity=" + polarity + ", just one low node");
+                                touchNeighborhood(node);
+                                node.replaceBy(low);
+                                continue;
+                            }
+                        }
+                    }
+                }
+                else if(polarity == Polarity.NEGATIVE) {
+                    if(node.upper != null && node.upper.aNext == null) {
+                        Node high = node.upper.b;
+                        if(node.upperBound == high.upperBound && high instanceof VarNode) {
+                            VarNode varHigh = (VarNode)high;
+                            
+                            node.upper.remove();
+                            if(DEBUG)
+                                System.out.println("replace " + toName(node) + " by " + toName(varHigh) + ", polarity=" + polarity + ", just one high node");
+                            touchNeighborhood(node);
+                            node.replaceBy(varHigh);
+                            continue;
+                        }
+                    }
+                }
+            }
+            else {
+                UnionNode union = (UnionNode)node_;
+                if(union.constPart == SubsumptionGraph.REMOVED)
+                    continue;
+                if(union.lower == null) {
+                    int low = union.constPart;
+                    for(PartOfUnion partOf=union.parts;partOf!=null;partOf=partOf.bNext)
+                        low |= partOf.a.lowerBound;
+
+                    if(subsumes(union.lowerBound, low)) {
+                        if(DEBUG) {
+                            System.out.print("remove union, " + constToString(union.lowerBound) + " < " + constToString(low));
+                            printUnion(union);
+                        }
+                        touchNeighborhood(union);
+                        union.remove();
+                        continue;
+                    }
+                }
+                else {
+                    for(Sub cur=union.lower;cur!=null;cur=cur.bNext) {
+                        VarNode lowNode = union.lower.a;
+                        for(PartOfUnion partOf=union.parts;partOf!=null;partOf=partOf.bNext)
+                            if(partOf.a == lowNode) {
+                                cur.remove();
+                                touch(union);
+                                break;
+                            }
+                    }
+                }
+            }
+        }
+    }
+
+    private void checkLowerBounds() {
+        for(VarNode node : varNodeMap.values())
+            checkLowerBound(node);
+        for(UnionNode node : unionNodes) 
+            checkLowerBound(node);
+    }
+
+    private void checkLowerBound(Node node) {
+        int upperBound = node.upperBound;
+        if(!subsumes(node.lowerBound, upperBound))
+            for(LowerBoundSource source=node.lowerBoundSource;source!=null;source=source.next)
+                if(!subsumes(source.lower, upperBound))
+                    reportSubsumptionFailure(source.location, source.lower, upperBound);
+        node.lowerBoundSource = null;
+    }
+
+    private void propagateLowerBounds() {
+        for(VarNode node : sortedNodes) {
+            for(Sub cur=node.lower;cur!=null;cur=cur.bNext)
+                node.lowerBound |= cur.a.lowerBound;
+        }
+        if(!unionNodes.isEmpty()) {
+            for(UnionNode node : unionNodes) {
+                if(node.parts != null && node.parts.bNext != null) {
+                    // Remove duplicate parts of the union, might be there because of merging of strongly connected components
+                    THashSet<VarNode> varSet = new THashSet<VarNode>(); 
+                    for(PartOfUnion cur=node.parts;cur!=null;cur=cur.bNext)
+                        if(!varSet.add(cur.a))
+                            cur.remove();
+                }
+                
+                for(Sub cur=node.lower;cur!=null;cur=cur.bNext)
+                    node.lowerBound |= cur.a.lowerBound;
+
+                activeSet.add(node);
+                queue.addLast(node);
+            }
+            while(!queue.isEmpty()) {
+                Node node = queue.removeFirst();
+                activeSet.remove(node);
+                int lowerBound = node.lowerBound;
+
+                if(node instanceof VarNode) {
+                    VarNode var = (VarNode)node;
+                    for(Sub cur=var.upper;cur!=null;cur=cur.aNext) {
+                        Node highNode = cur.b;
+                        int newLowerBound = highNode.lowerBound & lowerBound;
+                        if(newLowerBound != highNode.lowerBound) {
+                            highNode.lowerBound = newLowerBound;
+                            touch(highNode);
+                        }
+                    }
+                }
+                else {
+                    UnionNode union = (UnionNode)node;
+                    for(PartOfUnion cur=union.parts;cur!=null;cur=cur.bNext) {
+                        int residual = lowerBound & (~union.constPart);
+                        for(PartOfUnion cur2=union.parts;cur2!=null;cur2=cur2.bNext)
+                            if(cur2 != cur)
+                                residual = lowerBound & (~cur2.a.upperBound);
+                        VarNode partNode = cur.a;
+                        int newLowerBound = partNode.lowerBound | residual;
+                        if(newLowerBound != partNode.lowerBound) {
+                            partNode.lowerBound = newLowerBound;
+                            touch(partNode);
+                        }
+                    }
+                }
+            }
+        }
+    }
+
+    private void reportSubsumptionFailure(long location, int lowerBound, int upperBound) {
+        errorLog.log(location, "Side-effect " + effectIds.toType(lowerBound & (~upperBound)) + " is forbidden here.");        
+    }
+
+    private final THashSet<Node> activeSet = new THashSet<>();
+    private final ArrayDeque<Node> queue = new ArrayDeque<>(); 
+
+    private void touch(Node node) {
+        if(activeSet.add(node))
+            queue.addLast(node);
+    }
+    
+    private void propagateUpperBounds() {
+        for(VarNode node : varNodeMap.values())
+            if(node.upperBound != EffectIdMap.MAX) {
+                activeSet.add(node);
+                queue.addLast(node);
+            }
+
+        while(!queue.isEmpty()) {
+            Node node = queue.removeFirst();
+            activeSet.remove(node);
+            int upperBound = node.upperBound;
+
+            if(node instanceof VarNode) {
+                // Upper bounds for unions are not calculated immediately
+                for(PartOfUnion cur=((VarNode)node).partOf;cur!=null;cur=cur.aNext) {
+                    UnionNode union = cur.b;
+                    touch(union);
+                }
+            }
+            else {
+                // New upper bound for union is calculated here
+                UnionNode union = (UnionNode)node;
+                int newUpperBound = union.constPart;
+                for(PartOfUnion cur=union.parts;cur!=null;cur=cur.bNext)
+                    newUpperBound |= cur.a.upperBound;
+                if(newUpperBound != upperBound)
+                    node.upperBound = upperBound = newUpperBound;
+                else
+                    continue; // No changes in upper bound, no need to propagate
+            }
+
+            // Propagate upper bound to smaller variables
+            for(Sub cur=node.lower;cur!=null;cur=cur.bNext) {
+                VarNode lowNode = cur.a;
+                int newUpperBound = lowNode.upperBound & upperBound;
+                if(newUpperBound != lowNode.upperBound) {
+                    lowNode.upperBound = newUpperBound;
+                    touch(lowNode);
+                }
+            }
+        }
+    }
+
+    int curIndex;
+    private void stronglyConnectedComponents() {
+        sortedNodes = new ArrayList<VarNode>(varNodeMap.size());
+        for(VarNode node : varNodeMap.values())
+            node.index = -1;
+        for(VarNode node : varNodeMap.values())
+            if(node.index == -1) {
+                curIndex = 0;
+                stronglyConnectedComponents(node);
+            }
+    }
+
+    ArrayList<VarNode> sortedNodes;
+    ArrayList<VarNode> stack = new ArrayList<VarNode>(); 
+    private int stronglyConnectedComponents(VarNode node) {
+        int lowindex = node.index = curIndex++;
+        stack.add(node);
+        for(Sub sub=node.lower;sub != null;sub=sub.bNext) {
+            VarNode child = sub.a;
+            int childIndex = child.index;
+            if(childIndex == -1)
+                childIndex = stronglyConnectedComponents(child);
+            lowindex = Math.min(lowindex, childIndex);
+        }
+        if(node.index == lowindex) {
+            // root of strongly connected component
+            VarNode stackNode = stack.remove(stack.size()-1);
+            if(stackNode != node) {
+                ArrayList<VarNode> otherInComponent = new ArrayList<VarNode>(4);
+                while(stackNode != node) {
+                    otherInComponent.add(stackNode);
+                    stackNode = stack.remove(stack.size()-1);
+                }
+                mergeComponent(node, otherInComponent);
+            }
+            node.index = Integer.MAX_VALUE;
+            sortedNodes.add(node);
+        }
+        return lowindex;
+    }
+
+    private void mergeComponent(VarNode root, ArrayList<VarNode> otherInComponent) {
+        // There is no need to merge upper bounds, because they have been propagated
+        int lowerBound = root.lowerBound;
+        for(VarNode node : otherInComponent)
+            lowerBound |= node.lowerBound;
+        root.lowerBound = lowerBound;
+
+        for(VarNode node : otherInComponent) {
+            if(DEBUG)
+                System.out.println("replace " + toName(node) + " by " + toName(root));
+            node.replaceBy(root);
+        }
+    }
+
+    // Dummy debugging functions
+    private String toName(Node node) {
+        return "";
+    }
+    private void printUnion(UnionNode union) {
+    }
+    private void print() {
+    }
+    private String constToString(int cons) {
+        return "";
+    }
+    /*
+    private TypeUnparsingContext tuc = new TypeUnparsingContext();
+    private THashMap<Node, String> nameMap = new THashMap<Node, String>();
+    private char nextChar = 'a';
+    
+    private String toName(Node node) {
+        String name = nameMap.get(node);
+        if(name == null) {
+            name = new String(new char[] {'?', nextChar++});
+            nameMap.put(node, name);
+        }
+        return name;
+    }
+    
+    private String constToString(int cons) {
+        return effectIds.toType(cons).toString(tuc);
+    }
+    
+    private boolean hasContent() {
+        for(VarNode node : varNodeMap.values())
+            if(node.index != SubsumptionGraph.REMOVED)
+//                if(node.lower != null)
+                return true;
+        for(UnionNode node : unionNodes)
+            if(node.constPart != SubsumptionGraph.REMOVED)
+                return true;
+        return false;
+    }
+    
+    private void print() {
+        if(!hasContent())
+            return;
+        System.out.println("vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv");
+        TypeUnparsingContext tuc = new TypeUnparsingContext();
+        for(VarNode node : varNodeMap.values()) {
+            if(node.index == SubsumptionGraph.REMOVED) {
+                //System.out.println(toName(node) + " removed");
+                continue;
+            }
+            System.out.print(toName(node));
+            if(node.lowerBound != EffectIdMap.MIN || node.upperBound != EffectIdMap.MAX) {
+                System.out.print(" in [");
+                if(node.lowerBound != EffectIdMap.MIN)
+                    System.out.print(constToString(node.lowerBound));
+                System.out.print("..");
+                if(node.upperBound != EffectIdMap.MAX) {
+                    if(node.upperBound == 0)
+                        System.out.print("Pure");
+                    else
+                        System.out.print(constToString(node.upperBound));
+                }
+                System.out.print("]");
+            }
+            System.out.println(" (" + node.getPolarity() + ")");
+            
+            for(Sub cur=node.upper;cur!=null;cur=cur.aNext) {
+                System.out.print("    < ");
+                Node highNode = cur.b;
+                if(highNode instanceof VarNode) {
+                    System.out.println(toName(highNode));
+                }
+                else
+                    printUnion((UnionNode)highNode);
+            }
+        }
+        for(UnionNode node : unionNodes) {
+            if(node.lower != null)
+                continue;
+            System.out.print(constToString(node.lowerBound) + " < ");
+            printUnion(node);
+        }
+        System.out.println("^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^");
+    }
+    
+    private void printUnion(UnionNode union) {
+        System.out.print("union(");
+        boolean first = true;
+        if(union.constPart != EffectIdMap.MIN) {
+            System.out.print(constToString(union.constPart));
+            first = false;
+        }
+        for(PartOfUnion part=union.parts;part!=null;part=part.bNext) {
+            if(first)
+                first = false;
+            else
+                System.out.print(", ");
+            System.out.print(toName(part.a));
+        }
+        System.out.println(")");
+    }
+    */
+    
+    public static void solve(ErrorLog errorLog, ArrayList<Subsumption> subsumptions) {
+        new SubSolver2(errorLog, subsumptions).solve();
+    }
+}
diff --git a/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/internal/elaboration/subsumption2/SubsumptionGraph.java b/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/internal/elaboration/subsumption2/SubsumptionGraph.java
new file mode 100644 (file)
index 0000000..c382108
--- /dev/null
@@ -0,0 +1,227 @@
+package org.simantics.scl.compiler.internal.elaboration.subsumption2;
+
+import org.simantics.scl.compiler.common.exceptions.InternalCompilerError;
+import org.simantics.scl.compiler.internal.types.effects.EffectIdMap;
+import org.simantics.scl.compiler.types.TMetaVar;
+import org.simantics.scl.compiler.types.exceptions.UnificationException;
+import org.simantics.scl.compiler.types.util.Polarity;
+
+public class SubsumptionGraph {
+    public static final int REMOVED = Integer.MAX_VALUE-1;
+    
+    public static class LowerBoundSource {
+        public final long location;
+        public final int lower;
+        public final LowerBoundSource next;
+        public LowerBoundSource(long location, int lower, LowerBoundSource next) {
+            this.location = location;
+            this.lower = lower;
+            this.next = next;
+        }
+    }
+    
+    public static abstract class Node {
+        int lowerBound = EffectIdMap.MIN;
+        int upperBound = EffectIdMap.MAX;
+        Sub lower;
+        LowerBoundSource lowerBoundSource;
+        
+        public void addLowerBoundSource(long location, int lower) {
+            lowerBoundSource = new LowerBoundSource(location, lower, lowerBoundSource);
+        }
+    }
+    
+    public static class VarNode extends Node {
+        TMetaVar origin;
+        Sub upper;
+        PartOfUnion partOf;
+        int index;
+        
+        public VarNode(TMetaVar origin) {
+            this.origin = origin;
+        }
+        
+        public Polarity getPolarity() {
+            return origin.getPolarity();
+        }
+
+        public void replaceBy(VarNode replacement) {
+            try {
+                origin.setRef(replacement.origin);
+            } catch(UnificationException e) {
+                throw new InternalCompilerError(e);
+            }
+            {
+                Sub last = null;
+                for(Sub cur=upper;cur!=null;cur=cur.aNext) {
+                    cur.a = replacement;
+                    last = cur;
+                }
+                if(last != null) {
+                    last.aNext = replacement.upper;
+                    if(last.aNext != null)
+                        last.aNext.aPrev = last;
+                    replacement.upper = upper;
+                }
+
+                last = null;
+                for(Sub cur=lower;cur!=null;cur=cur.bNext) {
+                    cur.b = replacement;
+                    last = cur;
+                }
+                if(last != null) {
+                    last.bNext = replacement.lower;
+                    if(last.bNext != null)
+                        last.bNext.bPrev = last;
+                    replacement.lower = lower;
+                }
+            }
+            {
+                PartOfUnion last = null;
+                for(PartOfUnion cur=partOf;cur!=null;cur=cur.bNext) {
+                    cur.a = replacement;
+                    last = cur;
+                }
+                if(last != null) {
+                    last.aNext = replacement.partOf;
+                    if(last.aNext != null)
+                        last.aNext.bPrev = last;
+                    replacement.partOf = partOf;
+                }
+            }
+            index = REMOVED;
+        }
+
+        public void removeConstantNode(EffectIdMap effectIds, int constValue) {
+            try {
+                origin.setRef(effectIds.toType(constValue));
+            } catch (UnificationException e) {
+                throw new InternalCompilerError(e);
+            }
+            for(Sub cur=lower;cur!=null;cur=cur.bNext)
+                cur.detachA();
+            for(Sub cur=upper;cur!=null;cur=cur.aNext)
+                cur.detachB();
+            for(PartOfUnion cur=partOf;cur!=null;cur=cur.aNext) {
+                cur.detachB();
+                cur.b.constPart |= constValue;
+            }
+            index = REMOVED;
+        }
+    }
+    
+    public static class UnionNode extends Node {
+        long location;
+        PartOfUnion parts;
+        int constPart;
+        
+        public UnionNode(long location, int constPart) {
+            this.location = location;
+            this.constPart = constPart;
+            this.lowerBound = constPart;
+        }
+
+        public void remove() {
+            for(Sub cur=lower;cur!=null;cur=cur.bNext)
+                cur.detachA();
+            for(PartOfUnion cur=parts;cur!=null;cur=cur.bNext)
+                cur.detachA();
+            constPart = REMOVED;
+        }
+    }
+    
+    public static class Sub {
+        VarNode a;
+        Node b;
+        Sub aNext;
+        Sub aPrev;
+        Sub bNext;
+        Sub bPrev;
+        
+        public Sub(VarNode a, Node b) {
+            this.a = a;
+            this.b = b;
+            
+            aNext = a.upper;
+            if(aNext != null)
+                aNext.aPrev = this;
+            a.upper = this;
+        
+            bNext = b.lower;
+            if(bNext != null)
+                bNext.bPrev = this;
+            b.lower = this;
+        }
+        
+        public void detachA() {
+            if(aNext != null)
+                aNext.aPrev = aPrev;
+            if(aPrev != null)
+                aPrev.aNext = aNext;
+            else
+                a.upper = aNext;
+        }
+
+        public void detachB() {
+            if(bNext != null)
+                bNext.bPrev = bPrev;
+            if(bPrev != null)
+                bPrev.bNext = bNext;
+            else
+                b.lower = bNext;
+        }
+        
+        public void remove() {
+            detachA();
+            detachB();
+        }
+    }
+    
+    public static class PartOfUnion {
+        VarNode a;
+        UnionNode b;
+        PartOfUnion aNext;
+        PartOfUnion aPrev;
+        PartOfUnion bNext;
+        PartOfUnion bPrev;
+        
+        public PartOfUnion(VarNode a, UnionNode b) {
+            this.a = a;
+            this.b = b;
+            
+            aNext = a.partOf;
+            if(aNext != null)
+                aNext.aPrev = this;
+            a.partOf = this;
+        
+            bNext = b.parts;
+            if(bNext != null)
+                bNext.bPrev = this;
+            b.parts = this;
+        }
+        
+        public void detachA() {
+            if(aNext != null)
+                aNext.aPrev = aPrev;
+            if(aPrev != null)
+                aPrev.aNext = aNext;
+            else
+                a.partOf = aNext;
+        }
+        
+        public void detachB() {
+            if(bNext != null)
+                bNext.bPrev = bPrev;
+            if(bPrev != null)
+                bPrev.bNext = bNext;
+            else
+                b.parts = bNext;
+        }
+        
+        public void remove() {
+            detachA();
+            detachB();
+        }
+
+    }
+}
index 32582affa867947fbac5167b94c4d8919c0bd91c..4a51875b2be4595c056e725f734aaee8cd26cfab 100644 (file)
@@ -1166,10 +1166,12 @@ class IndexedSequence f where
 
 "Returns the first element of a sequence"
 @inline
+first :: [a] -> a
 first l = l!0
 
 "Returns the last element of a sequence"
 @inline
+last :: [a] -> a
 last l = l!(length l-1)
 
 instance IndexedSequence [] where
@@ -2058,6 +2060,7 @@ Transposes the rows and columns of its argument. For example,
     transpose [[1,2,3],[4,5,6]] == [[1,4],[2,5],[3,6]]
     transpose [[1,2],[3,4,5]] == [[1,3],[2,4],[5]]
 """
+transpose :: [[a]] -> [[a]]
 transpose xss = [[xs!i | xs <- xss, i < length xs]
                 | i <- [0..maximum [length xs | xs <- xss]-1]]
 
index fcf31dd15dd5fb021fe17b8582b6b031471ab3be..a2c4acc3971a5a7a3972fed08af0e3f7e664e1f4 100644 (file)
@@ -3,12 +3,14 @@ package org.simantics.scl.compiler.tests;
 import org.junit.runner.RunWith;
 import org.junit.runners.Suite;
 import org.junit.runners.Suite.SuiteClasses;
+import org.simantics.scl.compiler.tests.unit.TestSubSolver2;
 
 @RunWith(Suite.class)
 @SuiteClasses({
     ModuleRegressionTests.class,
     TestExpressionEvaluator.class,
-    TestCommandSession.class
+    TestCommandSession.class,
+    TestSubSolver2.class
 })
 public class TestRegression {
 }
diff --git a/tests/org.simantics.scl.compiler.tests/src/org/simantics/scl/compiler/tests/unit/TestSubSolver2.java b/tests/org.simantics.scl.compiler.tests/src/org/simantics/scl/compiler/tests/unit/TestSubSolver2.java
new file mode 100644 (file)
index 0000000..41913e2
--- /dev/null
@@ -0,0 +1,115 @@
+package org.simantics.scl.compiler.tests.unit;
+
+import java.util.ArrayList;
+
+import org.junit.Assert;
+import org.junit.Test;
+import org.simantics.scl.compiler.errors.ErrorLog;
+import org.simantics.scl.compiler.errors.Locations;
+import org.simantics.scl.compiler.internal.elaboration.subsumption.Subsumption;
+import org.simantics.scl.compiler.internal.elaboration.subsumption2.SubSolver2;
+import org.simantics.scl.compiler.types.TMetaVar;
+import org.simantics.scl.compiler.types.Type;
+import org.simantics.scl.compiler.types.Types;
+import org.simantics.scl.compiler.types.kinds.Kinds;
+import org.simantics.scl.compiler.types.util.Polarity;
+
+public class TestSubSolver2 {
+    ErrorLog errorLog = new ErrorLog();
+    ArrayList<Subsumption> subsumptions = new ArrayList<Subsumption>(); 
+    
+    private void sub(Type a, Type b) {
+        subsumptions.add(new Subsumption(Locations.NO_LOCATION, a, b));
+    }
+    
+    private TMetaVar metaVar(Polarity p) {
+        TMetaVar var = Types.metaVar(Kinds.EFFECT);
+        var.addPolarity(p);
+        return var;
+    }
+    
+    @Test
+    public void subFF() {
+        TMetaVar a = metaVar(Polarity.NO_POLARITY);
+        TMetaVar b = metaVar(Polarity.NO_POLARITY);
+        sub(a, b);
+        SubSolver2.solve(errorLog, subsumptions);
+        Assert.assertEquals(0, errorLog.getErrorCount());
+        Assert.assertEquals(a, b);
+    }
+    
+    @Test
+    public void subPP() {
+        TMetaVar a = metaVar(Polarity.POSITIVE);
+        TMetaVar b = metaVar(Polarity.POSITIVE);
+        sub(a, b);
+        SubSolver2.solve(errorLog, subsumptions);
+        Assert.assertEquals(0, errorLog.getErrorCount());
+        Assert.assertEquals(a, b);
+    }
+    
+    @Test
+    public void subNN() {
+        TMetaVar a = metaVar(Polarity.NEGATIVE);
+        TMetaVar b = metaVar(Polarity.NEGATIVE);
+        sub(a, b);
+        SubSolver2.solve(errorLog, subsumptions);
+        Assert.assertEquals(0, errorLog.getErrorCount());
+        Assert.assertEquals(a, b);
+    }
+    
+    @Test
+    public void subPN() {
+        TMetaVar a = metaVar(Polarity.POSITIVE);
+        TMetaVar b = metaVar(Polarity.NEGATIVE);
+        sub(a, b);
+        SubSolver2.solve(errorLog, subsumptions);
+        Assert.assertEquals(0, errorLog.getErrorCount());
+        Assert.assertNotEquals(a, b);
+    }
+    
+    @Test
+    public void subNP() {
+        TMetaVar a = metaVar(Polarity.NEGATIVE);
+        TMetaVar b = metaVar(Polarity.POSITIVE);
+        sub(a, b);
+        SubSolver2.solve(errorLog, subsumptions);
+        Assert.assertEquals(0, errorLog.getErrorCount());
+        Assert.assertEquals(a, b);
+    }
+    
+    @Test
+    public void loop() {
+        TMetaVar a = metaVar(Polarity.BIPOLAR);
+        TMetaVar b = metaVar(Polarity.BIPOLAR);
+        TMetaVar c = metaVar(Polarity.BIPOLAR);
+        sub(a, b);
+        sub(b, c);
+        sub(c, a);
+        SubSolver2.solve(errorLog, subsumptions);
+        Assert.assertEquals(0, errorLog.getErrorCount());
+        Assert.assertEquals(a, b);
+        Assert.assertEquals(a, c);
+    }
+    
+    @Test
+    public void union() {
+        TMetaVar a = metaVar(Polarity.POSITIVE);
+        TMetaVar b = metaVar(Polarity.POSITIVE);
+        sub(a, Types.union(a, b));
+        sub(Types.PROC, b);
+        SubSolver2.solve(errorLog, subsumptions);
+        Assert.assertEquals(0, errorLog.getErrorCount());
+        Assert.assertEquals(Types.PROC, b);
+    }
+    
+    @Test
+    public void union2() {
+        TMetaVar a = metaVar(Polarity.POSITIVE);
+        TMetaVar b = metaVar(Polarity.POSITIVE);
+        sub(Types.union(a, Types.PROC), Types.union(a, b));
+        SubSolver2.solve(errorLog, subsumptions);
+        Assert.assertEquals(0, errorLog.getErrorCount());
+        Assert.assertNotEquals(Types.NO_EFFECTS, b);
+    }
+}