Show
Ignore:
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:
1 removed
11 modified
3 moved

Legend:

Unmodified
Added
Removed

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

    r4280 r4285  
    2525import static edu.rice.cs.plt.tuple.Option.some; 
    2626import static edu.rice.cs.plt.tuple.Option.wrap; 
    27 import static com.sun.fortress.compiler.typechecker.constraints.JavaConstraintUtil.*; 
     27import static com.sun.fortress.compiler.typechecker.constraints.ConstraintUtil.*; 
    2828 
    2929import java.math.BigInteger; 

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

    r3966 r4285  
    5050 
    5151import static com.sun.fortress.exceptions.InterpreterBug.bug; 
    52 import static com.sun.fortress.compiler.typechecker.constraints.JavaConstraintUtil.*; 
     52import static com.sun.fortress.compiler.typechecker.constraints.ConstraintUtil.*; 
    5353 
    5454public class TypeCheckerResult extends StaticPhaseResult { 

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

    r3881 r4285  
    2525import java.util.Set; 
    2626 
    27 import static com.sun.fortress.compiler.typechecker.constraints.JavaConstraintUtil.*; 
     27import static com.sun.fortress.compiler.typechecker.constraints.ConstraintUtil.*; 
    2828 
    2929import com.sun.fortress.compiler.Types; 
    3030import com.sun.fortress.compiler.typechecker.SubtypeHistory; 
    31 import com.sun.fortress.compiler.typechecker.constraints.JavaConstraintUtil.TypeExpander; 
     31import com.sun.fortress.compiler.typechecker.constraints.ConstraintUtil.TypeExpander; 
    3232import com.sun.fortress.exceptions.InterpreterBug; 
    3333import com.sun.fortress.nodes.Node; 

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

    r3509 r4285  
    3333import com.sun.fortress.useful.UsefulPLT; 
    3434 
    35 public class JavaConstraintUtil { 
     35public class ConstraintUtil { 
    3636 
    3737        static protected class TypeExpander extends NodeUpdateVisitor{ 

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

    r3881 r4285  
    3434import edu.rice.cs.plt.iter.IterUtil; 
    3535import edu.rice.cs.plt.lambda.Lambda; 
    36 import static com.sun.fortress.compiler.typechecker.constraints.JavaConstraintUtil.*; 
     36import static com.sun.fortress.compiler.typechecker.constraints.ConstraintUtil.*; 
    3737 
    3838 

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

    r3448 r4285  
    2929import edu.rice.cs.plt.collect.CollectUtil; 
    3030import edu.rice.cs.plt.lambda.Lambda; 
    31 import static com.sun.fortress.compiler.typechecker.constraints.JavaConstraintUtil.*; 
     31import static com.sun.fortress.compiler.typechecker.constraints.ConstraintUtil.*; 
    3232 
    3333/** 

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

    r4267 r4285  
    2727import com.sun.fortress.nodes_util.NodeFactory._ 
    2828import com.sun.fortress.scala_src.nodes._ 
    29 import com.sun.fortress.scala_src.typechecker.ScalaConstraint 
     29import com.sun.fortress.scala_src.typechecker.ConstraintFormula 
    3030import com.sun.fortress.scala_src.typechecker.CnFalse 
    3131import com.sun.fortress.scala_src.typechecker.CnTrue 

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

    r4276 r4285  
    2525import com.sun.fortress.compiler.typechecker.SubtypeHistory 
    2626import com.sun.fortress.compiler.typechecker.InferenceVarReplacer 
    27 import com.sun.fortress.compiler.typechecker.constraints.ConstraintFormula 
    2827import com.sun.fortress.exceptions.InterpreterBug.bug 
     28import com.sun.fortress.scala_src.types.TypeAnalyzer 
    2929import com.sun.fortress.scala_src.useful.Maps._ 
    3030import com.sun.fortress.scala_src.useful.Sets._ 
    3131import com.sun.fortress.scala_src.useful.STypesUtil 
    32 import com.sun.fortress.scala_src.useful.STypesUtil.Subtype 
    3332import edu.rice.cs.plt.lambda.Lambda 
    3433 
    3534/** 
    3635 * This class represents the constraints accummulated on inference variables. All 
    37  * constraints are kept in disjunctive normal form. In scalaOrder to keep the size of 
    38  * the scalaOr method eliminates redundant constraints. Further information can be found 
     36 * constraints are kept in disjunctive normal form. In order to keep the size of 
     37 * the or method eliminates redundant constraints. Further information can be found 
    3938 * in Section 3.2.2 of Dan Smith's paper Java Type Inference is Broken. 
    4039 *  
    4140 * Currently it also works as a wrapper to interface with the Java Constraint Formulas 
    4241 *  
    43  * @TODO: Top type for inference is ANY or BOTTOM? 
    44  */ 
    45 sealed abstract class ScalaConstraint extends ConstraintFormula{ 
    46   /** 
    47    * This method scalaAnds two constraint formulas 
    48    */ 
    49   def scalaAnd(c2 :ScalaConstraint, newSubtype: Subtype): ScalaConstraint 
    50  
    51   /** 
    52    * This method scalaOrs two constraint formulas 
    53    */ 
    54   def scalaOr(c2: ScalaConstraint, newSubtype: Subtype): ScalaConstraint 
     42 * @TODO: Top type for inference is ANY or Object? 
     43 */ 
     44sealed abstract class ConstraintFormula { 
     45  /** 
     46   * This method ands two constraint formulas 
     47   */ 
     48  def and(c2 :ConstraintFormula, newTa: TypeAnalyzer): ConstraintFormula 
     49 
     50  /** 
     51   * This method ors two constraint formulas 
     52   */ 
     53  def or(c2: ConstraintFormula, newTa: TypeAnalyzer): ConstraintFormula 
    5554 
    5655  /** 
    5756   * This method is used to determine whether a constraint formula is redundant 
    5857   */ 
    59   def implies(c2: ScalaConstraint, newSubtype: Subtype) : Boolean 
     58  def implies(c2: ConstraintFormula, newTa: TypeAnalyzer) : Boolean 
     59   
     60  def isTrue(): Boolean = false 
     61   
     62  def isFalse(): Boolean = false 
    6063   
    6164  /** 
    6265   *  
    6366   */ 
    64   def reduce(): ScalaConstraint 
     67  def reduce(): ConstraintFormula 
    6568   
    6669   
    … …  
    7174   * inference variables that satisfies the constraints. 
    7275   */ 
    73   def scalaSolve(bounds: Map[_InferenceVarType,Type]): Option[Map[_InferenceVarType,Type]] 
    74    
    75   override def and(c: ConstraintFormula, h: SubtypeHistory):ConstraintFormula = c match{ 
    76     case c2:ScalaConstraint => scalaAnd(c2,(t1,t2)=>h.subtypeNormal(t1,t2).isTrue) 
    77     case _ => bug("Can't and a scala formula with a java formula") 
    78   } 
    79    
    80   override def or(c: ConstraintFormula, h: SubtypeHistory):ConstraintFormula = c match{ 
    81     case c2:ScalaConstraint => scalaOr(c2,(t1,t2)=>h.subtypeNormal(t1,t2).isTrue) 
    82     case _ => bug("Can't or a scala formula with a java formula") 
    83   } 
    84    
    85   override def solve() = bug("Use scalaSolve for scala formulas") 
     76  def solve(bounds: Map[_InferenceVarType,Type]): Option[Map[_InferenceVarType,Type]] 
    8677   
    8778} 
    … …  
    9182 * The formula with bounds Any:>$i:>Bottom for all $i 
    9283 */ 
    93 object CnTrue extends ScalaConstraint{ 
    94   override def scalaAnd(c2: ScalaConstraint, newSubtype: Subtype): ScalaConstraint = c2.reduce 
    95    
    96   override def scalaOr(c2: ScalaConstraint, newSubtype: Subtype): ScalaConstraint = this 
    97    
    98   override def implies(c2: ScalaConstraint, newSubtype: Subtype): Boolean = c2 match { 
     84object CnTrue extends ConstraintFormula{ 
     85  override def and(c2: ConstraintFormula, newTa: TypeAnalyzer): ConstraintFormula = c2.reduce 
     86   
     87  override def or(c2: ConstraintFormula, newTa: TypeAnalyzer): ConstraintFormula = this 
     88   
     89  override def implies(c2: ConstraintFormula, newTa: TypeAnalyzer): Boolean = c2 match { 
    9990    case CnTrue => true 
    100     case CnAnd(u,l,h) => CnAnd(Map.empty,Map.empty,newSubtype).implies(c2,newSubtype) 
    101     case CnOr(conjuncts,h) => conjuncts.exists((c: ScalaConstraint)=> this.implies(c,newSubtype)) 
     91    case CnAnd(u, l, t) => CnAnd(Map.empty,Map.empty, newTa).implies(c2, newTa) 
     92    case CnOr(conjuncts, t) => conjuncts.exists((c: ConstraintFormula)=> this.implies(c, newTa)) 
    10293    case CnFalse => false 
    10394  } 
    10495   
    105   override def scalaSolve(bounds: Map[_InferenceVarType,Type]): Option[Map[_InferenceVarType,Type]] = Some(Map.empty) 
     96  override def solve(bounds: Map[_InferenceVarType,Type]): Option[Map[_InferenceVarType,Type]] = Some(Map.empty) 
    10697   
    10798  override def isTrue():Boolean = true 
    108    
    109   override def applySubstitution(substitution: Lambda[Type,Type]): ScalaConstraint = this 
    110  
    111   override def reduce():ScalaConstraint = this 
     99 
     100  override def reduce():ConstraintFormula = this 
    112101 
    113102  override def toString():String = "CnTrue" 
    … …  
    117106 * The empty formula 
    118107 */ 
    119 case object CnFalse extends ScalaConstraint{ 
    120   override def scalaAnd(c2: ScalaConstraint, newSubtype: Subtype): ScalaConstraint = this 
    121    
    122   override def scalaOr(c2: ScalaConstraint, newSubtype: Subtype): ScalaConstraint = c2.reduce 
    123    
    124   override def implies(c2: ScalaConstraint, newSubtype: Subtype): Boolean = true 
    125    
    126   override def scalaSolve(bounds: Map[_InferenceVarType,Type]): Option[Map[_InferenceVarType,Type]] = None 
     108case object CnFalse extends ConstraintFormula{ 
     109  override def and(c2: ConstraintFormula, newTa: TypeAnalyzer): ConstraintFormula = this 
     110   
     111  override def or(c2: ConstraintFormula, newTa: TypeAnalyzer): ConstraintFormula = c2.reduce 
     112   
     113  override def implies(c2: ConstraintFormula, newTa: TypeAnalyzer): Boolean = true 
     114   
     115  override def solve(bounds: Map[_InferenceVarType,Type]): Option[Map[_InferenceVarType,Type]] = None 
    127116   
    128117  override def isFalse():Boolean = true 
    129    
    130   override def applySubstitution(substitution: Lambda[Type,Type]): ScalaConstraint = this 
    131  
    132   override def reduce():ScalaConstraint = this 
     118 
     119  override def reduce():ConstraintFormula = this 
    133120 
    134121  override def toString():String = "CnFalse" 
    … …  
    140127 * U>:$i>:B 
    141128 */ 
    142 case class CnAnd(uppers: Map[_InferenceVarType, Type], lowers: Map[_InferenceVarType, Type], subtype: Subtype) extends ScalaConstraint{ 
    143  
    144   override def scalaAnd(c2: ScalaConstraint, newSubtype: Subtype): ScalaConstraint = c2 match{ 
     129case class CnAnd(uppers: Map[_InferenceVarType, Type], lowers: Map[_InferenceVarType, Type], ta: TypeAnalyzer) extends ConstraintFormula{ 
     130 
     131  override def and(c2: ConstraintFormula, newTa: TypeAnalyzer): ConstraintFormula = c2 match{ 
    145132    case CnTrue => this.reduce 
    146133       
    147134    case CnFalse => CnFalse 
    148135     
    149     case CnAnd(u2,l2,h2) => 
    150       val newUppers = mergeBounds(uppers,u2,(x:Type, y:Type) => NodeFactory.makeIntersectionType(x,y)) 
    151       val newLowers = mergeBounds(lowers,l2,(x:Type, y:Type) => NodeFactory.makeUnionType(x,y)) 
    152       CnAnd(newUppers,newLowers,newSubtype).reduce 
     136    case CnAnd(u2, l2, t2) => 
     137      val newUppers = mergeBounds(uppers, u2, (x:Type, y:Type) => ta.meet(x, y)) 
     138      val newLowers = mergeBounds(lowers, l2, (x:Type, y:Type) => ta.join(x, y)) 
     139      CnAnd(newUppers, newLowers, newTa).reduce 
    153140     
    154     case CnOr(conjuncts,h2) => 
    155       val newConjuncts=conjuncts.map((sf: ScalaConstraint)=>this.scalaAnd(sf,newSubtype)) 
    156       newConjuncts.foldRight(CnFalse.asInstanceOf[ScalaConstraint])((c1: ScalaConstraint, c2: ScalaConstraint) => c1.scalaOr(c2,newSubtype)) 
    157   } 
    158  
    159   override def scalaOr(c2: ScalaConstraint, newSubtype: Subtype): ScalaConstraint = c2 match{ 
     141    case CnOr(conjuncts, t2) => 
     142      val newConjuncts = conjuncts.map((sf: ConstraintFormula) => this.and(sf, newTa)) 
     143      newConjuncts.foldRight(CnFalse.asInstanceOf[ConstraintFormula])((c1: ConstraintFormula, c2: ConstraintFormula) => c1.or(c2, newTa)) 
     144  } 
     145 
     146  override def or(c2: ConstraintFormula, newTa: TypeAnalyzer): ConstraintFormula = c2 match{ 
    160147    case CnTrue => c2.reduce 
    161148    case CnFalse => this.reduce 
    162     case c2@CnAnd(u2,l2,h2) => (this.implies(c2,newSubtype),c2.implies(this,newSubtype)) match{ 
    163       case (false,false) => CnOr(this::List(c2),newSubtype).reduce 
    164       case (true,false) => c2.reduce 
    165       case (false,true) => this.reduce 
    166       case (true,true) => c2.reduce 
     149    case c2@CnAnd(u2, l2, t2) => (this.implies(c2, newTa),c2.implies(this, newTa)) match{ 
     150      case (false, false) => CnOr(this::List(c2), newTa).reduce 
     151      case (true, false) => c2.reduce 
     152      case (false, true) => this.reduce 
     153      case (true, true) => c2.reduce 
    167154    } 
    168155    case CnOr(conjuncts,h2) => 
    169       if(this.implies(c2,newSubtype)) 
     156      if(this.implies(c2, newTa)) 
    170157        return c2.reduce 
    171       val minimal = conjuncts.filter((sf: CnAnd)=> !sf.implies(this,newSubtype)) 
    172       CnOr(this::minimal,newSubtype).reduce 
    173   } 
    174  
    175   override def implies(c2: ScalaConstraint, newSubtype: Subtype): Boolean = c2 match{ 
     158      val minimal = conjuncts.filter((sf: CnAnd)=> !sf.implies(this, newTa)) 
     159      CnOr(this::minimal, newTa).reduce 
     160  } 
     161 
     162  override def implies(c2: ConstraintFormula, newTa: TypeAnalyzer): Boolean = c2 match{ 
    176163    case CnTrue => true 
    177164    //the CnFalse case is almost certainly wrong 
    178     case CnFalse => !compareBounds(lowers,uppers,BOTTOM,ANY,(t1: Type,t2:Type) => newSubtype(t1,t2)) 
     165    case CnFalse => !compareBounds(lowers,uppers,BOTTOM,ANY, newTa.lteq) 
    179166    case CnAnd(u2,l2,h2) => 
    180       val impliesUppers = compareBounds(uppers, u2, ANY , ANY, 
    181                                         (t1:Type, t2:Type) => newSubtype(t1,t2)) 
    182       val impliesLowers = compareBounds(lowers, l2, BOTTOM, BOTTOM, 
    183                                         (t1:Type, t2:Type) => newSubtype(t2,t1)) 
     167      val impliesUppers = compareBounds(uppers, u2, ANY , ANY, newTa.lteq) 
     168      val impliesLowers = compareBounds(lowers, l2, BOTTOM, BOTTOM, newTa.gteq) 
    184169      impliesUppers && impliesLowers 
    185     case CnOr(conjuncts,h) => conjuncts.exists((c: ScalaConstraint)=>this.implies(c,newSubtype))  
    186   } 
    187  
    188   override def scalaSolve(bounds: Map[_InferenceVarType,Type]): Option[Map[_InferenceVarType,Type]] = { 
    189     if(!isFalse && inBounds(lowers,bounds)) 
     170    case CnOr(conjuncts,h) => conjuncts.exists((c: ConstraintFormula)=>this.implies(c, newTa))  
     171  } 
     172 
     173  override def solve(bounds: Map[_InferenceVarType,Type]): Option[Map[_InferenceVarType,Type]] = { 
     174    if(!isFalse && inBounds(lowers, bounds)) 
    190175      Some(lowers) 
    191176    else 
    … …  
    193178  } 
    194179   
    195   override def isFalse(): Boolean = this.implies(CnFalse, subtype) 
    196    
    197   override def isTrue(): Boolean = CnTrue.implies(this,subtype) 
    198    
    199   override def reduce(): ScalaConstraint = { 
     180  override def isFalse(): Boolean = this.implies(CnFalse, ta) 
     181   
     182  override def isTrue(): Boolean = CnTrue.implies(this, ta) 
     183   
     184  override def reduce(): ConstraintFormula = { 
    200185    if(this.isTrue) 
    201186      return CnTrue 
    … …  
    204189    this 
    205190  } 
    206    
    207   override def applySubstitution(substitution: Lambda[Type,Type]): CnAnd = { 
    208     var newUppers = Map.empty[_InferenceVarType,Type] 
    209     for(key <- uppers.keys){ 
    210       newUppers=newUppers.update(substitution.value(key).asInstanceOf[_InferenceVarType], substitution.value(uppers.apply(key))) 
    211     } 
    212     var newLowers = Map.empty[_InferenceVarType,Type] 
    213     for(key <- lowers.keys){ 
    214       newLowers=newLowers.update(substitution.value(key).asInstanceOf[_InferenceVarType], substitution.value(lowers.apply(key))) 
    215     } 
    216     CnAnd(newUppers,newLowers,subtype) 
    217   }   
    218191   
    219192  /** 
    … …  
    230203        (bound1,bound2) match{ 
    231204          case (None, None) => () 
    232           case (Some(b1), Some(b2)) => newBounds=newBounds.update(ivar, merge(b1,b2)) 
    233           case (Some(b), None) => newBounds=newBounds.update(ivar,b) 
    234           case (None, Some(b)) => newBounds=newBounds.update(ivar,b) 
     205          case (Some(b1), Some(b2)) => newBounds=newBounds.update(ivar, merge(b1, b2)) 
     206          case (Some(b), None) => newBounds=newBounds.update(ivar, b) 
     207          case (None, Some(b)) => newBounds=newBounds.update(ivar, b) 
    235208        } 
    236209      } 
    … …  
    252225      (bound1,bound2) match{ 
    253226        case (None, None) => true 
    254         case (Some(b1), Some(b2)) => compare(b1,b2) 
    255         case (Some(b), None) => compare(b,defaultBound2) 
     227        case (Some(b1), Some(b2)) => compare(b1, b2) 
     228        case (Some(b), None) => compare(b, defaultBound2) 
    256229        case (None, Some(b)) => compare(defaultBound1, b) 
    257230      } 
    … …  
    267240    val pred = (ivar: _InferenceVarType) => { 
    268241      val bound  = bounds(ivar) 
    269       val newBound=STypesUtil.substituteTypesForInferenceVars(substitutions, bound) 
     242      val newBound = STypesUtil.substituteTypesForInferenceVars(substitutions, bound) 
    270243      substitutions.get(ivar) match { 
    271         case None => subtype(BOTTOM,newBound) 
    272         case Some(substitution) => subtype(substitution,newBound) 
     244        case None => ta.lteq(BOTTOM, newBound) 
     245        case Some(substitution) => ta.lteq(substitution, newBound) 
    273246      } 
    274247    } 
    … …  
    304277 * A disjunction of simple formulas 
    305278 */ 
    306 case class CnOr(conjuncts: List[CnAnd], subtype: Subtype) extends ScalaConstraint{ 
    307    
    308   override def scalaAnd(c2: ScalaConstraint, newSubtype: Subtype): ScalaConstraint = c2 match{ 
     279case class CnOr(conjuncts: List[CnAnd], ta: TypeAnalyzer) extends ConstraintFormula{ 
     280   
     281  override def and(c2: ConstraintFormula, newTa: TypeAnalyzer): ConstraintFormula = c2 match{ 
    309282    case CnFalse => CnFalse 
    310283    case CnTrue => this.reduce 
    311     case CnAnd(u,l,h) => c2.scalaAnd(this,newSubtype) 
    312     case CnOr(conjuncts2,h2) => 
    313       val newConjuncts = conjuncts.map((cf: ScalaConstraint) => cf.scalaAnd(c2,newSubtype)) 
    314       newConjuncts.foldRight(CnFalse.asInstanceOf[ScalaConstraint])((c1: ScalaConstraint, c2: ScalaConstraint) => c1.scalaOr(c2,newSubtype)) 
    315   } 
    316  
    317   override def scalaOr(c2: ScalaConstraint, newSubtype: Subtype): ScalaConstraint = c2 match{ 
     284    case CnAnd(u, l, _) => c2.and(this, newTa) 
     285    case CnOr(conjuncts2, _) => 
     286      val newConjuncts = conjuncts.map((cf: ConstraintFormula) => cf.and(c2, newTa)) 
     287      newConjuncts.foldRight(CnFalse.asInstanceOf[ConstraintFormula])((c1, c2) => c1.or(c2, newTa)) 
     288  } 
     289 
     290  override def or(c2: ConstraintFormula, newTa: TypeAnalyzer): ConstraintFormula = c2 match{ 
    318291    case CnFalse => this.reduce 
    319292    case CnTrue => CnTrue 
    320     case CnAnd(u,l,h) => c2.scalaOr(this,newSubtype) 
    321     case CnOr(conjuncts2,h2) => 
     293    case CnAnd(u, l, _) => c2.or(this, newTa) 
     294    case CnOr(conjuncts2, _) => 
    322295      val newConjuncts = conjuncts.union(conjuncts2) 
    323       newConjuncts.foldRight(CnFalse.asInstanceOf[ScalaConstraint])((c1: ScalaConstraint, c2: ScalaConstraint) => c1.scalaOr(c2,newSubtype)) 
    324   } 
    325  
    326   override def scalaSolve(bounds: Map[_InferenceVarType,Type]): Option[Map[_InferenceVarType,Type]] = { 
     296      newConjuncts.foldRight(CnFalse.asInstanceOf[ConstraintFormula])((c1, c2) => c1.or(c2, newTa)) 
     297  } 
     298 
     299  override def solve(bounds: Map[_InferenceVarType,Type]): Option[Map[_InferenceVarType,Type]] = { 
    327300    for(conjunct <- conjuncts){ 
    328       val solved = conjunct.scalaSolve(bounds) 
     301      val solved = conjunct.solve(bounds) 
    329302      if(solved.isDefined) 
    330303        return solved 
    … …  
    333306  } 
    334307 
    335   override def implies(c2: ScalaConstraint, newSubtype: Subtype) = conjuncts.forall((c: ScalaConstraint) => c.implies(c2,newSubtype)) 
    336    
    337   override def isFalse(): Boolean = this.implies(CnFalse, subtype) 
    338    
    339   override def isTrue(): Boolean = CnTrue.implies(this,subtype) 
    340    
    341   override def applySubstitution(substitution: Lambda[Type,Type]): ScalaConstraint =  
    342     CnOr(conjuncts.map((c:CnAnd) => c.applySubstitution(substitution)),subtype) 
    343    
    344   override def reduce(): ScalaConstraint = { 
     308  override def implies(c2: ConstraintFormula, newTa: TypeAnalyzer) = conjuncts.forall((c: ConstraintFormula) => c.implies(c2, newTa)) 
     309   
     310  override def isFalse(): Boolean = this.implies(CnFalse, ta) 
     311   
     312  override def isTrue(): Boolean = CnTrue.implies(this, ta) 
     313   
     314  override def reduce(): ConstraintFormula = { 
    345315    if(this.isTrue) 
    346316      return CnTrue 

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

    r3813 r4285  
    2020import com.sun.fortress.compiler.typechecker.TypeAnalyzerJUTest._ 
    2121import _root_.junit.framework.TestCase 
    22 import com.sun.fortress.compiler.typechecker.SubtypeHistory 
    23 import com.sun.fortress.compiler.typechecker.TypeAnalyzer 
     22import com.sun.fortress.scala_src.types.TypeAnalyzer 
    2423import com.sun.fortress.nodes_util.NodeFactory._ 
    2524import com.sun.fortress.nodes._ 
    26  
    27 class ScalaConstraintJUTest extends TestCase { 
    28  
     25import com.sun.fortress.scala_src.useful.TypeParser 
     26 
     27class ConstraintJUTest extends TestCase { 
     28 
     29  def typeAnalyzer(str:String) = TypeParser.parse(TypeParser.typeAnalyzer, str).get 
     30  def typ(str: String) = TypeParser.parse(TypeParser.typ, str).get 
     31   
    2932  def testAnd() = { 
    30     val analyzer = makeAnalyzer() 
    31     val history = new SubtypeHistory(analyzer) 
    32     def subtype(t1: Type, t2: Type) = history.subtypeNormal(t1,t2).isTrue 
     33    val analyzer = typeAnalyzer("{}") 
    3334    //Test basic formulas 
    34     assert(CnFalse==CnFalse.scalaAnd(CnFalse,subtype), "AND(CnFalse,CnFalse)=/=CnFalse") 
    35     assert(CnFalse==CnFalse.scalaAnd(CnTrue,subtype), "AND(CnFalse,CnTrue)=/=CnFalse") 
    36     assert(CnFalse==CnTrue.scalaAnd(CnFalse,subtype), "AND(CnTrue,CnFalse)=/=CnFalse") 
    37     assert(CnTrue==CnTrue.scalaAnd(CnTrue,subtype), "AND(CnTrue,CnTrue)=/=CnTrue") 
     35    assert(CnFalse==CnFalse.and(CnFalse,analyzer), "AND(CnFalse,CnFalse)=/=CnFalse") 
     36    assert(CnFalse==CnFalse.and(CnTrue,analyzer), "AND(CnFalse,CnTrue)=/=CnFalse") 
     37    assert(CnFalse==CnTrue.and(CnFalse,analyzer), "AND(CnTrue,CnFalse)=/=CnFalse") 
     38    assert(CnTrue==CnTrue.and(CnTrue,analyzer), "AND(CnTrue,CnTrue)=/=CnTrue") 
    3839    //Test that CnAnd(Empty,Empty) acts like CnTrue 
    39     val alternateTrue = CnAnd(Map.empty,Map.empty,subtype) 
     40    val alternateTrue = CnAnd(Map.empty,Map.empty,analyzer) 
    4041    assert(alternateTrue.isTrue,"!CnAnd(Empty,Empty).isTrue") 
    41     assert(alternateTrue.scalaAnd(CnTrue,subtype)==CnTrue, "AND(alternateTrue,CnTrue) =/= CnTrue") 
    42     assert(alternateTrue.scalaAnd(CnFalse,subtype)==CnFalse, "AND(alternateTrue,CnFalse) =/= CnFalse") 
    43     assert(CnTrue.scalaAnd(alternateTrue,subtype)==CnTrue, "AND(CnTrue, alternateTrue) =/= CnTrue") 
    44     assert(CnFalse.scalaAnd(alternateTrue,subtype)==CnFalse, "AND(CnFalse, alternateTrue) =/= CnFalse") 
     42    assert(alternateTrue.and(CnTrue,analyzer)==CnTrue, "AND(alternateTrue,CnTrue) =/= CnTrue") 
     43    assert(alternateTrue.and(CnFalse,analyzer)==CnFalse, "AND(alternateTrue,CnFalse) =/= CnFalse") 
     44    assert(CnTrue.and(alternateTrue,analyzer)==CnTrue, "AND(CnTrue, alternateTrue) =/= CnTrue") 
     45    assert(CnFalse.and(alternateTrue,analyzer)==CnFalse, "AND(CnFalse, alternateTrue) =/= CnFalse") 
    4546    //Test that CnOr(CnAnd(Empty,Empty)) acts like CnTrue 
    46     val alternateTrue2 = CnOr(List(CnAnd(Map.empty,Map.empty,subtype)),subtype) 
     47    val alternateTrue2 = CnOr(List(CnAnd(Map.empty,Map.empty,analyzer)),analyzer) 
    4748    assert(alternateTrue2.isTrue,"CnOr(CnAnd(Empty,Empty)).isTrue") 
    48     assert(alternateTrue2.scalaAnd(CnTrue,subtype)==CnTrue, "AND(alternateTrue2,CnTrue) =/= CnTrue") 
    49     assert(alternateTrue2.scalaAnd(CnFalse,subtype)==CnFalse, "AND(alternateTrue2,CnFalse) =/= CnFalse") 
    50     assert(CnTrue.scalaAnd(alternateTrue2,subtype)==CnTrue, "AND(CnTrue, alternateTrue2) =/= CnTrue") 
    51     assert(CnFalse.scalaAnd(alternateTrue2,subtype)==CnFalse, "AND(CnFalse, alternateTrue2) =/= CnFalse") 
     49    assert(alternateTrue2.and(CnTrue,analyzer)==CnTrue, "AND(alternateTrue2,CnTrue) =/= CnTrue") 
     50    assert(alternateTrue2.and(CnFalse,analyzer)==CnFalse, "AND(alternateTrue2,CnFalse) =/= CnFalse") 
     51    assert(CnTrue.and(alternateTrue2,analyzer)==CnTrue, "AND(CnTrue, alternateTrue2) =/= CnTrue") 
     52    assert(CnFalse.and(alternateTrue2,analyzer)==CnFalse, "AND(CnFalse, alternateTrue2) =/= CnFalse") 
    5253    //Test that CnOr(Empty) acts like CnFalse 
    53     val alternateFalse = CnOr(List(),subtype) 
     54    val alternateFalse = CnOr(List(),analyzer) 
    5455    assert(alternateFalse.isFalse,"CnOr(Empty).isFalse") 
    55     assert(alternateFalse.scalaAnd(CnTrue,subtype)==CnFalse, "AND(alternateFalse,CnTrue) =/= CnTrue") 
    56     assert(alternateFalse.scalaAnd(CnFalse,subtype)==CnFalse, "AND(alternateFalse,CnFalse) =/= CnFalse") 
    57     assert(CnTrue.scalaAnd(alternateFalse,subtype)==CnFalse, "AND(CnFalse, alternateFalse) =/= CnFalse") 
    58     assert(CnFalse.scalaAnd(alternateFalse,subtype)==CnFalse, "AND(CnFalse, alternateFalse) =/= CnFalse") 
     56    assert(alternateFalse.and(CnTrue,analyzer)==CnFalse, "AND(alternateFalse,CnTrue) =/= CnTrue") 
     57    assert(alternateFalse.and(CnFalse,analyzer)==CnFalse, "AND(alternateFalse,CnFalse) =/= CnFalse") 
     58    assert(CnTrue.and(alternateFalse,analyzer)==CnFalse, "AND(CnFalse, alternateFalse) =/= CnFalse") 
     59    assert(CnFalse.and(alternateFalse,analyzer)==CnFalse, "AND(CnFalse, alternateFalse) =/= CnFalse") 
    5960    //Test test that all alternate forms are eliminated 
    60     assert(alternateTrue.scalaAnd(alternateTrue,subtype) == CnTrue, "AND(alternateTrue,alternateTrue) =/= CnTrue") 
    61     assert(alternateTrue.scalaAnd(alternateTrue2,subtype) == CnTrue, "AND(alternateTrue,alternateTrue2) =/= CnTrue") 
    62     assert(alternateTrue2.scalaAnd(alternateTrue,subtype) == CnTrue, "AND(alternateTrue2,alternateTrue) =/= CnTrue") 
    63     assert(alternateTrue2.scalaAnd(alternateTrue2,subtype) == CnTrue, "AND(alternateTrue2,alternateTrue2) =/= CnTrue") 
    64     assert(alternateTrue.scalaAnd(alternateFalse,subtype) == CnFalse, "AND(alternateTrue,alternateFalse) =/= CnFalse") 
    65     assert(alternateFalse.scalaAnd(alternateTrue,subtype) == CnFalse, "AND(alternateFalse,alternateTrue) =/= CnFalse") 
    66     assert(alternateTrue2.scalaAnd(alternateFalse,subtype) == CnFalse, "AND(alternateTrue2,alternateFalse) =/= CnFalse") 
    67     assert(alternateFalse.scalaAnd(alternateTrue2,subtype) == CnFalse, "AND(alternateFalse,alternateTrue2) =/= CnFalse") 
    68     assert(alternateFalse.scalaAnd(alternateFalse,subtype) == CnFalse, "AND(alternateFalse,alternateFalse) =/= CnFalse") 
     61    assert(alternateTrue.and(alternateTrue,analyzer) == CnTrue, "AND(alternateTrue,alternateTrue) =/= CnTrue") 
     62    assert(alternateTrue.and(alternateTrue2,analyzer) == CnTrue, "AND(alternateTrue,alternateTrue2) =/= CnTrue") 
     63    assert(alternateTrue2.and(alternateTrue,analyzer) == CnTrue, "AND(alternateTrue2,alternateTrue) =/= CnTrue") 
     64    assert(alternateTrue2.and(alternateTrue2,analyzer) == CnTrue, "AND(alternateTrue2,alternateTrue2) =/= CnTrue") 
     65    assert(alternateTrue.and(alternateFalse,analyzer) == CnFalse, "AND(alternateTrue,alternateFalse) =/= CnFalse") 
     66    assert(alternateFalse.and(alternateTrue,analyzer) == CnFalse, "AND(alternateFalse,alternateTrue) =/= CnFalse") 
     67    assert(alternateTrue2.and(alternateFalse,analyzer) == CnFalse, "AND(alternateTrue2,alternateFalse) =/= CnFalse") 
     68    assert(alternateFalse.and(alternateTrue2,analyzer) == CnFalse, "AND(alternateFalse,alternateTrue2) =/= CnFalse") 
     69    assert(alternateFalse.and(alternateFalse,analyzer) == CnFalse, "AND(alternateFalse,alternateFalse) =/= CnFalse") 
    6970  } 
    7071 
    7172  def testOr() = { 
    72     val analyzer = makeAnalyzer() 
    73     val history = new SubtypeHistory(analyzer) 
    74     def subtype(t1: Type, t2: Type) = history.subtypeNormal(t1,t2).isTrue 
     73    val analyzer = typeAnalyzer("{}") 
    7574    //Test basic formulas 
    76     assert(CnFalse==CnFalse.scalaOr(CnFalse,subtype), "OR(CnFalse,CnFalse)=/=CnFalse") 
    77     assert(CnTrue==CnFalse.scalaOr(CnTrue,subtype), "OR(CnFalse,CnTrue)=/=CnTrue") 
    78     assert(CnTrue==CnTrue.scalaOr(CnFalse,subtype), "OR(CnTrue,CnFalse)=/=CnTrue") 
    79     assert(CnTrue==CnTrue.scalaOr(CnTrue,subtype), "OR(CnTrue,CnTrue)=/=CnTrue") 
     75    assert(CnFalse==CnFalse.or(CnFalse,analyzer), "OR(CnFalse,CnFalse)=/=CnFalse") 
     76    assert(CnTrue==CnFalse.or(CnTrue,analyzer), "OR(CnFalse,CnTrue)=/=CnTrue") 
     77    assert(CnTrue==CnTrue.or(CnFalse,analyzer), "OR(CnTrue,CnFalse)=/=CnTrue") 
     78    assert(CnTrue==CnTrue.or(CnTrue,analyzer), "OR(CnTrue,CnTrue)=/=CnTrue") 
    8079    //Test that CnAnd(Empty,Empty) acts like CnTrue 
    81     val alternateTrue = CnAnd(Map.empty,Map.empty,subtype) 
    82     assert(alternateTrue.scalaOr(CnTrue,subtype)==CnTrue, "OR(alternateTrue,CnTrue) == CnTrue") 
    83     assert(alternateTrue.scalaOr(CnFalse,subtype)==CnTrue, "OR(alternateTrue,CnFalse) == CnTrue") 
    84     assert(CnTrue.scalaOr(alternateTrue,subtype)==CnTrue, "OR(CnTrue, alternateTrue) == CnTrue") 
    85     assert(CnFalse.scalaOr(alternateTrue,subtype)==CnTrue, "OR(CnFalse, alternateTrue) == CnTrue") 
     80    val alternateTrue = CnAnd(Map.empty,Map.empty,analyzer) 
     81    assert(alternateTrue.or(CnTrue,analyzer)==CnTrue, "OR(alternateTrue,CnTrue) == CnTrue") 
     82    assert(alternateTrue.or(CnFalse,analyzer)==CnTrue, "OR(alternateTrue,CnFalse) == CnTrue") 
     83    assert(CnTrue.or(alternateTrue,analyzer)==CnTrue, "OR(CnTrue, alternateTrue) == CnTrue") 
     84    assert(CnFalse.or(alternateTrue,analyzer)==CnTrue, "OR(CnFalse, alternateTrue) == CnTrue") 
    8685    //Test that CnOr(CnAnd(Empty,Empty)) acts like CnTrue 
    87     val alternateTrue2 = CnOr(List(alternateTrue),subtype) 
     86    val alternateTrue2 = CnOr(List(alternateTrue),analyzer) 
    8887    assert(alternateTrue2.isTrue,"CnOr(CnAnd(Empty,Empty)).isTrue") 
    89     assert(alternateTrue2.scalaOr(CnTrue,subtype)==CnTrue, "OR(alternateTrue2,CnTrue) == CnTrue") 
    90     assert(alternateTrue2.scalaOr(CnFalse,subtype)==CnTrue, "OR(alternateTrue2,CnFalse) == CnTrue") 
    91     assert(CnTrue.scalaOr(alternateTrue2,subtype)==CnTrue, "OR(CnTrue, alternateTrue2) == CnTrue") 
    92     assert(CnFalse.scalaOr(alternateTrue2,subtype)==CnTrue, "OR(CnFalse, alternateTrue2) == CnTrue") 
     88    assert(alternateTrue2.or(CnTrue,analyzer)==CnTrue, "OR(alternateTrue2,CnTrue) == CnTrue") 
     89    assert(alternateTrue2.or(CnFalse,analyzer)==CnTrue, "OR(alternateTrue2,CnFalse) == CnTrue") 
     90    assert(CnTrue.or(alternateTrue2,analyzer)==CnTrue, "OR(CnTrue, alternateTrue2) == CnTrue") 
     91    assert(CnFalse.or(alternateTrue2,analyzer)==CnTrue, "OR(CnFalse, alternateTrue2) == CnTrue") 
    9392    //Test that CnOr(Empty) acts like CnFalse 
    94     val alternateFalse = CnOr(List(),subtype) 
    95     assert(alternateFalse.scalaOr(CnTrue,subtype)==CnTrue, "OR(alternateFalse,CnTrue) == CnTrue") 
    96     assert(alternateFalse.scalaOr(CnFalse,subtype)==CnFalse, "OR(alternateFalse,CnFalse) == CnFalse") 
    97     assert(CnTrue.scalaOr(alternateFalse,subtype)==CnTrue, "OR(CnFalse, alternateFalse) == CnTrue") 
    98     assert(CnFalse.scalaOr(alternateFalse,subtype)==CnFalse, "OR(CnFalse, alternateFalse) == CnFalse") 
     93    val alternateFalse = CnOr(List(),analyzer) 
     94    assert(alternateFalse.or(CnTrue,analyzer)==CnTrue, "OR(alternateFalse,CnTrue) == CnTrue") 
     95    assert(alternateFalse.or(CnFalse,analyzer)==CnFalse, "OR(alternateFalse,CnFalse) == CnFalse") 
     96    assert(CnTrue.or(alternateFalse,analyzer)==CnTrue, "OR(CnFalse, alternateFalse) == CnTrue") 
     97    assert(CnFalse.or(alternateFalse,analyzer)==CnFalse, "OR(CnFalse, alternateFalse) == CnFalse") 
    9998    //Test test that all alternate forms are eliminated 
    100     assert(alternateTrue.scalaOr(alternateTrue,subtype) == CnTrue, "OR(alternateTrue,alternateTrue) =/= CnTrue") 
    101     assert(alternateTrue.scalaOr(alternateTrue2,subtype) == CnTrue, "OR(alternateTrue,alternateTrue2) =/= CnTrue") 
    102     assert(alternateTrue2.scalaOr(alternateTrue,subtype) == CnTrue, "OR(alternateTrue2,alternateTrue) =/= CnTrue") 
    103     assert(alternateTrue2.scalaOr(alternateTrue2,subtype) == CnTrue, "OR(alternateTrue2,alternateTrue2) =/= CnTrue") 
    104     assert(alternateTrue.scalaOr(alternateFalse,subtype) == CnTrue, "OR(alternateTrue,alternateFalse) =/= CnTrue") 
    105     assert(alternateFalse.scalaOr(alternateTrue,subtype) == CnTrue, "OR(alternateFalse,alternateTrue) =/= CnTrue") 
    106     assert(alternateTrue2.scalaOr(alternateFalse,subtype) == CnTrue, "OR(alternateTrue2,alternateFalse) =/= CnTrue") 
    107     assert(alternateFalse.scalaOr(alternateTrue2,subtype) == CnTrue, "OR(alternateFalse,alternateTrue2) =/= CnTrue") 
    108     assert(alternateFalse.scalaOr(alternateFalse,subtype) == CnFalse, "OR(alternateFalse,alternateFalse) =/= CnFalse") 
     99    assert(alternateTrue.or(alternateTrue,analyzer) == CnTrue, "OR(alternateTrue,alternateTrue) =/= CnTrue") 
     100    assert(alternateTrue.or(alternateTrue2,analyzer) == CnTrue, "OR(alternateTrue,alternateTrue2) =/= CnTrue") 
     101    assert(alternateTrue2.or(alternateTrue,analyzer) == CnTrue, "OR(alternateTrue2,alternateTrue) =/= CnTrue") 
     102    assert(alternateTrue2.or(alternateTrue2,analyzer) == CnTrue, "OR(alternateTrue2,alternateTrue2) =/= CnTrue") 
     103    assert(alternateTrue.or(alternateFalse,analyzer) == CnTrue, "OR(alternateTrue,alternateFalse) =/= CnTrue") 
     104    assert(alternateFalse.or(alternateTrue,analyzer) == CnTrue, "OR(alternateFalse,alternateTrue) =/= CnTrue") 
     105    assert(alternateTrue2.or(alternateFalse,analyzer) == CnTrue, "OR(alternateTrue2,alternateFalse) =/= CnTrue") 
     106    assert(alternateFalse.or(alternateTrue2,analyzer) == CnTrue, "OR(alternateFalse,alternateTrue2) =/= CnTrue") 
     107    assert(alternateFalse.or(alternateFalse,analyzer) == CnFalse, "OR(alternateFalse,alternateFalse) =/= CnFalse") 
    109108  } 
    110109 
    111110  def testImplies() = { 
    112     val analyzer = makeAnalyzer() 
    113     val history = new SubtypeHistory(analyzer) 
    114     def subtype(t1: Type, t2: Type) = history.subtypeNormal(t1,t2).isTrue 
     111    val analyzer = typeAnalyzer("{}") 
    115112    //Test basic formulas 
    116     assert(CnFalse.implies(CnFalse,subtype), "CnFalse -> CnFalse =/= true") 
    117     assert(CnFalse.implies(CnTrue,subtype), "CnFalse -> CnTrue =/= true") 
    118     assert(!CnTrue.implies(CnFalse,subtype), "CnTrue -> CnFalse =/= false") 
    119     assert(CnTrue.implies(CnTrue,subtype), "CnTrue -> CnTrue =/= true") 
     113    assert(CnFalse.implies(CnFalse,analyzer), "CnFalse -> CnFalse =/= true") 
     114    assert(CnFalse.implies(CnTrue,analyzer), "CnFalse -> CnTrue =/= true") 
     115    assert(!CnTrue.implies(CnFalse,analyzer), "CnTrue -> CnFalse =/= false") 
     116    assert(CnTrue.implies(CnTrue,analyzer), "CnTrue -> CnTrue =/= true") 
    120117    //Test that CnAnd(Empty,Empty) is equivalent to CnTrue 
    121     val alternateTrue = CnAnd(Map.empty,Map.empty,subtype) 
     118    val alternateTrue = CnAnd(Map.empty,Map.empty,analyzer) 
    122119    assert(alternateTrue.isTrue,"!CnAnd(Empty,Empty).isTrue") 
    123120    //Test that CnAnd(Empty,Empty) is equivalent to CnTrue 
    124     val alternateTrue2 = CnOr(List(alternateTrue),subtype) 
     121    val alternateTrue2 = CnOr(List(alternateTrue),analyzer) 
    125122    assert(alternateTrue2.isTrue,"CnOr(CnAnd(Empty,Empty)).isTrue") 
    126123    //Test that CnOr(Empty) is equivalent to CnFalse 
    127     val alternateFalse = CnOr(List(),subtype) 
     124    val alternateFalse = CnOr(List(),analyzer) 
    128125    assert(alternateFalse.isFalse,"CnOr(Empty).isFalse") 
    129     val analyzer2 = makeAnalyzer(makeTrait("A"),makeTrait("B","A"),makeTrait("C"),makeTrait("D","C")) 
    130     val history2 = new SubtypeHistory(analyzer2) 
    131     def subtype2(t1: Type, t2: Type) = history2.subtypeNormal(t1,t2).isTrue 
     126    val analyzer2 = typeAnalyzer("{trait Aa, trait Bb extends {Aa}, trait Cc, trait Dd extends {Cc}}") 
    132127    //Declarations 
    133128    val ivar1 = make_InferenceVarType(typeSpan) 
    134129    val ivar2 = make_InferenceVarType(typeSpan) 
    135     val typea = makeType("A") 
    136     val typeb = makeType("B") 
    137     val typec = makeType("C") 
    138     val typed = makeType("D") 
     130    val typea = typ("Aa") 
     131    val typeb = typ("Bb") 
     132    val typec = typ("Cc") 
     133    val typed = typ("Dd") 
    139134    val map1a = Map.empty.update(ivar1,typea) 
    140135    val map1b = Map.empty.update(ivar1,typeb) 
    … …  
    147142     
    148143    //Test that unsatisfiable formulas are equivalent to CnFalse 
    149     val c1b = CnAnd(map1b,map1c,subtype2) 
     144    val c1b = CnAnd(map1b,map1c,analyzer2) 
    150145    assert(c1b.isFalse,"c <: 1 <: b is not false ") 
    151146    //Test that a satisfiable formula is not false 
    152     val b1a = CnAnd(map1a,map1b,subtype2) 
     147    val b1a = CnAnd(map1a,map1b,analyzer2) 
    153148    assert(!b1a.isFalse,"b <: 1 <: a is false") 
    154149    //Test that implication works for conjunctions and disjunctions 
    155     val bot1b = CnAnd(map1b,Map.empty,subtype2) 
    156     val bot1a = CnAnd(map1a,Map.empty,subtype2) 
    157     assert(bot1b.implies(bot1a,subtype2),"(1 <: B) -> (1 <: A) =/= true") 
    158     val a1any = CnAnd(Map.empty, map1a, subtype2) 
    159     val b1any = CnAnd(Map.empty, map1b, subtype2) 
    160     assert(a1any.implies(b1any,subtype2),"(A <: 1) -> (B <: 1) =/= true") 
    161     val a2any = CnAnd(Map.empty, map2a, subtype2) 
    162     assert(!a1any.implies(a2any,subtype2),"(A <: 1) -> (A <: 2) =/= false") 
    163     val b2any = CnAnd(Map.empty, map2b, subtype2) 
    164     val a1anyAnda2any = a1any.scalaAnd(a2any,subtype2) 
    165     val b1anyAndb2any = b1any.scalaAnd(b2any,subtype2) 
    166     assert(a1anyAnda2any.implies(b1anyAndb2any,subtype2),"(A<:1 and A<:2)->(B<:1 and B<:2) =/= true") 
    167     assert(!b1anyAndb2any.implies(a1anyAnda2any,subtype2),"(B<:1 and B<:2)->(A<:1 and A<:2) =/= false") 
    168     val b1anyOrb2any = b1any.scalaOr(b2any,subtype2) 
    169     assert(a1anyAnda2any.implies(b1anyOrb2any,subtype2),"(A<:1 and A<:2)->(B<:1 or B<:2) =/= true") 
    170     val a1anyOrb1any = a1any.scalaOr(a1any,subtype2) 
    171     assert(a1anyOrb1any.implies(b1any,subtype2),"(A<:1 or B<:1)->(B<:1) =/= true") 
    172     assert(a1anyOrb1any.implies(a1any,subtype2),"(A<:1 or B<:1)->(A<:1) =/= false") 
     150    val bot1b = CnAnd(map1b,Map.empty,analyzer2) 
     151    val bot1a = CnAnd(map1a,Map.empty,analyzer2) 
     152    assert(bot1b.implies(bot1a,analyzer2),"(1 <: B) -> (1 <: A) =/= true") 
     153    val a1any = CnAnd(Map.empty, map1a, analyzer2) 
     154    val b1any = CnAnd(Map.empty, map1b, analyzer2) 
     155    assert(a1any.implies(b1any,analyzer2),"(A <: 1) -> (B <: 1) =/= true") 
     156    val a2any = CnAnd(Map.empty, map2a, analyzer2) 
     157    assert(!a1any.implies(a2any,analyzer2),"(A <: 1) -> (A <: 2) =/= false") 
     158    val b2any = CnAnd(Map.empty, map2b, analyzer2) 
     159    val a1anyAnda2any = a1any.and(a2any,analyzer2) 
     160    val b1anyAndb2any = b1any.and(b2any,analyzer2) 
     161    assert(a1anyAnda2any.implies(b1anyAndb2any,analyzer2),"(A<:1 and A<:2)->(B<:1 and B<:2) =/= true") 
     162    assert(!b1anyAndb2any.implies(a1anyAnda2any,analyzer2),"(B<:1 and B<:2)->(A<:1 and A<:2) =/= false") 
     163    val b1anyOrb2any = b1any.or(b2any,analyzer2) 
     164    assert(a1anyAnda2any.implies(b1anyOrb2any,analyzer2),"(A<:1 and A<:2)->(B<:1 or B<:2) =/= true") 
     165    val a1anyOrb1any = a1any.or(a1any,analyzer2) 
     166    assert(a1anyOrb1any.implies(b1any,analyzer2),"(A<:1 or B<:1)->(B<:1) =/= true") 
     167    assert(a1anyOrb1any.implies(a1any,analyzer2),"(A<:1 or B<:1)->(A<:1) =/= false") 
    173168  } 
    174169   
    175170  def testSolve() = { 
    176     val analyzer = makeAnalyzer() 
    177     val history = new SubtypeHistory(analyzer) 
    178     def subtype(t1: Type, t2: Type) = history.subtypeNormal(t1,t2).isTrue 
    179     assert(CnFalse.scalaSolve(Map.empty).isEmpty, "SOLVE(CnFalse) =/= None") 
    180     assert(CnTrue.scalaSolve(Map.empty).get.isEmpty, "SOLVE(CnTrue) =/= Some(Nil)") 
    181     val alternateTrue = CnAnd(Map.empty,Map.empty,subtype) 
    182     val alternateTrue2 = CnOr(List(alternateTrue),subtype) 
    183     val alternateFalse = CnOr(List(),subtype) 
    184     assert(alternateFalse.scalaSolve(Map.empty).isEmpty, "SOLVE(CnFalse) =/= None") 
    185     assert(alternateTrue.scalaSolve(Map.empty).get.isEmpty, "SOLVE(CnTrue) =/= Some(Nil)") 
    186     assert(alternateTrue2.scalaSolve(Map.empty).get.isEmpty, "SOLVE(CnTrue) =/= Some(Nil)") 
    187     val analyzer2 = makeAnalyzer(makeTrait("A"),makeTrait("B","A"),makeTrait("C"),makeTrait("D","C")) 
    188     val history2 = new SubtypeHistory(analyzer2)  
    189     def subtype2(t1: Type, t2: Type) = history2.subtypeNormal(t1,t2).isTrue 
     171    val analyzer = typeAnalyzer("{ }") 
     172    assert(CnFalse.solve(Map.empty).isEmpty, "SOLVE(CnFalse) =/= None") 
     173    assert(CnTrue.solve(Map.empty).get.isEmpty, "SOLVE(CnTrue) =/= Some(Nil)") 
     174    val alternateTrue = CnAnd(Map.empty,Map.empty,analyzer) 
     175    val alternateTrue2 = CnOr(List(alternateTrue),analyzer) 
     176    val alternateFalse = CnOr(List(),analyzer) 
     177    assert(alternateFalse.solve(Map.empty).isEmpty, "SOLVE(CnFalse) =/= None") 
     178    assert(alternateTrue.solve(Map.empty).get.isEmpty, "SOLVE(CnTrue) =/= Some(Nil)") 
     179    assert(alternateTrue2.solve(Map.empty).get.isEmpty, "SOLVE(CnTrue) =/= Some(Nil)") 
     180    val analyzer2 = typeAnalyzer("{trait Aa, trait Bb extends {Aa}, trait Cc, trait Dd extends {Cc}}") 
    190181        //Declarations 
    191182    val ivar1 = make_InferenceVarType(typeSpan) 
    192183    val ivar2 = make_InferenceVarType(typeSpan) 
    193     val typea = makeType("A") 
    194     val typeb = makeType("B") 
    195     val typec = makeType("C") 
    196     val typed = makeType("D") 
     184    val typea = typ("Aa") 
     185    val typeb = typ("Bb") 
     186    val typec = typ("Cc") 
     187    val typed = typ("Dd") 
    197188    val map1a = Map.empty.update(ivar1,typea) 
    198189    val map1b = Map.empty.update(ivar1,typeb) 
    … …  
    203194    val map2c = Map.empty.update(ivar2,typec) 
    204195    val map2d = Map.empty.update(ivar2,typed) 
    205     val b1a = CnAnd(map1a,map1b,subtype2) 
     196    val b1a = CnAnd(map1a,map1b,analyzer2) 
    206197    //Check that solving a contradictory formula gives you nothing 
    207     val c1b = CnAnd(map1b,map1c,subtype2) 
    208     val solved_c1b = c1b.scalaSolve(Map.empty) 
     198    val c1b = CnAnd(map1b,map1c,analyzer2) 
     199    val solved_c1b = c1b.solve(Map.empty) 
    209200    //Check that solving a constraint with no bounds works 
    210201    assert(solved_c1b.isEmpty,"solve(C<:1<:B, {}) is not empty") 
    211     val solved_b1a = b1a.scalaSolve(Map.empty) 
     202    val solved_b1a = b1a.solve(Map.empty) 
    212203    assert(solved_b1a.isDefined && solved_b1a.get==map1b,"SOLVE(B<:1<:A , {}) = 1:=B") 
    213204    //Check that if the solution to a constraint is out of bounds it fails 
    214     val solved_b1a_1c = b1a.scalaSolve(map1c) 
     205    val solved_b1a_1c = b1a.solve(map1c) 
    215206    assert(solved_b1a_1c.isEmpty,"Solve(B<:1<:A, {1<:C}) is not empty") 
    216207    //Check that if the solution to a constraint is in bounds it succeeds 
    217     val solved_b1a_1a = b1a.scalaSolve(map1a) 
     208    val solved_b1a_1a = b1a.solve(map1a) 
    218209    assert(solved_b1a_1a.isDefined && solved_b1a_1a.get==map1b,"SOLVE(B<:1<:A, {1<:A}) = 1:=B") 
    219210  } 

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

    r4251 r4285  
    288288   * Return the conditions for subtype <: supertype to hold. 
    289289   */ 
    290   protected def checkSubtype(subtype: Type, supertype: Type): ScalaConstraint = { 
    291     val constraint = analyzer.subtype(subtype, supertype) 
    292     if (!constraint.isInstanceOf[ScalaConstraint]) { 
    293       bug("Not a ScalaConstraint.") 
    294     } 
    295     constraint.asInstanceOf[ScalaConstraint] 
     290  protected def checkSubtype(subtype: Type, supertype: Type): ConstraintFormula = { 
     291    analyzer.subtype(subtype, supertype) 
    296292  } 
    297293 

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

    r4278 r4285  
    3636class CoveringAnalyzer(ta: TypeAnalyzer) { 
    3737 
    38   def minimalCover(x: Type): Type = ta.normalize(x) match { 
     38  def minimize(x: Type): Type = ta.normalize(x) match { 
    3939    case SIntersectionType(_, e) =>  
    4040      val (as, ts) = List.separate(e.map(_ match { 
    4141        case a:ArrowType => Left(a) 
    42         case t => Right(minimalCover(t)) 
     42        case t => Right(minimize(t)) 
    4343      })) 
    4444      ta.meet(ts) 
    45     case SUnionType(_, e) => ta.join(e.map(minimalCover)) 
    46     case t:TraitType => makeUnionType(comprisesLeaves(t)) 
     45    case SUnionType(_, e) => ta.join(e.map(minimize)) 
     46    case t:TraitType => ta.join(comprisesLeaves(t)) 
    4747    //ToDo: Handle keywords 
    48     case STupleType(i, e, mv, _) => STupleType(i, e.map(minimalCover), mv.map(minimalCover), Nil) 
     48    case STupleType(i, e, mv, _) => STupleType(i, e.map(minimize), mv.map(minimize), Nil) 
    4949    case SArrowType(i, d, r, e, io, m) => 
    50       SArrowType(i, d, minimalCover(r), e, io, m) 
     50      SArrowType(i, d, minimize(r), e, io, m) 
    5151    case _ => x 
    5252  } 
    5353   
    5454  private def mergeArrows(x: ArrowType, y: ArrowType): ArrowType = { 
    55     //val SArrowType(i1, d1, r1, SEffect(), io1, mi1) = x 
    56     //val SArrowType(i2, d2, r2, SEffect(), io2, mi2) = y 
    57     //SArrowType(_, ta.join(d1, d2), minimalcover(ta.meet(r1, r2)), io1 || io2, SEffect(), _) 
    58     x 
     55    val SArrowType(i1, d1, r1, e1, io1, mi1) = x 
     56    val SArrowType(i2, d2, r2, e2, io2, mi2) = y 
     57    //merge method info? 
     58    SArrowType(mergeTypeInfo(i1, i2), 
     59               ta.join(d1, d2), 
     60               minimize(ta.meet(r1, r2)),  
     61               mergeEffects(e1, e2), 
     62               io1 || io2, 
     63               mi1) 
    5964  } 
    6065   
    … …  
    6469  } 
    6570   
     71  private def mergeTypeInfo(x: TypeInfo, y: TypeInfo) = x 
     72   
     73  private def mergeEffects(x: Effect, y: Effect) = { 
     74    val SEffect(i1, t1, io1) = x 
     75    val SEffect(i2, t2, io2) = y 
     76    val tc = minimize(ta.meet(ta.join(t1.getOrElse(Nil)), ta.join(t2.getOrElse(Nil)))) match { 
     77      case t:BottomType => None 
     78      case SUnionType(_, elts) => Some(elts) 
     79      case t => Some(List(t)) 
     80    } 
     81    //merge ASTNodeInfo? 
     82    SEffect(i1, tc, io1 || io2) 
     83  } 
     84   
    6685  private def comprisesLeaves(x: TraitType): Set[TraitType] = ta.comprisesClause(x) match { 
    6786    case ts if ts.isEmpty => Set(x) 
    … …  
    6988  } 
    7089   
    71  
    72    
    73    
    74    
    7590} 

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

    r4278 r4285  
    2626import com.sun.fortress.nodes_util.NodeFactory.typeSpan 
    2727import com.sun.fortress.scala_src.nodes._ 
    28 import com.sun.fortress.scala_src.typechecker.ScalaConstraint 
     28import com.sun.fortress.scala_src.typechecker.ConstraintFormula 
    2929import com.sun.fortress.scala_src.typechecker.CnFalse 
    3030import com.sun.fortress.scala_src.typechecker.CnTrue 
    … …  
    5454  def join(x: Iterable[Type]): Type = normalize(makeUnionType(x)) 
    5555 
    56   def subtype(x: Type, y: Type): ScalaConstraint = sub(normalize(x), normalize(y)) 
    57  
    58   private def sub(x: Type, y: Type): ScalaConstraint = (x,y) match { 
     56  def subtype(x: Type, y: Type): ConstraintFormula = sub(normalize(x), normalize(y)) 
     57 
     58  private def sub(x: Type, y: Type): ConstraintFormula = (x,y) match { 
    5959    case (s,t) if (s==t) => TRUE 
    6060    case (s: BottomType, _) => TRUE 
    … …  
    109109  } 
    110110 
    111   private def sub(x: List[KeywordType], y: List[KeywordType]): ScalaConstraint = { 
     111  private def sub(x: List[KeywordType], y: List[KeywordType]): ConstraintFormula = { 
    112112    def toPair(k: KeywordType) = (k.getName, k.getKeywordType) 
    113113    val xmap = Map(x.map(toPair):_*) 
    … …  
    121121  } 
    122122 
    123   private def sub(x: Effect, y: Effect): ScalaConstraint = { 
     123  private def sub(x: Effect, y: Effect): ConstraintFormula = { 
    124124    val (SEffect(_, tc1, io1), SEffect(_, tc2, io2)) = (x,y) 
    125125    if (!io1 || io2) 
    … …  
    130130 
    131131 
    132   def equivalent(x: Type, y: Type): ScalaConstraint = { 
     132  def equivalent(x: Type, y: Type): ConstraintFormula = { 
    133133    val s = normalize(x) 
    134134    val t = normalize(y) 
    … …  
    136136  } 
    137137 
    138   private def eq(x: Type, y:Type): ScalaConstraint  = { 
     138  private def eq(x: Type, y:Type): ConstraintFormula  = { 
    139139    and(sub(x, y), sub(x, y)) 
    140140  } 
    141141 
    142   private def eq(x: StaticArg, y: StaticArg): ScalaConstraint = (x,y) match { 
     142  private def eq(x: StaticArg, y: StaticArg): ConstraintFormula = (x,y) match { 
    143143    case (STypeArg(_, _, s), STypeArg(_, _, t)) => eq(s, t) 
    144144    case (SIntArg(_, _, a), SIntArg(_, _, b)) => fromBoolean(a==b) 
    … …  
    323323    new TypeAnalyzer(traits, env.extend(params, where)) 
    324324   
    325   private val TRUE: ScalaConstraint = CnTrue 
    326   private val FALSE: ScalaConstraint = CnFalse 
    327   private def and(x: ScalaConstraint, y: ScalaConstraint): ScalaConstraint = 
    328     x.scalaAnd(y, this.lteq) 
    329   private def or(x: ScalaConstraint, y: ScalaConstraint): ScalaConstraint = 
    330     x.scalaOr(y, this.lteq) 
    331   private def upperBound(i: _InferenceVarType, t: Type): ScalaConstraint = 
    332     CnAnd(Map((i,t)), Map(), this.lteq) 
    333   private def lowerBound(i: _InferenceVarType, t: Type): ScalaConstraint = 
    334     CnAnd(Map(), Map((i,t)), this.lteq) 
     325  private val TRUE: ConstraintFormula = CnTrue 
     326  private val FALSE: ConstraintFormula = CnFalse 
     327  private def and(x: ConstraintFormula, y: ConstraintFormula): ConstraintFormula = 
     328    x.and(y, this) 
     329  private def or(x: ConstraintFormula, y: ConstraintFormula): ConstraintFormula = 
     330    x.or(y, this) 
     331  private def upperBound(i: _InferenceVarType, t: Type): ConstraintFormula = 
     332    CnAnd(Map((i,t)), Map(), this) 
     333  private def lowerBound(i: _InferenceVarType, t: Type): ConstraintFormula = 
     334    CnAnd(Map(), Map((i,t)), this) 
    335335  private def fromBoolean(x: Boolean) = if (x) TRUE else FALSE 
    336336   

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

    r4276 r4285  
    6262     
    6363    val ca = new CoveringAnalyzer(ta) 
    64     assert(ca.minimalCover(typ("&&{Aa, Ee}")) == typ("Dd")) 
     64    assert(ca.minimize(typ("&&{Aa, Ee}")) == typ("Dd")) 
    6565  } 
    6666   

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

    r4281 r4285  
    3434import com.sun.fortress.nodes_util.{NodeUtil => NU} 
    3535import com.sun.fortress.scala_src.nodes._ 
    36 import com.sun.fortress.scala_src.typechecker.ScalaConstraint 
    37 import com.sun.fortress.scala_src.typechecker.ScalaConstraintUtil._ 
     36import com.sun.fortress.scala_src.typechecker.ConstraintFormula 
     37import com.sun.fortress.scala_src.typechecker.CnFalse 
     38import com.sun.fortress.scala_src.typechecker.CnTrue 
    3839import com.sun.fortress.scala_src.types.TypeAnalyzer 
    3940import com.sun.fortress.scala_src.useful.Lists._ 
    … …  
    162163    // Get the substitution resulting from params :> expectedDomain 
    163164    val paramsDomain = makeDomainType(params).get 
    164     val subst = analyzer.subtype(expectedDomain, paramsDomain). 
    165                 asInstanceOf[ScalaConstraint].scalaSolve(Map()) 
     165    val subst = analyzer.subtype(expectedDomain, paramsDomain).solve(Map()) 
    166166    subst.map(s => 
    167167      params.map(p => p match { 
    … …  
    405405  /** Return the [Scala-based] conditions for subtype <: supertype to hold. */ 
    406406  def checkSubtype(subtype: Type, supertype: Type) 
    407                   (implicit analyzer: TypeAnalyzer): ScalaConstraint = { 
     407                  (implicit analyzer: TypeAnalyzer): ConstraintFormula = { 
    408408    val constraint = analyzer.subtype(subtype, supertype) 
    409     if (!constraint.isInstanceOf[ScalaConstraint]) { 
    410       bug("Not a ScalaConstraint.") 
    411     } 
    412     constraint.asInstanceOf[ScalaConstraint] 
     409    if (!constraint.isInstanceOf[ConstraintFormula]) { 
     410      bug("Not a ConstraintFormula.") 
     411    } 
     412    constraint.asInstanceOf[ConstraintFormula] 
    413413  } 
    414414 
    … …  
    660660 
    661661    // Builds a constraint given the arrow with inference variables. 
    662     def makeConstraint(infArrow: ArrowType): ScalaConstraint = { 
     662    def makeConstraint(infArrow: ArrowType): ConstraintFormula = { 
    663663       
    664664      // argType <:? dom(infArrow) yields a constraint, C1 
    … …  
    667667      // if context given, C := C1 AND range(infArrow) <:? context 
    668668      val rangeConstraint = context.map(t => 
    669         checkSubtype(infArrow.getRange, t)).getOrElse(TRUE_FORMULA) 
    670       domainConstraint.scalaAnd(rangeConstraint, isSubtype) 
     669        checkSubtype(infArrow.getRange, t)).getOrElse(CnTrue) 
     670      domainConstraint.and(rangeConstraint, analyzer) 
    671671    } 
    672672 
    … …  
    678678  def inferStaticParamsHelper(fnType: ArrowType, 
    679679                              sparams: List[StaticParam], 
    680                               constraintMaker: ArrowType => ScalaConstraint) 
     680                              constraintMaker: ArrowType => ConstraintFormula) 
    681681                             (implicit analyzer: TypeAnalyzer) 
    682682                              : Option[(ArrowType, List[StaticArg])] = { 
    … …  
    700700    val infVars = sargs.flatMap(staticArgType) 
    701701    val sparamBounds = sparams.flatMap(staticParamBoundType). 
    702                                map(t => insertStaticParams(t, sparams)) 
     702      map(t => staticInstantiation(sparams zip sargs, insertStaticParams(t, sparams)).get) 
    703703    val boundsMap = Map(infVars.zip(sparamBounds): _*) 
    704704 
    705705    // 6. solve C to yield a substitution S' = [$T_i -> U_i] 
    706     val subst = constraint.scalaSolve(boundsMap).getOrElse(return None) 
     706    val subst = constraint.solve(boundsMap).getOrElse(return None) 
    707707 
    708708    // 7. instantiate infArrow with [U_i] to get resultArrow 
    … …  
    732732 
    733733    // Builds a constraint given the arrow with inference variables. 
    734     def makeConstraint(infArrow: ArrowType): ScalaConstraint = { 
     734    def makeConstraint(infArrow: ArrowType): ConstraintFormula = { 
    735735     
    736736      // Get the type of the `self` arg and form selfArg <:? selfType 
    … …  
    738738      getTypeAt(argType, selfPosition) match { 
    739739        case Some(selfArgType) => checkSubtype(selfArgType, selfType) 
    740         case None => FALSE_FORMULA 
     740        case None => CnFalse 
    741741      } 
    742742    }