Tip printing-parsing tests

src/it/scala/inox/tip/TipPrintingSuite.scala

+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package tip
+
+import org.scalatest._
+
+class TipPrintingSuite extends FunSuite with ResourceUtils {
+  import inox.trees._
+
+  val ctx = TestContext.empty
+
+  val files = resourceFiles("regression/tip/SAT", _.endsWith(".tip")).toList ++
+    resourceFiles("regression/tip/UNSAT", _.endsWith(".tip"))
+
+  private def checkScript(syms: Symbols, expr: Expr): Unit = {
+    for (fd <- syms.functions.values) {
+      assert(fd.fullBody.getType(syms) != Untyped)
+    }
+
+    assert(expr.getType(syms) != Untyped)
+  }
+
+  for (file <- files) {
+    test(s"Parsing file ${file.getName}") {
+      for ((syms, expr) <- new Parser(file).parseScript) {
+        checkScript(syms, expr)
+      }
+    }
+
+    test(s"Re-printing file ${file.getName}") {
+      for ((syms, expr) <- new Parser(file).parseScript) {
+        val program = InoxProgram(ctx, syms)
+
+        val file = java.io.File.createTempFile("test-output", ".tip")
+        val fw = new java.io.FileWriter(file, false)
+        val printer = new Printer(program, fw)
+        printer.printScript(expr)
+        printer.emit(smtlib.parser.Commands.CheckSat())
+        printer.free()
+
+        val Seq((newSyms, newExpr)) = new Parser(file).parseScript
+        file.delete()
+        checkScript(newSyms, newExpr)
+      }
+    }
+  }
+}

src/it/scala/inox/tip/TIPTestSuite.scala → src/it/scala/inox/tip/TipTestSuite.scala

@@ -6,13 +6,13 @@ package tip
 import solvers._
 import org.scalatest._
 
-class TIPTestSuite extends FunSuite with ResourceUtils {
+class TipTestSuite extends FunSuite with ResourceUtils {
 
   val ctx = TestContext.empty
 
   for (file <- resourceFiles("regression/tip/SAT", _.endsWith(".tip"))) {
     test(s"SAT - ${file.getName}") {
-      for ((syms, expr) <- new tip.Parser(file).parseScript) {
+      for ((syms, expr) <- new Parser(file).parseScript) {
         val program = InoxProgram(ctx, syms)
         assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(expr).isSAT)
       }
@@ -21,7 +21,7 @@ class TIPTestSuite extends FunSuite with ResourceUtils {
 
   for (file <- resourceFiles("regression/tip/UNSAT", _.endsWith(".tip"))) {
     test(s"UNSAT - ${file.getName}") {
-      for ((syms, expr) <- new tip.Parser(file).parseScript) {
+      for ((syms, expr) <- new Parser(file).parseScript) {
         val program = InoxProgram(ctx, syms)
         assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(expr).isUNSAT)
       }