From 928b4793b88f867b973fd2b87f8e6cd040c758f8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 11 May 2012 14:01:15 +0200
Subject: [PATCH] capture binding variables of pattern matching
---
src/main/scala/leon/FunctionClosure.scala | 20 ++++++++++++--------
1 file changed, 12 insertions(+), 8 deletions(-)
diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala
index 661a05287..56239d319 100644
--- a/src/main/scala/leon/FunctionClosure.scala
+++ b/src/main/scala/leon/FunctionClosure.scala
@@ -118,17 +118,19 @@ object FunctionClosure extends Pass {
val scrutRec = functionClosure(scrut, bindedVars, id2freshId, fd2FreshFd)
val csesRec = cses.map{
case SimpleCase(pat, rhs) => {
+ val binders = pat.binders
val cond = conditionForPattern(scrut, pat)
pathConstraints ::= cond
- val rRhs = functionClosure(rhs, bindedVars, id2freshId, fd2FreshFd)
+ val rRhs = functionClosure(rhs, bindedVars ++ binders, id2freshId, fd2FreshFd)
pathConstraints = pathConstraints.tail
SimpleCase(pat, rRhs)
}
case GuardedCase(pat, guard, rhs) => {
+ val binders = pat.binders
val cond = conditionForPattern(scrut, pat)
pathConstraints ::= cond
- val rRhs = functionClosure(rhs, bindedVars, id2freshId, fd2FreshFd)
- val rGuard = functionClosure(guard, bindedVars, id2freshId, fd2FreshFd)
+ val rRhs = functionClosure(rhs, bindedVars ++ binders, id2freshId, fd2FreshFd)
+ val rGuard = functionClosure(guard, bindedVars ++ binders, id2freshId, fd2FreshFd)
pathConstraints = pathConstraints.tail
GuardedCase(pat, rGuard, rRhs)
}
@@ -140,15 +142,17 @@ object FunctionClosure extends Pass {
case None => v
case Some(nid) => Variable(nid)
}
- /*replace(
- id2freshId.map(p => (p._1.toVariable, p._2.toVariable)),
- enclosingLets.foldLeft(v: Expr){
- case (expr, (id, value)) => replace(Map(id.toVariable -> value), expr)
- })*/
case t if t.isInstanceOf[Terminal] => t
case unhandled => scala.sys.error("Non-terminal case should be handled in FunctionClosure: " + unhandled)
}
+ def freshIdInPat(pat: Pattern, id2freshId: Map[Identifier, Identifier]): Pattern = pat match {
+ case InstanceOfPattern(binder, classTypeDef) => InstanceOfPattern(binder.map(id2freshId(_)), classTypeDef)
+ case WildcardPattern(binder) => WildcardPattern(binder.map(id2freshId(_)))
+ case CaseClassPattern(binder, caseClassDef, subPatterns) => CaseClassPattern(binder.map(id2freshId(_)), caseClassDef, subPatterns.map(freshIdInPat(_, id2freshId)))
+ case TuplePattern(binder, subPatterns) => TuplePattern(binder.map(id2freshId(_)), subPatterns.map(freshIdInPat(_, id2freshId)))
+ }
+
//filter the list of constraints, only keeping those relevant to the set of variables
def filterConstraints(vars: Set[Identifier]): (List[Expr], Set[Identifier]) = {
var allVars = vars
--
GitLab