From 8f807c6482ac378bdcb34fffd5783aea0b95d2f3 Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Mon, 15 Nov 2021 00:27:59 +0100
Subject: [PATCH] unify iterative

---
 index.html                                    |  8 +++---
 src/main/scala/hb/dhbw/CartesianProduct.scala |  9 +++----
 src/main/scala/hb/dhbw/FJTypeinference.scala  |  2 +-
 src/main/scala/hb/dhbw/Unify.scala            | 27 ++++++++++++++-----
 4 files changed, 28 insertions(+), 18 deletions(-)
diff --git a/index.html b/index.html
index cea856d..6527dd1 100644
--- a/index.html
+++ b/index.html
@@ -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>
diff --git a/src/main/scala/hb/dhbw/CartesianProduct.scala b/src/main/scala/hb/dhbw/CartesianProduct.scala
index 798c87a..b075424 100644
--- a/src/main/scala/hb/dhbw/CartesianProduct.scala
+++ b/src/main/scala/hb/dhbw/CartesianProduct.scala
@@ -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
diff --git a/src/main/scala/hb/dhbw/FJTypeinference.scala b/src/main/scala/hb/dhbw/FJTypeinference.scala
index 3a9f823..818ab31 100644
--- a/src/main/scala/hb/dhbw/FJTypeinference.scala
+++ b/src/main/scala/hb/dhbw/FJTypeinference.scala
@@ -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
diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala
index da71241..5cb0ab9 100644
--- a/src/main/scala/hb/dhbw/Unify.scala
+++ b/src/main/scala/hb/dhbw/Unify.scala
@@ -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]] = {
