Mercurial > urweb

comparison src/specialize.sml @ 193:8a70e2919e86

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