From: Hannu Niemistö Date: Wed, 25 Apr 2018 13:57:31 +0000 (+0300) Subject: New solver for SCL effects inequalities X-Git-Tag: v1.43.0~136^2~486 X-Git-Url: https://gerrit.simantics.org/r/gitweb?a=commitdiff_plain;h=e3cd3cd49bc2585f57d030a8743f9012f6161a92;p=simantics%2Fplatform.git New solver for SCL effects inequalities In particularly, solving of cyclic inequalities. Change-Id: I5d5734e9f029bf694221db2d7fc994d16d8d607a --- diff --git a/bundles/org.simantics.scl.compiler/META-INF/MANIFEST.MF b/bundles/org.simantics.scl.compiler/META-INF/MANIFEST.MF index 91014207d..7bfc9da61 100644 --- a/bundles/org.simantics.scl.compiler/META-INF/MANIFEST.MF +++ b/bundles/org.simantics.scl.compiler/META-INF/MANIFEST.MF @@ -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, diff --git a/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/compilation/TypeChecking.java b/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/compilation/TypeChecking.java index 373a9a333..ff713b170 100644 --- a/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/compilation/TypeChecking.java +++ b/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/compilation/TypeChecking.java @@ -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) { diff --git a/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/elaboration/contexts/TypingContext.java b/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/elaboration/contexts/TypingContext.java index f862d2128..68468076d 100644 --- a/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/elaboration/contexts/TypingContext.java +++ b/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/elaboration/contexts/TypingContext.java @@ -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 vars = new THashSet(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) { diff --git a/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/internal/elaboration/subsumption/SubSolver.java b/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/internal/elaboration/subsumption/SubSolver.java index 40f8fdf6a..088cf3396 100644 --- a/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/internal/elaboration/subsumption/SubSolver.java +++ b/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/internal/elaboration/subsumption/SubSolver.java @@ -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 index 000000000..3acd0ca74 --- /dev/null +++ b/bundles/org.simantics.scl.compiler/src/org/simantics/scl/compiler/internal/elaboration/subsumption2/SubSolver2.java @@ -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 subsumptions; + + // + private final EffectIdMap effectIds = new EffectIdMap(); + private final THashMap varNodeMap = new THashMap(); + private final ArrayList unionNodes = new ArrayList(); + + private static TIntIntHashMap STATISTICS = new TIntIntHashMap(); + + private SubSolver2(ErrorLog errorLog, ArrayList 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 aVars = new ArrayList(2); + ArrayList bVars = new ArrayList(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 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 set = new THashSet(); + 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 varSet = new THashSet(); + 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 activeSet = new THashSet<>(); + private final ArrayDeque 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(varNodeMap.size()); + for(VarNode node : varNodeMap.values()) + node.index = -1; + for(VarNode node : varNodeMap.values()) + if(node.index == -1) { + curIndex = 0; + stronglyConnectedComponents(node); + } + } + + ArrayList sortedNodes; + ArrayList stack = new ArrayList(); + 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 otherInComponent = new ArrayList(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 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 nameMap = new THashMap(); + 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 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 index 000000000..c38210853 --- /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(); + } + + } +} diff --git a/bundles/org.simantics.scl.runtime/scl/Prelude.scl b/bundles/org.simantics.scl.runtime/scl/Prelude.scl index 32582affa..4a51875b2 100644 --- a/bundles/org.simantics.scl.runtime/scl/Prelude.scl +++ b/bundles/org.simantics.scl.runtime/scl/Prelude.scl @@ -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]] diff --git a/tests/org.simantics.scl.compiler.tests/src/org/simantics/scl/compiler/tests/TestRegression.java b/tests/org.simantics.scl.compiler.tests/src/org/simantics/scl/compiler/tests/TestRegression.java index fcf31dd15..a2c4acc39 100644 --- a/tests/org.simantics.scl.compiler.tests/src/org/simantics/scl/compiler/tests/TestRegression.java +++ b/tests/org.simantics.scl.compiler.tests/src/org/simantics/scl/compiler/tests/TestRegression.java @@ -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 index 000000000..41913e215 --- /dev/null +++ b/tests/org.simantics.scl.compiler.tests/src/org/simantics/scl/compiler/tests/unit/TestSubSolver2.java @@ -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 subsumptions = new ArrayList(); + + 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); + } +}