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

unify iterative

Browse Source
This commit is contained in:
Andreas Stadelmeier 2021-11-15 00:27:59 +01:00
parent f659ff1536
commit 8f807c6482
4 changed files with 28 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
index.html
View File

@ -3,10 +3,10 @@
<head>
<meta charset="UTF-8">
<link rel="stylesheet" type="text/css" href="index.css">
<title>Simple-sub demonstration</title>
<title>Type-inference for Featherweight Java</title>
</head>
<body>
<h1>Simple-sub demonstration</h1>
<h1>Type-inference for Featherweight Java</h1>
<div id="content">
<div id="left">
<textarea id="fj-input">
@ -25,8 +25,6 @@
</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>
<p>Credit: the CSS style sheet of this page was shamelessly stolen from <a href="https://github.com/LPTK/simple-algebraic-subtyping">the Simple-sub demo page</a>.</p>
</body>
</html>

9
src/main/scala/hb/dhbw/CartesianProduct.scala
View File

@ -6,7 +6,6 @@ class CartesianProduct[A](private val setOfSets: List[List[A]]){
var base: Long = 1
ret.sizes = ret.setOfSets.map(_.size)
ret.sizes.foreach(size => {
ret.bases = ret.bases :+ size
base = base * size
})
ret.max = base
@ -15,7 +14,6 @@ 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
@ -23,8 +21,8 @@ class CartesianProduct[A](private val setOfSets: List[List[A]]){
this(setOfSets.map(_.toList).toList)
var base: Long = 1
sizes = this.setOfSets.map(_.size)
if(sizes.size == 0) base = 0
sizes.foreach(size => {
bases = bases :+ size
base = base * size
})
max = base
@ -33,9 +31,10 @@ class CartesianProduct[A](private val setOfSets: List[List[A]]){
def hasNext() = i < max
def nextProduct() = {
val baseIt = bases.iterator
var currentI = i
val ret = setOfSets.map(set => {
val num = (i/baseIt.next())%set.size
val num = (currentI%set.size)
currentI = currentI/set.size
set(num.toInt)
})
i = i + 1

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

@ -42,7 +42,7 @@ object FJTypeinference {
ast.foldLeft(List[Class]())((cOld, c) => {
val newClassList = cOld :+ c
val typeResult = TYPE.generateConstraints(newClassList, generateFC(newClassList))
val unifyResult = Unify.unify(convertOrConstraints(typeResult._1), typeResult._2)
val unifyResult = Unify.unifyIterative(convertOrConstraints(typeResult._1), typeResult._2)
//Insert intersection types
val typeInsertedC = InsertTypes.insert(unifyResult, c)
unifyResults = unifyResults + unifyResult

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

@ -22,15 +22,28 @@ final case class AEqualsN(a: TypeVariable, n: ResultRefType) extends UnifyResult
object Unify {
def unifyIteratove(orCons: Set[Set[Set[UnifyConstraint]]], fc: FiniteClosure) : Set[Set[UnifyConstraint]] = {
var eqSets = new CartesianProduct[Set[UnifyConstraint]](orCons)
while(eqSets.hasNext()){
val eqSet = eqSets.nextProduct()
val rulesResult = applyRules(fc)(eqSet.flatten)
val step2Result = step2(rulesResult, fc)
def unifyIterative(orCons: Set[Set[Set[UnifyConstraint]]], fc: FiniteClosure) : Set[Set[UnifyConstraint]] = {
def getNext[A](from: Set[(CartesianProduct[A],Set[UnifyConstraint])])=
from.find(_._1.hasNext()).map(it => (it._1.nextProduct(), it._2))
var eqSets: Set[(CartesianProduct[Set[UnifyConstraint]],Set[UnifyConstraint])] =
Set((new CartesianProduct[Set[UnifyConstraint]](orCons), Set()))
var result: Set[UnifyConstraint] = null
var it: Option[(Set[Set[UnifyConstraint]], Set[UnifyConstraint])] = getNext(eqSets)
var results: Set[Set[UnifyConstraint]] = Set()
while(it.isDefined){
val eqSet = it.get
val rulesResult = applyRules(fc)(eqSet._1.flatten)
val step2Result = step2(rulesResult, fc)
val substResult = step2Result.map(eqSet => substStep(eqSet))
val newEqs = substResult.filter(res => res._2.isDefined).map(res => (res._1, res._2.get))
eqSets = eqSets ++ newEqs.map(it => (new CartesianProduct[Set[UnifyConstraint]](Set(Set(it._1))), eqSet._2 + it._2))
result = substResult.find(p => !p._2.isDefined && isSolvedForm(p._1)).map(it => it._1 ++ eqSet._2).getOrElse(null)
if(result != null)
results = results + result
it = getNext(eqSets)
}
Set()
results
}
def unify(orCons: Set[Set[Set[UnifyConstraint]]], fc: FiniteClosure) : Set[Set[UnifyConstraint]] = {