When ambiguous references all resolve to the same declaration, don't complain

9 files changed, 330 insertions, 38 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index ebb291fb..f95c05ed 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -115,7 +115,6 @@ namespace Microsoft.Dafny
         } else if (d is AliasModuleDecl) {

           var a = (AliasModuleDecl)d;

           var alias = new AliasModuleDecl(a.Path, a.tok, m, a.Opened);

-          alias.ModuleReference = a.ModuleReference;

           alias.Signature = a.Signature;

           return alias;

         } else if (d is ModuleFacadeDecl) {

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 0742ee43..f1fbd7ff 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1323,7 +1323,17 @@ namespace Microsoft.Dafny {
 

   // ------------------------------------------------------------------------------------------------------

 

-  public abstract class Declaration : IUniqueNameGenerator {

+  /// <summary>

+  /// This interface is used by the Dafny IDE.

+  /// </summary>

+  public interface INamedRegion

+  {

+    IToken BodyStartTok { get; }

+    IToken BodyEndTok { get; }

+    string Name { get; }

+  }

+

+  public abstract class Declaration : IUniqueNameGenerator, INamedRegion {

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(tok != null);

@@ -1334,6 +1344,9 @@ namespace Microsoft.Dafny {
     public IToken BodyStartTok = Token.NoToken;

     public IToken BodyEndTok = Token.NoToken;

     public readonly string Name;

+    IToken INamedRegion.BodyStartTok { get { return BodyStartTok; } }

+    IToken INamedRegion.BodyEndTok { get { return BodyEndTok; } }

+    string INamedRegion.Name { get { return Name; } }

     string compileName;

     public virtual string CompileName {

       get {

@@ -1452,6 +1465,7 @@ namespace Microsoft.Dafny {
       Signature = null;

       Opened = opened;

     }

+    public abstract object Dereference();

   }

   // Represents module X { ... }

   public class LiteralModuleDecl : ModuleDecl

@@ -1461,20 +1475,19 @@ namespace Microsoft.Dafny {
       : base(module.tok, module.Name, parent, false) {

       ModuleDef = module;

     }

+    public override object Dereference() { return ModuleDef; }

   }

-  // Represents "module name = path;", where name is a identifier and path is a possibly qualified name.

+  // Represents "module name = path;", where name is an identifier and path is a possibly qualified name.

   public class AliasModuleDecl : ModuleDecl

   {

-    public ModuleDecl ModuleReference; // should refer to another declaration somewhere. NOTE: cyclicity is possible, and should

-                                       // be detected and warned.

     public readonly List<IToken> Path; // generated by the parser, this is looked up

     public ModuleDecl Root;            // the moduleDecl that Path[0] refers to.

     public AliasModuleDecl(List<IToken> path, IToken name, ModuleDefinition parent, bool opened)

       : base(name, name.val, parent, opened) {

        Contract.Requires(path != null && path.Count > 0);

        Path = path;

-       ModuleReference = null;

     }

+    public override object Dereference() { return Signature.ModuleDef; }

   }

   // Represents "module name as path [ = compilePath];", where name is a identifier and path is a possibly qualified name.

   public class ModuleFacadeDecl : ModuleDecl

@@ -1491,6 +1504,7 @@ namespace Microsoft.Dafny {
       Root = null;

       CompilePath = compilePath;

     }

+    public override object Dereference() { return this; }

   }

 

   public class ModuleSignature {

@@ -1507,18 +1521,27 @@ namespace Microsoft.Dafny {
 

     public bool FindSubmodule(string name, out ModuleSignature pp) {

       TopLevelDecl top;

-      pp = null;

-      if (TopLevels.TryGetValue(name, out top)) {

-        if (top is ModuleDecl) {

-          pp = ((ModuleDecl)top).Signature;

-          return true;

-        } else return false;

-      } else return false;

+      if (TopLevels.TryGetValue(name, out top) && top is ModuleDecl) {

+        pp = ((ModuleDecl)top).Signature;

+        return true;

+      } else {

+        pp = null;

+        return false;

+      }

     }

-

-

   }

-  public class ModuleDefinition : TopLevelDecl {

+

+  public class ModuleDefinition : INamedRegion

+  {

+    public readonly IToken tok;

+    public IToken BodyStartTok = Token.NoToken;

+    public IToken BodyEndTok = Token.NoToken;

+    public readonly string Name;

+    IToken INamedRegion.BodyStartTok { get { return BodyStartTok; } }

+    IToken INamedRegion.BodyEndTok { get { return BodyEndTok; } }

+    string INamedRegion.Name { get { return Name; } }

+    public readonly ModuleDefinition Module;

+    public readonly Attributes Attributes;

     public readonly List<IToken> RefinementBaseName;  // null if no refinement base

     public ModuleDecl RefinementBaseRoot; // filled in early during resolution, corresponds to RefinementBaseName[0]

     public ModuleDefinition RefinementBase;  // filled in during resolution (null if no refinement base)

@@ -1537,9 +1560,13 @@ namespace Microsoft.Dafny {
     }

 

     public ModuleDefinition(IToken tok, string name, bool isAbstract, bool isFacade, List<IToken> refinementBase, ModuleDefinition parent, Attributes attributes, bool isBuiltinName)

-      : base(tok, name, parent, new List<TypeParameter>(), attributes) {

+    {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

+      this.tok = tok;

+      this.Name = name;

+      this.Attributes = attributes;

+      this.Module = parent;

       RefinementBaseName = refinementBase;

       IsAbstract = isAbstract;

       IsFacade = isFacade;

@@ -1554,7 +1581,7 @@ namespace Microsoft.Dafny {
       }

     }

     string compileName;

-    new public string CompileName {

+    public string CompileName {

       get {

         if (compileName == null) {

           if (IsBuiltinName)

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 23f6bc6c..887a387f 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -92,15 +92,36 @@ namespace Microsoft.Dafny
       }

     }

 

-    class AmbiguousTopLevelDecl : TopLevelDecl  // only used with "classes"

+    interface IAmbiguousThing<Thing>

+    {

+      /// <summary>

+      /// Returns a non-zero number of non-null Thing's

+      /// </summary>

+      IEnumerable<Thing> AllDecls();

+    }

+    class AmbiguousTopLevelDecl : TopLevelDecl, IAmbiguousThing<TopLevelDecl>  // only used with "classes"

     {

       readonly TopLevelDecl A;

       readonly TopLevelDecl B;

       public AmbiguousTopLevelDecl(ModuleDefinition m, TopLevelDecl a, TopLevelDecl b)

         : base(a.tok, a.Name + "/" + b.Name, m, new List<TypeParameter>(), null) {

+        Contract.Requires(a != null);

+        Contract.Requires(b != null);

         A = a;

         B = b;

       }

+      public IEnumerable<TopLevelDecl> AllDecls() {

+        foreach (var a in new TopLevelDecl[] { A, B }) {

+          var amb = a as AmbiguousTopLevelDecl;

+          if (amb != null) {

+            foreach (var decl in amb.AllDecls()) {

+              yield return decl;

+            }

+          } else {

+            yield return a;

+          }

+        }

+      }

       public string ModuleNames() {

         string nm;

         if (A is AmbiguousTopLevelDecl) {

@@ -117,15 +138,35 @@ namespace Microsoft.Dafny
       }

     }

 

-    class AmbiguousMemberDecl : MemberDecl  // only used with "classes"

+    class AmbiguousMemberDecl : MemberDecl, IAmbiguousThing<MemberDecl>  // only used with "classes"

     {

       readonly MemberDecl A;

       readonly MemberDecl B;

       public AmbiguousMemberDecl(ModuleDefinition m, MemberDecl a, MemberDecl b)

         : base(a.tok, a.Name + "/" + b.Name, true, a.IsGhost, null) {

+        Contract.Requires(a != null);

+        Contract.Requires(b != null);

         A = a;

         B = b;

       }

+      public IEnumerable<MemberDecl> AllDecls() {

+        var amb = A as AmbiguousMemberDecl;

+        if (amb == null) {

+          yield return A;

+        } else {

+          foreach (var decl in amb.AllDecls()) {

+            yield return decl;

+          }

+        }

+        amb = B as AmbiguousMemberDecl;

+        if (amb == null) {

+          yield return B;

+        } else {

+          foreach (var decl in amb.AllDecls()) {

+            yield return decl;

+          }

+        }

+      }

       public string ModuleNames() {

         string nm;

         if (A is AmbiguousMemberDecl) {

@@ -4028,7 +4069,7 @@ namespace Microsoft.Dafny
 

           if (d == null) {

             // error has been reported above

-          } else if (d is AmbiguousTopLevelDecl) {

+          } else if (ReallyAmbiguousTopLevelDecl(ref d)) {

             Error(t.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", t.Name, ((AmbiguousTopLevelDecl)d).ModuleNames());

           } else {

             string what;

@@ -4076,6 +4117,39 @@ namespace Microsoft.Dafny
       return null;

     }

 

+    bool ReallyAmbiguousTopLevelDecl(ref TopLevelDecl decl) {

+      return ReallyAmbiguousThing(ref decl, (d0, d1) => {

+        // We'd like to resolve any AliasModuleDecl to whatever module they refer to.

+        // It seems that the only way to do that is to look at alias.Signature.ModuleDef,

+        // but that is a ModuleDefinition, which is not a TopLevelDecl.  Therefore, we

+        // convert to a ModuleDefinition anything that might refer to something that an

+        // AliasModuleDecl can refer to; this is AliasModuleDecl and LiteralModuleDecl.

+        object a = d0 is ModuleDecl ? ((ModuleDecl)d0).Dereference() : d0;

+        object b = d1 is ModuleDecl ? ((ModuleDecl)d1).Dereference() : d1;

+        return a == b;

+      });

+    }

+

+    bool ReallyAmbiguousThing<Thing>(ref Thing decl, Func<Thing, Thing, bool> eq = null) where Thing : class {

+      Contract.Requires(decl != null);

+      Contract.Ensures(decl != null);

+      Contract.Ensures(!Contract.Result<bool>() || (decl == Contract.OldValue<Thing>(decl) && decl is IAmbiguousThing<Thing>));

+      var amb = decl as IAmbiguousThing<Thing>;

+      if (amb != null) {

+        var allDecls = new List<Thing>(amb.AllDecls());

+        Contract.Assert(1 <= allDecls.Count);  // that's what the specification of AllDecls says

+        var repr = allDecls[0];  // pick one of them

+        // check if all are the same

+        if (amb.AllDecls().All(d => eq == null ? d == repr : eq(d, repr))) {

+          // all ambiguity gets resolved to the same declaration, so there really isn't any ambiguity after all

+          decl = repr;

+          return false;

+        }

+        return true;  // decl is an AmbiguousThing and the declarations it can stand for are not all the same--so this really is an ambiguity

+      }

+      return false;

+    }

+

     /// <summary>

     /// Adds to "typeArgs" a list of "n" type arguments, possibly extending "defaultTypeArguments".

     /// </summary>

@@ -6390,7 +6464,7 @@ namespace Microsoft.Dafny
         TopLevelDecl d;

         if (!moduleInfo.TopLevels.TryGetValue(dtv.DatatypeName, out d)) {

           Error(expr.tok, "Undeclared datatype: {0}", dtv.DatatypeName);

-        } else if (d is AmbiguousTopLevelDecl) {

+        } else if (ReallyAmbiguousTopLevelDecl(ref d)) {

           Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1}", dtv.DatatypeName, ((AmbiguousTopLevelDecl)d).ModuleNames());

         } else if (!(d is DatatypeDecl)) {

           Error(expr.tok, "Expected datatype: {0}", dtv.DatatypeName);

@@ -7403,7 +7477,7 @@ namespace Microsoft.Dafny
         }

       } else if (moduleInfo.TopLevels.TryGetValue(expr.Name, out decl)) {

         // ----- 3. Member of the enclosing module

-        if (decl is AmbiguousTopLevelDecl) {

+        if (ReallyAmbiguousTopLevelDecl(ref decl)) {

           Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1}", expr.Name, ((AmbiguousTopLevelDecl)decl).ModuleNames());

         } else {

           // We have found a module name or a type name, neither of which is an expression. However, the NameSegment we're

@@ -7416,7 +7490,7 @@ namespace Microsoft.Dafny
       } else if (moduleInfo.StaticMembers.TryGetValue(expr.Name, out member)) {

         // ----- 4. static member of the enclosing module

         Contract.Assert(member.IsStatic); // moduleInfo.StaticMembers is supposed to contain only static members of the module's implicit class _default

-        if (member is AmbiguousMemberDecl) {

+        if (ReallyAmbiguousThing(ref member)) {

           Error(expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1}", expr.Name, ((AmbiguousMemberDecl)member).ModuleNames());

         } else {

           var receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass);

@@ -7535,7 +7609,7 @@ namespace Microsoft.Dafny
           }

         } else if (sig.TopLevels.TryGetValue(expr.SuffixName, out decl)) {

           // ----- 1. Member of the specified module

-          if (decl is AmbiguousTopLevelDecl) {

+          if (ReallyAmbiguousTopLevelDecl(ref decl)) {

             Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1}", expr.SuffixName, ((AmbiguousTopLevelDecl)decl).ModuleNames());

           } else {

             // We have found a module name or a type name, neither of which is an expression. However, the ExprDotName we're

@@ -7547,7 +7621,7 @@ namespace Microsoft.Dafny
         } else if (sig.StaticMembers.TryGetValue(expr.SuffixName, out member)) {

           // ----- 2. static member of the specified module

           Contract.Assert(member.IsStatic); // moduleInfo.StaticMembers is supposed to contain only static members of the module's implicit class _default

-          if (member is AmbiguousMemberDecl) {

+          if (ReallyAmbiguousThing(ref member)) {

             Error(expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1}", expr.SuffixName, ((AmbiguousMemberDecl)member).ModuleNames());

           } else {

             var receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 3decb1f8..9379fac7 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -9062,16 +9062,8 @@ namespace Microsoft.Dafny {
     }

 

     static public List<TypeParameter> GetTypeParams(TopLevelDecl d) {

-      if (d is ClassDecl) {

-        return Concat(GetTypeParams(d.Module), d.TypeArgs);

-      } else if (d is DatatypeDecl) {

-        return Concat(GetTypeParams(d.Module), d.TypeArgs);

-      } else if (d is ModuleDefinition) {

-        return new List<TypeParameter>();

-      } else {

-        Contract.Assert(false);

-        return null;

-      }

+      Contract.Requires(d is ClassDecl || d is DatatypeDecl);

+      return d.TypeArgs;

     }

 

     static List<TypeParameter> GetTypeParams(Function f) {

diff --git a/Source/DafnyExtension/OutliningTagger.cs b/Source/DafnyExtension/OutliningTagger.cs
index 55f5e677..c4b88f98 100644
--- a/Source/DafnyExtension/OutliningTagger.cs
+++ b/Source/DafnyExtension/OutliningTagger.cs
@@ -200,7 +200,7 @@ namespace DafnyLanguage
       public readonly int Start;

       public readonly int Length;

       public readonly string HoverText;

-      public OutliningRegion(Dafny.Declaration decl, string kind) {

+      public OutliningRegion(Dafny.INamedRegion decl, string kind) {

         int startPosition = decl.BodyStartTok.pos + 1;  // skip the open-curly brace itself

         int length = decl.BodyEndTok.pos - startPosition;

         Start = startPosition;

diff --git a/Test/dafny0/DiamondImports.dfy b/Test/dafny0/DiamondImports.dfy
new file mode 100644
index 00000000..1292211f
--- /dev/null
+++ b/Test/dafny0/DiamondImports.dfy
@@ -0,0 +1,143 @@
+// RUN: %dafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

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

+

+module ImportByName {

+  module A {

+    type T

+    function method P(): T

+    method M(t: T)

+  }

+

+  module B {

+    import A

+  }

+

+  module C {

+    import A

+    type K = A.T

+    import W_A = W_B

+    import W_B = A

+  }

+

+  module D {

+    import B

+    import C

+

+    method Client() returns (t: B.A.T, u: C.A.T) {

+      t := u;

+      u := t;

+      var x, y := B.A.P(), C.A.P();

+      assert x == y;

+      C.A.M(t);

+      B.A.M(u);

+      var anything;

+      assert t == anything;  // error: (testing that it's not possible to prove false here)

+    }

+  }

+

+  module E {

+    import A

+    import B

+    import C

+    method Client() returns (r: A.T, k: C.K) {

+      var x, y, z := B.A.P(), C.A.P(), A.P();

+      assert x == z == y;

+      r, r, r := x, y, z;

+      k, k, k, k := x, y, z, r;

+      assert r == C.W_A.P();

+      assert r == C.W_B.P();

+      var anything;

+      assert r == anything;  // error: (testing that it's not possible to prove false here)

+    }

+  }

+}

+

+// ------------------------------------------------------------

+

+module ImportOpened {

+  module A {

+    type T

+    function method P(): T

+    method M(t: T)

+  }

+

+  module B {

+    import opened A

+  }

+

+  module C {

+    import opened A

+    type K = T

+    type L = A.T  // should work when name is qualified, too

+    import W_A = W_B

+    import W_B = A

+  }

+

+  module C' {

+    import A  // import by name

+    type K = A.T

+  }

+

+  module D {

+    import opened B

+    import opened C

+    import opened C'

+

+    method Client() returns (t: B.A.T, u: C.A.T, v: C'.A.T, w: B.T) {

+      t,u, v, w := u, v, w, t;

+      var x, y, z := B.A.P(), C.A.P(), C'.A.P();

+      assert x == y == z;

+      var o;

+      x, y, z, o := B.P(), C.P(), C'.A.P(), A.P();

+      assert x == y == z == o;

+

+      B.A.M(u);

+      C.A.M(t);

+      C'.A.M(t);

+      B.M(t);

+      C.M(t);

+      M(t);

+      var anything;

+      assert t == anything;  // error: (testing that it's not possible to prove false here)

+    }

+  }

+

+  module E {

+    import opened A

+    import opened B

+    import opened C

+    method Client() returns (r: A.T, k: C.K, l: C.L, m: K, n: L) {

+      var x, y, z := B.A.P(), C.A.P(), A.P();

+      assert x == z == y;

+      r, r, r := x, y, z;

+      k, k, k, k := x, y, z, r;

+      l, l, l, l, l := x, y, z, r, k;

+      m, n := k, l;

+      assert m == n == k;

+      assert r == C.W_A.P() == C.W_B.P();

+      assert r == W_A.P() == W_B.P();

+      var anything;

+      assert r == anything;  // error: (testing that it's not possible to prove false here)

+    }

+  }

+}

+

+module AmbiguousModuleReference {

+  module A {

+    module Inner {

+      predicate Q()

+    }

+  }

+  module B {

+    module Inner {

+      predicate Q()

+    }

+  }

+  module Client {

+    import A

+    import B

+    method M() {

+      assert A.Inner.Q() <==> B.Inner.Q();  // error: no reason to think these would be equal

+    }

+  }

+}

diff --git a/Test/dafny0/DiamondImports.dfy.expect b/Test/dafny0/DiamondImports.dfy.expect
new file mode 100644
index 00000000..e9e8c2b9
--- /dev/null
+++ b/Test/dafny0/DiamondImports.dfy.expect
@@ -0,0 +1,32 @@
+DiamondImports.dfy(34,16): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+DiamondImports.dfy(50,16): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+    (0,0): anon2

+DiamondImports.dfy(101,16): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon7_Then

+    (0,0): anon2

+    (0,0): anon8_Then

+    (0,0): anon9_Then

+    (0,0): anon6

+DiamondImports.dfy(120,16): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon9_Then

+    (0,0): anon2

+    (0,0): anon10_Then

+    (0,0): anon4

+    (0,0): anon11_Then

+    (0,0): anon6

+    (0,0): anon12_Then

+    (0,0): anon8

+DiamondImports.dfy(140,26): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 11 verified, 5 errors

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 4b290bb7..12593b8c 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1306,3 +1306,27 @@ module FrameTargetFields {
     }

   }

 }

+

+// ------------------------------------------------------

+

+module AmbiguousModuleReference {

+  module A {

+    module Inner {

+      predicate Q()

+    }

+  }

+  module B {

+    module Inner {

+      predicate Q()

+    }

+  }

+  module OpenClient {

+    import opened A

+    import opened B

+    lemma M() {

+      var a := A.Inner.Q();  // fine

+      var b := B.Inner.Q();  // fine

+      var p := Inner.Q();  // error: Inner is ambiguous (A.Inner or B.Inner)

+    }

+  }

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index f1c5532e..89531a5c 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -86,6 +86,7 @@ ResolutionErrors.dfy(1253,21): Error: Undeclared top-level type or type paramete
 ResolutionErrors.dfy(1254,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

 ResolutionErrors.dfy(1291,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)

 ResolutionErrors.dfy(1301,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

+ResolutionErrors.dfy(1329,15): Error: The name Inner ambiguously refers to a type in one of the modules A, B

 ResolutionErrors.dfy(432,2): Error: More than one anonymous constructor

 ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context

 ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')

@@ -181,4 +182,4 @@ ResolutionErrors.dfy(1106,8): Error: new cannot be applied to a trait
 ResolutionErrors.dfy(1127,13): Error: first argument to / must be of numeric type (instead got set<bool>)

 ResolutionErrors.dfy(1134,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating

 ResolutionErrors.dfy(1149,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

-183 resolution/type errors detected in ResolutionErrors.dfy

+184 resolution/type errors detected in ResolutionErrors.dfy