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
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
|
//-----------------------------------------------------------------------------
//
// 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;
using IToken = Microsoft.Boogie.IToken;
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(CloneDeclaration(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);
}
}
}
}
}
IToken Tok(IToken tok) {
// TODO: do something that makes it clear that this token is from a copy
return tok;
}
// -------------------------------------------------- Cloning ---------------------------------------------------------------
TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDecl m) {
Contract.Requires(d != null);
Contract.Requires(m != null);
// top-level declarations clone their tokens
if (d is ArbitraryTypeDecl) {
var dd = (ArbitraryTypeDecl)d;
return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, null);
} else if (d is DatatypeDecl) {
var dd = (DatatypeDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
var ctors = dd.Ctors.ConvertAll(CloneCtor);
var dt = new DatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, null);
return dt;
} else if (d is ClassDecl) {
var dd = (ClassDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
var mm = dd.Members.ConvertAll(CloneMember);
var cl = new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, null);
return cl;
} else {
Contract.Assert(false); // unexpected declaration
return null; // to please compiler
}
}
DatatypeCtor CloneCtor(DatatypeCtor ct) {
// datatype constructors clone their tokens
return new DatatypeCtor(Tok(ct.tok), ct.Name, ct.Formals.ConvertAll(CloneFormal), null);
}
TypeParameter CloneTypeParam(TypeParameter tp) {
return new TypeParameter(tp.tok, tp.Name);
}
MemberDecl CloneMember(MemberDecl member) {
// members clone their tokens
if (member is Field) {
var f = (Field)member;
return new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, CloneType(f.Type), null);
} else if (member is Function) {
var f = (Function)member;
var tps = f.TypeArgs.ConvertAll(CloneTypeParam);
return new Function(Tok(f.tok), f.Name, f.IsStatic, f.IsGhost, f.IsUnlimited, tps, f.Formals.ConvertAll(CloneFormal), CloneType(f.ResultType),
f.Req.ConvertAll(CloneExpr), f.Reads.ConvertAll(CloneFrameExpr), f.Ens.ConvertAll(CloneExpr), CloneSpecExpr(f.Decreases), CloneExpr(f.Body), null);
} else {
var m = (Method)member;
var tps = m.TypeArgs.ConvertAll(CloneTypeParam);
return new Method(Tok(m.tok), m.Name, m.IsStatic, m.IsGhost, tps, m.Ins.ConvertAll(CloneFormal), m.Outs.ConvertAll(CloneFormal),
m.Req.ConvertAll(CloneMayBeFreeExpr), CloneSpecFrameExpr(m.Mod), m.Ens.ConvertAll(CloneMayBeFreeExpr), CloneSpecExpr(m.Decreases), CloneBlockStmt(m.Body), null);
}
}
Type CloneType(Type t) {
// TODO
return t;
}
Formal CloneFormal(Formal formal) {
// TODO
return formal;
}
Specification<Expression> CloneSpecExpr(Specification<Expression> spec) {
// TODO
return spec;
}
Specification<FrameExpression> CloneSpecFrameExpr(Specification<FrameExpression> frame) {
// TODO
return frame;
}
FrameExpression CloneFrameExpr(FrameExpression frame) {
// TODO
return frame;
}
MaybeFreeExpression CloneMayBeFreeExpr(MaybeFreeExpression expr) {
// TODO
return expr;
}
Expression CloneExpr(Expression expr) {
// TODO
return expr;
}
BlockStmt CloneBlockStmt(BlockStmt stmt) {
// TODO
return stmt;
}
Statement CloneStmt(Statement stmt) {
// TODO
return stmt;
}
// -------------------------------------------------- Merging ---------------------------------------------------------------
DatatypeDecl MergeDatatype(DatatypeDecl nw, DatatypeDecl prev) {
// TODO
return nw;
}
ClassDecl MergeClass(ClassDecl nw, ClassDecl prev) {
// TODO
return nw;
}
}
}
|
