1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
// This file contains the transformations that are applied to a module that is
// constructed as a refinement of another. It is invoked during program resolution,
// so the transformation is done syntactically. Upon return from the RefinementTransformer,
// the caller is expected to resolve the resulting module.
//-----------------------------------------------------------------------------
using System;
using System.Collections.Generic;
using System.Numerics;
using System.Diagnostics.Contracts;
namespace Microsoft.Dafny {
public class RefinementTransformer
{
ResolutionErrorReporter reporter;
public RefinementTransformer(ResolutionErrorReporter reporter) {
Contract.Requires(reporter != null);
this.reporter = reporter;
}
public void Construct(ModuleDecl m) {
Contract.Requires(m != null);
Contract.Requires(m.RefinementBase != null);
var prev = m.RefinementBase;
// TODO: What to do with the attributes of prev? Should they be copied as well?
// Include the imports of the base. Note, prev is itself NOT added as an import
// of m; instead, the contents from prev is merged directly into m.
// (Here, we change the import declarations. But edges for these imports will
// not be added to the importGraph of the calling resolver. However, the refines
// clause gave rise to an edge in the importGraph, so the transitive import edges
// are represented in the importGraph.)
foreach (var im in prev.Imports) {
if (!m.ImportNames.Contains(im.Name)) {
m.ImportNames.Add(im.Name);
m.Imports.Add(im);
}
}
// Create a simple name-to-decl dictionary. Ignore any duplicates at this time.
var declaredNames = new Dictionary<string, int>();
for (int i = 0; i < m.TopLevelDecls.Count; i++) {
var d = m.TopLevelDecls[i];
if (!declaredNames.ContainsKey(d.Name)) {
declaredNames.Add(d.Name, i);
}
}
// Merge the declarations of prev into the declarations of m
foreach (var d in prev.TopLevelDecls) {
int index;
if (!declaredNames.TryGetValue(d.Name, out index)) {
m.TopLevelDecls.Add(CreateRefinementCopy(d, m));
} else {
var nw = m.TopLevelDecls[index];
if (d is ArbitraryTypeDecl) {
// this is allowed to be refined by any type declaration, so just keep the new one
} else if (nw is ArbitraryTypeDecl) {
reporter.Error(nw, "an arbitrary 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) {
if (d is ClassDecl) {
reporter.Error(nw, "a datatype declaration ({0}) in a refining module cannot replace a class declaration in the refinement base", nw.Name);
} else {
m.TopLevelDecls[index] = MergeDatatype((DatatypeDecl)nw, (DatatypeDecl)d);
}
} else {
Contract.Assert(nw is ClassDecl);
if (d is DatatypeDecl) {
reporter.Error(nw, "a class declaration ({0}) in a refining module cannot replace a datatype declaration in the refinement base", nw.Name);
} else {
m.TopLevelDecls[index] = MergeClass((ClassDecl)nw, (ClassDecl)d);
}
}
}
}
}
TopLevelDecl CreateRefinementCopy(TopLevelDecl d, ModuleDecl m) {
Contract.Requires(d != null);
Contract.Requires(m != null);
if (d is ArbitraryTypeDecl) {
var dd = (ArbitraryTypeDecl)d;
return new ArbitraryTypeDecl(dd.tok, dd.Name, m, null);
} else if (d is DatatypeDecl) {
var dd = (DatatypeDecl)d;
var dt = new DatatypeDecl(dd.tok, dd.Name, m, dd.TypeArgs/*TODO*/, dd.Ctors/*TODO*/, null);
return dt;
} else if (d is ClassDecl) {
var dd = (ClassDecl)d;
var cl = new ClassDecl(dd.tok, dd.Name, m, dd.TypeArgs/*TODO*/, dd.Members/*TODO*/, null);
return cl;
} else {
Contract.Assert(false); // unexpected declaration
return null; // to please compiler
}
}
DatatypeDecl MergeDatatype(DatatypeDecl nw, DatatypeDecl prev) {
// TODO
return nw;
}
ClassDecl MergeClass(ClassDecl nw, ClassDecl prev) {
// TODO
return nw;
}
}
}
|
