diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala index 61e6af5c567b25c55ff7695c5a5805ad4b6af279..8f77e8812e172a362b7ffa46086fa4045b020cce 100644 --- a/src/main/scala/leon/purescala/FunctionClosure.scala +++ b/src/main/scala/leon/purescala/FunctionClosure.scala @@ -122,19 +122,6 @@ object FunctionClosure extends TransformationPhase { args.map(arg => functionClosure(arg, bindedVars, id2freshId, fd2FreshFd)) ++ extraArgs.map(v => replace(id2freshId.map(p => (p._1.toVariable, p._2.toVariable)), v))).copiedFrom(fi) } - case n @ NAryOperator(args, recons) => { - val rargs = args.map(a => functionClosure(a, bindedVars, id2freshId, fd2FreshFd)) - recons(rargs).copiedFrom(n) - } - case b @ BinaryOperator(t1,t2,recons) => { - val r1 = functionClosure(t1, bindedVars, id2freshId, fd2FreshFd) - val r2 = functionClosure(t2, bindedVars, id2freshId, fd2FreshFd) - recons(r1,r2).copiedFrom(b) - } - case u @ UnaryOperator(t,recons) => { - val r = functionClosure(t, bindedVars, id2freshId, fd2FreshFd) - recons(r).copiedFrom(u) - } case m @ MatchExpr(scrut,cses) => { val scrutRec = functionClosure(scrut, bindedVars, id2freshId, fd2FreshFd) val csesRec = cses.map{ cse => @@ -153,7 +140,20 @@ object FunctionClosure extends TransformationPhase { case None => v case Some(nid) => Variable(nid) } - case t if t.isInstanceOf[Terminal] => t + case n @ NAryOperator(args, recons) => { + val rargs = args.map(a => functionClosure(a, bindedVars, id2freshId, fd2FreshFd)) + recons(rargs).copiedFrom(n) + } + case b @ BinaryOperator(t1,t2,recons) => { + val r1 = functionClosure(t1, bindedVars, id2freshId, fd2FreshFd) + val r2 = functionClosure(t2, bindedVars, id2freshId, fd2FreshFd) + recons(r1,r2).copiedFrom(b) + } + case u @ UnaryOperator(t,recons) => { + val r = functionClosure(t, bindedVars, id2freshId, fd2FreshFd) + recons(r).copiedFrom(u) + } + case t : Terminal => t case unhandled => scala.sys.error("Non-terminal case should be handled in FunctionClosure: " + unhandled) }