From d55013f84e250a477b5ae2794832a68a14011175 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 18 Aug 2014 18:41:17 +0200
Subject: [PATCH] Fix choose not returning a stable type, add constructor to
 help

---
 .../scala/leon/purescala/Constructors.scala   |  8 ++++++++
 .../scala/leon/synthesis/ConvertHoles.scala   |  2 +-
 .../leon/synthesis/ConvertWithOracles.scala   |  2 +-
 .../regression/synthesis/Holes/Hole1.scala    | 20 -------------------
 4 files changed, 10 insertions(+), 22 deletions(-)

diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index d02804e45..6aeda471b 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -24,4 +24,12 @@ object Constructors {
     case xs =>
       LetTuple(xs, value, body)
   }
+
+  def tupleChoose(ch: Choose): Expr = {
+    if (ch.vars.size > 1) {
+      ch
+    } else {
+      Tuple(Seq(ch))
+    }
+  }
 }
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
index be878918a..55e3e685d 100644
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -63,7 +63,7 @@ object ConvertHoles extends LeonPhase[Program, Program] {
               BooleanLiteral(true)
           }
 
-          val withChoose = letTuple(holes, Choose(cids, pred), newBody)
+          val withChoose = letTuple(holes, tupleChoose(Choose(cids, pred)), newBody)
 
           fd.body = Some(withChoose)
         }
diff --git a/src/main/scala/leon/synthesis/ConvertWithOracles.scala b/src/main/scala/leon/synthesis/ConvertWithOracles.scala
index f8072b71a..0d7948e41 100644
--- a/src/main/scala/leon/synthesis/ConvertWithOracles.scala
+++ b/src/main/scala/leon/synthesis/ConvertWithOracles.scala
@@ -54,7 +54,7 @@ object ConvertWithOracle extends LeonPhase[Program, Program] {
                     BooleanLiteral(true)
                 }
 
-                Some(letTuple(os, Choose(chooseOs, pred), b))
+                Some(letTuple(os, tupleChoose(Choose(chooseOs, pred)), b))
               case None =>
                 None
             }
diff --git a/src/test/resources/regression/synthesis/Holes/Hole1.scala b/src/test/resources/regression/synthesis/Holes/Hole1.scala
index 785271b22..65ff08381 100644
--- a/src/test/resources/regression/synthesis/Holes/Hole1.scala
+++ b/src/test/resources/regression/synthesis/Holes/Hole1.scala
@@ -3,26 +3,6 @@ import leon.collection._
 import leon.lang.synthesis._
 
 object Holes {
-  def abs1(a: Int) = {
-    if (?(true, false)) {
-      a
-    } else {
-      -a
-    }
-  } ensuring {
-    _ >= 0
-  }
-
-  def abs2(a: Int) = {
-    if (???[Boolean]) {
-      a
-    } else {
-      -a
-    }
-  } ensuring {
-    _ >= 0
-  }
-
   def abs3(a: Int) = {
     if (?(a > 0, a < 0)) {
       a
-- 
GitLab