diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index e5bb4b2af730bb0002887daf2e64e7333a5dc9e1..f4bb00795246d15d3148bfbaa01dc4e9a1afab1a 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -369,7 +369,7 @@ trait CodeGeneration {
ch << InvokeVirtual(MapClass, "add", s"(L$ObjectClass;L$ObjectClass;)V")
}
- case MapGet(m, k) =>
+ case MapApply(m, k) =>
val MapType(_, tt) = m.getType
mkExpr(m, ch)
mkBoxedExpr(k, ch)
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index c05355bdc4c2c2bbbc8b1d1f107c01f687d7dd8e..3f4a67f484dad28589684b4803d701316784860c 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -524,7 +524,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case f @ FiniteMap(ss, kT, vT) =>
FiniteMap(ss.map{ case (k, v) => (e(k), e(v)) }.distinct, kT, vT)
- case g @ MapGet(m,k) => (e(m), e(k)) match {
+ case g @ MapApply(m,k) => (e(m), e(k)) match {
case (FiniteMap(ss, _, _), e) => ss.find(_._1 == e) match {
case Some((_, v0)) => v0
case None => throw RuntimeError("Key not found: " + e.asString)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index f39b2947260ad39da151bdbb0a514f7687d12593..cc2d8938e5c1629e9ce27af4bd62d86e5cb2695a 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1639,19 +1639,19 @@ trait CodeExtraction extends ASTExtractors {
// Map methods
case (IsTyped(a1, MapType(_, vt)), "apply", List(a2)) =>
- MapGet(a1, a2)
+ MapApply(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(someClass, Seq(MapApply(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),
+ MapApply(a1, a2).setPos(current.pos),
a3)
case (IsTyped(a1, mt: MapType), "isDefinedAt", List(a2)) =>
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index f2ff6ea1b6b465c1f0a4c5edf9d19217e1e4ad46..69267f7afe5c87c2007f67911e23381bdae2f424 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -996,7 +996,7 @@ object ExprOps {
/** Rewrites all map accesses with additional error conditions. */
def mapGetWithChecks(expr: Expr): Expr = {
postMap({
- case mg @ MapGet(m,k) =>
+ case mg @ MapApply(m,k) =>
val ida = MapIsDefinedAt(m, k)
Some(IfExpr(ida, mg, Error(mg.getType, "Key not found for map access").copiedFrom(mg)).copiedFrom(mg))
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 1e3722565312e3157de6044351791b49a5235513..7882a6269774c32485c2584f63d1e728ebe81d65 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -778,8 +778,8 @@ object Expressions {
case class FiniteMap(singletons: Seq[(Expr, Expr)], keyType: TypeTree, valueType: TypeTree) extends Expr {
val getType = MapType(keyType, valueType).unveilUntyped
}
- /** $encodingof `map.get(key)` */
- case class MapGet(map: Expr, key: Expr) extends Expr {
+ /** $encodingof `map.apply(key)` (or `map(key)`)*/
+ case class MapApply(map: Expr, key: Expr) extends Expr {
val getType = map.getType match {
case MapType(from, to) if isSubtypeOf(key.getType, from) =>
to
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index bace7746c6c7d0eb86320ac36daae771ba34d58c..c8d54731ce53cb7ba6cd1dc8cdad769f0432181a 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -114,8 +114,8 @@ object Extractors {
Some(Seq(t1, t2), (es: Seq[Expr]) => SetUnion(es(0), es(1)))
case SetDifference(t1, t2) =>
Some(Seq(t1, t2), (es: Seq[Expr]) => SetDifference(es(0), es(1)))
- case mg@MapGet(t1, t2) =>
- Some(Seq(t1, t2), (es: Seq[Expr]) => MapGet(es(0), es(1)))
+ case mg@MapApply(t1, t2) =>
+ Some(Seq(t1, t2), (es: Seq[Expr]) => MapApply(es(0), es(1)))
case MapUnion(t1, t2) =>
Some(Seq(t1, t2), (es: Seq[Expr]) => MapUnion(es(0), es(1)))
case MapDifference(t1, t2) =>
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index a0b9207a07a42003fef911df88a29c83ca887af3..77c33a62dbcf7105034e1757c924c024f1abfc01 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -261,7 +261,7 @@ class PrettyPrinter(opts: PrinterOptions,
case SetDifference(l,r) => p"$l \\ $r"
case SetIntersection(l,r) => p"$l \u2229 $r"
case SetCardinality(s) => p"|$s|"
- case MapGet(m,k) => p"$m($k)"
+ case MapApply(m,k) => p"$m($k)"
case MapIsDefinedAt(m,k) => p"$m.isDefinedAt($k)"
case ArrayLength(a) => p"$a.length"
case ArraySelect(a, i) => p"$a($i)"
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index e90749e95c50764626d3b57cd3a9776087a8a6a7..aaf65f508e0d700ea08036734ba95d131e763781 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -435,7 +435,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
}.toMap, CaseClass(library.noneType(to), Seq())))
- case MapGet(m, k) =>
+ case MapApply(m, k) =>
val mt @ MapType(_, to) = m.getType
declareSort(mt)
// m(k) becomes
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 6aabf292f53608d970a67e8fb8bd66dc0c162213..07943a8b971900220ec2b2771ee320dae5896dea 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -508,7 +508,7 @@ trait AbstractZ3Solver extends Solver {
case (k, v) => (k, CaseClass(library.someType(t), Seq(v)))
}.toMap, CaseClass(library.noneType(t), Seq())))
- case MapGet(m, k) =>
+ case MapApply(m, k) =>
val mt @ MapType(_, t) = normalizeType(m.getType)
typeToSort(mt)
diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index 3c3d89f4859449195584c1bd28460da956ab37fb..871662815ff0efb3d5484c89e8b5569fa5c2a350 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -32,7 +32,7 @@ object InjectAsserts extends LeonPhase[Program, Program] {
).setPos(e))
case e @ ArrayUpdate(a, i, _) =>
Some(Assert(indexUpTo(i, ArrayLength(a)), Some("Array index out of range"), e).setPos(e))
- case e @ MapGet(m,k) =>
+ case e @ MapApply(m,k) =>
Some(Assert(MapIsDefinedAt(m, k), Some("Map undefined at this index"), e).setPos(e))
case e @ AsInstanceOf(expr, ct) =>