Remove parentheses in GenC for dropped val's

epfl-lara · Jul 28, 2021 · c479ca6 · c479ca6
1 parent b6bec40
commit c479ca6
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 4 deletions.
diff --git a/core/src/main/scala/stainless/genc/ir/IR.scala b/core/src/main/scala/stainless/genc/ir/IR.scala
@@ -51,7 +51,7 @@ private[genc] sealed trait IR { ir =>
   // Define a function body as either a regular AST or a manually defined
   // function using @cCode.function
   sealed abstract class FunBody
-  case object FunDropped extends FunBody // for @cCode.drop
+  case class FunDropped(isAccessor: Boolean) extends FunBody // for @cCode.drop; `isAccessor` is true for `val`'s to avoid parentheses
   case class FunBodyAST(body: Expr) extends FunBody
   case class FunBodyManual(includes: Seq[String], body: String) extends FunBody // NOTE `body` is actually the whole function!
 

diff --git a/core/src/main/scala/stainless/genc/ir/Transformer.scala b/core/src/main/scala/stainless/genc/ir/Transformer.scala
@@ -77,7 +77,7 @@ abstract class Transformer[From <: IR, To <: IR](final val from: From, final val
   }
 
   protected def rec(fb: FunBody)(implicit env: Env): to.FunBody = (fb: @unchecked) match {
-    case FunDropped => to.FunDropped
+    case FunDropped(isAccessor) => to.FunDropped(isAccessor)
     case FunBodyAST(body) => to.FunBodyAST(rec(body))
     case FunBodyManual(includes, body) => to.FunBodyManual(includes, body)
   }

diff --git a/core/src/main/scala/stainless/genc/phases/IR2CPhase.scala b/core/src/main/scala/stainless/genc/phases/IR2CPhase.scala
@@ -99,7 +99,7 @@ private class IR2CImpl(val ctx: inox.Context) {
       includes foreach { i => register(C.Include(i)) }
       Right(body)
 
-    case FunDropped => Right("")
+    case FunDropped(_) => Right("")
   }
 
   private def rec(cd: ClassDef): Unit = {
@@ -225,6 +225,8 @@ private class IR2CImpl(val ctx: inox.Context) {
 
     case Decl(vd, Some(value)) => C.Decl(rec(vd.id), rec(vd.getType), Some(rec(value)))
 
+    case App(FunVal(fd), Seq(), Seq()) if fd.body == FunDropped(true) => C.Binding(rec(fd.id))
+
     case App(callable, extra, args) => C.Call(rec(callable), (extra ++ args).map(rec(_)))
 
     case Construct(cd, args) => constructObject(cd, args) // can be a StructInit or an EnumLiteral

diff --git a/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala b/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala
@@ -512,7 +512,7 @@ private class S2IRImpl(val context: inox.Context, val ctxDB: FunCtxDB, val deps:
         val impl = fa.getManualDefinition
         CIR.FunBodyManual(impl.includes, impl.code)
       } else if (fa.isDropped) {
-        CIR.FunDropped
+        CIR.FunDropped(fa.flags.exists(_.name == "accessor"))
       } else {
         // Build the new environment from context and parameters
         val ctxKeys: Seq[(ValDef, Type)] = ctxDBAbs map { c => c.vd -> instantiateType(c.typ, tm1) }