slightly cleaner work-around #581

viperproject · May 27, 2022 · 2fe26fb · 2fe26fb
1 parent f6fbefa
commit 2fe26fb
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 41 deletions.
diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala
@@ -463,6 +463,7 @@ case class PDestructorCall(name: String, rcv: PExp)
   override def args: Seq[PExp] = Seq(rcv)
 
   override def translateExp(t: Translator): Exp = {
+    val actualRcv = t.exp(rcv)
     val so: Option[Map[TypeVar, Type]] = adtSubstitution match {
       case Some(ps) => Some(ps.m.map(kv => TypeVar(kv._1) -> t.ttyp(kv._2)))
       case None => None
@@ -471,10 +472,6 @@ case class PDestructorCall(name: String, rcv: PExp)
       case Some(s) =>
         val adt = t.getMembers()(this.adt.idndef.name).asInstanceOf[Adt]
         assert(s.keys.toSet == adt.typVars.toSet)
-        val actualRcv = rcv match {
-          case pr@PResultLit() => Result(AdtType(adt, s))(t.liftPos(pr))
-          case _ => t.exp(rcv)
-        }
         AdtDestructorApp(adt, name, actualRcv, s)(t.liftPos(this))
       case _ => sys.error("type unification error - should report and not crash")
     }
@@ -499,6 +496,7 @@ case class PDiscriminatorCall(name: PIdnUse, rcv: PExp)
   override def args: Seq[PExp] = Seq(rcv)
 
   override def translateExp(t: Translator): Exp = {
+    val actualRcv = t.exp(rcv)
     val so: Option[Map[TypeVar, Type]] = adtSubstitution match {
       case Some(ps) => Some(ps.m.map(kv => TypeVar(kv._1) -> t.ttyp(kv._2)))
       case None => None
@@ -507,34 +505,8 @@ case class PDiscriminatorCall(name: PIdnUse, rcv: PExp)
       case Some(s) =>
         val adt = t.getMembers()(this.adt.idndef.name).asInstanceOf[Adt]
         assert(s.keys.toSet == adt.typVars.toSet)
-        val actualRcv = rcv match {
-          case pr@PResultLit() => Result(AdtType(adt, s))(t.liftPos(pr))
-          case _ => t.exp(rcv)
-        }
         AdtDiscriminatorApp(adt, name.name, actualRcv, s)(t.liftPos(this))
       case _ => sys.error("type unification error - should report and not crash")
     }
   }
-}
-
-case class PAdtResultLit(adt: PIdnUse, args: Seq[PType])(val pos: (Position, Position)) extends PExtender with PExp {
-  // These two function must be mandatorily extended due to semantic analysis rules
-  override final val typeSubstitutions = Seq(PTypeSubstitution.id)
-  override def forceSubstitution(ts: PTypeSubstitution) = {}
-
-  override def getSubnodes(): Seq[PNode] = Seq(adt) ++ args
-
-  // The typecheck funtion for PAst node corresponding to the expression
-  override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = None
-
-  // The translator function to translate the PAst node corresponding to the Ast node
-  override def translateExp(t: Translator): Exp = {
-    t.getMembers().get(adt.name) match {
-      case Some(d) =>
-        val adt = d.asInstanceOf[Adt]
-        val typVarMapping = adt.typVars zip (args map t.ttyp)
-        Result(AdtType(adt, typVarMapping.toMap))(t.liftPos(this))
-      case None => sys.error("undeclared adt type")
-    }
-  }
-}
+}
diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
@@ -120,15 +120,19 @@ class AdtPlugin(reporter: viper.silver.reporter.Reporter,
       case pfa@PFieldAccess(rcv, idnuse) if declaredConstructorArgsNames.exists(_.name == idnuse.name) => PDestructorCall(idnuse.name, rcv)(pfa.pos)
       case pfa@PFieldAccess(rcv, idnuse) if declaredConstructorNames.exists("is" + _.name == idnuse.name) => PDiscriminatorCall(PIdnUse(idnuse.name.substring(2))(idnuse.pos), rcv)(pfa.pos)
       case pr@PResultLit() => {
-        var parent = pr.parent.get
-        while (!parent.isInstanceOf[PFunction] && !parent.isInstanceOf[PFieldAccess] && !parent.isInstanceOf[PDestructorCall] && !parent.isInstanceOf[PDiscriminatorCall]) {
-          if (parent == null) sys.error("cannot use 'result' outside of function")
-          parent = parent.parent.get
-        }
-        parent match {
-          case pf@PFunction(_, _, typ@PDomainType(idnuse, args), _, _, _) if declaredAdtNames.exists(_.name == idnuse.name) => PAdtResultLit(idnuse, args)(pr.pos)
-          case _ => pr
+        // The transformations applied to the return type of the parent `PFunction` are not known to the `PResultLit`.
+        // This is hack to make the return type known despite that, see https://github.com/viperproject/silver/issues/581.
+        var par: PNode = pr.parent.get
+        while (!par.isInstanceOf[PFunction]) {
+          if (par == null) sys.error("cannot use 'result' outside of function")
+          val nextpar = par.parent.get
+          if (nextpar.isInstanceOf[PFunction]) {
+            val func = nextpar.asInstanceOf[PFunction]
+            par.parent = Some(func.copy(typ = transformStrategy(func.typ))(func.pos))
+          }
+          par = par.parent.get
         }
+        pr
       }
     }).recurseFunc({
       // Stop the recursion if a destructor call or discriminator call is parsed as left-hand side of a field assignment

diff --git a/src/test/resources/adt/issue-581.vpr b/src/test/resources/adt/issue-581.vpr
@@ -22,10 +22,10 @@ function inv(t: Test): Bool {
 }
 
 // FIXME: this triggers an error: [typechecker.error] expected identifier, but got PAdtConstructor(PIdnDef(A),List())
-// FIXME: see https://github.com/viperproject/silver/issues/581
+// FIXME: due to `PBinExp` losing its information about `parent`, see https://github.com/viperproject/silver/issues/581
 // function baz(): Test
 //     ensures A() == result
-//     // ensures result == A()
+//     ensures result == A()
 // {
 //     A
 // }