From df8ef8c828a794c6d2b96755db822969a4551dc8 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Tue, 11 Oct 2016 09:39:40 +0200
Subject: [PATCH] Fixed TIP parser for hex bitvectors & generalized identity
transformers in TreeOps
---
src/main/scala/inox/ast/TreeOps.scala | 8 ++++++--
src/main/scala/inox/tip/Parser.scala | 5 +----
2 files changed, 7 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/inox/ast/TreeOps.scala b/src/main/scala/inox/ast/TreeOps.scala
index a5cc023e1..973c25e22 100644
--- a/src/main/scala/inox/ast/TreeOps.scala
+++ b/src/main/scala/inox/ast/TreeOps.scala
@@ -19,7 +19,7 @@ trait TreeOps { self: Trees =>
} = self.deconstructor
}
- lazy val TreeIdentity = new SelfTreeTransformer {
+ class TreeIdentity extends SelfTreeTransformer {
override def transform(id: Identifier, tpe: s.Type): (Identifier, t.Type) = (id, tpe)
override def transform(v: s.Variable): t.Variable = v
override def transform(vd: s.ValDef): t.ValDef = vd
@@ -28,11 +28,15 @@ trait TreeOps { self: Trees =>
override def transform(flag: s.Flag): t.Flag = flag
}
- lazy val SymbolIdentity = new SymbolTransformer {
+ lazy val TreeIdentity: SelfTransformer = new TreeIdentity
+
+ class SymbolIdentity extends SymbolTransformer {
val transformer = TreeIdentity
override def transform(syms: s.Symbols): t.Symbols = syms
}
+ lazy val SymbolIdentity: SymbolTransformer { val transformer: SelfTransformer } = new SymbolIdentity
+
trait TreeTraverser {
def traverse(vd: ValDef): Unit = traverse(vd.tpe)
diff --git a/src/main/scala/inox/tip/Parser.scala b/src/main/scala/inox/tip/Parser.scala
index 613bdf879..51024b61a 100644
--- a/src/main/scala/inox/tip/Parser.scala
+++ b/src/main/scala/inox/tip/Parser.scala
@@ -380,10 +380,7 @@ class Parser(file: File) {
case SNumeral(n) =>
IntegerLiteral(n)
- // TODO: hexadecimal case
- //case SHexadecimal(value) => BVLiteral()
-
- case SBinary(bs) =>
+ case FixedSizeBitVectors.BitVectorLit(bs) =>
BVLiteral(BitSet.empty ++ bs.reverse.zipWithIndex.collect { case (true, i) => i }, bs.size)
case SDecimal(value) =>
--
GitLab