From 163702f9f34d16986f0e800038f8188b78dc9601 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Wed, 16 Nov 2016 18:00:11 +0100
Subject: [PATCH] Fix for tip parsing
---
src/it/scala/inox/tip/TipPrintingSuite.scala | 10 +++++-----
src/main/scala/inox/tip/Parser.scala | 2 +-
2 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/src/it/scala/inox/tip/TipPrintingSuite.scala b/src/it/scala/inox/tip/TipPrintingSuite.scala
index 8eb71ef04..ccce4fe17 100644
--- a/src/it/scala/inox/tip/TipPrintingSuite.scala
+++ b/src/it/scala/inox/tip/TipPrintingSuite.scala
@@ -10,8 +10,8 @@ class TipPrintingSuite extends FunSuite with ResourceUtils {
val ctx = TestContext.empty
- val files = resourceFiles("regression/tip/SAT", _.endsWith(".tip")).toList ++
- resourceFiles("regression/tip/UNSAT", _.endsWith(".tip"))
+ val files = resourceFiles("regression/tip/SAT", _.endsWith(".tip")).toList.map("SAT" -> _) ++
+ resourceFiles("regression/tip/UNSAT", _.endsWith(".tip")).map("UNSAT" -> _)
private def checkScript(syms: Symbols, expr: Expr): Unit = {
for (fd <- syms.functions.values) {
@@ -21,14 +21,14 @@ class TipPrintingSuite extends FunSuite with ResourceUtils {
assert(expr.getType(syms) != Untyped)
}
- for (file <- files) {
- test(s"Parsing file ${file.getName}") {
+ for ((cat, file) <- files) {
+ test(s"Parsing file $cat/${file.getName}") {
for ((syms, expr) <- new Parser(file).parseScript) {
checkScript(syms, expr)
}
}
- test(s"Re-printing file ${file.getName}") {
+ test(s"Re-printing file $cat/${file.getName}") {
for ((syms, expr) <- new Parser(file).parseScript) {
val program = InoxProgram(ctx, syms)
diff --git a/src/main/scala/inox/tip/Parser.scala b/src/main/scala/inox/tip/Parser.scala
index 422cedd2b..bacfda922 100644
--- a/src/main/scala/inox/tip/Parser.scala
+++ b/src/main/scala/inox/tip/Parser.scala
@@ -272,7 +272,7 @@ class Parser(file: File) {
)
).setPos(pred.optPos)
} else {
- extractTerm(pred)(locals.withVariable(s, vd.toVariable))
+ extractTerm(pred)(locals.withGenerics(syms zip root.typeArgs).withVariable(s, vd.toVariable))
}
val (optAdt, fd) = root.invariant(locals.symbols) match {
--
GitLab