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
204
205
206
207
208
209
210
211
|
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
class ChaliceToCSharp {
def convertProgram(classes: List[Class]): String = {
"using Chalice;" + nl + nl +
rep(classes map convertClass)
}
def convertClass(cl: Class): String = if (cl.IsExternal) "" else {
"public class " + cl.id + " {" + nl +
indentMore { indent + "public " + cl.id + "() " + "{" + nl + indent + "}" } + nl + nl +
(if(0 < cl.Fields.length) {
indentMore { indent + "public " + cl.id + "(" + repsep(cl.Fields map { f => convertType(f.typ) + " " + f.Id }, ", ") + ") " + "{" + nl +
indentMore { rep(cl.Fields map { f => indent + "this." + f.Id + " = " + f.Id + ";" + nl}) } +
indent + "}" } + nl + nl
} else "") +
indentMore { repsep(cl.members map convertMember, nl) } +
"}" + nl + nl
}
def convertMember(member: Member): String = {
member match {
case Field(id, tp) =>
indent + "public " + convertType(tp) + " " + id + ";" + nl
case meth@Method(id, ins, outs, spec, body) =>
var csharpmain = if(id.equals("Start") && ins.length == 0 && outs.length == 0) {
indent + "public static void Main() { " + nl +
indentMore {
indent + meth.Parent.id + " newObject = new " + meth.Parent.id + "();" + nl +
indent + "newObject.Start();" + nl
} +
indent + "}" + nl + nl
} else { "" };
var params = repsep(ins map { variable => convertType(variable.t) + " " + variable.id }, ", ") + (if(ins.length > 0 && outs.length > 0) ", " else "") +
repsep(outs map { variable => "out " + convertType(variable.t) + " " + variable.id }, ", ");
csharpmain +
indent + "public " + "void " + id + "(" + params + ") " + "{" + nl +
indentMore {
rep(outs map { x => indent + x.id + " = " + defaultValue(x.t) + ";" + nl } ) +
rep(body map convertStatement)
} +
indent + "}" + nl + nl +
indent + "public delegate " + "void " + id + "_delegate" + "(" + params + ");" + nl + nl +
indent + "public class " + "Token_" + id + " { " + nl +
(indentMore {
indent + "public " + id + "_delegate " + "del;" + nl +
indent + "public " + "System.IAsyncResult " + "async;" + nl +
(rep(outs map { o: Variable => indent + "public " + convertType(o.t) + " " + o.id + ";" + nl }))
}) +
indent + "}" + nl
case Function(id, ins, out, spec, definition) =>
indent + "public " + convertType(out) + " " + id + "(" +
repsep(ins map { variable => convertType(variable.t) + " " + variable.id }, ", ") +
") " + "{" + nl +
indentMore { indent + "return " + convertExpression(definition) + ";" + nl } +
indent + "}" + nl
case MonitorInvariant(_) => indent + "// monitor invariant" + nl
case Predicate(_, _) => indent + "//predicate" + nl
}
}
def convertStatement(statement: Statement): String = {
statement match {
case Assert(e) => indent + "// assert" + nl
case Assume(e) => indent + "assert " + convertExpression(e) + ";" // todo: what if e contains old, result, ...
case BlockStmt(ss) => indent + "{" + nl + (indentMore { rep(ss map convertStatement) }) + indent + "}" + nl
case IfStmt(guard, thn, els) => indent + "if (" + convertExpression(guard) + ")" + nl + convertStatement(thn) +
(if(els.isDefined) (indent + "else" + nl + convertStatement(els.get)) else { "" }) + nl
case LocalVar(id, tp, const, ghost, rhs) =>
indent + convertType(tp) + " " + id + " = " +
(if(rhs.isDefined) convertExpression(rhs.get) else defaultValue(tp)) +
";" + nl
case FieldUpdate(MemberAccess(target, f), rhs) =>
indent + convertExpression(target) + "." + f + " = " + convertExpression(rhs) + ";" + nl
case Assign(VariableExpr(x), rhs) =>
indent + x + " = " + convertExpression(rhs) + ";" + nl
case WhileStmt(guard, _, _, body) =>
indent + "while (" + convertExpression(guard) + ")" + nl + convertStatement(body) + nl
case Call(lhs, target, id, args) =>
indent + convertExpression(target) + "." + id + "(" +
repsep(args map convertExpression, ", ") +
(if(args.length > 0 && lhs.length > 0) ", " else "") +
repsep(lhs map { l => "out " + convertExpression(l) }, ", ") +
")" + ";" + nl
case Install(_, _, _) => indent + "// install" + nl
case Share(_, _, _) => indent + "// share" + nl
case Unshare(_) => indent + "// unshare" + nl
case Downgrade(_) => indent + "// downgrade" + nl
case Acquire(obj) => indent + "System.Threading.Monitor.Enter(" + convertExpression(obj) + ")" + ";" + nl
case Release(obj) => indent + "System.Threading.Monitor.Exit(" + convertExpression(obj) + ")" + ";" + nl
case Lock(obj, body, false) => indent + "lock(" + convertExpression(obj) + ") " + nl + convertStatement(body) + nl
case Free(_) => indent + "// free" + nl
case Fold(_) => indent + "// fold" + nl
case Unfold(_) => indent + "// unfold" + nl
case RdAcquire(obj) => assert(false); ""
case RdRelease(obj) => assert(false); ""
case Lock(_, _, true) => assert(false); ""
case ca@CallAsync(declaresLocal, lhs, obj, id, args) =>
val tokenName = if(declaresLocal) lhs.id else { uniqueInt += 1; "tok_" + uniqueInt };
val call = convertExpression(obj) + "." + id;
val tokenClass = ca.m.Parent.id + ".Token_" + id;
val delegateName = ca.m.Parent.id + "." + id + "_delegate";
indent + tokenClass + " " + tokenName + " = new " + tokenClass + "();" + nl +
indent + tokenName + "." + "del" + " = new " + delegateName + "(" + call + ");" + nl +
indent + tokenName + "." + "async" + " = " + tokenName + "." + "del" + "." + "BeginInvoke(" + repsep(args map convertExpression, ", ") +
(if(args.length > 0 && ca.m.outs.length > 0) ", " else "") + repsep(ca.m.outs map { o => "out " + tokenName + "." + o.id }, ", ") +
(if(args.length > 0 || ca.m.outs.length > 0) ", " else "") + "null, null" +
");" + nl
case ja@JoinAsync(lhs, token) =>
indent + convertExpression(token) + "." + "del.EndInvoke(" +
repsep(lhs map { x => "out " + x.id}, ", ") +
(if(lhs.length > 0) ", " else "") + convertExpression(token) + "." + "async" + ");" + nl
}
}
def convertExpression(expression: RValue): String = {
expression match {
case IntLiteral(n) => "" + n
case BoolLiteral(b) => "" + b
case NullLiteral() => "null"
case th: ThisExpr => "this"
case VariableExpr(id) => id
case MemberAccess(target, f) => convertExpression(target) + "." + f
case newrhs@NewRhs(c, initialization) =>
if(initialization.length == 0) { "new " + c + "()" } else {
val init = repsep(newrhs.typ.Fields map { f => (initialization.find { i => i.f == f}) match {
case None => defaultValue(f.typ)
case Some(init) => convertExpression(init.e);
}
}, ", ");
"new " + c + "(" + init + ")";
}
case At(s, i) => convertExpression(s) + ".At(" + convertExpression(i) + ")"
case Append(s1, s2) => convertExpression(s1) + ".Append(" + convertExpression(s2) + ")"
case Take(s, i) => convertExpression(s) + ".Take(" + convertExpression(i) + ")"
case Drop(s, i) => convertExpression(s) + ".Drop(" + convertExpression(i) + ")"
case bin: BinaryExpr => "(" + convertExpression(bin.E0) + " " + bin.OpName + " " + convertExpression(bin.E1) + ")"// todo: <==> and ==>
case Unfolding(p, e) => convertExpression(e)
case FunctionApplication(target, id, args) => convertExpression(target) + "." + id + "(" + repsep(args map convertExpression, ", ") + ")"
case Not(e) => "(! " + convertExpression(e) + ")"
case EmptySeq(tp) => "new Chalice.ImmutableList<" + convertType(tp) + ">()"
case es@ExplicitSeq(elems) =>
val elemType = new Type(es.typ.asInstanceOf[SeqClass].parameter);
"new Chalice.ImmutableList<" + convertType(elemType) + ">(" +
"new " + convertType(elemType) + "[] {" + repsep(elems map convertExpression, ", ") + "}" +
")"
case Range(min, max) => "Chalice.ImmutableList.Range(" + convertExpression(min) + ", " + convertExpression(max) + ")"
case Length(s) => convertExpression(s) + ".Length"
case IfThenElse(c, thn, els) => "(" + convertExpression(c) + " ? " + convertExpression(thn) + " : " + convertExpression(els) + ")"
}
}
def convertType(tp: Type): String = {
tp.typ match {
case t: TokenClass => t.c.FullName + ".Token_" + t.m
case s: SeqClass => "Chalice.ImmutableList<" + convertType(new Type(s.parameter)) + ">"
case IntClass => "int"
case BoolClass => "bool"
case NullClass => "object"
case Class(id, _, _, _) => id
}
}
def defaultValue(tp: Type) = {
tp.typ match {
case t: TokenClass => "null"
case s: SeqClass => "new Chalice.ImmutableList<" + convertType(new Type(s.parameter)) + ">()"
case IntClass => "0"
case BoolClass => "false"
case NullClass => "null"
case Class(id, _, _, _) => "null"
}
}
// utility methods below
var uniqueInt: int = 0;
val nl = System.getProperty("line.separator");
var indentLevel = 0
def rep(strings: List[String]): String = {
strings.foldLeft("")({ (a, b) => a + b })
}
def repsep(strings: List[String], separator: String): String = {
if(strings.length == 0) {
""
} else {
strings.reduceLeft({ (a, b) => a + separator + b })
}
}
def indent: String = {
def doIndent(i: int): String = {
if(i==0) { "" } else { " " + doIndent(i-1) }
}
doIndent(indentLevel);
}
def indentMore(what: => String) = {
val prev = indentLevel
indentLevel = indentLevel + 1
val result = what
indentLevel = prev
result
}
}
|
