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