From 95769d85da74b3eb44d239fdc8c3705250bc027c Mon Sep 17 00:00:00 2001
From: kyessenov <unknown>
Date: Mon, 2 Aug 2010 08:18:36 +0000
Subject: Chalice: * added quantifiers over any type (forall i: int :: i + 1 ==
 i + 1) * cleaned up AST transformation code; organized one transform
 operation that should preserve source positions -- it was very annoying to
 see assertions with lost source positions * added a desugar method that
 simplifies Chalice AST by unrolling a few constructs -- maybe useful in the
 future to quickly add a syntactic sugar

---
 Chalice/src/Ast.scala             | 237 +++++++++++++++++----
 Chalice/src/Boogie.scala          |  17 +-
 Chalice/src/ChaliceToCSharp.scala |   2 +-
 Chalice/src/Parser.scala          |  53 +++--
 Chalice/src/PrettyPrinter.scala   |  12 +-
 Chalice/src/Resolver.scala        | 134 ++++--------
 Chalice/src/Translator.scala      | 428 ++++++++++++++------------------------
 7 files changed, 446 insertions(+), 437 deletions(-)

(limited to 'Chalice/src')

diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 25bfb975..0414285d 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -4,6 +4,7 @@
 //
 //-----------------------------------------------------------------------------
 import scala.util.parsing.input.Position
+import scala.util.parsing.input.NoPosition
 import scala.util.parsing.input.Positional
 
 trait ASTNode extends Positional
@@ -124,10 +125,8 @@ sealed abstract class NamedMember(id: String) extends Member {
   var Parent: Class = null
   def FullName = Parent.id + "." + Id
 }
-case class Field(id: String, typ: Type) extends NamedMember(id) {
-  val IsGhost: Boolean = false
-}
-case class SpecialField(name: String, tp: Type) extends Field(name, tp) {  // direct assignments are not allowed to a SpecialField
+case class Field(id: String, typ: Type, isGhost: Boolean) extends NamedMember(id)
+case class SpecialField(name: String, tp: Type) extends Field(name, tp, false) {  // direct assignments are not allowed to a SpecialField
   override def FullName = id
 }
 case class Method(id: String, ins: List[Variable], outs: List[Variable], spec: List[Specification], body: List[Statement]) extends NamedMember(id)
@@ -146,12 +145,12 @@ class Variable(name: String, typ: Type) extends ASTNode {
   val IsGhost: Boolean = false
   val IsImmutable: Boolean = false
   val UniqueName = {
-    val n = S_Variable.VariableCount
-    S_Variable.VariableCount = S_Variable.VariableCount + 1
+    val n = Variable.VariableCount
+    Variable.VariableCount = Variable.VariableCount + 1
     name + "#" + n
   }
 }
-object S_Variable { var VariableCount = 0 }
+object Variable { var VariableCount = 0 }
 class ImmutableVariable(id: String, t: Type) extends Variable(id, t) {
   override val IsImmutable: Boolean = true
 }
@@ -234,7 +233,9 @@ case class NewRhs(id: String, initialization: List[Init], lowerBounds: List[Expr
 case class Init(id: String, e: Expression) extends ASTNode {
   var f: Field = null;
 }
-sealed abstract class Expression extends RValue
+sealed abstract class Expression extends RValue {
+  def transform(f: Expression => Option[Expression]) = AST.transform(this, f)
+}
 sealed abstract class Literal extends Expression
 case class IntLiteral(n: Int) extends Literal
 case class BoolLiteral(b: Boolean) extends Literal
@@ -273,14 +274,12 @@ case class Epsilons(n: Expression) extends Read   // Some(Some(n))
 
 sealed abstract class PermissionExpr(perm: Permission) extends Expression
 sealed abstract class WildCardPermission(perm: Permission) extends PermissionExpr(perm)
-case class Access(e: MemberAccess, perm: Permission) extends PermissionExpr(perm) {
-  def getMemberAccess = e : MemberAccess;
-}
+case class Access(ma: MemberAccess, perm: Permission) extends PermissionExpr(perm) 
 case class AccessAll(obj: Expression, perm: Permission) extends WildCardPermission(perm)
 case class AccessSeq(s: Expression, f: Option[MemberAccess], perm: Permission) extends WildCardPermission(perm)
 
 case class Credit(e: Expression, n: Option[Expression]) extends Expression {
-  def N = n match { case None => IntLiteral(1) case Some(n) => n }
+  val N = n match { case None => IntLiteral(1) case Some(n) => n }
 }
 
 case class Holds(e: Expression) extends Expression
@@ -295,10 +294,10 @@ case class FunctionApplication(obj: Expression, id: String, args: List[Expressio
 }
 case class Unfolding(pred: Access, in: Expression) extends Expression
 sealed abstract class BinaryExpr(e0: Expression, e1: Expression) extends Expression {
-  def E0 = e0
-  def E1 = e1
-  def ExpectedLhsType: Class = BoolClass  // sometimes undefined
-  def ExpectedRhsType: Class = BoolClass  // sometimes undefined
+  val E0 = e0
+  val E1 = e1
+  val ExpectedLhsType: Class = BoolClass  // sometimes undefined
+  val ExpectedRhsType: Class = BoolClass  // sometimes undefined
   val ResultType: Class = BoolClass
   val OpName: String
 }
@@ -315,8 +314,8 @@ case class Or(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
   override val OpName = "||"
 }
 sealed abstract class ArithmeticExpr(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
-  override def ExpectedLhsType = IntClass
-  override def ExpectedRhsType = IntClass
+  override val ExpectedLhsType = IntClass
+  override val ExpectedRhsType = IntClass
   override val ResultType = IntClass
 }
 case class Plus(e0: Expression, e1: Expression) extends ArithmeticExpr(e0,e1) {
@@ -335,12 +334,12 @@ case class Mod(e0: Expression, e1: Expression) extends ArithmeticExpr(e0,e1) {
   override val OpName = "%"
 }
 sealed abstract class CompareExpr(e0: Expression, e1: Expression) extends BinaryExpr(e0,e1) {
-  override def ExpectedLhsType = IntClass
-  override def ExpectedRhsType = IntClass
+  override val ExpectedLhsType = IntClass
+  override val ExpectedRhsType = IntClass
 }
 sealed abstract class EqualityCompareExpr(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
-  override def ExpectedLhsType = throw new Exception("EqualityCompareExpr does not have a single ExpectedArgsType")
-  override def ExpectedRhsType = throw new Exception("EqualityCompareExpr does not have a single ExpectedArgsType")
+  override val ExpectedLhsType = null;
+  override val ExpectedRhsType = null;
 }
 case class Eq(e0: Expression, e1: Expression) extends EqualityCompareExpr(e0,e1) {
   override val OpName = "=="
@@ -361,23 +360,24 @@ case class Greater(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
   override val OpName = ">"
 }
 case class LockBelow(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) {
-  override def ExpectedLhsType = throw new Exception("LockBelow does not have a single ExpectedArgsType")
-  override def ExpectedRhsType = throw new Exception("LockBelow does not have a single ExpectedArgsType")
+  override val ExpectedLhsType = null;
+  override val ExpectedRhsType = null;
   override val OpName = "<<"
 }
-sealed abstract class Quantification(is: List[String], seq: Expression, e: Expression) extends Expression {
-  def Quantor: String; 
-  def Is = is
-  def Seq = seq
-  def E = e
-  var variables = null: List[Variable];
-}
-case class Forall(is: List[String], seq: Expression, e: Expression) extends Quantification(is, seq, e) {
-  override def Quantor = "forall"
-}
-case class Exists(is: List[String], seq: Expression, e: Expression) extends Quantification(is, seq, e) {
-  override def Quantor = "exists"
-}
+
+// quantifiers
+trait Quant
+object Forall extends Quant
+object Exists extends Quant
+
+sealed abstract class Quantification(q: Quant, is: List[String], e: Expression) extends Expression {
+  val Q = q;
+  val Is = is;
+  val E = e;
+  var variables = null: List[Variable]; // resolved by type checker
+}
+case class SeqQuantification(q: Quant, is: List[String], seq: Expression, e: Expression) extends Quantification(q, is, e)
+case class TypeQuantification(q: Quant, is: List[String], t: Type, e: Expression) extends Quantification(q, is, e)
 
 // sequences
 
@@ -387,7 +387,11 @@ case class Range(min: Expression, max: Expression /* non-inclusive*/) extends Ex
 case class Append(s0: Expression, s1: Expression) extends SeqAccess(s0, s1) {
   override val OpName = "++"
 }
-sealed abstract case class SeqAccess(e0: Expression, e1: Expression) extends BinaryExpr(e0, e1)
+sealed abstract case class SeqAccess(e0: Expression, e1: Expression) extends BinaryExpr(e0, e1) {
+  override val ExpectedLhsType = null
+  override val ExpectedRhsType = null
+  override val ResultType = null
+}
 case class Length(e: Expression) extends Expression
 case class At(s: Expression, n: Expression) extends SeqAccess(s, n) {
   override val OpName = ""
@@ -398,11 +402,10 @@ case class Drop(s: Expression, n: Expression) extends SeqAccess(s, n) {
 case class Take(s: Expression, n: Expression) extends SeqAccess(s, n) {
   override val OpName = ""
 }
-case class Contains(s: Expression, n: Expression) extends SeqAccess(s, n) {
+case class Contains(n: Expression, s: Expression) extends SeqAccess(n, s) {
   override val OpName = "in"
 }
 
-
 // eval
 
 case class Eval(h: EvalState, e: Expression) extends Expression
@@ -419,3 +422,157 @@ case class CallState(token: Expression, obj: Expression, id: String, args: List[
   var m = null: Method;
   def target() = token;
 }
+
+// visitors / operations
+
+object AST {
+  /**
+   * Transforms an expression using f. f must produce expressions of the appropriate type (e.g. not replace int literal with a bool literal)
+   * Ensures that mutable fields of expressions are carried over. f must make sure that mutable fields of its value are filled in.
+   */
+  def transform(expr: Expression, f: Expression => Option[Expression]):Expression = {
+    val func = (e:Expression) => transform(e, f);
+    val x = f(expr);
+    // apply recursively
+    val result = if (x isDefined) x.get else expr match {
+      case _:Literal => expr
+      case _:ThisExpr => expr
+      case _:Result => expr
+      case _:VariableExpr => expr
+      case ma@MemberAccess(e, id) =>
+        val g = MemberAccess(func(e), id);
+        g.f = ma.f;
+        g.predicate = ma.predicate;
+        g.isPredicate = ma.isPredicate;
+        g
+      case Full | Epsilon | Star => expr
+      case Frac(perm) => Frac(func(perm))
+      case Epsilons(perm) => Epsilons(func(perm))
+      case Access(e, perm) => Access(func(e).asInstanceOf[MemberAccess], func(perm).asInstanceOf[Permission]);
+      case AccessAll(obj, perm) => AccessAll(func(obj), func(perm).asInstanceOf[Permission]);
+      case AccessSeq(s, None, perm) => AccessSeq(func(s), None, func(perm).asInstanceOf[Permission])
+      case AccessSeq(s, Some(f), perm) => AccessSeq(func(s), Some(func(f).asInstanceOf[MemberAccess]), func(perm).asInstanceOf[Permission])
+      case Credit(e, None) => Credit(func(e), None)
+      case Credit(e, Some(n)) => Credit(func(e), Some(func(n)))
+      case Holds(e) => Holds(func(e))
+      case RdHolds(e) => RdHolds(func(e))
+      case _: Assigned => expr
+      case Old(e) => Old(func(e))
+      case IfThenElse(con, then, els) => IfThenElse(func(con), func(then), func(els))
+      case Not(e) => Not(func(e))
+      case funapp@FunctionApplication(obj, id, args) =>
+        val appl = FunctionApplication(func(obj), id, args map { arg => func(arg)});
+        appl.f = funapp.f;
+        appl
+      case Unfolding(pred, e) =>
+        Unfolding(func(pred).asInstanceOf[Access], func(e))
+      case Iff(e0,e1) => Iff(func(e0), func(e1))
+      case Implies(e0,e1) => Implies(func(e0), func(e1))
+      case And(e0,e1) => And(func(e0), func(e1))
+      case Or(e0,e1) => Or(func(e0), func(e1))
+      case Eq(e0,e1) => Eq(func(e0), func(e1))
+      case Neq(e0,e1) => Neq(func(e0), func(e1))
+      case Less(e0,e1) => Less(func(e0), func(e1))
+      case AtMost(e0,e1) => AtMost(func(e0), func(e1))
+      case AtLeast(e0,e1) => AtLeast(func(e0), func(e1))
+      case Greater(e0,e1) => Greater(func(e0), func(e1))
+      case LockBelow(e0,e1) => LockBelow(func(e0), func(e1))
+      case Plus(e0,e1) => Plus(func(e0), func(e1))
+      case Minus(e0,e1) => Minus(func(e0), func(e1))
+      case Times(e0,e1) => Times(func(e0), func(e1))
+      case Div(e0,e1) => Div(func(e0), func(e1))
+      case Mod(e0,e1) => Mod(func(e0), func(e1))
+      case ExplicitSeq(es) => ExplicitSeq(es map { e => func(e) })
+      case Range(min, max)=> Range(func(min), func(max))
+      case Append(e0, e1) => Append(func(e0), func(e1))
+      case At(e0, e1) => At(func(e0), func(e1))
+      case Drop(e0, e1) => Drop(func(e0), func(e1))
+      case Take(e0, e1) => Take(func(e0), func(e1))
+      case Length(e) => Length(func(e))
+      case Contains(e0, e1) => Contains(func(e0), func(e1))
+      case qe @ SeqQuantification(q, is, seq, e) =>
+        val result = SeqQuantification(q, is, func(seq), func(e));
+        result.variables = qe.variables;
+        result;
+      case qe @ TypeQuantification(q, is, t, e) =>
+        val result = TypeQuantification(q, is, t, func(e));
+        result.variables = qe.variables;
+        result;
+      case Eval(h, e) =>
+        Eval(h match {
+          case AcquireState(obj) => AcquireState(func(obj))
+          case ReleaseState(obj) => ReleaseState(func(obj))
+          case cs @ CallState(token, obj, i, args) =>
+            val result = CallState(func(token), func(obj), i, args map { a => func(a)});
+            result.m = cs.m;
+            result;
+        }, func(e))
+    };
+    
+    // preserve type
+    if (result.typ == null) result.typ = expr.typ;
+    // preserve position
+    if (result.pos == NoPosition) result.pos = expr.pos
+    result
+  }
+
+  // Applies recursively the function f first to the expression and then to its subexpressions (that is members of type RValue)  
+  def visit(expr: RValue, f: RValue => Unit) {
+    f(expr);
+    expr match {
+     case _:Literal => ;
+     case _:ThisExpr => ;
+     case _:Result => ;
+     case _:VariableExpr => ;
+     case MemberAccess(e, _) =>
+       visit(e, f);
+
+     case Frac(p) => visit(p, f);
+     case Epsilons(p) => visit(p, f);
+     case Full | Epsilon | Star =>;
+     case Access(e, perm) =>
+       visit(e, f); visit(perm, f);
+     case AccessAll(obj, perm) =>
+       visit(obj, f); visit(perm, f);
+     case AccessSeq(s, _, perm) =>
+       visit(s, f); visit(perm, f);
+
+     case Credit(e, n) =>
+       visit(e, f); n match { case Some(n) => visit(n, f); case _ => }
+     case Holds(e) => visit(e, f);
+     case RdHolds(e) => visit(e, f);
+
+     case e: BinaryExpr =>
+       visit(e.E0, f); visit(e.E1, f);
+     case Range(min, max) =>
+       visit(min, f); visit(max, f);
+     case e: Assigned => e
+     case Old(e) => visit(e, f);
+     case IfThenElse(con, then, els) => visit(con, f); visit(then, f); visit(els, f);
+     case Not(e) => visit(e, f);
+     case funapp@FunctionApplication(obj, id, args) =>
+       visit(obj, f); args foreach { arg => visit(arg, f) };
+     case Unfolding(pred, e) =>
+       visit(pred, f); visit(e, f);
+
+     case SeqQuantification(_, _, seq, e) => visit(seq, f); visit(e, f);
+     case TypeQuantification(_, _, _, e) => visit(e, f);
+
+     case ExplicitSeq(es) =>
+       es foreach { e => visit(e, f) }
+     case Length(e) =>
+       visit(e, f)
+     case Eval(h, e) =>
+       h match {
+         case AcquireState(obj) => visit(obj, f);
+         case ReleaseState(obj) => visit(obj, f);
+         case CallState(token, obj, id, args) =>
+           visit(token, f); visit(obj, f); args foreach {a : Expression => visit(a, f)};
+       }
+       visit(e, f);
+     case NewRhs(_, init, lowerBounds, upperBounds) =>
+       lowerBounds foreach { e => visit(e, f)};
+       upperBounds foreach { e => visit(e, f)};
+   }
+ }
+}
\ No newline at end of file
diff --git a/Chalice/src/Boogie.scala b/Chalice/src/Boogie.scala
index 50404f2a..32593da5 100644
--- a/Chalice/src/Boogie.scala
+++ b/Chalice/src/Boogie.scala
@@ -68,8 +68,9 @@ object Boogie {
    def apply(e: Expr, f: Expr) = new MapSelect(this, e, Some(f))
    def apply(e: Expr) = new MapSelect(this, e, None)
    def thenElse(thenE: Expr, elseE: Expr) = new Ite(this, thenE, elseE)
-   def select(e: Expr, s: String) = new MapSelect(this, e, s)
+   def select(e: Expr, s: String) = new MapSelect(this, e, s) // useful for working on heap
    def forall(x: BVar) = new Forall(x, this)
+   def exists(x: BVar) = new Exists(x, this)
    def store(e: Expr, f: Expr, rhs: Expr) = MapUpdate(this, e, Some(f), rhs)
  }
  case class IntLiteral(n: Int) extends Expr
@@ -94,12 +95,13 @@ object Boogie {
    def this(f: String, a0: Expr, a1: Expr, a2: Expr) = this(f, List(a0, a1, a2))
  }
  case class Forall(ta: List[TVar], xs: List[BVar], triggers: List[Expr], body: Expr) extends Expr {
-   def this(xs: List[BVar], triggers: List[Expr], body: Expr) = this(List(), xs, triggers, body)
-   def this(x: BVar, body: Expr) = this(List(), List(x), List(), body)
-   def this(t: TVar, x: BVar, body: Expr) = this(List(t), List(x), List(), body)
+   def this(x: BVar, body: Expr) = this(Nil, List(x), Nil, body)   
+   def this(xs: List[BVar], triggers: List[Expr], body: Expr) = this(Nil, xs, triggers, body)
+   def this(t: TVar, x: BVar, body: Expr) = this(List(t), List(x), Nil, body)
  }
- case class Exists(xs: List[BVar], triggers: List[Expr], body: Expr) extends Expr {
-   def this(x: BVar, body: Expr) = this(List(x), List(), body)
+ case class Exists(ta: List[TVar], xs: List[BVar], triggers: List[Expr], body: Expr) extends Expr {
+   def this(x: BVar, body: Expr) = this(Nil, List(x), List(), body)
+   def this(xs: List[BVar], triggers: List[Expr], body: Expr) = this(Nil, xs, triggers, body)   
  }
  case class Lambda(ta: List[TVar], xs: List[BVar], body: Expr) extends Expr
 
@@ -274,8 +276,9 @@ object Boogie {
      Print(triggers , "", { s: Expr => "{" + PrintExpr(s) + "} " }) +
      PrintExpr(body) +
      ")"
-   case Exists(xs, triggers, body) =>
+   case Exists(ts, xs, triggers, body) =>
      "(exists " +
+     (if (ts.length == 0) " " else "<" + Print(ts, ", ", { x: TVar => x.id }) + "> ") +     
      Print(xs, ", ", { x: BVar => x.id +  ": " + PrintType(x.t) }) +
      " :: " +
      Print(triggers , "", { s: Expr => "{" + PrintExpr(s) + "} " }) +
diff --git a/Chalice/src/ChaliceToCSharp.scala b/Chalice/src/ChaliceToCSharp.scala
index 0c35bd5b..0e9c5d39 100644
--- a/Chalice/src/ChaliceToCSharp.scala
+++ b/Chalice/src/ChaliceToCSharp.scala
@@ -56,7 +56,7 @@ class ChaliceToCSharp {
   
   def convertMember(member: Member): String = {
     member match {
-      case Field(id, tp) =>
+      case Field(id, tp, false) =>
         indent + "public " + convertType(tp) + " " + id + ";" + nl
       case meth@Method(id, ins, outs, spec, body) =>
         var csharpmain = if(id.equals("Start") && ins.length == 0 && outs.length == 0) {
diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index 69c011a8..cfb41bc0 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -57,8 +57,8 @@ class Parser extends StandardTokenParsers {
                    predicateDecl | functionDecl)
 
   def fieldDecl =
-        ( "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id,t) }
-        | "ghost" ~> "var" ~> idType <~ Semi ^^ { case (id,t) => new Field(id,t){override val IsGhost = true} }
+        ( "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id, t, false) }
+        | "ghost" ~> "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id, t, true) }
         )
   def Ident = 
     positioned(ident ^^ PositionedString)
@@ -78,14 +78,15 @@ class Parser extends StandardTokenParsers {
 
   def invariantDecl = positioned("invariant" ~> expression <~ Semi ^^ MonitorInvariant)
 
-  def methodDecl =
-        "method" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~
-        (methodSpec*) ~ blockStatement ^^ {
-          case id ~ ins ~ outs ~ spec ~ body =>
-            currentLocalVariables = Set[String]()
-            outs match {
-              case None => Method(id, ins, Nil, spec, body)
-              case Some(outs) => Method(id, ins, outs, spec, body) }}
+  def methodDecl = {
+    currentLocalVariables = Set[String]()
+    "method" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~
+    (methodSpec*) ~ blockStatement ^^ {
+      case id ~ ins ~ outs ~ spec ~ body =>
+        outs match {
+          case None => Method(id, ins, Nil, spec, body)
+          case Some(outs) => Method(id, ins, outs, spec, body) }}
+  }
   def channelDecl =
     "channel" ~> ident ~ formalParameters(true) ~ ("where" ~> expression ?) <~ Semi ^^ {
       case id ~ ins ~ None => Channel(id, ins, BoolLiteral(true))
@@ -476,21 +477,37 @@ class Parser extends StandardTokenParsers {
     | ("ite" ~> "(" ~> expression <~ ",") ~ (expression <~ ",") ~ (expression <~ ")") ^^ {
         case con ~ then ~ els => IfThenElse (con, then, els) }
     | "(" ~> expression <~ ")"
-    | forall
+    | quantifierType
+    | quantifierSeq
     | ("[" ~> expression) ~ (":" ~> expression <~ "]") ^^ { case from ~ to => Range(from, to) }
     | ("nil" ~> "<") ~> (typeDecl <~ ">") ^^ EmptySeq
     | ("[" ~> expressionList <~ "]") ^^ { case es => ExplicitSeq(es) }
     )
-  def forall: Parser[Quantification] =
-    (("forall" | "exists") ~ repsep(ident, ",") <~ "in") into {case quant ~ is => quantifierBody(quant, is)}
 
-  def quantifierBody(quant: String, is: List[String]) : Parser[Quantification] =
-    ((expression <~ "::") ~ (exprWithLocals(is))) ^^
+  // Scala type inference resists figuring out | (alternative) for these two
+
+  def quantifierSeq: Parser[Quantification] =
+    (quant ~ repsep(ident, ",")) into {case q ~ is => quantifierSeqBody(q, is)}
+
+  def quantifierSeqBody(q: Quant, is: List[String]) : Parser[Quantification] =
+    (("in" ~> expression <~ "::") ~ (exprWithLocals(is))) ^^
       { case seq ~ e =>
-        val result = quant match {case "forall" => Forall(is, seq, e); case "exists" => Exists(is, seq, e);};
         currentLocalVariables = currentLocalVariables -- is;
-        result
-      }  
+        SeqQuantification(q, is, seq, e);
+      }
+  
+  def quantifierType: Parser[Quantification] =
+    (quant ~ repsep(ident, ",")) into {case q ~ is => quantifierTypeBody(q, is)}
+
+  def quantifierTypeBody(q: Quant, is: List[String]) : Parser[Quantification] =
+    ((":" ~> typeDecl <~ "::") ~ (exprWithLocals(is))) ^^
+      { case t ~ e =>
+        currentLocalVariables = currentLocalVariables -- is;
+        TypeQuantification(q, is, t, e);
+      }
+
+  def quant: Parser[Quant] =
+    ( "forall" ^^^ Forall | "exists" ^^^ Exists)
 
   def exprWithLocals(i: List[String]) : Parser[Expression] = {
     currentLocalVariables = currentLocalVariables ++ i;
diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index 82e7658c..205349c6 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -18,8 +18,8 @@ object PrintProgram {
   def Member(m: Member) = m match {
     case MonitorInvariant(e) =>
       print("  invariant "); Expr(e); println(Semi)
-    case f@ Field(id, t) =>
-      println("  " + (if (f.IsGhost) "ghost " else "") + "var " + id + ": " + t.FullName + Semi)
+    case f@ Field(id, t, ghost) =>
+      println("  " + (if (ghost) "ghost " else "") + "var " + id + ": " + t.FullName + Semi)
     case m: Method =>
       print("  method " + m.id)
       print("("); VarList(m.ins); print(")")
@@ -257,12 +257,16 @@ object PrintProgram {
     case e:Div => BinExpr(e, e.OpName, 0x60, false, true, contextBindingPower, fragileContext)
     case e:Mod => BinExpr(e, e.OpName, 0x60, false, true, contextBindingPower, fragileContext)
     case q:Quantification => 
-      print("(" + q.Quantor + " "); 
+      print("(" + (q.Q match {case Forall => "forall"; case Exists => "exists"}) + " ");
       q.Is match {
         case Nil =>
         case i :: rest => print(i); rest foreach { v => print(", " + v) }
       }
-      print(" in "); Expr(q.Seq); print(" :: "); Expr(q.E); print(")");
+      q match {
+        case q: SeqQuantification => print(" in "); Expr(q.seq);
+        case q: TypeQuantification => print(": "); print(q.t.typ.FullName);
+      }
+      print(" :: "); Expr(q.E); print(")");
     case EmptySeq(t) =>
       print("nil<"); print(t.FullName); print(">");
     case ExplicitSeq(es) =>
diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index c14b68c8..6ea3e155 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -78,9 +78,9 @@ object Resolver {
      case cl: Class =>
        for (m <- cl.asInstanceOf[Class].members) m match {
          case _:MonitorInvariant =>
-         case Field(id,t) =>
+         case Field(_, t, _) =>
            ResolveType(t, contextNoCurrentClass)
-         case Method(id, ins, outs, spec, body) =>
+         case Method(_, ins, outs, _, _) =>
            for (v <- ins ++ outs) {
              ResolveType(v.t, contextNoCurrentClass)
            }
@@ -101,7 +101,7 @@ object Resolver {
    //  * VariableExpr and FieldSelect expressions
    for (decl <- prog) decl match {
      case ch: Channel =>
-        val context = new ProgramContext(decls, ChannelClass(ch))
+       val context = new ProgramContext(decls, ChannelClass(ch))
        var ctx = context
        for (v <- ch.parameters) {
          ctx = ctx.AddVariable(v)
@@ -276,11 +276,11 @@ object Resolver {
      }
    case fu@FieldUpdate(lhs, rhs) =>
      ResolveExpr(lhs, context, false, false)(false)
-     if (! lhs.isPredicate && lhs.f != null && !lhs.f.IsGhost) CheckNoGhost(lhs.e, context)
+     if (! lhs.isPredicate && lhs.f != null && !lhs.f.isGhost) CheckNoGhost(lhs.e, context)
      if (! lhs.isPredicate && lhs.f.isInstanceOf[SpecialField]) context.Error(lhs.pos, "cannot assign directly to special field: " + lhs.id)
      ResolveExpr(rhs, context, false, false)(false)
      if (! lhs.isPredicate && !canAssign(lhs.typ, rhs.typ)) context.Error(fu.pos, "type mismatch in assignment, lhs=" + lhs.typ.FullName + " rhs=" + rhs.typ.FullName)
-     if (! lhs.isPredicate && lhs.f != null && !lhs.f.IsGhost) CheckNoGhost(rhs, context)
+     if (! lhs.isPredicate && lhs.f != null && !lhs.f.isGhost) CheckNoGhost(rhs, context)
    case lv:LocalVar => throw new Exception("unexpected LocalVar; should have been handled in BlockStmt above")
    case c @ Call(declaresLocal, lhs, obj, id, args) =>
      ResolveExpr(obj, context, false, false)(false)
@@ -361,11 +361,11 @@ object Resolver {
    case fld@Fold(e) =>
      ResolveExpr(e, context, false, true)(false);
      CheckNoGhost(e, context);
-     if(!e.getMemberAccess.isPredicate) context.Error(fld.pos, "Fold can only be applied to predicates.")
+     if(!e.ma.isPredicate) context.Error(fld.pos, "Fold can only be applied to predicates.")
    case ufld@Unfold(e) =>
      ResolveExpr(e, context, false, true)(false);
      CheckNoGhost(e, context);
-     if(!e.getMemberAccess.isPredicate) context.Error(ufld.pos, "Unfold can only be applied to predicates.")
+     if(!e.ma.isPredicate) context.Error(ufld.pos, "Unfold can only be applied to predicates.")
    case c@CallAsync(declaresLocal, token, obj, id, args) => 
      // resolve receiver
      ResolveExpr(obj, context, false, false)(false)
@@ -575,7 +575,7 @@ object Resolver {
          } else {
            fieldNames = fieldNames + f
            e.typ.LookupMember(f) match {
-             case Some(field@Field(name, tp)) =>
+             case Some(field@Field(name, tp, _)) =>
                if(field.isInstanceOf[SpecialField]) context.Error(init.pos, "Initializer cannot assign to special field " + name + ".");
                ResolveExpr(init, context, false, false);
                if(! canAssign(tp.typ, init.typ)) context.Error(init.pos, "The field " + name + " cannot be initialized with an expression of type " + init.typ.id + ".");
@@ -715,7 +715,7 @@ object Resolver {
    case uf@Unfolding(pred, e) =>
      ResolveExpr(pred, context, twoStateContext, true);
      ResolveExpr(e, context, twoStateContext, false);
-     if(! pred.getMemberAccess.isPredicate) context.Error(uf.pos, "Only predicates can be unfolded.")
+     if(! pred.ma.isPredicate) context.Error(uf.pos, "Only predicates can be unfolded.")
      uf.typ = e.typ;
    case bin: EqualityCompareExpr =>
      ResolveExpr(bin.E0, context, twoStateContext, false)
@@ -777,16 +777,26 @@ object Resolver {
                      " (expected " + bin.ExpectedRhsType.FullName + ", found " + bin.E1.typ.FullName + ")")
      bin.typ = bin.ResultType
    case q: Quantification =>
-     q.Is foreach { i => if(context.LookupVariable(i).isDefined) context.Error(q.pos, "The variable " + i + " hides another local.") }
-     ResolveExpr(q.Seq, context, twoStateContext, false);
-     if(! q.Seq.typ.IsSeq) 
-       context.Error(q.Seq.pos, "A quantification must range over a sequence. (found: " + q.Seq.typ.FullName + ").");
-     else {
-       val elementType = q.Seq.typ.parameters(0);
+     q.Is foreach { i => if(context.LookupVariable(i).isDefined) context.Error(q.pos, "The variable " + i + " hides another local.") };
+     val typ = q match {
+       case q: SeqQuantification =>
+         ResolveExpr(q.seq, context, twoStateContext, false);
+         if(! q.seq.typ.IsSeq) {
+           context.Error(q.seq.pos, "A quantification must range over a sequence. (found: " + q.seq.typ.FullName + ").");
+           None;
+         } else
+           Some(q.seq.typ.parameters(0));
+       case q: TypeQuantification =>
+         ResolveType(q.t, context);
+         if (q.t.typ == null) None else Some(q.t.typ);
+     };
+
+     if (typ.isDefined) {
+       val vartype = typ.get;
        var bodyContext = context;
        var bvariables = Nil: List[Variable];
        q.Is foreach { i =>
-         val variable = new Variable(i, new Type(elementType));
+         val variable = new Variable(i, new Type(vartype));
          bodyContext = bodyContext.AddVariable(variable);
          bvariables = bvariables ::: List(variable);
        }
@@ -895,27 +905,26 @@ object Resolver {
        case ve: VariableExpr =>
          if (ve.v != null && ve.v.IsGhost) context.Error(ve.pos, "ghost variable not allowed here")
        case fs@ MemberAccess(e, id) =>
-         if (!fs.isPredicate && fs.f != null && fs.f.IsGhost) context.Error(fs.pos, "ghost fields not allowed here")
-         CheckNoGhost(e, context)
+         if (!fs.isPredicate && fs.f != null && fs.f.isGhost) context.Error(fs.pos, "ghost fields not allowed here")
        case a: Assigned =>
          if (a.v != null && a.v.IsGhost) context.Error(a.pos, "ghost variable not allowed here")
-       case _ => visitE(e, specOk)
+       case _ => // do nothing
      }
    }
-   specOk(expr)
+   AST.visit(expr, specOk);
  }
 
  def CheckNoImmutableGhosts(expr: RValue, context: ProgramContext): Unit = {
-   def specOk(e: RValue): Unit = { 
+   def specOk(e: RValue): Unit = {
      e match {
        case ve: VariableExpr =>
          if (ve.v != null && ve.v.IsGhost && ve.v.IsImmutable) context.Error(ve.pos, "ghost const not allowed here")
        case a: Assigned =>
          if (a.v != null && a.v.IsGhost && a.v.IsImmutable) context.Error(a.pos, "ghost const not allowed here")
-       case _ => visitE(e, specOk)
+       case _ => // do nothing
      }
    }
-   specOk(expr)
+   AST.visit(expr, specOk);
  }
 
  def CheckRunSpecification(e: Expression, context: ProgramContext, allowMaxLock: Boolean): Unit = e match {
@@ -972,8 +981,10 @@ object Resolver {
    case bin: BinaryExpr =>
      CheckRunSpecification(bin.E0, context, false)
      CheckRunSpecification(bin.E1, context, false)
-   case q: Quantification =>
-     CheckRunSpecification(q.Seq, context, false)
+   case q: SeqQuantification =>
+     CheckRunSpecification(q.seq, context, false)
+     CheckRunSpecification(q.E, context, true)
+   case q: TypeQuantification =>
      CheckRunSpecification(q.E, context, true)
    case Length(e) =>
      CheckRunSpecification(e, context, false);
@@ -990,77 +1001,4 @@ object Resolver {
      }
      CheckRunSpecification(e, context, allowMaxLock)
  }
-
- def visitE(expr: RValue, func: RValue => Unit): Unit = {
-   expr match {
-     case _:NewRhs =>
-     case e: Literal => ;
-     case _:ThisExpr => ;
-     case _:Result => ;
-     case e:VariableExpr => ;
-     case acc@MemberAccess(e,f) =>
-       func(e);
-     case Frac(p) => func(p);
-     case Epsilons(p) => func(p);
-     case Full | Epsilon | Star =>;
-     case Access(e, perm) =>
-       func(e); visitE(perm, func);
-     case AccessAll(obj, perm) =>
-       func(obj); visitE(perm, func);
-     case AccessSeq(s, f, perm) =>
-       func(s); visitE(perm, func);
-     case Credit(e, n) =>
-       func(e); n match { case Some(n) => func(n); case _ => }
-     case Holds(e) => func(e);
-     case RdHolds(e) => func(e);
-     case e: Assigned => e
-     case Old(e) => func(e);
-     case IfThenElse(con, then, els) => func(con); func(then); func(els);
-     case Not(e) => func(e);
-     case funapp@FunctionApplication(obj, id, args) =>
-       func(obj); args foreach { arg => func(arg) };
-     case Unfolding(pred, e) =>
-       func(pred); func(e); 
-     case Iff(e0,e1) => func(e0); func(e1);
-     case Implies(e0,e1) => func(e0); func(e1);
-     case And(e0,e1) =>func(e0); func(e1);
-     case Or(e0,e1) => func(e0); func(e1);
-     case Eq(e0,e1) => func(e0); func(e1);
-     case Neq(e0,e1) => func(e0); func(e1);
-     case Less(e0,e1) => func(e0); func(e1);
-     case AtMost(e0,e1) => func(e0); func(e1);
-     case AtLeast(e0,e1) => func(e0); func(e1);
-     case Greater(e0,e1) => func(e0); func(e1);
-     case LockBelow(e0,e1) => func(e0); func(e1);
-     case Plus(e0,e1) => func(e0); func(e1);
-     case Minus(e0,e1) => func(e0); func(e1);
-     case Times(e0,e1) => func(e0); func(e1);
-     case Div(e0,e1) => func(e0); func(e1);
-     case Mod(e0,e1) => func(e0); func(e1);
-     case Forall(i, seq, e) => func(seq); func(e);
-     case Exists(i, seq, e) => func(seq); func(e);
-     case ExplicitSeq(es) =>
-       es foreach { e => func(e) }
-     case Range(min, max) =>
-       func(min); func(max);
-     case Append(e0, e1) =>
-       func(e0); func(e1);
-     case at@At(e0, e1) =>
-       func(e0); func(e1);
-     case Drop(e0, e1) =>
-       func(e0); func(e1);
-     case Take(e0, e1) =>
-       func(e0); func(e1);
-     case Length(e) =>
-       func(e)
-     case Contains(s, n) => func(s); func(n);
-     case Eval(h, e) =>
-       h match {
-         case AcquireState(obj) => func(obj);
-         case ReleaseState(obj) => func(obj);
-         case CallState(token, obj, id, args) => func(token); func(obj); args foreach {a : Expression => func(a)};
-       }
-       func(e);
-   }
- }
 }
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index ff840986..2bfbd69f 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -4,6 +4,7 @@
 //
 //-----------------------------------------------------------------------------
 import scala.util.parsing.input.Position
+import scala.util.parsing.input.NoPosition
 
 import Boogie.Proc, Boogie.NamedType, Boogie.NewBVar, Boogie.Havoc, Boogie.Stmt, Boogie.Const,
        Boogie.Decl, Boogie.Expr, Boogie.FunctionApp, Boogie.Axiom, Boogie.BVar, Boogie.BType,
@@ -579,7 +580,7 @@ class Translator {
         } :::
         // exhale preconditions
         Exhale(Preconditions(c.m.spec) map
-          (p => SubstVars(p, Some(formalThis), c.m.ins, formalIns)) zip (Preconditions(c.m.spec) map { p => ErrorMessage(c.pos, "The precondition at " + p.pos + " might not hold.")}), "precondition") :::
+          (p => SubstVars(p, formalThis, c.m.ins, formalIns)) zip (Preconditions(c.m.spec) map { p => ErrorMessage(c.pos, "The precondition at " + p.pos + " might not hold.")}), "precondition") :::
         // create a new token
         BLocal(tokenV) :: Havoc(tokenId) :: bassume(nonNull(tokenId)) ::
         // the following assumes help in proving that the token is fresh
@@ -637,7 +638,7 @@ class Translator {
         etran.SetNoPermission(token, "joinable", etran.Mask) ::
         // inhale postcondition of the call
         postEtran.Inhale(Postconditions(jn.m.spec) map
-                         { p => SubstVars(p, Some(formalThis), jn.m.ins ++ jn.m.outs, formalIns ++ formalOuts)}, "postcondition", false) :::
+                         { p => SubstVars(p, formalThis, jn.m.ins ++ jn.m.outs, formalIns ++ formalOuts)}, "postcondition", false) :::
         // assign formal outs to actual outs
         (for ((v,e) <- lhs zip formalOuts) yield (v := e))
       case s@Send(ch, args) =>
@@ -660,7 +661,7 @@ class Translator {
         new Boogie.MapUpdate(etran.Credits, TrExpr(ch), new Boogie.MapSelect(etran.Credits, TrExpr(ch)) + 1) ::
         // exhale where clause
         Exhale(List(
-          (SubstVars(channel.where, Some(formalThis), channel.parameters, formalParams),
+          (SubstVars(channel.where, formalThis, channel.parameters, formalParams),
            ErrorMessage(s.pos, "The where clause at " + channel.where.pos + " might not hold."))),
           "channel where clause")
       case r@Receive(_, ch, outs) =>
@@ -684,7 +685,7 @@ class Translator {
         (formalThis := ch) ::
         (for (v <- formalParams) yield Havoc(v)) :::
         // inhale where clause
-        Inhale(List(SubstVars(channel.where, Some(formalThis), channel.parameters, formalParams)), "channel where clause") :::
+        Inhale(List(SubstVars(channel.where, formalThis, channel.parameters, formalParams)), "channel where clause") :::
         // declare any new local variables among the actual outs
         (for (v <- r.locals) yield BLocal(Variable2BVarWhere(v))) :::
         // assign formal outs to actual outs
@@ -820,14 +821,14 @@ class Translator {
     (for ((v,e) <- formalIns zip args) yield (v := e)) :::
     // exhale preconditions
     Exhale(Preconditions(c.m.spec) map
-          (p => SubstVars(p, Some(formalThis), c.m.ins, formalIns)) zip (Preconditions(c.m.spec) map { p => ErrorMessage(c.pos, "The precondition at " + p.pos + " might not hold.")}), "precondition") :::
+          (p => SubstVars(p, formalThis, c.m.ins, formalIns)) zip (Preconditions(c.m.spec) map { p => ErrorMessage(c.pos, "The precondition at " + p.pos + " might not hold.")}), "precondition") :::
     // havoc formal outs
     (for (v <- formalOuts) yield Havoc(v)) :::
     // havoc lockchanges
-    LockHavoc(for (e <- LockChanges(c.m.spec) map (p => SubstVars(p, Some(formalThis), c.m.ins, formalIns))) yield etran.Tr(e), postEtran) :::
+    LockHavoc(for (e <- LockChanges(c.m.spec) map (p => SubstVars(p, formalThis, c.m.ins, formalIns))) yield etran.Tr(e), postEtran) :::
     // inhale postconditions (using the state before the call as the "old" state)
     postEtran.Inhale(Postconditions(c.m.spec) map
-                     (p => SubstVars(p, Some(formalThis), c.m.ins ++ c.m.outs, formalIns ++ formalOuts)) , "postcondition", false) :::
+                     (p => SubstVars(p, formalThis, c.m.ins ++ c.m.outs, formalIns ++ formalOuts)) , "postcondition", false) :::
     // declare any new local variables among the actual outs
     (for (v <- c.locals) yield BLocal(Variable2BVarWhere(v))) :::
     // assign formal outs to actual outs
@@ -846,9 +847,9 @@ class Translator {
     val iterStartEtran = etran.FromPreGlobals(iterStartGlobals)
     val saveLocalsV = for (v <- w.LoopTargetsList) yield new Variable(v.id, v.t)
     val iterStartLocalsV = for (v <- w.LoopTargetsList) yield new Variable(v.id, v.t)
-    val lkchOld = lkch map (e => SubstVars(e, None, w.LoopTargetsList,
+    val lkchOld = lkch map (e => SubstVars(e, w.LoopTargetsList,
                                              for (v <- saveLocalsV) yield new VariableExpr(v)))
-    val lkchIterStart = lkch map (e => SubstVars(e, None, w.LoopTargetsList,
+    val lkchIterStart = lkch map (e => SubstVars(e, w.LoopTargetsList,
                                                    for (v <- iterStartLocalsV) yield new VariableExpr(v)))
     val oldLocks = lkchOld map (e => loopEtran.oldEtran.Tr(e))
     val iterStartLocks = lkchIterStart map (e => iterStartEtran.oldEtran.Tr(e))
@@ -1147,10 +1148,10 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
   **********************************************************************/
 
   def isDefined(e: Expression)(implicit assumption: Expr): List[Boogie.Stmt] = {
-    def prove(goal: Expr, pos: Position, msg: String)(implicit assumption: Expr): Boogie.Assert = {
+    def prove(goal: Expr, pos: Position, msg: String)(implicit assumption: Expr) =
       bassert(assumption ==> goal, pos, msg)
-    }
-    e match {
+    
+    desugar(e) match {
       case IntLiteral(n) => Nil
       case BoolLiteral(b) => Nil
       case NullLiteral() => Nil
@@ -1198,7 +1199,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         BLocal(tmpHeapV) :: (tmpHeap := Heap) ::
         BLocal(tmpMaskV) :: (tmpMask := Mask) :::
         BLocal(tmpCreditsV) :: (tmpCredits := Credits) :::
-        tmpTranslator.Exhale(Preconditions(func.f.spec) map { pre=> (SubstVars(pre, Some(obj), func.f.ins, args), ErrorMessage(func.pos, "Precondition at " + pre.pos + " might not hold."))},
+        tmpTranslator.Exhale(Preconditions(func.f.spec) map { pre=> (SubstVars(pre, obj, func.f.ins, args), ErrorMessage(func.pos, "Precondition at " + pre.pos + " might not hold."))},
                              "function call",
                              false) :::
         // size of the heap of callee must be strictly smaller than size of the heap of the caller
@@ -1260,16 +1261,6 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         isDefined(e0) ::: isDefined(e1) ::: List(prove(Tr(e1) !=@ 0, e1.pos, "Denominator might be zero."))
       case e: ArithmeticExpr =>
         isDefined(e.E0) ::: isDefined(e.E1)
-      case q@Forall(i, Range(min, max), e) =>
-        isDefinedQuantification(q.variables, min, max, e)
-      case q@Exists(i, Range(min, max), e) =>
-        isDefinedQuantification(q.variables, min, max, e)
-      case q@Forall(i, seq, e) =>
-        var newVars = q.variables map (v => new Variable(v.UniqueName, new Type(IntClass)))
-        isDefinedQuantification(newVars, IntLiteral(0), Length(seq), SubstVars(e, None, q.variables, newVars map {v => At(seq, new VariableExpr(v)) }))
-      case q@Exists(i, seq, e) =>
-        var newVars = q.variables map (v => new Variable(v.UniqueName, new Type(IntClass)))
-        isDefinedQuantification(newVars, IntLiteral(0), Length(seq), SubstVars(e, None, q.variables, newVars map {v => At(seq, new VariableExpr(v)) }))
       case EmptySeq(t) => Nil
       case ExplicitSeq(es) =>
         es flatMap { e => isDefined(e) }
@@ -1280,15 +1271,15 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
       case at@At(e0, e1) =>
         isDefined(e0) ::: isDefined(e1) :::
         prove(0 <= Tr(e1), at.pos, "Sequence index might be negative.") ::
-        prove(Tr(e1) < Boogie.FunctionApp("Seq#Length", List(Tr(e0))), at.pos, "Sequence index might be larger than or equal to the length of the sequence.")
+        prove(Tr(e1) < SeqLength(Tr(e0)), at.pos, "Sequence index might be larger than or equal to the length of the sequence.")
       case Drop(e0, e1) => 
         isDefined(e0) ::: isDefined(e1) :::
         prove(0 <= Tr(e1), e.pos, "Cannot drop less than zero elements.") ::
-        prove(Tr(e1) <= Boogie.FunctionApp("Seq#Length", List(Tr(e0))), e.pos, "Cannot drop more than elements than the length of the sequence.")
+        prove(Tr(e1) <= SeqLength(Tr(e0)), e.pos, "Cannot drop more than elements than the length of the sequence.")
       case Take(e0, e1) => 
         isDefined(e0) ::: isDefined(e1) :::
         prove(0 <= Tr(e1), e.pos, "Cannot take less than zero elements.") ::
-        prove(Tr(e1) <= Boogie.FunctionApp("Seq#Length", List(Tr(e0))), e.pos, "Cannot take more than elements than the length of the sequence.")
+        prove(Tr(e1) <= SeqLength(Tr(e0)), e.pos, "Cannot take more than elements than the length of the sequence.")
       case Length(e) =>
         isDefined(e)
       case Contains(e0, e1) =>
@@ -1297,28 +1288,16 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         val (evalHeap, evalMask, evalCredits, checks, assumptions) = fromEvalState(h);
         val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask, evalCredits), currentClass);
         evalEtran.isDefined(e)
+      case _ : SeqQuantification => throw new Exception("should be desugared")
+      case tq @ TypeQuantification(_, _, _, e) =>
+        // replace variables since we need locals
+        val vars = tq.variables map {v => val result = new Variable(v.id, v.t); result.pos = v.pos; result;}
+        (vars map {v => BLocal(Boogie.BVar(v.UniqueName, type2BType(v.t.typ)))}) :::
+        isDefined(SubstVars(e, tq.variables, vars map {v => new VariableExpr(v);}))
     }
   }
 
-  def isDefinedQuantification(is: List[Variable], min: Expression, max: Expression, e: Expression)(implicit assumption: Expr): List[Stmt] = {
-    var iTmps = Nil: List[Variable];
-    var assumption2 = assumption;
-    for(i <- is) { 
-      val iTmp = new Variable(i.UniqueName, new Type(IntClass));
-      iTmps = iTmp :: iTmps; 
-      assumption2 = assumption2 && (Tr(min)<=VarExpr(iTmp.UniqueName)) && (VarExpr(iTmp.UniqueName) < Tr(max))
-    }
-    // check definedness of the bounds
-    isDefined(min) ::: isDefined(max) :::
-    // introduce a new local iTmp with an arbitrary value
-    (iTmps map { iTmp =>
-      BLocal(Boogie.BVar(iTmp.UniqueName, tint))
-    }) :::
-    // prove that the body is well-defined for iTmp, provided iTmp lies between min and max
-    isDefined(SubstVars(e, None, is, iTmps map { iTmp => new VariableExpr(iTmp)}))(assumption2)
-  }
-
-  def Tr(e: Expression): Boogie.Expr = e match {
+  def Tr(e: Expression): Boogie.Expr = desugar(e) match {
     case IntLiteral(n) => n
     case BoolLiteral(b) => b
     case NullLiteral() => bnull
@@ -1409,8 +1388,6 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
       Tr(e0) / Tr(e1)
     case Mod(e0,e1) =>
       Tr(e0) % Tr(e1)
-    case q: Quantification =>
-      translateQuantification(q)
     case EmptySeq(t) =>
       createEmptySeq
     case ExplicitSeq(es) =>
@@ -1423,44 +1400,22 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
       createRange(Tr(min), Tr(max))
     case Append(e0, e1) =>
       createAppendSeq(Tr(e0), Tr(e1))
-    case at@At(e0, e1) =>
-      FunctionApp("Seq#Index", List(Tr(e0), Tr(e1)))  // of type: VarExpr(TrClass(e0.typ.parameters(0)))
+    case at@At(e0, e1) =>SeqIndex(Tr(e0), Tr(e1))
     case Drop(e0, e1) =>
       Boogie.FunctionApp("Seq#Drop", List(Tr(e0), Tr(e1)))
     case Take(e0, e1) =>
       Boogie.FunctionApp("Seq#Take", List(Tr(e0), Tr(e1)))
-    case Length(e) =>
-      Boogie.FunctionApp("Seq#Length", List(Tr(e)))
-    case Contains(e0, e1) =>
-      Boogie.FunctionApp("Seq#Contains", List(Tr(e1), Tr(e0)))
+    case Length(e) => SeqLength(e)
+    case Contains(e0, e1) => SeqContains(Tr(e1), Tr(e0))
     case Eval(h, e) =>
       val (evalHeap, evalMask, evalCredits, checks, assumptions) = fromEvalState(h);
       val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask, evalCredits), currentClass);
       evalEtran.Tr(e)
-  }
-
-  def translateQuantification(q: Quantification): Expr = {
-    // generate index variables
-    var (is, min, max, e) = q match {
-      case Forall(_, Range(min, max), e) => (q.variables, min, max, e);
-      case Exists(_, Range(min, max), e) => (q.variables, min, max, e);
-      case Forall(_, seq, eo) =>
-        var is = q.variables map (v => new Variable(v.UniqueName, new Type(IntClass)));
-        var e = SubstVars(eo, None, q.variables, is map {v => At(seq, new VariableExpr(v))});
-        (is, IntLiteral(0), Length(seq), e);
-      case Exists(_, seq, eo) =>
-        var is = q.variables map (v => new Variable(v.UniqueName, new Type(IntClass)));
-        var e = SubstVars(eo, None, q.variables, is map {v => At(seq, new VariableExpr(v))});
-        (is, IntLiteral(0), Length(seq), e);
-    }
-    var assumption = true: Expr;
-    for(i <- is) {
-      assumption = assumption && (Tr(min) <= VarExpr(i.UniqueName) && VarExpr(i.UniqueName) < Tr(max));
-    }
-    q match {
-      case _: Forall => new Boogie.Forall(is map { i => Variable2BVar(i)}, Nil, assumption ==> Tr(e));
-      case _: Exists => new Boogie.Exists(is map { i => Variable2BVar(i)}, Nil, assumption && Tr(e));
-    }
+    case _:SeqQuantification => throw new Exception("should be desugared")
+    case tq @ TypeQuantification(Forall, _, _, e) =>
+      new Boogie.Forall(tq.variables map { v => Variable2BVar(v)}, Nil, Tr(e))
+    case tq @ TypeQuantification(Exists, _, _, e) =>
+      new Boogie.Exists(tq.variables map { v => Variable2BVar(v)}, Nil, Tr(e))
   }
 
   def ShaveOffOld(e: Expression): (Expression, Boolean) = e match {
@@ -1500,24 +1455,13 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
     Comment("end inhale")
   }
 
-  def Inhale(p: Expression, ih: Boogie.Expr, check: Boolean): List[Boogie.Stmt] = p match {
+  def Inhale(p: Expression, ih: Boogie.Expr, check: Boolean): List[Boogie.Stmt] = desugar(p) match {
     case pred@MemberAccess(e, p) if pred.isPredicate => 
       val tmp = Access(pred, Full);
       tmp.pos = pred.pos;
       Inhale(tmp, ih, check)
-    case acc@AccessAll(obj, perm) =>
-      obj.typ.Fields flatMap { f => 
-        val ma = MemberAccess(obj, f.id);
-        ma.f = f;
-        ma.pos = acc.pos;
-        val inhalee = Access(ma, perm);
-        inhalee.pos = acc.pos;
-        Inhale(inhalee, ih, check) }
-    case AccessSeq(s, None, perm) =>
-      s.typ.parameters(0).Fields flatMap { f =>
-        val ma = MemberAccess(At(s, IntLiteral(0)), f.id); ma.f = f; ma.pos = p.pos;
-        val inhalee = AccessSeq(s, Some(ma), perm); inhalee.pos = p.pos;
-        Inhale(inhalee, ih, check) }
+    case AccessAll(obj, perm) => throw new Exception("should be desugared")
+    case AccessSeq(s, None, perm) => throw new Exception("should be desugared")
     case acc@Access(e,perm) =>
       val trE = Tr(e.e)
       val module = currentClass.module;
@@ -1559,9 +1503,9 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         val (refV, ref) = Boogie.NewBVar("ref", tref, true);
         val (fV, f) = Boogie.NewBVar("f", FieldType(a), true);
         (Heap := Lambda(List(aV), List(refV, fV),
-          (FunctionApp("Seq#Contains", List(e, ref)) && f ==@ memberName).thenElse
+          (SeqContains(e, ref) && f ==@ memberName).thenElse
             (ih(ref, f), Heap(ref, f)))) ::
-        bassume((FunctionApp("Seq#Contains", List(e, ref)) ==> TypeInformation(Heap(ref, memberName), member.f.typ.typ)).forall(refV))
+        bassume((SeqContains(e, ref) ==> TypeInformation(Heap(ref, memberName), member.f.typ.typ)).forall(refV))
       } :::
       bassume(wf(Heap, Mask)) ::
       {
@@ -1570,7 +1514,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         val (fV, f) = Boogie.NewBVar("f", FieldType(a), true);
         val (pcV,pc) = Boogie.NewBVar("p", tperm, true);
         Mask := Lambda(List(aV), List(refV, fV),
-          (FunctionApp("Seq#Contains", List(e, ref)) && f ==@ memberName).thenElse
+          (SeqContains(e, ref) && f ==@ memberName).thenElse
             (Lambda(List(), List(pcV),
               Boogie.Ite(pc ==@ "perm$R",
                 Mask(ref, f)("perm$R") + r,
@@ -1649,24 +1593,13 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
     Comment("end exhale")
   }
 
-  def Exhale(p: Expression, em: Boogie.Expr, eh: Boogie.Expr, error: ErrorMessage, check: Boolean): List[Boogie.Stmt] = p match {
+  def Exhale(p: Expression, em: Boogie.Expr, eh: Boogie.Expr, error: ErrorMessage, check: Boolean): List[Boogie.Stmt] = desugar(p) match {
     case pred@MemberAccess(e, p) if pred.isPredicate =>
       val tmp = Access(pred, Full);
       tmp.pos = pred.pos;
       Exhale(tmp, em , eh, error, check)
-    case acc@AccessAll(obj, perm) =>
-      obj.typ.Fields flatMap { f => 
-        val ma = MemberAccess(obj, f.id);
-        ma.f = f;
-        ma.pos = acc.pos;
-        val exhalee = Access(ma, perm);
-        exhalee.pos = acc.pos;
-        Exhale(exhalee, em, eh, error, check) }
-    case AccessSeq(s, None, perm) =>
-      s.typ.parameters(0).Fields flatMap { f =>
-        val ma = MemberAccess(At(s, IntLiteral(0)), f.id); ma.f = f; ma.pos = p.pos;
-        val exhalee = AccessSeq(s, Some(ma), perm); exhalee.pos = p.pos;
-        Exhale(exhalee, em, eh, error, check) }
+    case AccessAll(obj, perm) => throw new Exception("should be desugared")
+    case AccessSeq(s, None, perm) => throw new Exception("should be desugared")
     case acc@Access(e,perm:Write) =>
       val memberName = if(e.isPredicate) e.predicate.FullName else e.f.FullName;
 
@@ -1751,13 +1684,13 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         val mr = em(ref, memberName)("perm$R");
         val mn = em(ref, memberName)("perm$N");
 
-        bassert((FunctionApp("Seq#Contains", List(e, ref)) ==>
+        bassert((SeqContains(e, ref) ==>
           (perm match {
             case _: Read => mr ==@ 0 ==> n <= mn
             case _: Write => r <= mr && (r ==@ mr ==> 0 <= mn)
           })).forall(refV), error.pos, error.message + " Insufficient permissions") ::
         (em := Lambda(List(aV), List(refV, fV),
-          (FunctionApp("Seq#Contains", List(e, ref)) && f ==@ memberName).thenElse(
+          (SeqContains(e, ref) && f ==@ memberName).thenElse(
             Lambda(List(), List(pcV), (pc ==@ "perm$R").thenElse(mr - r, mn - n)),
             em(ref, f))))
       } :::
@@ -1835,6 +1768,79 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
     }
   }
 
+
+  // De-sugar expression (idempotent)
+  // * unroll wildcard pattern (for objects) in permission expression
+  // * convert sequence quantification into type quantification
+  def desugar(expr: Expression): Expression = expr transform {
+    _ match {
+      case AccessAll(obj, perm) =>
+        Some(obj.typ.Fields.map({f =>
+          val ma = MemberAccess(desugar(obj), f.id);
+          ma.f = f; ma.pos = expr.pos; ma.typ = f.typ.typ;
+          val acc = Access(ma, perm);
+          acc.pos = expr.pos; acc.typ = acc.typ; acc
+        }).foldLeft(BoolLiteral(true): Expression){(e1, e2) =>
+          val and = And(e1, e2);
+          and.pos = expr.pos; and.typ = BoolClass; and
+        })
+      case AccessSeq(s, None, perm) =>
+        Some(s.typ.parameters(0).Fields.map({(f) =>
+          val ma = MemberAccess(At(desugar(s), IntLiteral(0)), f.id);
+          ma.f = f; ma.pos = expr.pos; ma.typ = f.typ.typ;
+          val acc = AccessSeq(s, Some(ma), perm);
+          acc.pos = expr.pos; acc.typ = acc.typ; acc
+        }).foldLeft(BoolLiteral(true): Expression){(e1, e2) =>
+          val and = And(e1, e2);
+          and.pos = expr.pos; and.typ = BoolClass; and
+        })
+      case qe @ SeqQuantification(q, is, Range(min, max), e) =>
+        val dmin = desugar(min);
+        val dmax = desugar(max);
+        val dis = qe.variables;
+        val disx = dis map {v => new VariableExpr(v)};
+        val de = desugar(e);
+
+        val assumption = disx map {x =>
+          And(AtMost(dmin, x), Less(x, dmax))
+        } reduceLeft {(e0, e1) =>
+          And(e0, e1)
+        };
+        assumption transform {e => e.pos = expr.pos; None};
+        val body = q match {
+          case Forall => Implies(assumption, de);
+          case Exists => And(assumption, de);
+        }
+        body.pos = expr.pos;
+        val result = TypeQuantification(q, is, new Type(IntClass), body);
+        result.variables = dis;
+        Some(result);
+      case qe @ SeqQuantification(q, is, seq, e) =>
+        val dseq = desugar(seq);
+        val min = IntLiteral(0);
+        val max = Length(dseq);
+        val dis = qe.variables map {v => new Variable(v.UniqueName, new Type(IntClass))};
+        val disx = dis map {v => new VariableExpr(v)};
+        val de = SubstVars(desugar(e), qe.variables, disx map {x => At(dseq, x)});
+
+        val assumption = disx map {x =>
+          And(AtMost(min, x), Less(x, max))
+        } reduceLeft {(e0, e1) =>
+          And(e0, e1)
+        };
+        assumption transform {e => e.pos = expr.pos; None};
+        val body = q match {
+          case Forall => Implies(assumption, de);
+          case Exists => And(assumption, de);
+        }
+        body.pos = expr.pos;
+        val result = TypeQuantification(q, is, new Type(IntClass), body);
+        result.variables = dis;
+        Some(result);
+      case _ => None;
+    }
+  }
+
   // permissions
 
   def CanRead(obj: Boogie.Expr, field: Boogie.Expr): Boogie.Expr = new Boogie.FunctionApp("CanRead", Mask, obj, field)
@@ -2077,11 +2083,17 @@ object TranslationHelper {
   def NonEmptyMask(m: Expr) = ! FunctionApp("EmptyMask", List(m))
   def NonPredicateField(f: String) = FunctionApp("NonPredicateField", List(VarExpr(f)))
   def PredicateField(f: String) = FunctionApp("PredicateField", List(VarExpr(f)))
+  def cast(a: Expr, b: Expr) = FunctionApp("cast", List(a, b))
+
+  // Sequences
+
   def createEmptySeq = FunctionApp("Seq#Empty", List())
   def createSingletonSeq(e: Expr) = FunctionApp("Seq#Singleton", List(e)) 
   def createAppendSeq(a: Expr, b: Expr) = FunctionApp("Seq#Append", List(a, b)) 
   def createRange(min: Expr, max: Expr) = FunctionApp("Seq#Range", List(min, max))
-  def cast(a: Expr, b: Expr) = FunctionApp("cast", List(a, b))
+  def SeqLength(s: Expr) = FunctionApp("Seq#Length", List(s))
+  def SeqContains(s: Expr, elt: Expr) = FunctionApp("Seq#Contains", List(s, elt))
+  def SeqIndex(s: Expr, idx: Expr) = FunctionApp("Seq#Index", List(s, idx))
 
   def Variable2BVar(v: Variable) = new Boogie.BVar(v.UniqueName, v.t.typ)
   def Variable2BVarWhere(v: Variable) = NewBVarWhere(v.UniqueName, v.t)
@@ -2137,16 +2149,14 @@ object TranslationHelper {
       (e ==@ Boogie.Null()) || (dtype(e) ==@ className(cl))
     } else if (cl.IsSeq && cl.parameters(0).IsRef) {
       val (v,ve) = Boogie.NewBVar("$i", tint, true);
-      new Boogie.Forall(List(v), Nil,
-        0 <= ve && ve < Boogie.FunctionApp("Seq#Length", List(e)) ==>
-        TypeInformation(Boogie.FunctionApp("Seq#Index", List(e,ve)), cl.parameters(0)));
+      (0 <= ve && ve < SeqLength(e)
+        ==> TypeInformation(SeqIndex(e,ve), cl.parameters(0))).forall(v);
     } else {
       true
     }
   }
 
-  def Version(expr: Expression, etran: ExpressionTranslator): Boogie.Expr =
-  {
+  def Version(expr: Expression, etran: ExpressionTranslator): Boogie.Expr = {
     expr match{
       case pred@MemberAccess(e, p) if pred.isPredicate =>
         Version(Access(pred, Full), etran)
@@ -2162,26 +2172,7 @@ object TranslationHelper {
       case e => Boogie.VarExpr("nostate")
     }
   }
-  /* Unused code that would fail for a nontrivial class
-  def FieldTp(f: Field): String = {
-    f match {
-      case SpecialField("mu", _) => "Mu"
-      case SpecialField("held", _) => "int"
-      case SpecialField("rdheld", _) => "bool"
-      case SpecialField("joinable", _) => "int"
-      case f: Field => TrClass(f.typ.typ)
-    }
-  }
-
-  def TrClass(tp: Class): String = {
-    tp.id match {
-      case "int" => "int"
-      case "bool" => "bool"
-      case "$Mu" => "Mu"
-      case _ => if(tp.IsSeq) "seq" else "ref"
-    }
-  }
- */
+  
   def Preconditions(spec: List[Specification]): List[Expression] = {
     val result = spec flatMap ( s => s match {
       case Precondition(e) => List(e)
@@ -2258,10 +2249,6 @@ object TranslationHelper {
         val (assumptions, handled1) = automagic(bin.E0, handled);
         val result = automagic(bin.E1, handled1); 
         (assumptions ::: result._1, result._2)
-      case q@Forall(is, Range(min, max), e) =>
-        (Nil, handled)
-      case q@Forall(is, seq, e) =>
-        (Nil, handled)
       case EmptySeq(t) =>
         (Nil, handled)
       case ExplicitSeq(es) =>
@@ -2301,160 +2288,63 @@ object TranslationHelper {
 
   def SubstRd(e: Expression): Expression = e match {
     case Access(e, _:Write) =>
-      val r = Access(e,Epsilon); r.typ = BoolClass; r
-    case Access(_, _:Read) => e
+      val r = Access(e,Epsilon); r.pos = e.pos; r.typ = BoolClass; r
     case Implies(e0,e1) =>
-      val r = Implies(e0, SubstRd(e1)); r.typ = BoolClass; r
+      val r = Implies(e0, SubstRd(e1)); r.pos = e.pos; r.typ = BoolClass; r
     case And(e0,e1) =>
-      val r = And(SubstRd(e0), SubstRd(e1)); r.typ = BoolClass; r
-    case e => e
+      val r = And(SubstRd(e0), SubstRd(e1)); r.pos = e.pos; r.typ = BoolClass; r
+    case _ => e
   }
 
   def UnfoldPredicatesWithReceiverThis(expr: Expression): Expression = {
-    def unfoldPred(e: Expression): Expression = {
+    val func = (e:Expression) =>
       e match {
         case pred@MemberAccess(o, f) if pred.isPredicate && o.isInstanceOf[ThisExpr] =>
-          SubstThis(DefinitionOf(pred.predicate), o)
+          Some(SubstThis(DefinitionOf(pred.predicate), o))
         case Access(pred@MemberAccess(o, f), p) if pred.isPredicate && o.isInstanceOf[ThisExpr] =>
-          p match {
+          Some(p match {
             case Full => SubstThis(DefinitionOf(pred.predicate), o)
             case Frac(p) => FractionOf(SubstThis(DefinitionOf(pred.predicate), o), p)
             case Epsilon => EpsilonsOf(SubstThis(DefinitionOf(pred.predicate), o), IntLiteral(1))
             case Star => throw new Exception("not supported yet")
             case Epsilons(p) => EpsilonsOf(SubstThis(DefinitionOf(pred.predicate), o), p)
-          }
+          })
         case func@FunctionApplication(obj: ThisExpr, name, args) if 2<=TranslationOptions.defaults =>
-          SubstVars(func.f.definition, Some(obj), func.f.ins, args) 
-        case _ => manipulate(e, {ex => unfoldPred(ex)})
+          Some(SubstVars(func.f.definition, obj, func.f.ins, args))
+        case _ => None
       }
-    }
-    unfoldPred(expr)
+    AST.transform(expr, func)
   }
 
   // needed to do a _simultaneous_ substitution!
-  def SubstVars(expr: Expression, thisReplacement: Option[Expression], vs: List[Variable], xs: List[Expression]): Expression = {
-    def replace(e: Expression, sub: List[(Variable, Expression)]): Expression = {
-      e match {
-        case _: ThisExpr =>
-          thisReplacement match {
-            case Some(e) => e;
-            case None => e;
-          }
-        case e: VariableExpr =>
-          // TODO: this will update the value of x's position many times -- better than none
-          for ((v,x) <- sub if v == e.v) { x.pos = v.pos; x.typ = e.typ; return x }
-          e
-        case q: Quantification =>
-          // would be better if this is a part of manipulate method
-          val newSub = sub filter { xv => q.Is forall { variable => ! variable.id.equals(xv._1)}};
-          val result = q match {
-            case _ : Forall => Forall(q.Is, replace(q.Seq, sub), replace(q.E, newSub));
-            case _ : Exists => Exists(q.Is, replace(q.Seq, sub), replace(q.E, newSub));
-          }
-          result.variables = q.variables;
-          result.typ = q.typ;
-          result.pos = q.pos;
-          result
-        case _ => manipulate(e, {ex => replace(ex, sub)})
-      }
-    }
-    replace(expr, vs zip xs)
-  }
-
-  def SubstThis(expr: Expression, x: Expression): Expression = {
-    def replaceThis(e: Expression): Expression = {
-      e match {
-        case _: ThisExpr => x
-        case _ => manipulate(e, {ex => replaceThis(ex)})
-      }
+  def SubstVars(expr: Expression, x:Expression, vs:List[Variable], es:List[Expression]): Expression =
+    SubstVars(expr, Some(x), Map() ++ (vs zip es));
+  def SubstVars(expr: Expression, vs:List[Variable], es:List[Expression]): Expression =
+    SubstVars(expr, None, Map() ++ (vs zip es));
+  def SubstVars(expr: Expression, t: Option[Expression], vs: Map[Variable, Expression]): Expression = expr.transform {
+    _ match {
+      case _: ThisExpr if t.isDefined => t
+      case e: VariableExpr =>
+        if (vs.contains(e.v)) Some(vs(e.v)) else None;
+      case q: Quantification =>
+        q.variables foreach { (v) => if (vs.contains(v)) throw new Exception("cannot substitute a variable bound in the quantifier")}
+        None;
+      case _ => None;
     }
-    replaceThis(expr)
   }
 
-  def SubstResult(expr: Expression, x: Expression): Expression = {
-    def replaceThis(e: Expression): Expression = {
-      e match {
-        case _: Result => x
-        case _ => manipulate(e, {ex => replaceThis(ex)})
-      }
+  def SubstThis(expr: Expression, x: Expression): Expression = expr.transform {
+    _ match {
+      case _: ThisExpr => Some(x)
+      case _ => None
     }
-    replaceThis(expr)
   }
 
-  /** Applies function to the children of an AST node but not the node itself. */
-  def manipulate(expr: Expression, func: Expression => Expression): Expression = {
-    val result = expr match {
-      case e: Literal => expr
-      case _:ThisExpr => expr
-      case _:Result => expr
-      case e:VariableExpr => expr
-      case acc@MemberAccess(e,f) =>
-        val g = MemberAccess(func(e), f); g.f = acc.f; g.predicate = acc.predicate; g.isPredicate = acc.isPredicate; g
-      case Full | Epsilon | Star => expr
-      case Frac(perm) => Frac(func(perm))
-      case Epsilons(perm) => Epsilons(func(perm))
-      case Access(e, perm) => Access(func(e).asInstanceOf[MemberAccess], manipulate(perm, func).asInstanceOf[Permission]);
-      case AccessAll(obj, perm) => AccessAll(func(obj), manipulate(perm, func).asInstanceOf[Permission]);
-      case AccessSeq(s, None, perm) => AccessSeq(func(s), None, manipulate(perm, func).asInstanceOf[Permission])
-      case AccessSeq(s, Some(f), perm) => AccessSeq(func(s), Some(func(f).asInstanceOf[MemberAccess]), manipulate(perm, func).asInstanceOf[Permission])
-      case Credit(e, None) => Credit(func(e), None)
-      case Credit(e, Some(n)) => Credit(func(e), Some(func(n)))
-      case Holds(e) => Holds(func(e))
-      case RdHolds(e) => RdHolds(func(e))
-      case e: Assigned => e
-      case Old(e) => Old(func(e))
-      case IfThenElse(con, then, els) => IfThenElse(func(con), func(then), func(els))
-      case Not(e) => Not(func(e))
-      case funapp@FunctionApplication(obj, id, args) =>
-        val appl = FunctionApplication(func(obj), id, args map { arg => func(arg)}); appl.f = funapp.f; appl
-      case Unfolding(pred, e) =>
-        Unfolding(func(pred).asInstanceOf[Access], func(e))
-      case Iff(e0,e1) => Iff(func(e0), func(e1))
-      case Implies(e0,e1) => Implies(func(e0), func(e1))
-      case And(e0,e1) => And(func(e0), func(e1))
-      case Or(e0,e1) => Or(func(e0), func(e1))
-      case Eq(e0,e1) => Eq(func(e0), func(e1))
-      case Neq(e0,e1) => Neq(func(e0), func(e1))
-      case Less(e0,e1) => Less(func(e0), func(e1))
-      case AtMost(e0,e1) => AtMost(func(e0), func(e1))
-      case AtLeast(e0,e1) => AtLeast(func(e0), func(e1))
-      case Greater(e0,e1) => Greater(func(e0), func(e1))
-      case LockBelow(e0,e1) => LockBelow(func(e0), func(e1))
-      case Plus(e0,e1) => Plus(func(e0), func(e1))
-      case Minus(e0,e1) => Minus(func(e0), func(e1))
-      case Times(e0,e1) => Times(func(e0), func(e1))
-      case Div(e0,e1) => Div(func(e0), func(e1))
-      case Mod(e0,e1) => Mod(func(e0), func(e1))
-      case forall@Forall(i, seq, e) => val result = Forall(i, func(seq), func(e)); result.variables = forall.variables; result
-      case exists@Exists(i, seq, e) => val result = Exists(i, func(seq), func(e)); result.variables = exists.variables; result
-      case ExplicitSeq(es) =>
-        ExplicitSeq(es map { e => func(e) })
-      case Range(min, max)=>
-        Range(func(min), func(max))
-      case Append(e0, e1) =>
-        Append(func(e0), func(e1))
-      case At(e0, e1) =>
-        At(func(e0), func(e1))
-      case Drop(e0, e1) =>
-        Drop(func(e0), func(e1))
-      case Take(e0, e1) =>
-        Take(func(e0), func(e1))
-      case Length(e) =>
-        Length(func(e))
-      case Contains(e0, e1) =>
-        Contains(func(e0), func(e1))
-      case Eval(h, e) =>
-        Eval(h match { 
-          case AcquireState(obj) => AcquireState(func(obj)) 
-          case ReleaseState(obj) => ReleaseState(func(obj)) 
-          case CallState(token, obj, i, args) => CallState(func(token), func(obj), i, args map { a => func(a)})
-        }, func(e)) 
-    }
-    if(result.typ == null) {
-      result.typ = expr.typ;
+  def SubstResult(expr: Expression, x: Expression): Expression = expr.transform {
+    _ match {
+      case _: Result => Some(x)
+      case _ => None
     }
-    result.pos = expr.pos
-    result
   }
 }
 }
-- 
cgit v1.2.3