From a955db93047e64df0807d993104a775b866788ae Mon Sep 17 00:00:00 2001
From: Utkarsh Upadhyay <musically.ut@gmail.com>
Date: Sat, 10 Jul 2010 19:41:34 +0000
Subject: [PATCH] Added handling of case expressions after substitution to
Leaf() terms (which do not contain any variables).
---
src/orderedsets/UnifierMain.scala | 32 ++++++++++++++++++-------------
1 file changed, 19 insertions(+), 13 deletions(-)
diff --git a/src/orderedsets/UnifierMain.scala b/src/orderedsets/UnifierMain.scala
index 9655be8e7..951279fbd 100644
--- a/src/orderedsets/UnifierMain.scala
+++ b/src/orderedsets/UnifierMain.scala
@@ -76,22 +76,28 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
}
def isAlpha(varMap: Variable => Expr)(t: Expr): Option[Expr] = t match {
- case FunctionInvocation(fd, Seq(v@ Variable(_))) => asCatamorphism(program, fd) match {
+ case FunctionInvocation(fd, arg) => asCatamorphism(program, fd) match {
case None => None
- case Some(lstMatch) => varMap(v) match {
- case CaseClass(cd, args) => {
- val (_, _, ids, rhs) = lstMatch.find( _._1 == cd).get
- val repMap = Map( ids.map(id => Variable(id):Expr).zip(args): _* )
- Some(searchAndReplace(repMap.get)(rhs))
- }
- case u @ Variable(_) => {
- val c = Variable(FreshIdentifier("Coll", true)).setType(t.getType)
- // TODO: Keep track of these variables for M1(t, c)
- Some(c)
+ case Some(lstMatch) => arg match {
+ case Seq(v@Variable(_)) => varMap(v) match {
+ case CaseClass(cd, args) => {
+ val (_, _, ids, rhs) = lstMatch.find( _._1 == cd).get
+ val repMap = Map( ids.map(id => Variable(id):Expr).zip(args): _* )
+ reporter.warning("Converting " + t + " to " + rhs)
+ Some(searchAndReplace(repMap.get)(rhs))
+ }
+ case u @ Variable(_) => {
+ val c = Variable(FreshIdentifier("Coll", true)).setType(t.getType)
+ // TODO: Keep track of these variables for M1(t, c)
+ Some(c)
+ }
+ case _ => error("Bad substitution")
}
- case _ => error("Bad substitution")
+ case Seq(CaseClass(cd, _)) =>
+ val (_, _, ids, rhs) = lstMatch.find( _._1 == cd).get
+ Some(rhs)
+ case _ => error("Not a catamorphism.")
}
- case _ => None
}
case _ => None
}
--
GitLab