From e00949f09d3ebf124efa21f82ed4c6711cfed128 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Fri, 22 Apr 2016 10:26:33 +0200
Subject: [PATCH] Added ExprOps.explainTyping to explain the typing of an
expression.
---
src/main/scala/leon/purescala/ExprOps.scala | 12 ++++++++++++
.../leon/solvers/unrolling/TemplateGenerator.scala | 6 +-----
2 files changed, 13 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 6cc0a39bd..1828709ef 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -2187,4 +2187,16 @@ object ExprOps extends GenTreeOps[Expr] {
/** Returns true if expr is a value. Stronger than isGround */
val isValue = (e: Expr) => isValueOfType(e, e.getType)
+
+ /** Returns a nested string explaining why this expression is typed the way it is.*/
+ def explainTyping(e: Expr): String = {
+ leon.purescala.ExprOps.fold[String]{ (e, se) =>
+ e match {
+ case FunctionInvocation(tfd, args) =>
+ s"$e is of type ${e.getType}" + se.map(child => "\n " + "\n".r.replaceAllIn(child, "\n ")).mkString + s" because ${tfd.fd.id.name} was instantiated with ${tfd.fd.tparams.zip(args).map(k => k._1 +":="+k._2).mkString(",")} with type ${tfd.fd.params.map(_.getType).mkString(",")} => ${tfd.fd.returnType}"
+ case e =>
+ s"$e is of type ${e.getType}" + se.map(child => "\n " + "\n".r.replaceAllIn(child, "\n ")).mkString
+ }
+ }(e)
+ }
}
diff --git a/src/main/scala/leon/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/leon/solvers/unrolling/TemplateGenerator.scala
index 6d29458e2..29b307f3d 100644
--- a/src/main/scala/leon/solvers/unrolling/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/unrolling/TemplateGenerator.scala
@@ -224,11 +224,7 @@ class TemplateGenerator[T](val theories: TheoryEncoder,
// id => expr && ... && expr
var guardedExprs = Map[Identifier, Seq[Expr]]()
def storeGuarded(guardVar: Identifier, expr: Expr) : Unit = {
- assert(expr.getType == BooleanType, expr.asString(Program.empty)(LeonContext.empty) + " is not of type Boolean. " + (
- purescala.ExprOps.fold[String]{ (e, se) =>
- s"$e is of type ${e.getType}" + se.map(child => "\n " + "\n".r.replaceAllIn(child, "\n ")).mkString
- }(expr)
- ))
+ assert(expr.getType == BooleanType, expr.asString(Program.empty)(LeonContext.empty) + " is not of type Boolean. " + purescala.ExprOps.explainTyping(expr))
val prev = guardedExprs.getOrElse(guardVar, Nil)
guardedExprs += guardVar -> (expr +: prev)
--
GitLab