diff --git a/doc/purescala.rst b/doc/purescala.rst
index 004d37a133f1a14c12cf77162247c605d9796406..f3c40b5fd57e5620fa33e2872ef51f7bfeb4583a 100644
--- a/doc/purescala.rst
+++ b/doc/purescala.rst
@@ -297,6 +297,10 @@ Map
m isDefinedAt index
m contains index
m.updated(index, value)
+ m + (index -> value)
+ m + (value, index)
+ m.get(index)
+ m.getOrElse(index, value2)
Function
diff --git a/library/lang/Map.scala b/library/lang/Map.scala
index bd186b721d7d7d62a194366fceedabd55b04986d..368c028abd1622c8236615121c3f324e54feffc6 100644
--- a/library/lang/Map.scala
+++ b/library/lang/Map.scala
@@ -12,10 +12,21 @@ object Map {
}
@ignore
-case class Map[A, B](val theMap: scala.collection.immutable.Map[A,B]) {
+case class Map[A, B] (theMap: scala.collection.immutable.Map[A,B]) {
def apply(k: A): B = theMap.apply(k)
def ++(b: Map[A, B]): Map[A,B] = new Map (theMap ++ b.theMap)
def updated(k: A, v: B): Map[A,B] = new Map(theMap.updated(k, v))
def contains(a: A): Boolean = theMap.contains(a)
def isDefinedAt(a: A): Boolean = contains(a)
+
+ def +(kv: (A, B)): Map[A,B] = updated(kv._1, kv._2)
+ def +(k: A, v: B): Map[A,B] = updated(k, v)
+
+ def getOrElse(k: A, default: B): B = get(k).getOrElse(default)
+
+ def get(k: A): Option[B] = if (contains(k)) {
+ Some[B](apply(k))
+ } else {
+ None[B]()
+ }
}
diff --git a/library/collection/Option.scala b/library/lang/Option.scala
similarity index 98%
rename from library/collection/Option.scala
rename to library/lang/Option.scala
index 56feffdc0fc5b017b8b8a5dc9862d1f3a06d5811..0d77ef74e34fca33a583b96d0a2b6e26af17d74c 100644
--- a/library/collection/Option.scala
+++ b/library/lang/Option.scala
@@ -1,6 +1,6 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-package leon.collection
+package leon.lang
import leon.annotation._
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index b37b6672fe7c741e5c76e09408dd56bb2c55871d..2047200929bf3e3d9876e4e01f0ab5eefab34708 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -520,6 +520,7 @@ trait CodeExtraction extends ASTExtractors {
parent.foreach(_.classDef.registerChildren(ccd))
+
classesToClasses += sym -> ccd
val fields = args.map { case (symbol, t) =>
@@ -1704,6 +1705,19 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, MapType(_, vt)), "apply", List(a2)) =>
MapGet(a1, a2)
+ case (IsTyped(a1, MapType(_, vt)), "get", List(a2)) =>
+ val someClass = CaseClassType(libraryCaseClass(sym.pos, "leon.lang.Some"), Seq(vt))
+ val noneClass = CaseClassType(libraryCaseClass(sym.pos, "leon.lang.None"), Seq(vt))
+
+ IfExpr(MapIsDefinedAt(a1, a2).setPos(current.pos),
+ CaseClass(someClass, Seq(MapGet(a1, a2).setPos(current.pos))).setPos(current.pos),
+ CaseClass(noneClass, Seq()).setPos(current.pos))
+
+ case (IsTyped(a1, MapType(_, vt)), "getOrElse", List(a2, a3)) =>
+ IfExpr(MapIsDefinedAt(a1, a2).setPos(current.pos),
+ MapGet(a1, a2).setPos(current.pos),
+ a3)
+
case (IsTyped(a1, mt: MapType), "isDefinedAt", List(a2)) =>
MapIsDefinedAt(a1, a2)
@@ -1713,6 +1727,17 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, mt: MapType), "updated", List(k, v)) =>
MapUnion(a1, FiniteMap(Seq((k, v)), mt.from, mt.to))
+ case (IsTyped(a1, mt: MapType), "+", List(k, v)) =>
+ MapUnion(a1, FiniteMap(Seq((k, v)), mt.from, mt.to))
+
+ case (IsTyped(a1, mt: MapType), "+", List(IsTyped(kv, TupleType(List(_, _))))) =>
+ kv match {
+ case Tuple(List(k, v)) =>
+ MapUnion(a1, FiniteMap(Seq((k, v)), mt.from, mt.to))
+ case kv =>
+ MapUnion(a1, FiniteMap(Seq((TupleSelect(kv, 1), TupleSelect(kv, 2))), mt.from, mt.to))
+ }
+
case (IsTyped(a1, mt1: MapType), "++", List(IsTyped(a2, mt2: MapType))) if mt1 == mt2 =>
MapUnion(a1, a2)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 3df3f89e57d809ba8d1ba6ef2785dbd078a71333..ae77673d813e66d10a0e0a75451f0a0ef3ba82d1 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -225,7 +225,12 @@ abstract class SMTLIBSolver(val context: LeonContext,
case MapType(from, to) =>
// We expect a RawArrayValue with keys in from and values in Option[to],
// with default value == None
- require(from == r.keyTpe && r.default == OptionManager.mkLeonNone(to))
+ if (r.default != OptionManager.mkLeonNone(to)) {
+ reporter.warning("Co-finite maps are not supported. (Default was "+r.default+")")
+ throw new IllegalArgumentException
+ }
+ require(r.keyTpe == from, s"Type error in solver model, expected $from, found ${r.keyTpe}")
+
val elems = r.elems.flatMap {
case (k, CaseClass(leonSome, Seq(x))) => Some(k -> x)
case (k, _) => None
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
index 37efdd120ba60bcafb27cc325ad7c84782d6c587..cc6e2161c3ee3d7c1ebd0ee27546a13dfe56f403 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
@@ -156,6 +156,7 @@ class SMTLIBZ3Solver(context: LeonContext, program: Program) extends SMTLIBSolve
case DefineFun(SMTFunDef(a, Seq(SortedVar(arg, akind)), rkind, body)) =>
val (argTpe, retTpe) = tpe match {
case SetType(base) => (base, BooleanType)
+ case MapType(from, to) => (from, OptionManager.leonOptionType(to))
case ArrayType(base) => (Int32Type, base)
case FunctionType(args, ret) => (tupleTypeWrap(args), ret)
case RawArrayType(from, to) => (from, to)
diff --git a/src/main/scala/leon/utils/Library.scala b/src/main/scala/leon/utils/Library.scala
index f22169ba94f177f762fb114f8c3da7cf20880c43..e7c76c83165969a7cf12b32b6f96af12a1657010 100644
--- a/src/main/scala/leon/utils/Library.scala
+++ b/src/main/scala/leon/utils/Library.scala
@@ -11,9 +11,9 @@ case class Library(pgm: Program) {
lazy val Cons = lookup("leon.collection.Cons") collect { case ccd : CaseClassDef => ccd }
lazy val Nil = lookup("leon.collection.Nil") collect { case ccd : CaseClassDef => ccd }
- lazy val Option = lookup("leon.collection.Option") collect { case acd : AbstractClassDef => acd }
- lazy val Some = lookup("leon.collection.Some") collect { case ccd : CaseClassDef => ccd }
- lazy val None = lookup("leon.collection.None") collect { case ccd : CaseClassDef => ccd }
+ lazy val Option = lookup("leon.lang.Option") collect { case acd : AbstractClassDef => acd }
+ lazy val Some = lookup("leon.lang.Some") collect { case ccd : CaseClassDef => ccd }
+ lazy val None = lookup("leon.lang.None") collect { case ccd : CaseClassDef => ccd }
lazy val String = lookup("leon.lang.string.String") collect { case ccd : CaseClassDef => ccd }
diff --git a/src/test/resources/regression/frontends/passing/ImplicitDefs2.scala b/src/test/resources/regression/frontends/passing/ImplicitDefs2.scala
index a157e5dd6bf437d11ae0d1ea51cca47d6d3723e0..9f4b1a83fbb7dd4c6e4600d1030d083335344b62 100644
--- a/src/test/resources/regression/frontends/passing/ImplicitDefs2.scala
+++ b/src/test/resources/regression/frontends/passing/ImplicitDefs2.scala
@@ -3,7 +3,6 @@ package leon.blup
import leon._
import leon.lang._
import leon.annotation._
-import leon.collection.{Option,None,Some}
//import leon.proof._
// FIXME: the following should go into the leon.proof package object.
diff --git a/src/test/resources/regression/verification/purescala/valid/MapGetOrElse2.scala b/src/test/resources/regression/verification/purescala/valid/MapGetOrElse2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7b1e19418f09cdcf1df212934e7ca795780f4cf6
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/MapGetOrElse2.scala
@@ -0,0 +1,17 @@
+import leon.lang._
+
+object MapGetOrElse2 {
+ def test1(a: Map[BigInt, BigInt]) = {
+ require(!(a contains 0))
+ a.get(0)
+ } ensuring {
+ _ == None[BigInt]()
+ }
+
+ def test2(a: Map[BigInt, BigInt]) = {
+ require(!(a contains 0))
+ a.getOrElse(0, 0)
+ } ensuring {
+ _ == 0
+ }
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/MapPlus.scala b/src/test/resources/regression/verification/purescala/valid/MapPlus.scala
new file mode 100644
index 0000000000000000000000000000000000000000..86a3d6d22b15764f66be716052ab6737f63dda91
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/MapPlus.scala
@@ -0,0 +1,18 @@
+import leon.lang._
+
+object MapGetPlus {
+ def test1(a: Map[BigInt, BigInt]) = {
+ require(!(a contains 0))
+ val b = a + (0, 1)
+ val c = a + (BigInt(0) -> BigInt(1))
+ b(0) == c(0)
+ }.holds
+
+ def test2(a: Map[BigInt, BigInt]) = {
+ require(!(a contains 0))
+ val t = (BigInt(0) -> BigInt(1))
+ val b = a + (0, 1)
+ val c = a + t
+ b(0) == c(0)
+ }.holds
+}
diff --git a/testcases/repair/Parser/Parser.scala b/testcases/repair/Parser/Parser.scala
index 876652d8e5c94bff65b3172b190efbd9e82c5893..8d838f470d63d8e8967f53cf88b2a6bcaf98061c 100644
--- a/testcases/repair/Parser/Parser.scala
+++ b/testcases/repair/Parser/Parser.scala
@@ -1,4 +1,5 @@
import leon._
+import leon.lang._
import leon.collection._
object Parser {
diff --git a/testcases/repair/Parser/Parser1.scala b/testcases/repair/Parser/Parser1.scala
index 1a12b820cba019fb40ff3fe7ae8cc71849f1a85a..5fd18245f4cc6d62ecef9278ae29cfb9e8a16bd0 100644
--- a/testcases/repair/Parser/Parser1.scala
+++ b/testcases/repair/Parser/Parser1.scala
@@ -1,4 +1,5 @@
import leon._
+import leon.lang._
import leon.collection._
object Parser {
diff --git a/testcases/repair/Parser/Parser2.scala b/testcases/repair/Parser/Parser2.scala
index 24fef56869854373c8367981fc38dea19af49218..919132e04b7fe97ac81b836b02140eb42fb57b77 100644
--- a/testcases/repair/Parser/Parser2.scala
+++ b/testcases/repair/Parser/Parser2.scala
@@ -1,4 +1,5 @@
import leon._
+import leon.lang._
import leon.collection._
object Parser {
diff --git a/testcases/repair/Parser/Parser3.scala b/testcases/repair/Parser/Parser3.scala
index dcc8107f3e1e439e94c93083b5cb7370065678f5..cf11c4d3ff54ce42b6858f532e56a3f03e487fa0 100644
--- a/testcases/repair/Parser/Parser3.scala
+++ b/testcases/repair/Parser/Parser3.scala
@@ -1,4 +1,5 @@
import leon._
+import leon.lang._
import leon.collection._
object Parser {
diff --git a/testcases/repair/Parser/Parser4.scala b/testcases/repair/Parser/Parser4.scala
index dcc8107f3e1e439e94c93083b5cb7370065678f5..cf11c4d3ff54ce42b6858f532e56a3f03e487fa0 100644
--- a/testcases/repair/Parser/Parser4.scala
+++ b/testcases/repair/Parser/Parser4.scala
@@ -1,4 +1,5 @@
import leon._
+import leon.lang._
import leon.collection._
object Parser {
diff --git a/testcases/repair/Parser/Parser5.scala b/testcases/repair/Parser/Parser5.scala
index dcc8107f3e1e439e94c93083b5cb7370065678f5..cf11c4d3ff54ce42b6858f532e56a3f03e487fa0 100644
--- a/testcases/repair/Parser/Parser5.scala
+++ b/testcases/repair/Parser/Parser5.scala
@@ -1,4 +1,5 @@
import leon._
+import leon.lang._
import leon.collection._
object Parser {