diff --git a/library/lang/package.scala b/library/lang/package.scala index a598c251e702d2cf3253a2ebbd4278c24fce22dd..25e5027c161a5c67215ec301a390159d48f52f99 100644 --- a/library/lang/package.scala +++ b/library/lang/package.scala @@ -35,4 +35,18 @@ package object lang { try { tests(in) == out } catch { case _ : MatchError => true } } + @ignore + object BigInt { + def apply(b: Int): scala.math.BigInt = scala.math.BigInt(b) + def apply(b: String): scala.math.BigInt = scala.math.BigInt(b) + + def unapply(b: scala.math.BigInt): scala.Option[Int] = { + if(b > Integer.MIN_VALUE && b < Integer.MAX_VALUE) { + scala.Some(b.intValue()) + } else { + scala.None + } + } + } + } diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala index d469f0ce18be11333dbadc3b9237d5774e48029a..37f233b741c937e90b19babf8ef13b6b8d2c176f 100644 --- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala +++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala @@ -229,6 +229,8 @@ trait ASTExtractors { def unapply(tree: Tree): Option[Tree] = tree match { case Apply(ExSelected("scala", "package", "BigInt", "apply"), n :: Nil) => Some(n) + case Apply(ExSelected("leon", "lang", "package", "BigInt", "apply"), n :: Nil) => + Some(n) case _ => None } @@ -821,6 +823,15 @@ trait ASTExtractors { if(tree != null) Some((tree.selector, tree.cases)) else None } + object ExBigIntPattern { + def unapply(tree: UnApply): Option[Tree] = tree match { + case ua @ UnApply(Apply(ExSelected("leon", "lang", "package", "BigInt", "unapply"), _), List(l)) => + Some(l) + case _ => + None + } + } + object ExIsInstanceOf { def unapply(tree: TypeApply) : Option[(Tree, Tree)] = tree match { case TypeApply(Select(t, isInstanceOfName), typeTree :: Nil) if isInstanceOfName.toString == "isInstanceOf" => Some((typeTree, t)) diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala index 60e5f7a76fb187c990464d60b2e6ded2ecd2a7f2..ce7661ceb720a73ac72322b798bb134b9a4c121d 100644 --- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala +++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala @@ -993,6 +993,10 @@ trait CodeExtraction extends ASTExtractors { outOfSubsetError(a, "Invalid type "+a.tpe+" for .isInstanceOf") } + case ExBigIntPattern(n: Literal) => + val lit = InfiniteIntegerLiteral(BigInt(n.value.stringValue)) + (LiteralPattern(binder, lit), dctx) + case ExInt32Literal(i) => (LiteralPattern(binder, IntLiteral(i)), dctx) case ExBooleanLiteral(b) => (LiteralPattern(binder, BooleanLiteral(b)), dctx) case ExUnitLiteral() => (LiteralPattern(binder, UnitLiteral()), dctx) @@ -1277,9 +1281,9 @@ trait CodeExtraction extends ASTExtractors { val newValueRec = extractTree(newValue) ArrayUpdate(lhsRec, indexRec, newValueRec) - case ExBigIntLiteral(n: Literal) => { + case ExBigIntLiteral(n: Literal) => InfiniteIntegerLiteral(BigInt(n.value.stringValue)) - } + case ExBigIntLiteral(n) => outOfSubsetError(tr, "Non-literal BigInt constructor") case ExIntToBigInt(tree) => { diff --git a/src/test/resources/regression/frontends/passing/bigintExtr.scala b/src/test/resources/regression/frontends/passing/bigintExtr.scala new file mode 100644 index 0000000000000000000000000000000000000000..983bd750e44604aefc3eb171c5cfac666a2ba23f --- /dev/null +++ b/src/test/resources/regression/frontends/passing/bigintExtr.scala @@ -0,0 +1,9 @@ +import leon.lang._ +import leon.collection._ + +object Test { + def b(b: List[BigInt]) = b match { + case Cons(BigInt(42), Nil()) => true + case _ => false + } +}