adamc@443
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@443
|
2 * All rights reserved.
|
adamc@443
|
3 *
|
adamc@443
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@443
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@443
|
6 *
|
adamc@443
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@443
|
8 * this list of conditions and the following disclaimer.
|
adamc@443
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@443
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@443
|
11 * and/or other materials provided with the distribution.
|
adamc@443
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@443
|
13 * derived from this software without specific prior written permission.
|
adamc@443
|
14 *
|
adamc@443
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@443
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@443
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@443
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@443
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@443
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@443
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@443
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@443
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@443
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@443
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@443
|
26 *)
|
adamc@443
|
27
|
adamc@443
|
28 structure ESpecialize :> ESPECIALIZE = struct
|
adamc@443
|
29
|
adamc@443
|
30 open Core
|
adamc@443
|
31
|
adamc@443
|
32 structure E = CoreEnv
|
adamc@443
|
33 structure U = CoreUtil
|
adamc@443
|
34
|
adamc@479
|
35 type skey = exp
|
adamc@453
|
36
|
adamc@453
|
37 structure K = struct
|
adamc@479
|
38 type ord_key = exp list
|
adamc@479
|
39 val compare = Order.joinL U.Exp.compare
|
adamc@443
|
40 end
|
adamc@443
|
41
|
adamc@453
|
42 structure KM = BinaryMapFn(K)
|
adamc@443
|
43 structure IM = IntBinaryMap
|
adamc@443
|
44
|
adamc@479
|
45 val sizeOf = U.Exp.fold {kind = fn (_, n) => n,
|
adamc@479
|
46 con = fn (_, n) => n,
|
adamc@479
|
47 exp = fn (_, n) => n + 1}
|
adamc@479
|
48 0
|
adamc@479
|
49
|
adamc@479
|
50 val isOpen = U.Exp.existsB {kind = fn _ => false,
|
adamc@479
|
51 con = fn ((nc, _), c) =>
|
adamc@479
|
52 case c of
|
adamc@479
|
53 CRel n => n >= nc
|
adamc@479
|
54 | _ => false,
|
adamc@479
|
55 exp = fn ((_, ne), e) =>
|
adamc@479
|
56 case e of
|
adamc@479
|
57 ERel n => n >= ne
|
adamc@479
|
58 | _ => false,
|
adamc@479
|
59 bind = fn ((nc, ne), b) =>
|
adamc@479
|
60 case b of
|
adamc@479
|
61 U.Exp.RelC _ => (nc + 1, ne)
|
adamc@479
|
62 | U.Exp.RelE _ => (nc, ne + 1)
|
adamc@479
|
63 | _ => (nc, ne)}
|
adamc@479
|
64 (0, 0)
|
adamc@479
|
65
|
adamc@479
|
66 fun baseBad (e, _) =
|
adamc@453
|
67 case e of
|
adamc@479
|
68 EAbs (_, _, _, e) => sizeOf e > 20
|
adamc@479
|
69 | ENamed _ => false
|
adamc@479
|
70 | _ => true
|
adamc@453
|
71
|
adamc@479
|
72 fun isBad e =
|
adamc@479
|
73 case e of
|
adamc@479
|
74 (ERecord xes, _) =>
|
adamc@479
|
75 length xes > 10
|
adamc@479
|
76 orelse List.exists (fn (_, e, _) => baseBad e) xes
|
adamc@479
|
77 | _ => baseBad e
|
adamc@479
|
78
|
adamc@479
|
79 fun skeyIn e =
|
adamc@479
|
80 if isBad e orelse isOpen e then
|
adamc@479
|
81 NONE
|
adamc@479
|
82 else
|
adamc@479
|
83 SOME e
|
adamc@479
|
84
|
adamc@479
|
85 fun skeyOut e = e
|
adamc@453
|
86
|
adamc@443
|
87 type func = {
|
adamc@443
|
88 name : string,
|
adamc@453
|
89 args : int KM.map,
|
adamc@443
|
90 body : exp,
|
adamc@443
|
91 typ : con,
|
adamc@443
|
92 tag : string
|
adamc@443
|
93 }
|
adamc@443
|
94
|
adamc@443
|
95 type state = {
|
adamc@443
|
96 maxName : int,
|
adamc@443
|
97 funcs : func IM.map,
|
adamc@443
|
98 decls : (string * int * con * exp * string) list
|
adamc@443
|
99 }
|
adamc@443
|
100
|
adamc@443
|
101 fun kind (k, st) = (k, st)
|
adamc@443
|
102 fun con (c, st) = (c, st)
|
adamc@443
|
103
|
adamc@443
|
104 fun exp (e, st : state) =
|
adamc@443
|
105 let
|
adamc@443
|
106 fun getApp e =
|
adamc@443
|
107 case e of
|
adamc@443
|
108 ENamed f => SOME (f, [], [])
|
adamc@480
|
109 | EField ((ERecord xes, _), (CName x, _), _) =>
|
adamc@480
|
110 (case List.find (fn ((CName x', _), _,_) => x' = x
|
adamc@480
|
111 | _ => false) xes of
|
adamc@480
|
112 NONE => NONE
|
adamc@480
|
113 | SOME (_, (e, _), _) => getApp e)
|
adamc@443
|
114 | EApp (e1, e2) =>
|
adamc@443
|
115 (case getApp (#1 e1) of
|
adamc@443
|
116 NONE => NONE
|
adamc@453
|
117 | SOME (f, xs, xs') =>
|
adamc@453
|
118 let
|
adamc@453
|
119 val k =
|
adamc@453
|
120 if List.null xs' then
|
adamc@453
|
121 skeyIn e2
|
adamc@453
|
122 else
|
adamc@453
|
123 NONE
|
adamc@453
|
124 in
|
adamc@453
|
125 case k of
|
adamc@453
|
126 NONE => SOME (f, xs, xs' @ [e2])
|
adamc@453
|
127 | SOME k => SOME (f, xs @ [k], xs')
|
adamc@453
|
128 end)
|
adamc@443
|
129 | _ => NONE
|
adamc@443
|
130 in
|
adamc@443
|
131 case getApp e of
|
adamc@443
|
132 NONE => (e, st)
|
adamc@480
|
133 | SOME (f, [], xs') => (#1 (foldl (fn (arg, e) => (EApp (e, arg), ErrorMsg.dummySpan))
|
adamc@480
|
134 (ENamed f, ErrorMsg.dummySpan) xs'), st)
|
adamc@443
|
135 | SOME (f, xs, xs') =>
|
adamc@443
|
136 case IM.find (#funcs st, f) of
|
adamc@480
|
137 NONE =>
|
adamc@480
|
138 let
|
adamc@480
|
139 val e = foldl (fn (arg, e) => (EApp (e, skeyOut arg), ErrorMsg.dummySpan))
|
adamc@480
|
140 (ENamed f, ErrorMsg.dummySpan) xs
|
adamc@480
|
141 in
|
adamc@480
|
142 (#1 (foldl (fn (arg, e) => (EApp (e, arg), ErrorMsg.dummySpan))
|
adamc@480
|
143 e xs'), st)
|
adamc@480
|
144 end
|
adamc@443
|
145 | SOME {name, args, body, typ, tag} =>
|
adamc@453
|
146 case KM.find (args, xs) of
|
adamc@453
|
147 SOME f' => ((*Print.prefaces "Pre-existing" [("e", CorePrint.p_exp CoreEnv.empty (e, ErrorMsg.dummySpan))];*)
|
adamc@453
|
148 (#1 (foldl (fn (e, arg) => (EApp (e, arg), ErrorMsg.dummySpan))
|
adamc@453
|
149 (ENamed f', ErrorMsg.dummySpan) xs'),
|
adamc@453
|
150 st))
|
adamc@443
|
151 | NONE =>
|
adamc@443
|
152 let
|
adamc@453
|
153 (*val () = Print.prefaces "New" [("e", CorePrint.p_exp CoreEnv.empty (e, ErrorMsg.dummySpan))]*)
|
adamc@453
|
154
|
adamc@443
|
155 fun subBody (body, typ, xs) =
|
adamc@443
|
156 case (#1 body, #1 typ, xs) of
|
adamc@443
|
157 (_, _, []) => SOME (body, typ)
|
adamc@443
|
158 | (EAbs (_, _, _, body'), TFun (_, typ'), x :: xs) =>
|
adamc@453
|
159 let
|
adamc@479
|
160 val body'' = E.subExpInExp (0, skeyOut x) body'
|
adamc@453
|
161 in
|
adamc@453
|
162 (*Print.prefaces "espec" [("body'", CorePrint.p_exp CoreEnv.empty body'),
|
adamc@453
|
163 ("body''", CorePrint.p_exp CoreEnv.empty body'')];*)
|
adamc@453
|
164 subBody (body'',
|
adamc@453
|
165 typ',
|
adamc@453
|
166 xs)
|
adamc@453
|
167 end
|
adamc@443
|
168 | _ => NONE
|
adamc@443
|
169 in
|
adamc@443
|
170 case subBody (body, typ, xs) of
|
adamc@443
|
171 NONE => (e, st)
|
adamc@443
|
172 | SOME (body', typ') =>
|
adamc@443
|
173 let
|
adamc@443
|
174 val f' = #maxName st
|
adamc@453
|
175 (*val () = print ("f' = " ^ Int.toString f' ^ "\n")*)
|
adamc@443
|
176 val funcs = IM.insert (#funcs st, f, {name = name,
|
adamc@453
|
177 args = KM.insert (args, xs, f'),
|
adamc@443
|
178 body = body,
|
adamc@443
|
179 typ = typ,
|
adamc@443
|
180 tag = tag})
|
adamc@443
|
181 val st = {
|
adamc@443
|
182 maxName = f' + 1,
|
adamc@443
|
183 funcs = funcs,
|
adamc@443
|
184 decls = #decls st
|
adamc@443
|
185 }
|
adamc@443
|
186
|
adamc@443
|
187 val (body', st) = specExp st body'
|
adamc@443
|
188 val e' = foldl (fn (e, arg) => (EApp (e, arg), ErrorMsg.dummySpan))
|
adamc@443
|
189 (ENamed f', ErrorMsg.dummySpan) xs'
|
adamc@443
|
190 in
|
adamc@443
|
191 (#1 e',
|
adamc@443
|
192 {maxName = #maxName st,
|
adamc@443
|
193 funcs = #funcs st,
|
adamc@444
|
194 decls = (name, f', typ', body', tag) :: #decls st})
|
adamc@443
|
195 end
|
adamc@443
|
196 end
|
adamc@443
|
197 end
|
adamc@443
|
198
|
adamc@443
|
199 and specExp st = U.Exp.foldMap {kind = kind, con = con, exp = exp} st
|
adamc@443
|
200
|
adamc@443
|
201 fun decl (d, st) = (d, st)
|
adamc@443
|
202
|
adamc@443
|
203 val specDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl}
|
adamc@443
|
204
|
adamc@453
|
205 fun specialize' file =
|
adamc@443
|
206 let
|
adamc@453
|
207 fun doDecl (d, (st : state, changed)) =
|
adamc@443
|
208 let
|
adamc@453
|
209 val funcs = #funcs st
|
adamc@453
|
210 val funcs =
|
adamc@453
|
211 case #1 d of
|
adamc@453
|
212 DValRec vis =>
|
adamc@453
|
213 foldl (fn ((x, n, c, e, tag), funcs) =>
|
adamc@453
|
214 IM.insert (funcs, n, {name = x,
|
adamc@453
|
215 args = KM.empty,
|
adamc@453
|
216 body = e,
|
adamc@453
|
217 typ = c,
|
adamc@453
|
218 tag = tag}))
|
adamc@453
|
219 funcs vis
|
adamc@453
|
220 | _ => funcs
|
adamc@453
|
221
|
adamc@453
|
222 val st = {maxName = #maxName st,
|
adamc@453
|
223 funcs = funcs,
|
adamc@453
|
224 decls = []}
|
adamc@453
|
225
|
adamc@443
|
226 val (d', st) = specDecl st d
|
adamc@443
|
227
|
adamc@443
|
228 val funcs = #funcs st
|
adamc@443
|
229 val funcs =
|
adamc@443
|
230 case #1 d of
|
adamc@443
|
231 DVal (x, n, c, e as (EAbs _, _), tag) =>
|
adamc@443
|
232 IM.insert (funcs, n, {name = x,
|
adamc@453
|
233 args = KM.empty,
|
adamc@443
|
234 body = e,
|
adamc@443
|
235 typ = c,
|
adamc@443
|
236 tag = tag})
|
adamc@469
|
237 | DVal (_, n, _, (ENamed n', _), _) =>
|
adamc@469
|
238 (case IM.find (funcs, n') of
|
adamc@469
|
239 NONE => funcs
|
adamc@469
|
240 | SOME v => IM.insert (funcs, n, v))
|
adamc@443
|
241 | _ => funcs
|
adamc@443
|
242
|
adamc@453
|
243 val (changed, ds) =
|
adamc@443
|
244 case #decls st of
|
adamc@453
|
245 [] => (changed, [d'])
|
adamc@453
|
246 | vis =>
|
adamc@453
|
247 (true, case d' of
|
adamc@453
|
248 (DValRec vis', _) => [(DValRec (vis @ vis'), ErrorMsg.dummySpan)]
|
adamc@453
|
249 | _ => [(DValRec vis, ErrorMsg.dummySpan), d'])
|
adamc@443
|
250 in
|
adamc@453
|
251 (ds, ({maxName = #maxName st,
|
adamc@453
|
252 funcs = funcs,
|
adamc@453
|
253 decls = []}, changed))
|
adamc@443
|
254 end
|
adamc@443
|
255
|
adamc@453
|
256 val (ds, (_, changed)) = ListUtil.foldlMapConcat doDecl
|
adamc@453
|
257 ({maxName = U.File.maxName file + 1,
|
adamc@453
|
258 funcs = IM.empty,
|
adamc@453
|
259 decls = []}, false)
|
adamc@453
|
260 file
|
adamc@443
|
261 in
|
adamc@453
|
262 (changed, ds)
|
adamc@443
|
263 end
|
adamc@443
|
264
|
adamc@453
|
265 fun specialize file =
|
adamc@453
|
266 let
|
adamc@453
|
267 val (changed, file) = specialize' file
|
adamc@453
|
268 in
|
adamc@453
|
269 if changed then
|
adamc@453
|
270 specialize file
|
adamc@453
|
271 else
|
adamc@453
|
272 file
|
adamc@453
|
273 end
|
adamc@453
|
274
|
adamc@443
|
275
|
adamc@443
|
276 end
|