From 300576df9121c194831c6816a1022a2b1980eb3e Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 19 Oct 2012 17:42:44 +0200
Subject: [PATCH] Implement Choose here and there, not complete yet but should
 be mostly functional

---
 src/main/scala/leon/ArrayTransformation.scala |  5 ++++
 .../scala/leon/plugin/CodeExtraction.scala    | 17 ++++++++++++++
 src/main/scala/leon/plugin/Extractors.scala   | 15 ++++++++++++
 .../scala/leon/purescala/PrettyPrinter.scala  |  8 +++++++
 src/main/scala/leon/purescala/Trees.scala     | 23 +++++++++++++++++++
 5 files changed, 68 insertions(+)

diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
index 7d0d94458..38f1fce44 100644
--- a/src/main/scala/leon/ArrayTransformation.scala
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -98,6 +98,11 @@ object ArrayTransformation extends Pass {
       IfExpr(rc, rt, re).setType(rt.getType)
     }
 
+    case c @ Choose(args, body) =>
+      val body2 = transform(body)
+
+      Choose(args, body2).setType(c.getType).setPosInfo(c)
+
     case m @ MatchExpr(scrut, cses) => {
       val scrutRec = transform(scrut)
       val csesRec = cses.map{
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 1ff95e4c9..24f49dfab 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -681,6 +681,23 @@ trait CodeExtraction extends Extractors {
             }
             Epsilon(c1).setType(pstpe).setPosInfo(epsi.pos.line, epsi.pos.column)
           }
+
+          case chs @ ExChooseExpression(args, tpe, body) => {
+            val cTpe  = scalaType2PureScala(unit, silent)(tpe) 
+
+            val vars = args map { case (tpe, sym) => 
+              val aTpe  = scalaType2PureScala(unit, silent)(tpe)
+              val newID = FreshIdentifier(sym.name.toString).setType(aTpe)
+              owners += (Variable(newID) -> None)
+              varSubsts(sym) = (() => Variable(newID))
+              newID
+            }
+
+            val cBody = rec(body)
+
+            Choose(vars, cBody).setType(cTpe).setPosInfo(chs.pos.line, chs.pos.column)
+          }
+
           case ExWaypointExpression(tpe, i, tree) => {
             val pstpe = scalaType2PureScala(unit, silent)(tpe)
             val IntLiteral(ri) = rec(i)
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index eae464827..d3879226b 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -174,6 +174,21 @@ trait Extractors {
         case _ => None
       }
     }
+
+    object ExChooseExpression {
+      def unapply(tree: Apply) : Option[(List[(Type, Symbol)], Type, Tree)] = tree match {
+        case a @ Apply(
+              TypeApply(Select(Select(funcheckIdent, utilsName), chooseName), types),
+              Function(vds, predicateBody) :: Nil) => {
+          if (utilsName.toString == "Utils" && chooseName.toString == "choose")
+            Some(((types.map(_.tpe) zip vds.map(_.symbol)).toList, a.tpe, predicateBody))
+          else 
+            None
+        }
+        case _ => None
+      }
+    }
+
     object ExWaypointExpression {
       def unapply(tree: Apply) : Option[(Type, Tree, Tree)] = tree match {
         case Apply(
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index b7b5bd343..72d87cec1 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -154,6 +154,14 @@ object PrettyPrinter {
       nsb
     }
 
+    case c@Choose(vars, pred) => {
+      var nsb = sb
+      nsb.append("choose("+vars.mkString(", ")+" => ")
+      nsb = pp(pred, nsb, lvl)
+      nsb.append(")")
+      nsb
+    }
+
     case Waypoint(i, expr) => {
       sb.append("waypoint_" + i + "(")
       pp(expr, sb, lvl)
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index ea5b7ca0f..4778c9b2d 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -612,6 +612,16 @@ object Trees {
             i
         }
         case m @ MatchExpr(scrut,cses) => MatchExpr(rec(scrut), cses.map(inCase(_))).setType(m.getType).setPosInfo(m)
+
+        case c @ Choose(args, body) =>
+          val body2 = rec(body)
+
+          if (body != body2) {
+            Choose(args, body2).setType(c.getType)
+          } else {
+            c
+          }
+
         case t if t.isInstanceOf[Terminal] => t
         case unhandled => scala.sys.error("Non-terminal case should be handled in searchAndReplace: " + unhandled)
       }
@@ -724,6 +734,16 @@ object Trees {
           m
         })
       }
+
+      case c @ Choose(args, body) =>
+        val body2 = rec(body)
+
+        applySubst(if (body != body2) {
+          Choose(args, body2).setType(c.getType).setPosInfo(c)
+        } else {
+          c
+        })
+
       case t if t.isInstanceOf[Terminal] => applySubst(t)
       case unhandled => scala.sys.error("Non-terminal case should be handled in searchAndReplaceDFS: " + unhandled)
     }
@@ -850,6 +870,7 @@ object Trees {
       case ArrayMake(_) => false
       case ArrayClone(_) => false
       case Epsilon(_) => false
+      case Choose(_, _) => false
       case _ => true
     }
     def combine(b1: Boolean, b2: Boolean) = b1 && b2
@@ -863,6 +884,7 @@ object Trees {
       case ArrayMake(_) => false
       case ArrayClone(_) => false
       case Epsilon(_) => false
+      case Choose(_, _) => false
       case _ => b
     }
     treeCatamorphism(convert, combine, compute, expr)
@@ -880,6 +902,7 @@ object Trees {
     }
     treeCatamorphism(convert, combine, compute, expr)
   }
+
   def containsLetDef(expr: Expr): Boolean = {
     def convert(t : Expr) : Boolean = t match {
       case (l : LetDef) => true
-- 
GitLab