Unfinished backup

This commit is contained in:
JanUlrich 2022-03-10 14:24:17 +01:00
parent b5083ba46a
commit be7ccf8265
4 changed files with 44 additions and 3 deletions

View File

@ -78,6 +78,11 @@ object FJTypeinference {
Class(in.name, in.genericParams, in.superType, in.fields, newMethods.toList)
}
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, (Set[Set[UnifyConstraint]], List[Class])] = {
val ast = Parser.parse(str).map(ASTBuilder.fromParseTree(_))
var typedClasses: List[Class] = List()
@ -87,8 +92,26 @@ object FJTypeinference {
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.insert(unifyResult, c)
val typeInsertedC = InsertTypes.applyResult(sigma, generics, c)//InsertTypes.insert(unifyResult, c)
typedClasses = typedClasses :+ typeInsertedC
unifyResults = unifyResults + unifyResult
cOld :+ typeInsertedC

View File

@ -32,6 +32,9 @@ object InsertTypes {
ret ++ alessdotB.map(cons => UnifyEqualsDot(cons.left, cons.right))
}
def applyResult(sigma: Map[String, Type], generics: Set[(Type, Type)], into: Class): Class = {
//TODO
}
def insert(unifyResult: Set[Set[UnifyConstraint]], into: Class): Class = {

View File

@ -73,8 +73,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))

View File

@ -35,6 +35,20 @@ object Unify {
override def result: Set[UnifyConstraint] = eq
}
def removeALessdotB(eq: Set[UnifyConstraint]): Set[UnifyConstraint] = {
var ret = eq
val alessdotb = eq.filter(_ match{
case UnifyLessDot(UnifyTV(a), UnifyTV(b)) => true
case _ => false
})
alessdotb.foreach(it => ret = subst(it.left.asInstanceOf[UnifyTV], it.right, ret))
ret.filter(_ match{
case UnifyEqualsDot(UnifyTV(a), UnifyTV(b)) => a != b
case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => false
case _ => true
}) ++ 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 +65,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)))