Changeset 4285

Timestamp:

10/23/09 18:11:33 (5 weeks ago)

Author:

jrhil47

Message:

[Constraint Formulas] Made scala constraints normalize types. Decoupled them from the java code.

[Type Checker] Fixed a bug with typechecking functions that have recursive bounds on their type parameters.

Location:

trunk/ProjectFortress/src/com/sun/fortress

Files:

• compiler/typechecker/TypeChecker.java (modified) (1 diff)
• compiler/typechecker/TypeCheckerResult.java (modified) (1 diff)
• compiler/typechecker/constraints/ConjunctiveFormula.java (modified) (1 diff)
• compiler/typechecker/constraints/ConstraintUtil.java (moved) (moved from trunk/ProjectFortress/src/com/sun/fortress/compiler/typechecker/constraints/JavaConstraintUtil.java) (1 diff)
• compiler/typechecker/constraints/DisjunctiveFormula.java (modified) (1 diff)
• compiler/typechecker/constraints/PartiallySolvedFormula.java (modified) (1 diff)
• scala_src/overloading/OverloadingOracle.scala (modified) (1 diff)
• scala_src/typechecker/ConstraintFormula.scala (moved) (moved from trunk/ProjectFortress/src/com/sun/fortress/scala_src/typechecker/ScalaConstraint.scala) (12 diffs)
• scala_src/typechecker/ConstraintJUTest.scala (moved) (moved from trunk/ProjectFortress/src/com/sun/fortress/scala_src/typechecker/ScalaConstraintJUTest.scala) (3 diffs)
• scala_src/typechecker/STypeChecker.scala (modified) (1 diff)
• scala_src/typechecker/ScalaConstraintUtil.scala (deleted)
• scala_src/types/CoveringAnalyzer.scala (modified) (3 diffs)
• scala_src/types/TypeAnalyzer.scala (modified) (7 diffs)
• scala_src/types/TypeAnalyzerJUTest.scala (modified) (1 diff)
• scala_src/useful/STypesUtil.scala (modified) (9 diffs)

trunk/ProjectFortress/src/com/sun/fortress/compiler/typechecker/TypeChecker.java

@@ -25 +25 @@
 import static edu.rice.cs.plt.tuple.Option.some;
 import static edu.rice.cs.plt.tuple.Option.wrap;
-import static com.sun.fortress.compiler.typechecker.constraints.JavaConstraintUtil.*;
+import static com.sun.fortress.compiler.typechecker.constraints.ConstraintUtil.*;
 
 import java.math.BigInteger;

trunk/ProjectFortress/src/com/sun/fortress/compiler/typechecker/TypeCheckerResult.java

@@ -50 +50 @@
 
 import static com.sun.fortress.exceptions.InterpreterBug.bug;
-import static com.sun.fortress.compiler.typechecker.constraints.JavaConstraintUtil.*;
+import static com.sun.fortress.compiler.typechecker.constraints.ConstraintUtil.*;
 
 public class TypeCheckerResult extends StaticPhaseResult {

trunk/ProjectFortress/src/com/sun/fortress/compiler/typechecker/constraints/ConjunctiveFormula.java

@@ -25 +25 @@
 import java.util.Set;
 
-import static com.sun.fortress.compiler.typechecker.constraints.JavaConstraintUtil.*;
+import static com.sun.fortress.compiler.typechecker.constraints.ConstraintUtil.*;
 
 import com.sun.fortress.compiler.Types;
 import com.sun.fortress.compiler.typechecker.SubtypeHistory;
-import com.sun.fortress.compiler.typechecker.constraints.JavaConstraintUtil.TypeExpander;
+import com.sun.fortress.compiler.typechecker.constraints.ConstraintUtil.TypeExpander;
 import com.sun.fortress.exceptions.InterpreterBug;
 import com.sun.fortress.nodes.Node;

trunk/ProjectFortress/src/com/sun/fortress/compiler/typechecker/constraints/ConstraintUtil.java

@@ -33 +33 @@
 import com.sun.fortress.useful.UsefulPLT;
 
-public class JavaConstraintUtil {
+public class ConstraintUtil {
 
         static protected class TypeExpander extends NodeUpdateVisitor{

trunk/ProjectFortress/src/com/sun/fortress/compiler/typechecker/constraints/DisjunctiveFormula.java

@@ -34 +34 @@
 import edu.rice.cs.plt.iter.IterUtil;
 import edu.rice.cs.plt.lambda.Lambda;
-import static com.sun.fortress.compiler.typechecker.constraints.JavaConstraintUtil.*;
+import static com.sun.fortress.compiler.typechecker.constraints.ConstraintUtil.*;
 
 

trunk/ProjectFortress/src/com/sun/fortress/compiler/typechecker/constraints/PartiallySolvedFormula.java

@@ -29 +29 @@
 import edu.rice.cs.plt.collect.CollectUtil;
 import edu.rice.cs.plt.lambda.Lambda;
-import static com.sun.fortress.compiler.typechecker.constraints.JavaConstraintUtil.*;
+import static com.sun.fortress.compiler.typechecker.constraints.ConstraintUtil.*;
 
 /**

trunk/ProjectFortress/src/com/sun/fortress/scala_src/overloading/OverloadingOracle.scala

@@ -27 +27 @@
 import com.sun.fortress.nodes_util.NodeFactory._
 import com.sun.fortress.scala_src.nodes._
-import com.sun.fortress.scala_src.typechecker.ScalaConstraint
+import com.sun.fortress.scala_src.typechecker.ConstraintFormula
 import com.sun.fortress.scala_src.typechecker.CnFalse
 import com.sun.fortress.scala_src.typechecker.CnTrue

trunk/ProjectFortress/src/com/sun/fortress/scala_src/typechecker/ConstraintFormula.scala

@@ -25 +25 @@
 import com.sun.fortress.compiler.typechecker.SubtypeHistory
 import com.sun.fortress.compiler.typechecker.InferenceVarReplacer
-import com.sun.fortress.compiler.typechecker.constraints.ConstraintFormula
 import com.sun.fortress.exceptions.InterpreterBug.bug
+import com.sun.fortress.scala_src.types.TypeAnalyzer
 import com.sun.fortress.scala_src.useful.Maps._
 import com.sun.fortress.scala_src.useful.Sets._
 import com.sun.fortress.scala_src.useful.STypesUtil
-import com.sun.fortress.scala_src.useful.STypesUtil.Subtype
 import edu.rice.cs.plt.lambda.Lambda
 
 /**
  * This class represents the constraints accummulated on inference variables. All
- * constraints are kept in disjunctive normal form. In scalaOrder to keep the size of
- * the scalaOr method eliminates redundant constraints. Further information can be found
+ * constraints are kept in disjunctive normal form. In order to keep the size of
+ * the or method eliminates redundant constraints. Further information can be found
  * in Section 3.2.2 of Dan Smith's paper Java Type Inference is Broken.
  * 
  * Currently it also works as a wrapper to interface with the Java Constraint Formulas
  * 
- * @TODO: Top type for inference is ANY or BOTTOM?
- */
-sealed abstract class ScalaConstraint extends ConstraintFormula{
-  /**
-   * This method scalaAnds two constraint formulas
-   */
-  def scalaAnd(c2 :ScalaConstraint, newSubtype: Subtype): ScalaConstraint
-
-  /**
-   * This method scalaOrs two constraint formulas
-   */
-  def scalaOr(c2: ScalaConstraint, newSubtype: Subtype): ScalaConstraint
+ * @TODO: Top type for inference is ANY or Object?
+ */
+sealed abstract class ConstraintFormula {
+  /**
+   * This method ands two constraint formulas
+   */
+  def and(c2 :ConstraintFormula, newTa: TypeAnalyzer): ConstraintFormula
+
+  /**
+   * This method ors two constraint formulas
+   */
+  def or(c2: ConstraintFormula, newTa: TypeAnalyzer): ConstraintFormula
 
   /**
    * This method is used to determine whether a constraint formula is redundant
    */
-  def implies(c2: ScalaConstraint, newSubtype: Subtype) : Boolean
+  def implies(c2: ConstraintFormula, newTa: TypeAnalyzer) : Boolean
+  
+  def isTrue(): Boolean = false
+  
+  def isFalse(): Boolean = false
   
   /**
    * 
    */
-  def reduce(): ScalaConstraint
+  def reduce(): ConstraintFormula
   
   
@@ -71 +74 @@
    * inference variables that satisfies the constraints.
    */
-  def scalaSolve(bounds: Map[_InferenceVarType,Type]): Option[Map[_InferenceVarType,Type]]
-  
-  override def and(c: ConstraintFormula, h: SubtypeHistory):ConstraintFormula = c match{
-    case c2:ScalaConstraint => scalaAnd(c2,(t1,t2)=>h.subtypeNormal(t1,t2).isTrue)
-    case _ => bug("Can't and a scala formula with a java formula")
-  }
-  
-  override def or(c: ConstraintFormula, h: SubtypeHistory):ConstraintFormula = c match{
-    case c2:ScalaConstraint => scalaOr(c2,(t1,t2)=>h.subtypeNormal(t1,t2).isTrue)
-    case _ => bug("Can't or a scala formula with a java formula")
-  }
-  
-  override def solve() = bug("Use scalaSolve for scala formulas")
+  def solve(bounds: Map[_InferenceVarType,Type]): Option[Map[_InferenceVarType,Type]]
   
 }
@@ -91 +82 @@
  * The formula with bounds Any:>$i:>Bottom for all $i
  */
-object CnTrue extends ScalaConstraint{
-  override def scalaAnd(c2: ScalaConstraint, newSubtype: Subtype): ScalaConstraint = c2.reduce
-  
-  override def scalaOr(c2: ScalaConstraint, newSubtype: Subtype): ScalaConstraint = this
-  
-  override def implies(c2: ScalaConstraint, newSubtype: Subtype): Boolean = c2 match {
+object CnTrue extends ConstraintFormula{
+  override def and(c2: ConstraintFormula, newTa: TypeAnalyzer): ConstraintFormula = c2.reduce
+  
+  override def or(c2: ConstraintFormula, newTa: TypeAnalyzer): ConstraintFormula = this
+  
+  override def implies(c2: ConstraintFormula, newTa: TypeAnalyzer): Boolean = c2 match {
     case CnTrue => true
-    case CnAnd(u,l,h) => CnAnd(Map.empty,Map.empty,newSubtype).implies(c2,newSubtype)
-    case CnOr(conjuncts,h) => conjuncts.exists((c: ScalaConstraint)=> this.implies(c,newSubtype))
+    case CnAnd(u, l, t) => CnAnd(Map.empty,Map.empty, newTa).implies(c2, newTa)
+    case CnOr(conjuncts, t) => conjuncts.exists((c: ConstraintFormula)=> this.implies(c, newTa))
     case CnFalse => false
   }
   
-  override def scalaSolve(bounds: Map[_InferenceVarType,Type]): Option[Map[_InferenceVarType,Type]] = Some(Map.empty)
+  override def solve(bounds: Map[_InferenceVarType,Type]): Option[Map[_InferenceVarType,Type]] = Some(Map.empty)
   
   override def isTrue():Boolean = true
-  
-  override def applySubstitution(substitution: Lambda[Type,Type]): ScalaConstraint = this
-
-  override def reduce():ScalaConstraint = this
+
+  override def reduce():ConstraintFormula = this
 
   override def toString():String = "CnTrue"
@@ -117 +106 @@
  * The empty formula
  */
-case object CnFalse extends ScalaConstraint{
-  override def scalaAnd(c2: ScalaConstraint, newSubtype: Subtype): ScalaConstraint = this
-  
-  override def scalaOr(c2: ScalaConstraint, newSubtype: Subtype): ScalaConstraint = c2.reduce
-  
-  override def implies(c2: ScalaConstraint, newSubtype: Subtype): Boolean = true
-  
-  override def scalaSolve(bounds: Map[_InferenceVarType,Type]): Option[Map[_InferenceVarType,Type]] = None
+case object CnFalse extends ConstraintFormula{
+  override def and(c2: ConstraintFormula, newTa: TypeAnalyzer): ConstraintFormula = this
+  
+  override def or(c2: ConstraintFormula, newTa: TypeAnalyzer): ConstraintFormula = c2.reduce
+  
+  override def implies(c2: ConstraintFormula, newTa: TypeAnalyzer): Boolean = true
+  
+  override def solve(bounds: Map[_InferenceVarType,Type]): Option[Map[_InferenceVarType,Type]] = None
   
   override def isFalse():Boolean = true
-  
-  override def applySubstitution(substitution: Lambda[Type,Type]): ScalaConstraint = this
-
-  override def reduce():ScalaConstraint = this
+
+  override def reduce():ConstraintFormula = this
 
   override def toString():String = "CnFalse"
@@ -140 +127 @@
  * U>:$i>:B
  */
-case class CnAnd(uppers: Map[_InferenceVarType, Type], lowers: Map[_InferenceVarType, Type], subtype: Subtype) extends ScalaConstraint{
-
-  override def scalaAnd(c2: ScalaConstraint, newSubtype: Subtype): ScalaConstraint = c2 match{
+case class CnAnd(uppers: Map[_InferenceVarType, Type], lowers: Map[_InferenceVarType, Type], ta: TypeAnalyzer) extends ConstraintFormula{
+
+  override def and(c2: ConstraintFormula, newTa: TypeAnalyzer): ConstraintFormula = c2 match{
     case CnTrue => this.reduce
       
     case CnFalse => CnFalse
     
-    case CnAnd(u2,l2,h2) =>
-      val newUppers = mergeBounds(uppers,u2,(x:Type, y:Type) => NodeFactory.makeIntersectionType(x,y))
-      val newLowers = mergeBounds(lowers,l2,(x:Type, y:Type) => NodeFactory.makeUnionType(x,y))
-      CnAnd(newUppers,newLowers,newSubtype).reduce
+    case CnAnd(u2, l2, t2) =>
+      val newUppers = mergeBounds(uppers, u2, (x:Type, y:Type) => ta.meet(x, y))
+      val newLowers = mergeBounds(lowers, l2, (x:Type, y:Type) => ta.join(x, y))
+      CnAnd(newUppers, newLowers, newTa).reduce
     
-    case CnOr(conjuncts,h2) =>
-      val newConjuncts=conjuncts.map((sf: ScalaConstraint)=>this.scalaAnd(sf,newSubtype))
-      newConjuncts.foldRight(CnFalse.asInstanceOf[ScalaConstraint])((c1: ScalaConstraint, c2: ScalaConstraint) => c1.scalaOr(c2,newSubtype))
-  }
-
-  override def scalaOr(c2: ScalaConstraint, newSubtype: Subtype): ScalaConstraint = c2 match{
+    case CnOr(conjuncts, t2) =>
+      val newConjuncts = conjuncts.map((sf: ConstraintFormula) => this.and(sf, newTa))
+      newConjuncts.foldRight(CnFalse.asInstanceOf[ConstraintFormula])((c1: ConstraintFormula, c2: ConstraintFormula) => c1.or(c2, newTa))
+  }
+
+  override def or(c2: ConstraintFormula, newTa: TypeAnalyzer): ConstraintFormula = c2 match{
     case CnTrue => c2.reduce
     case CnFalse => this.reduce
-    case c2@CnAnd(u2,l2,h2) => (this.implies(c2,newSubtype),c2.implies(this,newSubtype)) match{
-      case (false,false) => CnOr(this::List(c2),newSubtype).reduce
-      case (true,false) => c2.reduce
-      case (false,true) => this.reduce
-      case (true,true) => c2.reduce
+    case c2@CnAnd(u2, l2, t2) => (this.implies(c2, newTa),c2.implies(this, newTa)) match{
+      case (false, false) => CnOr(this::List(c2), newTa).reduce
+      case (true, false) => c2.reduce
+      case (false, true) => this.reduce
+      case (true, true) => c2.reduce
     }
     case CnOr(conjuncts,h2) =>
-      if(this.implies(c2,newSubtype))
+      if(this.implies(c2, newTa))
         return c2.reduce
-      val minimal = conjuncts.filter((sf: CnAnd)=> !sf.implies(this,newSubtype))
-      CnOr(this::minimal,newSubtype).reduce
-  }
-
-  override def implies(c2: ScalaConstraint, newSubtype: Subtype): Boolean = c2 match{
+      val minimal = conjuncts.filter((sf: CnAnd)=> !sf.implies(this, newTa))
+      CnOr(this::minimal, newTa).reduce
+  }
+
+  override def implies(c2: ConstraintFormula, newTa: TypeAnalyzer): Boolean = c2 match{
     case CnTrue => true
     //the CnFalse case is almost certainly wrong
-    case CnFalse => !compareBounds(lowers,uppers,BOTTOM,ANY,(t1: Type,t2:Type) => newSubtype(t1,t2))
+    case CnFalse => !compareBounds(lowers,uppers,BOTTOM,ANY, newTa.lteq)
     case CnAnd(u2,l2,h2) =>
-      val impliesUppers = compareBounds(uppers, u2, ANY , ANY,
-                                        (t1:Type, t2:Type) => newSubtype(t1,t2))
-      val impliesLowers = compareBounds(lowers, l2, BOTTOM, BOTTOM,
-                                        (t1:Type, t2:Type) => newSubtype(t2,t1))
+      val impliesUppers = compareBounds(uppers, u2, ANY , ANY, newTa.lteq)
+      val impliesLowers = compareBounds(lowers, l2, BOTTOM, BOTTOM, newTa.gteq)
       impliesUppers && impliesLowers
-    case CnOr(conjuncts,h) => conjuncts.exists((c: ScalaConstraint)=>this.implies(c,newSubtype)) 
-  }
-
-  override def scalaSolve(bounds: Map[_InferenceVarType,Type]): Option[Map[_InferenceVarType,Type]] = {
-    if(!isFalse && inBounds(lowers,bounds))
+    case CnOr(conjuncts,h) => conjuncts.exists((c: ConstraintFormula)=>this.implies(c, newTa)) 
+  }
+
+  override def solve(bounds: Map[_InferenceVarType,Type]): Option[Map[_InferenceVarType,Type]] = {
+    if(!isFalse && inBounds(lowers, bounds))
       Some(lowers)
     else
@@ -193 +178 @@
   }
   
-  override def isFalse(): Boolean = this.implies(CnFalse, subtype)
-  
-  override def isTrue(): Boolean = CnTrue.implies(this,subtype)
-  
-  override def reduce(): ScalaConstraint = {
+  override def isFalse(): Boolean = this.implies(CnFalse, ta)
+  
+  override def isTrue(): Boolean = CnTrue.implies(this, ta)
+  
+  override def reduce(): ConstraintFormula = {
     if(this.isTrue)
       return CnTrue
@@ -204 +189 @@
     this
   }
-  
-  override def applySubstitution(substitution: Lambda[Type,Type]): CnAnd = {
-    var newUppers = Map.empty[_InferenceVarType,Type]
-    for(key <- uppers.keys){
-      newUppers=newUppers.update(substitution.value(key).asInstanceOf[_InferenceVarType], substitution.value(uppers.apply(key)))
-    }
-    var newLowers = Map.empty[_InferenceVarType,Type]
-    for(key <- lowers.keys){
-      newLowers=newLowers.update(substitution.value(key).asInstanceOf[_InferenceVarType], substitution.value(lowers.apply(key)))
-    }
-    CnAnd(newUppers,newLowers,subtype)
-  }  
   
   /**
@@ -230 +203 @@
         (bound1,bound2) match{
           case (None, None) => ()
-          case (Some(b1), Some(b2)) => newBounds=newBounds.update(ivar, merge(b1,b2))
-          case (Some(b), None) => newBounds=newBounds.update(ivar,b)
-          case (None, Some(b)) => newBounds=newBounds.update(ivar,b)
+          case (Some(b1), Some(b2)) => newBounds=newBounds.update(ivar, merge(b1, b2))
+          case (Some(b), None) => newBounds=newBounds.update(ivar, b)
+          case (None, Some(b)) => newBounds=newBounds.update(ivar, b)
         }
       }
@@ -252 +225 @@
       (bound1,bound2) match{
         case (None, None) => true
-        case (Some(b1), Some(b2)) => compare(b1,b2)
-        case (Some(b), None) => compare(b,defaultBound2)
+        case (Some(b1), Some(b2)) => compare(b1, b2)
+        case (Some(b), None) => compare(b, defaultBound2)
         case (None, Some(b)) => compare(defaultBound1, b)
       }
@@ -267 +240 @@
     val pred = (ivar: _InferenceVarType) => {
       val bound  = bounds(ivar)
-      val newBound=STypesUtil.substituteTypesForInferenceVars(substitutions, bound)
+      val newBound = STypesUtil.substituteTypesForInferenceVars(substitutions, bound)
       substitutions.get(ivar) match {
-        case None => subtype(BOTTOM,newBound)
-        case Some(substitution) => subtype(substitution,newBound)
+        case None => ta.lteq(BOTTOM, newBound)
+        case Some(substitution) => ta.lteq(substitution, newBound)
       }
     }
@@ -304 +277 @@
  * A disjunction of simple formulas
  */
-case class CnOr(conjuncts: List[CnAnd], subtype: Subtype) extends ScalaConstraint{
-  
-  override def scalaAnd(c2: ScalaConstraint, newSubtype: Subtype): ScalaConstraint = c2 match{
+case class CnOr(conjuncts: List[CnAnd], ta: TypeAnalyzer) extends ConstraintFormula{
+  
+  override def and(c2: ConstraintFormula, newTa: TypeAnalyzer): ConstraintFormula = c2 match{
     case CnFalse => CnFalse
     case CnTrue => this.reduce
-    case CnAnd(u,l,h) => c2.scalaAnd(this,newSubtype)
-    case CnOr(conjuncts2,h2) =>
-      val newConjuncts = conjuncts.map((cf: ScalaConstraint) => cf.scalaAnd(c2,newSubtype))
-      newConjuncts.foldRight(CnFalse.asInstanceOf[ScalaConstraint])((c1: ScalaConstraint, c2: ScalaConstraint) => c1.scalaOr(c2,newSubtype))
-  }
-
-  override def scalaOr(c2: ScalaConstraint, newSubtype: Subtype): ScalaConstraint = c2 match{
+    case CnAnd(u, l, _) => c2.and(this, newTa)
+    case CnOr(conjuncts2, _) =>
+      val newConjuncts = conjuncts.map((cf: ConstraintFormula) => cf.and(c2, newTa))
+      newConjuncts.foldRight(CnFalse.asInstanceOf[ConstraintFormula])((c1, c2) => c1.or(c2, newTa))
+  }
+
+  override def or(c2: ConstraintFormula, newTa: TypeAnalyzer): ConstraintFormula = c2 match{
     case CnFalse => this.reduce
     case CnTrue => CnTrue
-    case CnAnd(u,l,h) => c2.scalaOr(this,newSubtype)
-    case CnOr(conjuncts2,h2) =>
+    case CnAnd(u, l, _) => c2.or(this, newTa)
+    case CnOr(conjuncts2, _) =>
       val newConjuncts = conjuncts.union(conjuncts2)
-      newConjuncts.foldRight(CnFalse.asInstanceOf[ScalaConstraint])((c1: ScalaConstraint, c2: ScalaConstraint) => c1.scalaOr(c2,newSubtype))
-  }
-
-  override def scalaSolve(bounds: Map[_InferenceVarType,Type]): Option[Map[_InferenceVarType,Type]] = {
+      newConjuncts.foldRight(CnFalse.asInstanceOf[ConstraintFormula])((c1, c2) => c1.or(c2, newTa))
+  }
+
+  override def solve(bounds: Map[_InferenceVarType,Type]): Option[Map[_InferenceVarType,Type]] = {
     for(conjunct <- conjuncts){
-      val solved = conjunct.scalaSolve(bounds)
+      val solved = conjunct.solve(bounds)
       if(solved.isDefined)
         return solved
@@ -333 +306 @@
   }
 
-  override def implies(c2: ScalaConstraint, newSubtype: Subtype) = conjuncts.forall((c: ScalaConstraint) => c.implies(c2,newSubtype))
-  
-  override def isFalse(): Boolean = this.implies(CnFalse, subtype)
-  
-  override def isTrue(): Boolean = CnTrue.implies(this,subtype)
-  
-  override def applySubstitution(substitution: Lambda[Type,Type]): ScalaConstraint = 
-    CnOr(conjuncts.map((c:CnAnd) => c.applySubstitution(substitution)),subtype)
-  
-  override def reduce(): ScalaConstraint = {
+  override def implies(c2: ConstraintFormula, newTa: TypeAnalyzer) = conjuncts.forall((c: ConstraintFormula) => c.implies(c2, newTa))
+  
+  override def isFalse(): Boolean = this.implies(CnFalse, ta)
+  
+  override def isTrue(): Boolean = CnTrue.implies(this, ta)
+  
+  override def reduce(): ConstraintFormula = {
     if(this.isTrue)
       return CnTrue

trunk/ProjectFortress/src/com/sun/fortress/scala_src/typechecker/ConstraintJUTest.scala

@@ -20 +20 @@
 import com.sun.fortress.compiler.typechecker.TypeAnalyzerJUTest._
 import _root_.junit.framework.TestCase
-import com.sun.fortress.compiler.typechecker.SubtypeHistory
-import com.sun.fortress.compiler.typechecker.TypeAnalyzer
+import com.sun.fortress.scala_src.types.TypeAnalyzer
 import com.sun.fortress.nodes_util.NodeFactory._
 import com.sun.fortress.nodes._
-
-class ScalaConstraintJUTest extends TestCase {
-
+import com.sun.fortress.scala_src.useful.TypeParser
+
+class ConstraintJUTest extends TestCase {
+
+  def typeAnalyzer(str:String) = TypeParser.parse(TypeParser.typeAnalyzer, str).get
+  def typ(str: String) = TypeParser.parse(TypeParser.typ, str).get
+  
   def testAnd() = {
-    val analyzer = makeAnalyzer()
-    val history = new SubtypeHistory(analyzer)
-    def subtype(t1: Type, t2: Type) = history.subtypeNormal(t1,t2).isTrue
+    val analyzer = typeAnalyzer("{}")
     //Test basic formulas
-    assert(CnFalse==CnFalse.scalaAnd(CnFalse,subtype), "AND(CnFalse,CnFalse)=/=CnFalse")
-    assert(CnFalse==CnFalse.scalaAnd(CnTrue,subtype), "AND(CnFalse,CnTrue)=/=CnFalse")
-    assert(CnFalse==CnTrue.scalaAnd(CnFalse,subtype), "AND(CnTrue,CnFalse)=/=CnFalse")
-    assert(CnTrue==CnTrue.scalaAnd(CnTrue,subtype), "AND(CnTrue,CnTrue)=/=CnTrue")
+    assert(CnFalse==CnFalse.and(CnFalse,analyzer), "AND(CnFalse,CnFalse)=/=CnFalse")
+    assert(CnFalse==CnFalse.and(CnTrue,analyzer), "AND(CnFalse,CnTrue)=/=CnFalse")
+    assert(CnFalse==CnTrue.and(CnFalse,analyzer), "AND(CnTrue,CnFalse)=/=CnFalse")
+    assert(CnTrue==CnTrue.and(CnTrue,analyzer), "AND(CnTrue,CnTrue)=/=CnTrue")
     //Test that CnAnd(Empty,Empty) acts like CnTrue
-    val alternateTrue = CnAnd(Map.empty,Map.empty,subtype)
+    val alternateTrue = CnAnd(Map.empty,Map.empty,analyzer)
     assert(alternateTrue.isTrue,"!CnAnd(Empty,Empty).isTrue")
-    assert(alternateTrue.scalaAnd(CnTrue,subtype)==CnTrue, "AND(alternateTrue,CnTrue) =/= CnTrue")
-    assert(alternateTrue.scalaAnd(CnFalse,subtype)==CnFalse, "AND(alternateTrue,CnFalse) =/= CnFalse")
-    assert(CnTrue.scalaAnd(alternateTrue,subtype)==CnTrue, "AND(CnTrue, alternateTrue) =/= CnTrue")
-    assert(CnFalse.scalaAnd(alternateTrue,subtype)==CnFalse, "AND(CnFalse, alternateTrue) =/= CnFalse")
+    assert(alternateTrue.and(CnTrue,analyzer)==CnTrue, "AND(alternateTrue,CnTrue) =/= CnTrue")
+    assert(alternateTrue.and(CnFalse,analyzer)==CnFalse, "AND(alternateTrue,CnFalse) =/= CnFalse")
+    assert(CnTrue.and(alternateTrue,analyzer)==CnTrue, "AND(CnTrue, alternateTrue) =/= CnTrue")
+    assert(CnFalse.and(alternateTrue,analyzer)==CnFalse, "AND(CnFalse, alternateTrue) =/= CnFalse")
     //Test that CnOr(CnAnd(Empty,Empty)) acts like CnTrue
-    val alternateTrue2 = CnOr(List(CnAnd(Map.empty,Map.empty,subtype)),subtype)
+    val alternateTrue2 = CnOr(List(CnAnd(Map.empty,Map.empty,analyzer)),analyzer)
     assert(alternateTrue2.isTrue,"CnOr(CnAnd(Empty,Empty)).isTrue")
-    assert(alternateTrue2.scalaAnd(CnTrue,subtype)==CnTrue, "AND(alternateTrue2,CnTrue) =/= CnTrue")
-    assert(alternateTrue2.scalaAnd(CnFalse,subtype)==CnFalse, "AND(alternateTrue2,CnFalse) =/= CnFalse")
-    assert(CnTrue.scalaAnd(alternateTrue2,subtype)==CnTrue, "AND(CnTrue, alternateTrue2) =/= CnTrue")
-    assert(CnFalse.scalaAnd(alternateTrue2,subtype)==CnFalse, "AND(CnFalse, alternateTrue2) =/= CnFalse")
+    assert(alternateTrue2.and(CnTrue,analyzer)==CnTrue, "AND(alternateTrue2,CnTrue) =/= CnTrue")
+    assert(alternateTrue2.and(CnFalse,analyzer)==CnFalse, "AND(alternateTrue2,CnFalse) =/= CnFalse")
+    assert(CnTrue.and(alternateTrue2,analyzer)==CnTrue, "AND(CnTrue, alternateTrue2) =/= CnTrue")
+    assert(CnFalse.and(alternateTrue2,analyzer)==CnFalse, "AND(CnFalse, alternateTrue2) =/= CnFalse")
     //Test that CnOr(Empty) acts like CnFalse
-    val alternateFalse = CnOr(List(),subtype)
+    val alternateFalse = CnOr(List(),analyzer)
     assert(alternateFalse.isFalse,"CnOr(Empty).isFalse")
-    assert(alternateFalse.scalaAnd(CnTrue,subtype)==CnFalse, "AND(alternateFalse,CnTrue) =/= CnTrue")
-    assert(alternateFalse.scalaAnd(CnFalse,subtype)==CnFalse, "AND(alternateFalse,CnFalse) =/= CnFalse")
-    assert(CnTrue.scalaAnd(alternateFalse,subtype)==CnFalse, "AND(CnFalse, alternateFalse) =/= CnFalse")
-    assert(CnFalse.scalaAnd(alternateFalse,subtype)==CnFalse, "AND(CnFalse, alternateFalse) =/= CnFalse")
+    assert(alternateFalse.and(CnTrue,analyzer)==CnFalse, "AND(alternateFalse,CnTrue) =/= CnTrue")
+    assert(alternateFalse.and(CnFalse,analyzer)==CnFalse, "AND(alternateFalse,CnFalse) =/= CnFalse")
+    assert(CnTrue.and(alternateFalse,analyzer)==CnFalse, "AND(CnFalse, alternateFalse) =/= CnFalse")
+    assert(CnFalse.and(alternateFalse,analyzer)==CnFalse, "AND(CnFalse, alternateFalse) =/= CnFalse")
     //Test test that all alternate forms are eliminated
-    assert(alternateTrue.scalaAnd(alternateTrue,subtype) == CnTrue, "AND(alternateTrue,alternateTrue) =/= CnTrue")
-    assert(alternateTrue.scalaAnd(alternateTrue2,subtype) == CnTrue, "AND(alternateTrue,alternateTrue2) =/= CnTrue")
-    assert(alternateTrue2.scalaAnd(alternateTrue,subtype) == CnTrue, "AND(alternateTrue2,alternateTrue) =/= CnTrue")
-    assert(alternateTrue2.scalaAnd(alternateTrue2,subtype) == CnTrue, "AND(alternateTrue2,alternateTrue2) =/= CnTrue")
-    assert(alternateTrue.scalaAnd(alternateFalse,subtype) == CnFalse, "AND(alternateTrue,alternateFalse) =/= CnFalse")
-    assert(alternateFalse.scalaAnd(alternateTrue,subtype) == CnFalse, "AND(alternateFalse,alternateTrue) =/= CnFalse")
-    assert(alternateTrue2.scalaAnd(alternateFalse,subtype) == CnFalse, "AND(alternateTrue2,alternateFalse) =/= CnFalse")
-    assert(alternateFalse.scalaAnd(alternateTrue2,subtype) == CnFalse, "AND(alternateFalse,alternateTrue2) =/= CnFalse")
-    assert(alternateFalse.scalaAnd(alternateFalse,subtype) == CnFalse, "AND(alternateFalse,alternateFalse) =/= CnFalse")
+    assert(alternateTrue.and(alternateTrue,analyzer) == CnTrue, "AND(alternateTrue,alternateTrue) =/= CnTrue")
+    assert(alternateTrue.and(alternateTrue2,analyzer) == CnTrue, "AND(alternateTrue,alternateTrue2) =/= CnTrue")
+    assert(alternateTrue2.and(alternateTrue,analyzer) == CnTrue, "AND(alternateTrue2,alternateTrue) =/= CnTrue")
+    assert(alternateTrue2.and(alternateTrue2,analyzer) == CnTrue, "AND(alternateTrue2,alternateTrue2) =/= CnTrue")
+    assert(alternateTrue.and(alternateFalse,analyzer) == CnFalse, "AND(alternateTrue,alternateFalse) =/= CnFalse")
+    assert(alternateFalse.and(alternateTrue,analyzer) == CnFalse, "AND(alternateFalse,alternateTrue) =/= CnFalse")
+    assert(alternateTrue2.and(alternateFalse,analyzer) == CnFalse, "AND(alternateTrue2,alternateFalse) =/= CnFalse")
+    assert(alternateFalse.and(alternateTrue2,analyzer) == CnFalse, "AND(alternateFalse,alternateTrue2) =/= CnFalse")
+    assert(alternateFalse.and(alternateFalse,analyzer) == CnFalse, "AND(alternateFalse,alternateFalse) =/= CnFalse")
   }
 
   def testOr() = {
-    val analyzer = makeAnalyzer()
-    val history = new SubtypeHistory(analyzer)
-    def subtype(t1: Type, t2: Type) = history.subtypeNormal(t1,t2).isTrue
+    val analyzer = typeAnalyzer("{}")
     //Test basic formulas
-    assert(CnFalse==CnFalse.scalaOr(CnFalse,subtype), "OR(CnFalse,CnFalse)=/=CnFalse")
-    assert(CnTrue==CnFalse.scalaOr(CnTrue,subtype), "OR(CnFalse,CnTrue)=/=CnTrue")
-    assert(CnTrue==CnTrue.scalaOr(CnFalse,subtype), "OR(CnTrue,CnFalse)=/=CnTrue")
-    assert(CnTrue==CnTrue.scalaOr(CnTrue,subtype), "OR(CnTrue,CnTrue)=/=CnTrue")
+    assert(CnFalse==CnFalse.or(CnFalse,analyzer), "OR(CnFalse,CnFalse)=/=CnFalse")
+    assert(CnTrue==CnFalse.or(CnTrue,analyzer), "OR(CnFalse,CnTrue)=/=CnTrue")
+    assert(CnTrue==CnTrue.or(CnFalse,analyzer), "OR(CnTrue,CnFalse)=/=CnTrue")
+    assert(CnTrue==CnTrue.or(CnTrue,analyzer), "OR(CnTrue,CnTrue)=/=CnTrue")
     //Test that CnAnd(Empty,Empty) acts like CnTrue
-    val alternateTrue = CnAnd(Map.empty,Map.empty,subtype)
-    assert(alternateTrue.scalaOr(CnTrue,subtype)==CnTrue, "OR(alternateTrue,CnTrue) == CnTrue")
-    assert(alternateTrue.scalaOr(CnFalse,subtype)==CnTrue, "OR(alternateTrue,CnFalse) == CnTrue")
-    assert(CnTrue.scalaOr(alternateTrue,subtype)==CnTrue, "OR(CnTrue, alternateTrue) == CnTrue")
-    assert(CnFalse.scalaOr(alternateTrue,subtype)==CnTrue, "OR(CnFalse, alternateTrue) == CnTrue")
+    val alternateTrue = CnAnd(Map.empty,Map.empty,analyzer)
+    assert(alternateTrue.or(CnTrue,analyzer)==CnTrue, "OR(alternateTrue,CnTrue) == CnTrue")
+    assert(alternateTrue.or(CnFalse,analyzer)==CnTrue, "OR(alternateTrue,CnFalse) == CnTrue")
+    assert(CnTrue.or(alternateTrue,analyzer)==CnTrue, "OR(CnTrue, alternateTrue) == CnTrue")
+    assert(CnFalse.or(alternateTrue,analyzer)==CnTrue, "OR(CnFalse, alternateTrue) == CnTrue")
     //Test that CnOr(CnAnd(Empty,Empty)) acts like CnTrue
-    val alternateTrue2 = CnOr(List(alternateTrue),subtype)
+    val alternateTrue2 = CnOr(List(alternateTrue),analyzer)
     assert(alternateTrue2.isTrue,"CnOr(CnAnd(Empty,Empty)).isTrue")
-    assert(alternateTrue2.scalaOr(CnTrue,subtype)==CnTrue, "OR(alternateTrue2,CnTrue) == CnTrue")
-    assert(alternateTrue2.scalaOr(CnFalse,subtype)==CnTrue, "OR(alternateTrue2,CnFalse) == CnTrue")
-    assert(CnTrue.scalaOr(alternateTrue2,subtype)==CnTrue, "OR(CnTrue, alternateTrue2) == CnTrue")
-    assert(CnFalse.scalaOr(alternateTrue2,subtype)==CnTrue, "OR(CnFalse, alternateTrue2) == CnTrue")
+    assert(alternateTrue2.or(CnTrue,analyzer)==CnTrue, "OR(alternateTrue2,CnTrue) == CnTrue")
+    assert(alternateTrue2.or(CnFalse,analyzer)==CnTrue, "OR(alternateTrue2,CnFalse) == CnTrue")
+    assert(CnTrue.or(alternateTrue2,analyzer)==CnTrue, "OR(CnTrue, alternateTrue2) == CnTrue")
+    assert(CnFalse.or(alternateTrue2,analyzer)==CnTrue, "OR(CnFalse, alternateTrue2) == CnTrue")
     //Test that CnOr(Empty) acts like CnFalse
-    val alternateFalse = CnOr(List(),subtype)
-    assert(alternateFalse.scalaOr(CnTrue,subtype)==CnTrue, "OR(alternateFalse,CnTrue) == CnTrue")
-    assert(alternateFalse.scalaOr(CnFalse,subtype)==CnFalse, "OR(alternateFalse,CnFalse) == CnFalse")
-    assert(CnTrue.scalaOr(alternateFalse,subtype)==CnTrue, "OR(CnFalse, alternateFalse) == CnTrue")
-    assert(CnFalse.scalaOr(alternateFalse,subtype)==CnFalse, "OR(CnFalse, alternateFalse) == CnFalse")
+    val alternateFalse = CnOr(List(),analyzer)
+    assert(alternateFalse.or(CnTrue,analyzer)==CnTrue, "OR(alternateFalse,CnTrue) == CnTrue")
+    assert(alternateFalse.or(CnFalse,analyzer)==CnFalse, "OR(alternateFalse,CnFalse) == CnFalse")
+    assert(CnTrue.or(alternateFalse,analyzer)==CnTrue, "OR(CnFalse, alternateFalse) == CnTrue")
+    assert(CnFalse.or(alternateFalse,analyzer)==CnFalse, "OR(CnFalse, alternateFalse) == CnFalse")
     //Test test that all alternate forms are eliminated
-    assert(alternateTrue.scalaOr(alternateTrue,subtype) == CnTrue, "OR(alternateTrue,alternateTrue) =/= CnTrue")
-    assert(alternateTrue.scalaOr(alternateTrue2,subtype) == CnTrue, "OR(alternateTrue,alternateTrue2) =/= CnTrue")
-    assert(alternateTrue2.scalaOr(alternateTrue,subtype) == CnTrue, "OR(alternateTrue2,alternateTrue) =/= CnTrue")
-    assert(alternateTrue2.scalaOr(alternateTrue2,subtype) == CnTrue, "OR(alternateTrue2,alternateTrue2) =/= CnTrue")
-    assert(alternateTrue.scalaOr(alternateFalse,subtype) == CnTrue, "OR(alternateTrue,alternateFalse) =/= CnTrue")
-    assert(alternateFalse.scalaOr(alternateTrue,subtype) == CnTrue, "OR(alternateFalse,alternateTrue) =/= CnTrue")
-    assert(alternateTrue2.scalaOr(alternateFalse,subtype) == CnTrue, "OR(alternateTrue2,alternateFalse) =/= CnTrue")
-    assert(alternateFalse.scalaOr(alternateTrue2,subtype) == CnTrue, "OR(alternateFalse,alternateTrue2) =/= CnTrue")
-    assert(alternateFalse.scalaOr(alternateFalse,subtype) == CnFalse, "OR(alternateFalse,alternateFalse) =/= CnFalse")
+    assert(alternateTrue.or(alternateTrue,analyzer) == CnTrue, "OR(alternateTrue,alternateTrue) =/= CnTrue")
+    assert(alternateTrue.or(alternateTrue2,analyzer) == CnTrue, "OR(alternateTrue,alternateTrue2) =/= CnTrue")
+    assert(alternateTrue2.or(alternateTrue,analyzer) == CnTrue, "OR(alternateTrue2,alternateTrue) =/= CnTrue")
+    assert(alternateTrue2.or(alternateTrue2,analyzer) == CnTrue, "OR(alternateTrue2,alternateTrue2) =/= CnTrue")
+    assert(alternateTrue.or(alternateFalse,analyzer) == CnTrue, "OR(alternateTrue,alternateFalse) =/= CnTrue")
+    assert(alternateFalse.or(alternateTrue,analyzer) == CnTrue, "OR(alternateFalse,alternateTrue) =/= CnTrue")
+    assert(alternateTrue2.or(alternateFalse,analyzer) == CnTrue, "OR(alternateTrue2,alternateFalse) =/= CnTrue")
+    assert(alternateFalse.or(alternateTrue2,analyzer) == CnTrue, "OR(alternateFalse,alternateTrue2) =/= CnTrue")
+    assert(alternateFalse.or(alternateFalse,analyzer) == CnFalse, "OR(alternateFalse,alternateFalse) =/= CnFalse")
   }
 
   def testImplies() = {
-    val analyzer = makeAnalyzer()
-    val history = new SubtypeHistory(analyzer)
-    def subtype(t1: Type, t2: Type) = history.subtypeNormal(t1,t2).isTrue
+    val analyzer = typeAnalyzer("{}")
     //Test basic formulas
-    assert(CnFalse.implies(CnFalse,subtype), "CnFalse -> CnFalse =/= true")
-    assert(CnFalse.implies(CnTrue,subtype), "CnFalse -> CnTrue =/= true")
-    assert(!CnTrue.implies(CnFalse,subtype), "CnTrue -> CnFalse =/= false")
-    assert(CnTrue.implies(CnTrue,subtype), "CnTrue -> CnTrue =/= true")
+    assert(CnFalse.implies(CnFalse,analyzer), "CnFalse -> CnFalse =/= true")
+    assert(CnFalse.implies(CnTrue,analyzer), "CnFalse -> CnTrue =/= true")
+    assert(!CnTrue.implies(CnFalse,analyzer), "CnTrue -> CnFalse =/= false")
+    assert(CnTrue.implies(CnTrue,analyzer), "CnTrue -> CnTrue =/= true")
     //Test that CnAnd(Empty,Empty) is equivalent to CnTrue
-    val alternateTrue = CnAnd(Map.empty,Map.empty,subtype)
+    val alternateTrue = CnAnd(Map.empty,Map.empty,analyzer)
     assert(alternateTrue.isTrue,"!CnAnd(Empty,Empty).isTrue")
     //Test that CnAnd(Empty,Empty) is equivalent to CnTrue
-    val alternateTrue2 = CnOr(List(alternateTrue),subtype)
+    val alternateTrue2 = CnOr(List(alternateTrue),analyzer)
     assert(alternateTrue2.isTrue,"CnOr(CnAnd(Empty,Empty)).isTrue")
     //Test that CnOr(Empty) is equivalent to CnFalse
-    val alternateFalse = CnOr(List(),subtype)
+    val alternateFalse = CnOr(List(),analyzer)
     assert(alternateFalse.isFalse,"CnOr(Empty).isFalse")
-    val analyzer2 = makeAnalyzer(makeTrait("A"),makeTrait("B","A"),makeTrait("C"),makeTrait("D","C"))
-    val history2 = new SubtypeHistory(analyzer2)
-    def subtype2(t1: Type, t2: Type) = history2.subtypeNormal(t1,t2).isTrue
+    val analyzer2 = typeAnalyzer("{trait Aa, trait Bb extends {Aa}, trait Cc, trait Dd extends {Cc}}")
     //Declarations
     val ivar1 = make_InferenceVarType(typeSpan)
     val ivar2 = make_InferenceVarType(typeSpan)
-    val typea = makeType("A")
-    val typeb = makeType("B")
-    val typec = makeType("C")
-    val typed = makeType("D")
+    val typea = typ("Aa")
+    val typeb = typ("Bb")
+    val typec = typ("Cc")
+    val typed = typ("Dd")
     val map1a = Map.empty.update(ivar1,typea)
     val map1b = Map.empty.update(ivar1,typeb)
@@ -147 +142 @@
     
     //Test that unsatisfiable formulas are equivalent to CnFalse
-    val c1b = CnAnd(map1b,map1c,subtype2)
+    val c1b = CnAnd(map1b,map1c,analyzer2)
     assert(c1b.isFalse,"c <: 1 <: b is not false ")
     //Test that a satisfiable formula is not false
-    val b1a = CnAnd(map1a,map1b,subtype2)
+    val b1a = CnAnd(map1a,map1b,analyzer2)
     assert(!b1a.isFalse,"b <: 1 <: a is false")
     //Test that implication works for conjunctions and disjunctions
-    val bot1b = CnAnd(map1b,Map.empty,subtype2)
-    val bot1a = CnAnd(map1a,Map.empty,subtype2)
-    assert(bot1b.implies(bot1a,subtype2),"(1 <: B) -> (1 <: A) =/= true")
-    val a1any = CnAnd(Map.empty, map1a, subtype2)
-    val b1any = CnAnd(Map.empty, map1b, subtype2)
-    assert(a1any.implies(b1any,subtype2),"(A <: 1) -> (B <: 1) =/= true")
-    val a2any = CnAnd(Map.empty, map2a, subtype2)
-    assert(!a1any.implies(a2any,subtype2),"(A <: 1) -> (A <: 2) =/= false")
-    val b2any = CnAnd(Map.empty, map2b, subtype2)
-    val a1anyAnda2any = a1any.scalaAnd(a2any,subtype2)
-    val b1anyAndb2any = b1any.scalaAnd(b2any,subtype2)
-    assert(a1anyAnda2any.implies(b1anyAndb2any,subtype2),"(A<:1 and A<:2)->(B<:1 and B<:2) =/= true")
-    assert(!b1anyAndb2any.implies(a1anyAnda2any,subtype2),"(B<:1 and B<:2)->(A<:1 and A<:2) =/= false")
-    val b1anyOrb2any = b1any.scalaOr(b2any,subtype2)
-    assert(a1anyAnda2any.implies(b1anyOrb2any,subtype2),"(A<:1 and A<:2)->(B<:1 or B<:2) =/= true")
-    val a1anyOrb1any = a1any.scalaOr(a1any,subtype2)
-    assert(a1anyOrb1any.implies(b1any,subtype2),"(A<:1 or B<:1)->(B<:1) =/= true")
-    assert(a1anyOrb1any.implies(a1any,subtype2),"(A<:1 or B<:1)->(A<:1) =/= false")
+    val bot1b = CnAnd(map1b,Map.empty,analyzer2)
+    val bot1a = CnAnd(map1a,Map.empty,analyzer2)
+    assert(bot1b.implies(bot1a,analyzer2),"(1 <: B) -> (1 <: A) =/= true")
+    val a1any = CnAnd(Map.empty, map1a, analyzer2)
+    val b1any = CnAnd(Map.empty, map1b, analyzer2)
+    assert(a1any.implies(b1any,analyzer2),"(A <: 1) -> (B <: 1) =/= true")
+    val a2any = CnAnd(Map.empty, map2a, analyzer2)
+    assert(!a1any.implies(a2any,analyzer2),"(A <: 1) -> (A <: 2) =/= false")
+    val b2any = CnAnd(Map.empty, map2b, analyzer2)
+    val a1anyAnda2any = a1any.and(a2any,analyzer2)
+    val b1anyAndb2any = b1any.and(b2any,analyzer2)
+    assert(a1anyAnda2any.implies(b1anyAndb2any,analyzer2),"(A<:1 and A<:2)->(B<:1 and B<:2) =/= true")
+    assert(!b1anyAndb2any.implies(a1anyAnda2any,analyzer2),"(B<:1 and B<:2)->(A<:1 and A<:2) =/= false")
+    val b1anyOrb2any = b1any.or(b2any,analyzer2)
+    assert(a1anyAnda2any.implies(b1anyOrb2any,analyzer2),"(A<:1 and A<:2)->(B<:1 or B<:2) =/= true")
+    val a1anyOrb1any = a1any.or(a1any,analyzer2)
+    assert(a1anyOrb1any.implies(b1any,analyzer2),"(A<:1 or B<:1)->(B<:1) =/= true")
+    assert(a1anyOrb1any.implies(a1any,analyzer2),"(A<:1 or B<:1)->(A<:1) =/= false")
   }
   
   def testSolve() = {
-    val analyzer = makeAnalyzer()
-    val history = new SubtypeHistory(analyzer)
-    def subtype(t1: Type, t2: Type) = history.subtypeNormal(t1,t2).isTrue
-    assert(CnFalse.scalaSolve(Map.empty).isEmpty, "SOLVE(CnFalse) =/= None")
-    assert(CnTrue.scalaSolve(Map.empty).get.isEmpty, "SOLVE(CnTrue) =/= Some(Nil)")
-    val alternateTrue = CnAnd(Map.empty,Map.empty,subtype)
-    val alternateTrue2 = CnOr(List(alternateTrue),subtype)
-    val alternateFalse = CnOr(List(),subtype)
-    assert(alternateFalse.scalaSolve(Map.empty).isEmpty, "SOLVE(CnFalse) =/= None")
-    assert(alternateTrue.scalaSolve(Map.empty).get.isEmpty, "SOLVE(CnTrue) =/= Some(Nil)")
-    assert(alternateTrue2.scalaSolve(Map.empty).get.isEmpty, "SOLVE(CnTrue) =/= Some(Nil)")
-    val analyzer2 = makeAnalyzer(makeTrait("A"),makeTrait("B","A"),makeTrait("C"),makeTrait("D","C"))
-    val history2 = new SubtypeHistory(analyzer2) 
-    def subtype2(t1: Type, t2: Type) = history2.subtypeNormal(t1,t2).isTrue
+    val analyzer = typeAnalyzer("{ }")
+    assert(CnFalse.solve(Map.empty).isEmpty, "SOLVE(CnFalse) =/= None")
+    assert(CnTrue.solve(Map.empty).get.isEmpty, "SOLVE(CnTrue) =/= Some(Nil)")
+    val alternateTrue = CnAnd(Map.empty,Map.empty,analyzer)
+    val alternateTrue2 = CnOr(List(alternateTrue),analyzer)
+    val alternateFalse = CnOr(List(),analyzer)
+    assert(alternateFalse.solve(Map.empty).isEmpty, "SOLVE(CnFalse) =/= None")
+    assert(alternateTrue.solve(Map.empty).get.isEmpty, "SOLVE(CnTrue) =/= Some(Nil)")
+    assert(alternateTrue2.solve(Map.empty).get.isEmpty, "SOLVE(CnTrue) =/= Some(Nil)")
+    val analyzer2 = typeAnalyzer("{trait Aa, trait Bb extends {Aa}, trait Cc, trait Dd extends {Cc}}")
         //Declarations
     val ivar1 = make_InferenceVarType(typeSpan)
     val ivar2 = make_InferenceVarType(typeSpan)
-    val typea = makeType("A")
-    val typeb = makeType("B")
-    val typec = makeType("C")
-    val typed = makeType("D")
+    val typea = typ("Aa")
+    val typeb = typ("Bb")
+    val typec = typ("Cc")
+    val typed = typ("Dd")
     val map1a = Map.empty.update(ivar1,typea)
     val map1b = Map.empty.update(ivar1,typeb)
@@ -203 +194 @@
     val map2c = Map.empty.update(ivar2,typec)
     val map2d = Map.empty.update(ivar2,typed)
-    val b1a = CnAnd(map1a,map1b,subtype2)
+    val b1a = CnAnd(map1a,map1b,analyzer2)
     //Check that solving a contradictory formula gives you nothing
-    val c1b = CnAnd(map1b,map1c,subtype2)
-    val solved_c1b = c1b.scalaSolve(Map.empty)
+    val c1b = CnAnd(map1b,map1c,analyzer2)
+    val solved_c1b = c1b.solve(Map.empty)
     //Check that solving a constraint with no bounds works
     assert(solved_c1b.isEmpty,"solve(C<:1<:B, {}) is not empty")
-    val solved_b1a = b1a.scalaSolve(Map.empty)
+    val solved_b1a = b1a.solve(Map.empty)
     assert(solved_b1a.isDefined && solved_b1a.get==map1b,"SOLVE(B<:1<:A , {}) = 1:=B")
     //Check that if the solution to a constraint is out of bounds it fails
-    val solved_b1a_1c = b1a.scalaSolve(map1c)
+    val solved_b1a_1c = b1a.solve(map1c)
     assert(solved_b1a_1c.isEmpty,"Solve(B<:1<:A, {1<:C}) is not empty")
     //Check that if the solution to a constraint is in bounds it succeeds
-    val solved_b1a_1a = b1a.scalaSolve(map1a)
+    val solved_b1a_1a = b1a.solve(map1a)
     assert(solved_b1a_1a.isDefined && solved_b1a_1a.get==map1b,"SOLVE(B<:1<:A, {1<:A}) = 1:=B")
   }

trunk/ProjectFortress/src/com/sun/fortress/scala_src/typechecker/STypeChecker.scala

@@ -288 +288 @@
    * Return the conditions for subtype <: supertype to hold.
    */
-  protected def checkSubtype(subtype: Type, supertype: Type): ScalaConstraint = {
-    val constraint = analyzer.subtype(subtype, supertype)
-    if (!constraint.isInstanceOf[ScalaConstraint]) {
-      bug("Not a ScalaConstraint.")
-    }
-    constraint.asInstanceOf[ScalaConstraint]
+  protected def checkSubtype(subtype: Type, supertype: Type): ConstraintFormula = {
+    analyzer.subtype(subtype, supertype)
   }
 

trunk/ProjectFortress/src/com/sun/fortress/scala_src/types/CoveringAnalyzer.scala

@@ -36 +36 @@
 class CoveringAnalyzer(ta: TypeAnalyzer) {
 
-  def minimalCover(x: Type): Type = ta.normalize(x) match {
+  def minimize(x: Type): Type = ta.normalize(x) match {
     case SIntersectionType(_, e) => 
       val (as, ts) = List.separate(e.map(_ match {
         case a:ArrowType => Left(a)
-        case t => Right(minimalCover(t))
+        case t => Right(minimize(t))
       }))
       ta.meet(ts)
-    case SUnionType(_, e) => ta.join(e.map(minimalCover))
-    case t:TraitType => makeUnionType(comprisesLeaves(t))
+    case SUnionType(_, e) => ta.join(e.map(minimize))
+    case t:TraitType => ta.join(comprisesLeaves(t))
     //ToDo: Handle keywords
-    case STupleType(i, e, mv, _) => STupleType(i, e.map(minimalCover), mv.map(minimalCover), Nil)
+    case STupleType(i, e, mv, _) => STupleType(i, e.map(minimize), mv.map(minimize), Nil)
     case SArrowType(i, d, r, e, io, m) =>
-      SArrowType(i, d, minimalCover(r), e, io, m)
+      SArrowType(i, d, minimize(r), e, io, m)
     case _ => x
   }
   
   private def mergeArrows(x: ArrowType, y: ArrowType): ArrowType = {
-    //val SArrowType(i1, d1, r1, SEffect(), io1, mi1) = x
-    //val SArrowType(i2, d2, r2, SEffect(), io2, mi2) = y
-    //SArrowType(_, ta.join(d1, d2), minimalcover(ta.meet(r1, r2)), io1 || io2, SEffect(), _)
-    x
+    val SArrowType(i1, d1, r1, e1, io1, mi1) = x
+    val SArrowType(i2, d2, r2, e2, io2, mi2) = y
+    //merge method info?
+    SArrowType(mergeTypeInfo(i1, i2),
+               ta.join(d1, d2),
+               minimize(ta.meet(r1, r2)), 
+               mergeEffects(e1, e2),
+               io1 || io2,
+               mi1)
   }
   
@@ -64 +69 @@
   }
   
+  private def mergeTypeInfo(x: TypeInfo, y: TypeInfo) = x
+  
+  private def mergeEffects(x: Effect, y: Effect) = {
+    val SEffect(i1, t1, io1) = x
+    val SEffect(i2, t2, io2) = y
+    val tc = minimize(ta.meet(ta.join(t1.getOrElse(Nil)), ta.join(t2.getOrElse(Nil)))) match {
+      case t:BottomType => None
+      case SUnionType(_, elts) => Some(elts)
+      case t => Some(List(t))
+    }
+    //merge ASTNodeInfo?
+    SEffect(i1, tc, io1 || io2)
+  }
+  
   private def comprisesLeaves(x: TraitType): Set[TraitType] = ta.comprisesClause(x) match {
     case ts if ts.isEmpty => Set(x)
@@ -69 +88 @@
   }
   
-
-  
-  
-  
 }

trunk/ProjectFortress/src/com/sun/fortress/scala_src/types/TypeAnalyzer.scala

@@ -26 +26 @@
 import com.sun.fortress.nodes_util.NodeFactory.typeSpan
 import com.sun.fortress.scala_src.nodes._
-import com.sun.fortress.scala_src.typechecker.ScalaConstraint
+import com.sun.fortress.scala_src.typechecker.ConstraintFormula
 import com.sun.fortress.scala_src.typechecker.CnFalse
 import com.sun.fortress.scala_src.typechecker.CnTrue
@@ -54 +54 @@
   def join(x: Iterable[Type]): Type = normalize(makeUnionType(x))
 
-  def subtype(x: Type, y: Type): ScalaConstraint = sub(normalize(x), normalize(y))
-
-  private def sub(x: Type, y: Type): ScalaConstraint = (x,y) match {
+  def subtype(x: Type, y: Type): ConstraintFormula = sub(normalize(x), normalize(y))
+
+  private def sub(x: Type, y: Type): ConstraintFormula = (x,y) match {
     case (s,t) if (s==t) => TRUE
     case (s: BottomType, _) => TRUE
@@ -109 +109 @@
   }
 
-  private def sub(x: List[KeywordType], y: List[KeywordType]): ScalaConstraint = {
+  private def sub(x: List[KeywordType], y: List[KeywordType]): ConstraintFormula = {
     def toPair(k: KeywordType) = (k.getName, k.getKeywordType)
     val xmap = Map(x.map(toPair):_*)
@@ -121 +121 @@
   }
 
-  private def sub(x: Effect, y: Effect): ScalaConstraint = {
+  private def sub(x: Effect, y: Effect): ConstraintFormula = {
     val (SEffect(_, tc1, io1), SEffect(_, tc2, io2)) = (x,y)
     if (!io1 || io2)
@@ -130 +130 @@
 
 
-  def equivalent(x: Type, y: Type): ScalaConstraint = {
+  def equivalent(x: Type, y: Type): ConstraintFormula = {
     val s = normalize(x)
     val t = normalize(y)
@@ -136 +136 @@
   }
 
-  private def eq(x: Type, y:Type): ScalaConstraint  = {
+  private def eq(x: Type, y:Type): ConstraintFormula  = {
     and(sub(x, y), sub(x, y))
   }
 
-  private def eq(x: StaticArg, y: StaticArg): ScalaConstraint = (x,y) match {
+  private def eq(x: StaticArg, y: StaticArg): ConstraintFormula = (x,y) match {
     case (STypeArg(_, _, s), STypeArg(_, _, t)) => eq(s, t)
     case (SIntArg(_, _, a), SIntArg(_, _, b)) => fromBoolean(a==b)
@@ -323 +323 @@
     new TypeAnalyzer(traits, env.extend(params, where))
   
-  private val TRUE: ScalaConstraint = CnTrue
-  private val FALSE: ScalaConstraint = CnFalse
-  private def and(x: ScalaConstraint, y: ScalaConstraint): ScalaConstraint =
-    x.scalaAnd(y, this.lteq)
-  private def or(x: ScalaConstraint, y: ScalaConstraint): ScalaConstraint =
-    x.scalaOr(y, this.lteq)
-  private def upperBound(i: _InferenceVarType, t: Type): ScalaConstraint =
-    CnAnd(Map((i,t)), Map(), this.lteq)
-  private def lowerBound(i: _InferenceVarType, t: Type): ScalaConstraint =
-    CnAnd(Map(), Map((i,t)), this.lteq)
+  private val TRUE: ConstraintFormula = CnTrue
+  private val FALSE: ConstraintFormula = CnFalse
+  private def and(x: ConstraintFormula, y: ConstraintFormula): ConstraintFormula =
+    x.and(y, this)
+  private def or(x: ConstraintFormula, y: ConstraintFormula): ConstraintFormula =
+    x.or(y, this)
+  private def upperBound(i: _InferenceVarType, t: Type): ConstraintFormula =
+    CnAnd(Map((i,t)), Map(), this)
+  private def lowerBound(i: _InferenceVarType, t: Type): ConstraintFormula =
+    CnAnd(Map(), Map((i,t)), this)
   private def fromBoolean(x: Boolean) = if (x) TRUE else FALSE
   

trunk/ProjectFortress/src/com/sun/fortress/scala_src/types/TypeAnalyzerJUTest.scala

@@ -62 +62 @@
     
     val ca = new CoveringAnalyzer(ta)
-    assert(ca.minimalCover(typ("&&{Aa, Ee}")) == typ("Dd"))
+    assert(ca.minimize(typ("&&{Aa, Ee}")) == typ("Dd"))
   }
   

trunk/ProjectFortress/src/com/sun/fortress/scala_src/useful/STypesUtil.scala

@@ -34 +34 @@
 import com.sun.fortress.nodes_util.{NodeUtil => NU}
 import com.sun.fortress.scala_src.nodes._
-import com.sun.fortress.scala_src.typechecker.ScalaConstraint
-import com.sun.fortress.scala_src.typechecker.ScalaConstraintUtil._
+import com.sun.fortress.scala_src.typechecker.ConstraintFormula
+import com.sun.fortress.scala_src.typechecker.CnFalse
+import com.sun.fortress.scala_src.typechecker.CnTrue
 import com.sun.fortress.scala_src.types.TypeAnalyzer
 import com.sun.fortress.scala_src.useful.Lists._
@@ -162 +163 @@
     // Get the substitution resulting from params :> expectedDomain
     val paramsDomain = makeDomainType(params).get
-    val subst = analyzer.subtype(expectedDomain, paramsDomain).
-                asInstanceOf[ScalaConstraint].scalaSolve(Map())
+    val subst = analyzer.subtype(expectedDomain, paramsDomain).solve(Map())
     subst.map(s =>
       params.map(p => p match {
@@ -405 +405 @@
   /** Return the [Scala-based] conditions for subtype <: supertype to hold. */
   def checkSubtype(subtype: Type, supertype: Type)
-                  (implicit analyzer: TypeAnalyzer): ScalaConstraint = {
+                  (implicit analyzer: TypeAnalyzer): ConstraintFormula = {
     val constraint = analyzer.subtype(subtype, supertype)
-    if (!constraint.isInstanceOf[ScalaConstraint]) {
-      bug("Not a ScalaConstraint.")
-    }
-    constraint.asInstanceOf[ScalaConstraint]
+    if (!constraint.isInstanceOf[ConstraintFormula]) {
+      bug("Not a ConstraintFormula.")
+    }
+    constraint.asInstanceOf[ConstraintFormula]
   }
 
@@ -660 +660 @@
 
     // Builds a constraint given the arrow with inference variables.
-    def makeConstraint(infArrow: ArrowType): ScalaConstraint = {
+    def makeConstraint(infArrow: ArrowType): ConstraintFormula = {
       
       // argType <:? dom(infArrow) yields a constraint, C1
@@ -667 +667 @@
       // if context given, C := C1 AND range(infArrow) <:? context
       val rangeConstraint = context.map(t =>
-        checkSubtype(infArrow.getRange, t)).getOrElse(TRUE_FORMULA)
-      domainConstraint.scalaAnd(rangeConstraint, isSubtype)
+        checkSubtype(infArrow.getRange, t)).getOrElse(CnTrue)
+      domainConstraint.and(rangeConstraint, analyzer)
     }
 
@@ -678 +678 @@
   def inferStaticParamsHelper(fnType: ArrowType,
                               sparams: List[StaticParam],
-                              constraintMaker: ArrowType => ScalaConstraint)
+                              constraintMaker: ArrowType => ConstraintFormula)
                              (implicit analyzer: TypeAnalyzer)
                               : Option[(ArrowType, List[StaticArg])] = {
@@ -700 +700 @@
     val infVars = sargs.flatMap(staticArgType)
     val sparamBounds = sparams.flatMap(staticParamBoundType).
-                               map(t => insertStaticParams(t, sparams))
+      map(t => staticInstantiation(sparams zip sargs, insertStaticParams(t, sparams)).get)
     val boundsMap = Map(infVars.zip(sparamBounds): _*)
 
     // 6. solve C to yield a substitution S' = [$T_i -> U_i]
-    val subst = constraint.scalaSolve(boundsMap).getOrElse(return None)
+    val subst = constraint.solve(boundsMap).getOrElse(return None)
 
     // 7. instantiate infArrow with [U_i] to get resultArrow
@@ -732 +732 @@
 
     // Builds a constraint given the arrow with inference variables.
-    def makeConstraint(infArrow: ArrowType): ScalaConstraint = {
+    def makeConstraint(infArrow: ArrowType): ConstraintFormula = {
     
       // Get the type of the `self` arg and form selfArg <:? selfType
@@ -738 +738 @@
       getTypeAt(argType, selfPosition) match {
         case Some(selfArgType) => checkSubtype(selfArgType, selfType)
-        case None => FALSE_FORMULA
+        case None => CnFalse
       }
     }