Compare commits
27 Commits
Author | SHA1 | Date | |
---|---|---|---|
|
abe4f78490 | ||
|
0e0c096d0f | ||
|
6f48d04a7e | ||
|
3c8cd30284 | ||
|
880fbdd905 | ||
|
c176dfdc9f | ||
|
09c7c1457f | ||
|
84ee7b260a | ||
|
80dcad7a13 | ||
|
8d3c6992ac | ||
|
2d12836262 | ||
|
0be9ca406d | ||
|
66a589faab | ||
|
0e648ce112 | ||
|
3ae2bc2d61 | ||
|
43ad1c4964 | ||
|
fdf3c03eb8 | ||
|
a24faf8f2d | ||
|
58261b1fc4 | ||
|
f88da9e736 | ||
|
d26363ec19 | ||
|
556995716f | ||
|
3018c060f4 | ||
|
df9f34c739 | ||
|
37ae27a521 | ||
|
93af1d12f6 | ||
|
0267a2df24 |
10
README.md
10
README.md
@ -1,7 +1,13 @@
|
||||
## Typeinference for Featherweight Java
|
||||
# Typeinference for Featherweight Java
|
||||
|
||||
## Getting started
|
||||
|
||||
[Try it here](https://janulrich.github.io/FeatherweightTypeInference/)
|
||||
|
||||
## Building
|
||||
|
||||
```sbt fullLinkJS```
|
||||
|
||||
### Input Examples
|
||||
|
||||
```
|
||||
@ -22,7 +28,7 @@ class Overloading extends Object{
|
||||
|
||||
class TestOverloading extends Object{
|
||||
test(a){
|
||||
return new Test().m(this,a);
|
||||
return new Overloading().m(this,a);
|
||||
}
|
||||
}
|
||||
```
|
||||
|
@ -1,18 +1,18 @@
|
||||
package hb.dhbw
|
||||
|
||||
class CartesianProduct[A](private val setOfSets: List[List[A]]){
|
||||
def productWith(product: CartesianProduct[A]) = {
|
||||
val ret = new CartesianProduct[A](setOfSets ++ product.setOfSets)
|
||||
var base: Long = 1
|
||||
ret.sizes = ret.setOfSets.map(_.size)
|
||||
ret.sizes.foreach(size => {
|
||||
base = base * size
|
||||
})
|
||||
ret.max = base
|
||||
ret.i = i
|
||||
ret
|
||||
}
|
||||
class CartesianProductBuilder[A](){
|
||||
var ret : Set[Set[A]] = Set()
|
||||
def build() : CartesianProduct[A] = new CartesianProduct[A](ret)
|
||||
|
||||
def addSingleton(a:A){
|
||||
ret += Set(a)
|
||||
}
|
||||
def add(as : Set[A]): Unit ={
|
||||
ret += as
|
||||
}
|
||||
}
|
||||
|
||||
class CartesianProduct[A](private val setOfSets: List[List[A]]){
|
||||
private var sizes: List[Int] = null
|
||||
private var max: Long = 1
|
||||
private var i: Long = 0
|
||||
|
@ -75,6 +75,17 @@ object FJTypeinference {
|
||||
Class(in.name, in.genericParams, in.superType, in.fields, newMethods.toList)
|
||||
}
|
||||
|
||||
def removeLessDotGenericConstraints(unifyResult: Set[Set[UnifyConstraint]], generics: Set[String]) :Set[Set[UnifyConstraint]] =
|
||||
unifyResult.map(_.map( _ match { //
|
||||
case UnifyLessDot(UnifyTV(a), UnifyRefType(name, List())) =>
|
||||
if(generics.contains(name))
|
||||
UnifyEqualsDot(UnifyTV(a), UnifyRefType(name, List()))
|
||||
else
|
||||
UnifyLessDot(UnifyTV(a), UnifyRefType(name, List()))
|
||||
case x => x
|
||||
}
|
||||
))
|
||||
|
||||
def typeinference(str: String): Either[String, List[Class]] = {
|
||||
val ast = Parser.parse(str).map(ASTBuilder.fromParseTree(_))
|
||||
var typedClasses: List[Class] = List()
|
||||
@ -85,9 +96,9 @@ object FJTypeinference {
|
||||
val typeResult = TYPE.generateConstraints(newClassList, fc)
|
||||
val unifyResult = Unify.unifyIterative(convertOrConstraints(typeResult._1), typeResult._2)
|
||||
|
||||
val postProcessed = removeLessDotGenericConstraints(unifyResult, c.genericParams.map(_._1.asInstanceOf[GenericType].name).toSet)
|
||||
//Insert intersection types
|
||||
//val typeInsertedC = InsertTypes.applyResult(sigma, generics, c)//InsertTypes.insert(unifyResult, c)
|
||||
val typeInsertedC = removeOverloadedSubtypeMethods(InsertTypes.applyUnifyResult(unifyResult, c), fc)
|
||||
val typeInsertedC = removeOverloadedSubtypeMethods(InsertTypes.applyUnifyResult(postProcessed, c), fc)
|
||||
typedClasses = typedClasses :+ typeInsertedC
|
||||
cOld :+ typeInsertedC
|
||||
})
|
||||
|
@ -28,10 +28,14 @@ class FiniteClosure(val extendsRelations : Set[(FJNamedType, FJNamedType)]){
|
||||
ref.result()
|
||||
}
|
||||
private def superClassTypes(of: FJNamedType) = {
|
||||
def paramSubst(param : FJType, paramMap : Map[FJType, FJType]): FJType = param match{
|
||||
case FJNamedType(n, params) => FJNamedType(n, params.map(paramSubst(_, paramMap)))
|
||||
case typeVariable => paramMap.get(typeVariable).get
|
||||
}
|
||||
val extendsRelation = extendsRelations.filter(pair => pair._1.name.equals(of.name))
|
||||
extendsRelation.map(p => {
|
||||
val paramMap = p._1.params.zip(of.params).toMap
|
||||
(of,FJNamedType(p._2.name, p._2.params.map(paramMap)))
|
||||
(of,FJNamedType(p._2.name, p._2.params.map(paramSubst(_, paramMap))))
|
||||
})
|
||||
}
|
||||
private def superClassTypes(of: Set[(FJNamedType, FJNamedType)]) : Set[(FJNamedType, FJNamedType)] ={
|
||||
|
@ -5,20 +5,21 @@ object InsertTypes {
|
||||
|
||||
// Unify step 6:
|
||||
//TODO: a <. X must be replaced by X -> sigma(a) = GenericType(X) in that case
|
||||
private class UnifyResult(solvedCons: Set[UnifyConstraint]){
|
||||
private class UnifyResult(solvedCons: Set[UnifyConstraint], genericNames: Set[String]){
|
||||
def sigma(x: Type): Type = x match {
|
||||
case TypeVariable(n) => sigma(UnifyTV(x.asInstanceOf[TypeVariable].name))
|
||||
case v => v
|
||||
}
|
||||
def sigma(x: UnifyType): Type = { x match {
|
||||
case UnifyTV(n) => {
|
||||
case UnifyTV(_) =>
|
||||
val to = solvedCons.find(_.left == x).get
|
||||
to match {
|
||||
case UnifyEqualsDot(UnifyTV(_), UnifyTV(x)) => this.sigma(UnifyTV(x))
|
||||
case UnifyEqualsDot(UnifyTV(_), UnifyTV(x)) => GenericType(x)
|
||||
case UnifyEqualsDot(UnifyTV(_), UnifyRefType(n, List())) => if(genericNames.contains(n)) GenericType(n) else RefType(n, List())
|
||||
case UnifyEqualsDot(UnifyTV(_), UnifyRefType(n, ps)) => RefType(n, ps.map(this.sigma(_)))
|
||||
case UnifyLessDot(UnifyTV(x), UnifyRefType(n, ps)) => GenericType(x)
|
||||
}
|
||||
}
|
||||
case UnifyRefType(n, List()) => if(genericNames.contains(n)) GenericType(n) else RefType(n, List())
|
||||
case UnifyRefType(n, ps) => RefType(n, ps.map(sigma))
|
||||
}
|
||||
|
||||
@ -34,7 +35,7 @@ object InsertTypes {
|
||||
def applyUnifyResult(eq: Set[Set[UnifyConstraint]], into: Class) = {
|
||||
val newMethods = into.methods.flatMap(m => {
|
||||
eq.map(req => {
|
||||
val result = new UnifyResult(req)
|
||||
val result = new UnifyResult(req, into.genericParams.map(_._1.asInstanceOf[GenericType].name).toSet)
|
||||
Method(result.delta(), result.sigma(m.retType), m.name, m.params.map(p => (result.sigma(p._1), p._2)), m.retExpr)
|
||||
})
|
||||
})
|
||||
|
@ -45,13 +45,16 @@ object Parser {
|
||||
|
||||
def constructor[_: P]: P[ParserExpr] = P( kw("new") ~ methodCall).map(m => PConstructor(m.name,m.params))
|
||||
|
||||
def classDefinition[_: P]: P[ParserClass] = P(kw("class") ~ ident ~ genericParamList.? ~ kw("extends") ~ typeParser ~ "{" ~ field.rep(0) ~ method.rep(0) ~ "}")
|
||||
.map(ite => ParserClass(ite._1, ite._2.getOrElse(List()),ite._3, ite._4.toList, ite._5.toList))
|
||||
def classDefinition[_: P]: P[ParserClass] = P(kw("class") ~ ident ~ genericParamList.? ~ kw("extends") ~ typeParser ~ "{" ~ field.rep(0) ~ constructorDef.? ~ method.rep(0) ~ "}")
|
||||
.map(ite => ParserClass(ite._1, ite._2.getOrElse(List()),ite._3, ite._4.toList, ite._6.toList))
|
||||
def constructorDef[_:P] = P(ident ~ methodParameters ~ "{" ~ fieldAssign.rep ~ "}")
|
||||
def fieldAssign[_:P]:P[_] = P("this." ~ ident.! ~"=" ~ ident.! ~ ";")
|
||||
def field[_: P]: P[(NType, String)] = P(typeParser ~ ident ~ ";")
|
||||
def parameterDef[_ : P]: P[(Option[NType], String)] = P((typeParser.? ~ ident) | ident.map((None, _)))
|
||||
def methodParameters[_ : P] : P[List[(Option[NType],String)]] = ("("~")").map(it => List()) | ("(" ~ parameterDef ~ ("," ~ parameterDef).rep(0) ~ ")")
|
||||
.map(ite => (ite._1, ite._2) +: ite._3.toList)
|
||||
def method[_: P]: P[ParserMethod] =
|
||||
P(parameterDef ~ (("("~")").map(it => List()) | ("(" ~ parameterDef ~ ("," ~ parameterDef).rep(0) ~ ")")
|
||||
.map(ite => (ite._1, ite._2) +: ite._3.toList))
|
||||
P(parameterDef ~ methodParameters
|
||||
~ "{" ~ kw("return") ~ expr ~ ";" ~ "}")
|
||||
.map(ite => ParserMethod(ite._1, ite._2, ite._3, ite._4))
|
||||
def genericParamList[_: P]: P[List[(NType,NType)]] =
|
||||
|
@ -1,6 +1,5 @@
|
||||
package hb.dhbw
|
||||
|
||||
|
||||
sealed abstract class UnifyConstraint(val left: UnifyType, val right: UnifyType)
|
||||
final case class UnifyLessDot(override val left: UnifyType, override val right: UnifyType) extends UnifyConstraint(left, right)
|
||||
final case class UnifyEqualsDot(override val left: UnifyType, override val right: UnifyType) extends UnifyConstraint(left, right)
|
||||
@ -24,15 +23,23 @@ object Unify {
|
||||
override def result: Set[UnifyConstraint] = eq
|
||||
}
|
||||
|
||||
def removeALessdotB(eq: Set[UnifyConstraint]): Set[UnifyConstraint] = {
|
||||
def postProcessing(eq: Set[UnifyConstraint]): Set[UnifyConstraint] = {
|
||||
var ret = eq
|
||||
val alessdotb:Set[UnifyConstraint] = eq.filter(_ match{
|
||||
var ruleResult = subElimRule(ret)
|
||||
while(ruleResult.isDefined){
|
||||
ret = ruleResult.get
|
||||
ruleResult = subElimRule(ruleResult.get)
|
||||
}
|
||||
ret
|
||||
}
|
||||
|
||||
def subElimRule(eq: Set[UnifyConstraint]) : Option[Set[UnifyConstraint]] = {
|
||||
eq.find(_ match{
|
||||
case UnifyLessDot(UnifyTV(a), UnifyTV(b)) => true
|
||||
case _ => false
|
||||
}).map(it => {
|
||||
subst(it.right.asInstanceOf[UnifyTV], it.left, eq.filter(it != _)) ++ Set(UnifyEqualsDot(it.right, it.left), UnifyEqualsDot(it.left, it.left))
|
||||
})
|
||||
ret = ret.filter(it => !alessdotb.contains(it))
|
||||
alessdotb.foreach(it => ret = subst(it.left.asInstanceOf[UnifyTV], it.right, ret))
|
||||
ret ++ alessdotb.map(_ match {case UnifyLessDot(a, b) => UnifyEqualsDot(a,b)})
|
||||
}
|
||||
|
||||
def unifyIterative(orCons: Set[Set[Set[UnifyConstraint]]], fc: FiniteClosure) : Set[Set[UnifyConstraint]] = {
|
||||
@ -51,7 +58,7 @@ object Unify {
|
||||
val substResult = substStep(step2Result.nextProduct().flatten)
|
||||
substResult match{
|
||||
case UnchangedSet(eq) => if(isSolvedForm(eq)){
|
||||
results = results + removeALessdotB(eq)
|
||||
results = results + postProcessing(eq)
|
||||
}
|
||||
case ChangedSet(eq) =>
|
||||
eqSets = eqSets + new CartesianProduct[Set[UnifyConstraint]](Set(Set(eq)))
|
||||
@ -62,56 +69,45 @@ object Unify {
|
||||
results
|
||||
}
|
||||
|
||||
def step2(eq : Set[UnifyConstraint], fc: FiniteClosure) ={
|
||||
val eq1 = eq.filter(c => c match{
|
||||
case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true
|
||||
case UnifyEqualsDot(UnifyTV(_), UnifyTV(_)) => true
|
||||
case _ => false
|
||||
})
|
||||
val cUnifyLessDotACons: Set[Set[Set[UnifyConstraint]]] = eq.map(c => c match{
|
||||
case UnifyLessDot(UnifyRefType(name,params), UnifyTV(a)) =>
|
||||
getSuperTypes(UnifyRefType(name,params), fc)
|
||||
.map(superType => Set(UnifyEqualsDot(UnifyTV(a), superType).asInstanceOf[UnifyConstraint]))
|
||||
case _ => null
|
||||
}).filter(s => s!=null)
|
||||
def expandLB(lowerBound: UnifyLessDot, upperBound: UnifyLessDot, fc: FiniteClosure): Set[Set[UnifyConstraint]] ={
|
||||
val b:UnifyTV = lowerBound.right.asInstanceOf[UnifyTV]
|
||||
val lowerBoundType : UnifyRefType = lowerBound.left.asInstanceOf[UnifyRefType]
|
||||
val upperBoundType : UnifyRefType = upperBound.right.asInstanceOf[UnifyRefType]
|
||||
fc.superTypes(convertRefType(lowerBoundType)).filter(t => fc.aIsSubtypeOfb(t, convertRefType(upperBoundType)))
|
||||
.map(t => Set(UnifyEqualsDot(b, convertNamedType(t))))
|
||||
}
|
||||
|
||||
val aUnifyLessDota = eq1.filter(c => c match{
|
||||
private def getUpperBoundOrSetUpperBoundToObject(forTV: UnifyTV, eq: Set[UnifyConstraint]) = eq.find(_ match {
|
||||
case UnifyLessDot(UnifyTV(a), UnifyRefType(n, params)) => UnifyTV(a).eq(forTV)
|
||||
case _ => false
|
||||
}).getOrElse(UnifyLessDot(forTV, UnifyRefType("Object", List()))).asInstanceOf[UnifyLessDot]
|
||||
|
||||
def step2(eq : Set[UnifyConstraint], fc: FiniteClosure) ={
|
||||
val cpBuilder = new CartesianProductBuilder[Set[UnifyConstraint]]()
|
||||
val aUnifyLessDota = eq.filter(c => c match{
|
||||
case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true
|
||||
case _ => false
|
||||
}).asInstanceOf[Set[UnifyLessDot]]
|
||||
|
||||
val aUnifyLessDotCConsAndBs: Set[(UnifyLessDot,Option[UnifyTV])] = eq.map(c => c match{
|
||||
case UnifyLessDot(UnifyTV(a),UnifyRefType(name,params)) =>{
|
||||
val bs = aUnifyLessDota.flatMap(c => Set(c.left, c.right)).asInstanceOf[Set[UnifyTV]]
|
||||
.filter(c => !a.equals(c) && isLinked(UnifyTV(a), c, aUnifyLessDota))
|
||||
if(bs.isEmpty){
|
||||
Set((UnifyLessDot(UnifyTV(a),UnifyRefType(name,params)),None))
|
||||
}else{
|
||||
bs.map(b => (UnifyLessDot(UnifyTV(a),UnifyRefType(name,params)),Some(b)))
|
||||
}
|
||||
}
|
||||
case _ => null
|
||||
}).filter(s => s!=null).flatten
|
||||
|
||||
val aUnifyLessDotCCons = aUnifyLessDotCConsAndBs.map{
|
||||
case (ac:UnifyLessDot,Some(b)) =>
|
||||
Set(Set(UnifyLessDot(b, ac.right))) ++
|
||||
getSuperTypes(ac.right.asInstanceOf[UnifyRefType], fc)
|
||||
.map(superType => Set(UnifyEqualsDot(b, superType)))
|
||||
case (ac, None) => null
|
||||
}.filter(c => c != null).asInstanceOf[Set[Set[Set[UnifyConstraint]]]]
|
||||
|
||||
val eq2 = eq.filter(c => c match{
|
||||
case UnifyLessDot(UnifyTV(_), UnifyRefType(_,_)) => true
|
||||
case UnifyEqualsDot(UnifyTV(_), UnifyRefType(_,_)) => true
|
||||
case UnifyEqualsDot(UnifyRefType(_,_),UnifyTV(_)) => true
|
||||
case UnifyEqualsDot(UnifyRefType(_,_),UnifyRefType(_,_)) => true
|
||||
case UnifyLessDot(UnifyRefType(_,_),UnifyRefType(_,_)) => true
|
||||
case _ => false
|
||||
eq.foreach(cons => cons match {
|
||||
case UnifyLessDot(UnifyRefType(n, ps), UnifyTV(a)) =>
|
||||
val lowerBound = UnifyLessDot(UnifyRefType(n, ps), UnifyTV(a))
|
||||
val upperBound = getUpperBoundOrSetUpperBoundToObject(lowerBound.right.asInstanceOf[UnifyTV], eq)
|
||||
cpBuilder.add(expandLB(lowerBound, upperBound, fc))
|
||||
case UnifyLessDot(UnifyTV(a), UnifyRefType(n, ps)) =>
|
||||
getLinks(UnifyTV(a), aUnifyLessDota)
|
||||
.map(b => {
|
||||
val upperBound = getUpperBoundOrSetUpperBoundToObject(b, eq)
|
||||
val lowerBound = UnifyLessDot(UnifyRefType(n, ps), b)
|
||||
//ExpandLB and add to return constraint set + {b <. C<T>} constraint
|
||||
cpBuilder.add(expandLB(lowerBound, upperBound, fc) + Set(UnifyLessDot(b, b)))
|
||||
})
|
||||
cpBuilder.addSingleton(Set(UnifyLessDot(UnifyTV(a), UnifyRefType(n, ps))))
|
||||
//the upper bound constraint remains in the constraint set:
|
||||
cpBuilder.addSingleton(Set(UnifyLessDot(UnifyTV(a), UnifyRefType(n, ps))))
|
||||
case cons => cpBuilder.addSingleton(Set(cons))
|
||||
})
|
||||
val eqSet = new CartesianProduct[Set[UnifyConstraint]](
|
||||
Set(Set(eq1)) ++ Set(Set(eq2)) ++ aUnifyLessDotCCons ++ cUnifyLessDotACons)
|
||||
eqSet
|
||||
cpBuilder.build()
|
||||
}
|
||||
|
||||
private def getAUnifyLessDotC(from: Set[UnifyConstraint]) = from.filter(c => c match{
|
||||
@ -121,12 +117,13 @@ object Unify {
|
||||
|
||||
def matchRule(eq : Set[UnifyConstraint], fc: FiniteClosure) = {
|
||||
val aUnifyLessDotC = getAUnifyLessDotC(eq)
|
||||
(eq -- aUnifyLessDotC) ++ aUnifyLessDotC.map(c => {
|
||||
val smallerC = aUnifyLessDotC.find(c2 => c2 != c && c2.left.equals(c.left) && fc.isPossibleSupertype(c2.right.asInstanceOf[UnifyRefType].name,c.right.asInstanceOf[UnifyRefType].name))
|
||||
(eq -- aUnifyLessDotC) ++ aUnifyLessDotC.flatMap(c => {
|
||||
val smallerC = aUnifyLessDotC.filter(c2 => c2 != c && c2.left.equals(c.left) && fc.isPossibleSupertype(c2.right.asInstanceOf[UnifyRefType].name,c.right.asInstanceOf[UnifyRefType].name))
|
||||
if(smallerC.isEmpty){
|
||||
c
|
||||
List(c)
|
||||
}else{
|
||||
UnifyLessDot(smallerC.get.right, c.right)
|
||||
val list = smallerC.toList
|
||||
UnifyLessDot(list.head.right, c.right) :: list.tail
|
||||
}
|
||||
}
|
||||
)
|
||||
@ -197,6 +194,14 @@ object Unify {
|
||||
case _ => true
|
||||
})
|
||||
|
||||
/**
|
||||
* Every 'b' with a <.* b
|
||||
*/
|
||||
def getLinks(a: UnifyTV, aUnifyLessDota: Set[UnifyLessDot]): Set[UnifyTV] =
|
||||
aUnifyLessDota.filter(c => c.left.asInstanceOf[UnifyTV].name.equals(a.name))
|
||||
.flatMap(cons => Set(cons.right.asInstanceOf[UnifyTV]) ++ getLinks(cons.right.asInstanceOf[UnifyTV], aUnifyLessDota))
|
||||
|
||||
|
||||
private def isLinked(a: UnifyTV, b: UnifyTV, aUnifyLessDota: Set[UnifyLessDot]): Boolean = {
|
||||
def getRightSides(of: UnifyTV) ={
|
||||
aUnifyLessDota.filter(c => c.left.asInstanceOf[UnifyTV].name.equals(of.name))
|
||||
@ -211,33 +216,29 @@ object Unify {
|
||||
}
|
||||
}
|
||||
|
||||
private def findCircles(aUnifyLessDota: Set[UnifyLessDot]) ={
|
||||
def getRightSides(of: UnifyTV) ={
|
||||
aUnifyLessDota.filter(c => c.left.asInstanceOf[UnifyTV].name.equals(of.name))
|
||||
}
|
||||
def findCircle(graph: List[UnifyLessDot]): List[UnifyLessDot] = {
|
||||
val newAdditions = getRightSides(graph.last.right.asInstanceOf[UnifyTV])
|
||||
var circle: List[UnifyLessDot] = List()
|
||||
val iterator = newAdditions.iterator
|
||||
while(iterator.hasNext && circle.isEmpty){
|
||||
val newAdd = iterator.next()
|
||||
if(newAdd.right.equals(graph.head.left)){
|
||||
circle = graph :+ newAdd
|
||||
}else{
|
||||
circle = findCircle(graph ++ List(newAdd))
|
||||
}
|
||||
}
|
||||
circle
|
||||
}
|
||||
aUnifyLessDota.view.map(c => findCircle(List(c)))
|
||||
}
|
||||
|
||||
def equalsRule(eq: Set[UnifyConstraint]) ={
|
||||
val aUnifyLessDota = eq.filter(c => c match{
|
||||
case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => true
|
||||
case _ => false
|
||||
}).asInstanceOf[Set[UnifyLessDot]]
|
||||
val circle = findCircles(aUnifyLessDota).find(!_.isEmpty)
|
||||
def getRightSides(of: UnifyTV) ={
|
||||
aUnifyLessDota.filter(c => c.left.asInstanceOf[UnifyTV].name.equals(of.name))
|
||||
}
|
||||
def findCircle(start: UnifyTV) : List[UnifyLessDot] = findCircleRec(start, Set(start))
|
||||
def findCircleRec(next: UnifyTV, visited: Set[UnifyTV]): List[UnifyLessDot] = {
|
||||
val rightSides = getRightSides(next).iterator
|
||||
while(rightSides.hasNext){ //Deep search
|
||||
val rightSide = rightSides.next()
|
||||
val nextTV = rightSide.right.asInstanceOf[UnifyTV]
|
||||
if(visited.contains(nextTV)){
|
||||
return List(rightSide)
|
||||
}else{
|
||||
return rightSide :: findCircleRec(nextTV, visited + nextTV)
|
||||
}
|
||||
}
|
||||
List() // empty list means there are no circles
|
||||
}
|
||||
val circle = aUnifyLessDota.map(cons => findCircle(cons.left.asInstanceOf[UnifyTV])).find(!_.isEmpty)
|
||||
if(circle.isDefined){
|
||||
val newEq = eq -- circle.get
|
||||
Some(newEq ++ (circle.get.map(c => UnifyEqualsDot(c.left, c.right))))
|
||||
@ -318,18 +319,16 @@ object Unify {
|
||||
var eqFinish: Set[UnifyConstraint] = eq
|
||||
do{
|
||||
eqNew = doWhileSome(Unify.equalsRule,eqFinish) //We have to apply equals rule first, to get rid of circles
|
||||
eqFinish = eraseRule(swapRule(reduceRule(matchRule(adoptRule(adaptRule(eqNew, fc), fc), fc))))
|
||||
val adaptRuleResult = adaptRule(eqNew, fc)
|
||||
val adoptRuleResult = adoptRule(adaptRuleResult, fc)
|
||||
val matchRuleResult = matchRule(adoptRuleResult, fc)
|
||||
val reduceRuleResult = reduceRule(matchRuleResult)
|
||||
val swapRuleResult = swapRule(reduceRuleResult)
|
||||
val eraseRuleResult = eraseRule(swapRuleResult)
|
||||
eqFinish = eraseRuleResult
|
||||
}while(!eqNew.equals(eqFinish))
|
||||
eqNew
|
||||
}
|
||||
|
||||
def cartesianProduct[T](xss: Set[Set[T]]): Set[Set[T]] =
|
||||
if(xss.isEmpty){
|
||||
Set(Set())
|
||||
} else{
|
||||
for(xh <- xss.head; xt <- cartesianProduct(xss.tail)) yield xt + xh
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
||||
|
@ -8,15 +8,4 @@ class CartesianProductTest extends FunSuite{
|
||||
val result = List(1,2,3,4).map( _ => test.nextProduct())
|
||||
assert(result.contains(Set(1,4)))
|
||||
}
|
||||
|
||||
test("productWith"){
|
||||
val test = new CartesianProduct[Int](Set(Set(1,2),Set(4,3)))
|
||||
val test2 = new CartesianProduct[Int](Set(Set(5,6), Set(7,8)))
|
||||
val test3 = test.productWith(test2)
|
||||
val result = for( i <- 1 to 16) yield test3.nextProduct()
|
||||
assert(result.contains(Set(2,3,6,8)))
|
||||
assert(result.toSet.size == 16)
|
||||
println(result)
|
||||
}
|
||||
|
||||
}
|
||||
|
@ -7,168 +7,101 @@ class IntegrationTest extends FunSuite {
|
||||
val ast = (fastparse.parse(("e.m(a)"), hb.dhbw.Parser.classDefinition(_)))
|
||||
//hb.dhbw.TYPE.TYPEClass(ast.get)
|
||||
val result = FJTypeinference.typeinference("class Test extends Object {\n\n}")
|
||||
assert(result.isRight)
|
||||
println(result)
|
||||
}
|
||||
|
||||
test("IdMethod"){
|
||||
val result = FJTypeinference.typeinference("class Test extends Object {\nObject f;\nm(a){return a;}\n}")
|
||||
assert(result.isRight)
|
||||
println(result)
|
||||
println(result.map(Main.prettyPrintAST(_)))
|
||||
}
|
||||
|
||||
test("IdMethodRecursive"){
|
||||
val result = FJTypeinference.typeinference("class Test extends Object {\n Object f;\n m(a, b){return this.m(b, a); }\n}")
|
||||
assert(result.isRight)
|
||||
println(result)
|
||||
}
|
||||
|
||||
test("ListAddDefinition"){
|
||||
val result = FJTypeinference.typeinference("class List<A extends Object> extends Object{\n add(a){\n return this;\n}\n}")
|
||||
assert(result.isRight)
|
||||
println(result.map(Main.prettyPrintAST(_)))
|
||||
}
|
||||
/*
|
||||
test("PaperExample"){
|
||||
val result = FJTypeinference.typeinference("class List<A extends Object> extends Object{\n add( a){\n return this;\n}\n}\nclass Test extends Object{\nm(a){ return a.add(this);}\n}")
|
||||
println(result.map(Main.prettyPrint(_)))
|
||||
}
|
||||
|
||||
test("GenericVar"){
|
||||
val result = FJTypeinference.typeinference("class List<A extends Object> extends Object{\nA a;\n\nget(){ return this.a;\n\n}\n}\n\n\nclass Test extends Object{\nList<String> test;\n\nm(a){\n return this.test.get();\n}\n\n}")
|
||||
println(result.map(Main.prettyPrint(_)))
|
||||
}
|
||||
|
||||
test("IdentCallExample"){
|
||||
val result = FJTypeinference.typeinference("class Test extends Object{\n\n m(a,b){return this.m(a);\n}\nm(a){return a;}\n}")
|
||||
println(result.map(Main.prettyPrint(_)))
|
||||
}
|
||||
|
||||
test("IdentRecursive"){
|
||||
val result = FJTypeinference.typeinference("class Test extends Object{\n\nm(a){\nreturn this.m(a);\n}\n}")
|
||||
println(result.map(Main.prettyPrint(_)))
|
||||
}
|
||||
|
||||
test("GetMethods"){
|
||||
val result = FJTypeinference.typeinference("class Test extends Object{\nget(){ return this.get().get();}\n}\n\nclass Test2 extends Object{\nget(){ return this;}\n}" )
|
||||
println(result.map(Main.prettyPrint(_)))
|
||||
}
|
||||
|
||||
test("constructorTest"){
|
||||
val input= "class Test extends Object{m(){ return new Test();}}"
|
||||
val result = FJTypeinference.typeinference(input )
|
||||
println(result.map(Main.prettyPrint(_)))
|
||||
}
|
||||
|
||||
test("fieldVar access"){
|
||||
val input ="class List<A extends Object> extends Object{\nA f;\nget(){ return this.f; }\n}\n\nclass Test2 extends Object{\nget(){ return new List(this).get();}\n}"
|
||||
val result = FJTypeinference.typeinference(input )
|
||||
println(result.map(Main.prettyPrint(_)))
|
||||
}
|
||||
*/
|
||||
|
||||
test("constructor.FieldInitialization") {
|
||||
val input = "class List<A extends Object> extends Object{\nA f;\n add(a){\n return new List(a);\n}\n}"
|
||||
val result = FJTypeinference.typeinference(input )
|
||||
assert(result.isRight)
|
||||
println(result.map(it => Main.prettyPrintAST(it)))
|
||||
}
|
||||
test("list.add") {
|
||||
val input = "class List<A extends Object> extends Object{\nA f;\n add( a){\n return new List(a);\n}\n}\nclass Test extends Object{\n\nm(a){return a.add(this);}\n}"
|
||||
val result = FJTypeinference.typeinference(input )
|
||||
assert(result.isRight)
|
||||
println(result.map(it => Main.prettyPrintAST(it)))
|
||||
}
|
||||
test("list.add.2") {
|
||||
val input = "class List<A extends Object> extends Object{\n A head;\n List<A> tail;\n add( a){\n return new List(a, this);\n}\nget(){\nreturn this.head;\n}\n}\n\nclass Test extends Object{\nm(a){\nreturn a.add(this).get();\n}\n}"
|
||||
val result = FJTypeinference.typeinference(input )
|
||||
assert(result.isRight)
|
||||
println(result.map(it => Main.prettyPrintAST(it)))
|
||||
}
|
||||
|
||||
test("functionClass") {
|
||||
val input = "class SameType<A extends Object, B extends Object> extends Object{\nA a;\nA b;\nB c;\nget(){return this.c;}\n}\nclass Function<A extends Object, B extends Object> extends Object{\nA ret;\nB param;\napply(a){\nreturn new SameType(this.param, a, this).get().ret;\n}\n\n}"
|
||||
val result = FJTypeinference.typeinference(input )
|
||||
assert(result.isRight)
|
||||
println(result.map(it => Main.prettyPrintAST(it)))
|
||||
}
|
||||
|
||||
test("TwoRecursiveMethods") {
|
||||
val input = "class RecursiveMethods extends Object{\n\na1(x){ return this.a2(x);}\na2(y){ return this.a1(y);}}"
|
||||
val result = FJTypeinference.typeinference(input)
|
||||
assert(result.isRight)
|
||||
println(result.map(it => Main.prettyPrintAST(it)))
|
||||
}
|
||||
|
||||
test("Function.typeAnnotaded") {
|
||||
val input = "\nclass Function<A extends Object, B extends Object> extends Object{\nB b;\nB apply(A a){\nreturn this.b;\n}\n\n}"
|
||||
val result = FJTypeinference.typeinference(input)
|
||||
assert(result.isRight)
|
||||
println(result.map(it => Main.prettyPrintAST(it)))
|
||||
}
|
||||
|
||||
test("Box.Map") {
|
||||
val input = "class Function<A extends Object, B extends Object> extends Object{\nB b;\nB apply(A a){\nreturn this.b;\n}\n}\n\n\nclass Box<S extends Object> extends Object {\nS val ;\nmap( f ) {\nreturn new Box(f.apply(this.val)) ;\n}\n}"
|
||||
val result = FJTypeinference.typeinference(input)
|
||||
assert(result.isRight)
|
||||
println(result.map(it => Main.prettyPrintAST(it)))
|
||||
}
|
||||
|
||||
test("PrincipalType") {
|
||||
val input = "\nclass List<A extends Object> extends Object{\n A head;\n List<A> tail;\n add( a){\n return new List(a, this);\n }\n get(){\n return this.head;\n }\n}\n\nclass PrincipleType extends Object {\n function(a){\n return a.add(this).get();\n }\n}"
|
||||
val result = FJTypeinference.typeinference(input)
|
||||
assert(result.isRight)
|
||||
println(result.map(it => Main.prettyPrintAST(it)))
|
||||
}
|
||||
/*
|
||||
|
||||
class List<A extends Object> extends Object{
|
||||
A head;
|
||||
List<A> tail;
|
||||
add( a){
|
||||
return new List(a, this);
|
||||
test("ListExample") {
|
||||
val input = "\n\nclass List<A extends Object> extends Object{\n A element;\n List<A> succ; \n add(a){\n return new List(a, this);\n }\n\n}\n\nclass Example extends Object{\n\n test(a){\n return a.add(this);\n }\n}"
|
||||
val result = FJTypeinference.typeinference(input)
|
||||
assert(result.isRight)
|
||||
println(result.map(it => Main.prettyPrintAST(it)))
|
||||
}
|
||||
get(){
|
||||
return this.head;
|
||||
|
||||
test("extendsWithComplexType") {
|
||||
val input = "class Pair<A extends Object, B extends Object> extends Object {}\n\nclass Test<A extends Object> extends Pair<Pair<A,A>,A> {\n\nm(a){return this;}\n\n\n}"
|
||||
val result = FJTypeinference.typeinference(input)
|
||||
assert(result.isRight)
|
||||
println(result.map(it => Main.prettyPrintAST(it)))
|
||||
}
|
||||
|
||||
test("pairAdd.twoTimes") {
|
||||
val input = "class Pair<A extends Object> extends Object{\n A fst;\n \n setfst(p) {\n return p;\n }\n }\n\n class Example extends Object{\n\n m(p){\n return p.setfst(p.setfst(this));\n }\n }"
|
||||
val result = FJTypeinference.typeinference(input)
|
||||
assert(result.isRight)
|
||||
println(result.map(it => Main.prettyPrintAST(it)))
|
||||
}
|
||||
}
|
||||
|
||||
class PrincipleType extends Object {
|
||||
function(a){
|
||||
return a.add(this).get();
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
class Function<A extends Object, B extends Object> extends Object{
|
||||
B b;
|
||||
B apply(A a){
|
||||
return this.b;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
class Box<S extends Object> extends Object {
|
||||
S val ;
|
||||
map( f ) {
|
||||
return new Box(f.apply(this.val)) ;
|
||||
}
|
||||
}
|
||||
|
||||
class Function<A extends Object, B extends Object> extends Object{
|
||||
B b;
|
||||
B apply(A a){
|
||||
return this.b;
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
|
||||
class RecursiveMethods extends Object{
|
||||
|
||||
a1(x){ return this.a2(x);}
|
||||
a2(y){ return this.a1(y);}
|
||||
}
|
||||
*/
|
||||
/*
|
||||
Additional Tests:
|
||||
|
||||
class Test extends Object{
|
||||
m(a, b){return a;}
|
||||
m(a,b){return b;}
|
||||
}
|
||||
|
||||
class Test2 extends Object{
|
||||
test(a){return new Test().m(this,a);}
|
||||
}
|
||||
|
||||
*/
|
||||
}
|
||||
|
@ -62,4 +62,11 @@ class ParserTest extends FunSuite {
|
||||
println(fastparse.parse("class List<A extends Object> extends Object{asd(){ return this; }get(){ return this.head;}}"
|
||||
, hb.dhbw.Parser.program(_)))
|
||||
}
|
||||
|
||||
test("Konstruktor"){
|
||||
val parsed = fastparse.parse("class Pair<X extends Object, Y extends Object> extends Object{\n X fst;\n Y snd;\n Pair(fst, snd) {\n this.fst=fst;\n this.snd=snd;\n }\n}"
|
||||
, hb.dhbw.Parser.program(_))
|
||||
assert(parsed.isSuccess)
|
||||
println(parsed.get)
|
||||
}
|
||||
}
|
||||
|
@ -1,5 +1,6 @@
|
||||
|
||||
import hb.dhbw.{FiniteClosure, RefType, TypeVariable, Unify, UnifyEqualsDot, UnifyLessDot, UnifyRefType, UnifyTV}
|
||||
|
||||
import hb.dhbw.{FJNamedType, FiniteClosure, RefType, TypeVariable, Unify, UnifyConstraint, UnifyEqualsDot, UnifyLessDot, UnifyRefType, UnifyTV}
|
||||
import org.scalatest.FunSuite
|
||||
|
||||
class UnifyTest extends FunSuite {
|
||||
@ -9,7 +10,37 @@ class UnifyTest extends FunSuite {
|
||||
|
||||
val fc = new FiniteClosure(Set())
|
||||
|
||||
test("sub-elim rule"){
|
||||
val input : Set[UnifyConstraint] = Set(UnifyLessDot(UnifyTV("a"), UnifyTV("b")), UnifyEqualsDot(UnifyTV("a"), UnifyRefType("a", List())))
|
||||
val result = Unify.postProcessing(input)
|
||||
println(result)
|
||||
assert(result.contains(UnifyEqualsDot(UnifyTV("a"), UnifyTV("b"))))
|
||||
assert(result.contains(UnifyEqualsDot(UnifyTV("b"), UnifyTV("a"))))
|
||||
}
|
||||
|
||||
test("error"){
|
||||
val input : Set[Set[Set[UnifyConstraint]]]= Set(Set(Set(UnifyLessDot(UnifyTV("1"), UnifyTV("B")), UnifyLessDot(UnifyTV("1"), UnifyTV("2")),
|
||||
UnifyLessDot(UnifyRefType("Test", List()), UnifyTV("2")))))
|
||||
val result = Unify.unifyIterative(input, new FiniteClosure(Set((FJNamedType("Test", List()), FJNamedType("Object", List())))))
|
||||
println(result)
|
||||
}
|
||||
|
||||
test("example"){
|
||||
val input : Set[UnifyConstraint] = Set(UnifyEqualsDot(UnifyTV("b"), UnifyTV("y")),
|
||||
UnifyLessDot(UnifyRefType("Pair", List(UnifyRefType("X", List()), UnifyRefType("Y", List()))), UnifyRefType("Pair", List(UnifyTV("w"), UnifyTV("y")))),
|
||||
UnifyLessDot(UnifyRefType("Pair", List(UnifyTV("d"), UnifyTV("e"))), UnifyTV("A")),
|
||||
UnifyLessDot(UnifyTV("F"), UnifyTV("d")),
|
||||
UnifyLessDot(UnifyTV("b"), UnifyTV("e")),
|
||||
UnifyLessDot(UnifyTV("F"), UnifyRefType("Object", List())))
|
||||
val result = Unify.unifyIterative(Set(Set(input)), new FiniteClosure(Set((FJNamedType("Pair", List(FJNamedType("X", List()),FJNamedType("X", List()))), FJNamedType("Object", List())))))
|
||||
println(result)
|
||||
}
|
||||
|
||||
test("getLinks.emptySet"){
|
||||
val input : Set[UnifyLessDot] = Set()
|
||||
val ret = Unify.getLinks(UnifyTV("a"), input)
|
||||
assert(ret.equals(Set.empty))
|
||||
}
|
||||
/*
|
||||
test("Unify.step2") {
|
||||
var step2 = Unify.step2(Set(UnifyLessDot(TypeVariable("a"), TypeVariable("b")),
|
||||
|
Loading…
Reference in New Issue
Block a user