From 83af620c1c591b72150026ca739f326c07d6590c Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Wed, 18 Feb 2015 13:11:42 +0100
Subject: [PATCH] Promote IntLiterals to BigIntLiterals when used in a
comparison
---
.../scala/leon/frontends/scalac/CodeExtraction.scala | 12 +++++++++---
1 file changed, 9 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index df19be74d..7acbe7175 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1335,11 +1335,17 @@ trait CodeExtraction extends ASTExtractors {
val rl = extractTree(l)
val rr = extractTree(r)
- (rl.getType, rr.getType) match {
- case (rt, lt) if isSubtypeOf(rt, lt) || isSubtypeOf(lt, rt) =>
+ (rl, rr) match {
+ case (IsTyped(_, rt), IsTyped(_, lt)) if isSubtypeOf(rt, lt) || isSubtypeOf(lt, rt) =>
Equals(rl, rr)
- case (rt, lt) =>
+ case (IntLiteral(v), IsTyped(_, IntegerType)) =>
+ Equals(InfiniteIntegerLiteral(v), rr)
+
+ case (IsTyped(_, IntegerType), IntLiteral(v)) =>
+ Equals(rl, InfiniteIntegerLiteral(v))
+
+ case (IsTyped(_, rt), IsTyped(_, lt)) =>
outOfSubsetError(tr, "Invalid comparison: (_: "+rt+") == (_: "+lt+")")
}
--
GitLab