From ac68a436515d7b9f54bc4a9959eb271db1550084 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 3 Jul 2015 14:05:41 +0200
Subject: [PATCH] Small changes
---
.../leon/evaluators/RecursiveEvaluator.scala | 2 +-
src/main/scala/leon/purescala/ExprOps.scala | 2 +-
.../scala/leon/purescala/Expressions.scala | 13 ++++++------
.../scala/leon/purescala/MethodLifting.scala | 4 ++--
src/main/scala/leon/synthesis/Rules.scala | 21 +++++++++----------
5 files changed, 21 insertions(+), 21 deletions(-)
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 9de0a2a05..4265fbecd 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -86,7 +86,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
e(caller) match {
case l@Lambda(params, body) =>
val newArgs = args.map(e)
- val mapping = l.substitutions(newArgs)
+ val mapping = l.paramSubst(newArgs)
e(body)(rctx.withNewVars(mapping), gctx)
case f =>
throw EvalError("Cannot apply non-lambda function " + f)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 50740179a..1809ba00e 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1730,7 +1730,7 @@ object ExprOps {
case LetTuple(is, es, b) =>
letTuple(is, es, apply(b, args))
case l@Lambda(params, body) =>
- l.withSubstitutions(args, body)
+ l.withParamSubst(args, body)
case _ => Application(expr, args)
}
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 4f6ce8433..0d2a840a3 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -94,19 +94,19 @@ object Expressions {
}
}
- case class Application(caller: Expr, args: Seq[Expr]) extends Expr {
- require(caller.getType.isInstanceOf[FunctionType])
- val getType = caller.getType.asInstanceOf[FunctionType].to
+ case class Application(callee: Expr, args: Seq[Expr]) extends Expr {
+ require(callee.getType.isInstanceOf[FunctionType])
+ val getType = callee.getType.asInstanceOf[FunctionType].to
}
case class Lambda(args: Seq[ValDef], body: Expr) extends Expr {
val getType = FunctionType(args.map(_.getType), body.getType).unveilUntyped
- def substitutions(realArgs: Seq[Expr]) = {
+ def paramSubst(realArgs: Seq[Expr]) = {
require(realArgs.size == args.size)
(args map { _.id } zip realArgs).toMap
}
- def withSubstitutions(realArgs: Seq[Expr], e: Expr) = {
- replaceFromIDs(substitutions(realArgs), e)
+ def withParamSubst(realArgs: Seq[Expr], e: Expr) = {
+ replaceFromIDs(paramSubst(realArgs), e)
}
}
@@ -261,6 +261,7 @@ object Expressions {
val value = ()
}
+ /* Case classes */
case class CaseClass(ct: CaseClassType, args: Seq[Expr]) extends Expr {
val getType = ct
}
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index f8a130090..e63dad484 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -39,7 +39,7 @@ object MethodLifting extends TransformationPhase {
}
val paramsMap = fd.params.zip(fdParams).map{case (x,y) => (x.id, y.id)}.toMap
- val receiver = FreshIdentifier("this", recType).setPos(cd.id)
+ val receiver = FreshIdentifier("thiss", recType).setPos(cd.id)
val nfd = new FunDef(id, ctParams ++ fd.tparams, retType, ValDef(receiver) +: fdParams)
nfd.copyContentFrom(fd)
@@ -70,7 +70,7 @@ object MethodLifting extends TransformationPhase {
// 4) Remove methods in classes
for (cd <- u.definedClasses) {
- cd.clearMethods
+ cd.clearMethods()
}
u.copy(defs = defs ++ newCompanions)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 20596de87..2195cb126 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -178,16 +178,15 @@ trait RuleDSL {
// pc corresponds to the pc to reach the point where the solution is used. It
// will be used if the sub-solution has a non-true pre.
def termWrap(f: Expr => Expr, pc: Expr = BooleanLiteral(true)): List[Solution] => Option[Solution] = {
- (sols: List[Solution]) => sols match {
- case List(s) =>
- val pre = if (s.pre == BooleanLiteral(true)) {
- BooleanLiteral(true)
- } else {
- and(pc, s.pre)
- }
-
- Some(Solution(pre, s.defs, f(s.term), s.isTrusted))
- case _ => None
- }
+ case List(s) =>
+ val pre = if (s.pre == BooleanLiteral(true)) {
+ BooleanLiteral(true)
+ } else {
+ and(pc, s.pre)
+ }
+
+ Some(Solution(pre, s.defs, f(s.term), s.isTrusted))
+ case _ => None
+
}
}
--
GitLab