Unify working. Unify output working. Ast output working, but ugly

This commit is contained in:
JanUlrich 2021-10-26 01:41:05 +02:00
parent b576d90f9a
commit 8b4bfa0f47
15 changed files with 651 additions and 147 deletions

View File

@ -1 +1,11 @@
libraryDependencies += "org.scalatest" %% "scalatest" % "3.0.8" % Test
enablePlugins(ScalaJSPlugin)
name := "FJ-Typeinference"
scalaVersion := "2.13.1" // or any other Scala version >= 2.11.12
// This is an application with a main method
scalaJSUseMainModuleInitializer := true
libraryDependencies += "org.scalatest" %% "scalatest" % "3.0.8" % Test
libraryDependencies += "com.lihaoyi" %%% "fastparse" % "2.3.0"
libraryDependencies += "org.scala-js" %%% "scalajs-dom" % "1.1.0"

114
index.css Normal file
View File

@ -0,0 +1,114 @@
body {
background-color: #eee8d5;
max-width: 1200px;
margin: 0px auto;
padding: 5px;
color: #073642;
}
h1,
p {
font-family: sans-serif;
padding: 0px 10px;
}
#content {
width: 100%;
padding: 0px;
height: 460px;
}
#content::after {
content: ".";
visibility: hidden;
display: block;
height: 0;
clear: both;
}
#left,
#right,
textarea {
width: 50%;
height: 100%;
padding: 10px;
box-sizing: border-box;
font-family: monospace;
}
#bottom {
width: 100%;
height: 400px;
padding: 10px;
box-sizing: border-box;
font-family: monospace;
}
#left {
float: left;
}
#right {
float: right;
}
#fj-input,
#ast-output,
#unify-output {
width: 100%;
height: 100%;
box-sizing: border-box;
border-radius: 10px;
padding: 10px;
background-color: #002b36;
/* color: #93a1a1; */
/* color: #cacaca; */
color: #efefef;
font-size: 14px;
}
#fj-input {
resize: none;
outline: none;
}
#ast-output {
border: 1px solid black;
}
.binding {
font-family: monospace;
white-space: pre;
}
.name::before {
content: "val ";
color: #839496;
}
.name::after {
content: " : ";
color: #839496;
}
.name,
.type {
display: inline;
}
.name {
color: #93a1a1;
font-weight: bold;
}
.type {
color: #859900;
font-weight: bold;
display: inline-block;
}
.code-line {
!padding: 0;
!margin: 0;
text-indent: 1em;
}

32
index.html Normal file
View File

@ -0,0 +1,32 @@
<!DOCTYPE html>
<html>
<head>
<meta charset="UTF-8">
<link rel="stylesheet" type="text/css" href="index.css">
<title>Simple-sub demonstration</title>
</head>
<body>
<h1>Simple-sub demonstration</h1>
<div id="content">
<div id="left">
<textarea id="fj-input">
class Test extends Object{}
</textarea>
<!-- let rec recursive_monster = fun x ->
{ thing = x;
self = recursive_monster x } -->
</div>
<div id="right">
<div id="ast-output"></div>
</div>
</div>
<div id="bottom">
<div id="unify-output"></div>
</div>
<script type="text/javascript" src="target/scala-2.13/fj-typeinference-fastopt/main.js"></script>
<br/>
<p>The code is available <a href="https://github.com/LPTK/simple-algebraic-subtyping">on github</a>.</p>
<br/>
<p>Credit: the CSS style sheet of this page was shamelessly stolen from <a href="https://www.cl.cam.ac.uk/~sd601/mlsub/">the MLsub demo page</a>.</p>
</body>
</html>

View File

@ -0,0 +1,44 @@
package hb.dhbw
final case class Class(name: String, params: List[(Type,Type)], superType: RefType, fields: List[(Type,String)], methods: List[Method])
final case class Method(retType: Type, name: String, params: List[(Type, String)], retExpr: Expr)
sealed trait Type
final case class RefType(name: String, params: List[Type]) extends Type
final case class TypeVariable(name: String) extends Type
sealed trait Expr
final case class LocalVar(x: String) extends Expr
final case class FieldVar(e: Expr, f: String) extends Expr
final case class MethodCall(e: Expr, name: String, params: List[Expr]) extends Expr
final case class Constructor(className: String, params: List[Expr]) extends Expr
object ASTBuilder {
def fromParseTree(toAst: List[ParserClass]) = new ASTBuilderMonad().fromParseTree(toAst)
private class ASTBuilderMonad{
var tpvNum = 0
def fromParseTree(toAst: List[ParserClass]) = toAst.map(c => Class(c.name, c.params.map(p => (nTypeToType(p._1), nTypeToType(p._2))),
nTypeToType(c.superType).asInstanceOf[RefType],
c.fields.map(f => (nTypeToType(f._1),f._2)), c.methods.map(m => Method(freshTPV(), m.name, m.params.map(p => (freshTPV(), p)), m.retExpr))))
private def freshTPV() = {
def numToLetter(num: Int) = {
val alphabet = "ABCDEFGHIJKLMNOPQRSTUVWXYZ"
var ret = ""
var n = num
while (n > alphabet.length){
val char = num % alphabet.length
n= num / alphabet.length
ret = ret + alphabet.charAt(char)
}
ret + alphabet.charAt(n)
}
tpvNum = tpvNum+1
TypeVariable(numToLetter(tpvNum))
}
private def nTypeToType(t : NType): Type = RefType(t.name, t.params.map(nTypeToType))
}
}

View File

@ -0,0 +1,51 @@
package hb.dhbw
class CartesianProduct[A](private val setOfSets: List[List[A]]){
private var sizes: List[Int] = null
private var bases: List[Long] = List()
private var max: Long = 1
private var i: Long = 0
def this(setOfSets: Set[Set[A]]){
this(setOfSets.map(_.toList).toList)
var base: Long = 1
sizes = this.setOfSets.map(_.size)
sizes.foreach(size => {
bases = bases :+ size
base = base * size
})
max = base
/*
sizes = constraints.stream().map(OderConstraint::getSize).collect(Collectors.toList());
long base = 1;
for(int size : sizes){
bases.add(base);
base *= size;
}
i = 0;
max = estimateSize() - 1;
*/
}
def hasNext() = i < max
def nextProduct() = {
val baseIt = bases.iterator
val ret = setOfSets.map(set => {
val num = (i/baseIt.next())%set.size
set(num.toInt)
})
i = i + 1
ret.toSet
}
/*
private Set<Pair> get(long num){
Set<Pair> ret = new HashSet<>();
Iterator<Long> baseIt = bases.iterator();
for(OderConstraint constraint : constraints){
ret.addAll(constraint.get((int) ((num/baseIt.next())%constraint.getSize())));
}
return ret;
}
*/
}

View File

@ -0,0 +1,8 @@
package hb.dhbw
class EqSet {
def addAndConstraint(cons: Set[Constraint]) {}
}

View File

@ -0,0 +1,28 @@
package hb.dhbw
object FJTypeinference {
private def convertAndCons(andCons: Constraint): Set[UnifyConstraint] = andCons match {
case AndConstraint(andCons) => andCons.map(convertSingleConstraint).toSet
case c => Set(convertSingleConstraint(c))
}
private def convertOrCons(constraint: Constraint): Set[Set[UnifyConstraint]] = constraint match {
case AndConstraint(andCons) => Set(andCons.map(convertSingleConstraint).toSet)
case OrConstraint(orCons) => orCons.map(convertAndCons).toSet
case x => Set(Set(convertSingleConstraint(x)))
}
private def convertOrConstraints(constraints: List[Constraint]): Set[Set[Set[UnifyConstraint]]] = constraints.map(
convertOrCons
).toSet
private def convertSingleConstraint(constraint: Constraint) = constraint match {
case LessDot(l, r) => UnifyLessDot(l,r)
case EqualsDot(l, r) => UnifyEqualsDot(l,r)
case _ => throw new Exception("Error: Möglicherweise zu tiefe Verschachtelung von OrConstraints")
}
def typeinference(str: String): Either[String, Set[Set[UnifyConstraint]]] = {
val ast = Parser.parse(str).map(ASTBuilder.fromParseTree(_))
val typeResult = ast.map(TYPE.generateConstraints(_))
val unifyResult = typeResult.map(res => Unify.unify(convertOrConstraints(res._1), res._2))
unifyResult
}
}

View File

@ -1,10 +1,6 @@
package hb.dhbw
sealed abstract class Type
final case class TypeVariable(name : String) extends Type
final case class RefType(name : String, params : List[Type]) extends Type
class FiniteClosure(val extendsRelations : Set[(RefType, RefType)]){
private def calculateSupertypes(of: RefType) ={

View File

@ -1,58 +1,86 @@
package hb.dhbw
import hb.dhbw.Unify.{Constraint, EqualsDot, LessDot}
;
import scala.util.Try
import scala.scalajs.js.annotation.JSExportTopLevel
import org.scalajs.dom
import org.scalajs.dom.document
import org.scalajs.dom.raw.{Event, TextEvent, UIEvent, HTMLTextAreaElement}
object Main {
def main(args: Array[String]): Unit = {
val fcPair1 = (RefType("ArrayList", List(TypeVariable("A"))), RefType("List", List(TypeVariable("A"))))
val fcPair3 = (RefType("List", List(TypeVariable("A"))), RefType("Object", List()))
val fcPair2 = (RefType("MyMap", List(TypeVariable("A"), TypeVariable("B"))), RefType("Map", List(RefType("String", List(TypeVariable("A"))), TypeVariable("B"))))
val cTest: Set[Set[Int]] = Set(Set(1,2), Set(4,3))
val fc = new FiniteClosure(Set(fcPair1, fcPair2, fcPair3))
//val cart = Unify.cartesianProduct(cTest)
//println(cart)
//val superTypes = fc.superTypes(RefType("List", List(RefType("Object", List()))))
//println(superTypes)
//val step1 = Unify.step2(Set(LessDot(TypeVariable("a"), TypeVariable("b")),
// LessDot(TypeVariable("a"), RefType("List", List(RefType("Object", List()))))), fc)
//println(step1)
//val step2 = Unify.step2(Set(LessDot(TypeVariable("a"), TypeVariable("b")),
// LessDot(RefType("List", List(RefType("Object", List()))), TypeVariable("a"))), fc)
//println(step2)
//println(fc.isPossibleSupertype("MyMap", "List"))
val eqMatchTest = Set(LessDot(TypeVariable("a"), RefType("List", List(RefType("Object", List())))), LessDot(TypeVariable("a"), RefType("ArrayList", List(RefType("Object", List())))))
//println(Unify.matchRule(eqMatchTest.asInstanceOf[Set[Unify.Constraint]], fc))
val eqEqualsTest : Set[Constraint] = Set(LessDot(TypeVariable("a"), TypeVariable("b")),LessDot(TypeVariable("b"), TypeVariable("c")), LessDot(TypeVariable("c"), TypeVariable("a")))
//println(Unify.equalsRule(eqEqualsTest))
//val eqIsLinkedTest = Set(LessDot(TypeVariable("a"), TypeVariable("c")), LessDot(TypeVariable("b"), TypeVariable("c")))
//println(Unify.isLinked(TypeVariable("a"), TypeVariable("b"), eqIsLinkedTest))
val eqAdoptTest = Set(LessDot(TypeVariable("b"), TypeVariable("a")),LessDot(TypeVariable("a"), RefType("List", List(RefType("Object", List())))), LessDot(TypeVariable("b"), RefType("ArrayList", List(RefType("Object", List())))))
//println(Unify.adoptRule(eqAdoptTest.asInstanceOf[Set[Constraint]], fc))
val eqAdaptTest: Set[Constraint] = Set(EqualsDot(TypeVariable("a"), TypeVariable("b")),LessDot(RefType("ArrayList",List(RefType("Test",List()))),RefType("List",List(RefType("Object",List())))))
//println(Unify.adaptRule(eqAdaptTest, fc))
val eqReduceTest : Set[Constraint] = Set(EqualsDot(RefType("List",List(RefType("Test",List()))),RefType("List",List(RefType("Object",List())))))
//println(Unify.reduceRule(eqReduceTest))
val applyRulesTest = eqMatchTest ++ eqEqualsTest ++ eqAdoptTest ++ eqAdaptTest ++ eqReduceTest
//println(Unify.applyRules(fc)(applyRulesTest))
println(Unify.unify(Set(Set(applyRulesTest)), fc))
//val replacedType = fc.replaceParams(RefType("List", List(TypePlaceholder("A"))), RefType("ArrayList", List(RefType("String", List()))))
//println(replacedType)
//val replacedType2 = fc.replaceParams(RefType("Map", List(RefType("String", List(TypePlaceholder("A"))), TypePlaceholder("B"))), RefType("MyMap", List(RefType("String", List()), RefType("Integer", List()))))
//println(replacedType2)
val source = document.querySelector("#fj-input")
update(source.textContent)
source.addEventListener("input", typecheck)
}
}
@JSExportTopLevel("typecheck")
def typecheck(e: UIEvent): Unit = {
e.target match {
case elt: HTMLTextAreaElement =>
update(elt.value)
}
}
def update(str: String): Unit = {
val target = document.querySelector("#unify-output")
target.innerHTML = FJTypeinference.typeinference(str).fold(
(error) => error,
(result) => prettyPrintHTML(result)
)
val astOutput = document.querySelector("#ast-output")
astOutput.innerHTML = Parser.parse(str).map( parseTree =>
prettyPrintHTMLAST(ASTBuilder.fromParseTree(parseTree))).merge
}
def prettyPrintHTML(c: Class): String = {
"class "+c.name+" extends " + prettyPrintHTML(c.superType) + "{</br>" +
"<p class=\"code-line\">"+
c.fields.map(f => prettyPrintHTML(f._1)+" "+f._2+";").mkString("</br>")+"</br>" +
c.methods.map(prettyPrintHTML(_)).mkString("</br>")+"</br>}" +
"</p>"
}
def prettyPrintHTMLAST(ast: List[Class]): String = {
ast.map(prettyPrintHTML(_)).mkString("</br>")
}
def prettyPrintHTML(method: Method): String = {
prettyPrintHTML(method.retType) + " " +
method.name + "(" + method.params.map(p => prettyPrintHTML(p._1) + " " + p._2).mkString(", ") + ") { </br>" +
"<p class=\"code-line\">"+
"return "+prettyPrintHTML(method.retExpr)+";" +
"</p></br>}"
}
def prettyPrintHTML(expr : Expr): String = expr match {
case MethodCall(e, name, params) => prettyPrintHTML(e)+"."+name+"("+params.map(prettyPrintHTML(_)).mkString(", ")+")"
case FieldVar(e, f) => prettyPrintHTML(e)+"."+f
case LocalVar(x) => x
case Constructor(className, params) => "new "+className+"("+params.map(prettyPrintHTML(_)).mkString(", ")+")"
}
def prettyPrintHTML(unifyResult : Set[Set[UnifyConstraint]]): String = unifyResult.map(
solution => "<p>{" + solution.map(prettyPrintHTML(_)).mkString(", ") + "}</p>"
).foldLeft("Solutions:")(_ + "" + _)
def prettyPrintHTML(cons: UnifyConstraint): String = cons match {
case UnifyLessDot(a, b) => "("+prettyPrintHTML(a)+" <. "+prettyPrintHTML(b)+")"
case UnifyEqualsDot(a, b) => "("+prettyPrintHTML(a)+" =. "+prettyPrintHTML(b)+")"
}
def prettyPrintHTML(t: Type): String = t match {
case RefType(name, List()) => name
case RefType(name, params) => name + "&lt;" + params.map(prettyPrintHTML).mkString(", ") + "&gt;"
case TypeVariable(name) => "<b>" + name + "</b>"
}
def prettyPrint(unifyResult : Set[Set[UnifyConstraint]]): String = unifyResult.map(
solution => "{" + solution.map(prettyPrint(_)).mkString(", ") + "}"
).foldLeft("Solutions:")(_ + "\n\n" + _)
def prettyPrint(cons: UnifyConstraint): String = cons match {
case UnifyLessDot(a, b) => "("+prettyPrint(a)+" <. "+prettyPrint(b)+")"
case UnifyEqualsDot(a, b) => "("+prettyPrint(a)+" =. "+prettyPrint(b)+")"
}
def prettyPrint(t: Type): String = t match {
case RefType(name, List()) => name
case RefType(name, params) => name + "<" + params.map(prettyPrint).mkString(", ") + ">"
case TypeVariable(name) => "_" + name + "_"
}
}

View File

@ -0,0 +1,52 @@
package hb.dhbw
import fastparse._, fastparse.ScalaWhitespace._
final case class ParserClass(name: String, params: List[(NType,NType)], superType: NType, fields: List[(NType,String)], methods: List[ParserMethod])
final case class ParserMethod(name: String, params: List[String], retExpr: Expr)
final case class NType(name: String, params: List[NType])
object Parser {
val keywords = Set("class", "new", "extends")
def kw[_: P](s: String) = s ~~ !(letter | digit | "_" | "'")
def letter[_: P] = P( lowercase | uppercase )
def lowercase[_: P] = P( CharIn("a-z") )
def uppercase[_: P] = P( CharIn("A-Z") )
def digit[_: P] = P( CharIn("0-9") )
def number[_: P]: P[Int] = P( CharIn("0-9").repX(1).!.map(_.toInt) )
def ident[_: P]: P[String] =
P( (letter | "_") ~~ (letter | digit | "_" | "'").repX ).!.filter(!keywords(_))
def fieldVar[_: P]: P[Expr] = P( ".".! ~ ident ).map(ite => FieldVar(null, ite._2) )
def prefixMethodCall[_: P]: P[Expr] = P( "." ~ methodCall)
def methodCall[_: P]: P[MethodCall] =P( ident ~ "(".! ~ (expr ~ (",".! ~ expr).rep.map(_.toList.map{_._2})).? ~ ")".! ).map(ite => MethodCall(null, ite._1, ite._3.map { ite => ite._1 :: ite._2 } .getOrElse(List.empty)) )
def variable[_: P]: P[Expr] = P(ident).map(LocalVar)
def expr[_: P]: P[Expr] = P( variable ~ (prefixMethodCall | fieldVar).rep.map(_.toList) )
.map(ite => ite._2.foldLeft(ite._1) { (e1 : Expr, e2 : Expr) =>
e2 match{
case MethodCall(_, name, e3) => MethodCall(e1, name, e3)
case FieldVar(_, name) => FieldVar(e1, name)
}
})
def constructor[_: P]: P[Expr] = P( kw("new") ~ methodCall).map(m => Constructor(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 field[_: P]: P[(NType, String)] = P(typeParser ~ ident ~ ";")
def method[_: P]: P[ParserMethod] = P(ident ~ (("("~")").map(it => List()) | ("(" ~ ident ~ ("," ~ ident).rep(0) ~ ")").map(ite => List(ite._1) ++ ite._2))
~ "{" ~ kw("return") ~ expr ~ ";" ~ "}")
.map(ite => ParserMethod(ite._1, ite._2, ite._3))
def genericParamList[_: P]: P[List[(NType,NType)]] = P("<" ~ (typeParser ~ kw("extends") ~ typeParser) ~ ("," ~ (typeParser ~ kw("extends") ~ typeParser)).rep(0) ~ ">").map(ite => List((ite._1, ite._2)) ++ ite._3.map(ite3 => (ite3._1, ite3._2)))
def typeParser[_: P]: P[NType] = P(ident ~ ("<" ~ typeParser ~ ("," ~ typeParser).rep(0) ~ ">").?)
.map(ite => NType(ite._1, ite._2.map(ite => List(ite._1) ++ ite._2).getOrElse(List())))
def program[_: P]: P[List[ParserClass]] = "" ~ classDefinition.rep(1).map(_.toList) ~ End
def parse(input: String): Either[String, List[ParserClass]] = fastparse.parse(input, program(_)).fold(
(_, _, extra) => Left(s"Parser Error: $extra"),
(v, _) => Right(v)
)
}

View File

@ -0,0 +1,69 @@
package hb.dhbw
sealed trait Constraint
final case class AndConstraint(andCons: List[Constraint]) extends Constraint
final case class OrConstraint(orCons: List[Constraint]) extends Constraint
final case class EqualsDot(l: Type, r: Type) extends Constraint
final case class LessDot(l: Type, r: Type) extends Constraint
object TYPE {
def generateConstraints(c: List[Class]) = {
new TYPEMonad().TYPEClass(c)
}
private class TYPEMonad{
var tpvNum = 0
private def generateFC(ast: List[Class]): FiniteClosure = new FiniteClosure(ast.map(c => (cToType(c), c.superType)).toSet)
def TYPEClass(ast: List[Class]) = {
(ast.flatMap(cl => cl.methods.flatMap(m => TYPEMethod(m, cToType(cl), ast))), generateFC(ast))
}
private def freshTPV() = {
tpvNum = tpvNum+1
TypeVariable(tpvNum.toString)
}
private def TYPEMethod(method: Method, thisType: RefType, ast: List[Class]) = {
val (rty, cons) = TYPEExpr(method.retExpr, List((thisType, "this")) ++ method.params, ast)
LessDot(rty, method.retType) :: cons
}
private def TYPEExpr(expr: Expr, localVars: List[(Type, String)],ast: List[Class]) : (Type, List[Constraint]) =expr match {
case LocalVar(n) => localVars.find(it => it._2.equals(n)).map(p => (p._1, List()))
.getOrElse(throw new Exception("Local Variable "+ n + " not found"))
case FieldVar(e, f) => {
val (rty, cons) = TYPEExpr(e, localVars, ast)
val fields = findFields(f, ast)
val a = freshTPV()
val orCons = OrConstraint(fields.map(f => AndConstraint(List(EqualsDot(rty, cToType(f._1)), EqualsDot(a, f._2)))))
(a, orCons :: cons)
}
case MethodCall(e, name, params) => {
val a = freshTPV()
val (rty, cons) = TYPEExpr(e, localVars, ast)
val es = params.map(ex => TYPEExpr(ex, localVars, ast))
val methods = findMethods(name, es.size, ast)
val consM = methods.map(m => AndConstraint(
List(EqualsDot(rty, cToType(m._1)), EqualsDot(a, m._2.retType))
++ m._2.params.map(_._1).zip(es.map(_._1)).map(a => LessDot(a._2, a._1))
))
(a, cons ++ es.flatMap(_._2) ++ List(OrConstraint(consM)))
}
case Constructor(className, params) => {
throw new NotImplementedError()
}
}
private def findMethods(m: String, numParams: Int, ast: List[Class]) =
ast.flatMap(c => c.methods.filter(method => method.name.equals(m) && method.params.size == numParams).map(it => (c, it)))
private def findFields(f: String, ast: List[Class]) =
ast.flatMap(c => c.fields.filter(field => field._2.equals(f)).map(it => (c, it._1)))
private def cToType(c: Class) = RefType(c.name, c.params.map(it => it._1))
}
}

View File

@ -1,13 +1,13 @@
package hb.dhbw
sealed abstract class UnifyConstraint(val left: Type, val right: Type)
final case class UnifyLessDot(override val left: Type, override val right: Type) extends UnifyConstraint(left, right)
final case class UnifyEqualsDot(override val left: Type, override val right: Type) extends UnifyConstraint(left, right)
object Unify {
sealed abstract class Constraint(val left: Type, val right: Type)
final case class LessDot(override val left: Type, override val right: Type) extends Constraint(left, right)
final case class EqualsDot(override val left: Type, override val right: Type) extends Constraint(left, right)
def unify(orCons: Set[Set[Set[Constraint]]], fc: FiniteClosure) : Set[Set[Constraint]] = {
def unify(orCons: Set[Set[Set[UnifyConstraint]]], fc: FiniteClosure) : Set[Set[UnifyConstraint]] = {
val eqSets = cartesianProduct(orCons)
val step2Results = eqSets.flatMap(eqSet => {
val rulesResult = applyRules(fc)(eqSet.flatten)
@ -23,124 +23,124 @@ object Unify {
})
}
def step2(eq : Set[Constraint], fc: FiniteClosure) ={
def step2(eq : Set[UnifyConstraint], fc: FiniteClosure) ={
val eq1 = eq.filter(c => c match{
case LessDot(TypeVariable(_), TypeVariable(_)) => true
case EqualsDot(TypeVariable(_), TypeVariable(_)) => true
case UnifyLessDot(TypeVariable(_), TypeVariable(_)) => true
case UnifyEqualsDot(TypeVariable(_), TypeVariable(_)) => true
case _ => false
})
val cLessdotACons: Set[Set[Set[Constraint]]] = eq.map(c => c match{
case LessDot(RefType(name,params), TypeVariable(a)) =>
val cUnifyLessDotACons: Set[Set[Set[UnifyConstraint]]] = eq.map(c => c match{
case UnifyLessDot(RefType(name,params), TypeVariable(a)) =>
fc.superTypes(RefType(name,params))
.map(superType => Set(EqualsDot(TypeVariable(a), superType).asInstanceOf[Constraint]))
.map(superType => Set(UnifyEqualsDot(TypeVariable(a), superType).asInstanceOf[UnifyConstraint]))
case _ => null
}).filter(s => s!=null)
val alessdota = eq1.filter(c => c match{
case LessDot(TypeVariable(_), TypeVariable(_)) => true
val aUnifyLessDota = eq1.filter(c => c match{
case UnifyLessDot(TypeVariable(_), TypeVariable(_)) => true
case _ => false
}).asInstanceOf[Set[LessDot]]
}).asInstanceOf[Set[UnifyLessDot]]
val aLessdotCConsAndBs: Set[(LessDot,Option[TypeVariable])] = eq.map(c => c match{
case LessDot(TypeVariable(a),RefType(name,params)) =>{
val bs = alessdota.flatMap(c => Set(c.left, c.right)).asInstanceOf[Set[TypeVariable]]
.filter(c => !a.equals(c) && isLinked(TypeVariable(a), c, alessdota))
val aUnifyLessDotCConsAndBs: Set[(UnifyLessDot,Option[TypeVariable])] = eq.map(c => c match{
case UnifyLessDot(TypeVariable(a),RefType(name,params)) =>{
val bs = aUnifyLessDota.flatMap(c => Set(c.left, c.right)).asInstanceOf[Set[TypeVariable]]
.filter(c => !a.equals(c) && isLinked(TypeVariable(a), c, aUnifyLessDota))
if(bs.isEmpty){
Set((LessDot(TypeVariable(a),RefType(name,params)),None))
Set((UnifyLessDot(TypeVariable(a),RefType(name,params)),None))
}else{
bs.map(b => (LessDot(TypeVariable(a),RefType(name,params)),Some(b)))
bs.map(b => (UnifyLessDot(TypeVariable(a),RefType(name,params)),Some(b)))
}
}
case _ => null
}).filter(s => s!=null).flatten
val aLessdotCCons = aLessdotCConsAndBs.map{
case (ac:LessDot,Some(b)) =>
Set(Set(LessDot(b, ac.right))) ++
val aUnifyLessDotCCons = aUnifyLessDotCConsAndBs.map{
case (ac:UnifyLessDot,Some(b)) =>
Set(Set(UnifyLessDot(b, ac.right))) ++
fc.superTypes(ac.right.asInstanceOf[RefType])
.map(superType => Set(EqualsDot(b, superType)))
.map(superType => Set(UnifyEqualsDot(b, superType)))
case (ac, None) => null
}.filter(c => c != null).asInstanceOf[Set[Set[Set[Constraint]]]]
}.filter(c => c != null).asInstanceOf[Set[Set[Set[UnifyConstraint]]]]
val eq2 = eq.filter(c => c match{
case LessDot(TypeVariable(_), RefType(_,_)) => true
case EqualsDot(TypeVariable(_), RefType(_,_)) => true
case EqualsDot(RefType(_,_),TypeVariable(_)) => true
case UnifyLessDot(TypeVariable(_), RefType(_,_)) => true
case UnifyEqualsDot(TypeVariable(_), RefType(_,_)) => true
case UnifyEqualsDot(RefType(_,_),TypeVariable(_)) => true
case _ => false
})
val eqSet = cartesianProduct(Set(Set(eq1)) ++ Set(Set(eq2)) ++ aLessdotCCons ++ cLessdotACons)
val eqSet = cartesianProduct(Set(Set(eq1)) ++ Set(Set(eq2)) ++ aUnifyLessDotCCons ++ cUnifyLessDotACons)
eqSet.map( s => s.flatten)
}
private def getALessdotC(from: Set[Constraint]) = from.filter(c => c match{
case LessDot(TypeVariable(_), RefType(_,_)) => true
private def getAUnifyLessDotC(from: Set[UnifyConstraint]) = from.filter(c => c match{
case UnifyLessDot(TypeVariable(_), RefType(_,_)) => true
case _ => false
}).asInstanceOf[Set[LessDot]]
}).asInstanceOf[Set[UnifyLessDot]]
def matchRule(eq : Set[Constraint], fc: FiniteClosure) = {
val aLessdotC = getALessdotC(eq)
(eq -- aLessdotC) ++ aLessdotC.map(c => {
val smallerC = aLessdotC.find(c2 => c2 != c && c2.left.equals(c.left) && fc.isPossibleSupertype(c2.right.asInstanceOf[RefType].name,c.right.asInstanceOf[RefType].name))
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[RefType].name,c.right.asInstanceOf[RefType].name))
if(smallerC.isEmpty){
c
}else{
LessDot(smallerC.get.right, c.right)
UnifyLessDot(smallerC.get.right, c.right)
}
}
)
}
def reduceRule(eq: Set[Constraint]) = eq.flatMap(c => c match {
case EqualsDot(RefType(an, ap), RefType(bn, bp)) => {
def reduceRule(eq: Set[UnifyConstraint]) = eq.flatMap(c => c match {
case UnifyEqualsDot(RefType(an, ap), RefType(bn, bp)) => {
if(an.equals(bn)){
ap.zip(bp).map(p => EqualsDot(p._1, p._2))
ap.zip(bp).map(p => UnifyEqualsDot(p._1, p._2))
}else{
Set(LessDot(RefType(an, ap), RefType(bn, bp)))
Set(UnifyLessDot(RefType(an, ap), RefType(bn, bp)))
}
}
case x => Set(x)
})
def swapRule(eq : Set[Constraint]) = eq.map(c => c match {
case EqualsDot(RefType(an, ap), TypeVariable(a)) => EqualsDot(TypeVariable(a), RefType(an, ap))
def swapRule(eq : Set[UnifyConstraint]) = eq.map(c => c match {
case UnifyEqualsDot(RefType(an, ap), TypeVariable(a)) => UnifyEqualsDot(TypeVariable(a), RefType(an, ap))
case x => x
})
def adaptRule(eq: Set[Constraint], fc: FiniteClosure) = {
def adaptRule(eq: Set[UnifyConstraint], fc: FiniteClosure) = {
eq.map(c => c match {
case LessDot(RefType(an, ap), RefType(bn, bp)) => {
case UnifyLessDot(RefType(an, ap), RefType(bn, bp)) => {
if(fc.isPossibleSupertype(an, bn)){
EqualsDot(fc.superTypes(RefType(an, ap)).find(r => r.name.equals(bn)).get, RefType(bn, bp))
UnifyEqualsDot(fc.superTypes(RefType(an, ap)).find(r => r.name.equals(bn)).get, RefType(bn, bp))
}else{
LessDot(RefType(an, ap), RefType(bn, bp))
UnifyLessDot(RefType(an, ap), RefType(bn, bp))
}
}
case x => x
})
}
def adoptRule(eq: Set[Constraint], fc: FiniteClosure) ={
val aLessdota = eq.filter(c => c match{
case LessDot(TypeVariable(_), TypeVariable(_)) => true
def adoptRule(eq: Set[UnifyConstraint], fc: FiniteClosure) ={
val aUnifyLessDota = eq.filter(c => c match{
case UnifyLessDot(TypeVariable(_), TypeVariable(_)) => true
case _ => false
}).asInstanceOf[Set[LessDot]]
val aLessdotC = getALessdotC(eq)
(eq -- aLessdotC) ++ aLessdotC.map(c => {
val smallerC = aLessdotC.find(c2 => c2 != c
&& isLinked(c2.left.asInstanceOf[TypeVariable], c.left.asInstanceOf[TypeVariable], aLessdota)
}).asInstanceOf[Set[UnifyLessDot]]
val aUnifyLessDotC = getAUnifyLessDotC(eq)
(eq -- aUnifyLessDotC) ++ aUnifyLessDotC.map(c => {
val smallerC = aUnifyLessDotC.find(c2 => c2 != c
&& isLinked(c2.left.asInstanceOf[TypeVariable], c.left.asInstanceOf[TypeVariable], aUnifyLessDota)
&& fc.isPossibleSupertype(c2.right.asInstanceOf[RefType].name,c.right.asInstanceOf[RefType].name))
if(smallerC.isEmpty){
c
}else{
LessDot(smallerC.get.right, c.right)
UnifyLessDot(smallerC.get.right, c.right)
}
}
)
}
private def isLinked(a: TypeVariable, b: TypeVariable, aLessdota: Set[LessDot]): Boolean = {
private def isLinked(a: TypeVariable, b: TypeVariable, aUnifyLessDota: Set[UnifyLessDot]): Boolean = {
def getRightSides(of: TypeVariable) ={
aLessdota.filter(c => c.left.asInstanceOf[TypeVariable].name.equals(of.name))
aUnifyLessDota.filter(c => c.left.asInstanceOf[TypeVariable].name.equals(of.name))
}
val rightsides = getRightSides(a).map(c => c.right)
if(rightsides.isEmpty){
@ -148,17 +148,17 @@ object Unify {
} else if (rightsides.contains(b)){
true
}else{
rightsides.foldLeft(false)((r, c) => r || isLinked(c.asInstanceOf[TypeVariable],b, aLessdota))
rightsides.foldLeft(false)((r, c) => r || isLinked(c.asInstanceOf[TypeVariable],b, aUnifyLessDota))
}
}
private def findCircles(aLessdota: Set[LessDot]) ={
private def findCircles(aUnifyLessDota: Set[UnifyLessDot]) ={
def getRightSides(of: TypeVariable) ={
aLessdota.filter(c => c.left.asInstanceOf[TypeVariable].name.equals(of.name))
aUnifyLessDota.filter(c => c.left.asInstanceOf[TypeVariable].name.equals(of.name))
}
def findCircle(graph: List[LessDot]): List[LessDot] = {
def findCircle(graph: List[UnifyLessDot]): List[UnifyLessDot] = {
val newAdditions = getRightSides(graph.last.right.asInstanceOf[TypeVariable])
var circle: List[LessDot] = List()
var circle: List[UnifyLessDot] = List()
val iterator = newAdditions.iterator
while(iterator.hasNext && circle.isEmpty){
val newAdd = iterator.next()
@ -170,18 +170,18 @@ object Unify {
}
circle
}
aLessdota.view.map(c => findCircle(List(c)))
aUnifyLessDota.view.map(c => findCircle(List(c)))
}
def equalsRule(eq: Set[Constraint]) ={
val aLessdota = eq.filter(c => c match{
case LessDot(TypeVariable(_), TypeVariable(_)) => true
def equalsRule(eq: Set[UnifyConstraint]) ={
val aUnifyLessDota = eq.filter(c => c match{
case UnifyLessDot(TypeVariable(_), TypeVariable(_)) => true
case _ => false
}).asInstanceOf[Set[LessDot]]
val circle = findCircles(aLessdota).find(!_.isEmpty)
}).asInstanceOf[Set[UnifyLessDot]]
val circle = findCircles(aUnifyLessDota).find(!_.isEmpty)
if(circle.isDefined){
val newEq = eq -- circle.get
Some(newEq ++ (circle.get.map(c => EqualsDot(c.left, c.right))))
Some(newEq ++ (circle.get.map(c => UnifyEqualsDot(c.left, c.right))))
}else{
None
}
@ -192,30 +192,31 @@ object Unify {
case TypeVariable(a) => tv.equals(TypeVariable(a))
case RefType(a,p) => paramsContain(tv, RefType(a,p))
}).isDefined
def substStep(eq: Set[Constraint]) = eq.find(c => c match {
case EqualsDot(TypeVariable(a), RefType(n, p)) => !paramsContain(TypeVariable(a), RefType(n,p))
def substStep(eq: Set[UnifyConstraint]) = eq.find(c => c match {
case UnifyEqualsDot(TypeVariable(a), RefType(n, p)) => !paramsContain(TypeVariable(a), RefType(n,p))
case UnifyEqualsDot(TypeVariable(a), TypeVariable(b)) => true
case _ => false
}).map(c => (subst(c.left.asInstanceOf[TypeVariable], c.right.asInstanceOf[RefType], eq), Some(c))).getOrElse((eq, None))
}).map(c => (subst(c.left.asInstanceOf[TypeVariable], c.right, eq), Some(c))).getOrElse((eq, None))
private def subst(a: TypeVariable, withType: RefType,in: Type) :Type = in match {
case RefType(n, p) => RefType(n,p.map(t => subst(a, withType, t)).asInstanceOf[List[Type]])
private def substHelper(a: TypeVariable, withType: Type,in: Type) :Type = in match {
case RefType(n, p) => RefType(n,p.map(t => substHelper(a, withType, t)).asInstanceOf[List[Type]])
case TypeVariable(n) =>
if(a.equals(in)){withType}else{in}
}
def subst(a: TypeVariable, refType: RefType,eq: Set[Constraint]): Set[Constraint] = {
def subst(a: TypeVariable, substType: Type,eq: Set[UnifyConstraint]): Set[UnifyConstraint] = {
eq.map(c => c match {
case LessDot(left, right) => LessDot(subst(a, refType, left), subst(a, refType, right))
case EqualsDot(left, right) => EqualsDot(subst(a, refType, left), subst(a, refType, right))
case UnifyLessDot(left, right) => UnifyLessDot(substHelper(a, substType, left), substHelper(a, substType, right))
case UnifyEqualsDot(left, right) => UnifyEqualsDot(substHelper(a, substType, left), substHelper(a, substType, right))
})
}
private def doWhileSome(fun: Set[Constraint]=>Option[Set[Constraint]], eqTemp: Set[Constraint]): Set[Constraint] =
private def doWhileSome(fun: Set[UnifyConstraint]=>Option[Set[UnifyConstraint]], eqTemp: Set[UnifyConstraint]): Set[UnifyConstraint] =
fun(eqTemp).map(eqTemp2 => doWhileSome(fun,eqTemp2)).getOrElse(eqTemp)
def applyRules(fc: FiniteClosure) = (eq: Set[Constraint]) => {
var eqNew: Set[Constraint] = null
var eqFinish: Set[Constraint] = eq
def applyRules(fc: FiniteClosure) = (eq: Set[UnifyConstraint]) => {
var eqNew: Set[UnifyConstraint] = null
var eqFinish: Set[UnifyConstraint] = eq
do{
eqNew = doWhileSome(Unify.equalsRule,eqFinish)
eqFinish = reduceRule(matchRule(adaptRule(adaptRule(eqNew, fc), fc), fc))

View File

@ -0,0 +1,30 @@
import hb.dhbw.{FJTypeinference, Main}
import org.scalatest.FunSuite
class IntegrationTest extends FunSuite {
test("EmptyClass"){
val ast = (fastparse.parse(("e.m(a)"), hb.dhbw.Parser.classDefinition(_)))
//hb.dhbw.TYPE.TYPEClass(ast.get)
}
test("IdMethod"){
val result = FJTypeinference.typeinference("class Test extends Object {\nObject f;\nm(a){return a;}\n}")
println(result)
}
test("IdMethodRecursive"){
val result = FJTypeinference.typeinference("class Test extends Object {\n Object f;\n m(a, b){return this.m(b, a); }\n}")
println(result)
}
test("ListAddDefinition"){
val result = FJTypeinference.typeinference("class List<A extends Object> extends Object{\n add(a){\n return this;\n}\n}")
println(result)
}
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(_)))
}
}

View File

@ -0,0 +1,42 @@
import org.scalatest.FunSuite
class ParserTest extends FunSuite {
test("Parser.class"){
println(hb.dhbw.Parser.parse(" class Test extends Object{}"))
}
test("Parser.methodCall"){
println(fastparse.parse(("e.m(a)"), hb.dhbw.Parser.methodCall(_)))
}
test("Parser.constructor"){
println(fastparse.parse(("new Test(a)"), hb.dhbw.Parser.constructor(_)))
}
test("Parser.type"){
println(fastparse.parse("Test<Test<Object>>", hb.dhbw.Parser.typeParser(_)))
}
test("Parser.method"){
println(fastparse.parse("m(a,b){return a;}", hb.dhbw.Parser.method(_)))
println(fastparse.parse("m(){return a;}", hb.dhbw.Parser.method(_)))
assert(fastparse.parse("m(){return a;}", hb.dhbw.Parser.method(_)).isSuccess)
assert(fastparse.parse("m(a,b){return a.f;}", hb.dhbw.Parser.method(_)).isSuccess)
}
test("Parser.classDefinition"){
println(fastparse.parse("class Test{\n m(a,b){return a;}}", hb.dhbw.Parser.classDefinition(_)))
assert(fastparse.parse("class Test{m(a,b){return a;}}", hb.dhbw.Parser.classDefinition(_)).isSuccess)
}
test("Parser.classDefinition.generics"){
println(fastparse.parse("class Test{\n m(a,b){return a;}}", hb.dhbw.Parser.classDefinition(_)))
assert(fastparse.parse("class Test{m(a,b){return a;}}", hb.dhbw.Parser.classDefinition(_)).isSuccess)
}
test("Parser.genericParamList"){
println(fastparse.parse("<Test extends Object>", hb.dhbw.Parser.genericParamList(_)))
println(fastparse.parse("<Test extends Object, Test<Object> extends Test<Object>>", hb.dhbw.Parser.genericParamList(_)))
}
}

View File

@ -1,6 +1,5 @@
import hb.dhbw.{FiniteClosure, RefType, TypeVariable, Unify}
import hb.dhbw.Unify.LessDot
import hb.dhbw.{FiniteClosure, RefType, TypeVariable, Unify, UnifyEqualsDot, UnifyLessDot}
import org.scalatest.FunSuite
class UnifyTest extends FunSuite {
@ -11,19 +10,19 @@ class UnifyTest extends FunSuite {
val fc = new FiniteClosure(Set(fcPair1, fcPair2, fcPair3))
test("Unify.step2.alinkedb"){
var step2 = Unify.step2(Set(LessDot(TypeVariable("c"), TypeVariable("b")),
LessDot(TypeVariable("a"), RefType("List", List(RefType("Object", List()))))), fc)
var step2 = Unify.step2(Set(UnifyLessDot(TypeVariable("c"), TypeVariable("b")),
UnifyLessDot(TypeVariable("a"), RefType("List", List(RefType("Object", List()))))), fc)
assert(step2.head.size == 2)
}
test("Unify.step2") {
var step2 = Unify.step2(Set(LessDot(TypeVariable("a"), TypeVariable("b")),
LessDot(TypeVariable("a"), RefType("List", List(RefType("Object", List()))))), fc)
var step2 = Unify.step2(Set(UnifyLessDot(TypeVariable("a"), TypeVariable("b")),
UnifyLessDot(TypeVariable("a"), RefType("List", List(RefType("Object", List()))))), fc)
println(step2)
assert(!step2.isEmpty)
step2 = Unify.step2(Set(LessDot(TypeVariable("a"), TypeVariable("b")),
LessDot(RefType("List", List(RefType("Object", List()))), TypeVariable("a"))), fc)
step2 = Unify.step2(Set(UnifyLessDot(TypeVariable("a"), TypeVariable("b")),
UnifyLessDot(RefType("List", List(RefType("Object", List()))), TypeVariable("a"))), fc)
println(step2)
}