Fixed ClassLoader issue and type errors in evaluation.

This fixes the classloader issue that we had, where, in codegen, a
library class would be loaded twice and be incompatible with itself.

It also fixes an oversight in evaluating expressions, where the returned
ground term was sometimes untyped (typically: empty sets and the like).
We now copy the type of the (unevaluated) expression in such situations.

src/main/scala/leon/codegen/CompilationUnit.scala

@@ -25,7 +25,7 @@ class CompilationUnit(val program: Program, val classes: Map[Definition, ClassFi
   }.toMap
 
   protected[codegen] val loader = {
-    val l = new CafebabeClassLoader
+    val l = new CafebabeClassLoader(classOf[CompilationUnit].getClassLoader)
     classes.values.foreach(l.register(_))
     l
   }
@@ -72,6 +72,7 @@ class CompilationUnit(val program: Program, val classes: Map[Definition, ClassFi
       compileExpression(e, Seq()).evalToJVM(Seq())
   }
 
+  // Note that this may produce untyped expressions! (typically: sets, maps)
   private[codegen] def jvmToValue(e: AnyRef): Expr = e match {
     case i: Integer =>
       IntLiteral(i.toInt)

src/main/scala/leon/codegen/CompiledExpression.scala

@@ -18,6 +18,8 @@ class CompiledExpression(unit: CompilationUnit, cf: ClassFile, expression : Expr
   private lazy val cl = unit.loader.loadClass(cf.className)
   private lazy val meth = cl.getMethods()(0)
 
+  private val exprType = expression.getType
+
   protected[codegen] def evalToJVM(args: Seq[Expr]): AnyRef = {
     assert(args.size == argsDecl.size)
 
@@ -29,9 +31,14 @@ class CompiledExpression(unit: CompilationUnit, cf: ClassFile, expression : Expr
   }
 
   // This may throw an exception. We unwrap it if needed.
+  // We also need to reattach a type in some cases (sets, maps).
   def eval(args: Seq[Expr]) : Expr = {
     try {
-      unit.jvmToValue(evalToJVM(args))
+      val result = unit.jvmToValue(evalToJVM(args))
+      if(!result.isTyped) {
+        result.setType(exprType)
+      }
+      result
     } catch {
       case ite : InvocationTargetException => throw ite.getCause()
     }

src/main/scala/leon/evaluators/CodeGenEvaluator.scala

@@ -28,6 +28,7 @@ class CodeGenEvaluator(ctx : LeonContext, val unit : CompilationUnit) extends Ev
 
   override def compile(expression : Expr, argorder : Seq[Identifier]) : Option[Seq[Expr]=>EvaluationResult] = {
     import leon.codegen.runtime.LeonCodeGenRuntimeException
+    import leon.codegen.runtime.LeonCodeGenEvaluationException
 
     val ce = unit.compileExpression(expression, argorder)
 
@@ -41,13 +42,8 @@ class CodeGenEvaluator(ctx : LeonContext, val unit : CompilationUnit) extends Ev
         case e : LeonCodeGenRuntimeException =>
           EvaluationFailure(e.getMessage)
 
-        // Required, because the class may be loaded from a different classloader,
-        // and the check above would fail.
-        case t : Throwable if t.getClass.toString.endsWith("LeonCodeGenRuntimeException") => 
-          EvaluationFailure(t.getMessage)
-
-        case t : Throwable if t.getClass.toString.endsWith("LeonCodeGenEvaluationException") => 
-          EvaluationError(t.getMessage)
+        case e : LeonCodeGenEvaluationException =>
+          EvaluationError(e.getMessage)
       }
     })
   }

src/main/scala/leon/purescala/TypeTrees.scala

@@ -21,6 +21,8 @@ object TypeTrees {
       case Some(o) if o != tt => scala.sys.error("Resetting type information! Type [" + o + "] is modified to [" + tt)
       case _ => this
     }
+
+    def isTyped : Boolean = (getType != Untyped)
   }
 
   class TypeErrorException(msg: String) extends Exception(msg)