From 5e6413e5ed0fa0266c8068a7177a1b8d7e498f2d Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Wed, 13 Nov 2013 17:20:00 +0100
Subject: [PATCH] Basic flattening for pattern match reconstruction
---
src/main/scala/leon/purescala/TreeOps.scala | 19 ++++++++++++++++---
1 file changed, 16 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index d31c7a392..09f6a01c8 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1040,7 +1040,7 @@ object TreeOps {
// This transformation assumes IfExpr of the form generated by decomposeIfs
def patternMatchReconstruction(e: Expr): Expr = {
- def pre(e: Expr): Expr = e match {
+ def post(e: Expr): Expr = e match {
case IfExpr(cond, thenn, elze) =>
val TopLevelAnds(cases) = cond
@@ -1133,7 +1133,20 @@ object TreeOps {
p
}
- MatchExpr(scrutinee, Seq(SimpleCase(simplifyPattern(pattern), newThen), SimpleCase(WildcardPattern(None), elze))).setType(e.getType)
+ elze match {
+ case MatchExpr(scrut, cases) if scrut == scrutinee =>
+ MatchExpr(scrutinee,
+ SimpleCase(simplifyPattern(pattern), newThen) +:
+ cases
+ ).setType(e.getType)
+
+ case _ =>
+ MatchExpr(scrutinee,
+ Seq(SimpleCase(simplifyPattern(pattern), newThen),
+ SimpleCase(WildcardPattern(None), elze)
+ )
+ ).setType(e.getType)
+ }
} else {
e
}
@@ -1141,7 +1154,7 @@ object TreeOps {
e
}
- simplePreTransform(pre)(e)
+ simplePostTransform(post)(e)
}
def simplifyTautologies(sf: SolverFactory[Solver])(expr : Expr) : Expr = {
--
GitLab