Skip to content
Snippets Groups Projects
Commit 3aa8929e authored by Regis Blanc's avatar Regis Blanc
Browse files

fix issue with generic function

parent 6a522199
No related branches found
No related tags found
No related merge requests found
...@@ -219,7 +219,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T], ...@@ -219,7 +219,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
// id => expr && ... && expr // id => expr && ... && expr
var guardedExprs = Map[Identifier, Seq[Expr]]() var guardedExprs = Map[Identifier, Seq[Expr]]()
def storeGuarded(guardVar: Identifier, expr: Expr) : Unit = { def storeGuarded(guardVar: Identifier, expr: Expr) : Unit = {
assert(expr.getType == BooleanType, expr.asString(Program.empty)(LeonContext.empty) + " is not of type Boolean." + ( assert(expr.getType == BooleanType, expr.asString(Program.empty)(LeonContext.empty) + " is not of type Boolean. " + (
purescala.ExprOps.fold[String]{ (e, se) => purescala.ExprOps.fold[String]{ (e, se) =>
s"$e is of type ${e.getType}" + se.map(child => "\n " + "\n".r.replaceAllIn(child, "\n ")).mkString s"$e is of type ${e.getType}" + se.map(child => "\n " + "\n".r.replaceAllIn(child, "\n ")).mkString
}(expr) }(expr)
......
...@@ -217,7 +217,7 @@ object AntiAliasingPhase extends TransformationPhase { ...@@ -217,7 +217,7 @@ object AntiAliasingPhase extends TransformationPhase {
if(duplicatedParams.nonEmpty) if(duplicatedParams.nonEmpty)
ctx.reporter.fatalError(fi.getPos, "Illegal passing of aliased parameter: " + duplicatedParams.head) ctx.reporter.fatalError(fi.getPos, "Illegal passing of aliased parameter: " + duplicatedParams.head)
val freshRes = FreshIdentifier("res", nfd.returnType) val freshRes = FreshIdentifier("res", nfd.typed(fd.tps).returnType)
val extractResults = Block( val extractResults = Block(
modifiedArgs.zipWithIndex.map(p => Assignment(p._1.id, TupleSelect(freshRes.toVariable, p._2 + 2))), modifiedArgs.zipWithIndex.map(p => Assignment(p._1.id, TupleSelect(freshRes.toVariable, p._2 + 2))),
......
...@@ -3,40 +3,38 @@ import leon.collection._ ...@@ -3,40 +3,38 @@ import leon.collection._
object FunctionCaching { object FunctionCaching {
case class Cache() { case class CachedFun[A,B](fun: (A) => B, var cached: Map[A, B], var cacheHit: Set[A]) {
var cached: Map[BigInt, BigInt] = Map()
//contains the set of elements where cache has been used
var cacheHit: Set[BigInt] = Set()
}
def cachedFun(f: (BigInt) => BigInt, x: BigInt)(implicit cache: Cache) = { def call(a: A): B = {
cache.cached.get(x) match { cached.get(a) match {
case None() => case None() =>
val res = f(x) val res = fun(a)
cache.cached = cache.cached.updated(x, res) cached = cached.updated(a, res)
res res
case Some(cached) => case Some(res) =>
cache.cacheHit = cache.cacheHit ++ Set(x) cacheHit = cacheHit ++ Set(a)
cached res
}
} }
} }
def funProperlyCached(x: BigInt, fun: (BigInt) => BigInt, trash: List[BigInt]): Boolean = { def funProperlyCached(x: BigInt, fun: (BigInt) => BigInt, trash: List[BigInt]): Boolean = {
implicit val cache = Cache() val cachedFun = CachedFun[BigInt, BigInt](fun, Map(), Set())
val res1 = cachedFun(fun, x) val res1 = cachedFun.call(x)
multipleCalls(trash, x, fun) multipleCalls(trash, cachedFun, x)
val res2 = cachedFun(fun, x) val res2 = cachedFun.call(x)
res1 == res2 && cache.cacheHit.contains(x) res1 == res2 && cachedFun.cacheHit.contains(x)
} holds } holds
def multipleCalls(args: List[BigInt], x: BigInt, fun: (BigInt) => BigInt)(implicit cache: Cache): Unit = { def multipleCalls(args: List[BigInt], cachedFun: CachedFun[BigInt, BigInt], x: BigInt): Unit = {
require(cache.cached.isDefinedAt(x)) require(cachedFun.cached.isDefinedAt(x))
args match { args match {
case Nil() => () case Nil() => ()
case y::ys => case y::ys =>
cachedFun(fun, y) cachedFun.call(x)
multipleCalls(ys, x, fun) multipleCalls(ys, cachedFun, x)
} }
} ensuring(_ => old(cache).cached.get(x) == cache.cached.get(x)) } ensuring(_ => old(cachedFun).cached.get(x) == cachedFun.cached.get(x))
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment