diff --git a/src/main/scala/leon/invariant/structure/FunctionUtils.scala b/src/main/scala/leon/invariant/structure/FunctionUtils.scala index a0acdcda7388ee4b6971106cf78cdb49c42768a4..565a6f9f41cbc140c7b6814606897f7cc7eb11f1 100644 --- a/src/main/scala/leon/invariant/structure/FunctionUtils.scala +++ b/src/main/scala/leon/invariant/structure/FunctionUtils.scala @@ -5,13 +5,11 @@ import purescala.Common._ import purescala.Definitions._ import purescala.Expressions._ import purescala.ExprOps._ -import purescala.Extractors._ import purescala.Types._ import invariant.factories._ import invariant.util._ import Util._ import PredicateUtil._ -import ProgramUtil._ import scala.language.implicitConversions /** @@ -37,8 +35,8 @@ object FunctionUtils { def isTemplateInvocation(finv: Expr) = { finv match { case FunctionInvocation(funInv, args) => - (funInv.id.name == "tmpl" && funInv.returnType == BooleanType && - args.size == 1 && args(0).isInstanceOf[Lambda]) + funInv.id.name == "tmpl" && funInv.returnType == BooleanType && + args.size == 1 && args(0).isInstanceOf[Lambda] case _ => false } @@ -46,8 +44,7 @@ object FunctionUtils { def isQMark(e: Expr) = e match { case FunctionInvocation(TypedFunDef(fd, Seq()), args) => - (fd.id.name == "?" && fd.returnType == IntegerType && - args.size <= 1) + fd.id.name == "?" && fd.returnType == IntegerType && args.size <= 1 case _ => false } @@ -104,7 +101,7 @@ object FunctionUtils { val Lambda(_, postBody) = fd.postcondition.get // collect all terms with question marks and convert them to a template val postWoQmarks = postBody match { - case And(args) if args.exists(exists(isQMark) _) => + case And(args) if args.exists(exists(isQMark)) => val (tempExprs, otherPreds) = args.partition { case a if exists(isQMark)(a) => true case _ => false diff --git a/src/main/scala/leon/invariant/util/CallGraph.scala b/src/main/scala/leon/invariant/util/CallGraph.scala index 23f87d5bc0b62163ef40e852d7cc0af0cd658bc3..5e93c451215e9e1f6679e7e94da47a4a2d707a3c 100644 --- a/src/main/scala/leon/invariant/util/CallGraph.scala +++ b/src/main/scala/leon/invariant/util/CallGraph.scala @@ -1,15 +1,10 @@ package leon package invariant.util -import purescala._ -import purescala.Common._ import purescala.Definitions._ import purescala.Expressions._ import purescala.ExprOps._ -import purescala.Extractors._ -import purescala.Types._ import ProgramUtil._ -import Util._ import invariant.structure.FunctionUtils._ import invariant.datastructure._ @@ -71,7 +66,7 @@ class CallGraph { graph.getNodes.toList.foreach((f) => { var inserted = false var index = 0 - for (i <- 0 to funcList.length - 1) { + for (i <- funcList.indices) { if (!inserted && this.transitivelyCalls(funcList(i), f)) { index = i inserted = true @@ -97,7 +92,6 @@ class CallGraph { object CallGraphUtil { def constructCallGraph(prog: Program, onlyBody: Boolean = false, withTemplates: Boolean = false): CallGraph = { -// // println("Constructing call graph") val cg = new CallGraph() functionsWOFields(prog.definedFunctions).foreach((fd) => { @@ -125,17 +119,11 @@ object CallGraphUtil { cg } - def getCallees(expr: Expr): Set[FunDef] = { - var callees = Set[FunDef]() - simplePostTransform((expr) => expr match { - //note: do not consider field invocations - case FunctionInvocation(TypedFunDef(callee, _), args) - if callee.isRealFunction => { - callees += callee - expr - } - case _ => expr - })(expr) - callees - } + def getCallees(expr: Expr): Set[FunDef] = collect { + case expr@FunctionInvocation(TypedFunDef(callee, _), _) if callee.isRealFunction => + Set(callee) + case _ => + Set[FunDef]() + }(expr) + } \ No newline at end of file diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala index 1337e74d0331775be13e7d1d3311281c630ffdef..c8cf8f118ac17ca29272f2941f71b8d99a99af9c 100644 --- a/src/main/scala/leon/purescala/Extractors.scala +++ b/src/main/scala/leon/purescala/Extractors.scala @@ -357,22 +357,20 @@ object Extractors { } def unapply(me : MatchExpr) : Option[(Pattern, Expr, Expr)] = { - if (me eq null) None else { me match { + Option(me) collect { case MatchExpr(scrut, List(SimpleCase(pattern, body))) if !aliased(pattern.binders, variablesOf(scrut)) => - Some(( pattern, scrut, body )) - case _ => None - }} + ( pattern, scrut, body ) + } } } object LetTuple { def unapply(me : MatchExpr) : Option[(Seq[Identifier], Expr, Expr)] = { - if (me eq null) None else { me match { + Option(me) collect { case LetPattern(TuplePattern(None,subPatts), value, body) if subPatts forall { case WildcardPattern(Some(_)) => true; case _ => false } => - Some((subPatts map { _.binder.get }, value, body )) - case _ => None - }} + (subPatts map { _.binder.get }, value, body ) + } } }