Address feedback

Source/Dafny/Dafny.atg

@@ -3848,39 +3848,24 @@ ParensExpression<out Expression e>
        e = new ParensExpression(x, args[0].Actual);
      } else {
        // Compute the actual position of ghost arguments
-       List<bool> argumentGhostness;
-       if (args.TrueForAll(arg => arg.FormalParameterName != null)) {
-         bool[] ghostness = new bool[args.Count];
-         bool[] initialized = new bool[args.Count];
-         for (int i = 0; i < initialized.Length; ++i) {
-           initialized[i] = false;
-         }
-         foreach (var arg in args) {
-           var success = int.TryParse(arg.FormalParameterName.val, out var index);
-           if (!success) {
-             SemErr(arg.FormalParameterName, "the name of tuple arguments must be an integer");
+       var ghostness = new bool[args.Count];
+       for (var i = 0; i < args.Count; i++) {
+         ghostness[i] = false;
+       }
+       for (var i = 0; i < args.Count; i++) {
+         var arg = args[i];
+         if (arg.IsGhost) {
+           if (arg.FormalParameterName == null) {
+             ghostness[i] = true;
            } else {
-             if (index < 0 || ghostness.Length <= index) {
-               SemErr(arg.FormalParameterName, "the name of tuple argument must describe a valid position in the tuple, starting from zero");
-             } else {
-               if (initialized[index]) {
-                 SemErr(arg.FormalParameterName, "different tuple arguments cannot have the same name");
-               } else {
-                 ghostness[index] = arg.IsGhost;
-                 initialized[index] = true;
-               }
+             var success = int.TryParse(arg.FormalParameterName.val, out var index);
+             if (success && 0 <= index && index < args.Count) {
+               ghostness[index] = true;
              }
            }
          }
-		 argumentGhostness = ghostness.ToList();
-       } else {
-         foreach (var arg in args) {
-           if (arg.FormalParameterName != null) {
-             SemErr(arg.FormalParameterName, "mixing named and positional tuple arguments is not allowed");
-           }
-         }
-         argumentGhostness = args.ConvertAll(arg => arg.IsGhost);
        }
+       var argumentGhostness = ghostness.ToList();
        // make sure the corresponding tuple type exists
        var tmp = theBuiltIns.TupleType(x, args.Count, true, argumentGhostness);
        e = new DatatypeValue(x, BuiltIns.TupleTypeName(argumentGhostness), BuiltIns.TupleTypeCtorNamePrefix + args.Count, args);

Source/Dafny/DafnyAst.cs

@@ -114,7 +114,7 @@ public class BuiltIns
     public readonly Dictionary<int, ArrowTypeDecl> ArrowTypeDecls = new Dictionary<int, ArrowTypeDecl>();
     public readonly Dictionary<int, SubsetTypeDecl> PartialArrowTypeDecls = new Dictionary<int, SubsetTypeDecl>();  // same keys as arrowTypeDecl
     public readonly Dictionary<int, SubsetTypeDecl> TotalArrowTypeDecls = new Dictionary<int, SubsetTypeDecl>();  // same keys as arrowTypeDecl
-    readonly Dictionary<object, TupleTypeDecl> tupleTypeDecls = new Dictionary<object, TupleTypeDecl>();
+    readonly Dictionary<List<bool>, TupleTypeDecl> tupleTypeDecls = new Dictionary<List<bool>, TupleTypeDecl>(new Dafny.ListComparer<bool>());
     public readonly ISet<int> Bitwidths = new HashSet<int>();
     public SpecialField ORDINAL_Offset;  // filled in by the resolver, used by the translator
 
@@ -325,29 +325,20 @@ Type GetTypeOfFunction(Function f, List<Type> typeArgumentsClass, List<Type> typ
       return new ArrowType(f.tok, atd, f.Formals.ConvertAll(arg => Resolver.SubstType(arg.Type, typeMap)), Resolver.SubstType(f.ResultType, typeMap));
     }
 
-    private object MakeTupleKey(List<bool> isGhost, int dims) {
-      if (dims == 0) {
-        return 0;
-      } else {
-        var g = isGhost[dims - 1];
-        return Tuple.Create(g, MakeTupleKey(isGhost, dims - 1));
-      }
-    }
-
     public TupleTypeDecl TupleType(IToken tok, int dims, bool allowCreationOfNewType, List<bool> argumentGhostness = null) {
       Contract.Requires(tok != null);
       Contract.Requires(0 <= dims);
+      Contract.Requires(argumentGhostness == null || argumentGhostness.Count == dims);
       Contract.Ensures(Contract.Result<TupleTypeDecl>() != null);
 
       TupleTypeDecl tt;
       argumentGhostness = argumentGhostness ?? new bool[dims].Select(_ => false).ToList();
-      object key = MakeTupleKey(argumentGhostness, dims);
-      if (!tupleTypeDecls.TryGetValue(key, out tt)) {
+      if (!tupleTypeDecls.TryGetValue(argumentGhostness, out tt)) {
         Contract.Assume(allowCreationOfNewType);  // the parser should ensure that all needed tuple types exist by the time of resolution
         // tuple#2 is already defined in DafnyRuntime.cs
         var attributes = dims == 2 && !argumentGhostness.Contains(true) ? DontCompile() : null;
         tt = new TupleTypeDecl(argumentGhostness, SystemModule, attributes);
-        tupleTypeDecls.Add(key, tt);
+        tupleTypeDecls.Add(argumentGhostness, tt);
         SystemModule.TopLevelDecls.Add(tt);
       }
       return tt;
@@ -3040,7 +3031,7 @@ public override string TypeName(ModuleDefinition context, bool parseAble) {
         // Unfortunately, ResolveClass may be null, so Name is all we have.  Reverse-engineer the string name.
         IEnumerable<bool> argumentGhostness = BuiltIns.ArgumentGhostnessFromString(Name, TypeArgs.Count);
         return "(" + Util.Comma(System.Linq.Enumerable.Zip(TypeArgs, argumentGhostness),
-          (ty_u) => Resolver.IsGhostPrefix(ty_u.Item2) + ty_u.Item1.TypeName(context, parseAble)) + ")";
+          (ty_u) => Resolver.GhostPrefix(ty_u.Item2) + ty_u.Item1.TypeName(context, parseAble)) + ")";
       } else if (ArrowType.IsPartialArrowTypeName(Name)) {
         return ArrowType.PrettyArrowTypeName(ArrowType.PARTIAL_ARROW, TypeArgs, null, context, parseAble);
       } else if (ArrowType.IsTotalArrowTypeName(Name)) {
@@ -4734,22 +4725,16 @@ public class TupleTypeDecl : IndDatatypeDecl
   {
     public readonly List<bool> ArgumentGhostness;
 
-    public int Dims
-    {
-      get { return ArgumentGhostness.Count; }
-    }
-
-    public int NonGhostDims
-    {
-      get { return ArgumentGhostness.Count(x => !x); }
-    }
+    public int Dims => ArgumentGhostness.Count;
+
+    public int NonGhostDims => ArgumentGhostness.Count(x => !x);
 
     /// <summary>
     /// Construct a resolved built-in tuple type with "dim" arguments.  "systemModule" is expected to be the _System module.
     /// </summary>
     public TupleTypeDecl(List<bool> argumentGhostness, ModuleDefinition systemModule, Attributes attributes)
       : this(systemModule, CreateCovariantTypeParameters(argumentGhostness.Count), argumentGhostness, attributes) {
-      Contract.Requires(0 <= Dims);
+      Contract.Requires(0 <= argumentGhostness.Count);
       Contract.Requires(systemModule != null);
 
       // Resolve the type parameters here

Source/Dafny/Resolver.cs

@@ -16926,7 +16926,7 @@ private bool ResolveDatatypeValue(ResolveOpts opts, DatatypeValue dtv, DatatypeD
       return ok && ctor.Formals.Count == dtv.Arguments.Count;
     }
 
-    public static string IsGhostPrefix(bool isGhost) {
+    public static string GhostPrefix(bool isGhost) {
       return isGhost ? "ghost " : "";
     }
 

Source/Dafny/Util.cs

@@ -445,4 +445,18 @@ public void PrintMap() {
       }
     }
   }
+
+  class ListComparer<T> : IEqualityComparer<List<T>> {
+    public bool Equals(List<T> x, List<T> y) {
+      return x.SequenceEqual(y);
+    }
+
+    public int GetHashCode(List<T> obj) {
+      var hash = new HashCode();
+      foreach (T t in obj) {
+        hash.Add(t);
+      }
+      return hash.ToHashCode();
+    }
+  }
 }

Test/ghost/AllowedGhost.dfy

@@ -3,8 +3,10 @@
 
 method Test()
 {
-    // Tuples with a single ghost component are allowed and they are compiled to empty tuples.
-    var x := (ghost 123);
-    var (y) := (ghost 123);
-    ghost var z: (ghost int) := (ghost 123);
+  // Tuples with a single ghost component are allowed and they are compiled to empty tuples.
+  var x := (ghost 123);
+  var (y) := (ghost 123);
+  ghost var z: (ghost int) := (ghost 123);
+  var t: (int, ghost int, int) := (20, 2 := 50, ghost 1 := 30);
+  var u: () := ();
 }

Test/ghost/AllowedGhost.dfy.expect

@@ -6,6 +6,8 @@ method Test()
   var (y) := (ghost 123);
 
   ghost var z: (ghost int) := (ghost 123);
+  var t: (int, ghost int, int) := (20, 2 := 50, ghost 1 := 30);
+  var u: () := ();
 }
 
 Dafny program verifier finished with 0 verified, 0 errors

Test/ghost/AllowedGhostBindings.dfy

@@ -3,14 +3,14 @@
 
 method Test1()
 {
-    var tuple0 := (ghost 0:=123, ghost 1:=234);
-    var tuple1 := (ghost 123, ghost 234);
-    assert tuple0 == tuple1;
+  var tuple0 := (ghost 0:=123, ghost 1:=234);
+  var tuple1 := (ghost 123, ghost 234);
+  assert tuple0 == tuple1;
 }
 
 method Test2()
 {
-    var tuple0 := (ghost 10:=10, 3:=3, 0:=0, 1:=1, 2:=2, 4:=4, 5:=5, 6:=6, 7:=7, 8:=8, 9:=9);
-    var tuple1 := (0, 1, 2, 3, 4, 5, 6, 7, 8, 9, ghost 10);
-    assert tuple0 == tuple1;
+  var tuple0 := (ghost 10:=10, 3:=3, 0:=0, 1:=1, 2:=2, 4:=4, 5:=5, 6:=6, 7:=7, 8:=8, 9:=9);
+  var tuple1 := (0, 1, 2, 3, 4, 5, 6, 7, 8, 9, ghost 10);
+  assert tuple0 == tuple1;
 }

Test/ghost/AmbiguousGhost.dfy

@@ -2,15 +2,11 @@
 // RUN: %diff "%s.expect" "%t"
 
 // Test that the `IsTypeSequence` method of the parser allows tuples with ghost components.
-module M1 {
-  class C1 {
-    function method F(x: int): () { () }
-    function method a<T,U>(x: int): int { x }
-    method M<b, c>(d: int) {
-      var u;
-      u := F( a < (b, ghost b), c > (d) );
-      u := F( a < (b, (ghost b, ghost b)), c > (d) );
-      u := F( a < (b, ((ghost b, b), ghost b)), c > (d) );
-    }
-  }
+function method F(x: int): () { () }
+function method a<T,U>(x: int): int { x }
+method M<b, c>(d: int) {
+  var u;
+  u := F( a < (b, ghost b), c > (d) );
+  u := F( a < (b, (ghost b, ghost b)), c > (d) );
+  u := F( a < (b, ((ghost b, b), ghost b)), c > (d) );
 }

Test/ghost/AmbiguousGhost.dfy.expect

@@ -1,26 +1,21 @@
 // AmbiguousGhost.dfy
 
+function method F(x: int): ()
+{
+  ()
+}
 
-module M1 {
-  class C1 {
-    function method F(x: int): ()
-    {
-      ()
-    }
-
-    function method a<T, U>(x: int): int
-    {
-      x
-    }
+function method a<T, U>(x: int): int
+{
+  x
+}
 
-    method M<b, c>(d: int)
-    {
-      var u;
-      u := F(a<(b, ghost b), c>(d));
-      u := F(a<(b, (ghost b, ghost b)), c>(d));
-      u := F(a<(b, ((ghost b, b), ghost b)), c>(d));
-    }
-  }
+method M<b, c>(d: int)
+{
+  var u;
+  u := F(a<(b, ghost b), c>(d));
+  u := F(a<(b, (ghost b, ghost b)), c>(d));
+  u := F(a<(b, ((ghost b, b), ghost b)), c>(d));
 }
 
 Dafny program verifier finished with 0 verified, 0 errors

Test/ghost/Comp.dfy

@@ -13,13 +13,13 @@ method Test2(t2: (int, ghost int, int)) { print "Test2: ", t2, "\n"; }
 method Test3(t3: ((ghost int), (ghost int, int), ghost int)) { print "Test3: ", t3, "\n"; }
 
 method Main() {
-    var p := PhantomData(123);
-    var t0 := (ghost 00);
-    var t1 := (ghost 11, 22);
-    var t2 := (33, ghost 44, 55);
-    var t3 := ((ghost 66), (ghost 77, 88), ghost 99);
-    Test0(t0);
-    Test1(t1);
-    Test2(t2);
-    Test3(t3);
+  var p := PhantomData(123);
+  var t0 := (ghost 00);
+  var t1 := (ghost 11, 22);
+  var t2 := (33, ghost 44, 55);
+  var t3 := ((ghost 66), (ghost 77, 88), ghost 99);
+  Test0(t0);
+  Test1(t1);
+  Test2(t2);
+  Test3(t3);
 }

Test/ghost/DisallowedGhost1.dfy

@@ -0,0 +1,18 @@
+// RUN: %dafny /compile:0 /dprint:- "%s" /env:0 > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Test1()
+{
+  var first := 0;
+  var t := (ghost first:=123, 1:=234); // error
+}
+
+method Test2()
+{
+  var t := (1:=123, 2:=234); // error
+}
+
+method Test3()
+{
+  var t := (1:=123, 1:=234); // error
+}

Test/ghost/DisallowedGhost1.dfy.expect

@@ -0,0 +1,24 @@
+// DisallowedGhost1.dfy
+
+method Test1()
+{
+  var first := 0;
+  var t := (ghost first := 123, 1 := 234);
+}
+
+method Test2()
+{
+  var t := (1 := 123, 2 := 234);
+}
+
+method Test3()
+{
+  var t := (1 := 123, 1 := 234);
+}
+DisallowedGhost1.dfy(7,18): Error: the binding named 'first' does not correspond to any formal parameter
+DisallowedGhost1.dfy(7,11): Error: no actual argument passed for datatype constructor argument '0'
+DisallowedGhost1.dfy(12,20): Error: the binding named '2' does not correspond to any formal parameter
+DisallowedGhost1.dfy(12,11): Error: no actual argument passed for datatype constructor argument '0'
+DisallowedGhost1.dfy(17,20): Error: duplicate binding for parameter name '1'
+DisallowedGhost1.dfy(17,11): Error: no actual argument passed for datatype constructor argument '0'
+6 resolution/type errors detected in DisallowedGhost1.dfy

Test/ghost/DisallowedGhost2.dfy

@@ -0,0 +1,7 @@
+// RUN: %dafny /compile:0 /dprint:- "%s" /env:0 > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Test()
+{
+  var (ghost x) := 123; // syntax error
+}

Test/ghost/DisallowedGhost2.dfy.expect

@@ -0,0 +1,2 @@
+DisallowedGhost2.dfy(6,7): Error: closeparen expected
+1 parse errors detected in DisallowedGhost2.dfy