From 1675d9f2d616d043f02cab3fac4071741d77127b Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Thu, 13 Nov 2014 14:28:30 +0100
Subject: [PATCH] Refactor Patterns a bit

---
 src/main/scala/leon/purescala/Trees.scala | 22 +++++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index e43986632..c88b7c38f 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -279,12 +279,32 @@ object Trees {
     def expressions = List(guard, rhs)
   }
 
+
+  object Pattern {
+    def unapply(p : Pattern) : Option[(
+      Option[Identifier], 
+      Seq[Pattern], 
+      (Option[Identifier], Seq[Pattern]) => Pattern
+    )] = Some(p match {
+      case InstanceOfPattern(b, ct)       => (b, Seq(), (b,_) => InstanceOfPattern(b,ct))
+      case WildcardPattern(b)             => (b, Seq(), (b,_) => WildcardPattern(b)     )
+      case CaseClassPattern(b, ct, subs)  => (b, subs,  CaseClassPattern(_, ct, _)      )
+      case TuplePattern(b,subs)           => (b, subs,  TuplePattern                    )
+      case LiteralPattern(b, l)           => (b, Seq(), (b,_) => LiteralPattern(b, l)   )
+    })
+  }
+
   sealed abstract class Pattern extends Tree {
     val subPatterns: Seq[Pattern]
     val binder: Option[Identifier]
 
     private def subBinders = subPatterns.map(_.binders).foldLeft[Set[Identifier]](Set.empty)(_ ++ _)
-    def binders: Set[Identifier] = subBinders ++ (if(binder.isDefined) Set(binder.get) else Set.empty)
+    def binders: Set[Identifier] = subBinders ++ binder.toSet
+
+    def withBinder(b : Identifier) = { this match {
+      case Pattern(None, subs, builder) => builder(Some(b), subs)
+      case other => other
+    }}.copiedFrom(this)
   }
 
   case class InstanceOfPattern(binder: Option[Identifier], ct: ClassType) extends Pattern { // c: Class
-- 
GitLab