From 800df59d55f211dc18cbe8fb67adb1dd9ea3b91a Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 3 Sep 2015 10:57:59 +0200
Subject: [PATCH] MapGet -> MapApply
---
src/main/scala/leon/codegen/CodeGeneration.scala | 2 +-
src/main/scala/leon/evaluators/RecursiveEvaluator.scala | 2 +-
src/main/scala/leon/frontends/scalac/CodeExtraction.scala | 6 +++---
src/main/scala/leon/purescala/ExprOps.scala | 2 +-
src/main/scala/leon/purescala/Expressions.scala | 4 ++--
src/main/scala/leon/purescala/Extractors.scala | 4 ++--
src/main/scala/leon/purescala/PrettyPrinter.scala | 2 +-
src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala | 2 +-
src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala | 2 +-
src/main/scala/leon/verification/InjectAsserts.scala | 2 +-
10 files changed, 14 insertions(+), 14 deletions(-)
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index e5bb4b2af..f4bb00795 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 c05355bdc..3f4a67f48 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 f39b29472..cc2d8938e 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 f2ff6ea1b..69267f7af 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 1e3722565..7882a6269 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 bace7746c..c8d54731c 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 a0b9207a0..77c33a62d 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 e90749e95..aaf65f508 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 6aabf292f..07943a8b9 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 3c3d89f48..871662815 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) =>
--
GitLab