adamc@193
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@193
|
2 * All rights reserved.
|
adamc@193
|
3 *
|
adamc@193
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@193
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@193
|
6 *
|
adamc@193
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@193
|
8 * this list of conditions and the following disclaimer.
|
adamc@193
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@193
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@193
|
11 * and/or other materials provided with the distribution.
|
adamc@193
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@193
|
13 * derived from this software without specific prior written permission.
|
adamc@193
|
14 *
|
adamc@193
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@193
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@193
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@193
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@193
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@193
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@193
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@193
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@193
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@193
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@193
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@193
|
26 *)
|
adamc@193
|
27
|
adamc@315
|
28 (* Simplify a Core program by repeating polymorphic definitions of datatypes *)
|
adamc@193
|
29
|
adamc@193
|
30 structure Specialize :> SPECIALIZE = struct
|
adamc@193
|
31
|
adamc@193
|
32 open Core
|
adamc@193
|
33
|
adamc@193
|
34 structure E = CoreEnv
|
adamc@193
|
35 structure U = CoreUtil
|
adamc@193
|
36
|
adamc@193
|
37 val liftConInCon = E.liftConInCon
|
adamc@193
|
38 val subConInCon = E.subConInCon
|
adamc@193
|
39
|
adamc@193
|
40 structure CK = struct
|
adamc@193
|
41 type ord_key = con list
|
adamc@193
|
42 val compare = Order.joinL U.Con.compare
|
adamc@193
|
43 end
|
adamc@193
|
44
|
adamc@193
|
45 structure CM = BinaryMapFn(CK)
|
adamc@193
|
46 structure IM = IntBinaryMap
|
adamc@193
|
47
|
adamc@193
|
48 type datatyp' = {
|
adamc@193
|
49 name : int,
|
adamc@193
|
50 constructors : int IM.map
|
adamc@193
|
51 }
|
adamc@193
|
52
|
adamc@193
|
53 type datatyp = {
|
adamc@193
|
54 name : string,
|
adamc@193
|
55 params : int,
|
adamc@193
|
56 constructors : (string * int * con option) list,
|
adamc@193
|
57 specializations : datatyp' CM.map
|
adamc@193
|
58 }
|
adamc@193
|
59
|
adamc@193
|
60 type state = {
|
adamc@193
|
61 count : int,
|
adamc@193
|
62 datatypes : datatyp IM.map,
|
adamc@193
|
63 constructors : int IM.map,
|
adamc@846
|
64 decls : (string * int * string list * (string * int * con option) list) list
|
adamc@193
|
65 }
|
adamc@193
|
66
|
adamc@193
|
67 fun kind (k, st) = (k, st)
|
adamc@193
|
68
|
adamc@193
|
69 val isOpen = U.Con.exists {kind = fn _ => false,
|
adamc@193
|
70 con = fn c =>
|
adamc@193
|
71 case c of
|
adamc@193
|
72 CRel _ => true
|
adamc@193
|
73 | _ => false}
|
adamc@193
|
74
|
adamc@193
|
75 fun considerSpecialization (st : state, n, args, dt : datatyp) =
|
adamc@193
|
76 case CM.find (#specializations dt, args) of
|
adamc@193
|
77 SOME dt' => (#name dt', #constructors dt', st)
|
adamc@193
|
78 | NONE =>
|
adamc@193
|
79 let
|
adamc@194
|
80 (*val () = Print.prefaces "Args" [("args", Print.p_list (CorePrint.p_con CoreEnv.empty) args)]*)
|
adamc@194
|
81
|
adamc@193
|
82 val n' = #count st
|
adamc@193
|
83
|
adamc@194
|
84 val nxs = length args - 1
|
adamc@193
|
85 fun sub t = ListUtil.foldli (fn (i, arg, t) =>
|
adamc@194
|
86 subConInCon (nxs - i, arg) t) t args
|
adamc@193
|
87
|
adamc@193
|
88 val (cons, (count, cmap)) =
|
adamc@193
|
89 ListUtil.foldlMap (fn ((x, n, to), (count, cmap)) =>
|
adamc@193
|
90 let
|
adamc@193
|
91 val to = Option.map sub to
|
adamc@193
|
92 in
|
adamc@193
|
93 ((x, count, to),
|
adamc@193
|
94 (count + 1,
|
adamc@193
|
95 IM.insert (cmap, n, count)))
|
adamc@193
|
96 end) (n' + 1, IM.empty) (#constructors dt)
|
adamc@193
|
97
|
adamc@193
|
98 val st = {count = count,
|
adamc@193
|
99 datatypes = IM.insert (#datatypes st, n,
|
adamc@193
|
100 {name = #name dt,
|
adamc@193
|
101 params = #params dt,
|
adamc@193
|
102 constructors = #constructors dt,
|
adamc@193
|
103 specializations = CM.insert (#specializations dt,
|
adamc@193
|
104 args,
|
adamc@193
|
105 {name = n',
|
adamc@193
|
106 constructors = cmap})}),
|
adamc@193
|
107 constructors = #constructors st,
|
adamc@193
|
108 decls = #decls st}
|
adamc@193
|
109
|
adamc@193
|
110 val (cons, st) = ListUtil.foldlMap (fn ((x, n, NONE), st) => ((x, n, NONE), st)
|
adamc@193
|
111 | ((x, n, SOME t), st) =>
|
adamc@193
|
112 let
|
adamc@193
|
113 val (t, st) = specCon st t
|
adamc@193
|
114 in
|
adamc@193
|
115 ((x, n, SOME t), st)
|
adamc@193
|
116 end) st cons
|
adamc@193
|
117
|
adamc@846
|
118 val dt = (#name dt ^ "_s",
|
adamc@846
|
119 n',
|
adamc@846
|
120 [],
|
adamc@846
|
121 cons)
|
adamc@193
|
122 in
|
adamc@193
|
123 (n', cmap, {count = #count st,
|
adamc@193
|
124 datatypes = #datatypes st,
|
adamc@193
|
125 constructors = #constructors st,
|
adamc@846
|
126 decls = dt :: #decls st})
|
adamc@193
|
127 end
|
adamc@193
|
128
|
adamc@193
|
129 and con (c, st : state) =
|
adamc@193
|
130 let
|
adamc@193
|
131 fun findApp (c, args) =
|
adamc@193
|
132 case c of
|
adamc@193
|
133 CApp ((c', _), arg) => findApp (c', arg :: args)
|
adamc@193
|
134 | CNamed n => SOME (n, args)
|
adamc@193
|
135 | _ => NONE
|
adamc@193
|
136 in
|
adamc@193
|
137 case findApp (c, []) of
|
adamc@193
|
138 SOME (n, args as (_ :: _)) =>
|
adamc@193
|
139 if List.exists isOpen args then
|
adamc@193
|
140 (c, st)
|
adamc@193
|
141 else
|
adamc@193
|
142 (case IM.find (#datatypes st, n) of
|
adamc@193
|
143 NONE => (c, st)
|
adamc@193
|
144 | SOME dt =>
|
adamc@193
|
145 if length args <> #params dt then
|
adamc@193
|
146 (c, st)
|
adamc@193
|
147 else
|
adamc@193
|
148 let
|
adamc@193
|
149 val (n, _, st) = considerSpecialization (st, n, args, dt)
|
adamc@193
|
150 in
|
adamc@193
|
151 (CNamed n, st)
|
adamc@193
|
152 end)
|
adamc@193
|
153 | _ => (c, st)
|
adamc@193
|
154 end
|
adamc@193
|
155
|
adamc@193
|
156 and specCon st = U.Con.foldMap {kind = kind, con = con} st
|
adamc@193
|
157
|
adamc@193
|
158 fun pat (p, st) =
|
adamc@193
|
159 case #1 p of
|
adamc@193
|
160 PWild => (p, st)
|
adamc@193
|
161 | PVar _ => (p, st)
|
adamc@193
|
162 | PPrim _ => (p, st)
|
adamc@193
|
163 | PCon (dk, PConVar pn, args as (_ :: _), po) =>
|
adamc@193
|
164 let
|
adamc@193
|
165 val (po, st) =
|
adamc@193
|
166 case po of
|
adamc@193
|
167 NONE => (NONE, st)
|
adamc@193
|
168 | SOME p =>
|
adamc@193
|
169 let
|
adamc@193
|
170 val (p, st) = pat (p, st)
|
adamc@193
|
171 in
|
adamc@193
|
172 (SOME p, st)
|
adamc@193
|
173 end
|
adamc@193
|
174 val p = (PCon (dk, PConVar pn, args, po), #2 p)
|
adamc@193
|
175 in
|
adamc@193
|
176 if List.exists isOpen args then
|
adamc@193
|
177 (p, st)
|
adamc@193
|
178 else
|
adamc@193
|
179 case IM.find (#constructors st, pn) of
|
adamc@193
|
180 NONE => (p, st)
|
adamc@193
|
181 | SOME n =>
|
adamc@193
|
182 case IM.find (#datatypes st, n) of
|
adamc@193
|
183 NONE => (p, st)
|
adamc@193
|
184 | SOME dt =>
|
adamc@193
|
185 let
|
adamc@193
|
186 val (n, cmap, st) = considerSpecialization (st, n, args, dt)
|
adamc@193
|
187 in
|
adamc@193
|
188 case IM.find (cmap, pn) of
|
adamc@193
|
189 NONE => raise Fail "Specialize: Missing datatype constructor (pat)"
|
adamc@193
|
190 | SOME pn' => ((PCon (dk, PConVar pn', [], po), #2 p), st)
|
adamc@193
|
191 end
|
adamc@193
|
192 end
|
adamc@193
|
193 | PCon _ => (p, st)
|
adamc@193
|
194 | PRecord xps =>
|
adamc@193
|
195 let
|
adamc@193
|
196 val (xps, st) = ListUtil.foldlMap (fn ((x, p, t), st) =>
|
adamc@193
|
197 let
|
adamc@193
|
198 val (p, st) = pat (p, st)
|
adamc@193
|
199 in
|
adamc@193
|
200 ((x, p, t), st)
|
adamc@193
|
201 end)
|
adamc@193
|
202 st xps
|
adamc@193
|
203 in
|
adamc@193
|
204 ((PRecord xps, #2 p), st)
|
adamc@193
|
205 end
|
adamc@193
|
206
|
adamc@193
|
207 fun exp (e, st) =
|
adamc@193
|
208 case e of
|
adamc@193
|
209 ECon (dk, PConVar pn, args as (_ :: _), eo) =>
|
adamc@193
|
210 if List.exists isOpen args then
|
adamc@193
|
211 (e, st)
|
adamc@193
|
212 else
|
adamc@193
|
213 (case IM.find (#constructors st, pn) of
|
adamc@193
|
214 NONE => (e, st)
|
adamc@193
|
215 | SOME n =>
|
adamc@193
|
216 case IM.find (#datatypes st, n) of
|
adamc@193
|
217 NONE => (e, st)
|
adamc@193
|
218 | SOME dt =>
|
adamc@193
|
219 let
|
adamc@193
|
220 val (n, cmap, st) = considerSpecialization (st, n, args, dt)
|
adamc@193
|
221 in
|
adamc@193
|
222 case IM.find (cmap, pn) of
|
adamc@193
|
223 NONE => raise Fail "Specialize: Missing datatype constructor"
|
adamc@193
|
224 | SOME pn' => (ECon (dk, PConVar pn', [], eo), st)
|
adamc@193
|
225 end)
|
adamc@193
|
226 | ECase (e, pes, r) =>
|
adamc@193
|
227 let
|
adamc@193
|
228 val (pes, st) = ListUtil.foldlMap (fn ((p, e), st) =>
|
adamc@193
|
229 let
|
adamc@193
|
230 val (p, st) = pat (p, st)
|
adamc@193
|
231 in
|
adamc@193
|
232 ((p, e), st)
|
adamc@193
|
233 end) st pes
|
adamc@193
|
234 in
|
adamc@193
|
235 (ECase (e, pes, r), st)
|
adamc@193
|
236 end
|
adamc@193
|
237 | _ => (e, st)
|
adamc@193
|
238
|
adamc@193
|
239 fun decl (d, st) = (d, st)
|
adamc@193
|
240
|
adamc@193
|
241 val specDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl}
|
adamc@193
|
242
|
adamc@193
|
243 fun specialize file =
|
adamc@193
|
244 let
|
adamc@792
|
245 fun doDecl (d, st) =
|
adamc@194
|
246 let
|
adamc@194
|
247 (*val () = Print.preface ("decl:", CorePrint.p_decl CoreEnv.empty all)*)
|
adamc@792
|
248 val (d, st) = specDecl st d
|
adamc@846
|
249
|
adamc@846
|
250 val ds =
|
adamc@846
|
251 case #decls st of
|
adamc@846
|
252 [] => []
|
adamc@846
|
253 | dts => [(DDatatype dts, #2 d)]
|
adamc@194
|
254 in
|
adamc@792
|
255 case #1 d of
|
adamc@846
|
256 DDatatype dts =>
|
adamc@846
|
257 (rev (d :: ds),
|
adamc@792
|
258 {count = #count st,
|
adamc@846
|
259 datatypes = foldl (fn ((x, n, xs, xnts), dts) =>
|
adamc@846
|
260 IM.insert (dts, n,
|
adamc@846
|
261 {name = x,
|
adamc@846
|
262 params = length xs,
|
adamc@846
|
263 constructors = xnts,
|
adamc@846
|
264 specializations = CM.empty}))
|
adamc@846
|
265 (#datatypes st) dts,
|
adamc@846
|
266 constructors = foldl (fn ((x, n, xs, xnts), cs) =>
|
adamc@846
|
267 foldl (fn ((_, n', _), constructors) =>
|
adamc@846
|
268 IM.insert (constructors, n', n))
|
adamc@846
|
269 cs xnts)
|
adamc@846
|
270 (#constructors st) dts,
|
adamc@792
|
271 decls = []})
|
adamc@194
|
272 | _ =>
|
adamc@846
|
273 (rev (d :: ds),
|
adamc@792
|
274 {count = #count st,
|
adamc@792
|
275 datatypes = #datatypes st,
|
adamc@792
|
276 constructors = #constructors st,
|
adamc@792
|
277 decls = []})
|
adamc@194
|
278 end
|
adamc@193
|
279
|
adamc@193
|
280 val (ds, _) = ListUtil.foldlMapConcat doDecl
|
adamc@193
|
281 {count = U.File.maxName file + 1,
|
adamc@193
|
282 datatypes = IM.empty,
|
adamc@193
|
283 constructors = IM.empty,
|
adamc@193
|
284 decls = []} file
|
adamc@193
|
285 in
|
adamc@193
|
286 ds
|
adamc@193
|
287 end
|
adamc@193
|
288
|
adamc@193
|
289
|
adamc@193
|
290 end
|