From a90615dc6e2673b591e154e59cd7f04e1ff90563 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Mon, 11 Jul 2011 19:43:42 -0700
Subject: Multiset forming operators added.

---
 Binaries/DafnyPrelude.bpl  |  18 +--
 Source/Dafny/Dafny.atg     |  23 +++-
 Source/Dafny/DafnyAst.cs   |  22 ++++
 Source/Dafny/Parser.cs     | 270 +++++++++++++++++++++++++--------------------
 Source/Dafny/Resolver.cs   |  11 +-
 Source/Dafny/Scanner.cs    |  21 ++--
 Source/Dafny/Translator.cs |  51 ++++++++-
 7 files changed, 262 insertions(+), 154 deletions(-)

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 1a8bb027..e11acf26 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -100,8 +100,10 @@ axiom (forall a: int :: { Math#clip(a) } a < 0  ==> Math#clip(a) == 0);
 
 type MultiSet T = [T]int;
 
-// ints are non-negative
-axiom (forall<T> o: T, ms: MultiSet T :: { ms[o] } 0 <= ms[o] );
+function $IsGoodMultiSet<T>(ms: MultiSet T): bool;
+// ints are non-negative, used after havocing.
+axiom (forall<T> ms: MultiSet T :: { $IsGoodMultiSet(ms) } 
+     $IsGoodMultiSet(ms) <==> (forall o: T :: { ms[o] } 0 <= ms[o]));
 
 function MultiSet#Empty<T>(): MultiSet T;
 axiom (forall<T> o: T :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0);
@@ -178,14 +180,12 @@ axiom (forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Disjoint(a,b) }
 // conversion to a multiset. each element in the original set has duplicity 1.
 function MultiSet#FromSet<T>(Set T): MultiSet T;
 axiom (forall<T> s: Set T, a: T :: { MultiSet#FromSet(s)[a] }
-  MultiSet#FromSet(s)[a] == 0 <==> !s[a] &&
-  MultiSet#FromSet(s)[a] == 1 <==> s[a]);
-
-// avoiding this for now.
-//function Set#Choose<T>(Set T, TickType): T;
-//axiom (forall<T> a: Set T, tick: TickType :: { Set#Choose(a, tick) }
-//  a != Set#Empty() ==> a[Set#Choose(a, tick)]);
+  (MultiSet#FromSet(s)[a] == 0 <==> !s[a]) &&
+  (MultiSet#FromSet(s)[a] == 1 <==> s[a]));
 
+// conversion to a multiset. each element in the original set has duplicity 1.
+function MultiSet#FromSeq<T>(Seq T): MultiSet T;
+// no axioms yet.
 
 // ---------------------------------------------------------------
 // -- Axiomatization of sequences --------------------------------
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 294df3d2..06af76d1 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1208,6 +1208,7 @@ UnaryExpression<out Expression/*!*/ e>
   | DottedIdentifiersAndFunction<out e>
     { Suffix<ref e> }
   | DisplayExpr<out e>
+  | MultiSetExpr<out e>
   | ConstAtomExpression<out e>
     { Suffix<ref e> }
   )
@@ -1259,18 +1260,30 @@ DisplayExpr<out Expression e>
 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
      IToken/*!*/ x = null;  List<Expression/*!*/>/*!*/ elements;
      e = dummyExpr;
-     bool isMulti = false;
   .)
-  ( [ "multi"  (. x = t; isMulti = true; .) ]
-    "{"                                        (. if (!isMulti) x = t;  elements = new List<Expression/*!*/>(); .)
-      [ Expressions<elements> ]                (. if (isMulti) e = new MultiSetDisplayExpr(x, elements);
-	                                                else e = new SetDisplayExpr(x, elements);.)
+  ( "{"                                        (. x = t;  elements = new List<Expression/*!*/>(); .)
+      [ Expressions<elements> ]                (. e = new SetDisplayExpr(x, elements);.)
     "}"
   | "["                                        (. x = t;  elements = new List<Expression/*!*/>(); .)
       [ Expressions<elements> ]                (. e = new SeqDisplayExpr(x, elements); .)
     "]"
   )
   .
+MultiSetExpr<out Expression e>
+= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
+     IToken/*!*/ x = null;  List<Expression/*!*/>/*!*/ elements;
+     e = dummyExpr;
+  .)
+  "multiset"                                   (. x = t; .)
+  ( "{"                                        (. elements = new List<Expression/*!*/>(); .)
+      [ Expressions<elements> ]                (. e = new MultiSetDisplayExpr(x, elements);.)
+    "}"
+  | "("                                        (. x = t;  elements = new List<Expression/*!*/>(); .)
+      Expression<out e>                        (. e = new MultiSetFormingExpr(x, e); .)
+    ")"
+  | (. SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); .)
+  )
+  .
 
 EndlessExpression<out Expression e>
 = (. IToken/*!*/ x;
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 3b53c046..871a8b34 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2275,6 +2275,28 @@ namespace Microsoft.Dafny {
     }
   }
 
+  public class MultiSetFormingExpr : Expression
+  {
+    [Peer]
+    public readonly Expression E;
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(E != null);
+    }
+
+    [Captured]
+    public MultiSetFormingExpr(IToken tok, Expression expr)
+      : base(tok) {
+      Contract.Requires(tok != null);
+      Contract.Requires(expr != null);
+      cce.Owner.AssignSame(this, expr);
+      E = expr;
+    }
+
+    public override IEnumerable<Expression> SubExpressions {
+      get { yield return E; }
+    }
+  }
   public class FreshExpr : Expression {
     public readonly Expression E;
     [ContractInvariantMethod]
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 091d9f5d..31a46f4b 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -20,7 +20,7 @@ public class Parser {
 	public const int _digits = 2;
 	public const int _arrayToken = 3;
 	public const int _string = 4;
-	public const int maxT = 106;
+	public const int maxT = 105;
 
 	const bool T = true;
 	const bool x = false;
@@ -387,7 +387,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			mm.Add(m); 
 		} else if (la.kind == 20) {
 			CouplingInvDecl(mmod, mm);
-		} else SynErr(107);
+		} else SynErr(106);
 	}
 
 	void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
@@ -470,7 +470,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			}
 			FunctionBody(out bb, out bodyStart, out bodyEnd);
 			body = bb; 
-		} else SynErr(108);
+		} else SynErr(107);
 		f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, decreases, body, attrs);
 		f.BodyStartTok = bodyStart;
 		f.BodyEndTok = bodyEnd;
@@ -502,7 +502,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		} else if (la.kind == 10) {
 			Get();
 			isRefinement = true; 
-		} else SynErr(109);
+		} else SynErr(108);
 		if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
 		if (isConstructor) {
 		  if (mmod.IsGhost) {
@@ -537,7 +537,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			}
 			BlockStmt(out bb, out bodyStart, out bodyEnd);
 			body = (BlockStmt)bb; 
-		} else SynErr(110);
+		} else SynErr(109);
 		if (isRefinement)
 		 m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
 		else if (isConstructor)
@@ -745,7 +745,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			ReferenceType(out tok, out ty);
 			break;
 		}
-		default: SynErr(111); break;
+		default: SynErr(110); break;
 		}
 	}
 
@@ -796,12 +796,12 @@ List<Expression/*!*/>/*!*/ decreases) {
 				Expression(out e);
 				Expect(17);
 				ens.Add(new MaybeFreeExpression(e, isFree)); 
-			} else SynErr(112);
+			} else SynErr(111);
 		} else if (la.kind == 32) {
 			Get();
 			DecreasesList(decreases, false);
 			Expect(17);
-		} else SynErr(113);
+		} else SynErr(112);
 	}
 
 	void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -891,7 +891,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 				GenericInstantiation(gt);
 			}
 			ty = new UserDefinedType(tok, tok.val, gt); 
-		} else SynErr(114);
+		} else SynErr(113);
 	}
 
 	void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {
@@ -923,7 +923,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();
 			DecreasesList(decreases, false);
 			Expect(17);
-		} else SynErr(115);
+		} else SynErr(114);
 	}
 
 	void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -942,7 +942,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			fe = new FrameExpression(new WildcardExpr(t), null); 
 		} else if (StartOf(8)) {
 			FrameExpression(out fe);
-		} else SynErr(116);
+		} else SynErr(115);
 	}
 
 	void PossiblyWildExpression(out Expression/*!*/ e) {
@@ -953,7 +953,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new WildcardExpr(t); 
 		} else if (StartOf(8)) {
 			Expression(out e);
-		} else SynErr(117);
+		} else SynErr(116);
 	}
 
 	void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -1030,7 +1030,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 					Get();
 					breakCount++; 
 				}
-			} else SynErr(118);
+			} else SynErr(117);
 			Expect(17);
 			s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); 
 			break;
@@ -1039,7 +1039,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			ReturnStmt(out s);
 			break;
 		}
-		default: SynErr(119); break;
+		default: SynErr(118); break;
 		}
 	}
 
@@ -1110,7 +1110,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 22) {
 			Get();
 			SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); 
-		} else SynErr(120);
+		} else SynErr(119);
 		s = new UpdateStmt(x, lhss, rhss); 
 	}
 
@@ -1183,13 +1183,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 				} else if (la.kind == 7) {
 					BlockStmt(out s, out bodyStart, out bodyEnd);
 					els = s; 
-				} else SynErr(121);
+				} else SynErr(120);
 			}
 			ifStmt = new IfStmt(x, guard, thn, els); 
 		} else if (la.kind == 7) {
 			AlternativeBlock(out alternatives);
 			ifStmt = new AlternativeStmt(x, alternatives); 
-		} else SynErr(122);
+		} else SynErr(121);
 	}
 
 	void WhileStmt(out Statement/*!*/ stmt) {
@@ -1215,7 +1215,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			LoopSpec(out invariants, out decreases, out mod);
 			AlternativeBlock(out alternatives);
 			stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives); 
-		} else SynErr(123);
+		} else SynErr(122);
 	}
 
 	void MatchStmt(out Statement/*!*/ s) {
@@ -1352,7 +1352,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(8)) {
 			Expression(out e);
 			r = new ExprRhs(e); 
-		} else SynErr(124);
+		} else SynErr(123);
 	}
 
 	void Lhs(out Expression e) {
@@ -1369,7 +1369,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			while (la.kind == 51 || la.kind == 53) {
 				Suffix(ref e);
 			}
-		} else SynErr(125);
+		} else SynErr(124);
 	}
 
 	void Expressions(List<Expression/*!*/>/*!*/ args) {
@@ -1392,7 +1392,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(8)) {
 			Expression(out ee);
 			e = ee; 
-		} else SynErr(126);
+		} else SynErr(125);
 		Expect(34);
 	}
 
@@ -1490,7 +1490,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(8)) {
 			Expression(out e);
 			arg = new Attributes.Argument(e); 
-		} else SynErr(127);
+		} else SynErr(126);
 	}
 
 	void EquivExpression(out Expression/*!*/ e0) {
@@ -1520,7 +1520,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();
 		} else if (la.kind == 68) {
 			Get();
-		} else SynErr(128);
+		} else SynErr(127);
 	}
 
 	void LogicalExpression(out Expression/*!*/ e0) {
@@ -1558,7 +1558,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();
 		} else if (la.kind == 70) {
 			Get();
-		} else SynErr(129);
+		} else SynErr(128);
 	}
 
 	void RelationalExpression(out Expression/*!*/ e) {
@@ -1656,7 +1656,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();
 		} else if (la.kind == 72) {
 			Get();
-		} else SynErr(130);
+		} else SynErr(129);
 	}
 
 	void OrOp() {
@@ -1664,7 +1664,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();
 		} else if (la.kind == 74) {
 			Get();
-		} else SynErr(131);
+		} else SynErr(130);
 	}
 
 	void Term(out Expression/*!*/ e0) {
@@ -1740,7 +1740,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			x = t;  op = BinaryExpr.Opcode.Ge; 
 			break;
 		}
-		default: SynErr(132); break;
+		default: SynErr(131); break;
 		}
 	}
 
@@ -1762,7 +1762,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 85) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Sub; 
-		} else SynErr(133);
+		} else SynErr(132);
 	}
 
 	void UnaryExpression(out Expression/*!*/ e) {
@@ -1782,7 +1782,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); 
 			break;
 		}
-		case 38: case 55: case 61: case 100: case 101: case 102: case 103: {
+		case 38: case 55: case 61: case 99: case 100: case 101: case 102: {
 			EndlessExpression(out e);
 			break;
 		}
@@ -1793,10 +1793,14 @@ List<Expression/*!*/>/*!*/ decreases) {
 			}
 			break;
 		}
-		case 7: case 51: case 97: {
+		case 7: case 51: {
 			DisplayExpr(out e);
 			break;
 		}
+		case 39: {
+			MultiSetExpr(out e);
+			break;
+		}
 		case 2: case 16: case 33: case 90: case 91: case 92: case 93: case 94: case 95: case 96: {
 			ConstAtomExpression(out e);
 			while (la.kind == 51 || la.kind == 53) {
@@ -1804,7 +1808,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			}
 			break;
 		}
-		default: SynErr(134); break;
+		default: SynErr(133); break;
 		}
 	}
 
@@ -1819,7 +1823,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 87) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Mod; 
-		} else SynErr(135);
+		} else SynErr(134);
 	}
 
 	void NegOp() {
@@ -1827,7 +1831,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();
 		} else if (la.kind == 89) {
 			Get();
-		} else SynErr(136);
+		} else SynErr(135);
 	}
 
 	void EndlessExpression(out Expression e) {
@@ -1839,7 +1843,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();
 			x = t; 
 			Expression(out e);
-			Expect(98);
+			Expect(97);
 			Expression(out e0);
 			Expect(56);
 			Expression(out e1);
@@ -1850,7 +1854,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			QuantifierGuts(out e);
 		} else if (la.kind == 38) {
 			ComprehensionExpr(out e);
-		} else SynErr(137);
+		} else SynErr(136);
 	}
 
 	void DottedIdentifiersAndFunction(out Expression e) {
@@ -1901,7 +1905,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			if (StartOf(8)) {
 				Expression(out ee);
 				e0 = ee; 
-				if (la.kind == 99) {
+				if (la.kind == 98) {
 					Get();
 					anyDots = true; 
 					if (StartOf(8)) {
@@ -1923,12 +1927,15 @@ List<Expression/*!*/>/*!*/ decreases) {
 						multipleIndices.Add(ee);
 						
 					}
-				} else SynErr(138);
-			} else if (la.kind == 99) {
+				} else SynErr(137);
+			} else if (la.kind == 98) {
 				Get();
-				Expression(out ee);
-				anyDots = true;  e1 = ee; 
-			} else SynErr(139);
+				anyDots = true; 
+				if (StartOf(8)) {
+					Expression(out ee);
+					e1 = ee; 
+				}
+			} else SynErr(138);
 			if (multipleIndices != null) {
 			 e = new MultiSelectExpr(x, e, multipleIndices);
 			 // make sure an array class with this dimensionality exists
@@ -1940,7 +1947,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			  }
 			  Contract.Assert(anyDots || e0 != null);
 			  if (anyDots) {
-			    Contract.Assert(e0 != null || e1 != null);
+			    //Contract.Assert(e0 != null || e1 != null);
 			    e = new SeqSelectExpr(x, false, e, e0, e1);
 			  } else if (e1 == null) {
 			    Contract.Assert(e0 != null);
@@ -1952,27 +1959,21 @@ List<Expression/*!*/>/*!*/ decreases) {
 			}
 			
 			Expect(52);
-		} else SynErr(140);
+		} else SynErr(139);
 	}
 
 	void DisplayExpr(out Expression e) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null);
 		IToken/*!*/ x = null;  List<Expression/*!*/>/*!*/ elements;
 		e = dummyExpr;
-		bool isMulti = false;
 		
-		if (la.kind == 7 || la.kind == 97) {
-			if (la.kind == 97) {
-				Get();
-				x = t; isMulti = true; 
-			}
-			Expect(7);
-			if (!isMulti) x = t;  elements = new List<Expression/*!*/>(); 
+		if (la.kind == 7) {
+			Get();
+			x = t;  elements = new List<Expression/*!*/>(); 
 			if (StartOf(8)) {
 				Expressions(elements);
 			}
-			if (isMulti) e = new MultiSetDisplayExpr(x, elements);
-			else e = new SetDisplayExpr(x, elements);
+			e = new SetDisplayExpr(x, elements);
 			Expect(8);
 		} else if (la.kind == 51) {
 			Get();
@@ -1982,6 +1983,32 @@ List<Expression/*!*/>/*!*/ decreases) {
 			}
 			e = new SeqDisplayExpr(x, elements); 
 			Expect(52);
+		} else SynErr(140);
+	}
+
+	void MultiSetExpr(out Expression e) {
+		Contract.Ensures(Contract.ValueAtReturn(out e) != null);
+		IToken/*!*/ x = null;  List<Expression/*!*/>/*!*/ elements;
+		e = dummyExpr;
+		
+		Expect(39);
+		x = t; 
+		if (la.kind == 7) {
+			Get();
+			elements = new List<Expression/*!*/>(); 
+			if (StartOf(8)) {
+				Expressions(elements);
+			}
+			e = new MultiSetDisplayExpr(x, elements);
+			Expect(8);
+		} else if (la.kind == 33) {
+			Get();
+			x = t;  elements = new List<Expression/*!*/>(); 
+			Expression(out e);
+			e = new MultiSetFormingExpr(x, e); 
+			Expect(34);
+		} else if (StartOf(18)) {
+			SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); 
 		} else SynErr(141);
 	}
 
@@ -2098,10 +2125,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expression range = null;
 		Expression/*!*/ body;
 		
-		if (la.kind == 100 || la.kind == 101) {
+		if (la.kind == 99 || la.kind == 100) {
 			Forall();
 			x = t;  univ = true; 
-		} else if (la.kind == 102 || la.kind == 103) {
+		} else if (la.kind == 101 || la.kind == 102) {
 			Exists();
 			x = t; 
 		} else SynErr(143);
@@ -2148,7 +2175,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		}
 		Expect(16);
 		Expression(out range);
-		if (la.kind == 104 || la.kind == 105) {
+		if (la.kind == 103 || la.kind == 104) {
 			QSep();
 			Expression(out body);
 		}
@@ -2182,17 +2209,17 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}
 
 	void Forall() {
-		if (la.kind == 100) {
+		if (la.kind == 99) {
 			Get();
-		} else if (la.kind == 101) {
+		} else if (la.kind == 100) {
 			Get();
 		} else SynErr(144);
 	}
 
 	void Exists() {
-		if (la.kind == 102) {
+		if (la.kind == 101) {
 			Get();
-		} else if (la.kind == 103) {
+		} else if (la.kind == 102) {
 			Get();
 		} else SynErr(145);
 	}
@@ -2212,9 +2239,9 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}
 
 	void QSep() {
-		if (la.kind == 104) {
+		if (la.kind == 103) {
 			Get();
-		} else if (la.kind == 105) {
+		} else if (la.kind == 104) {
 			Get();
 		} else SynErr(147);
 	}
@@ -2227,7 +2254,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expect(22);
 		Expect(1);
 		aName = t.val; 
-		if (StartOf(18)) {
+		if (StartOf(19)) {
 			AttributeArg(out aArg);
 			aArgs.Add(aArg); 
 			while (la.kind == 19) {
@@ -2251,25 +2278,26 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}
 
 	static readonly bool[,]/*!*/ set = {
-		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
-		{x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,T, x,T,T,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x},
-		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
-		{x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
-		{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x},
-		{x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x}
+		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x},
+		{x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,T, x,T,T,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x},
+		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x},
+		{x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x},
+		{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x},
+		{x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, T,T,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, T,x,x,x, T,T,T,x, x,x,x,T, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,T, T,x,x},
+		{x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x}
 
 	};
 } // end Parser
@@ -2391,51 +2419,51 @@ public class Errors {
 			case 94: s = "\"fresh\" expected"; break;
 			case 95: s = "\"allocated\" expected"; break;
 			case 96: s = "\"old\" expected"; break;
-			case 97: s = "\"multi\" expected"; break;
-			case 98: s = "\"then\" expected"; break;
-			case 99: s = "\"..\" expected"; break;
-			case 100: s = "\"forall\" expected"; break;
-			case 101: s = "\"\\u2200\" expected"; break;
-			case 102: s = "\"exists\" expected"; break;
-			case 103: s = "\"\\u2203\" expected"; break;
-			case 104: s = "\"::\" expected"; break;
-			case 105: s = "\"\\u2022\" expected"; break;
-			case 106: s = "??? expected"; break;
-			case 107: s = "invalid ClassMemberDecl"; break;
-			case 108: s = "invalid FunctionDecl"; break;
+			case 97: s = "\"then\" expected"; break;
+			case 98: s = "\"..\" expected"; break;
+			case 99: s = "\"forall\" expected"; break;
+			case 100: s = "\"\\u2200\" expected"; break;
+			case 101: s = "\"exists\" expected"; break;
+			case 102: s = "\"\\u2203\" expected"; break;
+			case 103: s = "\"::\" expected"; break;
+			case 104: s = "\"\\u2022\" expected"; break;
+			case 105: s = "??? expected"; break;
+			case 106: s = "invalid ClassMemberDecl"; break;
+			case 107: s = "invalid FunctionDecl"; break;
+			case 108: s = "invalid MethodDecl"; break;
 			case 109: s = "invalid MethodDecl"; break;
-			case 110: s = "invalid MethodDecl"; break;
-			case 111: s = "invalid TypeAndToken"; break;
+			case 110: s = "invalid TypeAndToken"; break;
+			case 111: s = "invalid MethodSpec"; break;
 			case 112: s = "invalid MethodSpec"; break;
-			case 113: s = "invalid MethodSpec"; break;
-			case 114: s = "invalid ReferenceType"; break;
-			case 115: s = "invalid FunctionSpec"; break;
-			case 116: s = "invalid PossiblyWildFrameExpression"; break;
-			case 117: s = "invalid PossiblyWildExpression"; break;
+			case 113: s = "invalid ReferenceType"; break;
+			case 114: s = "invalid FunctionSpec"; break;
+			case 115: s = "invalid PossiblyWildFrameExpression"; break;
+			case 116: s = "invalid PossiblyWildExpression"; break;
+			case 117: s = "invalid OneStmt"; break;
 			case 118: s = "invalid OneStmt"; break;
-			case 119: s = "invalid OneStmt"; break;
-			case 120: s = "invalid UpdateStmt"; break;
+			case 119: s = "invalid UpdateStmt"; break;
+			case 120: s = "invalid IfStmt"; break;
 			case 121: s = "invalid IfStmt"; break;
-			case 122: s = "invalid IfStmt"; break;
-			case 123: s = "invalid WhileStmt"; break;
-			case 124: s = "invalid Rhs"; break;
-			case 125: s = "invalid Lhs"; break;
-			case 126: s = "invalid Guard"; break;
-			case 127: s = "invalid AttributeArg"; break;
-			case 128: s = "invalid EquivOp"; break;
-			case 129: s = "invalid ImpliesOp"; break;
-			case 130: s = "invalid AndOp"; break;
-			case 131: s = "invalid OrOp"; break;
-			case 132: s = "invalid RelOp"; break;
-			case 133: s = "invalid AddOp"; break;
-			case 134: s = "invalid UnaryExpression"; break;
-			case 135: s = "invalid MulOp"; break;
-			case 136: s = "invalid NegOp"; break;
-			case 137: s = "invalid EndlessExpression"; break;
+			case 122: s = "invalid WhileStmt"; break;
+			case 123: s = "invalid Rhs"; break;
+			case 124: s = "invalid Lhs"; break;
+			case 125: s = "invalid Guard"; break;
+			case 126: s = "invalid AttributeArg"; break;
+			case 127: s = "invalid EquivOp"; break;
+			case 128: s = "invalid ImpliesOp"; break;
+			case 129: s = "invalid AndOp"; break;
+			case 130: s = "invalid OrOp"; break;
+			case 131: s = "invalid RelOp"; break;
+			case 132: s = "invalid AddOp"; break;
+			case 133: s = "invalid UnaryExpression"; break;
+			case 134: s = "invalid MulOp"; break;
+			case 135: s = "invalid NegOp"; break;
+			case 136: s = "invalid EndlessExpression"; break;
+			case 137: s = "invalid Suffix"; break;
 			case 138: s = "invalid Suffix"; break;
 			case 139: s = "invalid Suffix"; break;
-			case 140: s = "invalid Suffix"; break;
-			case 141: s = "invalid DisplayExpr"; break;
+			case 140: s = "invalid DisplayExpr"; break;
+			case 141: s = "invalid MultiSetExpr"; break;
 			case 142: s = "invalid ConstAtomExpression"; break;
 			case 143: s = "invalid QuantifierGuts"; break;
 			case 144: s = "invalid Forall"; break;
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 19a0da05..2b3128ae 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2390,7 +2390,7 @@ namespace Microsoft.Dafny {
       } else if (expr is FunctionCallExpr) {
         FunctionCallExpr e = (FunctionCallExpr)expr;
         ResolveFunctionCallExpr(e, twoState, false);
-        
+
       } else if (expr is OldExpr) {
         OldExpr e = (OldExpr)expr;
         if (!twoState) {
@@ -2398,7 +2398,14 @@ namespace Microsoft.Dafny {
         }
         ResolveExpression(e.E, twoState);
         expr.Type = e.E.Type;
-        
+
+      } else if (expr is MultiSetFormingExpr) {
+        MultiSetFormingExpr e = (MultiSetFormingExpr)expr;
+        ResolveExpression(e.E, twoState);
+        if (!UnifyTypes(e.E.Type, new SetType(new InferredTypeProxy())) && !UnifyTypes(e.E.Type, new SeqType(new InferredTypeProxy()))) {
+          Error(e.tok, "can only form a multiset from a seq or set.");
+        }
+        expr.Type = new MultiSetType(((CollectionType)e.E.Type).Arg);
       } else if (expr is FreshExpr) {
         FreshExpr e = (FreshExpr)expr;
         if (!twoState) {
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index a1fd9851..da72d8a1 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer {
 public class Scanner {
 	const char EOL = '\n';
 	const int eofSym = 0; /* pdt */
-	const int maxT = 106;
-	const int noSym = 106;
+	const int maxT = 105;
+	const int noSym = 105;
 
 
 	[ContractInvariantMethod]
@@ -538,10 +538,9 @@ public class Scanner {
 			case "fresh": t.kind = 94; break;
 			case "allocated": t.kind = 95; break;
 			case "old": t.kind = 96; break;
-			case "multi": t.kind = 97; break;
-			case "then": t.kind = 98; break;
-			case "forall": t.kind = 100; break;
-			case "exists": t.kind = 102; break;
+			case "then": t.kind = 97; break;
+			case "forall": t.kind = 99; break;
+			case "exists": t.kind = 101; break;
 			default: break;
 		}
 	}
@@ -716,15 +715,15 @@ public class Scanner {
 			case 51:
 				{t.kind = 89; break;}
 			case 52:
-				{t.kind = 99; break;}
+				{t.kind = 98; break;}
 			case 53:
-				{t.kind = 101; break;}
+				{t.kind = 100; break;}
 			case 54:
-				{t.kind = 103; break;}
+				{t.kind = 102; break;}
 			case 55:
-				{t.kind = 104; break;}
+				{t.kind = 103; break;}
 			case 56:
-				{t.kind = 105; break;}
+				{t.kind = 104; break;}
 			case 57:
 				recEnd = pos; recKind = 15;
 				if (ch == '>') {AddCh(); goto case 28;}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index b0f42465..dacbf143 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1554,6 +1554,9 @@ namespace Microsoft.Dafny {
       } else if (expr is OldExpr) {
         OldExpr e = (OldExpr)expr;
         return new Bpl.OldExpr(expr.tok, IsTotal(e.E, etran));
+      } else if (expr is MultiSetFormingExpr) {
+        MultiSetFormingExpr e = (MultiSetFormingExpr)expr;
+        return IsTotal(e.E, etran);
       } else if (expr is FreshExpr) {
         FreshExpr e = (FreshExpr)expr;
         return IsTotal(e.E, etran);
@@ -1699,6 +1702,9 @@ namespace Microsoft.Dafny {
       } else if (expr is OldExpr) {
         OldExpr e = (OldExpr)expr;
         return new Bpl.OldExpr(expr.tok, CanCallAssumption(e.E, etran));
+      } else if (expr is MultiSetFormingExpr) {
+        MultiSetFormingExpr e = (MultiSetFormingExpr)expr;
+        return CanCallAssumption(e.E, etran);
       } else if (expr is FreshExpr) {
         FreshExpr e = (FreshExpr)expr;
         return CanCallAssumption(e.E, etran);
@@ -2035,6 +2041,9 @@ namespace Microsoft.Dafny {
       } else if (expr is OldExpr) {
         OldExpr e = (OldExpr)expr;
         CheckWellformed(e.E, options, locals, builder, etran.Old);
+      } else if (expr is MultiSetFormingExpr) {
+        MultiSetFormingExpr e = (MultiSetFormingExpr)expr;
+        CheckWellformed(e.E, options, locals, builder, etran.Old);
       } else if (expr is FreshExpr) {
         FreshExpr e = (FreshExpr)expr;
         CheckWellformed(e.E, options, locals, builder, etran);
@@ -4057,7 +4066,7 @@ namespace Microsoft.Dafny {
 
       } else if (type is MultiSetType) {
         MultiSetType st = (MultiSetType)type;
-        // (forall t: BoxType :: { x[t] } 0 < x[t] ==> Unbox(t)-has-the-expected-type)
+        // $IsGoodMultiSet(x) && (forall t: BoxType :: { x[t] } 0 < x[t] ==> Unbox(t)-has-the-expected-type)
         Bpl.BoundVariable tVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$t#" + otherTmpVarCount, predef.BoxType));
         otherTmpVarCount++;
         Bpl.Expr t = new Bpl.IdentifierExpr(tok, tVar);
@@ -4067,9 +4076,10 @@ namespace Microsoft.Dafny {
         Bpl.Expr wh = GetWhereClause(tok, unboxT, st.Arg, etran);
         if (wh != null) {
           Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubT));
-          return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(xSubT, wh));
+          return Bpl.Expr.And(FunctionCall(tok, BuiltinFunction.IsGoodMultiSet, Bpl.Type.Bool, x),
+                              new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(xSubT, wh)));
         }
-
+        return FunctionCall(tok, BuiltinFunction.IsGoodMultiSet, null, x);
       } else if (type is SeqType) {
         SeqType st = (SeqType)type;
         // (forall i: int :: { Seq#Index(x,i) }
@@ -4790,11 +4800,22 @@ namespace Microsoft.Dafny {
           }
           Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(dtv.tok, dtv.Ctor.FullName, predef.DatatypeType);
           return new Bpl.NAryExpr(dtv.tok, new Bpl.FunctionCall(id), args);
-            
+
         } else if (expr is OldExpr) {
           OldExpr e = (OldExpr)expr;
           return new Bpl.OldExpr(expr.tok, TrExpr(e.E));
-        
+
+        } else if (expr is MultiSetFormingExpr) {
+          MultiSetFormingExpr e = (MultiSetFormingExpr)expr;
+          if (e.E.Type is SetType) {
+            return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetFromSet, translator.TrType(cce.NonNull((SetType)e.E.Type).Arg), TrExpr(e.E));
+          } else if (e.E.Type is SeqType) {
+            return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetFromSeq, translator.TrType(cce.NonNull((SeqType)e.E.Type).Arg), TrExpr(e.E));
+          } else {
+            Contract.Assert(false); throw new cce.UnreachableException();
+          }
+
+
         } else if (expr is FreshExpr) {
           FreshExpr e = (FreshExpr)expr;
           Bpl.Expr oldHeap = new Bpl.OldExpr(expr.tok, HeapExpr);
@@ -5453,6 +5474,9 @@ namespace Microsoft.Dafny {
       MultiSetEqual,
       MultiSetSubset,
       MultiSetDisjoint,
+      MultiSetFromSet,
+      MultiSetFromSeq,
+      IsGoodMultiSet,
 
       SeqLength,
       SeqEmpty,
@@ -5472,7 +5496,7 @@ namespace Microsoft.Dafny {
       Box,
       Unbox,
       IsCanonicalBoolBox,
-      
+
       IsGoodHeap,
       HeapSucc,
       
@@ -5574,6 +5598,18 @@ namespace Microsoft.Dafny {
           Contract.Assert(args.Length == 2);
           Contract.Assert(typeInstantiation == null);
           return FunctionCall(tok, "MultiSet#Disjoint", Bpl.Type.Bool, args);
+        case BuiltinFunction.MultiSetFromSet:
+          Contract.Assert(args.Length == 1);
+          Contract.Assert(typeInstantiation != null);
+          return FunctionCall(tok, "MultiSet#FromSet", predef.MultiSetType(tok, typeInstantiation), args);
+        case BuiltinFunction.MultiSetFromSeq:
+          Contract.Assert(args.Length == 1);
+          Contract.Assert(typeInstantiation != null);
+          return FunctionCall(tok, "MultiSet#FromSeq", predef.MultiSetType(tok, typeInstantiation), args);
+        case BuiltinFunction.IsGoodMultiSet:
+          Contract.Assert(args.Length == 1);
+          Contract.Assert(typeInstantiation == null);
+          return FunctionCall(tok, "$IsGoodMultiSet", Bpl.Type.Bool, args);
         // avoiding this for now
         /*case BuiltinFunction.SetChoose:
           Contract.Assert(args.Length == 2);
@@ -6113,6 +6149,9 @@ namespace Microsoft.Dafny {
       } else if (expr is OldExpr) {
         var e = (OldExpr)expr;
         return VarOccursInArgumentToRecursiveFunction(e.E, n, p);
+      } else if (expr is MultiSetFormingExpr) {
+        var e = (MultiSetFormingExpr)expr;
+        return VarOccursInArgumentToRecursiveFunction(e.E, n, p);
       } else if (expr is FreshExpr) {
         var e = (FreshExpr)expr;
         return VarOccursInArgumentToRecursiveFunction(e.E, n, null);
-- 
cgit v1.2.3