adamc@607
|
1 (* Copyright (c) 2009, Adam Chlipala
|
adamc@607
|
2 * All rights reserved.
|
adamc@607
|
3 *
|
adamc@607
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@607
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@607
|
6 *
|
adamc@607
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@607
|
8 * this list of conditions and the following disclaimer.
|
adamc@607
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@607
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@607
|
11 * and/or other materials provided with the distribution.
|
adamc@607
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@607
|
13 * derived from this software without specific prior written permission.
|
adamc@607
|
14 *
|
adamc@607
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@607
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@607
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@607
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@607
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@607
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@607
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@607
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@607
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@607
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@607
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@607
|
26 *)
|
adamc@607
|
27
|
adamc@607
|
28 structure Rpcify :> RPCIFY = struct
|
adamc@607
|
29
|
adamc@607
|
30 open Core
|
adamc@607
|
31
|
adamc@607
|
32 structure U = CoreUtil
|
adamc@607
|
33 structure E = CoreEnv
|
adamc@607
|
34
|
adamc@954
|
35 fun multiLiftExpInExp n e =
|
adamc@954
|
36 if n = 0 then
|
adamc@954
|
37 e
|
adamc@954
|
38 else
|
adamc@954
|
39 multiLiftExpInExp (n - 1) (E.liftExpInExp 0 e)
|
adamc@954
|
40
|
adamc@607
|
41 structure IS = IntBinarySet
|
adamc@607
|
42 structure IM = IntBinaryMap
|
adamc@607
|
43
|
adamc@607
|
44 structure SS = BinarySetFn(struct
|
adamc@607
|
45 type ord_key = string
|
adamc@607
|
46 val compare = String.compare
|
adamc@607
|
47 end)
|
adamc@607
|
48
|
adamc@607
|
49 type state = {
|
adamc@608
|
50 exported : IS.set,
|
adamc@954
|
51 export_decls : decl list,
|
adamc@954
|
52
|
adamc@954
|
53 cpsed : exp' IM.map,
|
adamc@954
|
54 rpc : IS.set
|
adamc@607
|
55 }
|
adamc@607
|
56
|
adamc@607
|
57 fun frob file =
|
adamc@607
|
58 let
|
adamc@908
|
59 val rpcBaseIds = foldl (fn ((d, _), rpcIds) =>
|
adamc@908
|
60 case d of
|
adamc@908
|
61 DVal (_, n, _, (EFfi ("Basis", "rpc"), _), _) => IS.add (rpcIds, n)
|
adamc@908
|
62 | DVal (_, n, _, (ENamed n', _), _) => if IS.member (rpcIds, n') then
|
adamc@908
|
63 IS.add (rpcIds, n)
|
adamc@908
|
64 else
|
adamc@908
|
65 rpcIds
|
adamc@908
|
66 | _ => rpcIds)
|
adamc@908
|
67 IS.empty file
|
adamc@607
|
68
|
adamc@609
|
69 val tfuncs = foldl
|
adamc@609
|
70 (fn ((d, _), tfuncs) =>
|
adamc@609
|
71 let
|
adamc@642
|
72 fun doOne ((x, n, t, e, _), tfuncs) =
|
adamc@609
|
73 let
|
adamc@642
|
74 val loc = #2 e
|
adamc@642
|
75
|
adamc@642
|
76 fun crawl (t, e, args) =
|
adamc@642
|
77 case (#1 t, #1 e) of
|
adamc@642
|
78 (CApp (_, ran), _) =>
|
adamc@642
|
79 SOME (x, rev args, ran, e)
|
adamc@642
|
80 | (TFun (arg, rest), EAbs (x, _, _, e)) =>
|
adamc@642
|
81 crawl (rest, e, (x, arg) :: args)
|
adamc@642
|
82 | (TFun (arg, rest), _) =>
|
adamc@642
|
83 crawl (rest, (EApp (e, (ERel (length args), loc)), loc), ("x", arg) :: args)
|
adamc@609
|
84 | _ => NONE
|
adamc@609
|
85 in
|
adamc@642
|
86 case crawl (t, e, []) of
|
adamc@609
|
87 NONE => tfuncs
|
adamc@609
|
88 | SOME sg => IM.insert (tfuncs, n, sg)
|
adamc@609
|
89 end
|
adamc@609
|
90 in
|
adamc@609
|
91 case d of
|
adamc@609
|
92 DVal vi => doOne (vi, tfuncs)
|
adamc@609
|
93 | DValRec vis => foldl doOne tfuncs vis
|
adamc@609
|
94 | _ => tfuncs
|
adamc@609
|
95 end)
|
adamc@609
|
96 IM.empty file
|
adamc@609
|
97
|
adamc@607
|
98 fun exp (e, st) =
|
adamc@649
|
99 let
|
adamc@649
|
100 fun getApp (e', args) =
|
adamc@908
|
101 case e' of
|
adamc@908
|
102 ENamed n => SOME (n, args)
|
adamc@908
|
103 | EApp (e1, e2) => getApp (#1 e1, e2 :: args)
|
adamc@908
|
104 | _ => NONE
|
adamc@642
|
105
|
adamc@908
|
106 fun newRpc (trans : exp, st : state) =
|
adamc@908
|
107 case getApp (#1 trans, []) of
|
adamc@908
|
108 NONE => (ErrorMsg.errorAt (#2 trans)
|
adamc@908
|
109 "RPC code doesn't use a named function or transaction";
|
adamc@908
|
110 (#1 trans, st))
|
adamc@908
|
111 | SOME (n, args) =>
|
adamc@908
|
112 case IM.find (tfuncs, n) of
|
adamc@908
|
113 NONE => ((*Print.prefaces "BAD" [("e", CorePrint.p_exp CoreEnv.empty (e, loc))];*)
|
adamc@908
|
114 raise Fail ("Rpcify: Undetected transaction function " ^ Int.toString n))
|
adamc@908
|
115 | SOME (_, _, ran, _) =>
|
adamc@908
|
116 let
|
adamc@908
|
117 val loc = #2 trans
|
adamc@642
|
118
|
adamc@908
|
119 val (exported, export_decls) =
|
adamc@908
|
120 if IS.member (#exported st, n) then
|
adamc@908
|
121 (#exported st, #export_decls st)
|
adamc@908
|
122 else
|
adamc@908
|
123 (IS.add (#exported st, n),
|
adamc@908
|
124 (DExport (Rpc ReadWrite, n), loc) :: #export_decls st)
|
adamc@642
|
125
|
adamc@908
|
126 val st = {exported = exported,
|
adamc@954
|
127 export_decls = export_decls,
|
adamc@954
|
128 cpsed = #cpsed st,
|
adamc@954
|
129 rpc = #rpc st}
|
adamc@642
|
130
|
adamc@908
|
131 val k = (ECApp ((EFfi ("Basis", "return"), loc),
|
adamc@908
|
132 (CFfi ("Basis", "transaction"), loc)), loc)
|
adamc@908
|
133 val k = (ECApp (k, ran), loc)
|
adamc@908
|
134 val k = (EApp (k, (EFfi ("Basis", "transaction_monad"), loc)), loc)
|
adamc@908
|
135 val e' = EServerCall (n, args, k, ran, ran)
|
adamc@651
|
136 in
|
adamc@908
|
137 (e', st)
|
adamc@651
|
138 end
|
adamc@649
|
139 in
|
adamc@649
|
140 case e of
|
adamc@908
|
141 EApp ((ECApp ((EFfi ("Basis", "rpc"), _), ran), _), trans) => newRpc (trans, st)
|
adamc@908
|
142 | EApp ((ECApp ((ENamed n, _), ran), _), trans) =>
|
adamc@908
|
143 if IS.member (rpcBaseIds, n) then
|
adamc@908
|
144 newRpc (trans, st)
|
adamc@908
|
145 else
|
adamc@908
|
146 (e, st)
|
adamc@642
|
147
|
adamc@954
|
148 | ENamed n =>
|
adamc@954
|
149 (case IM.find (#cpsed st, n) of
|
adamc@954
|
150 NONE => (e, st)
|
adamc@954
|
151 | SOME re => (re, st))
|
adamc@954
|
152
|
adamc@649
|
153 | _ => (e, st)
|
adamc@649
|
154 end
|
adamc@607
|
155
|
adamc@642
|
156 and doExp (e, st) = U.Exp.foldMap {kind = fn x => x,
|
adamc@642
|
157 con = fn x => x,
|
adamc@642
|
158 exp = exp} st (ReduceLocal.reduceExp e)
|
adamc@642
|
159
|
adamc@607
|
160 fun decl (d, st : state) =
|
adamc@607
|
161 let
|
adamc@954
|
162 val makesServerCall = U.Exp.exists {kind = fn _ => false,
|
adamc@954
|
163 con = fn _ => false,
|
adamc@954
|
164 exp = fn EFfi ("Basis", "rpc") => true
|
adamc@954
|
165 | ENamed n => IS.member (#rpc st, n)
|
adamc@954
|
166 | _ => false}
|
adamc@954
|
167
|
adamc@954
|
168 val (d, st) =
|
adamc@954
|
169 case #1 d of
|
adamc@954
|
170 DValRec vis =>
|
adamc@954
|
171 if List.exists (fn (_, _, _, e, _) => makesServerCall e) vis then
|
adamc@954
|
172 let
|
adamc@954
|
173 val all = foldl (fn ((_, n, _, _, _), all) => IS.add (all, n)) IS.empty vis
|
adamc@954
|
174
|
adamc@954
|
175 val usesRec = U.Exp.exists {kind = fn _ => false,
|
adamc@954
|
176 con = fn _ => false,
|
adamc@954
|
177 exp = fn ENamed n => IS.member (all, n)
|
adamc@954
|
178 | _ => false}
|
adamc@954
|
179
|
adamc@954
|
180 val noRec = not o usesRec
|
adamc@954
|
181
|
adamc@954
|
182 fun tailOnly (e, _) =
|
adamc@954
|
183 case e of
|
adamc@954
|
184 EPrim _ => true
|
adamc@954
|
185 | ERel _ => true
|
adamc@954
|
186 | ENamed _ => true
|
adamc@954
|
187 | ECon (_, _, _, SOME e) => noRec e
|
adamc@954
|
188 | ECon _ => true
|
adamc@954
|
189 | EFfi _ => true
|
adamc@954
|
190 | EFfiApp (_, _, es) => List.all noRec es
|
adamc@954
|
191 | EApp (e1, e2) => noRec e2 andalso tailOnly e1
|
adamc@954
|
192 | EAbs (_, _, _, e) => noRec e
|
adamc@954
|
193 | ECApp (e1, _) => tailOnly e1
|
adamc@954
|
194 | ECAbs (_, _, e) => noRec e
|
adamc@954
|
195
|
adamc@954
|
196 | EKAbs (_, e) => noRec e
|
adamc@954
|
197 | EKApp (e1, _) => tailOnly e1
|
adamc@954
|
198
|
adamc@954
|
199 | ERecord xes => List.all (noRec o #2) xes
|
adamc@954
|
200 | EField (e1, _, _) => noRec e1
|
adamc@954
|
201 | EConcat (e1, _, e2, _) => noRec e1 andalso noRec e2
|
adamc@954
|
202 | ECut (e1, _, _) => noRec e1
|
adamc@954
|
203 | ECutMulti (e1, _, _) => noRec e1
|
adamc@954
|
204
|
adamc@954
|
205 | ECase (e1, pes, _) => noRec e1 andalso List.all (tailOnly o #2) pes
|
adamc@954
|
206
|
adamc@954
|
207 | EWrite e1 => noRec e1
|
adamc@954
|
208
|
adamc@954
|
209 | EClosure (_, es) => List.all noRec es
|
adamc@954
|
210
|
adamc@954
|
211 | ELet (_, _, e1, e2) => noRec e1 andalso tailOnly e2
|
adamc@954
|
212
|
adamc@954
|
213 | EServerCall (_, es, (EAbs (_, _, _, e), _), _, _) =>
|
adamc@954
|
214 List.all noRec es andalso tailOnly e
|
adamc@954
|
215 | EServerCall (_, es, e, _, _) => List.all noRec es andalso noRec e
|
adamc@954
|
216
|
adamc@954
|
217 | ETailCall _ => raise Fail "Rpcify: ETailCall too early"
|
adamc@954
|
218
|
adamc@954
|
219 fun tailOnlyF e =
|
adamc@954
|
220 case #1 e of
|
adamc@954
|
221 EAbs (_, _, _, e) => tailOnlyF e
|
adamc@954
|
222 | ECAbs (_, _, e) => tailOnlyF e
|
adamc@954
|
223 | EKAbs (_, e) => tailOnlyF e
|
adamc@954
|
224 | _ => tailOnly e
|
adamc@954
|
225
|
adamc@954
|
226 val nonTail = foldl (fn ((_, n, _, e, _), nonTail) =>
|
adamc@954
|
227 if tailOnlyF e then
|
adamc@954
|
228 nonTail
|
adamc@954
|
229 else
|
adamc@954
|
230 IS.add (nonTail, n)) IS.empty vis
|
adamc@954
|
231 in
|
adamc@954
|
232 if IS.isEmpty nonTail then
|
adamc@954
|
233 (d, {exported = #exported st,
|
adamc@954
|
234 export_decls = #export_decls st,
|
adamc@954
|
235 cpsed = #cpsed st,
|
adamc@954
|
236 rpc = IS.union (#rpc st, all)})
|
adamc@954
|
237 else
|
adamc@954
|
238 let
|
adamc@954
|
239 val rpc = foldl (fn ((_, n, _, _, _), rpc) =>
|
adamc@954
|
240 IS.add (rpc, n)) (#rpc st) vis
|
adamc@954
|
241
|
adamc@954
|
242 val (cpsed, vis') =
|
adamc@954
|
243 foldl (fn (vi as (x, n, t, e, s), (cpsed, vis')) =>
|
adamc@954
|
244 if IS.member (nonTail, n) then
|
adamc@954
|
245 let
|
adamc@954
|
246 fun getArgs (t, acc) =
|
adamc@954
|
247 case #1 t of
|
adamc@954
|
248 TFun (dom, ran) =>
|
adamc@954
|
249 getArgs (ran, dom :: acc)
|
adamc@954
|
250 | _ => (rev acc, t)
|
adamc@954
|
251 val (ts, ran) = getArgs (t, [])
|
adamc@954
|
252 val ran = case #1 ran of
|
adamc@954
|
253 CApp (_, ran) => ran
|
adamc@954
|
254 | _ => raise Fail "Rpcify: Tail function not transactional"
|
adamc@954
|
255 val len = length ts
|
adamc@954
|
256
|
adamc@954
|
257 val loc = #2 e
|
adamc@954
|
258 val args = ListUtil.mapi
|
adamc@954
|
259 (fn (i, _) =>
|
adamc@954
|
260 (ERel (len - i - 1), loc))
|
adamc@954
|
261 ts
|
adamc@955
|
262 val k = (EFfi ("Basis", "return"), loc)
|
adamc@955
|
263 val trans = (CFfi ("Basis", "transaction"), loc)
|
adamc@955
|
264 val k = (ECApp (k, trans), loc)
|
adamc@955
|
265 val k = (ECApp (k, ran), loc)
|
adamc@955
|
266 val k = (EApp (k, (EFfi ("Basis", "transaction_monad"),
|
adamc@955
|
267 loc)), loc)
|
adamc@954
|
268 val re = (ETailCall (n, args, k, ran, ran), loc)
|
adamc@954
|
269 val (re, _) = foldr (fn (dom, (re, ran)) =>
|
adamc@954
|
270 ((EAbs ("x", dom, ran, re),
|
adamc@954
|
271 loc),
|
adamc@954
|
272 (TFun (dom, ran), loc)))
|
adamc@954
|
273 (re, ran) ts
|
adamc@954
|
274
|
adamc@954
|
275 val be = multiLiftExpInExp (len + 1) e
|
adamc@954
|
276 val be = ListUtil.foldli
|
adamc@954
|
277 (fn (i, _, be) =>
|
adamc@954
|
278 (EApp (be, (ERel (len - i), loc)), loc))
|
adamc@954
|
279 be ts
|
adamc@954
|
280 val ne = (EFfi ("Basis", "bind"), loc)
|
adamc@954
|
281 val ne = (ECApp (ne, trans), loc)
|
adamc@954
|
282 val ne = (ECApp (ne, ran), loc)
|
adamc@954
|
283 val unit = (TRecord (CRecord ((KType, loc), []),
|
adamc@954
|
284 loc), loc)
|
adamc@954
|
285 val ne = (ECApp (ne, unit), loc)
|
adamc@954
|
286 val ne = (EApp (ne, (EFfi ("Basis", "transaction_monad"),
|
adamc@954
|
287 loc)), loc)
|
adamc@954
|
288 val ne = (EApp (ne, be), loc)
|
adamc@954
|
289 val ne = (EApp (ne, (ERel 0, loc)), loc)
|
adamc@954
|
290 val tunit = (CApp (trans, unit), loc)
|
adamc@954
|
291 val kt = (TFun (ran, tunit), loc)
|
adamc@954
|
292 val ne = (EAbs ("k", kt, tunit, ne), loc)
|
adamc@954
|
293 val (ne, res) = foldr (fn (dom, (ne, ran)) =>
|
adamc@954
|
294 ((EAbs ("x", dom, ran, ne), loc),
|
adamc@954
|
295 (TFun (dom, ran), loc)))
|
adamc@954
|
296 (ne, (TFun (kt, tunit), loc)) ts
|
adamc@954
|
297 in
|
adamc@954
|
298 (IM.insert (cpsed, n, #1 re),
|
adamc@954
|
299 (x, n, res, ne, s) :: vis')
|
adamc@954
|
300 end
|
adamc@954
|
301 else
|
adamc@954
|
302 (cpsed, vi :: vis'))
|
adamc@954
|
303 (#cpsed st, []) vis
|
adamc@954
|
304 in
|
adamc@954
|
305 ((DValRec (rev vis'), ErrorMsg.dummySpan),
|
adamc@954
|
306 {exported = #exported st,
|
adamc@954
|
307 export_decls = #export_decls st,
|
adamc@954
|
308 cpsed = cpsed,
|
adamc@954
|
309 rpc = rpc})
|
adamc@954
|
310 end
|
adamc@954
|
311 end
|
adamc@954
|
312 else
|
adamc@954
|
313 (d, st)
|
adamc@954
|
314 | DVal (x, n, t, e, s) =>
|
adamc@954
|
315 (d,
|
adamc@954
|
316 {exported = #exported st,
|
adamc@954
|
317 export_decls = #export_decls st,
|
adamc@954
|
318 cpsed = #cpsed st,
|
adamc@954
|
319 rpc = if makesServerCall e then
|
adamc@954
|
320 IS.add (#rpc st, n)
|
adamc@954
|
321 else
|
adamc@954
|
322 #rpc st})
|
adamc@954
|
323 | _ => (d, st)
|
adamc@954
|
324
|
adamc@607
|
325 val (d, st) = U.Decl.foldMap {kind = fn x => x,
|
adamc@607
|
326 con = fn x => x,
|
adamc@607
|
327 exp = exp,
|
adamc@607
|
328 decl = fn x => x}
|
adamc@607
|
329 st d
|
adamc@607
|
330 in
|
adamc@908
|
331 (#export_decls st @ [d],
|
adamc@908
|
332 {exported = #exported st,
|
adamc@954
|
333 export_decls = [],
|
adamc@954
|
334 cpsed = #cpsed st,
|
adamc@954
|
335 rpc = #rpc st})
|
adamc@607
|
336 end
|
adamc@607
|
337
|
adamc@607
|
338 val (file, _) = ListUtil.foldlMapConcat decl
|
adamc@908
|
339 {exported = IS.empty,
|
adamc@954
|
340 export_decls = [],
|
adamc@954
|
341 cpsed = IM.empty,
|
adamc@954
|
342 rpc = rpcBaseIds}
|
adamc@607
|
343 file
|
adamc@607
|
344 in
|
adamc@607
|
345 file
|
adamc@607
|
346 end
|
adamc@607
|
347
|
adamc@607
|
348 end
|