annotate src/rpcify.sml @ 2220:794017f378de

Merge.
author Ziv Scully <ziv@mit.edu>
date Mon, 24 Nov 2014 20:47:38 -0500
parents e15234fbb163
children
rev   line source
adam@1848 1 (* Copyright (c) 2009, 2012-2013, 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 type state = {
adamc@608 39 exported : IS.set,
adamc@957 40 export_decls : decl list
adamc@607 41 }
adamc@607 42
adamc@607 43 fun frob file =
adamc@607 44 let
adam@1848 45 val (rpcBaseIds, trpcBaseIds) =
adam@1848 46 foldl (fn ((d, _), (rpcIds, trpcIds)) =>
adam@1848 47 case d of
adam@1848 48 DVal (_, n, _, (EFfi ("Basis", "rpc"), _), _) =>
adam@1848 49 (IS.add (rpcIds, n), trpcIds)
adam@1848 50 | DVal (_, n, _, (EFfi ("Basis", "tryRpc"), _), _) =>
adam@1848 51 (rpcIds, IS.add (trpcIds, n))
adam@1848 52 | DVal (_, n, _, (ENamed n', _), _) =>
adam@1848 53 if IS.member (rpcIds, n') then
adam@1848 54 (IS.add (rpcIds, n), trpcIds)
adam@1848 55 else if IS.member (trpcIds, n') then
adam@1848 56 (rpcIds, IS.add (trpcIds, n))
adam@1848 57 else
adam@1848 58 (rpcIds, trpcIds)
adam@1848 59 | _ => (rpcIds, trpcIds))
adam@1848 60 (IS.empty, IS.empty) file
adamc@607 61
adamc@609 62 val tfuncs = foldl
adamc@609 63 (fn ((d, _), tfuncs) =>
adamc@609 64 let
adamc@642 65 fun doOne ((x, n, t, e, _), tfuncs) =
adamc@609 66 let
adamc@642 67 val loc = #2 e
adamc@642 68
adamc@642 69 fun crawl (t, e, args) =
adamc@642 70 case (#1 t, #1 e) of
adamc@642 71 (CApp (_, ran), _) =>
adamc@642 72 SOME (x, rev args, ran, e)
adamc@642 73 | (TFun (arg, rest), EAbs (x, _, _, e)) =>
adamc@642 74 crawl (rest, e, (x, arg) :: args)
adamc@642 75 | (TFun (arg, rest), _) =>
adamc@642 76 crawl (rest, (EApp (e, (ERel (length args), loc)), loc), ("x", arg) :: args)
adamc@609 77 | _ => NONE
adamc@609 78 in
adamc@642 79 case crawl (t, e, []) of
adamc@609 80 NONE => tfuncs
adamc@609 81 | SOME sg => IM.insert (tfuncs, n, sg)
adamc@609 82 end
adamc@609 83 in
adamc@609 84 case d of
adamc@609 85 DVal vi => doOne (vi, tfuncs)
adamc@609 86 | DValRec vis => foldl doOne tfuncs vis
adamc@609 87 | _ => tfuncs
adamc@609 88 end)
adamc@609 89 IM.empty file
adamc@609 90
adamc@607 91 fun exp (e, st) =
adamc@649 92 let
adamc@649 93 fun getApp (e', args) =
adamc@908 94 case e' of
adamc@908 95 ENamed n => SOME (n, args)
adamc@908 96 | EApp (e1, e2) => getApp (#1 e1, e2 :: args)
adamc@908 97 | _ => NONE
adamc@642 98
adam@1848 99 fun newRpc (trans : exp, st : state, fm) =
adamc@908 100 case getApp (#1 trans, []) of
adamc@908 101 NONE => (ErrorMsg.errorAt (#2 trans)
adamc@908 102 "RPC code doesn't use a named function or transaction";
adam@1677 103 (*Print.preface ("Expression",
adam@1677 104 CorePrint.p_exp CoreEnv.empty trans);*)
adamc@908 105 (#1 trans, st))
adamc@908 106 | SOME (n, args) =>
adamc@908 107 case IM.find (tfuncs, n) of
adamc@908 108 NONE => ((*Print.prefaces "BAD" [("e", CorePrint.p_exp CoreEnv.empty (e, loc))];*)
adamc@908 109 raise Fail ("Rpcify: Undetected transaction function " ^ Int.toString n))
adamc@908 110 | SOME (_, _, ran, _) =>
adamc@908 111 let
adamc@908 112 val loc = #2 trans
adamc@642 113
adamc@908 114 val (exported, export_decls) =
adamc@908 115 if IS.member (#exported st, n) then
adamc@908 116 (#exported st, #export_decls st)
adamc@908 117 else
adamc@908 118 (IS.add (#exported st, n),
adamc@1104 119 (DExport (Rpc ReadWrite, n, false), loc) :: #export_decls st)
adamc@642 120
adamc@908 121 val st = {exported = exported,
adamc@957 122 export_decls = export_decls}
adamc@642 123
adam@1848 124 val e' = EServerCall (n, args, ran, fm)
adamc@651 125 in
adamc@908 126 (e', st)
adamc@651 127 end
adamc@649 128 in
adamc@649 129 case e of
adam@1848 130 EApp ((ECApp ((EFfi ("Basis", "rpc"), _), ran), _), trans) => newRpc (trans, st, None)
adam@1848 131 | EApp ((ECApp ((EFfi ("Basis", "tryRpc"), _), ran), _), trans) => newRpc (trans, st, Error)
adamc@908 132 | EApp ((ECApp ((ENamed n, _), ran), _), trans) =>
adamc@908 133 if IS.member (rpcBaseIds, n) then
adam@1848 134 newRpc (trans, st, None)
adam@1848 135 else if IS.member (trpcBaseIds, n) then
adam@1848 136 newRpc (trans, st, Error)
adamc@908 137 else
adamc@908 138 (e, st)
adamc@642 139
adamc@649 140 | _ => (e, st)
adamc@649 141 end
adamc@607 142
adamc@642 143 and doExp (e, st) = U.Exp.foldMap {kind = fn x => x,
adamc@642 144 con = fn x => x,
adamc@642 145 exp = exp} st (ReduceLocal.reduceExp e)
adamc@642 146
adamc@607 147 fun decl (d, st : state) =
adamc@607 148 let
adamc@607 149 val (d, st) = U.Decl.foldMap {kind = fn x => x,
adamc@607 150 con = fn x => x,
adamc@607 151 exp = exp,
adamc@607 152 decl = fn x => x}
adamc@607 153 st d
adamc@607 154 in
adam@1695 155 (d :: #export_decls st,
adamc@908 156 {exported = #exported st,
adamc@957 157 export_decls = []})
adamc@607 158 end
adamc@607 159
adamc@607 160 val (file, _) = ListUtil.foldlMapConcat decl
adamc@908 161 {exported = IS.empty,
adamc@957 162 export_decls = []}
adamc@607 163 file
adamc@607 164 in
adamc@607 165 file
adamc@607 166 end
adamc@607 167
adamc@607 168 end