diff options
| -rw-r--r-- | Source/Dafny/Cloner.cs | 5 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 15 | ||||
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 174 | ||||
| -rw-r--r-- | Source/Dafny/Reporting.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 11 | ||||
| -rw-r--r-- | Test/dafny0/Modules0.dfy | 12 | ||||
| -rw-r--r-- | Test/dafny0/Modules0.dfy.expect | 3 | ||||
| -rw-r--r-- | Test/dafny4/Bug125.dfy | 82 | ||||
| -rw-r--r-- | Test/dafny4/Bug125.dfy.expect | 2 |
9 files changed, 225 insertions, 81 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 8971d2c1..6d5e2961 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -23,7 +23,10 @@ namespace Microsoft.Dafny nw.TopLevelDecls.Add(CloneDeclaration(d, nw));
}
if (null != m.RefinementBase) {
- nw.RefinementBase = m.RefinementBase;
+ nw.RefinementBase = m.RefinementBase;
+ }
+ if (null != m.RefinementBaseSig) {
+ nw.RefinementBaseSig = m.RefinementBaseSig;
}
nw.ClonedFrom = m;
nw.Height = m.Height;
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 33186a76..0e4c4751 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1823,6 +1823,21 @@ namespace Microsoft.Dafny { public int ExclusiveRefinementCount { get; set; }
+ private ModuleSignature refinementBaseSig; // module signature of the refinementBase.
+ public ModuleSignature RefinementBaseSig {
+ get {
+ return refinementBaseSig;
+ }
+
+ set {
+ // the refinementBase member may only be changed once.
+ if (null != refinementBaseSig) {
+ throw new InvalidOperationException(string.Format("This module ({0}) already has a refinement base ({1}).", Name, refinementBase.Name));
+ }
+ refinementBaseSig = value;
+ }
+ }
+
private ModuleDefinition refinementBase; // filled in during resolution via RefinementBase property (null if no refinement base yet or at all).
public ModuleDefinition RefinementBase {
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 6281417d..a243ad53 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -141,99 +141,117 @@ namespace Microsoft.Dafny }
// Merge the declarations of prev into the declarations of m
+ List<string> processedDecl = new List<string>();
foreach (var d in prev.TopLevelDecls) {
int index;
+ processedDecl.Add(d.Name);
if (!declaredNames.TryGetValue(d.Name, out index)) {
m.TopLevelDecls.Add(refinementCloner.CloneDeclaration(d, m));
} else {
var nw = m.TopLevelDecls[index];
- if (d is ModuleDecl) {
- if (!(nw is ModuleDecl)) {
- reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) must refine another module", nw.Name);
- } else if (!(d is ModuleFacadeDecl)) {
- reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) can only refine a module facade", nw.Name);
- } else {
- ModuleSignature original = ((ModuleFacadeDecl)d).OriginalSignature;
- ModuleSignature derived = null;
- if (nw is AliasModuleDecl) {
- derived = ((AliasModuleDecl)nw).Signature;
- } else if (nw is ModuleFacadeDecl) {
- derived = ((ModuleFacadeDecl)nw).Signature;
- } else {
- reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) can only be refined by an alias module or a module facade", d.Name);
+ MergeTopLevelDecls(m, nw, d, index);
+ }
+ }
+
+ // Merge the imports of prev
+ var prevTopLevelDecls = RefinedSig.TopLevels.Values;
+ foreach (var d in prevTopLevelDecls) {
+ int index;
+ if (!processedDecl.Contains(d.Name) && (declaredNames.TryGetValue(d.Name, out index))) {
+ // if it is redefined, we need to merge them.
+ var nw = m.TopLevelDecls[index];
+ MergeTopLevelDecls(m, nw, d, index);
+ }
+ }
+ m.RefinementBaseSig = RefinedSig;
+
+ Contract.Assert(moduleUnderConstruction == m); // this should be as it was set earlier in this method
+ }
+
+ private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDecl d, int index) {
+ if (d is ModuleDecl) {
+ if (!(nw is ModuleDecl)) {
+ reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) must refine another module", nw.Name);
+ } else if (!(d is ModuleFacadeDecl)) {
+ reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) can only refine a module facade", nw.Name);
+ } else {
+ ModuleSignature original = ((ModuleFacadeDecl)d).OriginalSignature;
+ ModuleSignature derived = null;
+ if (nw is AliasModuleDecl) {
+ derived = ((AliasModuleDecl)nw).Signature;
+ } else if (nw is ModuleFacadeDecl) {
+ derived = ((ModuleFacadeDecl)nw).Signature;
+ } else {
+ reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) can only be refined by an alias module or a module facade", d.Name);
+ }
+ if (derived != null) {
+ // check that the new module refines the previous declaration
+ if (!CheckIsRefinement(derived, original))
+ reporter.Error(MessageSource.RefinementTransformer, nw.tok, "a module ({0}) can only be replaced by a refinement of the original module", d.Name);
+ }
+ }
+ } else if (d is OpaqueTypeDecl) {
+ if (nw is ModuleDecl) {
+ reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) must refine another module", nw.Name);
+ } else {
+ bool dDemandsEqualitySupport = ((OpaqueTypeDecl)d).MustSupportEquality;
+ if (nw is OpaqueTypeDecl) {
+ if (dDemandsEqualitySupport != ((OpaqueTypeDecl)nw).MustSupportEquality) {
+ reporter.Error(MessageSource.RefinementTransformer, nw, "type declaration '{0}' is not allowed to change the requirement of supporting equality", nw.Name);
+ }
+ if (nw.TypeArgs.Count != d.TypeArgs.Count) {
+ reporter.Error(MessageSource.RefinementTransformer, nw, "type '{0}' is not allowed to change its number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);
+ }
+ } else if (dDemandsEqualitySupport) {
+ if (nw is ClassDecl) {
+ // fine, as long as "nw" takes the right number of type parameters
+ if (nw.TypeArgs.Count != d.TypeArgs.Count) {
+ reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}' is not allowed to be replaced by a class that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);
}
- if (derived != null) {
- // check that the new module refines the previous declaration
- if (!CheckIsRefinement(derived, original))
- reporter.Error(MessageSource.RefinementTransformer, nw.tok, "a module ({0}) can only be replaced by a refinement of the original module", d.Name);
+ } else if (nw is NewtypeDecl) {
+ // fine, as long as "nw" does not take any type parameters
+ if (nw.TypeArgs.Count != 0) {
+ reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}', which has {1} type argument{2}, is not allowed to be replaced by a newtype, which takes none", nw.Name, d.TypeArgs.Count, d.TypeArgs.Count == 1 ? "" : "s");
}
- }
- } else if (d is OpaqueTypeDecl) {
- if (nw is ModuleDecl) {
- reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) must refine another module", nw.Name);
+ } else if (nw is CoDatatypeDecl) {
+ reporter.Error(MessageSource.RefinementTransformer, nw, "a type declaration that requires equality support cannot be replaced by a codatatype");
} else {
- bool dDemandsEqualitySupport = ((OpaqueTypeDecl)d).MustSupportEquality;
- if (nw is OpaqueTypeDecl) {
- if (dDemandsEqualitySupport != ((OpaqueTypeDecl)nw).MustSupportEquality) {
- reporter.Error(MessageSource.RefinementTransformer, nw, "type declaration '{0}' is not allowed to change the requirement of supporting equality", nw.Name);
- }
- if (nw.TypeArgs.Count != d.TypeArgs.Count) {
- reporter.Error(MessageSource.RefinementTransformer, nw, "type '{0}' is not allowed to change its number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);
- }
- } else if (dDemandsEqualitySupport) {
- if (nw is ClassDecl) {
- // fine, as long as "nw" takes the right number of type parameters
- if (nw.TypeArgs.Count != d.TypeArgs.Count) {
- reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}' is not allowed to be replaced by a class that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);
- }
- } else if (nw is NewtypeDecl) {
- // fine, as long as "nw" does not take any type parameters
- if (nw.TypeArgs.Count != 0) {
- reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}', which has {1} type argument{2}, is not allowed to be replaced by a newtype, which takes none", nw.Name, d.TypeArgs.Count, d.TypeArgs.Count == 1 ? "" : "s");
- }
- } else if (nw is CoDatatypeDecl) {
- reporter.Error(MessageSource.RefinementTransformer, nw, "a type declaration that requires equality support cannot be replaced by a codatatype");
- } else {
- Contract.Assert(nw is IndDatatypeDecl || nw is TypeSynonymDecl);
- if (nw.TypeArgs.Count != d.TypeArgs.Count) {
- reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}' is not allowed to be replaced by a type that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);
- } else {
- // Here, we need to figure out if the new type supports equality. But we won't know about that until resolution has
- // taken place, so we defer it until the PostResolve phase.
- var udt = UserDefinedType.FromTopLevelDecl(nw.tok, nw);
- postTasks.Enqueue(() => {
- if (!udt.SupportsEquality) {
- reporter.Error(MessageSource.RefinementTransformer, udt.tok, "type '{0}' is used to refine an opaque type with equality support, but '{0}' does not support equality", udt.Name);
- }
- });
- }
- }
- } else if (d.TypeArgs.Count != nw.TypeArgs.Count) {
+ Contract.Assert(nw is IndDatatypeDecl || nw is TypeSynonymDecl);
+ if (nw.TypeArgs.Count != d.TypeArgs.Count) {
reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}' is not allowed to be replaced by a type that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);
+ } else {
+ // Here, we need to figure out if the new type supports equality. But we won't know about that until resolution has
+ // taken place, so we defer it until the PostResolve phase.
+ var udt = UserDefinedType.FromTopLevelDecl(nw.tok, nw);
+ postTasks.Enqueue(() => {
+ if (!udt.SupportsEquality) {
+ reporter.Error(MessageSource.RefinementTransformer, udt.tok, "type '{0}' is used to refine an opaque type with equality support, but '{0}' does not support equality", udt.Name);
+ }
+ });
}
}
- } else if (nw is OpaqueTypeDecl) {
- reporter.Error(MessageSource.RefinementTransformer, nw, "an opaque type declaration ({0}) in a refining module cannot replace a more specific type declaration in the refinement base", nw.Name);
- } else if (nw is DatatypeDecl) {
- reporter.Error(MessageSource.RefinementTransformer, nw, "a datatype declaration ({0}) in a refinement module can only replace an opaque type declaration", nw.Name);
- } else if (nw is IteratorDecl) {
- if (d is IteratorDecl) {
- m.TopLevelDecls[index] = MergeIterator((IteratorDecl)nw, (IteratorDecl)d);
- } else {
- reporter.Error(MessageSource.RefinementTransformer, nw, "an iterator declaration ({0}) is a refining module cannot replace a different kind of declaration in the refinement base", nw.Name);
- }
- } else {
- Contract.Assert(nw is ClassDecl);
- if (d is DatatypeDecl) {
- reporter.Error(MessageSource.RefinementTransformer, nw, "a class declaration ({0}) in a refining module cannot replace a different kind of declaration in the refinement base", nw.Name);
- } else {
- m.TopLevelDecls[index] = MergeClass((ClassDecl)nw, (ClassDecl)d);
- }
+ } else if (d.TypeArgs.Count != nw.TypeArgs.Count) {
+ reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}' is not allowed to be replaced by a type that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);
}
}
+ } else if (nw is OpaqueTypeDecl) {
+ reporter.Error(MessageSource.RefinementTransformer, nw, "an opaque type declaration ({0}) in a refining module cannot replace a more specific type declaration in the refinement base", nw.Name);
+ } else if (nw is DatatypeDecl) {
+ reporter.Error(MessageSource.RefinementTransformer, nw, "a datatype declaration ({0}) in a refinement module can only replace an opaque type declaration", nw.Name);
+ } else if (nw is IteratorDecl) {
+ if (d is IteratorDecl) {
+ m.TopLevelDecls[index] = MergeIterator((IteratorDecl)nw, (IteratorDecl)d);
+ } else {
+ reporter.Error(MessageSource.RefinementTransformer, nw, "an iterator declaration ({0}) is a refining module cannot replace a different kind of declaration in the refinement base", nw.Name);
+ }
+ } else {
+ Contract.Assert(nw is ClassDecl);
+ if (d is DatatypeDecl) {
+ reporter.Error(MessageSource.RefinementTransformer, nw, "a class declaration ({0}) in a refining module cannot replace a different kind of declaration in the refinement base", nw.Name);
+ } else {
+ m.TopLevelDecls[index] = MergeClass((ClassDecl)nw, (ClassDecl)d);
+ }
}
-
- Contract.Assert(moduleUnderConstruction == m); // this should be as it was set earlier in this method
}
public bool CheckIsRefinement(ModuleSignature derived, ModuleSignature original) {
diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs index 760392ca..b36efc55 100644 --- a/Source/Dafny/Reporting.cs +++ b/Source/Dafny/Reporting.cs @@ -37,7 +37,7 @@ namespace Microsoft.Dafny { // This is the only thing that needs to be overriden
public virtual bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) {
bool discard = (ErrorsOnly && level != ErrorLevel.Error) || // Discard non-errors if ErrorsOnly is set
- (tok is TokenWrapper && !(tok is NestedToken)); // Discard wrapped tokens, except for nested ones
+ (tok is TokenWrapper && !(tok is NestedToken) && !(tok is RefinementToken)); // Discard wrapped tokens, except for nested and refinement
if (!discard) {
AllMessages[level].Add(new ErrorMessage { token = tok, message = msg });
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index e47220d7..99b31923 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1103,6 +1103,17 @@ namespace Microsoft.Dafny }
}
}
+
+ // second go through and overriding anything from the opened imports with the ones from the refinementBase
+ if (useImports && moduleDef.RefinementBaseSig != null) {
+ foreach (var kv in moduleDef.RefinementBaseSig.TopLevels) {
+ sig.TopLevels[kv.Key] = kv.Value;
+ }
+ foreach (var kv in moduleDef.RefinementBaseSig.StaticMembers) {
+ sig.StaticMembers[kv.Key] = kv.Value;
+ }
+ }
+
// This is solely used to detect duplicates amongst the various e
Dictionary<string, TopLevelDecl> toplevels = new Dictionary<string, TopLevelDecl>();
// Now add the things present
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index dbbffd87..4b86d848 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -335,3 +335,15 @@ module TopLevelStatics { static method M() // error/warning: static keyword does not belong here
{ }
}
+
+module Library {
+ class T { }
+}
+
+module AA {
+ import opened Library
+}
+
+module B refines AA {
+ datatype T = MakeT(int) // illegal
+}
diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect index e4b46cce..f51e0f6c 100644 --- a/Test/dafny0/Modules0.dfy.expect +++ b/Test/dafny0/Modules0.dfy.expect @@ -30,5 +30,6 @@ Modules0.dfy(320,11): Error: Undeclared top-level type or type parameter: Wazzup Modules0.dfy(321,17): Error: module 'Q_Imp' does not declare a type 'Edon'
Modules0.dfy(323,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)
Modules0.dfy(324,30): Error: member Create does not exist in class Klassy
+Modules0.dfy(348,11): Error: a datatype declaration (T) in a refinement module can only replace an opaque type declaration
Modules0.dfy(101,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name or declare a module import 'opened?')
-31 resolution/type errors detected in Modules0.dfy
+32 resolution/type errors detected in Modules0.dfy
diff --git a/Test/dafny4/Bug125.dfy b/Test/dafny4/Bug125.dfy new file mode 100644 index 00000000..916dd3f8 --- /dev/null +++ b/Test/dafny4/Bug125.dfy @@ -0,0 +1,82 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+abstract module AbstractModuleA
+{
+ type T
+}
+
+abstract module AbstractModuleB
+{
+ import opened AMA : AbstractModuleA
+
+ method Foo(t:T)
+}
+
+abstract module AbstractModuleC refines AbstractModuleB
+{
+ import opened AMA2 : AbstractModuleA
+}
+
+module LibA {
+ class G {
+ static function f(x:int) : bool {
+ x >= 10
+ }
+ }
+
+ function g() : bool {
+ true
+ }
+}
+
+module LibB {
+ class G {
+ static function f(x:int) : bool {
+ x < 10
+ }
+ }
+
+ function g() : bool {
+ false
+ }
+}
+
+module R {
+ import opened LibA
+}
+
+module S refines R {
+ import opened LibB
+ method m() {
+ assert g(); // should be LibA.g
+ }
+
+ method m1() {
+ assert G.f(20); // should be LibA.G.f
+ }
+}
+
+
+module Library {
+
+ class T { }
+
+}
+
+
+
+module A {
+
+ import opened Library
+ class T {
+ }
+}
+
+
+
+module B refines A {
+
+ datatype T = MakeT(int) // illegal for the same reason as above, but Dafny fails to issue an error
+
+}
diff --git a/Test/dafny4/Bug125.dfy.expect b/Test/dafny4/Bug125.dfy.expect new file mode 100644 index 00000000..c87e2af2 --- /dev/null +++ b/Test/dafny4/Bug125.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 10 verified, 0 errors
|