Mercurial > urweb

comparison src/unnest.sml @ 448:85819353a84f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
First Unnest tests working
author Adam Chlipala <adamc@hcoop.net>
date Sat, 01 Nov 2008 15:58:55 -0400
parents
children 07f6576aeb0a
comparison
equal deleted inserted replaced
447:b77863cd0be2 448:85819353a84f
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 (* Remove nested function definitions *)
29
30 structure Unnest :> UNNEST = struct
31
32 open Elab
33
34 structure E = ElabEnv
35 structure U = ElabUtil
36
37 structure IS = IntBinarySet
38
39 val fvsCon = U.Con.foldB {kind = fn (_, st) => st,
40 con = fn (cb, c, cvs) =>
41 case c of
42 CRel n =>
43 if n >= cb then
44 IS.add (cvs, n - cb)
45 else
46 cvs
47 | _ => cvs,
48 bind = fn (cb, b) =>
49 case b of
50 U.Con.Rel _ => cb + 1
51 | _ => cb}
52 0 IS.empty
53
54 fun fvsExp nr = U.Exp.foldB {kind = fn (_, st) => st,
55 con = fn ((cb, eb), c, st as (cvs, evs)) =>
56 case c of
57 CRel n =>
58 if n >= cb then
59 (IS.add (cvs, n - cb), evs)
60 else
61 st
62 | _ => st,
63 exp = fn ((cb, eb), e, st as (cvs, evs)) =>
64 case e of
65 ERel n =>
66 if n >= eb then
67 (cvs, IS.add (evs, n - eb))
68 else
69 st
70 | _ => st,
71 bind = fn (ctx as (cb, eb), b) =>
72 case b of
73 U.Exp.RelC _ => (cb + 1, eb)
74 | U.Exp.RelE _ => (cb, eb + 1)
75 | _ => ctx}
76 (0, nr) (IS.empty, IS.empty)
77
78 fun positionOf (x : int) ls =
79 let
80 fun po n ls =
81 case ls of
82 [] => raise Fail "Unnest.positionOf"
83 | x' :: ls' =>
84 if x' = x then
85 n
86 else
87 po (n + 1) ls'
88 in
89 po 0 ls
90 handle Fail _ => raise Fail ("Unnset.positionOf("
91 ^ Int.toString x
92 ^ ", "
93 ^ String.concatWith ";" (map Int.toString ls)
94 ^ ")")
95 end
96
97 fun squishCon cfv =
98 U.Con.mapB {kind = fn k => k,
99 con = fn cb => fn c =>
100 case c of
101 CRel n =>
102 if n >= cb then
103 CRel (positionOf (n - cb) cfv + cb)
104 else
105 c
106 | _ => c,
107 bind = fn (cb, b) =>
108 case b of
109 U.Con.Rel _ => cb + 1
110 | _ => cb}
111 0
112
113 fun squishExp (nr, cfv, efv) =
114 U.Exp.mapB {kind = fn k => k,
115 con = fn (cb, eb) => fn c =>
116 case c of
117 CRel n =>
118 if n >= cb then
119 CRel (positionOf (n - cb) cfv + cb)
120 else
121 c
122 | _ => c,
123 exp = fn (cb, eb) => fn e =>
124 case e of
125 ERel n =>
126 if n >= eb then
127 ERel (positionOf (n - eb) efv + eb)
128 else
129 e
130 | _ => e,
131 bind = fn (ctx as (cb, eb), b) =>
132 case b of
133 U.Exp.RelC _ => (cb + 1, eb)
134 | U.Exp.RelE _ => (cb, eb + 1)
135 | _ => ctx}
136 (0, nr)
137
138 type state = {
139 maxName : int,
140 decls : decl list
141 }
142
143 fun kind (k, st) = (k, st)
144
145 fun exp ((ks, ts), e, st : state) =
146 case e of
147 ELet (eds, e) =>
148 let
149 val doSubst = foldl (fn (p, e) => E.subExpInExp p e)
150
151 val (eds, (maxName, ds, subs)) =
152 ListUtil.foldlMapConcat
153 (fn (ed, (maxName, ds, subs)) =>
154 case #1 ed of
155 EDVal _ => ([ed], (maxName, ds, map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs))
156 | EDValRec vis =>
157 let
158 val loc = #2 ed
159
160 val nr = length vis
161 val (cfv, efv) = foldl (fn ((_, t, e), (cfv, efv)) =>
162 let
163 val (cfv', efv') = fvsExp nr e
164 (*val () = Print.prefaces "fvsExp"
165 [("e", ElabPrint.p_exp E.empty e),
166 ("cfv", Print.PD.string
167 (Int.toString (IS.numItems cfv'))),
168 ("efv", Print.PD.string
169 (Int.toString (IS.numItems efv')))]*)
170 val cfv'' = fvsCon t
171 in
172 (IS.union (cfv, IS.union (cfv', cfv'')),
173 IS.union (efv, efv'))
174 end)
175 (IS.empty, IS.empty) vis
176
177 (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n")*)
178 val cfv = IS.foldl (fn (x, cfv) =>
179 let
180 (*val () = print (Int.toString x ^ "\n")*)
181 val (_, t) = List.nth (ts, x)
182 in
183 IS.union (cfv, fvsCon t)
184 end)
185 cfv efv
186 (*val () = print "B\n"*)
187
188 val (vis, maxName) =
189 ListUtil.foldlMap (fn ((x, t, e), maxName) =>
190 ((x, maxName, t, e),
191 maxName + 1))
192 maxName vis
193
194 fun apply e =
195 let
196 val e = IS.foldl (fn (x, e) =>
197 (ECApp (e, (CRel x, loc)), loc))
198 e cfv
199 in
200 IS.foldl (fn (x, e) =>
201 (EApp (e, (ERel x, loc)), loc))
202 e efv
203 end
204
205 val subs = map (fn (n, e) => (n + nr, E.liftExpInExp nr e)) subs
206
207 val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) =>
208 let
209 val e = apply (ENamed n, loc)
210 in
211 (0, E.liftExpInExp (nr - i - 1) e)
212 end)
213 vis
214 val subs' = rev subs'
215
216 val cfv = IS.listItems cfv
217 val efv = IS.listItems efv
218 val efn = length efv
219
220 (*val subsInner = subs
221 @ map (fn (i, e) =>
222 (i + efn,
223 E.liftExpInExp efn e)) subs'*)
224
225 val subs = subs @ subs'
226
227 val vis = map (fn (x, n, t, e) =>
228 let
229 (*val () = Print.prefaces "preSubst"
230 [("e", ElabPrint.p_exp E.empty e)]*)
231 val e = doSubst e subs(*Inner*)
232
233 (*val () = Print.prefaces "squishCon"
234 [("t", ElabPrint.p_con E.empty t)]*)
235 val t = squishCon cfv t
236 (*val () = Print.prefaces "squishExp"
237 [("e", ElabPrint.p_exp E.empty e)]*)
238 val e = squishExp (nr, cfv, efv) e
239
240 val (e, t) = foldr (fn (ex, (e, t)) =>
241 let
242 val (name, t') = List.nth (ts, ex)
243 in
244 ((EAbs (name,
245 t',
246 t,
247 e), loc),
248 (TFun (t',
249 t), loc))
250 end)
251 (e, t) efv
252
253 val (e, t) = foldr (fn (cx, (e, t)) =>
254 let
255 val (name, k) = List.nth (ks, cx)
256 in
257 ((ECAbs (Explicit,
258 name,
259 k,
260 e), loc),
261 (TCFun (Explicit,
262 name,
263 k,
264 t), loc))
265 end)
266 (e, t) cfv
267 in
268 (x, n, t, e)
269 end)
270 vis
271
272 val d = (DValRec vis, #2 ed)
273 in
274 ([], (maxName, d :: ds, subs))
275 end)
276 (#maxName st, #decls st, []) eds
277 in
278 (ELet (eds, doSubst e subs),
279 {maxName = maxName,
280 decls = ds})
281 end
282
283 | _ => (e, st)
284
285 fun default (ctx, d, st) = (d, st)
286
287 fun bind ((ks, ts), b) =
288 case b of
289 U.Decl.RelC p => (p :: ks, map (fn (name, t) => (name, E.liftConInCon 0 t)) ts)
290 | U.Decl.RelE p => (ks, p :: ts)
291 | _ => (ks, ts)
292
293 val unnestDecl = U.Decl.foldMapB {kind = kind,
294 con = default,
295 exp = exp,
296 sgn_item = default,
297 sgn = default,
298 str = default,
299 decl = default,
300 bind = bind}
301 ([], [])
302
303 fun unnest file =
304 let
305 fun doDecl (all as (d, loc), st : state) =
306 let
307 fun default () = ([all], st)
308 fun explore () =
309 let
310 val (d, st) = unnestDecl st all
311 in
312 (rev (d :: #decls st),
313 {maxName = #maxName st,
314 decls = []})
315 end
316 in
317 case d of
318 DCon _ => default ()
319 | DDatatype _ => default ()
320 | DDatatypeImp _ => default ()
321 | DVal _ => explore ()
322 | DValRec _ => explore ()
323 | DSgn _ => default ()
324 | DStr (x, n, sgn, str) =>
325 let
326 val (str, st) = doStr (str, st)
327 in
328 ([(DStr (x, n, sgn, str), loc)], st)
329 end
330 | DFfiStr _ => default ()
331 | DConstraint _ => default ()
332 | DExport _ => default ()
333 | DTable _ => default ()
334 | DSequence _ => default ()
335 | DClass _ => default ()
336 | DDatabase _ => default ()
337 end
338
339 and doStr (all as (str, loc), st) =
340 let
341 fun default () = (all, st)
342 in
343 case str of
344 StrConst ds =>
345 let
346 val (ds, st) = ListUtil.foldlMapConcat doDecl st ds
347 in
348 ((StrConst ds, loc), st)
349 end
350 | StrVar _ => default ()
351 | StrProj _ => default ()
352 | StrFun (x, n, dom, ran, str) =>
353 let
354 val (str, st) = doStr (str, st)
355 in
356 ((StrFun (x, n, dom, ran, str), loc), st)
357 end
358 | StrApp _ => default ()
359 | StrError => raise Fail "Unnest: StrError"
360 end
361
362 val (ds, _) = ListUtil.foldlMapConcat doDecl
363 {maxName = U.File.maxName file + 1,
364 decls = []} file
365 in
366 ds
367 end
368
369 end