From 4ee5234ab7c9f39a97807845d70e43c55d09f143 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 17 Apr 2015 19:56:47 +0200
Subject: [PATCH] Leon defines its own Maps
In order to have support for maps, you need to import leon.lang._
---
.../leon/frontends/scalac/ASTExtractors.scala | 9 +++-
.../frontends/scalac/CodeExtraction.scala | 41 ++++++++-----------
.../scala/leon/purescala/PrettyPrinter.scala | 5 +--
src/main/scala/leon/purescala/TypeOps.scala | 5 +++
.../frontends/passing/ImplicitDefs2.scala | 1 -
.../newsolvers/valid/LiteralMaps.scala | 1 +
.../newsolvers/valid/PositiveMap.scala | 2 +
.../purescala/valid/LiteralMaps.scala | 2 +
.../scala/leon/test/purescala/DataGen.scala | 3 +-
9 files changed, 39 insertions(+), 30 deletions(-)
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 6fab7051b..f7a40b953 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -25,9 +25,10 @@ trait ASTExtractors {
protected lazy val tuple3Sym = classFromName("scala.Tuple3")
protected lazy val tuple4Sym = classFromName("scala.Tuple4")
protected lazy val tuple5Sym = classFromName("scala.Tuple5")
- protected lazy val mapSym = classFromName("scala.collection.immutable.Map")
+ protected lazy val scalaMapSym = classFromName("scala.collection.immutable.Map")
protected lazy val scalaSetSym = classFromName("scala.collection.immutable.Set")
protected lazy val setSym = classFromName("leon.lang.Set")
+ protected lazy val mapSym = classFromName("leon.lang.Map")
protected lazy val optionClassSym = classFromName("scala.Option")
protected lazy val arraySym = classFromName("scala.Array")
protected lazy val someClassSym = classFromName("scala.Some")
@@ -65,10 +66,14 @@ trait ASTExtractors {
getResolvedTypeSym(sym) == scalaSetSym
}
- def isMapTraitSym(sym: Symbol) : Boolean = {
+ def isMapSym(sym: Symbol) : Boolean = {
getResolvedTypeSym(sym) == mapSym
}
+ def isScalaMapSym(sym: Symbol) : Boolean = {
+ getResolvedTypeSym(sym) == scalaMapSym
+ }
+
def isMultisetTraitSym(sym: Symbol) : Boolean = {
sym == multisetTraitSym
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 70a0eacf2..fd148e997 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1413,8 +1413,20 @@ trait CodeExtraction extends ASTExtractors {
case cct: CaseClassType =>
CaseClass(cct, args.map(extractTree))
- case SetType(underlying) =>
- finiteSet(args.map(extractTree).toSet, underlying)
+ case SetType(a) =>
+ finiteSet(args.map(extractTree).toSet, a)
+
+ case MapType(a, b) =>
+ val singletons: Seq[(LeonExpr, LeonExpr)] = args.collect {
+ case ExTuple(tpes, trees) if trees.size == 2 =>
+ (extractTree(trees(0)), extractTree(trees(1)))
+ }
+
+ if (singletons.size != args.size) {
+ outOfSubsetError(tr, "Some map elements could not be extracted as Tuple2")
+ }
+
+ finiteMap(singletons, a, b)
case _ =>
outOfSubsetError(tr, "Construction of a non-case class.")
@@ -1471,26 +1483,6 @@ trait CodeExtraction extends ASTExtractors {
val underlying = extractType(tt)
EmptyMultiset(underlying)
- case ExEmptyMap(ft, tt) =>
- val fromUnderlying = extractType(ft)
- val toUnderlying = extractType(tt)
- EmptyMap(fromUnderlying, toUnderlying)
-
- case ExLiteralMap(ft, tt, elems) =>
- val fromUnderlying = extractType(ft)
- val toUnderlying = extractType(tt)
-
- val singletons: Seq[(LeonExpr, LeonExpr)] = elems.collect {
- case ExTuple(tpes, trees) if trees.size == 2 =>
- (extractTree(trees(0)), extractTree(trees(1)))
- }
-
- if (singletons.size != elems.size) {
- outOfSubsetError(tr, "Some map elements could not be extracted as Tuple2")
- }
-
- finiteMap(singletons, fromUnderlying, toUnderlying)
-
case ExArrayFill(baseType, length, defaultValue) =>
val lengthRec = extractTree(length)
val defaultValueRec = extractTree(defaultValue)
@@ -1797,13 +1789,16 @@ trait CodeExtraction extends ASTExtractors {
case TypeRef(_, sym, btt :: Nil) if isScalaSetSym(sym) =>
outOfSubsetError(pos, "Scala's Set API is no longer extracted. Make sure you import leon.lang.Set that defines supported Set operations.")
+ case TypeRef(_, sym, List(a,b)) if isScalaMapSym(sym) =>
+ outOfSubsetError(pos, "Scala's Map API is no longer extracted. Make sure you import leon.lang.Map that defines supported Map operations.")
+
case TypeRef(_, sym, btt :: Nil) if isSetSym(sym) =>
SetType(extractType(btt))
case TypeRef(_, sym, btt :: Nil) if isMultisetTraitSym(sym) =>
MultisetType(extractType(btt))
- case TypeRef(_, sym, List(ftt,ttt)) if isMapTraitSym(sym) =>
+ case TypeRef(_, sym, List(ftt,ttt)) if isMapSym(sym) =>
MapType(extractType(ftt), extractType(ttt))
case TypeRef(_, sym, List(t1,t2)) if isTuple2(sym) =>
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index a4718d515..f5b82b8f4 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -372,7 +372,8 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case BVShiftLeft(l,r) => optP { p"$l << $r" }
case BVAShiftRight(l,r) => optP { p"$l >> $r" }
case BVLShiftRight(l,r) => optP { p"$l >>> $r" }
- case FiniteSet(rs) => p"{${rs.toSeq}}"
+ case fs @ FiniteSet(rs) => p"{${rs.toSeq}}"
+ case fm @ FiniteMap(rs) => p"{$rs}"
case FiniteMultiset(rs) => p"{|$rs|)"
case EmptyMultiset(_) => p"\u2205"
case Not(ElementOfSet(e,s)) => p"$e \u2209 $s"
@@ -435,8 +436,6 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case TypeParameterDef(tp) => p"$tp"
case TypeParameter(id) => p"$id"
- case FiniteMap(rs) =>
- p"{$rs}"
case IfExpr(c, t, ie : IfExpr) =>
optP {
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index c22bf4796..1f05a5d64 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -313,6 +313,11 @@ object TypeOps {
val SetType(tp) = s.getType
EmptySet(tpeSub(tp)).copiedFrom(s)
+ case m @ FiniteMap(elements) if elements.isEmpty =>
+ val MapType(a,b) = m.getType
+ EmptyMap(tpeSub(a), tpeSub(b)).copiedFrom(m)
+
+
case v @ Variable(id) if idsMap contains id =>
Variable(idsMap(id)).copiedFrom(v)
diff --git a/src/test/resources/regression/frontends/passing/ImplicitDefs2.scala b/src/test/resources/regression/frontends/passing/ImplicitDefs2.scala
index 1ab625164..a157e5dd6 100644
--- a/src/test/resources/regression/frontends/passing/ImplicitDefs2.scala
+++ b/src/test/resources/regression/frontends/passing/ImplicitDefs2.scala
@@ -7,7 +7,6 @@ import leon.collection.{Option,None,Some}
//import leon.proof._
// FIXME: the following should go into the leon.proof package object.
-import leon.annotation._
import scala.language.implicitConversions
object proof {
diff --git a/src/test/resources/regression/verification/newsolvers/valid/LiteralMaps.scala b/src/test/resources/regression/verification/newsolvers/valid/LiteralMaps.scala
index d6c07c261..0acd6c81e 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/LiteralMaps.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/LiteralMaps.scala
@@ -1,4 +1,5 @@
/* Copyright 2009-2014 EPFL, Lausanne */
+import leon.lang._
object LiteralMaps {
def test(): Map[Int, Int] = {
diff --git a/src/test/resources/regression/verification/newsolvers/valid/PositiveMap.scala b/src/test/resources/regression/verification/newsolvers/valid/PositiveMap.scala
index 0441ec26c..93c87331e 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/PositiveMap.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/PositiveMap.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
import leon.lang._
object PositiveMap {
diff --git a/src/test/resources/regression/verification/purescala/valid/LiteralMaps.scala b/src/test/resources/regression/verification/purescala/valid/LiteralMaps.scala
index 4ce05fd25..07894524a 100644
--- a/src/test/resources/regression/verification/purescala/valid/LiteralMaps.scala
+++ b/src/test/resources/regression/verification/purescala/valid/LiteralMaps.scala
@@ -1,5 +1,7 @@
/* Copyright 2009-2015 EPFL, Lausanne */
+import leon.lang._
+
object LiteralMaps {
def test(): Map[Int, Int] = {
Map(1 -> 2, 3 -> 4, (5, 6))
diff --git a/src/test/scala/leon/test/purescala/DataGen.scala b/src/test/scala/leon/test/purescala/DataGen.scala
index 3d47e364f..8fcc97be2 100644
--- a/src/test/scala/leon/test/purescala/DataGen.scala
+++ b/src/test/scala/leon/test/purescala/DataGen.scala
@@ -30,7 +30,8 @@ class DataGen extends LeonTestSuite {
}
test("Lists") {
- val p = """|object Program {
+ val p = """|import leon.lang._
+ |object Program {
| sealed abstract class List
| case class Cons(head : Int, tail : List) extends List
| case object Nil extends List
--
GitLab