comparison src/rpcify.sml @ 649:96ebc6bdb5a0

Batch example
author Adam Chlipala <adamc@hcoop.net>
date Tue, 10 Mar 2009 15:17:23 -0400
parents 4a125bbc602d
children fcf0bd3d1667
comparison
equal deleted inserted replaced
648:3c6d535d3d8b 649:96ebc6bdb5a0
138 | _ => tfuncs 138 | _ => tfuncs
139 end) 139 end)
140 IM.empty file 140 IM.empty file
141 141
142 fun exp (e, st) = 142 fun exp (e, st) =
143 case e of 143 let
144 EApp ( 144 fun getApp (e', args) =
145 (EApp 145 let
146 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _), 146 val loc = #2 e'
147 (EFfi ("Basis", "transaction_monad"), _)), _), 147 in
148 (ECase (ed, pes, {disc, ...}), _)), _),
149 trans2) =>
150 let
151 val e' = (EFfi ("Basis", "bind"), loc)
152 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
153 val e' = (ECApp (e', t1), loc)
154 val e' = (ECApp (e', t2), loc)
155 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
156
157 val (pes, st) = ListUtil.foldlMap (fn ((p, e), st) =>
158 let
159 val e' = (EApp (e', e), loc)
160 val e' = (EApp (e',
161 multiLiftExpInExp (E.patBindsN p)
162 trans2), loc)
163 val (e', st) = doExp (e', st)
164 in
165 ((p, e'), st)
166 end) st pes
167 in
168 (ECase (ed, pes, {disc = disc,
169 result = (CApp ((CFfi ("Basis", "transaction"), loc), t2), loc)}),
170 st)
171 end
172
173 | EApp (
174 (EApp
175 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _),
176 (EFfi ("Basis", "transaction_monad"), _)), _),
177 (EServerCall (n, es, ke, t), _)), _),
178 trans2) =>
179 let
180 val e' = (EFfi ("Basis", "bind"), loc)
181 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
182 val e' = (ECApp (e', t), loc)
183 val e' = (ECApp (e', t2), loc)
184 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
185 val e' = (EApp (e', (EApp (E.liftExpInExp 0 ke, (ERel 0, loc)), loc)), loc)
186 val e' = (EApp (e', E.liftExpInExp 0 trans2), loc)
187 val e' = (EAbs ("x", t, t2, e'), loc)
188 val e' = (EServerCall (n, es, e', t), loc)
189 val (e', st) = doExp (e', st)
190 in
191 (#1 e', st)
192 end
193
194 | EApp (
195 (EApp
196 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), _), _), t3), _),
197 (EFfi ("Basis", "transaction_monad"), _)), _),
198 (EApp ((EApp
199 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), _), _), _), t1), _), t2), _),
200 (EFfi ("Basis", "transaction_monad"), _)), _),
201 trans1), _), trans2), _)), _),
202 trans3) =>
203 let
204 val e'' = (EFfi ("Basis", "bind"), loc)
205 val e'' = (ECApp (e'', (CFfi ("Basis", "transaction"), loc)), loc)
206 val e'' = (ECApp (e'', t2), loc)
207 val e'' = (ECApp (e'', t3), loc)
208 val e'' = (EApp (e'', (EFfi ("Basis", "transaction_monad"), loc)), loc)
209 val e'' = (EApp (e'', (EApp (E.liftExpInExp 0 trans2, (ERel 0, loc)), loc)), loc)
210 val e'' = (EApp (e'', E.liftExpInExp 0 trans3), loc)
211 val e'' = (EAbs ("x", t1, (CApp ((CFfi ("Basis", "transaction"), loc), t3), loc), e''), loc)
212
213 val e' = (EFfi ("Basis", "bind"), loc)
214 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
215 val e' = (ECApp (e', t1), loc)
216 val e' = (ECApp (e', t3), loc)
217 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
218 val e' = (EApp (e', trans1), loc)
219 val e' = (EApp (e', e''), loc)
220 val (e', st) = doExp (e', st)
221 in
222 (#1 e', st)
223 end
224
225 | EApp (
226 (EApp
227 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), _), _), _), _), _), _), _),
228 (EFfi ("Basis", "transaction_monad"), _)), _),
229 _), loc),
230 (EAbs (_, _, _, (EWrite _, _)), _)) => (e, st)
231
232 | EApp (
233 (EApp
234 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), _), _), _), t1), _), t2), _),
235 (EFfi ("Basis", "transaction_monad"), _)), _),
236 trans1), loc),
237 trans2) =>
238 let
239 (*val () = Print.prefaces "Default"
240 [("e", CorePrint.p_exp CoreEnv.empty (e, ErrorMsg.dummySpan))]*)
241
242 fun getApp (e', args) =
243 case #1 e' of 148 case #1 e' of
244 ENamed n => (n, args) 149 ENamed n => (n, args)
245 | EApp (e1, e2) => getApp (e1, e2 :: args) 150 | EApp (e1, e2) => getApp (e1, e2 :: args)
246 | _ => (ErrorMsg.errorAt loc "Mixed client/server code doesn't use a named function for server part"; 151 | _ => (ErrorMsg.errorAt loc "Mixed client/server code doesn't use a named function for server part";
247 Print.prefaces "Bad" [("e", CorePrint.p_exp CoreEnv.empty (e, ErrorMsg.dummySpan))]; 152 Print.prefaces "Bad" [("e", CorePrint.p_exp CoreEnv.empty (e, ErrorMsg.dummySpan))];
248 (0, [])) 153 (0, []))
249 in 154 end
250 case (serverSide (#cpsed_range st) trans1, clientSide (#cpsed_range st) trans1, 155
251 serverSide (#cpsed_range st) trans2, clientSide (#cpsed_range st) trans2) of 156 fun newRpc (trans1, trans2, st : state) =
252 (true, false, _, true) => 157 let
253 let 158 val loc = #2 trans1
254 val (n, args) = getApp (trans1, []) 159
255 160 val (n, args) = getApp (trans1, [])
256 val (exported, export_decls) = 161
257 if IS.member (#exported st, n) then 162 val (exported, export_decls) =
258 (#exported st, #export_decls st) 163 if IS.member (#exported st, n) then
259 else 164 (#exported st, #export_decls st)
260 (IS.add (#exported st, n), 165 else
261 (DExport (Rpc, n), loc) :: #export_decls st) 166 (IS.add (#exported st, n),
262 167 (DExport (Rpc, n), loc) :: #export_decls st)
263 val st = {cpsed = #cpsed st, 168
264 cpsed_range = #cpsed_range st, 169 val st = {cpsed = #cpsed st,
265 cps_decls = #cps_decls st, 170 cpsed_range = #cpsed_range st,
266 171 cps_decls = #cps_decls st,
267 exported = exported, 172
268 export_decls = export_decls, 173 exported = exported,
269 174 export_decls = export_decls,
270 maxName = #maxName st} 175
271 176 maxName = #maxName st}
272 val ran = 177
273 case IM.find (tfuncs, n) of 178 val ran =
274 NONE => (Print.prefaces "BAD" [("e", CorePrint.p_exp CoreEnv.empty (e, loc))]; 179 case IM.find (tfuncs, n) of
275 raise Fail ("Rpcify: Undetected transaction function " ^ Int.toString n)) 180 NONE => (Print.prefaces "BAD" [("e", CorePrint.p_exp CoreEnv.empty (e, loc))];
276 | SOME (_, _, ran, _) => ran 181 raise Fail ("Rpcify: Undetected transaction function " ^ Int.toString n))
277 182 | SOME (_, _, ran, _) => ran
278 val e' = EServerCall (n, args, trans2, ran) 183
279 in 184 val e' = EServerCall (n, args, trans2, ran)
280 (EServerCall (n, args, trans2, ran), st) 185 in
281 end 186 (e', st)
282 | (true, true, _, _) => 187 end
283 let 188 in
284 val (n, args) = getApp (trans1, []) 189 case e of
285 190 EApp (
286 fun makeCall n' = 191 (EApp
287 let 192 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _),
288 val e = (ENamed n', loc) 193 (EFfi ("Basis", "transaction_monad"), _)), _),
289 val e = (EApp (e, trans2), loc) 194 (ECase (ed, pes, {disc, ...}), _)), _),
290 in 195 trans2) =>
291 #1 (foldl (fn (arg, e) => (EApp (e, arg), loc)) e args) 196 let
292 end 197 val e' = (EFfi ("Basis", "bind"), loc)
293 in 198 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
294 case IM.find (#cpsed_range st, n) of 199 val e' = (ECApp (e', t1), loc)
295 SOME kdom => 200 val e' = (ECApp (e', t2), loc)
296 (case args of 201 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
297 [] => raise Fail "Rpcify: cps'd function lacks first argument" 202
298 | ke :: args => 203 val (pes, st) = ListUtil.foldlMap (fn ((p, e), st) =>
204 let
205 val e' = (EApp (e', e), loc)
206 val e' = (EApp (e',
207 multiLiftExpInExp (E.patBindsN p)
208 trans2), loc)
209 val (e', st) = doExp (e', st)
210 in
211 ((p, e'), st)
212 end) st pes
213 in
214 (ECase (ed, pes, {disc = disc,
215 result = (CApp ((CFfi ("Basis", "transaction"), loc), t2), loc)}),
216 st)
217 end
218
219 | EApp (
220 (EApp
221 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _),
222 (EFfi ("Basis", "transaction_monad"), _)), _),
223 (EServerCall (n, es, ke, t), _)), _),
224 trans2) =>
225 let
226 val e' = (EFfi ("Basis", "bind"), loc)
227 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
228 val e' = (ECApp (e', t), loc)
229 val e' = (ECApp (e', t2), loc)
230 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
231 val e' = (EApp (e', (EApp (E.liftExpInExp 0 ke, (ERel 0, loc)), loc)), loc)
232 val e' = (EApp (e', E.liftExpInExp 0 trans2), loc)
233 val e' = (EAbs ("x", t, t2, e'), loc)
234 val e' = (EServerCall (n, es, e', t), loc)
235 val (e', st) = doExp (e', st)
236 in
237 (#1 e', st)
238 end
239
240 | EApp (
241 (EApp
242 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), _), _), t3), _),
243 (EFfi ("Basis", "transaction_monad"), _)), _),
244 (EApp ((EApp
245 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), _), _), _), t1), _), t2), _),
246 (EFfi ("Basis", "transaction_monad"), _)), _),
247 trans1), _), trans2), _)), _),
248 trans3) =>
249 let
250 val e'' = (EFfi ("Basis", "bind"), loc)
251 val e'' = (ECApp (e'', (CFfi ("Basis", "transaction"), loc)), loc)
252 val e'' = (ECApp (e'', t2), loc)
253 val e'' = (ECApp (e'', t3), loc)
254 val e'' = (EApp (e'', (EFfi ("Basis", "transaction_monad"), loc)), loc)
255 val e'' = (EApp (e'', (EApp (E.liftExpInExp 0 trans2, (ERel 0, loc)), loc)), loc)
256 val e'' = (EApp (e'', E.liftExpInExp 0 trans3), loc)
257 val e'' = (EAbs ("x", t1, (CApp ((CFfi ("Basis", "transaction"), loc), t3), loc), e''), loc)
258
259 val e' = (EFfi ("Basis", "bind"), loc)
260 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
261 val e' = (ECApp (e', t1), loc)
262 val e' = (ECApp (e', t3), loc)
263 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
264 val e' = (EApp (e', trans1), loc)
265 val e' = (EApp (e', e''), loc)
266 val (e', st) = doExp (e', st)
267 in
268 (#1 e', st)
269 end
270
271 | EApp (
272 (EApp
273 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), _), _), _), _), _), _), _),
274 (EFfi ("Basis", "transaction_monad"), _)), _),
275 _), loc),
276 (EAbs (_, _, _, (EWrite _, _)), _)) => (e, st)
277
278 | EApp (
279 (EApp
280 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), _), _), _), t1), _), t2), _),
281 (EFfi ("Basis", "transaction_monad"), _)), _),
282 trans1), loc),
283 trans2) =>
284 (case (serverSide (#cpsed_range st) trans1, clientSide (#cpsed_range st) trans1,
285 serverSide (#cpsed_range st) trans2, clientSide (#cpsed_range st) trans2) of
286 (true, false, _, true) => newRpc (trans1, trans2, st)
287 | (true, true, _, _) =>
288 let
289 val (n, args) = getApp (trans1, [])
290
291 fun makeCall n' =
292 let
293 val e = (ENamed n', loc)
294 val e = (EApp (e, trans2), loc)
295 in
296 #1 (foldl (fn (arg, e) => (EApp (e, arg), loc)) e args)
297 end
298 in
299 case IM.find (#cpsed_range st, n) of
300 SOME kdom =>
301 (case args of
302 [] => raise Fail "Rpcify: cps'd function lacks first argument"
303 | ke :: args =>
304 let
305 val ke' = (EFfi ("Basis", "bind"), loc)
306 val ke' = (ECApp (ke', (CFfi ("Basis", "transaction"), loc)), loc)
307 val ke' = (ECApp (ke', kdom), loc)
308 val ke' = (ECApp (ke', t2), loc)
309 val ke' = (EApp (ke', (EFfi ("Basis", "transaction_monad"), loc)), loc)
310 val ke' = (EApp (ke', (EApp (E.liftExpInExp 0 ke, (ERel 0, loc)), loc)), loc)
311 val ke' = (EApp (ke', E.liftExpInExp 0 trans2), loc)
312 val ke' = (EAbs ("x", kdom,
313 (CApp ((CFfi ("Basis", "transaction"), loc), t2), loc),
314 ke'), loc)
315
316 val e' = (ENamed n, loc)
317 val e' = (EApp (e', ke'), loc)
318 val e' = foldl (fn (arg, e') => (EApp (e', arg), loc)) e' args
319 val (e', st) = doExp (e', st)
320 in
321 (#1 e', st)
322 end)
323 | NONE =>
324 case IM.find (#cpsed st, n) of
325 SOME n' => (makeCall n', st)
326 | NONE =>
299 let 327 let
300 val ke' = (EFfi ("Basis", "bind"), loc) 328 val (name, fargs, ran, e) =
301 val ke' = (ECApp (ke', (CFfi ("Basis", "transaction"), loc)), loc) 329 case IM.find (tfuncs, n) of
302 val ke' = (ECApp (ke', kdom), loc) 330 NONE => (Print.prefaces "BAD" [("e",
303 val ke' = (ECApp (ke', t2), loc) 331 CorePrint.p_exp CoreEnv.empty (e, loc))];
304 val ke' = (EApp (ke', (EFfi ("Basis", "transaction_monad"), loc)), loc) 332 raise Fail "Rpcify: Undetected transaction function [2]")
305 val ke' = (EApp (ke', (EApp (E.liftExpInExp 0 ke, (ERel 0, loc)), loc)), loc) 333 | SOME x => x
306 val ke' = (EApp (ke', E.liftExpInExp 0 trans2), loc) 334
307 val ke' = (EAbs ("x", kdom, 335 val n' = #maxName st
308 (CApp ((CFfi ("Basis", "transaction"), loc), t2), loc), 336
309 ke'), loc) 337 val st = {cpsed = IM.insert (#cpsed st, n, n'),
310 338 cpsed_range = IM.insert (#cpsed_range st, n', ran),
311 val e' = (ENamed n, loc) 339 cps_decls = #cps_decls st,
312 val e' = (EApp (e', ke'), loc) 340 exported = #exported st,
313 val e' = foldl (fn (arg, e') => (EApp (e', arg), loc)) e' args 341 export_decls = #export_decls st,
314 val (e', st) = doExp (e', st) 342 maxName = n' + 1}
343
344 val unit = (TRecord (CRecord ((KType, loc), []), loc), loc)
345 val body = (EFfi ("Basis", "bind"), loc)
346 val body = (ECApp (body, (CFfi ("Basis", "transaction"), loc)), loc)
347 val body = (ECApp (body, t1), loc)
348 val body = (ECApp (body, unit), loc)
349 val body = (EApp (body, (EFfi ("Basis", "transaction_monad"), loc)), loc)
350 val body = (EApp (body, e), loc)
351 val body = (EApp (body, (ERel (length args), loc)), loc)
352 val bt = (CApp ((CFfi ("Basis", "transaction"), loc), unit), loc)
353 val (body, bt) = foldr (fn ((x, t), (body, bt)) =>
354 ((EAbs (x, t, bt, body), loc),
355 (TFun (t, bt), loc)))
356 (body, bt) fargs
357 val kt = (TFun (ran, (CApp ((CFfi ("Basis", "transaction"), loc),
358 unit),
359 loc)), loc)
360 val body = (EAbs ("k", kt, bt, body), loc)
361 val bt = (TFun (kt, bt), loc)
362
363 val (body, st) = doExp (body, st)
364
365 val vi = (name ^ "_cps",
366 n',
367 bt,
368 body,
369 "")
370
371 val st = {cpsed = #cpsed st,
372 cpsed_range = #cpsed_range st,
373 cps_decls = vi :: #cps_decls st,
374 exported = #exported st,
375 export_decls = #export_decls st,
376 maxName = #maxName st}
315 in 377 in
316 (#1 e', st) 378 (makeCall n', st)
317 end) 379 end
318 | NONE => 380 end
319 case IM.find (#cpsed st, n) of 381 | _ => (e, st))
320 SOME n' => (makeCall n', st) 382
321 | NONE => 383 | ERecord xes =>
322 let 384 let
323 val (name, fargs, ran, e) = 385 val loc = case xes of
324 case IM.find (tfuncs, n) of 386 [] => ErrorMsg.dummySpan
325 NONE => (Print.prefaces "BAD" [("e", 387 | (_, (_, loc), _) :: _ => loc
326 CorePrint.p_exp CoreEnv.empty (e, loc))]; 388
327 raise Fail "Rpcify: Undetected transaction function [2]") 389 fun candidate (x, e) =
328 | SOME x => x 390 String.isPrefix "On" x
329 391 andalso serverSide (#cpsed_range st) e
330 val n' = #maxName st 392 andalso not (clientSide (#cpsed_range st) e)
331 393 in
332 val st = {cpsed = IM.insert (#cpsed st, n, n'), 394 if List.exists (fn ((CName x, _), e, _) => candidate (x, e)
333 cpsed_range = IM.insert (#cpsed_range st, n', ran), 395 | _ => false) xes then
334 cps_decls = #cps_decls st, 396 let
335 exported = #exported st, 397 val unit = (TRecord (CRecord ((KType, loc), []), loc), loc)
336 export_decls = #export_decls st, 398
337 maxName = n' + 1} 399 val k = (EFfi ("Basis", "return"), loc)
338 400 val k = (ECApp (k, (CFfi ("Basis", "transaction"), loc)), loc)
339 val unit = (TRecord (CRecord ((KType, loc), []), loc), loc) 401 val k = (ECApp (k, unit), loc)
340 val body = (EFfi ("Basis", "bind"), loc) 402 val k = (EApp (k, (EFfi ("Basis", "transaction_monad"), loc)), loc)
341 val body = (ECApp (body, (CFfi ("Basis", "transaction"), loc)), loc) 403 val k = (EApp (k, (ERecord [], loc)), loc)
342 val body = (ECApp (body, t1), loc) 404 val k = (EAbs ("_", unit, unit, k), loc)
343 val body = (ECApp (body, unit), loc) 405
344 val body = (EApp (body, (EFfi ("Basis", "transaction_monad"), loc)), loc) 406 val (xes, st) = ListUtil.foldlMap
345 val body = (EApp (body, e), loc) 407 (fn (y as (nm as (CName x, _), e, t), st) =>
346 val body = (EApp (body, (ERel (length args), loc)), loc) 408 if candidate (x, e) then
347 val bt = (CApp ((CFfi ("Basis", "transaction"), loc), unit), loc) 409 let
348 val (body, bt) = foldr (fn ((x, t), (body, bt)) => 410 val (n, args) = getApp (e, [])
349 ((EAbs (x, t, bt, body), loc), 411
350 (TFun (t, bt), loc))) 412 val (e, st) = newRpc (e, k, st)
351 (body, bt) fargs 413 in
352 val kt = (TFun (ran, (CApp ((CFfi ("Basis", "transaction"), loc), 414 ((nm, (e, loc), t), st)
353 unit), 415 end
354 loc)), loc) 416 else
355 val body = (EAbs ("k", kt, bt, body), loc) 417 (y, st)
356 val bt = (TFun (kt, bt), loc) 418 | y => y)
357 419 st xes
358 val (body, st) = doExp (body, st) 420 in
359 421 (ERecord xes, st)
360 val vi = (name ^ "_cps", 422 end
361 n', 423 else
362 bt, 424 (e, st)
363 body, 425 end
364 "") 426
365 427 | _ => (e, st)
366 val st = {cpsed = #cpsed st, 428 end
367 cpsed_range = #cpsed_range st,
368 cps_decls = vi :: #cps_decls st,
369 exported = #exported st,
370 export_decls = #export_decls st,
371 maxName = #maxName st}
372 in
373 (makeCall n', st)
374 end
375 end
376 | _ => (e, st)
377 end
378 | _ => (e, st)
379 429
380 and doExp (e, st) = U.Exp.foldMap {kind = fn x => x, 430 and doExp (e, st) = U.Exp.foldMap {kind = fn x => x,
381 con = fn x => x, 431 con = fn x => x,
382 exp = exp} st (ReduceLocal.reduceExp e) 432 exp = exp} st (ReduceLocal.reduceExp e)
383 433