From 002ef769d193513d993fe62bc783cd5173128aff Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Tue, 19 Sep 2023 21:52:28 +0200
Subject: [PATCH 1/8] start fixing triggers maps

---
 .../gobra/translator/context/Context.scala    |  2 ++
 .../combinators/FinalTypeEncoding.scala       |  1 +
 .../encodings/combinators/TypeEncoding.scala  | 28 +++++++++++++++++++
 .../combinators/TypeEncodingCombiner.scala    |  1 +
 .../encodings/maps/MapEncoding.scala          |  9 ++++++
 .../typeless/AssertionEncoding.scala          | 12 +-------
 6 files changed, 42 insertions(+), 11 deletions(-)

diff --git a/src/main/scala/viper/gobra/translator/context/Context.scala b/src/main/scala/viper/gobra/translator/context/Context.scala
index 259598ebb..e6aab54e5 100644
--- a/src/main/scala/viper/gobra/translator/context/Context.scala
+++ b/src/main/scala/viper/gobra/translator/context/Context.scala
@@ -87,6 +87,8 @@ trait Context {
 
   def expression(x: in.Expr): CodeWriter[vpr.Exp] = typeEncoding.finalExpression(this)(x)
 
+  def triggerExpr(x: in.TriggerExpr): CodeWriter[vpr.Exp] = typeEncoding.finalTriggerExpr(this)(x)
+
   def assertion(x: in.Assertion): CodeWriter[vpr.Exp] = typeEncoding.finalAssertion(this)(x)
 
   def invariant(x: in.Assertion): (CodeWriter[Unit], vpr.Exp) = typeEncoding.invariant(this)(x)
diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala
index 3b7a49e89..6434533d9 100644
--- a/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala
@@ -61,6 +61,7 @@ class FinalTypeEncoding(te: TypeEncoding) extends TypeEncoding {
   override def extendFunction(ctx: Context): in.Member ==> Extension[MemberWriter[vpr.Function]] = te.extendFunction(ctx) orElse { _ => identity }
   override def extendPredicate(ctx: Context): in.Member ==> Extension[MemberWriter[vpr.Predicate]] = te.extendPredicate(ctx) orElse { _ => identity }
   override def extendExpression(ctx: Context): in.Expr ==> Extension[CodeWriter[vpr.Exp]] = te.extendExpression(ctx) orElse { _ => identity }
+  override def extendTriggerExpr(ctx: Context): in.TriggerExpr ==> Extension[CodeWriter[vpr.Exp]] = te.extendTriggerExpr(ctx) orElse { _ => identity }
   override def extendAssertion(ctx: Context): in.Assertion ==> Extension[CodeWriter[vpr.Exp]] = te.extendAssertion(ctx) orElse { _ => identity }
   override def extendStatement(ctx: Context): in.Stmt ==> Extension[CodeWriter[vpr.Stmt]] = te.extendStatement(ctx) orElse { _ => identity }
 }
diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
index b130a0c2a..973f22040 100644
--- a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
@@ -233,6 +233,22 @@ trait TypeEncoding extends Generator {
     case in.Conversion(t2, expr :: t) if typ(ctx).isDefinedAt(t) && typ(ctx).isDefinedAt(t2) => ctx.expression(expr)
   }
 
+  // TODO: doc
+  // TODO: enable consistency checks on triggers when --checkConsistency
+  def triggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = PartialFunction.empty
+
+  /*
+  {
+    // use predicate access encoding but then take just the predicate access, i.e. remove `acc` and the permission amount:
+    case in.Accessible.Predicate(op) =>
+      for {
+        v <- ctx.assertion(in.Access(in.Accessible.Predicate(op), in.FullPerm(op.info))(op.info))
+        pap = v.asInstanceOf[vpr.PredicateAccessPredicate]
+      } yield pap.loc
+    case e: in.Expr => ctx.expression(e)
+  }
+  */
+
   /**
     * Encodes assertions.
     *
@@ -406,6 +422,18 @@ trait TypeEncoding extends Generator {
     val f = expression(ctx); { case n@f(v) => extendExpression(ctx).lift(n).fold(v)(_(v)) }
   }
 
+  /** Adds to the encoding of [[triggerExpr]]. The extension is applied to the result of the final trigger expression
+    * encoding.
+    */
+  def extendTriggerExpr(@unused ctx: Context): in.TriggerExpr ==> Extension[CodeWriter[vpr.Exp]] = PartialFunction.empty
+
+  final def finalTriggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = {
+    val f = triggerExpr(ctx);
+    {
+      case n@f(v) => extendTriggerExpr(ctx).lift(n).fold(v)(_(v))
+    }
+  }
+
   /** Adds to the encoding of [[assertion]]. The extension is applied to the result of the final assertion encoding. */
   def extendAssertion(@unused ctx: Context): in.Assertion ==> Extension[CodeWriter[vpr.Exp]] = PartialFunction.empty
   final def finalAssertion(ctx: Context): in.Assertion ==> CodeWriter[vpr.Exp] = {
diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncodingCombiner.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncodingCombiner.scala
index 81b646efd..d9d05577d 100644
--- a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncodingCombiner.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncodingCombiner.scala
@@ -64,6 +64,7 @@ abstract class TypeEncodingCombiner(encodings: Vector[TypeEncoding], defaults: V
   override def extendFunction(ctx: Context): in.Member ==> Extension[MemberWriter[vpr.Function]] = extender(_.extendFunction(ctx))
   override def extendPredicate(ctx: Context): in.Member ==> Extension[MemberWriter[vpr.Predicate]] = extender(_.extendPredicate(ctx))
   override def extendExpression(ctx: Context): in.Expr ==> Extension[CodeWriter[vpr.Exp]] = extender(_.extendExpression(ctx))
+  override def extendTriggerExpr(ctx: Context): in.TriggerExpr ==> Extension[CodeWriter[vpr.Exp]] = extender(_.extendTriggerExpr(ctx))
   override def extendAssertion(ctx: Context): in.Assertion ==> Extension[CodeWriter[vpr.Exp]] = extender(_.extendAssertion(ctx))
   override def extendStatement(ctx: Context): in.Stmt ==> Extension[CodeWriter[vpr.Stmt]] = extender(_.extendStatement(ctx))
 }
diff --git a/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala
index f8e9116ca..2667b7cfb 100644
--- a/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala
@@ -24,6 +24,9 @@ import viper.silver.verifier.reasons.AssertionFalse
 import viper.silver.verifier.{ErrorReason, errors => err}
 import viper.silver.{ast => vpr}
 
+// TODO: use macros to make the generated code readable?
+// TODO: remove call to assert2 when the condition is the true lit
+
 /**
   * Encoding for Go maps. Unlike slices, maps are not thread-safe;
   * thus, all concurrent accesses to maps must be synchronized. In particular,
@@ -111,6 +114,12 @@ class MapEncoding extends LeafTypeEncoding {
     }
   }
 
+  override def triggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = {
+    default(super.triggerExpr(ctx)) {
+      case in.IndexedExp(_ :: ctx.Map(_, _), _, _) => unit(vpr.TrueLit()())
+    }
+  }
+
   /**
     * Encodes the allocation of a new map
     *  [r := make(map[T1]T2, n)] ->
diff --git a/src/main/scala/viper/gobra/translator/encodings/typeless/AssertionEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/typeless/AssertionEncoding.scala
index 46c9b13d6..f9918f755 100644
--- a/src/main/scala/viper/gobra/translator/encodings/typeless/AssertionEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/typeless/AssertionEncoding.scala
@@ -106,20 +106,10 @@ class AssertionEncoding extends Encoding {
 
   def trigger(trigger: in.Trigger)(ctx: Context) : CodeWriter[vpr.Trigger] = {
     val (pos, info, errT) = trigger.vprMeta
-    for { expr <- sequence(trigger.exprs map (triggerExpr(_)(ctx))) }
+    for { expr <- sequence(trigger.exprs map ctx.triggerExpr)}
       yield vpr.Trigger(expr)(pos, info, errT)
   }
 
-  def triggerExpr(expr: in.TriggerExpr)(ctx: Context): CodeWriter[vpr.Exp] = expr match {
-    // use predicate access encoding but then take just the predicate access, i.e. remove `acc` and the permission amount:
-    case in.Accessible.Predicate(op) =>
-      for {
-        v <- ctx.assertion(in.Access(in.Accessible.Predicate(op), in.FullPerm(op.info))(op.info))
-        pap = v.asInstanceOf[vpr.PredicateAccessPredicate]
-      } yield pap.loc
-    case e: in.Expr => ctx.expression(e)
-  }
-
   def quantifier(vars: Vector[in.BoundVar], triggers: Vector[in.Trigger], body: in.Expr)(ctx: Context) : CodeWriter[(Seq[vpr.LocalVarDecl], Seq[vpr.Trigger], vpr.Exp)] = {
     val newVars = vars map ctx.variable
 

From 93798d6de672e0953972ef58754758448125056f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Thu, 21 Sep 2023 10:55:21 +0200
Subject: [PATCH 2/8] cleanup

---
 .../scala/viper/gobra/frontend/Desugar.scala  |  1 +
 .../typing/ghost/GhostExprTyping.scala        |  1 +
 .../gobra/translator/context/Context.scala    |  2 +-
 .../combinators/FinalTypeEncoding.scala       |  4 +-
 .../encodings/combinators/TypeEncoding.scala  | 22 ++--------
 .../combinators/TypeEncodingCombiner.scala    |  2 +-
 .../encodings/maps/MapEncoding.scala          | 40 ++++++++++++++++++-
 .../gobra/translator/util/ViperWriter.scala   |  8 +++-
 .../features/maps/maps-simple1.gobra          | 17 +++++---
 9 files changed, 68 insertions(+), 29 deletions(-)

diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala
index 9a0704d51..cf4cf6c0c 100644
--- a/src/main/scala/viper/gobra/frontend/Desugar.scala
+++ b/src/main/scala/viper/gobra/frontend/Desugar.scala
@@ -4304,6 +4304,7 @@ object Desugar extends LazyLogging {
         } yield underlyingType(dright.typ) match {
           case _: in.SequenceT | _: in.SetT => in.Contains(dleft, dright)(src)
           case _: in.MultisetT => in.LessCmp(in.IntLit(0)(src), in.Contains(dleft, dright)(src))(src)
+          case _: in.MapT => in.Contains(dleft, dright)(src)
           case t => violation(s"expected a sequence or (multi)set type, but got $t")
         }
 
diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala
index a49c58c22..d52d4d17a 100644
--- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala
+++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala
@@ -139,6 +139,7 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
       case PIn(left, right) => isExpr(left).out ++ isExpr(right).out ++ {
         underlyingType(exprType(right)) match {
           case t : GhostCollectionType => ghostComparableTypes.errors(exprType(left), t.elem)(expr)
+          case t : MapT => ghostComparableTypes.errors(exprType(left), t.key)(expr)
           case _ : AdtT => noMessages
           case t => error(right, s"expected a ghost collection, but got $t")
         }
diff --git a/src/main/scala/viper/gobra/translator/context/Context.scala b/src/main/scala/viper/gobra/translator/context/Context.scala
index e6aab54e5..224a5c613 100644
--- a/src/main/scala/viper/gobra/translator/context/Context.scala
+++ b/src/main/scala/viper/gobra/translator/context/Context.scala
@@ -87,7 +87,7 @@ trait Context {
 
   def expression(x: in.Expr): CodeWriter[vpr.Exp] = typeEncoding.finalExpression(this)(x)
 
-  def triggerExpr(x: in.TriggerExpr): CodeWriter[vpr.Exp] = typeEncoding.finalTriggerExpr(this)(x)
+  def triggerExpr(x: in.TriggerExpr): CodeWriter[vpr.Exp] = typeEncoding.triggerExpr(this)(x)
 
   def assertion(x: in.Assertion): CodeWriter[vpr.Exp] = typeEncoding.finalAssertion(this)(x)
 
diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala
index 6434533d9..21144f527 100644
--- a/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala
@@ -46,6 +46,9 @@ class FinalTypeEncoding(te: TypeEncoding) extends TypeEncoding {
   override def equal(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = te.equal(ctx) orElse expectedMatch("equal")
   override def goEqual(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = te.goEqual(ctx) orElse expectedMatch("equal")
   override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = te.expression(ctx) orElse expectedMatch("expression")
+  override def triggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = te.triggerExpr(ctx) orElse {
+    case e: in.Expr => te.expression(ctx)(e)
+  }
   override def assertion(ctx: Context): in.Assertion ==> CodeWriter[vpr.Exp] = te.assertion(ctx) orElse expectedMatch("assertion")
   override def reference(ctx: Context): in.Location ==> CodeWriter[vpr.Exp] = te.reference(ctx) orElse expectedMatch("reference")
   override def addressFootprint(ctx: Context): (in.Location, in.Expr) ==> CodeWriter[vpr.Exp] = te.addressFootprint(ctx) orElse expectedMatch("addressFootprint")
@@ -61,7 +64,6 @@ class FinalTypeEncoding(te: TypeEncoding) extends TypeEncoding {
   override def extendFunction(ctx: Context): in.Member ==> Extension[MemberWriter[vpr.Function]] = te.extendFunction(ctx) orElse { _ => identity }
   override def extendPredicate(ctx: Context): in.Member ==> Extension[MemberWriter[vpr.Predicate]] = te.extendPredicate(ctx) orElse { _ => identity }
   override def extendExpression(ctx: Context): in.Expr ==> Extension[CodeWriter[vpr.Exp]] = te.extendExpression(ctx) orElse { _ => identity }
-  override def extendTriggerExpr(ctx: Context): in.TriggerExpr ==> Extension[CodeWriter[vpr.Exp]] = te.extendTriggerExpr(ctx) orElse { _ => identity }
   override def extendAssertion(ctx: Context): in.Assertion ==> Extension[CodeWriter[vpr.Exp]] = te.extendAssertion(ctx) orElse { _ => identity }
   override def extendStatement(ctx: Context): in.Stmt ==> Extension[CodeWriter[vpr.Stmt]] = te.extendStatement(ctx) orElse { _ => identity }
 }
diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
index 973f22040..5d30ff2e2 100644
--- a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
@@ -234,20 +234,18 @@ trait TypeEncoding extends Generator {
   }
 
   // TODO: doc
+  // TODO: optimize assert2(true, ...)
+  // TODO: key in map, instead of key in domain(map)
   // TODO: enable consistency checks on triggers when --checkConsistency
-  def triggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = PartialFunction.empty
-
-  /*
-  {
+  def triggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = {
     // use predicate access encoding but then take just the predicate access, i.e. remove `acc` and the permission amount:
     case in.Accessible.Predicate(op) =>
       for {
         v <- ctx.assertion(in.Access(in.Accessible.Predicate(op), in.FullPerm(op.info))(op.info))
         pap = v.asInstanceOf[vpr.PredicateAccessPredicate]
       } yield pap.loc
-    case e: in.Expr => ctx.expression(e)
+    // case e: in.Expr => ctx.expression(e)
   }
-  */
 
   /**
     * Encodes assertions.
@@ -422,18 +420,6 @@ trait TypeEncoding extends Generator {
     val f = expression(ctx); { case n@f(v) => extendExpression(ctx).lift(n).fold(v)(_(v)) }
   }
 
-  /** Adds to the encoding of [[triggerExpr]]. The extension is applied to the result of the final trigger expression
-    * encoding.
-    */
-  def extendTriggerExpr(@unused ctx: Context): in.TriggerExpr ==> Extension[CodeWriter[vpr.Exp]] = PartialFunction.empty
-
-  final def finalTriggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = {
-    val f = triggerExpr(ctx);
-    {
-      case n@f(v) => extendTriggerExpr(ctx).lift(n).fold(v)(_(v))
-    }
-  }
-
   /** Adds to the encoding of [[assertion]]. The extension is applied to the result of the final assertion encoding. */
   def extendAssertion(@unused ctx: Context): in.Assertion ==> Extension[CodeWriter[vpr.Exp]] = PartialFunction.empty
   final def finalAssertion(ctx: Context): in.Assertion ==> CodeWriter[vpr.Exp] = {
diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncodingCombiner.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncodingCombiner.scala
index d9d05577d..c4e80a245 100644
--- a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncodingCombiner.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncodingCombiner.scala
@@ -49,6 +49,7 @@ abstract class TypeEncodingCombiner(encodings: Vector[TypeEncoding], defaults: V
   override def equal(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = combiner(_.equal(ctx))
   override def goEqual(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = combiner(_.goEqual(ctx))
   override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = combiner(_.expression(ctx))
+  override def triggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = combiner(_.triggerExpr(ctx))
   override def assertion(ctx: Context): in.Assertion ==> CodeWriter[vpr.Exp] = combiner(_.assertion(ctx))
   override def reference(ctx: Context): in.Location ==> CodeWriter[vpr.Exp] = combiner(_.reference(ctx))
   override def addressFootprint(ctx: Context): (in.Location, in.Expr) ==> CodeWriter[vpr.Exp] = combiner(_.addressFootprint(ctx))
@@ -64,7 +65,6 @@ abstract class TypeEncodingCombiner(encodings: Vector[TypeEncoding], defaults: V
   override def extendFunction(ctx: Context): in.Member ==> Extension[MemberWriter[vpr.Function]] = extender(_.extendFunction(ctx))
   override def extendPredicate(ctx: Context): in.Member ==> Extension[MemberWriter[vpr.Predicate]] = extender(_.extendPredicate(ctx))
   override def extendExpression(ctx: Context): in.Expr ==> Extension[CodeWriter[vpr.Exp]] = extender(_.extendExpression(ctx))
-  override def extendTriggerExpr(ctx: Context): in.TriggerExpr ==> Extension[CodeWriter[vpr.Exp]] = extender(_.extendTriggerExpr(ctx))
   override def extendAssertion(ctx: Context): in.Assertion ==> Extension[CodeWriter[vpr.Exp]] = extender(_.extendAssertion(ctx))
   override def extendStatement(ctx: Context): in.Stmt ==> Extension[CodeWriter[vpr.Stmt]] = extender(_.extendStatement(ctx))
 }
diff --git a/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala
index 2667b7cfb..5867590f3 100644
--- a/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala
@@ -61,6 +61,7 @@ class MapEncoding extends LeafTypeEncoding {
     * R[ (e: map[K]V)[idx] ] -> [e] == null? [ dflt(V) ] : goMapLookup(e[idx])
     * R[ keySet(e: map[K]V) ] -> [e] == null? 0 : MapDomain(getCorrespondingMap(e))
     * R[ valueSet(e: map[K]V) ] -> [e] == null? 0 : MapRange(getCorrespondingMap(e))
+    * TODO: doc contains
     */
   override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = {
     def goE(x: in.Expr): CodeWriter[vpr.Exp] = ctx.expression(x)
@@ -88,6 +89,15 @@ class MapEncoding extends LeafTypeEncoding {
 
       case l@in.IndexedExp(_ :: ctx.Map(_, _), _, _) => for {(res, _) <- goMapLookup(l)(ctx)} yield res
 
+      case l@in.Contains(key, exp :: ctx.Map(keys, values)) =>
+        for {
+          keyVpr <- goE(key)
+          isComp <- MapEncoding.checkKeyComparability(key)(ctx)
+          correspondingMap <- getCorrespondingMap(exp, keys, values)(ctx)
+          containsExp = withSrc(vpr.MapContains(keyVpr, correspondingMap), l)
+          checkCompAndContains <- assert(isComp, containsExp, comparabilityErrorT)(ctx)
+        } yield checkCompAndContains
+
       case k@in.MapKeys(mapExp :: ctx.Map(keys, values), _) =>
         for {
           vprMap <- goE(mapExp)
@@ -116,7 +126,35 @@ class MapEncoding extends LeafTypeEncoding {
 
   override def triggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = {
     default(super.triggerExpr(ctx)) {
-      case in.IndexedExp(_ :: ctx.Map(_, _), _, _) => unit(vpr.TrueLit()())
+      case l@in.IndexedExp(m :: ctx.Map(keys, values), idx, _) =>
+        for {
+          vIdx <- ctx.expression(idx)
+          correspondingMap <- getCorrespondingMap(m, keys, values)(ctx)
+          lookupRes = withSrc(vpr.MapLookup(correspondingMap, vIdx), l)
+        } yield lookupRes
+
+      case l@in.Contains(key, m :: ctx.Map(keys, values)) =>
+        for {
+          vKey <- ctx.expression(key)
+          correspondingMap <- getCorrespondingMap(m, keys, values)(ctx)
+          contains = withSrc(vpr.MapContains(correspondingMap, vKey), l)
+        } yield contains
+
+      case l@in.Contains(key, in.MapKeys(m :: ctx.Map(keys, values), _)) =>
+        for {
+          vKey <- ctx.expression(key)
+          correspondingMap <- getCorrespondingMap(m, keys, values)(ctx)
+          vDomainMap = withSrc(vpr.MapDomain(correspondingMap), l)
+          contains = withSrc(vpr.AnySetContains(vKey, vDomainMap), l)
+        } yield contains
+
+      case l@in.Contains(key, in.MapValues(m :: ctx.Map(keys, values), _)) =>
+        for {
+          vKey <- ctx.expression(key)
+          correspondingMap <- getCorrespondingMap(m, keys, values)(ctx)
+          vRangeMap = withSrc(vpr.MapRange(correspondingMap), l)
+          contains = withSrc(vpr.AnySetContains(vKey, vRangeMap), l)
+        } yield contains
     }
   }
 
diff --git a/src/main/scala/viper/gobra/translator/util/ViperWriter.scala b/src/main/scala/viper/gobra/translator/util/ViperWriter.scala
index de0f8bc67..cbbf6ae82 100644
--- a/src/main/scala/viper/gobra/translator/util/ViperWriter.scala
+++ b/src/main/scala/viper/gobra/translator/util/ViperWriter.scala
@@ -399,8 +399,12 @@ object ViperWriter {
     /* Can be used in expressions. */
     def assert(cond: vpr.Exp, exp: vpr.Exp, reasonT: (Source.Verifier.Info, ErrorReason) => VerificationError)(ctx: Context): Writer[vpr.Exp] = {
       // In the future, this might do something more sophisticated
-      val (res, errT) = ctx.condition.assert(cond, exp, reasonT)
-      errorT(errT).map(_ => res)
+      if (cond.isInstanceOf[vpr.TrueLit]) {
+        unit(exp)
+      } else {
+        val (res, errT) = ctx.condition.assert(cond, exp, reasonT)
+        errorT(errT).map(_ => res)
+      }
     }
 
     /* Emits Viper statements. */
diff --git a/src/test/resources/regressions/features/maps/maps-simple1.gobra b/src/test/resources/regressions/features/maps/maps-simple1.gobra
index 8a53e22cd..e98f05d1a 100644
--- a/src/test/resources/regressions/features/maps/maps-simple1.gobra
+++ b/src/test/resources/regressions/features/maps/maps-simple1.gobra
@@ -52,6 +52,9 @@ func test6() {
 	m[3] = 10
 	v3, ok3 := m[3]
 	assert ok3 && v3 == 10
+
+	// check if key exists in the map
+	assert 3 in m
 }
 
 type T struct {
@@ -110,24 +113,24 @@ func test11() {
 requires acc(m, _)
 requires "key" in domain(m)
 func test12(m map[string]string) (r string){
-    return m["key"]
+	return m["key"]
 }
 
 requires acc(m, _)
 requires "value" in range(m)
 func test13(m map[string]string) {
-    assert exists k string :: m[k] == "value"
+	assert exists k string :: m[k] == "value"
 }
 
 func test14() (res map[int]int) {
 	x := 1
 	y := 2
-    m := map[int]int{x: y, y: x}
+	m := map[int]int{x: y, y: x}
 	return m
 }
 
 func test15() (res map[int]int) {
-    m := map[int]int{C1: C2, C2: C1}
+	m := map[int]int{C1: C2, C2: C1}
 	return m
 }
 
@@ -137,4 +140,8 @@ func test16() {
 	assert x == 0
 	x, contained := m[2]
 	assert x == 0 && !contained
-}
\ No newline at end of file
+}
+
+requires m != nil ==> acc(m)
+requires forall s string :: { s in domain(m) } s in domain(m) ==> acc(m[s])
+func test17(m map[string]*int) {}

From 5cd4b21ec574a7618ae78a88bbe52a3240535598 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Thu, 21 Sep 2023 11:58:17 +0200
Subject: [PATCH 3/8] fix issues with 'contains' in maps and with trigger
 generation

---
 .../encodings/combinators/FinalTypeEncoding.scala  |  6 ++++++
 .../encodings/combinators/TypeEncoding.scala       | 13 +------------
 .../translator/encodings/maps/MapEncoding.scala    | 14 +++++++++-----
 .../regressions/features/maps/maps-simple1.gobra   |  8 ++++++++
 4 files changed, 24 insertions(+), 17 deletions(-)

diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala
index 21144f527..6665e9fb2 100644
--- a/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala
@@ -47,6 +47,12 @@ class FinalTypeEncoding(te: TypeEncoding) extends TypeEncoding {
   override def goEqual(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = te.goEqual(ctx) orElse expectedMatch("equal")
   override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = te.expression(ctx) orElse expectedMatch("expression")
   override def triggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = te.triggerExpr(ctx) orElse {
+    // use predicate access encoding but then take just the predicate access, i.e. remove `acc` and the permission amount:
+    case in.Accessible.Predicate(op) =>
+      for {
+        v <- ctx.assertion(in.Access(in.Accessible.Predicate(op), in.FullPerm(op.info))(op.info))
+        pap = v.asInstanceOf[vpr.PredicateAccessPredicate]
+      } yield pap.loc
     case e: in.Expr => te.expression(ctx)(e)
   }
   override def assertion(ctx: Context): in.Assertion ==> CodeWriter[vpr.Exp] = te.assertion(ctx) orElse expectedMatch("assertion")
diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
index 5d30ff2e2..a41fb5f28 100644
--- a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
@@ -234,18 +234,7 @@ trait TypeEncoding extends Generator {
   }
 
   // TODO: doc
-  // TODO: optimize assert2(true, ...)
-  // TODO: key in map, instead of key in domain(map)
-  // TODO: enable consistency checks on triggers when --checkConsistency
-  def triggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = {
-    // use predicate access encoding but then take just the predicate access, i.e. remove `acc` and the permission amount:
-    case in.Accessible.Predicate(op) =>
-      for {
-        v <- ctx.assertion(in.Access(in.Accessible.Predicate(op), in.FullPerm(op.info))(op.info))
-        pap = v.asInstanceOf[vpr.PredicateAccessPredicate]
-      } yield pap.loc
-    // case e: in.Expr => ctx.expression(e)
-  }
+  def triggerExpr(@unused ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = PartialFunction.empty
 
   /**
     * Encodes assertions.
diff --git a/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala
index 5867590f3..9f3e5e8dd 100644
--- a/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala
@@ -24,9 +24,6 @@ import viper.silver.verifier.reasons.AssertionFalse
 import viper.silver.verifier.{ErrorReason, errors => err}
 import viper.silver.{ast => vpr}
 
-// TODO: use macros to make the generated code readable?
-// TODO: remove call to assert2 when the condition is the true lit
-
 /**
   * Encoding for Go maps. Unlike slices, maps are not thread-safe;
   * thus, all concurrent accesses to maps must be synchronized. In particular,
@@ -91,10 +88,16 @@ class MapEncoding extends LeafTypeEncoding {
 
       case l@in.Contains(key, exp :: ctx.Map(keys, values)) =>
         for {
+          mapVpr <- goE(exp)
           keyVpr <- goE(key)
           isComp <- MapEncoding.checkKeyComparability(key)(ctx)
           correspondingMap <- getCorrespondingMap(exp, keys, values)(ctx)
-          containsExp = withSrc(vpr.MapContains(keyVpr, correspondingMap), l)
+          containsExp =
+            withSrc(vpr.CondExp(
+              withSrc(vpr.EqCmp(mapVpr, withSrc(vpr.NullLit(), l)), l),
+              withSrc(vpr.FalseLit(), l),
+              withSrc(vpr.MapContains(keyVpr, correspondingMap), l)
+            ), l)
           checkCompAndContains <- assert(isComp, containsExp, comparabilityErrorT)(ctx)
         } yield checkCompAndContains
 
@@ -124,6 +127,7 @@ class MapEncoding extends LeafTypeEncoding {
     }
   }
 
+  // TODO: doc
   override def triggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = {
     default(super.triggerExpr(ctx)) {
       case l@in.IndexedExp(m :: ctx.Map(keys, values), idx, _) =>
@@ -137,7 +141,7 @@ class MapEncoding extends LeafTypeEncoding {
         for {
           vKey <- ctx.expression(key)
           correspondingMap <- getCorrespondingMap(m, keys, values)(ctx)
-          contains = withSrc(vpr.MapContains(correspondingMap, vKey), l)
+          contains = withSrc(vpr.MapContains(vKey, correspondingMap), l)
         } yield contains
 
       case l@in.Contains(key, in.MapKeys(m :: ctx.Map(keys, values), _)) =>
diff --git a/src/test/resources/regressions/features/maps/maps-simple1.gobra b/src/test/resources/regressions/features/maps/maps-simple1.gobra
index e98f05d1a..571d8437a 100644
--- a/src/test/resources/regressions/features/maps/maps-simple1.gobra
+++ b/src/test/resources/regressions/features/maps/maps-simple1.gobra
@@ -145,3 +145,11 @@ func test16() {
 requires m != nil ==> acc(m)
 requires forall s string :: { s in domain(m) } s in domain(m) ==> acc(m[s])
 func test17(m map[string]*int) {}
+
+requires m != nil ==> acc(m)
+requires forall s string :: { s in m } s in m ==> acc(m[s])
+func test18(m map[string]*int) {}
+
+requires m != nil ==> acc(m)
+requires forall i int :: { i in range(m) } i in range(m) ==> 0 < i
+func test19(m map[string]int) {}
\ No newline at end of file

From f23467b48602b20b6011896cc1e8a30f87cf755f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Fri, 22 Sep 2023 16:10:47 +0200
Subject: [PATCH 4/8] backup

---
 .../context/DfltTranslatorConfig.scala        |  5 ++--
 .../combinators/FinalTypeEncoding.scala       | 10 +------
 .../defaults/DefaultTriggerExprEncoding.scala | 27 +++++++++++++++++++
 3 files changed, 31 insertions(+), 11 deletions(-)
 create mode 100644 src/main/scala/viper/gobra/translator/encodings/defaults/DefaultTriggerExprEncoding.scala

diff --git a/src/main/scala/viper/gobra/translator/context/DfltTranslatorConfig.scala b/src/main/scala/viper/gobra/translator/context/DfltTranslatorConfig.scala
index 4361f570a..04825342f 100644
--- a/src/main/scala/viper/gobra/translator/context/DfltTranslatorConfig.scala
+++ b/src/main/scala/viper/gobra/translator/context/DfltTranslatorConfig.scala
@@ -16,7 +16,7 @@ import viper.gobra.translator.encodings.closures.ClosureEncoding
 import viper.gobra.translator.encodings.combinators.{DefaultEncoding, FinalTypeEncoding, SafeTypeEncodingCombiner, TypeEncoding}
 import viper.gobra.translator.encodings.interfaces.InterfaceEncoding
 import viper.gobra.translator.encodings.maps.{MapEncoding, MathematicalMapEncoding}
-import viper.gobra.translator.encodings.defaults.{DefaultGlobalVarEncoding, DefaultMethodEncoding, DefaultPredicateEncoding, DefaultPureMethodEncoding}
+import viper.gobra.translator.encodings.defaults.{DefaultGlobalVarEncoding, DefaultMethodEncoding, DefaultPredicateEncoding, DefaultPureMethodEncoding, DefaultTriggerExprEncoding}
 import viper.gobra.translator.encodings.options.OptionEncoding
 import viper.gobra.translator.encodings.preds.PredEncoding
 import viper.gobra.translator.encodings.sequences.SequenceEncoding
@@ -61,6 +61,7 @@ class DfltTranslatorConfig(
   val pureMethodEncoding = new DefaultPureMethodEncoding
   val predicateEncoding = new DefaultPredicateEncoding
   val globalVarEncoding = new DefaultGlobalVarEncoding
+  val triggerExprEncoding = new DefaultTriggerExprEncoding
 
   val typeEncoding: TypeEncoding = new FinalTypeEncoding(
     new SafeTypeEncodingCombiner(Vector(
@@ -73,7 +74,7 @@ class DfltTranslatorConfig(
       new TerminationEncoding, new BuiltInEncoding, new OutlineEncoding, new DeferEncoding,
       new GlobalEncoding, new Comments,
     ), Vector(
-      methodEncoding, pureMethodEncoding, predicateEncoding, globalVarEncoding
+      methodEncoding, pureMethodEncoding, predicateEncoding, globalVarEncoding, triggerExprEncoding
     ))
   )
 
diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala
index 6665e9fb2..0bd923b91 100644
--- a/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala
@@ -46,15 +46,7 @@ class FinalTypeEncoding(te: TypeEncoding) extends TypeEncoding {
   override def equal(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = te.equal(ctx) orElse expectedMatch("equal")
   override def goEqual(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = te.goEqual(ctx) orElse expectedMatch("equal")
   override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = te.expression(ctx) orElse expectedMatch("expression")
-  override def triggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = te.triggerExpr(ctx) orElse {
-    // use predicate access encoding but then take just the predicate access, i.e. remove `acc` and the permission amount:
-    case in.Accessible.Predicate(op) =>
-      for {
-        v <- ctx.assertion(in.Access(in.Accessible.Predicate(op), in.FullPerm(op.info))(op.info))
-        pap = v.asInstanceOf[vpr.PredicateAccessPredicate]
-      } yield pap.loc
-    case e: in.Expr => te.expression(ctx)(e)
-  }
+  override def triggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = te.triggerExpr(ctx) orElse
   override def assertion(ctx: Context): in.Assertion ==> CodeWriter[vpr.Exp] = te.assertion(ctx) orElse expectedMatch("assertion")
   override def reference(ctx: Context): in.Location ==> CodeWriter[vpr.Exp] = te.reference(ctx) orElse expectedMatch("reference")
   override def addressFootprint(ctx: Context): (in.Location, in.Expr) ==> CodeWriter[vpr.Exp] = te.addressFootprint(ctx) orElse expectedMatch("addressFootprint")
diff --git a/src/main/scala/viper/gobra/translator/encodings/defaults/DefaultTriggerExprEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/defaults/DefaultTriggerExprEncoding.scala
new file mode 100644
index 000000000..591107b1f
--- /dev/null
+++ b/src/main/scala/viper/gobra/translator/encodings/defaults/DefaultTriggerExprEncoding.scala
@@ -0,0 +1,27 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2023 ETH Zurich.
+
+package viper.gobra.translator.encodings.defaults
+
+import org.bitbucket.inkytonik.kiama.==>
+import viper.gobra.ast.{internal => in}
+import viper.gobra.translator.context.Context
+import viper.gobra.translator.encodings.combinators.Encoding
+import viper.silver.{ast => vpr}
+
+class DefaultTriggerExprEncoding extends Encoding {
+  import viper.gobra.translator.util.ViperWriter._
+
+  override def triggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = {
+    // use predicate access encoding but then take just the predicate access, i.e. remove `acc` and the permission amount:
+    case in.Accessible.Predicate(op) =>
+      for {
+        v <- ctx.assertion(in.Access(in.Accessible.Predicate(op), in.FullPerm(op.info))(op.info))
+        pap = v.asInstanceOf[vpr.PredicateAccessPredicate]
+      } yield pap.loc
+    case e: in.Expr => ctx.expression(e)
+  }
+}

From d0cad5303b7f94b794e23552d487e0741e572108 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Fri, 22 Sep 2023 16:18:36 +0200
Subject: [PATCH 5/8] backup

---
 .../translator/encodings/combinators/FinalTypeEncoding.scala    | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala
index 0bd923b91..b6731e0f1 100644
--- a/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/combinators/FinalTypeEncoding.scala
@@ -46,7 +46,7 @@ class FinalTypeEncoding(te: TypeEncoding) extends TypeEncoding {
   override def equal(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = te.equal(ctx) orElse expectedMatch("equal")
   override def goEqual(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = te.goEqual(ctx) orElse expectedMatch("equal")
   override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = te.expression(ctx) orElse expectedMatch("expression")
-  override def triggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = te.triggerExpr(ctx) orElse
+  override def triggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = te.triggerExpr(ctx) orElse expectedMatch("trigger expression")
   override def assertion(ctx: Context): in.Assertion ==> CodeWriter[vpr.Exp] = te.assertion(ctx) orElse expectedMatch("assertion")
   override def reference(ctx: Context): in.Location ==> CodeWriter[vpr.Exp] = te.reference(ctx) orElse expectedMatch("reference")
   override def addressFootprint(ctx: Context): (in.Location, in.Expr) ==> CodeWriter[vpr.Exp] = te.addressFootprint(ctx) orElse expectedMatch("addressFootprint")

From b6518a740b93ebb9a0e1381b2e29d6c83948c224 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Fri, 22 Sep 2023 16:46:27 +0200
Subject: [PATCH 6/8] doc

---
 .../encodings/combinators/TypeEncoding.scala  |  6 +++++-
 .../encodings/maps/MapEncoding.scala          | 21 +++++++++++++------
 2 files changed, 20 insertions(+), 7 deletions(-)

diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
index a41fb5f28..6f1574340 100644
--- a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
@@ -233,7 +233,11 @@ trait TypeEncoding extends Generator {
     case in.Conversion(t2, expr :: t) if typ(ctx).isDefinedAt(t) && typ(ctx).isDefinedAt(t2) => ctx.expression(expr)
   }
 
-  // TODO: doc
+  /**
+    * Encodes expressions when they occur as the top-level expression in a trigger. The default implements
+    * an encoding for predicate instances that and defers the encoding of all expressions occurring in
+    * a trigger to the expression encoding.
+    */
   def triggerExpr(@unused ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = PartialFunction.empty
 
   /**
diff --git a/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala
index 9f3e5e8dd..6d9ef5c9f 100644
--- a/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala
@@ -54,11 +54,11 @@ class MapEncoding extends LeafTypeEncoding {
     * Encodes expressions as values that do not occupy some identifiable location in memory.
     * R[ nil(map[K]V°) ] -> null
     * R[ dflt(map[K]V°) ] -> null
-    * R[ len(e: map[K]V) ] -> [e] == null? 0 : | getCorrespondingMap([e]) |
-    * R[ (e: map[K]V)[idx] ] -> [e] == null? [ dflt(V) ] : goMapLookup(e[idx])
-    * R[ keySet(e: map[K]V) ] -> [e] == null? 0 : MapDomain(getCorrespondingMap(e))
-    * R[ valueSet(e: map[K]V) ] -> [e] == null? 0 : MapRange(getCorrespondingMap(e))
-    * TODO: doc contains
+    * R[ len(e: map[K]V) ] -> [ e ] == null? 0 : | getCorrespondingMap([ e ]) |
+    * R[ (e: map[K]V)[idx] ] -> [ e ] == null? [ dflt(V) ] : goMapLookup(e[idx])
+    * R[ keySet(e: map[K]V) ] -> [ e ] == null? 0 : MapDomain(getCorrespondingMap([ e ]))
+    * R[ valueSet(e: map[K]V) ] -> [ e ] == null? 0 : MapRange(getCorrespondingMap([ e ]))
+    * R[ k in (e: map[K]V) ] -> [ e ] == null? false : MapContains([ k ], getCorrespondingMap([ e ]))
     */
   override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = {
     def goE(x: in.Expr): CodeWriter[vpr.Exp] = ctx.expression(x)
@@ -127,7 +127,16 @@ class MapEncoding extends LeafTypeEncoding {
     }
   }
 
-  // TODO: doc
+  /**
+    * Encodes expressions when they occur as the top-level expression in a trigger.
+    * Notice that if we had used the expression encoding for the following triggers,
+    * they would have resulted in ill-formed triggers at the Viper level (e.g., because
+    * they would have ternary operations).
+    *   { m[i] } -> { getCorrespondingMap([ m ])[ [ i ] ] }
+    *   { k in m } -> { [ k ] in getCorrespondingMap([ m ]) }
+    *   { k in domain(m) } -> { [ k ] in domain(getCorrespondingMap([ m ])) }
+    *   { k in range(m) } -> { [ k ] in range(getCorrespondingMap([ m ])) }
+    */
   override def triggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = {
     default(super.triggerExpr(ctx)) {
       case l@in.IndexedExp(m :: ctx.Map(keys, values), idx, _) =>

From 31498c42f55bc4913e47a249df470c53eface2dc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Fri, 22 Sep 2023 18:46:27 +0200
Subject: [PATCH 7/8] Apply suggestions from code review

Co-authored-by: Felix Wolf <60103963+Felalolf@users.noreply.github.com>
---
 .../encodings/defaults/DefaultTriggerExprEncoding.scala     | 2 +-
 .../viper/gobra/translator/encodings/maps/MapEncoding.scala | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/main/scala/viper/gobra/translator/encodings/defaults/DefaultTriggerExprEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/defaults/DefaultTriggerExprEncoding.scala
index 591107b1f..ecca61171 100644
--- a/src/main/scala/viper/gobra/translator/encodings/defaults/DefaultTriggerExprEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/defaults/DefaultTriggerExprEncoding.scala
@@ -16,7 +16,7 @@ class DefaultTriggerExprEncoding extends Encoding {
   import viper.gobra.translator.util.ViperWriter._
 
   override def triggerExpr(ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = {
-    // use predicate access encoding but then take just the predicate access, i.e. remove `acc` and the permission amount:
+    // use predicate access encoding but then take just the predicate access, i.e. without the access predicate:
     case in.Accessible.Predicate(op) =>
       for {
         v <- ctx.assertion(in.Access(in.Accessible.Predicate(op), in.FullPerm(op.info))(op.info))
diff --git a/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala
index 6d9ef5c9f..d92fa27f2 100644
--- a/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala
@@ -129,9 +129,9 @@ class MapEncoding extends LeafTypeEncoding {
 
   /**
     * Encodes expressions when they occur as the top-level expression in a trigger.
-    * Notice that if we had used the expression encoding for the following triggers,
-    * they would have resulted in ill-formed triggers at the Viper level (e.g., because
-    * they would have ternary operations).
+    * Notice that using the expression encoding for the following triggers,
+    * results in ill-formed triggers at the Viper level (e.g., because
+    * they have ternary operations).
     *   { m[i] } -> { getCorrespondingMap([ m ])[ [ i ] ] }
     *   { k in m } -> { [ k ] in getCorrespondingMap([ m ]) }
     *   { k in domain(m) } -> { [ k ] in domain(getCorrespondingMap([ m ])) }

From e87d2ddb7fab7950dec7c5a94d9565875e17ffa3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Fri, 22 Sep 2023 18:52:03 +0200
Subject: [PATCH 8/8] feedback from Felix

---
 .../encodings/combinators/TypeEncoding.scala          |  6 +++---
 .../viper/gobra/translator/util/ViperWriter.scala     | 11 ++++++-----
 2 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
index 6f1574340..1421fdcc7 100644
--- a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
@@ -234,9 +234,9 @@ trait TypeEncoding extends Generator {
   }
 
   /**
-    * Encodes expressions when they occur as the top-level expression in a trigger. The default implements
-    * an encoding for predicate instances that and defers the encoding of all expressions occurring in
-    * a trigger to the expression encoding.
+    * Encodes expressions when they occur as the top-level expression in a trigger.
+    * The default implements an encoding for predicate instances and defers the
+    * encoding of all expressions to the expression encoding.
     */
   def triggerExpr(@unused ctx: Context): in.TriggerExpr ==> CodeWriter[vpr.Exp] = PartialFunction.empty
 
diff --git a/src/main/scala/viper/gobra/translator/util/ViperWriter.scala b/src/main/scala/viper/gobra/translator/util/ViperWriter.scala
index cbbf6ae82..3983445f9 100644
--- a/src/main/scala/viper/gobra/translator/util/ViperWriter.scala
+++ b/src/main/scala/viper/gobra/translator/util/ViperWriter.scala
@@ -399,11 +399,12 @@ object ViperWriter {
     /* Can be used in expressions. */
     def assert(cond: vpr.Exp, exp: vpr.Exp, reasonT: (Source.Verifier.Info, ErrorReason) => VerificationError)(ctx: Context): Writer[vpr.Exp] = {
       // In the future, this might do something more sophisticated
-      if (cond.isInstanceOf[vpr.TrueLit]) {
-        unit(exp)
-      } else {
-        val (res, errT) = ctx.condition.assert(cond, exp, reasonT)
-        errorT(errT).map(_ => res)
+      cond match {
+        case vpr.TrueLit() =>
+          unit(exp)
+        case _ =>
+          val (res, errT) = ctx.condition.assert(cond, exp, reasonT)
+          errorT(errT).map(_ => res)
       }
     }