Merge branch 'transfer'
This commit is contained in:
commit
ef75c83ef6
@ -18,9 +18,6 @@
|
||||
<pre><div id="ast-output"></div></pre>
|
||||
</div>
|
||||
</div>
|
||||
<div id="bottom">
|
||||
<div id="unify-output"></div>
|
||||
</div>
|
||||
<script type="text/javascript" src="highlight.min.js"></script>
|
||||
<script type="text/javascript" src="target/scala-2.13/fj-typeinference-opt/main.js"></script>
|
||||
<br/>
|
||||
|
@ -78,28 +78,26 @@ object FJTypeinference {
|
||||
Class(in.name, in.genericParams, in.superType, in.fields, newMethods.toList)
|
||||
}
|
||||
|
||||
def typeinference(str: String): Either[String, (Set[Set[UnifyConstraint]], List[Class])] = {
|
||||
def sigmaReplace(sigma:Map[String, Type], unifyType: UnifyType): Type = unifyType match {
|
||||
case UnifyRefType(n, ps) => RefType(n, ps.map(it => sigmaReplace(sigma, it)))
|
||||
case UnifyTV(a) => sigma(a)
|
||||
}
|
||||
|
||||
def typeinference(str: String): Either[String, List[Class]] = {
|
||||
val ast = Parser.parse(str).map(ASTBuilder.fromParseTree(_))
|
||||
var typedClasses: List[Class] = List()
|
||||
val typeResult = ast.map(ast => {
|
||||
var unifyResults = Set[Set[Set[UnifyConstraint]]]()
|
||||
ast.map(ast => {
|
||||
ast.foldLeft(List[Class]())((cOld, c) => {
|
||||
val newClassList = cOld :+ c
|
||||
val typeResult = TYPE.generateConstraints(newClassList, generateFC(newClassList))
|
||||
val unifyResult = Unify.unifyIterative(convertOrConstraints(typeResult._1), typeResult._2)
|
||||
|
||||
//Insert intersection types
|
||||
val typeInsertedC = InsertTypes.insert(unifyResult, c)
|
||||
//val typeInsertedC = InsertTypes.applyResult(sigma, generics, c)//InsertTypes.insert(unifyResult, c)
|
||||
val typeInsertedC = InsertTypes.applyUnifyResult(unifyResult, c)
|
||||
typedClasses = typedClasses :+ typeInsertedC
|
||||
unifyResults = unifyResults + unifyResult
|
||||
cOld :+ typeInsertedC
|
||||
})
|
||||
unifyResults
|
||||
})
|
||||
val fc = generateFC(typedClasses)
|
||||
typedClasses =
|
||||
typedClasses.map(cl => {
|
||||
removeOverloadedSubtypeMethods(cl, fc)
|
||||
})
|
||||
typeResult.map(it => (it.flatten, typedClasses))
|
||||
}
|
||||
}
|
||||
|
@ -2,6 +2,45 @@ package hb.dhbw
|
||||
|
||||
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]){
|
||||
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) => {
|
||||
val to = solvedCons.find(_.left == x).get
|
||||
to match {
|
||||
case UnifyEqualsDot(UnifyTV(_), UnifyTV(x)) => this.sigma(UnifyTV(x))
|
||||
case UnifyEqualsDot(UnifyTV(_), UnifyRefType(n, ps)) => RefType(n, ps.map(this.sigma(_)))
|
||||
case UnifyLessDot(UnifyTV(x), UnifyRefType(n, ps)) => GenericType(x)
|
||||
}
|
||||
}
|
||||
case UnifyRefType(n, ps) => RefType(n, ps.map(sigma))
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
def delta() = {
|
||||
solvedCons.collect{
|
||||
case UnifyLessDot(UnifyTV(a), UnifyRefType(n, ps)) => LessDot(GenericType(a), RefType(n, ps.map(sigma)))
|
||||
}.toList
|
||||
}
|
||||
}
|
||||
|
||||
def applyUnifyResult(eq: Set[Set[UnifyConstraint]], into: Class) = {
|
||||
val newMethods = into.methods.flatMap(m => {
|
||||
eq.map(req => {
|
||||
val result = new UnifyResult(req)
|
||||
Method(result.delta(), result.sigma(m.retType), m.name, m.params.map(p => (result.sigma(p._1), p._2)), m.retExpr)
|
||||
})
|
||||
})
|
||||
Class(into.name, into.genericParams, into.superType, into.fields, newMethods)
|
||||
}
|
||||
|
||||
/**
|
||||
* Remove a <. b constraints
|
||||
* @param eq
|
||||
@ -32,6 +71,17 @@ object InsertTypes {
|
||||
ret ++ alessdotB.map(cons => UnifyEqualsDot(cons.left, cons.right))
|
||||
}
|
||||
|
||||
def applyResult(sigma: Map[String, Type], generics: Set[(Type, Type)], into: Class): Class = {
|
||||
def applySigma(t: Type): Type = t match{
|
||||
case RefType(n, params) => RefType(n, params.map(applySigma))
|
||||
case TypeVariable(name) => sigma(name)
|
||||
case GenericType(name) => GenericType(name)
|
||||
}
|
||||
val newMethods = into.methods.map(m => {
|
||||
Method(m.genericParams, applySigma(m.retType), m.name, m.params.map(p => (applySigma(p._1), p._2)), m.retExpr)
|
||||
})
|
||||
Class(into.name, into.genericParams, into.superType, into.fields, newMethods)
|
||||
}
|
||||
|
||||
def insert(unifyResult: Set[Set[UnifyConstraint]], into: Class): Class = {
|
||||
|
||||
|
@ -20,10 +20,9 @@ class HLJSResult extends js.Object{
|
||||
}
|
||||
|
||||
object Main {
|
||||
|
||||
def main(args: Array[String]): Unit = {
|
||||
val source = document.querySelector("#fj-input")
|
||||
update(source.textContent)
|
||||
//update(source.textContent)
|
||||
source.addEventListener("input", typecheck)
|
||||
}
|
||||
@JSExportTopLevel("typecheck")
|
||||
@ -35,19 +34,14 @@ object Main {
|
||||
}
|
||||
|
||||
def update(str: String): Unit = {
|
||||
val target = document.querySelector("#unify-output")
|
||||
val tiResult = FJTypeinference.typeinference(str)
|
||||
target.innerHTML = tiResult.fold(
|
||||
(error) => error,
|
||||
(result) => prettyPrintHTML(result._1)
|
||||
)
|
||||
val astOutput = document.querySelector("#ast-output")
|
||||
astOutput.innerHTML = tiResult.fold(
|
||||
(error) => Parser.parse(str).map( parseTree =>
|
||||
hljs.highlightAuto(prettyPrintAST(ASTBuilder.fromParseTree(parseTree))).value
|
||||
).merge,
|
||||
(result) => {
|
||||
hljs.highlightAuto(prettyPrintAST(result._2)).value
|
||||
hljs.highlightAuto(prettyPrintAST(result)).value
|
||||
}
|
||||
)
|
||||
|
||||
|
@ -52,7 +52,8 @@ object TYPE {
|
||||
|
||||
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
|
||||
LessDot(rty, method.retType) :: LessDot(method.retType, RefType("Object", List())) ::
|
||||
cons ++ method.params.map(_._1).map(LessDot(_, RefType("Object", List())))
|
||||
}
|
||||
|
||||
private def TYPEExpr(expr: Expr, localVars: List[(Type, String)], ast: List[Class]) : (Type, List[Constraint]) =expr match {
|
||||
@ -73,8 +74,9 @@ object TYPE {
|
||||
val es = params.map(ex => TYPEExpr(ex, localVars, ast))
|
||||
val methods = findMethods(name, es.size, ast)
|
||||
val consM = methods.map(m => AndConstraint(m._2.genericParams ++
|
||||
List(EqualsDot(rty, cToType(m._1)), EqualsDot(a, m._2.retType))
|
||||
List(LessDot(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))
|
||||
++ m._1.genericParams.map(it => LessDot(it._1, it._2))
|
||||
))
|
||||
val retCons = (cons ++ es.flatMap(_._2) ++ List(OrConstraint(consM)))
|
||||
(a, genericReplace.replaceGenerics(retCons))
|
||||
|
@ -35,6 +35,24 @@ object Unify {
|
||||
override def result: Set[UnifyConstraint] = eq
|
||||
}
|
||||
|
||||
def removeALessdotB(eq: Set[UnifyConstraint]): Set[UnifyConstraint] = {
|
||||
var ret = eq
|
||||
val alessdotb:Set[UnifyConstraint] = eq.filter(_ match{
|
||||
case UnifyLessDot(UnifyTV(a), UnifyTV(b)) => true
|
||||
case _ => false
|
||||
})
|
||||
ret = ret.filter(it => !alessdotb.contains(it))
|
||||
alessdotb.foreach(it => ret = subst(it.left.asInstanceOf[UnifyTV], it.right, ret))
|
||||
/*
|
||||
.filter(_ match{
|
||||
case UnifyEqualsDot(UnifyTV(a), UnifyTV(b)) => a != b
|
||||
case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => false
|
||||
case _ => true
|
||||
})
|
||||
*/
|
||||
ret ++ alessdotb.map(_ match {case UnifyLessDot(a, b) => UnifyEqualsDot(a,b)})
|
||||
}
|
||||
|
||||
def unifyIterative(orCons: Set[Set[Set[UnifyConstraint]]], fc: FiniteClosure) : Set[Set[UnifyConstraint]] = {
|
||||
def getNext[A](from: Set[CartesianProduct[A]])=
|
||||
from.find(_.hasNext()).map(it => it.nextProduct())
|
||||
@ -51,7 +69,7 @@ object Unify {
|
||||
val substResult = substStep(step2Result.nextProduct().flatten)
|
||||
substResult match{
|
||||
case UnchangedSet(eq) => if(isSolvedForm(eq)){
|
||||
results = results + eq
|
||||
results = results + removeALessdotB(eq)
|
||||
}
|
||||
case ChangedSet(eq) =>
|
||||
eqSets = eqSets + new CartesianProduct[Set[UnifyConstraint]](Set(Set(eq)))
|
||||
|
@ -6,6 +6,8 @@ class IntegrationTest extends FunSuite {
|
||||
test("EmptyClass"){
|
||||
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}")
|
||||
println(result)
|
||||
}
|
||||
|
||||
test("IdMethod"){
|
||||
@ -64,47 +66,47 @@ class IntegrationTest extends FunSuite {
|
||||
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 )
|
||||
println(result.map(it => Main.prettyPrintAST(it._2)))
|
||||
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 )
|
||||
println(result.map(it => Main.prettyPrintAST(it._2)))
|
||||
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 )
|
||||
println(result.map(it => Main.prettyPrintAST(it._2)))
|
||||
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 )
|
||||
println(result.map(it => Main.prettyPrintAST(it._2)))
|
||||
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)
|
||||
println(result.map(it => Main.prettyPrintAST(it._2)))
|
||||
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)
|
||||
println(result.map(it => Main.prettyPrintAST(it._2)))
|
||||
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)
|
||||
println(result.map(it => Main.prettyPrintAST(it._2)))
|
||||
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)
|
||||
println(result.map(it => Main.prettyPrintAST(it._2)))
|
||||
println(result.map(it => Main.prettyPrintAST(it)))
|
||||
}
|
||||
/*
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user