stan/FeatherweightTypeInference
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Change type insert to non-filtered method

Browse Source
This commit is contained in:
Andreas Stadelmeier 2022-03-17 02:52:05 +01:00
parent 573e91b6a3
commit 3cb0973a71
6 changed files with 57 additions and 62 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
index.html
View File

@ -18,11 +18,8 @@
<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-fastopt/main.js"></script>
<script type="text/javascript" src="target/scala-2.13/fj-typeinference-opt/main.js"></script>
<br/>
<p>Credit: the layout of this page was shamelessly stolen from <a href="https://github.com/LPTK/simple-algebraic-subtyping">the Simple-sub demo page</a>.</p>
</body>

35
src/main/scala/hb/dhbw/FJTypeinference.scala
View File

@ -83,46 +83,21 @@ object FJTypeinference {
case UnifyTV(a) => sigma(a)
}
def typeinference(str: String): Either[String, (Set[Set[UnifyConstraint]], List[Class])] = {
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)
// Unify step 6:
val genericNames = c.genericParams.map(_._1).map(_ match{case GenericType(x) => x})
val sigma = unifyResult.map(result => {
val lessdotSigma = result.filter(_ match {
case UnifyLessDot(UnifyTV(a), _) => true
case _ => false
}).map(_ match{
case UnifyLessDot(UnifyTV(a), UnifyRefType(n, _)) =>
if (genericNames.find(_ == n).isDefined) (a -> GenericType(n)) else (a -> GenericType(a))
}).toMap[String, Type]
val eqDotSigma = result.map(_ match{
case UnifyEqualsDot(UnifyTV(a), toRefType) => (a -> sigmaReplace(lessdotSigma, toRefType))
case UnifyLessDot(UnifyTV(a), UnifyRefType(n, p)) => (a -> GenericType(a))
}).toMap
//merge the two maps:
lessdotSigma ++ eqDotSigma
}).toList.head
val generics:Set[(Type, Type)] = Set()
//Insert intersection types
val typeInsertedC = InsertTypes.applyResult(sigma, generics, c)//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))
}
}

39
src/main/scala/hb/dhbw/InsertTypes.scala
View File

@ -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

10
src/main/scala/hb/dhbw/Main.scala
View File

@ -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
}
)

12
src/main/scala/hb/dhbw/Unify.scala
View File

@ -20,18 +20,6 @@ final case class AEqualsB(a: TypeVariable, b: TypeVariable) extends UnifyResultC
final case class AEqualsN(a: TypeVariable, n: ResultRefType) extends UnifyResultConstraint
*/
class UnifyResult(solvedCons: Set[UnifyConstraint]){
def sigma(x: UnifyType): UnifyType = {
assert(x.isInstanceOf[UnifyTV])
val to = solvedCons.find(_.left == x).get
to match {
case UnifyEqualsDot(_, UnifyTV(x)) => this.sigma(UnifyTV(x))
case UnifyEqualsDot(_, UnifyRefType(n, ps)) => UnifyRefType(n, ps.map(this.sigma(_)))
case UnifyLessDot(UnifyTV(x), UnifyRefType(n, ps)) => UnifyTV(x)
}
}
}
object Unify {
sealed trait Step4Result{

18
src/test/scala/IntegrationTest.scala
View File

@ -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)))
}
/*