diff options
| -rw-r--r-- | Source/Dafny/Resolver.cs | 18 | ||||
| -rw-r--r-- | Test/dafny0/ModuleExport.dfy | 37 | ||||
| -rw-r--r-- | Test/dafny0/ModuleExport.dfy.expect | 6 |
3 files changed, 56 insertions, 5 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index d3b59b51..aa9ce148 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -742,7 +742,7 @@ namespace Microsoft.Dafny d.ExtendDecls.Add(extend);
exportDependencies.AddEdge(d, extend);
} else {
- reporter.Error(MessageSource.Resolver, m.tok, s + " must be an export of" + m + " to be extended");
+ reporter.Error(MessageSource.Resolver, m.tok, s + " must be an export of " + m.Name + " to be extended");
}
}
foreach (ExportSignature export in d.Exports) {
@@ -757,7 +757,7 @@ namespace Microsoft.Dafny } else if (sig.StaticMembers.TryGetValue(name, out member)) {
export.Decl = member;
} else {
- reporter.Error(MessageSource.Resolver, d.tok, name + " must be a member of " + m + " to be exported");
+ reporter.Error(MessageSource.Resolver, d.tok, name + " must be a member of " + m.Name + " to be exported");
}
}
}
@@ -779,7 +779,7 @@ namespace Microsoft.Dafny if (defaultExport == null) {
defaultExport = decl;
} else {
- reporter.Error(MessageSource.Resolver, m.tok, "more than one default export declared: {0}, {1}", defaultExport, decl);
+ reporter.Error(MessageSource.Resolver, m.tok, "more than one default export declared in module {0}", m.Name);
}
}
// fill in export signature
@@ -811,9 +811,14 @@ namespace Microsoft.Dafny }
}
- // set the default export if it exists, otherwise, default is export everything
+ // set the default export if it exists
if (defaultExport != null) {
literalDecl.DefaultExport = defaultExport.Signature;
+ } else {
+ // if there is at least one exported view, but no exported view marked as default, then defaultExport should be null.
+ if (sortedDecls.Count > 0) {
+ literalDecl.DefaultExport = null;
+ }
}
}
@@ -1437,6 +1442,11 @@ namespace Microsoft.Dafny // use the default export when the importing the root
LiteralModuleDecl decl = (LiteralModuleDecl)root;
p = decl.DefaultExport;
+ if (p == null) {
+ // no default view is specified.
+ reporter.Error(MessageSource.Resolver, decl.tok, "no default export declared in module: {0}", decl.Name);
+ return false;
+ }
return true;
}
diff --git a/Test/dafny0/ModuleExport.dfy b/Test/dafny0/ModuleExport.dfy index 81fe0ed5..1e69764f 100644 --- a/Test/dafny0/ModuleExport.dfy +++ b/Test/dafny0/ModuleExport.dfy @@ -65,4 +65,41 @@ module E { case Kiwi(x) => 7
case Orang => 8 // error
}
+}
+
+module F {
+ default export Public { f, h}
+ default export E1 { f, g}
+ export E2 extends Public2, E1 {T} // error: Public2 is not a exported view of F
+ export Friend extends Public {g2, T} // error: g2 is not a member of F
+ export Fruit {Data}
+
+ method h() {}
+ function f(): int { 818 }
+ function g() : int { 819 }
+ function k() : int { 820 }
+
+ class T
+ {
+ static method l() {}
+ }
+
+ datatype Data = Lemon | Kiwi(int)
+}
+
+module G {
+ export Public { f, h}
+
+ method h() {}
+ function f(): int { 818 }
+ function g() : int { 819 }
+ function k() : int { 820 }
+}
+
+module H {
+ import G // error: G has no default export
+}
+
+module I {
+ import G.Public // OK
}
\ No newline at end of file diff --git a/Test/dafny0/ModuleExport.dfy.expect b/Test/dafny0/ModuleExport.dfy.expect index c7444bdb..274c8f31 100644 --- a/Test/dafny0/ModuleExport.dfy.expect +++ b/Test/dafny0/ModuleExport.dfy.expect @@ -6,4 +6,8 @@ ModuleExport.dfy(42,11): Error: unresolved identifier: k ModuleExport.dfy(52,9): Error: unresolved identifier: g
ModuleExport.dfy(53,9): Error: unresolved identifier: k
ModuleExport.dfy(66,2): Error: member Orang does not exist in datatype Data
-8 resolution/type errors detected in ModuleExport.dfy
+ModuleExport.dfy(70,7): Error: Public2 must be an export of F to be extended
+ModuleExport.dfy(74,9): Error: g2 must be a member of F to be exported
+ModuleExport.dfy(70,7): Error: more than one default export declared in module F
+ModuleExport.dfy(90,7): Error: no default export declared in module: G
+12 resolution/type errors detected in ModuleExport.dfy
|