New solver for SCL effects inequalities

[simantics/platform.git] / bundles / org.simantics.scl.compiler / src / org / simantics / scl / compiler / internal / elaboration / subsumption2 / SubsumptionGraph.java

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
+++ b/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/internal/elaboration/subsumption2/SubsumptionGraph.java
@@ -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();
+        }
+
+    }
+}