Added ExprOps.explainTyping to explain the typing of an expression.

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)
+  }
 }

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)