Mercurial > urweb

annotate src/rpcify.sml @ 628:12b73f3c108e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Switch to TDisjoint from CDisjoint; still need to implement obligation generation at EDisjoint uses
author Adam Chlipala <adamc@hcoop.net>
date Tue, 24 Feb 2009 12:01:24 -0500
parents c5991cdb0c4b
children 4a125bbc602d
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@607 43 val ssBasis = SS.addList (SS.empty,
adamc@607 44 ["requestHeader",
adamc@607 45 "query",
adamc@607 46 "dml",
adamc@607 47 "nextval"])
adamc@607 48
adamc@607 49 val csBasis = SS.addList (SS.empty,
adamc@607 50 ["source",
adamc@607 51 "get",
adamc@607 52 "set",
adamc@607 53 "alert"])
adamc@607 54
adamc@607 55 type state = {
adamc@608 56 cpsed : int IM.map,
adamc@608 57 cps_decls : (string * int * con * exp * string) list,
adamc@608 58
adamc@608 59 exported : IS.set,
adamc@608 60 export_decls : decl list
adamc@607 61 }
adamc@607 62
adamc@607 63 fun frob file =
adamc@607 64 let
adamc@607 65 fun sideish (basis, ssids) =
adamc@607 66 U.Exp.exists {kind = fn _ => false,
adamc@607 67 con = fn _ => false,
adamc@607 68 exp = fn ENamed n => IS.member (ssids, n)
adamc@607 69 | EFfi ("Basis", x) => SS.member (basis, x)
adamc@607 70 | EFfiApp ("Basis", x, _) => SS.member (basis, x)
adamc@607 71 | _ => false}
adamc@607 72
adamc@607 73 fun whichIds basis =
adamc@607 74 let
adamc@607 75 fun decl ((d, _), ssids) =
adamc@607 76 let
adamc@607 77 val impure = sideish (basis, ssids)
adamc@607 78 in
adamc@607 79 case d of
adamc@607 80 DVal (_, n, _, e, _) => if impure e then
adamc@607 81 IS.add (ssids, n)
adamc@607 82 else
adamc@607 83 ssids
adamc@607 84 | DValRec xes => if List.exists (fn (_, _, _, e, _) => impure e) xes then
adamc@607 85 foldl (fn ((_, n, _, _, _), ssids) => IS.add (ssids, n))
adamc@607 86 ssids xes
adamc@607 87 else
adamc@607 88 ssids
adamc@607 89 | _ => ssids
adamc@607 90 end
adamc@607 91 in
adamc@607 92 foldl decl IS.empty file
adamc@607 93 end
adamc@607 94
adamc@607 95 val ssids = whichIds ssBasis
adamc@607 96 val csids = whichIds csBasis
adamc@607 97
adamc@607 98 val serverSide = sideish (ssBasis, ssids)
adamc@607 99 val clientSide = sideish (csBasis, csids)
adamc@607 100
adamc@609 101 val tfuncs = foldl
adamc@609 102 (fn ((d, _), tfuncs) =>
adamc@609 103 let
adamc@609 104 fun doOne ((_, n, t, _, _), tfuncs) =
adamc@609 105 let
adamc@613 106 fun crawl (t, args) =
adamc@613 107 case #1 t of
adamc@609 108 CApp ((CFfi ("Basis", "transaction"), _), ran) => SOME (rev args, ran)
adamc@609 109 | TFun (arg, rest) => crawl (rest, arg :: args)
adamc@609 110 | _ => NONE
adamc@609 111 in
adamc@609 112 case crawl (t, []) of
adamc@609 113 NONE => tfuncs
adamc@609 114 | SOME sg => IM.insert (tfuncs, n, sg)
adamc@609 115 end
adamc@609 116 in
adamc@609 117 case d of
adamc@609 118 DVal vi => doOne (vi, tfuncs)
adamc@609 119 | DValRec vis => foldl doOne tfuncs vis
adamc@609 120 | _ => tfuncs
adamc@609 121 end)
adamc@609 122 IM.empty file
adamc@609 123
adamc@607 124 fun exp (e, st) =
adamc@607 125 case e of
adamc@607 126 EApp (
adamc@607 127 (EApp
adamc@607 128 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _),
adamc@607 129 (EFfi ("Basis", "transaction_monad"), _)), _),
adamc@607 130 trans1), _),
adamc@607 131 trans2) =>
adamc@607 132 (case (serverSide trans1, clientSide trans1, serverSide trans2, clientSide trans2) of
adamc@613 133 (true, false, false, true) =>
adamc@607 134 let
adamc@607 135 fun getApp (e, args) =
adamc@607 136 case #1 e of
adamc@607 137 ENamed n => (n, args)
adamc@607 138 | EApp (e1, e2) => getApp (e1, e2 :: args)
adamc@607 139 | _ => (ErrorMsg.errorAt loc "Mixed client/server code doesn't use a named function for server part";
adamc@607 140 (0, []))
adamc@607 141
adamc@607 142 val (n, args) = getApp (trans1, [])
adamc@608 143
adamc@608 144 val (exported, export_decls) =
adamc@608 145 if IS.member (#exported st, n) then
adamc@608 146 (#exported st, #export_decls st)
adamc@608 147 else
adamc@608 148 (IS.add (#exported st, n),
adamc@608 149 (DExport (Rpc, n), loc) :: #export_decls st)
adamc@608 150
adamc@608 151 val st = {cpsed = #cpsed st,
adamc@608 152 cps_decls = #cps_decls st,
adamc@608 153
adamc@608 154 exported = exported,
adamc@608 155 export_decls = export_decls}
adamc@609 156
adamc@609 157 val ran =
adamc@609 158 case IM.find (tfuncs, n) of
adamc@613 159 NONE => (Print.prefaces "BAD" [("e", CorePrint.p_exp CoreEnv.empty (e, loc))];
adamc@613 160 raise Fail "Rpcify: Undetected transaction function")
adamc@609 161 | SOME (_, ran) => ran
adamc@607 162 in
adamc@609 163 (EServerCall (n, args, trans2, ran), st)
adamc@607 164 end
adamc@607 165 | _ => (e, st))
adamc@607 166 | _ => (e, st)
adamc@607 167
adamc@607 168 fun decl (d, st : state) =
adamc@607 169 let
adamc@607 170 val (d, st) = U.Decl.foldMap {kind = fn x => x,
adamc@607 171 con = fn x => x,
adamc@607 172 exp = exp,
adamc@607 173 decl = fn x => x}
adamc@607 174 st d
adamc@607 175 in
adamc@608 176 (List.revAppend (case #cps_decls st of
adamc@608 177 [] => [d]
adamc@608 178 | ds =>
adamc@608 179 case d of
adamc@608 180 (DValRec vis, loc) => [(DValRec (ds @ vis), loc)]
adamc@608 181 | (_, loc) => [d, (DValRec ds, loc)],
adamc@608 182 #export_decls st),
adamc@608 183 {cpsed = #cpsed st,
adamc@608 184 cps_decls = [],
adamc@608 185
adamc@608 186 exported = #exported st,
adamc@608 187 export_decls = []})
adamc@607 188 end
adamc@607 189
adamc@607 190 val (file, _) = ListUtil.foldlMapConcat decl
adamc@608 191 {cpsed = IM.empty,
adamc@608 192 cps_decls = [],
adamc@608 193
adamc@608 194 exported = IS.empty,
adamc@608 195 export_decls = []}
adamc@607 196 file
adamc@607 197 in
adamc@607 198 file
adamc@607 199 end
adamc@607 200
adamc@607 201 end