diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index 831057ebf..d34d04abb 100644 --- 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") - } - } -} +} \ No newline at end of file diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala index 066b8eb0a..159fdbf4e 100644 --- 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 index 4a5c7e4ca..5684fef86 100644 --- 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 // }