From 8424cae58aeb7882c80a7000719715a3bd08af7f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Fri, 29 Apr 2016 14:38:11 +0200
Subject: [PATCH] Fixed ExprOps.isValue for covariant/contravariant function
types. Fixed SelfPrettyPrinter to not evaluate the argument again. Removed
unused debug variable.
---
src/main/scala/leon/purescala/ExprOps.scala | 12 +++++++-----
.../scala/leon/purescala/SelfPrettyPrinter.scala | 7 +++----
2 files changed, 10 insertions(+), 9 deletions(-)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 02510c7c8..98cc822d8 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -2142,9 +2142,10 @@ object ExprOps extends GenTreeOps[Expr] {
case _ =>
fun
}
- var msgs: String = ""
- implicit class BooleanAdder(b: Boolean) {
- def <(msg: String) = {if(!b) msgs += msg; b}
+
+ // Use this only to debug isValueOfType
+ private implicit class BooleanAdder(b: Boolean) {
+ @inline def <(msg: String) = {/*if(!b) println(msg); */b}
}
/** Returns true if expr is a value of type t */
@@ -2181,11 +2182,12 @@ object ExprOps extends GenTreeOps[Expr] {
(ct == ct2) < s"$ct not equal to $ct2" &&
((args zip ct.fieldsTypes) forall (argstyped => isValueOfType(argstyped._1, argstyped._2)))
case (FiniteLambda(mapping, default, tpe), exTpe@FunctionType(ins, out)) =>
+ variablesOf(e).isEmpty &&
tpe == exTpe
case (Lambda(valdefs, body), FunctionType(ins, out)) =>
variablesOf(e).isEmpty &&
- (valdefs zip ins forall (vdin => (vdin._1.getType == vdin._2) < s"${vdin._1.getType} is not equal to ${vdin._2}")) &&
- (body.getType == out) < s"${body.getType} is not equal to ${out}"
+ (valdefs zip ins forall (vdin => TypeOps.isSubtypeOf(vdin._2, vdin._1.getType) < s"${vdin._2} is not a subtype of ${vdin._1.getType}")) &&
+ (TypeOps.isSubtypeOf(body.getType, out)) < s"${body.getType} is not a subtype of ${out}"
case (FiniteBag(elements, fbtpe), BagType(tpe)) =>
fbtpe == tpe && elements.forall{ case (key, value) => isValueOfType(key, tpe) && isValueOfType(value, IntegerType) }
case _ => false
diff --git a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
index 2488aec8c..9212163a7 100644
--- a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
@@ -109,12 +109,11 @@ class SelfPrettyPrinter {
case _ => false
} match {
case None => orElse
- case Some(l) =>
- ctx.reporter.debug("Executing pretty printer for type " + v.getType + " : " + l + " on " + v)
+ case Some(Lambda(Seq(ValDef(id)), body)) =>
+ ctx.reporter.debug("Executing pretty printer for type " + v.getType + " : " + v + " on " + v)
val ste = new DefaultEvaluator(ctx, program)
try {
- val toEvaluate = application(l, Seq(v))
- val result = ste.eval(toEvaluate)
+ val result = ste.eval(body, Map(id -> v))
result.result match {
case Some(StringLiteral(res)) if res != "" =>
--
GitLab