A few new trees

src/main/scala/inox/ast/Expressions.scala

@@ -61,6 +61,7 @@ trait Expressions { self: Trees =>
 
 
   /** Variable
+    *
     * @param id The identifier of this variable
     */
   case class Variable(id: Identifier, tpe: Type) extends Expr with Terminal with VariableSymbol {
@@ -245,13 +246,18 @@ trait Expressions { self: Trees =>
     * [[purescala.Constructors#caseClassSelector purescala's constructor caseClassSelector]]
     */
   case class CaseClassSelector(caseClass: Expr, selector: Identifier) extends Expr with CachingTyped {
-    protected def computeType(implicit s: Symbols): Type = caseClass.getType match {
+
+    def classIndex(implicit s: Symbols) = caseClass.getType match {
       case ct: ClassType => ct.lookupClass match {
         case Some(tcd: TypedCaseClassDef) =>
-          val index = tcd.cd.selectorID2Index(selector)
-          tcd.fieldsTypes(index)
-        case _ => Untyped
+          Some(tcd, tcd.cd.selectorID2Index(selector))
+        case _ => None
       }
+      case _ => None
+    }
+
+    protected def computeType(implicit s: Symbols): Type = classIndex match {
+      case Some((tcd, ind)) => tcd.fieldsTypes(ind)
       case _ => Untyped
     }
   }
@@ -468,6 +474,15 @@ trait Expressions { self: Trees =>
 
 
   /* Bit-vector operations */
+  /** $encodingof `... | ...` $noteBitvector */
+  case class BVOr(lhs: Expr, rhs: Expr) extends Expr with CachingTyped {
+    protected def computeType(implicit s: Symbols): Type = bitVectorType(lhs.getType, rhs.getType)
+  }
+
+  /** $encodingof `... & ...` $noteBitvector */
+  case class BVAnd(lhs: Expr, rhs: Expr) extends Expr with CachingTyped {
+    protected def computeType(implicit s: Symbols): Type = bitVectorType(lhs.getType, rhs.getType)
+  }
 
   /** $encodingof `... ^ ...` $noteBitvector */
   case class BVXOr(lhs: Expr, rhs: Expr) extends Expr with CachingTyped {
@@ -646,4 +661,11 @@ trait Expressions { self: Trees =>
       case _ => Untyped
     }
   }
+
+  case class MapUpdated(map: Expr, key: Expr, value: Expr) extends Expr with CachingTyped {
+    protected def computeType(implicit s: Symbols) = map.getType match {
+      case mt@MapType(from, to) => checkParamTypes(Seq(key.getType, value.getType), Seq(from, to), mt)
+      case _ => Untyped
+    }
+  }
 }

src/main/scala/inox/ast/Extractors.scala

@@ -70,6 +70,10 @@ trait Extractors { self: Trees =>
         Some(Seq(t1, t2), (es: Seq[Expr]) => LessEquals(es(0), es(1)))
       case GreaterEquals(t1, t2) =>
         Some(Seq(t1, t2), (es: Seq[Expr]) => GreaterEquals(es(0), es(1)))
+      case BVOr(t1, t2) =>
+        Some(Seq(t1, t2), (es: Seq[Expr]) => BVOr(es(0), es(1)))
+      case BVAnd(t1, t2) =>
+        Some(Seq(t1, t2), (es: Seq[Expr]) => BVAnd(es(0), es(1)))
       case BVXOr(t1, t2) =>
         Some(Seq(t1, t2), (es: Seq[Expr]) => BVXOr(es(0), es(1)))
       case BVShiftLeft(t1, t2) =>
@@ -102,7 +106,9 @@ trait Extractors { self: Trees =>
         Some(Seq(e1, e2), (es: Seq[Expr]) => BagUnion(es(0), es(1)))
       case BagDifference(e1, e2) =>
         Some(Seq(e1, e2), (es: Seq[Expr]) => BagDifference(es(0), es(1)))
-      case mg @ MapApply(t1, t2) =>
+      case MapUpdated(map, k, v) =>
+        Some(Seq(map, k, v), (es: Seq[Expr]) => MapUpdated(es(0), es(1), es(2)))
+      case MapApply(t1, t2) =>
         Some(Seq(t1, t2), (es: Seq[Expr]) => MapApply(es(0), es(1)))
       case Let(binder, e, body) =>
         Some(Seq(e, body), (es: Seq[Expr]) => Let(binder, es(0), es(1)))