diff options
| author |  Michael Lowell Roberts <mirobert@microsoft.com> | 2015-07-02 15:00:52 -0700 |
|---|---|---|
| committer | Michael Lowell Roberts <mirobert@microsoft.com> | 2015-07-02 15:00:52 -0700 |
| commit | 85d4456ccf1e1d8c456dffa012d3f3d724f50a4a (patch) | |
| tree | da1311552725ba7809e4f3445870c86c98a5fbe6 /Source/Dafny/RefinementTransformer.cs | |
| parent | c7f6887e452cbb91a8297bb64db39a8066750351 (diff) | |
multiple changes...
- fix for requirement inheritance in refinement.
- minimimally viable implementation of exclusive refinement feature.
Diffstat (limited to 'Source/Dafny/RefinementTransformer.cs')
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 05146b7d..2d32f78a 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -86,6 +86,15 @@ namespace Microsoft.Dafny if (Resolver.ResolvePath(m.RefinementBaseRoot, m.RefinementBaseName, out RefinedSig, reporter)) {
if (RefinedSig.ModuleDef != null) {
m.RefinementBase = RefinedSig.ModuleDef;
+ if (m.IsExclusiveRefinement) {
+ if (null == m.RefinementBase.ExclusiveRefinement) {
+ m.RefinementBase.ExclusiveRefinement = m;
+ } else {
+ this.reporter.Error(
+ m.tok,
+ "no more than one exclusive refinement may exist for a given module.");
+ }
+ }
PreResolveWorker(m);
} else {
reporter.Error(m.RefinementBaseName[0], "module ({0}) named as refinement base is not a literal module or simple reference to a literal module", Util.Comma(".", m.RefinementBaseName, x => x.val));
|