annotate src/rpcify.sml @ 646:fb2a0e76dcef

ListEdit demo, minus prose
author Adam Chlipala <adamc@hcoop.net>
date Tue, 10 Mar 2009 12:44:40 -0400
parents 4a125bbc602d
children 96ebc6bdb5a0
rev   line source
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@607 35 structure IS = IntBinarySet
adamc@607 36 structure IM = IntBinaryMap
adamc@607 37
adamc@607 38 structure SS = BinarySetFn(struct
adamc@607 39 type ord_key = string
adamc@607 40 val compare = String.compare
adamc@607 41 end)
adamc@607 42
adamc@642 43 fun multiLiftExpInExp n e =
adamc@642 44 if n = 0 then
adamc@642 45 e
adamc@642 46 else
adamc@642 47 multiLiftExpInExp (n - 1) (E.liftExpInExp 0 e)
adamc@642 48
adamc@607 49 val ssBasis = SS.addList (SS.empty,
adamc@607 50 ["requestHeader",
adamc@607 51 "query",
adamc@607 52 "dml",
adamc@607 53 "nextval"])
adamc@607 54
adamc@607 55 val csBasis = SS.addList (SS.empty,
adamc@607 56 ["source",
adamc@607 57 "get",
adamc@607 58 "set",
adamc@607 59 "alert"])
adamc@607 60
adamc@607 61 type state = {
adamc@608 62 cpsed : int IM.map,
adamc@642 63 cpsed_range : con IM.map,
adamc@608 64 cps_decls : (string * int * con * exp * string) list,
adamc@608 65
adamc@608 66 exported : IS.set,
adamc@642 67 export_decls : decl list,
adamc@642 68
adamc@642 69 maxName : int
adamc@607 70 }
adamc@607 71
adamc@607 72 fun frob file =
adamc@607 73 let
adamc@607 74 fun sideish (basis, ssids) =
adamc@607 75 U.Exp.exists {kind = fn _ => false,
adamc@607 76 con = fn _ => false,
adamc@607 77 exp = fn ENamed n => IS.member (ssids, n)
adamc@607 78 | EFfi ("Basis", x) => SS.member (basis, x)
adamc@607 79 | EFfiApp ("Basis", x, _) => SS.member (basis, x)
adamc@607 80 | _ => false}
adamc@607 81
adamc@607 82 fun whichIds basis =
adamc@607 83 let
adamc@607 84 fun decl ((d, _), ssids) =
adamc@607 85 let
adamc@607 86 val impure = sideish (basis, ssids)
adamc@607 87 in
adamc@607 88 case d of
adamc@607 89 DVal (_, n, _, e, _) => if impure e then
adamc@607 90 IS.add (ssids, n)
adamc@607 91 else
adamc@607 92 ssids
adamc@607 93 | DValRec xes => if List.exists (fn (_, _, _, e, _) => impure e) xes then
adamc@607 94 foldl (fn ((_, n, _, _, _), ssids) => IS.add (ssids, n))
adamc@607 95 ssids xes
adamc@607 96 else
adamc@607 97 ssids
adamc@607 98 | _ => ssids
adamc@607 99 end
adamc@607 100 in
adamc@607 101 foldl decl IS.empty file
adamc@607 102 end
adamc@607 103
adamc@607 104 val ssids = whichIds ssBasis
adamc@607 105 val csids = whichIds csBasis
adamc@607 106
adamc@642 107 fun sideish' (basis, ids) extra =
adamc@642 108 sideish (basis, IM.foldli (fn (id, _, ids) => IS.add (ids, id)) ids extra)
adamc@642 109
adamc@642 110 val serverSide = sideish' (ssBasis, ssids)
adamc@642 111 val clientSide = sideish' (csBasis, csids)
adamc@607 112
adamc@609 113 val tfuncs = foldl
adamc@609 114 (fn ((d, _), tfuncs) =>
adamc@609 115 let
adamc@642 116 fun doOne ((x, n, t, e, _), tfuncs) =
adamc@609 117 let
adamc@642 118 val loc = #2 e
adamc@642 119
adamc@642 120 fun crawl (t, e, args) =
adamc@642 121 case (#1 t, #1 e) of
adamc@642 122 (CApp (_, ran), _) =>
adamc@642 123 SOME (x, rev args, ran, e)
adamc@642 124 | (TFun (arg, rest), EAbs (x, _, _, e)) =>
adamc@642 125 crawl (rest, e, (x, arg) :: args)
adamc@642 126 | (TFun (arg, rest), _) =>
adamc@642 127 crawl (rest, (EApp (e, (ERel (length args), loc)), loc), ("x", arg) :: args)
adamc@609 128 | _ => NONE
adamc@609 129 in
adamc@642 130 case crawl (t, e, []) of
adamc@609 131 NONE => tfuncs
adamc@609 132 | SOME sg => IM.insert (tfuncs, n, sg)
adamc@609 133 end
adamc@609 134 in
adamc@609 135 case d of
adamc@609 136 DVal vi => doOne (vi, tfuncs)
adamc@609 137 | DValRec vis => foldl doOne tfuncs vis
adamc@609 138 | _ => tfuncs
adamc@609 139 end)
adamc@609 140 IM.empty file
adamc@609 141
adamc@607 142 fun exp (e, st) =
adamc@607 143 case e of
adamc@607 144 EApp (
adamc@607 145 (EApp
adamc@607 146 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _),
adamc@607 147 (EFfi ("Basis", "transaction_monad"), _)), _),
adamc@642 148 (ECase (ed, pes, {disc, ...}), _)), _),
adamc@607 149 trans2) =>
adamc@642 150 let
adamc@642 151 val e' = (EFfi ("Basis", "bind"), loc)
adamc@642 152 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
adamc@642 153 val e' = (ECApp (e', t1), loc)
adamc@642 154 val e' = (ECApp (e', t2), loc)
adamc@642 155 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
adamc@607 156
adamc@642 157 val (pes, st) = ListUtil.foldlMap (fn ((p, e), st) =>
adamc@642 158 let
adamc@642 159 val e' = (EApp (e', e), loc)
adamc@642 160 val e' = (EApp (e',
adamc@642 161 multiLiftExpInExp (E.patBindsN p)
adamc@642 162 trans2), loc)
adamc@642 163 val (e', st) = doExp (e', st)
adamc@642 164 in
adamc@642 165 ((p, e'), st)
adamc@642 166 end) st pes
adamc@642 167 in
adamc@642 168 (ECase (ed, pes, {disc = disc,
adamc@642 169 result = (CApp ((CFfi ("Basis", "transaction"), loc), t2), loc)}),
adamc@642 170 st)
adamc@642 171 end
adamc@608 172
adamc@642 173 | EApp (
adamc@642 174 (EApp
adamc@642 175 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _),
adamc@642 176 (EFfi ("Basis", "transaction_monad"), _)), _),
adamc@642 177 (EServerCall (n, es, ke, t), _)), _),
adamc@642 178 trans2) =>
adamc@642 179 let
adamc@642 180 val e' = (EFfi ("Basis", "bind"), loc)
adamc@642 181 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
adamc@642 182 val e' = (ECApp (e', t), loc)
adamc@642 183 val e' = (ECApp (e', t2), loc)
adamc@642 184 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
adamc@642 185 val e' = (EApp (e', (EApp (E.liftExpInExp 0 ke, (ERel 0, loc)), loc)), loc)
adamc@642 186 val e' = (EApp (e', E.liftExpInExp 0 trans2), loc)
adamc@642 187 val e' = (EAbs ("x", t, t2, e'), loc)
adamc@642 188 val e' = (EServerCall (n, es, e', t), loc)
adamc@642 189 val (e', st) = doExp (e', st)
adamc@642 190 in
adamc@642 191 (#1 e', st)
adamc@642 192 end
adamc@608 193
adamc@642 194 | EApp (
adamc@642 195 (EApp
adamc@642 196 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), _), _), t3), _),
adamc@642 197 (EFfi ("Basis", "transaction_monad"), _)), _),
adamc@642 198 (EApp ((EApp
adamc@642 199 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), _), _), _), t1), _), t2), _),
adamc@642 200 (EFfi ("Basis", "transaction_monad"), _)), _),
adamc@642 201 trans1), _), trans2), _)), _),
adamc@642 202 trans3) =>
adamc@642 203 let
adamc@642 204 val e'' = (EFfi ("Basis", "bind"), loc)
adamc@642 205 val e'' = (ECApp (e'', (CFfi ("Basis", "transaction"), loc)), loc)
adamc@642 206 val e'' = (ECApp (e'', t2), loc)
adamc@642 207 val e'' = (ECApp (e'', t3), loc)
adamc@642 208 val e'' = (EApp (e'', (EFfi ("Basis", "transaction_monad"), loc)), loc)
adamc@642 209 val e'' = (EApp (e'', (EApp (E.liftExpInExp 0 trans2, (ERel 0, loc)), loc)), loc)
adamc@642 210 val e'' = (EApp (e'', E.liftExpInExp 0 trans3), loc)
adamc@642 211 val e'' = (EAbs ("x", t1, (CApp ((CFfi ("Basis", "transaction"), loc), t3), loc), e''), loc)
adamc@608 212
adamc@642 213 val e' = (EFfi ("Basis", "bind"), loc)
adamc@642 214 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
adamc@642 215 val e' = (ECApp (e', t1), loc)
adamc@642 216 val e' = (ECApp (e', t3), loc)
adamc@642 217 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
adamc@642 218 val e' = (EApp (e', trans1), loc)
adamc@642 219 val e' = (EApp (e', e''), loc)
adamc@642 220 val (e', st) = doExp (e', st)
adamc@642 221 in
adamc@642 222 (#1 e', st)
adamc@642 223 end
adamc@609 224
adamc@642 225 | EApp (
adamc@642 226 (EApp
adamc@642 227 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), _), _), _), _), _), _), _),
adamc@642 228 (EFfi ("Basis", "transaction_monad"), _)), _),
adamc@642 229 _), loc),
adamc@642 230 (EAbs (_, _, _, (EWrite _, _)), _)) => (e, st)
adamc@642 231
adamc@642 232 | EApp (
adamc@642 233 (EApp
adamc@642 234 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), _), _), _), t1), _), t2), _),
adamc@642 235 (EFfi ("Basis", "transaction_monad"), _)), _),
adamc@642 236 trans1), loc),
adamc@642 237 trans2) =>
adamc@642 238 let
adamc@642 239 (*val () = Print.prefaces "Default"
adamc@642 240 [("e", CorePrint.p_exp CoreEnv.empty (e, ErrorMsg.dummySpan))]*)
adamc@642 241
adamc@642 242 fun getApp (e', args) =
adamc@642 243 case #1 e' of
adamc@642 244 ENamed n => (n, args)
adamc@642 245 | EApp (e1, e2) => getApp (e1, e2 :: args)
adamc@642 246 | _ => (ErrorMsg.errorAt loc "Mixed client/server code doesn't use a named function for server part";
adamc@642 247 Print.prefaces "Bad" [("e", CorePrint.p_exp CoreEnv.empty (e, ErrorMsg.dummySpan))];
adamc@642 248 (0, []))
adamc@642 249 in
adamc@642 250 case (serverSide (#cpsed_range st) trans1, clientSide (#cpsed_range st) trans1,
adamc@642 251 serverSide (#cpsed_range st) trans2, clientSide (#cpsed_range st) trans2) of
adamc@642 252 (true, false, _, true) =>
adamc@642 253 let
adamc@642 254 val (n, args) = getApp (trans1, [])
adamc@642 255
adamc@642 256 val (exported, export_decls) =
adamc@642 257 if IS.member (#exported st, n) then
adamc@642 258 (#exported st, #export_decls st)
adamc@642 259 else
adamc@642 260 (IS.add (#exported st, n),
adamc@642 261 (DExport (Rpc, n), loc) :: #export_decls st)
adamc@642 262
adamc@642 263 val st = {cpsed = #cpsed st,
adamc@642 264 cpsed_range = #cpsed_range st,
adamc@642 265 cps_decls = #cps_decls st,
adamc@642 266
adamc@642 267 exported = exported,
adamc@642 268 export_decls = export_decls,
adamc@642 269
adamc@642 270 maxName = #maxName st}
adamc@642 271
adamc@642 272 val ran =
adamc@642 273 case IM.find (tfuncs, n) of
adamc@642 274 NONE => (Print.prefaces "BAD" [("e", CorePrint.p_exp CoreEnv.empty (e, loc))];
adamc@642 275 raise Fail ("Rpcify: Undetected transaction function " ^ Int.toString n))
adamc@642 276 | SOME (_, _, ran, _) => ran
adamc@642 277
adamc@642 278 val e' = EServerCall (n, args, trans2, ran)
adamc@642 279 in
adamc@642 280 (EServerCall (n, args, trans2, ran), st)
adamc@642 281 end
adamc@642 282 | (true, true, _, _) =>
adamc@642 283 let
adamc@642 284 val (n, args) = getApp (trans1, [])
adamc@642 285
adamc@642 286 fun makeCall n' =
adamc@642 287 let
adamc@642 288 val e = (ENamed n', loc)
adamc@642 289 val e = (EApp (e, trans2), loc)
adamc@642 290 in
adamc@642 291 #1 (foldl (fn (arg, e) => (EApp (e, arg), loc)) e args)
adamc@642 292 end
adamc@642 293 in
adamc@642 294 case IM.find (#cpsed_range st, n) of
adamc@642 295 SOME kdom =>
adamc@642 296 (case args of
adamc@642 297 [] => raise Fail "Rpcify: cps'd function lacks first argument"
adamc@642 298 | ke :: args =>
adamc@642 299 let
adamc@642 300 val ke' = (EFfi ("Basis", "bind"), loc)
adamc@642 301 val ke' = (ECApp (ke', (CFfi ("Basis", "transaction"), loc)), loc)
adamc@642 302 val ke' = (ECApp (ke', kdom), loc)
adamc@642 303 val ke' = (ECApp (ke', t2), loc)
adamc@642 304 val ke' = (EApp (ke', (EFfi ("Basis", "transaction_monad"), loc)), loc)
adamc@642 305 val ke' = (EApp (ke', (EApp (E.liftExpInExp 0 ke, (ERel 0, loc)), loc)), loc)
adamc@642 306 val ke' = (EApp (ke', E.liftExpInExp 0 trans2), loc)
adamc@642 307 val ke' = (EAbs ("x", kdom,
adamc@642 308 (CApp ((CFfi ("Basis", "transaction"), loc), t2), loc),
adamc@642 309 ke'), loc)
adamc@642 310
adamc@642 311 val e' = (ENamed n, loc)
adamc@642 312 val e' = (EApp (e', ke'), loc)
adamc@642 313 val e' = foldl (fn (arg, e') => (EApp (e', arg), loc)) e' args
adamc@642 314 val (e', st) = doExp (e', st)
adamc@642 315 in
adamc@642 316 (#1 e', st)
adamc@642 317 end)
adamc@642 318 | NONE =>
adamc@642 319 case IM.find (#cpsed st, n) of
adamc@642 320 SOME n' => (makeCall n', st)
adamc@642 321 | NONE =>
adamc@642 322 let
adamc@642 323 val (name, fargs, ran, e) =
adamc@642 324 case IM.find (tfuncs, n) of
adamc@642 325 NONE => (Print.prefaces "BAD" [("e",
adamc@642 326 CorePrint.p_exp CoreEnv.empty (e, loc))];
adamc@642 327 raise Fail "Rpcify: Undetected transaction function [2]")
adamc@642 328 | SOME x => x
adamc@642 329
adamc@642 330 val n' = #maxName st
adamc@642 331
adamc@642 332 val st = {cpsed = IM.insert (#cpsed st, n, n'),
adamc@642 333 cpsed_range = IM.insert (#cpsed_range st, n', ran),
adamc@642 334 cps_decls = #cps_decls st,
adamc@642 335 exported = #exported st,
adamc@642 336 export_decls = #export_decls st,
adamc@642 337 maxName = n' + 1}
adamc@642 338
adamc@642 339 val unit = (TRecord (CRecord ((KType, loc), []), loc), loc)
adamc@642 340 val body = (EFfi ("Basis", "bind"), loc)
adamc@642 341 val body = (ECApp (body, (CFfi ("Basis", "transaction"), loc)), loc)
adamc@642 342 val body = (ECApp (body, t1), loc)
adamc@642 343 val body = (ECApp (body, unit), loc)
adamc@642 344 val body = (EApp (body, (EFfi ("Basis", "transaction_monad"), loc)), loc)
adamc@642 345 val body = (EApp (body, e), loc)
adamc@642 346 val body = (EApp (body, (ERel (length args), loc)), loc)
adamc@642 347 val bt = (CApp ((CFfi ("Basis", "transaction"), loc), unit), loc)
adamc@642 348 val (body, bt) = foldr (fn ((x, t), (body, bt)) =>
adamc@642 349 ((EAbs (x, t, bt, body), loc),
adamc@642 350 (TFun (t, bt), loc)))
adamc@642 351 (body, bt) fargs
adamc@642 352 val kt = (TFun (ran, (CApp ((CFfi ("Basis", "transaction"), loc),
adamc@642 353 unit),
adamc@642 354 loc)), loc)
adamc@642 355 val body = (EAbs ("k", kt, bt, body), loc)
adamc@642 356 val bt = (TFun (kt, bt), loc)
adamc@642 357
adamc@642 358 val (body, st) = doExp (body, st)
adamc@642 359
adamc@642 360 val vi = (name ^ "_cps",
adamc@642 361 n',
adamc@642 362 bt,
adamc@642 363 body,
adamc@642 364 "")
adamc@642 365
adamc@642 366 val st = {cpsed = #cpsed st,
adamc@642 367 cpsed_range = #cpsed_range st,
adamc@642 368 cps_decls = vi :: #cps_decls st,
adamc@642 369 exported = #exported st,
adamc@642 370 export_decls = #export_decls st,
adamc@642 371 maxName = #maxName st}
adamc@642 372 in
adamc@642 373 (makeCall n', st)
adamc@642 374 end
adamc@642 375 end
adamc@642 376 | _ => (e, st)
adamc@642 377 end
adamc@607 378 | _ => (e, st)
adamc@607 379
adamc@642 380 and doExp (e, st) = U.Exp.foldMap {kind = fn x => x,
adamc@642 381 con = fn x => x,
adamc@642 382 exp = exp} st (ReduceLocal.reduceExp e)
adamc@642 383
adamc@607 384 fun decl (d, st : state) =
adamc@607 385 let
adamc@607 386 val (d, st) = U.Decl.foldMap {kind = fn x => x,
adamc@607 387 con = fn x => x,
adamc@607 388 exp = exp,
adamc@607 389 decl = fn x => x}
adamc@607 390 st d
adamc@607 391 in
adamc@608 392 (List.revAppend (case #cps_decls st of
adamc@608 393 [] => [d]
adamc@608 394 | ds =>
adamc@608 395 case d of
adamc@608 396 (DValRec vis, loc) => [(DValRec (ds @ vis), loc)]
adamc@608 397 | (_, loc) => [d, (DValRec ds, loc)],
adamc@608 398 #export_decls st),
adamc@608 399 {cpsed = #cpsed st,
adamc@642 400 cpsed_range = #cpsed_range st,
adamc@608 401 cps_decls = [],
adamc@608 402
adamc@608 403 exported = #exported st,
adamc@642 404 export_decls = [],
adamc@642 405
adamc@642 406 maxName = #maxName st})
adamc@607 407 end
adamc@607 408
adamc@607 409 val (file, _) = ListUtil.foldlMapConcat decl
adamc@608 410 {cpsed = IM.empty,
adamc@642 411 cpsed_range = IM.empty,
adamc@608 412 cps_decls = [],
adamc@608 413
adamc@608 414 exported = IS.empty,
adamc@642 415 export_decls = [],
adamc@642 416
adamc@642 417 maxName = U.File.maxName file + 1}
adamc@607 418 file
adamc@607 419 in
adamc@607 420 file
adamc@607 421 end
adamc@607 422
adamc@607 423 end