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
|