From ca731869d284d35e32acf98a9605ee76b30cadb8 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Thu, 27 Oct 2016 14:25:11 +0200
Subject: [PATCH] Better typing checking and typing debug

---
 src/main/scala/inox/ast/Expressions.scala | 5 ++---
 src/main/scala/inox/ast/SymbolOps.scala   | 3 ++-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index 9c87a1acb..66f2f55c5 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -271,9 +271,8 @@ trait Expressions { self: Trees =>
       case _ => None
     }
 
-    protected def computeType(implicit s: Symbols): Type = constructor.map { tccd =>
-      val index = tccd.definition.selectorID2Index(selector)
-      tccd.fieldsTypes(index)
+    protected def computeType(implicit s: Symbols): Type = constructor.flatMap { tccd =>
+      scala.util.Try(tccd.definition.selectorID2Index(selector)).toOption.map(tccd.fieldsTypes)
     }.getOrElse(Untyped)
   }
 
diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index 239f0cc62..b9f5f56b7 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -648,7 +648,8 @@ trait SymbolOps { self: TypeOps =>
               se.map(child => "\n  " + "\n".r.replaceAllIn(child, "\n  ")).mkString +
               s" because ${tfd.fd.id.name} was instantiated with " +
               s"${tfd.fd.tparams.zip(tps).map(k => k._1.asString + ":=" + k._2.asString).mkString(",")} " +
-              s"with type ${tfd.fd.params.map(_.getType.asString).mkString(",")} => ${tfd.fd.returnType.asString}"
+              s"with type ${tfd.fd.params.map(_.getType.asString).mkString("(", ",", ")")} => " +
+              s"${tfd.fd.returnType.asString}"
             case None =>
               s"${e.asString} is of type ${e.getType.asString}" +
               se.map(child => "\n  " + "\n".r.replaceAllIn(child, "\n  ")).mkString +
-- 
GitLab