From 7424ec4289006f0f3ce9b506b965fe9245fcf2c8 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Mon, 5 Feb 2024 14:56:16 +0100 Subject: [PATCH] INitial commit. Work in Progress --- .gitignore | 32 +++ README.md | 8 + build.sbt | 12 + project/build.properties | 1 + src/main/scala/Main.scala | 5 + src/main/scala/unify/algorithm/Rules.scala | 22 ++ src/main/scala/unify/model/Constraint.scala | 12 + .../scala/unify/model/ConstraintSet.scala | 249 ++++++++++++++++++ src/main/scala/unify/model/Type.scala | 24 ++ .../unify/model/WildcardEnvironment.scala | 12 + src/test/scala/MySuite.scala | 9 + 11 files changed, 386 insertions(+) create mode 100644 .gitignore create mode 100644 README.md create mode 100644 build.sbt create mode 100644 project/build.properties create mode 100644 src/main/scala/Main.scala create mode 100644 src/main/scala/unify/algorithm/Rules.scala create mode 100644 src/main/scala/unify/model/Constraint.scala create mode 100644 src/main/scala/unify/model/ConstraintSet.scala create mode 100644 src/main/scala/unify/model/Type.scala create mode 100644 src/main/scala/unify/model/WildcardEnvironment.scala create mode 100644 src/test/scala/MySuite.scala diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..9e79245 --- /dev/null +++ b/.gitignore @@ -0,0 +1,32 @@ +# macOS +.DS_Store + +# sbt specific +dist/* +target/ +lib_managed/ +src_managed/ +project/boot/ +project/plugins/project/ +project/local-plugins.sbt +.history +.ensime +.ensime_cache/ +.sbt-scripted/ +local.sbt + +# Bloop +.bsp + +# VS Code +.vscode/ + +# Metals +.bloop/ +.metals/ +metals.sbt + +# IDEA +.idea +.idea_modules +/.worksheet/ diff --git a/README.md b/README.md new file mode 100644 index 0000000..102c5ca --- /dev/null +++ b/README.md @@ -0,0 +1,8 @@ +## sbt project compiled with Scala 3 + +### Usage + +This is a normal sbt project. You can compile code with `sbt compile`, run it with `sbt run`, and `sbt console` will start a Scala 3 REPL. + +For more information on the sbt-dotty plugin, see the +[scala3-example-project](https://github.com/scala/scala3-example-project/blob/main/README.md). diff --git a/build.sbt b/build.sbt new file mode 100644 index 0000000..24d5cb6 --- /dev/null +++ b/build.sbt @@ -0,0 +1,12 @@ +val scala3Version = "3.3.1" + +lazy val root = project + .in(file(".")) + .settings( + name := "WildFJ-TI", + version := "0.1.0-SNAPSHOT", + + scalaVersion := scala3Version, + + libraryDependencies += "org.scalameta" %% "munit" % "0.7.29" % Test + ) diff --git a/project/build.properties b/project/build.properties new file mode 100644 index 0000000..abbbce5 --- /dev/null +++ b/project/build.properties @@ -0,0 +1 @@ +sbt.version=1.9.8 diff --git a/src/main/scala/Main.scala b/src/main/scala/Main.scala new file mode 100644 index 0000000..bd01e94 --- /dev/null +++ b/src/main/scala/Main.scala @@ -0,0 +1,5 @@ +@main def hello(): Unit = + println("Hello world!") + println(msg) + +def msg = "I was compiled by Scala 3. :)" diff --git a/src/main/scala/unify/algorithm/Rules.scala b/src/main/scala/unify/algorithm/Rules.scala new file mode 100644 index 0000000..5418a02 --- /dev/null +++ b/src/main/scala/unify/algorithm/Rules.scala @@ -0,0 +1,22 @@ +package unify.algorithm + +import unify.model.LessDot + +object Rules { + private def adaptRule(cons: LessDot, cs: ConstraintSet, fc: FiniteClosure) = { + def paramSubst(param: Type, paramMap: Map[Type, Type]): Type = param match { + case RefType(w, n, params) => RefType(w, n, params.map(paramSubst(_, paramMap))) + case typeVariable => paramMap.get(typeVariable).get + } + + val left = cons.left.asInstanceOf[RefType] + val right = cons.right.asInstanceOf[RefType] + if (fc.isPossibleSupertype(left.name, right.name)) { + val subtypeRelation = fc.supertype(left.name) // C <. D + val paramMap = subtypeRelation._1.params.zip(left.params).toMap + val newParams = subtypeRelation._2.params.map(paramSubst(_, paramMap)) + cs.remove(cons) + cs.add(LessDot(RefType(left.wildcards, right.name, newParams), right)) + } + } +} diff --git a/src/main/scala/unify/model/Constraint.scala b/src/main/scala/unify/model/Constraint.scala new file mode 100644 index 0000000..a2e6bc4 --- /dev/null +++ b/src/main/scala/unify/model/Constraint.scala @@ -0,0 +1,12 @@ +package unify.model + +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){ + override def toString: String = left.toString + " <. " + right.toString +} +final case class LessDotCC(override val left: Type, override val right: Type) extends Constraint(left, right){ + override def toString: String = left.toString + " !params.find(tvInType).isEmpty + case x => x.equals(tv) + } + val alessdotT : Set[Constraint] = getLessDotCons.filter(cons => cons.left.equals(tv) && !tvInType(cons.right)).toSet + val tvIsOnlyInAlessdotTCons = getAllConstraints.filter(!alessdotT.contains(_)).find(cons => tvInType(cons.left) || tvInType(cons.right)).isEmpty + bounds.map(_._2._2).toSet.contains(tv) && tvIsOnlyInAlessdotTCons && !bounds.map(_._2._1).toSet.contains(tv) + } + + /** + * ground rule. removes all a <. T constraints in cons and sets a to bottom type + */ + def groundRule(cons: LessDot) = { + this.remove(cons) + this.addUnifier(EqualsDot(cons.left, BotType())) + this.bounds = this.bounds.map(bound => if(bound._2._2.equals(cons.left)) { + (bound._1 -> (bound._2._1, BotType())) + } else bound) + } + + def tvs(t: Type) : Set[TypeVariable] = t match { + case TypeVariable(a) => Set(TypeVariable(a)) + case RefType(wildcards, name, params) => params.flatMap(tvs).toSet + case _ => Set() + } + def fv(t: Type) : Set[Type] = t match { + case TypeVariable(a) => Set() + case WTypeVariable(a) => Set(WTypeVariable(a)) + case RefType(wc, _, ps) => { + ps.map(fv).flatten.filter(t => !wc.contains(t)).toSet + } + case Wildcard(w) => Set(Wildcard(w)) + } + + /** + * Method removes all wildcard type variables a? from the constraint set + * and replaces them with normal type variables a + */ + def trimWTVs() = { + def trimWTV(t: Type): Type = t match { + case WTypeVariable(n) => { + changed = true + TypeVariable(n) + } + case RefType(ws, n, ps) => RefType(ws.map(trimWTV).asInstanceOf[List[Wildcard]], n, ps.map(trimWTV)) + case Wildcard(name) => { + Wildcard(name) + } + case x => x + } + unifier = unifier.map(c => EqualsDot(trimWTV(c.left), trimWTV(c.right))) + lessdot = lessdot.map(c => LessDot(trimWTV(c.left), trimWTV(c.right))) + equalsdot = equalsdot.map(c => EqualsDot(trimWTV(c.left), trimWTV(c.right))) + bounds = bounds.map(b => b._1 -> (trimWTV(b._2._1), trimWTV(b._2._2))) + } + + def generateFreeWildcard(wc: Wildcard, tvFactory: TypeVariableFactory): Wildcard = { + val freshWC = Wildcard(tvFactory.freshName()) + bounds.put(freshWC, bounds(wc)) + freshWC + } + + def freshWildcard(tvFactory: TypeVariableFactory, wcFactory: WildcardFactory): Wildcard = { + val newWC = Wildcard(wcFactory.freshName()) + bounds.put(newWC,(tvFactory.freshTV(),tvFactory.freshTV())) + newWC + } + + /** + * checks if from <.* to + * + * @return + */ + def isLinked(from: TypeVariable, to: TypeVariable): Boolean = { + var searchNext = Set(from) + var visited: Set[TypeVariable] = Set() + do { + searchNext --= visited + searchNext = searchNext.flatMap(tv => { + visited = visited + tv + this.getALessDotBCons.filter(c => c.left.equals(tv)).map(c => c.right.asInstanceOf[TypeVariable]) + }) + if (searchNext.contains(to)) return true + } while (searchNext.nonEmpty) + false + } + + def notProcessed(a: TypeVariable, b: TypeVariable): Boolean = !processed.contains((a,b)) + + def hasChanged(): Boolean = { + val ret = changed + changed = false + ret + } + + def setProcessedByAdopt(a: TypeVariable, b: TypeVariable): Unit = { + processed = processed + ((a,b)) + } + + /** + * Also returns unifier a =. T and all other constraints a <. T, a <. b + * @return + */ + private def getAllConstraints: Set[Constraint] = Set[Constraint]() ++ lessdot ++ equalsdot ++ unifier + def getLessDotCons: List[LessDot] = lessdot + + def getEqualsDotCons: Set[EqualsDot] = equalsdot + + def getALessDotBCons: Set[LessDot] = lessdot.filter(c => c.left.isInstanceOf[TypeVariable] && c.right.isInstanceOf[TypeVariable]).toSet + + def getALessDotCCons() = getLessDotCons.filter(c => c match { + case LessDot(TypeVariable(_), RefType(_, _, _)) => true + case _ => false + }) + + def addUnifier(c: EqualsDot) = { + changed = true + unifier = unifier + c + } + + def copy(): ConstraintSet = { + val ret = ConstraintSet() + ret.processed = processed + ret.lessdot = lessdot + ret.equalsdot = equalsdot + ret.unifier = unifier + ret.bounds ++= bounds + ret + } + + def substitute(withType: Type, toSubstitute: Type): Unit = { + def substitute(inType: Type): Type = if(inType.equals(toSubstitute)) { + withType + } else {inType match { + case RefType(wildcards, name, params) => RefType(wildcards.map(substitute).map(_.asInstanceOf[Wildcard]), name, params.map(substitute)) + case t => t + } + } + getEqualsDotCons.foreach(c => { + val subst = EqualsDot(substitute(c.left), substitute(c.right)) + if(! c.equals(subst)){ + remove(c) + add(subst) + } + }) + lessdot = getLessDotCons.map(c => { + LessDot(substitute(c.left), substitute(c.right)) + }) + unifier = unifier.map(c => { + EqualsDot(substitute(c.left), substitute(c.right)) + }) + this.bounds = this.bounds.map(wc => wc._1 -> (substitute(wc._2._1), substitute(wc._2._2))) + } + + def addAll(value: Iterable[Constraint]) = value.map(add) + + def add(cons: Constraint): Unit = { + cons match { + case EqualsDot(l,r) => equalsdot += (EqualsDot(l,r)) + case LessDot(TypeVariable(a), TypeVariable(b)) => { + lessdot ::= (LessDot(TypeVariable(a), TypeVariable(b))) + } + case LessDot(l,r) => lessdot ::= (LessDot(l,r)) + } + changed = true + } + + def remove(cons: Constraint): Unit = { + cons match { + case EqualsDot(l, r) => { + equalsdot -= (EqualsDot(l, r)) + } + case LessDot(TypeVariable(a), TypeVariable(b)) => { + lessdot = lessdot.diff(List(LessDot(TypeVariable(a), TypeVariable(b)))) + } + case LessDot(l, r) => lessdot = lessdot.diff(List(LessDot(l, r))) + } + changed = true + } + def removeAll(cons: List[Constraint]): Unit = cons.foreach(remove) + + private def isSolvedConstraint(c :Constraint) = c match { + case LessDot(TypeVariable(_), RefType(wc, n, ps)) => + fv(RefType(wc, n, ps)).isEmpty + case EqualsDot(TypeVariable(a), RefType(wc, n, ps)) => + !tvs(RefType(wc, n, ps)).contains(TypeVariable(a)) + case EqualsDot(TypeVariable(a), TypeVariable(b)) => true + case _ => false + } + def isSolvedForm: Boolean = getEqualsDotCons.isEmpty && + getLessDotCons.map(isSolvedConstraint).reduceOption((a,b) => a && b).getOrElse(true) && + getAllConstraints.map(_.left).size == getAllConstraints.size //No TV is double on the left side + //unifier.map(isSolvedConstraint).reduceOption((a,b) => a && b).getOrElse(true) + + def solvedForm(): Option[UnifySolution] = { + var sigma = Map[TypeVariable, Type]() + var delta: Map[Wildcard, (Type, Type)] = Map() + + //GenDelta + do{ + val toRemove = getLessDotCons.filter(c => tvs(c.right).isEmpty).map(c => { + val B = Wildcard("X"+c.left.asInstanceOf[TypeVariable].name) + sigma = sigma + (c.left.asInstanceOf[TypeVariable] -> B) + delta = delta + (B -> (c.right, BotType())) + c + }) + this.removeAll(toRemove) + //Do the substitution afterwards: + sigma.map(c => substitute(c._2, c._1)) + }while(hasChanged()) + + //AddDelta + this.bounds.filter(wc => tvs(wc._2._1).isEmpty && tvs(wc._2._2).isEmpty).map(wc =>{ + delta = delta + (wc._1 -> wc._2) + }) + if(this.bounds.filterNot(wc => tvs(wc._2._1).isEmpty && tvs(wc._2._2).isEmpty).nonEmpty)return None + + //GenSigma + val toRemove = unifier.filter(c => tvs(c.right).isEmpty).map(c => { + sigma = sigma + (c.left.asInstanceOf[TypeVariable] -> c.right) + c + }) + this.unifier = this.unifier.filterNot(toRemove.contains(_)) + + if(this.getAllConstraints.isEmpty){ + val ret = new UnifySolution(delta, sigma) + Some(ret) + }else{ + None + } + } +} diff --git a/src/main/scala/unify/model/Type.scala b/src/main/scala/unify/model/Type.scala new file mode 100644 index 0000000..1e2483f --- /dev/null +++ b/src/main/scala/unify/model/Type.scala @@ -0,0 +1,24 @@ +package unify.model + +sealed abstract class Type + +final case class RefType(wildcards: WildcardEnvironment, name: String, params: List[Type]) extends Type{ + override def toString: String = { + var ret = "" + ret += wildcards.toString + ret += name + if(!params.isEmpty) ret += params.mkString( "<", ", ", ">") + ret + } +} + +final case class BotType() extends Type {} +final case class TypeVariable(name: String) extends Type{ + override def toString: String = name +} +final case class Wildcard(name: String) extends Type { + override def toString: String = name // + "^" + upperBound.toString + "_" + lowerBound.toString +} +final case class WTypeVariable(name: String) extends Type { + override def toString: String = name + "?" +} \ No newline at end of file diff --git a/src/main/scala/unify/model/WildcardEnvironment.scala b/src/main/scala/unify/model/WildcardEnvironment.scala new file mode 100644 index 0000000..9b05c98 --- /dev/null +++ b/src/main/scala/unify/model/WildcardEnvironment.scala @@ -0,0 +1,12 @@ +package unify.model + +case class WildcardBounds(name: String, upper: Type, lower: Type){} +class WildcardEnvironment(wcBounds: Set[WildcardBounds]) { + val bounds: Map[String, (Type, Type)] = wcBounds.map(b => (b.name -> (b.upper, b.lower))).toMap + + def getUpperBound(wc: Wildcard): Type = bounds(wc.name)._1 + + def getLowerBound(wc: Wildcard): Type = bounds(wc.name)._2 + + override def toString: String = bounds.map(_._1).mkString("", ",", ".") +} diff --git a/src/test/scala/MySuite.scala b/src/test/scala/MySuite.scala new file mode 100644 index 0000000..621784d --- /dev/null +++ b/src/test/scala/MySuite.scala @@ -0,0 +1,9 @@ +// For more information on writing tests, see +// https://scalameta.org/munit/docs/getting-started.html +class MySuite extends munit.FunSuite { + test("example test that succeeds") { + val obtained = 42 + val expected = 42 + assertEquals(obtained, expected) + } +}