adamc@1272
|
1 (* Copyright (c) 2008-2010, Adam Chlipala
|
adamc@448
|
2 * All rights reserved.
|
adamc@448
|
3 *
|
adamc@448
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@448
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@448
|
6 *
|
adamc@448
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@448
|
8 * this list of conditions and the following disclaimer.
|
adamc@448
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@448
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@448
|
11 * and/or other materials provided with the distribution.
|
adamc@448
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@448
|
13 * derived from this software without specific prior written permission.
|
adamc@448
|
14 *
|
adamc@448
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@448
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@448
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@448
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@448
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@448
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@448
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@448
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@448
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@448
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@448
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@448
|
26 *)
|
adamc@448
|
27
|
adamc@448
|
28 (* Remove nested function definitions *)
|
adamc@448
|
29
|
adamc@448
|
30 structure Unnest :> UNNEST = struct
|
adamc@448
|
31
|
adamc@448
|
32 open Elab
|
adamc@448
|
33
|
adamc@448
|
34 structure E = ElabEnv
|
adamc@448
|
35 structure U = ElabUtil
|
adamc@448
|
36
|
adamc@448
|
37 structure IS = IntBinarySet
|
adamc@448
|
38
|
adamc@487
|
39 fun liftExpInExp by =
|
adamc@623
|
40 U.Exp.mapB {kind = fn _ => fn k => k,
|
adamc@487
|
41 con = fn _ => fn c => c,
|
adamc@487
|
42 exp = fn bound => fn e =>
|
adamc@487
|
43 case e of
|
adamc@487
|
44 ERel xn =>
|
adamc@487
|
45 if xn < bound then
|
adamc@487
|
46 e
|
adamc@487
|
47 else
|
adamc@487
|
48 ERel (xn + by)
|
adamc@487
|
49 | _ => e,
|
adamc@487
|
50 bind = fn (bound, U.Exp.RelE _) => bound + 1
|
adamc@487
|
51 | (bound, _) => bound}
|
adamc@487
|
52
|
adamc@487
|
53 val subExpInExp =
|
adamc@623
|
54 U.Exp.mapB {kind = fn _ => fn k => k,
|
adamc@487
|
55 con = fn _ => fn c => c,
|
adamc@487
|
56 exp = fn (xn, rep) => fn e =>
|
adamc@487
|
57 case e of
|
adamc@487
|
58 ERel xn' =>
|
adamc@487
|
59 if xn' = xn then
|
adamc@487
|
60 #1 rep
|
adamc@487
|
61 else
|
adamc@487
|
62 e
|
adamc@487
|
63 | _ => e,
|
adamc@487
|
64 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, E.liftExpInExp 0 rep)
|
adamc@487
|
65 | ((xn, rep), U.Exp.RelC _) => (xn, E.liftConInExp 0 rep)
|
adamc@487
|
66 | (ctx, _) => ctx}
|
adamc@487
|
67
|
adamc@623
|
68 val fvsCon = U.Con.foldB {kind = fn (_, _, st) => st,
|
adamc@448
|
69 con = fn (cb, c, cvs) =>
|
adamc@448
|
70 case c of
|
adamc@448
|
71 CRel n =>
|
adamc@448
|
72 if n >= cb then
|
adamc@448
|
73 IS.add (cvs, n - cb)
|
adamc@448
|
74 else
|
adamc@448
|
75 cvs
|
adamc@448
|
76 | _ => cvs,
|
adamc@448
|
77 bind = fn (cb, b) =>
|
adamc@448
|
78 case b of
|
adamc@623
|
79 U.Con.RelC _ => cb + 1
|
adamc@448
|
80 | _ => cb}
|
adamc@448
|
81 0 IS.empty
|
adamc@448
|
82
|
adamc@623
|
83 fun fvsExp nr = U.Exp.foldB {kind = fn (_, _, st) => st,
|
adamc@448
|
84 con = fn ((cb, eb), c, st as (cvs, evs)) =>
|
adamc@448
|
85 case c of
|
adamc@448
|
86 CRel n =>
|
adamc@448
|
87 if n >= cb then
|
adamc@448
|
88 (IS.add (cvs, n - cb), evs)
|
adamc@448
|
89 else
|
adamc@448
|
90 st
|
adamc@448
|
91 | _ => st,
|
adamc@448
|
92 exp = fn ((cb, eb), e, st as (cvs, evs)) =>
|
adamc@448
|
93 case e of
|
adamc@448
|
94 ERel n =>
|
adamc@448
|
95 if n >= eb then
|
adamc@448
|
96 (cvs, IS.add (evs, n - eb))
|
adamc@448
|
97 else
|
adamc@448
|
98 st
|
adamc@448
|
99 | _ => st,
|
adamc@448
|
100 bind = fn (ctx as (cb, eb), b) =>
|
adamc@448
|
101 case b of
|
adamc@448
|
102 U.Exp.RelC _ => (cb + 1, eb)
|
adamc@448
|
103 | U.Exp.RelE _ => (cb, eb + 1)
|
adamc@448
|
104 | _ => ctx}
|
adamc@448
|
105 (0, nr) (IS.empty, IS.empty)
|
adamc@448
|
106
|
adamc@448
|
107 fun positionOf (x : int) ls =
|
adamc@448
|
108 let
|
adamc@448
|
109 fun po n ls =
|
adamc@448
|
110 case ls of
|
adamc@448
|
111 [] => raise Fail "Unnest.positionOf"
|
adamc@448
|
112 | x' :: ls' =>
|
adamc@448
|
113 if x' = x then
|
adamc@448
|
114 n
|
adamc@448
|
115 else
|
adamc@448
|
116 po (n + 1) ls'
|
adamc@448
|
117 in
|
adamc@448
|
118 po 0 ls
|
adamc@487
|
119 handle Fail _ => raise Fail ("Unnest.positionOf("
|
adamc@448
|
120 ^ Int.toString x
|
adamc@448
|
121 ^ ", "
|
adamc@448
|
122 ^ String.concatWith ";" (map Int.toString ls)
|
adamc@448
|
123 ^ ")")
|
adamc@448
|
124 end
|
adamc@448
|
125
|
adamc@448
|
126 fun squishCon cfv =
|
adamc@623
|
127 U.Con.mapB {kind = fn _ => fn k => k,
|
adamc@448
|
128 con = fn cb => fn c =>
|
adamc@448
|
129 case c of
|
adamc@448
|
130 CRel n =>
|
adamc@448
|
131 if n >= cb then
|
adamc@448
|
132 CRel (positionOf (n - cb) cfv + cb)
|
adamc@448
|
133 else
|
adamc@448
|
134 c
|
adamc@448
|
135 | _ => c,
|
adamc@448
|
136 bind = fn (cb, b) =>
|
adamc@448
|
137 case b of
|
adamc@623
|
138 U.Con.RelC _ => cb + 1
|
adamc@448
|
139 | _ => cb}
|
adamc@448
|
140 0
|
adamc@448
|
141
|
adamc@448
|
142 fun squishExp (nr, cfv, efv) =
|
adamc@623
|
143 U.Exp.mapB {kind = fn _ => fn k => k,
|
adamc@448
|
144 con = fn (cb, eb) => fn c =>
|
adamc@448
|
145 case c of
|
adamc@448
|
146 CRel n =>
|
adamc@448
|
147 if n >= cb then
|
adamc@448
|
148 CRel (positionOf (n - cb) cfv + cb)
|
adamc@448
|
149 else
|
adamc@448
|
150 c
|
adamc@448
|
151 | _ => c,
|
adamc@448
|
152 exp = fn (cb, eb) => fn e =>
|
adamc@448
|
153 case e of
|
adamc@448
|
154 ERel n =>
|
adamc@448
|
155 if n >= eb then
|
adamc@487
|
156 ERel (positionOf (n - eb) efv + eb - nr)
|
adamc@448
|
157 else
|
adamc@448
|
158 e
|
adamc@448
|
159 | _ => e,
|
adamc@448
|
160 bind = fn (ctx as (cb, eb), b) =>
|
adamc@448
|
161 case b of
|
adamc@448
|
162 U.Exp.RelC _ => (cb + 1, eb)
|
adamc@448
|
163 | U.Exp.RelE _ => (cb, eb + 1)
|
adamc@448
|
164 | _ => ctx}
|
adamc@448
|
165 (0, nr)
|
adamc@448
|
166
|
adamc@448
|
167 type state = {
|
adamc@448
|
168 maxName : int,
|
adamc@455
|
169 decls : (string * int * con * exp) list
|
adamc@448
|
170 }
|
adamc@448
|
171
|
adamc@623
|
172 fun kind (_, k, st) = (k, st)
|
adamc@448
|
173
|
adam@1888
|
174 val basis = ref 0
|
adam@1888
|
175
|
adamc@453
|
176 fun exp ((ks, ts), e as old, st : state) =
|
adamc@448
|
177 case e of
|
adamc@825
|
178 ELet (eds, e, t) =>
|
adamc@448
|
179 let
|
adamc@487
|
180 (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*)
|
adamc@453
|
181
|
adamc@487
|
182 fun doSubst' (e, subs) = foldl (fn (p, e) => subExpInExp p e) e subs
|
adamc@448
|
183
|
adamc@487
|
184 fun doSubst (e, subs, by) =
|
adamc@487
|
185 let
|
adamc@487
|
186 val e = doSubst' (e, subs)
|
adamc@487
|
187 in
|
adamc@487
|
188 liftExpInExp (~by) (length subs) e
|
adamc@487
|
189 end
|
adamc@487
|
190
|
adam@1888
|
191 fun functionInside (t : con) =
|
adam@1888
|
192 case #1 t of
|
adam@1888
|
193 TFun _ => true
|
adam@1888
|
194 | CApp ((CModProj (basis', [], "transaction"), _), _) => basis' = !basis
|
adam@1888
|
195 | _ => false
|
adam@1888
|
196
|
adam@1888
|
197 val eds = map (fn ed =>
|
adam@1888
|
198 case #1 ed of
|
adam@1888
|
199 EDVal ((PVar (x, _), _), t, e) =>
|
adam@1888
|
200 if functionInside t then
|
adam@1888
|
201 (EDValRec [(x, t, E.liftExpInExp 0 e)], #2 ed)
|
adam@1888
|
202 else
|
adam@1888
|
203 ed
|
adam@1888
|
204 | _ => ed) eds
|
adam@1888
|
205
|
adamc@487
|
206 val (eds, (ts, maxName, ds, subs, by)) =
|
adamc@448
|
207 ListUtil.foldlMapConcat
|
adamc@487
|
208 (fn (ed, (ts, maxName, ds, subs, by)) =>
|
adamc@448
|
209 case #1 ed of
|
adamc@825
|
210 EDVal (p, t, e) =>
|
adamc@487
|
211 let
|
adamc@487
|
212 val e = doSubst (e, subs, by)
|
adamc@825
|
213
|
adamc@825
|
214 fun doVars ((p, _), ts) =
|
adamc@825
|
215 case p of
|
adamc@825
|
216 PWild => ts
|
adamc@825
|
217 | PVar xt => xt :: ts
|
adamc@825
|
218 | PPrim _ => ts
|
adamc@825
|
219 | PCon (_, _, _, NONE) => ts
|
adamc@825
|
220 | PCon (_, _, _, SOME p) => doVars (p, ts)
|
adamc@825
|
221 | PRecord xpcs =>
|
adamc@825
|
222 foldl (fn ((_, p, _), ts) => doVars (p, ts))
|
adamc@825
|
223 ts xpcs
|
adamc@1272
|
224
|
adamc@1272
|
225 fun bindOne subs = ((0, (ERel 0, #2 ed))
|
adamc@1272
|
226 :: map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs)
|
adamc@1272
|
227
|
adamc@1272
|
228 fun bindMany (n, subs) =
|
adamc@1272
|
229 case n of
|
adamc@1272
|
230 0 => subs
|
adamc@1272
|
231 | _ => bindMany (n - 1, bindOne subs)
|
adamc@487
|
232 in
|
adamc@825
|
233 ([(EDVal (p, t, e), #2 ed)],
|
adamc@825
|
234 (doVars (p, ts),
|
adamc@487
|
235 maxName, ds,
|
adamc@1272
|
236 bindMany (E.patBindsN p, subs),
|
adamc@487
|
237 by))
|
adamc@487
|
238 end
|
adamc@448
|
239 | EDValRec vis =>
|
adamc@448
|
240 let
|
adamc@448
|
241 val loc = #2 ed
|
adamc@448
|
242
|
adamc@448
|
243 val nr = length vis
|
adamc@490
|
244 val subsLocal = List.filter (fn (_, (ERel _, _)) => false
|
adamc@490
|
245 | _ => true) subs
|
adamc@490
|
246 val subsLocal = map (fn (n, e) => (n + nr, liftExpInExp nr 0 e))
|
adamc@490
|
247 subsLocal
|
adamc@490
|
248
|
adamc@490
|
249 val vis = map (fn (x, t, e) =>
|
adamc@490
|
250 (x, t, doSubst' (e, subsLocal))) vis
|
adamc@490
|
251
|
adamc@448
|
252 val (cfv, efv) = foldl (fn ((_, t, e), (cfv, efv)) =>
|
adamc@448
|
253 let
|
adamc@448
|
254 val (cfv', efv') = fvsExp nr e
|
adamc@448
|
255 (*val () = Print.prefaces "fvsExp"
|
adamc@448
|
256 [("e", ElabPrint.p_exp E.empty e),
|
adamc@448
|
257 ("cfv", Print.PD.string
|
adamc@448
|
258 (Int.toString (IS.numItems cfv'))),
|
adamc@448
|
259 ("efv", Print.PD.string
|
adamc@448
|
260 (Int.toString (IS.numItems efv')))]*)
|
adamc@448
|
261 val cfv'' = fvsCon t
|
adamc@448
|
262 in
|
adamc@448
|
263 (IS.union (cfv, IS.union (cfv', cfv'')),
|
adamc@448
|
264 IS.union (efv, efv'))
|
adamc@448
|
265 end)
|
adamc@448
|
266 (IS.empty, IS.empty) vis
|
adamc@448
|
267
|
adamc@826
|
268 (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*)
|
adamc@826
|
269 (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n")*)
|
adamc@826
|
270 (*val () = app (fn (x, t) =>
|
adamc@453
|
271 Print.prefaces "Var" [("x", Print.PD.string x),
|
adamc@826
|
272 ("t", ElabPrint.p_con E.empty t)]) ts
|
adamc@826
|
273 val () = IS.app (fn n => print ("Free: " ^ Int.toString n ^ "\n")) efv*)
|
adamc@487
|
274
|
adamc@448
|
275 val cfv = IS.foldl (fn (x, cfv) =>
|
adamc@448
|
276 let
|
adamc@448
|
277 (*val () = print (Int.toString x ^ "\n")*)
|
adamc@448
|
278 val (_, t) = List.nth (ts, x)
|
adamc@448
|
279 in
|
adamc@448
|
280 IS.union (cfv, fvsCon t)
|
adamc@448
|
281 end)
|
adamc@448
|
282 cfv efv
|
adamc@448
|
283 (*val () = print "B\n"*)
|
adamc@448
|
284
|
adamc@448
|
285 val (vis, maxName) =
|
adamc@448
|
286 ListUtil.foldlMap (fn ((x, t, e), maxName) =>
|
adamc@448
|
287 ((x, maxName, t, e),
|
adamc@448
|
288 maxName + 1))
|
adamc@448
|
289 maxName vis
|
adamc@448
|
290
|
adamc@487
|
291 val subs = map (fn (n, e) => (n + nr,
|
adamc@487
|
292 case e of
|
adamc@487
|
293 (ERel _, _) => e
|
adamc@487
|
294 | _ => liftExpInExp nr 0 e))
|
adamc@487
|
295 subs
|
adamc@487
|
296
|
adamc@448
|
297 val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) =>
|
adamc@448
|
298 let
|
adamc@487
|
299 val e = (ENamed n, loc)
|
adamc@487
|
300
|
adamc@487
|
301 val e = IS.foldr (fn (x, e) =>
|
adamc@487
|
302 (ECApp (e, (CRel x, loc)), loc))
|
adamc@487
|
303 e cfv
|
adamc@487
|
304
|
adamc@487
|
305 val e = IS.foldr (fn (x, e) =>
|
adamc@487
|
306 (EApp (e, (ERel (nr + x), loc)),
|
adamc@487
|
307 loc))
|
adamc@487
|
308 e efv
|
adamc@448
|
309 in
|
adamc@487
|
310 (nr - i - 1, e)
|
adamc@448
|
311 end)
|
adamc@450
|
312 vis
|
adamc@450
|
313
|
adamc@448
|
314 val cfv = IS.listItems cfv
|
adamc@448
|
315 val efv = IS.listItems efv
|
adamc@448
|
316
|
adamc@487
|
317 val subs = subs' @ subs
|
adamc@448
|
318
|
adamc@448
|
319 val vis = map (fn (x, n, t, e) =>
|
adamc@448
|
320 let
|
adamc@448
|
321 (*val () = Print.prefaces "preSubst"
|
adamc@448
|
322 [("e", ElabPrint.p_exp E.empty e)]*)
|
adamc@490
|
323 val e = doSubst' (e, subs')
|
adamc@448
|
324
|
adamc@448
|
325 (*val () = Print.prefaces "squishCon"
|
adamc@448
|
326 [("t", ElabPrint.p_con E.empty t)]*)
|
adamc@448
|
327 val t = squishCon cfv t
|
adamc@448
|
328 (*val () = Print.prefaces "squishExp"
|
adamc@448
|
329 [("e", ElabPrint.p_exp E.empty e)]*)
|
adamc@487
|
330 val e = squishExp (nr, cfv, efv) e
|
adamc@448
|
331
|
adamc@487
|
332 (*val () = print ("Avail: " ^ Int.toString (length ts) ^ "\n")*)
|
adamc@453
|
333 val (e, t) = foldl (fn (ex, (e, t)) =>
|
adamc@448
|
334 let
|
adamc@487
|
335 (*val () = print (Int.toString ex ^ "\n")*)
|
adamc@448
|
336 val (name, t') = List.nth (ts, ex)
|
adamc@1272
|
337 val t' = squishCon cfv t'
|
adamc@448
|
338 in
|
adamc@448
|
339 ((EAbs (name,
|
adamc@448
|
340 t',
|
adamc@448
|
341 t,
|
adamc@448
|
342 e), loc),
|
adamc@448
|
343 (TFun (t',
|
adamc@448
|
344 t), loc))
|
adamc@448
|
345 end)
|
adamc@448
|
346 (e, t) efv
|
adamc@487
|
347 (*val () = print "Done\n"*)
|
adamc@448
|
348
|
adamc@453
|
349 val (e, t) = foldl (fn (cx, (e, t)) =>
|
adamc@448
|
350 let
|
adamc@448
|
351 val (name, k) = List.nth (ks, cx)
|
adamc@448
|
352 in
|
adamc@448
|
353 ((ECAbs (Explicit,
|
adamc@448
|
354 name,
|
adamc@448
|
355 k,
|
adamc@448
|
356 e), loc),
|
adamc@448
|
357 (TCFun (Explicit,
|
adamc@448
|
358 name,
|
adamc@448
|
359 k,
|
adamc@448
|
360 t), loc))
|
adamc@448
|
361 end)
|
adamc@448
|
362 (e, t) cfv
|
adamc@448
|
363 in
|
adamc@487
|
364 (*Print.prefaces "Have a vi"
|
adamc@487
|
365 [("x", Print.PD.string x),
|
adamc@487
|
366 ("e", ElabPrint.p_exp ElabEnv.empty e)];*)
|
adamc@1017
|
367 ("$" ^ x, n, t, e)
|
adamc@448
|
368 end)
|
adamc@448
|
369 vis
|
adamc@448
|
370
|
adamc@487
|
371 val ts = List.revAppend (map (fn (x, _, t, _) => (x, t)) vis, ts)
|
adamc@448
|
372 in
|
adamc@487
|
373 ([], (ts, maxName, vis @ ds, subs, by + nr))
|
adamc@448
|
374 end)
|
adamc@487
|
375 (ts, #maxName st, #decls st, [], 0) eds
|
adamc@487
|
376
|
adamc@487
|
377 val e' = doSubst (e, subs, by)
|
adamc@448
|
378 in
|
adamc@487
|
379 (*Print.prefaces "Before" [("e", ElabPrint.p_exp ElabEnv.empty e),
|
adamc@487
|
380 ("se", ElabPrint.p_exp ElabEnv.empty (doSubst' (e, subs))),
|
adamc@487
|
381 ("e'", ElabPrint.p_exp ElabEnv.empty e')];*)
|
adamc@1272
|
382 (*Print.prefaces "Let" [("Before", ElabPrint.p_exp ElabEnv.empty (old, ErrorMsg.dummySpan)),
|
adamc@1272
|
383 ("After", ElabPrint.p_exp ElabEnv.empty (ELet (eds, e', t), ErrorMsg.dummySpan))];*)
|
adamc@825
|
384 (ELet (eds, e', t),
|
adamc@448
|
385 {maxName = maxName,
|
adamc@448
|
386 decls = ds})
|
adamc@487
|
387 (*(ELet (eds, doSubst (liftExpInExp (~(length subs - numRemaining)) (length subs) e) subs),*)
|
adamc@448
|
388 end
|
adamc@448
|
389
|
adamc@448
|
390 | _ => (e, st)
|
adamc@448
|
391
|
adamc@448
|
392 fun default (ctx, d, st) = (d, st)
|
adamc@448
|
393
|
adamc@448
|
394 fun bind ((ks, ts), b) =
|
adamc@448
|
395 case b of
|
adamc@448
|
396 U.Decl.RelC p => (p :: ks, map (fn (name, t) => (name, E.liftConInCon 0 t)) ts)
|
adamc@448
|
397 | U.Decl.RelE p => (ks, p :: ts)
|
adamc@448
|
398 | _ => (ks, ts)
|
adamc@448
|
399
|
adamc@448
|
400 val unnestDecl = U.Decl.foldMapB {kind = kind,
|
adamc@448
|
401 con = default,
|
adamc@448
|
402 exp = exp,
|
adamc@448
|
403 sgn_item = default,
|
adamc@448
|
404 sgn = default,
|
adamc@448
|
405 str = default,
|
adamc@448
|
406 decl = default,
|
adamc@448
|
407 bind = bind}
|
adamc@448
|
408 ([], [])
|
adamc@448
|
409
|
adamc@448
|
410 fun unnest file =
|
adamc@448
|
411 let
|
adamc@448
|
412 fun doDecl (all as (d, loc), st : state) =
|
adamc@448
|
413 let
|
adamc@448
|
414 fun default () = ([all], st)
|
adamc@448
|
415 fun explore () =
|
adamc@448
|
416 let
|
adamc@448
|
417 val (d, st) = unnestDecl st all
|
adamc@455
|
418
|
adamc@455
|
419 val ds =
|
adamc@455
|
420 case #1 d of
|
adamc@455
|
421 DValRec vis => [(DValRec (vis @ #decls st), #2 d)]
|
adamc@455
|
422 | _ => [(DValRec (#decls st), #2 d), d]
|
adamc@448
|
423 in
|
adamc@455
|
424 (ds,
|
adamc@448
|
425 {maxName = #maxName st,
|
adamc@448
|
426 decls = []})
|
adamc@448
|
427 end
|
adamc@448
|
428 in
|
adamc@448
|
429 case d of
|
adamc@448
|
430 DCon _ => default ()
|
adamc@448
|
431 | DDatatype _ => default ()
|
adamc@448
|
432 | DDatatypeImp _ => default ()
|
adamc@448
|
433 | DVal _ => explore ()
|
adamc@448
|
434 | DValRec _ => explore ()
|
adamc@448
|
435 | DSgn _ => default ()
|
adamc@448
|
436 | DStr (x, n, sgn, str) =>
|
adamc@448
|
437 let
|
adamc@448
|
438 val (str, st) = doStr (str, st)
|
adamc@448
|
439 in
|
adamc@448
|
440 ([(DStr (x, n, sgn, str), loc)], st)
|
adamc@448
|
441 end
|
adam@1888
|
442 | DFfiStr ("Basis", n, _) => (basis := n; default ())
|
adamc@448
|
443 | DFfiStr _ => default ()
|
adamc@448
|
444 | DConstraint _ => default ()
|
adamc@448
|
445 | DExport _ => default ()
|
adamc@448
|
446 | DTable _ => default ()
|
adamc@448
|
447 | DSequence _ => default ()
|
adamc@754
|
448 | DView _ => default ()
|
adamc@448
|
449 | DDatabase _ => default ()
|
adamc@459
|
450 | DCookie _ => default ()
|
adamc@718
|
451 | DStyle _ => default ()
|
adamc@1075
|
452 | DTask _ => explore ()
|
adamc@1199
|
453 | DPolicy _ => explore ()
|
adam@1294
|
454 | DOnError _ => default ()
|
adamc@448
|
455 end
|
adamc@448
|
456
|
adamc@448
|
457 and doStr (all as (str, loc), st) =
|
adamc@448
|
458 let
|
adamc@448
|
459 fun default () = (all, st)
|
adamc@448
|
460 in
|
adamc@448
|
461 case str of
|
adamc@448
|
462 StrConst ds =>
|
adamc@448
|
463 let
|
adamc@448
|
464 val (ds, st) = ListUtil.foldlMapConcat doDecl st ds
|
adamc@448
|
465 in
|
adamc@448
|
466 ((StrConst ds, loc), st)
|
adamc@448
|
467 end
|
adamc@448
|
468 | StrVar _ => default ()
|
adamc@448
|
469 | StrProj _ => default ()
|
adamc@448
|
470 | StrFun (x, n, dom, ran, str) =>
|
adamc@448
|
471 let
|
adamc@448
|
472 val (str, st) = doStr (str, st)
|
adamc@448
|
473 in
|
adamc@448
|
474 ((StrFun (x, n, dom, ran, str), loc), st)
|
adamc@448
|
475 end
|
adamc@448
|
476 | StrApp _ => default ()
|
adamc@448
|
477 | StrError => raise Fail "Unnest: StrError"
|
adamc@448
|
478 end
|
adamc@448
|
479
|
adamc@448
|
480 val (ds, _) = ListUtil.foldlMapConcat doDecl
|
adamc@448
|
481 {maxName = U.File.maxName file + 1,
|
adamc@448
|
482 decls = []} file
|
adamc@448
|
483 in
|
adamc@448
|
484 ds
|
adamc@448
|
485 end
|
adamc@448
|
486
|
adamc@448
|
487 end
|