From 32ffe524b50e65e0b0350dce354e0fe431b68a1a Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Mon, 8 May 2023 16:23:53 +0200 Subject: [PATCH] fix #1025 and better inline binding origins --- src/col/vct/col/print/Namer.scala | 17 +++++++++++------ src/rewrite/vct/rewrite/InlineApplicables.scala | 17 ++++++++++++----- 2 files changed, 23 insertions(+), 11 deletions(-) diff --git a/src/col/vct/col/print/Namer.scala b/src/col/vct/col/print/Namer.scala index 8feae24bde..2d43790e85 100644 --- a/src/col/vct/col/print/Namer.scala +++ b/src/col/vct/col/print/Namer.scala @@ -10,8 +10,8 @@ case class Namer[G](syntax: Ctx.Syntax) { private val stack = ScopedStack[Node[G]]() private val names = mutable.Map[(scala.Any, String, Int), Declaration[G]]() - def nearest(f: PartialFunction[Node[G], Unit]): Option[Node[G]] = - stack.toSeq.find(n => f.isDefinedAt(n)) + def nearest(f: PartialFunction[Node[G], Unit]): Seq[Node[G]] = + stack.toSeq.filter(n => f.isDefinedAt(n)) private def nearestClass = nearest { case _: Class[G] | _: JavaClass[G] | _: VeyMontSeqProg[G] | _: JavaInterface[G] | _: JavaAnnotationInterface[G] => () @@ -73,14 +73,19 @@ case class Namer[G](syntax: Ctx.Syntax) { if (index == 0) name else s"$name$index" - def nameKeyed(key: scala.Any, decl: Declaration[G]): Unit = { + def nameKeyed(keys: Seq[scala.Any], decl: Declaration[G]): Unit = { + if(keys.isEmpty) { + // Refuse to name this declaration, it is unclear how to distinguish them. + return + } + var (baseName, index) = unpackName(decl.o.preferredName) - while(names.contains((key, baseName, index))) { + while(keys.exists(key => names.contains((key, baseName, index)))) { index += 1 } - names((key, baseName, index)) = decl + names((keys.head, baseName, index)) = decl } def name(node: Node[G]): Unit = { @@ -89,7 +94,7 @@ case class Namer[G](syntax: Ctx.Syntax) { node match { case decl: GlobalDeclaration[G] => nameKeyed(nearest { case _: Program[G] => () }, decl) case decl: ClassDeclaration[G] => nameKeyed(nearestClass, decl) - case decl: ADTDeclaration[G] => nameKeyed(if(syntax == Ctx.Silver) 3 else nearest { case _: AxiomaticDataType[G] => () }, decl) + case decl: ADTDeclaration[G] => nameKeyed(if(syntax == Ctx.Silver) Seq(3) else nearest { case _: AxiomaticDataType[G] => () }, decl) case decl: ModelDeclaration[G] => nameKeyed(nearest { case _: Model[G] => () }, decl) case decl: EnumConstant[G] => nameKeyed(nearest { case _: Enum[G] => () }, decl) case decl: Variable[G] => nameKeyed(nearestVariableScope, decl) diff --git a/src/rewrite/vct/rewrite/InlineApplicables.scala b/src/rewrite/vct/rewrite/InlineApplicables.scala index 4f84961a5d..1cdfb9a67d 100644 --- a/src/rewrite/vct/rewrite/InlineApplicables.scala +++ b/src/rewrite/vct/rewrite/InlineApplicables.scala @@ -76,6 +76,13 @@ case object InlineApplicables extends RewriterBuilder { override def inlineContext: String = s"${definition.inlineContext} [inlined from] ${usages.head.o.inlineContext}" } + case object InlineLetThisOrigin extends Origin { + override def preferredName: String = "self" + override def context: String = "[At let binding for `this`]" + override def inlineContext: String = "[Let binding for `this`]" + override def shortPosition: String = "generated" + } + case class InlineFoldAssertFailed(fold: Fold[_]) extends Blame[AssertFailed] { override def blame(error: AssertFailed): Unit = fold.blame.blame(FoldFailed(error.failure, fold)) @@ -191,26 +198,26 @@ case class InlineApplicables[Pre <: Generation]() extends Rewriter[Pre] with Laz lazy val obj = { val instanceApply = apply.asInstanceOf[InstanceApply[Pre]] val cls = classOwner(instanceApply.ref.decl) - Replacement(ThisObject[Pre](cls.ref), instanceApply.obj) + Replacement(ThisObject[Pre](cls.ref), instanceApply.obj)(InlineLetThisOrigin) } lazy val args = Replacements(for((arg, v) <- apply.args.zip(apply.ref.decl.args)) - yield Replacement(v.get, arg)) + yield Replacement(v.get, arg)(v.o)) lazy val givenArgs = Replacements(for((Ref(v), arg) <- apply.asInstanceOf[InvokingNode[Pre]].givenMap) - yield Replacement(v.get, arg)) + yield Replacement(v.get, arg)(v.o)) lazy val outArgs = { val inv = apply.asInstanceOf[AnyMethodInvocation[Pre]] Replacements(for((out, v) <- inv.outArgs.zip(inv.ref.decl.outArgs)) - yield Replacement(v.get, out)) + yield Replacement(v.get, out)(v.o)) } lazy val yields = Replacements(for((out, Ref(v)) <- apply.asInstanceOf[InvokingNode[Pre]].yields) - yield Replacement(v.get, out)) + yield Replacement(v.get, out)(v.o)) val replacements = apply.ref.decl.args.map(_.get).zip(apply.args).toMap[Expr[Pre], Expr[Pre]] // TODO: consider type arguments and out-arguments and given and yields (oof)