From ec0a294e917656a1be6d4d34d8ed1c2100d2d1f3 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Mon, 22 Feb 2016 18:23:31 +0100
Subject: [PATCH] extract synthetic copy from case classes

---
 library/collection/List.scala                    |  2 ++
 library/lang/Option.scala                        |  2 ++
 library/lang/package.scala                       |  1 +
 .../leon/frontends/scalac/ASTExtractors.scala    |  6 +++++-
 src/main/scala/leon/purescala/Definitions.scala  | 15 +++++++++++++++
 .../verification/purescala/valid/Copy.scala      | 16 ++++++++++++++++
 6 files changed, 41 insertions(+), 1 deletion(-)
 create mode 100644 src/test/resources/regression/verification/purescala/valid/Copy.scala

diff --git a/library/collection/List.scala b/library/collection/List.scala
index 74a0f0c66..8ee7c398a 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -556,9 +556,11 @@ sealed abstract class List[T] {
 }
 
 @isabelle.constructor(name = "List.list.Cons")
+@library
 case class Cons[T](h: T, t: List[T]) extends List[T]
 
 @isabelle.constructor(name = "List.list.Nil")
+@library
 case class Nil[T]() extends List[T]
 
 object List {
diff --git a/library/lang/Option.scala b/library/lang/Option.scala
index a6f09db68..04412e51b 100644
--- a/library/lang/Option.scala
+++ b/library/lang/Option.scala
@@ -78,7 +78,9 @@ sealed abstract class Option[T] {
 }
 
 @isabelle.constructor(name = "Option.option.Some")
+@library
 case class Some[T](v: T) extends Option[T]
 
 @isabelle.constructor(name = "Option.option.None")
+@library
 case class None[T]() extends Option[T]
diff --git a/library/lang/package.scala b/library/lang/package.scala
index b19ec529b..679495565 100644
--- a/library/lang/package.scala
+++ b/library/lang/package.scala
@@ -8,6 +8,7 @@ import scala.language.implicitConversions
 package object lang {
 
   implicit class BooleanDecorations(val underlying: Boolean) {
+
     @inline
     def holds : Boolean = {
       underlying
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 67e5c4502..cb0c7f96f 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -453,7 +453,11 @@ trait ASTExtractors {
           } else if (!dd.symbol.isSynthetic) {
             Some((dd.symbol, tparams.map(_.symbol), vparamss.flatten, tpt.tpe, rhs))
           } else {
-            None
+            if(name.toString == "copy" || name.toString.startsWith("copy$default$")) {
+              Some((dd.symbol, tparams.map(_.symbol), vparamss.flatten, tpt.tpe, rhs))
+            } else {
+              None
+            }
           }
         case _ => None
       }
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 8fb753d23..40091637c 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -351,6 +351,21 @@ object Definitions {
       CaseClassType(this, tps)
     }
     def typed: CaseClassType = typed(tparams.map(_.tp))
+
+    //TODO: the function works via a horrible hack, as it is not very clear where the
+    //      companion object will end up being defined.
+    //      This also return an Option as Leon compiles some non-case class (so without
+    //      copy) towards an internal case class.
+    //FIXME: it does not properly handle copy methods coming from multiple children
+    //       that got lifted to a single root class.
+    def copyDef(implicit pgm: Program): Option[FunDef] = {
+      val tryName1 = DefOps.fullName(this.root) + ".copy"
+      val tryName2 = this.root.id.name + ".copy" //generated companion object of case classes defined inside objects are currently lifted at the top level.
+      pgm.lookup(tryName1).collectFirst { case (fd: FunDef) => fd }.orElse(
+        pgm.lookup(tryName2).collectFirst { case (fd: FunDef) => fd }
+      )
+    }
+
   }
 
   /** Function/method definition.
diff --git a/src/test/resources/regression/verification/purescala/valid/Copy.scala b/src/test/resources/regression/verification/purescala/valid/Copy.scala
new file mode 100644
index 000000000..d30d403a0
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Copy.scala
@@ -0,0 +1,16 @@
+object Copy {
+
+  case class A(a: Int, b: Int)
+
+  def f(a: A): A = {
+    a.copy(b = 17)
+  } ensuring(res => res.a == a.a && res.b == 17)
+
+  def g(a: A): A = {
+    a.copy(b = 17)
+  } ensuring(res => res.a == a.a)
+
+  def h(a: A): A = {
+    a.copy(b = 17)
+  } ensuring(res => res.b == 17)
+}
-- 
GitLab