From 3877a916f11480b1223cdaf65ce3c99f0ff6028f Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Mon, 31 Oct 2016 18:55:26 +0100
Subject: [PATCH] Added some let simplification support in SymbolOps

---
 src/main/scala/inox/ast/SymbolOps.scala | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index 7bd557dae..7a007f114 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -236,6 +236,29 @@ trait SymbolOps { self: TypeOps =>
     normalizeClauses(inlineFunctions(e))
   }
 
+  def simplifyLets(expr: Expr): Expr = postMap({
+    case Let(v1, Let(v2, e2, b2), b1) =>
+      Some(Let(v2, e2, Let(v1, b2, b1)))
+
+    case Let(v, ts @ (
+      TupleSelect(_: Variable, _) |
+      ADTSelector(_: Variable, _) |
+      FiniteMap(Seq(), _, _, _)   |
+      FiniteBag(Seq(), _)         |
+      FiniteSet(Seq(), _)
+    ), b) =>
+      Some(replaceFromSymbols(Map(v -> ts), b))
+
+    case Let(vd, e, b) =>
+      exprOps.count { case v: Variable if vd.toVariable == v => 1 case _ => 0 } (b) match {
+        case 0 => Some(b)
+        case 1 => Some(replaceFromSymbols(Map(vd -> e), b))
+        case _ => None
+      }
+
+    case _ => None
+  }, applyRec = true)(expr)
+
   /** Fully expands all let expressions. */
   def expandLets(expr: Expr): Expr = {
     def rec(ex: Expr, s: Map[Variable,Expr]) : Expr = ex match {
-- 
GitLab