Added tuples and tuple types. Syntax is the expected one, namely parentheses around a comma-delimited list of expressions or types. Unit and the unit type are denoted ().

11 files changed, 342 insertions, 58 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 537dae1d..5b8f8cc5 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -30,6 +30,9 @@ namespace Microsoft.Dafny
       if (d is ArbitraryTypeDecl) {

         var dd = (ArbitraryTypeDecl)d;

         return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, CloneAttributes(dd.Attributes));

+      } else if (d is TupleTypeDecl) {

+        var dd = (TupleTypeDecl)d;

+        return new TupleTypeDecl(dd.Dims, dd.Module);

       } else if (d is IndDatatypeDecl) {

         var dd = (IndDatatypeDecl)d;

         var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 56c6edc2..fcf8a2ca 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -107,6 +107,10 @@ namespace Microsoft.Dafny {
           indent += IndentAmount;

         }

         foreach (TopLevelDecl d in m.TopLevelDecls) {

+          bool compileIt = true;

+          if (Attributes.ContainsBool(d.Attributes, "compile", ref compileIt) && !compileIt) {

+            continue;

+          }

           wr.WriteLine();

           if (d is ArbitraryTypeDecl) {

             var at = (ArbitraryTypeDecl)d;

@@ -411,7 +415,12 @@ namespace Microsoft.Dafny {
 

         if (dt is IndDatatypeDecl) {

           Indent(ind); wr.WriteLine("public override string ToString() {");

-          string nm = (dt.Module.IsDefaultModule ? "" : dt.Module.CompileName + ".") + dt.CompileName + "." + ctor.CompileName;

+          string nm;

+          if (dt is TupleTypeDecl) {

+            nm = "";

+          } else {

+            nm = (dt.Module.IsDefaultModule ? "" : dt.Module.CompileName + ".") + dt.CompileName + "." + ctor.CompileName;

+          }

           Indent(ind + IndentAmount); wr.WriteLine("string s = \"{0}\";", nm);

           if (ctor.Formals.Count != 0) {

             Indent(ind + IndentAmount); wr.WriteLine("s += \"(\";");

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 2ab70c4f..5c1148c6 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -739,8 +739,9 @@ Type<out Type/*!*/ ty>
   TypeAndToken<out tok, out ty>

   .

 TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>

-= (. Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

-     List<Type/*!*/>/*!*/ gt;

+= (. Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);

+     tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

+     List<Type> gt;

   .)

   ( "bool"                          (. tok = t; .)

   | "nat"                           (. tok = t;  ty = new NatType(); .)

@@ -774,6 +775,20 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
                                          ty = new MapType(gt[0], gt[1]);

                                        }

                                     .)

+  | "("                             (. tok = t; gt = new List<Type>(); .)

+    [ Type<out ty>                  (. gt.Add(ty); .)

+      { "," Type<out ty>            (. gt.Add(ty); .)

+      }

+    ]

+    ")"                             (. if (gt.Count == 1) {

+                                         // just return the type 'ty'

+                                       } else {

+                                         // make sure the nullary tuple type exists

+                                         var dims = gt.Count;

+                                         var tmp = theBuiltIns.TupleType(tok, dims, true);

+                                         ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(dims), gt, new List<IToken>());

+                                       }

+                                    .)

   | ReferenceType<out tok, out ty>

   )

   .

@@ -1876,25 +1891,51 @@ ConstAtomExpression<out Expression e>
   | "|"                                        (. x = t; .)

       Expression<out e, true>                  (. e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); .)

     "|"

-  | "("                                        (. x = t; .)

-      Expression<out e, true>                  (. e = new ParensExpression(x, e); .)

-    ")"

-  | "real"									   (. x = t; .)

-    "("										   (. IToken openParen = t; .)

-	Expression<out e, true>

-	")"										   (. IToken classTok = new Token(t.line, t.col); classTok.val = "Real";

-											      IToken fnTok = new Token(t.line, t.col); fnTok.val = "IntToReal";

-											      //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });

-												  e = new FunctionCallExpr(x, "IntToReal", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });

-												.)

-  | "int"									   (. x = t; .)

-    "("										   (. IToken openParen = t; .)

-	Expression<out e, true>

-	")"										   (. IToken classTok = new Token(t.line, t.col); classTok.val = "Real";

-											      IToken fnTok = new Token(t.line, t.col); fnTok.val = "RealToInt";

-											      //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });

-												  e = new FunctionCallExpr(x, "RealToInt", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });

-												.)

+  | ParensExpression<out e>

+  | "real"                                     (. x = t; .)

+    "("                                        (. IToken openParen = t; .)

+    Expression<out e, true>

+    ")"                                        (. IToken classTok = new Token(t.line, t.col); classTok.val = "Real";

+                                                  IToken fnTok = new Token(t.line, t.col); fnTok.val = "IntToReal";

+                                                  //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });

+                                                  e = new FunctionCallExpr(x, "IntToReal", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });

+                                               .)

+  | "int"                                      (. x = t; .)

+    "("                                        (. IToken openParen = t; .)

+    Expression<out e, true>

+    ")"                                        (. IToken classTok = new Token(t.line, t.col); classTok.val = "Real";

+                                                  IToken fnTok = new Token(t.line, t.col); fnTok.val = "RealToInt";

+                                                  //e = new IdentifierSequence(new List<IToken>() { classTok, fnTok }, openParen, new List<Expression/*!*/>() { e });

+                                                  e = new FunctionCallExpr(x, "RealToInt", new StaticReceiverExpr(x, theBuiltIns.RealClass), openParen, new List<Expression/*!*/>() { e });

+                                               .)

+  )

+  .

+ParensExpression<out Expression e>

+= (. IToken x;

+     List<Expression> args = null;

+  .)

+  "("                                 (. x = t; e = null; .)

+  ( ")"                               (. // unit

+                                         // make sure the nullary tuple type exists

+                                         var tmp = theBuiltIns.TupleType(x, 0, true);

+                                         e = new DatatypeValue(x, BuiltIns.TupleTypeName(0), BuiltIns.TupleTypeCtorName, new List<Expression>());

+                                      .)

+  | Expression<out e, true>

+    { ","                             (. if (args == null) {

+                                           args = new List<Expression>();

+                                           args.Add(e);  // add the first argument, which was parsed above

+                                        }

+                                      .)

+      Expression<out e, true>         (. args.Add(e); .)

+    }

+    ")"                               (. if (args == null) {

+                                           e = new ParensExpression(x, e);

+                                         } else {

+                                           // make sure the corresponding tuple type exists

+                                           var tmp = theBuiltIns.TupleType(x, args.Count, true);

+                                           e = new DatatypeValue(x, BuiltIns.TupleTypeName(args.Count), BuiltIns.TupleTypeCtorName, args);

+                                         }

+                                      .)

   )

   .

 DisplayExpr<out Expression e>

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index ad98a0c0..55dc973f 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -88,15 +88,17 @@ namespace Microsoft.Dafny {
   {

     public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, null, null, null, true);

     Dictionary<int, ClassDecl> arrayTypeDecls = new Dictionary<int, ClassDecl>();

+    Dictionary<int, TupleTypeDecl> tupleTypeDecls = new Dictionary<int, TupleTypeDecl>();

     public readonly ClassDecl ObjectDecl;

     public readonly ClassDecl RealClass;

     //public readonly Function RealToInt;

     //public readonly Function IntToReal;

     public BuiltIns() {

       // create class 'object'

-      ObjectDecl = new ClassDecl(Token.NoToken, "object", SystemModule, new List<TypeParameter>(), new List<MemberDecl>(), null);

+      ObjectDecl = new ClassDecl(Token.NoToken, "object", SystemModule, new List<TypeParameter>(), new List<MemberDecl>(), DontCompile());

       SystemModule.TopLevelDecls.Add(ObjectDecl);

       // add one-dimensional arrays, since they may arise during type checking

+      // Arrays of other dimensions may be added during parsing as the parser detects the need for these

       UserDefinedType tmp = ArrayType(Token.NoToken, 1, Type.Int, true);

       // add real number functions

       Function RealToInt = new Function(Token.NoToken, "RealToInt", true, true, new List<TypeParameter>(), Token.NoToken,

@@ -108,12 +110,19 @@ namespace Microsoft.Dafny {
         new List<FrameExpression>(), new List<Expression>(), new Specification<Expression>(new List<Expression>(), null),

         null, null, Token.NoToken);

       RealClass = new ClassDecl(Token.NoToken, "Real", SystemModule, new List<TypeParameter>(),

-        new List<MemberDecl>() { RealToInt, IntToReal }, null);

+        new List<MemberDecl>() { RealToInt, IntToReal }, DontCompile());

       RealToInt.EnclosingClass = RealClass;

       IntToReal.EnclosingClass = RealClass;

       RealToInt.IsBuiltin = true;

       IntToReal.IsBuiltin = true;

       SystemModule.TopLevelDecls.Add(RealClass);

+      // Note, in addition to these types, the _System module contains tuple types.  These tuple types are added to SystemModule

+      // by the parser as the parser detects the need for these.

+    }

+

+    private Attributes DontCompile() {

+      var flse = new Attributes.Argument(Token.NoToken, Expression.CreateBoolLiteral(Token.NoToken, false));

+      return new Attributes("compile", new List<Attributes.Argument>() { flse }, null);

     }

 

     public UserDefinedType ArrayType(int dims, Type arg) {

@@ -129,7 +138,7 @@ namespace Microsoft.Dafny {
       typeArgs.Add(arg);

       UserDefinedType udt = new UserDefinedType(tok, ArrayClassName(dims), typeArgs, null);

       if (allowCreationOfNewClass && !arrayTypeDecls.ContainsKey(dims)) {

-        ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule);

+        ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule, DontCompile());

         for (int d = 0; d < dims; d++) {

           string name = dims == 1 ? "Length" : "Length" + d;

           string compiledName = dims == 1 ? "Length" : "GetLength(" + d + ")";

@@ -152,6 +161,30 @@ namespace Microsoft.Dafny {
         return "array" + dims;

       }

     }

+

+    public TupleTypeDecl TupleType(IToken tok, int dims, bool allowCreationOfNewType) {

+      Contract.Requires(tok != null);

+      Contract.Requires(0 <= dims);

+      Contract.Ensures(Contract.Result<TupleTypeDecl>() != null);

+

+      TupleTypeDecl tt;

+      if (!tupleTypeDecls.TryGetValue(dims, out tt)) {

+        Contract.Assume(allowCreationOfNewType);  // the parser should ensure that all needed tuple types exist by the time of resolution

+        tt = new TupleTypeDecl(dims, SystemModule);

+        tupleTypeDecls.Add(dims, tt);

+        SystemModule.TopLevelDecls.Add(tt);

+      }

+      return tt;

+    }

+    public static string TupleTypeName(int dims) {

+      Contract.Requires(0 <= dims);

+      return "_tuple#" + dims;

+    }

+    public static bool IsTupleTypeName(string s) {

+      Contract.Requires(s != null);

+      return s.StartsWith("_tuple#");

+    }

+    public const string TupleTypeCtorName = "_#Make";  // the printer wants this name to be uniquely recognizable

   }

 

   public class Attributes {

@@ -714,6 +747,9 @@ namespace Microsoft.Dafny {
     [Pure]

     public override string TypeName(ModuleDefinition context) {

       Contract.Ensures(Contract.Result<string>() != null);

+      if (BuiltIns.IsTupleTypeName(Name)) {

+        return "(" + Util.Comma(",", TypeArgs, ty => ty.TypeName(context)) + ")";

+      }

       string s = "";

       foreach (var t in Path) {

         if (context != null && t == context.tok) {

@@ -1355,10 +1391,10 @@ namespace Microsoft.Dafny {
 

   public class ArrayClassDecl : ClassDecl {

     public readonly int Dims;

-    public ArrayClassDecl(int dims, ModuleDefinition module)

+    public ArrayClassDecl(int dims, ModuleDefinition module, Attributes attrs)

     : base(Token.NoToken, BuiltIns.ArrayClassName(dims), module,

       new List<TypeParameter>(new TypeParameter[]{new TypeParameter(Token.NoToken, "arg")}),

-      new List<MemberDecl>(), null)

+      new List<MemberDecl>(), attrs)

     {

       Contract.Requires(1 <= dims);

       Contract.Requires(module != null);

@@ -1367,7 +1403,8 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public abstract class DatatypeDecl : TopLevelDecl {

+  public abstract class DatatypeDecl : TopLevelDecl

+  {

     public readonly List<DatatypeCtor> Ctors;

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -1413,6 +1450,52 @@ namespace Microsoft.Dafny {
     }

   }

 

+  public class TupleTypeDecl : IndDatatypeDecl

+  {

+    public readonly int Dims;

+    /// <summary>

+    /// Construct a resolved built-in tuple type with "dim" arguments.  "systemModule" is expected to be the _System module.

+    /// </summary>

+    public TupleTypeDecl(int dims, ModuleDefinition systemModule)

+      : this(systemModule, CreateTypeParameters(dims)) {

+      Contract.Requires(0 <= dims);

+      Contract.Requires(systemModule != null);

+    }

+    private TupleTypeDecl(ModuleDefinition systemModule, List<TypeParameter> typeArgs)

+      : base(Token.NoToken, BuiltIns.TupleTypeName(typeArgs.Count), systemModule, typeArgs, CreateConstructors(typeArgs), null) {

+      Contract.Requires(systemModule != null);

+      Contract.Requires(typeArgs != null);

+      Dims = typeArgs.Count;

+      foreach (var ctor in Ctors) {

+        ctor.EnclosingDatatype = this;  // resolve here

+        DefaultCtor = ctor;

+        TypeParametersUsedInConstructionByDefaultCtor = new bool[typeArgs.Count];

+        for (int i = 0; i < typeArgs.Count; i++) {

+          TypeParametersUsedInConstructionByDefaultCtor[i] = true;

+        }

+      }

+    }

+    private static List<TypeParameter> CreateTypeParameters(int dims) {

+      Contract.Requires(0 <= dims);

+      var ts = new List<TypeParameter>();

+      for (int i = 0; i < dims; i++) {

+        ts.Add(new TypeParameter(Token.NoToken, "T" + i));

+      }

+      return ts;

+    }

+    private static List<DatatypeCtor> CreateConstructors(List<TypeParameter> typeArgs) {

+      Contract.Requires(typeArgs != null);

+      var formals = new List<Formal>();

+      for (int i = 0; i < typeArgs.Count; i++) {

+        var tp = typeArgs[i];

+        var f = new Formal(Token.NoToken, i.ToString(), new UserDefinedType(Token.NoToken, tp.Name, tp), true, false);

+        formals.Add(f);

+      }

+      var ctor = new DatatypeCtor(Token.NoToken, BuiltIns.TupleTypeCtorName, formals, null);

+      return new List<DatatypeCtor>() { ctor };

+    }

+  }

+

   public class CoDatatypeDecl : DatatypeDecl

   {

     public CoDatatypeDecl SscRepr;  // filled in during resolution

@@ -1918,7 +2001,7 @@ namespace Microsoft.Dafny {
       }

       return UniqueName;

     }

-    static char[] specialChars = new char[] { '\'', '_', '?', '\\' };

+    static char[] specialChars = new char[] { '\'', '_', '?', '\\', '#' };

     public static string CompilerizeName(string nm) {

       if ('0' <= nm[0] && nm[0] <= '9') {

         // the identifier is one that consists of just digits

@@ -1942,6 +2025,7 @@ namespace Microsoft.Dafny {
             case '_': name += "__"; break;

             case '?': name += "_q"; break;

             case '\\': name += "_b"; break;

+            case '#': name += "_h"; break;

             default:

               Contract.Assume(false);  // unexpected character

               break;

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 969774db..a7f058db 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1115,8 +1115,9 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 	}

 

 	void TypeAndToken(out IToken/*!*/ tok, out Type/*!*/ ty) {

-		Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

-		List<Type/*!*/>/*!*/ gt;

+		Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);

+		tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

+		List<Type> gt;

 		

 		switch (la.kind) {

 		case 52: {

@@ -1195,6 +1196,30 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 			

 			break;

 		}

+		case 11: {

+			Get();

+			tok = t; gt = new List<Type>(); 

+			if (StartOf(10)) {

+				Type(out ty);

+				gt.Add(ty); 

+				while (la.kind == 31) {

+					Get();

+					Type(out ty);

+					gt.Add(ty); 

+				}

+			}

+			Expect(12);

+			if (gt.Count == 1) {

+			 // just return the type 'ty'

+			} else {

+			 // make sure the nullary tuple type exists

+			 var dims = gt.Count;

+			 var tmp = theBuiltIns.TupleType(tok, dims, true);

+			 ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(dims), gt, new List<IToken>());

+			}

+			

+			break;

+		}

 		case 1: case 5: case 60: {

 			ReferenceType(out tok, out ty);

 			break;

@@ -3352,11 +3377,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			break;

 		}

 		case 11: {

-			Get();

-			x = t; 

-			Expression(out e, true);

-			e = new ParensExpression(x, e); 

-			Expect(12);

+			ParensExpression(out e);

 			break;

 		}

 		case 55: {

@@ -3427,6 +3448,41 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 	}

 

+	void ParensExpression(out Expression e) {

+		IToken x;

+		List<Expression> args = null;

+		

+		Expect(11);

+		x = t; e = null; 

+		if (la.kind == 12) {

+			Get();

+			var tmp = theBuiltIns.TupleType(x, 0, true);

+			e = new DatatypeValue(x, BuiltIns.TupleTypeName(0), BuiltIns.TupleTypeCtorName, new List<Expression>());

+			

+		} else if (StartOf(16)) {

+			Expression(out e, true);

+			while (la.kind == 31) {

+				Get();

+				if (args == null) {

+				 args = new List<Expression>();

+				 args.Add(e);  // add the first argument, which was parsed above

+				}

+				

+				Expression(out e, true);

+				args.Add(e); 

+			}

+			Expect(12);

+			if (args == null) {

+			 e = new ParensExpression(x, e);

+			} else {

+			 // make sure the corresponding tuple type exists

+			 var tmp = theBuiltIns.TupleType(x, args.Count, true);

+			 e = new DatatypeValue(x, BuiltIns.TupleTypeName(args.Count), BuiltIns.TupleTypeCtorName, args);

+			}

+			

+		} else SynErr(223);

+	}

+

 	void MapLiteralExpressions(out List<ExpressionPair> elements) {

 		Expression/*!*/ d, r;

 		elements = new List<ExpressionPair/*!*/>(); 

@@ -3448,7 +3504,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 125) {

 			Get();

-		} else SynErr(223);

+		} else SynErr(224);

 	}

 

 	void MatchExpression(out Expression e, bool allowSemi) {

@@ -3471,7 +3527,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(10);

 		} else if (StartOf(31)) {

 			if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); } 

-		} else SynErr(224);

+		} else SynErr(225);

 		e = new MatchExpr(x, e, cases, usesOptionalBrace); 

 	}

 

@@ -3489,7 +3545,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 122 || la.kind == 123) {

 			Exists();

 			x = t; 

-		} else SynErr(225);

+		} else SynErr(226);

 		QuantifierDomain(out bvars, out attrs, out range);

 		QSep();

 		Expression(out body, allowSemi);

@@ -3537,7 +3593,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			AssumeStmt(out s);

 		} else if (la.kind == 88) {

 			CalcStmt(out s);

-		} else SynErr(226);

+		} else SynErr(227);

 	}

 

 	void LetExpr(out Expression e, bool allowSemi) {

@@ -3577,7 +3633,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 }

 			}

 			

-		} else SynErr(227);

+		} else SynErr(228);

 		Expression(out e, false);

 		letRHSs.Add(e); 

 		while (la.kind == 31) {

@@ -3628,7 +3684,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			IdentTypeOptional(out bv);

 			pat = new CasePattern(bv.tok, bv);

 			

-		} else SynErr(228);

+		} else SynErr(229);

 	}

 

 	void CaseExpression(out MatchCaseExpr c, bool allowSemi) {

@@ -3661,7 +3717,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 121) {

 			Get();

-		} else SynErr(229);

+		} else SynErr(230);

 	}

 

 	void Exists() {

@@ -3669,7 +3725,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 123) {

 			Get();

-		} else SynErr(230);

+		} else SynErr(231);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -3714,8 +3770,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,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, 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,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,T,T,x, x,T,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, 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,T,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, 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,T,T,x, x,T,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,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,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,x, x,x,x,x, x,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},

 		{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,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,T,T,T, T,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,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,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,x,T,T, x,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, 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,x, x,x,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,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},

@@ -3986,14 +4042,15 @@ public class Errors {
 			case 220: s = "invalid MultiSetExpr"; break;

 			case 221: s = "invalid ConstAtomExpression"; break;

 			case 222: s = "invalid Nat"; break;

-			case 223: s = "invalid QSep"; break;

-			case 224: s = "invalid MatchExpression"; break;

-			case 225: s = "invalid QuantifierGuts"; break;

-			case 226: s = "invalid StmtInExpr"; break;

-			case 227: s = "invalid LetExpr"; break;

-			case 228: s = "invalid CasePattern"; break;

-			case 229: s = "invalid Forall"; break;

-			case 230: s = "invalid Exists"; break;

+			case 223: s = "invalid ParensExpression"; break;

+			case 224: s = "invalid QSep"; break;

+			case 225: s = "invalid MatchExpression"; break;

+			case 226: s = "invalid QuantifierGuts"; break;

+			case 227: s = "invalid StmtInExpr"; break;

+			case 228: s = "invalid LetExpr"; break;

+			case 229: s = "invalid CasePattern"; break;

+			case 230: s = "invalid Forall"; break;

+			case 231: s = "invalid Exists"; break;

 

 			default: s = "error " + n; break;

 		}

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 0a970498..5be5614d 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1191,9 +1191,16 @@ namespace Microsoft.Dafny {
         wr.Write(((IdentifierExpr)expr).Name);

 

       } else if (expr is DatatypeValue) {

-        DatatypeValue dtv = (DatatypeValue)expr;

-        wr.Write("#{0}.{1}", dtv.DatatypeName, dtv.MemberName);

-        if (dtv.Arguments.Count != 0) {

+        var dtv = (DatatypeValue)expr;

+        bool printParens;

+        if (dtv.MemberName == BuiltIns.TupleTypeCtorName) {

+          // we're looking at a tuple, whose printed constructor name is essentially the empty string

+          printParens = true;

+        } else {

+          wr.Write("{0}.{1}", dtv.DatatypeName, dtv.MemberName);

+          printParens = dtv.Arguments.Count != 0;

+        }

+        if (printParens) {

           wr.Write("(");

           PrintExpressionList(dtv.Arguments, false);

           wr.Write(")");

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 8de010fb..73925aef 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -197,6 +197,7 @@ namespace Microsoft.Dafny
       rewriters.Add(opaqueRewriter);

 

       systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule, false);

+      prog.CompileModules.Add(prog.BuiltIns.SystemModule);

       foreach (var decl in sortedDecls) {

         if (decl is LiteralModuleDecl) {

           // The declaration is a literal module, so it has members and such that we need

@@ -1019,6 +1020,9 @@ namespace Microsoft.Dafny
       if (d is ArbitraryTypeDecl) {

         var dd = (ArbitraryTypeDecl)d;

         return new ArbitraryTypeDecl(dd.tok, dd.Name, m, dd.EqualitySupport, null);

+      } else if (d is TupleTypeDecl) {

+        var dd = (TupleTypeDecl)d;

+        return new TupleTypeDecl(dd.Dims, dd.Module);

       } else if (d is IndDatatypeDecl) {

         var dd = (IndDatatypeDecl)d;

         var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index f3297ed7..35c17112 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -912,3 +912,34 @@ method DirtyM(S: set<int>) {
   forall s | s in S ensures s < 0;

   assert s < 0; // error: s is unresolved

 }

+

+// ------------------- tuples -------------------

+

+method TupleResolution(x: int, y: int, r: real)

+{

+  var unit: () := ();

+  var expr: int := (x);

+  var pair: (int,int) := (x, x);

+  var triple: (int,int,int) := (y, x, x);

+  var badTriple: (int,real,int) := (y, x, r);  // error: parameters 1 and 2 have the wrong types

+  var quadruple: (int,real,int,real) := (y, r, x);  // error: trying to use a triple as a quadruple

+

+  assert unit == ();

+  assert pair.0 == pair.1;

+  assert triple.2 == x;

+

+  assert triple.2;  // error: 2 has type int, not the expected bool

+  assert triple.3 == pair.x;  // error(s):  3 and x are not destructors

+

+  var k0 := (5, (true, 2, 3.14));

+  var k1 := (((false, 10, 2.7)), 100, 120);

+  if k0.1 == k1.0 {

+    assert false;

+  } else if k0.1.1 < k1.0.1 {

+    assert k1.2 == 120;

+  }

+

+  // int and (int) are the same type (i.e., there are no 1-tuples)

+  var pp: (int) := x;

+  var qq: int := pp;

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 2c0664d9..22f3274e 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -133,4 +133,10 @@ ResolutionErrors.dfy(545,7): Error: let-such-that expressions are allowed only i
 ResolutionErrors.dfy(546,18): Error: unresolved identifier: w

 ResolutionErrors.dfy(653,11): Error: lemmas are not allowed to have modifies clauses

 ResolutionErrors.dfy(913,9): Error: unresolved identifier: s

-135 resolution/type errors detected in ResolutionErrors.dfy

+ResolutionErrors.dfy(924,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))

+ResolutionErrors.dfy(925,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))

+ResolutionErrors.dfy(931,9): Error: condition is expected to be of type bool, but is int

+ResolutionErrors.dfy(932,16): Error: member 3 does not exist in datatype _tuple#3

+ResolutionErrors.dfy(932,26): Error: member x does not exist in datatype _tuple#2

+ResolutionErrors.dfy(932,18): Error: arguments must have the same type (got (int,int,int) and (int,int))

+141 resolution/type errors detected in ResolutionErrors.dfy

diff --git a/Test/dafny0/Tuples.dfy b/Test/dafny0/Tuples.dfy
new file mode 100644
index 00000000..81d054dd
--- /dev/null
+++ b/Test/dafny0/Tuples.dfy
@@ -0,0 +1,34 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+method M(x: int)

+{

+  var unit := ();

+  var expr := (x);

+  var pair := (x, x);

+  var triple := (x, x, x);

+}

+

+method N(x: int, y: int)

+{

+  var unit: () := ();

+  var expr: int := (x);

+  var pair: (int,int) := (x, x);

+  var triple: (int,int,int) := (y, x, x);

+

+  assert unit == ();

+  assert pair.0 == pair.1;

+  assert triple.2 == x;

+  assert triple.0 == triple.1;  // error: they may be different

+

+  var k := (24, 100 / y);  // error: possible division by zero

+  assert 2 <= k.0 < 29;

+

+  var k0 := (5, (true, 2, 3.14));

+  var k1 := (((false, 10, 2.7)), 100, 120);

+  if k0.1 == k1.0 {

+    assert false;

+  } else if k0.1.1 < k1.0.1 {

+    assert k1.2 == 120;

+  }

+}

diff --git a/Test/dafny0/Tuples.dfy.expect b/Test/dafny0/Tuples.dfy.expect
new file mode 100644
index 00000000..13c706d3
--- /dev/null
+++ b/Test/dafny0/Tuples.dfy.expect
@@ -0,0 +1,8 @@
+Tuples.dfy(22,19): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Tuples.dfy(24,21): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 3 verified, 2 errors