From b47356fea94e574e46a2e5575e545eb476d0444d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Tue, 27 Mar 2012 14:35:36 +0000
Subject: [PATCH] Extracting loop invariant

---
 src/main/scala/leon/plugin/CodeExtraction.scala |  8 ++++++++
 src/main/scala/leon/plugin/Extractors.scala     | 10 ++++++++++
 2 files changed, 18 insertions(+)

diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 9f740b8ff..754ecdef4 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -466,6 +466,14 @@ trait CodeExtraction extends Extractors {
           val bodyTree = rec(body)
           While(condTree, bodyTree)
         }
+        case ExWhileWithInvariant(cond, body, inv) => {
+          val condTree = rec(cond)
+          val bodyTree = rec(body)
+          val invTree = rec(inv)
+          val w = While(condTree, bodyTree)
+          w.invariant = Some(invTree)
+          w
+        }
 
         case ExInt32Literal(v) => IntLiteral(v).setType(Int32Type)
         case ExBooleanLiteral(v) => BooleanLiteral(v).setType(BooleanType)
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index 54a5fb7f0..4bd9f9bf3 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -190,6 +190,16 @@ trait Extractors {
         case _ => None
       }
     }
+    object ExWhileWithInvariant {
+      def unapply(tree: Apply): Option[(Tree, Tree, Tree)] = tree match {
+        case Apply(
+          Select(
+            Apply(while2invariant, List(ExWhile(cond, body))),
+            invariantSym),
+          List(invariant)) if invariantSym.toString == "invariant" => Some((cond, body, invariant))
+        case _ => None
+      }
+    }
     object ExTuple {
       def unapply(tree: Apply): Option[(Seq[Type], Seq[Tree])] = tree match {
         case Apply(
-- 
GitLab