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