Skip to content

Commit a159885

Browse files
committed
frontend: handle captured function fields in IRTranslator
1 parent a7325b7 commit a159885

1 file changed

Lines changed: 61 additions & 6 deletions

File tree

frontend/shared/src/main/scala/org/sireum/lang/IRTranslator.scala

Lines changed: 61 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1147,6 +1147,33 @@ object IRTranslator {
11471147
return norm3AC(AST.IR.Exp.LocalVarRef(T, methodContext, "this", methodContext.receiverType, pos))
11481148
}
11491149

1150+
def ownerTypedName(owner: ISZ[String]): AST.Typed = {
1151+
val args: ISZ[AST.Typed] = th.typeMap.get(owner) match {
1152+
case Some(info: TypeInfo.Adt) =>
1153+
for (tp <- info.ast.typeParams) yield AST.Typed.TypeVar(tp.id.value, tp.kind)
1154+
case Some(info: TypeInfo.Sig) =>
1155+
for (tp <- info.ast.typeParams) yield AST.Typed.TypeVar(tp.id.value, tp.kind)
1156+
case _ =>
1157+
ISZ()
1158+
}
1159+
return AST.Typed.Name(owner, AST.Typed.noRType, args)
1160+
}
1161+
1162+
def liftedThiz(owner: ISZ[String], pos: message.Position): AST.IR.Exp = {
1163+
if (methodContext.isInObject) {
1164+
val thisType = ownerTypedName(owner)
1165+
return norm3AC(AST.IR.Exp.LocalVarRef(T, methodContext, "this", thisType, pos))
1166+
}
1167+
return thiz(pos)
1168+
}
1169+
1170+
def liftedThizFromReceiver(receiver: AST.Exp, owner: ISZ[String], pos: message.Position): AST.IR.Exp = {
1171+
receiver match {
1172+
case _: AST.Exp.This => return liftedThiz(owner, pos)
1173+
case _ => return translateExp(receiver)
1174+
}
1175+
}
1176+
11501177
def norm3AC(r: AST.IR.Exp): AST.IR.Exp = {
11511178
val e: AST.IR.Exp = r match {
11521179
case r: AST.IR.Exp.GlobalVarRef =>
@@ -1218,7 +1245,7 @@ object IRTranslator {
12181245
if (res.isInObject) {
12191246
return norm3AC(AST.IR.Exp.GlobalVarRef(res.owner :+ res.id, lowerByNameType(t), pos))
12201247
} else {
1221-
return norm3AC(AST.IR.Exp.FieldVarRef(thiz(pos), res.id, lowerByNameType(t), pos))
1248+
return norm3AC(AST.IR.Exp.FieldVarRef(liftedThiz(res.owner, pos), res.id, lowerByNameType(t), pos))
12221249
}
12231250
case res: AST.ResolvedInfo.EnumElement =>
12241251
return norm3AC(AST.IR.Exp.EnumElementRef(res.owner, res.name, res.ordinal, pos))
@@ -1241,7 +1268,7 @@ object IRTranslator {
12411268
return norm3AC(AST.IR.Exp.GlobalVarRef(res.owner :+ res.id, lowerByNameType(t), pos))
12421269
} else {
12431270
val receiver = exp.receiverOpt.get
1244-
val rcv = translateExp(receiver)
1271+
val rcv = liftedThizFromReceiver(receiver, res.owner, pos)
12451272
return norm3AC(AST.IR.Exp.FieldVarRef(rcv, res.id, lowerByNameType(t), pos))
12461273
}
12471274
case res: AST.ResolvedInfo.EnumElement =>
@@ -1545,6 +1572,34 @@ object IRTranslator {
15451572
}
15461573
val retType = exp.typedOpt.get
15471574
return norm3AC(AST.IR.Exp.ApplyClosure(closureVar, args, retType, pos))
1575+
case res: AST.ResolvedInfo.Var =>
1576+
// Calling a function-typed field/global variable, e.g. this.p(10) where p: T => B
1577+
val originalFunType = exp.ident.attr.typedOpt.get.asInstanceOf[AST.Typed.Fun]
1578+
val loweredFunType = lowerByNameFunType(originalFunType)
1579+
val closureVar: AST.IR.Exp =
1580+
if (res.isInObject) {
1581+
AST.IR.Exp.GlobalVarRef(res.owner :+ res.id, loweredFunType, pos)
1582+
} else {
1583+
exp.receiverOpt match {
1584+
case Some(receiver) =>
1585+
val receiverExp = liftedThizFromReceiver(receiver, res.owner, pos)
1586+
AST.IR.Exp.FieldVarRef(receiverExp, res.id, loweredFunType, pos)
1587+
case _ =>
1588+
AST.IR.Exp.FieldVarRef(liftedThiz(res.owner, pos), res.id, loweredFunType, pos)
1589+
}
1590+
}
1591+
var args = ISZ[AST.IR.Exp]()
1592+
for (i <- z"0" until exp.args.size) {
1593+
val formalT = originalFunType.args(i)
1594+
byNameValueTypeOpt(formalT) match {
1595+
case Some(_) =>
1596+
args = args :+ makeByNameClosure(exp.args(i), formalT.asInstanceOf[AST.Typed.Fun], pos)
1597+
case _ =>
1598+
args = args :+ translateExp(exp.args(i))
1599+
}
1600+
}
1601+
val retType = exp.typedOpt.get
1602+
return norm3AC(AST.IR.Exp.ApplyClosure(closureVar, args, retType, pos))
15481603
case res => halt(s"TODO: $exp (res: $res)")
15491604
}
15501605
case exp: AST.Exp.InvokeNamed =>
@@ -1658,11 +1713,11 @@ object IRTranslator {
16581713
exp.ref match {
16591714
case ref: AST.Exp.Select =>
16601715
ref.receiverOpt match {
1661-
case Some(receiver) => ISZ(translateExp(receiver))
1662-
case _ => ISZ(thiz(pos))
1716+
case Some(receiver) => ISZ(liftedThizFromReceiver(receiver, res.owner, pos))
1717+
case _ => ISZ(liftedThiz(res.owner, pos))
16631718
}
1664-
case _: AST.Exp.Ident => ISZ(thiz(pos))
1665-
case _ => ISZ(thiz(pos))
1719+
case _: AST.Exp.Ident => ISZ(liftedThiz(res.owner, pos))
1720+
case _ => ISZ(liftedThiz(res.owner, pos))
16661721
}
16671722
}
16681723
return norm3AC(AST.IR.Exp.ClosureRef(

0 commit comments

Comments
 (0)