Dodgy way to make a FunctionInvocation out of FunDef and args

src/main/scala/leon/purescala/Constructors.scala

@@ -10,6 +10,7 @@ object Constructors {
   import TypeTreeOps._
   import Common._
   import TypeTrees._
+  import Definitions.FunDef
 
   def tupleSelect(t: Expr, index: Int) = t match {
     case Tuple(es) =>
@@ -53,6 +54,45 @@ object Constructors {
     case more => TupleType(more)
   }
 
+  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 (TupleType(bases1), TupleType(bases2)) => 
+        unifyMany(bases1, bases2)
+      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)
+    
+  }
+  
   private def filterCases(scrutType : TypeTree, resType: Option[TypeTree], cases: Seq[MatchCase]): Seq[MatchCase] = {
     val casesFiltered = scrutType match {
       case c: CaseClassType =>