From 2dd6b190d11e5c66f15d58a404af52e11ad7c28b Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 27 Jul 2016 17:45:11 +0200
Subject: [PATCH] Pattern binders should be ordered
---
src/main/scala/inox/ast/Expressions.scala | 4 ++--
src/main/scala/inox/ast/Extractors.scala | 2 +-
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index b8d259cd1..20fccb748 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -229,8 +229,8 @@ trait Expressions { self: Trees =>
val subPatterns: Seq[Pattern]
val binder: Option[ValDef]
- private def subBinders = subPatterns.flatMap(_.binders).toSet
- def binders: Set[ValDef] = subBinders ++ binder.toSet
+ private def subBinders = subPatterns.flatMap(_.binders)
+ def binders: Seq[ValDef] = binder.toSeq ++ subBinders
def withBinder(b: ValDef) = { this match {
case Pattern(None, subs, builder) => builder(Some(b), subs)
diff --git a/src/main/scala/inox/ast/Extractors.scala b/src/main/scala/inox/ast/Extractors.scala
index 050f9a485..699874093 100644
--- a/src/main/scala/inox/ast/Extractors.scala
+++ b/src/main/scala/inox/ast/Extractors.scala
@@ -299,7 +299,7 @@ trait Extractors { self: Trees =>
def unapply(me: MatchExpr) : Option[(Pattern, Expr, Expr)] = {
Option(me) collect {
- case MatchExpr(scrut, List(SimpleCase(pattern, body))) if !aliasedSymbols(pattern.binders, exprOps.variablesOf(scrut)) =>
+ case MatchExpr(scrut, List(SimpleCase(pattern, body))) if !aliasedSymbols(pattern.binders.toSet, exprOps.variablesOf(scrut)) =>
( pattern, scrut, body )
}
}
--
GitLab