From 2caaa9598ff79ed2bf5a32a5a0e7bc8c0f4641b5 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 25 Jun 2015 18:44:19 +0200
Subject: [PATCH] Refactor TypedFunDef
---
.../scala/leon/purescala/Definitions.scala | 43 ++++---------------
.../leon/termination/StructuralSize.scala | 2 +-
2 files changed, 10 insertions(+), 35 deletions(-)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 08d33ccf6..4ecc80676 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -59,8 +59,7 @@ object Definitions {
def toVariable : Variable = Variable(id)
}
- /** A wrapper for a program. For now a program is simply a single object. The
- * name is meaningless and we just use the package name as id. */
+ /** A wrapper for a program. For now a program is simply a single object. */
case class Program(units: List[UnitDef]) extends Definition {
val id = FreshIdentifier("program")
@@ -481,43 +480,19 @@ object Definitions {
lazy val returnType: TypeTree = translated(fd.returnType)
private var trCache = Map[Expr, Expr]()
- private var postCache = Map[Expr, Expr]()
- def fullBody = {
- val fb = fd.fullBody
- trCache.getOrElse(fb, {
- val res = translated(fb)
- trCache += fb -> res
+ private def cached(e: Expr): Expr = {
+ trCache.getOrElse(e, {
+ val res = translated(e)
+ trCache += e -> res
res
})
}
- def body = fd.body.map { b =>
- trCache.getOrElse(b, {
- val res = translated(b)
- trCache += b -> res
- res
- })
- }
-
- def precondition = fd.precondition.map { pre =>
- trCache.getOrElse(pre, {
- val res = translated(pre)
- trCache += pre -> res
- res
- })
- }
-
- def postcondition = fd.postcondition.map {
- case post if typesMap.nonEmpty =>
- postCache.getOrElse(post, {
- val res = instantiateType(post, typesMap, paramsMap)
- postCache += (post -> res)
- res
- })
-
- case p => p
- }
+ def fullBody = cached(fd.fullBody)
+ def body = fd.body map cached
+ def precondition = fd.precondition map cached
+ def postcondition = fd.postcondition map cached
def hasImplementation = body.isDefined
def hasBody = hasImplementation
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index 8656a2005..a6b08d598 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -35,7 +35,7 @@ trait StructuralSize {
Variable(x),
uminus(Variable(x))
))
- TypedFunDef(absFun, Seq()) // Seq() because no generic type params
+ absFun.typed
}
def size(expr: Expr) : Expr = {
--
GitLab