adamc@1185
|
1 (* Copyright (c) 2008-2010, Adam Chlipala
|
adamc@315
|
2 * All rights reserved.
|
adamc@315
|
3 *
|
adamc@315
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@315
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@315
|
6 *
|
adamc@315
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@315
|
8 * this list of conditions and the following disclaimer.
|
adamc@315
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@315
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@315
|
11 * and/or other materials provided with the distribution.
|
adamc@315
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@315
|
13 * derived from this software without specific prior written permission.
|
adamc@315
|
14 *
|
adamc@315
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@315
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@315
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@315
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@315
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@315
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@315
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@315
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@315
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@315
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@315
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@315
|
26 *)
|
adamc@315
|
27
|
adamc@315
|
28 (* Simplify a Core program by repeating polymorphic function definitions *)
|
adamc@315
|
29
|
adamc@315
|
30 structure Unpoly :> UNPOLY = struct
|
adamc@315
|
31
|
adamc@315
|
32 open Core
|
adamc@315
|
33
|
adamc@315
|
34 structure E = CoreEnv
|
adamc@315
|
35 structure U = CoreUtil
|
adamc@315
|
36
|
adamc@315
|
37 structure IS = IntBinarySet
|
adamc@315
|
38 structure IM = IntBinaryMap
|
adamc@315
|
39
|
adamc@315
|
40
|
adamc@315
|
41 (** The actual specialization *)
|
adamc@315
|
42
|
adamc@315
|
43 val liftConInCon = E.liftConInCon
|
adamc@315
|
44 val subConInCon = E.subConInCon
|
adamc@315
|
45
|
adamc@315
|
46 val liftConInExp = E.liftConInExp
|
adamc@315
|
47 val subConInExp = E.subConInExp
|
adamc@315
|
48
|
adamc@1185
|
49 val isOpen = U.Con.existsB {kind = fn _ => false,
|
adamc@1185
|
50 con = fn (n, c) =>
|
adamc@1185
|
51 case c of
|
adamc@1185
|
52 CRel n' => n' >= n
|
adamc@1185
|
53 | _ => false,
|
adamc@1185
|
54 bind = fn (n, b) =>
|
adamc@1185
|
55 case b of
|
adamc@1185
|
56 U.Con.RelC _ => n + 1
|
adamc@1185
|
57 | _ => n} 0
|
adamc@399
|
58
|
adamc@316
|
59 fun unpolyNamed (xn, rep) =
|
adamc@316
|
60 U.Exp.map {kind = fn k => k,
|
adamc@316
|
61 con = fn c => c,
|
adamc@316
|
62 exp = fn e =>
|
adamc@316
|
63 case e of
|
adamc@399
|
64 ECApp (e', _) =>
|
adamc@325
|
65 let
|
adamc@325
|
66 fun isTheOne (e, _) =
|
adamc@325
|
67 case e of
|
adamc@325
|
68 ENamed xn' => xn' = xn
|
adamc@325
|
69 | ECApp (e, _) => isTheOne e
|
adamc@325
|
70 | _ => false
|
adamc@325
|
71 in
|
adamc@325
|
72 if isTheOne e' then
|
adamc@399
|
73 rep
|
adamc@325
|
74 else
|
adamc@325
|
75 e
|
adamc@325
|
76 end
|
adamc@316
|
77 | _ => e}
|
adamc@316
|
78
|
adamc@794
|
79 structure M = BinaryMapFn(struct
|
adamc@794
|
80 type ord_key = con list
|
adamc@794
|
81 val compare = Order.joinL U.Con.compare
|
adamc@794
|
82 end)
|
adamc@794
|
83
|
adamc@794
|
84 type func = {
|
adamc@794
|
85 kinds : kind list,
|
adamc@794
|
86 defs : (string * int * con * exp * string) list,
|
adamc@794
|
87 replacements : int M.map
|
adamc@794
|
88 }
|
adamc@794
|
89
|
adamc@315
|
90 type state = {
|
adamc@794
|
91 funcs : func IM.map,
|
adamc@315
|
92 decls : decl list,
|
adamc@315
|
93 nextName : int
|
adamc@315
|
94 }
|
adamc@315
|
95
|
adamc@315
|
96 fun kind (k, st) = (k, st)
|
adamc@315
|
97
|
adamc@315
|
98 fun con (c, st) = (c, st)
|
adamc@315
|
99
|
adamc@315
|
100 fun exp (e, st : state) =
|
adamc@315
|
101 case e of
|
adamc@315
|
102 ECApp _ =>
|
adamc@315
|
103 let
|
adamc@315
|
104 fun unravel (e, cargs) =
|
adamc@315
|
105 case e of
|
adamc@315
|
106 ECApp ((e, _), c) => unravel (e, c :: cargs)
|
adamc@315
|
107 | ENamed n => SOME (n, rev cargs)
|
adamc@315
|
108 | _ => NONE
|
adamc@315
|
109 in
|
adamc@315
|
110 case unravel (e, []) of
|
adamc@315
|
111 NONE => (e, st)
|
adamc@315
|
112 | SOME (n, cargs) =>
|
adamc@399
|
113 if List.exists isOpen cargs then
|
adamc@399
|
114 (e, st)
|
adamc@399
|
115 else
|
adamc@399
|
116 case IM.find (#funcs st, n) of
|
adamc@399
|
117 NONE => (e, st)
|
adamc@794
|
118 | SOME {kinds = ks, defs = vis, replacements} =>
|
adamc@794
|
119 case M.find (replacements, cargs) of
|
adamc@794
|
120 SOME n => (ENamed n, st)
|
adamc@794
|
121 | NONE =>
|
adamc@794
|
122 let
|
adamc@794
|
123 val old_vis = vis
|
adamc@794
|
124 val (vis, (thisName, nextName)) =
|
adamc@794
|
125 ListUtil.foldlMap
|
adamc@794
|
126 (fn ((x, n', t, e, s), (thisName, nextName)) =>
|
adamc@794
|
127 ((x, nextName, n', t, e, s),
|
adamc@794
|
128 (if n' = n then nextName else thisName,
|
adamc@794
|
129 nextName + 1)))
|
adamc@794
|
130 (0, #nextName st) vis
|
adamc@315
|
131
|
adamc@794
|
132 fun specialize (x, n, n_old, t, e, s) =
|
adamc@794
|
133 let
|
adamc@794
|
134 fun trim (t, e, cargs) =
|
adamc@794
|
135 case (t, e, cargs) of
|
adamc@794
|
136 ((TCFun (_, _, t), _),
|
adamc@794
|
137 (ECAbs (_, _, e), _),
|
adamc@794
|
138 carg :: cargs) =>
|
adamc@794
|
139 let
|
adamc@794
|
140 val t = subConInCon (length cargs, carg) t
|
adamc@794
|
141 val e = subConInExp (length cargs, carg) e
|
adamc@794
|
142 in
|
adamc@794
|
143 trim (t, e, cargs)
|
adamc@794
|
144 end
|
adamc@796
|
145 | (_, _, []) => SOME (t, e)
|
adamc@794
|
146 | _ => NONE
|
adamc@794
|
147 in
|
adamc@794
|
148 (*Print.prefaces "specialize"
|
adamc@1185
|
149 [("n", Print.PD.string (Int.toString n)),
|
adamc@1185
|
150 ("nold", Print.PD.string (Int.toString n_old)),
|
adamc@1185
|
151 ("t", CorePrint.p_con CoreEnv.empty t),
|
adamc@1185
|
152 ("e", CorePrint.p_exp CoreEnv.empty e),
|
adamc@1185
|
153 ("|cargs|", Print.PD.string (Int.toString (length cargs)))];*)
|
adamc@794
|
154 Option.map (fn (t, e) => (x, n, n_old, t, e, s))
|
adamc@794
|
155 (trim (t, e, cargs))
|
adamc@794
|
156 end
|
adamc@315
|
157
|
adamc@794
|
158 val vis = List.map specialize vis
|
adamc@794
|
159 in
|
adamc@794
|
160 if List.exists (not o Option.isSome) vis orelse length cargs > length ks then
|
adamc@794
|
161 (e, st)
|
adamc@794
|
162 else
|
adamc@794
|
163 let
|
adamc@794
|
164 val vis = List.mapPartial (fn x => x) vis
|
adamc@316
|
165
|
adamc@794
|
166 val vis = map (fn (x, n, n_old, t, e, s) =>
|
adamc@794
|
167 (x ^ "_unpoly", n, n_old, t, e, s)) vis
|
adamc@794
|
168 val vis' = map (fn (x, n, _, t, e, s) =>
|
adamc@794
|
169 (x, n, t, e, s)) vis
|
adamc@794
|
170
|
adamc@1016
|
171 val funcs = foldl (fn ((_, n, n_old, _, _, _), funcs) =>
|
adamc@1016
|
172 let
|
adamc@1016
|
173 val replacements = case IM.find (funcs, n_old) of
|
adamc@1016
|
174 NONE => M.empty
|
adamc@1016
|
175 | SOME {replacements = r, ...} => r
|
adamc@1016
|
176 in
|
adamc@1016
|
177 IM.insert (funcs, n_old,
|
adamc@1016
|
178 {kinds = ks,
|
adamc@1016
|
179 defs = old_vis,
|
adamc@1016
|
180 replacements = M.insert (replacements,
|
adamc@1016
|
181 cargs,
|
adamc@1016
|
182 n)})
|
adamc@1016
|
183 end) (#funcs st) vis
|
adamc@794
|
184
|
adamc@794
|
185 val ks' = List.drop (ks, length cargs)
|
adamc@794
|
186
|
adamc@794
|
187 val st = {funcs = foldl (fn (vi, funcs) =>
|
adamc@794
|
188 IM.insert (funcs, #2 vi,
|
adamc@794
|
189 {kinds = ks',
|
adamc@794
|
190 defs = vis',
|
adamc@794
|
191 replacements = M.empty}))
|
adamc@794
|
192 funcs vis',
|
adamc@794
|
193 decls = #decls st,
|
adamc@794
|
194 nextName = nextName}
|
adamc@794
|
195
|
adamc@794
|
196 val (vis', st) = ListUtil.foldlMap (fn ((x, n, t, e, s), st) =>
|
adamc@794
|
197 let
|
adamc@794
|
198 val (e, st) = polyExp (e, st)
|
adamc@794
|
199 in
|
adamc@794
|
200 ((x, n, t, e, s), st)
|
adamc@794
|
201 end)
|
adamc@794
|
202 st vis'
|
adamc@794
|
203 in
|
adamc@794
|
204 (ENamed thisName,
|
adamc@794
|
205 {funcs = #funcs st,
|
adamc@399
|
206 decls = (DValRec vis', ErrorMsg.dummySpan) :: #decls st,
|
adamc@794
|
207 nextName = #nextName st})
|
adamc@794
|
208 end
|
adamc@794
|
209 end
|
adamc@315
|
210 end
|
adamc@315
|
211 | _ => (e, st)
|
adamc@315
|
212
|
adamc@794
|
213 and polyExp (x, st) = U.Exp.foldMap {kind = kind, con = con, exp = exp} st x
|
adamc@794
|
214
|
adamc@315
|
215 fun decl (d, st : state) =
|
adamc@1122
|
216 let
|
adamc@1122
|
217 fun unravel (e, cargs) =
|
adamc@1122
|
218 case e of
|
adamc@1122
|
219 (ECAbs (_, k, e), _) =>
|
adamc@1122
|
220 unravel (e, k :: cargs)
|
adamc@1122
|
221 | _ => rev cargs
|
adamc@1122
|
222 in
|
adamc@1122
|
223 case d of
|
adamc@1122
|
224 DVal (vi as (x, n, t, e, s)) =>
|
adamc@1122
|
225 let
|
adamc@1122
|
226 val cargs = unravel (e, [])
|
adamc@315
|
227
|
adamc@1122
|
228 val ns = IS.singleton n
|
adamc@1122
|
229 in
|
adamc@1122
|
230 (d, {funcs = IM.insert (#funcs st, n, {kinds = cargs,
|
adamc@1122
|
231 defs = [vi],
|
adamc@1122
|
232 replacements = M.empty}),
|
adamc@1122
|
233 decls = #decls st,
|
adamc@1122
|
234 nextName = #nextName st})
|
adamc@1122
|
235 end
|
adamc@1122
|
236 | DValRec (vis as ((x, n, t, e, s) :: rest)) =>
|
adamc@1122
|
237 let
|
adamc@1122
|
238 val cargs = unravel (e, [])
|
adamc@315
|
239
|
adamc@1122
|
240 fun unravel (e, cargs) =
|
adamc@1122
|
241 case (e, cargs) of
|
adamc@1122
|
242 ((ECAbs (_, k, e), _), k' :: cargs) =>
|
adamc@1122
|
243 U.Kind.compare (k, k') = EQUAL
|
adamc@1122
|
244 andalso unravel (e, cargs)
|
adamc@1122
|
245 | (_, []) => true
|
adamc@1122
|
246 | _ => false
|
adamc@1122
|
247
|
adamc@1122
|
248 fun deAbs (e, cargs) =
|
adamc@1122
|
249 case (e, cargs) of
|
adamc@1122
|
250 ((ECAbs (_, _, e), _), _ :: cargs) => deAbs (e, cargs)
|
adamc@1122
|
251 | (_, []) => e
|
adamc@1122
|
252 | _ => raise Fail "Unpoly: deAbs"
|
adamc@315
|
253
|
adamc@1122
|
254 in
|
adamc@1122
|
255 if List.exists (fn vi => not (unravel (#4 vi, cargs))) rest then
|
adamc@1122
|
256 (d, st)
|
adamc@1122
|
257 else
|
adamc@1122
|
258 let
|
adamc@1122
|
259 val ns = IS.addList (IS.empty, map #2 vis)
|
adamc@1122
|
260 val nargs = length cargs
|
adamc@315
|
261
|
adamc@1122
|
262 (** Verifying lack of polymorphic recursion *)
|
adamc@315
|
263
|
adamc@1122
|
264 fun kind _ = false
|
adamc@1122
|
265 fun con _ = false
|
adamc@315
|
266
|
adamc@1180
|
267 fun exp (cn, e) =
|
adamc@1122
|
268 case e of
|
adamc@1180
|
269 orig as ECApp (e, c) =>
|
adamc@1122
|
270 let
|
adamc@1122
|
271 fun isIrregular (e, pos) =
|
adamc@1122
|
272 case #1 e of
|
adamc@1122
|
273 ENamed n =>
|
adamc@1122
|
274 IS.member (ns, n)
|
adamc@1122
|
275 andalso
|
adamc@1122
|
276 (case #1 c of
|
adamc@1180
|
277 CRel i => i <> nargs - pos + cn
|
adamc@1122
|
278 | _ => true)
|
adamc@1122
|
279 | ECApp (e, _) => isIrregular (e, pos + 1)
|
adamc@1122
|
280 | _ => false
|
adamc@1122
|
281 in
|
adamc@1122
|
282 isIrregular (e, 1)
|
adamc@1122
|
283 end
|
adamc@1122
|
284 | _ => false
|
adamc@315
|
285
|
adamc@1180
|
286 fun bind (cn, b) =
|
adamc@1180
|
287 case b of
|
adamc@1180
|
288 U.Exp.RelC _ => cn+1
|
adamc@1180
|
289 | _ => cn
|
adamc@1180
|
290
|
adamc@1180
|
291 val irregular = U.Exp.existsB {kind = kind, con = con, exp = exp, bind = bind} 0
|
adamc@1122
|
292 in
|
adamc@1122
|
293 if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then
|
adamc@1185
|
294 (d, st)
|
adamc@1122
|
295 else
|
adamc@1122
|
296 (d, {funcs = foldl (fn (vi, funcs) =>
|
adamc@1122
|
297 IM.insert (funcs, #2 vi, {kinds = cargs,
|
adamc@1122
|
298 defs = vis,
|
adamc@1122
|
299 replacements = M.empty}))
|
adamc@1122
|
300 (#funcs st) vis,
|
adamc@1122
|
301 decls = #decls st,
|
adamc@1122
|
302 nextName = #nextName st})
|
adamc@1122
|
303 end
|
adamc@1122
|
304 end
|
adamc@315
|
305
|
adamc@1122
|
306 | _ => (d, st)
|
adamc@1122
|
307 end
|
adamc@315
|
308
|
adamc@315
|
309 val polyDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl}
|
adamc@315
|
310
|
adamc@315
|
311 fun unpoly file =
|
adamc@315
|
312 let
|
adamc@315
|
313 fun doDecl (d : decl, st : state) =
|
adamc@315
|
314 let
|
adamc@315
|
315 val (d, st) = polyDecl st d
|
adamc@315
|
316 in
|
adamc@315
|
317 (rev (d :: #decls st),
|
adamc@315
|
318 {funcs = #funcs st,
|
adamc@315
|
319 decls = [],
|
adamc@315
|
320 nextName = #nextName st})
|
adamc@315
|
321 end
|
adamc@315
|
322
|
adamc@315
|
323 val (ds, _) = ListUtil.foldlMapConcat doDecl
|
adamc@315
|
324 {funcs = IM.empty,
|
adamc@315
|
325 decls = [],
|
adamc@315
|
326 nextName = U.File.maxName file + 1} file
|
adamc@315
|
327 in
|
adamc@315
|
328 ds
|
adamc@315
|
329 end
|
adamc@315
|
330
|
adamc@315
|
331 end
|