From 6ca663fe92cc2c7db07312403267e670d2dad144 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 30 Oct 2012 03:54:10 +0100
Subject: [PATCH] Nasty Nary extractor for MatchExpr
---
src/main/scala/leon/purescala/Extractors.scala | 12 ++++++++++++
1 file changed, 12 insertions(+)
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 57b108ddb..94eb5fba0 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -101,6 +101,18 @@ object Extractors {
case Block(args, rest) => Some((args :+ rest, exprs => Block(exprs.init, exprs.last)))
case Tuple(args) => Some((args, Tuple))
case IfExpr(cond, then, elze) => Some((Seq(cond, then, elze), (as: Seq[Expr]) => IfExpr(as(0), as(1), as(2))))
+ case MatchExpr(scrut, cases) =>
+ Some((scrut +: cases.flatMap{ case SimpleCase(_, e) => Seq(e)
+ case GuardedCase(_, e1, e2) => Seq(e1, e2) }
+ , { es: Seq[Expr] =>
+ var i = 1;
+ val newcases = for (caze <- cases) yield caze match {
+ case SimpleCase(b, _) => i+=1; SimpleCase(b, es(i-1))
+ case GuardedCase(b, _, _) => i+=2; GuardedCase(b, es(i-2), es(i-1))
+ }
+
+ MatchExpr(es(0), newcases)
+ }))
case ex: NAryExtractable => ex.extract
case _ => None
}
--
GitLab