From d96c10a8e0533bb81dde802f16b653fe159ae2cb Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 4 Aug 2016 14:15:21 +0200
Subject: [PATCH] A few new trees
---
src/main/scala/inox/ast/Expressions.scala | 30 ++++++++++++++++++++---
src/main/scala/inox/ast/Extractors.scala | 8 +++++-
2 files changed, 33 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index 7049e7c65..08e25f437 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/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
+ }
+ }
}
diff --git a/src/main/scala/inox/ast/Extractors.scala b/src/main/scala/inox/ast/Extractors.scala
index e7cd86bbd..2f9ae2bca 100644
--- a/src/main/scala/inox/ast/Extractors.scala
+++ b/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)))
--
GitLab