From 4b91096a924da0c5b56291381620cf1df30447a2 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Wed, 21 Jan 2015 16:42:56 +0100
Subject: [PATCH] Fix functionInvocation constructor

---
 .../scala/leon/purescala/Constructors.scala   | 42 +++++--------------
 1 file changed, 11 insertions(+), 31 deletions(-)

diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 1b1dfbf06..2f7092fce 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -59,41 +59,21 @@ object Constructors {
     case more => TupleType(more)
   }
 
+  /** Will instantiate the type parameters of the function according to argument types */
   def functionInvocation(fd : FunDef, args : Seq[Expr]) = {
     
-    def unifyMany(ts1 : Seq[TypeTree], ts2 : Seq[TypeTree]) = {
-      ts1.zip(ts2).map{ case (t1, t2) => unify(t1,t2) }.foldLeft(Map[Identifier, TypeTree]())(_ ++ _)
-    }
-    
-    def unify(t1 : TypeTree, t2 : TypeTree) : Map[Identifier, TypeTree] = (t1,t2) match {
-      case (TypeParameter(id), _) => Map(id -> t2)
-      case (_, TypeParameter(id)) => Map(id -> t1)
-      case (BooleanType, BooleanType) |
-           (Int32Type, Int32Type) |
-           (UnitType, UnitType) |
-           (CharType, CharType) => Map()
-      case (TupleType(bases1), TupleType(bases2)) => 
-        unifyMany(bases1, bases2)
-      case (SetType(base1), SetType(base2)) => 
-        unify(base1,base2)
-      case (ArrayType(base1), ArrayType(base2)) => 
-        unify(base1,base2)
-      case (MultisetType(base1), MultisetType(base2)) => 
-        unify(base1,base2)
-      case (MapType(from1, to1), MapType(from2, to2)) => 
-        unify(from1, from2) ++ unify(to1,to2)
-      case (FunctionType(from1, to1), FunctionType(from2, to2)) => 
-        unifyMany(to1 :: from1, to2 :: from2)
-      case (c1 : ClassType, c2 : ClassType) if isSubtypeOf(c1, c2) || isSubtypeOf(c2,c1) =>
-        unifyMany(c1.tps, c2.tps)
-      case _ => throw new java.lang.IllegalArgumentException()
-    }
-    
     require(fd.params.length == args.length)
-    val typeInstantiations = unifyMany(fd.params map { _.getType}, args map { _.getType })
-    val tps = fd.tparams map { tpar => typeInstantiations(tpar.id) }
-    FunctionInvocation(fd.typed(tps), args)
     
+    val formalType = tupleTypeWrap(fd.params map { _.getType })
+    val actualType = tupleTypeWrap(args map { _.getType })
+    
+    canBeSubtypeOf(actualType, typeParamsOf(formalType).toSeq, formalType) match {
+      case Some(tmap) =>
+        FunctionInvocation(fd.typed(fd.tparams map { tpd => tmap.getOrElse(tpd.tp, tpd.tp) }), args)
+      case None => sys.error(s"$actualType cannot be a subtype of $formalType!")
+    }
+
+   
   }
   
   private def filterCases(scrutType : TypeTree, resType: Option[TypeTree], cases: Seq[MatchCase]): Seq[MatchCase] = {
-- 
GitLab