From 5d20989aba76ae77b5a4fe750687582b650f0a87 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Wed, 26 Oct 2016 00:56:56 +0200
Subject: [PATCH] Minor aesthetic changes in Expressions

---
 src/main/scala/inox/ast/Expressions.scala | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index d7fcf07d6..3d6d4064d 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -123,7 +123,7 @@ trait Expressions { self: Trees =>
     protected def computeType(implicit s: Symbols): Type = s.lookupFunction(id, tps) match {
       case Some(tfd) =>
         require(args.size == tfd.params.size)
-        checkParamTypes(args.map(_.getType), tfd.params.map(_.getType), tfd.returnType)
+        checkParamTypes(args.map(_.getType), tfd.params.map(_.tpe), tfd.returnType)
       case _ => Untyped
     }
 
@@ -562,9 +562,10 @@ trait Expressions { self: Trees =>
   /* Set operations */
 
   /** $encodingof `Set[base](elements)` */
-  case class FiniteSet(elements: Seq[Expr], base: Type) extends Expr {
-    private lazy val tpe = SetType(base).unveilUntyped
-    def getType(implicit s: Symbols): Type = tpe
+  case class FiniteSet(elements: Seq[Expr], base: Type) extends Expr with CachingTyped {
+    protected def computeType(implicit s: Symbols): Type = SetType(
+      checkParamTypes(elements.map(_.getType), List.fill(elements.size)(base), base)
+    ).unveilUntyped
   }
 
   /** $encodingof `set + elem` */
@@ -663,8 +664,10 @@ trait Expressions { self: Trees =>
 
   /** $encodingof `Map[keyType, valueType](key1 -> value1, key2 -> value2 ...)` */
   case class FiniteMap(pairs: Seq[(Expr, Expr)], default: Expr, keyType: Type) extends Expr with CachingTyped {
-    protected def computeType(implicit s: Symbols): Type =
-      MapType(keyType, default.getType).unveilUntyped
+    protected def computeType(implicit s: Symbols): Type = MapType(
+      checkParamTypes(pairs.map(_._1.getType), List.fill(pairs.size)(keyType), keyType),
+      s.leastUpperBound(pairs.map(_._2.getType) :+ default.getType).getOrElse(Untyped)
+    ).unveilUntyped
   }
 
   /** $encodingof `map.apply(key)` (or `map(key)`) */
-- 
GitLab