New solver for SCL effects inequalities

[simantics/platform.git] / bundles / org.simantics.scl.compiler / src / org / simantics / scl / compiler / elaboration / contexts / TypingContext.java

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 ac004eab692a062e0777c0ebd1d8c3dab3329087..68468076d32fa155d81d3e7c82371d33162eff97 100644 (file)
--- 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,9 @@ 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;
 import org.simantics.scl.compiler.types.TForAll;
@@ -34,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;
@@ -116,8 +118,10 @@ public class TypingContext {
         
         if(a instanceof TMetaVar) {
             TMetaVar aVar = (TMetaVar)a;
-            if(b instanceof TMetaVar) 
+            if(b instanceof TMetaVar) {
+                Skeletons.unifySkeletons(a, b);
                 subsumptions.add(new Subsumption(loc, a, b));
+            }
             else {
                 if(b.contains(aVar))
                     throw new UnificationException(a, b);
@@ -182,6 +186,11 @@ public class TypingContext {
         else if(type instanceof TMetaVar) {
             TMetaVar var = (TMetaVar)type;
             TMetaVar newVar = Types.metaVar(var.getKind());
+            try {
+                newVar.setSkeletonRef(var);
+            } catch (UnificationException e) {
+                throw new InternalCompilerError(loc, e);
+            }
             subsumptions.add(new Subsumption(loc, newVar, var));
             return newVar;
         }
@@ -232,6 +241,11 @@ public class TypingContext {
         else if(type instanceof TMetaVar) {
             TMetaVar var = (TMetaVar)type;
             TMetaVar newVar = Types.metaVar(var.getKind());
+            try {
+                newVar.setSkeletonRef(var);
+            } catch (UnificationException e) {
+                throw new InternalCompilerError(loc, e);
+            }
             subsumptions.add(new Subsumption(loc, var, newVar));
             return newVar;
         }
@@ -372,7 +386,7 @@ public class TypingContext {
                 Types.unify(sub.a, sub.b);
             } catch (UnificationException e) {
                 // Should not happen. Both types should be metavars.
-                throw new InternalCompilerError();
+                throw new InternalCompilerError(e);
             }
         subsumptions.clear();
         return true;
@@ -393,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) {
@@ -472,7 +506,7 @@ public class TypingContext {
     public Expression solveConstraints(Environment environment, Expression expression) {
         ArrayList<EVariable> constraintDemand = getConstraintDemand();
         if(!constraintDemand.isEmpty()) {
-            ConstraintEnvironment ce = new ConstraintEnvironment(environment);
+            ConstraintEnvironment ce = new ConstraintEnvironment(compilationContext);
             ReducedConstraints red = ConstraintSolver.solve(
                     ce, new ArrayList<TPred>(0), constraintDemand,
                     true);