From dd96dbf7e4722ba49ddda621b027c6c7c0575bdf Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Tue, 15 Nov 2016 16:16:45 +0100
Subject: [PATCH] Tip printer fix for generic adt fields
---
src/main/scala/inox/tip/Printer.scala | 14 ++++++++++----
1 file changed, 10 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/inox/tip/Printer.scala b/src/main/scala/inox/tip/Printer.scala
index 1761d5db3..17395843a 100644
--- a/src/main/scala/inox/tip/Printer.scala
+++ b/src/main/scala/inox/tip/Printer.scala
@@ -143,7 +143,13 @@ class Printer(val program: InoxProgram, writer: Writer) extends solvers.smtlib.S
case _ => false
}
- for ((tpe, DataType(id, _)) <- adts) {
+ val (ours, externals) = adts.partition {
+ case (adt: ADTType, _) => adt == adt.getADT.definition.typed.toType
+ case (tpe @ TupleType(tps), _) => tpe == tuples(tps.size)
+ case _ => true
+ }
+
+ for ((tpe, DataType(id, _)) <- ours) {
val tparams: Seq[TypeParameter] = tpe match {
case ADTType(_, tps) => tps.map(_.asInstanceOf[TypeParameter])
case TupleType(tps) => tps.map(_.asInstanceOf[TypeParameter])
@@ -154,12 +160,12 @@ class Printer(val program: InoxProgram, writer: Writer) extends solvers.smtlib.S
sorts += tpe -> Sort(SMTIdentifier(id2sym(id)), tpSorts)
}
- val generics = adts.flatMap { case (tp, _) => typeParamsOf(tp) }.toSet
+ val generics = ours.flatMap { case (tp, _) => typeParamsOf(tp) }.toSet
val genericSyms = generics.map(tp => id2sym(tp.id))
- if (adts.nonEmpty) {
+ if (ours.nonEmpty) {
emit(DeclareDatatypesPar(genericSyms.toList,
- (for ((tpe, DataType(sym, cases)) <- adts.toList) yield {
+ (for ((tpe, DataType(sym, cases)) <- ours.toList) yield {
id2sym(sym) -> (for (c <- cases) yield {
val s = id2sym(c.sym)
--
GitLab